diff --git a/CHANGES.md b/CHANGES.md new file mode 100644 --- /dev/null +++ b/CHANGES.md @@ -0,0 +1,4 @@ +0.1.0.0 +======= + +Initial release. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,19 @@ +MIT License Copyright (c) 2020 Tocqueville Group + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is furnished +to do so, subject to the following conditions: + +The above copyright notice and this permission notice (including the next +paragraph) shall be included in all copies or substantial portions of the +Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS +OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF +OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,35 @@ +# Indigo eDSL + +[![Hackage](https://img.shields.io/hackage/v/indigo.svg)](https://hackage.haskell.org/package/indigo) + +Indigo eDSL is a high level language for Michelson contract development. +It is meant first and foremost to free you from the burden of manual stack +management and supports common features of imperative languages. + +It is built on top of `Lorentz`, which in turn is built on top of `Morley`, a +dialect that is a superset of vanilla Michelson. +If you are interested more in the relationships between these projects you can +start by taking a look at [Morley's README](../../README.md). + +## Overall idea + +Michelson contracts are stack-based and often follow the repetitive pattern of +copying the required values on top of the stack to apply an instruction to them. +Indigo can associate variables to values in the stack and it's able to refer to +them in order to handle this pattern automatically. + +In addition to this it can override existing variables with new values, allowing +the manipulation of the stack to be automatic. + +Leveraging this ability, it also supports features such as: imperative statements +(`if`, `while`, ...), expressions, operators (`+`, `||`, `==`, ...), scoped +functions definition and errors. + +Indigo uses Morley to map values from Michelson to Haskell and to compile to +Michelson code (or to any of the other projects in the chain mentioned above). + +## Tutorial and documentation + +Indigo has a tutorial that you can find [here](tutorial/). + +In addition, as for the other Morley projects, it has Haddock documentation. diff --git a/indigo.cabal b/indigo.cabal new file mode 100644 --- /dev/null +++ b/indigo.cabal @@ -0,0 +1,128 @@ +cabal-version: 2.2 + +-- This file has been generated from package.yaml by hpack version 0.33.0. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: 89d2d9515cfb2c4865221da490f19007abfc84bf0545ecf6319d2c748bb5f52a + +name: indigo +version: 0.1.0.0 +synopsis: Convenient imperative eDSL over Lorentz. +description: Syntax and implementation of Indigo eDSL. +category: Language +homepage: https://indigo-lang.gitlab.io/ +bug-reports: https://gitlab.com/morley-framework/morley/-/issues +author: Serokell, Tocqueville Group +maintainer: Serokell +copyright: 2019-2020 Tocqueville Group +license: MIT +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + CHANGES.md + +source-repository head + type: git + location: git@gitlab.com:morley-framework/morley.git + +library + exposed-modules: + Indigo + Indigo.Backend + Indigo.Backend.Case + Indigo.Backend.Conditional + Indigo.Backend.Error + Indigo.Backend.Lambda + Indigo.Backend.Prelude + Indigo.Backend.Scope + Indigo.Backend.Var + Indigo.Compilation + Indigo.Compilation.Lambda + Indigo.Compilation.Params + Indigo.FromLorentz + Indigo.Frontend + Indigo.Frontend.Language + Indigo.Frontend.Program + Indigo.Frontend.Statement + Indigo.Internal + Indigo.Internal.Expr + Indigo.Internal.Expr.Compilation + Indigo.Internal.Expr.Decompose + Indigo.Internal.Expr.Symbolic + Indigo.Internal.Expr.Types + Indigo.Internal.Field + Indigo.Internal.Lookup + Indigo.Internal.Object + Indigo.Internal.SIS + Indigo.Internal.State + Indigo.Lib + Indigo.Lorentz + Indigo.Prelude + Indigo.Print + Indigo.Rebinded + other-modules: + Paths_indigo + autogen-modules: + Paths_indigo + hs-source-dirs: + src + default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns DeriveAnyClass DerivingStrategies NoApplicativeDo RebindableSyntax FunctionalDependencies + ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-unused-do-bind + build-depends: + base >=4.7 && <5 + , constraints + , containers + , lorentz + , morley + , morley-prelude + , reflection + , singletons + , template-haskell + , vinyl + mixins: + base hiding (Prelude) + default-language: Haskell2010 + +test-suite indigo-test + type: exitcode-stdio-1.0 + main-is: Main.hs + other-modules: + Test.Code.Decomposition + Test.Code.Examples + Test.Code.Expr + Test.Code.Lambda + Test.Decomposition + Test.Examples + Test.Expr + Test.Lambda + Test.Lookup + Test.Util + Test.Util.Golden + Tree + Paths_indigo + hs-source-dirs: + test + default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns DeriveAnyClass DerivingStrategies NoApplicativeDo RebindableSyntax FunctionalDependencies + ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -threaded -eventlog -rtsopts "-with-rtsopts=-N -A64m -AL256m" + build-tool-depends: + tasty-discover:tasty-discover + build-depends: + HUnit + , base >=4.7 && <5 + , containers + , fmt + , hedgehog + , hspec-expectations + , indigo + , lorentz + , morley + , morley-prelude + , singletons + , tasty + , tasty-hedgehog + , tasty-hunit-compat + mixins: + base hiding (Prelude) + default-language: Haskell2010 diff --git a/src/Indigo.hs b/src/Indigo.hs new file mode 100644 --- /dev/null +++ b/src/Indigo.hs @@ -0,0 +1,17 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Indigo + ( module Exports + ) where + +import Indigo.Compilation as Exports +import Indigo.FromLorentz as Exports +import Indigo.Frontend as Exports +import Indigo.Internal as Exports hiding (return, (=<<), (>>), (>>=)) +import Indigo.Lib as Exports +import Indigo.Lorentz as Exports +import Indigo.Prelude as Exports +import Indigo.Print as Exports +import Indigo.Rebinded as Exports diff --git a/src/Indigo/Backend.hs b/src/Indigo/Backend.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Backend.hs @@ -0,0 +1,248 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +-- | Strictly typed statements of Indigo language. + +module Indigo.Backend + ( module ReExports + + -- * Loop + , forEach + , while + , whileLeft + + -- * Contract call + , selfCalling + , contractCalling + + -- * Documentation + , doc + , docGroup + , docStorage + , contractName + , finalizeParamCallingDoc + , contractGeneral + , contractGeneralDefault + + -- * Side-effects + , transferTokens + , setDelegate + + -- * Functions, Procedures and Scopes + , scope + + -- * Comments + , comment + + -- * Conversion from Lorentz + , fromLorentzFun1 + , fromLorentzFun2 + , fromLorentzFun3 + , fromLorentzFun1Void + , fromLorentzFun2Void + , fromLorentzFun3Void + ) where + +import Indigo.Backend.Case as ReExports +import Indigo.Backend.Conditional as ReExports +import Indigo.Backend.Error as ReExports +import Indigo.Backend.Lambda as ReExports +import Indigo.Backend.Scope as ReExports +import Indigo.Backend.Var as ReExports + +import Indigo.Backend.Prelude +import Indigo.FromLorentz +import Indigo.Internal +import Indigo.Lorentz +import qualified Lorentz.Doc as L +import qualified Lorentz.EntryPoints.Doc as L (finalizeParamCallingDoc) +import Lorentz.EntryPoints.Helpers (RequireSumType) +import qualified Lorentz.Instr as L +import qualified Michelson.Typed as MT +import Util.Type (type (++)) + +---------------------------------------------------------------------------- +-- Loop +---------------------------------------------------------------------------- + +-- | While statement. The same rule about releasing. +while :: forall inp xs ex . ex :~> Bool => ex -> IndigoState inp xs () -> IndigoState inp inp () +while e body = IndigoState $ \md -> + let expCd = gcCode $ runIndigoState (compileToExpr e) md in + let bodyIndigoState = cleanGenCode $ runIndigoState body md in + GenCode () md (expCd # L.loop (bodyIndigoState # expCd)) L.nop + +whileLeft + :: forall inp xs ex l r . + ( ex :~> Either l r + , KnownValue l + , KnownValue r + ) + => ex + -> (Var l -> IndigoState (l & inp) xs ()) + -> IndigoState inp (r & inp) (Var r) +whileLeft e body = IndigoState $ \md -> + let + cde = gcCode $ runIndigoState (compileToExpr e) md + (l, newMd) = pushRefMd md + gc = cleanGenCode $ runIndigoState (body l) newMd + (r, resMd) = pushRefMd md + in GenCode r resMd (cde # L.loopLeft (gc # L.drop # cde)) L.drop + +-- | For statements to iterate over container. +forEach + :: forall a e inp xs. (IterOpHs a, KnownValue (IterOpElHs a), e :~> a) + => e -> (Var (IterOpElHs a) -> IndigoState ((IterOpElHs a) & inp) xs ()) + -> IndigoState inp inp () +forEach container body = IndigoState $ \md -> + let cde = gcCode $ runIndigoState (compileToExpr container) md in + let (var, newMd) = pushRefMd md in + let bodyIndigoState = cleanGenCode $ runIndigoState (body var) newMd in + GenCode () md (cde # L.iter (bodyIndigoState # L.drop)) L.nop + +---------------------------------------------------------------------------- +-- Documentation +---------------------------------------------------------------------------- + +-- | Put a document item. +doc :: DocItem di => di -> IndigoState s s () +doc di = IndigoState \md -> GenCode () md (L.doc di) L.nop + +-- | Group documentation built in the given piece of code +-- into block dedicated to one thing, e.g. to one entrypoint. +docGroup :: DocGrouping -> IndigoState i o () -> IndigoState i o () +docGroup gr ii = IndigoState $ \md -> + let GenCode _ mdii cd clr = runIndigoState ii md in + GenCode () mdii (L.docGroup gr cd) clr + +-- | Insert documentation of the contract storage type. The type +-- should be passed using type applications. +docStorage :: forall storage s. TypeHasDoc storage => IndigoState s s () +docStorage = IndigoState \md -> GenCode () md (L.docStorage @storage) L.nop + +-- | Give a name to given contract. Apply it to the whole contract code. +contractName :: Text -> IndigoState i o () -> IndigoState i o () +contractName cName b = IndigoState $ \md -> + let GenCode _ mdb gc clr = runIndigoState b md in + GenCode () mdb (L.contractName cName gc) clr + +-- | Attach general info to given contract. +contractGeneral :: IndigoState i o () -> IndigoState i o () +contractGeneral b = IndigoState $ \md -> + let GenCode _ mdb gc clr = runIndigoState b md in + GenCode () mdb (L.contractGeneral gc) clr + +-- | Attach default general info to the contract documentation. +contractGeneralDefault :: IndigoState s s () +contractGeneralDefault = + IndigoState \md -> GenCode () md L.contractGeneralDefault L.nop + +-- | Indigo version for the function of the same name from Lorentz. +finalizeParamCallingDoc + :: forall cp param inp out x. (param :~> cp, NiceParameterFull cp, RequireSumType cp, HasCallStack) + => (Var cp -> IndigoState (cp & inp) out x) + -> (param -> IndigoState inp out x) +finalizeParamCallingDoc act param = IndigoState $ \md -> + let cde = gcCode $ runIndigoState (compileToExpr param) md in + let (var, newMd) = pushRefMd md in + let GenCode x md1 cd clr = runIndigoState (act var) newMd in + GenCode x md1 (cde # L.finalizeParamCallingDoc cd) (clr # L.drop) + +---------------------------------------------------------------------------- +-- Contract call +---------------------------------------------------------------------------- + +selfCalling + :: forall p inp mname. + ( NiceParameterFull p + , KnownValue (GetEntryPointArgCustom p mname) + ) + => EntryPointRef mname + -> IndigoState inp (ContractRef (GetEntryPointArgCustom p mname) & inp) + (Var (ContractRef (GetEntryPointArgCustom p mname))) +selfCalling epRef = do + nullaryOp (L.selfCalling @p epRef) + makeTopVar + +contractCalling + :: forall cp inp epRef epArg addr exAddr. + ( HasEntryPointArg cp epRef epArg + , ToTAddress cp addr + , ToT addr ~ ToT Address + , IsExpr exAddr addr + , KnownValue epArg + ) + => epRef -> exAddr + -> IndigoState inp (Maybe (ContractRef epArg) & inp) (Var (Maybe (ContractRef epArg))) +contractCalling epRef addr = do + unaryOp addr (L.contractCalling @cp epRef) + makeTopVar + +---------------------------------------------------------------------------- +-- Side-effects +---------------------------------------------------------------------------- + +transferTokens + :: (IsExpr exp p, IsExpr exm Mutez, IsExpr exc (ContractRef p), NiceParameter p, HasSideEffects) + => exp -> exm -> exc -> IndigoState inp inp () +transferTokens ep em ec = do + MetaData s _ <- iget + ternaryOpFlat ep em ec (L.transferTokens # varActionOperation s) + +setDelegate :: (HasSideEffects, IsExpr ex (Maybe KeyHash)) => ex -> IndigoState inp inp () +setDelegate e = do + MetaData s _ <- iget + unaryOpFlat e (L.setDelegate # varActionOperation s) + +---------------------------------------------------------------------------- +-- Functions, Procedures and Scopes +---------------------------------------------------------------------------- + +-- | Takes an arbitrary 'IndigoM' and wraps it into an 'IndigoFunction' +-- producing a local scope for its execution. Once it executed, all +-- non-returned variables are cleaned up so that the stack has only +-- returned variables at the top. This also can be interpreted as +-- @if True then f else nop@. +-- +-- Note, that by default we do not define scope inside indigo functions, +-- meaning that once we want to create a new variable or return it from +-- a function we need to do it inside @scope $ instr@ construction, for +-- example: +-- +-- @ +-- f :: IndigoFunction s Natural +-- f = scope $ do +-- *[s]* +-- res <- newVar (0 :: Natural) +-- *[Natural, s]* +-- scope $ do +-- _n <- newVar (1 :: Integer) +-- *[Integer, Natural, s] +-- res += 4 +-- *[Natural, s]* +-- return res +-- *[s]* +-- @ +scope + :: forall a inp out . ScopeCodeGen a + => IndigoState inp out a + -> IndigoState inp (RetOutStack a ++ inp) (RetVars a) +scope f = IndigoState $ \md -> + let gc = runIndigoState f md in + finalizeStatement @a md (compileScope gc) + +-- | Add a comment +comment :: MT.CommentType -> IndigoState i i () +comment t = IndigoState $ \md -> GenCode () md (L.comment t) L.nop + +---------------------------------------------------------------------------- +-- Conversion from Lorentz +---------------------------------------------------------------------------- + +-- Functions that convert Lorentz code to Indigo. +-- Will be removed when all Lorentz code is translated in Indigo. + +$(genFromLorentzFunN 3) diff --git a/src/Indigo/Backend/Case.hs b/src/Indigo/Backend/Case.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Backend/Case.hs @@ -0,0 +1,135 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +-- | High level statements of Indigo language. + +module Indigo.Backend.Case + ( (#=) + , caseRec + , entryCaseRec + , entryCaseSimpleRec + + , IndigoCaseClauseL + , CaseCommonF + , CaseCommon + , IndigoAnyOut (..) + ) where + +import Data.Vinyl.Core (RMap(..)) +import Util.Type (type (++)) +import Util.TypeLits (AppendSymbol) + +import Indigo.Backend.Prelude +import Indigo.Backend.Scope +import Indigo.Internal +import Indigo.Lorentz +import qualified Lorentz.ADT as L +import qualified Lorentz.EntryPoints.Doc as L +import qualified Lorentz.Instr as L +import Michelson.Typed.Haskell.Instr.Sum + (CaseClauseParam(..), CaseClauses, CtorField(..), InstrCaseC) + +-- | This type is analogous to the 'CaseClauseL' type but instead of wrapping a Lorentz +-- instruction, this wraps an Indigo value with the same input/output types. +data IndigoCaseClauseL ret (param :: CaseClauseParam) where + OneFieldIndigoCaseClauseL + :: (forall inp . MetaData inp -> CaseClauseL inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x))) + -> IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x)) + +data IndigoAnyOut x ret = forall retBranch . + ( ScopeCodeGen retBranch + , RetOutStack ret ~ RetOutStack retBranch + ) => + IndigoAnyOut (forall inp . SomeIndigoState (x : inp) retBranch) + +instance + ( name ~ AppendSymbol "c" ctor + , KnownValue x + ) + => + CaseArrow + name + (Var x -> IndigoAnyOut x ret) + (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x))) + where + (/->) _ ind = + OneFieldIndigoCaseClauseL (\(md :: MetaData inp) -> + -- Create a reference to the top of stack + let (varCase, mdCaseBody) = pushRefMd md in + -- Pass the reference to the case body + case ind varCase of + IndigoAnyOut (SomeIndigoState body :: SomeIndigoState (x : inp) retBr) -> + case body mdCaseBody of + SomeGenCode gc -> + CaseClauseL $ + -- Compute returning expressions and clean up everything + compileScope gc # + -- Remove @x@ from the stack too + liftClear' @(ClassifyReturnValue retBr) @retBr @(x & inp) @inp L.drop + ) + +-- | An alias for '/->' to use when the body is a lambda so that the +-- whole thing won't have multiple arrows. +(#=) :: CaseArrow name body clause => Label name -> body -> clause +(#=) a b = a /-> b + +-- This constraint is shared by all @case*@ functions. +type CaseCommonF f dt guard ret clauses = + ( guard :~> dt + , InstrCaseC dt + , RMap (CaseClauses dt) + , clauses ~ Rec (f ret) (CaseClauses dt) + , ScopeCodeGen ret + ) + +type CaseCommon dt guard ret clauses = CaseCommonF IndigoCaseClauseL dt guard ret clauses + +-- | A case statement for indigo. See examples for a sample usage. +caseRec + :: forall dt guard inp ret clauses . ( CaseCommon dt guard ret clauses) + => guard + -> clauses + -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret) +caseRec g cls = IndigoState $ \md -> + let cdG = gcCode $ runIndigoState (compileToExpr g) md in + finalizeStatement @ret md (cdG # L.case_ (toCaseClauseL md cls)) + +-- | 'case_' for pattern-matching on parameter. +entryCaseRec + :: forall dt entryPointKind guard inp ret clauses . + ( CaseCommon dt guard ret clauses + , DocumentEntryPoints entryPointKind dt + ) + => Proxy entryPointKind + -> guard + -> clauses + -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret) +entryCaseRec proxy g cls = IndigoState $ \md -> + let cdG = gcCode $ runIndigoState (compileToExpr g) md in + finalizeStatement @ret md (cdG # L.entryCase_ proxy (toCaseClauseL md cls)) + +-- | 'entryCase_' for contracts with flat parameter. +entryCaseSimpleRec + :: forall cp guard inp ret clauses . + ( CaseCommon cp guard ret clauses + , DocumentEntryPoints PlainEntryPointsKind cp + , NiceParameterFull cp + , RequireFlatParamEps cp + ) + => guard + -> clauses + -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret) +entryCaseSimpleRec g cls = IndigoState $ \md -> + let cdG = gcCode $ runIndigoState (compileToExpr g) md in + finalizeStatement @ret md (cdG # L.entryCaseSimple_ (toCaseClauseL md cls)) + +toCaseClauseL + :: forall inp ret cs . + MetaData inp + -> Rec (IndigoCaseClauseL ret) cs + -> Rec (CaseClauseL inp (RetOutStack ret ++ inp)) cs +toCaseClauseL _ RNil = RNil +toCaseClauseL md (OneFieldIndigoCaseClauseL fn :& rest) = fn md :& toCaseClauseL md rest diff --git a/src/Indigo/Backend/Conditional.hs b/src/Indigo/Backend/Conditional.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Backend/Conditional.hs @@ -0,0 +1,143 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +-- | Conditional statements of Indigo language. + +module Indigo.Backend.Conditional + ( if_ + , ifSome + , ifRight + , ifCons + , IfConstraint + ) where + +import qualified Data.Kind as Kind +import qualified GHC.TypeLits as Lit +import Util.Type (type (++)) + +import Indigo.Backend.Prelude +import Indigo.Backend.Scope +import Indigo.Internal +import Indigo.Lorentz +import qualified Lorentz.Instr as L +import qualified Lorentz.Macro as L + +type family CompareBranchesResults (a :: Kind.Type) (b :: Kind.Type) :: Constraint where + CompareBranchesResults x x = () + CompareBranchesResults x y = Lit.TypeError + ('Lit.Text " Result types of if branches diverged: " + 'Lit.:<>: 'Lit.ShowType x 'Lit.:<>: ('Lit.Text " against ") 'Lit.:<>: 'Lit.ShowType y + ) + +type IfConstraint a b = + ( ScopeCodeGen a + , ScopeCodeGen b + , CompareBranchesResults (RetExprs a) (RetExprs b) + -- These constraints below are implied by the one above, but GHC needs a proof + , RetVars a ~ RetVars b + , RetOutStack a ~ RetOutStack b + ) + +-- | If statement. All variables created inside its branches will be released +-- after the execution leaves the scope in which they were created. +if_ + :: forall inp xs ys a b exc . + ( IfConstraint a b + , exc :~> Bool + ) + => exc + -> IndigoState inp xs a + -> IndigoState inp ys b + -> IndigoState inp (RetOutStack a ++ inp) (RetVars a) +if_ e t f = IndigoState $ \md -> + let cde = gcCode $ runIndigoState (compileToExpr e) md in + let gc1 = runIndigoState t md in + let gc2 = runIndigoState f md in + finalizeStatement @a md (cde # L.if_ (compileScope gc1) (compileScope gc2)) + +-- | If which works like case for Maybe. +ifSome + :: forall inp xs ys x a b exa . + ( IfConstraint a b, KnownValue x + , exa :~> Maybe x + ) + => exa + -> (Var x -> IndigoState (x & inp) xs a) + -> IndigoState inp ys b + -> IndigoState inp (RetOutStack a ++ inp) (RetVars a) +ifSome e t f = IndigoState $ \md -> + let cde = gcCode $ runIndigoState (compileToExpr e) md in + let (v, mdJust) = pushRefMd md in + let gc1 = runIndigoState (t v) mdJust in + let gc2 = runIndigoState f md in + finalizeStatement @a md $ + cde # + L.ifSome + ( compileScope gc1 # + -- after this we have stack (e1 & e2 .. & ek & x & inp) + liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp L.drop + -- this can be lifted together with glClear code, but let's leave it like this for now + ) + (compileScope gc2) + +-- | If which works like case for Either. +ifRight + :: forall inp xs ys x y a b exa . + ( IfConstraint a b, KnownValue x, KnownValue y + , exa :~> Either y x + ) + => exa + -> (Var x -> IndigoState (x & inp) xs a) + -> (Var y -> IndigoState (y & inp) ys b) + -> IndigoState inp (RetOutStack a ++ inp) (RetVars a) +ifRight e r l = IndigoState $ \md -> + let + cde = gcCode $ runIndigoState (compileToExpr e) md + (v, mdRight) = pushRefMd md + (w, mdLeft) = pushRefMd md + gc1 = runIndigoState (r v) mdRight + gc2 = runIndigoState (l w) mdLeft + in + finalizeStatement @a md $ + cde # + L.ifRight + ( compileScope gc1 # + -- after this we have stack (e1 & e2 .. & ek & x & inp) + liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp L.drop + -- this can be lifted together with glClear code, but let's leave it like this for now + ) + ( compileScope gc2 # + -- after this we have stack (e1 & e2 .. & ek & x & inp) + liftClear' @(ClassifyReturnValue b) @b @(y & inp) @inp L.drop + -- this can be lifted together with glClear code, but let's leave it like this for now + ) + +ifCons + :: forall inp xs ys x a b exa . + ( IfConstraint a b + , KnownValue x + , exa :~> List x + ) + => exa + -> (Var x -> Var (List x) -> IndigoState (x & List x & inp) xs a) + -> IndigoState inp ys b + -> IndigoState inp (RetOutStack a ++ inp) (RetVars a) +ifCons e t f = IndigoState $ \md -> + let + cde = gcCode $ runIndigoState (compileToExpr e) md + (l, mdList) = pushRefMd md + (v, mdVal) = pushRefMd mdList + gc1 = runIndigoState (t v l) mdVal + gc2 = runIndigoState f md + in + finalizeStatement @a md $ + cde # + L.ifCons + ( compileScope gc1 # + liftClear' @(ClassifyReturnValue a) @a @(x & List x & inp) @inp (L.drop # L.drop) + ) + (compileScope gc2) + diff --git a/src/Indigo/Backend/Error.hs b/src/Indigo/Backend/Error.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Backend/Error.hs @@ -0,0 +1,153 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +-- | Error related statements of Indigo language. + +module Indigo.Backend.Error + ( failWith + , failUsing_ + , failCustom + , failCustom_ + , failUnexpected_ + , assert + , assertSome + , assertNone + , assertRight + , assertLeft + , assertCustom + , assertCustom_ + ) where + +import Indigo.Backend.Conditional +import Indigo.Backend.Prelude +import Indigo.Internal.Expr.Compilation +import Indigo.Internal.Expr.Types +import Indigo.Internal.State +import Indigo.Lorentz +import qualified Lorentz.Errors as L +import qualified Lorentz.Instr as L + +failIndigoState :: inp :-> out -> IndigoState inp out r +failIndigoState code = iput $ GenCode errOut errMd code failCl + where + -- note: here we can use errors for the output and MetaData, because they + -- are lazy field of GenCode and, due to the way # combines the generated + -- code (ignores everything following a failWith) they won't actually ever + -- be accessed again. The same goes for the "cleaning" code, except it is + -- not lazy and needs to typecheck, so we have to use `failWith` again. + msg = " is undefined after a failing instruction" + errOut = error $ "Output" <> msg + errMd = error $ "MetaData" <> msg + failCl = L.unit # L.failWith + +failWith + :: IsExpr ex a + => ex -> IndigoState s t r +failWith exa = compileToExpr exa >> failIndigoState L.failWith + +failUsing_ :: (IsError x) => x -> IndigoState s t r +failUsing_ x = failIndigoState (failUsing x) + +failCustom + :: forall tag err ex s t r. + ( err ~ ErrorArg tag + , CustomErrorHasDoc tag + , NiceConstant err + , IsExpr ex err + ) + => Label tag -> ex -> IndigoState s t r +failCustom l errEx = withDict (niceConstantEvi @err) $ do + compileToExpr errEx + failIndigoState $ L.failCustom l + +failCustom_ + :: forall tag s t r notVoidErrorMsg. + ( RequireNoArgError tag notVoidErrorMsg + , CustomErrorHasDoc tag + ) + => Label tag -> IndigoState s t r +failCustom_ = failIndigoState . L.failCustom_ + +failUnexpected_ :: MText -> IndigoState s t r +failUnexpected_ msg = failUsing_ $ [mt|Unexpected: |] <> msg + +assert + :: forall s x ex. + ( IsError x + , IsExpr ex Bool + ) + => x -> ex -> IndigoState s s () +assert err e = if_ (toExpr e) (return ()) (failUsing_ err :: IndigoState s s ()) + +assertSome + :: forall x s err ex. + ( IsError err + , KnownValue x + , ex :~> Maybe x + ) + => err -> ex -> IndigoState s s () +assertSome err ex = + ifSome ex + (\_ -> failUsing_ err :: IndigoState (x & s) s ()) + (return ()) + +assertNone + :: forall x s err ex. + ( IsError err + , KnownValue x + , ex :~> Maybe x + ) + => err -> ex -> IndigoState s s () +assertNone err ex = + ifSome ex + (\_ -> return ()) + (failUsing_ err :: IndigoState s s ()) + +assertRight + :: forall x y s err ex. + ( IsError err + , KnownValue x + , KnownValue y + , ex :~> Either y x + ) + => err -> ex -> IndigoState s s () +assertRight err ex = + ifRight ex + (\_ -> failUsing_ err :: IndigoState (x & s) s ()) + (\_ -> return ()) + +assertLeft + :: forall x y s err ex. + ( IsError err + , KnownValue x + , KnownValue y + , ex :~> Either y x + ) + => err -> ex -> IndigoState s s () +assertLeft err ex = + ifRight ex + (\_ -> return ()) + (\_ -> failUsing_ err :: IndigoState (y & s) s ()) + +assertCustom + :: forall tag err errEx ex s. + ( err ~ ErrorArg tag + , CustomErrorHasDoc tag + , NiceConstant err + , IsExpr errEx err + , IsExpr ex Bool + ) + => Label tag -> errEx -> ex -> IndigoState s s () +assertCustom tag errEx e = if_ (toExpr e) (return ()) (failCustom tag errEx :: IndigoState s s ()) + +assertCustom_ + :: forall tag s notVoidErrorMsg ex. + ( RequireNoArgError tag notVoidErrorMsg + , CustomErrorHasDoc tag + , IsExpr ex Bool + ) + => Label tag -> ex -> IndigoState s s () +assertCustom_ tag e = if_ (toExpr e) (return ()) (failCustom_ tag :: IndigoState s s ()) diff --git a/src/Indigo/Backend/Lambda.hs b/src/Indigo/Backend/Lambda.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Backend/Lambda.hs @@ -0,0 +1,238 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | This module implements the ability to put +-- Indigo computations on the stack as a lambda and execute them. +module Indigo.Backend.Lambda + ( LambdaPure1 + , createLambdaPure1 + , CreateLambdaPure1C + , executeLambdaPure1 + , ExecuteLambdaPure1C + , initMetaDataPure + + , Lambda1 + , createLambda1 + , CreateLambda1C + , executeLambda1 + , ExecuteLambda1C + , initMetaData + + , LambdaEff1 + , createLambdaEff1 + , CreateLambdaEff1C + , executeLambdaEff1 + , ExecuteLambdaEff1C + , initMetaDataEff + + , Lambda1Generic + , LambdaExecutor + , LambdaCreator + ) where + +import Data.Constraint (Dict(..)) + +import Indigo.Backend.Prelude +import Indigo.Backend.Scope +import Indigo.Backend.Var +import Indigo.Internal +import Indigo.Lorentz +import qualified Lorentz.Instr as L +import Lorentz.Zip (ZipInstr, ZippedStack) +import Util.Type (type (++), KnownList, listOfTypesConcatAssociativityAxiom) + +---------------------------------------------------------------------------- +-- Pure lambdas +---------------------------------------------------------------------------- + +type LambdaPure1 arg res = Lambda1Generic '[] arg res + +type CreateLambdaPure1C arg res = CreateLambda1CGeneric '[] arg res + +-- | Create a lambda, that takes only one argument, from the given computation. +-- The lambda is not allowed to modify storage and emit operations. +createLambdaPure1 + :: forall res arg inp out . CreateLambdaPure1C arg res + => LambdaCreator '[] arg res inp out +createLambdaPure1 = createLambda1Generic initMetaDataPure + +type ExecuteLambdaPure1C arg res = ExecuteLambda1CGeneric '[] arg res + +-- | Execute a lambda, which accepts only one argument, on passed expression. +executeLambdaPure1 + :: forall res arg inp . ExecuteLambdaPure1C arg res + => LambdaExecutor '[] arg res inp +executeLambdaPure1 = executeLambda1Generic @res (return ()) + +initMetaDataPure :: KnownValue arg => (Var arg, MetaData '[arg]) +initMetaDataPure = let v = Cell 0 in (v, MetaData (Ref 0 :& RNil) 1) + +---------------------------------------------------------------------------- +-- Impure lambda (modifying storage only) +---------------------------------------------------------------------------- + +type Lambda1 st arg res = Lambda1Generic '[st] arg res + +type CreateLambda1C st arg res = (KnownValue st, CreateLambda1CGeneric '[st] arg res) + +-- | Create a lambda, that takes only one argument, from the given computation. +-- The lambda is not allowed to emit operations. +createLambda1 + :: forall st res arg inp out . CreateLambda1C st arg res + => LambdaCreator '[st] arg res inp out +createLambda1 = createLambda1Generic initMetaData + +type ExecuteLambda1C st arg res = + ( IsObject st + , HasStorage st + , ExecuteLambda1CGeneric '[st] arg res + ) + +-- | Execute a lambda that accepts only one argument on the given expression. +executeLambda1 + :: forall st res arg inp . ExecuteLambda1C st arg res + => LambdaExecutor '[st] arg res inp +executeLambda1 = + executeLambda1Generic @res + -- TODO this @compileExpr (V (storageVar @st))@ call materialises the whole decomposed storage. + -- This is pretty expensive operation and it has to be fixed: + -- we have to materialise only fields used in the lambda + (IndigoState $ \md -> + let GenCode _ newMd alloc _ = usingIndigoState md $ compileExpr (V (storageVar @st)) in + let GenCode _ _ cleanup _ = usingIndigoState newMd (makeTopVar >>= (setVar (storageVar @st) . V)) in + GenCode () newMd alloc (cleanup # L.drop) + ) + +initMetaData :: (KnownValue arg, KnownValue st) => (Var arg, MetaData '[arg, st]) +initMetaData = + -- This numeration is intentional. + -- We have to provide HasStorage for a lambda. + -- To avoid excessive 'given' calls with new indexes, + -- we just refer to storage variable with the same index. + let argm = Cell 2 in + (argm, MetaData (Ref 2 :& Ref 1 :& RNil) 3) + +---------------------------------------------------------------------------- +-- Lambda with side effects (might emit operations) +---------------------------------------------------------------------------- + +type LambdaEff1 st arg res = Lambda1Generic '[st, Ops] arg res + +type CreateLambdaEff1C st arg res = (KnownValue st, CreateLambda1CGeneric '[st, Ops] arg res) + +-- | Create a lambda, that takes only one argument, from the given computation, +-- and return a variable referring to this lambda. +-- The lambda is allowed to modify storage and emit operations. +createLambdaEff1 + :: forall st res arg inp out . CreateLambdaEff1C st arg res + => LambdaCreator '[st, Ops] arg res inp out +createLambdaEff1 = createLambda1Generic initMetaDataEff + +type ExecuteLambdaEff1C st arg res = + ( HasStorage st + , HasSideEffects + , IsObject st + , ExecuteLambda1CGeneric '[st, Ops] arg res + ) + +-- | Execute a lambda that accepts only one argument on the given expression. +-- Also updates the storage and operations with the values returned from the lambda. +executeLambdaEff1 + :: forall st res arg inp . ExecuteLambdaEff1C st arg res + => LambdaExecutor '[st, Ops] arg res inp +executeLambdaEff1 = + executeLambda1Generic @res + -- TODO this @compileExpr (V (storageVar @st))@ call materialises the whole decomposed storage. + -- This is pretty expensive operation and it has to be fixed: + -- we have to materialise only fields used in the lambda + (IndigoState $ \md -> + let GenCode _ newMd alloc _ = + usingIndigoState md (do + compileExpr (V operationsVar) + compileExpr (V (storageVar @st))) in + let (newStoreVar, newMdStore) = pushRefMd (pushNoRefMd md) in + let (newOpsVar, newMdOps) = pushRefMd md in + let cleanup = + gcCode (usingIndigoState newMdStore $ setVar (storageVar @st) (V newStoreVar)) # + L.drop # + gcCode (usingIndigoState newMdOps $ setVar operationsVar (V newOpsVar)) # + L.drop + in GenCode () newMd alloc cleanup + ) + +initMetaDataEff :: (KnownValue arg, KnownValue st) => (Var arg, MetaData '[arg, st, Ops]) +initMetaDataEff = + let argm = Cell 2 in + (argm, MetaData (Ref 2 :& Ref 1 :& Ref 0 :& RNil) 3) + +---------------------------------------------------------------------------- +-- Common lambda functionality +---------------------------------------------------------------------------- + +type Lambda1Generic extra arg res = (arg & extra) :-> (RetOutStack res ++ extra) + +type CreateLambda1CGeneric extra arg res = + ( ScopeCodeGen res, KnownValue arg, Typeable extra + , ZipInstr (arg & extra) + , KnownValue (ZippedStack (arg ': extra)) + , KnownValue (ZippedStack (RetOutStack res ++ extra)) + , ZipInstr (RetOutStack res ++ extra) + , Typeable (RetOutStack res ++ extra) + ) + +type LambdaCreator extra arg res inp out + = (Var arg -> IndigoState (arg & extra) out res) + -> IndigoState inp (Lambda1Generic extra arg res & inp) (Var (Lambda1Generic extra arg res)) + +-- | Create a lambda, that takes only one argument, from the given computation, +-- and return a variable referring to this lambda. +createLambda1Generic + :: forall arg res extra inp out . CreateLambda1CGeneric extra arg res + => (Var arg, MetaData (arg & extra)) + -> (Var arg -> IndigoState (arg & extra) out res) + -> IndigoState inp (Lambda1Generic extra arg res & inp) (Var (Lambda1Generic extra arg res)) +createLambda1Generic (varArg, initMd) act = IndigoState $ \md -> + let gc = runIndigoState (act varArg) initMd in + let (var, md1) = pushRefMd md in + GenCode var md1 (L.lambda (compileScope gc # liftClear @res @extra @(arg & extra) L.drop)) L.drop + + +type ExecuteLambda1CGeneric extra arg res = + ( ScopeCodeGen res, KnownValue arg + , KnownValue ((arg & extra) :-> (RetOutStack res ++ extra)) + , KnownList extra + , ZipInstr (arg & extra) + , KnownList (RetOutStack res ++ extra) + , ZipInstr (RetOutStack res ++ extra) + , Typeable (RetOutStack res ++ extra) + , KnownValue (ZippedStack (RetOutStack res ++ extra)) + ) + +type LambdaExecutor extra arg res inp + = Var (Lambda1Generic extra arg res) + -> Expr arg + -> IndigoState inp (RetOutStack res ++ inp) (RetVars res) + +-- | Execute a lambda that accepts only one argument on the given expression. +-- Also updates the storage and operations with the values returned from the lambda. +executeLambda1Generic + :: forall res arg extra inp . ExecuteLambda1CGeneric extra arg res + => IndigoState inp (extra ++ inp) () + -> Var (Lambda1Generic extra arg res) + -> Expr arg + -> IndigoState inp (RetOutStack res ++ inp) (RetVars res) +executeLambda1Generic allocateCleanup varF argm = IndigoState $ \md -> + let GenCode _ allocMd allocate cleanup = runIndigoState allocateCleanup md in + let getArgs = + allocate # + (gcCode $ + usingIndigoState allocMd $ do + compileExpr argm + compileToExpr (V varF)) in + case listOfTypesConcatAssociativityAxiom @(RetOutStack res) @extra @inp of + Dict -> + let code = getArgs # + L.execute @_ @_ @inp # + liftClear @res cleanup + in finalizeStatement @res md code diff --git a/src/Indigo/Backend/Prelude.hs b/src/Indigo/Backend/Prelude.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Backend/Prelude.hs @@ -0,0 +1,14 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | This module is intended to be imported instead of @morley-prelude@ by +-- Backend Indigo modules. +-- +-- This only serves the purpose of listing @hiding@ rules once and avoid boilerplate. + +module Indigo.Backend.Prelude + ( module Prelude + ) where + +import Prelude hiding ((>>), (>>=), (=<<), return) diff --git a/src/Indigo/Backend/Scope.hs b/src/Indigo/Backend/Scope.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Backend/Scope.hs @@ -0,0 +1,237 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +-- | Machinery that provides the ability to return values from Indigo statements +-- (like @if@, @case@, @while@, etc). +-- You are allowed to return unit, one expression or a tuple of expressions. +-- For instance: +-- +-- @ +-- (a, b) <- if flag +-- then do +-- anotherFlag <- newVar True +-- return (5 +. var, anotherFlag ||. True) +-- else return (0, anotherVar) +-- @ +-- is a valid construction. +-- Pay attention to the fact that @5 +. var@ has the type 'Expr' 'Integer', +-- but 0 is just an 'Integer' and @anotherFlag ||. True@ has type 'Expr' 'Bool', +-- but @anotherVar@ has type 'Var' 'Bool'; and this code will compile anyway. +-- This is done intentionally to avoid the burden of manually converting values +-- to expressions (or variables). +-- So you can write the same constructions as in a regular language. + +module Indigo.Backend.Scope + ( BranchRetKind (..) + , ScopeCodeGen + , ScopeCodeGen' (..) + , ReturnableValue + , ReturnableValue' (..) + , RetOutStack + , RetVars + , RetExprs + , ClassifyReturnValue + , liftClear + , compileScope + , allocateVars + , finalizeStatement + ) where + +import qualified Data.Kind as Kind +import qualified GHC.TypeLits as Lit +import Util.Type (type (++)) + +import Indigo.Backend.Prelude +import Indigo.Internal.Expr +import Indigo.Internal.Object +import Indigo.Internal.State +import Indigo.Lorentz +import qualified Lorentz.Instr as L + +-- | To avoid overlapping instances we need to somehow distinguish single values +-- from tuples, because the instances: +-- +-- @ +-- instance Something a +-- instance Something (a, b) +-- @ +-- overlap and adding @{-\# OVERLAPPING \#-}@ doesn't rescue in some cases, +-- especially for type families defined in @Something@. +data BranchRetKind = + Unit + -- ^ If value is unit (don't return anything) + | SingleVal + -- ^ If it's a single value (not tuple) + | Tuple + -- ^ If it's tuple (we don't care how many elements are in) + +-- | This type family returns a promoted value of type 'BranchRetKind' +-- or causes a compilation error if a tuple with too many elements is used. +type family ClassifyReturnValue (ret :: Kind.Type) where + ClassifyReturnValue () = 'Unit + ClassifyReturnValue (_, _) = 'Tuple + -- These type errors are an attempt to make compilation errors clear + -- in cases where one tries to return a tuple with more elements from a statement + ClassifyReturnValue (_, _, _) = 'Tuple + ClassifyReturnValue (_, _, _, _) = + Lit.TypeError ('Lit.Text "Tuple with 4 elements is not supported yet as returning value") + ClassifyReturnValue (_, _, _, _, _) = + Lit.TypeError ('Lit.Text "Tuple with 5 elements is not supported yet as returning value") + ClassifyReturnValue (_, _, _, _, _, _) = + Lit.TypeError ('Lit.Text "Tuple with 6 elements is not supported yet as returning value") + -- I hope nobody will try to return as a value tuples with more elements + ClassifyReturnValue _ = 'SingleVal + +-- | Class for values that can be returned from Indigo statements. +-- They include @()@ and tuples. +class ReturnableValue' (retKind :: BranchRetKind) (ret :: Kind.Type) where + -- | Type family reflecting the top elements of stack produced by + -- a statement returning the value. + type family RetOutStack' retKind ret :: [Kind.Type] + + -- | Type family reflecting the returning value from a statement. + type family RetVars' retKind ret :: Kind.Type + + -- | Tuple looking like @(Expr x, Expr y, ..)@ that corresponds + -- to expressions returning from the scope. + -- 'RetVars\'' and 'RetExprs\'' are twin types because + -- the former just adds 'Var' over each expression of the latter. + type family RetExprs' retKind ret :: Kind.Type + + -- | Allocate variables referring to result of the statement. + allocateVars' + :: (forall inpt x . KnownValue x => MetaData inpt -> (Var x, MetaData (x & inpt))) -- ^ Single variable allocator + -> MetaData inp + -> (RetVars' retKind ret, MetaData (RetOutStack' retKind ret ++ inp)) + +-- | Type class which unions all related management of computations in a scope, +-- like in @if@ branch, in @case@ body, etc. +-- +-- Particularly, it takes care of the computation of expressions returning +-- from a scope to leave it safely. +-- Basically, this type class encapsulates the generation of Lorentz code that looks like: +-- +-- @ +-- branch_code # +-- -- we get some arbitrary type of a stack here, lets call it @xs@ +-- compute_returning_expressions # +-- -- we get type of stack [e1, e2, ... ek] ++ xs +-- cleanup_xs_to_inp +-- -- we get [e1, e2, e3, ..., ek] ++ inp +-- @ +class ReturnableValue' retKind ret => ScopeCodeGen' (retKind :: BranchRetKind) (ret :: Kind.Type) where + -- | Produces an Indigo computation that puts on the stack + -- the evaluated returned expressions from the leaving scope. + compileScopeReturn' :: ret -> IndigoState xs (RetOutStack' retKind ret ++ xs) () + + -- | Drop the stack cells that were produced in the leaving scope, + -- apart from ones corresponding to the returning expressions. + liftClear' :: (xs :-> inp) -> (RetOutStack' retKind ret ++ xs :-> RetOutStack' retKind ret ++ inp) + + -- | Generate 'gcClear' for the whole statement + genGcClear' :: (RetOutStack' retKind ret ++ inp) :-> inp + +type RetOutStack ret = RetOutStack' (ClassifyReturnValue ret) ret +type RetVars ret = RetVars' (ClassifyReturnValue ret) ret +type RetExprs ret = RetExprs' (ClassifyReturnValue ret) ret +type ReturnableValue ret = ReturnableValue' (ClassifyReturnValue ret) ret +type ScopeCodeGen ret = ScopeCodeGen' (ClassifyReturnValue ret) ret + +-- | Specific version of 'allocateVars\'' +allocateVars + :: forall ret inp . ReturnableValue ret + => (forall inpt x . KnownValue x => MetaData inpt -> (Var x, MetaData (x & inpt))) -- Single variable allocator + -> MetaData inp + -> (RetVars ret, MetaData (RetOutStack ret ++ inp)) +allocateVars = allocateVars' @(ClassifyReturnValue ret) @ret + +-- | Specific version of 'liftClear\'' +liftClear + :: forall ret inp xs . ScopeCodeGen ret + => (xs :-> inp) + -> (RetOutStack ret ++ xs :-> RetOutStack ret ++ inp) +liftClear = liftClear' @(ClassifyReturnValue ret) @ret + +-- | Concatenate a scoped code, generation of returning expressions, +-- and clean up of redundant cells from the stack. +compileScope + :: forall ret inp xs . ScopeCodeGen ret + => GenCode inp xs ret + -> (inp :-> RetOutStack ret ++ inp) +compileScope gc = + gcCode gc # + gcCode (runIndigoState (compileScopeReturn' @(ClassifyReturnValue ret) (gcOut gc)) (gcMeta gc)) # + liftClear' @(ClassifyReturnValue ret) @ret (gcClear gc) + +-- | Push a variables in 'MetaData', referring to the generated expressions, +-- and generate 'gcClear' for the whole statement. +finalizeStatement + :: forall ret inp . ScopeCodeGen ret + => MetaData inp + -> (inp :-> RetOutStack ret ++ inp) + -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret) +finalizeStatement md code = + let (vars, newMd) = allocateVars' @(ClassifyReturnValue ret) @ret pushRefMd md in + GenCode vars newMd code (genGcClear' @(ClassifyReturnValue ret) @ret) + +-- Type instances for ScopeCodeGen'. +-- Perhaps, they could be implemented more succinctly +-- and expressed inductively via previous instances, +-- but I don't think it makes sense to spend a lot of time to shorten them. + +type KnownValueExpr a = (KnownValue (ExprType a), ToExpr a) + +instance ReturnableValue' 'Unit () where + type RetOutStack' 'Unit () = '[] + type RetVars' 'Unit () = () + type RetExprs' 'Unit () = () + allocateVars' _ md = ((), md) + +instance ScopeCodeGen' 'Unit () where + compileScopeReturn' _ = return () + liftClear' = id + genGcClear' = L.nop + +instance KnownValueExpr single => ReturnableValue' 'SingleVal single where + type RetOutStack' 'SingleVal single = '[ExprType single] + type RetVars' 'SingleVal single = Var (ExprType single) + type RetExprs' 'SingleVal single = ExprType single + allocateVars' allocator = allocator + +instance KnownValueExpr single => ScopeCodeGen' 'SingleVal single where + compileScopeReturn' = compileToExpr + liftClear' = L.dip + genGcClear' = L.drop + +instance (KnownValueExpr x, KnownValueExpr y) => ReturnableValue' 'Tuple (x, y) where + type RetOutStack' 'Tuple (x, y) = ExprType x ': '[ExprType y] + type RetVars' 'Tuple (x, y) = (Var (ExprType x), Var (ExprType y)) + type RetExprs' 'Tuple (x, y) = (ExprType x, ExprType y) + allocateVars' allocator md = + let (var2, newMd1) = allocator md in + let (var1, newMd2) = allocator newMd1 in + ((var1, var2), newMd2) + +instance (KnownValueExpr x, KnownValueExpr y) => ScopeCodeGen' 'Tuple (x, y) where + compileScopeReturn' (e1, e2) = compileToExpr e2 >> compileToExpr e1 + -- TODO is L.dip . L.dip cheaper than L.dipN ? + liftClear' = L.dip . L.dip + genGcClear' = L.drop # L.drop + +instance (KnownValueExpr x, KnownValueExpr y, KnownValueExpr z) => ReturnableValue' 'Tuple (x, y, z) where + type RetOutStack' 'Tuple (x, y, z) = ExprType x ': ExprType y ': '[ExprType z] + type RetVars' 'Tuple (x, y, z) = (Var (ExprType x), Var (ExprType y), Var (ExprType z)) + type RetExprs' 'Tuple (x, y, z) = (ExprType x, ExprType y, ExprType z) + allocateVars' allocator md = + let (var3, newMd1) = allocator md in + let (var2, newMd2) = allocator newMd1 in + let (var1, newMd3) = allocator newMd2 in + ((var1, var2, var3), newMd3) + +instance (KnownValueExpr x, KnownValueExpr y, KnownValueExpr z) => ScopeCodeGen' 'Tuple (x, y, z) where + compileScopeReturn' (e1, e2, e3) = compileToExpr e3 >> compileToExpr e2 >> compileToExpr e1 + liftClear' = L.dipN @3 + genGcClear' = L.drop # L.drop # L.drop diff --git a/src/Indigo/Backend/Var.hs b/src/Indigo/Backend/Var.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Backend/Var.hs @@ -0,0 +1,100 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Backend of the statements to create and modify variables +module Indigo.Backend.Var + ( newVar + , setVar + , setField + , updateVar + ) where + +import Indigo.Backend.Prelude +import Indigo.Internal +import Indigo.Lorentz +import qualified Lorentz.Instr as L +import Michelson.Typed.Haskell.Instr.Product (GetFieldType) +import Util.Type (type (++)) + +-- | Create a new variable with passed expression as an initial value. +newVar :: IsExpr ex x => ex -> IndigoState inp (x & inp) (Var x) +newVar e = compileToExpr e >> makeTopVar + +-- | Set the variable to a new value. +-- +-- If a variable is a cell on the stack, +-- we just compile passed expression and replace variable cell on stack. +-- If a variable is decomposed, we decompose passed expression +-- and call 'setVar' recursively from its fields. +setVar + :: forall a ex inp . ex :~> a + => Var a -> ex -> IndigoState inp inp () +setVar (Cell refId) e = do + MetaData s _ <- iget + unaryOpFlat e $ varActionSet refId s +setVar (Decomposed fields) ex = case decomposeExpr (toExpr ex) of + ExprFields fieldsExpr -> + rmapZipM (namedToTypedRec @a namedToTypedFieldVar fields) fieldsExpr + Deconstructed comp -> + IndigoState $ \md -> + let GenCode _ decomposeMd decomposeExCd _ = usingIndigoState md comp in + let setAllFieldsCd = setFieldsOnStack (namedToTypedRec @a namedToTypedFieldVar fields) decomposeMd in + GenCode () md (decomposeExCd # setAllFieldsCd) L.nop + where + -- Set fields, if they are decomposed on stack. + setFieldsOnStack :: forall rs . Rec TypedFieldVar rs -> MetaData (rs ++ inp) -> (rs ++ inp) :-> inp + setFieldsOnStack RNil _ = L.nop + setFieldsOnStack (TypedFieldVar f :& vs) md = + let (val, setVarMd) = pushRefMd (popNoRefMd md) in + let setVarCd = gcCode $ usingIndigoState setVarMd $ setVar f (V val) in + setVarCd # + L.drop # + setFieldsOnStack vs (popNoRefMd md) + + -- Take list of fields (variables, referring to them) + -- and list of corresponding expressions and call 'setVar' recursively. + rmapZipM :: Rec TypedFieldVar rs -> Rec Expr rs -> IndigoState inp inp () + rmapZipM RNil RNil = return () + rmapZipM (TypedFieldVar f :& flds) (e :& exprs) = setVar f e >> rmapZipM flds exprs + +-- | Set the field (direct or indirect) of a complex object. +setField :: + forall dt fname ftype ex inp . + ( ex :~> ftype + , IsObject dt + , IsObject ftype + , HasField dt fname ftype + ) + => Var dt -> Label fname -> ex -> IndigoState inp inp () +setField v@(Cell _) lb ex = updateVar (sopSetField (flSFO fieldLens) lb) v ex +setField (Decomposed fields) targetLb ex = case fieldLens @dt @fname @ftype of + TargetField lb _ -> + case fetchField @dt lb fields of + NamedFieldVar v -> + setVar v ex + DeeperField (lb :: Label fnameInterm) _ -> + case fetchField @dt lb fields of + NamedFieldVar vf -> + setField @(GetFieldType dt fnameInterm) @fname @ftype vf targetLb ex + +-- | Call binary operator with constant argument to update variable in-place. +updateVar + :: (IsExpr ey y, IsObject x) + => [y, x] :-> '[x] + -> Var x + -> ey + -> IndigoState inp inp () +updateVar action (Cell refId) e = do + MetaData s _ <- iget + unaryOpFlat e $ varActionUpdate refId s action +-- This function doesn't have to be called for complex data types, +-- it's only supposed to be used for assign-like statements +-- (+=), (-=), etc. +-- But it's implemented just in case. +updateVar action v@(Decomposed _) e = IndigoState $ \md -> + let (var, newMd) = pushRefMd md in + usingIndigoState md $ binaryOpFlat e (V v) $ + L.framed action # + gcCode (usingIndigoState newMd (setVar v (V var))) # + L.drop diff --git a/src/Indigo/Compilation.hs b/src/Indigo/Compilation.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Compilation.hs @@ -0,0 +1,264 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | This module contains everything related to compilation from Indigo to Lorentz, +-- including plain Indigo code, as well as Indigo contracts. + +module Indigo.Compilation + ( compileIndigo + , IndigoWithParams + , IndigoContract + , compileIndigoContract + + , Ops + , HasSideEffects + , operationsVar + , HasStorage + , storageVar + ) where + +import qualified Data.Map as M +import Data.Reflection (give) +import qualified Data.Set as S +import Data.Singletons (SingI(..)) +import Data.Typeable ((:~:)(..), eqT) +import Data.Vinyl.Core (RMap(..)) + +import qualified Indigo.Backend as B +import Indigo.Compilation.Lambda +import Indigo.Compilation.Params +import Indigo.Frontend.Program (IndigoM(..), Program(..)) +import Indigo.Frontend.Statement +import Indigo.Internal hiding (SetField, return, (>>), (>>=)) +import qualified Indigo.Internal as I +import Indigo.Lorentz +import Indigo.Prelude +import qualified Lorentz.Instr as L +import qualified Lorentz.Macro as L +import Util.Peano + +-- | Iteration over Indigo freer monad +compileIndigoM + :: forall inp a . + (forall x anyInp . StatementF IndigoM x -> SomeIndigoState anyInp x) + -> IndigoM a + -> SomeIndigoState inp a +compileIndigoM _ (IndigoM (Done a)) = returnSIS a +compileIndigoM interp (IndigoM (Instr i)) = interp i +compileIndigoM interp (IndigoM (Bind instr cont)) = + compileIndigoM interp (IndigoM instr) `bindSIS` (compileIndigoM interp . IndigoM . cont) + +-- | Convert frontend Freer to 'IndigoState'. +-- +-- First of all, this function generates the definitions of +-- lambdas, creates the variables that refer to them +-- and calls them in the places where they are used. +-- This happens only for those lambdas that are called +-- at least twice, those that are used only once will be +-- inlined instead. +-- +-- After that the generation of the body code starts. +simpleCompileIndigoM :: forall inp a . IndigoM a -> SomeIndigoState inp a +simpleCompileIndigoM indigoM = + let lambdas = S.toList (collectLambdas indigoM) in + forMSIS lambdas defineLambda + `bindSIS` + (\defined -> + let definedLambdas = M.fromList $ map (\l -> (_clName l, l)) defined + in compileBody definedLambdas indigoM + ) + where + compileBody definedLambdas = compileIndigoM (usingReader definedLambdas . compileSt) + + compileSt :: StatementF IndigoM x -> Reader (Map String CompiledLambda) (SomeIndigoState anyInp x) + compileSt (LiftIndigoState cd) = pure cd + compileSt (NewVar ex) = pure $ toSIS (B.newVar ex) + compileSt (SetVar v ex) = pure $ toSIS (B.setVar v ex) + compileSt (SetField v fName ex) = pure $ toSIS (B.setField v fName ex) + compileSt (VarModification act var ex) = pure $ toSIS (B.updateVar act var ex) + + compileSt (LambdaPure1Call lName (body :: (Var arg -> IndigoM res)) argm) = + execGenericLambda @'[] @res (B.executeLambdaPure1 @res) lName body argm + + compileSt (Lambda1Call (_ :: Proxy st) lName (body :: (Var arg -> IndigoM res)) argm) = + execGenericLambda @'[st] @res (B.executeLambda1 @st @res) lName body argm + + compileSt (LambdaEff1Call (_ :: Proxy st) lName (body :: (Var arg -> IndigoM res)) argm) = + execGenericLambda @'[st, Ops] @res (B.executeLambdaEff1 @st @res) lName body argm + + compileSt (Scope cd) = do + definedLambdas <- ask + pure $ withSIS (compileBody definedLambdas cd) (toSIS . B.scope) + compileSt (If ex tb fb) = do + definedLambdas <- ask + pure $ withSIS (compileBody definedLambdas tb) $ \tb' -> + withSIS (compileBody definedLambdas fb) $ \fb' -> + toSIS (B.if_ ex tb' fb') + compileSt (IfSome ex tb fb) = do + definedLambdas <- ask + pure $ withSIS1 (compileBody definedLambdas . tb) $ \tb' -> + withSIS (compileBody definedLambdas fb) $ \fb' -> + toSIS (B.ifSome ex tb' fb') + compileSt (IfRight ex rb lb) = do + definedLambdas <- ask + pure $ withSIS1 (compileBody definedLambdas . rb) $ \rb' -> + withSIS1 (compileBody definedLambdas . lb) $ \lb' -> + toSIS (B.ifRight ex rb' lb') + compileSt (IfCons ex tb fb) = do + definedLambdas <- ask + pure $ withSIS2 (\x y -> compileBody definedLambdas $ tb x y) $ \tb' -> + withSIS (compileBody definedLambdas fb) $ \fb' -> + toSIS (B.ifCons ex tb' fb') + compileSt (Case grd clauses) = do + definedLambdas <- ask + pure $ toSIS $ B.caseRec grd (rmapClauses definedLambdas clauses) + compileSt (EntryCase proxy grd clauses) = do + definedLambdas <- ask + pure $ toSIS $ B.entryCaseRec proxy grd (rmapClauses definedLambdas clauses) + compileSt (EntryCaseSimple grd clauses) = do + definedLambdas <- ask + pure $ toSIS $ B.entryCaseSimpleRec grd (rmapClauses definedLambdas clauses) + + compileSt (While ex body) = do + definedLambdas <- ask + pure $ withSIS (compileBody definedLambdas body) $ \bd -> toSIS (B.while ex bd) + compileSt (WhileLeft ex lb) = do + definedLambdas <- ask + pure $ + withSIS1 (compileBody definedLambdas . lb) $ \lb' -> do + toSIS (B.whileLeft ex lb') + compileSt (ForEach e body) = do + definedLambdas <- ask + pure $ withSIS1 (compileBody definedLambdas . body) $ \bd -> toSIS (B.forEach e bd) + + compileSt (ContractName cName contr) = do + definedLambdas <- ask + pure $ withSIS (compileBody definedLambdas contr) $ toSIS . B.contractName cName + compileSt (DocGroup gr ii) = do + definedLambdas <- ask + pure $ withSIS (compileBody definedLambdas ii) $ toSIS . B.docGroup gr + compileSt (ContractGeneral contr) = do + definedLambdas <- ask + pure $ withSIS (compileBody definedLambdas contr) (toSIS . B.contractGeneral) + compileSt (FinalizeParamCallingDoc entrypoint param) = do + definedLambdas <- ask + pure $ withSIS1 (compileBody definedLambdas . entrypoint) + (\bd -> toSIS $ B.finalizeParamCallingDoc bd param) + + compileSt (TransferTokens expar exm exc) = pure $ toSIS (B.transferTokens expar exm exc) + compileSt (SetDelegate kh) = pure $ toSIS (B.setDelegate kh) + compileSt (CreateContract lCtr ek em es) = pure $ toSIS $ + I.iget I.>>= \(MetaData s _) -> + ternaryOp ek em es (L.createContract lCtr + # varActionOperation (NoRef :& s)) + I.>> makeTopVar + compileSt (ContractCalling (_ :: Proxy cp) ref addr) = pure $ toSIS $ B.contractCalling @cp ref addr + + compileSt (FailWith ex) = pure $ toSIS $ B.failWith ex + compileSt (Assert err expr) = pure $ toSIS $ B.assert err expr + compileSt (FailCustom l expr) = pure $ toSIS $ B.failCustom l expr + + rmapClauses:: forall ret cs . RMap cs + => Map String CompiledLambda + -> Rec (IndigoMCaseClauseL IndigoM ret) cs + -> Rec (B.IndigoCaseClauseL ret) cs + rmapClauses definedLambdas = rmap (\(OneFieldIndigoMCaseClauseL cName clause) -> + cName /-> (\v -> B.IndigoAnyOut $ compileBody definedLambdas $ clause v)) + + forMSIS :: [r] -> (forall someInp . r -> SomeIndigoState someInp v) -> SomeIndigoState someInp1 [v] + forMSIS [] _ = returnSIS [] + forMSIS (x : xs) f = f x `bindSIS` (\what -> (what :) <$> forMSIS xs f) + + defineLambda :: Lambda1Def -> SomeIndigoState someOut CompiledLambda + defineLambda (LambdaPure1Def (_ :: Proxy (_s, arg, res)) lName fun) = + defineGenericLambda @'[] B.initMetaDataPure B.createLambdaPure1 lName fun + defineLambda (Lambda1Def (_ :: Proxy (st, arg, res)) lName fun) = + defineGenericLambda @'[st] B.initMetaData B.createLambda1 lName fun + defineLambda (LambdaEff1Def (_ :: Proxy (st, arg, res)) lName fun) = + defineGenericLambda @'[st, Ops] B.initMetaDataEff B.createLambdaEff1 lName fun + + defineGenericLambda + :: forall extra res arg someOut . + (Typeable arg, Typeable res, Typeable extra) + => (Var arg, MetaData (arg & extra)) + -> (forall inpt out . B.LambdaCreator extra arg res inpt out) + -> String + -> (Var arg -> IndigoM res) + -> SomeIndigoState someOut CompiledLambda + defineGenericLambda (varArg, initMd) lambdaCreator lName fun = do + runSIS + (simpleCompileIndigoM $ fun varArg) initMd + (\gc -> toSIS $ lambdaCreator (\_v -> IndigoState $ \_md -> gc)) + `bindSIS` + (returnSIS . CompiledLambda (Proxy @res) lName) + + execGenericLambda + :: forall extra res arg someOut . + (Typeable extra, KnownValue arg, Typeable res, B.ScopeCodeGen res) + => (forall inpt . B.LambdaExecutor extra arg res inpt) + -> String + -> (Var arg -> IndigoM res) + -> Expr arg + -> Reader (Map String CompiledLambda) (SomeIndigoState someOut (B.RetVars res)) + execGenericLambda executor lName (body :: (Var arg -> IndigoM res)) (argm :: Expr arg) = do + compiled <- ask + let maybeToRight' = flip maybeToRight + -- This code seems to be pretty unsafe, but it works almost inevitably + pure $ either (error . fromString) id $ do + case M.lookup lName compiled of + Nothing -> Right $ + -- Just inline lambda without calling Lorentz lambda + withSIS1 (compileBody compiled . body) + (\bd -> toSIS $ B.newVar argm I.>>= (B.scope @res . bd)) + Just compLam -> case compLam of + CompiledLambda (_ :: Proxy res1) _ (varF :: Var (B.Lambda1Generic extra1 arg1 res1)) -> do + Refl <- maybeToRight' (eqT @res @res1) ("unexpected result type of " ++ lName ++ " lambda didn't match") + Refl <- maybeToRight' (eqT @arg @arg1) ("unexpected argument type of " ++ lName ++ " lambda didn't match") + Refl <- maybeToRight' (eqT @extra @extra1) ("unexpected storage type of " ++ lName ++ " lambda didn't match") + pure $ toSIS (executor varF argm) + +-- | Compile Indigo code to Lorentz. +-- +-- Note: it is necessary to specify the number of parameters (using the first +-- type variable) of the Indigo function. Also, these should be on the top of +-- the input stack in inverse order (see 'IndigoWithParams'). +compileIndigo + :: forall n inp a. + ( SingI (ToPeano n), Default (MetaData inp) + , AreIndigoParams (ToPeano n) inp, KnownValue a + ) + => IndigoWithParams (ToPeano n) inp a + -> inp :-> inp +compileIndigo paramCode = + runSIS (simpleCompileIndigoM code) md cleanGenCode + where + (code, md) = fromIndigoWithParams @inp @_ @a paramCode def (sing @(ToPeano n)) + +-- | Type of a contract that can be compiled to Lorentz with 'compileIndigoContract'. +type IndigoContract param st = + (HasStorage st, HasSideEffects) => Var param -> IndigoM () + +-- | Compile Indigo code to Lorentz contract. +-- Drop elements from the stack to return only @[Operation]@ and @storage@. +compileIndigoContract + :: forall param st . + ( KnownValue param + , IsObject st + ) + => IndigoContract param st + -> ContractCode param st +compileIndigoContract code = + let (varOps, opsMd) = pushRefMd emptyMetadata + mdSt = pushNoRefMd opsMd in + -- Decompose storage value first, run contract and then compose it back. + runSIS (deepDecomposeCompose @st) mdSt $ \(GenCode varSt decomposedMd decomposeSt composeSt) -> + let (varParam, initMd) = pushRefMd decomposedMd + everythingGiven = (give @(Var Ops) varOps $ give @(Var st) varSt code) varParam + indigoCode = runSIS (simpleCompileIndigoM everythingGiven) initMd cleanGenCode in + L.nil # L.swap # L.unpair # + L.dip decomposeSt # -- decompose storage + indigoCode # -- run indigo code + L.drop # -- drop param + composeSt # -- compose storage back + L.swap # L.pair diff --git a/src/Indigo/Compilation/Lambda.hs b/src/Indigo/Compilation/Lambda.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Compilation/Lambda.hs @@ -0,0 +1,154 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Indigo.Compilation.Lambda + ( CompiledLambda (..) + , Lambda1Def (..) + , collectLambdas + ) where + +import Prelude +import qualified Data.Map as M + +import Indigo.Backend as B +import Indigo.Frontend.Program (IndigoM(..), interpretProgram) +import Indigo.Frontend.Statement +import Indigo.Internal.Object +import Indigo.Internal.SIS +import Indigo.Internal.State hiding ((>>)) +import Indigo.Lorentz + +data CompiledLambda where + CompiledLambda + :: (Typeable arg, Typeable res, Typeable extra) + => { _clProxyRes :: Proxy res + , _clName :: String + , _clVarLam :: Var (B.Lambda1Generic extra arg res) + } -> CompiledLambda + +data Lambda1Def where + LambdaPure1Def + :: (Typeable res, CreateLambdaPure1C arg res) + => { _ldProxy :: Proxy (_stUnit, arg, res) + , _ldName :: String + , _ldBody :: Var arg -> IndigoM res + } -> Lambda1Def + + Lambda1Def + :: (Typeable res, CreateLambda1C st arg res) + => { _ldProxy :: Proxy (st, arg, res) + , _ldName :: String + , _ldBody :: Var arg -> IndigoM res + } -> Lambda1Def + + LambdaEff1Def + :: (Typeable res, CreateLambdaEff1C st arg res) + => { _ldProxy :: Proxy (st, arg, res) + , _ldName :: String + , _ldBody :: Var arg -> IndigoM res + } -> Lambda1Def + +instance Eq Lambda1Def where + (==) l1 l2 = _ldName l1 == _ldName l2 + +instance Ord Lambda1Def where + (<=) l1 l2 = _ldName l1 <= _ldName l2 + +-- | This is a hack, which prevents using +-- a variable from an outer scope in a body of the lambda. +-- This is not needed when a lambda is defined as top level function, +-- but made just in case, if one wanted to define something like this: +-- +-- @ +-- f :: Var Storage -> IndigoM () +-- f storage = do +-- field <- getStorageField +-- let lambda = defNamedLambda1 $ \arg -> ... using field here ... +-- @ +-- The idea is that when we pass this variable in +-- a bind it will be propagated in all expressions, +-- including the ones that are in the lambdas. +-- An error will be raised during a variable lookup. +-- This hack will be rewritten later. +leakedVar :: KnownValue a => Var a +leakedVar = Cell $ + error "In a scope of function you are using a variable from an outer scope. Closures are not supported yet." + +leakedScopeVariableAllocator :: KnownValue a => MetaData _inp -> (Var a, MetaData (a & _inp)) +leakedScopeVariableAllocator (MetaData stk cnt) = + let v = leakedVar + in (v, MetaData (Ref cnt :& stk) (cnt + 1)) + +allocateVarsLeaked :: forall a . ReturnableValue a => RetVars a +allocateVarsLeaked = fst (allocateVars @a leakedScopeVariableAllocator emptyMetadata) + +allocateVarsLeakedM :: forall a m . (Monad m, ReturnableValue a) => m a -> m (RetVars a) +allocateVarsLeakedM ma = allocateVarsLeaked @a <$ ma + +-- | Collect all used lambdas in a computation +-- (which might be either a contract body or another function body), +-- which are called at least twice. +-- Only outer functions will be gathered, for instance, +-- if we call lambda func1 from func0, only func0 will be taken. +collectLambdas :: forall a . IndigoM a -> Set Lambda1Def +collectLambdas indigoM = + M.keysSet $ M.filter (> 1) $ executingState mempty (lookForLambdas indigoM) + where + lookForLambdas :: IndigoM x -> State (Map Lambda1Def Word) x + lookForLambdas (IndigoM program) = interpretProgram inspectLambda program + + inspectLambda :: StatementF IndigoM x -> State (Map Lambda1Def Word) x + inspectLambda (LambdaPure1Call name (body :: (Var arg -> IndigoM res)) _) = + allocateVarsLeaked @res <$ modify (addLambda (LambdaPure1Def (Proxy @((), arg, res)) name body)) + + inspectLambda (Lambda1Call (_ :: Proxy st) name (body :: (Var arg -> IndigoM res)) _) = + allocateVarsLeaked @res <$ modify (addLambda (Lambda1Def (Proxy @(st, arg, res)) name body)) + + inspectLambda (LambdaEff1Call (_ :: Proxy st) name (body :: (Var arg -> IndigoM res)) _) = + allocateVarsLeaked @res <$ modify (addLambda (LambdaEff1Def (Proxy @(st, arg, res)) name body)) + + inspectLambda (Scope cd) = allocateVarsLeakedM $ lookForLambdas cd + inspectLambda (If _ tb fb) = allocateVarsLeakedM $ lookForLambdas tb >> lookForLambdas fb + inspectLambda (IfSome _ tb fb) = allocateVarsLeakedM $ lookForLambdas (tb leakedVar) >> lookForLambdas fb + inspectLambda (IfRight _ rb lb) = allocateVarsLeakedM $ lookForLambdas (rb leakedVar) >> lookForLambdas (lb leakedVar) + inspectLambda (IfCons _ tb fb) = allocateVarsLeakedM $ lookForLambdas (tb leakedVar leakedVar) >> lookForLambdas fb + inspectLambda (Case _ clauses) = rmapClauses clauses + inspectLambda (EntryCase _ _ clauses) = rmapClauses clauses + inspectLambda (EntryCaseSimple _ clauses) = rmapClauses clauses + inspectLambda (While _ body) = lookForLambdas body + inspectLambda (WhileLeft _ body) = lookForLambdas (body leakedVar) >> pure leakedVar + inspectLambda (ForEach _ body) = lookForLambdas $ body leakedVar + inspectLambda (ContractName _ contr) = lookForLambdas contr + inspectLambda (DocGroup _ ii) = lookForLambdas ii + inspectLambda (ContractGeneral contr) = lookForLambdas contr + inspectLambda (FinalizeParamCallingDoc entrypoint _) = lookForLambdas (entrypoint leakedVar) + + -- Not recursive simple statements. They are terminal ones + inspectLambda (LiftIndigoState cd) = pure $ runSIS cd emptyMetadata gcOut + inspectLambda (NewVar _) = pure leakedVar + inspectLambda (SetVar _ _) = pure () + inspectLambda (SetField {}) = pure () + inspectLambda (VarModification {}) = pure () + inspectLambda (TransferTokens {}) = pure () + inspectLambda (SetDelegate _) = pure () + inspectLambda (CreateContract{}) = pure leakedVar + inspectLambda (ContractCalling{}) = pure leakedVar + + inspectLambda (FailWith ex) = pure $ gcOut $ runIndigoState (B.failWith ex) emptyMetadata + inspectLambda (Assert _ _) = pure () + inspectLambda (FailCustom tag ex) = pure $ gcOut $ runIndigoState (B.failCustom tag ex) emptyMetadata + + rmapClauses:: forall ret cs . ReturnableValue ret + => Rec (IndigoMCaseClauseL IndigoM ret) cs + -> State (Map Lambda1Def Word) (RetVars ret) + rmapClauses RNil = pure (allocateVarsLeaked @ret) + rmapClauses ((OneFieldIndigoMCaseClauseL _ clause) :& rs) = + lookForLambdas (clause leakedVar) >> rmapClauses rs + + addLambda :: Lambda1Def -> Map Lambda1Def Word -> Map Lambda1Def Word + addLambda = + M.alter (\case + Nothing -> Just 1 + Just x -> Just (x + 1) + ) diff --git a/src/Indigo/Compilation/Params.hs b/src/Indigo/Compilation/Params.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Compilation/Params.hs @@ -0,0 +1,67 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Indigo.Compilation.Params + ( IndigoWithParams + , AreIndigoParams + , fromIndigoWithParams + ) where + +import Data.Singletons (Sing) +import Data.Typeable ((:~:)(..), eqT) + +import Indigo.Backend.Prelude +import Indigo.Frontend.Program (IndigoM) +import Indigo.Internal.Object +import Indigo.Internal.State +import Indigo.Lorentz +import Util.Peano + +---------------------------------------------------------------------------- +-- Utility for compatibility with Lorentz +---------------------------------------------------------------------------- + +-- | Type of a function with @n@ 'Var' arguments and @IndigoM a@ result. +-- +-- Note that the arguments are the first @n@ elements of the @inp@ stack in +-- inverse order, for example: +-- @IndigoWithParams (\'S (\'S \'Z)) \'[a, b, c] x@ is the same as: +-- @Var b -> Var a -> IndigoM x@ +type family IndigoWithParams n inp a where + IndigoWithParams 'Z _ a = IndigoM a + IndigoWithParams ('S n) inp a = Var (At n inp) -> IndigoWithParams n inp a + +-- | Typeable and stack size constraint for the parameters of an 'IndigoWithParams'. +type family AreIndigoParams n stk :: Constraint where + AreIndigoParams 'Z _ = (() :: Constraint) + AreIndigoParams ('S n) stk = (KnownValue (At n stk), RequireLongerThan stk n, AreIndigoParams n stk) + +-- | Converts an 'IndigoWithParams' to its form without input 'Var's, alongside +-- the 'MetaData' to use it with. +-- If there is an 'Ops' to the bottom of the stack it also assigns a 'Var' to it. +fromIndigoWithParams + :: forall inp n a . (AreIndigoParams n inp, KnownValue a) + => IndigoWithParams n inp a + -> MetaData inp + -> Sing n + -> (IndigoM a, MetaData inp) +fromIndigoWithParams code md = \case + SZ -> (code, assignVarToOps md) + SS n -> let (md2, var) = withVarAt md n in fromIndigoWithParams @inp (code var) md2 n + +-- | Assigns a variable to the 'Ops' list at the bottom of the stack iff there is +-- one and it does not have one already. Otherwise returns the same 'MetaData'. +assignVarToOps :: MetaData inp -> MetaData inp +assignVarToOps md@(MetaData stk vRef) = case stk of + RNil -> md + (_ :& RNil) -> assingVarIfOps md + (x :& xs) -> case assignVarToOps $ MetaData xs vRef of + MetaData xs' vRef' -> MetaData (x :& xs') vRef' + +assingVarIfOps :: forall x. MetaData '[x] -> MetaData '[x] +assingVarIfOps md@(MetaData stk vRef) = case stk of + (Ref _ :& RNil) -> md + ((NoRef :: StkEl x) :& RNil) -> case eqT @x @Ops of + Nothing -> md + Just Refl -> MetaData (Ref vRef :& RNil) (vRef + 1) diff --git a/src/Indigo/FromLorentz.hs b/src/Indigo/FromLorentz.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/FromLorentz.hs @@ -0,0 +1,101 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# LANGUAGE NoRebindableSyntax #-} + +-- | Generation of functions that convert Lorentz code to Indigo + +module Indigo.FromLorentz + ( genFromLorentzFunN + , fromLorentzFunN + ) where + +import Control.Monad hiding (replicateM) +import Language.Haskell.TH + +import Indigo.Backend.Prelude +import Indigo.Internal.Expr (IsExpr) +import qualified Indigo.Internal.Object as O +import qualified Indigo.Internal.State as S +import Indigo.Lorentz (type (&), (:->), KnownValue) +import qualified Lorentz.Instr as L + +-- | Generates all of the 'fromLorentzFunN' (both with and without return value) +-- from 1 to the given @n@ +genFromLorentzFunN :: Int -> Q [Dec] +genFromLorentzFunN n = do + fsArgs <- mapM (`fromLorentzFunN` True ) [1..n] + fsVoid <- mapM (`fromLorentzFunN` False) [1..n] + return $ concat (fsArgs ++ fsVoid) + +-- | Generates a function that converts a Lorentz expression to an Indigo one. +-- +-- The first parameter is the number of elements that the Lorentz code consumes +-- from the stack, as well as the number of Indigo 'IsExpr' values. +-- +-- The second parameter is to establish if there is a return value or not, +-- as well as the name of the function. +-- +-- Examples: +-- +-- * @fromLorentzFunN 1 False@ produces: +-- +-- @ +-- fromLorentzFun1Void :: IsExpr ex a => a & s :-> s -> ex -> IndigoM s s () +-- @ +-- * @fromLorentzFunN 2 True@ produces: +-- +-- @ +-- fromLorentzFun2 +-- :: (KnownValue ret, IsExpr ex1 a, IsExpr ex2 b) +-- => a & b & s :-> ret & s +-- -> ex1 -> ex2 -> IndigoM s (ret & s) (Var ret) +-- @ +fromLorentzFunN :: Int -> Bool -> Q [Dec] +fromLorentzFunN n hasRet + | n <= 0 = fail "fromLorentzFunN requires a positive number of arguments" + | otherwise = do + -- Names + lz <- newName "lz" + exs <- replicateM n $ newName "ex" + as <- replicateM n $ newName "a" + st <- newName "s" + ret <- newName "ret" + let + -- Parameters + args = map varP (lz : exs) + -- Expressions + exCompile = map (\x -> [| compileToExpr $(varE x) |]) exs + compile = foldl1 (\l r -> [| $r S.>> $l |]) exCompile + updateMd = if hasRet then [| pushNoRefMd |] else [| id |] + clear = if hasRet then [| L.drop |] else [| L.nop |] + fun = varE lz + execute = [| S.IndigoState $ \md -> + let cdc = gcCode $ runIndigoState $compile md in + S.GenCode () ($updateMd md) (cdc # $fun) $clear |] + body = if hasRet + then [| $execute S.>> O.makeTopVar |] + else [| $execute |] + -- Types + asType = map varT as + exTypes = map varT exs + stType = varT st + retType = varT ret + + inpType = foldr1 (\a c -> [t| ($a & $c) |] ) (asType ++ [stType]) + outType = if hasRet then [t| $retType & $stType |] else stType + lzType = [t| $inpType :-> $outType |] + + indigoRetType = if hasRet then [t| O.Var $retType |] else [t| () |] + indigoType = [t| S.IndigoState $stType $outType $indigoRetType |] + + fullType = foldr (appT . appT arrowT) indigoType (lzType : exTypes) + constraints = cxt . (if hasRet then ([t| KnownValue $retType |] :) else id) $ + zipWith (\ex a -> [t| IsExpr $ex $a |]) exTypes asType + -- Definitions + signature <- sigD name $ forallT [] constraints fullType + definition <- funD name [clause args (normalB body) []] + return [signature, definition] + where + name = mkName $ "fromLorentzFun" ++ show n ++ (if hasRet then "" else "Void") diff --git a/src/Indigo/Frontend.hs b/src/Indigo/Frontend.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Frontend.hs @@ -0,0 +1,10 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Indigo.Frontend + ( module ReExports + ) where + +import Indigo.Frontend.Language as ReExports +import Indigo.Frontend.Program as ReExports diff --git a/src/Indigo/Frontend/Language.hs b/src/Indigo/Frontend/Language.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Frontend/Language.hs @@ -0,0 +1,778 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Duplication of Backend functions, but without input and output stack. + +module Indigo.Frontend.Language + ( -- * Assignment and modifications + new + , setVar + , setField + , (+=) + , (-=) + , (*=) + , (<<<=) + , (>>>=) + , (&&=) + , (||=) + , (^=) + , (=:) + + -- * Storage Fields + , getStorageField + , setStorageField + , updateStorageField + + -- * Conditional + , if_ + , when + , unless + , ifSome + , ifNone + , whenSome + , whenNone + , ifRight + , ifLeft + , whenRight + , whenLeft + , ifCons + + -- * Case + , case_ + , caseRec + , entryCase + , entryCaseRec + , entryCaseSimple + , (//->) + + -- * Scope + , scope + , defFunction + , defContract + , defNamedPureLambda1 + , defNamedLambda1 + , defNamedLambda0 + , defNamedEffLambda1 + + -- * Loop + , while + , whileLeft + , forEach + + -- * Contract call + , selfCalling + , contractCalling + + -- * Documentation + , doc + , docGroup + , docStorage + , contractName + , contractGeneral + , contractGeneralDefault + , finalizeParamCallingDoc + + -- * Side-effects operations + , transferTokens + , setDelegate + , createContract + , createLorentzContract + + -- * Failures + , failWith + , assert + , failCustom + , failCustom_ + , failUnexpected_ + , assertCustom + , assertCustom_ + + -- * Comments + , comment + , justComment + , commentAroundFun + , commentAroundStmt + + -- * Blocks + , IndigoFunction + , IndigoProcedure + , IndigoEntrypoint + + -- * Helpers + , liftIndigoState + ) where + +import qualified Indigo.Backend as B +import Indigo.Backend.Case hiding (caseRec, entryCaseRec) +import Indigo.Backend.Lambda +import Indigo.Backend.Scope +import Indigo.Compilation (compileIndigoContract) +import Indigo.Frontend.Program +import Indigo.Frontend.Statement +import Indigo.Internal hiding (SetField, return, (>>), (>>=)) +import Indigo.Lorentz +import Indigo.Prelude +import Lorentz.EntryPoints.Helpers (RequireSumType) +import qualified Lorentz.Instr as L +import qualified Lorentz.Run as L +import qualified Michelson.Typed as MT +import qualified Michelson.Typed.Arith as M +import Michelson.Typed.Haskell.Instr.Sum (CaseClauseParam(..), CtorField(..)) +import Util.TypeLits (AppendSymbol) +import Util.TypeTuple.Class + +oneIndigoM :: StatementF IndigoM a -> IndigoM a +oneIndigoM st = IndigoM (Instr st) + +liftIndigoState :: (forall inp. SomeIndigoState inp a) -> IndigoM a +liftIndigoState code = IndigoM (Instr $ LiftIndigoState code) + +varModification + :: (IsExpr ey y, IsObject x) + => ([y, x] :-> '[x]) -> Var x -> ey -> IndigoM () +varModification act v ex = oneIndigoM $ VarModification act v ex + +---------------------------------------------------------------------------- +-- Var creation and assignment +---------------------------------------------------------------------------- + +-- | Create a new variable with the result of the given expression as its initial value. +new :: IsExpr ex x => ex -> IndigoM (Var x) +new e = oneIndigoM $ NewVar e + +-- | Set the given variable to the result of the given expression. +setVar :: (IsExpr ex x, IsObject x) => Var x -> ex -> IndigoM () +setVar v e = oneIndigoM $ SetVar v e + +infixr 0 =: +(=:) :: (IsExpr ex x, IsObject x) => Var x -> ex -> IndigoM () +v =: e = setVar v e + +setField + :: ( ex :~> ftype + , IsObject dt + , IsObject ftype + , HasField dt fname ftype + ) + => Var dt -> Label fname -> ex -> IndigoM () +setField v fName e = oneIndigoM $ SetField v fName e + +(+=) + :: ( IsExpr ex1 n, IsObject m + , ArithOpHs M.Add n m, ArithResHs M.Add n m ~ m + ) => Var m -> ex1 -> IndigoM () +(+=) = varModification L.add + +(-=) + :: ( IsExpr ex1 n, IsObject m + , ArithOpHs M.Sub n m, ArithResHs M.Sub n m ~ m + ) => Var m -> ex1 -> IndigoM () +(-=) = varModification L.sub + +(*=) + :: ( IsExpr ex1 n, IsObject m + , ArithOpHs M.Mul n m, ArithResHs M.Mul n m ~ m + ) => Var m -> ex1 -> IndigoM () +(*=) = varModification L.mul + +(||=) + :: ( IsExpr ex1 n, IsObject m + , ArithOpHs M.Or n m, ArithResHs M.Or n m ~ m + ) => Var m -> ex1 -> IndigoM () +(||=) = varModification L.or + +(&&=) + :: ( IsExpr ex1 n, IsObject m + , ArithOpHs M.And n m, ArithResHs M.And n m ~ m + ) => Var m -> ex1 -> IndigoM () +(&&=) = varModification L.and + +(^=) + :: ( IsExpr ex1 n, IsObject m + , ArithOpHs M.Xor n m, ArithResHs M.Xor n m ~ m + ) => Var m -> ex1 -> IndigoM () +(^=) = varModification L.xor + +(<<<=) + :: ( IsExpr ex1 n, IsObject m + , ArithOpHs M.Lsl n m, ArithResHs M.Lsl n m ~ m + ) => Var m -> ex1 -> IndigoM () +(<<<=) = varModification L.lsl + +(>>>=) + :: ( IsExpr ex1 n, IsObject m + , ArithOpHs M.Lsr n m, ArithResHs M.Lsr n m ~ m + ) => Var m -> ex1 -> IndigoM () +(>>>=) = varModification L.lsr + +---------------------------------------------------------------------------- +-- Storage Fields +---------------------------------------------------------------------------- + +-- | Sets a storage field to a new value. +setStorageField + :: forall store name ftype ex. + ( HasStorage store + , ex :~> ftype + , IsObject store + , IsObject ftype + , HasField store name ftype + ) + => Label name -> ex -> IndigoM () +setStorageField field expr = setField (storageVar @store) field expr + +-- | Updates a storage field by using an updating 'IndigoM'. +updateStorageField + :: forall store ftype fname fex. + ( HasStorage store + , fex :~> ftype + , HasField store fname ftype + , IsObject store + , IsObject ftype + ) + => Label fname + -> (Var ftype -> IndigoM fex) + -> IndigoM () +updateStorageField field upd = scope $ do + let storage = storageVar @store + fieldVar <- new$ storage #! field + expr <- upd fieldVar + setField storage field expr + +-- | Get a field from the storage, returns a variable. +-- +-- Note that the storage type almost always needs to be specified. +getStorageField + :: forall store ftype fname . + ( HasStorage store + , HasField store fname ftype + ) + => Label fname -> IndigoM (Var ftype) +getStorageField field = new$ storageVar @store #! field + +---------------------------------------------------------------------------- +-- Conditional +---------------------------------------------------------------------------- + +if_ + :: forall a b ex . (IfConstraint a b, ex :~> Bool) + => ex + -> IndigoM a + -> IndigoM b + -> IndigoM (RetVars a) +if_ ex tb fb = oneIndigoM $ If ex tb fb + +-- | Run the instruction when the condition is met, do nothing otherwise. +when :: (exc :~> Bool) => exc -> IndigoM () -> IndigoM () +when cond expr = if_ cond expr (return ()) + +-- | Reverse of 'when'. +unless :: (exc :~> Bool) => exc -> IndigoM () -> IndigoM () +unless cond expr = if_ cond (return ()) expr + +ifSome + :: forall x a b ex . (KnownValue x, ex :~> Maybe x, IfConstraint a b) + => ex + -> (Var x -> IndigoM a) + -> IndigoM b + -> IndigoM (RetVars a) +ifSome ex tb fb = oneIndigoM $ IfSome ex tb fb + +ifNone + :: forall x a b ex . (KnownValue x, ex :~> Maybe x, IfConstraint a b) + => ex + -> IndigoM b + -> (Var x -> IndigoM a) + -> IndigoM (RetVars a) +ifNone ex fb tb = ifSome ex tb fb + +-- | Run the instruction when the given expression returns 'Just' a value, +-- do nothing otherwise. +whenSome + :: forall x exa . + ( KnownValue x + , exa :~> Maybe x + ) + => exa + -> (Var x -> IndigoM ()) + -> IndigoM () +whenSome c f = ifSome c f (return ()) + +-- | Run the instruction when the given expression returns 'Nothing', +-- do nothing otherwise. +whenNone + :: forall x exa . + ( KnownValue x + , exa :~> Maybe x + ) + => exa + -> IndigoM () + -> IndigoM () +whenNone c f = ifSome c (\_ -> return ()) f + +ifRight + :: forall x y a b ex . + ( KnownValue x + , KnownValue y + , ex :~> Either y x + , IfConstraint a b + ) + => ex + -> (Var x -> IndigoM a) + -> (Var y -> IndigoM b) + -> IndigoM (RetVars a) +ifRight ex rb lb = oneIndigoM $ IfRight ex rb lb + +ifLeft + :: forall x y a b ex . + ( KnownValue x + , KnownValue y + , ex :~> Either y x + , IfConstraint a b + ) + => ex + -> (Var y -> IndigoM b) + -> (Var x -> IndigoM a) + -> IndigoM (RetVars a) +ifLeft ex lb rb = ifRight ex rb lb + +whenRight + :: forall x y ex . + ( KnownValue x + , KnownValue y + , ex :~> Either y x + ) + => ex + -> (Var x -> IndigoM ()) + -> IndigoM () +whenRight c f = ifRight c f (\_ -> return ()) + +whenLeft + :: forall x y ex . + ( KnownValue x + , KnownValue y + , ex :~> Either y x + ) + => ex + -> (Var y -> IndigoM ()) + -> IndigoM () +whenLeft c f = ifRight c (\_ -> return ()) f + +ifCons + :: forall x a b ex . (KnownValue x, ex :~> List x, IfConstraint a b) + => ex + -> (Var x -> Var (List x) -> IndigoM a) + -> IndigoM b + -> IndigoM (RetVars a) +ifCons ex tb fb = oneIndigoM $ IfCons ex tb fb + +---------------------------------------------------------------------------- +-- Case +---------------------------------------------------------------------------- + +-- | A case statement for indigo. See examples for a sample usage. +caseRec + :: forall dt guard ret clauses . + CaseCommonF (IndigoMCaseClauseL IndigoM) dt guard ret clauses + => guard + -> clauses + -> IndigoM (RetVars ret) +caseRec = oneIndigoM ... Case + +-- | 'caseRec' for tuples. +case_ + :: forall dt guard ret clauses. + ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt guard ret clauses + , RecFromTuple clauses + ) + => guard + -> IsoRecTuple clauses + -> IndigoM (RetVars ret) +case_ g = caseRec g . recFromTuple @clauses + + +-- | 'caseRec' for pattern-matching on parameter. +entryCaseRec + :: forall dt entryPointKind guard ret clauses . + ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt guard ret clauses + , DocumentEntryPoints entryPointKind dt + ) + => Proxy entryPointKind + -> guard + -> clauses + -> IndigoM (RetVars ret) +entryCaseRec proxy g cls = oneIndigoM $ EntryCase proxy g cls + +-- | 'entryCaseRec' for tuples. +entryCase + :: forall dt entryPointKind guard ret clauses . + ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt guard ret clauses + , RecFromTuple clauses + , DocumentEntryPoints entryPointKind dt + ) + => Proxy entryPointKind + -> guard + -> IsoRecTuple clauses + -> IndigoM (RetVars ret) +entryCase proxy g = entryCaseRec proxy g . recFromTuple @clauses + +entryCaseSimple + :: forall cp guard ret clauses . + ( CaseCommonF (IndigoMCaseClauseL IndigoM) cp guard ret clauses + , RecFromTuple clauses + , DocumentEntryPoints PlainEntryPointsKind cp + , NiceParameterFull cp + , RequireFlatParamEps cp + ) + => guard + -> IsoRecTuple clauses + -> IndigoM (RetVars ret) +entryCaseSimple g = oneIndigoM . EntryCaseSimple g . recFromTuple @clauses + +-- | Use this instead of '/->'. +-- +-- This operator is like '/->' but wraps a body into 'IndigoAnyOut', +-- which is needed for two reasons: to allow having any output stack +-- and to allow returning not exactly the same values. +(//->) + :: ( CaseArrow name (Var x -> IndigoAnyOut x ret) + (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x))) + , ScopeCodeGen retBr + , ret ~ RetExprs retBr + , RetOutStack ret ~ RetOutStack retBr + , KnownValue x + , name ~ (AppendSymbol "c" ctor) + ) + => Label name + -> (Var x -> IndigoM retBr) + -> IndigoMCaseClauseL IndigoM ret ('CaseClauseParam ctor ('OneField x)) +(//->) cName b = OneFieldIndigoMCaseClauseL cName b +infixr 0 //-> + +---------------------------------------------------------------------------- +-- Scope & Functions +---------------------------------------------------------------------------- + +-- | Utility type for an 'IndigoM' that adds one element to the stack and returns +-- a variable pointing at it. +type IndigoFunction ret = IndigoM (RetVars ret) + +-- | Utility type for an 'IndigoM' that does not modify the stack (only the +-- values in it) and returns nothing. +type IndigoProcedure = IndigoM () + +type IndigoEntrypoint param = param -> IndigoProcedure + +scope + :: forall a . ScopeCodeGen a + => IndigoM a + -> IndigoFunction a +scope = oneIndigoM . Scope + +-- | Alias for 'scope' we use in the tutorial. +defFunction + :: forall a . ScopeCodeGen a + => IndigoM a + -> IndigoFunction a +defFunction = scope + +-- | A more specific version of 'defFunction' meant to more easily create +-- 'IndigoContract's. +-- +-- Used in the tutorial. The 'HasSideEffects' constraint is +-- specified to avoid the warning for redundant constraints. +defContract + :: (HasSideEffects => IndigoM ()) + -> (HasSideEffects => IndigoProcedure) +defContract = scope + +-- | Family of @defNamed*LambdaN@ functions put an Indigo computation +-- on the stack to later call it avoiding code duplication. +-- @defNamed*LambdaN@ takes a computation with N arguments. +-- This family of functions add some overhead to contract byte size +-- for every call of the function, +-- therefore, DON'T use @defNamed*LambdaN@ if: +-- * Your computation is pretty small. +-- It would be cheaper just to inline it, so use 'defFunction'. +-- * Your computation is called only once, in this case also use 'defFunction'. +-- +-- Also, pay attention that @defNamed*LambdaN@ accepts a string that is +-- a name of the passed computation. Be careful and make sure that all +-- declared computations have different names. +-- Later the name will be removed. +-- +-- Pay attention, that lambda argument will be evaluated +-- to variable before lambda calling. +-- +-- TODO Approach with lambda names has critical pitfall: +-- in case if a function takes @Label name@, lambda body +-- won't be regenerated for every different label. +-- So be carefully, this will be fixed in a following issue. +defNamedEffLambda1 + :: forall st argExpr res . + ( ToExpr argExpr + , Typeable res + , ExecuteLambdaEff1C st (ExprType argExpr) res + , CreateLambdaEff1C st (ExprType argExpr) res) + => String + -> (Var (ExprType argExpr) -> IndigoM res) + -> (argExpr -> IndigoM (RetVars res)) +defNamedEffLambda1 lName body = \ex -> + oneIndigoM $ LambdaEff1Call (Proxy @st) lName body (toExpr ex) + +-- | Like defNamedEffLambda1 but doesn't make side effects. +defNamedLambda1 + :: forall st argExpr res . + ( ToExpr argExpr + , Typeable res + , ExecuteLambda1C st (ExprType argExpr) res + , CreateLambda1C st (ExprType argExpr) res) + => String + -> (Var (ExprType argExpr) -> IndigoM res) + -> (argExpr -> IndigoM (RetVars res)) +defNamedLambda1 lName body = \ex -> + oneIndigoM $ Lambda1Call (Proxy @st) lName body (toExpr ex) + +-- | Like defNamedLambda1 but doesn't take an argument. +defNamedLambda0 + :: forall st res . + ( Typeable res + , ExecuteLambda1C st () res + , CreateLambda1C st () res) + => String + -> IndigoM res + -> IndigoM (RetVars res) +defNamedLambda0 lName body = oneIndigoM $ Lambda1Call (Proxy @st) lName (\(_ :: Var ()) -> body) (C ()) + +-- | Like defNamedEffLambda1 but doesn't modify storage and doesn't make side effects. +defNamedPureLambda1 + :: forall argExpr res . + ( ToExpr argExpr + , Typeable res + , ExecuteLambdaPure1C (ExprType argExpr) res + , CreateLambdaPure1C (ExprType argExpr) res) + => String + -> (Var (ExprType argExpr) -> IndigoM res) + -> (argExpr -> IndigoM (RetVars res)) +defNamedPureLambda1 lName body = \ex -> + oneIndigoM $ LambdaPure1Call lName body (toExpr ex) + +---------------------------------------------------------------------------- +-- Loop +---------------------------------------------------------------------------- + +-- | While statement. +while :: forall ex . ex :~> Bool => ex -> IndigoM () -> IndigoM () +while e body = oneIndigoM $ While e body + +whileLeft + :: forall x y ex . + ( ex :~> Either y x + , KnownValue y + , KnownValue x + ) + => ex + -> (Var y -> IndigoM ()) + -> IndigoM (Var x) +whileLeft e body = oneIndigoM $ WhileLeft e body + +-- | For statements to iterate over a container. +forEach + :: forall a e . (IterOpHs a, KnownValue (IterOpElHs a), e :~> a) + => e -> (Var (IterOpElHs a) -> IndigoM ()) + -> IndigoM () +forEach container body = oneIndigoM $ ForEach container body + +---------------------------------------------------------------------------- +-- Documentation +---------------------------------------------------------------------------- + +-- | Put a document item. +doc :: DocItem di => di -> IndigoM () +doc di = liftIndigoState $ toSIS $ B.doc di + +-- | Group documentation built in the given piece of code +-- into a block dedicated to one thing, e.g. to one entrypoint. +docGroup :: DocGrouping -> IndigoM () -> IndigoM () +docGroup = oneIndigoM ... DocGroup + +-- | Insert documentation of the contract's storage type. The type +-- should be passed using type applications. +docStorage :: forall storage. TypeHasDoc storage => IndigoM () +docStorage = liftIndigoState $ toSIS $ B.docStorage @storage + +-- | Give a name to the given contract. Apply it to the whole contract code. +contractName :: Text -> IndigoM () -> IndigoM () +contractName = oneIndigoM ... ContractName + +-- | Attach general info to the given contract. +contractGeneral :: IndigoM () -> IndigoM () +contractGeneral = oneIndigoM . ContractGeneral + +-- | Attach default general info to the contract documentation. +contractGeneralDefault :: IndigoM () +contractGeneralDefault = liftIndigoState $ toSIS $ B.contractGeneralDefault + +-- | Indigo version for the homonym Lorentz function. +finalizeParamCallingDoc + :: forall param x. + ( ToExpr param + , NiceParameterFull (ExprType param) + , RequireSumType (ExprType param) + , HasCallStack + ) + => (Var (ExprType param) -> IndigoM x) -> (param -> IndigoM x) +finalizeParamCallingDoc = oneIndigoM ... FinalizeParamCallingDoc + +---------------------------------------------------------------------------- +-- Contract call +---------------------------------------------------------------------------- + +selfCalling + :: forall p mname. + ( NiceParameterFull p + , KnownValue (GetEntryPointArgCustom p mname) + ) + => EntryPointRef mname + -> IndigoM (Var (ContractRef (GetEntryPointArgCustom p mname))) +selfCalling ep = liftIndigoState $ toSIS $ B.selfCalling @p ep + +contractCalling + :: forall cp epRef epArg addr exAddr. + ( HasEntryPointArg cp epRef epArg + , ToTAddress cp addr + , ToT addr ~ ToT Address + , exAddr :~> addr + , KnownValue epArg + ) + => epRef -> exAddr -> IndigoM (Var (Maybe (ContractRef epArg))) +contractCalling = oneIndigoM ... ContractCalling (Proxy @cp) + +---------------------------------------------------------------------------- +-- Side-effects operations +---------------------------------------------------------------------------- + +transferTokens + :: (IsExpr exp p, IsExpr exm Mutez, IsExpr exc (ContractRef p), NiceParameter p, HasSideEffects) + => exp -> exm -> exc -> IndigoM () +transferTokens = oneIndigoM ... TransferTokens + +setDelegate :: (HasSideEffects, IsExpr ex (Maybe KeyHash)) => ex -> IndigoM () +setDelegate = oneIndigoM ... SetDelegate + +-- | Create contract using default compilation options for Lorentz compiler. +-- +-- See "Lorentz.Run". +createContract + :: ( IsObject st + , IsExpr exk (Maybe KeyHash), IsExpr exm Mutez, IsExpr exs st + , NiceStorage st, NiceParameterFull param + , HasSideEffects + ) + => (HasStorage st => Var param -> IndigoM ()) + -> exk + -> exm + -> exs + -> IndigoM (Var Address) +createContract iCtr ek em es = oneIndigoM $ CreateContract (defaultContract $ compileIndigoContract iCtr) ek em es + +-- | Create contract from raw Lorentz 'L.Contract'. +createLorentzContract + :: ( IsObject st + , IsExpr exk (Maybe KeyHash), IsExpr exm Mutez, IsExpr exs st + , NiceStorage st, NiceParameterFull param + , HasSideEffects + ) + => L.Contract param st + -> exk + -> exm + -> exs + -> IndigoM (Var Address) +createLorentzContract lCtr ek em es = oneIndigoM $ CreateContract lCtr ek em es + +---------------------------------------------------------------------------- +-- Error +---------------------------------------------------------------------------- + +assert + :: forall x ex. + ( IsError x + , IsExpr ex Bool + ) + => x -> ex -> IndigoM () +assert = oneIndigoM ... Assert + +failWith + :: forall r a ex . IsExpr ex a + => ex -> IndigoM r +failWith = oneIndigoM . FailWith + +failCustom + :: forall r tag err ex. + ( err ~ ErrorArg tag + , CustomErrorHasDoc tag + , NiceConstant err + , ex :~> err + ) + => Label tag -> ex -> IndigoM r +failCustom l errEx = oneIndigoM $ FailCustom l errEx + +failCustom_ + :: forall r tag notVoidErrorMsg. + ( RequireNoArgError tag notVoidErrorMsg + , CustomErrorHasDoc tag + ) + => Label tag -> IndigoM r +failCustom_ lab = liftIndigoState $ toSIS $ B.failCustom_ lab + +failUnexpected_ :: MText -> IndigoM r +failUnexpected_ tx = liftIndigoState $ toSIS $ B.failUnexpected_ tx + +assertCustom + :: forall tag err errEx ex . + ( err ~ ErrorArg tag + , CustomErrorHasDoc tag + , NiceConstant err + , IsExpr errEx err + , IsExpr ex Bool + ) + => Label tag -> errEx -> ex -> IndigoM () +assertCustom tag errEx e = if_ (toExpr e) (return ()) (failCustom tag errEx :: IndigoM ()) + +assertCustom_ + :: forall tag notVoidErrorMsg ex. + ( RequireNoArgError tag notVoidErrorMsg + , CustomErrorHasDoc tag + , IsExpr ex Bool + ) + => Label tag -> ex -> IndigoM () +assertCustom_ tag e = if_ (toExpr e) (return ()) (failCustom_ tag :: IndigoM ()) + +---------------------------------------------------------------------------- +-- Comments +---------------------------------------------------------------------------- + +-- | Add a comment in a generated Michelson code +justComment :: Text -> IndigoM () +justComment = comment . MT.JustComment + +-- | Add a comment in a generated Michelson code +comment :: MT.CommentType -> IndigoM () +comment t = liftIndigoState $ toSIS (B.comment t) + +-- | Add a comment before and after the given Indigo function code. +-- The first argument is the name of the function. +commentAroundFun :: Text -> IndigoM a -> IndigoM a +commentAroundFun fName body = + comment (MT.FunctionStarts fName) >> + body >>= + \res -> res <$ comment (MT.FunctionEnds fName) + +-- | Add a comment before and after the given Indigo statement code. +-- The first argument is the name of the statement. +commentAroundStmt :: Text -> IndigoM a -> IndigoM a +commentAroundStmt sName body = + comment (MT.StatementStarts sName) >> + body >>= + \res -> res <$ comment (MT.StatementEnds sName) diff --git a/src/Indigo/Frontend/Program.hs b/src/Indigo/Frontend/Program.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Frontend/Program.hs @@ -0,0 +1,57 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Indigo.Frontend.Program + ( IndigoM (..) + + , Program (..) + , interpretProgram + ) where + +import Control.Monad (liftM) +import Prelude + +import Indigo.Frontend.Statement + +-- | This is freer monad (in other words operational monad). +-- +-- It preserves the structure of the computation performed over it, +-- including @return@ and @bind@ operations. +-- This was introduced to be able to iterate over Indigo code and optimize/analyze it. +-- +-- You can read a clearer description of this construction in +-- "The Book of Monads" by Alejandro Serrano. +-- There is a chapter about free monads, specifically about Freer you can read at page 259. +-- There is "operational" package which contains transformer of this monad and +-- auxiliary functions but it's not used because we are using only some basics of it. +data Program instr a where + Done :: a -> Program instr a + Instr :: instr a -> Program instr a + Bind :: Program instr a -> (a -> Program instr b) -> Program instr b + +instance Functor (Program instr) where + fmap = liftM + +instance Applicative (Program instr) where + pure = Done + (<*>) = ap + +instance Monad (Program instr) where + return = pure + (>>=) = Bind + +-- | Traverse over Freer structure and interpret it +interpretProgram + :: Monad m + => (forall x . instr x -> m x) + -> Program instr a -> m a +interpretProgram _ (Done a) = return a +interpretProgram interp (Instr a) = interp a +interpretProgram interp (Bind instr rest) = + interpretProgram interp instr >>= (interpretProgram interp . rest) + +-- | Monad for writing your contracts in. +newtype IndigoM a = IndigoM {unIndigoM :: Program (StatementF IndigoM) a} + deriving stock (Functor) + deriving newtype (Applicative, Monad) diff --git a/src/Indigo/Frontend/Statement.hs b/src/Indigo/Frontend/Statement.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Frontend/Statement.hs @@ -0,0 +1,204 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | 'StatementF' functor datatype for Freer monad + +module Indigo.Frontend.Statement + ( StatementF (..) + + , IfConstraint + , IndigoMCaseClauseL (..) + ) where + +import qualified Data.Kind as Kind +import Util.TypeLits (AppendSymbol) + +import Lorentz.EntryPoints.Helpers (RequireSumType) +import qualified Lorentz.Run as L (Contract) +import Michelson.Typed.Haskell.Instr.Sum (CaseClauseParam(..), CtorField(..)) + +import Indigo.Prelude +import Indigo.Lorentz +import Indigo.Internal +import Indigo.Backend + +-- | Analogous datatype as IndigoCaseClauseL from Indigo.Backend.Case +data IndigoMCaseClauseL freer ret (param :: CaseClauseParam) where + OneFieldIndigoMCaseClauseL + :: ( CaseArrow name + (Var x -> IndigoAnyOut x ret) + (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x))) + , name ~ (AppendSymbol "c" ctor) + , KnownValue x + , ScopeCodeGen retBr + , ret ~ RetExprs retBr + , RetOutStack ret ~ RetOutStack retBr + ) + => Label name + -> (Var x -> freer retBr) + -> IndigoMCaseClauseL freer ret ('CaseClauseParam ctor ('OneField x)) + +-- | StatementF functor for Freer monad. +-- +-- The constructors correspond to every Indigo statement that has expressions +-- (@'Expr' x@) in its signature. +-- +-- The ones that don't take expressions are compiled directly to 'IndigoState' +-- (and kept in 'LiftIndigoState'), because they won't be taken into consideration +-- by an optimizer anyway. +-- +-- One more detail about 'StatementF' is that it takes a @cont@ type parameter, +-- which is basically 'IndigoM' (freer monad), to avoid cyclic dependencies. +-- @cont@ is needed to support statements which have recursive structure +-- (like: @if@, @while@, @case@, etc). +data StatementF (freer :: Kind.Type -> Kind.Type) a where + -- | Direct injection of IndigoState of statements + -- which are not going to be analyzed by optimizer. + LiftIndigoState :: (forall inp . SomeIndigoState inp a) -> StatementF freer a + + NewVar :: (ex :~> x) => ex -> StatementF freer (Var x) + SetVar :: (ex :~> x, IsObject x) => Var x -> ex -> StatementF freer () + VarModification + :: (ey :~> y, IsObject x) + => [y, x] :-> '[x] + -> Var x + -> ey + -> StatementF freer () + SetField :: + ( ex :~> ftype + , IsObject dt + , IsObject ftype + , HasField dt fname ftype + ) + => Var dt -> Label fname -> ex -> StatementF cont () + + -- | Pure lambda + LambdaPure1Call + :: (ExecuteLambdaPure1C arg res, CreateLambdaPure1C arg res, Typeable res) + => String + -> (Var arg -> freer res) + -> Expr arg + -> StatementF freer (RetVars res) + + -- | "Default" lambda which can modify storage + Lambda1Call + :: (ExecuteLambda1C st arg res, CreateLambda1C st arg res, Typeable res) + => Proxy st + -> String + -> (Var arg -> freer res) + -> Expr arg + -> StatementF freer (RetVars res) + + -- | Lambda which can modify storage and emit operations + LambdaEff1Call + :: (ExecuteLambdaEff1C st arg res, CreateLambdaEff1C st arg res, Typeable res) + => Proxy st + -> String + -> (Var arg -> freer res) + -> Expr arg + -> StatementF freer (RetVars res) + + Scope :: ScopeCodeGen a => freer a -> StatementF freer (RetVars a) + If :: (IfConstraint a b, ex :~> Bool) + => ex + -> freer a + -> freer b + -> StatementF freer (RetVars a) + IfSome :: (IfConstraint a b, KnownValue x, ex :~> Maybe x) + => ex + -> (Var x -> freer a) + -> freer b + -> StatementF freer (RetVars a) + IfRight + :: (IfConstraint a b, KnownValue x, KnownValue y, ex :~> Either y x) + => ex + -> (Var x -> freer a) + -> (Var y -> freer b) + -> StatementF freer (RetVars a) + IfCons + :: (IfConstraint a b, KnownValue x, ex :~> (List x) ) + => ex + -> (Var x -> Var (List x) -> freer a) + -> freer b + -> StatementF freer (RetVars a) + Case :: CaseCommonF (IndigoMCaseClauseL freer) dt guard ret clauses + => guard -> clauses + -> StatementF freer (RetVars ret) + EntryCase :: + ( CaseCommonF (IndigoMCaseClauseL freer) dt guard ret clauses + , DocumentEntryPoints entryPointKind dt + ) + => Proxy entryPointKind + -> guard + -> clauses + -> StatementF freer (RetVars ret) + EntryCaseSimple :: + ( CaseCommonF (IndigoMCaseClauseL freer) cp guard ret clauses + , DocumentEntryPoints PlainEntryPointsKind cp + , NiceParameterFull cp + , RequireFlatParamEps cp + ) + => guard + -> clauses + -> StatementF freer (RetVars ret) + + While :: ex :~> Bool => ex -> freer () -> StatementF freer () + WhileLeft + :: (KnownValue x, KnownValue y, ex :~> Either y x) + => ex + -> (Var y -> freer ()) + -> StatementF freer (Var x) + ForEach :: (IterOpHs a, KnownValue (IterOpElHs a), e :~> a) + => e + -> (Var (IterOpElHs a) -> freer ()) + -> StatementF freer () + + ContractName :: Text -> freer () -> StatementF freer () + DocGroup :: DocGrouping -> freer () -> StatementF freer () + ContractGeneral :: freer () -> StatementF freer () + FinalizeParamCallingDoc + :: (ToExpr param, NiceParameterFull (ExprType param), RequireSumType (ExprType param), HasCallStack) + => (Var (ExprType param) -> freer x) -> param -> StatementF freer x + + TransferTokens + :: (exp :~> p, exm :~> Mutez, exc :~> ContractRef p, NiceParameter p, HasSideEffects) + => exp -> exm -> exc -> StatementF freer () + SetDelegate :: (HasSideEffects, ex :~> Maybe KeyHash) => ex -> StatementF freer () + + CreateContract :: + ( IsObject st + , exk :~> Maybe KeyHash, exm :~> Mutez, exs :~> st + , NiceStorage st, NiceParameterFull param + , HasSideEffects + ) + => L.Contract param st + -> exk + -> exm + -> exs + -> StatementF freer (Var Address) + ContractCalling :: + ( HasEntryPointArg cp epRef epArg + , ToTAddress cp addr + , ToT addr ~ ToT Address + , exAddr :~> addr + , KnownValue epArg + ) + => Proxy cp -> epRef -> exAddr -> StatementF freer (Var (Maybe (ContractRef epArg))) + + FailWith :: + ( ex :~> a + ) + => ex -> StatementF freer r + Assert :: + ( IsError x + , ex :~> Bool + ) + => x -> ex -> StatementF freer () + FailCustom :: + ( err ~ ErrorArg tag + , CustomErrorHasDoc tag + , NiceConstant err + , ex :~> err + ) + => Label tag -> ex -> StatementF freer r diff --git a/src/Indigo/Internal.hs b/src/Indigo/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal.hs @@ -0,0 +1,14 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Indigo.Internal + ( module ReExports + ) where + +import Indigo.Internal.Expr as ReExports +import Indigo.Internal.Field as ReExports +import Indigo.Internal.Lookup as ReExports +import Indigo.Internal.SIS as ReExports +import Indigo.Internal.State as ReExports +import Indigo.Internal.Object as ReExports diff --git a/src/Indigo/Internal/Expr.hs b/src/Indigo/Internal/Expr.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/Expr.hs @@ -0,0 +1,19 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | 'Expr'essions supported in Indigo language and their compilation to +-- Lorentz code. +-- +-- This module contains only basic building blocks that can be used to +-- implement anything else. Other modules provide high level language +-- constructions and standard functions. + +module Indigo.Internal.Expr + ( module Exported + ) where + +import Indigo.Internal.Expr.Compilation as Exported +import Indigo.Internal.Expr.Decompose as Exported +import Indigo.Internal.Expr.Symbolic as Exported +import Indigo.Internal.Expr.Types as Exported diff --git a/src/Indigo/Internal/Expr/Compilation.hs b/src/Indigo/Internal/Expr/Compilation.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/Expr/Compilation.hs @@ -0,0 +1,326 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | 'Expr' compilation + +module Indigo.Internal.Expr.Compilation + ( compileExpr + , compileToExpr + + , ObjManipulationRes (..) + , runObjectManipulation + + , nullaryOp + , unaryOp + , binaryOp + , ternaryOp + + , nullaryOpFlat + , unaryOpFlat + , binaryOpFlat + , ternaryOpFlat + ) where + +import Data.Vinyl.Core (RMap(..)) + +import qualified Lorentz.ADT as L +import qualified Lorentz.Instr as L +import qualified Lorentz.Macro as L +import Michelson.Typed.Haskell.Instr.Product (GetFieldType) + +import Indigo.Backend.Prelude +import Indigo.Internal.Expr.Types +import Indigo.Internal.Field +import Indigo.Internal.Lookup (varActionGet) +import Indigo.Internal.Object + (IndigoObjectF(..), NamedFieldVar(..), castFieldConstructors, namedToTypedRec, pushNoRefMd, + typedToNamedRec) +import Indigo.Internal.State + (GenCode(..), IndigoState(..), MetaData(..), iget, iput, usingIndigoState, (>>=)) +import Indigo.Lorentz + +compileExpr :: forall a inp . Expr a -> IndigoState inp (a & inp) () +compileExpr (C a) = do + md <- iget + iput $ GenCode () (pushNoRefMd md) (L.push a) L.drop +compileExpr (V v) = compileObjectF (\(NamedFieldVar fl) -> V fl) v +compileExpr (Update m key val) = ternaryOp key val m L.update +compileExpr (Add e1 e2) = binaryOp e1 e2 L.add +compileExpr (Sub e1 e2) = binaryOp e1 e2 L.sub +compileExpr (Mul e1 e2) = binaryOp e1 e2 L.mul +compileExpr (Div e1 e2) = binaryOp e1 e2 (L.ediv # L.ifSome L.car (failUsing [mt|devision by zero|])) +compileExpr (Mod e1 e2) = binaryOp e1 e2 (L.ediv # L.ifSome L.cdr (failUsing [mt|devision by zero|])) +compileExpr (Abs e) = unaryOp e L.abs +compileExpr (Neg e) = unaryOp e L.neg + +compileExpr (Lsl e1 e2) = binaryOp e1 e2 L.lsl +compileExpr (Lsr e1 e2) = binaryOp e1 e2 L.lsr + +compileExpr (Eq' e1 e2) = binaryOp e1 e2 L.eq +compileExpr (Neq e1 e2) = binaryOp e1 e2 L.neq +compileExpr (Lt e1 e2) = binaryOp e1 e2 L.lt +compileExpr (Le e1 e2) = binaryOp e1 e2 L.le +compileExpr (Gt e1 e2) = binaryOp e1 e2 L.gt +compileExpr (Ge e1 e2) = binaryOp e1 e2 L.ge +compileExpr (IsNat e) = unaryOp e L.isNat +compileExpr (Int' e) = unaryOp e L.int +compileExpr (And e1 e2) = binaryOp e1 e2 L.and +compileExpr (Or e1 e2) = binaryOp e1 e2 L.or +compileExpr (Xor e1 e2) = binaryOp e1 e2 L.xor +compileExpr (Not e) = unaryOp e L.not + +compileExpr (Fst e) = unaryOp e L.car +compileExpr (Snd e) = unaryOp e L.cdr +compileExpr (Pair e1 e2) = binaryOp e1 e2 L.pair + +compileExpr (Some e) = unaryOp e L.some +compileExpr None = nullaryOp L.none +compileExpr (Right' e) = unaryOp e L.right +compileExpr (Left' e) = unaryOp e L.left +compileExpr (Pack e) = unaryOp e L.pack +compileExpr (Unpack e) = unaryOp e L.unpack +compileExpr Nil = nullaryOp L.nil +compileExpr (Cons e1 e2) = binaryOp e1 e2 L.cons +compileExpr (Contract e) = unaryOp e L.contract +compileExpr Self = nullaryOp L.self +compileExpr (ContractAddress ec) = unaryOp ec L.address +compileExpr (ContractCallingUnsafe epName addr) = unaryOp addr (L.contractCallingUnsafe epName) +compileExpr (RunFutureContract con) = unaryOp con L.runFutureContract +compileExpr (ConvertEpAddressToContract epAddr) = unaryOp epAddr L.epAddressToContract +compileExpr (MakeView e1 e2) = binaryOp e1 e2 (L.pair # L.wrapView) +compileExpr (MakeVoid e1 e2) = binaryOp e1 e2 (L.pair # L.wrapVoid) + +compileExpr (Mem k c) = binaryOp k c L.mem +compileExpr (Size s) = unaryOp s L.size + +compileExpr (UInsertNew l err k v store) = + ternaryOp k v store $ ustoreInsertNew l (failUsing err) +compileExpr (UInsert l k v store) = + ternaryOp k v store $ ustoreInsert l +compileExpr (UGet l ekey estore) = binaryOp ekey estore (ustoreGet l) +compileExpr (UMem l ekey estore) = binaryOp ekey estore (ustoreMem l) +compileExpr (UUpdate l ekey evalue estore) = ternaryOp ekey evalue estore (ustoreUpdate l) +compileExpr (UDelete l ekey estore) = binaryOp ekey estore (ustoreDelete l) + +compileExpr (ObjMan fldAcc) = compileObjectManipulation fldAcc +compileExpr (Construct fields) = IndigoState $ \md -> + let cd = L.construct $ rmap (\e -> fieldCtor $ gcCode $ runIndigoState (compileExpr e) md) fields in + GenCode () (pushNoRefMd md) cd L.drop +compileExpr (ConstructWithoutNamed fields) = IndigoState $ \md -> + let fieldCtrs = + castFieldConstructors @a $ + rmap (fieldCtor . gcCode . usingIndigoState md . compileExpr) fields + in GenCode () (pushNoRefMd md) (L.construct @a fieldCtrs) L.drop +compileExpr (Name _ e) = unaryOp e forcedCoerce_ +compileExpr (UnName _ e) = unaryOp e forcedCoerce_ + +compileExpr (Slice ex1 ex2 ex3) = ternaryOp ex1 ex2 ex3 L.slice +compileExpr (Cast ex) = unaryOp ex L.cast +compileExpr (Concat ex1 ex2) = binaryOp ex1 ex2 L.concat +compileExpr (Concat' ex) = unaryOp ex L.concat' + +compileExpr (ImplicitAccount kh) = unaryOp kh L.implicitAccount +compileExpr Now = nullaryOp L.now +compileExpr Sender = nullaryOp L.sender +compileExpr Amount = nullaryOp L.amount +compileExpr (CheckSignature pk sig bs) = ternaryOp pk sig bs L.checkSignature +compileExpr (Sha256 c) = unaryOp c L.sha256 +compileExpr (Sha512 c) = unaryOp c L.sha512 +compileExpr (Blake2b c) = unaryOp c L.blake2B +compileExpr (HashKey hk) = unaryOp hk L.hashKey +compileExpr ChainId = nullaryOp L.chainId +compileExpr Balance = nullaryOp L.balance + +compileExpr EmptySet = nullaryOp L.emptySet + +compileExpr (Get k m) = binaryOp k m L.get +compileExpr EmptyMap = nullaryOp L.emptyMap +compileExpr EmptyBigMap = nullaryOp L.emptyBigMap + +compileExpr (Exec inp lambda) = binaryOp inp lambda L.exec +compileExpr (NonZero e) = unaryOp e L.nonZero + +-- | Convert arbitrary 'IndigoObjectF' into 'Expr', +-- having converter for fields. +objToExpr + :: forall a f . + (forall name . f name -> Expr (GetFieldType a name)) + -> IndigoObjectF f a + -> Expr a +objToExpr _ (Cell refId) = V (Cell @a refId) +objToExpr convExpr (Decomposed fields) = + ConstructWithoutNamed $ namedToTypedRec @a convExpr fields + +-- | Compile 'IndigoObjectF' to a stack cell, +-- having a function which compiles inner fields. +compileObjectF + :: forall a inp f . + (forall name . f name -> Expr (GetFieldType a name)) + -> IndigoObjectF f a + -> IndigoState inp (a & inp) () +compileObjectF _ (Cell ref) = do + md@(MetaData s _) <- iget + iput $ GenCode () (pushNoRefMd md) (varActionGet @a ref s) L.drop +compileObjectF conv obj = compileExpr $ objToExpr conv obj + +-- | Compile 'ObjectManipulation' datatype to a cell on the stack. +-- This function leverages 'ObjManipulationRes' to put off actual field compilation. +compileObjectManipulation :: forall a inp . ObjectManipulation a -> IndigoState inp (a & inp) () +compileObjectManipulation fa = case runObjectManipulation fa of + StillObject composite -> compileObjectF unNamedFieldExpr composite + OnStack comp -> comp + +-- | 'ObjManipulationRes' represents a postponed compilation of +-- 'ObjectManipulation' datatype. When 'ObjectManipulation' is being compiled +-- we are trying to put off the generation of code for work with an object +-- because we can just go to a deeper field without its "materialization" +-- onto stack. +data ObjManipulationRes inp a where + StillObject :: ObjectExpr a -> ObjManipulationRes inp a + OnStack :: IndigoState inp (a & inp) () -> ObjManipulationRes inp a + +-- | This function might look cumbersome +-- but it basically either goes deeper to an inner field or generates Lorentz code. +runObjectManipulation :: ObjectManipulation x -> ObjManipulationRes inp x +runObjectManipulation (Object e) = exprToManRes e + +runObjectManipulation (ToField (v :: ObjectManipulation dt) (targetLb :: Label fname)) = + case runObjectManipulation v of + -- In case of decomposed fields, we just go deeper. + StillObject (Decomposed fields) -> + case fieldLens @dt @fname of + -- If we access direct field, we just fetch it from fields + TargetField lb _ -> exprToManRes $ unNamedFieldExpr (fetchField @dt lb fields) + -- If we access deeper field, we fetch direct field and goes to the deeper field + DeeperField lb _ -> + let fe = unNamedFieldExpr $ fetchField @dt lb fields in + runObjectManipulation (ToField (Object fe) targetLb) + -- If stored object as cell on the stack, we get its field + -- using 'sopToField', and since this moment 'ObjManipulationRes becomes + -- a computation, not object anymore. + StillObject (Cell refId) -> + OnStack $ unaryOp (V $ Cell refId) (sopToField @dt (flSFO fieldLens) targetLb) + -- If we already got into computation, we use 'sopToField' to fetch field. + OnStack compLHS -> OnStack $ IndigoState $ \md -> + let cd = gcCode $ runIndigoState compLHS md in + GenCode () (pushNoRefMd md) (cd # sopToField (flSFO fieldLens) targetLb) L.drop + +runObjectManipulation (SetField (ev :: ObjectManipulation dt) (targetLb :: Label fname) ef) = + case runObjectManipulation ev of + StillObject lhsObj@(Decomposed fields) -> + case fieldLens @dt @fname of + -- If we set direct field, we just reassign its value with new one. + TargetField lb _ -> + StillObject $ Decomposed $ assignField @dt lb (NamedFieldExpr ef) fields + -- If we set deeper field, we need to call recursively + -- from a direct field, and set a target field of direct field. + -- Getting a new value of direct field, we set the direct field to this value. + DeeperField (lb :: Label interm) _ -> + let fe = unNamedFieldExpr (fetchField @dt lb fields) in + -- Computing new value of direct field + case runObjectManipulation (SetField (Object fe) targetLb ef) of + -- If it's still object, we just reassign direct field with it. + StillObject updField -> StillObject $ Decomposed $ + assignField @dt lb (NamedFieldExpr $ objToExpr unNamedFieldExpr updField) fields + -- Otherwise, we use power of 'L.setField' to set a new value. + OnStack rhs -> + setFieldOnStack (compileObjectF unNamedFieldExpr lhsObj) rhs (L.setField @dt @interm lb) + -- If stored object is Cell on stack, we set its field + -- using 'sopSetField', and since this moment 'ObjManipulationRes' becomes + -- a computation, not object anymore. + StillObject (Cell refId) -> + OnStack $ binaryOp ef (V $ Cell refId) $ sopSetField (flSFO fieldLens) targetLb + -- If we already got into computation, we use 'sopSetField' to set a field. + OnStack compLHS -> + setFieldOnStack compLHS (compileExpr ef) (sopSetField (flSFO $ fieldLens @dt) targetLb) + where + setFieldOnStack + :: IndigoState inp (dt & inp) () + -> IndigoState (dt & inp) (fld & dt & inp) () + -> fld & dt & inp :-> dt & inp + -> ObjManipulationRes inp dt + setFieldOnStack lhs rhs setOp = OnStack $ IndigoState $ \md -> + let GenCode _ md1 cdObj _cl1 = runIndigoState lhs md in + let GenCode _ _md2 cdFld _cl2 = runIndigoState rhs md1 in + GenCode () (pushNoRefMd md) (cdObj # cdFld # setOp) L.drop + +-- | Convert an expression to 'ObjManipulationRes'. +-- The function pattern matches on some specific cases +-- of expression those compilation into a stack cell may be postponed. +-- They include 'Decomposed' variables and 'ConstructWithoutNamed' expressions. +-- +-- This function can't be called for 'ObjMan' constructor, but we +-- take care of it just in case. +exprToManRes :: forall x inp . Expr x -> ObjManipulationRes inp x +exprToManRes (ObjMan objMan) = runObjectManipulation objMan +exprToManRes (ConstructWithoutNamed fields) = + StillObject $ Decomposed $ typedToNamedRec @x NamedFieldExpr fields +exprToManRes (V (Decomposed fields)) = + StillObject $ Decomposed $ rmap (\(NamedFieldVar f) -> NamedFieldExpr $ V f) fields +exprToManRes (V (Cell refId)) = StillObject $ Cell refId +exprToManRes ex = OnStack $ compileExpr ex + +ternaryOp + :: forall n m l ex1 ex2 ex3 res inp. (AreExprs ex1 ex2 n m, IsExpr ex3 l, KnownValue res) + => ex1 + -> ex2 + -> ex3 + -> n & m & l & inp :-> res & inp -> IndigoState inp (res & inp) () +ternaryOp e1 e2 e3 opCode = IndigoState $ \md -> + let GenCode _ md3 cd3 _cl3 = runIndigoState (compileToExpr e3) md in + let GenCode _ md2 cd2 _cl2 = runIndigoState (compileToExpr e2) md3 in + let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileToExpr e1) md2 in + GenCode () (pushNoRefMd md) (cd3 # cd2 # cd1 # opCode) L.drop + +binaryOp + :: forall n m ex1 ex2 res inp . (AreExprs ex1 ex2 n m, KnownValue res) + => ex1 -> ex2 -> n & m & inp :-> res & inp -> IndigoState inp (res & inp) () +binaryOp e1 e2 opCode = IndigoState $ \md -> + let GenCode _ md2 cd2 _cl2 = runIndigoState (compileToExpr e2) md in + let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileToExpr e1) md2 in + GenCode () (pushNoRefMd md) (cd2 # cd1 # opCode) L.drop + +unaryOp + :: forall n ex res inp . (IsExpr ex n, KnownValue res) + => ex -> n & inp :-> res & inp -> IndigoState inp (res & inp) () +unaryOp e opCode = IndigoState $ \md -> + let cd = gcCode $ runIndigoState (compileToExpr e) md in + GenCode () (pushNoRefMd md) (cd # opCode) L.drop + +nullaryOp :: KnownValue res => inp :-> res ': inp -> IndigoState inp (res ': inp) () +nullaryOp lorentzInstr = IndigoState $ \md -> + GenCode () (pushNoRefMd md) lorentzInstr L.drop + +ternaryOpFlat + :: forall n m l ex1 ex2 ex3 inp. (AreExprs ex1 ex2 n m, IsExpr ex3 l) + => ex1 + -> ex2 + -> ex3 + -> n & m & l & inp :-> inp -> IndigoState inp inp () +ternaryOpFlat e1 e2 e3 opCode = IndigoState $ \md -> + let GenCode _ md3 cd3 _cl3 = runIndigoState (compileToExpr e3) md in + let GenCode _ md2 cd2 _cl2 = runIndigoState (compileToExpr e2) md3 in + let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileToExpr e1) md2 in + GenCode () md (cd3 # cd2 # cd1 # opCode) L.nop + +binaryOpFlat + :: forall n m ex1 ex2 inp . (AreExprs ex1 ex2 n m) + => ex1 -> ex2 -> n & m & inp :-> inp -> IndigoState inp inp () +binaryOpFlat e1 e2 opCode = IndigoState $ \md -> + let GenCode _ md2 cd2 _cl2 = runIndigoState (compileToExpr e2) md in + let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileToExpr e1) md2 in + GenCode () md (cd2 # cd1 # opCode) L.nop + +unaryOpFlat + :: forall n ex inp . (IsExpr ex n) + => ex -> n & inp :-> inp -> IndigoState inp inp () +unaryOpFlat e opCode = IndigoState $ \md -> + let cd = gcCode $ runIndigoState (compileToExpr e) md in + GenCode () md (cd # opCode) L.nop + +nullaryOpFlat :: inp :-> inp -> IndigoState inp inp () +nullaryOpFlat lorentzInstr = IndigoState $ \md -> GenCode () md lorentzInstr L.nop + +compileToExpr :: ToExpr a => a -> IndigoState inp ((ExprType a) & inp) () +compileToExpr = compileExpr . toExpr diff --git a/src/Indigo/Internal/Expr/Decompose.hs b/src/Indigo/Internal/Expr/Decompose.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/Expr/Decompose.hs @@ -0,0 +1,110 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Decompose a complex value into its fields +-- to be used in 'setVar'. +-- Also functionality to generate code to deconstruct storage +-- into primitive fields the storage consists of +-- and to construct it back. +module Indigo.Internal.Expr.Decompose + ( decomposeExpr + , deepDecomposeCompose + , ExprDecomposition (..) + , IsObject + ) where + +import Data.Constraint (Dict(..)) +import Data.Vinyl.TypeLevel +import Prelude (fst) + +import Indigo.Internal.Expr.Compilation +import Indigo.Internal.Expr.Types +import Indigo.Internal.Lookup +import Indigo.Internal.Object +import Indigo.Internal.SIS +import Indigo.Internal.State +import Indigo.Lorentz +import Indigo.Prelude +import qualified Lorentz.ADT as L +import qualified Lorentz.Instr as L +import Michelson.Typed.Haskell.Instr.Product (GetFieldType) +import Util.Type + +-- | Datatype representing decomposition of 'Expr'. +data ExprDecomposition inp a where + ExprFields :: Rec Expr (FieldTypes a) -> ExprDecomposition inp a + Deconstructed :: IndigoState inp (FieldTypes a ++ inp) () -> ExprDecomposition inp a + +-- | Decompose an expression to list of its direct fields. +decomposeExpr :: ComplexObjectC a => Expr a -> ExprDecomposition inp a +decomposeExpr (ConstructWithoutNamed fields) = ExprFields fields +decomposeExpr (V v) = decomposeObjectF (\(NamedFieldVar vr) -> V vr) v +decomposeExpr (ObjMan objMan) = case runObjectManipulation objMan of + StillObject obj -> decomposeObjectF unNamedFieldExpr obj + OnStack comp -> deconstructOnStack comp +decomposeExpr ex = deconstructOnStack $ compileExpr ex + +-- | For given element on stack, generate code which +-- decomposes it to list of its deep non-decomposable fields. +-- Clean up code of 'SomeIndigoState' composes the value back. +deepDecomposeCompose + :: forall a inp . IsObject a + => SomeIndigoState (a & inp) (Var a) +deepDecomposeCompose + | Just Dict <- complexObjectDict @a = SomeIndigoState $ \md -> + let decomposedMd = fst (noRefGenCode @(FieldTypes a) $ popNoRefMd md) in + runSIS (decomposeComposeFields @(FieldTypes a)) decomposedMd $ \gc -> + SomeGenCode $ GenCode + { gcOut = Decomposed (typedToNamedRec @a typedToNamedFieldVar (gcOut gc)) + , gcMeta = gcMeta gc + , gcCode = L.deconstruct @a @(FieldTypes a) # gcCode gc + , gcClear = gcClear gc # L.constructStack @a @(FieldTypes a) + } + | otherwise = SomeIndigoState $ SomeGenCode . runIndigoState makeTopVar + where + decomposeComposeFields + :: forall flds . (KnownList flds, AllConstrained IsObject flds) + => SomeIndigoState (flds ++ inp) (Rec TypedFieldVar flds) + decomposeComposeFields = case klist @flds of + KNil -> returnSIS RNil + KCons (_ :: Proxy r) (_ :: Proxy rest) -> SomeIndigoState $ \md -> + runSIS (decomposeComposeFields @rest) (popNoRefMd md) $ \restGc -> + runSIS (deepDecomposeCompose @r) (pushNoRefMd $ gcMeta restGc) $ \curGc -> + SomeGenCode $ GenCode + { gcOut = TypedFieldVar (gcOut curGc) :& gcOut restGc + , gcMeta = gcMeta curGc + , gcCode = L.dip (gcCode restGc) # gcCode curGc + , gcClear = gcClear curGc # L.dip (gcClear restGc) + } + +-- | Decompose any 'IndigoObjectF' having decomposer for field. +decomposeObjectF + :: forall a inp f . ComplexObjectC a + => (forall name . f name -> Expr (GetFieldType a name)) + -> IndigoObjectF f a + -> ExprDecomposition inp a +decomposeObjectF _ (Cell refId) = + deconstructOnStack $ + IndigoState $ \md -> GenCode () (pushNoRefMd md) (varActionGet @a refId (mdStack md)) L.drop +decomposeObjectF unF (Decomposed fields) = + ExprFields $ namedToTypedRec @a unF fields + +-- | Deconstruct top element of the stack and return it +-- wrapped into 'Deconstructed' constructor. +deconstructOnStack + :: forall a inp . ComplexObjectC a + => IndigoState inp (a & inp) () + -> ExprDecomposition inp a +deconstructOnStack fetchFld = + Deconstructed $ IndigoState $ \md -> + let (newMd, clean) = noRefGenCode @(FieldTypes a) md in + GenCode () newMd (gcCode (runIndigoState fetchFld md) # L.deconstruct @a @(FieldTypes a)) clean + +-- | Push the passed stack cells without references to them. +noRefGenCode + :: forall rs inp . (KnownList rs, AllConstrained KnownValue rs) + => MetaData inp -> (MetaData (rs ++ inp), (rs ++ inp) :-> inp) +noRefGenCode md = case klist @rs of + KNil -> (md, L.nop) + KCons Proxy (_ :: Proxy rest) -> bimap pushNoRefMd (L.drop #) (noRefGenCode @rest md) diff --git a/src/Indigo/Internal/Expr/Symbolic.hs b/src/Indigo/Internal/Expr/Symbolic.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/Expr/Symbolic.hs @@ -0,0 +1,775 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | All the basic 'Expr'essions used in Indigo code. +-- +-- Note: infix operators acting on structure follow a naming convention: +-- +-- 1. the last character identifies the structure type: +-- +-- - @:@ for containers ('Map', 'BigMap', 'Set', 'List') +-- - @\@@ for 'UStore' +-- - @!@ for 'HasField' +-- - @~@ fot 'Util.Named' +-- +-- 2. the preceding characters identify the action: +-- +-- - @#@ for get, lookup or from +-- - @!@ for set, update or to +-- - @+@ for insert +-- - @++@ for insertNew +-- - @-@ for remove +-- - @?@ for mem or elem +-- +-- The only exception to this convention is '(.:)' (for 'cons') + +module Indigo.Internal.Expr.Symbolic + ( -- * Basic + constExpr, varExpr, cast + + -- * Math + , add, sub, mul, div, mod, neg, abs + , (+), (-), (*), (/), (%) + + -- * Comparison + , eq, neq, lt, gt, le, ge + , (==), (/=), (<), (>), (<=), (>=) + + -- * Conversion + , isNat, toInt, nonZero + + -- * Bits and boolean + , lsl, lsr, and, or, xor, not + , (<<<), (>>>), (&&), (||), (^) + + -- * Serialization + , pack, unpack + + -- * Pairs + , pair, car, cdr, fst, snd + + -- * Maybe + , some, none + + -- * Either + , right, left + + -- * Bytes and string + , slice, concat, (<>) + + -- * List + , concatAll, nil, cons, (.:) + + -- * Containers + , get, update, insert, remove, mem, size + , (#:), (!:), (+:), (-:), (?:) + , empty, emptyBigMap, emptyMap, emptySet + + -- * UStore + , uGet, uUpdate, uInsert, uInsertNew, uDelete, uMem + , (#@), (!@), (+@), (++@), (-@), (?@) + + -- * HasField + , (!!), (#!) + + -- * Record and Named + , name, unName, (!~), (#~) + , construct, constructRec + + -- * Contract + , contract + , self + , contractAddress + , contractCallingUnsafe + , contractCallingString + , runFutureContract + , implicitAccount + , convertEpAddressToContract + , makeView + , makeVoid + + -- * Auxiliary + , now + , amount + , sender + , blake2b + , sha256 + , sha512 + , hashKey + , chainId + , balance + , checkSignature + ) where + +import Data.Vinyl.Core (RMap(..)) + +import Indigo.Internal.Expr.Types +import Indigo.Internal.Field +import Indigo.Internal.Object (Var) +import Indigo.Lorentz +import Indigo.Prelude +import qualified Michelson.Typed.Arith as M +import Util.TypeTuple +import Michelson.Text (unMText) +import Michelson.Untyped.EntryPoints (unsafeBuildEpName) + +---------------------------------------------------------------------------- +-- Basic +---------------------------------------------------------------------------- + +constExpr :: NiceConstant a => a -> Expr a +constExpr = C + +-- | Create an expression holding a variable. +varExpr :: KnownValue a => Var a -> Expr a +varExpr = V + +cast :: (ex :~> a) => ex -> Expr a +cast = Cast + +---------------------------------------------------------------------------- +-- Math +---------------------------------------------------------------------------- + +infixl 6 + +add, (+) + :: IsArithExpr exN exM M.Add n m + => exN -> exM + -> Expr (ArithResHs M.Add n m) +add = Add +(+) = Add + +infixl 6 - +sub, (-) + :: IsArithExpr exN exM M.Sub n m + => exN -> exM + -> Expr (ArithResHs M.Sub n m) +sub = Sub +(-) = Sub + +infixl 7 * +mul, (*) + :: IsArithExpr exN exM M.Mul n m + => exN -> exM + -> Expr (ArithResHs M.Mul n m) +mul = Mul +(*) = Mul + +infixl 7 / +div, (/) + :: IsDivExpr exN exM n m + => exN -> exM + -> Expr (EDivOpResHs n m) +div = Div +(/) = Div + +infixl 7 % +mod, (%) + :: IsModExpr exN exM n m + => exN -> exM + -> Expr (EModOpResHs n m) +mod = Mod +(%) = Mod + +abs + :: IsUnaryArithExpr exN M.Abs n + => exN + -> Expr (UnaryArithResHs M.Abs n) +abs = Abs + +neg + :: IsUnaryArithExpr exN M.Neg n + => exN + -> Expr (UnaryArithResHs M.Neg n) +neg = Neg + +---------------------------------------------------------------------------- +-- Comparison +---------------------------------------------------------------------------- + +infix 4 == +eq, (==) + :: (NiceComparable n, AreExprs c c1 n n) + => c -> c1 + -> Expr Bool +eq = Eq' +(==) = Eq' + +infix 4 /= +neq, (/=) + :: (NiceComparable n, AreExprs c c1 n n) + => c -> c1 + -> Expr Bool +neq = Neq +(/=) = Neq + +infix 4 < +lt, (<) + :: (NiceComparable n, AreExprs c c1 n n) + => c -> c1 + -> Expr Bool +lt = Lt +(<) = Lt + +infix 4 > +gt, (>) + :: (NiceComparable n, AreExprs c c1 n n) + => c -> c1 + -> Expr Bool +gt = Gt +(>) = Gt + +infix 4 <= +le, (<=) + :: (NiceComparable n, AreExprs c c1 n n) + => c -> c1 + -> Expr Bool +le = Le +(<=) = Le + +infix 4 >= +ge, (>=) + :: (NiceComparable n, AreExprs c c1 n n) + => c -> c1 + -> Expr Bool +ge = Ge +(>=) = Ge + +---------------------------------------------------------------------------- +-- Conversion +---------------------------------------------------------------------------- + +isNat :: (ex :~> Integer) => ex -> Expr (Maybe Natural) +isNat = IsNat + +toInt :: (ex :~> Natural) => ex -> Expr Integer +toInt = Int' + +nonZero :: (ex :~> n, NonZero n, KnownValue (Maybe n)) => ex -> Expr (Maybe n) +nonZero = NonZero + +---------------------------------------------------------------------------- +-- Bits and boolean +---------------------------------------------------------------------------- + +infixl 8 <<< +lsl, (<<<) + :: IsArithExpr exN exM M.Lsl n m + => exN -> exM + -> Expr (ArithResHs M.Lsl n m) +lsl = Lsl +(<<<) = Lsl + +infixl 8 >>> +lsr, (>>>) + :: IsArithExpr exN exM M.Lsr n m + => exN -> exM + -> Expr (ArithResHs M.Lsr n m) +lsr = Lsr +(>>>) = Lsr + +infixr 2 || +or, (||) + :: IsArithExpr exN exM M.Or n m + => exN -> exM + -> Expr (ArithResHs M.Or n m) +or = Or +(||) = Or + +infixr 3 && +and, (&&) + :: IsArithExpr exN exM M.And n m + => exN -> exM + -> Expr (ArithResHs M.And n m) +and = And +(&&) = And + +infixr 2 ^ +xor, (^) + :: IsArithExpr exN exM M.Xor n m + => exN -> exM + -> Expr (ArithResHs M.Xor n m) +xor = Xor +(^) = Xor + +not + :: IsUnaryArithExpr exN M.Not n + => exN + -> Expr (UnaryArithResHs M.Not n) +not = Not + +---------------------------------------------------------------------------- +-- Serialization +---------------------------------------------------------------------------- + +pack :: (IsExpr ex a, NicePackedValue a) => ex -> Expr ByteString +pack = Pack + +unpack :: (NiceUnpackedValue a, exb :~> ByteString) => exb -> Expr (Maybe a) +unpack = Unpack + +---------------------------------------------------------------------------- +-- Pairs +---------------------------------------------------------------------------- + +pair :: (AreExprs ex1 ex2 n m, KnownValue (n, m)) => ex1 -> ex2 -> Expr (n, m) +pair = Pair + +car, fst :: (op :~> (n, m), KnownValue n) => op -> Expr n +car = Fst +fst = Fst + +cdr, snd :: (op :~> (n, m), KnownValue m) => op -> Expr m +cdr = Snd +snd = Snd + +---------------------------------------------------------------------------- +-- Maybe +---------------------------------------------------------------------------- + +some :: (ex :~> t, KnownValue (Maybe t)) => ex -> Expr (Maybe t) +some = Some + +none :: KnownValue t => Expr (Maybe t) +none = None + +---------------------------------------------------------------------------- +-- Either +---------------------------------------------------------------------------- + +right :: (ex :~> x, KnownValue y, KnownValue (Either y x)) => ex -> Expr (Either y x) +right = Right' + +left :: (ex :~> y, KnownValue x, KnownValue (Either y x)) => ex -> Expr (Either y x) +left = Left' + +---------------------------------------------------------------------------- +-- Bytes and string +---------------------------------------------------------------------------- + +slice + :: ( an :~> Natural + , bn :~> Natural + , IsSliceExpr ex c + ) + => (an, bn) -> ex + -> Expr (Maybe c) +slice (a, b) = Slice a b + +infixr 6 <> +concat, (<>) + :: IsConcatExpr exN1 exN2 n + => exN1 -> exN2 + -> Expr n +concat = Concat +(<>) = Concat + +---------------------------------------------------------------------------- +-- List +---------------------------------------------------------------------------- + +infixr 5 .: +cons, (.:) :: (ex1 :~> a, ex2 :~> List a) => ex1 -> ex2 -> Expr (List a) +cons = Cons +(.:) = Cons + +concatAll :: IsConcatListExpr exN n => exN -> Expr n +concatAll = Concat' + +nil :: KnownValue a => Expr (List a) +nil = Nil + +---------------------------------------------------------------------------- +-- Containers +---------------------------------------------------------------------------- + +class ExprMagma c where + empty :: (NiceComparable (UpdOpKeyHs c), KnownValue c) => Expr c + +instance KnownValue v => ExprMagma (BigMap k v) where + empty = EmptyBigMap + +instance KnownValue v => ExprMagma (Map k v) where + empty = EmptyMap + +instance ExprMagma (Set k) where + empty = EmptySet + +-- | Expression class to insert an element into a data structure. +-- +-- Note that while this is based on 'update' and 'UpdOpHs', it is necessary to +-- have different instances to allow for different 'update' parameter types, +-- ('Set' uses a 'Bool' instead of a 'Maybe'), just like 'ExprRemovable'. +-- +-- Moreover, this class is parameterized with an @insParam@ as well in order to +-- have both key-value pairs ('Map' and 'BigMap') as well as key only ('Set'). +class UpdOpHs c => ExprInsertable c insParam where + insert :: ex :~> c => insParam -> ex -> Expr c + +instance (NiceComparable k, exKey :~> k, exValue :~> v) + => ExprInsertable (BigMap k v) (exKey, exValue) where + insert (k, v) c = Update c k (some v) + +instance (NiceComparable k, exKey :~> k, exValue :~> v) + => ExprInsertable (Map k v) (exKey, exValue) where + insert (k, v) c = Update c k (some v) + +instance (NiceComparable a, exKey :~> a) => ExprInsertable (Set a) exKey where + insert k c = Update c k True + +-- | Expression class to remove an element from a data structure. +-- +-- Note that while this is based on 'update' and 'UpdOpHs', it is necessary to +-- have different instances to allow for different 'update' parameter types, +-- ('Set' uses a 'Bool' instead of a 'Maybe'). +class UpdOpHs c => ExprRemovable c where + remove + :: (exStruct :~> c, exKey :~> UpdOpKeyHs c) + => exKey -> exStruct -> Expr c + +instance (NiceComparable k, KnownValue v) => ExprRemovable (BigMap k v) where + remove k c = Update c k none + +instance (NiceComparable k, KnownValue v) => ExprRemovable (Map k v) where + remove k c = Update c k none + +instance NiceComparable a => ExprRemovable (Set a) where + remove k c = Update c k False + +get + :: IsGetExpr exKey exMap map + => exKey -> exMap + -> Expr (Maybe (GetOpValHs map)) +get = Get + +update + :: IsUpdExpr exKey exVal exMap map + => (exKey, exVal) -> exMap + -> Expr map +update (k, v) s = Update s k v + +mem + :: IsMemExpr exKey exN n + => exKey -> exN + -> Expr Bool +mem = Mem + +size + :: IsSizeExpr exN n + => exN -> Expr Natural +size = Size + +infixl 8 #: +(#:) + :: IsGetExpr exKey exMap map + => exMap -> exKey + -> Expr (Maybe (GetOpValHs map)) +(#:) = flip get + +infixl 8 !: +(!:) + :: IsUpdExpr exKey exVal exMap map + => exMap -> (exKey, exVal) + -> Expr map +(!:) = flip update + +infixl 8 +: +(+:) + :: ( ExprInsertable c exParam + , exStructure :~> c + ) + => exStructure -> exParam + -> Expr c +(+:) = flip insert + +infixl 8 -: +(-:) + :: ( ExprRemovable c + , exStruct :~> c + , exKey :~> UpdOpKeyHs c + ) + => exStruct -> exKey + -> Expr c +(-:) = flip remove + +infixl 8 ?: +(?:) + :: IsMemExpr exKey exN n + => exN -> exKey + -> Expr Bool +(?:) = flip mem + +emptyBigMap + :: (KnownValue value, NiceComparable key, KnownValue (BigMap key value)) + => Expr (BigMap key value) +emptyBigMap = empty + +emptyMap + :: (KnownValue value, NiceComparable key, KnownValue (Map key value)) + => Expr (Map key value) +emptyMap = empty + +emptySet + :: (NiceComparable key, KnownValue (Set key)) + => Expr (Set key) +emptySet = empty + +---------------------------------------------------------------------------- +-- UStore +---------------------------------------------------------------------------- + +infixr 8 #@ +uGet, (#@) + :: ( HasUStore name key value store + , exKey :~> key + , exStore :~> (UStore store) + ) + => exStore -> (Label name, exKey) + -> Expr (Maybe value) +uGet store (uName, key) = UGet uName key store +(#@) = uGet + +infixl 8 !@ +uUpdate, (!@) + :: ( HasUStore name key value store + , exKey :~> key + , exVal :~> Maybe value + , exStore :~> UStore store + ) + => exStore -> (Label name, exKey, exVal) + -> Expr (UStore store) +uUpdate store (uName, key, val) = UUpdate uName key val store +(!@) = uUpdate + +infixr 8 +@ +uInsert, (+@) + :: ( HasUStore name key value store + , exKey :~> key + , exVal :~> value + , exStore :~> UStore store + ) + => exStore -> (Label name, exKey, exVal) + -> Expr (UStore store) +uInsert store (uName, key, val) = UInsert uName key val store +(+@) = uInsert + +infixr 8 ++@ +uInsertNew, (++@) + :: ( HasUStore name key value store + , IsError err + , exKey :~> key + , exVal :~> value + , exStore :~> UStore store + ) + => exStore + -> (Label name, err, exKey, exVal) + -> Expr (UStore store) +uInsertNew store (uName, err, key, val) = UInsertNew uName err key val store +(++@) = uInsertNew + +infixl 8 -@ +uDelete, (-@) + :: ( HasUStore name key value store + , exKey :~> key + , exStore :~> (UStore store) + ) + => exStore -> (Label name, exKey) + -> Expr (UStore store) +uDelete store (uName, key) = UDelete uName key store +(-@) = uDelete + +infixl 8 ?@ +uMem, (?@) + :: ( HasUStore name key value store + , exKey :~> key + , exStore :~> (UStore store) + ) + => exStore -> (Label name, exKey) + -> Expr Bool +uMem store (uName, key) = UMem uName key store +(?@) = uMem + +---------------------------------------------------------------------------- +-- HasField +---------------------------------------------------------------------------- + +infixl 8 #! +(#!) + :: (HasField dt name ftype, exDt :~> dt) + => exDt + -> Label name + -> Expr ftype +(#!) (toExpr -> (ObjMan fa)) fName = ObjMan (ToField fa fName) +(#!) exDt fName = ObjMan (ToField (Object $ toExpr exDt) fName) + +infixl 8 !! +(!!) + :: ( HasField dt name ftype + , exDt :~> dt + , exFld :~> ftype + ) + => exDt + -> (Label name, exFld) + -> Expr dt +(!!) (toExpr -> (ObjMan fa)) (fName, fld) = ObjMan (SetField fa fName (toExpr fld)) +dt !! (fName, fld) = ObjMan (SetField (Object $ toExpr dt) fName (toExpr fld)) + +---------------------------------------------------------------------------- +-- Record and Named +---------------------------------------------------------------------------- + +name :: (ex :~> t, KnownValue (name :! t)) => Label name -> ex -> Expr (name :! t) +name = Name + +unName :: (ex :~> (name :! t), KnownValue t) => Label name -> ex -> Expr t +unName = UnName + +infixl 8 !~ +(!~) + :: (ex :~> t, KnownValue (name :! t)) + => ex -> Label name + -> Expr (name :! t) +(!~) = flip name + +infixl 8 #~ +(#~) + :: (ex :~> (name :! t), KnownValue t) + => ex -> Label name + -> Expr t +(#~) = flip unName + +construct + :: ( InstrConstructC dt, KnownValue dt + , RMap (ConstructorFieldTypes dt) + , fields ~ Rec Expr (ConstructorFieldTypes dt) + , RecFromTuple fields + ) + => IsoRecTuple fields -> Expr dt +construct = Construct . recFromTuple + +constructRec + :: ( InstrConstructC dt + , RMap (ConstructorFieldTypes dt) + , KnownValue dt + ) + => Rec Expr (ConstructorFieldTypes dt) + -> Expr dt +constructRec = Construct + +---------------------------------------------------------------------------- +-- Contract +---------------------------------------------------------------------------- + +contract + :: ( NiceParameterFull p + , NoExplicitDefaultEntryPoint p + , ToTAddress p addr + , ToT addr ~ ToT Address + , exAddr :~> addr + ) + => exAddr -> Expr (Maybe (ContractRef p)) +contract = Contract + +self + :: ( NiceParameterFull p + , NoExplicitDefaultEntryPoint p + ) + => Expr (ContractRef p) +self = Self + +contractAddress :: (exc :~> ContractRef p) => exc -> Expr Address +contractAddress = ContractAddress + +contractCallingUnsafe + :: ( NiceParameter arg + , exAddr :~> Address + ) + => EpName -> exAddr -> Expr (Maybe (ContractRef arg)) +contractCallingUnsafe = ContractCallingUnsafe + +contractCallingString + :: ( NiceParameter arg + , exAddr :~> Address + ) + => MText -> exAddr -> Expr (Maybe (ContractRef arg)) +contractCallingString = + contractCallingUnsafe + . unsafeBuildEpName + . unMText + +runFutureContract + :: ( NiceParameter p + , conExpr :~> FutureContract p + ) + => conExpr -> Expr (Maybe (ContractRef p)) +runFutureContract = RunFutureContract + +implicitAccount + :: (exkh :~> KeyHash) + => exkh + -> Expr (ContractRef ()) +implicitAccount = ImplicitAccount + +convertEpAddressToContract + :: ( NiceParameter p + , epExpr :~> EpAddress + ) + => epExpr -> Expr (Maybe (ContractRef p)) +convertEpAddressToContract = ConvertEpAddressToContract + +makeView + :: ( KnownValue (View a r) + , exa :~> a + , exCRef :~> ContractRef r + ) + => exa -> exCRef -> Expr (View a r) +makeView = MakeView + +makeVoid + :: ( KnownValue (Void_ a b) + , exa :~> a + , exCRef :~> Lambda b b + ) + => exa -> exCRef -> Expr (Void_ a b) +makeVoid = MakeVoid + +---------------------------------------------------------------------------- +-- Auxiliary +---------------------------------------------------------------------------- + +now :: Expr Timestamp +now = Now + +amount :: Expr Mutez +amount = Amount + +sender :: Expr Address +sender = Sender + +checkSignature + :: ( pkExpr :~> PublicKey + , sigExpr :~> Signature + , hashExpr :~> ByteString + ) + => pkExpr -> sigExpr -> hashExpr + -> Expr Bool +checkSignature = CheckSignature + +sha256 :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString +sha256 = Sha256 + +sha512 :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString +sha512 = Sha512 + +blake2b :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString +blake2b = Blake2b + +hashKey :: (keyExpr :~> PublicKey) => keyExpr -> Expr KeyHash +hashKey = HashKey + +chainId :: Expr ChainId +chainId = ChainId + +balance :: Expr Mutez +balance = Balance diff --git a/src/Indigo/Internal/Expr/Types.hs b/src/Indigo/Internal/Expr/Types.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/Expr/Types.hs @@ -0,0 +1,538 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | 'Expr' data type and its generalizations + +module Indigo.Internal.Expr.Types + ( -- * The Expr data type + Expr (..) + + -- * Generalizations of Expr + , IsExpr + , AreExprs + , ToExpr + , ExprType + , (:~>) + , toExpr + + -- * Arithmetic Expr + , IsArithExpr + , IsUnaryArithExpr + + -- * Polymorphic Expr + , IsConcatExpr + , IsConcatListExpr + , IsDivExpr + , IsModExpr + , IsGetExpr + , IsMemExpr + , IsSizeExpr + , IsSliceExpr + , IsUpdExpr + + , ObjectManipulation (..) + , ObjectExpr + , NamedFieldExpr (..) + ) where + +import qualified Data.Kind as Kind +import Data.Vinyl.Core (RMap(..)) + +import Indigo.Prelude (Either (..), id) +import Indigo.Lorentz +import Indigo.Internal.Field +import Indigo.Internal.Object (Var, IndigoObjectF (..), FieldTypes, ComplexObjectC) +import qualified Michelson.Typed.Arith as M +import Michelson.Typed.Haskell.Instr.Product (GetFieldType) + +---------------------------------------------------------------------------- +-- The Expr data type +---------------------------------------------------------------------------- + +data Expr a where + C :: NiceConstant a => a -> Expr a + + V :: KnownValue a => Var a -> Expr a + + ObjMan :: ObjectManipulation a -> Expr a + + Cast + :: (ex :~> a) + => ex -> Expr a + + Size :: (IsExpr exc c, SizeOpHs c) + => exc -> Expr Natural + + Update + :: ( UpdOpHs c + , IsExpr exKey (UpdOpKeyHs c) + , IsExpr exVal (UpdOpParamsHs c) + , IsExpr exStructure c + ) + => exStructure -> exKey -> exVal -> Expr c + + Add :: (AreExprs ex1 ex2 n m, ArithOpHs M.Add n m, KnownValue (ArithResHs M.Add n m)) + => ex1 -> ex2 -> Expr (ArithResHs M.Add n m) + + Sub :: (AreExprs ex1 ex2 n m, ArithOpHs M.Sub n m, KnownValue (ArithResHs M.Sub n m)) + => ex1 -> ex2 -> Expr (ArithResHs M.Sub n m) + + Mul :: (AreExprs ex1 ex2 n m, ArithOpHs M.Mul n m, KnownValue (ArithResHs M.Mul n m)) + => ex1 -> ex2 -> Expr (ArithResHs M.Mul n m) + + Div :: (AreExprs ex1 ex2 n m, EDivOpHs n m, KnownValue (EDivOpResHs n m)) + => ex1 -> ex2 -> Expr (EDivOpResHs n m) + + Mod :: (AreExprs ex1 ex2 n m, EDivOpHs n m, KnownValue (EModOpResHs n m)) + => ex1 -> ex2 -> Expr (EModOpResHs n m) + + Abs :: (IsExpr ex n, UnaryArithOpHs M.Abs n, KnownValue (UnaryArithResHs M.Abs n)) + => ex -> Expr (UnaryArithResHs M.Abs n) + + Neg :: (IsExpr ex n, UnaryArithOpHs M.Neg n, KnownValue (UnaryArithResHs M.Neg n)) + => ex -> Expr (UnaryArithResHs M.Neg n) + + + Lsl :: (AreExprs ex1 ex2 n m, ArithOpHs M.Lsl n m, KnownValue (ArithResHs M.Lsl n m)) + => ex1 -> ex2 -> Expr (ArithResHs M.Lsl n m) + + Lsr :: (AreExprs ex1 ex2 n m, ArithOpHs M.Lsr n m, KnownValue (ArithResHs M.Lsr n m)) + => ex1 -> ex2 -> Expr (ArithResHs M.Lsr n m) + + + Eq' :: ( AreExprs ex1 ex2 n n + , NiceComparable n + ) + => ex1 -> ex2 -> Expr Bool + + Neq :: ( AreExprs ex1 ex2 n n + , NiceComparable n + ) + => ex1 -> ex2 -> Expr Bool + + Le :: ( AreExprs ex1 ex2 n n + , NiceComparable n + ) + => ex1 -> ex2 -> Expr Bool + + Lt :: ( AreExprs ex1 ex2 n n + , NiceComparable n + ) + => ex1 -> ex2 -> Expr Bool + + Ge :: ( AreExprs ex1 ex2 n n + , NiceComparable n + ) + => ex1 -> ex2 -> Expr Bool + + Gt :: ( AreExprs ex1 ex2 n n + , NiceComparable n + ) + => ex1 -> ex2 -> Expr Bool + + Or :: (AreExprs ex1 ex2 n m, ArithOpHs M.Or n m, KnownValue (ArithResHs M.Or n m)) + => ex1 -> ex2 -> Expr (ArithResHs M.Or n m) + + Xor :: (AreExprs ex1 ex2 n m, ArithOpHs M.Xor n m, KnownValue (ArithResHs M.Xor n m)) + => ex1 -> ex2 -> Expr (ArithResHs M.Xor n m) + + And :: (AreExprs ex1 ex2 n m, ArithOpHs M.And n m, KnownValue (ArithResHs M.And n m)) + => ex1 -> ex2 -> Expr (ArithResHs M.And n m) + + Not :: (IsExpr op n, UnaryArithOpHs M.Not n, KnownValue (UnaryArithResHs M.Not n)) + => op -> Expr (UnaryArithResHs M.Not n) + + Int' + :: IsExpr ex Natural + => ex -> Expr Integer + + IsNat + :: IsExpr ex Integer + => ex -> Expr (Maybe Natural) + + + Fst :: (IsExpr op (n, m), KnownValue n) => op -> Expr n + Snd :: (IsExpr op (n, m), KnownValue m) => op -> Expr m + + Pair :: (AreExprs ex1 ex2 n m, KnownValue (n, m)) => ex1 -> ex2 -> Expr (n, m) + + Some :: (IsExpr ex t, KnownValue (Maybe t)) => ex -> Expr (Maybe t) + None :: KnownValue t => Expr (Maybe t) + + Right' :: (IsExpr ex x, KnownValue y, KnownValue (Either y x)) => ex -> Expr (Either y x) + Left' :: (IsExpr ex y, KnownValue x, KnownValue (Either y x)) => ex -> Expr (Either y x) + + Mem + :: ( MemOpHs c + , IsExpr exc c + , IsExpr exck (MemOpKeyHs c) + ) + => exck -> exc -> Expr Bool + + UGet + :: ( HasUStore name key value store + , IsExpr exKey key + , IsExpr exStore (UStore store) + , KnownValue value + ) + => Label name -> exKey -> exStore -> Expr (Maybe value) + + UInsertNew + :: ( HasUStore name key value store + , IsError err + , IsExpr exKey key + , IsExpr exVal value + , IsExpr exStore (UStore store) + ) + => Label name -> err + -> exKey -> exVal -> exStore -> Expr (UStore store) + + UInsert + :: ( HasUStore name key value store + , IsExpr exKey key + , IsExpr exVal value + , IsExpr exStore (UStore store) + ) + => Label name + -> exKey -> exVal -> exStore -> Expr (UStore store) + + UMem + :: ( HasUStore name key val store + , exKey :~> key + , exStore :~> UStore store + , KnownValue val + ) + => Label name -> exKey -> exStore -> Expr Bool + + UUpdate + :: ( HasUStore name key val store + , exKey :~> key + , exVal :~> Maybe val + , exStore :~> UStore store + ) + => Label name -> exKey -> exVal -> exStore -> Expr (UStore store) + + UDelete + :: ( HasUStore name key val store + , exKey :~> key + , exStore :~> UStore store + ) + => Label name -> exKey -> exStore -> Expr (UStore store) + + Construct + :: ( InstrConstructC dt + , RMap (ConstructorFieldTypes dt) + , KnownValue dt + ) + => Rec Expr (ConstructorFieldTypes dt) -> Expr dt + + -- TODO remove Construct and rename this one + ConstructWithoutNamed + :: ComplexObjectC dt + => Rec Expr (FieldTypes dt) -> Expr dt + + Name + :: (IsExpr ex t, KnownValue (name :! t)) + => Label name -> ex -> Expr (name :! t) + UnName + :: (IsExpr ex (name :! t), KnownValue t) + => Label name -> ex -> Expr t + + EmptySet + :: (NiceComparable key, KnownValue (Set key)) + => Expr (Set key) + + Get + :: ( GetOpHs c + , KnownValue (Maybe (GetOpValHs c)) + , IsExpr exKey (GetOpKeyHs c) + , IsExpr exMap c + , KnownValue (GetOpValHs c) + ) + => exKey -> exMap -> Expr (Maybe (GetOpValHs c)) + + EmptyMap + :: (KnownValue value, NiceComparable key, KnownValue (Map key value)) + => Expr (Map key value) + + EmptyBigMap + :: (KnownValue value, NiceComparable key, KnownValue (BigMap key value)) + => Expr (BigMap key value) + + Pack + :: (IsExpr ex a, NicePackedValue a) + => ex -> Expr ByteString + + Unpack + :: ( NiceUnpackedValue a + , IsExpr bsExpr ByteString + ) + => bsExpr -> Expr (Maybe a) + + Cons + :: ( IsExpr ex1 a + , IsExpr ex2 (List a) + ) + => ex1 -> ex2 -> Expr (List a) + + Nil :: KnownValue a => Expr (List a) + + Concat + :: ( IsExpr ex1 c + , IsExpr ex2 c + , ConcatOpHs c + ) + => ex1 -> ex2 -> Expr c + + Concat' + :: ( IsExpr ex (List c) + , ConcatOpHs c + , KnownValue c + ) + => ex -> Expr c + + Slice + :: ( IsExpr ex c + , SliceOpHs c + , IsExpr an Natural + , IsExpr bn Natural + ) + => an -> bn -> ex -> Expr (Maybe c) + + Contract + :: ( NiceParameterFull p + , NoExplicitDefaultEntryPoint p + , ToTAddress p addr + , ToT addr ~ ToT Address + , IsExpr exAddr addr + ) + => exAddr -> Expr (Maybe (ContractRef p)) + + Self + :: ( NiceParameterFull p + , NoExplicitDefaultEntryPoint p + ) + => Expr (ContractRef p) + + ContractAddress + :: IsExpr exc (ContractRef p) + => exc -> Expr Address + + ContractCallingUnsafe + :: ( NiceParameter arg + , IsExpr exAddr Address + ) + => EpName -> exAddr -> Expr (Maybe (ContractRef arg)) + + RunFutureContract + :: ( NiceParameter p + , IsExpr conExpr (FutureContract p) + ) + => conExpr -> Expr (Maybe (ContractRef p)) + + ImplicitAccount + :: (IsExpr exkh KeyHash) + => exkh -> Expr (ContractRef ()) + + ConvertEpAddressToContract + :: ( NiceParameter p + , IsExpr epExpr EpAddress + ) + => epExpr -> Expr (Maybe (ContractRef p)) + + MakeView + :: ( KnownValue (View a r) + , exa :~> a + , exCRef :~> ContractRef r + ) + => exa -> exCRef -> Expr (View a r) + + MakeVoid + :: ( KnownValue (Void_ a b) + , exa :~> a + , exCRef :~> Lambda b b + ) + => exa -> exCRef -> Expr (Void_ a b) + + CheckSignature + :: ( IsExpr pkExpr PublicKey + , IsExpr sigExpr Signature + , IsExpr hashExpr ByteString + ) + => pkExpr -> sigExpr -> hashExpr -> Expr Bool + + Sha256 :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString + Sha512 :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString + Blake2b :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString + HashKey :: (IsExpr keyExpr PublicKey) => keyExpr -> Expr KeyHash + + ChainId :: Expr ChainId + + Now :: Expr Timestamp + Amount :: Expr Mutez + Balance :: Expr Mutez + Sender :: Expr Address + + Exec + :: ( IsExpr exA a, IsExpr exLambda (Lambda a b) + , KnownValue b + ) + => exA -> exLambda -> Expr b + + NonZero + :: (IsExpr ex n, NonZero n, KnownValue (Maybe n)) + => ex -> Expr (Maybe n) + +---------------------------------------------------------------------------- +-- Object manipulation +---------------------------------------------------------------------------- + +-- | Datatype describing access to an inner fields of object, like +-- @object !. field1 !. field2 ~. (field3, value3) ~. (field4, value4)@ +data ObjectManipulation a where + Object :: Expr a -> ObjectManipulation a + + ToField + :: HasField dt fname ftype + => ObjectManipulation dt + -> Label fname + -> ObjectManipulation ftype + + -- NB. @SetField (Object expr) field1 + -- (ObjMan $ SetField (ToField (Object expr) field1) field2 targetExpr)@ + -- is a bad representation, which will cause generation of not optimal code + -- (like expr would be materialized object), + -- so it would be nice to enforce only + -- @SetField (Object expr) (field1 . field2) targetExpr@ representation. + SetField + :: HasField dt fname ftype + => ObjectManipulation dt + -> Label fname + -> Expr ftype + -> ObjectManipulation dt + +-- | Auxiliary datatype where each field refers to +-- an expression the field equals to. It's not recursive one. +data NamedFieldExpr a name where + NamedFieldExpr + :: { unNamedFieldExpr :: Expr (GetFieldType a name) } + -> NamedFieldExpr a name + +type ObjectExpr a = IndigoObjectF (NamedFieldExpr a) a + +---------------------------------------------------------------------------- +-- Generalizations of Expr +---------------------------------------------------------------------------- + +type IsExpr op n = (ToExpr op, ExprType op ~ n, KnownValue n) +type (:~>) op n = IsExpr op n + +type AreExprs ex1 ex2 n m = (IsExpr ex1 n, IsExpr ex2 m) + +type ExprType a = ExprType' (Decide a) a + +toExpr :: forall a . ToExpr a => a -> Expr (ExprType a) +toExpr = toExpr' @(Decide a) @a + +class ToExpr' (Decide x) x => ToExpr x +instance ToExpr' (Decide x) x => ToExpr x + +-- This type class is needed to cope with overlapping instances. +class ToExpr' decision c where + type family ExprType' decision c :: Kind.Type + toExpr' :: c -> Expr (ExprType' decision c) + +-- Instance for a var +instance KnownValue (a :: Kind.Type) => ToExpr' 'VarD (Var a) where + type instance ExprType' 'VarD (Var a) = a + toExpr' = V + +-- Instance for a value +instance NiceConstant a => ToExpr' 'ValD a where + type instance ExprType' 'ValD a = a + toExpr' = C + +-- Instance for StructManipulation +instance ToExpr' 'ObjManD (ObjectManipulation a) where + type instance ExprType' 'ObjManD (ObjectManipulation a) = a + toExpr' = ObjMan + +-- Instance for Expr itself +instance ToExpr' 'ExprD (Expr a) where + type instance ExprType' 'ExprD (Expr a) = a + toExpr' = id + +data Decision = VarD | ValD | ExprD | ObjManD + +type family Decide x :: Decision where + Decide (Var _) = 'VarD + Decide (Expr _) = 'ExprD + Decide (ObjectManipulation _) = 'ObjManD + Decide _ = 'ValD + +type IsUnaryArithExpr exN a n = + ( exN :~> n + , UnaryArithOpHs a n + , KnownValue (UnaryArithResHs a n) + ) + +type IsArithExpr exN exM a n m = + ( AreExprs exN exM n m + , ArithOpHs a n m + , KnownValue (ArithResHs a n m) + ) + +type IsDivExpr exN exM n m = + ( AreExprs exN exM n m + , EDivOpHs n m + , KnownValue (EDivOpResHs n m) + ) + +type IsModExpr exN exM n m = + ( AreExprs exN exM n m + , EDivOpHs n m + , KnownValue (EModOpResHs n m) + ) + +type IsConcatExpr exN1 exN2 n = + ( exN1 :~> n + , exN2 :~> n + , ConcatOpHs n + ) + +type IsConcatListExpr exN n = + ( exN :~> List n + , ConcatOpHs n + , KnownValue n + ) + +type IsSliceExpr exN n = + ( exN :~> n + , SliceOpHs n + ) + +type IsGetExpr exKey exMap map = + ( exKey :~> GetOpKeyHs map + , exMap :~> map + , GetOpHs map + , KnownValue (GetOpValHs map) + ) + +type IsUpdExpr exKey exVal exMap map = + ( exKey :~> UpdOpKeyHs map + , exVal :~> UpdOpParamsHs map + , exMap :~> map + , UpdOpHs map + ) + +type IsMemExpr exKey exN n = + ( exKey :~> MemOpKeyHs n + , exN :~> n + , MemOpHs n + ) + +type IsSizeExpr exN n = + ( exN :~> n + , SizeOpHs n + ) diff --git a/src/Indigo/Internal/Field.hs b/src/Indigo/Internal/Field.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/Field.hs @@ -0,0 +1,138 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{- | This module contains a datatype representing a lens to a field, +helpers to compose new lens, and type class like StoreHasField returning a lens. -} + +module Indigo.Internal.Field + ( AccessFieldC + , fetchField + , assignField + + -- * Lens + , FieldLens (..) + , flSFO + -- * HasLens + , HasField (..) + , fieldLensDeeper + , fieldLensADT + ) where + +import Data.Vinyl (RElem) +import Data.Vinyl.TypeLevel (RIndex) +import Data.Vinyl.Lens (rget, rput) +import GHC.TypeLits (KnownSymbol) + +import Indigo.Lorentz +import Indigo.Prelude +import qualified Lorentz.ADT as L +import Michelson.Typed.Haskell.Instr.Product + (GetFieldType, InstrSetFieldC, InstrGetFieldC, ConstructorFieldNames) + +-- | Constraint to access/assign field stored in Rec +type AccessFieldC a name = + RElem name (ConstructorFieldNames a) (RIndex name (ConstructorFieldNames a)) + +-- | Get a field from list of fields +fetchField + :: forall a name f proxy . AccessFieldC a name + => proxy name -> Rec f (ConstructorFieldNames a) -> f name +fetchField _ = rget @name + +-- | Assign a field to a value +assignField + :: forall a name f proxy . AccessFieldC a name + => proxy name -> f name -> Rec f (ConstructorFieldNames a) -> Rec f (ConstructorFieldNames a) +assignField _ = rput @name + +-- | Lens to a field. +-- @obj.f1.f2.f3@ is represented as list names of @[f1, f2, f3]@. +-- +-- @dt@ is a type of source object (type of obj in example above) +-- @fname@ is a name of target field (@"f3"@ in example above) +-- @ftype@ is a type of target field +-- +-- However, a lens contains not only name of field +-- but for each field it contains operations to get and set +-- target field. +data FieldLens dt fname ftype where + -- Direct field of @dt@ (which is target one). + -- Pay attention that it holds a label of existential type @fname@ but not @targetFName@. + -- It's made to allow a developer to refer to a field + -- with a custom name. + -- The another argument is 'StoreFieldOps'. + TargetField + :: ( InstrGetFieldC dt fname + , InstrSetFieldC dt fname + , GetFieldType dt fname ~ targetFType + , AccessFieldC dt fname + ) + => Label fname + -> StoreFieldOps dt targetFName targetFType + -> FieldLens dt targetFName targetFType + + -- Deeper field of @dt@. + -- It takes a label with name of direct field and + -- 'HasField' with deeper field as source and + -- with the same target field, + -- so it's how this datatype is alike list of fields. + -- The last argument is Lorentz operations to get and set target field. + DeeperField + :: ( AccessFieldC dt fname + , InstrSetFieldC dt fname + , HasField (GetFieldType dt fname) targetFName targetFType + ) + => Label fname + -> StoreFieldOps dt targetFName targetFType + -> FieldLens dt targetFName targetFType + +-- | Access to 'StoreFieldOps' +flSFO :: FieldLens dt fname ftype -> StoreFieldOps dt fname ftype +flSFO (TargetField _ sfo) = sfo +flSFO (DeeperField _ sfo) = sfo + +-- | Class like 'StoreHasField' type class but holding a lens to a field. +class (KnownValue ftype, KnownValue dt) => HasField dt fname ftype | dt fname -> ftype where + fieldLens :: FieldLens dt fname ftype + +-- | Build a lens to a direct field of an object. +fieldLensADT + :: forall dt targetFName targetFType fname . + ( InstrGetFieldC dt fname + , InstrSetFieldC dt fname + , GetFieldType dt fname ~ targetFType + , AccessFieldC dt fname + ) + => Label fname -> FieldLens dt targetFName targetFType +fieldLensADT lb = + let sfo = storeFieldOpsADT @dt @fname in + TargetField lb $ StoreFieldOps + { sopToField = \_ -> sopToField sfo lb + , sopSetField = \_ -> sopSetField sfo lb + } + +-- | Build a lens to deeper field of an object. +fieldLensDeeper + :: forall dt targetName targetType fname . + ( AccessFieldC dt fname + , L.HasFieldOfType dt fname (GetFieldType dt fname) + , HasField (GetFieldType dt fname) targetName targetType + ) + => Label fname + -> FieldLens dt targetName targetType +fieldLensDeeper lb = + DeeperField lb (composeStoreFieldOps lb (storeFieldOpsADT @dt) (flSFO fieldLens)) + +-- | Default instance for datatype and its direct field name. +-- It will be useful unless you want to refer to a field using a custom name. +instance {-# OVERLAPPABLE #-} + ( InstrSetFieldC dt fname + , InstrGetFieldC dt fname + , GetFieldType dt fname ~ ftype + , AccessFieldC dt fname + , KnownSymbol fname + , KnownValue ftype, KnownValue dt + ) + => HasField dt fname ftype where + fieldLens = TargetField (Label @fname) storeFieldOpsADT diff --git a/src/Indigo/Internal/Lookup.hs b/src/Indigo/Internal/Lookup.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/Lookup.hs @@ -0,0 +1,368 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{- | +This module contains the logic to lookup 'Var's in a stack and the actions to +manipulate it. + +For efficiency, actions are implemented using Lorentz macros. +To do so every necessary constraint is checked at runtime. +-} + +module Indigo.Internal.Lookup + ( -- * Variable Lookup Actions + varActionGet + , varActionSet + , varActionUpdate + , varActionOperation + + -- * Vinyl manipulation helpers + , rtake + , rdrop + ) where + +import Data.Constraint (Dict(..), HasDict) +import Data.Singletons (Sing, SingI(..)) +import Data.Type.Equality (TestEquality(..)) +import Data.Typeable ((:~:)(..), eqT) +import Data.Vinyl ((<+>)) +import Data.Vinyl.TypeLevel (type (++)) +import Prelude hiding (tail) + +import Indigo.Internal.Object (HasSideEffects, IndigoObjectF(..), Ops, operationsVar) +import Indigo.Internal.State (RefId, StackVars, StkEl(..)) +import Indigo.Lorentz +import qualified Lorentz.Instr as L +import qualified Lorentz.Macro as L +import Michelson.Typed (ToTs) +import qualified Michelson.Typed.Instr as MI +import qualified Michelson.Typed.T as MI +import Util.Peano + +---------------------------------------------------------------------------- +-- Variable Lookup Actions +---------------------------------------------------------------------------- + +-- | Puts a copy of the value for the given 'Var' on top of the stack +varActionGet :: forall a stk . KnownValue a => RefId -> StackVars stk -> stk :-> a & stk +varActionGet ref stk = case varDepth @a ref stk of + VarDepth n -> duupXVar n ref stk + +-- | Sets the value for the given 'Var' to the topmost value on the stack +varActionSet :: forall a stk . KnownValue a => RefId -> StackVars stk -> a & stk :-> stk +varActionSet ref stk = case varDepth @a ref stk of + VarDepth n -> replaceNVar (SS n) ref (NoRef :& stk) + +-- | Updates the value for the given 'Var' with the topmost value on the stack +-- using the given binary instruction. +varActionUpdate + :: forall a b stk . (KnownValue a, KnownValue b) + => RefId + -> StackVars stk + -> '[b, a] :-> '[a] + -> (b ': stk) :-> stk +varActionUpdate v stk instr = case varDepth @a v stk of + VarDepth n -> updateNVar (SS n) v (NoRef :& stk) instr + +-- | Given a stack with a list of 'Operation's on its bottom, updates it by +-- appending the 'Operation' on the top. +varActionOperation + :: HasSideEffects + => StackVars stk + -> (Operation ': stk) :-> stk +varActionOperation s = + case operationsVar of + Cell refId -> varActionUpdate @Ops refId s L.cons + +---------------------------------------------------------------------------- +-- Variable-based Macros +---------------------------------------------------------------------------- + +-- | Like 'varActionGet', but requires the depth of the 'Var' in the input stack +duupXVar + :: forall inp a (m :: Peano) s tail. + ( HasCallStack + , KnownValue a, KnownPeano m, SingI m + , s ~ ((Take m inp) ++ (a ': a ': Drop ('S m) inp)) + , tail ~ (Drop ('S m) inp) + ) + => Sing m -> RefId -> StackVars inp -> inp :-> (a ': inp) +duupXVar m v stk = + withVarMaybeDict (duupXClassConstraint n stk a s tail) $ + L.duupXImpl @('S m) @inp @a @s @tail + where + a = Ref @a v + n = SS m + s = (rtake m stk) <+> (a :& a :& rdrop n stk) + tail = rdrop n stk + +-- | Like 'varActionSet', but requires the depth of the 'Var' in the input stack +replaceNVar + :: forall s a (n :: Peano) mid tail. + ( HasCallStack + , KnownValue a + , mid ~ (Take n (a ': s) ++ Drop n s) + , tail ~ Drop n s + ) + => Sing n -> RefId -> StackVars (a ': s) -> (a ': s) :-> s +replaceNVar n v stk@(_ :& s) = + withVarMaybeDict (replaceNClassConstraint n s (Ref @a v) mid tail) $ + L.replaceNImpl @n @s @a @mid @tail + where + mid = rtake n stk <+> rdrop n s + tail = rdrop n s + +-- | Like 'varActionUpdate', but requires the depth of the 'Var' in the input stack +updateNVar + :: forall s a b mid tail (n :: Peano). + ( HasCallStack + , KnownValue b + , tail ~ Drop n s + , mid ~ ((Drop ('S 'Z) (Take n (a ': s))) ++ (a ': Drop n (a ': s))) + ) + => Sing n -> RefId -> StackVars (a ': s) + -> '[a, b] :-> '[b] + -> (a ': s) :-> s +updateNVar n v stk@(a :& s) instr = + withVarMaybeDict (updateNClassConstraint n s a (Ref @b v) mid tail) $ + L.updateNImpl @n @s @a @b @mid @tail instr + where + mid = rdrop (SS SZ) (rtake n stk) <+> a :& rdrop n stk + tail = rdrop n s + +withVarMaybeDict :: (HasDict c e, HasCallStack) => Maybe e -> (c => r) -> r +withVarMaybeDict mDict = withDict (fromMaybe (error constraintFailure) mDict) + where + -- NOTE: provided that the 'VarDepth' is correctly calculated every place + -- where this is used should never result in a 'Nothing', as this is only + -- necessary to prove to GHC properties that always hold. + -- For this reason a failure here is always unexpected + constraintFailure = "Unexpected failure in Var's constraint checking" + +---------------------------------------------------------------------------- +-- Variable's Depth +---------------------------------------------------------------------------- + +-- | Keeps the 0-indexed depth of a variable as a 'Peano' 'Sing'leton +data VarDepth where + VarDepth + :: forall idx . (KnownPeano idx, SingI idx) + => Sing (idx :: Peano) -> VarDepth + +-- | Calculates the 'VarDepth' of the given 'Var' in the stack +varDepth + :: forall a s. KnownValue a + => RefId + -> StackVars s + -> VarDepth +varDepth refId = \case + RNil -> error $ "Manually created or leaked variable. Ref #" <> show refId + stk@(_ :& _) -> varDepthNonEmpty @a refId stk + +varDepthNonEmpty + :: forall a s x xs. (KnownValue a, s ~ (x & xs)) + => RefId -> StackVars s -> VarDepth +varDepthNonEmpty ref (x :& xs) = case x of + Ref topRef | ref == topRef -> case eqT @a @x of + Just Refl -> VarDepth SZ + Nothing -> error $ "Invalid variable type. Ref #" <> show ref + _ -> case varDepth @a ref xs of + VarDepth idx -> VarDepth (SS idx) + +---------------------------------------------------------------------------- +-- Macro class constraints +---------------------------------------------------------------------------- + +duupXClassConstraint + :: Sing n -> StackVars inp -> StkEl a -> StackVars s -> StackVars s' + -> Maybe (Dict (L.DuupX n inp a s s')) +duupXClassConstraint n inp a s s' = case n of + SZ -> Nothing + SS SZ -> case inp of + (x :& _xs) -> do + Refl <- testEquality x a + return Dict + _ -> Nothing + SS (SS SZ) -> case inp of + (_ :& x :& _xs) -> do + Refl <- testEquality x a + return Dict + _ -> Nothing + SS (SS (SS m)) -> do + Dict <- duupXLorentzConstraint (SS (SS m)) inp a s s' + return Dict + +replaceNClassConstraint + :: Sing n -> StackVars s -> StkEl a -> StackVars mid -> StackVars tail + -> Maybe (Dict (L.ReplaceN n s a mid tail)) +replaceNClassConstraint n s a mid tail = case n of + SZ -> Nothing + SS SZ -> case s of + (x :& _xs) -> do + Refl <- testEquality x a + return Dict + _ -> Nothing + SS (SS m) -> do + Dict <- replaceNLorentzConstraint (SS m) s a mid tail + return Dict + +updateNClassConstraint + :: Sing n -> StackVars s -> StkEl a -> StkEl b -> StackVars mid -> StackVars tail + -> Maybe (Dict (L.UpdateN n s a b mid tail)) +updateNClassConstraint n s a b mid tail = case n of + SZ -> Nothing + SS SZ -> case s of + (x :& xs) -> do + Refl <- testEquality x b + Refl <- testEquality xs tail + return Dict + _ -> Nothing + SS (SS SZ) -> case s of + (_x :& y :& xs) -> do + Refl <- testEquality y b + Refl <- testEquality xs tail + return Dict + _ -> Nothing + SS (SS (SS m)) -> do + Dict <- updateNLorentzConstraint (SS (SS m)) s a b mid tail + return Dict + +---------------------------------------------------------------------------- +-- Lorentz constraints +---------------------------------------------------------------------------- + +duupXLorentzConstraint + :: (KnownPeano n, SingI n) + => Sing n -> StackVars inp -> StkEl a -> StackVars s -> StackVars s' + -> Maybe (Dict (L.ConstraintDuupXLorentz n inp a s s')) +duupXLorentzConstraint n s a s1 tail = do + Refl <- testEquality tail (rdrop (SS n) s) + Refl <- testEquality (toTVals tail) (rdrop (SS n) (toTVals s)) + Dict <- dipNLorentzConstraint n s s1 (a :& tail) (a :& a :& tail) + Dict <- digLorentzConstraint n s1 (a :& s) a + return Dict + +updateNLorentzConstraint + :: (KnownPeano n, SingI n) + => Sing n -> StackVars s -> StkEl a -> StkEl b -> StackVars mid -> StackVars tail + -> Maybe (Dict (L.ConstraintUpdateNLorentz n s a b mid tail)) +updateNLorentzConstraint n s a b mid tail = do + Refl <- testEquality tail (rdrop (SS n) s) + Refl <- testEquality (toTVals tail) (rdrop (SS n) (toTVals s)) + Dict <- dugLorentzConstraint n (a :& s) mid a + Dict <- dipNLorentzConstraint n mid s (a :& b :& tail) (b :& tail) + return Dict + +replaceNLorentzConstraint + :: (KnownPeano n, SingI n) + => Sing n -> StackVars s -> StkEl a -> StackVars mid -> StackVars tail + -> Maybe (Dict (L.ConstraintReplaceNLorentz n s a mid tail)) +replaceNLorentzConstraint n s a mid tail = do + Refl <- testEquality tail (rdrop (SS n) s) + Refl <- testEquality (toTVals tail) (rdrop (SS n) (toTVals s)) + Dict <- dipNLorentzConstraint (SS n) (a :& s) mid (a :& tail) tail + Dict <- dugLorentzConstraint n mid s a + return Dict + +dugLorentzConstraint + :: (KnownPeano n, SingI n) + => Sing n -> StackVars inp -> StackVars out -> StkEl a + -> Maybe (Dict (L.ConstraintDUGLorentz n inp out a)) +dugLorentzConstraint n inp out a = do + Dict <- dugConstraint n inp out a + Dict <- dugConstraint n (toTVals inp) (toTVals out) (toTVal a) + return Dict + +dipNLorentzConstraint + :: (KnownPeano n, SingI n) + => Sing n -> StackVars inp -> StackVars out -> StackVars s -> StackVars s' + -> Maybe (Dict (L.ConstraintDIPNLorentz n inp out s s')) +dipNLorentzConstraint n inp out s s' = do + Dict <- dipNConstraint n inp out s s' + Dict <- dipNConstraint n (toTVals inp) (toTVals out) (toTVals s) (toTVals s') + return Dict + +digLorentzConstraint + :: (KnownPeano n, SingI n) + => Sing n -> StackVars inp -> StackVars out -> StkEl a + -> Maybe (Dict (L.ConstraintDIGLorentz n inp out a)) +digLorentzConstraint n inp out a = do + Dict <- digConstraint n inp out a + Dict <- digConstraint n (toTVals inp) (toTVals out) (toTVal a) + return Dict + +---------------------------------------------------------------------------- +-- Morley constraints +---------------------------------------------------------------------------- + +dugConstraint + :: (KnownPeano n, SingI n, TestEquality any) + => Sing n -> Rec any inp -> Rec any out -> any a + -> Maybe (Dict (MI.ConstraintDUG' kind n inp out a)) +dugConstraint n inp out a = do + Dict <- requireLongerThan out n + Refl <- testEquality (a :& rdrop (SS SZ) inp) inp + Refl <- testEquality (rtake n (rdrop (SS SZ) inp) <+> a :& rdrop (SS n) inp) out + return Dict + +dipNConstraint + :: (KnownPeano n, SingI n, TestEquality any) + => Sing n -> Rec any inp -> Rec any out -> Rec any s -> Rec any s' + -> Maybe (Dict (MI.ConstraintDIPN' kind n inp out s s')) +dipNConstraint n inp out s s' = do + Dict <- requireLongerOrSameLength inp n + Refl <- testEquality (rtake n inp <+> s) inp + Refl <- testEquality (rtake n inp <+> s') out + return Dict + +digConstraint + :: (KnownPeano n, SingI n, TestEquality any) + => Sing n -> Rec any inp -> Rec any out -> any a + -> Maybe (Dict (MI.ConstraintDIG' kind n inp out a)) +digConstraint n inp out a = do + Dict <- requireLongerThan inp n + Refl <- testEquality inp (rtake n inp <+> a :& rdrop (SS n) inp) + Refl <- testEquality out (a :& rtake n inp <+> rdrop (SS n) inp) + return Dict + +---------------------------------------------------------------------------- +-- Conversion for ToT constraints +---------------------------------------------------------------------------- + +-- | Stack representation of 'MI.T' used for constraint checking +type TValStack (stk :: [MI.T]) = Rec TVal stk + +-- | Simple datatype used to keep a 'MI.T' and its 'Typeable' constraint +data TVal (a :: MI.T) where + TVal :: Typeable a => TVal a + +instance TestEquality TVal where + testEquality (TVal :: TVal a) (TVal :: TVal b) = eqT @a @b + +toTVal :: forall a. StkEl a -> TVal (ToT a) +toTVal = \case + NoRef -> TVal @(ToT a) + Ref _ -> TVal @(ToT a) + +toTVals :: StackVars stk -> TValStack (ToTs stk) +toTVals = \case + RNil -> RNil + (NoRef :& xs) -> TVal :& toTVals xs + (Ref _ :& xs) -> TVal :& toTVals xs + +---------------------------------------------------------------------------- +-- Vinyl manipulation helpers +---------------------------------------------------------------------------- + +rtake :: Sing n -> Rec any s -> Rec any (Take n s) +rtake sn stk = case (sn, stk) of + (SZ, _) -> RNil + (SS n, (x :& xs)) -> x :& rtake n xs + (SS _, RNil) -> error "given stack is too small" + +rdrop :: Sing n -> Rec any s -> Rec any (Drop n s) +rdrop sn stk = case (sn, stk) of + (SZ, _) -> stk + (SS n, (_ :& xs)) -> rdrop n xs + (SS _, RNil) -> error "given stack is too small" diff --git a/src/Indigo/Internal/Object.hs b/src/Indigo/Internal/Object.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/Object.hs @@ -0,0 +1,271 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Indigo.Internal.Object + ( IndigoObjectF (..) + , NamedFieldVar (..) + , TypedFieldVar (..) + , FieldTypes + , Var + , namedToTypedRec + , typedToNamedRec + , namedToTypedFieldVar + , typedToNamedFieldVar + + , IsObject + , complexObjectDict + , ComplexObjectC + , castFieldConstructors + + -- * Stack operations + , withVarAt + , makeTopVar + , pushRefMd + , pushNoRefMd + , popNoRefMd + + -- * Operations/Storage variables + , Ops + , HasSideEffects + , operationsVar + , HasStorage + , storageVar + ) where + +import Data.Vinyl (RMap) +import Data.Vinyl.TypeLevel (AllConstrained) +import Data.Reflection (Given (..)) +import Data.Constraint (Dict(..)) +import Data.Singletons (Sing) +import qualified GHC.Generics as G + +import Indigo.Backend.Prelude +import Indigo.Lorentz +import Indigo.Internal.State +import Michelson.Typed.Haskell.Instr.Product + ( GetFieldType, ConstructorFieldNames, GetFieldType + , InstrDeconstructC, FieldConstructor (..), CastFieldConstructors (..)) +import Michelson.Typed (IsPrimitiveValue) +import qualified Lorentz.Instr as L +import Util.Peano +import Util.Type (KnownList (..), KList (..)) + +---------------------------------------------------------------------------- +-- IndigoObjectF and Variable +---------------------------------------------------------------------------- + +-- | A object that can be either +-- stored in the single stack cell or split into fields. +-- Fields are identified by their names. +-- +-- @f@ is a functor to be applied to each of field names. +data IndigoObjectF f a where + -- | Value stored on the stack, it might be + -- either complex product type, like @(a, b)@, Storage, etc, + -- or sum type like 'Either', or primitive like 'Int', 'Operation', etc. + -- + -- Laziness of 'RefId' is needed here to make possible to put + -- 'error' in a variable. + -- This is used as a workaround in "Indigo.Compilation.Lambda". + Cell :: KnownValue a => ~RefId -> IndigoObjectF f a + -- | Decomposed product type, which is NOT stored + -- as one cell on the stack. + Decomposed :: ComplexObjectC a => Rec f (ConstructorFieldNames a) -> IndigoObjectF f a + +-- | Auxiliary type family to convert list of field names +-- to list of field types +type family MapGFT a rs where + MapGFT _ '[] = '[] + MapGFT a (name ': xs) = GetFieldType a name ': MapGFT a xs + +-- | Convert a list of fields from name-based list to type-based one +namedToTypedRec + :: forall a f g . + (forall name . f name -> g (GetFieldType a name)) + -> Rec f (ConstructorFieldNames a) + -> Rec g (FieldTypes a) +namedToTypedRec fun = namedToTypedRecImpl + where + namedToTypedRecImpl :: Rec f rs -> Rec g (MapGFT a rs) + namedToTypedRecImpl RNil = RNil + namedToTypedRecImpl (v :& xs) = fun v :& namedToTypedRecImpl xs + +-- | Convert a list of fields from type-based list to named-based one +typedToNamedRec :: forall a f g . KnownList (ConstructorFieldNames a) + => (forall name . f (GetFieldType a name) -> g name) + -> Rec f (FieldTypes a) + -> Rec g (ConstructorFieldNames a) +typedToNamedRec fun = typedToNamedRecImpl + where + typedToNamedRecImpl :: forall rs . KnownList rs => Rec f (MapGFT a rs) -> Rec g rs + typedToNamedRecImpl re = case (klist @rs, re) of + (KNil, RNil) -> RNil + (KCons (_ :: Proxy nm) (_ :: Proxy rs'), v :& vs) -> fun v :& typedToNamedRecImpl vs + +castFieldConstructors + :: forall a st . CastFieldConstructors (FieldTypes a) (ConstructorFieldTypes a) + => Rec (FieldConstructor st) (FieldTypes a) -> Rec (FieldConstructor st) (ConstructorFieldTypes a) +castFieldConstructors = castFieldConstructorsImpl + +-- | Auxiliary datatype to define a variable. +-- Keeps field name as type param +data NamedFieldVar a name where + NamedFieldVar + :: IsObject (GetFieldType a name) + => { unFieldVar :: Var (GetFieldType a name) + } + -> NamedFieldVar a name + +-- | Variable exposed to a user. +-- +-- 'Var' represents the tree of fields. +-- Each field is 'Var' itself: +-- either a value on the stack or 'Rec' of its direct fields. +type Var a = IndigoObjectF (NamedFieldVar a) a + +-- | Like 'NamedFieldVar', but this one doesn't keep name of a field +data TypedFieldVar a where + TypedFieldVar :: IsObject a => Var a -> TypedFieldVar a + +namedToTypedFieldVar :: forall a name . NamedFieldVar a name -> TypedFieldVar (GetFieldType a name) +namedToTypedFieldVar (NamedFieldVar f) = TypedFieldVar f + +typedToNamedFieldVar :: forall a name . TypedFieldVar (GetFieldType a name) -> NamedFieldVar a name +typedToNamedFieldVar (TypedFieldVar f) = NamedFieldVar f + +---------------------------------------------------------------------------- +-- IsObject type class +---------------------------------------------------------------------------- + +class IsObject' (TypeDecision a) a => IsObject a +instance IsObject' (TypeDecision a) a => IsObject a + +type FieldTypes a = MapGFT a (ConstructorFieldNames a) + +type ToDeconstructC a = + ( InstrDeconstructC a + , KnownList (FieldTypes a) + , AllConstrained KnownValue (FieldTypes a) + ) + +type ToConstructC a = + ( KnownValue a + , InstrConstructC a + , RMap (ConstructorFieldNames a) + , RMap (ConstructorFieldTypes a) + , RMap (FieldTypes a) + , KnownList (ConstructorFieldNames a) + , CastFieldConstructors (FieldTypes a) (ConstructorFieldTypes a) + ) + +type ComplexObjectC a = + ( ToDeconstructC a + , ToConstructC a + , AllConstrained IsObject (FieldTypes a) + ) + +-- | Type class instantiated for all possible Indigo types +class KnownValue a => IsObject' (decision :: Decision) a where + complexObjectDict' :: Maybe (Dict (ComplexObjectC a)) + +instance KnownValue a => IsObject' 'PrimitiveD a where + complexObjectDict' = Nothing + +instance KnownValue a => IsObject' 'SumTypeD a where + complexObjectDict' = Nothing + +instance ComplexObjectC a => IsObject' 'ProductTypeD a where + complexObjectDict' = Just Dict + +complexObjectDict :: forall a . IsObject a => Maybe (Dict (ComplexObjectC a)) +complexObjectDict = complexObjectDict' @(TypeDecision a) @a + +-- | Decide whether type is either primitive or ADT +type TypeDecision a = Decide (IsPrimitiveValue a) (IsSumType (G.Rep a)) + +data Decision + = PrimitiveD + | SumTypeD + | ProductTypeD + +type family Decide flagPrimitive flagSumType where + Decide 'True _ = 'PrimitiveD + Decide 'False 'True = 'SumTypeD + Decide 'False 'False = 'ProductTypeD + +type family IsSumType x where + IsSumType (G.D1 _ x) = IsSumType x + IsSumType (G.C1 _ x) = IsSumType x + IsSumType (G.M1 _ _ x) = IsSumType x + IsSumType (_ G.:*: _) = 'False + IsSumType (G.Rec0 _) = 'False + IsSumType G.V1 = 'False + IsSumType G.U1 = 'False + IsSumType (_ G.:+: _) = 'True + +---------------------------------------------------------------------------- +-- Stack operations +---------------------------------------------------------------------------- + +-- | Given a 'MetaData' and a @Peano@ singleton for a depth, it puts a new 'Var' +-- at that depth (0-indexed) and returns it with the updated 'MetaData'. +-- +-- If there is a 'Var' there already it is used and the 'MetaData' not changed. +withVarAt + :: (KnownValue a, a ~ At n inp, RequireLongerThan inp n) + => MetaData inp + -> Sing n + -> (MetaData inp, Var a) +withVarAt md@(MetaData (top :& xs) ref) = \case + SS n -> first (appendToStack top) $ withVarAt (MetaData xs ref) n + SZ -> case top of + Ref matRef -> (md, Cell matRef) + NoRef -> (MetaData (Ref ref :& xs) (ref + 1), Cell ref) + where + appendToStack :: StkEl x -> MetaData inp -> MetaData (x ': inp) + appendToStack v (MetaData st r) = MetaData (v :& st) r + +-- | Create a variable referencing the element on top of the stack. +makeTopVar :: KnownValue x => IndigoState (x & inp) (x & inp) (Var x) +makeTopVar = iget >>= \md -> + let (newMd, var) = withVarAt md SZ + in iput $ GenCode var newMd L.nop L.nop + +-- | Push a new stack element with a reference to it. +-- Return the variable referencing this element. +pushRefMd :: KnownValue x => MetaData stk -> (Var x, MetaData (x & stk)) +pushRefMd (MetaData stk cnt) = (Cell cnt, MetaData (Ref cnt :& stk) (cnt + 1)) + +-- | Push a new stack element without a reference to it. +pushNoRefMd :: KnownValue a => MetaData inp -> MetaData (a & inp) +pushNoRefMd (MetaData xs ref) = MetaData (NoRef :& xs) ref + +-- | Remove the top element of the stack. +-- It's supposed that no variable refers to this element. +popNoRefMd :: MetaData (a & inp) -> MetaData inp +popNoRefMd (MetaData (NoRef :& xs) ref) = MetaData xs ref +popNoRefMd (MetaData (Ref refId :& _) _) = + error $ "You try to pop stack element, which is referenced by some variable #" <> show refId + +---------------------------------------------------------------------------- +-- Operations/Storage variables +---------------------------------------------------------------------------- + +type Ops = [Operation] + +-- | Allows to get a variable with operations +type HasSideEffects = Given (Var Ops) + +-- | Return a variable which refers to a stack cell with operations +operationsVar :: HasSideEffects => Var Ops +operationsVar = given + +-- This storage machinery is here to avoid cyclic deps + +-- | Allows to get a variable with storage +type HasStorage st = Given (Var st) + +-- | Return a variable which refers to a stack cell with storage +storageVar :: HasStorage st => Var st +storageVar = given diff --git a/src/Indigo/Internal/SIS.hs b/src/Indigo/Internal/SIS.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/SIS.hs @@ -0,0 +1,101 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Indigo.Internal.SIS + ( SomeIndigoState (..) + , SomeGenCode (..) + , returnSIS + , bindSIS + , toSIS + , runSIS + , withSIS + , withSIS1 + , withSIS2 + ) where + + +import Indigo.Lorentz +import Indigo.Prelude + +import Indigo.Internal.State +import Indigo.Internal.Object +import qualified Lorentz.Instr as L + +-- | Gen code with hidden output stack +data SomeGenCode inp a where + SomeGenCode :: GenCode inp out a -> SomeGenCode inp a + +deriving stock instance Functor (SomeGenCode inp) + +-- | 'IndigoState' with hidden output stack, +-- necessary to generate typed Lorentz code from untyped Indigo frontend. +newtype SomeIndigoState inp a = SomeIndigoState {unSIS :: MetaData inp -> SomeGenCode inp a} + deriving stock Functor + +-- | 'return' for 'SomeIndigoState' +returnSIS :: a -> SomeIndigoState inp a +returnSIS a = SomeIndigoState $ \md -> SomeGenCode $ GenCode a md L.nop L.nop + +-- | Like bind, but the input type of the second parameter is determined by the +-- output of the first one. +bindSIS :: SomeIndigoState inp a -> (forall someOut . a -> SomeIndigoState someOut b) -> SomeIndigoState inp b +bindSIS m f = SomeIndigoState $ \md -> + case unSIS m md of + (SomeGenCode (GenCode a md1 cd1 cl1 :: GenCode inp out a)) -> + case unSIS (f @out a) md1 of + SomeGenCode (GenCode b md2 cd2 cl2) -> SomeGenCode (GenCode b md2 (cd1 ## cd2) (cl2 ## cl1)) + +-- | To run 'SomeIndigoState' you need to pass an handler of 'GenCode' with any output stack. +runSIS :: SomeIndigoState inp a -> MetaData inp -> (forall out . GenCode inp out a -> r) -> r +runSIS (SomeIndigoState act) md f = + case act md of + SomeGenCode gc -> f gc + +-- | Convert 'IndigoState' to 'SomeIndigoState' +toSIS :: IndigoState inp out a -> SomeIndigoState inp a +toSIS is = SomeIndigoState $ SomeGenCode <$> runIndigoState is + +-- | Call an action with 'IndigoState' stored in 'SomeIndigoState'. +-- +-- This function is kinda dummy because it passes +-- IndigoState to the function which produces a GenCode independently +-- on passed MetaData to it. It has to be used with only functions +-- which pass MetaData in the same way. +-- This function is needed to pass SomeIndigoState in contravariant positions +-- of statements like @if@, @case@, @while@, @forEach@, etc. +-- Alternative solution would be abstracting out IndigoState and SomeIndigoState +-- with typeclass +-- class CodeGenerator m where +-- runCodeGen :: m inp a -> MetaData inp -> (forall out . GenCode inp out a -> r) -> r +-- and passing CodeGenerator m in contravariant positions instead of IndigoState. +withSIS + :: SomeIndigoState inp a + -> (forall out . IndigoState inp out a -> SomeIndigoState inp b) + -> SomeIndigoState inp b +withSIS (SomeIndigoState act) f = SomeIndigoState $ \md -> + case act md of + SomeGenCode gc -> unSIS (f (IndigoState $ \_ -> gc)) md + +-- | The same as 'withSIS' but converting a function with one argument, also dummy. +withSIS1 + :: KnownValue x + => (Var x -> SomeIndigoState (x & inp) a) + -> (forall out . (Var x -> IndigoState (x & inp) out a) -> SomeIndigoState inp b) + -> SomeIndigoState inp b +withSIS1 act f = SomeIndigoState $ \md -> + let (var, newMd) = pushRefMd md in + case unSIS (act var) newMd of + SomeGenCode gc -> unSIS (f (\_v -> IndigoState $ \_md -> gc)) md + +-- | The same as 'withSIS1' but converting a function with 2 arguments, also dummy. +withSIS2 + :: (KnownValue x, KnownValue y) + => (Var x -> Var y -> SomeIndigoState (x & y & inp) a) + -> (forall out . (Var x -> Var y -> IndigoState (x & y & inp) out a) -> SomeIndigoState inp b) + -> SomeIndigoState inp b +withSIS2 act f = SomeIndigoState $ \md -> + let (var1, newMd1) = pushRefMd md in + let (var2, newMd2) = pushRefMd newMd1 in + case unSIS (act var2 var1) newMd2 of + SomeGenCode gc -> unSIS (f (\_v _w -> IndigoState $ \_md -> gc)) md diff --git a/src/Indigo/Internal/State.hs b/src/Indigo/Internal/State.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Internal/State.hs @@ -0,0 +1,159 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# LANGUAGE DerivingStrategies, InstanceSigs #-} + +{- | +This module contains the core of Indigo language: +the 'IndigoState' monad, a datatype that represents its state. +It also includes some convenient functions to work with the state in IndigoM, +to provide rebindable syntax. + +The 'IndigoState' monad implements the functionality of a symbolic interpreter. +During its execution Lorentz code is being generated. +-} + +module Indigo.Internal.State + ( -- * Indigo State + IndigoState (..) + , usingIndigoState + , (>>=) + , (=<<) + , (>>) + , (<$>) + , return + , iget + , iput + + , RefId + , StkEl (..) + , StackVars + , GenCode (..) + , MetaData (..) + , emptyMetadata + , cleanGenCode + , DefaultStack + ) where + +import qualified Data.Kind as Kind +import Data.Type.Equality (TestEquality (..)) +import Data.Typeable (eqT) + +import Indigo.Backend.Prelude +import Indigo.Lorentz +import qualified Lorentz.Instr as L + +{-# ANN module ("HLint: ignore Reduce duplication" :: Text) #-} + +---------------------------------------------------------------------------- +-- Indigo State +---------------------------------------------------------------------------- + +-- | IndigoState monad. It's basically +-- [Control.Monad.Indexed.State](https://hackage.haskell.org/package/category-extras-0.53.5/docs/Control-Monad-Indexed-State.html) +-- , however this package is not in the used lts and it doesn't compile. +-- +-- It takes as input a 'MetaData' (for the initial state) and returns a +-- 'GenCode' (for the resulting state and the generated Lorentz code). +-- +-- IndigoState has to be used to write backend typed Lorentz code +-- from the corresponding frontend constructions. +newtype IndigoState inp out a = + IndigoState {runIndigoState :: MetaData inp -> GenCode inp out a} + deriving stock Functor + +usingIndigoState :: MetaData inp -> IndigoState inp out a -> GenCode inp out a +usingIndigoState = flip runIndigoState + +-- | Return for rebindable syntax. +return :: a -> IndigoState inp inp a +return a = IndigoState $ \md -> GenCode a md L.nop L.nop + +-- | Bind for rebindable syntax. +-- +-- It's basically like the bind for the 'State' monad, but it also composes the +-- generated code from @m a@ and @a -> m b@. +(>>=) :: forall inp out out1 a b . IndigoState inp out a -> (a -> IndigoState out out1 b) -> IndigoState inp out1 b +(>>=) m f = IndigoState $ \md -> + let GenCode a md1 cd1 cl1 = runIndigoState m md in + let GenCode b md2 cd2 cl2 = runIndigoState (f a) md1 in + GenCode b md2 (cd1 ## cd2) (cl2 ## cl1) + +(=<<) :: (a -> IndigoState out out1 b) -> IndigoState inp out a -> IndigoState inp out1 b +(=<<) = flip (>>=) + +-- | Then for rebindable syntax. +(>>) :: IndigoState inp out a -> IndigoState out out1 b -> IndigoState inp out1 b +(>>) a b = a >>= const b + +-- | Get current 'MetaData'. +iget :: IndigoState inp inp (MetaData inp) +iget = IndigoState $ \md -> GenCode md md L.nop L.nop + +-- | Put new 'GenCode'. +iput :: GenCode inp out a -> IndigoState inp out a +iput gc = IndigoState $ \_ -> gc + +---------------------------------------------------------------------------- +-- Indigo stack and code gen primitives +---------------------------------------------------------------------------- + +-- | Reference id to a stack cell +newtype RefId = RefId Word + deriving stock (Show, Generic) + deriving newtype (Eq, Ord, Real, Num) + +-- | Stack element of the symbolic interpreter. +-- +-- It holds either a reference index that refers to this element +-- or just 'NoRef', indicating that there are no references +-- to this element. +data StkEl a where + NoRef :: KnownValue a => StkEl a + Ref :: KnownValue a => RefId -> StkEl a + +instance TestEquality StkEl where + testEquality NoRef NoRef = eqT + testEquality (Ref _) (Ref _) = eqT + testEquality (Ref _) NoRef = eqT + testEquality NoRef (Ref _) = eqT + +-- | Stack of the symbolic interpreter. +type StackVars (stk :: [Kind.Type]) = Rec StkEl stk + +-- | Initial state of 'IndigoState'. +data MetaData stk = MetaData + { mdStack :: StackVars stk + -- ^ Stack of the symbolic interpreter. + , mdRefCount :: RefId + -- ^ Number of allocated variables. + } + +emptyMetadata :: MetaData '[] +emptyMetadata = MetaData RNil 0 + +type DefaultStack stk = Default (MetaData stk) + +instance Default (MetaData '[]) where + def = emptyMetadata + +instance (KnownValue x, Default (MetaData xs)) => Default (MetaData (x ': xs)) where + def = MetaData (NoRef :& mdStack def) 0 + +-- | Resulting state of IndigoM. +data GenCode inp out a = GenCode + { gcOut :: ~a + -- ^ Interpreter output value + , gcMeta :: ~(MetaData out) + -- ^ Interpreter meta data. + , gcCode :: inp :-> out + -- ^ Generated Lorentz code. + , gcClear :: out :-> inp + -- ^ Clearing Lorentz code. + } deriving stock Functor + +-- | Produces the generated Lorentz code that cleans after itself, leaving the +-- same stack as the input one +cleanGenCode :: GenCode inp out a -> inp :-> inp +cleanGenCode GenCode {..} = gcCode ## gcClear diff --git a/src/Indigo/Lib.hs b/src/Indigo/Lib.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Lib.hs @@ -0,0 +1,128 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Standard library for Indigo. +-- +-- As opposed to Expr and Language modules, this module contains quite +-- standard things that are not present in vanilla Michelson and are +-- not typically found in imperative high level languages. + +module Indigo.Lib + ( -- * Views and Voids + view_ + , void_ + , project + , projectVoid + + -- * Others + , subGt0 + ) where + +import Indigo.Compilation +import Indigo.Frontend +import Indigo.Internal.Expr +import Indigo.Lorentz +import Indigo.Prelude +import Indigo.Rebinded + +---------------------------------------------------------------------------- +-- Views and Voids +---------------------------------------------------------------------------- + +-- | Indigo version of the @view@ macro. It takes a function from view +-- argument to view result and a 'View' structure that typically comes +-- from a top-level @case@. +view_ :: + forall arg r viewExpr exr. + ( KnownValue arg + , NiceParameter r + , viewExpr :~> View arg r + , exr :~> r + , HasSideEffects + ) + => (Expr arg -> IndigoM exr) + -> viewExpr + -> IndigoM () +view_ f v = do + r <- f (v #! #viewParam) + transferTokens r amount (v #! #viewCallbackTo) + +-- | Flipped version of 'view_' that is present due to the common +-- appearance of @flip view parameter $ instr@ construction. +-- +-- Semantically we "project" the given parameter inside the body +-- of the 'View' construction. +project :: + forall arg r viewExpr exr. + ( KnownValue arg + , NiceParameter r + , viewExpr :~> View arg r + , exr :~> r + , HasSideEffects + ) + => viewExpr + -> (Expr arg -> IndigoM exr) + -> IndigoM () +project = flip view_ + +-- | Indigo version of the @void@ macro. +void_ + :: forall a b voidExpr exb. + ( KnownValue a + , IsError (VoidResult b) + , NiceConstant b + , voidExpr :~> Void_ a b + , exb :~> b + ) + => (Expr a -> IndigoM exb) + -> voidExpr + -> IndigoM () +void_ f v = do + doc (DThrows (Proxy @(VoidResult b))) + r <- f (v #! #voidParam) + failWith $ pair voidResultTag (Exec r (v #! #voidResProxy)) + +-- | Flipped version of 'void_' that is present due to the common +-- appearance of @flip void_ parameter $ instr@ construction. +projectVoid + :: forall a b voidExpr exb. + ( KnownValue a + , IsError (VoidResult b) + , NiceConstant b + , voidExpr :~> Void_ a b + , exb :~> b + ) + => voidExpr + -> (Expr a -> IndigoM exb) + -> IndigoM () +projectVoid = flip void_ + +---------------------------------------------------------------------------- +-- Others +---------------------------------------------------------------------------- + +-- | If the first value is greater than the second one, it returns their +-- difference. If the values are equal, it returns 'Nothing'. Otherwise it +-- fails using the supplied function. +subGt0 + ::(ex1 :~> Natural, ex2 :~> Natural) + => ex1 + -> ex2 + -> IndigoM () + -> IndigoFunction (Maybe Natural) +subGt0 minuend subtrahend onNegative = do + let + diff :: Expr Integer + diff = minuend - subtrahend + + zero :: Expr Integer + zero = C $ 0 int + + when (diff < zero) onNegative + + resVar <- new$ Nothing + + if diff == zero then setVar resVar $ C Nothing else setVar resVar $ isNat diff + + return resVar diff --git a/src/Indigo/Lorentz.hs b/src/Indigo/Lorentz.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Lorentz.hs @@ -0,0 +1,41 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | This module is intended to be imported instead of "Lorentz" by Indigo +-- modules. +-- +-- The idea is to avoid repeating common @hiding@ rules and to not export any of +-- Lorentz's Instructions and Macros. + +module Indigo.Lorentz + ( module L + ) where + +import Lorentz.ADT as L hiding (caseT, case_, construct, constructT, HasField, setField) +import Lorentz.Arith as L +import Lorentz.Base as L +import Lorentz.Coercions as L +import Lorentz.Common as L +import Lorentz.Constraints as L +import Lorentz.Doc as L hiding + (contractGeneral, contractGeneralDefault, contractName, doc, docGroup, docStorage) +import Lorentz.EntryPoints as L +import Lorentz.EntryPoints.Doc as L hiding + (entryCase, entryCaseSimple, entryCase_, finalizeParamCallingDoc) +import Lorentz.Errors as L hiding (failCustom, failCustom_) +import Lorentz.Errors.Common as L () +import Lorentz.Errors.Numeric as L +import Lorentz.Ext as L +import Lorentz.Instr as L (NonZero) +import Lorentz.Macro as L (View, VoidResult, Void_, voidResultTag) +import Lorentz.Pack as L +import Lorentz.Polymorphic as L +import Lorentz.Print as L +import Lorentz.Referenced as L +import Lorentz.Run as L hiding (Contract(..)) +import Lorentz.StoreClass as L +import Lorentz.UParam as L +import Lorentz.UStore as L +import Lorentz.Value as L +import Lorentz.Zip as L () diff --git a/src/Indigo/Prelude.hs b/src/Indigo/Prelude.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Prelude.hs @@ -0,0 +1,16 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | This module serves the purpose of listing @hiding@ rules of +-- Prelude that conflicts with Indigo exported functions. + +module Indigo.Prelude + ( module Prelude + ) where + +import Prelude hiding + ( abs, and, concat, div, empty, fromInteger, fst, get, mod, not, or, snd, some + , unless, when, whenLeft, whenRight, xor, (%~), (&&), (*), (+), (-), (/), (/=) + , (<), (<=), (<>), (==), (>), (>=), (?:), (^), (^.), (^?), (||) + ) diff --git a/src/Indigo/Print.hs b/src/Indigo/Print.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Print.hs @@ -0,0 +1,59 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Module containing pretty-printing of Indigo contracts + +module Indigo.Print + ( printIndigoContract + + , printAsMichelson + , saveAsMichelson + ) where + +import Indigo.Compilation +import Indigo.Internal.Object +import Indigo.Lorentz +import Indigo.Prelude + +-- | Pretty-print an Indigo contract into Michelson code. +printIndigoContract + :: forall param st . + ( IsObject st + , NiceParameterFull param + , NiceStorage st + ) + => Bool -- ^ Force result to be single line + -> IndigoContract param st + -> LText +printIndigoContract forceSingleLine ctr = printLorentzContract forceSingleLine $ + defaultContract $ + compileIndigoContract @param @st ctr + +-- | Prints the pretty-printed Michelson code of an Indigo contract to +-- the standard output. +-- +-- This is intended to be easy to use for newcomers. +printAsMichelson + :: forall param st m . ( IsObject st + , NiceParameterFull param, NiceStorage st + , MonadIO m + ) + => IndigoContract param st + -> m () +printAsMichelson cntr = putStrLn (printIndigoContract @param @st False cntr) + +-- | Saves the pretty-printed Michelson code of an Indigo contract to +-- the given file. +-- +-- This is intended to be easy to use for newcomers. +saveAsMichelson + :: forall param st m . ( IsObject st + , NiceParameterFull param, NiceStorage st + , MonadIO m, MonadMask m + ) + => IndigoContract param st + -> FilePath + -> m () +saveAsMichelson cntr filePath = + withFile filePath WriteMode (`hPutStrLn` (printIndigoContract @param @st False cntr)) diff --git a/src/Indigo/Rebinded.hs b/src/Indigo/Rebinded.hs new file mode 100644 --- /dev/null +++ b/src/Indigo/Rebinded.hs @@ -0,0 +1,87 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Reimplementation of some syntax sugar +-- +-- You need the following module pragmas to make it work smoothly: +-- +-- @ +-- {-\# LANGUAGE NoApplicativeDo, RebindableSyntax \#-} +-- {-\# OPTIONS_GHC -Wno-unused-do-bind \#-} +-- @ + +module Indigo.Rebinded + ( -- * @if/then/else@ construct + ifThenElse + + -- * Numerical literals resolution + , fromInteger + , nat + , int + , mutez + + -- * Re-exports + , IsLabel (..) + ) where + +import qualified Prelude as P +import qualified Data.Kind as Kind + +import Indigo.Internal +import Indigo.Frontend +import Indigo.Backend.Scope +import Indigo.Backend.Conditional (IfConstraint) +import Indigo.Lorentz +import Util.Label (IsLabel(..)) + +---------------------------------------------------------------------------- +-- @if/then/else@ construct +---------------------------------------------------------------------------- + +-- | Defines semantics of @if ... then ... else ...@ construction for Indigo +-- where the predicate is a generic @exa@ for which @IsExpr exa Bool@ holds +ifThenElse + :: (IfConstraint a b, IsExpr exa Bool) + => exa + -> IndigoM a + -> IndigoM b + -> IndigoM (RetVars a) +ifThenElse cond = if_ (toExpr cond) + +---------------------------------------------------------------------------- +-- Numerical literals resolution +---------------------------------------------------------------------------- + +-- | Kind used for 'NumType' as part of the disambiguation machinery. +data NumKind = Nat | Int | Mtz + +-- | Disambiguation type used in 'fromInteger' that links a single 'NumKind' to +-- the numeric type to resolve to. +data NumType (n :: NumKind) (t :: Kind.Type) where + NNat :: NumType 'Nat Natural + NInt :: NumType 'Int Integer + NMtz :: NumType 'Mtz Mutez + +-- | Numerical literal disambiguation value for a 'Natural', see 'fromInteger'. +nat :: NumType 'Nat Natural +nat = NNat + +-- | Numerical literal disambiguation value for an 'Integer', see 'fromInteger'. +int :: NumType 'Int Integer +int = NInt + +-- | Numerical literal disambiguation value for a 'Mutez', see 'fromInteger'. +mutez :: NumType 'Mtz Mutez +mutez = NMtz + +-- | Defines numerical literals resolution for Indigo. +-- +-- It is implemented with an additional 'NumType' argument that disambiguates +-- the resulting type. +-- This allows, for example, @1 int@ to be resolved to @1 :: Integer@. +fromInteger :: Integer -> NumType n t -> t +fromInteger val = \case + NNat -> P.fromInteger val + NInt -> val + NMtz -> toMutez (P.fromInteger val) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,17 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Main + ( main + ) where + +import Prelude +import Test.Tasty (defaultMainWithIngredients) + +import Util.Test.Ingredients (ourIngredients) +import Test.Util.Golden (regenerateTests) +import Tree (tests) + +main :: IO () +main = tests >>= (defaultMainWithIngredients $ regenerateTests:ourIngredients) diff --git a/test/Test/Code/Decomposition.hs b/test/Test/Code/Decomposition.hs new file mode 100644 --- /dev/null +++ b/test/Test/Code/Decomposition.hs @@ -0,0 +1,84 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Test.Code.Decomposition + ( Meta (..) + , Color + , Storage (..) + , setDecomposedVariable + , setMaterializedVariable + , setDecomposedField + ) where + +import Indigo +import Lorentz.TypeAnns (HasTypeAnn) + +data Meta = Meta + { mWeight :: Integer + , mDescr :: MText + } deriving stock (Generic, Show) + deriving anyclass (IsoValue) + +data Color = Blue | White | Red + deriving stock (Generic, Show, Enum, Bounded) + deriving anyclass (IsoValue, HasTypeAnn) + +data Storage = Storage + { sColor :: Color + , sX :: Integer + , sY :: Integer + , sMeta :: Meta + } deriving stock (Generic, Show) + deriving anyclass (IsoValue) + +instance HasField Meta "weight" Integer where + fieldLens = fieldLensADT #mWeight + +instance HasField Meta "descr" MText where + fieldLens = fieldLensADT #mDescr + +instance HasField Storage "color" Color where + fieldLens = fieldLensADT #sColor + +instance HasField Storage "x" Integer where + fieldLens = fieldLensADT #sX + +instance HasField Storage "y" Integer where + fieldLens = fieldLensADT #sY + +instance HasField Storage "weight" Integer where + fieldLens = fieldLensDeeper #sMeta + +instance HasField Storage "descr" MText where + fieldLens = fieldLensDeeper #sMeta + +setDecomposedVariable :: ContractCode (Color, (Integer, Integer)) Storage +setDecomposedVariable = compileIndigoContract $ \param -> do + let storage = storageVar @Storage + let newStorageVal = + storage !! (#x, fst (snd param)) + !! (#y, snd (snd param)) + !! (#color, fst param) + !! (#weight, 0 int) + storage =: newStorageVal + +setMaterializedVariable :: ContractCode (Color, (Integer, Integer)) Storage +setMaterializedVariable = compileIndigoContract $ \param -> do + let storage = storageVar @Storage + let newStorageVal = + construct + ( fst param + , fst (snd param) + , snd (snd param) + , construct ( constExpr (0 int) + , constExpr [mt|"hello, Ivan!"|] + ) + ) + storage =: newStorageVal + +setDecomposedField :: ContractCode (Color, Integer) Storage +setDecomposedField = compileIndigoContract $ \param -> do + let storage = storageVar @Storage + setField storage #color (fst param) + setField storage #weight (snd param) diff --git a/test/Test/Code/Examples.hs b/test/Test/Code/Examples.hs new file mode 100644 --- /dev/null +++ b/test/Test/Code/Examples.hs @@ -0,0 +1,184 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Examples of Indigo Contracts and Tests for them + +module Test.Code.Examples + ( DummyOp (..) + , contractVarLorentz + , ifTest + , contractIfLorentz + , contractIfValueLorentz + , contractWhileLorentz + , contractForEachLorentz + , contractCaseLorentz + , contractDocLorentz + , contractOpsLorentz + , contractAssertLorentz + , contractCommentLorentz + , contractIfRightLorentz + , contractIfConsLorentz + , contractWhileLeftLorentz + ) where + +import Indigo +import qualified Lorentz.Run as L +import Michelson.Doc (DName(..)) +import Test.Util + +contractVarLorentz :: ContractCode Integer Integer +contractVarLorentz = compileIndigoContract $ \_param -> + when (5 int < 10 int) do + _a <- new$ 10 int + return () + +ifTest :: L.Contract Integer Integer +ifTest = noOptimizationContract $ compileIndigoContract $ \param -> do + a <- new$ 7 int + param + when (param < a) do + _c <- new$ storageVar @Integer + return () + _c <- new$ param < storageVar @Integer + return () + +contractIfLorentz :: ContractCode Integer Integer +contractIfLorentz = L.cCode ifTest + +contractIfValueLorentz :: ContractCode Integer Integer +contractIfValueLorentz = compileIndigoContract $ \param -> do + a <- new$ 7 int + param + when (param < a) do + _c <- new$ storageVar @Integer + return () + _c <- new$ param < storageVar @Integer + return () + +contractWhileLorentz :: ContractCode Integer Integer +contractWhileLorentz = compileIndigoContract $ \param -> do + i <- new$ 0 int + s <- new$ 0 int + while (i < storageVar @Integer) do + when (i % param == 0 nat) $ + s += i + i += 1 int + storageVar =: s + +contractForEachLorentz :: ContractCode [Integer] Integer +contractForEachLorentz = compileIndigoContract $ \param -> do + s <- new$ 0 int + forEach param $ \it -> do + s =: s + it + storageVar =: s + +contractCaseLorentz :: ContractCode DummyOp Integer +contractCaseLorentz = compileIndigoContract $ \param -> scope do + -- This example demostrates following: + -- 1. types of the stack case branched may be diverged, + -- they are automatically moved to the same stack + -- 2. branches can return not exactly the same types + --- it's useful when you have case bodies in-place, like + -- case_ param $ + -- ( #cSomething1 //-> const $ return (5 int) + -- , #cSomething2 //-> (\var -> return (10 +. var)) + -- , #cSomething3 //-> return var) + -- Pay attention, that all three branches have different return types + -- but they all correspond to the same expression 'Expr Integer'. + _flag <- case_ param $ + ( #cDSub //-> doSub storageVar + , #cDAdd //-> doAdd storageVar + ) + return () + +data DummyOp + = DSub (Integer, Integer) + | DAdd (Integer, Integer) + deriving stock (Generic, Show) + deriving anyclass (IsoValue) + +instance ParameterHasEntryPoints DummyOp where + type ParameterEntryPointsDerivation DummyOp = EpdPlain + +doSub :: Var Integer -> Var (Integer, Integer) -> IndigoM (Var Bool) +doSub storage p = do + -- Create a variable to demostrate that branches of case + -- are cleaned automatically + testVar <- new$ True + storage =: Fst p - Snd p + return testVar + +doAdd :: Var Integer -> Var (Integer, Integer) -> IndigoM Bool +doAdd storage p = do + storage =: Fst p + Snd p + return False + +contractDocLorentz :: ContractCode Integer Integer +contractDocLorentz = compileIndigoContract $ \param -> do + doc (DDescription "x") + contractName "aaa" (doc $ DDescription "a") + i <- new$ 10 int + docGroup (SomeDocItem . DName "bbb") (doc $ DDescription "b") + storageVar =: param + i + +contractOpsLorentz :: ContractCode (Maybe KeyHash) Address +contractOpsLorentz = compileIndigoContract $ \param -> do + setDelegate param + m <- new$ 0 mutez + is <- new$ 0 int + addr <- createLorentzContract ifTest param m is + storageVar =: addr + +contractAssertLorentz :: ContractCode Integer Integer +contractAssertLorentz = compileIndigoContract $ \param -> do + s <- new$ param + storageVar @Integer + z <- new$ 0 int + assert negativeResM (s > z) + storageVar =: s + +contractCommentLorentz :: ContractCode Integer Integer +contractCommentLorentz = compileIndigoContract $ \param -> do + s <- commentAroundStmt "param plus storage" $ new$ param + storageVar @Integer + _z <- new$ 0 int + justComment "just comment" + storageVar =: s + +contractIfRightLorentz :: ContractCode Integer Integer +contractIfRightLorentz = compileIndigoContract $ \param -> do + a <- new$ left $ 0 int + if_ (param >= 10 int) + (a =: right param) + (a =: left param) + + ifLeft a + (\_l -> do + storageVar =: 0 int + ) + (\_r -> do + storageVar =: 10 int + ) + +contractIfConsLorentz :: ContractCode Integer Integer +contractIfConsLorentz = compileIndigoContract $ \param -> do + a <- new$ ([] :: List Integer) + if_ (param >= 10 int) + (a =: 3 int .: 2 int .: []) + (a =: []) + + ifCons a + (\x _xs -> + storageVar =: x + ) + (storageVar =: 0 int) + +contractWhileLeftLorentz :: ContractCode Integer Integer +contractWhileLeftLorentz = compileIndigoContract $ \param -> do + iL <- new$ left $ param + s <- whileLeft (iL) \i -> do + if_ (i >= 10 int) + (iL =: right i) + (do + if_ (i % 2 int == 0 nat) + (iL =: left $ i + 2 int) + (iL =: right i) + ) + storageVar =: s diff --git a/test/Test/Code/Expr.hs b/test/Test/Code/Expr.hs new file mode 100644 --- /dev/null +++ b/test/Test/Code/Expr.hs @@ -0,0 +1,235 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Tests for Indigo Expr + +module Test.Code.Expr + ( MyUStore + , MyTemplate (..) + , SignatureData (..) + , sampleSignature + , partialParse + + , exprNullary + , exprUnary + , exprBinary + , exprAbs + , exprDivEq + , exprModNeq + , exprLe3 + , exprLt3OrGt10 + , exprGe3AndNotGe10 + , exprGe4OrNeq5AndEq6 + , exprNot + , exprIsNat + , exprSome + , exprNone + , exprFst + , exprSnd + , exprPack + , exprUnpack + , exprSet + , exprSize + , exprEmptySet + , exprCons + , exprConcat + , exprSlice + , exprBigMapLookup + , exprBigMapDelete + , exprBigMapInsert + , exprUStore + , exprCheckSignature + , exprCrypto + , exprHashKey + , exprNonZero + ) where + +import Fmt (Buildable, pretty) + +import Indigo +import Test.Util +import qualified Tezos.Crypto as C + +partialParse :: Buildable b => (a -> Either b c) -> a -> c +partialParse f = either (error . pretty) id . f + +data MyTemplate = MyTemplate + { ints :: Integer |~> () + , bool :: UStoreField Bool + } deriving stock (Eq, Show, Generic) + +type MyUStore = UStore MyTemplate + +---------------------------------------------------------------------------- +-- Sample data +---------------------------------------------------------------------------- + +data SignatureData = SignatureData + { sdPublicKey :: Text + , sdBytes :: ByteString + , sdSignature :: Text + } + +sampleSignature :: SignatureData +sampleSignature = SignatureData + { sdPublicKey = "edpkuwTWKgQNnhR5v17H2DYHbfcxYepARyrPGbf1tbMoGQAj8Ljr3V" + , sdBytes = "\0" + , sdSignature = "edsigtrs8bK7vNfiR4Kd9dWasVa1bAWaQSu2ipnmLGZuwQa8ktCEMYVKqbWsbJ7zTS8dgYT9tiSUKorWCPFHosL5zPsiDwBQ6vb" + } + +---------------------------------------------------------------------------- +-- Indigo Expr code +---------------------------------------------------------------------------- + +exprNullary + :: forall s. IsObject s => Expr s -> '[(), s] :-> '[(), s] +exprNullary expr = compileIndigo @2 $ \st _param -> st =: expr + +exprUnary + :: forall s. IsObject s => (Var s -> Expr s) -> '[s, s] :-> '[s, s] +exprUnary expr = compileIndigo @2 $ \st param -> st =: expr param + +exprBinary + :: forall s. IsObject s => (Var s -> Var s -> Expr s) -> '[s, s] :-> '[s, s] +exprBinary expr = compileIndigo @2 $ \st param -> st =: expr param st + +exprAbs :: '[Integer, Natural] :-> '[Integer, Natural] +exprAbs = compileIndigo @2 $ \st param -> st =: abs param + +exprDivEq :: '[Integer, Integer] :-> '[Integer, Integer] +exprDivEq = compileIndigo @2 $ \st param -> st =: st / param + +exprModNeq :: '[Integer, Integer] :-> '[Integer, Integer] +exprModNeq = compileIndigo @2 $ \st param -> do + if st % param /= 0 nat then st =: 0 int else st =: 1 int + +exprLe3 :: '[Integer, Bool] :-> '[Integer, Bool] +exprLe3 = compileIndigo @2 $ \st param -> + st =: param <= 3 int + +exprLt3OrGt10 :: '[Integer, Bool] :-> '[Integer, Bool] +exprLt3OrGt10 = compileIndigo @2 $ \st param -> + st =: param < 3 int || param > 10 int + +{-# ANN exprGe3AndNotGe10 ("HLint: ignore Use <" :: Text) #-} +exprGe3AndNotGe10 :: '[Integer, Bool] :-> '[Integer, Bool] +exprGe3AndNotGe10 = compileIndigo @2 $ \st param -> + st =: param >= 3 int && not (param >= 10 int) + +exprGe4OrNeq5AndEq6 :: '[Integer, Bool] :-> '[Integer, Bool] +exprGe4OrNeq5AndEq6 = compileIndigo @2 $ \st param -> + st =: param >= 4 int || param /= 5 int && param == 6 int + +exprNot :: '[Bool, Bool] :-> '[Bool, Bool] +exprNot = compileIndigo @2 $ \st param -> + st =: not param + +exprIsNat :: '[Integer, Maybe Natural] :-> '[Integer, Maybe Natural] +exprIsNat = compileIndigo @2 $ \st param -> + st =: isNat param + +exprSome :: KnownValue a => '[a, Maybe a] :-> '[a, Maybe a] +exprSome = compileIndigo @2 $ \st param -> + st =: some param + +exprNone :: KnownValue a => '[a, Maybe a] :-> '[a, Maybe a] +exprNone = compileIndigo @2 $ \st _ -> + st =: none + +exprFst :: '[(Integer, Integer), Integer] :-> '[(Integer, Integer), Integer] +exprFst = compileIndigo @2 $ \st param -> st =: fst param + +exprSnd :: '[(Integer, Integer), Integer] :-> '[(Integer, Integer), Integer] +exprSnd = compileIndigo @2 $ \st param -> st =: snd param + +exprPack :: '[Signature, ByteString] :-> '[Signature, ByteString] +exprPack = compileIndigo @2 $ \st param -> st =: pack param + +exprUnpack :: '[ByteString, Maybe Signature] :-> '[ByteString, Maybe Signature] +exprUnpack= compileIndigo @2 $ \st param -> st =: unpack param + +exprSet :: '[(Set Integer), Integer] :-> '[(Set Integer), Integer] +exprSet = compileIndigo @2 $ \st param -> do + z <- new$ 0 int + if_ (mem z param) -- Same, but also checks `mem` expression + (param =: param -: z) + (param =: param +: 1 int) + if_ (size param == 1 nat) + (st =: z) + (st =: 1 int) + +exprSize :: '[[Integer], Natural] :-> '[[Integer], Natural] +exprSize = compileIndigo @2 $ \st param -> do + st =: size param + +exprEmptySet :: '[(), Set Integer] :-> '[(), Set Integer] +exprEmptySet = compileIndigo @2 $ \st _param -> st =: emptySet + +exprCons :: '[Integer, List Integer] :-> '[Integer, List Integer] +exprCons = compileIndigo @2 $ \st param -> do + st =: param .: st + +exprConcat :: '[MText, MText] :-> '[MText, MText] +exprConcat = compileIndigo @2 $ \st param -> do + st =: param <> st + +exprSlice :: '[Natural, Maybe MText] :-> '[Natural, Maybe MText] +exprSlice = compileIndigo @2 $ \st' param -> do + ifSome st' + (\st -> do + ifSome (slice (0 nat, param) st) + (\r -> do + st =: r + st' =: some st + ) + (return ())) + (return ()) + +exprBigMapLookup :: '[BigMap Integer Integer, Maybe Integer] :-> '[BigMap Integer Integer, Maybe Integer] +exprBigMapLookup = compileIndigo @2 $ \st param -> do + st =: param #: 2 int + +exprBigMapDelete :: '[Integer, BigMap Integer Integer] :-> '[Integer, BigMap Integer Integer] +exprBigMapDelete = compileIndigo @2 $ \st param -> do + st =: st -: param + +exprBigMapInsert :: '[Integer, BigMap Integer Integer] :-> '[Integer, BigMap Integer Integer] +exprBigMapInsert = compileIndigo @2 $ \st param -> do + st =: st +: (param, param) + +exprUStore + :: '[Integer, MyUStore] + :-> '[Integer, MyUStore] +exprUStore = compileIndigo @2 $ \st param -> do + st1 <- new$ st +@ (#ints, param, ()) + st2 <- new$ st1 ++@ (#ints, notNewKeyM, 0 int, ()) + ifSome (st2 #@ (#ints, -1 int)) + (\_v -> st =: st) + (st =: st2) + +exprCheckSignature :: '[Bool, Bool] :-> '[Bool, Bool] +exprCheckSignature = compileIndigo @2 (phi sampleSignature) + where + phi SignatureData{..} st _param = do + st =: checkSignature + (constExpr $ partialParse C.parsePublicKey sdPublicKey) + (constExpr $ partialParse C.parseSignature sdSignature) + (constExpr sdBytes) + +exprCrypto + :: '[ByteString, ByteString] + :-> '[ByteString, ByteString] +exprCrypto = compileIndigo @2 $ \st param -> do + _sha256var <- new$ sha256 param + st =: blake2b param + param =: sha512 param + +exprHashKey :: '[PublicKey, KeyHash] :-> '[PublicKey, KeyHash] +exprHashKey = compileIndigo @2 $ \st param -> do + st =: hashKey param + +exprNonZero :: '[Integer, Maybe Integer] :-> '[Integer, Maybe Integer] +exprNonZero = compileIndigo @2 $ \st param -> + st =: nonZero param + diff --git a/test/Test/Code/Lambda.hs b/test/Test/Code/Lambda.hs new file mode 100644 --- /dev/null +++ b/test/Test/Code/Lambda.hs @@ -0,0 +1,116 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Test.Code.Lambda + ( SmallMatrix (..) + , dummyContract + , sumLambdaCalledOnce + , sumLambdaCalledTwice + , lambdasSideEffects + , lambdaInLambda1 + , lambdaInLambda2 + , lambdaOuterVarClosure + ) where + +import Indigo +import qualified Lorentz as L +import Lorentz.TypeAnns (HasTypeAnn) +import Test.Util + +sumLambda :: pr :~> (Integer, Integer) => pr -> IndigoM (Var Integer) +sumLambda = defNamedPureLambda1 "add" $ \pr -> pure (fst pr + snd pr) + +-- | Pure lambda called once. +-- In this case code has to be just inlined. +sumLambdaCalledOnce :: ContractCode [Integer] Integer +sumLambdaCalledOnce = compileIndigoContract $ \lst -> do + s <- new$ 0 int + forEach lst $ + setVar s <=< sumLambda . pair s + storageVar =: s + +-- | Pure lambda called twice. +-- In this case lambda has to be pushed on the stack and then called using @exec@. +sumLambdaCalledTwice :: ContractCode [Integer] Integer +sumLambdaCalledTwice = compileIndigoContract $ \lst -> do + s <- (new$ 0 int) >>= sumLambda . pair (0 int) + forEach lst $ + setVar s <=< sumLambda . pair s + storageVar =: s + +lambdaCreateContract :: + ( ex :~> (Maybe KeyHash, Integer) + , HasSideEffects, HasStorage Integer + ) => ex -> IndigoM () +lambdaCreateContract = defNamedEffLambda1 @Integer "create storage" $ \paramSt -> do + m <- new$ 0 mutez + _addr <- createLorentzContract dummyContract (fst paramSt) m (snd paramSt) + storageVar @Integer += 1 int + +dummyContract + :: L.Contract Integer Integer +dummyContract = noOptimizationContract $ compileIndigoContract $ \param -> do + a <- new$ 7 int + param + when (param < a) do + _c <- new$ storageVar @Integer + return () + _c <- new$ param < storageVar @Integer + return () + +-- | Lambda that creates new contract is called twice. +-- Test that original operations list is updated in lambda. +lambdasSideEffects :: ContractCode (Maybe KeyHash) Integer +lambdasSideEffects = compileIndigoContract $ \param -> do + lambdaCreateContract (pair param $ 0 int) + lambdaCreateContract (pair param $ 1 int) + +newtype SmallMatrix = SmallMatrix [[Integer]] + deriving stock (Generic, Show) + deriving anyclass (IsoValue) + deriving newtype (IterOpHs, HasTypeAnn) + +sumInRowTwice :: (HasStorage Integer, lst :~> [Integer]) => lst -> IndigoM () +sumInRowTwice = defNamedLambda1 @Integer "sum of the list" $ \lst -> do + let storage = storageVar @Integer + setVar storage =<< sumLambda (pair (0 int) storage) -- to call 'sumLambda' twice + forEach lst $ + setVar storage <=< sumLambda . pair storage + +-- | Define lambda inside another lambda and call it there. +lambdaInLambda1 :: ContractCode SmallMatrix Integer +lambdaInLambda1 = compileIndigoContract $ \matrix -> do + sumInRowTwice [] -- to call 'sumInRow' twice + forEach matrix sumInRowTwice + +sumInRowOnce :: (HasStorage Integer, lst :~> [Integer]) => lst -> IndigoM () +sumInRowOnce = defNamedLambda1 @Integer "sum of the list" $ \lst -> do + let storage = storageVar @Integer + forEach lst $ + setVar storage <=< sumLambda . pair storage + +-- | Define lambda in another lambda but call inner one +-- only once but outer twice, consequently, inner one +-- has to be inlined but outer one is executed via @exex@. +lambdaInLambda2 :: ContractCode SmallMatrix Integer +lambdaInLambda2 = compileIndigoContract $ \matrix -> do + sumInRowOnce [] -- to call 'sumInRowOnce' twice + let storage = storageVar @Integer + setVar storage =<< sumLambda (pair (0 int) storage) -- to pretend we call 'sumLambda' twice + forEach matrix sumInRowOnce + +-- | Use a variable from outer scope to check +-- that an error is raised. +-- TODO attach scopes to variables and prevent +-- variables from leaking more severely. +-- Current approach doesn't throw a proper error in the following cases: +-- * a contract param is in closure of lambda +-- * a pure lambda uses @storageVar@ or @opsVar@ +lambdaOuterVarClosure :: ContractCode Integer Integer +lambdaOuterVarClosure = compileIndigoContract $ \param -> do + plusTwo <- new$ param + 2 int + let lam :: pr :~> Integer => pr -> IndigoM (Var Integer) + lam = defNamedPureLambda1 "lambda" $ \innerPar -> pure (plusTwo + innerPar) + _v1 <- lam $ 3 int + _v2 <- lam $ 4 int + return () diff --git a/test/Test/Decomposition.hs b/test/Test/Decomposition.hs new file mode 100644 --- /dev/null +++ b/test/Test/Decomposition.hs @@ -0,0 +1,96 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Test.Decomposition + ( test_Decomposition + , setDecomposedVariable + , setMaterializedVariable + , setDecomposedField + , pathSetDecomposedVariable + , pathSetMaterializedVariable + , pathSetDecomposedField + ) where + +import Prelude + +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import Test.Tasty (TestTree) + +import Michelson.Interpret (MichelsonFailed(..)) +import Michelson.Test.Util (genTuple2) +import Michelson.Text (genMText, mt) +import Test.Code.Decomposition +import Test.Util + +test_Decomposition :: [TestTree] +test_Decomposition = + [ testIndigoContract "Set storage to a Decomposed variable" + (genTuple2 genColor (genTuple2 genInteger genInteger)) + genStorage + (validateContractSt setDecomposedVariableCheck) + setDecomposedVariable + pathSetDecomposedVariable + , testIndigoContract "Set storage to a Materialized variable" + (genTuple2 genColor (genTuple2 genInteger genInteger)) + genStorage + (validateContractSt setMaterializedVariableCheck) + setMaterializedVariable + pathSetMaterializedVariable + , testIndigoContract "Set storage field" + (genTuple2 genColor genInteger) + genStorage + (validateContractSt setDecomposedFieldCheck) + setDecomposedField + pathSetDecomposedField + ] + +pathSetDecomposedVariable :: FilePath +pathSetDecomposedVariable = "test/contracts/golden/decomposed/set_decomposed_variable.tz" + +pathSetMaterializedVariable :: FilePath +pathSetMaterializedVariable = "test/contracts/golden/decomposed/set_cell_variable.tz" + +pathSetDecomposedField :: FilePath +pathSetDecomposedField = "test/contracts/golden/decomposed/set_decomposed_field.tz" + +genInteger :: Gen Integer +genInteger = Gen.integral (Range.linearFrom 0 -1000 1000) + +genMeta :: Gen Meta +genMeta = Meta <$> Gen.integral (Range.linearFrom 0 -1000 1000) <*> genMText + +genColor :: Gen Color +genColor = Gen.enumBounded + +genStorage :: Gen Storage +genStorage = Storage + <$> genColor + <*> Gen.integral (Range.linearFrom 0 -1000 1000) + <*> Gen.integral (Range.linearFrom 0 -1000 1000) + <*> genMeta + +------------------------------ + +setDecomposedVariableCheck + :: (Color, (Integer, Integer)) + -> Storage + -> Either MichelsonFailed Storage +setDecomposedVariableCheck (c, (x, y)) Storage{..} = + Right $ Storage c x y (Meta 0 (mDescr sMeta)) + +setMaterializedVariableCheck + :: (Color, (Integer, Integer)) + -> Storage + -> Either MichelsonFailed Storage +setMaterializedVariableCheck (c, (x, y)) Storage{..} = + Right $ Storage c x y (Meta 0 [mt|"hello, Ivan!"|]) + +setDecomposedFieldCheck + :: (Color, Integer) + -> Storage + -> Either MichelsonFailed Storage +setDecomposedFieldCheck (c, w) Storage{..} = + Right $ Storage c sX sY (Meta w (mDescr sMeta)) diff --git a/test/Test/Examples.hs b/test/Test/Examples.hs new file mode 100644 --- /dev/null +++ b/test/Test/Examples.hs @@ -0,0 +1,273 @@ +{-# OPTIONS_GHC -Wno-name-shadowing #-} + +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Examples of Indigo Contracts and Tests for them + +module Test.Examples + ( test_Examples + , contractWhileLorentz + , contractWhileLeftLorentz + , contractForEachLorentz + , contractVarLorentz + , contractIfLorentz + , contractIfValueLorentz + , contractIfRightLorentz + , contractIfConsLorentz + , contractCaseLorentz + , contractOpsLorentz + , contractAssertLorentz + , contractCommentLorentz + , pathWhile + , pathWhileLeft + , pathForEach + , pathVar + , pathIf + , pathIfValue + , pathIfRight + , pathIfCons + , pathCase + , pathOps + , pathAssert + , pathComment + ) where + +import Prelude hiding (drop, swap) + +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import Test.Tasty (TestTree) + +import Lorentz +import Michelson.Doc (DName(..)) +import Michelson.Interpret (MichelsonFailed(..)) +import Michelson.Runtime.GState +import Michelson.Test.Util (genTuple2) +import qualified Michelson.Typed as T +import Test.Code.Examples +import Test.Util +import Tezos.Address (genAddress) +import Tezos.Crypto (genKeyHash) + +-------------------------------------------------------------------------------- +-- Tests +-------------------------------------------------------------------------------- + +{-# ANN module ("HLint: ignore Reduce duplication" :: Text) #-} + +-- | Tests on the Indigo examples. Indigo generated contracts need to match their +-- respective Michelson expected contract (by being made of the same instructions) +-- and need to pass validation for randomly generated param and storage. +-- These contracts can be regenerate via @Test.Util.Golden@ module. +test_Examples :: [TestTree] +test_Examples = + [ testIndigoContract "WHILE" + genInteger + genInteger + (validateContractSt whileCheck) + contractWhileLorentz + pathWhile + , testIndigoContract "WHILE_LEFT" + genInteger + genInteger + (validateContractSt whileLeftCheck) + contractWhileLeftLorentz + pathWhileLeft + , testIndigoContract "FOR_IN" + (Gen.list (Range.linear 0 100) genInteger) + genInteger + (validateContractSt forEachCheck) + contractForEachLorentz + pathForEach + , testIndigoContract "VAR" + genInteger + genInteger + validateContractConst + contractVarLorentz + pathVar + , testIndigoContract "IF" + genInteger + genInteger + validateContractConst + contractIfLorentz + pathIf + , testIndigoContract "IF_RIGHT" + genInteger + genInteger + (validateContractSt ifRightCheck) + contractIfRightLorentz + pathIfRight + , testIndigoContract "IF_CONS" + genInteger + genInteger + (validateContractSt ifConsCheck) + contractIfConsLorentz + pathIfCons + , testIndigoContract "IF_RET_VALUE" + genInteger + genInteger + validateContractConst + contractIfValueLorentz + pathIfValue + , testIndigoContract "CASE" + genDummyOp + genInteger + (validateContractSt caseCheck) + contractCaseLorentz + pathCase + , testIndigoDoc "DOC" + contractDocLorentz expectedDocContract + , testIndigoContract "OPS" + (Gen.maybe genKeyHash) + genAddress + (validateContractOps opsCheck) + contractOpsLorentz + pathOps + , testIndigoContract "ASSERT" + genInteger + genInteger + (validateContractSt assertCheck) + contractAssertLorentz + pathAssert + , testIndigoContract "COMMENTS" + genInteger + genInteger + (\_ _ _ -> pure ()) + contractCommentLorentz + pathComment + ] + where + genInteger :: Gen Integer + genInteger = Gen.integral (Range.linearFrom 0 -1000 1000) + + genDummyOp :: Gen DummyOp + genDummyOp = Gen.choice + [ DSub <$> genTuple2 genInteger genInteger + , DAdd <$> genTuple2 genInteger genInteger + ] + +-------------------------------------------------------------------------------- +-- Golden tests path +-------------------------------------------------------------------------------- + +pathWhile :: FilePath +pathWhile = "test/contracts/golden/while.tz" + +pathWhileLeft :: FilePath +pathWhileLeft = "test/contracts/golden/while_left.tz" + +pathForEach :: FilePath +pathForEach = "test/contracts/golden/foreach.tz" + +pathVar :: FilePath +pathVar = "test/contracts/golden/var.tz" + +pathIf :: FilePath +pathIf = "test/contracts/golden/if.tz" + +pathIfValue :: FilePath +pathIfValue = "test/contracts/golden/if_ret_value.tz" + +pathIfRight :: FilePath +pathIfRight = "test/contracts/golden/if_right_value.tz" + +pathIfCons :: FilePath +pathIfCons = "test/contracts/golden/if_cons_value.tz" + +pathCase :: FilePath +pathCase = "test/contracts/golden/case.tz" + +pathOps :: FilePath +pathOps = "test/contracts/golden/ops.tz" + +pathAssert :: FilePath +pathAssert = "test/contracts/golden/assert.tz" + +pathComment :: FilePath +pathComment = "test/contracts/golden/comments.tz" + +-------------------------------------------------------------------------------- +-- Validate Functions +-------------------------------------------------------------------------------- + +ifRightCheck :: Integer -> Integer -> Either MichelsonFailed Integer +ifRightCheck param _st + | param >= 10 = Right 10 + | otherwise = Right 0 + +ifConsCheck :: Integer -> Integer -> Either MichelsonFailed Integer +ifConsCheck param _st + | param >= 10 = Right 3 + | otherwise = Right 0 + +whileCheck :: Integer -> Integer -> Either MichelsonFailed Integer +whileCheck param st + | st <= 0 = Right 0 + | param == 0 = Left zeroDivFail + | otherwise = Right . sum $ filter ((== 0) . (`mod` param)) [0..(st - 1)] + +whileLeftCheck :: Integer -> Integer -> Either MichelsonFailed Integer +whileLeftCheck param _st + | param < 10 && (param `mod` 2) == 0 = Right 10 + | otherwise = Right param + +forEachCheck :: [Integer] -> Integer -> Either MichelsonFailed Integer +forEachCheck param _st = Right $ sum param + +caseCheck :: DummyOp -> Integer -> Either MichelsonFailed Integer +caseCheck param _st = Right $ case param of + DSub (a, b) -> a - b + DAdd (a, b) -> a + b + +opsCheck :: Maybe KeyHash -> Address -> Either MichelsonFailed [Operation] +opsCheck param _st = Right [crConOp, setDelOp] + where + setDelOp = T.OpSetDelegate $ T.SetDelegate param + crConOp = T.OpCreateContract $ + T.CreateContract genesisAddress param (toMutez 0) (T.VInt 0) + (T.cCode $ compileLorentzContract ifTest) + +assertCheck :: Integer -> Integer -> Either MichelsonFailed Integer +assertCheck param st + | sm <= 0 = Left negativeResFail + | otherwise = Right sm + where sm = st + param + +-------------------------------------------------------------------------------- +-- Expected Contracts +-------------------------------------------------------------------------------- + +-- Note that these contracts may diverge from the Indigo examples, but only for +-- differences that get eliminated by using `optimizeLorentz` on both + +expectedDocContract :: ContractCode Integer Integer +expectedDocContract = + -- add an empty operation list at the bottom of the stack + nil # swap # + -- leave `param` followed by `st` on the stack + unpair # + dip nop # + -- doc (DDescription "x") + doc (DDescription "x") # + -- contractName "aaa" (doc $ DDescription "a") + contractName "aaa" (doc $ DDescription "a") # + -- i <- new$ 10 int + push @Integer 10 # + -- docGroup (SomeDocItem . DName "bbb") (doc $ DDescription "b") + docGroup (SomeDocItem . DName "bbb") (doc $ DDescription "b") # + -- duplicate `i` + duupX @1 # + -- copy `param` to top of the stack + duupX @3 # + -- param +. i + add # + -- override `st` with it + replaceN @3 # + -- cleanup `i` and `param` + drop # drop # + -- return `st` + swap # pair + diff --git a/test/Test/Expr.hs b/test/Test/Expr.hs new file mode 100644 --- /dev/null +++ b/test/Test/Expr.hs @@ -0,0 +1,210 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Tests for Indigo Expr + +module Test.Expr + ( test_SmallIndigoExpr + ) where + +import Prelude + +import qualified Data.Bits as B +import qualified Data.Map as M +import qualified Data.Set as S +import GHC.Natural (intToNatural, naturalFromInteger, naturalToInt) +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import Test.Tasty (TestTree) + +import qualified Indigo as I +import Indigo.Lorentz +import Lorentz.UStore.Types (genUStoreFieldExt, genUStoreSubMap) +import Michelson.Interpret (MichelsonFailed(..), runUnpack) +import Michelson.Interpret.Pack +import Michelson.Runtime.GState (genesisAddress) +import Michelson.Test.Gen (genMutez) +import Michelson.Test.Util (genTuple2) +import Michelson.Text +import Michelson.Typed (genBigMap) +import qualified Michelson.Typed as T +import Test.Code.Expr +import Test.Util +import Tezos.Address (genAddress) +import Tezos.Core +import Tezos.Crypto (genKeyHash, genPublicKey, genSignature) +import qualified Tezos.Crypto as C + +genMyTemplate :: Gen MyTemplate +genMyTemplate = MyTemplate + <$> genUStoreSubMap (Gen.integral (Range.linearFrom 0 -1000 1000)) (pure ()) + <*> genUStoreFieldExt Gen.bool + +genMyUStore :: Gen MyUStore +genMyUStore = mkUStore <$> genMyTemplate + +-- | Tests on single Indigo `Expr`s or simple combinations of them. +-- Param and storage for these are generated randomly and their resulting stack +-- is validated against an Haskell function. +test_SmallIndigoExpr :: [TestTree] +test_SmallIndigoExpr = + [ testIndigo "Cast" genInteger genInteger (validateStSuccess const) (exprUnary @Integer I.cast) + , testIndigo "Size" genIntegerList genNatural (validateStSuccess (const . intToNatural . length)) exprSize + , testIndigo "Add" genInteger genInteger (validateStSuccess (+)) (exprBinary @Integer (I.+)) + , testIndigo "Sub" genInteger genInteger (validateStSuccess (-)) (exprBinary @Integer (I.-)) + , testIndigo "Mul" genInteger genInteger (validateStSuccess (*)) (exprBinary @Integer (I.*)) + , testIndigo "Neg" genInteger genInteger (validateStSuccess (const . negate)) (exprUnary @Integer I.neg) + , testIndigo "Abs" genInteger genNatural (validateStSuccess (\p _ -> naturalFromInteger $ abs p)) exprAbs + , testIndigo "DivEq" genInteger genInteger (validateStEither divEqCheck) exprDivEq + , testIndigo "ModNeq" genInteger genInteger (validateStEither modNeqCheck) exprModNeq + , testIndigo "Le3" genInteger Gen.bool (validateStSuccess (const . (<= 3))) exprLe3 + , testIndigo "Lt3OrGt10" genInteger Gen.bool (validateStSuccess (\p _ -> p < 3 || p > 10)) exprLt3OrGt10 + , testIndigo "Lt3OrGt10" genInteger Gen.bool (validateStSuccess (\p _ -> p >= 3 && p < 10)) exprGe3AndNotGe10 + , testIndigo "Xor" genNatural genNatural (validateStSuccess xor) (exprBinary @Natural (I.^)) + , testIndigo "Lsl" genNatural genShiftNatural (validateStSuccess (\p st -> B.shiftL p (naturalToInt st))) (exprBinary @Natural (I.<<<)) + , testIndigo "Lsr" genNatural genShiftNatural (validateStSuccess (\p st -> B.shiftR p (naturalToInt st))) (exprBinary @Natural (I.>>>)) + , testIndigo "Ge4OrNeq5AndEq6" genInteger Gen.bool (validateStSuccess (\p _ -> p >= 4 || p /= 5 && p == 6)) exprGe4OrNeq5AndEq6 + , testIndigo "Not" Gen.bool Gen.bool (validateStSuccess (\p _ -> not p)) exprNot + , testIndigo "IsNat" genInteger (Gen.maybe genNatural) (validateStSuccess isNatCheck) exprIsNat + , testIndigo "Fst" genIntegerPair genInteger (validateStSuccess (\(a,_) _ -> a)) exprFst + , testIndigo "Snd" genIntegerPair genInteger (validateStSuccess (\(_,b) _ -> b)) exprSnd + , testIndigo "Some" genInteger genIntegerMaybe (validateStSuccess (\p _ -> Just p)) (exprSome @Integer) + , testIndigo "None" genInteger genIntegerMaybe (validateStSuccess (\_ _ -> Nothing)) (exprNone @Integer) + , testIndigo "UStore" genInteger genMyUStore (validateStack2 ustoreCheck) exprUStore + + -- TODO: no `Arbitrary` instance for `Named` + -- , ToField + -- , SetField + -- , Name + -- , UnName + -- , Construct + -- , ConstructT + + , testIndigo "Set" genIntegerSet genInteger (validateStack2 setCheck) exprSet + , testIndigo "EmptySet" genUnit genIntegerSet (validateStSuccess (\_ _ -> S.empty)) exprEmptySet + , testIndigo "BigMapLookup" genBigMapInt genIntegerMaybe (validateStSuccess (\(BigMap p) _st -> M.lookup 2 p)) exprBigMapLookup + , testIndigo "BigMapDelete" genInteger genBigMapInt (validateStSuccess (\p (BigMap st) -> BigMap $ M.delete p st)) exprBigMapDelete + , testIndigo "BigMapInsert" genInteger genBigMapInt (validateStSuccess (\p (BigMap st) -> BigMap $ M.insert p p st)) exprBigMapInsert + , testIndigo "Pack" genSignature genByteString (validateStSuccess (\p _ -> packValue' $ T.VSignature p)) exprPack + , testIndigo "Unpack" genByteString (Gen.maybe genSignature) (validateStSuccess unpackCheck) exprUnpack + , testIndigo "Cons" genInteger genIntegerList (validateStSuccess (\(p :: Integer) s -> p : s)) exprCons + , testIndigo "Concat" genMText genMText (validateStSuccess @_ @MText (\p s -> p <> s)) exprConcat + , testIndigo "Slice" genNatural (Gen.maybe genMText) (validateStSuccess sliceCheck) exprSlice + + -- TODO: Our current testing framework uses storage type for + -- validation, meaning that we cannot test contracts that way + -- because we prohibit contract type from appearing in storage. + + -- , Contract + -- , ConvertEpAddressToContract + -- , ContractAddress + -- , Self + -- , ContractCallingUnsafe + -- , RunFutureContract + -- , ImplicitAccount + + , testIndigo "CheckSignature" Gen.bool Gen.bool (validateStSuccess checkSignatureCheck) exprCheckSignature + , testIndigo "Crypto" genByteString genByteString (validateStack2 cryptoCheck) exprCrypto + , testIndigo "HashKey" genPublicKey genKeyHash (validateStSuccess (\p _ -> C.hashKey p)) exprHashKey + , testIndigo "ChainId" genUnit genChainId (validateStSuccess (\_ _ -> dummyChainId)) (exprNullary I.chainId) + , testIndigo "Amount" genUnit genMutez (validateStSuccess (\_ _ -> unsafeMkMutez 100)) (exprNullary I.amount) + , testIndigo "Balance" genUnit genMutez (validateStSuccess (\_ _ -> unsafeMkMutez 100)) (exprNullary I.balance) + , testIndigo "Sender" genUnit genAddress (validateStSuccess (\_ _ -> genesisAddress)) (exprNullary I.sender) + + -- TODO: ContractEnv needed + -- , Now + + , testIndigo "NonZero" genInteger genIntegerMaybe (validateStSuccess nonZeroCheck) exprNonZero + ] + + where + genIntegerList = Gen.list (Range.linear 0 100) genInteger + genIntegerSet = Gen.set (Range.linear 0 100) genInteger + genIntegerPair = genTuple2 genInteger genInteger + genIntegerMaybe = Gen.maybe genInteger + genNatural = Gen.integral @_ @Natural (Range.linear 0 1000) + genInteger = Gen.integral @_ @Integer (Range.linearFrom 0 -1000 1000) + genByteString = Gen.bytes (Range.linear 0 100) + genUnit = pure () + genBigMapInt = genBigMap genInteger genInteger + + -- Cannot shift by more than 256 bits + genShiftNatural = Gen.integral @_ @Natural (Range.linear 0 256) + +---------------------------------------------------------------------------- +-- Expected behavior +---------------------------------------------------------------------------- + +divEqCheck :: Integer -> Integer -> Either MichelsonFailed Integer +divEqCheck param st + | param == 0 = Left zeroDivFail + | otherwise = Right $ st `div` param + +modNeqCheck :: Integer -> Integer -> Either MichelsonFailed Integer +modNeqCheck param st + | param == 0 = Left zeroDivFail + | st `mod` param /= 0 = Right 0 + | otherwise = Right 1 + +isNatCheck :: Integer -> Maybe Natural -> Maybe Natural +isNatCheck param _st + | param >= 0 = Just (naturalFromInteger param) + | otherwise = Nothing + +unpackCheck :: ByteString -> Maybe Signature -> Maybe Signature +unpackCheck param _st = + fmap unwrap . rightToMaybe . runUnpack $ param + where + unwrap :: Value 'T.TSignature -> Signature + unwrap (T.VSignature signature) = signature + +setCheck :: Set Integer -> Integer -> Either MichelsonFailed (Set Integer, Integer) +setCheck param _st = Right (newParam, newSt) + where + newParam + | S.member 0 param = S.delete 0 param + | otherwise = S.insert 1 param + newSt + | S.size newParam == 1 = 0 + | otherwise = 1 + +sliceCheck :: Natural -> Maybe MText -> Maybe MText +sliceCheck param (Just st) = Just . takeMText (naturalToInt param) $ st +sliceCheck _param Nothing = Nothing + +checkSignatureCheck :: Bool -> Bool -> Bool +checkSignatureCheck _param _st = check sampleSignature + where + check SignatureData{..} = C.checkSignature + (partialParse C.parsePublicKey sdPublicKey) + (partialParse C.parseSignature sdSignature) + sdBytes + +ustoreCheck + :: Integer + -> MyUStore + -> Either MichelsonFailed (Integer, MyUStore) +ustoreCheck param st + | param == 0 || M.member 0 stBigMap = Left notNewKeyFail + | M.member -1 st1BigMap = Right (param, st) + | otherwise = Right (param, st2) + where + myTemplate = either error id $ ustoreDecomposeFull st + stBigMap = unUStoreSubMap $ ints myTemplate + st1BigMap = M.insert param () stBigMap + st2BigMap = M.insert 0 () st1BigMap + -- st1 = mkUStore $ myTemplate {ints = UStoreSubMap st1BigMap} + st2 = mkUStore $ myTemplate {ints = UStoreSubMap st2BigMap} + +cryptoCheck + :: ByteString + -> ByteString + -> Either MichelsonFailed (ByteString, ByteString) +cryptoCheck param _st = Right (C.sha512 param, C.blake2b param) + +nonZeroCheck :: Integer -> Maybe Integer -> Maybe Integer +nonZeroCheck param _st + | param == 0 = Nothing + | otherwise = Just param diff --git a/test/Test/Lambda.hs b/test/Test/Lambda.hs new file mode 100644 --- /dev/null +++ b/test/Test/Lambda.hs @@ -0,0 +1,100 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Test.Lambda + ( test_Lambdas + , sumLambdaCalledOnce + , sumLambdaCalledTwice + , lambdasSideEffects + , lambdaInLambda1 + , lambdaInLambda2 + , pathSumLambdaCalledOnce + , pathSumLambdaCalledTwice + , pathLambdasSideEffects + , pathLambdaInLambda1 + , pathLambdaInLambda2 + ) where + +import Prelude + +import Hedgehog (Gen) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import Test.Hspec.Expectations (errorCall, shouldThrow) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (testCase) + +import Lorentz hiding (map) +import Michelson.Interpret (MichelsonFailed(..)) +import Michelson.Runtime.GState +import qualified Michelson.Typed as T +import Test.Code.Lambda +import Test.Util +import Tezos.Crypto (genKeyHash) + +test_Lambdas :: [TestTree] +test_Lambdas = + [ testIndigoContract "Pure lambda called once" + genIntegerList genInteger + (validateContractSt sumLambdaCheck) + sumLambdaCalledOnce pathSumLambdaCalledOnce + , testIndigoContract "Pure lambda called twice" + genIntegerList genInteger + (validateContractSt sumLambdaCheck) + sumLambdaCalledTwice pathSumLambdaCalledTwice + , testIndigoContract "Lambda with side effects" + (Gen.maybe genKeyHash) genInteger + (validateContract lambdasSideEffectsCheck) + lambdasSideEffects pathLambdasSideEffects + , testIndigoContract "Inner lambdas" + genSmallMatrix genInteger + (validateContractSt lambdaInLambdaCheck) + lambdaInLambda1 pathLambdaInLambda1 + , testIndigoContract "Inner lambdas2" + genSmallMatrix genInteger + (validateContractSt lambdaInLambdaCheck) + lambdaInLambda2 pathLambdaInLambda2 + , testCase "Outer scope error" $ + (pure $! lambdaOuterVarClosure) + `shouldThrow` + (errorCall "In a scope of function you are using a variable from an outer scope. Closures are not supported yet.") + ] + where + genInteger = Gen.integral (Range.linearFrom 0 -1000 1000) + genIntegerList = Gen.list (Range.linear 0 100) genInteger + +pathSumLambdaCalledOnce :: FilePath +pathSumLambdaCalledOnce = "test/contracts/golden/lambda/pure_lambda_called_once.tz" + +pathSumLambdaCalledTwice :: FilePath +pathSumLambdaCalledTwice = "test/contracts/golden/lambda/pure_lambda_called_twice.tz" + +pathLambdasSideEffects :: FilePath +pathLambdasSideEffects = "test/contracts/golden/lambda/lambda_side_effects.tz" + +pathLambdaInLambda1 :: FilePath +pathLambdaInLambda1 = "test/contracts/golden/lambda/impure_inner_lambdas.tz" + +pathLambdaInLambda2 :: FilePath +pathLambdaInLambda2 = "test/contracts/golden/lambda/impure_inner_lambdas2.tz" + +sumLambdaCheck :: [Integer] -> Integer -> Either MichelsonFailed Integer +sumLambdaCheck param _st = Right $ sum param + +lambdasSideEffectsCheck :: Maybe KeyHash -> Integer -> Either MichelsonFailed ([Operation], Integer) +lambdasSideEffectsCheck param st = Right ([crConOp 1, crConOp 0], st + 2) + where + crConOp c = T.OpCreateContract $ + T.CreateContract genesisAddress param (toMutez 0) (T.VInt c) + (T.cCode $ compileLorentzContract dummyContract) + +genSmallMatrix :: Gen SmallMatrix +genSmallMatrix = + fmap SmallMatrix + $ Gen.list (Range.linear 0 15) + $ Gen.list (Range.linear 0 15) + $ Gen.integral (Range.linearFrom 0 -1000 1000) + +lambdaInLambdaCheck :: SmallMatrix -> Integer -> Either MichelsonFailed Integer +lambdaInLambdaCheck (SmallMatrix param) st = Right $ sum (st : map sum param) diff --git a/test/Test/Lookup.hs b/test/Test/Lookup.hs new file mode 100644 --- /dev/null +++ b/test/Test/Lookup.hs @@ -0,0 +1,120 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +-- | Tests for Indigo Lookup + +module Test.Lookup + ( test_VarActions + ) where + +import Data.Singletons (Sing) +import Data.Typeable ((:~:)(..), eqT) +import Test.HUnit (Assertion, (@?=)) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase) +import Util.Test.Arbitrary () + +import Indigo hiding (fromInteger) +import Indigo.Backend.Prelude (fromInteger) +import qualified Lorentz.Instr as L +import qualified Lorentz.Macro as L +import Util.Peano + +-------------------------------------------------------------------------------- + +type FourInts = '[Integer, Integer, Integer, Integer] + +fullMd :: StackVars FourInts +fullMd = Ref 3 :& Ref 2 :& Ref 1 :& Ref 0 :& RNil + +nthVar :: Sing (n :: Peano) -> RefId +nthVar n = case rdrop n fullMd of + (Ref refId :: StkEl a) :& _ -> case eqT @a @Integer of + Just Refl -> refId + Nothing -> error "impossible: all Vars are for Integers" + _ -> error "this is not supposed to happen" + +-------------------------------------------------------------------------------- + +-- | Tests that VarActions match their Lorentz counterpart at different depths. +test_VarActions :: [TestTree] +test_VarActions = + [ testAtDepth1 + , testAtDepth2 + , testAtDepth3 + , testAtDepth4 + ] + +testAtDepth1 :: TestTree +testAtDepth1 = testGroup "varActions match Lorentz at depth 1" + [ testCase "get" $ testVarActionGet sn + , testCase "set" $ testVarActionSet sn + , testCase "update" $ testVarActionUpdate sn + ] + where + sn = SS SZ + +testAtDepth2 :: TestTree +testAtDepth2 = testGroup "varActions match Lorentz at depth 2" + [ testCase "get" $ testVarActionGet sn + , testCase "set" $ testVarActionSet sn + , testCase "update" $ testVarActionUpdate sn + ] + where + sn = SS $ SS SZ + +testAtDepth3 :: TestTree +testAtDepth3 = testGroup "varActions match Lorentz at depth 3" + [ testCase "get" $ testVarActionGet sn + , testCase "set" $ testVarActionSet sn + , testCase "update" $ testVarActionUpdate sn + ] + where + sn = SS . SS $ SS SZ + +testAtDepth4 :: TestTree +testAtDepth4 = testGroup "varActions match Lorentz at depth 4" + [ testCase "get" $ testVarActionGet sn + , testCase "set" $ testVarActionSet sn + , testCase "update" $ testVarActionUpdate sn + ] + where + sn = SS . SS . SS $ SS SZ + +-------------------------------------------------------------------------------- + +testVarActionGet + :: forall (n :: Peano) s1 tail. + ( L.ConstraintDuupXLorentz n FourInts Integer s1 tail + , L.DuupX ('S n) FourInts Integer s1 tail + ) + => Sing ('S n) -> Assertion +testVarActionGet (SS n) = duupXInstr @?= varActionGet (nthVar n) fullMd + where + duupXInstr :: FourInts :-> (Integer ': FourInts) + duupXInstr = L.duupXImpl @('S n) @FourInts @Integer @s1 @tail + +testVarActionSet + :: forall (n :: Peano) mid tail. + ( L.ConstraintReplaceNLorentz n FourInts Integer mid tail + , L.ReplaceN ('S n) FourInts Integer mid tail + ) + => Sing ('S n) -> Assertion +testVarActionSet (SS n) = replaceNInstr @?= varActionSet (nthVar n) fullMd + where + replaceNInstr :: (Integer ': FourInts) :-> FourInts + replaceNInstr = L.replaceNImpl @('S n) @FourInts @Integer @mid @tail + +testVarActionUpdate + :: forall (n :: Peano) mid tail. + ( L.ConstraintUpdateNLorentz n FourInts Integer Integer mid tail + , L.UpdateN ('S n) FourInts Integer Integer mid tail + ) + => Sing ('S n) -> Assertion +testVarActionUpdate (SS n) = updateNInstr @?= varActionUpdate @Integer (nthVar n) fullMd L.add + where + updateNInstr :: (Integer ': FourInts) :-> FourInts + updateNInstr = L.updateNImpl @('S n) @FourInts @Integer @Integer @mid @tail L.add diff --git a/test/Test/Util.hs b/test/Test/Util.hs new file mode 100644 --- /dev/null +++ b/test/Test/Util.hs @@ -0,0 +1,251 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | Utils for testing Indigo + +module Test.Util + ( testIndigoContract + , testIndigo + , testIndigoDoc + + , zeroDivFail + , notNewKeyFail + , notNewKeyM + , negativeResFail + , negativeResM + + , validateContract + , validateContractOps + , validateContractSt + , validateContractConst + + , validateStSuccess + , validateStEither + , validateStack2 + + , noOptimizationContract + ) where + +import Fmt (pretty) +import Hedgehog (Gen, MonadTest, PropertyT, annotate, forAll, property, (===)) +import Prelude +import Test.HUnit ((@?=)) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) +import Test.Tasty.HUnit (testCase) + +import Indigo.Lorentz +import Lorentz.Run (Contract(..)) +import Lorentz.Test (ContractPropValidator, contractProp, dummyContractEnv, failedTest) +import Michelson.Interpret (MichelsonFailed(..)) +import Michelson.Typed.Haskell.Value (IsoValuesStack) +import Util.IO (readFileUtf8) + +type IndigoInstrValidator m pm st out = + pm -> st -> Either MichelsonFailed (Rec Identity out) -> m () + +-------------------------------------------------------------------------------- +-- Tests +-------------------------------------------------------------------------------- + +-- | Takes a validating function, an Indigo-generated contract and a Lorentz +-- contract and checks that the two have equivalent code (aka made of the same +-- instructions) and that it passes validation for random param and storage. +testIndigoContract + :: forall pm st. + ( Show pm, Show st + , NiceParameterFull pm, NiceStorage st + ) + => String + -> Gen pm + -> Gen st + -> (pm -> st -> ContractPropValidator (ToT st) (PropertyT IO ())) + -> ContractCode pm st + -> FilePath + -> TestTree +testIndigoContract name genPm genSt propValidator iContract michelsonFile = + testGroup ("Indigo contract: " <> name) + [ testCase "matches Michelson reference contract" $ do + expectedContract <- readFileUtf8 michelsonFile + printLorentzContract False iContractWithoutOptimization @?= fromStrict expectedContract + , testProperty "has the correct resulting state and operations" $ property $ do + pm <- forAll genPm + st <- forAll genSt + contProp pm st + ] + where + iContractWithoutOptimization = noOptimizationContract iContract + + contProp :: pm -> st -> PropertyT IO () + contProp param storage = + withDict (niceParameterEvi @pm) $ + contractProp + (compileLorentzContract iContractWithoutOptimization) + (propValidator param storage) + dummyContractEnv param storage + +testIndigoDoc + :: forall pm st. + String + -> ContractCode pm st + -> ContractCode pm st + -> TestTree +testIndigoDoc name iContract lContract = + testCase (name <> " matches Lorentz docs content") $ + renderLorentzDoc iContract @?= renderLorentzDoc lContract + +-- | Takes a validating function and an Indigo-generated Lorentz `Instr` to check +-- the resulting stack content. +testIndigo + :: (Show pm, Show st, IsoValue pm, IsoValue st, IsoValuesStack out) + => String + -> Gen pm + -> Gen st + -> IndigoInstrValidator (PropertyT IO) pm st out + -> ('[pm, st] :-> out) + -> TestTree +testIndigo name genPm genSt validator iInstr = + testProperty (name <> " Indigo Expr has correct resulting stack") $ property $ do + pm <- forAll genPm + st <- forAll genSt + stackProp pm st + where + stackProp param storage = validator param storage . + interpretLorentzInstr dummyContractEnv iInstr $ + Identity param :& Identity storage :& RNil + +-------------------------------------------------------------------------------- +-- Common failures +-------------------------------------------------------------------------------- + +zeroDivFail :: MichelsonFailed +zeroDivFail = errorToVal [mt|devision by zero|] MichelsonFailedWith + +notNewKeyFail :: MichelsonFailed +notNewKeyFail = errorToVal notNewKeyM MichelsonFailedWith + +notNewKeyM :: MText +notNewKeyM = [mt|not new key|] + +negativeResFail :: MichelsonFailed +negativeResFail = errorToVal negativeResM MichelsonFailedWith + +negativeResM :: MText +negativeResM = [mt|unacceptable negative result|] + +-------------------------------------------------------------------------------- +-- Contract Validators +-------------------------------------------------------------------------------- + +-- | Makes a validator for `testIndigoContract` that can expect a failure or a +-- resulting [Operation] from the given function. Ignores new storage value. +validateContract + :: MonadTest m + => IsoValue st + => (pm -> st -> Either MichelsonFailed ([Operation], st)) + -> pm -> st -> ContractPropValidator (ToT st) (m ()) +validateContract fn param st (res, _) = + assertMichelsonResult (fn param st) res $ \(ops, val) (opsRes, resVal) -> do + annotate "matches resulting Storage and Operations" + (ops, toVal val) === (opsRes, resVal) + + +-- | Makes a validator for `testIndigoContract` that can expect a failure or a +-- resulting [Operation] from the given function. Ignores new storage value. +validateContractOps + :: MonadTest m + => (pm -> st -> Either MichelsonFailed [Operation]) + -> pm -> st -> ContractPropValidator (ToT st) (m ()) +validateContractOps fn param st (res, _) = + assertMichelsonResult (fn param st) res $ \ops (opsRes, _) -> do + annotate "matches resulting Operations" + ops === opsRes + +-- | Makes a validator for `testIndigoContract` that can expect a failure or a +-- new storage from the given function. Ignores resulting [Operation] +validateContractSt + :: MonadTest m + => IsoValue st + => (pm -> st -> Either MichelsonFailed st) + -> pm -> st -> ContractPropValidator (ToT st) (m ()) +validateContractSt fn param st (res, _) = + assertMichelsonResult (fn param st) res $ \val (_, resVal) -> do + annotate "matches resulting Storage" + toVal val === resVal + +-- | Validator for `testIndigoContract` that expects the storage to remain +-- the same and the resulting [Operation] to be empty. Ignores the parameter. +validateContractConst + :: MonadTest m + => IsoValue st + => pm -> st -> ContractPropValidator (ToT st) (m ()) +validateContractConst = validateContract (\_param st -> Right ([], st)) + +-------------------------------------------------------------------------------- +-- Instr Validators +-------------------------------------------------------------------------------- + +-- | Makes a validator for `testIndigo` that expects the stack not to change type +-- and the "storage" value to have changed as described by the given function. +-- Resulting "param" is ignored. +validateStSuccess + :: (MonadTest m, Eq st, Show st) + => (pm -> st -> st) + -> IndigoInstrValidator m pm st '[pm, st] +validateStSuccess fn = validateStEither (\p s -> Right $ fn p s) + +-- | Makes a validator for `testIndigo` that expects the stack not to change type +-- and Either end with a failure or with a new stack. Resulting "param" is ignored. +validateStEither + :: forall m st pm. (MonadTest m, Eq st, Show st) + => (pm -> st -> Either MichelsonFailed st) + -> IndigoInstrValidator m pm st '[pm, st] +validateStEither fn param st res = assertMichelsonResult (fn param st) res checkSt + where + checkSt :: st -> (Rec Identity '[pm, st]) -> m () + checkSt val resStack = do + let Identity _ :& Identity newState :& RNil = resStack + annotate "matches resulting state" + val === newState + +-- | Makes a validator for `testIndigo` that expects the stack to have 3 element +-- (in order and with given values) or a failure to occur. +validateStack2 + :: forall m st pm . (MonadTest m, Eq pm, Eq st, Show pm, Show st) + => (pm -> st -> Either MichelsonFailed (pm, st)) + -> IndigoInstrValidator m pm st '[pm, st] +validateStack2 fn param st res = assertMichelsonResult (fn param st) res checkSt + where + checkSt :: (pm, st) -> (Rec Identity '[pm, st]) -> m () + checkSt val resStack = do + let Identity newParam :& Identity newState :& RNil = resStack + annotate "matches resulting state" + val === (newParam, newState) + + +-------------------------------------------------------------------------------- +-- Helpers +-------------------------------------------------------------------------------- + +assertMichelsonResult + :: MonadTest m + => Either MichelsonFailed a + -> Either MichelsonFailed b + -> (a -> b -> m ()) + -> m () +assertMichelsonResult mRes1 mRes2 validatorRight = case (mRes1, mRes2) of + (Left err, Left e) -> annotate "expected failure" >> err === e + (Left err, Right _) -> failedTest $ "should have failed with: " <> pretty err + (Right _, Left e) -> failedTest $ "unexpected failure: " <> pretty e + (Right val1, Right val2) -> validatorRight val1 val2 + +noOptimizationContract :: ContractCode param st -> Contract param st +noOptimizationContract code = Contract + { cCode = code + , cDisableInitialCast = False + , cCompilationOptions = noOptimizationOptions + } + +noOptimizationOptions :: CompilationOptions +noOptimizationOptions = defaultCompilationOptions { coOptimizerConf = Nothing } diff --git a/test/Test/Util/Golden.hs b/test/Test/Util/Golden.hs new file mode 100644 --- /dev/null +++ b/test/Test/Util/Golden.hs @@ -0,0 +1,82 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +-- | This module contains tasty ingredient used for regenerating +-- Indigo golden test. + +-- To regenerate the Michelson contracts for golden tests +-- (without running the tests) execute: +-- @stack test indigo --ta --regenerate@ +module Test.Util.Golden + ( regenerateTests + ) where + +import Indigo hiding (Option) +import Test.Tasty.Ingredients +import Test.Tasty.Options + +import Test.Decomposition +import Test.Examples +import Test.Lambda +import Test.Util + +newtype RegenGoldenTests = RegenGoldenTests Bool + deriving newtype (Eq, Ord) + +instance IsOption RegenGoldenTests where + defaultValue = RegenGoldenTests False + parseValue = fmap RegenGoldenTests . safeReadBool + optionName = return "regenerate" + optionHelp = return "Regenerate indigo golden tests." + optionCLParser = flagCLParser (Just 'r') $ RegenGoldenTests True + +-- | The ingredient that provides the golden tests regeneration functionality. +regenerateTests :: Ingredient +regenerateTests = TestManager [Option (Proxy :: Proxy RegenGoldenTests)] $ + \opts _ -> + case lookupOption opts of + RegenGoldenTests False -> Nothing + RegenGoldenTests True -> Just runRegenerate + +-- | Regenerate Indigo golden tests. +-- If you add a new golden test, include its code and path in this +-- function to be able to regenerate it. +runRegenerate :: IO Bool +runRegenerate = do + -- Decomposition + saveToFile setDecomposedVariable pathSetDecomposedVariable + saveToFile setMaterializedVariable pathSetMaterializedVariable + saveToFile setDecomposedField pathSetDecomposedField + + -- Example + saveToFile contractWhileLorentz pathWhile + saveToFile contractWhileLeftLorentz pathWhileLeft + saveToFile contractForEachLorentz pathForEach + saveToFile contractVarLorentz pathVar + saveToFile contractIfLorentz pathIf + saveToFile contractIfValueLorentz pathIfValue + saveToFile contractIfRightLorentz pathIfRight + saveToFile contractIfConsLorentz pathIfCons + saveToFile contractCaseLorentz pathCase + saveToFile contractOpsLorentz pathOps + saveToFile contractAssertLorentz pathAssert + saveToFile contractCommentLorentz pathComment + + -- Lambda + saveToFile sumLambdaCalledOnce pathSumLambdaCalledOnce + saveToFile sumLambdaCalledTwice pathSumLambdaCalledTwice + saveToFile lambdasSideEffects pathLambdasSideEffects + saveToFile lambdaInLambda1 pathLambdaInLambda1 + saveToFile lambdaInLambda2 pathLambdaInLambda2 + + putTextLn "Regenerate completed." + return True + +saveToFile + :: forall cp m st. + (NiceParameterFull cp, NiceStorage st, MonadIO m, MonadMask m) + => ContractCode cp st -> FilePath + -> m () +saveToFile ctr filePath = withFile filePath WriteMode $ + flip hPutStr (printLorentzContract False $ noOptimizationContract ctr) diff --git a/test/Tree.hs b/test/Tree.hs new file mode 100644 --- /dev/null +++ b/test/Tree.hs @@ -0,0 +1,5 @@ +-- SPDX-FileCopyrightText: 2020 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display -optF --generated-module -optF Tree #-}