{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module Lorentz.Base
( (:->) (..)
, type (%>)
, type (&)
, (#)
, (##)
, pattern I
, pattern FI
, iGenericIf
, iAnyCode
, iNonFailingCode
, iMapAnyCode
, iForceNotFail
, iWithVarAnnotations
, parseLorentzValue
, transformStringsLorentz
, transformBytesLorentz
, optimizeLorentz
, optimizeLorentzWithConf
, ContractOut
, Contract
, SomeContract (..)
, Lambda
) where
import Data.Default (def)
import qualified Data.Kind as Kind
import qualified Data.List.NonEmpty as NE (fromList)
import Data.Singletons (SingI(..))
import Fmt (Buildable(..))
import Lorentz.Constraints
import Lorentz.Value
import Michelson.ErrorPos (InstrCallStack)
import Michelson.Optimizer (OptimizerConf, optimizeWithConf)
import Michelson.Parser (ParserException, parseExpandValue)
import Michelson.Preprocess (transformBytes, transformStrings)
import Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeVerifyValue)
import Michelson.Typed
(Instr(..), RemFail(..), ToT, ToTs, Value, rfAnyInstr, rfMapAnyInstr, rfMerge)
import qualified Michelson.Untyped as U
newtype (inp :: [Kind.Type]) :-> (out :: [Kind.Type]) = LorentzInstr
{ unLorentzInstr :: RemFail Instr (ToTs inp) (ToTs out)
} deriving newtype (Show, Eq)
infixr 1 :->
instance Semigroup (s :-> s) where
(<>) = (#)
instance Monoid (s :-> s) where
mempty = I Nop
pattern I :: Instr (ToTs inp) (ToTs out) -> inp :-> out
pattern I i = LorentzInstr (RfNormal i)
pattern FI :: (forall out'. Instr (ToTs inp) out') -> inp :-> out
pattern FI i = LorentzInstr (RfAlwaysFails i)
{-# COMPLETE I, FI #-}
iGenericIf
:: (forall s'. Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
-> (a :-> s) -> (b :-> s) -> (c :-> s)
iGenericIf merger (LorentzInstr instr1) (LorentzInstr instr2) =
LorentzInstr (rfMerge merger instr1 instr2)
iAnyCode :: inp :-> out -> Instr (ToTs inp) (ToTs out)
iAnyCode = rfAnyInstr . unLorentzInstr
iNonFailingCode :: HasCallStack => inp :-> out -> Instr (ToTs inp) (ToTs out)
iNonFailingCode (I i) = i
iNonFailingCode (FI _) = error "Always failing code cannot appear here"
iMapAnyCode
:: (forall o'. Instr (ToTs i1) o' -> Instr (ToTs i2) o')
-> (i1 :-> o)
-> (i2 :-> o)
iMapAnyCode f (LorentzInstr i) = LorentzInstr $ rfMapAnyInstr f i
iForceNotFail :: (i :-> o) -> (i :-> o)
iForceNotFail = I . iAnyCode
iWithVarAnnotations :: HasCallStack => [Text] -> inp :-> out -> inp :-> out
iWithVarAnnotations annots (LorentzInstr i) = case i of
RfNormal instr -> LorentzInstr $ RfNormal $
InstrWithVarNotes (NE.fromList $ map U.AnnotationUnsafe annots) instr
RfAlwaysFails instr -> LorentzInstr $ RfAlwaysFails $
InstrWithVarNotes (NE.fromList $ map U.AnnotationUnsafe annots) instr
type (%>) = (:->)
infixr 1 %>
type ContractOut st = '[([Operation], st)]
type Contract cp st = '[(cp, st)] :-> ContractOut st
data SomeContract where
SomeContract
:: (NiceParameterFull cp, NiceStorage st)
=> Contract cp st
-> SomeContract
type (&) (a :: Kind.Type) (b :: [Kind.Type]) = a ': b
infixr 2 &
(#) :: (a :-> b) -> (b :-> c) -> a :-> c
I l # I r = I (l `Seq` r)
I l # FI r = FI (l `Seq` r)
FI l # _ = FI l
infixl 8 #
(##) :: (a :-> b) -> (b :-> c) -> (a :-> c)
l ## r = case (l, r) of
(I Nop, I x) -> I x
(I x, I Nop) -> I x
_ -> l # r
type Lambda i o = '[i] :-> '[o]
data ParseLorentzError
= ParseLorentzParseError ParserException
| ParseLorentzTypecheckError TCError
deriving stock (Show, Eq)
instance Buildable ParseLorentzError where
build =
\case
ParseLorentzParseError e -> build e
ParseLorentzTypecheckError e -> build e
parseLorentzValue ::
forall v. (IsoValue v, SingI (ToT v), Typeable (ToT v))
=> Text
-> Either ParseLorentzError v
parseLorentzValue =
fmap fromVal . (toTyped <=< first ParseLorentzParseError . parseExpandValue)
where
toTyped :: U.Value -> Either ParseLorentzError (Value (ToT v))
toTyped =
first ParseLorentzTypecheckError .
runTypeCheckIsolated .
usingReaderT (def @InstrCallStack) .
typeVerifyValue
transformStringsLorentz ::
Bool -> (MText -> MText) -> inp :-> out -> inp :-> out
transformStringsLorentz goToValues f =
iMapAnyCode $ transformStrings goToValues f
transformBytesLorentz ::
Bool -> (ByteString -> ByteString) -> inp :-> out -> inp :-> out
transformBytesLorentz goToValues f =
iMapAnyCode $ transformBytes goToValues f
optimizeLorentzWithConf
:: OptimizerConf
-> inp :-> out
-> inp :-> out
optimizeLorentzWithConf conf =
iMapAnyCode (optimizeWithConf conf)
optimizeLorentz
:: inp :-> out
-> inp :-> out
optimizeLorentz = optimizeLorentzWithConf def