module Michelson.TypeCheck.Types
( HST (..)
, (-:&)
, SomeHST (..)
, SomeInstrOut (..)
, SomeInstr (..)
, SomeNotedValue (..)
, SomeContract (..)
, SomeCValue (..)
, BoundVars (..)
, TcExtFrames
, mapSomeContract
, 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.Untyped (Var, Type, noAnn)
import Michelson.Untyped.Annotation (VarAnn)
import Michelson.Typed
(Notes(..), Sing(..), T(..), fromSingT, starNotes)
import qualified Michelson.Typed as T
import Michelson.Typed.Instr
import Michelson.Typed.Value
import Util.Typeable
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, starNotes, noAnn) ::& hst
infixr 7 -:&
data SomeHST where
SomeHST :: Typeable ts => HST ts -> SomeHST
deriving stock 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 SomeNotedValue where
(::::) :: (SingI t, Typeable t)
=> T.Value t
-> (Sing t, Notes t)
-> SomeNotedValue
instance Show SomeNotedValue where
show (val :::: (sing, notes)) =
show val <> " :: " <> "(" <> show (fromSingT sing)
<> ", " <> show notes <> ")"
data SomeCValue where
(:--:) :: (SingI t, Typeable t)
=> CValue t -> Sing t -> SomeCValue
data SomeContract where
SomeContract :: FullContract cp st -> SomeContract
mapSomeContract ::
(forall inp out. Instr inp out -> Instr inp out)
-> SomeContract
-> SomeContract
mapSomeContract f (SomeContract fc) = SomeContract $ mapFullContractCode f fc
deriving stock instance Show SomeContract
data BoundVars = BoundVars (Map Var Type) (Maybe SomeHST)
noBoundVars :: BoundVars
noBoundVars = BoundVars Map.empty Nothing
type TcExtFrames = [BoundVars]