Language.IntrinsicTyping.STLCR

The content of this module is based on the MSc Thesis
Coinductive Formalization of SECD Machine in Agda
by Adam Krupička

Definitions

data STLCR : List (Ty, Ty) -> List Ty -> Ty -> Type

Totality: total
Visibility: public export
Constructors:

Var : Elem ty g -> STLCR r g ty

Lam : STLCR ((a, b) :: r) (a :: g) b -> STLCR r g (TyFun a b)

App : STLCR r g (TyFun a b) -> STLCR r g a -> STLCR r g b

Rec : Elem (a, b) r -> STLCR r g (TyFun a b)

If : STLCR r g TyBool -> STLCR r g a -> STLCR r g a -> STLCR r g a

Eqb : STLCR r g a -> STLCR r g a -> STLCR r g TyBool

Lit : Const ty -> STLCR r g ty

Add : STLCR r g TyInt -> STLCR r g TyInt -> STLCR r g TyInt

Sub : STLCR r g TyInt -> STLCR r g TyInt -> STLCR r g TyInt

Mul : STLCR r g TyInt -> STLCR r g TyInt -> STLCR r g TyInt

fromInteger : Integer -> STLCR r g TyInt

Totality: total
Visibility: public export

compile : STLCR r g ty -> Steps (MkState s g r) (MkState (ty :: s) g r)

Totality: total
Visibility: public export

compileT : STLCR ((a, b) :: r) (a :: g) b -> Steps (MkState [] (a :: g) ((a, b) :: r)) (MkState [b] (a :: g) ((a, b) :: r))

Totality: total
Visibility: public export

compileAcc : Stepz init (MkState s g r) -> STLCR r g ty -> Stepz init (MkState (ty :: s) g r)

Totality: total
Visibility: public export