Skip to content
Permalink
Browse files

Push/Enter and Constant Propagation for Michelson (#305)

* added TODO comment

* added multi-lambda, and removed some undefined

* added body of the logic for proper application

* major changes, won't compile, becoming closer to the real stack type

* added a new stack type and some abstarctions.

* made new position and called it lookup

* got utils to compile

* removed last inexhaustive call in Util

* got prims and datatypes to compile

* got the code to compile

* some paired programming work, got fully applied functions working

* started more work on the parital application case

* did more of the lambda case, and made helper stack functions

* added a stack file, which other files depend on, isntead of spreading
in types and utils

* updated the document and ran precommit

* changed genFunc to instToStackEff

* added a few more stack operations and finished the under applied
case (very error prone!)

* added comments on what to do for the over applied case

* Notes from discussion

* updated vstack to have a set of values it could be for future renaming

* Rename file

* made the code compile

* Rework lambda compilation

* Update recursive application handling

* Inline primitives

* forgot to commit Contract

* Promoted the values prim values take into really being on the stack

* Autoformat

* responded to suggetsions

* made evaluateAndPushArgs proper add names to already named variables

* removed anove int declaration

* commented on some WIP, and did a naive move for constants

* propagated changes from the VStack allowing lambdas to go through it

* added semigroup and monoid instance to the virtural stack

* modified evaluateAndPushArgs to act properly when an arg is a lambda

* handled the case where all arguments are constants

* ran the formatter

* added type to returnFromPi

Co-authored-by: Christopher Goes <cwgoes@pluranimity.org>
  • Loading branch information
mariari and cwgoes committed Feb 11, 2020
1 parent af7ee37 commit dcb4e81c3580bbbe379041c17f75360238a7447c
@@ -266,6 +266,8 @@ Serves as a module for various debugging functions
- _Relies on_
+ [[Michelson/Compilation]]
+ [[Michelson/Parameterisation]]
**** Contract
This module provides a default contract environment
**** Optimisation
- This is a simple optimization strategy which replaces sequences of
Michelson instructions with equivalent sequences of fewer
@@ -293,10 +295,12 @@ Serves as a module for various debugging functions
**** Compilation <<Michelson/Compilation>>
- Entrypoints into compilation from core terms to Michelson terms & contracts.
- _Relies on_
+ [[Lambda]]
+ [[Term]]
+ [[Compilation/Type]]
+ [[Michelson/Compilation/Types]]
+ [[Compilation/Util]]
+ [[VirtualStack]]
+ [[Optimisation]]
+ [[Michelson/Parameterisation]]
+ [[Library]]
@@ -305,19 +309,33 @@ Serves as a module for various debugging functions
- _Relies on_
+ [[Michelson/Compilation/Types]]
+ [[Compilation/Util]]
+ [[VirtualStack]]
+ [[Michelson/Parameterisation]]
+ [[Library]]
***** Datatypes
Datatypes & pattern matching.
- _Relies on_
+ [[Michelson/Compilation/Types]]
+ [[Compilation/Util]]
+ [[VirtualStack]]
+ [[Library]]
***** Lambda
- Compilation of core terms to Michelson instruction sequences.
- _Relies on_
+ [[Term]]
+ [[Compilation/Type]]
+ [[Michelson/Compilation/Types]]
+ [[Compilation/Util]]
+ [[VirtualStack]]
+ [[Michelson/Parameterisation]]
+ [[ErasedAnn]]
+ [[Library]]
***** Prim
- Compilation of primitive terms to Michelson instruction sequences.
- _Relies on_
+ [[Compilation/Type]]
+ [[Michelson/Compilation/Types]]
+ [[VirtualStack]]
+ [[Michelson/Parameterisation]]
+ [[ErasedAnn]]
+ [[Library]]
@@ -329,9 +347,10 @@ Datatypes & pattern matching.
+ [[Compilation/Type]]
+ [[Michelson/Compilation/Types]]
+ [[Compilation/Util]]
+ [[VirtualStack]]
+ [[Michelson/Parameterisation]]
+ [[Erased/Util]]
+ [[ErasedAnn]]
+ [[Usage]]
+ [[Library]]
***** Type <<Compilation/Type>>
- Functions for representation of types in the Michelson backend.
@@ -343,13 +362,34 @@ Datatypes & pattern matching.
***** Types <<Michelson/Compilation/Types>>
- Types used internally by the Michelson backend.
- _Relies on_
+ [[VirtualStack]]
+ [[Michelson/Parameterisation]]
+ [[Library]]
***** Util <<Compilation/Util>>
Utility functions used by the Michelson backend.
- _Relies on_
+ [[Michelson/Compilation/Types]]
+ [[VirtualStack]]
+ [[Library]]
***** VirtualStack
- Serves as a virtual stack over Michelson
- This stack has a few properties
+ The values on this stack may or may not be on the real
stack. However for convention this should be largely ignored,
except when you wish to do an operation like pair
* This can be fixed in the future
* Until then, one should filter out the virtual stack items
- We keep virtual items on the ="stack"= as that makes the details
on whether something is constant propagation or not act
consistently with each other.
+ After all, what may not be a constant now, may be in the
future, or vice versa!
- Import with qualified and the name of =VStack=
- _Relies on_
+ [[Michelson/Parameterisation]]
+ [[ErasedAnn]]
+ [[Library]]
+ [[HashMap]]
** Core
- _Relies on_
+ [[Core/Erasure]]
@@ -462,6 +502,7 @@ Utility functions used by the Michelson backend.
- _Relies on_
+ [[Erased/Types]]
+ [[ErasedAnn/Types]]
+ [[Library]]
**** Types <<ErasedAnn/Types>>
- _Relies on_
+ [[Usage]]
@@ -140,12 +140,14 @@ library:
- Juvix.Backends.Michelson.Compilation
- Juvix.Backends.Michelson.Compilation.Prim
- Juvix.Backends.Michelson.Compilation.Term
- Juvix.Backends.Michelson.Compilation.Lambda
- 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.Michelson.Compilation.VirtualStack
- Juvix.Backends.ArithmeticCircuit
- Juvix.Backends.ArithmeticCircuit.Parameterisation
- Juvix.Backends.ArithmeticCircuit.Compilation
@@ -4,10 +4,12 @@ module Juvix.Backends.Michelson.Compilation where

import qualified Data.Map as Map
import qualified Data.Text.Lazy as L
import Juvix.Backends.Michelson.Compilation.Lambda
import Juvix.Backends.Michelson.Compilation.Term
import Juvix.Backends.Michelson.Compilation.Type
import Juvix.Backends.Michelson.Compilation.Types
import Juvix.Backends.Michelson.Compilation.Util
import qualified Juvix.Backends.Michelson.Compilation.VirtualStack as VStack
import Juvix.Backends.Michelson.Optimisation
import Juvix.Backends.Michelson.Parameterisation
import Juvix.Library hiding (Type)
@@ -17,24 +19,28 @@ import qualified Michelson.Typed as MT
import qualified Michelson.Untyped as M

typedContractToSource M.SomeContract Text
typedContractToSource (M.SomeContract (MT.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)

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

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

compileToMichelsonContract
m.
( HasState "stack" Stack m,
( HasState "stack" VStack.T m,
HasThrow "compilationError" CompilationError m,
HasWriter "compilationLog" [CompilationLog] m
)
@@ -61,7 +67,7 @@ compileToMichelsonContract term ty = do
-- TODO: This shouldn't require being a function.
compileToMichelsonExpr
m.
( HasState "stack" Stack m,
( HasState "stack" VStack.T m,
HasThrow "compilationError" CompilationError m,
HasWriter "compilationLog" [CompilationLog] m
)
@@ -4,47 +4,51 @@ module Juvix.Backends.Michelson.Compilation.Checks where

import Juvix.Backends.Michelson.Compilation.Types
import Juvix.Backends.Michelson.Compilation.Util
import qualified Juvix.Backends.Michelson.Compilation.VirtualStack as VStack
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
( HasState "stack" VStack.T m,
HasThrow "compilationError" CompilationError m,
Show a
)
Term
a
M.Type
m Op
m Op
m (Either b Op)
m (Either b Op)
stackGuard term paramTy func = do
start get @"stack"
instr func
maybeInstr func
end get @"stack"
case stackToStack start of
M.SomeHST startStack do
-- TODO: Real originated contracts.
let originatedContracts = mempty
typedChecked = M.typeCheckList [instr] startStack
case M.runTypeCheck paramTy originatedContracts typedChecked 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
]
case maybeInstr of
Left _ pure maybeInstr
Right instr do
case stackToStack start of
M.SomeHST startStack do
-- TODO: Real originated contracts.
let originatedContracts = mempty
typedChecked = M.typeCheckList [instr] startStack
case M.runTypeCheck paramTy originatedContracts typedChecked 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 maybeInstr
else
throw @"compilationError"
( InternalFault
( mconcat
[ "stack mismatch while compiling ",
show term,
" - end stack: ",
show end,
", lifted stack: ",
show endType
]
)
)
)
@@ -4,6 +4,7 @@ module Juvix.Backends.Michelson.Compilation.Datatypes where

import Juvix.Backends.Michelson.Compilation.Types
import Juvix.Backends.Michelson.Compilation.Util
import qualified Juvix.Backends.Michelson.Compilation.VirtualStack as VStack
import Juvix.Library hiding (Type)
import Michelson.Untyped

@@ -17,7 +18,7 @@ pack ty = throw @"compilationError" (NotYetImplemented ("pack: " <> show ty))

unpack
m.
( HasState "stack" Stack m,
( HasState "stack" VStack.T m,
HasThrow "compilationError" CompilationError m
)
Type
@@ -26,18 +27,35 @@ unpack ∷
unpack (Type ty _) binds =
case ty of
Tbool do
modify @"stack" (drop 1)
modify @"stack" (VStack.drop 1)
return (SeqEx [])
TPair _ _ fT sT
case binds of
[Just fst, Just snd] do
modify @"stack" (appendDrop [(VarE fst, fT), (VarE snd, sT)])
modify @"stack"
( VStack.appendDrop
( VStack.fromList
[ (VStack.varNone fst, fT),
(VStack.varNone snd, sT)
]
)
)
pure (SeqEx [PrimEx (DUP ""), PrimEx (CDR "" ""), PrimEx SWAP, PrimEx (CAR "" "")])
[Just fst, Nothing] do
modify @"stack" (appendDrop [(VarE fst, fT)])
modify @"stack"
( VStack.appendDrop
( VStack.fromList
[(VStack.varNone fst, fT)]
)
)
pure (PrimEx (CAR "" ""))
[Nothing, Just snd] do
modify @"stack" (appendDrop [(VarE snd, sT)])
modify @"stack"
( VStack.appendDrop
( VStack.fromList
[(VStack.varNone snd, sT)]
)
)
pure (PrimEx (CDR "" ""))
[Nothing, Nothing]
genReturn (PrimEx DROP)
@@ -46,7 +64,7 @@ unpack (Type ty _) binds =

unpackDrop
m.
( HasState "stack" Stack m,
( HasState "stack" VStack.T m,
HasThrow "compilationError" CompilationError m
)
[Maybe Symbol]
@@ -55,7 +73,7 @@ unpackDrop binds = genReturn (foldDrop (fromIntegral (length (filter isJust bind

genSwitch
m.
( HasState "stack" Stack m,
( HasState "stack" VStack.T m,
HasThrow "compilationError" CompilationError m,
HasWriter "compilationLog" [CompilationLog] m
)

0 comments on commit dcb4e81

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