Skip to content
Permalink
Browse files

Merge PR #274: Misc Michelson backend work

  • Loading branch information
cwgoes committed Jan 2, 2020
1 parent 991ae75 commit 5d9f3338c823906ddef524f94efec39e10d1e18f
@@ -36,7 +36,7 @@ compile ∷ FilePath → FilePath → Backend → IO ()
compile fin fout backend = do
(term, ty) typecheck fin backend
-- TODO: Annotated version.
let (res, logs) = M.compile undefined undefined
let (res, logs) = M.compileContract undefined undefined
case res of
Left err do
T.putStrLn (show err)
@@ -262,6 +262,7 @@ Provides a mechanism for defining Sum types
+ [[Core/Types]]
+ [[Library]]
**** Compilation <<Michelson/Compilation>>
- Entrypoints into compilation from core terms to Michelson terms & contracts.
- _Relies on_
+ [[Term]]
+ [[Compilation/Type]]
@@ -270,8 +271,32 @@ Provides a mechanism for defining Sum types
+ [[Optimisation]]
+ [[Michelson/Parameterisation]]
+ [[Library]]
***** Checks
- Sanity checks for Michelson compilation.
- _Relies on_
+ [[Michelson/Compilation/Types]]
+ [[Compilation/Util]]
+ [[Michelson/Parameterisation]]
+ [[Library]]
***** Datatypes
Datatypes & pattern matching.
- _Relies on_
+ [[Michelson/Compilation/Types]]
+ [[Compilation/Util]]
+ [[Library]]
***** Prim
- Compilation of primitive terms to Michelson instruction sequences.
- _Relies on_
+ [[Compilation/Type]]
+ [[Michelson/Compilation/Types]]
+ [[Michelson/Parameterisation]]
+ [[ErasedAnn]]
+ [[Library]]
***** Term
- Compilation of core terms to Michelson instruction sequences.
- _Relies on_
+ [[Checks]]
+ [[Prim]]
+ [[Compilation/Type]]
+ [[Michelson/Compilation/Types]]
+ [[Compilation/Util]]
@@ -280,16 +305,19 @@ Provides a mechanism for defining Sum types
+ [[ErasedAnn]]
+ [[Library]]
***** Type <<Compilation/Type>>
- Functions for representation of types in the Michelson backend.
- _Relies on_
+ [[Michelson/Compilation/Types]]
+ [[Michelson/Parameterisation]]
+ [[ErasedAnn/Types]]
+ [[Library]]
***** Types <<Michelson/Compilation/Types>>
- Types used internally by the Michelson backend.
- _Relies on_
+ [[Michelson/Parameterisation]]
+ [[Library]]
***** Util <<Compilation/Util>>
Utility functions used by the Michelson backend.
- _Relies on_
+ [[Michelson/Compilation/Types]]
+ [[Library]]
@@ -108,6 +108,7 @@ Tests for the type checker and evaluator in Core/IR/Typechecker.hs
** Michelson
- _Relies on_
+ [[Compilation]]
+ [[Types]]
+ [[Optimisation]]
+ [[Parameterisation]]
+ [[ErasedAnn]]
@@ -0,0 +1,50 @@
import Juvix.Library hiding (Nat, foldM, map, one, pred, succ, zero)

newtype Nat = Nat {unNat r. r (Nat r) r}

zero Nat
zero = Nat $ \z \s z

succ Nat Nat
succ = \n Nat $ \z \s s n

cfun r. Nat r (Nat r) r
cfun = \n \a \b unNat n a b

one Nat
one = succ zero

two Nat
two = succ one

three Nat
three = succ two

four Nat
four = succ three

isEven Nat Bool
isEven = \n cfun n True (\p not (isEven p))

add Nat Nat Nat
add = \n \m cfun n m (\x succ (add x m))

pred Nat Nat
pred = \n cfun n zero (\x x)

toNum Nat Int
toNum = \n cfun n 0 (\x 1 + toNum x)

newtype List a = List {unList r. r (a List a r) r}

nil a. List a
nil = List (\n c n)

cons a. a List a List a
cons x xs = List (\n c c x xs)

isNull a. List a Bool
isNull l = unList l True (const (const False))

map a b. (a b) List a List b
map f l = unList l nil (\x xs cons (f x) (map f xs))
@@ -139,10 +139,13 @@ library:
- Juvix.Backends.Michelson
- Juvix.Backends.Michelson.Parameterisation
- Juvix.Backends.Michelson.Compilation
- Juvix.Backends.Michelson.Compilation.Prim
- Juvix.Backends.Michelson.Compilation.Term
- Juvix.Backends.Michelson.Compilation.Type
- Juvix.Backends.Michelson.Compilation.Checks
- Juvix.Backends.Michelson.Compilation.Types
- Juvix.Backends.Michelson.Compilation.Util
- Juvix.Backends.Michelson.Compilation.Datatypes
- Juvix.Backends.Michelson.Optimisation
- Juvix.Backends.ArithmeticCircuit
- Juvix.Backends.ArithmeticCircuit.Parameterisation
@@ -1,3 +1,5 @@
-- |
-- - Entrypoints into compilation from core terms to Michelson terms & contracts.
module Juvix.Backends.Michelson.Compilation where

import qualified Data.Map as Map
@@ -11,21 +13,26 @@ import Juvix.Backends.Michelson.Parameterisation
import Juvix.Library hiding (Type)
import qualified Michelson.Printer as M
import qualified Michelson.TypeCheck as M
import qualified Michelson.Typed as M (FullContract (..))
import qualified Michelson.Typed as MT
import qualified Michelson.Untyped as M

typedContractToSource M.SomeContract Text
typedContractToSource (M.SomeContract (M.FullContract instr _ _)) = L.toStrict (M.printTypedContract False instr)
typedContractToSource (M.SomeContract (MT.FullContract instr _ _)) = L.toStrict (M.printTypedContract False instr)

untypedContractToSource M.Contract' M.ExpandedOp Text
untypedContractToSource c = L.toStrict (M.printUntypedContract False c)

compile Term Type (Either CompilationError (M.Contract' M.ExpandedOp, M.SomeContract), [CompilationLog])
compile term ty =
let (ret, env) = execWithStack [] (compileToMichelson term ty)
compileContract Term Type (Either CompilationError (M.Contract' M.ExpandedOp, M.SomeContract), [CompilationLog])
compileContract term ty =
let (ret, env) = execWithStack [] (compileToMichelsonContract term ty)
in (ret, compilationLog env)

compileToMichelson
compileExpr Term Type (Either CompilationError SomeInstr, [CompilationLog])
compileExpr term ty =
let (ret, env) = execWithStack [] (compileToMichelsonExpr term ty)
in (ret, compilationLog env)

compileToMichelsonContract
m.
( HasState "stack" Stack m,
HasThrow "compilationError" CompilationError m,
@@ -34,7 +41,7 @@ compileToMichelson ∷
Term
Type
m (M.Contract' M.ExpandedOp, M.SomeContract)
compileToMichelson term ty = do
compileToMichelsonContract term ty = do
michelsonTy typeToType ty
case michelsonTy of
M.Type (M.TLambda argTy@(M.Type (M.TPair _ _ paramTy storageTy) _) _) _ do
@@ -50,3 +57,24 @@ compileToMichelson term ty = do
Left err throw @"compilationError" (DidNotTypecheckAfterOptimisation err)
Left err throw @"compilationError" (DidNotTypecheck err)
_ throw @"compilationError" InvalidInputType

-- TODO: This shouldn't require being a function.
compileToMichelsonExpr
m.
( HasState "stack" Stack m,
HasThrow "compilationError" CompilationError m,
HasWriter "compilationLog" [CompilationLog] m
)
Term
Type
m (SomeInstr)
compileToMichelsonExpr term ty = do
michelsonTy typeToType ty
case michelsonTy of
M.Type (M.TLambda argTy@(M.Type (M.TPair _ _ paramTy storageTy) _) _) _ do
michelsonOp' termToMichelson term argTy
let michelsonOp = leftSeq michelsonOp'
MT.withSomeSingT (MT.fromUType argTy) $ \sty
case M.runTypeCheckIsolated (M.typeCheckList [michelsonOp] (sty M.-:& M.SNil)) of
Right (_ M.:/ (s M.::: _)) pure (SomeInstr s)
Left err throw @"compilationError" (DidNotTypecheck err)
@@ -0,0 +1,48 @@
-- |
-- - Sanity checks for Michelson compilation.
module Juvix.Backends.Michelson.Compilation.Checks where

import Juvix.Backends.Michelson.Compilation.Types
import Juvix.Backends.Michelson.Compilation.Util
import Juvix.Backends.Michelson.Parameterisation
import Juvix.Library
import qualified Michelson.TypeCheck as M
import qualified Michelson.Untyped as M

-- Check that the stack types tracked internally & of the instruction match.
stackGuard
m.
( HasState "stack" Stack m,
HasThrow "compilationError" CompilationError m
)
Term
M.Type
m Op
m Op
stackGuard term paramTy func = do
start get @"stack"
instr func
end get @"stack"
case stackToStack start of
M.SomeHST startStack do
-- 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
if stackToStack end == M.SomeHST endType
then pure instr
else
throw @"compilationError"
( InternalFault
( mconcat
[ "stack mismatch while compiling ",
show term,
" - end stack: ",
show end,
", lifted stack: ",
show endType
]
)
)
@@ -0,0 +1,69 @@
-- |
-- Datatypes & pattern matching.
module Juvix.Backends.Michelson.Compilation.Datatypes where

import Juvix.Backends.Michelson.Compilation.Types
import Juvix.Backends.Michelson.Compilation.Util
import Juvix.Library hiding (Type)
import Michelson.Untyped

pack
m.
(HasThrow "compilationError" CompilationError m)
Type
m ExpandedInstr
pack (Type TUnit _) = pure (PUSH "" (Type TUnit "") ValueUnit)
pack ty = throw @"compilationError" (NotYetImplemented ("pack: " <> show ty))

unpack
m.
( HasState "stack" Stack m,
HasThrow "compilationError" CompilationError m
)
Type
[Maybe Symbol]
m ExpandedOp
unpack (Type ty _) binds =
case ty of
Tbool do
modify @"stack" (drop 1)
return (SeqEx [])
TPair _ _ fT sT
case binds of
[Just fst, Just snd] do
modify @"stack" (appendDrop [(VarE fst, fT), (VarE snd, sT)])
pure (SeqEx [PrimEx (DUP ""), PrimEx (CDR "" ""), PrimEx SWAP, PrimEx (CAR "" "")])
[Just fst, Nothing] do
modify @"stack" (appendDrop [(VarE fst, fT)])
pure (PrimEx (CAR "" ""))
[Nothing, Just snd] do
modify @"stack" (appendDrop [(VarE snd, sT)])
pure (PrimEx (CDR "" ""))
[Nothing, Nothing]
genReturn (PrimEx DROP)
_ throw @"compilationError" (InternalFault "binds do not match type")
_ throw @"compilationError" (NotYetImplemented ("unpack: " <> show ty))
unpack _ _ = throw @"compilationError" (InternalFault "invalid unpack type")

unpackDrop
m.
( HasState "stack" Stack m,
HasThrow "compilationError" CompilationError m
)
[Maybe Symbol]
m ExpandedOp
unpackDrop binds = genReturn (foldDrop (fromIntegral (length (filter isJust binds))))

genSwitch
m.
( HasState "stack" Stack m,
HasThrow "compilationError" CompilationError m,
HasWriter "compilationLog" [CompilationLog] m
)
T
m (ExpandedOp ExpandedOp ExpandedOp)
genSwitch Tbool = pure (\x y PrimEx (IF [y] [x])) -- TODO: Why flipped?
genSwitch (TOr _ _ _ _) = pure (\x y PrimEx (IF_LEFT [x] [y]))
genSwitch (TOption _) = pure (\x y PrimEx (IF_NONE [x] [y]))
genSwitch (TList _) = pure (\x y PrimEx (IF_CONS [x] [y]))
genSwitch ty = throw @"compilationError" (NotYetImplemented ("genSwitch: " <> show ty))

0 comments on commit 5d9f333

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