diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -2,8 +2,32 @@ ========== +1.14.0 +====== +* [!799](https://gitlab.com/morley-framework/morley/-/merge_requests/799) + + Fix product type instances of 1-nary constructors and empty types + (they could produce compilation error before). +* [!814](https://gitlab.com/morley-framework/morley/-/merge_requests/814) + + Renamed `Type` from `Michelson.Untyped.Type` with `Ty`. + + Added the usage of `Prelude.Type` instead of `Data.Kind.Type`, + as a result `Kind.Type` was replaced with just `Type`. +* [!733](https://gitlab.com/morley-framework/morley/-/merge_requests/733) + + Added special annotations handling for `LEFT` and `RIGHT` instructions. +* [!787](https://gitlab.com/morley-framework/morley/-/merge_requests/787) + + Added support for `CAR k` and `CDR k` macros. +* [!747](https://gitlab.com/morley-framework/morley/-/merge_requests/747) + + Fix `ligoLayout` not working for alphabetically unordered sum types. +* [!798](https://gitlab.com/morley-framework/morley/-/merge_requests/798) + + Added helper functions for recent Peano utility types. +* [!815](https://gitlab.com/morley-framework/morley/-/merge_requests/815) + + Added `IsList` and `Buildable` instances to `BigMap`. + 1.13.0 ====== +* [!796](https://gitlab.com/morley-framework/morley/-/merge_requests/796) + + Generalized `InstrWithNotes` to handle instructions that put + more than one value at the top of the stack. + + Added support for `GET_AND_UPDATE` instructions. * [!774](https://gitlab.com/morley-framework/morley/-/merge_requests/774) + Added support for `BLS12-381` crypto primitives. * [!776](https://gitlab.com/morley-framework/morley/-/merge_requests/776) diff --git a/app/REPL.hs b/app/REPL.hs --- a/app/REPL.hs +++ b/app/REPL.hs @@ -16,6 +16,7 @@ ( runRepl ) where +import Control.Exception (IOException) import qualified Data.Aeson as Aeson import qualified Data.ByteString.Lazy as BSL import Data.List (stripPrefix) @@ -80,7 +81,7 @@ ":help" -> printHelp (stripPrefix ":" -> Just cmd) -> printErr $ "Unknown command`"<> (toText cmd) <> "`. Use :help to see a list of commands" - _ -> handle (\Interrupt -> putTextLn "Cancelled") $ withInterrupt $ runCode (toText input) + _ -> flip catch (\Interrupt -> putTextLn "Cancelled") $ withInterrupt $ runCode (toText input) repl_ where strStrip = toString . strip . toText @@ -143,13 +144,13 @@ T.Dict -> case getWTP @t of Right wtpDict -> Right (T.Dict, (T.starNotes @t, wtpDict, U.noAnn) ::& hstIn) Left (NotWellTyped t) -> let - U.Type t' tann = T.toUType t + U.Ty t' tann = T.toUType t in Left $ "Value of type '" <> (renderT t' (U.fullAnnSet [tann] [] [])) <> "' is not well typed in the provided Value." renderType :: T.SingI t => T.Notes t -> U.VarAnn -> Text renderType notes vann = let - U.Type t tann = T.mkUType notes + U.Ty t tann = T.mkUType notes in renderT t (U.fullAnnSet [tann] [] [vann]) renderT :: U.T -> U.AnnotationSet -> Text diff --git a/doctests/Main.hs b/doctests/Main.hs --- a/doctests/Main.hs +++ b/doctests/Main.hs @@ -133,13 +133,13 @@ log opts $ "Reading cabal file:" <> cabalFilePath contents <- BS.readFile cabalFilePath case snd <$> runParseResult $ parseGenericPackageDescription contents of - Left (version, errs) -> do + Left (version, err :| errs) -> do die $ toString $ List.unlines $ [ "Failed to parse .cabal file: " <> cabalFilePath , "Version: " <> show version , "Errors:" ] - <> (showPError cabalFilePath <$> errs) + <> (showPError cabalFilePath <$> (err : errs)) Right cabal -> do case condLibrary cabal of Nothing -> die "Cabal file did not contain a library component." diff --git a/morley.cabal b/morley.cabal --- a/morley.cabal +++ b/morley.cabal @@ -1,11 +1,11 @@ cabal-version: 2.0 --- This file has been generated from package.yaml by hpack version 0.34.2. +-- This file has been generated from package.yaml by hpack version 0.34.3. -- -- see: https://github.com/sol/hpack name: morley -version: 1.13.0 +version: 1.14.0 synopsis: Developer tools for the Michelson Language description: A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective. category: Language @@ -13,7 +13,7 @@ bug-reports: https://gitlab.com/morley-framework/morley/-/issues author: camlCase, Serokell, Tocqueville Group maintainer: Serokell -copyright: 2018 camlCase, 2019-2020 Tocqueville Group +copyright: 2018 camlCase, 2019-2021 Tocqueville Group license: MIT license-file: LICENSE build-type: Simple @@ -164,7 +164,7 @@ 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 NumericUnderscores NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns - 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 + 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-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-unused-packages build-depends: MonadRandom , aeson @@ -225,7 +225,7 @@ hs-source-dirs: app 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 NumericUnderscores NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns - 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 + 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-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-unused-packages build-depends: aeson , base-noprelude >=4.7 && <5 @@ -251,7 +251,7 @@ hs-source-dirs: doctests 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 NumericUnderscores NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns - 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" + 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-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-unused-packages -threaded -eventlog -rtsopts "-with-rtsopts=-N -A64m -AL256m" build-tool-depends: tasty-discover:tasty-discover build-depends: diff --git a/src/Michelson/Doc.hs b/src/Michelson/Doc.hs --- a/src/Michelson/Doc.hs +++ b/src/Michelson/Doc.hs @@ -138,10 +138,10 @@ -- if two documentation items describe the same entity or property, they -- should be considered equal. type DocItemPlacement d :: DocItemPlacementKind - type DocItemPlacement d = 'DocItemInlined + type DocItemPlacement _ = 'DocItemInlined type DocItemReferenced d :: DocItemReferencedKind - type DocItemReferenced d = 'False + type DocItemReferenced _ = 'False -- | Defines a function which constructs an unique identifier of given doc item, -- if it has been decided to put the doc item into definitions section. diff --git a/src/Michelson/Interpret.hs b/src/Michelson/Interpret.hs --- a/src/Michelson/Interpret.hs +++ b/src/Michelson/Interpret.hs @@ -58,6 +58,7 @@ import Michelson.Typed hiding (Branch(..)) import qualified Michelson.Typed as T import Michelson.Typed.Origination (OriginationOperation(..), mkOriginationOperationHash) +import Michelson.Untyped.Annotation (annQ) import qualified Michelson.Untyped as U import Tezos.Address (Address(..), GlobalCounter(..), OriginationIndex(..), mkContractAddress) import Tezos.Core (ChainId, Mutez, Timestamp) @@ -104,7 +105,7 @@ -- | Represents @[FAILED]@ state of a Michelson program. Contains -- value that was on top of the stack when @FAILWITH@ was called. data MichelsonFailed where - MichelsonFailedWith :: (KnownT t) => T.Value t -> MichelsonFailed + MichelsonFailedWith :: (KnownT t, ConstantScope t) => T.Value t -> MichelsonFailed MichelsonArithError :: (Typeable n, Typeable m, Typeable instr) => ArithError (Value' instr n) (Value' instr m) -> MichelsonFailed @@ -228,7 +229,7 @@ mkInitStack param T.ParamNotesUnsafe{..} st stNotes = StkEl (T.VPair (param, st)) U.noAnn - (T.NTPair U.noAnn (U.convAnn pnRootAnn) U.noAnn "parameter" "storage" pnNotes stNotes) + (T.NTPair U.noAnn (U.convAnn pnRootAnn) U.noAnn [annQ|parameter|] [annQ|storage|] pnNotes stNotes) :& RNil fromFinalStack :: Rec StkEl (ContractOut st) -> ([T.Operation], T.Value st) @@ -355,7 +356,7 @@ runInstr :: EvalM m => InstrRunner m runInstr i@(Seq _i1 _i2) r = runInstrImpl runInstr i r runInstr i@(WithLoc _ _) r = runInstrImpl runInstr i r -runInstr i@(InstrWithNotes _ _i1) r = runInstrImpl runInstr i r +runInstr i@(InstrWithNotes _ _ _i1) r = runInstrImpl runInstr i r runInstr i@(InstrWithVarNotes _ _i1) r = runInstrImpl runInstr i r runInstr i@(InstrWithVarAnns _ _i1) r = runInstrImpl runInstr i r runInstr i@Nop r = runInstrImpl runInstr i r @@ -375,8 +376,13 @@ runInstrImpl :: EvalM m => InstrRunner m -> InstrRunner m runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r' runInstrImpl runner (WithLoc _ i) r = runner i r -runInstrImpl runner (InstrWithNotes (PackedNotes n) i) inp = - runner i inp <&> \(StkEl v vn _ :& r) -> StkEl v vn n :& r +runInstrImpl runner (InstrWithNotes (_ :: Proxy rest) notes instr) inp = do + out <- runner instr inp + let zipRec :: Rec Notes topElems -> Rec StkEl (topElems ++ rest) -> Rec StkEl (topElems ++ rest) + zipRec RNil stkElems = stkElems + zipRec (stkElemNotes :& xs) (stkElem :& ys) = + stkElem { seNotes = stkElemNotes } :& zipRec xs ys + pure $ zipRec notes out runInstrImpl runner (InstrWithVarNotes _vns i) inp = runner i inp runInstrImpl runner (InstrWithVarAnns vns i) inp = do runner i inp <&> \case @@ -491,12 +497,12 @@ :& go n' b bNotes runInstrImpl _ (AnnCAR _) (StkEl (VPair (a, _b)) _ _ :& r) = pure $ starNotesStkEl a :& r runInstrImpl _ (AnnCDR _) (StkEl (VPair (_a, b)) _ _ :& r) = pure $ starNotesStkEl b :& r -runInstrImpl _ LEFT ((seValue -> a) :& r) = +runInstrImpl _ (AnnLEFT nt nf1 nf2) ((StkEl a _ na) :& r) = withValueTypeSanity a $ - pure $ starNotesStkEl (VOr $ Left a) :& r -runInstrImpl _ RIGHT ((seValue -> b) :& r) = + pure $ StkEl (VOr $ Left a) U.noAnn (NTOr nt nf1 nf2 na starNotes) :& r +runInstrImpl _ (AnnRIGHT nt nf1 nf2) ((StkEl b _ nb) :& r) = withValueTypeSanity b $ - pure $ starNotesStkEl (VOr $ Right b) :& r + pure $ StkEl (VOr $ Right b) U.noAnn (NTOr nt nf1 nf2 starNotes nb) :& r runInstrImpl runner (IF_LEFT bLeft _) (StkEl (VOr (Left a)) vn (NTOr _ _ _ nl _) :& r) = runner bLeft (StkEl a vn nl :& r) runInstrImpl runner (IF_LEFT _ bRight) (StkEl (VOr (Right a)) vn (NTOr _ _ _ _ nr) :& r) = @@ -537,7 +543,7 @@ go (SS SZ) (VPair (left, _)) = left go (SS (SS n')) (VPair (_, right)) = go n' right runInstrImpl _ UPDATE (a :& b :& StkEl c _ _ :& r) = - pure $ starNotesStkEl (evalUpd (seValue a) (seValue b) c) :& r + pure $ starNotesStkEl (evalUpd (seValue a) (seValue b) c) :& r runInstrImpl _ (UPDATEN index0) (StkEl (val :: Value val) _ _ :& StkEl pair _ _ :& r) = do pure $ starNotesStkEl (go index0 pair) :& r where @@ -547,6 +553,11 @@ go SZ _ = val go (SS SZ) (VPair (_, right)) = VPair (val, right) go (SS (SS n')) (VPair (left, right)) = VPair (left, go n' right) +runInstrImpl _ GET_AND_UPDATE (StkEl key _ _ :& StkEl valMb _ _ :& StkEl collection _ _ :& r) = + pure $ + starNotesStkEl (VOption (evalGet key collection)) + :& starNotesStkEl (evalUpd key valMb collection) + :& r runInstrImpl runner (IF bTrue _) (StkEl (VBool True) _ _ :& r) = runner bTrue r runInstrImpl runner (IF _ bFalse) (StkEl (VBool False) _ _ :& r) = runner bFalse r runInstrImpl _ (LOOP _) (StkEl (VBool False) _ _ :& r) = pure $ r diff --git a/src/Michelson/Interpret/Pack.hs b/src/Michelson/Interpret/Pack.hs --- a/src/Michelson/Interpret/Pack.hs +++ b/src/Michelson/Interpret/Pack.hs @@ -28,6 +28,8 @@ import qualified Data.ByteString.Lazy as LBS import qualified Data.Map as Map import Data.Singletons (Sing, demote) +import Data.Vinyl (Rec(..)) +import Util.Type (type (++)) import Michelson.Interpret.Utils import Michelson.Text @@ -187,10 +189,14 @@ encodeInstr = \case WithLoc _ i -> encodeInstr i - InstrWithNotes n a -> - encodeNotedInstr a n [] - InstrWithVarNotes varNotes a -> - encodeVarNotedInstr a varNotes + InstrWithNotes proxy notes instr -> + encodeNotedInstr proxy instr notes [] + InstrWithVarNotes varNotes a -> case a of + AnnLEFT{} | _ :: Proxy ('TOr l r ': s) <- Proxy @out -> + encodeVarNotedInstr a varNotes (encodeT' @r) + AnnRIGHT{} | _ :: Proxy ('TOr l r ': s) <- Proxy @out -> + encodeVarNotedInstr a varNotes (encodeT' @l) + _ -> encodeVarNotedInstr a varNotes "" InstrWithVarAnns _ a -> encodeInstr a FrameInstr _ i -> @@ -239,10 +245,10 @@ encodeWithAnns [] [fn] [] "\x03\x16" (AnnCDR fn) -> encodeWithAnns [] [fn] [] "\x03\x17" - LEFT | _ :: Proxy ('TOr l r ': s) <- Proxy @out -> - "\x05\x33" <> encodeT' @r - RIGHT | _ :: Proxy ('TOr l r ': s) <- Proxy @out -> - "\x05\x44" <> encodeT' @l + (AnnLEFT tn fn1 fn2) | _ :: Proxy ('TOr l r ': s) <- Proxy @out -> + encodeWithAnns [tn] [fn1, fn2] [] $ "\x05\x33" <> encodeT' @r + (AnnRIGHT tn fn1 fn2) | _ :: Proxy ('TOr l r ': s) <- Proxy @out -> + encodeWithAnns [tn] [fn1, fn2] [] $ "\x05\x44" <> encodeT' @l IF_LEFT a b -> "\x07\x2e" <> encodeInstrs a <> encodeInstrs b NIL | _ :: Proxy ('TList t ': s) <- Proxy @out -> @@ -273,6 +279,8 @@ "\x03\x50" UPDATEN n -> "\x05\x50" <> encodeNumeric (peanoValSing n) + GET_AND_UPDATE -> + "\x03\x8c" IF a b -> "\x07\x2c" <> encodeInstrs a <> encodeInstrs b LOOP a -> @@ -423,58 +431,58 @@ inputIncrem = (1 + LBS.head encodedInput) `LBS.cons` LBS.tail encodedInput -- | Encode an instruction with variable annotations -encodeVarNotedInstr :: Instr inp out -> NonEmpty VarAnn -> LByteString -encodeVarNotedInstr i vns'@(toList -> vns) = case i of - InstrWithNotes n a -> encodeNotedInstr a n vns +encodeVarNotedInstr :: Instr inp out -> NonEmpty VarAnn -> LByteString -> LByteString +encodeVarNotedInstr i vns'@(toList -> vns) encodedType = case i of + InstrWithNotes proxy n a -> encodeNotedInstr proxy a n vns InstrWithVarAnns _ a -> encodeInstr $ InstrWithVarNotes vns' a - -- AnnPAIR, AnnCAR and AnnCDR are checked here because their cases on - -- `encodeInstr` increment them to \x04 when they have a field annotation, but - -- they would also get increment due to variable annotations, resulting in an - -- incorrect \x05 code. + -- AnnPAIR, AnnCAR, AnnCDR and AnnLEFT, AnnRIGHT are checked here because + -- their cases on `encodeInstr` increment them to \x04 and to \x05 respectively + -- when they have a field annotation, but they would also get increment due to + -- variable annotations, resulting in incorrect \x05 and \x06 codes respectively. AnnPAIR tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns "\x03\x42" AnnCAR fn -> encodeWithAnns [] [fn] vns "\x03\x16" AnnCDR fn -> encodeWithAnns [] [fn] vns "\x03\x17" + AnnLEFT tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x33" <> encodedType + AnnRIGHT tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x44" <> encodedType _ -> encodeWithAnns [] [] vns $ encodeInstr i -- | Encode an instruction with Annotations encodeNotedInstr - :: forall inp out. Instr inp out -> PackedNotes out -> [VarAnn] -> LByteString -encodeNotedInstr a (PackedNotes n) vns = case (a, Proxy @out, n) of - (WithLoc _ a0, _, _) -> - encodeNotedInstr a0 (PackedNotes n) vns - (SOME, _, NTOption tn _ns) -> - encodeWithAnns [tn] [] vns $ encodeInstr a - (NONE, _ :: Proxy ('TOption t ': s), NTOption tn ns) -> + :: forall inp out topElems rest. + out ~ (topElems ++ rest) + => Proxy rest -> Instr inp out -> Rec Notes topElems -> [VarAnn] -> LByteString +encodeNotedInstr proxy instr notes vns = case (instr, Proxy @out, notes) of + (WithLoc _ instr', _, _) -> + encodeNotedInstr proxy instr' notes vns + (SOME, _, NTOption tn _ns :& _) -> + encodeWithAnns [tn] [] vns $ encodeInstr instr + (NONE, _ :: Proxy ('TOption t ': s), NTOption tn ns :& _) -> encodeWithAnns [tn] [] vns $ "\x05\x3e" <> encodeNotedT' @t ns - (UNIT, _, NTUnit tn) -> - encodeWithAnns [tn] [] vns $ encodeInstr a - (LEFT, _ :: Proxy ('TOr l r ': s), NTOr tn fn1 fn2 _ns1 ns2) -> - encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x33" <> encodeNotedT' @r ns2 - (RIGHT, _ :: Proxy ('TOr l r ': s), NTOr tn fn1 fn2 ns1 _ns2) -> - encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x44" <> encodeNotedT' @l ns1 - (NIL, _ :: Proxy ('TList t ': s), NTList tn ns) -> + (UNIT, _, NTUnit tn :& _) -> + encodeWithAnns [tn] [] vns $ encodeInstr instr + (NIL, _ :: Proxy ('TList t ': s), NTList tn ns :& _) -> encodeWithAnns [tn] [] vns $ "\x05\x3d" <> encodeNotedT' @t ns - (EMPTY_SET, _ :: Proxy ('TSet t ': s), NTSet tn ns) -> + (EMPTY_SET, _ :: Proxy ('TSet t ': s), NTSet tn ns :& _) -> encodeWithAnns [tn] [] vns $ "\x05\x24" <> encodeNotedT' @t ns - (EMPTY_MAP, _ :: Proxy ('TMap k v ': s), NTMap tn1 nk ns) -> + (EMPTY_MAP, _ :: Proxy ('TMap k v ': s), NTMap tn1 nk ns :& _) -> encodeWithAnns [tn1] [] vns $ "\x07\x23" <> encodeNotedT' @k nk <> encodeNotedT' @v ns - (EMPTY_BIG_MAP, _ :: Proxy ('TBigMap k v ': s), NTBigMap tn1 nk ns) -> + (EMPTY_BIG_MAP, _ :: Proxy ('TBigMap k v ': s), NTBigMap tn1 nk ns :& _) -> encodeWithAnns [tn1] [] vns $ "\x07\x72" <> encodeNotedT' @k nk <> encodeNotedT' @v ns - (PUSH (v :: Value t), _, tn) -> + (PUSH (v :: Value t), _, tn :& _) -> "\x07\x43" <> encodeNotedT' @t tn <> encodeValue v - (LAMBDA (v :: Value ('TLambda i o)), _, NTLambda _tn ns1 ns2) -> + (LAMBDA (v :: Value ('TLambda i o)), _, NTLambda _tn ns1 ns2 :& _) -> "\x09\x31" <> encodeAsList (encodeNotedT' @i ns1 <> encodeNotedT' @o ns2 <> encodeValue v) <> encodeLength 0 -- encoding of a Variable Annotation (that we don't support) - (CAST, _ :: Proxy (t ': s), tn) -> + (CAST, _ :: Proxy (t ': s), tn :& _) -> "\x05\x57" <> encodeNotedT' @t tn - (UNPACK, _ :: Proxy ('TOption t ': s), NTOption tn ns) -> + (UNPACK, _ :: Proxy ('TOption t ': s), NTOption tn ns :& _) -> encodeWithAnns [tn] [] vns $ "\x05\x0d" <> encodeNotedT' @t ns -- NOTE: `CONTRACT` may be part of an `InstrWithNotes` with `NTOption`, but is -- taken care of in `encodeInstr` anyway (because it contains the note itself) - _ -> encodeInstr a + _ -> encodeInstr instr packNotedT' :: forall (t :: T). SingI t => Notes t -> ByteString packNotedT' = LBS.toStrict . encodeNotedT' diff --git a/src/Michelson/Interpret/Unpack.hs b/src/Michelson/Interpret/Unpack.hs --- a/src/Michelson/Interpret/Unpack.hs +++ b/src/Michelson/Interpret/Unpack.hs @@ -36,7 +36,6 @@ import qualified Data.ByteString.Lazy as LBS import Data.Constraint (Dict(..)) import Data.Default (def) -import qualified Data.Kind as Kind import qualified Data.Map as Map import qualified Data.Set as Set import Data.Singletons (Sing, SingI(..)) @@ -451,8 +450,8 @@ Left err -> -- dummy types, we have no full information to build untyped -- 'T' anyway - let tinp = Type TUnit noAnn - tout = Type TUnit noAnn + let tinp = Ty TUnit noAnn + tout = Ty TUnit noAnn in throwError $ TCFailedOnInstr (LAMBDA noAnn tinp tout uinstr) (SomeHST inp) def (Just LambdaCode) (Just err) @@ -517,6 +516,7 @@ (0x05, 0x29) -> GETN <$> decodeNoAnn <*> decodeTaggedInt "'GET n' parameter" (0x03, 0x50) -> UPDATE <$> decodeNoAnn (0x05, 0x50) -> UPDATEN <$> decodeNoAnn <*> decodeTaggedInt "'UPDATE n' parameter" + (0x03, 0x8c) -> GET_AND_UPDATE <$> decodeNoAnn (0x07, 0x2C) -> IF <$> decodeOps <*> decodeOps (0x05, 0x34) -> LOOP <$> decodeOps (0x05, 0x53) -> LOOP_LEFT <$> decodeOps @@ -640,6 +640,7 @@ n <- decodeTaggedInt "'UPDATE n' parameter" varAnn <- decodeVAnn pure $ UPDATEN varAnn n + (0x04, 0x8c) -> GET_AND_UPDATE <$> decodeVAnn (0x04, 0x26) -> EXEC <$> decodeVAnn (0x04, 0x73) -> APPLY <$> decodeVAnn (0x06, 0x57) -> do @@ -705,7 +706,7 @@ (other1, other2) -> fail $ "Unknown instruction tag: " +| bytesF [other1, other2] -decodePushVal :: Get (Type, Value) +decodePushVal :: Get (Ty, Value) decodePushVal = do typ <- decodeType T.withSomeSingT (T.fromUType typ) $ \(_ :: Sing t) -> @@ -728,7 +729,7 @@ expectTag "Pre contract parameter" 0x05 expectTag "Contract parameter" 0x00 (t, ta, root) <- decodeTWithAnns - pure $ ParameterType (Type t ta) root + pure $ ParameterType (Ty t ta) root decodeStorageBlock = CBStorage <$> do expectTag "Pre contract storage" 0x05 expectTag "Contract storage" 0x01 @@ -757,18 +758,18 @@ decodeOps :: Get [ExpandedOp] decodeOps = decodeAsList $ manyForced decodeOp -decodeComparable :: Get Type +decodeComparable :: Get Ty decodeComparable = do (ct, tAnn, fAnn) <- decodeComparableTWithAnns if fAnn == noAnn - then pure $ Type ct tAnn + then pure $ Ty ct tAnn else fail "This Comparable should not have a Field annotation" -decodeType :: Get Type +decodeType :: Get Ty decodeType = do (t, tAnn, fAnn) <- decodeTWithAnns if fAnn == noAnn - then pure $ Type t tAnn + then pure $ Ty t tAnn else fail "This Type should not have a Field annotation" decodeComparableTWithAnns :: Get (T, TypeAnn, FieldAnn) @@ -892,7 +893,7 @@ decodeTPair = do (t1, tAnn1, fAnn1) <- decodeTWithAnns (t2, tAnn2, fAnn2) <- decodeTWithAnns - pure $ TPair fAnn1 fAnn2 noAnn noAnn (Type t1 tAnn1) (Type t2 tAnn2) + pure $ TPair fAnn1 fAnn2 noAnn noAnn (Ty t1 tAnn1) (Ty t2 tAnn2) -- | Right-combed notation, e.g. `pair int int int` -- @@ -910,23 +911,23 @@ [] -> fail "The 'pair' type expects at least 2 type arguments, but 0 were given." [(t, _, _)] -> fail $ "The 'pair' type expects at least 2 type arguments, but only 1 was given: '" <> pretty t <> "'." [(t1, tAnn1, fAnn1), (t2, tAnn2, fAnn2)] -> - pure $ TPair fAnn1 fAnn2 noAnn noAnn (Type t1 tAnn1) (Type t2 tAnn2) + pure $ TPair fAnn1 fAnn2 noAnn noAnn (Ty t1 tAnn1) (Ty t2 tAnn2) (t1, t1Ann1, fAnn1) : fields -> do rightCombedT <- go fields - pure $ TPair fAnn1 noAnn noAnn noAnn (Type t1 t1Ann1) (Type rightCombedT noAnn) + pure $ TPair fAnn1 noAnn noAnn noAnn (Ty t1 t1Ann1) (Ty rightCombedT noAnn) decodeTOr :: Get T decodeTOr = do (t1, tAnn1, fAnn1) <- decodeTWithAnns (t2, tAnn2, fAnn2) <- decodeTWithAnns - pure $ TOr fAnn1 fAnn2 (Type t1 tAnn1) (Type t2 tAnn2) + pure $ TOr fAnn1 fAnn2 (Ty t1 tAnn1) (Ty t2 tAnn2) ---------------------------------------------------------------------------- -- Annotations ---------------------------------------------------------------------------- -- | Utility function to fill a constructor with an empty annotation -decodeNoAnn :: forall (t :: Kind.Type). Get (Annotation t) +decodeNoAnn :: forall (t :: Type). Get (Annotation t) decodeNoAnn = pure noAnn -- | Decodes an annotations' string and uses the provided `Parser` to parse diff --git a/src/Michelson/Let.hs b/src/Michelson/Let.hs --- a/src/Michelson/Let.hs +++ b/src/Michelson/Let.hs @@ -11,20 +11,20 @@ import qualified Data.Text as T import Michelson.Macro (ParsedOp) -import Michelson.Untyped (Type, Value') +import Michelson.Untyped (Ty, Value') import Util.Aeson -- | A programmer-defined constant data LetValue = LetValue { lvName :: T.Text - , lvSig :: Type + , lvSig :: Ty , lvVal :: (Value' ParsedOp) } deriving stock (Eq, Show) -- | A programmer-defined type-synonym data LetType = LetType { ltName :: T.Text - , ltSig :: Type + , ltSig :: Ty } deriving stock (Eq, Show) deriveJSON morleyAesonOptions ''LetValue diff --git a/src/Michelson/Macro.hs b/src/Michelson/Macro.hs --- a/src/Michelson/Macro.hs +++ b/src/Michelson/Macro.hs @@ -128,7 +128,7 @@ -- | Built-in Michelson Macros defined by the specification data Macro = CASE (NonEmpty [ParsedOp]) - | TAG Natural (NonEmpty Type) + | TAG Natural (NonEmpty Ty) | ACCESS Natural Positive | SET Natural Positive | CONSTRUCT (NonEmpty [ParsedOp]) @@ -141,6 +141,8 @@ | PAPAIR PairStruct TypeAnn VarAnn | UNPAIR UnpairStruct | CADR [CadrStruct] VarAnn FieldAnn + | CARN VarAnn Word + | CDRN VarAnn Word | SET_CADR [CadrStruct] VarAnn FieldAnn | MAP_CADR [CadrStruct] VarAnn FieldAnn [ParsedOp] | DIIP Word [ParsedOp] @@ -172,6 +174,8 @@ PAPAIR pairStruct typeAnn varAnn -> "" UNPAIR pairStruct -> "" CADR cadrStructs varAnn fieldAnn -> "" + CARN varAnn idx -> "" + CDRN varAnn idx -> "" SET_CADR cadrStructs varAnn fieldAnn -> "" MAP_CADR cadrStructs varAnn fieldAnn parsedOps -> "" DIIP integer parsedOps -> "" @@ -250,7 +254,7 @@ (expand cs <$> a) ++ [ PrimEx (DIP [PrimEx $ AMOUNT noAnn]) , PrimEx $ TRANSFER_TOKENS noAnn - , PrimEx $ NIL noAnn noAnn (Type TOperation noAnn) + , PrimEx $ NIL noAnn noAnn (Ty TOperation noAnn) , PrimEx $ SWAP , PrimEx $ CONS noAnn , PrimEx $ PAIR noAnn noAnn noAnn noAnn @@ -283,6 +287,8 @@ PAPAIR ps t v -> expandPapair p ps t v UNPAIR ps -> expandUnpapair p ps CADR c v f -> expandCadr p c v f + CARN v idx -> [PrimEx (GETN v (2 * idx + 1))] + CDRN v idx -> [PrimEx (GETN v (2 * idx))] SET_CADR c v f -> expandSetCadr p c v f MAP_CADR c v f ops -> expandMapCadr p c v f ops -- We handle DIIP and DUUP outside. @@ -349,43 +355,43 @@ D:css -> PrimEx (CDR noAnn noAnn) : expandMacro ics (CADR css v f) carNoAnn :: InstrAbstract op -carNoAnn = CAR "%%" noAnn +carNoAnn = CAR [annQ|%%|] noAnn cdrNoAnn :: InstrAbstract op -cdrNoAnn = CDR "%%" noAnn +cdrNoAnn = CDR [annQ|%%|] noAnn pairNoAnn :: VarAnn -> InstrAbstract op -pairNoAnn v = PAIR noAnn v "@" "@" +pairNoAnn v = PAIR noAnn v [annQ|@|] [annQ|@|] expandSetCadr :: InstrCallStack -> [CadrStruct] -> VarAnn -> FieldAnn -> [ExpandedOp] expandSetCadr ics cs v f = PrimEx <$> case cs of [] -> [] [A] -> [DUP noAnn, CAR noAnn f, DROP, -- ↑ These operations just check that the left element of pair has %f - cdrNoAnn, SWAP, PAIR noAnn v f "@"] + cdrNoAnn, SWAP, PAIR noAnn v f [annQ|@|]] [D] -> [DUP noAnn, CDR noAnn f, DROP, -- ↑ These operations just check that the right element of pair has %f - carNoAnn, PAIR noAnn v "@" f] + carNoAnn, PAIR noAnn v [annQ|@|] f] A:css -> [DUP noAnn, DIP (PrimEx carNoAnn : expandMacro ics (SET_CADR css noAnn f)), cdrNoAnn, SWAP, pairNoAnn v] D:css -> [DUP noAnn, DIP (PrimEx cdrNoAnn : expandMacro ics (SET_CADR css noAnn f)), carNoAnn, pairNoAnn v] expandMapCadr :: InstrCallStack -> [CadrStruct] -> VarAnn -> FieldAnn -> [ParsedOp] -> [ExpandedOp] expandMapCadr ics@InstrCallStack{icsCallStack=cls} cs v f ops = case cs of [] -> [] - [A] -> PrimEx <$> [DUP noAnn, cdrNoAnn, DIP [PrimEx $ CAR noAnn f, SeqEx (expand cls <$> ops)], SWAP, PAIR noAnn v f "@"] - [D] -> concat [PrimEx <$> [DUP noAnn, CDR noAnn f], [SeqEx (expand cls <$> ops)], PrimEx <$> [SWAP, carNoAnn, PAIR noAnn v "@" f]] + [A] -> PrimEx <$> [DUP noAnn, cdrNoAnn, DIP [PrimEx $ CAR noAnn f, SeqEx (expand cls <$> ops)], SWAP, PAIR noAnn v f [annQ|@|]] + [D] -> concat [PrimEx <$> [DUP noAnn, CDR noAnn f], [SeqEx (expand cls <$> ops)], PrimEx <$> [SWAP, carNoAnn, PAIR noAnn v [annQ|@|] f]] A:css -> PrimEx <$> [DUP noAnn, DIP (PrimEx carNoAnn : expandMacro ics (MAP_CADR css noAnn f ops)), cdrNoAnn, SWAP, pairNoAnn v] D:css -> PrimEx <$> [DUP noAnn, DIP (PrimEx cdrNoAnn : expandMacro ics (MAP_CADR css noAnn f ops)), carNoAnn, pairNoAnn v] expandCase :: NonEmpty [ExpandedOp] -> [ExpandedOp] expandCase = mkGenericTree (\_ l r -> one . PrimEx $ IF_LEFT l r) -expandTag :: Natural -> NonEmpty Type -> [ExpandedOp] +expandTag :: Natural -> NonEmpty Ty -> [ExpandedOp] expandTag idx unionTy = reverse . fst $ mkGenericTree merge (([], ) <$> unionTy) where merge i (li, lt) (ri, rt) = - let ty = Type (TOr noAnn noAnn lt rt) noAnn + let ty = Ty (TOr noAnn noAnn lt rt) noAnn in if idx < i then (PrimEx (LEFT noAnn noAnn noAnn noAnn rt) : li, ty) else (PrimEx (RIGHT noAnn noAnn noAnn noAnn lt) : ri, ty) diff --git a/src/Michelson/Optimizer.hs b/src/Michelson/Optimizer.hs --- a/src/Michelson/Optimizer.hs +++ b/src/Michelson/Optimizer.hs @@ -214,12 +214,12 @@ Seq (PUSH (VBool True)) (Seq (IF f _) c) -> Just (Seq f c) Seq (PUSH (VBool False)) (Seq (IF _ f) c) -> Just (Seq f c) - Seq LEFT (IF_LEFT f _) -> Just f - Seq RIGHT (IF_LEFT _ f) -> Just f - Seq CONS (IF_CONS f _) -> Just f - Seq NIL (IF_CONS _ f) -> Just f - Seq NONE (IF_NONE f _) -> Just f - Seq SOME (IF_NONE _ f) -> Just f + Seq LEFT (IF_LEFT f _) -> Just f + Seq RIGHT (IF_LEFT _ f) -> Just f + Seq CONS (IF_CONS f _) -> Just f + Seq NIL (IF_CONS _ f) -> Just f + Seq NONE (IF_NONE f _) -> Just f + Seq SOME (IF_NONE _ f) -> Just f Seq (PUSH (VBool True)) (IF f _) -> Just f Seq (PUSH (VBool False)) (IF _ f) -> Just f @@ -232,7 +232,7 @@ Seq (PUSH (VNat 0)) (Seq COMPARE (Seq EQ c)) -> Just (Seq INT (Seq EQ c)) Seq (PUSH (VInt 0)) (Seq COMPARE EQ) -> Just EQ Seq (PUSH (VNat 0)) (Seq COMPARE EQ) -> Just (Seq INT EQ) - _ -> Nothing + _ -> Nothing simpleDrops :: Rule simpleDrops = \case diff --git a/src/Michelson/Parser.hs b/src/Michelson/Parser.hs --- a/src/Michelson/Parser.hs +++ b/src/Michelson/Parser.hs @@ -104,13 +104,13 @@ rootAnn <- case (prefixRootAnn, inTypeRootAnn) of -- TODO: [#310] Handle cases where there are 2 empty root annotations. -- For example: root % (unit %) which should throw the error. - (Just "", "") -> pure noAnn - (Just a, "") -> pure a + (Just a, b) | a == noAnn && b == noAnn -> pure noAnn + (Just a, b) | b == noAnn -> pure a (Nothing, b) -> pure b (Just _, _) -> customFailure MultiRootAnnotationException pure $ ParameterType t rootAnn -cbStorage :: Parser Type +cbStorage :: Parser Ty cbStorage = symbol "storage" *> type_ cbCode :: Parser [ParsedOp] @@ -260,6 +260,7 @@ <|> (macWithPos (mapCadrMac parsedOp) <|> primWithPos (mapOp parsedOp)) <|> (try (primWithPos pairOp) <|> try (primWithPos pairNOp) <|> macWithPos pairMac) <|> (try (macWithPos duupMac) <|> primWithPos dupOp) + <|> (try (macWithPos carnMac) <|> try (macWithPos cdrnMac) <|> try (macWithPos cadrMac) <|> primWithPos carOp <|> primWithPos cdrOp) ------------------------------------------------------------------------------- -- Safe construction of Haskell values @@ -277,10 +278,10 @@ } --- | Creates 'U.Type' by its Morley representation. +-- | Creates 'U.Ty' by its Morley representation. -- -- >>> [utypeQ| (int :a | nat :b) |] --- Type (TOr % % (Type TInt :a) (Type TNat :b)) : +-- Ty (TOr % % (Ty TInt :a) (Ty TNat :b)) : utypeQ :: TH.QuasiQuoter utypeQ = parserToQuasiQuoter type_ diff --git a/src/Michelson/Parser/Annotations.hs b/src/Michelson/Parser/Annotations.hs --- a/src/Michelson/Parser/Annotations.hs +++ b/src/Michelson/Parser/Annotations.hs @@ -37,14 +37,14 @@ note = lexeme $ string (annPrefix @tag) >> (specialNote <|> note' <|> emptyNote) where -- TODO [#48] these are special annotations and should not always be accepted - specialVNote = ann <$> asum (map string specialVarAnns) - specialFNote = ann <$> string specialFieldAnn + specialVNote = mkAnnotationUnsafe <$> asum (map string specialVarAnns) + specialFNote = mkAnnotationUnsafe <$> string specialFieldAnn specialNote = specialVNote <|> specialFNote emptyNote = pure noAnn note' = do a <- satisfy isValidAnnStart b <- takeWhileP Nothing isValidAnnBodyChar - return . ann $ T.cons a b + return . mkAnnotationUnsafe $ T.cons a b noteV :: Parser VarAnn noteV = note diff --git a/src/Michelson/Parser/Instr.hs b/src/Michelson/Parser/Instr.hs --- a/src/Michelson/Parser/Instr.hs +++ b/src/Michelson/Parser/Instr.hs @@ -13,6 +13,8 @@ , pairNOp , cmpOp , dupOp + , carOp + , cdrOp ) where import Prelude hiding (EQ, GT, LT, many, note, some, try) @@ -33,9 +35,9 @@ primInstr :: Parser (Contract' ParsedOp) -> Parser ParsedOp -> Parser ParsedInstr primInstr contractParser opParser = choice [ dropOp, swapOp, digOp, dugOp, pushOp opParser, someOp, noneOp, unitOp - , ifNoneOp opParser, carOp, cdrOp, leftOp, rightOp, ifLeftOp opParser, nilOp + , ifNoneOp opParser, leftOp, rightOp, ifLeftOp opParser, nilOp , consOp, ifConsOp opParser, sizeOp, emptySetOp, emptyMapOp, emptyBigMapOp, iterOp opParser - , memOp, getOp, updateOp, loopLOp opParser, loopOp opParser + , memOp, getAndUpdateOp, getOp, updateOp, loopLOp opParser, loopOp opParser , lambdaOp opParser, execOp, applyOp, dipOp opParser, failWithOp, castOp, renameOp, levelOp , concatOp, packOp, unpackOp, sliceOp, isNatOp, addressOp, selfAddressOp, addOp, subOp , mulOp, edivOp, absOp, negOp, lslOp, lsrOp, orOp, andOp, xorOp, notOp @@ -246,6 +248,9 @@ varAnn <- noteDef ix <- optional (lexeme L.decimal) pure $ maybe (UPDATE varAnn) (UPDATEN varAnn) ix + +getAndUpdateOp :: Parser ParsedInstr +getAndUpdateOp = word' "GET_AND_UPDATE" GET_AND_UPDATE <*> noteDef iterOp :: Parser ParsedOp -> Parser ParsedInstr iterOp opParser = word' "ITER" ITER <*> ops' opParser diff --git a/src/Michelson/Parser/Let.hs b/src/Michelson/Parser/Let.hs --- a/src/Michelson/Parser/Let.hs +++ b/src/Michelson/Parser/Let.hs @@ -30,7 +30,7 @@ import Michelson.Parser.Type import Michelson.Parser.Types (LetEnv(..), Parser, noLetEnv) import Michelson.Parser.Value -import Michelson.Untyped (StackFn(..), Type(..), ann, noAnn) +import Michelson.Untyped (StackFn(..), Ty(..), mkAnnotation, noAnn) -- | Element of a let block data Let = LetM LetMacro | LetV LetValue | LetT LetType @@ -93,10 +93,12 @@ n <- letName upperChar <|> letName lowerChar symbol "=" return n - t@(Type t' a) <- type_ - return $ if a == noAnn - then LetType n (Type t' (ann n)) - else LetType n t + t@(Ty t' a) <- type_ + if a == noAnn + then case mkAnnotation n of + Right an -> return $ LetType n (Ty t' an) + Left err -> fail $ toString err + else return $ LetType n t letValue :: Parser ParsedOp -> Parser LetValue letValue opParser = lexeme $ do diff --git a/src/Michelson/Parser/Macro.hs b/src/Michelson/Parser/Macro.hs --- a/src/Michelson/Parser/Macro.hs +++ b/src/Michelson/Parser/Macro.hs @@ -11,6 +11,9 @@ , pairMac , ifCmpMac , mapCadrMac + , cadrMac + , carnMac + , cdrnMac ) where import Prelude hiding (note, try) @@ -27,7 +30,7 @@ import Michelson.Parser.Lexer import Michelson.Parser.Type import Michelson.Parser.Types (Parser) -import Michelson.Untyped (T(..), Type(..), noAnn) +import Michelson.Untyped (T(..), Ty(..), noAnn) import Util.Alternative (someNE) import Util.Positive @@ -53,7 +56,6 @@ <|> word' "ASSERT" ASSERT <|> do string' "DI"; n <- num "I"; symbol' "P"; DIIP (n + 1) <$> ops <|> unpairMac - <|> cadrMac <|> setCadrMac where ops = ops' opParser @@ -111,6 +113,12 @@ cadrInner :: Parser CadrStruct cadrInner = (string' "A" $> A) <|> (string' "D" $> D) +carnMac :: Parser Macro +carnMac = symbol' "CAR" *> (CARN <$> noteDef <*> lexeme decimal) + +cdrnMac :: Parser Macro +cdrnMac = symbol' "CDR" *> (CDRN <$> noteDef <*> lexeme decimal) + {-# ANN module ("HLint: ignore Reduce duplication" :: Text) #-} setCadrMac :: Parser Macro setCadrMac = do @@ -144,7 +152,7 @@ where unrollUnion ty = case ty of - Type (TOr _ _ l r) _ -> unrollUnion l . toList . unrollUnion r + Ty (TOr _ _ l r) _ -> unrollUnion l . toList . unrollUnion r _ -> (ty :|) accessMac :: Parser Macro diff --git a/src/Michelson/Parser/Type.hs b/src/Michelson/Parser/Type.hs --- a/src/Michelson/Parser/Type.hs +++ b/src/Michelson/Parser/Type.hs @@ -26,13 +26,13 @@ import Michelson.Untyped import Util.Generic -type_ :: Parser Type +type_ :: Parser Ty type_ = snd <$> typeInner (pure noAnn) -field :: Parser (FieldAnn, Type) +field :: Parser (FieldAnn, Ty) field = typeInner note -t_operator :: Parser FieldAnn -> Parser (FieldAnn, Type) +t_operator :: Parser FieldAnn -> Parser (FieldAnn, Ty) t_operator fp = do whole <- parens do optional do @@ -47,16 +47,16 @@ (f, t) <- fieldType fp case whole of Just (ty, Just (isOr, tys)) -> do - let (f', Type ty' _) = mkGenericTree (mergeTwo isOr) (ty :| tys) + let (f', Ty ty' _) = mkGenericTree (mergeTwo isOr) (ty :| tys) f'' <- mergeAnnots f f' - return (f'', Type ty' t) + return (f'', Ty ty' t) Just (res, _) -> do return res Nothing -> do - return (f, Type TUnit t) + return (f, Ty TUnit t) where mergeTwo isOr _ (l, a) (r, b) = - (noAnn, Type ((if isOr then TOr l r else TPair l r noAnn noAnn) a b) noAnn) + (noAnn, Ty ((if isOr then TOr l r else TPair l r noAnn noAnn) a b) noAnn) mergeAnnots l r | l == def = return r @@ -64,7 +64,7 @@ | otherwise = customFailure ExcessFieldAnnotation typeInner - :: Parser FieldAnn -> Parser (FieldAnn, Type) + :: Parser FieldAnn -> Parser (FieldAnn, Ty) typeInner fp = lexeme $ choice $ (\x -> x fp) <$> [ t_int, t_nat, t_string, t_bytes, t_mutez, t_bool , t_keyhash, t_timestamp, t_address @@ -82,101 +82,101 @@ -- Comparable types ---------------------------------------------------------------------------- -typeWithParen :: Parser Type +typeWithParen :: Parser Ty typeWithParen = mparens type_ ---------------------------------------------------------------------------- -- Non-comparable types ---------------------------------------------------------------------------- -mkType :: T -> (a, TypeAnn) -> (a, Type) -mkType t (a, ta) = (a, Type t ta) +mkType :: T -> (a, TypeAnn) -> (a, Ty) +mkType t (a, ta) = (a, Ty t ta) -t_int :: (Default a) => Parser a -> Parser (a, Type) +t_int :: (Default a) => Parser a -> Parser (a, Ty) t_int fp = word' "Int" (mkType TInt) <*> fieldType fp -t_nat :: (Default a) => Parser a -> Parser (a, Type) +t_nat :: (Default a) => Parser a -> Parser (a, Ty) t_nat fp = word' "Nat" (mkType TNat) <*> fieldType fp -t_string :: (Default a) => Parser a -> Parser (a, Type) +t_string :: (Default a) => Parser a -> Parser (a, Ty) t_string fp = word' "String" (mkType TString) <*> fieldType fp -t_bytes :: (Default a) => Parser a -> Parser (a, Type) +t_bytes :: (Default a) => Parser a -> Parser (a, Ty) t_bytes fp = word' "Bytes" (mkType TBytes) <*> fieldType fp -t_mutez :: (Default a) => Parser a -> Parser (a, Type) +t_mutez :: (Default a) => Parser a -> Parser (a, Ty) t_mutez fp = word' "Mutez" (mkType TMutez) <*> fieldType fp -t_bool :: (Default a) => Parser a -> Parser (a, Type) +t_bool :: (Default a) => Parser a -> Parser (a, Ty) t_bool fp = word' "Bool" (mkType TBool) <*> fieldType fp -t_keyhash :: (Default a) => Parser a -> Parser (a, Type) +t_keyhash :: (Default a) => Parser a -> Parser (a, Ty) t_keyhash fp = ((word' "KeyHash" (mkType TKeyHash)) <|> (word "key_hash" (mkType TKeyHash))) <*> fieldType fp -t_timestamp :: (Default a) => Parser a -> Parser (a, Type) +t_timestamp :: (Default a) => Parser a -> Parser (a, Ty) t_timestamp fp = word' "Timestamp" (mkType TTimestamp) <*> fieldType fp -t_address :: (Default a) => Parser a -> Parser (a, Type) +t_address :: (Default a) => Parser a -> Parser (a, Ty) t_address fp = word' "Address" (mkType TAddress) <*> fieldType fp -t_key :: (Default a) => Parser a -> Parser (a, Type) +t_key :: (Default a) => Parser a -> Parser (a, Ty) t_key fp = word' "Key" (mkType TKey) <*> fieldType fp -t_signature :: (Default a) => Parser a -> Parser (a, Type) +t_signature :: (Default a) => Parser a -> Parser (a, Ty) t_signature fp = word' "Signature" (mkType TSignature) <*> fieldType fp -t_bls12381fr :: (Default a) => Parser a -> Parser (a, Type) +t_bls12381fr :: (Default a) => Parser a -> Parser (a, Ty) t_bls12381fr fp = do symbol' "bls12_381_fr" <|> symbol' "Bls12381Fr" mkType TBls12381Fr <$> fieldType fp -t_bls12381g1 :: (Default a) => Parser a -> Parser (a, Type) +t_bls12381g1 :: (Default a) => Parser a -> Parser (a, Ty) t_bls12381g1 fp = do symbol' "bls12_381_g1" <|> symbol' "Bls12381G1" mkType TBls12381G1 <$> fieldType fp -t_bls12381g2 :: (Default a) => Parser a -> Parser (a, Type) +t_bls12381g2 :: (Default a) => Parser a -> Parser (a, Ty) t_bls12381g2 fp = do symbol' "bls12_381_g2" <|> symbol' "Bls12381G2" mkType TBls12381G2 <$> fieldType fp -t_chain_id :: (Default a) => Parser a -> Parser (a, Type) +t_chain_id :: (Default a) => Parser a -> Parser (a, Ty) t_chain_id fp = do symbol' "ChainId" <|> symbol' "chain_id" mkType TChainId <$> fieldType fp -t_operation :: (Default a) => Parser a -> Parser (a, Type) +t_operation :: (Default a) => Parser a -> Parser (a, Ty) t_operation fp = word' "Operation" (mkType TOperation) <*> fieldType fp -t_contract :: (Default a) => Parser a -> Parser (a, Type) +t_contract :: (Default a) => Parser a -> Parser (a, Ty) t_contract fp = do symbol' "Contract" (f, t) <- fieldType fp a <- type_ - return (f, Type (TContract a) t) + return (f, Ty (TContract a) t) -t_unit :: (Default a) => Parser a -> Parser (a, Type) +t_unit :: (Default a) => Parser a -> Parser (a, Ty) t_unit fp = do symbol' "Unit" <|> symbol' "()" (f,t) <- fieldType fp - return (f, Type TUnit t) + return (f, Ty TUnit t) -t_never :: (Default a) => Parser a -> Parser (a, Type) +t_never :: (Default a) => Parser a -> Parser (a, Ty) t_never fp = do symbol' "Never" <|> symbol' "⊥" (f,t) <- fieldType fp - return (f, Type TNever t) + return (f, Ty TNever t) -t_pair :: (Default a) => Parser a -> Parser (a, Type) +t_pair :: (Default a) => Parser a -> Parser (a, Ty) t_pair fp = do symbol' "Pair" (fieldAnn, typeAnn) <- fieldType fp fields <- many field tPair <- go fields - pure $ (fieldAnn, Type tPair typeAnn) + pure $ (fieldAnn, Ty tPair typeAnn) where - go :: [(FieldAnn, Type)] -> Parser T + go :: [(FieldAnn, Ty)] -> Parser T go = \case [] -> fail "The 'pair' type expects at least 2 type arguments, but 0 were given." [(_, t)] -> fail $ "The 'pair' type expects at least 2 type arguments, but only 1 was given: '" <> pretty t <> "'." @@ -184,24 +184,24 @@ pure $ TPair fieldAnnL fieldAnnR noAnn noAnn typeL typeR (fieldAnnL, typeL) : fields -> do rightCombedT <- go fields - pure $ TPair fieldAnnL noAnn noAnn noAnn typeL (Type rightCombedT noAnn) + pure $ TPair fieldAnnL noAnn noAnn noAnn typeL (Ty rightCombedT noAnn) -t_or :: (Default a) => Parser a -> Parser (a, Type) +t_or :: (Default a) => Parser a -> Parser (a, Ty) t_or fp = do symbol' "Or" (f, t) <- fieldType fp (l, a) <- field (r, b) <- field - return (f, Type (TOr l r a b) t) + return (f, Ty (TOr l r a b) t) -t_option :: (Default a) => Parser a -> Parser (a, Type) +t_option :: (Default a) => Parser a -> Parser (a, Ty) t_option fp = do symbol' "Option" (f, t) <- fieldType fp a <- mparens $ snd <$> typeInner (pure noAnn) - return (f, Type (TOption a) t) + return (f, Ty (TOption a) t) -t_lambda :: (Default a) => Parser a -> Parser (a, Type) +t_lambda :: (Default a) => Parser a -> Parser (a, Ty) t_lambda fp = core <|> slashLambda where core = do @@ -209,86 +209,86 @@ (f, t) <- fieldType fp a <- type_ b <- type_ - return (f, Type (TLambda a b) t) + return (f, Ty (TLambda a b) t) slashLambda = do symbol "\\" (f, t) <- fieldType fp a <- type_ symbol "->" b <- type_ - return (f, Type (TLambda a b) t) + return (f, Ty (TLambda a b) t) -- Container types -t_list :: (Default a) => Parser a -> Parser (a, Type) +t_list :: (Default a) => Parser a -> Parser (a, Ty) t_list fp = core <|> bracketList where core = do symbol' "List" (f, t) <- fieldType fp a <- type_ - return (f, Type (TList a) t) + return (f, Ty (TList a) t) bracketList = do a <- brackets type_ (f, t) <- fieldType fp - return (f, Type (TList a) t) + return (f, Ty (TList a) t) -t_set :: (Default a) => Parser a -> Parser (a, Type) +t_set :: (Default a) => Parser a -> Parser (a, Ty) t_set fp = core <|> braceSet where core = do symbol' "Set" (f, t) <- fieldType fp a <- typeWithParen - return (f, Type (TSet a) t) + return (f, Ty (TSet a) t) braceSet = do a <- braces typeWithParen (f, t) <- fieldType fp - return (f, Type (TSet a) t) + return (f, Ty (TSet a) t) t_map_like :: Default a - => Parser a -> Parser (Type, Type, a, TypeAnn) + => Parser a -> Parser (Ty, Ty, a, TypeAnn) t_map_like fp = do (f, t) <- fieldType fp a <- typeWithParen b <- type_ return (a, b, f, t) -t_map :: (Default a) => Parser a -> Parser (a, Type) +t_map :: (Default a) => Parser a -> Parser (a, Ty) t_map fp = do symbol' "Map" (a, b, f, t) <- t_map_like fp - return (f, Type (TMap a b) t) + return (f, Ty (TMap a b) t) -t_big_map :: (Default a) => Parser a -> Parser (a, Type) +t_big_map :: (Default a) => Parser a -> Parser (a, Ty) t_big_map fp = do symbol' "BigMap" <|> symbol "big_map" (a, b, f, t) <- t_map_like fp - return (f, Type (TBigMap a b) t) + return (f, Ty (TBigMap a b) t) ---------------------------------------------------------------------------- -- Non-standard types (Morley extensions) ---------------------------------------------------------------------------- -t_view :: Default a => Parser a -> Parser (a, Type) +t_view :: Default a => Parser a -> Parser (a, Ty) t_view fp = do symbol' "View" a <- type_ r <- type_ (f, t) <- fieldType fp - let c' = Type (TContract r) noAnn - return (f, Type (TPair noAnn noAnn noAnn noAnn a c') t) + let c' = Ty (TContract r) noAnn + return (f, Ty (TPair noAnn noAnn noAnn noAnn a c') t) -t_void :: Default a => Parser a -> Parser (a, Type) +t_void :: Default a => Parser a -> Parser (a, Ty) t_void fp = do symbol' "Void" a <- type_ b <- type_ (f, t) <- fieldType fp - let c = Type (TLambda b b) noAnn - return (f, Type (TPair noAnn noAnn noAnn noAnn a c) t) + let c = Ty (TLambda b b) noAnn + return (f, Ty (TPair noAnn noAnn noAnn noAnn a c) t) -t_letType :: Default fp => Parser fp -> Parser (fp, Type) +t_letType :: Default fp => Parser fp -> Parser (fp, Ty) t_letType fp = do lts <- asks letTypes lt <- ltSig <$> (mkLetType lts) diff --git a/src/Michelson/Runtime.hs b/src/Michelson/Runtime.hs --- a/src/Michelson/Runtime.hs +++ b/src/Michelson/Runtime.hs @@ -80,7 +80,7 @@ import qualified Michelson.Untyped as U import Tezos.Address (Address(..), OriginationIndex(..), mkContractAddress) import Tezos.Core - (Mutez, Timestamp(..), getCurrentTime, toMutez, unMutez, unsafeAddMutez, unsafeSubMutez) + (Mutez, Timestamp(..), getCurrentTime, unMutez, unsafeAddMutez, unsafeSubMutez, zeroMutez) import Tezos.Crypto (KeyHash, blake2b, parseKeyHash) import Util.Named ((.!)) @@ -518,7 +518,7 @@ let sourceAddr = fromMaybe senderAddr mSourceAddr let isKeyAddress (KeyAddress _) = True isKeyAddress _ = False - let isZeroTransfer = tdAmount txData == toMutez 0 + let isZeroTransfer = tdAmount txData == zeroMutez -- Transferring 0 XTZ to a key address is prohibited. when (isZeroTransfer && isKeyAddress addr) $ diff --git a/src/Michelson/Text.hs b/src/Michelson/Text.hs --- a/src/Michelson/Text.hs +++ b/src/Michelson/Text.hs @@ -165,9 +165,9 @@ Left err -> fail $ toString err Right txt -> [p| MTextUnsafe $(TH.litP $ TH.StringL txt) |] , TH.quoteType = \_ -> - fail "Cannot use this QuasyQuotation at type position" + fail "Cannot use this QuasiQuoter at type position" , TH.quoteDec = \_ -> - fail "Cannot use this QuasyQuotation at declaration position" + fail "Cannot use this QuasiQuoter at declaration position" } {-# ANN module ("HLint: ignore Use list literal pattern" :: Text) #-} @@ -185,13 +185,6 @@ | isMChar c -> (c :) <$> scan s | otherwise -> Left $ invalidMCharError c [] -> Right [] - -instance - TypeError ('Text "There is no instance defined for (IsString MText)" ':$$: - 'Text "Consider using QuasiQuotes: `[mt|some text...|]`" - ) => - IsString MText where - fromString = error "impossible" -- | A type error asking to use 'MText' instead of 'Text'. type family DoNotUseTextError where diff --git a/src/Michelson/TypeCheck/Error.hs b/src/Michelson/TypeCheck/Error.hs --- a/src/Michelson/TypeCheck/Error.hs +++ b/src/Michelson/TypeCheck/Error.hs @@ -25,7 +25,7 @@ import Michelson.Typed.Annotation (AnnConvergeError(..)) import Michelson.Typed.Extract (toUType) import Michelson.Typed.T (buildStack) -import Michelson.Untyped (StackFn, Type, Var) +import Michelson.Untyped (StackFn, Ty, Var) import qualified Michelson.Untyped as U import Tezos.Address (Address) import Tezos.Crypto (CryptoParseError) @@ -246,7 +246,7 @@ LengthMismatch U.StackTypePattern | VarError Text StackFn | TypeMismatch U.StackTypePattern Int TCTypeError - | TyVarMismatch Var Type U.StackTypePattern Int TCTypeError + | TyVarMismatch Var Ty U.StackTypePattern Int TCTypeError | StkRestMismatch U.StackTypePattern SomeHST SomeHST TCTypeError | TestAssertError Text | InvalidStackReference U.StackRef StackSize diff --git a/src/Michelson/TypeCheck/Ext.hs b/src/Michelson/TypeCheck/Ext.hs --- a/src/Michelson/TypeCheck/Ext.hs +++ b/src/Michelson/TypeCheck/Ext.hs @@ -22,7 +22,7 @@ import Michelson.Typed (Notes(..), converge, mkUType, notesT, withUType) import qualified Michelson.Typed as T import Michelson.Untyped - (ExpandedOp, StackFn, TyVar(..), Type, Var, VarAnn, sfnInPattern, sfnOutPattern, + (ExpandedOp, StackFn, TyVar(..), Ty, Var, VarAnn, sfnInPattern, sfnOutPattern, sfnQuantifiedVars, varSet) import qualified Michelson.Untyped as U import Util.Peano (SingNat(SS, SZ)) @@ -134,7 +134,7 @@ -> Either ExtError BoundVars checkStackType (BoundVars vars boundStkRest) s hst = go vars 0 s hst where - go :: Typeable xs => Map Var Type -> Int -> U.StackTypePattern -> HST xs + go :: Typeable xs => Map Var Ty -> Int -> U.StackTypePattern -> HST xs -> Either ExtError BoundVars go m _ U.StkRest sr = case boundStkRest of Nothing -> pure $ BoundVars m (Just $ SomeHST sr) @@ -147,7 +147,7 @@ go _ _ _ SNil = Left $ LengthMismatch s go m n (U.StkCons tyVar ts) ((xann :: Notes xt, _, _) ::& xs) = let - handleType :: U.Type -> Either ExtError BoundVars + handleType :: U.Ty -> Either ExtError BoundVars handleType t = withUType t $ \(tann :: Notes t) -> do Refl <- first diff --git a/src/Michelson/TypeCheck/Helpers.hs b/src/Michelson/TypeCheck/Helpers.hs --- a/src/Michelson/TypeCheck/Helpers.hs +++ b/src/Michelson/TypeCheck/Helpers.hs @@ -29,6 +29,7 @@ , memImpl , getImpl , updImpl + , getUpdImpl , sliceImpl , concatImpl , concatImpl' @@ -52,6 +53,7 @@ import Data.Singletons (Sing, SingI(sing), demote) import qualified Data.Text as T import Data.Typeable (eqT, (:~:)(..)) +import Data.Vinyl (Rec(..)) import Fmt ((+||), (||+)) import Michelson.ErrorPos (InstrCallStack) @@ -61,15 +63,15 @@ import Michelson.TypeCheck.Types import Michelson.Typed (BadTypeForScope(..), CommentType(StackTypeComment), Comparable, ExtInstr(COMMENT_ITEM), - Instr(..), KnownT, Notes(..), PackedNotes(..), SingT(..), T(..), WellTyped, converge, - getComparableProofS, notesT, starNotes) + Instr(..), KnownT, Notes(..), SingT(..), T(..), WellTyped, converge, getComparableProofS, notesT, + starNotes) import Michelson.Typed.Annotation (AnnConvergeError, isStar) import Michelson.Typed.Arith (Add, ArithOp(..), Mul, Sub, UnaryArithOp(..)) import Michelson.Typed.Polymorphic (ConcatOp, EDivOp(..), GetOp(..), MemOp(..), SizeOp, SliceOp, UpdOp(..)) import qualified Michelson.Untyped as Un -import Michelson.Untyped.Annotation (Annotation(..), FieldAnn, VarAnn, ann, orAnn) +import Michelson.Untyped.Annotation (Annotation(..), FieldAnn, VarAnn, orAnn, annQ, mkAnnotationUnsafe, noAnn) import Util.Type (onFirst) -- | Function which derives special annotations @@ -90,29 +92,29 @@ -> (VarAnn, FieldAnn, FieldAnn) deriveSpecialFNs pfn qfn pvn qvn vn = (vn', pfn', qfn') where - (vn1, pfn') = bool (vn, pfn) (splitLastDot pvn) (pfn == "@") - (vn2, qfn') = bool (vn, qfn) (splitLastDot qvn) (qfn == "@") + (vn1, pfn') = bool (vn, pfn) (splitLastDot pvn) (unAnnotation pfn == "@") + (vn2, qfn') = bool (vn, qfn) (splitLastDot qvn) (unAnnotation qfn == "@") vn' = bool vn (commonPrefix vn1 vn2) (vn == def) splitLastDot :: VarAnn -> (VarAnn, FieldAnn) splitLastDot v = case unsnoc $ T.splitOn "." $ unAnnotation v of Nothing -> def Just (_, "") -> (def, Un.convAnn v) - Just (vs, l) -> (foldMap ann vs, bool (ann l) def (l == "car" || l == "cdr")) + Just (vs, l) -> (foldMap mkAnnotationUnsafe vs, bool (mkAnnotationUnsafe l) def (l == "car" || l == "cdr")) commonPrefix :: VarAnn -> VarAnn -> VarAnn commonPrefix = curry \case (v1, v2) | v1 == v2 -> v1 - (v1, "") -> v1 - ("", v2) -> v2 + (v1, v2) | v2 == noAnn -> v1 + (v1, v2) | v1 == noAnn -> v2 _ -> def -- | Function which derives special annotations -- for CDR / CAR instructions. deriveSpecialVN :: VarAnn -> FieldAnn -> VarAnn -> VarAnn -> VarAnn deriveSpecialVN vn elFn pairVN elVn - | vn == "%" = Un.convAnn elFn - | vn == "%%" = pairVN <> Un.convAnn elFn + | (unAnnotation vn) == "%" = Un.convAnn elFn + | (unAnnotation vn) == "%%" = pairVN <> Un.convAnn elFn | otherwise = vn `orAnn` elVn -- | Append suffix to variable annotation (if it's not empty) @@ -126,8 +128,8 @@ -- annotations if variable annotation is not provided as second argument. deriveNsOr :: Notes ('TOr a b) -> VarAnn -> (Notes a, Notes b, VarAnn, VarAnn) deriveNsOr (NTOr _ afn bfn an bn) ovn = - let avn = deriveVN (Un.convAnn afn `orAnn` "left") ovn - bvn = deriveVN (Un.convAnn bfn `orAnn` "right") ovn + let avn = deriveVN (Un.convAnn afn `orAnn` [annQ|left|]) ovn + bvn = deriveVN (Un.convAnn bfn `orAnn` [annQ|right|]) ovn in (an, bn, avn, bvn) -- | Function which extracts annotations for @option t@ type. @@ -136,7 +138,7 @@ -- annotation for @Some@ case if it is not provided as second argument. deriveNsOption :: Notes ('TOption a) -> VarAnn -> (Notes a, VarAnn) deriveNsOption (NTOption _ an) ovn = - let avn = deriveVN "some" ovn + let avn = deriveVN [annQ|some|] ovn in (an, avn) convergeHSTEl @@ -305,7 +307,7 @@ FrameInstr _ _ -> instr' WithLoc _ _ -> instr' -- These three shouldn't happen, since annotations are added here. - InstrWithNotes _ _ -> instr' + InstrWithNotes {} -> instr' InstrWithVarAnns _ _ -> instr' InstrWithVarNotes _ _ -> instr' @@ -335,11 +337,23 @@ -- Instructions that produce at most two notes: CREATE_CONTRACT _ -> case outputStack of ((np, _, vp) ::& (_, _, vs) ::& _) -> - let withNotes = if isStar np then id else InstrWithNotes (PackedNotes np) + let withNotes = if isStar np then id else InstrWithNotes Proxy (np :& RNil) withVarNotes = if vp == Un.noAnn && vs == Un.noAnn then id else InstrWithVarNotes (vp :| [vs]) withVarNotes' = if vp == Un.noAnn && vs == Un.noAnn then id else InstrWithVarAnns $ Un.TwoVarAnns vp vs in withNotes . withVarNotes . withVarNotes' $ instr + GET_AND_UPDATE -> case outputStack of + ((valNotes, _, valVarAnn) ::& (mapNotes, _, mapVarAnn) ::& _) -> + let + -- `GET_AND_UPDATE` can have one var ann argument (e.g. 'GET_AND_UPDATE @var'), + -- which is applied to the 2nd element of the stack (the updated map). + withVarNotes = if mapVarAnn == Un.noAnn then id else InstrWithVarNotes (one mapVarAnn) + -- `GET_AND_UPDATE` puts two elements on the top of the stack, both of which + -- can have type/field/var annotations. + withNotes = if isStar valNotes && isStar mapNotes then id else InstrWithNotes Proxy (valNotes :& mapNotes :& RNil) + withVarNotes' = if valVarAnn == Un.noAnn && mapVarAnn == Un.noAnn then id else InstrWithVarAnns $ Un.TwoVarAnns valVarAnn mapVarAnn + in withNotes . withVarNotes . withVarNotes' $ instr + -- Instructions that produce at most one note: -- The cases for Ann{CAR,CDR} basically try to answer the question: -- were the var annotations explicitly written or do they come from @@ -361,8 +375,8 @@ SOME -> instr'' NONE -> instr'' AnnPAIR{} -> instr'' - LEFT -> instr'' - RIGHT -> instr'' + AnnLEFT{} -> instr'' + AnnRIGHT{} -> instr'' NIL -> instr'' CONS -> instr'' SIZE -> instr'' @@ -438,7 +452,7 @@ addNotesOneVarAnn :: HST d -> Instr c d -> Instr c d addNotesOneVarAnn outputStack instr = case outputStack of ((n, _, v) ::& _) -> - let withNotes = if isStar n then id else InstrWithNotes (PackedNotes n) + let withNotes = if isStar n then id else InstrWithNotes Proxy (n :& RNil) withVarNotes = if v == Un.noAnn then id else InstrWithVarNotes (one v) withVarNotes' = if v == Un.noAnn then id else InstrWithVarAnns $ Un.OneVarAnn v in withNotes . withVarNotes . withVarNotes' $ instr @@ -447,7 +461,7 @@ addNotesNoVarAnn :: HST d -> Instr c d -> Instr c d addNotesNoVarAnn outputStack instr = case outputStack of ((n, _, v) ::& _) -> - let withNotes = if isStar n then id else InstrWithNotes (PackedNotes n) + let withNotes = if isStar n then id else InstrWithNotes Proxy (n :& RNil) withVarNotes' = if v == Un.noAnn then id else InstrWithVarAnns $ Un.OneVarAnn v in withNotes . withVarNotes' $ instr SNil -> instr @@ -551,7 +565,7 @@ isNop :: Instr inp out -> Bool isNop (WithLoc _ i) = isNop i -isNop (InstrWithNotes _ i) = isNop i +isNop (InstrWithNotes _ _ i) = isNop i isNop (InstrWithVarNotes _ i) = isNop i isNop (FrameInstr _ i) = isNop i isNop (Seq i1 i2) = isNop i1 && isNop i2 @@ -686,6 +700,41 @@ (updValueNotes, Dict, _) = hst1 uInstr = Un.UPDATE varAnn +getUpdImpl + :: forall c updKey updParams rs inp m . + ( UpdOp c, GetOp c + , KnownT (UpdOpKey c) + , KnownT (GetOpVal c) + , inp ~ (updKey : updParams : c : rs) + , GetOpKey c ~ UpdOpKey c + , UpdOpParams c ~ 'TOption (GetOpVal c) + , MonadReader InstrCallStack m + , MonadError TCError m + ) + => Notes (UpdOpKey c) + -> HST inp + -> Notes (UpdOpParams c) + -> VarAnn + -> m (SomeInstr inp) +getUpdImpl cKeyNotes inputHST@(hst0 ::& hst1 ::& cTuple ::& hstTail) cValueNotes varAnn = + case (eqType @updKey @(UpdOpKey c), eqType @updParams @(UpdOpParams c)) of + (Right Refl, Right Refl) -> do + _ <- onTypeCheckInstrAnnErr uInstr inputHST + (Just ContainerKeyType) (converge updKeyNotes cKeyNotes) + _ <- onTypeCheckInstrAnnErr uInstr inputHST + (Just ContainerValueType) (converge updValueNotes cValueNotes) + let vn = varAnn `orAnn` (cTuple ^. _3) + pure $ inputHST :/ + GET_AND_UPDATE ::: (hst1 ::& (cTuple & _3 .~ vn) ::& hstTail) + (Left m, _) -> + typeCheckInstrErr' uInstr (SomeHST inputHST) (Just ContainerKeyType) m + (_, Left m) -> + typeCheckInstrErr' uInstr (SomeHST inputHST) (Just ContainerValueType) m + where + (updKeyNotes, Dict, _) = hst0 + (updValueNotes, Dict, _) = hst1 + uInstr = Un.GET_AND_UPDATE varAnn + sizeImpl :: (SizeOp c, inp ~ (c ': rs), Monad m) => HST inp @@ -700,7 +749,7 @@ -> Un.VarAnn -> m (SomeInstr inp) sliceImpl i@(_ ::& _ ::& (cn, Dict, cvn) ::& rs) vn = do - let vn' = vn `orAnn` deriveVN "slice" cvn + let vn' = vn `orAnn` deriveVN [annQ|slice|] cvn rn = NTOption def cn pure $ i :/ SLICE ::: ((rn, Dict, vn') ::& rs) diff --git a/src/Michelson/TypeCheck/Instr.hs b/src/Michelson/TypeCheck/Instr.hs --- a/src/Michelson/TypeCheck/Instr.hs +++ b/src/Michelson/TypeCheck/Instr.hs @@ -66,7 +66,7 @@ import Util.Type (onFirst, type (++)) import qualified Michelson.Untyped as U -import Michelson.Untyped.Annotation (FieldTag, VarAnn, VarTag, convAnn, orAnn) +import Michelson.Untyped.Annotation (FieldTag, VarAnn, VarTag, convAnn, orAnn, annQ) -- | Type check a contract and verify that the given storage -- is of the type expected by the contract. @@ -124,8 +124,8 @@ $ checkScope @(ParameterScope param) Dict <- either (hasTypeError @st "storage") pure $ checkScope @(StorageScope st) - let param = "parameter" - let store = "storage" + let param = [annQ|parameter|] + let store = [annQ|storage|] let inpNote = NTPair def def def param store paramNote storageNote let inp = (inpNote, Dict, def) ::& SNil @@ -259,16 +259,16 @@ -- Also accepts a 'TcOriginatedContracts' in order to be able to type-check -- @contract p@ values (which can only be part of a parameter). typeCheckParameter - :: TcOriginatedContracts -> U.Type -> U.Value -> Either TCError SomeValue + :: TcOriginatedContracts -> U.Ty -> U.Value -> Either TCError SomeValue typeCheckParameter originatedContracts = typeCheckTopLevelType (Just originatedContracts) -- | Like 'typeCheckValue', but for values to be used as storage. typeCheckStorage - :: U.Type -> U.Value -> Either TCError SomeValue + :: U.Ty -> U.Value -> Either TCError SomeValue typeCheckStorage = typeCheckTopLevelType Nothing typeCheckTopLevelType - :: Maybe TcOriginatedContracts -> U.Type -> U.Value -> Either TCError SomeValue + :: Maybe TcOriginatedContracts -> U.Ty -> U.Value -> Either TCError SomeValue typeCheckTopLevelType mOriginatedContracts typeU valueU = withSomeSingT (fromUType typeU) $ \(_ :: Sing t) -> SomeValue <$> typeVerifyTopLevelType @t mOriginatedContracts valueU @@ -607,19 +607,21 @@ (U.CDR _ _, SNil) -> notEnoughItemsOnStack - (U.LEFT tn vn pfn qfn bMt, (an :: Notes l, Dict, _) ::& rs) -> + (U.LEFT tn vn pfn qfn bMt, (an :: Notes l, Dict, avn) ::& rs) -> withUType bMt $ \(bn :: Notes r) -> workOnInstr uInstr $ do + let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn avn U.noAnn vn withWTPInstr @r $ do - let ns = NTOr tn pfn qfn an bn - pure (inp :/ LEFT ::: ((ns, Dict, vn) ::& rs)) + let ns = NTOr tn pfn' qfn' an bn + pure (inp :/ AnnLEFT tn pfn qfn ::: ((ns, Dict, vn') ::& rs)) (U.LEFT {}, SNil) -> notEnoughItemsOnStack - (U.RIGHT tn vn pfn qfn aMt, (bn :: Notes r, Dict, _) ::& rs) -> + (U.RIGHT tn vn pfn qfn aMt, (bn :: Notes r, Dict, bvn) ::& rs) -> withUType aMt $ \(an :: Notes l) -> workOnInstr uInstr $ do + let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn U.noAnn bvn vn withWTPInstr @l $ do - let ns = NTOr tn pfn qfn an bn - pure (inp :/ RIGHT ::: ((ns, Dict, vn) ::& rs)) + let ns = NTOr tn pfn' qfn' an bn + pure (inp :/ AnnRIGHT tn pfn qfn ::: ((ns, Dict, vn') ::& rs)) (U.RIGHT {}, SNil) -> notEnoughItemsOnStack @@ -791,15 +793,15 @@ TCGetNHelper (SS (SS ixSing)) out go _ _ = failWithErr' $ UnexpectedType $ (pairWithNodeIndex ix0 :| []) :| [] - (U.UPDATE varNotes, + (U.UPDATE varAnn, _ ::& _ ::& (STMap{}, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) -> - workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varNotes - (U.UPDATE varNotes, + workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varAnn + (U.UPDATE varAnn, _ ::& _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) -> - workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varNotes - (U.UPDATE varNotes, + workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varAnn + (U.UPDATE varAnn, _ ::& _ ::& (STSet{}, NTSet _ (notesK :: Notes k), _, _) ::&+ _) -> - workOnInstr uInstr $ updImpl notesK inp (NTBool U.noAnn) varNotes + workOnInstr uInstr $ updImpl notesK inp (NTBool U.noAnn) varAnn (U.UPDATE _, _ ::& _ ::& _ ::& _) -> failWithErr $ UnexpectedType @@ -830,6 +832,23 @@ go _ _ = failWithErr' $ UnexpectedType $ ("'val" :| [pairWithNodeIndex ix0]) :| [] (U.UPDATEN _ _, _) -> notEnoughItemsOnStack + (U.GET_AND_UPDATE varAnn, + _ ::& _ ::& (STMap{}, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) -> + workOnInstr uInstr $ + withWTPInstr @v $ + getUpdImpl notesK inp (NTOption U.noAnn notesV) varAnn + (U.GET_AND_UPDATE varAnn, + _ ::& _ ::& (STBigMap{}, (NTBigMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) -> + workOnInstr uInstr $ + withWTPInstr @v $ + getUpdImpl notesK inp (NTOption U.noAnn notesV) varAnn + (U.GET_AND_UPDATE _, _ ::& _ ::& _ ::& _) -> + failWithErr $ UnexpectedType + $ ("'k" :| ["option 'v", "map 'k 'v"]) :| + [ ("'k" :| ["option 'v", "big_map 'k 'v"]) + ] + (U.GET_AND_UPDATE _, _) -> notEnoughItemsOnStack + (U.IF mp mq, (NTBool{}, _, _) ::& rs) -> genericIf IF U.IF mp mq rs rs inp @@ -1521,7 +1540,7 @@ -> HST (c ': rs) -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs)) iterImpl en instr mp i@((_, _, lvn) ::& rs) = do - let evn = deriveVN "elt" lvn + let evn = deriveVN [annQ|elt|] lvn let tcAction = case mp of [] -> workOnInstr instr (typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode) diff --git a/src/Michelson/TypeCheck/Types.hs b/src/Michelson/TypeCheck/Types.hs --- a/src/Michelson/TypeCheck/Types.hs +++ b/src/Michelson/TypeCheck/Types.hs @@ -34,7 +34,7 @@ import Michelson.Typed.Haskell.Value (WellTyped) import qualified Michelson.Typed as T import Michelson.Typed.Instr -import Michelson.Untyped (Type, Var, noAnn) +import Michelson.Untyped (Ty, Var, noAnn) import Michelson.Untyped.Annotation (VarAnn) import Util.Typeable @@ -208,7 +208,7 @@ deriving stock instance Show SomeContractAndStorage -- | Set of variables defined in a let-block. -data BoundVars = BoundVars (Map Var Type) (Maybe SomeHST) +data BoundVars = BoundVars (Map Var Ty) (Maybe SomeHST) noBoundVars :: BoundVars noBoundVars = BoundVars Map.empty Nothing diff --git a/src/Michelson/TypeCheck/Value.hs b/src/Michelson/TypeCheck/Value.hs --- a/src/Michelson/TypeCheck/Value.hs +++ b/src/Michelson/TypeCheck/Value.hs @@ -69,7 +69,7 @@ | i >= 0 -> pure $ VNat (fromInteger i) | otherwise -> tcFailedOnValue v (fromSingT t) "" (Just NegativeNat) (v@(U.ValueInt i), t@STMutez) -> case mkMutez $ fromInteger i of - Just mtz -> pure $ VMutez mtz + Just m -> pure $ VMutez m Nothing -> tcFailedOnValue v (fromSingT t) "" (Just InvalidTimestamp) (U.ValueString s, STString) -> pure $ VString s (v@(U.ValueString s), t@STAddress) -> case T.parseEpAddress (unMText s) of diff --git a/src/Michelson/Typed/Annotation.hs b/src/Michelson/Typed/Annotation.hs --- a/src/Michelson/Typed/Annotation.hs +++ b/src/Michelson/Typed/Annotation.hs @@ -29,7 +29,6 @@ , notesT ) where -import qualified Data.Kind as Kind import Data.Singletons (Sing, SingI(..)) import Fmt (Buildable(..), (+|), (|+)) import Text.PrettyPrint.Leijen.Text (Doc, (<+>)) @@ -262,7 +261,7 @@ data AnnConvergeError where AnnConvergeError - :: forall (tag :: Kind.Type). + :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => Annotation tag -> Annotation tag -> AnnConvergeError @@ -277,7 +276,7 @@ "Annotations do not converge: " +| ann1 |+ " /= " +| ann2 |+ "" convergeAnnsImpl - :: forall (tag :: Kind.Type). + :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => (Annotation tag -> Annotation tag -> Maybe (Annotation tag)) -> Annotation tag -> Annotation tag -> Either AnnConvergeError (Annotation tag) @@ -285,7 +284,7 @@ -- | Converge two type or field notes (which may be wildcards). convergeAnns - :: forall (tag :: Kind.Type). + :: forall (tag :: Type). (Buildable (Annotation tag), Show (Annotation tag), Typeable tag) => Annotation tag -> Annotation tag -> Either AnnConvergeError (Annotation tag) convergeAnns = convergeAnnsImpl unifyAnn diff --git a/src/Michelson/Typed/Convert.hs b/src/Michelson/Typed/Convert.hs --- a/src/Michelson/Typed/Convert.hs +++ b/src/Michelson/Typed/Convert.hs @@ -22,7 +22,8 @@ import Data.Constraint (Dict(..)) import qualified Data.Map as Map import Data.Singletons (Sing, demote) -import Fmt (Buildable(..), fmt, listF, pretty) +import Data.Vinyl (Rec(..)) +import Fmt (Buildable(..), Builder, blockListF, fmt, indentF, listF, pretty, unlinesF) import Michelson.Text import Michelson.Typed.Aliases @@ -141,7 +142,7 @@ where vList ctor = maybe U.ValueNil ctor . nonEmpty -untypeDemoteT :: forall (t :: T). SingI t => U.Type +untypeDemoteT :: forall (t :: T). SingI t => U.Ty untypeDemoteT = toUType $ demote @t instrToOps :: HasCallStack => Instr inp out -> [U.ExpandedOp] @@ -156,19 +157,19 @@ -- this place should be updated to pass it from typed to untyped ASTs. WithLoc _ i -> instrToOps i InstrWithVarAnns _ i -> instrToOps i - InstrWithNotes n i -> case i of + InstrWithNotes proxy n i -> case i of Nop -> instrToOps i Seq _ _ -> instrToOps i Nested _ -> instrToOps i DocGroup _ _ -> instrToOps i Ext _ -> instrToOps i - WithLoc _ i0 -> instrToOps (InstrWithNotes n i0) - InstrWithNotes _ _ -> instrToOps i + WithLoc _ i0 -> instrToOps (InstrWithNotes proxy n i0) + InstrWithNotes {} -> instrToOps i -- For inner instruction, filter out values that we don't want to apply -- annotations to and delegate it's conversion to this function itself. -- If none of the above, convert a single instruction and copy annotations -- to it. - InstrWithVarNotes n0 (InstrWithVarAnns _ i0) -> instrToOps $ InstrWithNotes n $ InstrWithVarNotes n0 i0 + InstrWithVarNotes n0 (InstrWithVarAnns _ i0) -> instrToOps $ InstrWithNotes proxy n $ InstrWithVarNotes n0 i0 InstrWithVarNotes n0 i0 -> [U.PrimEx $ handleInstrAnnotateWithVarNotes i0 n n0] InstrWithVarAnns _ _ -> instrToOps i _ -> [U.PrimEx $ handleInstrAnnotate i n] @@ -179,137 +180,164 @@ DocGroup _ _ -> instrToOps i Ext _ -> instrToOps i WithLoc _ i0 -> instrToOps (InstrWithVarNotes n i0) - InstrWithNotes n0 (InstrWithVarAnns _ i0) -> instrToOps $ InstrWithNotes n0 $ InstrWithVarNotes n i0 - InstrWithNotes n0 i0 -> [U.PrimEx $ handleInstrAnnotateWithVarNotes i0 n0 n] + InstrWithNotes p0 n0 (InstrWithVarAnns _ i0) -> instrToOps $ InstrWithNotes p0 n0 $ InstrWithVarNotes n i0 + InstrWithNotes _ n0 i0 -> [U.PrimEx $ handleInstrAnnotateWithVarNotes i0 n0 n] InstrWithVarNotes _ _ -> instrToOps i InstrWithVarAnns _ i0 -> instrToOps $ InstrWithVarNotes n i0 _ -> [U.PrimEx $ handleInstrVarNotes i n] i -> [U.PrimEx $ handleInstr i] where handleInstrAnnotateWithVarNotes - :: forall inp' out' - . HasCallStack + :: forall inp' out' topElems + . (HasCallStack, Each '[SingI] topElems) => Instr inp' out' - -> PackedNotes out' + -> Rec Notes topElems -> NonEmpty U.VarAnn -> U.ExpandedInstr - handleInstrAnnotateWithVarNotes ins' (PackedNotes notes') varAnns = - let x = handleInstr ins' in addVarNotes (addInstrNote x notes') varAnns + handleInstrAnnotateWithVarNotes instr notes varAnns = + addVarNotes (addInstrNote (handleInstr instr) notes) varAnns handleInstrAnnotate - :: forall inp' out' . HasCallStack - => Instr inp' out' -> PackedNotes out' -> U.ExpandedInstr - handleInstrAnnotate ins' (PackedNotes notes') = let - x = handleInstr ins' in addInstrNote x notes' + :: forall inp' out' topElems. + (HasCallStack, Each '[SingI] topElems) + => Instr inp' out' -> Rec Notes topElems -> U.ExpandedInstr + handleInstrAnnotate ins' notes = + addInstrNote (handleInstr ins') notes addInstrNote - :: forall t. (SingI t, HasCallStack) - => U.ExpandedInstr -> Notes t -> U.ExpandedInstr - addInstrNote ins nte = case (sing @t, ins, nte) of - (_, U.PUSH va _ v, _) -> U.PUSH va (mkUType nte) v - (_, U.SOME _ va, NTOption ta _) -> U.SOME ta va - (STOption _, U.NONE _ va _, NTOption ta nt) -> U.NONE ta va (mkUType nt) - (_, U.UNIT _ va, NTUnit ta) -> U.UNIT ta va - (_, U.PAIR ta va f1 f2, _) -> U.PAIR ta va f1 f2 - (_, U.PAIRN va n, _) -> U.PAIRN va n - (_, U.CAR va f1, _) -> U.CAR va f1 - (_, U.CDR va f1, _) -> U.CDR va f1 - (STOr _ _, U.LEFT _ va _ _ _, NTOr ta f1 f2 _ n2) -> - U.LEFT ta va f1 f2 (mkUType n2) - (STOr _ _, U.RIGHT _ va _ _ _, NTOr ta f1 f2 n1 _) -> - U.RIGHT ta va f1 f2 (mkUType n1) - (STList _, U.NIL _ va _, NTList ta n) -> U.NIL ta va (mkUType n) - (STSet _, U.EMPTY_SET _ va _, NTSet ta1 n) -> - U.EMPTY_SET ta1 va (mkUType n) - (STMap _ _, U.EMPTY_MAP _ va _ _, NTMap ta1 k n) -> - U.EMPTY_MAP ta1 va (mkUType k) (mkUType n) - (STBigMap _ _, U.EMPTY_BIG_MAP _ va _ _, NTBigMap ta1 k n) -> - U.EMPTY_BIG_MAP ta1 va (mkUType k) (mkUType n) - (STLambda _ _, U.LAMBDA va _ _ ops, NTLambda _ n1 n2) -> - U.LAMBDA va (mkUType n1) (mkUType n2) ops - (_, U.CAST va _, n) -> U.CAST va (mkUType n) - (STOption _, U.UNPACK _ va _, NTOption ta nt) -> U.UNPACK ta va (mkUType nt) - (STOption (STContract _), U.CONTRACT va fa _, NTOption _ (NTContract _ nt)) -> - U.CONTRACT va fa (mkUType nt) - (_, U.CONTRACT va fa t, NTOption _ _) -> U.CONTRACT va fa t - (_, a@(U.APPLY {}), _) -> a - (_, a@(U.CHAIN_ID {}), _) -> a - (_, a@(U.EXT _), _) -> a - (_, a@(U.DROP), _) -> a - (_, a@(U.DROPN _), _) -> a - (_, a@(U.DUP _), _) -> a - (_, a@(U.DUPN _ _), _) -> a - (_, a@(U.SWAP), _) -> a - (_, a@(U.DIG {}), _) -> a - (_, a@(U.DUG {}), _) -> a - (_, a@(U.IF_NONE _ _), _) -> a - (_, a@(U.CONS _), _) -> a - (_, a@(U.IF_LEFT _ _), _) -> a - (_, a@(U.IF_CONS _ _), _) -> a - (_, a@(U.SIZE _), _) -> a - (_, a@(U.MAP _ _), _) -> a - (_, a@(U.ITER _), _) -> a - (_, a@(U.MEM _), _) -> a - (_, a@(U.GET _), _) -> a - (_, a@(U.GETN _ _), _) -> a - (_, a@(U.UPDATE _), _) -> a - (_, a@(U.UPDATEN _ _), _) -> a - (_, a@(U.IF _ _), _) -> a - (_, a@(U.LOOP _), _) -> a - (_, a@(U.LOOP_LEFT _), _) -> a - (_, a@(U.EXEC _), _) -> a - (_, a@(U.DIP _), _) -> a - (_, a@(U.DIPN {}), _) -> a - (_, a@(U.FAILWITH), _) -> a - (_, a@(U.RENAME _), _) -> a - (_, a@(U.PACK _), _) -> a - (_, a@(U.CONCAT _), _) -> a - (_, a@(U.SLICE _), _) -> a - (_, a@(U.ISNAT _), _) -> a - (_, a@(U.ADD _), _) -> a - (_, a@(U.SUB _), _) -> a - (_, a@(U.MUL _), _) -> a - (_, a@(U.EDIV _), _) -> a - (_, a@(U.ABS _), _) -> a - (_, a@(U.NEG _), _) -> a - (_, a@(U.LSL _), _) -> a - (_, a@(U.LSR _), _) -> a - (_, a@(U.OR _), _) -> a - (_, a@(U.AND _), _) -> a - (_, a@(U.XOR _), _) -> a - (_, a@(U.NOT _), _) -> a - (_, a@(U.COMPARE _), _) -> a - (_, a@(U.EQ _), _) -> a - (_, a@(U.NEQ _), _) -> a - (_, a@(U.LT _), _) -> a - (_, a@(U.GT _), _) -> a - (_, a@(U.LE _), _) -> a - (_, a@(U.GE _), _) -> a - (_, a@(U.INT _), _) -> a - (_, a@(U.SELF _ _), _) -> a - (_, a@(U.TRANSFER_TOKENS _), _) -> a - (_, a@(U.SET_DELEGATE _), _) -> a - (_, a@(U.CREATE_CONTRACT {}), _) -> a - (_, a@(U.IMPLICIT_ACCOUNT _), _) -> a - (_, a@(U.NOW _), _) -> a - (_, a@(U.LEVEL _), _) -> a - (_, a@(U.AMOUNT _), _) -> a - (_, a@(U.BALANCE _), _) -> a - (_, a@(U.VOTING_POWER _), _) -> a - (_, a@(U.TOTAL_VOTING_POWER _), _) -> a - (_, a@(U.CHECK_SIGNATURE _), _) -> a - (_, a@(U.SHA256 _), _) -> a - (_, a@(U.SHA512 _), _) -> a - (_, a@(U.BLAKE2B _), _) -> a - (_, a@(U.SHA3 _), _) -> a - (_, a@(U.KECCAK _), _) -> a - (_, a@(U.HASH_KEY _), _) -> a - (_, a@(U.SOURCE _), _) -> a - (_, a@(U.SENDER _), _) -> a - (_, a@(U.ADDRESS _), _) -> a - (_, a@(U.SELF_ADDRESS _), _) -> a - (_, a@(U.NEVER), _) -> a - (_, b, c) -> error $ "addInstrNote: Unexpected instruction/annotation combination: " <> show (b, c) + :: forall topElems. (Each '[SingI] topElems, HasCallStack) + => U.ExpandedInstr -> Rec Notes topElems -> U.ExpandedInstr + addInstrNote instr notes = + case (instr, notes) of + (U.PUSH va _ v, notes' :& _) -> U.PUSH va (mkUType notes') v + (U.SOME _ va, NTOption ta _ :& _) -> U.SOME ta va + (U.NONE _ va _, (NTOption ta nt :: Notes t) :& _) -> + case sing @t of + STOption {} -> U.NONE ta va (mkUType nt) + (U.UNIT _ va, NTUnit ta :& _) -> U.UNIT ta va + (U.PAIR ta va f1 f2, _) -> U.PAIR ta va f1 f2 + (U.PAIRN va n, _) -> U.PAIRN va n + (U.CAR va f1, _) -> U.CAR va f1 + (U.CDR va f1, _) -> U.CDR va f1 + (U.LEFT _ va _ _ _, (NTOr ta f1 f2 _ n2 :: Notes t) :& _) -> + case sing @t of + STOr {} -> U.LEFT ta va f1 f2 (mkUType n2) + (U.RIGHT _ va _ _ _, (NTOr ta f1 f2 n1 _ :: Notes t) :& _) -> + case sing @t of + STOr {} -> U.RIGHT ta va f1 f2 (mkUType n1) + (U.NIL _ va _, (NTList ta n :: Notes t) :& _) -> + case sing @t of + STList {} -> U.NIL ta va (mkUType n) + (U.EMPTY_SET _ va _, (NTSet ta1 n :: Notes t) :& _) -> + case sing @t of + STSet {} -> U.EMPTY_SET ta1 va (mkUType n) + (U.EMPTY_MAP _ va _ _, (NTMap ta1 k n :: Notes t) :& _) -> + case sing @t of + STMap {} -> U.EMPTY_MAP ta1 va (mkUType k) (mkUType n) + (U.EMPTY_BIG_MAP _ va _ _, (NTBigMap ta1 k n :: Notes t) :& _) -> + case sing @t of + STBigMap {} -> U.EMPTY_BIG_MAP ta1 va (mkUType k) (mkUType n) + (U.LAMBDA va _ _ ops, (NTLambda _ n1 n2 :: Notes t) :& _) -> + case sing @t of + STLambda {} -> U.LAMBDA va (mkUType n1) (mkUType n2) ops + (U.CAST va _, n :& _) -> U.CAST va (mkUType n) + (U.UNPACK _ va _, (NTOption ta nt :: Notes t) :& _) -> + case sing @t of + STOption {} -> U.UNPACK ta va (mkUType nt) + (U.CONTRACT va fa _, (NTOption _ (NTContract _ nt :: Notes t) :: Notes t2) :& _) -> + case sing @t2 of + STOption STContract {} -> U.CONTRACT va fa (mkUType nt) + (U.CONTRACT va fa t, NTOption _ _ :& _) -> U.CONTRACT va fa t + (U.APPLY {}, _) -> instr + (U.CHAIN_ID {}, _) -> instr + (U.EXT _, _) -> instr + (U.DROP, _) -> instr + (U.DROPN _, _) -> instr + (U.DUP _, _) -> instr + (U.DUPN _ _, _) -> instr + (U.SWAP, _) -> instr + (U.DIG {}, _) -> instr + (U.DUG {}, _) -> instr + (U.IF_NONE _ _, _) -> instr + (U.CONS _, _) -> instr + (U.IF_LEFT _ _, _) -> instr + (U.IF_CONS _ _, _) -> instr + (U.SIZE _, _) -> instr + (U.MAP _ _, _) -> instr + (U.ITER _, _) -> instr + (U.MEM _, _) -> instr + (U.GET _, _) -> instr + (U.GETN _ _, _) -> instr + (U.UPDATE _, _) -> instr + (U.UPDATEN _ _, _) -> instr + (U.GET_AND_UPDATE _, _) -> instr + (U.IF _ _, _) -> instr + (U.LOOP _, _) -> instr + (U.LOOP_LEFT _, _) -> instr + (U.EXEC _, _) -> instr + (U.DIP _, _) -> instr + (U.DIPN {}, _) -> instr + (U.FAILWITH, _) -> instr + (U.RENAME _, _) -> instr + (U.PACK _, _) -> instr + (U.CONCAT _, _) -> instr + (U.SLICE _, _) -> instr + (U.ISNAT _, _) -> instr + (U.ADD _, _) -> instr + (U.SUB _, _) -> instr + (U.MUL _, _) -> instr + (U.EDIV _, _) -> instr + (U.ABS _, _) -> instr + (U.NEG _, _) -> instr + (U.LSL _, _) -> instr + (U.LSR _, _) -> instr + (U.OR _, _) -> instr + (U.AND _, _) -> instr + (U.XOR _, _) -> instr + (U.NOT _, _) -> instr + (U.COMPARE _, _) -> instr + (U.EQ _, _) -> instr + (U.NEQ _, _) -> instr + (U.LT _, _) -> instr + (U.GT _, _) -> instr + (U.LE _, _) -> instr + (U.GE _, _) -> instr + (U.INT _, _) -> instr + (U.SELF _ _, _) -> instr + (U.TRANSFER_TOKENS _, _) -> instr + (U.SET_DELEGATE _, _) -> instr + (U.CREATE_CONTRACT {}, _) -> instr + (U.IMPLICIT_ACCOUNT _, _) -> instr + (U.NOW _, _) -> instr + (U.LEVEL _, _) -> instr + (U.AMOUNT _, _) -> instr + (U.BALANCE _, _) -> instr + (U.VOTING_POWER _, _) -> instr + (U.TOTAL_VOTING_POWER _, _) -> instr + (U.CHECK_SIGNATURE _, _) -> instr + (U.SHA256 _, _) -> instr + (U.SHA512 _, _) -> instr + (U.BLAKE2B _, _) -> instr + (U.SHA3 _, _) -> instr + (U.KECCAK _, _) -> instr + (U.HASH_KEY _, _) -> instr + (U.SOURCE _, _) -> instr + (U.SENDER _, _) -> instr + (U.ADDRESS _, _) -> instr + (U.SELF_ADDRESS _, _) -> instr + (U.NEVER, _) -> instr + _ -> error $ pretty $ unlinesF + [ "addInstrNote: Unexpected instruction/annotation combination" + , "Instruction:" + , indentF 2 $ build instr + , "Annotations:" + , indentF 2 $ blockListF $ buildNotes notes + ] + where + buildNotes :: Rec Notes ts -> [Builder] + buildNotes = \case + RNil -> [] + n :& ns -> build n : buildNotes ns handleInstrVarNotes :: forall inp' out' . HasCallStack => Instr inp' out' -> NonEmpty U.VarAnn -> U.ExpandedInstr @@ -349,6 +377,7 @@ U.GETN _ n -> U.GETN va n U.UPDATE _ -> U.UPDATE va U.UPDATEN _ n -> U.UPDATEN va n + U.GET_AND_UPDATE _ -> U.GET_AND_UPDATE va U.LAMBDA _ t1 t2 ops -> U.LAMBDA va t1 t2 ops U.EXEC _ -> U.EXEC va U.APPLY _ -> U.APPLY va @@ -411,7 +440,7 @@ handleInstr :: Instr inp out -> U.ExpandedInstr handleInstr = \case (WithLoc _ _) -> error "impossible" - (InstrWithNotes _ _) -> error "impossible" + InstrWithNotes {} -> error "impossible" (InstrWithVarNotes _ _) -> error "impossible" (InstrWithVarAnns _ _) -> error "impossible" (FrameInstr _ _) -> error "impossible" @@ -440,10 +469,10 @@ UNPAIRN n -> U.UNPAIRN (fromIntegral $ peanoValSing n) (AnnCAR fn) -> U.CAR U.noAnn fn (AnnCDR fn) -> U.CDR U.noAnn fn - i@LEFT | _ :: Instr (a ': s) ('TOr a b ': s) <- i -> - U.LEFT U.noAnn U.noAnn U.noAnn U.noAnn (untypeDemoteT @b) - i@RIGHT | _ :: Instr (b ': s) ('TOr a b ': s) <- i -> - U.RIGHT U.noAnn U.noAnn U.noAnn U.noAnn (untypeDemoteT @a) + i@(AnnLEFT tn fn1 fn2) | _ :: Instr (a ': s) ('TOr a b ': s) <- i -> + U.LEFT tn U.noAnn fn1 fn2 (untypeDemoteT @b) + i@(AnnRIGHT tn fn1 fn2) | _ :: Instr (b ': s) ('TOr a b ': s) <- i -> + U.RIGHT tn U.noAnn fn1 fn2 (untypeDemoteT @a) (IF_LEFT i1 i2) -> U.IF_LEFT (instrToOps i1) (instrToOps i2) i@NIL | _ :: Instr s ('TList p ': s) <- i -> U.NIL U.noAnn U.noAnn (untypeDemoteT @p) @@ -451,12 +480,12 @@ (IF_CONS i1 i2) -> U.IF_CONS (instrToOps i1) (instrToOps i2) SIZE -> U.SIZE U.noAnn i@EMPTY_SET | _ :: Instr s ('TSet e ': s) <- i -> - U.EMPTY_SET U.noAnn U.noAnn (U.Type (U.unwrapT $ untypeDemoteT @e) U.noAnn) + U.EMPTY_SET U.noAnn U.noAnn (U.Ty (U.unwrapT $ untypeDemoteT @e) U.noAnn) i@EMPTY_MAP | _ :: Instr s ('TMap a b ': s) <- i -> - U.EMPTY_MAP U.noAnn U.noAnn (U.Type (U.unwrapT $ untypeDemoteT @a) U.noAnn) + U.EMPTY_MAP U.noAnn U.noAnn (U.Ty (U.unwrapT $ untypeDemoteT @a) U.noAnn) (untypeDemoteT @b) i@EMPTY_BIG_MAP | _ :: Instr s ('TBigMap a b ': s) <- i -> - U.EMPTY_BIG_MAP U.noAnn U.noAnn (U.Type (U.unwrapT $ untypeDemoteT @a) U.noAnn) + U.EMPTY_BIG_MAP U.noAnn U.noAnn (U.Ty (U.unwrapT $ untypeDemoteT @a) U.noAnn) (untypeDemoteT @b) (MAP op) -> U.MAP U.noAnn $ instrToOps op (ITER op) -> U.ITER $ instrToOps op @@ -465,6 +494,7 @@ GETN n -> U.GETN U.noAnn (fromIntegral $ peanoValSing n) UPDATE -> U.UPDATE U.noAnn UPDATEN n -> U.UPDATEN U.noAnn (fromIntegral $ peanoValSing n) + GET_AND_UPDATE -> U.GET_AND_UPDATE U.noAnn (IF op1 op2) -> U.IF (instrToOps op1) (instrToOps op2) (LOOP op) -> U.LOOP (instrToOps op) (LOOP_LEFT op) -> U.LOOP_LEFT (instrToOps op) @@ -664,5 +694,5 @@ -- | Flatten a provided list of notes to a map of its entrypoints and its -- corresponding utype. Please refer to 'mkEntrypointsMap' in regards to how -- duplicate entrypoints are handled. -flattenEntrypoints :: SingI t => ParamNotes t -> Map EpName U.Type +flattenEntrypoints :: SingI t => ParamNotes t -> Map EpName U.Ty flattenEntrypoints = U.mkEntrypointsMap . convertParamNotes diff --git a/src/Michelson/Typed/Extract.hs b/src/Michelson/Typed/Extract.hs --- a/src/Michelson/Typed/Extract.hs +++ b/src/Michelson/Typed/Extract.hs @@ -2,12 +2,12 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ --- | Module, containing functions to convert @Michelson.Untyped.Type@ to +-- | Module, containing functions to convert @Michelson.Untyped.Ty@ to -- @Michelson.Typed.T.T@ Michelson type representation (type stripped off all -- annotations) and to @Michelson.Typed.Annotation.Notes@ value (which contains -- field and type annotations for a given Michelson type). -- --- I.e. @Michelson.Untyped.Type@ is split to value @t :: T@ and value of type +-- I.e. @Michelson.Untyped.Ty@ is split to value @t :: T@ and value of type -- @Notes t@ for which @t@ is a type representation of value @t@. module Michelson.Typed.Extract ( fromUType @@ -28,51 +28,51 @@ {-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-} -fromUType :: Un.Type -> T +fromUType :: Un.Ty -> T fromUType ut = withUType ut (fromSingT . notesSing) -mkUType :: SingI x => Notes x -> Un.Type +mkUType :: SingI x => Notes x -> Un.Ty mkUType notes = case (notesSing notes, notes) of - (STInt, NTInt tn) -> Un.Type Un.TInt tn - (STNat, NTNat tn) -> Un.Type Un.TNat tn - (STString, NTString tn) -> Un.Type Un.TString tn - (STBytes, NTBytes tn) -> Un.Type Un.TBytes tn - (STMutez, NTMutez tn) -> Un.Type Un.TMutez tn - (STBool, NTBool tn) -> Un.Type Un.TBool tn - (STKeyHash, NTKeyHash tn) -> Un.Type Un.TKeyHash tn - (STBls12381Fr, NTBls12381Fr tn) -> Un.Type Un.TBls12381Fr tn - (STBls12381G1, NTBls12381G1 tn) -> Un.Type Un.TBls12381G1 tn - (STBls12381G2, NTBls12381G2 tn) -> Un.Type Un.TBls12381G2 tn - (STTimestamp, NTTimestamp tn) -> Un.Type Un.TTimestamp tn - (STAddress, NTAddress tn) -> Un.Type Un.TAddress tn - (STKey, NTKey tn) -> Un.Type Un.TKey tn - (STUnit, NTUnit tn) -> Un.Type Un.TUnit tn - (STSignature, NTSignature tn) -> Un.Type Un.TSignature tn - (STChainId, NTChainId tn) -> Un.Type Un.TChainId tn - (STOption _, NTOption tn n) -> Un.Type (Un.TOption (mkUType n)) tn - (STList _, NTList tn n) -> Un.Type (Un.TList (mkUType n)) tn - (STSet _, NTSet tn n) -> Un.Type (Un.TSet (mkUType n)) tn - (STOperation, NTOperation tn) -> Un.Type Un.TOperation tn - (STNever, NTNever tn) -> Un.Type Un.TNever tn + (STInt, NTInt tn) -> Un.Ty Un.TInt tn + (STNat, NTNat tn) -> Un.Ty Un.TNat tn + (STString, NTString tn) -> Un.Ty Un.TString tn + (STBytes, NTBytes tn) -> Un.Ty Un.TBytes tn + (STMutez, NTMutez tn) -> Un.Ty Un.TMutez tn + (STBool, NTBool tn) -> Un.Ty Un.TBool tn + (STKeyHash, NTKeyHash tn) -> Un.Ty Un.TKeyHash tn + (STBls12381Fr, NTBls12381Fr tn) -> Un.Ty Un.TBls12381Fr tn + (STBls12381G1, NTBls12381G1 tn) -> Un.Ty Un.TBls12381G1 tn + (STBls12381G2, NTBls12381G2 tn) -> Un.Ty Un.TBls12381G2 tn + (STTimestamp, NTTimestamp tn) -> Un.Ty Un.TTimestamp tn + (STAddress, NTAddress tn) -> Un.Ty Un.TAddress tn + (STKey, NTKey tn) -> Un.Ty Un.TKey tn + (STUnit, NTUnit tn) -> Un.Ty Un.TUnit tn + (STSignature, NTSignature tn) -> Un.Ty Un.TSignature tn + (STChainId, NTChainId tn) -> Un.Ty Un.TChainId tn + (STOption _, NTOption tn n) -> Un.Ty (Un.TOption (mkUType n)) tn + (STList _, NTList tn n) -> Un.Ty (Un.TList (mkUType n)) tn + (STSet _, NTSet tn n) -> Un.Ty (Un.TSet (mkUType n)) tn + (STOperation, NTOperation tn) -> Un.Ty Un.TOperation tn + (STNever, NTNever tn) -> Un.Ty Un.TNever tn (STContract _, NTContract tn n) -> - Un.Type (Un.TContract (mkUType n)) tn + Un.Ty (Un.TContract (mkUType n)) tn (STPair _ _, NTPair tn fl fr vl vr nl nr) -> - Un.Type (Un.TPair fl fr vl vr (mkUType nl) (mkUType nr)) tn + Un.Ty (Un.TPair fl fr vl vr (mkUType nl) (mkUType nr)) tn (STOr _ _, NTOr tn fl fr nl nr) -> - Un.Type (Un.TOr fl fr (mkUType nl) (mkUType nr)) tn + Un.Ty (Un.TOr fl fr (mkUType nl) (mkUType nr)) tn (STLambda _ _, NTLambda tn np nq) -> - Un.Type (Un.TLambda (mkUType np) (mkUType nq)) tn + Un.Ty (Un.TLambda (mkUType np) (mkUType nq)) tn (STMap _ _, NTMap tn nk nv) -> - Un.Type (Un.TMap (mkUType nk) (mkUType nv)) tn + Un.Ty (Un.TMap (mkUType nk) (mkUType nv)) tn (STBigMap _ _, NTBigMap tn nk nv) -> - Un.Type (Un.TBigMap (mkUType nk) (mkUType nv)) tn + Un.Ty (Un.TBigMap (mkUType nk) (mkUType nv)) tn --- | Convert 'Un.Type' to the isomorphic set of information from typed world. +-- | Convert 'Un.Ty' to the isomorphic set of information from typed world. withUType - :: Un.Type + :: Un.Ty -> (forall t. KnownT t => Notes t -> r) -> r -withUType (Un.Type ut tn) cont = case ut of +withUType (Un.Ty ut tn) cont = case ut of Un.TInt -> cont (NTInt tn) @@ -172,7 +172,7 @@ -- Helper datatype for 'AsUType'. data SomeTypedInfo = forall t. KnownT t => SomeTypedInfo (Notes t) --- | Transparently represent untyped 'Type' as wrapper over @Notes t@ +-- | Transparently represent untyped 'Ty' as wrapper over @Notes t@ -- from typed world with @SingI t@ constraint. -- -- As expression this carries logic of 'mkUType', and as pattern it performs @@ -181,13 +181,13 @@ -- Note about constraints: pattern signatures usually require two constraints - -- one they require and another one which they provide. In our case we require -- nothing (thus first constraint is @()@) and provide some knowledge about @t@. -pattern AsUType :: () => (KnownT t) => Notes t -> Un.Type +pattern AsUType :: () => (KnownT t) => Notes t -> Un.Ty pattern AsUType notes <- ((\ut -> withUType ut SomeTypedInfo) -> SomeTypedInfo notes) where AsUType notes = mkUType notes {-# COMPLETE AsUType #-} -- | Similar to 'AsUType', but also gives 'Sing' for given type. -pattern AsUTypeExt :: () => (KnownT t) => Sing t -> Notes t -> Un.Type +pattern AsUTypeExt :: () => (KnownT t) => Sing t -> Notes t -> Un.Ty pattern AsUTypeExt sng notes <- AsUType notes@(notesSing -> sng) where AsUTypeExt _ notes = AsUType notes {-# COMPLETE AsUTypeExt #-} diff --git a/src/Michelson/Typed/Haskell/Compatibility.hs b/src/Michelson/Typed/Haskell/Compatibility.hs --- a/src/Michelson/Typed/Haskell/Compatibility.hs +++ b/src/Michelson/Typed/Haskell/Compatibility.hs @@ -36,5 +36,18 @@ -- | Comb layout in LIGO (@ [\@layout:comb] @). -- -- To be used with 'customGeneric'. +-- +-- Note: to make comb layout work for sum types, make sure that in LIGO +-- all the constructors are preceded by the bar symbol in your type declaration: +-- +-- @ +-- type my_type = +-- [@layout:comb] +-- | Ctor1 of nat ← bar symbol _must_ be here +-- | Ctor2 of int +-- ... +-- @ +-- +-- Though the situation may change: https://gitlab.com/ligolang/ligo/-/issues/1104. ligoCombLayout :: GenericStrategy ligoCombLayout = rightComb diff --git a/src/Michelson/Typed/Haskell/Doc.hs b/src/Michelson/Typed/Haskell/Doc.hs --- a/src/Michelson/Typed/Haskell/Doc.hs +++ b/src/Michelson/Typed/Haskell/Doc.hs @@ -50,7 +50,6 @@ import Control.Lens (_Just, each, to) import Data.Char (isLower, isUpper, toLower) -import qualified Data.Kind as Kind import Data.List (lookup) import Data.Singletons (SingI, demote) import qualified Data.Text as T @@ -245,7 +244,7 @@ -- -- For implementation of the check see 'FieldDescriptionsValid' type family. type TypeDocFieldDescriptions a :: FieldDescriptions - type TypeDocFieldDescriptions a = '[] + type TypeDocFieldDescriptions _ = '[] -- | Final michelson representation of a type. -- @@ -369,12 +368,12 @@ mdTocFromRef lvl (build $ typeDocName ap') d -- | Create a 'DType' in form suitable for putting to 'typeDocDependencies'. -dTypeDep :: forall (t :: Kind.Type). TypeHasDoc t => SomeDocDefinitionItem +dTypeDep :: forall (t :: Type). TypeHasDoc t => SomeDocDefinitionItem dTypeDep = SomeDocDefinitionItem (DType (Proxy @t)) -- | Proxy version of 'dTypeDep'. dTypeDepP - :: forall (t :: Kind.Type). + :: forall (t :: Type). TypeHasDoc t => Proxy t -> SomeDocDefinitionItem dTypeDepP _ = dTypeDep @t @@ -437,7 +436,7 @@ -- | Derive 'typeDocMdReference', for homomorphic types only. homomorphicTypeDocMdReference - :: forall (t :: Kind.Type). + :: forall (t :: Type). (Typeable t, TypeHasDoc t, IsHomomorphic t) => Proxy t -> WithinParens -> Markdown homomorphicTypeDocMdReference tp _ = @@ -449,7 +448,7 @@ -- | Derive 'typeDocMdReference', for polymorphic type with one -- type argument, like @Maybe Integer@. poly1TypeDocMdReference - :: forall t (r :: Kind.Type) (a :: Kind.Type). + :: forall t (r :: Type) (a :: Type). (r ~ t a, Typeable t, Each '[TypeHasDoc] [r, a], IsHomomorphic t) => Proxy r -> WithinParens -> Markdown poly1TypeDocMdReference tp = @@ -460,7 +459,7 @@ -- | Derive 'typeDocMdReference', for polymorphic type with two -- type arguments, like @Lambda Integer Natural@. poly2TypeDocMdReference - :: forall t (r :: Kind.Type) (a :: Kind.Type) (b :: Kind.Type). + :: forall t (r :: Type) (a :: Type) (b :: Type). (r ~ t a b, Typeable t, Each '[TypeHasDoc] [r, a, b], IsHomomorphic t) => Proxy r -> WithinParens -> Markdown poly2TypeDocMdReference tp = @@ -600,7 +599,7 @@ ) -- | Generic traversal for automatic deriving of some methods in 'TypeHasDoc'. -class GTypeHasDoc (x :: Kind.Type -> Kind.Type) where +class GTypeHasDoc (x :: Type -> Type) where gTypeDocHaskellRep :: FieldDescriptionsV -> ADTRep SomeTypeWithDoc instance GTypeHasDoc x => GTypeHasDoc (G.D1 ('G.MetaData _a _b _c 'False) x) where @@ -627,7 +626,7 @@ gTypeDocHaskellRep _ = [] -- | Product type traversal for 'TypeHasDoc'. -class GProductHasDoc (x :: Kind.Type -> Kind.Type) where +class GProductHasDoc (x :: Type -> Type) where gProductDocHaskellRep :: [(Text, Text)] -> [FieldRep SomeTypeWithDoc] instance (GProductHasDoc x, GProductHasDoc y) => GProductHasDoc (x :*: y) where diff --git a/src/Michelson/Typed/Haskell/Instr/Product.hs b/src/Michelson/Typed/Haskell/Instr/Product.hs --- a/src/Michelson/Typed/Haskell/Instr/Product.hs +++ b/src/Michelson/Typed/Haskell/Instr/Product.hs @@ -24,12 +24,11 @@ , CastFieldConstructors (..) ) where -import qualified Data.Kind as Kind import Data.Vinyl.Core (Rec(..)) import GHC.Generics ((:*:)(..), (:+:)(..)) import qualified GHC.Generics as G import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError) -import Named ((:!), (:?), NamedF(..)) +import Named (NamedF(..), (:!), (:?)) import Michelson.Text import Michelson.Typed.Haskell.Instr.Helpers @@ -44,7 +43,7 @@ -- | Result of field lookup - its type and path to it in -- the tree. -data LookupNamedResult = LNR Kind.Type Path +data LookupNamedResult = LNR Type Path type family LnrFieldType (lnr :: LookupNamedResult) where LnrFieldType ('LNR f _) = f @@ -60,7 +59,7 @@ -- | Force result of 'GLookupNamed' to be 'Just' type family LNRequireFound (name :: Symbol) - (a :: Kind.Type) + (a :: Type) (mf :: Maybe LookupNamedResult) :: LookupNamedResult where LNRequireFound _ _ ('Just lnr) = lnr @@ -68,7 +67,7 @@ ('Text "Datatype " ':<>: 'ShowType a ':<>: 'Text " has no field " ':<>: 'ShowType name) -type family GLookupNamed (name :: Symbol) (x :: Kind.Type -> Kind.Type) +type family GLookupNamed (name :: Symbol) (x :: Type -> Type) :: Maybe LookupNamedResult where GLookupNamed name (G.D1 _ x) = GLookupNamed name x GLookupNamed name (G.C1 _ x) = GLookupNamed name x @@ -143,9 +142,9 @@ class GIsoValue x => GInstrGet (name :: Symbol) - (x :: Kind.Type -> Kind.Type) + (x :: Type -> Type) (path :: Path) - (fieldTy :: Kind.Type) where + (fieldTy :: Type) where gInstrGetField :: GIsoValue x => Instr (GValueType x ': s) (ToT fieldTy ': s) @@ -214,9 +213,9 @@ class GIsoValue x => GInstrSetField (name :: Symbol) - (x :: Kind.Type -> Kind.Type) + (x :: Type -> Type) (path :: Path) - (fieldTy :: Kind.Type) where + (fieldTy :: Type) where gInstrSetField :: Instr (ToT fieldTy ': GValueType x ': s) (GValueType x ': s) @@ -250,7 +249,7 @@ ---------------------------------------------------------------------------- -- | Way to construct one of the fields in a complex datatype. -newtype FieldConstructor (st :: [k]) (field :: Kind.Type) = +newtype FieldConstructor (st :: [k]) (field :: Type) = FieldConstructor (Instr (ToTs' st) (ToT field ': ToTs' st)) -- | Ability to pass list of fields with the same ToTs. @@ -305,8 +304,8 @@ GFieldNames G.V1 = TypeError ('Text "Must be at least one constructor") -- | Generic traversal for 'instrConstruct'. -class GIsoValue x => GInstrConstruct (x :: Kind.Type -> Kind.Type) where - type GFieldTypes x :: [Kind.Type] +class GIsoValue x => GInstrConstruct (x :: Type -> Type) where + type GFieldTypes x :: [Type] gInstrConstruct :: Rec (FieldConstructor st) (GFieldTypes x) -> Instr st (GValueType x ': st) gInstrConstructStack :: Instr (ToTs (GFieldTypes x)) '[GValueType x] @@ -344,6 +343,12 @@ gInstrConstruct = error "impossible" gInstrConstructStack = error "impossible" +instance ( TypeError ('Text "Cannot construct void-like type") + ) => GInstrConstruct G.V1 where + type GFieldTypes G.V1 = '[] + gInstrConstruct = error "impossible" + gInstrConstructStack = error "impossible" + instance IsoValue a => GInstrConstruct (G.Rec0 a) where type GFieldTypes (G.Rec0 a) = '[a] gInstrConstruct (FieldConstructor i :& RNil) = i @@ -387,7 +392,7 @@ instrDeconstruct = FrameInstr (Proxy @st) $ gInstrDeconstruct @(G.Rep dt) -- | Generic traversal for 'instrDeconstruct'. -class GIsoValue x => GInstrDeconstruct (x :: Kind.Type -> Kind.Type) where +class GIsoValue x => GInstrDeconstruct (x :: Type -> Type) where gInstrDeconstruct :: Instr '[GValueType x] (ToTs (GFieldTypes x)) instance GInstrDeconstruct x => GInstrDeconstruct (G.M1 t i x) where @@ -409,6 +414,10 @@ instance ( TypeError ('Text "Cannot deconstruct sum type") , GIsoValue x, GIsoValue y ) => GInstrDeconstruct (x :+: y) where + gInstrDeconstruct = error "impossible" + +instance ( TypeError ('Text "Cannot deconstruct void-like type") + ) => GInstrDeconstruct G.V1 where gInstrDeconstruct = error "impossible" instance IsoValue a => GInstrDeconstruct (G.Rec0 a) where diff --git a/src/Michelson/Typed/Haskell/Instr/Sum.hs b/src/Michelson/Typed/Haskell/Instr/Sum.hs --- a/src/Michelson/Typed/Haskell/Instr/Sum.hs +++ b/src/Michelson/Typed/Haskell/Instr/Sum.hs @@ -40,14 +40,13 @@ , IsPrimitiveValue ) where -import qualified Data.Kind as Kind import Data.Singletons (SingI(..)) import Data.Type.Bool (type (||)) import Data.Vinyl.Core (Rec(..)) import GHC.Generics ((:*:)(..), (:+:)(..)) import qualified GHC.Generics as G import GHC.TypeLits (AppendSymbol, ErrorMessage(..), Symbol, TypeError) -import Named ((:!), NamedF) +import Named (NamedF, (:!)) import Type.Reflection ((:~:)(Refl)) import Unsafe.Coerce (unsafeCoerce) @@ -73,7 +72,7 @@ -- we can't even assign names to fields if there are many (the style -- guide prohibits partial records). data CtorField - = OneField Kind.Type + = OneField Type | NoFields -- | Get /something/ as field of the given constructor. @@ -84,13 +83,13 @@ -- | Push field to stack, if any. type family AppendCtorField (cf :: CtorField) (l :: [k]) :: [k] where AppendCtorField ('OneField t) (l :: [T]) = ToT t ': l - AppendCtorField ('OneField t) (l :: [Kind.Type]) = t ': l + AppendCtorField ('OneField t) (l :: [Type]) = t ': l AppendCtorField 'NoFields (l :: [T]) = l - AppendCtorField 'NoFields (l :: [Kind.Type]) = l + AppendCtorField 'NoFields (l :: [Type]) = l -- | To use 'AppendCtorField' not only here for 'T'-based stacks, but also --- later in Lorentz with 'Kind.Type'-based stacks we need the following property. -type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Kind.Type]) = +-- later in Lorentz with 'Type'-based stacks we need the following property. +type AppendCtorFieldAxiom (cf :: CtorField) (st :: [Type]) = ToTs (AppendCtorField cf st) ~ AppendCtorField cf (ToTs st) -- | Proof of 'AppendCtorFieldAxiom'. @@ -126,7 +125,7 @@ -- | Force result of 'GLookupNamed' to be 'Just' type family LNRequireFound (name :: Symbol) - (a :: Kind.Type) + (a :: Type) (mf :: Maybe LookupNamedResult) :: LookupNamedResult where LNRequireFound _ _ ('Just lnr) = lnr @@ -134,7 +133,7 @@ ('Text "Datatype " ':<>: 'ShowType a ':<>: 'Text " has no (sub)constructor " ':<>: 'ShowType name) -type family GLookupNamed (name :: Symbol) (x :: Kind.Type -> Kind.Type) +type family GLookupNamed (name :: Symbol) (x :: Type -> Type) :: Maybe LookupNamedResult where GLookupNamed name (G.D1 _ x) = GLookupNamed name x GLookupNamed name (G.C1 ('G.MetaCons ctorName _ _) x) = @@ -173,7 +172,7 @@ -- and which is not a primitive type. We do not go deeper when we -- encounter a product type here, because it means that there are multiple -- fields inside one constructor (it is not supported). -type family GCanGoDeeper (x :: Kind.Type -> Kind.Type) :: Bool where +type family GCanGoDeeper (x :: Type -> Type) :: Bool where GCanGoDeeper (_ :+: _) = 'True GCanGoDeeper (G.D1 _ x) = GCanGoDeeper x GCanGoDeeper (G.S1 _ (G.Rec0 x)) = CanGoDeeper x @@ -185,7 +184,7 @@ ('Text "GCanGoDeeper encountered unexpected pattern: " ':<>: 'ShowType x) -- | Whether given type represents an atomic Michelson value. -type family IsPrimitiveValue (x :: Kind.Type) :: Bool where +type family IsPrimitiveValue (x :: Type) :: Bool where IsPrimitiveValue (Maybe _) = 'True IsPrimitiveValue (NamedF _ _ _) = 'True IsPrimitiveValue Integer = 'True @@ -212,12 +211,12 @@ -- Some types don't have Generic instances (e. g. primitives like Integer), so -- we need another type family to handle them. -type CanGoDeeper (x :: Kind.Type) = +type CanGoDeeper (x :: Type) = If (IsPrimitiveValue x) 'False (GCanGoDeeper (G.Rep x)) -type family GLookupNamedDeeper (name :: Symbol) (x :: Kind.Type -> Kind.Type) +type family GLookupNamedDeeper (name :: Symbol) (x :: Type -> Type) :: Maybe LookupNamedResult where GLookupNamedDeeper name (G.S1 _ (G.Rec0 y)) = GLookupNamed name (G.Rep y) GLookupNamedDeeper name _ = TypeError @@ -238,7 +237,7 @@ LNMergeFound name ('Just _) ('Just _) = TypeError ('Text "Ambiguous reference to datatype constructor: " ':<>: 'ShowType name) -type family GExtractFields (x :: Kind.Type -> Kind.Type) +type family GExtractFields (x :: Type -> Type) :: CtorField where GExtractFields (G.S1 _ x) = GExtractFields x GExtractFields (G.Rec0 a) = 'OneField a @@ -260,7 +259,7 @@ type CtorHasOnlyField ctor dt f = GetCtorField dt ctor ~ 'OneField f -type family RequireOneField (ctor :: Symbol) (cf :: CtorField) :: Kind.Type where +type family RequireOneField (ctor :: Symbol) (cf :: CtorField) :: Type where RequireOneField _ ('OneField f) = f RequireOneField ctor 'NoFields = TypeError ('Text "Expected exactly one field" ':$$: @@ -331,7 +330,7 @@ -- | Generic traversal for 'instrWrap'. class GIsoValue x => GInstrWrap - (x :: Kind.Type -> Kind.Type) + (x :: Type -> Type) (path :: Path) (entryTy :: CtorField) where gInstrWrap @@ -522,7 +521,7 @@ type CaseClauses a = GCaseClauses (G.Rep a) -- | Generic traversal for 'instrWrap'. -class GIsoValue x => GInstrCase (x :: Kind.Type -> Kind.Type) where +class GIsoValue x => GInstrCase (x :: Type -> Type) where type GCaseClauses x :: [CaseClauseParam] @@ -541,13 +540,17 @@ let (leftClauses, rightClauses) = rsplit clauses in rfMerge IF_LEFT (gInstrCase @x leftClauses) (gInstrCase @y rightClauses) +instance GInstrCase G.V1 where + type GCaseClauses G.V1 = '[] + gInstrCase RNil = RfAlwaysFails NEVER + instance GInstrCaseBranch ctor x => GInstrCase (G.C1 ('G.MetaCons ctor _1 _2) x) where type GCaseClauses (G.C1 ('G.MetaCons ctor _1 _2) x) = '[GCaseBranchInput ctor x] gInstrCase (clause :& RNil) = gInstrCaseBranch @ctor @x clause -- | Traverse a single contructor and supply its field to instruction in case clause. class GIsoValue x => - GInstrCaseBranch (ctor :: Symbol) (x :: Kind.Type -> Kind.Type) where + GInstrCaseBranch (ctor :: Symbol) (x :: Type -> Type) where type GCaseBranchInput ctor x :: CaseClauseParam @@ -645,9 +648,9 @@ class GIsoValue x => GInstrUnwrap - (x :: Kind.Type -> Kind.Type) + (x :: Type -> Type) (path :: Path) - (entryTy :: Kind.Type) where + (entryTy :: Type) where gInstrUnwrapUnsafe :: GIsoValue x => Instr (GValueType x ': s) (ToT entryTy ': s) diff --git a/src/Michelson/Typed/Haskell/LooseSum.hs b/src/Michelson/Typed/Haskell/LooseSum.hs --- a/src/Michelson/Typed/Haskell/LooseSum.hs +++ b/src/Michelson/Typed/Haskell/LooseSum.hs @@ -19,7 +19,6 @@ , LooseSumC ) where -import qualified Data.Kind as Kind import Data.Typeable (TypeRep, cast, typeRep) import GHC.Generics ((:*:), (:+:)) import qualified GHC.Generics as G @@ -68,7 +67,7 @@ fromTaggedVal = fmap G.to . gFromTaggedVal -- | Generic traversal for 'toTaggedVal' and 'fromTaggedVal'. -class GLooseSum (x :: Kind.Type -> Kind.Type) where +class GLooseSum (x :: Type -> Type) where gToTaggedVal :: x p -> (Text, SomeValue) gFromTaggedVal :: (Text, SomeValue) -> ComposeResult (x p) @@ -97,7 +96,7 @@ gFromTaggedVal _ = mempty -- | Pick a field from constructor with zero or one fields. -class GAccessField (x :: Kind.Type -> Kind.Type) where +class GAccessField (x :: Type -> Type) where gExtractField :: x p -> SomeValue gMakeField :: SomeValue -> ComposeResult (x p) diff --git a/src/Michelson/Typed/Haskell/ValidateDescription.hs b/src/Michelson/Typed/Haskell/ValidateDescription.hs --- a/src/Michelson/Typed/Haskell/ValidateDescription.hs +++ b/src/Michelson/Typed/Haskell/ValidateDescription.hs @@ -9,7 +9,6 @@ , FieldDescriptionsValid ) where -import qualified Data.Kind as Kind import Data.Singletons (Demote) import Data.Type.Bool import qualified GHC.Generics as G @@ -54,7 +53,7 @@ -- -- When @descr@ is not empty, this family will demand 'G.Generic' instance for @typ@ and fail with a -- 'TypeError' if there none. -type family FieldDescriptionsValid (descr :: FieldDescriptions) (typ :: Kind.Type) :: Kind.Constraint where +type family FieldDescriptionsValid (descr :: FieldDescriptions) (typ :: Type) :: Constraint where FieldDescriptionsValid '[] _ = () FieldDescriptionsValid descr typ = Assert @@ -66,7 +65,7 @@ (FieldDescriptionsValidImpl descr typ) -- | Actual recursive implementation for 'FieldDescriptionsValid'. -type family FieldDescriptionsValidImpl (descr :: FieldDescriptions) (typ :: Kind.Type) :: Kind.Constraint where +type family FieldDescriptionsValidImpl (descr :: FieldDescriptions) (typ :: Type) :: Constraint where FieldDescriptionsValidImpl '[] _ = () FieldDescriptionsValidImpl ( '(conName, '(_, fields)) ': rest ) typ = ( HasAllFields conName fields typ @@ -74,7 +73,7 @@ ) -- | Check whether given constructor name @conName@ is present in 'G.Rep' of a datatype. -type family HasConstructor (conName :: Symbol) (g :: Kind.Type -> Kind.Type) :: Bool where +type family HasConstructor (conName :: Symbol) (g :: Type -> Type) :: Bool where HasConstructor conName (G.D1 _ cs) = HasConstructor conName cs HasConstructor conName (G.C1 ('G.MetaCons conName _ _) _) = 'True HasConstructor conName (l G.:+: r) = HasConstructor conName l || HasConstructor conName r @@ -84,7 +83,7 @@ -- -- This family also checks whether the constructor is present and fails with a 'TypeError' -- otherwise. -type family HasAllFields (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Kind.Type) :: Kind.Constraint where +type family HasAllFields (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Type) :: Constraint where HasAllFields conName fields typ = If (HasConstructor conName (G.Rep typ)) @@ -94,12 +93,12 @@ ) -- | Actual recursive implementation of 'HasAllFields'. -type family HasAllFieldsImpl (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Kind.Type) :: Kind.Constraint where +type family HasAllFieldsImpl (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Type) :: Constraint where HasAllFieldsImpl _ '[] _ = () HasAllFieldsImpl conName ( '(fieldName, _) ': rest ) typ = ( If (HasField conName fieldName (G.Rep typ)) - (() :: Kind.Constraint) + (() :: Constraint) (TypeError ('Text "No field " ':<>: 'ShowType fieldName ':<>: 'Text " in constructor " ':<>: 'ShowType conName ':<>: 'Text " of type " ':<>: 'ShowType typ ':<>: 'Text "." @@ -109,14 +108,14 @@ ) -- | Check that Generic 'G.Rep' has given field @fieldName@ in a given constructor @conName@. -type family HasField (conName :: Symbol) (fieldName :: Symbol) (g :: Kind.Type -> Kind.Type) :: Bool where +type family HasField (conName :: Symbol) (fieldName :: Symbol) (g :: Type -> Type) :: Bool where HasField conName fieldName (G.D1 _ cs) = HasField conName fieldName cs HasField conName fieldName (G.C1 ('G.MetaCons conName _ _) c) = ConHasField fieldName c HasField conName fieldName (l G.:+: r) = HasField conName fieldName l || HasField conName fieldName r HasField _ _ _ = 'False -- | Check that Generic representation for a constructor has given field @fieldName@. -type family ConHasField (fieldName :: Symbol) (g :: Kind.Type -> Kind.Type) :: Bool where +type family ConHasField (fieldName :: Symbol) (g :: Type -> Type) :: Bool where ConHasField fieldName (G.S1 ('G.MetaSel ('Just fieldName) _ _ _) _) = 'True ConHasField fieldName (l G.:*: r) = ConHasField fieldName l || ConHasField fieldName r ConHasField _ _ = 'False @@ -130,6 +129,6 @@ data T1 a -type family Assert (err :: Constraint) (break :: Kind.Type -> Kind.Type) (v :: k) :: k where +type family Assert (err :: Constraint) (break :: Type -> Type) (v :: k) :: k where Assert _ T1 _ = Any Assert _ _ k = k diff --git a/src/Michelson/Typed/Haskell/Value.hs b/src/Michelson/Typed/Haskell/Value.hs --- a/src/Michelson/Typed/Haskell/Value.hs +++ b/src/Michelson/Typed/Haskell/Value.hs @@ -39,11 +39,11 @@ import Data.Constraint (Dict(..), (:-)(..)) import Data.Default (Default(..)) -import qualified Data.Kind as Kind import qualified Data.Map.Strict as Map import qualified Data.Set as Set import Data.Vinyl.Core (Rec(..)) -import Fmt (Buildable(..)) +import Fmt (Buildable(..), mapF) +import GHC.Exts (IsList) import GHC.Generics ((:*:)(..), (:+:)(..)) import qualified GHC.Generics as G import Named (NamedF(..)) @@ -91,7 +91,7 @@ -- | Overloaded version of 'ToT' to work on Haskell and @T@ types. type family ToT' (t :: k) :: T where ToT' (t :: T) = t - ToT' (t :: Kind.Type) = ToT t + ToT' (t :: Type) = ToT t -- | Hides some Haskell value put in line with Michelson 'Value'. data SomeIsoValue where @@ -259,7 +259,7 @@ -- If a contract has explicit default entrypoint (and no root entrypoint), -- @ContractRef@ referring to it can never have the entire parameter as its -- type argument. -data ContractRef (arg :: Kind.Type) = ContractRef +data ContractRef (arg :: Type) = ContractRef { crAddress :: Address , crEntrypoint :: SomeEntrypointCall arg } deriving stock (Eq, Show) @@ -281,8 +281,11 @@ newtype BigMap k v = BigMap { unBigMap :: Map k v } deriving stock (Eq, Show) - deriving newtype (Default, Semigroup, Monoid) + deriving newtype (Default, Semigroup, Monoid, One, Container, IsList) +instance (Ord k, Buildable k, Buildable v) => Buildable (BigMap k v) where + build = mapF + instance ( WellTypedToT k, WellTypedToT v, Comparable (ToT k) , Ord k, IsoValue k, IsoValue v @@ -306,7 +309,7 @@ -- In case an unbalanced tree is needed, the Generic instance can be derived by -- using the utilities in the 'Util.Generics' module. class KnownT (GValueType x) => - GIsoValue (x :: Kind.Type -> Kind.Type) where + GIsoValue (x :: Type -> Type) where type GValueType x :: T gToValue :: x p -> Value (GValueType x) gFromValue :: Value (GValueType x) -> x p @@ -354,17 +357,17 @@ ---------------------------------------------------------------------------- -- | Type function to convert a Haskell stack type to @T@-based one. -type family ToTs (ts :: [Kind.Type]) :: [T] where +type family ToTs (ts :: [Type]) :: [T] where ToTs '[] = '[] ToTs (x ': xs) = ToT x ': ToTs xs -- | Overloaded version of 'ToTs' to work on Haskell and @T@ stacks. type family ToTs' (t :: [k]) :: [T] where ToTs' (t :: [T]) = t - ToTs' (a :: [Kind.Type]) = ToTs a + ToTs' (a :: [Type]) = ToTs a -- | Isomorphism between Michelson stack and its Haskell reflection. -class IsoValuesStack (ts :: [Kind.Type]) where +class IsoValuesStack (ts :: [Type]) where toValStack :: Rec Identity ts -> Rec Value (ToTs ts) fromValStack :: Rec Value (ToTs ts) -> Rec Identity ts @@ -401,7 +404,7 @@ class (KnownT t, WellTypedSuperC t) => WellTyped (t :: T) where -- | Constraints required for instance of a given type. type WellTypedSuperC t :: Constraint - type WellTypedSuperC t = () + type WellTypedSuperC _ = () instance WellTyped 'TKey where instance WellTyped 'TUnit where diff --git a/src/Michelson/Typed/Instr.hs b/src/Michelson/Typed/Instr.hs --- a/src/Michelson/Typed/Instr.hs +++ b/src/Michelson/Typed/Instr.hs @@ -2,6 +2,8 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +{-# OPTIONS_GHC -Wno-orphans #-} + -- | Module, containing data types for Michelson value. module Michelson.Typed.Instr ( Instr (..) @@ -18,9 +20,10 @@ , mapEntriesOrdered , pattern CAR , pattern CDR + , pattern LEFT , pattern PAIR + , pattern RIGHT , pattern UNPAIR - , PackedNotes(..) , ConstraintDUPN , ConstraintDUPN' , ConstraintDIPN @@ -42,14 +45,14 @@ import Data.Default import Data.Singletons (Sing) -import Fmt (Buildable(..), (+||), (||+)) +import Data.Vinyl (RMap, Rec(..), RecordToList, ReifyConstraint(..)) +import Fmt ((+||), (||+)) import GHC.TypeNats (type (+)) import qualified GHC.TypeNats as GHC (Nat) import qualified Text.Show import Michelson.Doc import Michelson.ErrorPos -import Michelson.Printer.Util (RenderDoc(..), buildRenderDoc, needsParens, printDocS) import Michelson.Typed.Annotation (Notes(..), starNotes) import Michelson.Typed.Arith import Michelson.Typed.Entrypoints @@ -71,29 +74,9 @@ -- This next comment is needed to run the doctest examples throughout this module. -- $setup --- >>> :m +Michelson.Typed.T Util.Peano Data.Singletons +-- >>> :m +Michelson.Typed.T Util.Peano -- >>> :set -XPartialTypeSignatures --- | A wrapper to wrap annotations and corresponding singleton. --- Apart from packing notes along with the corresponding Singleton, --- this wrapper type, when included with `Instr` also helps to derive --- the `Show` instance for `Instr` as `Sing a` does not have a `Show` --- instance on its own. -data PackedNotes a where - PackedNotes :: SingI a => Notes a -> PackedNotes (a ': s) - -instance NFData (PackedNotes a) where - rnf (PackedNotes n) = rnf n - -instance Show (PackedNotes a) where - show = printDocS True . renderDoc needsParens - -instance Buildable (PackedNotes a) where - build = buildRenderDoc - -instance RenderDoc (PackedNotes a) where - renderDoc pn (PackedNotes n) = renderDoc pn n - -- | Constraint that is used in DUPN, we want to share it with -- typechecking code and eDSL code. type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) = @@ -262,16 +245,25 @@ -- TODO [#283]: replace this wrapper with something more clever and abstract. WithLoc :: InstrCallStack -> Instr a b -> Instr a b - -- | A wrapper for an instruction that also contains annotations for the - -- top type on the result stack. + -- | A wrapper for an instruction that also contains annotations for + -- some of top types on the result stack. -- -- As of now, when converting from untyped representation, - -- we only preserve field annotations and type annotations in 'PackedNotes'. + -- we only preserve field annotations and type annotations in 'Notes'. -- Variable annotations are preserved in 'InstrWithVarAnns'. -- -- This can wrap only instructions with at least one non-failing execution -- branch. - InstrWithNotes :: PackedNotes b -> Instr a b -> Instr a b + InstrWithNotes + :: forall a (topElems :: [T]) (s :: [T]). + ( RMap topElems + , RecordToList topElems + , ReifyConstraint Show Notes topElems + , ReifyConstraint NFData Notes topElems + , Each '[ SingI ] topElems + ) + => Proxy s -> Rec Notes topElems + -> Instr a (topElems ++ s) -> Instr a (topElems ++ s) -- | A wrapper for an instruction which produces variable annotations on the -- top stack element(s). See also: 'InstrWithVarAnns'. @@ -415,8 +407,8 @@ ConstraintUnpairN n pair => Sing n -> Instr (pair : s) (UnpairN n pair ++ s) - LEFT :: forall b a s . KnownT b => Instr (a ': s) ('TOr a b ': s) - RIGHT :: forall a b s . KnownT a => Instr (b ': s) ('TOr a b ': s) + AnnLEFT :: KnownT b => TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': s) ('TOr a b ': s) + AnnRIGHT :: KnownT a => TypeAnn -> FieldAnn -> FieldAnn -> Instr (b ': s) ('TOr a b ': s) IF_LEFT :: Instr (a ': s) s' -> Instr (b ': s) s' @@ -516,6 +508,11 @@ ConstraintUpdateN ix pair => Sing ix -> Instr (val : pair : s) (UpdateN ix val pair ': s) + GET_AND_UPDATE + :: ( GetOp c, UpdOp c, KnownT (GetOpVal c) + , UpdOpKey c ~ GetOpKey c + ) + => Instr (UpdOpKey c ': UpdOpParams c ': c ': s) ('TOption (GetOpVal c) : c ': s) IF :: Instr s s' -> Instr s s' -> Instr ('TBool ': s) s' @@ -686,6 +683,12 @@ pattern PAIR :: () => (i ~ (a ': b ': s), o ~ ('TPair a b ': s)) => Instr i o pattern PAIR = AnnPAIR (AnnotationUnsafe "") (AnnotationUnsafe "") (AnnotationUnsafe "") + +pattern LEFT :: () => (KnownT b, i ~ (a ': s), o ~ ('TOr a b ': s)) => Instr i o +pattern LEFT = AnnLEFT (AnnotationUnsafe "") (AnnotationUnsafe "") (AnnotationUnsafe "") + +pattern RIGHT :: () => (KnownT a, i ~ (b ': s), o ~ ('TOr a b ': s)) => Instr i o +pattern RIGHT = AnnRIGHT (AnnotationUnsafe "") (AnnotationUnsafe "") (AnnotationUnsafe "") data TestAssert (s :: [T]) where TestAssert diff --git a/src/Michelson/Typed/Scope.hs b/src/Michelson/Typed/Scope.hs --- a/src/Michelson/Typed/Scope.hs +++ b/src/Michelson/Typed/Scope.hs @@ -61,6 +61,7 @@ , BadTypeForScope (..) , CheckScope (..) + , WithDeMorganScope (..) -- * Implementation internals , HasNoBigMap @@ -101,7 +102,6 @@ ) where import Data.Constraint ((:-)(..), Dict(..), withDict, (\\)) -import qualified Data.Constraint as C import Data.Singletons (Sing, SingI(..)) import Data.Type.Bool (type (||)) import Fmt (Buildable(..)) @@ -580,28 +580,38 @@ BtHasNestedBigMap -> "has nested 'big_map'" BtHasContract -> "has 'contract' type" --- | Alias for constraints which Michelson applies to parameter. -type ParameterScope t = - (KnownT t, HasNoOp t, HasNoNestedBigMaps t) +-- | Set of constraints that Michelson applies to parameters. +-- +-- Not just a type alias in order to be able to partially apply it +class (KnownT t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t +instance (KnownT t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t --- | Alias for constraints which Michelson applies to contract storage. -type StorageScope t = - (KnownT t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) +-- | Set of constraints that Michelson applies to contract storage. +-- +-- Not just a type alias in order to be able to partially apply it +class (KnownT t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t +instance (KnownT t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t --- | Alias for constraints which Michelson applies to pushed constants. -type ConstantScope t = - (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t) +-- | Set of constraints that Michelson applies to pushed constants. +-- +-- Not just a type alias in order to be able to partially apply it +class (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t) => ConstantScope t +instance (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t) => ConstantScope t --- | Alias for constraints which Michelson applies to packed values. -type PackedValScope t = - (SingI t, HasNoOp t, HasNoBigMap t) +-- | Set of constraints that Michelson applies to packed values. +-- +-- Not just a type alias in order to be able to partially apply it +class (SingI t, HasNoOp t, HasNoBigMap t) => PackedValScope t +instance (SingI t, HasNoOp t, HasNoBigMap t) => PackedValScope t --- | Alias for constraints which Michelson applies to unpacked values. +-- | Set of constraints that Michelson applies to unpacked values. -- -- It is different from 'PackedValScope', e.g. @contract@ type cannot appear -- in a value we unpack to. -type UnpackedValScope t = - (PackedValScope t, ConstantScope t) +-- +-- Not just a type alias in order to be able to partially apply it +class (PackedValScope t, ConstantScope t) => UnpackedValScope t +instance (PackedValScope t, ConstantScope t) => UnpackedValScope t -- | Alias for constraints which are required for printing. type PrintedValScope t = (SingI t, HasNoOp t) @@ -656,6 +666,115 @@ <$> checkScope @(PackedValScope t) <*> checkScope @(ConstantScope t) +-- | Allows using a scope that can be proven true with a De Morgan law. +-- +-- Many scopes are defined as @not a@ (or rather @a ~ 'False@) where @a@ is a +-- negative property we want to avoid as a 'Constraint'. +-- The negative constraints are implemented with a type family that for some +-- combination types resolves to itself applied to the type arguments in an @or@, +-- e.g. A @pair l r@ has @x@ if @l@ or @r@ contain @x@. +-- +-- Because of the De Morgan laws @not (a or b)@ implies @(not a) and (not b)@ +-- or in our case: @pair@ does not contain @x@ -> @a@ and @b@ don't contain @x@. +-- +-- GHC is however not able to prove this, so we need to use another (impossible) +-- 'error' to forcefully "prove" one of the two scopes. +-- Funnily enough however GHC is able to prove that if one holds then the other +-- does too, so we don't actually have to prove both, see 'mkWithDeMorgan'. +class WithDeMorganScope (c :: T -> Constraint) t a b where + withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret + +-- | Helper to builds a 'WithDeMorganScope' by using a 'CheckScope' that we know +-- cannot fail. +-- +-- This can be used to make instances that also prove the other side of a +-- negative @or-like@ scope constraint, see 'WithDeMorganScope'. +mkWithDeMorgan + :: forall scope a ret. CheckScope (scope a) + => (scope a => ret) -> ret +mkWithDeMorgan f = fromRight (error "impossible") $ do + Dict <- checkScope @(scope a) + pure f + +instance SingI a => WithDeMorganScope HasNoOp 'TPair a b where + withDeMorganScope = mkWithDeMorgan @HasNoOp @a + +instance SingI a => WithDeMorganScope HasNoContract 'TPair a b where + withDeMorganScope = mkWithDeMorgan @HasNoContract @a + +instance SingI a => WithDeMorganScope HasNoBigMap 'TPair a b where + withDeMorganScope = mkWithDeMorgan @HasNoBigMap @a + +instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where + withDeMorganScope = mkWithDeMorgan @HasNoNestedBigMaps @a + +instance SingI a => WithDeMorganScope HasNoOp 'TOr a b where + withDeMorganScope = mkWithDeMorgan @HasNoOp @a + +instance SingI a => WithDeMorganScope HasNoContract 'TOr a b where + withDeMorganScope = mkWithDeMorgan @HasNoContract @a + +instance SingI a => WithDeMorganScope HasNoBigMap 'TOr a b where + withDeMorganScope = mkWithDeMorgan @HasNoBigMap @a + +instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where + withDeMorganScope = mkWithDeMorgan @HasNoNestedBigMaps @a + +instance SingI k => WithDeMorganScope HasNoOp 'TMap k v where + withDeMorganScope = mkWithDeMorgan @HasNoOp @k + +instance SingI k => WithDeMorganScope HasNoOp 'TBigMap k v where + withDeMorganScope = mkWithDeMorgan @HasNoOp @k + +instance + ( WithDeMorganScope HasNoOp t a b + , WithDeMorganScope HasNoNestedBigMaps t a b + , KnownT a, KnownT b + ) => WithDeMorganScope ParameterScope t a b where + withDeMorganScope f = + withDeMorganScope @HasNoOp @t @a @b $ + withDeMorganScope @HasNoNestedBigMaps @t @a @b f + +instance + ( WithDeMorganScope HasNoOp t a b + , WithDeMorganScope HasNoNestedBigMaps t a b + , WithDeMorganScope HasNoContract t a b + , KnownT a, KnownT b + ) => WithDeMorganScope StorageScope t a b where + withDeMorganScope f = + withDeMorganScope @HasNoOp @t @a @b $ + withDeMorganScope @HasNoNestedBigMaps @t @a @b $ + withDeMorganScope @HasNoContract @t @a @b f + +instance + ( WithDeMorganScope HasNoOp t a b + , WithDeMorganScope HasNoBigMap t a b + , WithDeMorganScope HasNoContract t a b + , KnownT a, KnownT b + ) => WithDeMorganScope ConstantScope t a b where + withDeMorganScope f = + withDeMorganScope @HasNoOp @t @a @b $ + withDeMorganScope @HasNoBigMap @t @a @b $ + withDeMorganScope @HasNoContract @t @a @b f + +instance + ( WithDeMorganScope HasNoOp t a b + , WithDeMorganScope HasNoBigMap t a b + , KnownT a, KnownT b + ) => WithDeMorganScope PackedValScope t a b where + withDeMorganScope f = + withDeMorganScope @HasNoOp @t @a @b $ + withDeMorganScope @HasNoBigMap @t @a @b f + +instance + ( WithDeMorganScope PackedValScope t a b + , WithDeMorganScope ConstantScope t a b + , KnownT a, KnownT b + ) => WithDeMorganScope UnpackedValScope t a b where + withDeMorganScope f = + withDeMorganScope @PackedValScope @t @a @b $ + withDeMorganScope @ConstantScope @t @a @b f + -- Versions for eDSL ---------------------------------------------------------------------------- @@ -704,7 +823,9 @@ \\ forbiddenBigMapEvi @t properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t -properUnpackedValEvi = properPackedValEvi @t C.*** properConstantEvi @t +properUnpackedValEvi = Sub $ + Dict \\ properPackedValEvi @t + \\ properConstantEvi @t properPrintedValEvi :: forall t. ProperPrintedValBetterErrors t :- PrintedValScope t properPrintedValEvi = Sub $ diff --git a/src/Michelson/Typed/Sing.hs b/src/Michelson/Typed/Sing.hs --- a/src/Michelson/Typed/Sing.hs +++ b/src/Michelson/Typed/Sing.hs @@ -19,7 +19,6 @@ , fromSingT ) where -import Data.Kind (Type) import Data.Singletons (Sing, SingI(..), SingKind(..), SomeSing(..)) import Michelson.Typed.T (T(..)) diff --git a/src/Michelson/Typed/T.hs b/src/Michelson/Typed/T.hs --- a/src/Michelson/Typed/T.hs +++ b/src/Michelson/Typed/T.hs @@ -48,8 +48,8 @@ instance NFData T -- | Converts from 'T' to 'Michelson.Type.Type'. -toUType :: T -> Un.Type -toUType t = Un.Type (convert t) Un.noAnn +toUType :: T -> Un.Ty +toUType t = Un.Ty (convert t) Un.noAnn where convert :: T -> Un.T convert TInt = Un.TInt @@ -71,7 +71,7 @@ convert TNever = Un.TNever convert (TOption a) = Un.TOption (toUType a) convert (TList a) = Un.TList (toUType a) - convert (TSet a) = Un.TSet $ Un.Type (Un.unwrapT $ toUType a) Un.noAnn + convert (TSet a) = Un.TSet $ Un.Ty (Un.unwrapT $ toUType a) Un.noAnn convert (TOperation) = Un.TOperation convert (TContract a) = Un.TContract (toUType a) convert (TPair a b) = @@ -81,9 +81,9 @@ convert (TLambda a b) = Un.TLambda (toUType a) (toUType b) convert (TMap a b) = - Un.TMap (Un.Type (Un.unwrapT $ toUType a) Un.noAnn) (toUType b) + Un.TMap (Un.Ty (Un.unwrapT $ toUType a) Un.noAnn) (toUType b) convert (TBigMap a b) = - Un.TBigMap (Un.Type (Un.unwrapT $ toUType a) Un.noAnn) (toUType b) + Un.TBigMap (Un.Ty (Un.unwrapT $ toUType a) Un.noAnn) (toUType b) instance Buildable T where build = build . toUType diff --git a/src/Michelson/Typed/Util.hs b/src/Michelson/Typed/Util.hs --- a/src/Michelson/Typed/Util.hs +++ b/src/Michelson/Typed/Util.hs @@ -23,10 +23,15 @@ , isStringValue , isBytesValue , allAtomicValues + + -- * Instruction generation + , PushableStorageSplit (..) + , splitPushableStorage ) where import Prelude hiding (Ordering(..)) +import Data.Constraint (Dict(..)) import Data.Default (Default(..)) import qualified Data.Foldable as F import qualified Data.Map as M @@ -36,6 +41,8 @@ import Michelson.Text (MText) import Michelson.Typed.Aliases import Michelson.Typed.Instr +import Michelson.Typed.Scope +import qualified Michelson.Typed.T as T import Michelson.Typed.Value -- | Options for 'dfsInstr'. @@ -92,7 +99,7 @@ case i of Seq i1 i2 -> recursion2 Seq i1 i2 WithLoc loc i1 -> recursion1 (WithLoc loc) i1 - InstrWithNotes notes i1 -> recursion1 (InstrWithNotes notes) i1 + InstrWithNotes p notes i1 -> recursion1 (InstrWithNotes p notes) i1 InstrWithVarNotes varNotes i1 -> recursion1 (InstrWithVarNotes varNotes) i1 InstrWithVarAnns varAnns i1 -> recursion1 (InstrWithVarAnns varAnns) i1 FrameInstr p i1 -> recursion1 (FrameInstr p) i1 @@ -163,8 +170,8 @@ AnnPAIR{} -> step i PAIRN{} -> step i UNPAIRN{} -> step i - LEFT{} -> step i - RIGHT{} -> step i + AnnLEFT{} -> step i + AnnRIGHT{} -> step i NIL{} -> step i CONS{} -> step i SIZE{} -> step i @@ -176,6 +183,7 @@ GETN{} -> step i UPDATE{} -> step i UPDATEN{} -> step i + GET_AND_UPDATE{} -> step i EXEC{} -> step i APPLY{} -> step i FAILWITH{} -> step i @@ -295,9 +303,9 @@ RfNormal i0 -> RfNormal (WithLoc loc i0) r -> r - InstrWithNotes pn i -> case go i of + InstrWithNotes p pn i -> case go i of RfNormal i0 -> - RfNormal (InstrWithNotes pn i0) + RfNormal (InstrWithNotes p pn i0) RfAlwaysFails i0 -> error $ "InstrWithNotes wraps always-failing instruction: " <> show i0 InstrWithVarNotes vn i -> case go i of @@ -350,8 +358,8 @@ i@AnnPAIR{} -> RfNormal i i@PAIRN{} -> RfNormal i i@UNPAIRN{} -> RfNormal i - i@LEFT{} -> RfNormal i - i@RIGHT{} -> RfNormal i + i@AnnLEFT{} -> RfNormal i + i@AnnRIGHT{} -> RfNormal i i@NIL{} -> RfNormal i i@CONS{} -> RfNormal i i@SIZE{} -> RfNormal i @@ -363,6 +371,7 @@ i@GETN{} -> RfNormal i i@UPDATE{} -> RfNormal i i@UPDATEN{} -> RfNormal i + i@GET_AND_UPDATE{} -> RfNormal i i@EXEC{} -> RfNormal i i@APPLY{} -> RfNormal i FAILWITH -> RfAlwaysFails FAILWITH @@ -589,3 +598,177 @@ allAtomicValues :: forall t a. (forall t'. Value t' -> Maybe a) -> Value t -> [a] allAtomicValues selector = dfsFoldValue (maybeToList . selector) + + +-------------------------------------------------------------------------------- +-- Instruction generation +-------------------------------------------------------------------------------- + +-- | Result of splitting a storage 'Value' of @st@ on the stack @s@. +-- +-- The idea behind this is to either: prove that the whole 'Value' can be put on +-- the stack without containing a single @big_map@ or to split it into: +-- a 'Value' containing its @big_map@s and an instruction to reconstruct the +-- storage. +-- +-- The main idea behind this is to create a large storage in Michelson code to +-- then create a contract using 'CREATE_CONTRACT'. +-- Note: a simpler solution would have been to replace @big_map@ 'Value's with +-- an 'EMPTY_BIG_MAP' followed by many 'UPDATE' to push its content, but sadly +-- a bug (tezos/tezos/1154) prevents this from being done. +data PushableStorageSplit s st where + -- | The type of the storage is fully constant. + ConstantStorage + :: ConstantScope st + => Value st + -> PushableStorageSplit s st + + -- | The type of the storage is not a constant, but its value does not contain + -- @big_map@s. E.g. A 'Right ()' value of type 'Either (BigMap k v) ()'. + PushableValueStorage + :: StorageScope st + => Instr s (st ': s) + -> PushableStorageSplit s st + + -- | The type of the storage and part of its value (here @bms@) contain one or + -- more @big_map@s. The instruction can take the non-pushable 'Value bms' and + -- reconstruct the original 'Value st' without using any 'EMPTY_BIG_MAP'. + PartlyPushableStorage + :: (StorageScope bms, StorageScope st) + => Value bms -> Instr (bms ': s) (st ': s) + -> PushableStorageSplit s st + +-- | Splits the given storage 'Value' into a 'PushableStorageSplit'. +-- +-- This is based off the fact that the only storages that cannot be directly +-- 'PUSH'ed are the ones that contain 'BigMap's. +-- See difference between 'StorageScope' and 'ConstantScope'. +-- +-- So what we do here is to create a 'Value' as small as possible with all the +-- @big_map@s in it (if any) and an 'Instr' that can use it to rebuild the original +-- storage 'Value'. +-- +-- Note: This is done this way to avoid using 'EMPTY_BIG_MAP' instructions, see +-- 'PushableStorageSplit' for motivation. +splitPushableStorage :: StorageScope t => Value t -> PushableStorageSplit s t +splitPushableStorage v = case v of + -- Atomic (except op and contract) + VKey{} -> ConstantStorage v + VUnit -> ConstantStorage v + VSignature{} -> ConstantStorage v + VChainId{} -> ConstantStorage v + VLam{} -> ConstantStorage v + VInt{} -> ConstantStorage v + VNat{} -> ConstantStorage v + VString{} -> ConstantStorage v + VBytes{} -> ConstantStorage v + VMutez{} -> ConstantStorage v + VBool{} -> ConstantStorage v + VKeyHash{} -> ConstantStorage v + VBls12381Fr{} -> ConstantStorage v + VBls12381G1{} -> ConstantStorage v + VBls12381G2{} -> ConstantStorage v + VTimestamp{} -> ConstantStorage v + VAddress{} -> ConstantStorage v + + -- Non-atomic + VOption (Nothing :: Maybe (Value tm)) -> case checkScope @(HasNoBigMap tm) of + Right Dict -> ConstantStorage $ VOption Nothing + Left _ -> PushableValueStorage $ NONE + VOption (Just jVal :: Maybe (Value tm)) -> case splitPushableStorage jVal of + ConstantStorage _ -> ConstantStorage . VOption $ Just jVal + PushableValueStorage instr -> PushableValueStorage $ instr `Seq` SOME + PartlyPushableStorage val instr -> PartlyPushableStorage val $ instr `Seq` SOME + + VList (vals :: [Value tl]) -> case checkScope @(HasNoBigMap tl) of + Right Dict -> ConstantStorage v + Left _ -> + -- Here we check that even tho the type contains big_maps, we actually + -- have big_maps in (one or more of) the values too. + let handleList + :: Instr s ('T.TList tl ': s) -> Value tl + -> Maybe (Instr s ('T.TList tl ': s)) + handleList instr ele = case splitPushableStorage ele of + ConstantStorage val -> + Just $ instr `Seq` PUSH val `Seq` CONS + PushableValueStorage eleInstr -> + Just $ instr `Seq` eleInstr `Seq` CONS + PartlyPushableStorage _ _ -> Nothing + in maybe (PartlyPushableStorage v Nop) PushableValueStorage $ + foldM handleList NIL vals + + VSet{} -> ConstantStorage v + + VPair (v1 :: Value t1, v2 :: Value t2) -> + withValueTypeSanity v1 $ withValueTypeSanity v2 $ + withDeMorganScope @StorageScope @'T.TPair @t1 @t2 $ + let handlePair + :: PushableStorageSplit s t2 + -> PushableStorageSplit (t2 ': s) t1 + -> PushableStorageSplit s ('T.TPair t1 t2) + handlePair psp2 psp1 = case (psp2, psp1) of + -- at least one side is a constant + (ConstantStorage _, ConstantStorage _) -> + ConstantStorage v + (ConstantStorage val2, _) -> + handlePair (PushableValueStorage $ PUSH val2) psp1 + (_, ConstantStorage val1) -> + handlePair psp2 (PushableValueStorage $ PUSH val1) + -- at least one side is a constant or has no big_map values + (PushableValueStorage instr2, PushableValueStorage instr1) -> + PushableValueStorage $ instr2 `Seq` instr1 `Seq` PAIR + (PushableValueStorage instr2, PartlyPushableStorage val1 instr1) -> + PartlyPushableStorage val1 $ DIP instr2 `Seq` instr1 `Seq` PAIR + (PartlyPushableStorage val2 instr2, PushableValueStorage instr1) -> + PartlyPushableStorage val2 $ instr2 `Seq` instr1 `Seq` PAIR + -- both sides contain a big_map + (PartlyPushableStorage val2 instr2, PartlyPushableStorage val1 instr1) -> + PartlyPushableStorage (VPair (val1, val2)) $ + UNPAIR `Seq` DIP instr2 `Seq` instr1 `Seq` PAIR + in handlePair (splitPushableStorage v2) (splitPushableStorage v1) + + VOr (Left orVal :: Either (Value t1) (Value t2)) -> + withValueTypeSanity orVal $ withDeMorganScope @StorageScope @'T.TOr @t1 @t2 $ + case splitPushableStorage orVal of + ConstantStorage val -> case checkScope @(HasNoBigMap t2) of + -- note: here we need to check for the opposite branch too + Right Dict -> ConstantStorage v + Left _ -> PushableValueStorage $ PUSH val `Seq` LEFT + PushableValueStorage instr -> PushableValueStorage $ instr `Seq` LEFT + PartlyPushableStorage val instr -> PartlyPushableStorage val $ instr `Seq` LEFT + VOr (Right orVal :: Either (Value t1) (Value t2)) -> + withValueTypeSanity orVal $ withDeMorganScope @StorageScope @'T.TOr @t1 @t2 $ + case splitPushableStorage orVal of + ConstantStorage val -> case checkScope @(HasNoBigMap t1) of + -- note: here we need to check for the opposite branch too + Right Dict -> ConstantStorage v + Left _ -> PushableValueStorage $ PUSH val `Seq` RIGHT + PushableValueStorage instr -> PushableValueStorage $ instr `Seq` RIGHT + PartlyPushableStorage val instr -> PartlyPushableStorage val $ instr `Seq` RIGHT + + VMap (vMap :: (Map (Value tk) (Value tv))) -> case checkScope @(ConstantScope tk) of + Left _ -> + -- NOTE: all keys for a map need to be comparable and (even tho it's + -- not a superclass) that means they have to be constants. + -- I (@pasqu4le) found no exception to this rule, perhaps it should be + -- enforced in the type system as well, but it may have more + -- downsides than it's worth accepting. + error "impossible: all map keys should be PUSHable" + Right Dict -> case checkScope @(HasNoBigMap tv) of + Right Dict -> ConstantStorage v + _ -> withDeMorganScope @HasNoOp @'T.TMap @tk @tv $ + -- Similarly as for lists, here we check that even tho the value type + -- contains a big_map, we actually have big_maps in (one or more of) them. + let handleMap + :: Instr s ('T.TMap tk tv ': s) -> (Value tk, Value tv) + -> Maybe (Instr s ('T.TMap tk tv ': s)) + handleMap instr (key, ele) = case splitPushableStorage (VOption $ Just ele) of + ConstantStorage val -> + Just $ instr `Seq` PUSH val `Seq` PUSH key `Seq` UPDATE + PushableValueStorage eleInstr -> + Just $ instr `Seq` eleInstr `Seq` PUSH key `Seq` UPDATE + PartlyPushableStorage _ _ -> Nothing + in maybe (PartlyPushableStorage v Nop) PushableValueStorage $ + foldM handleMap EMPTY_MAP $ M.toList vMap + + VBigMap _ -> PartlyPushableStorage v Nop diff --git a/src/Michelson/Typed/Value.hs b/src/Michelson/Typed/Value.hs --- a/src/Michelson/Typed/Value.hs +++ b/src/Michelson/Typed/Value.hs @@ -38,7 +38,6 @@ ) where import Data.Constraint (Dict(..), (\\)) -import qualified Data.Kind as Kind import Data.Singletons (Sing, SingI(..)) import Data.Type.Bool (type (&&)) import Fmt (Buildable(build), Builder, (+|), (|+)) @@ -144,7 +143,7 @@ -- | Wrapper over instruction which remembers whether this instruction -- always fails or not. -data RemFail (instr :: k -> k -> Kind.Type) (i :: k) (o :: k) where +data RemFail (instr :: k -> k -> Type) (i :: k) (o :: k) where RfNormal :: instr i o -> RemFail instr i o RfAlwaysFails :: (forall o'. instr i o') -> RemFail instr i o diff --git a/src/Michelson/Untyped/Annotation.hs b/src/Michelson/Untyped/Annotation.hs --- a/src/Michelson/Untyped/Annotation.hs +++ b/src/Michelson/Untyped/Annotation.hs @@ -32,7 +32,11 @@ -- * Creation and conversions , noAnn - , ann + , annQ + , varAnnQ + , fieldAnnQ + , typeAnnQ + , mkAnnotationUnsafe , mkAnnotation , specialVarAnns , specialFieldAnn @@ -43,7 +47,6 @@ , unifyPairFieldAnn , convergeVarAnns , ifAnnUnified - , disjoinVn , convAnn ) where @@ -51,7 +54,6 @@ import Data.Char (isAlpha, isAscii, isDigit, isNumber) import Data.Data (Data(..)) import Data.Default (Default(..)) -import qualified Data.Kind as Kind import qualified Data.Text as T import Data.Typeable (eqT, (:~:)(..)) import Fmt (Buildable(build)) @@ -59,6 +61,8 @@ import Language.Haskell.TH.Lift (deriveLift) import Text.PrettyPrint.Leijen.Text (Doc, hsep, textStrict, (<+>)) import qualified Text.Show +import qualified Language.Haskell.TH as TH +import qualified Language.Haskell.TH.Quote as TH import Michelson.Printer.Util (RenderDoc(..), buildRenderDoc, doesntNeedParens, printDocS) import Util.Aeson @@ -71,7 +75,6 @@ -- @%|@%%|%@|[@:%][_0-9a-zA-Z][_0-9a-zA-Z\.%@]* newtype Annotation tag = AnnotationUnsafe { unAnnotation :: Text } deriving stock (Eq, Data, Functor, Generic) - deriving newtype (IsString) instance NFData (Annotation tag) @@ -170,7 +173,7 @@ -- Rendering -------------------------------------------------------------------------------- -class Typeable (tag :: Kind.Type) => KnownAnnTag tag where +class Typeable (tag :: Type) => KnownAnnTag tag where annPrefix :: Text instance KnownAnnTag tag => Show (Annotation tag) where @@ -233,8 +236,8 @@ -- | Makes an `Annotation` from its textual value, prefix (%/@/:) excluded -- Throws an error if the given `Text` contains invalid characters -ann :: HasCallStack => Text -> Annotation a -ann = either error id . mkAnnotation +mkAnnotationUnsafe :: HasCallStack => Text -> Annotation a +mkAnnotationUnsafe = either error id . mkAnnotation -- | Makes an `Annotation` from its textual value, prefix (%/@/:) excluded -- Returns a `Text` error message if the given `Text` contains invalid characters @@ -251,6 +254,53 @@ maybe (Right $ AnnotationUnsafe text) (\c -> Left $ "Invalid character: '" <> one c <> "'") $ T.find (not . isValidAnnBodyChar) suffix +-- | +-- >>> :t [annQ|abc|] +-- ... +-- ... :: forall k (tag :: k). Annotation tag +annQ :: TH.QuasiQuoter +annQ = annQImpl Nothing + +-- | +-- >>> :t [typeAnnQ|abc|] +-- ... +-- ... :: TypeAnn +typeAnnQ :: TH.QuasiQuoter +typeAnnQ = annQImpl (Just [t|TypeAnn|]) + +-- | +-- >>> :t [fieldAnnQ|abc|] +-- ... +-- ... :: FieldAnn +fieldAnnQ :: TH.QuasiQuoter +fieldAnnQ = annQImpl (Just [t|FieldAnn|]) + +-- | +-- >>> :t [varAnnQ|abc|] +-- ... +-- ... :: VarAnn +varAnnQ :: TH.QuasiQuoter +varAnnQ = annQImpl (Just [t|VarAnn|]) + +annQImpl :: Maybe TH.TypeQ -> TH.QuasiQuoter +annQImpl annTypeMb = TH.QuasiQuoter + { + TH.quoteExp = \s -> + case (mkAnnotation $ toText @String s) of + Left err -> fail $ toString err + Right _ -> case annTypeMb of + Nothing -> [e| (AnnotationUnsafe s) |] + Just annType -> [e| (AnnotationUnsafe s :: $(annType)) |] + , TH.quotePat = \s -> + case (mkAnnotation $ toText @String s) of + Left err -> fail $ toString err + Right _ -> case annTypeMb of + Nothing -> [p| AnnotationUnsafe $(TH.litP $ TH.StringL s) |] + Just annType -> [p| (AnnotationUnsafe $(TH.litP $ TH.StringL s) :: $(annType)) |] + , TH.quoteType = \_ -> fail "Cannot use this QuasiQuoter at type position" + , TH.quoteDec = \_ -> fail "Cannot use this QuasiQuoter at declaration position" + } + -- | List of all the special Variable Annotations, only allowed in `CAR` and `CDR` -- instructions, prefix (@) excluded. -- These do not respect the rules of `isValidAnnStart` and `isValidAnnBodyChar`. @@ -282,8 +332,8 @@ instance Semigroup VarAnn where Annotation a <> Annotation b - | a == "" || b == "" = ann $ a <> b - | otherwise = ann $ a <> "." <> b + | a == "" || b == "" = AnnotationUnsafe $ a <> b + | otherwise = AnnotationUnsafe $ a <> "." <> b instance Monoid VarAnn where mempty = noAnn @@ -306,9 +356,9 @@ -- This function is used primarily for type-checking and attempts to imitate the -- reference implementation's observed behavior with annotations. unifyAnn :: Annotation tag -> Annotation tag -> Maybe (Annotation tag) -unifyAnn (Annotation ann1) (Annotation ann2) +unifyAnn a@(Annotation ann1) (Annotation ann2) | ann1 == "" || ann2 == "" = Just noAnn - | ann1 == ann2 = Just $ ann ann1 + | ann1 == ann2 = Just $ a | otherwise = Nothing -- | Given two field annotations where one of them is used in CAR or CDR, @@ -321,9 +371,9 @@ -- reference implementation's observed behavior with field annotations when CAR -- and CDR are used with pairs. unifyPairFieldAnn :: FieldAnn -> FieldAnn -> Maybe FieldAnn -unifyPairFieldAnn ann1 ann2 - | ann1 == "" || ann2 == "" = Just $ ann1 `orAnn` ann2 - | ann1 == ann2 = Just ann1 +unifyPairFieldAnn a1@(Annotation ann1) a2@(Annotation ann2) + | ann1 == "" || ann2 == "" = Just $ a1 `orAnn` a2 + | ann1 == ann2 = Just a1 | otherwise = Nothing -- | Keeps an annotation if and only if the two of them are equal and returns an @@ -336,15 +386,8 @@ ifAnnUnified :: Annotation tag -> Annotation tag -> Bool ifAnnUnified a1 a2 = isJust $ a1 `unifyAnn` a2 -disjoinVn :: VarAnn -> (VarAnn, VarAnn) -disjoinVn (Annotation a) = case T.findIndex (== '.') $ T.reverse a of - Just ((n - 1 -) -> pos) -> (ann $ T.take pos a, ann $ T.drop (pos + 1) a) - Nothing -> (noAnn, ann a) - where - n = T.length a - convAnn :: Annotation tag1 -> Annotation tag2 -convAnn (Annotation a) = ann a +convAnn (Annotation a) = AnnotationUnsafe a pattern WithAnn :: Annotation tag -> Annotation tag pattern WithAnn ann <- ann@(Annotation (toString -> _:_)) diff --git a/src/Michelson/Untyped/Contract.hs b/src/Michelson/Untyped/Contract.hs --- a/src/Michelson/Untyped/Contract.hs +++ b/src/Michelson/Untyped/Contract.hs @@ -25,7 +25,7 @@ import Michelson.Printer.Util (Prettier(..), RenderDoc(..), assertParensNotNeeded, buildRenderDoc, needsParens, renderOpsList) -import Michelson.Untyped.Type (ParameterType(..), Type(..)) +import Michelson.Untyped.Type (ParameterType(..), Ty(..)) import Util.Aeson -- | Top-level entries order of the contract. @@ -69,7 +69,7 @@ -- | Contract block, convenient when parsing data ContractBlock op = CBParam ParameterType - | CBStorage Type + | CBStorage Ty | CBCode [op] deriving stock (Eq, Show) @@ -101,7 +101,7 @@ where (paramPos, storagePos, codePos) = entriesOrderToInt entriesOrder -type Storage = Type +type Storage = Ty data Contract' op = Contract { contractParameter :: ParameterType , contractStorage :: Storage diff --git a/src/Michelson/Untyped/Entrypoints.hs b/src/Michelson/Untyped/Entrypoints.hs --- a/src/Michelson/Untyped/Entrypoints.hs +++ b/src/Michelson/Untyped/Entrypoints.hs @@ -98,8 +98,8 @@ -- | Turn entrypoint name into annotation for contract parameter declaration. epNameToParamAnn :: EpName -> FieldAnn epNameToParamAnn (EpNameUnsafe name) - | name == "" = ann "default" - | otherwise = ann name + | name == "" = [annQ|default|] + | otherwise = mkAnnotationUnsafe name data EpNameFromRefAnnError = InEpNameBadAnnotation FieldAnn @@ -133,7 +133,7 @@ -- | Turn entrypoint name into annotation used as reference to entrypoint. epNameToRefAnn :: EpName -> FieldAnn -epNameToRefAnn (EpNameUnsafe name) = ann name +epNameToRefAnn (EpNameUnsafe name) = mkAnnotationUnsafe name -- | Make a valid entrypoint name from an arbitrary text. This -- function prohibits explicit @default@ entrypoint name which is @@ -160,11 +160,11 @@ -- to the their parameter types. If there are duplicate entrypoints in the -- given Type then the duplicate entrypoints at a deeper nesting level will get -- overwritten with the ones that are on top. -mkEntrypointsMap :: ParameterType -> Map EpName Type +mkEntrypointsMap :: ParameterType -> Map EpName Ty mkEntrypointsMap (ParameterType ty rootAnn) = mkEntrypointsMapRec rootAnn ty -- | Version of 'mkEntrypointMaps' for plain untyped type. -mkEntrypointsMapRec :: FieldAnn -> Type -> Map EpName Type +mkEntrypointsMapRec :: FieldAnn -> Ty -> Map EpName Ty mkEntrypointsMapRec curRootAnn ty = accountRoot curRootAnn <> accountTree ty where @@ -172,7 +172,7 @@ Just rootEp <- pure $ epNameFromParamAnn rootAnn return (rootEp, ty) - accountTree (Type t _) = case t of + accountTree (Ty t _) = case t of -- We are only interested in `Or` branches to extract entrypoint -- annotations. TOr f1 f2 t1 t2 -> mkEntrypointsMapRec f1 t1 <> mkEntrypointsMapRec f2 t2 diff --git a/src/Michelson/Untyped/Ext.hs b/src/Michelson/Untyped/Ext.hs --- a/src/Michelson/Untyped/Ext.hs +++ b/src/Michelson/Untyped/Ext.hs @@ -80,7 +80,7 @@ -- | A type-variable or a type-constant data TyVar = VarID Var - | TyCon Type + | TyCon Ty deriving stock (Eq, Show, Data, Generic) instance NFData TyVar diff --git a/src/Michelson/Untyped/Instr.hs b/src/Michelson/Untyped/Instr.hs --- a/src/Michelson/Untyped/Instr.hs +++ b/src/Michelson/Untyped/Instr.hs @@ -31,7 +31,7 @@ (Annotation, FieldAnn, KnownAnnTag, TypeAnn, VarAnn, fullAnnSet, singleAnnSet) import Michelson.Untyped.Contract (Contract'(..)) import Michelson.Untyped.Ext (ExtInstrAbstract) -import Michelson.Untyped.Type (Type) +import Michelson.Untyped.Type (Ty) import Michelson.Untyped.Value (Value'(..)) import Tezos.Address (OperationHash(..)) import Util.Aeson @@ -115,9 +115,9 @@ | SWAP | DIG Word | DUG Word - | PUSH VarAnn Type (Value' op) + | PUSH VarAnn Ty (Value' op) | SOME TypeAnn VarAnn - | NONE TypeAnn VarAnn Type + | NONE TypeAnn VarAnn Ty | UNIT TypeAnn VarAnn | IF_NONE [op] [op] | PAIR TypeAnn VarAnn FieldAnn FieldAnn @@ -125,16 +125,16 @@ | UNPAIRN Word | CAR VarAnn FieldAnn | CDR VarAnn FieldAnn - | LEFT TypeAnn VarAnn FieldAnn FieldAnn Type - | RIGHT TypeAnn VarAnn FieldAnn FieldAnn Type + | LEFT TypeAnn VarAnn FieldAnn FieldAnn Ty + | RIGHT TypeAnn VarAnn FieldAnn FieldAnn Ty | IF_LEFT [op] [op] - | NIL TypeAnn VarAnn Type + | NIL TypeAnn VarAnn Ty | CONS VarAnn | IF_CONS [op] [op] | SIZE VarAnn - | EMPTY_SET TypeAnn VarAnn Type - | EMPTY_MAP TypeAnn VarAnn Type Type - | EMPTY_BIG_MAP TypeAnn VarAnn Type Type + | EMPTY_SET TypeAnn VarAnn Ty + | EMPTY_MAP TypeAnn VarAnn Ty Ty + | EMPTY_BIG_MAP TypeAnn VarAnn Ty Ty | MAP VarAnn [op] | ITER [op] | MEM VarAnn @@ -142,19 +142,20 @@ | GETN VarAnn Word | UPDATE VarAnn | UPDATEN VarAnn Word + | GET_AND_UPDATE VarAnn | IF [op] [op] | LOOP [op] | LOOP_LEFT [op] - | LAMBDA VarAnn Type Type [op] + | LAMBDA VarAnn Ty Ty [op] | EXEC VarAnn | APPLY VarAnn | DIP [op] | DIPN Word [op] | FAILWITH - | CAST VarAnn Type + | CAST VarAnn Ty | RENAME VarAnn | PACK VarAnn - | UNPACK TypeAnn VarAnn Type + | UNPACK TypeAnn VarAnn Ty | CONCAT VarAnn | SLICE VarAnn | ISNAT VarAnn @@ -179,7 +180,7 @@ | GE VarAnn | INT VarAnn | SELF VarAnn FieldAnn - | CONTRACT VarAnn FieldAnn Type + | CONTRACT VarAnn FieldAnn Ty | TRANSFER_TOKENS VarAnn | SET_DELEGATE VarAnn | CREATE_CONTRACT VarAnn VarAnn (Contract' op) @@ -262,6 +263,7 @@ GETN va n -> "GET" <+> renderAnnot va <+> text (show n) UPDATE va -> "UPDATE" <+> renderAnnot va UPDATEN va n -> "UPDATE" <+> renderAnnot va <+> text (show n) + GET_AND_UPDATE va -> "GET_AND_UPDATE" <+> renderAnnot va IF x y -> "IF" <+> nest 4 (renderOps x) <$$> spaces 3 <> nest 4 (renderOps y) LOOP s -> "LOOP" <+> nest 6 (renderOps s) LOOP_LEFT s -> "LOOP_LEFT" <+> nest 11 (renderOps s) @@ -327,8 +329,8 @@ SELF_ADDRESS va -> "SELF_ADDRESS" <+> renderAnnot va NEVER -> "NEVER" where - renderTy = renderDoc @Type needsParens - renderComp = renderDoc @Type needsParens + renderTy = renderDoc @Ty needsParens + renderComp = renderDoc @Ty needsParens renderOps = renderOpsList False renderAnnot :: KnownAnnTag tag => Annotation tag -> Doc diff --git a/src/Michelson/Untyped/OpSize.hs b/src/Michelson/Untyped/OpSize.hs --- a/src/Michelson/Untyped/OpSize.hs +++ b/src/Michelson/Untyped/OpSize.hs @@ -100,6 +100,7 @@ GETN va n -> annsOpSize va <> stackDepthOpSize n UPDATE va -> annsOpSize va UPDATEN va n -> annsOpSize va <> stackDepthOpSize n + GET_AND_UPDATE va -> annsOpSize va IF l r -> ifOpSize l r LOOP is -> expandedInstrsOpSize is LOOP_LEFT is -> expandedInstrsOpSize is @@ -206,11 +207,11 @@ seqOpSize = OpSize 4 eltOpSize (Elt k v) = OpSize 2 <> valueOpSize k <> valueOpSize v -typeOpSize :: Type -> OpSize +typeOpSize :: Ty -> OpSize typeOpSize = typeOpSize' [] -typeOpSize' :: [FieldAnn] -> Type -> OpSize -typeOpSize' anns (Type t ta) = +typeOpSize' :: [FieldAnn] -> Ty -> OpSize +typeOpSize' anns (Ty t ta) = tOpSize t <> annsOpSize ta anns tOpSize :: T -> OpSize @@ -245,8 +246,8 @@ TAddress -> mempty TNever -> mempty -innerOpSize :: Type -> OpSize -innerOpSize (Type _ a) = +innerOpSize :: Ty -> OpSize +innerOpSize (Ty _ a) = (OpSize 2) <> annsOpSize a -- | Accepts an arbitrary number of 'TypeAnn' 'FieldAnn' and/or 'VarAnn' that diff --git a/src/Michelson/Untyped/Type.hs b/src/Michelson/Untyped/Type.hs --- a/src/Michelson/Untyped/Type.hs +++ b/src/Michelson/Untyped/Type.hs @@ -5,7 +5,7 @@ -- | Michelson types represented in untyped model. module Michelson.Untyped.Type - ( Type (..) + ( Ty (..) , T (..) , ParameterType (..) , toption @@ -49,39 +49,40 @@ (AnnotationSet, FieldAnn, RootAnn, TypeAnn, VarAnn, emptyAnnSet, fullAnnSet, noAnn, singleAnnSet) import Util.Aeson --- Annotated type -data Type - = Type ~T TypeAnn +-- Annotated type. +-- We don't name it 'Type' to avoid conflicts with 'Data.Kind.Type'. +data Ty + = Ty ~T TypeAnn deriving stock (Eq, Show, Data, Generic) -unwrapT :: Type -> T -unwrapT (Type t _) = t +unwrapT :: Ty -> T +unwrapT (Ty t _) = t -instance NFData Type +instance NFData Ty -instance RenderDoc (Prettier Type) where +instance RenderDoc (Prettier Ty) where renderDoc pn (Prettier w) = case w of - (Type t ta) -> renderType t False pn (singleAnnSet ta) + (Ty t ta) -> renderType t False pn (singleAnnSet ta) -instance RenderDoc Type where - renderDoc pn (Type t ta) = renderType t True pn (singleAnnSet ta) +instance RenderDoc Ty where + renderDoc pn (Ty t ta) = renderType t True pn (singleAnnSet ta) instance RenderDoc T where renderDoc pn t = renderType t True pn emptyAnnSet -- | Since Babylon parameter type can have special root annotation. -data ParameterType = ParameterType Type RootAnn +data ParameterType = ParameterType Ty RootAnn deriving stock (Eq, Show, Data, Generic) instance NFData ParameterType instance RenderDoc (Prettier ParameterType) where renderDoc pn (Prettier w) = case w of - ParameterType (Type t ta) ra -> + ParameterType (Ty t ta) ra -> renderType t False pn (fullAnnSet [ta] [ra] []) instance RenderDoc ParameterType where - renderDoc pn (ParameterType (Type t ta) ra) = + renderDoc pn (ParameterType (Ty t ta) ra) = renderType t True pn (fullAnnSet [ta] [ra] []) -- Ordering between different kinds of annotations is not significant, @@ -125,58 +126,58 @@ TOperation -> wrapInParens pn $ "operation" :| [annDoc] TNever -> wrapInParens pn $ "never" :| [annDoc] - TOption (Type t1 ta1) -> + TOption (Ty t1 ta1) -> addParens pn $ "option" <+> annDoc <+> recRenderer t1 (singleAnnSet ta1) - TList (Type t1 ta1) -> + TList (Ty t1 ta1) -> addParens pn $ "list" <+> annDoc <+> recRenderer t1 (singleAnnSet ta1) - TSet (Type t1 ta1) -> + TSet (Ty t1 ta1) -> addParens pn $ "set" <+> annDoc <+> recRenderer t1 (singleAnnSet ta1) - TContract (Type t1 ta1) -> + TContract (Ty t1 ta1) -> addParens pn $ "contract" <+> annDoc <+> recRenderer t1 (singleAnnSet ta1) - TPair fa1 fa2 va1 va2 (Type t1 ta1) (Type t2 ta2) -> + TPair fa1 fa2 va1 va2 (Ty t1 ta1) (Ty t2 ta2) -> addParens pn $ "pair" <+> annDoc <+> renderBranches (recRenderer t1 $ fullAnnSet [ta1] [fa1] [va1]) (recRenderer t2 $ fullAnnSet [ta2] [fa2] [va2]) - TOr fa1 fa2 (Type t1 ta1) (Type t2 ta2) -> + TOr fa1 fa2 (Ty t1 ta1) (Ty t2 ta2) -> addParens pn $ "or" <+> annDoc <+> renderBranches (recRenderer t1 $ fullAnnSet [ta1] [fa1] []) (recRenderer t2 $ fullAnnSet [ta2] [fa2] []) - TLambda (Type t1 ta1) (Type t2 ta2) -> + TLambda (Ty t1 ta1) (Ty t2 ta2) -> addParens pn $ "lambda" <+> annDoc <+> renderBranches (recRenderer t1 $ singleAnnSet ta1) (recRenderer t2 $ singleAnnSet ta2) - TMap (Type t1 ta1) (Type t2 ta2) -> + TMap (Ty t1 ta1) (Ty t2 ta2) -> addParens pn $ "map" <+> annDoc <+> renderBranches (recRenderer t1 $ singleAnnSet ta1) (recRenderer t2 $ singleAnnSet ta2) - TBigMap (Type t1 ta1) (Type t2 ta2) -> + TBigMap (Ty t1 ta1) (Ty t2 ta2) -> addParens pn $ "big_map" <+> annDoc <+> renderBranches (recRenderer t1 $ singleAnnSet ta1) (recRenderer t2 $ singleAnnSet ta2) -instance Buildable Type where +instance Buildable Ty where build = buildRenderDoc instance Buildable ParameterType where @@ -188,16 +189,16 @@ | TUnit | TSignature | TChainId - | TOption Type - | TList Type - | TSet Type + | TOption Ty + | TList Ty + | TSet Ty | TOperation - | TContract Type - | TPair FieldAnn FieldAnn VarAnn VarAnn Type Type - | TOr FieldAnn FieldAnn Type Type - | TLambda Type Type - | TMap Type Type - | TBigMap Type Type + | TContract Ty + | TPair FieldAnn FieldAnn VarAnn VarAnn Ty Ty + | TOr FieldAnn FieldAnn Ty Ty + | TLambda Ty Ty + | TMap Ty Ty + | TBigMap Ty Ty | TInt | TNat | TString @@ -218,61 +219,61 @@ instance NFData T -toption :: Type -> T +toption :: Ty -> T toption t = TOption t -tpair :: Type -> Type -> T +tpair :: Ty -> Ty -> T tpair l r = TPair noAnn noAnn noAnn noAnn l r -tor :: Type -> Type -> T +tor :: Ty -> Ty -> T tor l r = TOr noAnn noAnn l r -tyint :: Type -tyint = Type TInt noAnn +tyint :: Ty +tyint = Ty TInt noAnn -tynat :: Type -tynat = Type TNat noAnn +tynat :: Ty +tynat = Ty TNat noAnn -tyunit :: Type -tyunit = Type TUnit noAnn +tyunit :: Ty +tyunit = Ty TUnit noAnn -tybool :: Type -tybool = Type TBool noAnn +tybool :: Ty +tybool = Ty TBool noAnn -typair :: Type -> Type -> Type -typair l r = Type (tpair l r) noAnn +typair :: Ty -> Ty -> Ty +typair l r = Ty (tpair l r) noAnn -tyor :: Type -> Type -> Type -tyor l r = Type (tor l r) noAnn +tyor :: Ty -> Ty -> Ty +tyor l r = Ty (tor l r) noAnn --- | For implicit account, which type its parameter seems to have +-- | For implicit account, which Ty its parameter seems to have -- from outside. -tyImplicitAccountParam :: Type -tyImplicitAccountParam = Type TUnit noAnn +tyImplicitAccountParam :: Ty +tyImplicitAccountParam = Ty TUnit noAnn -isAtomicType :: Type -> Bool -isAtomicType t@(Type _ tAnn) | tAnn == noAnn = +isAtomicType :: Ty -> Bool +isAtomicType t@(Ty _ tAnn) | tAnn == noAnn = isComparable t || isKey t || isUnit t || isSignature t || isOperation t isAtomicType _ = False -isKey :: Type -> Bool -isKey (Type TKey _) = True +isKey :: Ty -> Bool +isKey (Ty TKey _) = True isKey _ = False -isUnit :: Type -> Bool -isUnit (Type TUnit _) = True +isUnit :: Ty -> Bool +isUnit (Ty TUnit _) = True isUnit _ = False -isSignature :: Type -> Bool -isSignature (Type TSignature _) = True +isSignature :: Ty -> Bool +isSignature (Ty TSignature _) = True isSignature _ = False -isOperation :: Type -> Bool -isOperation (Type TOperation _) = True +isOperation :: Ty -> Bool +isOperation (Ty TOperation _) = True isOperation _ = False -isComparable :: Type -> Bool -isComparable (Type t _) = case t of +isComparable :: Ty -> Bool +isComparable (Ty t _) = case t of TInt -> True TNat -> True TString -> True @@ -284,49 +285,49 @@ TAddress -> True _ -> False -isMutez :: Type -> Bool -isMutez (Type TMutez _) = True +isMutez :: Ty -> Bool +isMutez (Ty TMutez _) = True isMutez _ = False -isTimestamp :: Type -> Bool -isTimestamp (Type TTimestamp _) = True +isTimestamp :: Ty -> Bool +isTimestamp (Ty TTimestamp _) = True isTimestamp _ = False -isKeyHash :: Type -> Bool -isKeyHash (Type TKeyHash _) = True +isKeyHash :: Ty -> Bool +isKeyHash (Ty TKeyHash _) = True isKeyHash _ = False -isBool :: Type -> Bool -isBool (Type TBool _) = True +isBool :: Ty -> Bool +isBool (Ty TBool _) = True isBool _ = False -isString :: Type -> Bool -isString (Type TString _) = True +isString :: Ty -> Bool +isString (Ty TString _) = True isString _ = False -isInteger :: Type -> Bool +isInteger :: Ty -> Bool isInteger a = isNat a || isInt a || isMutez a || isTimestamp a -isNat :: Type -> Bool -isNat (Type TNat _) = True +isNat :: Ty -> Bool +isNat (Ty TNat _) = True isNat _ = False -isInt :: Type -> Bool -isInt (Type TInt _) = True +isInt :: Ty -> Bool +isInt (Ty TInt _) = True isInt _ = False -isBytes :: Type -> Bool -isBytes (Type TBytes _) = True +isBytes :: Ty -> Bool +isBytes (Ty TBytes _) = True isBytes _ = False ---------------------------------------------------------------------------- -- TH derivations ---------------------------------------------------------------------------- -deriveJSON morleyAesonOptions ''Type +deriveJSON morleyAesonOptions ''Ty deriveJSON morleyAesonOptions ''T deriveJSON morleyAesonOptions ''ParameterType -deriveLift ''Type +deriveLift ''Ty deriveLift ''T deriveLift ''ParameterType diff --git a/src/Morley/Micheline/Class.hs b/src/Morley/Micheline/Class.hs --- a/src/Morley/Micheline/Class.hs +++ b/src/Morley/Micheline/Class.hs @@ -12,7 +12,7 @@ import qualified Data.ByteString.Lazy as LBS import Data.Sequence (fromList, (|>)) -import Data.Singletons (pattern FromSing, Sing, SingI, withSingI) +import Data.Singletons (Sing, SingI, SomeSing (..), toSing, withSingI) import Fmt (Buildable(..), pretty) import Michelson.Interpret.Pack (encodeValue', packCode', packNotedT', packT') @@ -40,20 +40,20 @@ toExpression = decodeExpression . packCode' instance ToExpression T where - toExpression (FromSing (ts :: Sing t)) = + toExpression t' | SomeSing (ts :: Sing t) <- toSing t' = decodeExpression $ withSingI ts $ (packT' @t) instance SingI t => ToExpression (Notes t) where toExpression = decodeExpression . packNotedT' -instance ToExpression Untyped.Type where +instance ToExpression Untyped.Ty where toExpression (AsUType notes) = toExpression notes instance (SingI t, HasNoOp t) => ToExpression (Value t) where toExpression = decodeExpression . encodeValue' instance ToExpression (Contract cp st) where - toExpression contract@Contract{..} = ExpressionSeq $ fromList $ mapEntriesOrdered contract + toExpression contract@Contract{} = ExpressionSeq $ fromList $ mapEntriesOrdered contract (\param -> ExpressionPrim $ MichelinePrimAp (MichelinePrimitive "parameter") (fromList [ addRootAnnToExpression (pnRootAnn param) $ @@ -114,7 +114,7 @@ first FromExpressionError . launchGet decodeContract . LBS.fromStrict . encodeExpression -instance FromExpression Untyped.Type where +instance FromExpression Untyped.Ty where fromExpression = first FromExpressionError . launchGet decodeType . @@ -123,7 +123,7 @@ instance FromExpression T where fromExpression = - second fromUType . fromExpression @Untyped.Type + second fromUType . fromExpression @Untyped.Ty -- Note: we should generalize this to work for any instruction, -- not just lambdas (i.e. instructions with one input and one output). diff --git a/src/Tezos/Core.hs b/src/Tezos/Core.hs --- a/src/Tezos/Core.hs +++ b/src/Tezos/Core.hs @@ -17,6 +17,7 @@ , subMutez , unsafeSubMutez , mulMutez + , unsafeMulMutez , divModMutez , divModMutezInt , mutezToInt64 @@ -163,6 +164,11 @@ where res = toInteger a * toInteger b {-# INLINE mulMutez #-} + +-- | Partial multiplication of 'Mutez' and an Natural number. +-- Should be used only if you're sure there'll be no overflow. +unsafeMulMutez :: Mutez -> Natural -> Mutez +unsafeMulMutez = fromMaybe (error "unsafeMulMutez: overflow") ... mulMutez -- | Euclidian division of two 'Mutez' values. divModMutez :: Mutez -> Mutez -> Maybe (Word64, Mutez) diff --git a/src/Util/CLI.hs b/src/Util/CLI.hs --- a/src/Util/CLI.hs +++ b/src/Util/CLI.hs @@ -27,7 +27,6 @@ , readerError ) where -import qualified Data.Kind as Kind import Data.Text.Manipulate (toSpinal) import Fmt (Buildable, pretty) import GHC.TypeLits (KnownSymbol, Symbol, symbolVal) @@ -167,7 +166,7 @@ -- This expects type-level name to be in camelCase as appropriate for Haskell -- and transforms the variable inside. namedParser :: - forall (a :: Kind.Type) (name :: Symbol). + forall (a :: Type) (name :: Symbol). (Buildable a, HasCLReader a, KnownSymbol name) => Maybe a -> String diff --git a/src/Util/CustomGeneric.hs b/src/Util/CustomGeneric.hs --- a/src/Util/CustomGeneric.hs +++ b/src/Util/CustomGeneric.hs @@ -35,6 +35,8 @@ , customGeneric' ) where +import Prelude hiding (Type) + import Control.Lens (traversed) import Generics.Deriving.TH (makeRep0Inline) import qualified GHC.Generics as G @@ -362,7 +364,7 @@ let cShapes = cNames <&> \(name, fNum, _) -> (name, fNum) cShapesSorted <- cReordering cShapes <&> map \(_fReorder, cShape) -> cShape treeDepths <- gsEvalDepths genStrategy cShapesSorted - weightedConstrs <- makeWeightedConstrs cReordering treeDepths cShapesSorted + weightedConstrs <- makeWeightedConstrs cReordering treeDepths cShapes -- If no 'Rep' type was given, derive one. let repType = diff --git a/src/Util/Fcf.hs b/src/Util/Fcf.hs --- a/src/Util/Fcf.hs +++ b/src/Util/Fcf.hs @@ -26,6 +26,6 @@ type instance Eval (TyEqSing a b) = DefaultEq a b data ApplyConstraints :: [a -> Constraint] -> a -> Exp Constraint -type instance Eval (ApplyConstraints '[] _) = () +type instance Eval (ApplyConstraints '[] _) = (() :: Constraint) type instance Eval (ApplyConstraints (c ': cs) a) = (c a, Eval (ApplyConstraints cs a)) diff --git a/src/Util/Generic.hs b/src/Util/Generic.hs --- a/src/Util/Generic.hs +++ b/src/Util/Generic.hs @@ -11,7 +11,6 @@ ) where import Control.Exception (assert) -import qualified Data.Kind as Kind import qualified Data.Vector as V import qualified GHC.Generics as G import GHC.TypeLits (Symbol) @@ -45,5 +44,5 @@ -- For polymorphic types this throws away all type arguments. type GenericTypeName a = GTypeName (G.Rep a) -type family GTypeName (x :: Kind.Type -> Kind.Type) :: Symbol where +type family GTypeName (x :: Type -> Type) :: Symbol where GTypeName (G.D1 ('G.MetaData tyName _ _ _) _) = tyName diff --git a/src/Util/Instances.hs b/src/Util/Instances.hs --- a/src/Util/Instances.hs +++ b/src/Util/Instances.hs @@ -8,6 +8,8 @@ module Util.Instances () where import Data.Default (Default(..)) +import Data.Vinyl (Dict(..), Rec(..), ReifyConstraint(reifyConstraint)) +import Data.Vinyl.Functor as Vinyl (Compose(..), (:.)) import Fmt (Buildable(..)) instance Default Natural where @@ -18,3 +20,13 @@ instance Buildable a => (Buildable (Identity a)) where build (Identity x) = build x + +-- I've added this orphan instance to @vinyl@, +-- so we'll be able to delete it in the future. +-- https://github.com/VinylRecords/Vinyl/pull/149 +instance ReifyConstraint NFData f xs => NFData (Rec f xs) where + rnf = go . reifyConstraint @NFData + where + go :: forall elems. Rec (Dict NFData :. f) elems -> () + go RNil = () + go (Vinyl.Compose (Dict x) :& xs) = rnf x `seq` go xs diff --git a/src/Util/Named.hs b/src/Util/Named.hs --- a/src/Util/Named.hs +++ b/src/Util/Named.hs @@ -20,7 +20,6 @@ import Control.Lens (Iso', Wrapped(..), iso) import Data.Aeson (FromJSON, ToJSON) import Data.Data (Data) -import qualified Data.Kind as Kind import Fmt (Buildable(..)) import GHC.TypeLits (KnownSymbol, symbolVal) import Named ((:!), (:?), Name, NamedF(..)) @@ -42,11 +41,11 @@ (<.?>) name = fmap (name .?) infixl 4 <.?> -type family ApplyNamedFunctor (f :: Kind.Type -> Kind.Type) (a :: Kind.Type) where +type family ApplyNamedFunctor (f :: Type -> Type) (a :: Type) where ApplyNamedFunctor Identity a = a ApplyNamedFunctor Maybe a = Maybe a -type family NamedInner (n :: Kind.Type) where +type family NamedInner (n :: Type) where NamedInner (NamedF f a _) = ApplyNamedFunctor f a -- | Isomorphism between named entity and the entity itself wrapped into the diff --git a/src/Util/Peano.hs b/src/Util/Peano.hs --- a/src/Util/Peano.hs +++ b/src/Util/Peano.hs @@ -35,6 +35,7 @@ -- * Peano Arithmetic , type (>=) + , peanoSingDecrement -- * Lists , Length @@ -53,6 +54,10 @@ -- * Length constraints 'Dict'ionaries , requireLongerThan , requireLongerOrSameLength + + -- * Length constraints 'Dict'ionaries + , isGreaterThan + , isGreaterEqualThan ) where import Data.Constraint (Dict(..)) @@ -134,6 +139,14 @@ Decrement 'Z = TypeError ('Text "Expected n > 0") Decrement ('S n) = n +-- | Utility to 'Decrement' a Peano 'Sing'leton. +-- +-- Useful when dealing with the constraint +peanoSingDecrement :: Sing n -> Maybe (Sing (Decrement n)) +peanoSingDecrement = \case + SZ -> Nothing + SS n -> pure n + type family (>) (x :: Peano) (y :: Peano) :: Bool where 'Z > _ = 'False 'S _ > 'Z = 'True @@ -303,3 +316,21 @@ requireLongerOrSameLength (_ :& xs) (SS n) = do Dict <- requireLongerOrSameLength xs n return Dict + +---------------------------------------------------------------------------- +-- Arith constraints 'Dict'ionaries +---------------------------------------------------------------------------- + +isGreaterThan + :: Sing a -> Sing b + -> Maybe (Dict ((a > b) ~ 'True)) +isGreaterThan SZ _ = Nothing +isGreaterThan (SS _) SZ = pure Dict +isGreaterThan (SS a) (SS b) = isGreaterThan a b + +isGreaterEqualThan + :: Sing a -> Sing b + -> Maybe (Dict ((a >= b) ~ 'True)) +isGreaterEqualThan _ SZ = pure Dict +isGreaterEqualThan SZ _ = Nothing +isGreaterEqualThan (SS a) (SS b) = isGreaterEqualThan a b diff --git a/src/Util/TH.hs b/src/Util/TH.hs --- a/src/Util/TH.hs +++ b/src/Util/TH.hs @@ -13,11 +13,12 @@ -- additional constraints to the generated instance if those are required. deriveGADTNFData :: Name -> Q [Dec] deriveGADTNFData name = do + seqQ <- [| seq |] + unit <- [| () |] (TyConI (DataD _ dataName vars _ cons _)) <- reify name let getNameFromVar (PlainTV n) = n getNameFromVar (KindedTV n _) = n - convertTyVars orig = foldr (\a b -> AppT b . VarT $ getNameFromVar a) orig vars -- Unfolds multiple constructors of form "A, B, C :: A -> Stuff" -- into a list of tuples of constructor names and their data @@ -25,23 +26,26 @@ unfoldConstructor (ForallC _ _ c) = unfoldConstructor c unfoldConstructor _ = fail "Non GADT constructors are not supported." - -- Constructs a clause "rnf (ConName a1 a2 ...) = rnf (a1, a2, ...) + -- Constructs a clause "rnf (ConName a1 a2 ...) = rnf a1 `seq` rnf a2 `seq` rnf a3 `seq` ..." makeClauses (conName, bangs) = do - varNames <- traverse (\_ -> newName "a") bangs - let rnfExp e = AppE (VarE $ mkName "rnf") e - return $ - (Clause - [ConP conName $ map VarP varNames] - (NormalB (rnfExp . TupE $ map VarE varNames)) - [] - ) + varNames <- traverse (\_ -> newName "a") bangs + let rnfVar = VarE 'rnf + let rnfExp = AppE rnfVar . VarE + let infixSeq e1 e2 = InfixE (Just e1) seqQ (Just e2) + return $ + (Clause + [ConP conName $ map VarP varNames] + (NormalB $ foldl' infixSeq unit (map rnfExp varNames)) + [] + ) + nfDataT = + AppT (ConT $ mkName "NFData") . foldl' AppT (ConT dataName) $ + map (VarT . getNameFromVar) vars + makeInstance clauses = - InstanceD - Nothing - [] - (AppT (ConT $ mkName "NFData") (convertTyVars $ ConT dataName)) - [FunD (mkName "rnf") clauses] + InstanceD Nothing [] nfDataT [FunD (mkName "rnf") clauses] + clauses <- traverse makeClauses $ cons >>= unfoldConstructor return [makeInstance clauses] diff --git a/src/Util/Type.hs b/src/Util/Type.hs --- a/src/Util/Type.hs +++ b/src/Util/Type.hs @@ -41,7 +41,6 @@ ) where import Data.Constraint ((:-)(..), Dict(..), (\\)) -import qualified Data.Kind as Kind import Data.Type.Bool (type (&&), If, Not) import Data.Type.Equality (type (==)) import Data.Vinyl.Core (Rec(..)) @@ -105,8 +104,8 @@ (RequireAllUnique' desc xs origL) -- | Make sure given type is evaluated. --- This type family fits only for types of 'Kind.Type' kind. -type family PatternMatch (a :: Kind.Type) :: Constraint where +-- This type family fits only for types of 'Type' kind. +type family PatternMatch (a :: Type) :: Constraint where PatternMatch Int = ((), ()) PatternMatch _ = () @@ -157,7 +156,7 @@ in (x :& x1, r1) -- | A value of type parametrized with /some/ type parameter. -data Some1 (f :: k -> Kind.Type) = +data Some1 (f :: k -> Type) = forall a. Some1 (f a) deriving stock instance (forall a. Show (f a)) => Show (Some1 f) diff --git a/src/Util/TypeTuple/Class.hs b/src/Util/TypeTuple/Class.hs --- a/src/Util/TypeTuple/Class.hs +++ b/src/Util/TypeTuple/Class.hs @@ -6,8 +6,6 @@ ( RecFromTuple (..) ) where -import qualified Data.Kind as Kind - -- | Building a record from tuple. -- -- It differs from similar typeclass in 'Data.Vinyl.FromTuple' module in that @@ -15,5 +13,5 @@ -- tuple should be provided - this improves error messages when constructing -- concrete 'Rec' objects. class RecFromTuple r where - type IsoRecTuple r :: Kind.Type + type IsoRecTuple r :: Type recFromTuple :: IsoRecTuple r -> r diff --git a/src/Util/TypeTuple/Instances.hs b/src/Util/TypeTuple/Instances.hs --- a/src/Util/TypeTuple/Instances.hs +++ b/src/Util/TypeTuple/Instances.hs @@ -6,6 +6,14 @@ module Util.TypeTuple.Instances () where +import Data.Vinyl.Core (Rec(..)) + +import Util.TypeTuple.Class import Util.TypeTuple.TH -concatMapM deriveRecFromTuple [0..25] +concatMapM deriveRecFromTuple (0 : [2..25]) +-- ↑ We skip 1-ary tuple because it is GHC.Tuple.Unit, and we don't want it. + +instance RecFromTuple (Rec f '[a]) where + type IsoRecTuple (Rec f '[a]) = f a + recFromTuple a = a :& RNil diff --git a/src/Util/TypeTuple/TH.hs b/src/Util/TypeTuple/TH.hs --- a/src/Util/TypeTuple/TH.hs +++ b/src/Util/TypeTuple/TH.hs @@ -10,7 +10,6 @@ ( deriveRecFromTuple ) where -import qualified Data.Kind as Kind import Data.Vinyl.Core (Rec(..)) import qualified Language.Haskell.TH as TH @@ -34,7 +33,7 @@ let consRec var acc = [e|(:&)|] `TH.appE` TH.varE var `TH.appE` acc let recRes = foldr consRec [e|RNil|] vars - [d| instance RecFromTuple (Rec ($(pure fVar) :: u -> Kind.Type) $tyList) where + [d| instance RecFromTuple (Rec ($(pure fVar) :: u -> Type) $tyList) where type IsoRecTuple (Rec $(pure fVar) $tyList) = $tyTuple recFromTuple $tyPat = $recRes |]