Skip to content
Permalink
Browse files

Core alterations in prep for Michelson backend work (#174)

* Squash into single commit

* Start untyped optimisations; 'make format'

* Switch to untyped optimisation passes

* Add lambda/exec optimisation & testcase

* Add TODOs

* Add type-annotated HR core

* Add type-annotated erased core

* `typeOf` returns non-empty list

* Update names of functions to match term/elim nomenclature

* Update a few test-cases

* Parameterise typechecker over a monad

* Finish error type, remove all `error` usage

* Add `IRAnn` (annotated core IR)

* Update comments

* Minimise required annotations

* Comment out Michelson tests for now
  • Loading branch information
cwgoes authored and thealmarty committed Nov 27, 2019
1 parent ef8b8c6 commit 7b81fdc6d1944c999098605ef66f4907e205ef23
@@ -22,7 +22,7 @@ build-watch:
stack build --copy-bins --fast --file-watch

build-opt: clean
stack build --copy-bins --ghc-options "-O3 -fllvm -DOPTIMISE"
stack build --copy-bins --ghc-options "-O3 -fllvm"

lint:
stack exec -- hlint app src test
@@ -31,7 +31,7 @@ format:
find . -path ./.stack-work -prune -o -path ./archived -prune -o -type f -name "*.hs" -exec ormolu --mode inplace {} \;

test:
stack test --fast --ghc-options "-DOPTIMISE"
stack test --fast

repl-lib:
stack ghci juvix:lib
@@ -80,8 +80,11 @@ library:
- Juvix
- Juvix.Core
- Juvix.Core.HR
- Juvix.Core.HRAnn
- Juvix.Core.IR
- Juvix.Core.IRAnn
- Juvix.Core.Erased
- Juvix.Core.ErasedAnn
- Juvix.Core.Erased.Evaluator
- Juvix.Core.Erased.Types
- Juvix.Core.Erasure
@@ -157,6 +160,12 @@ library:
- Juvix.Core.IR.Typechecker
- Juvix.Core.HR.Parser
- Juvix.Core.HR.Types
- Juvix.Core.HRAnn.Types
- Juvix.Core.HRAnn.Erasure
- Juvix.Core.IRAnn.Types
- Juvix.Core.IRAnn.Erasure
- Juvix.Core.ErasedAnn.Types
- Juvix.Core.ErasedAnn.Erasure

executables:
juvix:
@@ -15,8 +15,8 @@ type PrimTy = ()

type PrimVal = ()

typeOf PrimVal [PrimTy]
typeOf () = [()]
typeOf PrimVal NonEmpty PrimTy
typeOf () = () :| []

apply PrimVal PrimVal Maybe PrimVal
apply _ _ = Nothing
@@ -39,8 +39,11 @@ compileToMichelson term ty = do
let michelsonOp = leftSeq michelsonOp'
let contract = M.Contract paramTy storageTy [michelsonOp]
case M.typeCheckContract Map.empty contract of
Right (M.SomeContract instr start end) do
optimised optimise instr
pure (M.SomeContract optimised start end)
Right _ do
optimised optimise michelsonOp
let optimisedContract = M.Contract paramTy storageTy [optimised]
case M.typeCheckContract Map.empty optimisedContract of
Right c pure c
Left err throw @"compilationError" (DidNotTypecheckAfterOptimisation err)
Left err throw @"compilationError" (DidNotTypecheck err)
_ throw @"compilationError" InvalidInputType
@@ -17,9 +17,9 @@ termToMichelson ∷
Term
M.Type
m Op
termToMichelson term argTy = do
modify @"stack" ((FuncResultE, argTy) :)
instr termToInstr term
termToMichelson term paramTy = do
modify @"stack" ((FuncResultE, paramTy) :)
instr termToInstr term paramTy
tell @"compilationLog" [TermToInstr term instr]
pure instr

@@ -29,16 +29,18 @@ stackGuard ∷
HasThrow "compilationError" CompilationError m
)
Term
M.Type
(Term m Op)
m Op
stackGuard term func = do
stackGuard term paramTy func = do
start get @"stack"
instr func term
end get @"stack"
case stackToStack start of
M.SomeHST startStack do
-- TODO: Should use M.runTypeCheck instead.
case M.runTypeCheckTest (M.typeCheckList [instr] startStack) of
-- TODO: Real originated contracts.
let originatedContracts = mempty
case M.runTypeCheck paramTy originatedContracts (M.typeCheckList [instr] startStack) of
Left err throw @"compilationError" (DidNotTypecheck err)
Right (_ M.:/ (M.AnyOutInstr _)) throw @"compilationError" (NotYetImplemented "any out instr")
Right (_ M.:/ (_ M.::: endType)) do
@@ -71,8 +73,9 @@ termToInstr ∷
HasWriter "compilationLog" [CompilationLog] m
)
Term
M.Type
m Op
termToInstr term = stackGuard term $ \term do
termToInstr term paramTy = stackGuard term paramTy $ \term do
let notYetImplemented m Op
notYetImplemented = throw @"compilationError" (NotYetImplemented ("termToInstr: " <> show term))

@@ -93,12 +96,15 @@ termToInstr term = stackGuard term $ \term → do
case prim of
-- :: \x -> y ~ (x, s) => (y, s)
PrimFst stackCheck (lambda 1) $ do
-- TODO: return lambda (pair x y) x CAR
genReturn (M.PrimEx (M.CAR "" ""))
-- :: \x -> y ~ (x, s) => (y, s)
PrimSnd stackCheck (lambda 1) $ do
-- TODO: return lambda (pair x y) y CDR
genReturn (M.PrimEx (M.CDR "" ""))
-- :: \x y -> a ~ (x, (y, s)) => (a, s)
PrimPair stackCheck (lambda 2) $ do
-- TODO: return lambda (x, y) (x, y)
modify @"stack" (\((_, xT) : (_, yT) : xs) (FuncResultE, M.Type (M.TPair "" "" xT yT) "") : xs)
pure (M.PrimEx (M.PAIR "" "" "" ""))
-- :: a ~ s => (a, s)
@@ -133,28 +139,32 @@ termToInstr term = stackGuard term $ \term → do
J.Lam arg body
stackCheck (lambda 1) $ do
modify @"stack" (\((_, t) : xs) (VarE arg, t) : xs)
inner termToInstr body
inner termToInstr body paramTy
after genReturn (foldDrop 1)
pure (M.SeqEx [inner, after])
-- TODO (maybe): Multi-arg lambdas.
-- Ordering: Treat as \a b -> c ~= \a -> \b -> c, e.g. reverse stack order.
-- forM_ args (\a -> modify ((:) (M.VarE (prettyPrintValue a), M.PairT M.BoolT M.BoolT)))

-- TODO: This is a hack.
-- :: (\a b -> c) a b ~ (a, (b, s)) => (c, s)
J.App (J.App func arg1) arg2
{-
-- TODO: Will this work in all cases?
-- Consider app, e.g. (\f -> f 1 2) pair, seems problematic.
-- :: (\a ... {n} b -> c) a ... {n} b ~ (a, ... {n} (b, s)) => (c, s)
J.App func arg →
stackCheck addsOne $ do
arg2 termToInstr arg2
arg1 termToInstr arg1
func termToInstr func
pure (M.SeqEx [arg2, arg1, func])
let rec f args =
case f of
J.App f a → rec f (a : args)
_ → (f, args)
(fn, args) = rec func [arg]
args ← mapM (flip termToInstr paramTy) (reverse args)
func ← termToInstr fn paramTy
pure (M.SeqEx (args <> [func]))
-}

-- :: (\a -> b) a ~ (a, s) => (b, s)
-- Call-by-value (evaluate argument first).
J.App func arg
stackCheck addsOne $ do
arg termToInstr arg
func termToInstr func
pure (M.SeqEx [arg, func])
func termToInstr func paramTy -- :: Lam a b
arg termToInstr arg paramTy -- :: a
pure (M.SeqEx [func, arg, M.PrimEx (M.EXEC "")])

takesOne Stack Stack Bool
takesOne post pre = post == drop 1 pre
@@ -16,7 +16,7 @@ typeToType ty =
J.SymT _ throw @"compilationError" InvalidInputType
J.Star _ throw @"compilationError" InvalidInputType
J.PrimTy (PrimTy mTy) pure mTy
J.Pi argTy retTy do
J.Pi _ argTy retTy do
argTy typeToType argTy
retTy typeToType retTy
pure (M.Type (M.TLambda argTy retTy) "")
@@ -11,11 +11,12 @@ data CompilationError
| InvalidInputType
| InternalFault Text
| DidNotTypecheck M.TCError
| DidNotTypecheckAfterOptimisation M.TCError
deriving (Show, Eq, Generic)

data CompilationLog
= TermToInstr Term Op
| Optimised SomeInstr SomeInstr
| Optimised Op Op
deriving (Generic)

type Stack = [(StackElem, M.Type)]
@@ -1,61 +1,62 @@
{-# LANGUAGE CPP #-}
{- This is used to only build with full optimisations when building in release mode, since building with full optimisations is apparently very slow. -}

-- | 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).
module Juvix.Backends.Michelson.Optimisation where

import Juvix.Library
import Juvix.Backends.Michelson.Compilation.Types
import Michelson.Typed

{- 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).
This optimization function is typed in the Instr GADT, so it cannot produce invalid output Michelson.
However, the typesystem does not enforce computation correctness; that would require dependent types.
-}
import Juvix.Backends.Michelson.Parameterisation
import Juvix.Library
import Michelson.Untyped hiding (Op)

optimise a b m.
optimise
m.
(HasWriter "compilationLog" [CompilationLog] m)
Instr a b m (Instr a b)
optimise instr = do
let inner e = do
one optimise' e
two optimise' one
Op
m Op
optimise op = do
let inner o = do
let one = optimiseSingle o
two = optimiseSingle one
if one == two then pure two else inner two
ret <- inner instr
tell @"compilationLog" [Optimised (SomeInstr instr) (SomeInstr ret)]
ret inner op
tell @"compilationLog" [Optimised op ret]
pure ret

optimise' a b m.
(Monad m)
Instr a b
m (Instr a b)
optimise' expr =
case expr of
(IF x y) IF <$> optimise' x <*> optimise' y
(IF_LEFT x y) IF_LEFT <$> optimise' x <*> optimise' y
(IF_CONS x y) IF_CONS <$> optimise' x <*> optimise' y
(IF_NONE x y) IF_NONE <$> optimise' x <*> optimise' y
(DIP e) DIP |<< optimise' e
#if defined(OPTIMISE)
{- We can assume Seq will be left-forced. -}
(Seq (Seq DUP (DIP e)) DROP) optimise' e
(Seq (DIP e) DROP) optimise' (Seq DROP e)
(Seq (Seq (Seq e DUP) SWAP) DROP) optimise' e
(Seq (Seq DUP SWAP) DROP) pure Nop
(Seq DUP (DIP DROP)) pure Nop
(Seq (Seq SWAP DUP) (DIP SWAP)) pure (Seq (DIP DUP) SWAP)
(Seq DUP SWAP) pure DUP
(Seq DUP DROP) pure Nop
(Seq SWAP SWAP) pure Nop
(Seq FAILWITH _) pure FAILWITH
#endif
(Seq e Nop) optimise' e
(Seq Nop e) optimise' e
(Seq x y) Seq <$> optimise' x <*> optimise' y
expr pure expr
optimiseSeq [Op] [Op]
optimiseSeq ops =
case ops of
{- Simple stack manipulations. -}
(PrimEx (DUP _) : PrimEx (DIP e) : PrimEx DROP : rest) e <> rest
(PrimEx (DIP e) : PrimEx DROP : rest) PrimEx DROP : e <> rest
(PrimEx (DUP _) : PrimEx SWAP : PrimEx DROP : rest) rest
(PrimEx (DUP _) : PrimEx (DIP [PrimEx DROP]) : rest) rest
(PrimEx SWAP : PrimEx (DUP _) : PrimEx (DIP [PrimEx SWAP]) : rest) PrimEx (DIP [PrimEx (DUP "")]) : PrimEx SWAP : rest
(PrimEx (DUP ann) : PrimEx SWAP : rest) PrimEx (DUP ann) : rest
(PrimEx SWAP : PrimEx SWAP : rest) rest
(PrimEx (DUP _) : PrimEx DROP : rest) rest
{- Failures. -}
(PrimEx FAILWITH : _) [PrimEx FAILWITH]
{- Lambda / exec. -}
(PrimEx (LAMBDA _ _ _ l) : PrimEx (EXEC _) : rest) l <> rest
--(Seq (Seq op (LAMBDA (VLam l))) EXEC) -> pure (Seq op l)
{- Recursive case. -}
(op : rest) optimiseSingle op : optimiseSeq rest
{- Empty case. -}
[] []

optimiseSingle Op Op
optimiseSingle op =
case op of
PrimEx prim PrimEx $
case prim of
IF a b IF (optimiseSeq a) (optimiseSeq b)
IF_LEFT a b IF_LEFT (optimiseSeq a) (optimiseSeq b)
IF_CONS a b IF_CONS (optimiseSeq a) (optimiseSeq b)
IF_NONE a b IF_NONE (optimiseSeq a) (optimiseSeq b)
DIP a DIP (optimiseSeq a)
instr instr
SeqEx seq SeqEx (optimiseSeq seq)
WithSrcEx s op WithSrcEx s (optimiseSingle op)
@@ -30,8 +30,8 @@ data PrimVal
deriving (Show, Eq, Generic)

-- TODO: Add rest of primitive values.
typeOf PrimVal [PrimTy]
typeOf (PrimConst v) = [PrimTy (M.Type (constType v) "")]
typeOf PrimVal NonEmpty PrimTy
typeOf (PrimConst v) = PrimTy (M.Type (constType v) "") :| []

constType M.Value' Op M.T
constType v =
@@ -43,7 +43,7 @@ parameterizeType ty = do
pure (PPrimT p)
SymT sym
pure (PSymT param sym)
Pi arg body do
Pi _ arg body do
arg parameterizeType arg
body parameterizeType body
pure (PArrT param arg body)
@@ -111,8 +111,8 @@ boxAndTypeConstraint ∷
m (RPT primVal, PType primTy)
boxAndTypeConstraint parameterisation parameterizedAssignment term = do
let rec = boxAndTypeConstraint parameterisation parameterizedAssignment
arrow [x] = PPrimT x
arrow (x : xs) = PArrT 0 (PPrimT x) (arrow xs)
arrow (x :| []) = PPrimT x
arrow (x :| (y : ys)) = PArrT 0 (PPrimT x) (arrow (y :| ys))
varPaths get @"varPaths"
param addPath
path get @"path"
@@ -276,8 +276,8 @@ bracketCheckerErr t = left Brack (bracketChecker t)
typChecker primTy primVal. (Eq primTy) Parameterisation primTy primVal RPTO primVal ParamTypeAssignment primTy Either (TypeErrors primTy primVal) ()
typChecker parameterisation t typAssign = runEither (() <$ rec' t typAssign)
where
arrow [x] = PPrimT x
arrow (x : xs) = PArrT 0 (PPrimT x) (arrow xs)
arrow (x :| []) = PPrimT x
arrow (x :| (y : ys)) = PArrT 0 (PPrimT x) (arrow (y :| ys))
rec' (RBang bangVar (RVar s)) assign =
case assign Map.!? s of
Nothing throw @"typ" MissingOverUse
@@ -1,5 +1,6 @@
module Juvix.Core.Erased.Types where

import Juvix.Core.Usage
import Juvix.Library hiding (Type)
import qualified Juvix.Library.HashMap as Map

@@ -15,7 +16,7 @@ data Type primTy
| Star Natural
| PrimTy primTy
| -- TODO: How to deal with dependency?
Pi (Type primTy) (Type primTy)
Pi Usage (Type primTy) (Type primTy)
deriving (Show, Eq, Generic)

type TypeAssignment primTy = Map.Map Symbol (Type primTy)
@@ -0,0 +1,8 @@
module Juvix.Core.ErasedAnn
( module Juvix.Core.ErasedAnn.Types,
module Juvix.Core.ErasedAnn.Erasure,
)
where

import Juvix.Core.ErasedAnn.Erasure
import Juvix.Core.ErasedAnn.Types
@@ -0,0 +1,12 @@
module Juvix.Core.ErasedAnn.Erasure where

import qualified Juvix.Core.Erased.Types as E
import Juvix.Core.ErasedAnn.Types

eraseTerm primTy primVal. Term primTy primVal E.Term primVal
eraseTerm term =
case term of
Var s E.Var s
Prim p E.Prim p
Lam s b E.Lam s (eraseTerm b)
App (f, _, _) x E.App (eraseTerm f) (eraseTerm x)

0 comments on commit 7b81fdc

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