module Michelson.TypeCheck.Types
( HST (..)
, (-:&)
, SomeHST (..)
, SomeInstrOut (..)
, SomeInstr (..)
, SomeValue (..)
, SomeContract (..)
, SomeCValue (..)
, BoundVars (..)
, TcExtFrames
, noBoundVars
) where
import Data.Singletons (SingI)
import Prelude hiding (EQ, GT, LT)
import qualified Text.Show
import qualified Data.Map.Lazy as Map
import Michelson.EqParam (eqParam1)
import Michelson.Untyped (Var, Type, noAnn)
import Michelson.Typed
(HasNoBigMap, HasNoOp, Notes(..), Sing(..), BigMapConstraint, T(..), fromSingT)
import qualified Michelson.Typed as T
import Michelson.Typed.Instr
import Michelson.Typed.Value
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 ::&
instance Eq (HST ts) where
SNil == SNil = True
(_, n1, a1) ::& h1 == (_, n2, a2) ::& h2 =
n1 == n2 && a1 == a2 && h1 == h2
(-:&)
:: (Typeable xs, Typeable x, SingI x)
=> Sing x
-> HST xs
-> HST (x ': xs)
s -:& hst = (s, NStar, noAnn) ::& hst
infixr 7 -:&
data SomeHST where
SomeHST :: Typeable ts => HST ts -> SomeHST
deriving instance Show SomeHST
instance Eq SomeHST where
SomeHST hst1 == SomeHST hst2 = hst1 `eqParam1` hst2
data SomeInstrOut inp where
(:::)
:: (Typeable out)
=> Instr inp out
-> HST out
-> SomeInstrOut inp
AnyOutInstr
:: (forall out. Instr inp out)
-> SomeInstrOut inp
infix 9 :::
instance Show (ExtInstr inp) => Show (SomeInstrOut inp) where
show (i ::: out) = show i <> " :: " <> show out
show (AnyOutInstr i) = show i <> " :: *"
data SomeInstr inp where
(:/) :: HST inp -> SomeInstrOut inp -> SomeInstr inp
infix 8 :/
instance Show (ExtInstr inp) => Show (SomeInstr inp) where
show (inp :/ out) = show inp <> " -> " <> show out
data SomeValue where
(::::) :: (SingI t, Typeable t)
=> T.Value t
-> (Sing t, Notes t)
-> SomeValue
data SomeCValue where
(:--:) :: (SingI t, Typeable t)
=> CValue t -> Sing t -> SomeCValue
data SomeContract where
SomeContract
:: (Each [Typeable, SingI, HasNoOp] [st, cp]
, HasNoBigMap cp, BigMapConstraint st)
=> Contract cp st
-> HST (ContractInp cp st)
-> HST (ContractOut st)
-> SomeContract
deriving instance Show SomeContract
data BoundVars = BoundVars (Map Var Type) (Maybe SomeHST)
noBoundVars :: BoundVars
noBoundVars = BoundVars Map.empty Nothing
type TcExtFrames = [BoundVars]