Safe Haskell	None
Language	Haskell2010

TAL

Synopsis

Documentation

type TyName = Name Ty Source #

data Ty Source #

Constructors

TyVar TyName
TyInt
All (Bind [TyName] Gamma)
TyProd [(Ty, Flag)]
Exists (Bind TyName Ty)

Instances

Show Ty Source #
Methods showsPrec :: Int -> Ty -> ShowS # show :: Ty -> String # showList :: [Ty] -> ShowS #
Rep Ty Source #
Methods rep :: R Ty #
Alpha Ty Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Ty -> Ty # fv' :: Collection f => AlphaCtx -> Ty -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Ty -> (Ty -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Ty -> m (Ty, Perm AnyName) # aeq' :: AlphaCtx -> Ty -> Ty -> Bool # acompare' :: AlphaCtx -> Ty -> Ty -> Ordering # close :: Alpha b => AlphaCtx -> b -> Ty -> Ty # open :: Alpha b => AlphaCtx -> b -> Ty -> Ty # isPat :: Ty -> Maybe [AnyName] # isTerm :: Ty -> Bool # isEmbed :: Ty -> Bool # nthpatrec :: Ty -> NthCont # findpatrec :: Ty -> AnyName -> FindResult #
Display Ty Source #
Methods display :: Ty -> DM Doc Source #
(Sat (ctx0 TyName), Sat (ctx0 (Bind [TyName] Gamma)), Sat (ctx0 [(Ty, Flag)]), Sat (ctx0 (Bind TyName Ty))) => Rep1 ctx0 Ty Source #
Methods rep1 :: R1 ctx0 Ty #
Subst Ty InstrSeq Source #
Methods isvar :: InstrSeq -> Maybe (SubstName InstrSeq Ty) # isCoerceVar :: InstrSeq -> Maybe (SubstCoerce InstrSeq Ty) # subst :: Name Ty -> Ty -> InstrSeq -> InstrSeq # substs :: [(Name Ty, Ty)] -> InstrSeq -> InstrSeq # substPat :: AlphaCtx -> Ty -> InstrSeq -> InstrSeq # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> InstrSeq -> InstrSeq #
Subst Ty Instruction Source #
Methods isvar :: Instruction -> Maybe (SubstName Instruction Ty) # isCoerceVar :: Instruction -> Maybe (SubstCoerce Instruction Ty) # subst :: Name Ty -> Ty -> Instruction -> Instruction # substs :: [(Name Ty, Ty)] -> Instruction -> Instruction # substPat :: AlphaCtx -> Ty -> Instruction -> Instruction # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Instruction -> Instruction #
Subst Ty HeapVal Source #
Methods isvar :: HeapVal -> Maybe (SubstName HeapVal Ty) # isCoerceVar :: HeapVal -> Maybe (SubstCoerce HeapVal Ty) # subst :: Name Ty -> Ty -> HeapVal -> HeapVal # substs :: [(Name Ty, Ty)] -> HeapVal -> HeapVal # substPat :: AlphaCtx -> Ty -> HeapVal -> HeapVal # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> HeapVal -> HeapVal #
Subst Ty SmallVal Source #
Methods isvar :: SmallVal -> Maybe (SubstName SmallVal Ty) # isCoerceVar :: SmallVal -> Maybe (SubstCoerce SmallVal Ty) # subst :: Name Ty -> Ty -> SmallVal -> SmallVal # substs :: [(Name Ty, Ty)] -> SmallVal -> SmallVal # substPat :: AlphaCtx -> Ty -> SmallVal -> SmallVal # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> SmallVal -> SmallVal #
Subst Ty WordVal Source #
Methods isvar :: WordVal -> Maybe (SubstName WordVal Ty) # isCoerceVar :: WordVal -> Maybe (SubstCoerce WordVal Ty) # subst :: Name Ty -> Ty -> WordVal -> WordVal # substs :: [(Name Ty, Ty)] -> WordVal -> WordVal # substPat :: AlphaCtx -> Ty -> WordVal -> WordVal # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> WordVal -> WordVal #
Subst Ty Label Source #
Methods isvar :: Label -> Maybe (SubstName Label Ty) # isCoerceVar :: Label -> Maybe (SubstCoerce Label Ty) # subst :: Name Ty -> Ty -> Label -> Label # substs :: [(Name Ty, Ty)] -> Label -> Label # substPat :: AlphaCtx -> Ty -> Label -> Label # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Label -> Label #
Subst Ty Register Source #
Methods isvar :: Register -> Maybe (SubstName Register Ty) # isCoerceVar :: Register -> Maybe (SubstCoerce Register Ty) # subst :: Name Ty -> Ty -> Register -> Register # substs :: [(Name Ty, Ty)] -> Register -> Register # substPat :: AlphaCtx -> Ty -> Register -> Register # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Register -> Register #
Subst Ty Flag Source #
Methods isvar :: Flag -> Maybe (SubstName Flag Ty) # isCoerceVar :: Flag -> Maybe (SubstCoerce Flag Ty) # subst :: Name Ty -> Ty -> Flag -> Flag # substs :: [(Name Ty, Ty)] -> Flag -> Flag # substPat :: AlphaCtx -> Ty -> Flag -> Flag # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Flag -> Flag #
Subst Ty Ty Source #
Methods isvar :: Ty -> Maybe (SubstName Ty Ty) # isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Ty) # subst :: Name Ty -> Ty -> Ty -> Ty # substs :: [(Name Ty, Ty)] -> Ty -> Ty # substPat :: AlphaCtx -> Ty -> Ty -> Ty # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Ty -> Ty #
Subst Ty a => Subst Ty (Pack a) Source #
Methods isvar :: Pack a -> Maybe (SubstName (Pack a) Ty) # isCoerceVar :: Pack a -> Maybe (SubstCoerce (Pack a) Ty) # subst :: Name Ty -> Ty -> Pack a -> Pack a # substs :: [(Name Ty, Ty)] -> Pack a -> Pack a # substPat :: AlphaCtx -> Ty -> Pack a -> Pack a # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Pack a -> Pack a #
Subst Ty a => Subst Ty (TyApp a) Source #
Methods isvar :: TyApp a -> Maybe (SubstName (TyApp a) Ty) # isCoerceVar :: TyApp a -> Maybe (SubstCoerce (TyApp a) Ty) # subst :: Name Ty -> Ty -> TyApp a -> TyApp a # substs :: [(Name Ty, Ty)] -> TyApp a -> TyApp a # substPat :: AlphaCtx -> Ty -> TyApp a -> TyApp a # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> TyApp a -> TyApp a #
(Rep a, Subst Ty b) => Subst Ty (Map a b) Source #
Methods isvar :: Map a b -> Maybe (SubstName (Map a b) Ty) # isCoerceVar :: Map a b -> Maybe (SubstCoerce (Map a b) Ty) # subst :: Name Ty -> Ty -> Map a b -> Map a b # substs :: [(Name Ty, Ty)] -> Map a b -> Map a b # substPat :: AlphaCtx -> Ty -> Map a b -> Map a b # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Map a b -> Map a b #
Display (Ty, Flag) Source #
Methods display :: (Ty, Flag) -> DM Doc Source #

data Flag Source #

Constructors

Un
Init

Instances

Eq Flag Source #
Methods (==) :: Flag -> Flag -> Bool # (/=) :: Flag -> Flag -> Bool #
Ord Flag Source #
Methods compare :: Flag -> Flag -> Ordering # (<) :: Flag -> Flag -> Bool # (<=) :: Flag -> Flag -> Bool # (>) :: Flag -> Flag -> Bool # (>=) :: Flag -> Flag -> Bool # max :: Flag -> Flag -> Flag # min :: Flag -> Flag -> Flag #
Show Flag Source #
Methods showsPrec :: Int -> Flag -> ShowS # show :: Flag -> String # showList :: [Flag] -> ShowS #
Rep Flag Source #
Methods rep :: R Flag #
Alpha Flag Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Flag -> Flag # fv' :: Collection f => AlphaCtx -> Flag -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Flag -> (Flag -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Flag -> m (Flag, Perm AnyName) # aeq' :: AlphaCtx -> Flag -> Flag -> Bool # acompare' :: AlphaCtx -> Flag -> Flag -> Ordering # close :: Alpha b => AlphaCtx -> b -> Flag -> Flag # open :: Alpha b => AlphaCtx -> b -> Flag -> Flag # isPat :: Flag -> Maybe [AnyName] # isTerm :: Flag -> Bool # isEmbed :: Flag -> Bool # nthpatrec :: Flag -> NthCont # findpatrec :: Flag -> AnyName -> FindResult #
Rep1 ctx0 Flag Source #
Methods rep1 :: R1 ctx0 Flag #
Subst Ty Flag Source #
Methods isvar :: Flag -> Maybe (SubstName Flag Ty) # isCoerceVar :: Flag -> Maybe (SubstCoerce Flag Ty) # subst :: Name Ty -> Ty -> Flag -> Flag # substs :: [(Name Ty, Ty)] -> Flag -> Flag # substPat :: AlphaCtx -> Ty -> Flag -> Flag # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Flag -> Flag #
Display (Ty, Flag) Source #
Methods display :: (Ty, Flag) -> DM Doc Source #

type Psi = Map Label Ty Source #

type Gamma = [(Register, Ty)] Source #

newtype Register Source #

Constructors

Register String

Instances

Enum Register Source #
Methods succ :: Register -> Register # pred :: Register -> Register # toEnum :: Int -> Register # fromEnum :: Register -> Int # enumFrom :: Register -> [Register] # enumFromThen :: Register -> Register -> [Register] # enumFromTo :: Register -> Register -> [Register] # enumFromThenTo :: Register -> Register -> Register -> [Register] #
Eq Register Source #
Methods (==) :: Register -> Register -> Bool # (/=) :: Register -> Register -> Bool #
Ord Register Source #
Methods compare :: Register -> Register -> Ordering # (<) :: Register -> Register -> Bool # (<=) :: Register -> Register -> Bool # (>) :: Register -> Register -> Bool # (>=) :: Register -> Register -> Bool # max :: Register -> Register -> Register # min :: Register -> Register -> Register #
Show Register Source #
Methods showsPrec :: Int -> Register -> ShowS # show :: Register -> String # showList :: [Register] -> ShowS #
Rep Register Source #
Methods rep :: R Register #
Alpha Register Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Register -> Register # fv' :: Collection f => AlphaCtx -> Register -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Register -> (Register -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Register -> m (Register, Perm AnyName) # aeq' :: AlphaCtx -> Register -> Register -> Bool # acompare' :: AlphaCtx -> Register -> Register -> Ordering # close :: Alpha b => AlphaCtx -> b -> Register -> Register # open :: Alpha b => AlphaCtx -> b -> Register -> Register # isPat :: Register -> Maybe [AnyName] # isTerm :: Register -> Bool # isEmbed :: Register -> Bool # nthpatrec :: Register -> NthCont # findpatrec :: Register -> AnyName -> FindResult #
Sat (ctx0 String) => Rep1 ctx0 Register Source #
Methods rep1 :: R1 ctx0 Register #
Subst Ty Register Source #
Methods isvar :: Register -> Maybe (SubstName Register Ty) # isCoerceVar :: Register -> Maybe (SubstCoerce Register Ty) # subst :: Name Ty -> Ty -> Register -> Register # substs :: [(Name Ty, Ty)] -> Register -> Register # substPat :: AlphaCtx -> Ty -> Register -> Register # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Register -> Register #
Display a => Display [(Register, a)] Source #
Methods display :: [(Register, a)] -> DM Doc Source #
Alpha b => Alpha (Map Register b) Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Map Register b -> Map Register b # fv' :: Collection f => AlphaCtx -> Map Register b -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Map Register b -> (Map Register b -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Map Register b -> m (Map Register b, Perm AnyName) # aeq' :: AlphaCtx -> Map Register b -> Map Register b -> Bool # acompare' :: AlphaCtx -> Map Register b -> Map Register b -> Ordering # close :: Alpha b => AlphaCtx -> b -> Map Register b -> Map Register b # open :: Alpha b => AlphaCtx -> b -> Map Register b -> Map Register b # isPat :: Map Register b -> Maybe [AnyName] # isTerm :: Map Register b -> Bool # isEmbed :: Map Register b -> Bool # nthpatrec :: Map Register b -> NthCont # findpatrec :: Map Register b -> AnyName -> FindResult #
Display a => Display (Map Register a) Source #
Methods display :: Map Register a -> DM Doc Source #
Display (Heap, RegisterFile, InstrSeq) Source #
Methods display :: (Heap, RegisterFile, InstrSeq) -> DM Doc Source #

reg1 :: Register Source #

rtmp :: Int -> Register Source #

newtype Label Source #

Constructors

Label (Name Heap)

Instances

Eq Label Source #
Methods (==) :: Label -> Label -> Bool # (/=) :: Label -> Label -> Bool #
Ord Label Source #
Methods compare :: Label -> Label -> Ordering # (<) :: Label -> Label -> Bool # (<=) :: Label -> Label -> Bool # (>) :: Label -> Label -> Bool # (>=) :: Label -> Label -> Bool # max :: Label -> Label -> Label # min :: Label -> Label -> Label #
Show Label Source #
Methods showsPrec :: Int -> Label -> ShowS # show :: Label -> String # showList :: [Label] -> ShowS #
Rep Label Source #
Methods rep :: R Label #
Alpha Label Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Label -> Label # fv' :: Collection f => AlphaCtx -> Label -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Label -> (Label -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Label -> m (Label, Perm AnyName) # aeq' :: AlphaCtx -> Label -> Label -> Bool # acompare' :: AlphaCtx -> Label -> Label -> Ordering # close :: Alpha b => AlphaCtx -> b -> Label -> Label # open :: Alpha b => AlphaCtx -> b -> Label -> Label # isPat :: Label -> Maybe [AnyName] # isTerm :: Label -> Bool # isEmbed :: Label -> Bool # nthpatrec :: Label -> NthCont # findpatrec :: Label -> AnyName -> FindResult #
Display Label Source #
Methods display :: Label -> DM Doc Source #
Sat (ctx0 (Name Heap)) => Rep1 ctx0 Label Source #
Methods rep1 :: R1 ctx0 Label #
Subst Ty Label Source #
Methods isvar :: Label -> Maybe (SubstName Label Ty) # isCoerceVar :: Label -> Maybe (SubstCoerce Label Ty) # subst :: Name Ty -> Ty -> Label -> Label # substs :: [(Name Ty, Ty)] -> Label -> Label # substPat :: AlphaCtx -> Ty -> Label -> Label # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Label -> Label #
Display a => Display (Map Label a) Source #
Methods display :: Map Label a -> DM Doc Source #
Display (Heap, RegisterFile, InstrSeq) Source #
Methods display :: (Heap, RegisterFile, InstrSeq) -> DM Doc Source #

data TyApp a Source #

Constructors

TyApp a Ty

Instances

(Rep a0, Sat (ctx0 a0), Sat (ctx0 Ty)) => Rep1 ctx0 (TyApp a0) Source #
Methods rep1 :: R1 ctx0 (TyApp a0) #
Subst Ty a => Subst Ty (TyApp a) Source #
Methods isvar :: TyApp a -> Maybe (SubstName (TyApp a) Ty) # isCoerceVar :: TyApp a -> Maybe (SubstCoerce (TyApp a) Ty) # subst :: Name Ty -> Ty -> TyApp a -> TyApp a # substs :: [(Name Ty, Ty)] -> TyApp a -> TyApp a # substPat :: AlphaCtx -> Ty -> TyApp a -> TyApp a # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> TyApp a -> TyApp a #
Show a => Show (TyApp a) Source #
Methods showsPrec :: Int -> TyApp a -> ShowS # show :: TyApp a -> String # showList :: [TyApp a] -> ShowS #
Rep a0 => Rep (TyApp a0) Source #
Methods rep :: R (TyApp a0) #
Alpha a => Alpha (TyApp a) Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> TyApp a -> TyApp a # fv' :: Collection f => AlphaCtx -> TyApp a -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> TyApp a -> (TyApp a -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> TyApp a -> m (TyApp a, Perm AnyName) # aeq' :: AlphaCtx -> TyApp a -> TyApp a -> Bool # acompare' :: AlphaCtx -> TyApp a -> TyApp a -> Ordering # close :: Alpha b => AlphaCtx -> b -> TyApp a -> TyApp a # open :: Alpha b => AlphaCtx -> b -> TyApp a -> TyApp a # isPat :: TyApp a -> Maybe [AnyName] # isTerm :: TyApp a -> Bool # isEmbed :: TyApp a -> Bool # nthpatrec :: TyApp a -> NthCont # findpatrec :: TyApp a -> AnyName -> FindResult #
Display a => Display (TyApp a) Source #
Methods display :: TyApp a -> DM Doc Source #

sapps :: SmallVal -> [Ty] -> SmallVal Source #

data Pack a Source #

Constructors

Pack Ty a Ty

Instances

(Rep a0, Sat (ctx0 Ty), Sat (ctx0 a0)) => Rep1 ctx0 (Pack a0) Source #
Methods rep1 :: R1 ctx0 (Pack a0) #
Subst Ty a => Subst Ty (Pack a) Source #
Methods isvar :: Pack a -> Maybe (SubstName (Pack a) Ty) # isCoerceVar :: Pack a -> Maybe (SubstCoerce (Pack a) Ty) # subst :: Name Ty -> Ty -> Pack a -> Pack a # substs :: [(Name Ty, Ty)] -> Pack a -> Pack a # substPat :: AlphaCtx -> Ty -> Pack a -> Pack a # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Pack a -> Pack a #
Show a => Show (Pack a) Source #
Methods showsPrec :: Int -> Pack a -> ShowS # show :: Pack a -> String # showList :: [Pack a] -> ShowS #
Rep a0 => Rep (Pack a0) Source #
Methods rep :: R (Pack a0) #
Alpha a => Alpha (Pack a) Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Pack a -> Pack a # fv' :: Collection f => AlphaCtx -> Pack a -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Pack a -> (Pack a -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Pack a -> m (Pack a, Perm AnyName) # aeq' :: AlphaCtx -> Pack a -> Pack a -> Bool # acompare' :: AlphaCtx -> Pack a -> Pack a -> Ordering # close :: Alpha b => AlphaCtx -> b -> Pack a -> Pack a # open :: Alpha b => AlphaCtx -> b -> Pack a -> Pack a # isPat :: Pack a -> Maybe [AnyName] # isTerm :: Pack a -> Bool # isEmbed :: Pack a -> Bool # nthpatrec :: Pack a -> NthCont # findpatrec :: Pack a -> AnyName -> FindResult #
Display a => Display (Pack a) Source #
Methods display :: Pack a -> DM Doc Source #

data WordVal Source #

Constructors

LabelVal Label
TmInt Int
Junk Ty
WApp (TyApp WordVal)
WPack (Pack WordVal)

Instances

Show WordVal Source #
Methods showsPrec :: Int -> WordVal -> ShowS # show :: WordVal -> String # showList :: [WordVal] -> ShowS #
Rep WordVal Source #
Methods rep :: R WordVal #
Alpha WordVal Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> WordVal -> WordVal # fv' :: Collection f => AlphaCtx -> WordVal -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> WordVal -> (WordVal -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> WordVal -> m (WordVal, Perm AnyName) # aeq' :: AlphaCtx -> WordVal -> WordVal -> Bool # acompare' :: AlphaCtx -> WordVal -> WordVal -> Ordering # close :: Alpha b => AlphaCtx -> b -> WordVal -> WordVal # open :: Alpha b => AlphaCtx -> b -> WordVal -> WordVal # isPat :: WordVal -> Maybe [AnyName] # isTerm :: WordVal -> Bool # isEmbed :: WordVal -> Bool # nthpatrec :: WordVal -> NthCont # findpatrec :: WordVal -> AnyName -> FindResult #
Display WordVal Source #
Methods display :: WordVal -> DM Doc Source #
(Sat (ctx0 Label), Sat (ctx0 Int), Sat (ctx0 Ty), Sat (ctx0 (TyApp WordVal)), Sat (ctx0 (Pack WordVal))) => Rep1 ctx0 WordVal Source #
Methods rep1 :: R1 ctx0 WordVal #
Subst Ty WordVal Source #
Methods isvar :: WordVal -> Maybe (SubstName WordVal Ty) # isCoerceVar :: WordVal -> Maybe (SubstCoerce WordVal Ty) # subst :: Name Ty -> Ty -> WordVal -> WordVal # substs :: [(Name Ty, Ty)] -> WordVal -> WordVal # substPat :: AlphaCtx -> Ty -> WordVal -> WordVal # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> WordVal -> WordVal #
Display (Heap, RegisterFile, InstrSeq) Source #
Methods display :: (Heap, RegisterFile, InstrSeq) -> DM Doc Source #

data SmallVal Source #

Constructors

RegVal Register
WordVal WordVal
SApp (TyApp SmallVal)
SPack (Pack SmallVal)

Instances

Show SmallVal Source #
Methods showsPrec :: Int -> SmallVal -> ShowS # show :: SmallVal -> String # showList :: [SmallVal] -> ShowS #
Rep SmallVal Source #
Methods rep :: R SmallVal #
Alpha SmallVal Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> SmallVal -> SmallVal # fv' :: Collection f => AlphaCtx -> SmallVal -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> SmallVal -> (SmallVal -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> SmallVal -> m (SmallVal, Perm AnyName) # aeq' :: AlphaCtx -> SmallVal -> SmallVal -> Bool # acompare' :: AlphaCtx -> SmallVal -> SmallVal -> Ordering # close :: Alpha b => AlphaCtx -> b -> SmallVal -> SmallVal # open :: Alpha b => AlphaCtx -> b -> SmallVal -> SmallVal # isPat :: SmallVal -> Maybe [AnyName] # isTerm :: SmallVal -> Bool # isEmbed :: SmallVal -> Bool # nthpatrec :: SmallVal -> NthCont # findpatrec :: SmallVal -> AnyName -> FindResult #
Display SmallVal Source #
Methods display :: SmallVal -> DM Doc Source #
(Sat (ctx0 Register), Sat (ctx0 WordVal), Sat (ctx0 (TyApp SmallVal)), Sat (ctx0 (Pack SmallVal))) => Rep1 ctx0 SmallVal Source #
Methods rep1 :: R1 ctx0 SmallVal #
Subst Ty SmallVal Source #
Methods isvar :: SmallVal -> Maybe (SubstName SmallVal Ty) # isCoerceVar :: SmallVal -> Maybe (SubstCoerce SmallVal Ty) # subst :: Name Ty -> Ty -> SmallVal -> SmallVal # substs :: [(Name Ty, Ty)] -> SmallVal -> SmallVal # substPat :: AlphaCtx -> Ty -> SmallVal -> SmallVal # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> SmallVal -> SmallVal #

data HeapVal Source #

Constructors

Tuple [WordVal]
Code [TyName] Gamma InstrSeq

Instances

Show HeapVal Source #
Methods showsPrec :: Int -> HeapVal -> ShowS # show :: HeapVal -> String # showList :: [HeapVal] -> ShowS #
Rep HeapVal Source #
Methods rep :: R HeapVal #
Alpha HeapVal Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> HeapVal -> HeapVal # fv' :: Collection f => AlphaCtx -> HeapVal -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> HeapVal -> (HeapVal -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> HeapVal -> m (HeapVal, Perm AnyName) # aeq' :: AlphaCtx -> HeapVal -> HeapVal -> Bool # acompare' :: AlphaCtx -> HeapVal -> HeapVal -> Ordering # close :: Alpha b => AlphaCtx -> b -> HeapVal -> HeapVal # open :: Alpha b => AlphaCtx -> b -> HeapVal -> HeapVal # isPat :: HeapVal -> Maybe [AnyName] # isTerm :: HeapVal -> Bool # isEmbed :: HeapVal -> Bool # nthpatrec :: HeapVal -> NthCont # findpatrec :: HeapVal -> AnyName -> FindResult #
Display HeapVal Source #
Methods display :: HeapVal -> DM Doc Source #
(Sat (ctx0 [WordVal]), Sat (ctx0 [TyName]), Sat (ctx0 Gamma), Sat (ctx0 InstrSeq)) => Rep1 ctx0 HeapVal Source #
Methods rep1 :: R1 ctx0 HeapVal #
Subst Ty HeapVal Source #
Methods isvar :: HeapVal -> Maybe (SubstName HeapVal Ty) # isCoerceVar :: HeapVal -> Maybe (SubstCoerce HeapVal Ty) # subst :: Name Ty -> Ty -> HeapVal -> HeapVal # substs :: [(Name Ty, Ty)] -> HeapVal -> HeapVal # substPat :: AlphaCtx -> Ty -> HeapVal -> HeapVal # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> HeapVal -> HeapVal #
Display (Heap, RegisterFile, InstrSeq) Source #
Methods display :: (Heap, RegisterFile, InstrSeq) -> DM Doc Source #

type Heap = Map Label HeapVal Source #

type RegisterFile = Map Register WordVal Source #

data Instruction Source #

Instances

Show Instruction Source #
Methods showsPrec :: Int -> Instruction -> ShowS # show :: Instruction -> String # showList :: [Instruction] -> ShowS #
Rep Instruction Source #
Methods rep :: R Instruction #
Alpha Instruction Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> Instruction -> Instruction # fv' :: Collection f => AlphaCtx -> Instruction -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> Instruction -> (Instruction -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> Instruction -> m (Instruction, Perm AnyName) # aeq' :: AlphaCtx -> Instruction -> Instruction -> Bool # acompare' :: AlphaCtx -> Instruction -> Instruction -> Ordering # close :: Alpha b => AlphaCtx -> b -> Instruction -> Instruction # open :: Alpha b => AlphaCtx -> b -> Instruction -> Instruction # isPat :: Instruction -> Maybe [AnyName] # isTerm :: Instruction -> Bool # isEmbed :: Instruction -> Bool # nthpatrec :: Instruction -> NthCont # findpatrec :: Instruction -> AnyName -> FindResult #
Display Instruction Source #
Methods display :: Instruction -> DM Doc Source #
(Sat (ctx0 Register), Sat (ctx0 SmallVal), Sat (ctx0 Int), Sat (ctx0 [Ty]), Sat (ctx0 TyName)) => Rep1 ctx0 Instruction Source #
Methods rep1 :: R1 ctx0 Instruction #
Subst Ty Instruction Source #
Methods isvar :: Instruction -> Maybe (SubstName Instruction Ty) # isCoerceVar :: Instruction -> Maybe (SubstCoerce Instruction Ty) # subst :: Name Ty -> Ty -> Instruction -> Instruction # substs :: [(Name Ty, Ty)] -> Instruction -> Instruction # substPat :: AlphaCtx -> Ty -> Instruction -> Instruction # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Instruction -> Instruction #

data InstrSeq Source #

Constructors

Seq Instruction InstrSeq
Jump SmallVal
Halt Ty

Instances

Show InstrSeq Source #
Methods showsPrec :: Int -> InstrSeq -> ShowS # show :: InstrSeq -> String # showList :: [InstrSeq] -> ShowS #
Rep InstrSeq Source #
Methods rep :: R InstrSeq #
Alpha InstrSeq Source #
Methods swaps' :: AlphaCtx -> Perm AnyName -> InstrSeq -> InstrSeq # fv' :: Collection f => AlphaCtx -> InstrSeq -> f AnyName # lfreshen' :: LFresh m => AlphaCtx -> InstrSeq -> (InstrSeq -> Perm AnyName -> m b) -> m b # freshen' :: Fresh m => AlphaCtx -> InstrSeq -> m (InstrSeq, Perm AnyName) # aeq' :: AlphaCtx -> InstrSeq -> InstrSeq -> Bool # acompare' :: AlphaCtx -> InstrSeq -> InstrSeq -> Ordering # close :: Alpha b => AlphaCtx -> b -> InstrSeq -> InstrSeq # open :: Alpha b => AlphaCtx -> b -> InstrSeq -> InstrSeq # isPat :: InstrSeq -> Maybe [AnyName] # isTerm :: InstrSeq -> Bool # isEmbed :: InstrSeq -> Bool # nthpatrec :: InstrSeq -> NthCont # findpatrec :: InstrSeq -> AnyName -> FindResult #
Display InstrSeq Source #
Methods display :: InstrSeq -> DM Doc Source #
(Sat (ctx0 Instruction), Sat (ctx0 InstrSeq), Sat (ctx0 SmallVal), Sat (ctx0 Ty)) => Rep1 ctx0 InstrSeq Source #
Methods rep1 :: R1 ctx0 InstrSeq #
Subst Ty InstrSeq Source #
Methods isvar :: InstrSeq -> Maybe (SubstName InstrSeq Ty) # isCoerceVar :: InstrSeq -> Maybe (SubstCoerce InstrSeq Ty) # subst :: Name Ty -> Ty -> InstrSeq -> InstrSeq # substs :: [(Name Ty, Ty)] -> InstrSeq -> InstrSeq # substPat :: AlphaCtx -> Ty -> InstrSeq -> InstrSeq # substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> InstrSeq -> InstrSeq #
Display (Heap, RegisterFile, InstrSeq) Source #
Methods display :: (Heap, RegisterFile, InstrSeq) -> DM Doc Source #

type Machine = (Heap, RegisterFile, InstrSeq) Source #

rInstrSeq1 :: forall ctx. (ctx Instruction, ctx InstrSeq) -> ctx SmallVal -> ctx Ty -> R1 ctx InstrSeq Source #

rInstrSeq :: R InstrSeq Source #

rInstruction1 :: forall ctx. (ctx Register, ctx Register, ctx SmallVal) -> (ctx Register, ctx SmallVal) -> (ctx Register, ctx Register, ctx Int) -> (ctx Register, ctx [Ty]) -> (ctx Register, ctx SmallVal) -> (ctx Register, ctx Register, ctx SmallVal) -> (ctx Register, ctx Int, ctx Register) -> (ctx Register, ctx Register, ctx SmallVal) -> (ctx TyName, ctx Register, ctx SmallVal) -> R1 ctx Instruction Source #

rInstruction :: R Instruction Source #

rHeapVal1 :: forall ctx. ctx [WordVal] -> (ctx [TyName], ctx Gamma, ctx InstrSeq) -> R1 ctx HeapVal Source #

rHeapVal :: R HeapVal Source #

rSmallVal1 :: forall ctx. ctx Register -> ctx WordVal -> ctx (TyApp SmallVal) -> ctx (Pack SmallVal) -> R1 ctx SmallVal Source #

rSmallVal :: R SmallVal Source #

rWordVal1 :: forall ctx. ctx Label -> ctx Int -> ctx Ty -> ctx (TyApp WordVal) -> ctx (Pack WordVal) -> R1 ctx WordVal Source #

rWordVal :: R WordVal Source #

rPack1 :: forall ctx a. Rep a => (ctx Ty, ctx a, ctx Ty) -> R1 ctx (Pack a) Source #

rPack :: forall a. Rep a => R (Pack a) Source #

rTyApp1 :: forall ctx a. Rep a => (ctx a, ctx Ty) -> R1 ctx (TyApp a) Source #

rTyApp :: forall a. Rep a => R (TyApp a) Source #

rLabel1 :: forall ctx. ctx (Name Heap) -> R1 ctx Label Source #

rLabel :: R Label Source #

rRegister1 :: forall ctx. ctx String -> R1 ctx Register Source #

rRegister :: R Register Source #

rFlag1 :: forall ctx. () -> () -> R1 ctx Flag Source #

rFlag :: R Flag Source #

rTy1 :: forall ctx. ctx TyName -> () -> ctx (Bind [TyName] Gamma) -> ctx [(Ty, Flag)] -> ctx (Bind TyName Ty) -> R1 ctx Ty Source #

rTy :: R Ty Source #

freshForHeap :: Heap -> Label Source #

getIntReg :: RegisterFile -> Register -> M Int Source #

arith :: (Int -> Int -> Int) -> RegisterFile -> Register -> SmallVal -> M WordVal Source #

loadReg :: RegisterFile -> SmallVal -> M (WordVal, [Ty]) Source #

tyApp :: WordVal -> [Ty] -> WordVal Source #

jmpReg :: Heap -> RegisterFile -> SmallVal -> M Machine Source #

step :: Machine -> M Machine Source #

run :: Machine -> M Machine Source #

type Delta = [TyName] Source #

data Ctx Source #

Constructors

Ctx
Fields getDelta :: Delta getGamma :: Gamma getPsi :: Psi

emptyCtx :: Ctx Source #

checkTyVar :: Ctx -> TyName -> M () Source #

extendTy :: TyName -> Ctx -> Ctx Source #

extendTys :: [TyName] -> Ctx -> Ctx Source #

insertGamma :: Register -> Ty -> Gamma -> Gamma Source #

lookupHeapLabel :: Ctx -> Label -> M Ty Source #

lookupReg :: Ctx -> Register -> M Ty Source #

tcty :: Ctx -> Ty -> M () Source #

tcPsi :: Ctx -> Psi -> M () Source #

tcGamma :: Ctx -> Gamma -> M () Source #

subtype :: Ctx -> Ty -> Ty -> M () Source #

subGamma :: Ctx -> Gamma -> Gamma -> M () Source #

typeCheckHeap :: Heap -> Psi -> M () Source #

H : Psi

tcWordVal :: Ctx -> WordVal -> M Ty Source #

tcApp :: (Ctx -> a -> M Ty) -> Ctx -> TyApp a -> M Ty Source #

tcPack :: Display a => (Ctx -> a -> M Ty) -> Ctx -> Pack a -> M Ty Source #

tcSmallVal :: Ctx -> SmallVal -> M Ty Source #

tcInstrSeq :: Ctx -> InstrSeq -> M () Source #

tcArith :: Ctx -> Register -> Register -> SmallVal -> M Ctx Source #

tcInstr :: Ctx -> Instruction -> M Ctx Source #

progcheck :: Machine -> M () Source #

dispArith :: (Display t, Show a1, Show a) => String -> a -> a1 -> t -> DM Doc Source #

Add Register Register SmallVal
Bnz Register SmallVal
Ld Register Register Int
Malloc Register [Ty]
Mov Register SmallVal
Mul Register Register SmallVal
St Register Int Register
Sub Register Register SmallVal
Unpack TyName Register SmallVal