K

Documentation

type TyName = Name Ty

type ValName = Name Val

data Ty

Constructors

TyVar TyName

TyInt

All (Bind [TyName] [Ty])

TyProd [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])) => 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 AnnVal

Methods

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

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

subst :: Name Ty -> Ty -> AnnVal -> AnnVal

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

substPat :: AlphaCtx -> Ty -> AnnVal -> AnnVal

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

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

Display (ValName, Embed Ty)

Methods

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

data Val

Constructors

TmInt Int

TmVar ValName

Fix (Bind (ValName, [TyName]) (Bind [(ValName, Embed Ty)] Tm))

TmProd [AnnVal]

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 (Bind (ValName, [TyName]) (Bind [(ValName, Embed Ty)] Tm))), Sat (ctx0 [AnnVal])) => 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 AnnVal

Methods

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

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

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

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

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

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

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 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

Display (ValName, Embed Ty)

Methods

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

data AnnVal

Constructors

Ann Val Ty

Instances

Show AnnVal

Methods

showsPrec :: Int -> AnnVal -> ShowS

show :: AnnVal -> String

showList :: [AnnVal] -> ShowS

Rep AnnVal

Methods

rep :: R AnnVal

Alpha AnnVal

Methods

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

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

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

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

aeq' :: AlphaCtx -> AnnVal -> AnnVal -> Bool

acompare' :: AlphaCtx -> AnnVal -> AnnVal -> Ordering

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

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

isPat :: AnnVal -> Maybe [AnyName]

isTerm :: AnnVal -> Bool

isEmbed :: AnnVal -> Bool

nthpatrec :: AnnVal -> NthCont

findpatrec :: AnnVal -> AnyName -> FindResult

Display AnnVal

Methods

display :: AnnVal -> DM Doc

(Sat (ctx0 Val), Sat (ctx0 Ty)) => Rep1 ctx0 AnnVal

Methods

rep1 :: R1 ctx0 AnnVal

Subst Val AnnVal

Methods

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

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

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

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

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

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

Subst Ty AnnVal

Methods

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

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

subst :: Name Ty -> Ty -> AnnVal -> AnnVal

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

substPat :: AlphaCtx -> Ty -> AnnVal -> AnnVal

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

data Decl

Constructors

DeclVar ValName (Embed AnnVal)

DeclPrj Int ValName (Embed AnnVal)

DeclPrim ValName (Embed (AnnVal, Prim, AnnVal))

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 AnnVal)), Sat (ctx0 Int), Sat (ctx0 (Embed (AnnVal, Prim, AnnVal)))) => 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 AnnVal [Ty] [AnnVal]

TmIf0 AnnVal Tm Tm

Halt Ty AnnVal

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 AnnVal), Sat (ctx0 [Ty]), Sat (ctx0 [AnnVal]), 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

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

rTm :: R Tm

rDecl1 :: forall ctx. (ctx ValName, ctx (Embed AnnVal)) -> (ctx Int, ctx ValName, ctx (Embed AnnVal)) -> (ctx ValName, ctx (Embed (AnnVal, Prim, AnnVal))) -> R1 ctx Decl

rDecl :: R Decl

rAnnVal1 :: forall ctx. (ctx Val, ctx Ty) -> R1 ctx AnnVal

rAnnVal :: R AnnVal

rVal1 :: forall ctx. ctx Int -> ctx ValName -> ctx (Bind (ValName, [TyName]) (Bind [(ValName, Embed Ty)] Tm)) -> ctx [AnnVal] -> R1 ctx Val

rVal :: R Val

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

rTy :: R Ty

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

typecheckVal :: Ctx -> Val -> M Ty

typecheckAnnVal :: Ctx -> AnnVal -> ExceptT String FreshM Ty

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

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

mkSubst :: Decl -> M (Tm -> Tm)

step :: Tm -> M Tm

evaluate :: Tm -> M Val