Language.IntrinsicTyping.SECD(source)

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

Reexports

import public Data.Late
import public Data.List.Quantifiers

Definitions

data Ty : Type

Totality: total
Visibility: public export
Constructors:

TyInt : Ty
TyBool : Ty
TyPair : Ty -> Ty -> Ty
TyList : Ty -> Ty
TyFun : Ty -> Ty -> Ty

data Const : Ty -> Type

Totality: total
Visibility: public export
Constructors:

AnInt : Int -> Const TyInt
True : Const TyBool
False : Const TyBool

fromInteger : Integer -> Const TyInt

Totality: total
Visibility: public export

Stack : Type

Totality: total
Visibility: public export

Env : Type

Totality: total
Visibility: public export

FunDump : Type

Totality: total
Visibility: public export

record State : Type

Totality: total
Visibility: public export
Constructor:

MkState : Stack -> Env -> FunDump -> State

Projections:

.dump : State -> FunDump
.env : State -> Env
.stack : State -> Stack

.stack : State -> Stack

Totality: total
Visibility: public export

stack : State -> Stack

Totality: total
Visibility: public export

.env : State -> Env

Totality: total
Visibility: public export

env : State -> Env

Totality: total
Visibility: public export

.dump : State -> FunDump

Totality: total
Visibility: public export

dump : State -> FunDump

Totality: total
Visibility: public export

data Step : State -> State -> Type

Totality: total
Visibility: public export
Constructors:

LDC : Const ty -> Step (MkState s e f) (MkState (ty :: s) e f)

  Load a constant of a base type

LDA : Elem ty e -> Step (MkState s e f) (MkState (ty :: s) e f)

  Load a value from an address in the environment

LDF : Steps (MkState [] (a :: e) ((a, b) :: f)) (MkState [b] (a :: e) ((a, b) :: f)) -> Step (MkState s e f) (MkState (TyFun a b :: s) e f)

  Load a recursive function

LDR : Elem (a, b) f -> Step (MkState s e f) (MkState (TyFun a b :: s) e f)

  Load a function for recursive application

APP : Step (MkState (a :: (TyFun a b :: s)) e f) (MkState (b :: s) e f)

  Apply a function to its argument

TAP : Step (MkState (a :: (TyFun a b :: s)) e f) (MkState (b :: s) e f)

  Apply a function to its argument, tail call

RTN : Step (MkState (b :: s) e ((a, b) :: f)) (MkState [b] e ((a, b) :: f))

  Return a value from inside a function

BCH : Steps (MkState s e f) (MkState s' e f) -> Steps (MkState s e f) (MkState s' e f) -> Step (MkState (TyBool :: s) e f) (MkState s' e f)

  Branch over a boolean

FLP : Step (MkState (a :: (b :: s)) e f) (MkState (b :: (a :: s)) e f)

  Flip the stack's top values

NIL : Step (MkState s e f) (MkState (TyList a :: s) e f)

  Nil constructor

CNS : Step (MkState (a :: (TyList a :: s)) e f) (MkState (TyList a :: s) e f)

  Cons constructor

HED : Step (MkState (TyList a :: s) e f) (MkState (a :: s) e f)

  Head destructor

TAL : Step (MkState (TyList a :: s) e f) (MkState (TyList a :: s) e f)

  Tail destructor

MKP : Step (MkState (a :: (b :: s)) e f) (MkState (TyPair a b :: s) e f)

  Pair constructor

FST : Step (MkState (TyPair a b :: s) e f) (MkState (a :: s) e f)

  First pair destructor

SND : Step (MkState (TyPair a b :: s) e f) (MkState (b :: s) e f)

  Second pair destructor

ADD : Step (MkState (TyInt :: (TyInt :: s)) e f) (MkState (TyInt :: s) e f)

  Addition of ints

SUB : Step (MkState (TyInt :: (TyInt :: s)) e f) (MkState (TyInt :: s) e f)

  Subtraction of ints

MUL : Step (MkState (TyInt :: (TyInt :: s)) e f) (MkState (TyInt :: s) e f)

  Multiplication of ints

EQB : Step (MkState (a :: (a :: s)) e f) (MkState (TyBool :: s) e f)

  Structural equality test

NOT : Step (MkState (TyBool :: s) e f) (MkState (TyBool :: s) e f)

  Boolean negation

data Steps : State -> State -> Type

Totality: total
Visibility: public export
Constructors:

Nil : Steps s s
(::) : Step s t -> Steps t u -> Steps s u

data Stepz : State -> State -> Type

Totality: total
Visibility: public export
Constructors:

Lin : Stepz s s
(:<) : Stepz s t -> Step t u -> Stepz s u

(<>>) : Stepz s t -> Steps t u -> Steps s u

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 6

(<><) : Stepz s t -> Steps t u -> Stepz s u

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 7

(++) : Steps s t -> Steps t u -> Steps s u

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

NUL : Steps (MkState (TyList a :: s) e f) (MkState (TyBool :: s) e f)

Totality: total
Visibility: public export

LDL : List Int -> Steps (MkState s e f) (MkState (TyList TyInt :: s) e f)

Totality: total
Visibility: public export

PLS : Step (MkState s e f) (MkState (TyFun TyInt (TyFun TyInt TyInt) :: s) e f)

Totality: total
Visibility: public export

MAP : Step (MkState [] e f) (MkState [TyFun (TyFun a b) (TyFun (TyList a) (TyList b))] e f)

Totality: total
Visibility: public export

FLD : Step (MkState [] e f) (MkState [TyFun (TyFun b (TyFun a b)) (TyFun b (TyFun (TyList a) b))] e f)

Totality: total
Visibility: public export

SUM : Steps (MkState [] e f) (MkState [TyFun (TyList TyInt) TyInt] e f)

Totality: total
Visibility: public export

Meaning : Ty -> Type

Totality: total
Visibility: public export

fromConst : Const ty -> Meaning ty

Totality: total
Visibility: public export

Meaning : List Ty -> Type

Totality: total
Visibility: public export

0 Meaning : FunDump -> Type

Totality: total
Visibility: public export

tail : Meaning (ab :: f) -> Meaning f

Totality: total
Visibility: public export

lookup : Meaning f -> Elem (a, b) f -> Closure a b

Totality: total
Visibility: public export

record Meaning : State -> Type

Totality: total
Visibility: public export
Constructor:

MkMeaning : Meaning (st .stack) -> Meaning (st .env) -> Meaning (st .dump) -> Meaning st

Projections:

.dumpVal : Meaning st -> Meaning (st .dump)
.envVal : Meaning st -> Meaning (st .env)
.stackVal : Meaning st -> Meaning (st .stack)

.stackVal : Meaning st -> Meaning (st .stack)

Totality: total
Visibility: public export

stackVal : Meaning st -> Meaning (st .stack)

Totality: total
Visibility: public export

.envVal : Meaning st -> Meaning (st .env)

Totality: total
Visibility: public export

envVal : Meaning st -> Meaning (st .env)

Totality: total
Visibility: public export

.dumpVal : Meaning st -> Meaning (st .dump)

Totality: total
Visibility: public export

dumpVal : Meaning st -> Meaning (st .dump)

Totality: total
Visibility: public export

record Closure : Ty -> Ty -> Type

Totality: total
Visibility: public export
Constructor:

MkClosure : Steps (MkState [] (a :: localEnv) ((a, b) :: localFunDump)) (MkState [b] (a :: localEnv) ((a, b) :: localFunDump)) -> Meaning localEnv -> Meaning localFunDump -> Closure a b

Projections:

.code : ({rec:0} : Closure a b) -> Steps (MkState [] (a :: localEnv {rec:0}) ((a, b) :: localFunDump {rec:0})) (MkState [b] (a :: localEnv {rec:0}) ((a, b) :: localFunDump {rec:0}))
.dumpVal : ({rec:0} : Closure a b) -> Meaning (localFunDump {rec:0})
.envVal : ({rec:0} : Closure a b) -> Meaning (localEnv {rec:0})
0 .localEnv : Closure a b -> Env
0 .localFunDump : Closure a b -> FunDump

0 .localEnv : Closure a b -> Env

Totality: total
Visibility: public export

0 localEnv : Closure a b -> Env

Totality: total
Visibility: public export

0 .localFunDump : Closure a b -> FunDump

Totality: total
Visibility: public export

0 localFunDump : Closure a b -> FunDump

Totality: total
Visibility: public export

.code : ({rec:0} : Closure a b) -> Steps (MkState [] (a :: localEnv {rec:0}) ((a, b) :: localFunDump {rec:0})) (MkState [b] (a :: localEnv {rec:0}) ((a, b) :: localFunDump {rec:0}))

Totality: total
Visibility: public export

code : ({rec:0} : Closure a b) -> Steps (MkState [] (a :: localEnv {rec:0}) ((a, b) :: localFunDump {rec:0})) (MkState [b] (a :: localEnv {rec:0}) ((a, b) :: localFunDump {rec:0}))

Totality: total
Visibility: public export

.envVal : ({rec:0} : Closure a b) -> Meaning (localEnv {rec:0})

Totality: total
Visibility: public export

envVal : ({rec:0} : Closure a b) -> Meaning (localEnv {rec:0})

Totality: total
Visibility: public export

.dumpVal : ({rec:0} : Closure a b) -> Meaning (localFunDump {rec:0})

Totality: total
Visibility: public export

dumpVal : ({rec:0} : Closure a b) -> Meaning (localFunDump {rec:0})

Totality: total
Visibility: public export

eqb : (ty : Ty) -> Meaning ty -> Meaning ty -> Bool

Totality: total
Visibility: public export

eqbs : (ty : Ty) -> Meaning (TyList ty) -> Meaning (TyList ty) -> Bool

Totality: total
Visibility: public export

steps : Meaning st -> Steps st st' -> Late (Meaning st')

Totality: total
Visibility: public export

step : Meaning st -> Step st st' -> Late (Meaning st')

Totality: total
Visibility: public export

run : Steps (MkState [] [] []) (MkState (ty :: {_:12217}) [] []) -> Nat -> Maybe (Meaning ty)

Totality: total
Visibility: public export