module Michelson.TypeCheck.Types
( HST (..)
, SomeHST (..)
, SomeInstr (..)
, SomeVal (..)
, SomeContract (..)
, SomeValC (..)
, TCError (..)
, ExtC
, TcInstrHandler
, TcExtHandler
, TcExtFrames
, TcResult
, TypeCheckEnv (..)
, TypeCheckT
, runTypeCheckT
) where
import Data.Singletons (SingI)
import Fmt (Buildable(..), pretty, (+|), (|+), (||+))
import Prelude hiding (EQ, GT, LT)
import qualified Text.Show
import Michelson.Typed (ConversibleExt, Notes(..), Sing(..), T(..), fromSingT)
import Michelson.Typed.Extract (toUType)
import Michelson.Typed.Instr
import Michelson.Typed.Value
import qualified Michelson.Untyped as U
import Michelson.Untyped.Annotation (VarAnn)
data HST (ts :: [T]) where
SNil :: HST '[]
(::&) :: (Typeable xs, Typeable x, SingI x)
=> (Sing x, Notes x, VarAnn)
-> HST xs
-> HST (x ': xs)
instance Show (HST ts) where
show SNil = "[]"
show (r ::& rs) = "[ " <> showDo (r ::& rs) <> " ]"
where
showDo :: HST (t ': ts_) -> String
showDo ((a, _notes, _vn) ::& (b ::& c)) =
show (fromSingT a) <> ", " <> showDo (b ::& c)
showDo ((a, _notes, _vn) ::& SNil) = show (fromSingT a)
infixr 7 ::&
data SomeHST where
SomeHST :: Typeable ts => HST ts -> SomeHST
deriving instance Show SomeHST
data SomeInstr where
(:::) :: (Typeable inp, Typeable out)
=> Instr inp out
-> (HST inp, HST out)
-> SomeInstr
SiFail :: SomeInstr
instance Show InstrExtT => Show SomeInstr where
show (i ::: (inp, out)) = show i <> " :: " <> show inp <> " -> " <> show out
show SiFail = "failed"
data SomeVal where
(::::) :: (SingI t, Typeable t)
=> Val Instr t
-> (Sing t, Notes t)
-> SomeVal
data SomeValC where
(:--:) :: (SingI t, Typeable t)
=> CVal t -> Sing t -> SomeValC
data SomeContract where
SomeContract
:: (Typeable st, SingI st, SingI cp, Typeable cp)
=> Contract cp st
-> HST (ContractInp cp st)
-> HST (ContractOut st)
-> SomeContract
deriving instance Show InstrExtT => Show SomeContract
data TCError =
TCFailedOnInstr U.ExpandedInstr SomeHST Text
| TCFailedOnValue U.UntypedValue T Text
| TCOtherError Text
instance Buildable U.ExpandedInstr => Buildable TCError where
build = \case
TCFailedOnInstr instr (SomeHST t) custom ->
"Error checking expression " +| instr
|+ " against input stack type " +| t
||+ bool (": " +| custom |+ "") "" (null custom)
TCFailedOnValue v t custom ->
"Error checking value " +| v
|+ " against type " +| toUType t
|+ bool (": " +| custom |+ "") "" (null custom)
TCOtherError e ->
"Error occurred during type check: " +| e |+ ""
instance Buildable U.ExpandedInstr => Show TCError where
show = pretty
instance Buildable U.ExpandedInstr => Exception TCError
type TcExtFrames = [(U.ExpandedInstrExtU, SomeHST)]
type ExtC
= ( Show InstrExtT
, Eq U.ExpandedInstrExtU
, Typeable InstrExtT
, Buildable U.ExpandedInstr
, ConversibleExt
)
type TypeCheckT a =
ExceptT TCError
(State TypeCheckEnv) a
type TcExtHandler
= U.ExpandedInstrExtU -> TcExtFrames -> SomeHST -> TypeCheckT (TcExtFrames, Maybe InstrExtT)
data TypeCheckEnv = TypeCheckEnv
{ tcExtHandler :: TcExtHandler
, tcExtFrames :: TcExtFrames
, tcContractParam :: U.Type
}
runTypeCheckT :: TcExtHandler -> U.Type -> TypeCheckT a -> Either TCError a
runTypeCheckT nh param act = evaluatingState (TypeCheckEnv nh [] param) $ runExceptT act
type TcResult = Either TCError SomeInstr
type TcInstrHandler
= U.ExpandedInstr
-> SomeHST
-> TypeCheckT SomeInstr