Skip to content
Permalink
Browse files

Separate out evaluator (#210)

* Separate out evaluator.
  • Loading branch information
thealmarty committed Nov 27, 2019
1 parent 7b81fdc commit 2e8968393ead0b9d7d618f8fd6772545b995ea07
@@ -94,9 +94,16 @@ Provides a mechanism for defining Sum types
+ [[Library]]
*** Michelson
**** Optimisation
This is a simple optimization strategy which replaces sequences of Michelson instructions with equivalent sequences of fewer instructions.
At the moment nontrivial programs are unlikely to compile to the smallest equivalent Michelson instruction sequence,
but little time has been spent on optimization so far - a high degree should be possible; the Haskell typesystem provides very strong guarantees.
A more interesting / potentially more effective strategy might be to search the space of equivalent Michelson programs,
which at small program sizes using bounded heuristic search should be computationally feasible -
then choose the one with the fewest instructions (or based on some other gas-estimation preference function).
- _Relies on_
+ [[Library]]
+ [[Michelson/Compilation/Types]]
+ [[Michelson/Parameterisation]]
+ [[Library]]
**** Parameterisation <<Michelson/Parameterisation>>
- _Relies on_
+ [[Library]]
@@ -202,14 +209,26 @@ Provides a mechanism for defining Sum types
+ [[Library]]
*** Erased
- _Relies on_
+ [[Evaluator]]
+ [[Erased/Evaluator]]
+ [[Erased/Types]]
**** Evaluator
**** Evaluator <<Erased/Evaluator>>
- _Relies on_
+ [[Erased/Types]]
+ [[Library]]
**** Types <<Erased/Types>>
- _Relies on_
+ [[Usage]]
+ [[Library]]
*** ErasedAnn
- _Relies on_
+ [[ErasedAnn/Erasure]]
+ [[ErasedAnn/Types]]
**** Erasure <<ErasedAnn/Erasure>>
- _Relies on_
+ [[ErasedAnn/Types]]
**** Types <<ErasedAnn/Types>>
- _Relies on_
+ [[Usage]]
+ [[Library]]
*** Erasure <<Core/Erasure>>
- _Relies on_
@@ -233,20 +252,54 @@ Provides a mechanism for defining Sum types
+ [[Usage]]
+ [[Library]]
**** Types <<HR/Types>>
- _Relies on_
+ [[Usage]]
+ [[Library]]
*** HRAnn
- _Relies on_
+ [[HRAnn/Erasure]]
+ [[HRAnn/Types]]
**** Erasure <<HRAnn/Erasure>>
- _Relies on_
+ [[HRAnn/Types]]
**** Types <<HRAnn/Types>>
- _Relies on_
+ [[Usage]]
+ [[Library]]
*** IR
- _Relies on_
+ [[IR/Evaluator]]
+ [[Typechecker]]
+ [[IR/Types]]
**** Evaluator <<IR/Evaluator>>
This includes the evaluators (evalTerm and evalElim),
the value application function (vapp) and
the substitution functions (substTerm and substElim).
- _Relies on_
+ [[IR/Types]]
+ [[Core/Types]]
+ [[Library]]
**** Typechecker
- _Relies on_
+ [[IR/Evaluator]]
+ [[IR/Types]]
+ [[Core/Types]]
+ [[Usage]]
+ [[Library]]
**** Types <<IR/Types>>
Quantitative type implementation inspired by
Atkey 2018 and McBride 2016.
- _Relies on_
+ [[Usage]]
+ [[Library]]
*** IRAnn
- _Relies on_
+ [[IRAnn/Erasure]]
+ [[IRAnn/Types]]
**** Erasure <<IRAnn/Erasure>>
- _Relies on_
+ [[IRAnn/Types]]
**** Types <<IRAnn/Types>>
- _Relies on_
+ [[Usage]]
+ [[Library]]
@@ -29,6 +29,7 @@ Tests for the type checker and evaluator in Core/IR/Typechecker.hs
+ [[Check]]
+ [[Types]]
+ [[Types]]
+ [[Usage]]
+ [[Library]]
* Encoding
- _Relies on_
@@ -65,6 +66,7 @@ Tests for the type checker and evaluator in Core/IR/Typechecker.hs
- _Relies on_
+ [[Compilation]]
+ [[Parameterisation]]
+ [[Usage]]
+ [[Library]]
** LLVM
- _Relies on_
@@ -76,6 +78,7 @@ Tests for the type checker and evaluator in Core/IR/Typechecker.hs
+ [[Compilation]]
+ [[Optimisation]]
+ [[Parameterisation]]
+ [[Usage]]
+ [[Library]]
* Nets
** Combinators
@@ -158,6 +158,7 @@ library:
- Juvix.Core.Utility
- Juvix.Core.IR.Types
- Juvix.Core.IR.Typechecker
- Juvix.Core.IR.Evaluator
- Juvix.Core.HR.Parser
- Juvix.Core.HR.Types
- Juvix.Core.HRAnn.Types
@@ -248,7 +248,6 @@ vaList = StructureType
elementTypes = [PointerType Type.i8 (AddrSpace 32)]
}


bothPrimary Type
bothPrimary = StructureType
{ isPacked = False,
@@ -62,11 +62,11 @@ jit config mod name = do
loop = do
param readChan paramChan
case param of
Just p -> do
Just p do
res hsFunc p
writeChan resultChan res
loop
Nothing -> return ()
Nothing return ()
B.putStrLn "starting loop"
loop
Nothing return ()
@@ -1,8 +1,10 @@
module Juvix.Core.IR
( module Juvix.Core.IR.Types,
module Juvix.Core.IR.Typechecker,
module Juvix.Core.IR.Evaluator,
)
where

import Juvix.Core.IR.Evaluator
import Juvix.Core.IR.Typechecker
import Juvix.Core.IR.Types
@@ -0,0 +1,100 @@
-- |
-- This includes the evaluators (evalTerm and evalElim),
-- the value application function (vapp) and
-- the substitution functions (substTerm and substElim).
module Juvix.Core.IR.Evaluator where

import Control.Lens ((^?), ix)
import Juvix.Core.IR.Types
import Juvix.Core.Types
import Juvix.Library hiding (show)

-- evaluation of checkable terms
evalTerm
primTy primVal m.
( HasThrow "typecheckError" (TypecheckError primTy primVal m) m,
Show primTy,
Show primVal
)
Parameterisation primTy primVal
Term primTy primVal
Env primTy primVal m
m (Value primTy primVal m)
evalTerm _ (Star i) _d = pure (VStar i)
evalTerm _ (PrimTy p) _d = pure (VPrimTy p)
evalTerm param (Pi pi ty ty') d = do
ty evalTerm param ty d
pure (VPi pi ty (\x evalTerm param ty' (x : d)))
evalTerm param (Lam e) d = pure (VLam (\x evalTerm param e (x : d)))
evalTerm param (Elim ii) d = evalElim param ii d

toInt Natural Int
toInt = fromInteger . toInteger

-- evaluation of inferable terms
evalElim
primTy primVal m.
( HasThrow "typecheckError" (TypecheckError primTy primVal m) m,
Show primTy,
Show primVal
)
Parameterisation primTy primVal
Elim primTy primVal
Env primTy primVal m
m (Value primTy primVal m)
evalElim _ (Free x) _d = pure (vfree x)
evalElim _ (Prim p) _d = pure (VPrim p)
evalElim param (App elim term) d = do
elim evalElim param elim d
term evalTerm param term d
vapp param elim term
evalElim param (Ann _pi term _type) d = evalTerm param term d
evalElim _ (Bound ii) d =
fromMaybe (throw @"typecheckError" (UnboundIndex ii)) (pure |<< (d ^? ix (toInt ii)))

-- value application function
vapp
primTy primVal m.
( HasThrow "typecheckError" (TypecheckError primTy primVal m) m,
Show primTy,
Show primVal
)
Parameterisation primTy primVal
Value primTy primVal m
Value primTy primVal m
m (Value primTy primVal m)
vapp _ (VLam f) v = f v
vapp _ (VNeutral n) v = pure (VNeutral (NApp n v))
vapp param (VPrim x) (VPrim y) =
case Juvix.Core.Types.apply param x y of
Just v pure (VPrim v)
Nothing throw @"typecheckError" (CannotApply (VPrim x) (VPrim y))
vapp _ f x = throw @"typecheckError" (CannotApply f x)

-- substitution function for checkable terms
substTerm
(Show primTy, Show primVal)
Natural
Elim primTy primVal
Term primTy primVal
Term primTy primVal
substTerm _ii _r (Star i) = Star i
substTerm _ii _r (PrimTy p) = PrimTy p
substTerm ii r (Pi pi ty ty') = Pi pi (substTerm ii r ty) (substTerm (ii + 1) r ty')
substTerm ii r (Lam f) = Lam (substTerm (ii + 1) r f)
substTerm ii r (Elim e) = Elim (substElim ii r e)

-- substitution function for inferable terms
substElim
(Show primTy, Show primVal)
Natural
Elim primTy primVal
Elim primTy primVal
Elim primTy primVal
substElim ii r (Bound j)
| ii == j = r
| otherwise = Bound j
substElim _ii _r (Free y) = Free y
substElim _ii _r (Prim p) = Prim p
substElim ii r (App it ct) = App (substElim ii r it) (substTerm ii r ct)
substElim ii r (Ann pi term t) = Ann pi (substTerm ii r term) (substTerm ii r t)
@@ -1,102 +1,12 @@
module Juvix.Core.IR.Typechecker where

import Control.Lens ((^?), ix)
import Juvix.Core.IR.Evaluator
import Juvix.Core.IR.Types
import Juvix.Core.Types
import Juvix.Core.Usage
import Juvix.Library hiding (show)
import Prelude (lookup)

-- evaluation of checkable terms
evalTerm
primTy primVal m.
( HasThrow "typecheckError" (TypecheckError primTy primVal m) m,
Show primTy,
Show primVal
)
Parameterisation primTy primVal
Term primTy primVal
Env primTy primVal m
m (Value primTy primVal m)
evalTerm _ (Star i) _d = pure (VStar i)
evalTerm _ (PrimTy p) _d = pure (VPrimTy p)
evalTerm param (Pi pi ty ty') d = do
ty evalTerm param ty d
pure (VPi pi ty (\x evalTerm param ty' (x : d)))
evalTerm param (Lam e) d = pure (VLam (\x evalTerm param e (x : d)))
evalTerm param (Elim ii) d = evalElim param ii d

toInt Natural Int
toInt = fromInteger . toInteger

-- evaluation of inferable terms
evalElim
primTy primVal m.
( HasThrow "typecheckError" (TypecheckError primTy primVal m) m,
Show primTy,
Show primVal
)
Parameterisation primTy primVal
Elim primTy primVal
Env primTy primVal m
m (Value primTy primVal m)
evalElim _ (Free x) _d = pure (vfree x)
evalElim _ (Prim p) _d = pure (VPrim p)
evalElim param (App elim term) d = do
elim evalElim param elim d
term evalTerm param term d
vapp param elim term
evalElim param (Ann _pi term _type) d = evalTerm param term d
evalElim _ (Bound ii) d =
fromMaybe (throw @"typecheckError" (UnboundIndex ii)) (pure |<< (d ^? ix (toInt ii)))

-- value application function
vapp
primTy primVal m.
( HasThrow "typecheckError" (TypecheckError primTy primVal m) m,
Show primTy,
Show primVal
)
Parameterisation primTy primVal
Value primTy primVal m
Value primTy primVal m
m (Value primTy primVal m)
vapp _ (VLam f) v = f v
vapp _ (VNeutral n) v = pure (VNeutral (NApp n v))
vapp param (VPrim x) (VPrim y) =
case Juvix.Core.Types.apply param x y of
Just v pure (VPrim v)
Nothing throw @"typecheckError" (CannotApply (VPrim x) (VPrim y))
vapp _ f x = throw @"typecheckError" (CannotApply f x)

-- substitution function for checkable terms
substTerm
(Show primTy, Show primVal)
Natural
Elim primTy primVal
Term primTy primVal
Term primTy primVal
substTerm _ii _r (Star i) = Star i
substTerm _ii _r (PrimTy p) = PrimTy p
substTerm ii r (Pi pi ty ty') = Pi pi (substTerm ii r ty) (substTerm (ii + 1) r ty')
substTerm ii r (Lam f) = Lam (substTerm (ii + 1) r f)
substTerm ii r (Elim e) = Elim (substElim ii r e)

-- substitution function for inferable terms
substElim
(Show primTy, Show primVal)
Natural
Elim primTy primVal
Elim primTy primVal
Elim primTy primVal
substElim ii r (Bound j)
| ii == j = r
| otherwise = Bound j
substElim _ii _r (Free y) = Free y
substElim _ii _r (Prim p) = Prim p
substElim ii r (App it ct) = App (substElim ii r it) (substTerm ii r ct)
substElim ii r (Ann pi term t) = Ann pi (substTerm ii r term) (substTerm ii r t)

-- | 'checker' for checkable terms checks the term against an annotation and returns ().
typeTerm
primTy primVal m.

0 comments on commit 2e89683

Please sign in to comment.
You can’t perform that action at this time.