A

Documentation

type TyName = Name Ty

type ValName = Name Val

data Flag

Constructors

Un

Init

Instances

Eq Flag

Methods

(==) :: Flag -> Flag -> Bool

(/=) :: Flag -> Flag -> Bool

Ord Flag

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

Methods

showsPrec :: Int -> Flag -> ShowS

show :: Flag -> String

showList :: [Flag] -> ShowS

Rep Flag

Methods

rep :: R Flag

Alpha Flag

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

Methods

rep1 :: R1 ctx0 Flag

Subst Val Flag

Methods

isvar :: Flag -> Maybe (SubstName Flag Val)

isCoerceVar :: Flag -> Maybe (SubstCoerce Flag Val)

subst :: Name Val -> Val -> Flag -> Flag

substs :: [(Name Val, Val)] -> Flag -> Flag

substPat :: AlphaCtx -> Val -> Flag -> Flag

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Flag -> Flag

Subst Ty Flag

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)

Methods

display :: (Ty, Flag) -> DM Doc

data Ty

Constructors

TyVar TyName

TyInt

All (Bind [TyName] [Ty])

TyProd [(Ty, Flag)]

Exists (Bind TyName Ty)

Instances

Show Ty

Methods

showsPrec :: Int -> Ty -> ShowS

show :: Ty -> String

showList :: [Ty] -> ShowS

Rep Ty

Methods

rep :: R Ty

Alpha Ty

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

Methods

display :: Ty -> DM Doc

(Sat (ctx0 TyName), Sat (ctx0 (Bind [TyName] [Ty])), Sat (ctx0 [(Ty, Flag)]), Sat (ctx0 (Bind TyName Ty))) => Rep1 ctx0 Ty

Methods

rep1 :: R1 ctx0 Ty

Subst Val Ty

Methods

isvar :: Ty -> Maybe (SubstName Ty Val)

isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Val)

subst :: Name Val -> Val -> Ty -> Ty

substs :: [(Name Val, Val)] -> Ty -> Ty

substPat :: AlphaCtx -> Val -> Ty -> Ty

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Ty -> Ty

Subst Ty Prim

Methods

isvar :: Prim -> Maybe (SubstName Prim Ty)

isCoerceVar :: Prim -> Maybe (SubstCoerce Prim Ty)

subst :: Name Ty -> Ty -> Prim -> Prim

substs :: [(Name Ty, Ty)] -> Prim -> Prim

substPat :: AlphaCtx -> Ty -> Prim -> Prim

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Prim -> Prim

Subst Ty Tm

Methods

isvar :: Tm -> Maybe (SubstName Tm Ty)

isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Ty)

subst :: Name Ty -> Ty -> Tm -> Tm

substs :: [(Name Ty, Ty)] -> Tm -> Tm

substPat :: AlphaCtx -> Ty -> Tm -> Tm

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Tm -> Tm

Subst Ty Decl

Methods

isvar :: Decl -> Maybe (SubstName Decl Ty)

isCoerceVar :: Decl -> Maybe (SubstCoerce Decl Ty)

subst :: Name Ty -> Ty -> Decl -> Decl

substs :: [(Name Ty, Ty)] -> Decl -> Decl

substPat :: AlphaCtx -> Ty -> Decl -> Decl

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Decl -> Decl

Subst Ty Val

Methods

isvar :: Val -> Maybe (SubstName Val Ty)

isCoerceVar :: Val -> Maybe (SubstCoerce Val Ty)

subst :: Name Ty -> Ty -> Val -> Val

substs :: [(Name Ty, Ty)] -> Val -> Val

substPat :: AlphaCtx -> Ty -> Val -> Val

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Val -> Val

Subst Ty Ty

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 Flag

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 (Ann Val)

Methods

isvar :: Ann Val -> Maybe (SubstName (Ann Val) Ty)

isCoerceVar :: Ann Val -> Maybe (SubstCoerce (Ann Val) Ty)

subst :: Name Ty -> Ty -> Ann Val -> Ann Val

substs :: [(Name Ty, Ty)] -> Ann Val -> Ann Val

substPat :: AlphaCtx -> Ty -> Ann Val -> Ann Val

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Ann Val -> Ann Val

Display (Ty, Flag)

Methods

display :: (Ty, Flag) -> DM Doc

Display (ValName, Embed Ty)

Methods

display :: (ValName, Embed Ty) -> DM Doc

data Val

Constructors

TmInt Int

TmVar ValName

TApp (Ann Val) Ty

Pack Ty (Ann Val)

Instances

Show Val

Methods

showsPrec :: Int -> Val -> ShowS

show :: Val -> String

showList :: [Val] -> ShowS

Rep Val

Methods

rep :: R Val

Alpha Val

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Val -> Val

fv' :: Collection f => AlphaCtx -> Val -> f AnyName

lfreshen' :: LFresh m => AlphaCtx -> Val -> (Val -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Val -> m (Val, Perm AnyName)

aeq' :: AlphaCtx -> Val -> Val -> Bool

acompare' :: AlphaCtx -> Val -> Val -> Ordering

close :: Alpha b => AlphaCtx -> b -> Val -> Val

open :: Alpha b => AlphaCtx -> b -> Val -> Val

isPat :: Val -> Maybe [AnyName]

isTerm :: Val -> Bool

isEmbed :: Val -> Bool

nthpatrec :: Val -> NthCont

findpatrec :: Val -> AnyName -> FindResult

Display Val

Methods

display :: Val -> DM Doc

(Sat (ctx0 Int), Sat (ctx0 ValName), Sat (ctx0 (Ann Val)), Sat (ctx0 Ty)) => Rep1 ctx0 Val

Methods

rep1 :: R1 ctx0 Val

Subst Val Prim

Methods

isvar :: Prim -> Maybe (SubstName Prim Val)

isCoerceVar :: Prim -> Maybe (SubstCoerce Prim Val)

subst :: Name Val -> Val -> Prim -> Prim

substs :: [(Name Val, Val)] -> Prim -> Prim

substPat :: AlphaCtx -> Val -> Prim -> Prim

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Prim -> Prim

Subst Val Tm

Methods

isvar :: Tm -> Maybe (SubstName Tm Val)

isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Val)

subst :: Name Val -> Val -> Tm -> Tm

substs :: [(Name Val, Val)] -> Tm -> Tm

substPat :: AlphaCtx -> Val -> Tm -> Tm

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Tm -> Tm

Subst Val Decl

Methods

isvar :: Decl -> Maybe (SubstName Decl Val)

isCoerceVar :: Decl -> Maybe (SubstCoerce Decl Val)

subst :: Name Val -> Val -> Decl -> Decl

substs :: [(Name Val, Val)] -> Decl -> Decl

substPat :: AlphaCtx -> Val -> Decl -> Decl

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Decl -> Decl

Subst Val Val

Methods

isvar :: Val -> Maybe (SubstName Val Val)

isCoerceVar :: Val -> Maybe (SubstCoerce Val Val)

subst :: Name Val -> Val -> Val -> Val

substs :: [(Name Val, Val)] -> Val -> Val

substPat :: AlphaCtx -> Val -> Val -> Val

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Val -> Val

Subst Val Ty

Methods

isvar :: Ty -> Maybe (SubstName Ty Val)

isCoerceVar :: Ty -> Maybe (SubstCoerce Ty Val)

subst :: Name Val -> Val -> Ty -> Ty

substs :: [(Name Val, Val)] -> Ty -> Ty

substPat :: AlphaCtx -> Val -> Ty -> Ty

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Ty -> Ty

Subst Val Flag

Methods

isvar :: Flag -> Maybe (SubstName Flag Val)

isCoerceVar :: Flag -> Maybe (SubstCoerce Flag Val)

subst :: Name Val -> Val -> Flag -> Flag

substs :: [(Name Val, Val)] -> Flag -> Flag

substPat :: AlphaCtx -> Val -> Flag -> Flag

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Flag -> Flag

Subst Ty Val

Methods

isvar :: Val -> Maybe (SubstName Val Ty)

isCoerceVar :: Val -> Maybe (SubstCoerce Val Ty)

subst :: Name Ty -> Ty -> Val -> Val

substs :: [(Name Ty, Ty)] -> Val -> Val

substPat :: AlphaCtx -> Ty -> Val -> Val

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Val -> Val

Subst Val (Ann Val)

Methods

isvar :: Ann Val -> Maybe (SubstName (Ann Val) Val)

isCoerceVar :: Ann Val -> Maybe (SubstCoerce (Ann Val) Val)

subst :: Name Val -> Val -> Ann Val -> Ann Val

substs :: [(Name Val, Val)] -> Ann Val -> Ann Val

substPat :: AlphaCtx -> Val -> Ann Val -> Ann Val

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Ann Val -> Ann Val

Subst Ty (Ann Val)

Methods

isvar :: Ann Val -> Maybe (SubstName (Ann Val) Ty)

isCoerceVar :: Ann Val -> Maybe (SubstCoerce (Ann Val) Ty)

subst :: Name Ty -> Ty -> Ann Val -> Ann Val

substs :: [(Name Ty, Ty)] -> Ann Val -> Ann Val

substPat :: AlphaCtx -> Ty -> Ann Val -> Ann Val

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Ann Val -> Ann Val

Display (ValName, Embed Ty)

Methods

display :: (ValName, Embed Ty) -> DM Doc

data Ann v

Constructors

Ann v Ty

Instances

(Rep v0, Sat (ctx0 v0), Sat (ctx0 Ty)) => Rep1 ctx0 (Ann v0)

Methods

rep1 :: R1 ctx0 (Ann v0)

Subst Val (Ann Val)

Methods

isvar :: Ann Val -> Maybe (SubstName (Ann Val) Val)

isCoerceVar :: Ann Val -> Maybe (SubstCoerce (Ann Val) Val)

subst :: Name Val -> Val -> Ann Val -> Ann Val

substs :: [(Name Val, Val)] -> Ann Val -> Ann Val

substPat :: AlphaCtx -> Val -> Ann Val -> Ann Val

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Ann Val -> Ann Val

Subst Ty (Ann Val)

Methods

isvar :: Ann Val -> Maybe (SubstName (Ann Val) Ty)

isCoerceVar :: Ann Val -> Maybe (SubstCoerce (Ann Val) Ty)

subst :: Name Ty -> Ty -> Ann Val -> Ann Val

substs :: [(Name Ty, Ty)] -> Ann Val -> Ann Val

substPat :: AlphaCtx -> Ty -> Ann Val -> Ann Val

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Ann Val -> Ann Val

Show v => Show (Ann v)

Methods

showsPrec :: Int -> Ann v -> ShowS

show :: Ann v -> String

showList :: [Ann v] -> ShowS

Rep v0 => Rep (Ann v0)

Methods

rep :: R (Ann v0)

Alpha a => Alpha (Ann a)

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Ann a -> Ann a

fv' :: Collection f => AlphaCtx -> Ann a -> f AnyName

lfreshen' :: LFresh m => AlphaCtx -> Ann a -> (Ann a -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Ann a -> m (Ann a, Perm AnyName)

aeq' :: AlphaCtx -> Ann a -> Ann a -> Bool

acompare' :: AlphaCtx -> Ann a -> Ann a -> Ordering

close :: Alpha b => AlphaCtx -> b -> Ann a -> Ann a

open :: Alpha b => AlphaCtx -> b -> Ann a -> Ann a

isPat :: Ann a -> Maybe [AnyName]

isTerm :: Ann a -> Bool

isEmbed :: Ann a -> Bool

nthpatrec :: Ann a -> NthCont

findpatrec :: Ann a -> AnyName -> FindResult

Display a => Display (Ann a)

Methods

display :: Ann a -> DM Doc

data Decl

Constructors

DeclVar ValName (Embed (Ann Val))

DeclPrj Int ValName (Embed (Ann Val))

DeclPrim ValName (Embed (Ann Val, Prim, Ann Val))

DeclUnpack TyName ValName (Embed (Ann Val))

DeclMalloc ValName (Embed [Ty])

DeclAssign ValName (Embed (Ann Val, Int, Ann Val))

Instances

Show Decl

Methods

showsPrec :: Int -> Decl -> ShowS

show :: Decl -> String

showList :: [Decl] -> ShowS

Rep Decl

Methods

rep :: R Decl

Alpha Decl

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Decl -> Decl

fv' :: Collection f => AlphaCtx -> Decl -> f AnyName

lfreshen' :: LFresh m => AlphaCtx -> Decl -> (Decl -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Decl -> m (Decl, Perm AnyName)

aeq' :: AlphaCtx -> Decl -> Decl -> Bool

acompare' :: AlphaCtx -> Decl -> Decl -> Ordering

close :: Alpha b => AlphaCtx -> b -> Decl -> Decl

open :: Alpha b => AlphaCtx -> b -> Decl -> Decl

isPat :: Decl -> Maybe [AnyName]

isTerm :: Decl -> Bool

isEmbed :: Decl -> Bool

nthpatrec :: Decl -> NthCont

findpatrec :: Decl -> AnyName -> FindResult

Display Decl

Methods

display :: Decl -> DM Doc

(Sat (ctx0 ValName), Sat (ctx0 (Embed (Ann Val))), Sat (ctx0 Int), Sat (ctx0 (Embed (Ann Val, Prim, Ann Val))), Sat (ctx0 TyName), Sat (ctx0 (Embed [Ty])), Sat (ctx0 (Embed (Ann Val, Int, Ann Val)))) => Rep1 ctx0 Decl

Methods

rep1 :: R1 ctx0 Decl

Subst Val Decl

Methods

isvar :: Decl -> Maybe (SubstName Decl Val)

isCoerceVar :: Decl -> Maybe (SubstCoerce Decl Val)

subst :: Name Val -> Val -> Decl -> Decl

substs :: [(Name Val, Val)] -> Decl -> Decl

substPat :: AlphaCtx -> Val -> Decl -> Decl

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Decl -> Decl

Subst Ty Decl

Methods

isvar :: Decl -> Maybe (SubstName Decl Ty)

isCoerceVar :: Decl -> Maybe (SubstCoerce Decl Ty)

subst :: Name Ty -> Ty -> Decl -> Decl

substs :: [(Name Ty, Ty)] -> Decl -> Decl

substPat :: AlphaCtx -> Ty -> Decl -> Decl

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Decl -> Decl

data Tm

Constructors

Let (Bind Decl Tm)

App (Ann Val) [Ann Val]

TmIf0 (Ann Val) Tm Tm

Halt Ty (Ann Val)

Instances

Show Tm

Methods

showsPrec :: Int -> Tm -> ShowS

show :: Tm -> String

showList :: [Tm] -> ShowS

Rep Tm

Methods

rep :: R Tm

Alpha Tm

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Tm -> Tm

fv' :: Collection f => AlphaCtx -> Tm -> f AnyName

lfreshen' :: LFresh m => AlphaCtx -> Tm -> (Tm -> Perm AnyName -> m b) -> m b

freshen' :: Fresh m => AlphaCtx -> Tm -> m (Tm, Perm AnyName)

aeq' :: AlphaCtx -> Tm -> Tm -> Bool

acompare' :: AlphaCtx -> Tm -> Tm -> Ordering

close :: Alpha b => AlphaCtx -> b -> Tm -> Tm

open :: Alpha b => AlphaCtx -> b -> Tm -> Tm

isPat :: Tm -> Maybe [AnyName]

isTerm :: Tm -> Bool

isEmbed :: Tm -> Bool

nthpatrec :: Tm -> NthCont

findpatrec :: Tm -> AnyName -> FindResult

Display Tm

Methods

display :: Tm -> DM Doc

(Sat (ctx0 (Bind Decl Tm)), Sat (ctx0 (Ann Val)), Sat (ctx0 [Ann Val]), Sat (ctx0 Tm), Sat (ctx0 Ty)) => Rep1 ctx0 Tm

Methods

rep1 :: R1 ctx0 Tm

Subst Val Tm

Methods

isvar :: Tm -> Maybe (SubstName Tm Val)

isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Val)

subst :: Name Val -> Val -> Tm -> Tm

substs :: [(Name Val, Val)] -> Tm -> Tm

substPat :: AlphaCtx -> Val -> Tm -> Tm

substPats :: Proxy * Val -> AlphaCtx -> [Dyn] -> Tm -> Tm

Subst Ty Tm

Methods

isvar :: Tm -> Maybe (SubstName Tm Ty)

isCoerceVar :: Tm -> Maybe (SubstCoerce Tm Ty)

subst :: Name Ty -> Ty -> Tm -> Tm

substs :: [(Name Ty, Ty)] -> Tm -> Tm

substPat :: AlphaCtx -> Ty -> Tm -> Tm

substPats :: Proxy * Ty -> AlphaCtx -> [Dyn] -> Tm -> Tm

Display (Tm, Heap)

Methods

display :: (Tm, Heap) -> DM Doc

data HeapVal

Constructors

Tuple [Ann Val]

Code (Bind [TyName] (Bind [ValName] Tm))

Instances

Show HeapVal

Methods

showsPrec :: Int -> HeapVal -> ShowS

show :: HeapVal -> String

showList :: [HeapVal] -> ShowS

Rep HeapVal

Methods

rep :: R HeapVal

Display HeapVal

Methods

display :: HeapVal -> DM Doc

(Sat (ctx0 [Ann Val]), Sat (ctx0 (Bind [TyName] (Bind [ValName] Tm)))) => Rep1 ctx0 HeapVal

Methods

rep1 :: R1 ctx0 HeapVal

newtype Heap

Constructors

Heap (Map ValName (Ann HeapVal))

Instances

Show Heap

Methods

showsPrec :: Int -> Heap -> ShowS

show :: Heap -> String

showList :: [Heap] -> ShowS

Monoid Heap

Methods

mempty :: Heap

mappend :: Heap -> Heap -> Heap

mconcat :: [Heap] -> Heap

Display Heap

Methods

display :: Heap -> DM Doc

Display (Tm, Heap)

Methods

display :: (Tm, Heap) -> DM Doc

rTm1 :: forall ctx. ctx (Bind Decl Tm) -> (ctx (Ann Val), ctx [Ann Val]) -> (ctx (Ann Val), ctx Tm, ctx Tm) -> (ctx Ty, ctx (Ann Val)) -> R1 ctx Tm

rTm :: R Tm

rDecl1 :: forall ctx. (ctx ValName, ctx (Embed (Ann Val))) -> (ctx Int, ctx ValName, ctx (Embed (Ann Val))) -> (ctx ValName, ctx (Embed (Ann Val, Prim, Ann Val))) -> (ctx TyName, ctx ValName, ctx (Embed (Ann Val))) -> (ctx ValName, ctx (Embed [Ty])) -> (ctx ValName, ctx (Embed (Ann Val, Int, Ann Val))) -> R1 ctx Decl

rDecl :: R Decl

rAnn1 :: forall ctx v. Rep v => (ctx v, ctx Ty) -> R1 ctx (Ann v)

rAnn :: forall v. Rep v => R (Ann v)

rVal1 :: forall ctx. ctx Int -> ctx ValName -> (ctx (Ann Val), ctx Ty) -> (ctx Ty, ctx (Ann Val)) -> R1 ctx Val

rVal :: R Val

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

rTy :: R Ty

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

rFlag :: R Flag

rHeapVal1 :: forall ctx. ctx [Ann Val] -> ctx (Bind [TyName] (Bind [ValName] Tm)) -> R1 ctx HeapVal

rHeapVal :: R HeapVal

mkTyApp :: (MonadError String m, Fresh m) => Ann Val -> [Ty] -> m (Ann Val)

lets :: [Decl] -> Tm -> Tm

x :: Name Tm

y :: Name Tm

z :: Name Tm

a :: Name Ty

b :: Name Ty

c :: Name Ty

type Delta = [TyName]

type Gamma = [(ValName, Ty)]

data Ctx

Constructors

Ctx

Fields

• getDelta :: Delta
• getGamma :: Gamma

emptyCtx :: Ctx

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

lookupTmVar :: Ctx -> ValName -> M Ty

extendTy :: TyName -> Ctx -> Ctx

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

extendTm :: ValName -> Ty -> Ctx -> Ctx

extendTms :: [ValName] -> [Ty] -> Ctx -> Ctx

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

typecheckHeapVal :: Ctx -> Ann HeapVal -> M Ty

typecheckVal :: Ctx -> Val -> M Ty

typecheckAnnVal :: Ctx -> Ann Val -> ExceptT String FreshM Ty

typecheckDecl :: Ctx -> Decl -> ExceptT String FreshM Ctx

typecheck :: Ctx -> Tm -> M ()

progcheck :: (Tm, Heap) -> ExceptT String FreshM ()