Idris2Doc : Language.IntrinsicTyping.Krivine

Language.IntrinsicTyping.Krivine(source)

The content of this module is based on the paper
From Mathematics to Abstract Machine
A formal derivation of an executable Krivine machine
by Wouter Swierstra

Definitions

dataTy : Type
Totality: total
Visibility: public export
Constructors:
Base : Ty
Arr : Ty->Ty->Ty
Context : Type
Totality: total
Visibility: public export
dataTerm : Context->Ty->Type
Totality: total
Visibility: public export
Constructors:
Lam : Term (a::g) b->Termg (Arrab)
App : Termg (Arrab) ->Termga->Termgb
Var : Elemag->Termga
dataClosed : Ty->Type
Totality: total
Visibility: public export
Constructors:
Closure : Termga->Envg->Closeda
ClApp : Closed (Arrab) ->Closeda->Closedb
dataEnv : Context->Type
Totality: total
Visibility: public export
Constructors:
Nil : Env []
(::) : Closeda->Envg->Env (a::g)
dataIsValue : Closedg->Type
Totality: total
Visibility: public export
Constructor: 
Lam : IsValue (Closure (Lamb) env)
dataValue : Ty->Type
Totality: total
Visibility: public export
Constructor: 
Val : (c : Closeda) ->IsValuec->Valuea
dataRedex : Ty->Type
Totality: total
Visibility: public export
Constructors:
RVar : Elemag->Envg->Redexa
RApp : Termg (Arrab) ->Termga->Envg->Redexb
Beta : Term (a::g) b->Envg->Closeda->Redexb
redex : Redexa->Closeda
Totality: total
Visibility: public export
lookup : Envg->Elemag->Closeda
Totality: total
Visibility: public export
contract : Redexa->Closeda
Totality: total
Visibility: public export
dataEvalContext : Ty->Ty->Type
Totality: total
Visibility: public export
Constructors:
Nil : EvalContextinnerinner
(::) : Closeda->EvalContextinnerouter->EvalContext (Arrainner) outer
snoc : EvalContextinner (Arrdomouter) ->Closeddom->EvalContextinnerouter
Totality: total
Visibility: public export
dataSnocView : EvalContextinnerouter->Type
Totality: total
Visibility: public export
Constructors:
Lin : SnocView []
(:<) : (ctx : EvalContextinner (Arrdomouter)) -> (t : Closeddom) ->SnocView (snocctxt)
snocView : (ctx : EvalContextinnerouter) ->SnocViewctx
Totality: total
Visibility: public export
plug : EvalContextab->Closeda->Closedb
Totality: total
Visibility: public export
0plugSnoc : (ctx : EvalContexta (Arrdomb)) -> (t : Closeddom) -> (f : Closeda) ->plug (snocctxt) f=ClApp (plugctxf) t
Totality: total
Visibility: public export
dataDecomposition : Closeda->Type
Totality: total
Visibility: public export
Constructors:
Val : (sc : Term (a::g) b) -> (env : Envg) ->Decomposition (Closure (Lamsc) env)
Red : (r : Redexs) -> (ctx : EvalContextst) ->Decomposition (plugctx (redexr))
load : (ctx : EvalContextab) -> (c : Closeda) ->Decomposition (plugctxc)
Totality: total
Visibility: public export
unload : (ctx : EvalContext (Arrab) outer) -> (sc : Term (a::g) b) -> (env : Envg) ->Decomposition (plugctx (Closure (Lamsc) env))
Totality: total
Visibility: public export
decompose : (c : Closeda) ->Decompositionc
Totality: total
Visibility: public export
decomposePlug : (ctx : EvalContextab) -> (c : Closeda) ->decompose (plugctxc) =loadctxc
Totality: total
Visibility: public export
recompose : Decompositionc->Closeda
Totality: total
Visibility: public export
headReduce : Closeda->Closeda
Totality: total
Visibility: public export
loadRedex : (ctx : EvalContextab) -> (r : Redexa) ->loadctx (redexr) =Redrctx
Totality: total
Visibility: public export
headReducePlug : (ctx : EvalContextab) -> (r : Redexa) ->headReduce (plugctx (redexr)) =plugctx (contractr)
Totality: total
Visibility: public export
headReduceClApp : (f : Closed (Arrab)) ->Not (IsValuef) -> (t : Closeda) ->headReduce (ClAppft) =ClApp (headReducef) t
Totality: total
Visibility: public export
dataTrace : Decompositionc->Type
Totality: total
Visibility: public export
Constructors:
Done : (sc : Term ({a:5061}::{g:5060}) {b:5059}) -> (env : Env{g:5060}) ->Trace (Valscenv)
Step : (ctx : EvalContextab) -> (r : Redexa) ->Trace (decompose (plugctx (contractr))) ->Trace (Redrctx)
iterate : (0_ : Traced) ->Valuea
Totality: total
Visibility: public export
Reducible : (a : Ty) ->Closeda->Type
Totality: total
Visibility: public export
dataReducibleEnv : Envg->Type
Totality: total
Visibility: public export
Constructors:
Nil : ReducibleEnv []
(::) : Reducibleat->ReducibleEnvenv->ReducibleEnv (t::env)
lookup : ReducibleEnvenv-> (v : Elemag) ->Reduciblea (lookupenvv)
Totality: total
Visibility: public export
step : Trace (decompose (headReducec)) ->Trace (decomposec)
Totality: total
Visibility: public export
expand : Reduciblea (headReducec) ->Reducibleac
Totality: total
Visibility: public export
closure : (t : Termga) ->ReducibleEnvenv->Reduciblea (Closuretenv)
Totality: total
Visibility: public export
theorem : (c : Closeda) ->Reducibleac
Totality: total
Visibility: public export
theoremEnv : (env : Envg) ->ReducibleEnvenv
Totality: total
Visibility: public export
termination : (c : Closeda) ->Trace (decomposec)
Totality: total
Visibility: public export
evaluate : Closeda->Valuea
Totality: total
Visibility: public export
refocus : (ctx : EvalContextab) -> (c : Closeda) ->Decomposition (plugctxc)
Totality: total
Visibility: public export
refocusCorrect : (ctx : EvalContextab) -> (c : Closeda) ->refocusctxc=decompose (plugctxc)
Totality: total
Visibility: public export
dataTrace : Decompositionc->Type
Totality: total
Visibility: public export
Constructors:
Done : (0sc : Term ({a:6073}::{g:6072}) {b:6071}) -> (0env : Env{g:6072}) ->Trace (Valscenv)
Step : (0ctx : EvalContextab) -> (0r : Redexa) ->Trace (refocusctx (contractr)) ->Trace (Redrctx)
trace : Traced-> (0_ : e=d) ->Tracee
Totality: total
Visibility: public export
termination : (c : Closeda) ->Trace (decomposec)
Totality: total
Visibility: public export
iterate : (0_ : Traced) ->Valuea
Totality: total
Visibility: public export
evaluate : Closeda->Valuea
Totality: total
Visibility: public export
IsValidEnv : Envg->Type
Totality: total
Visibility: public export
IsValidClosed : Closeda->Type
Totality: total
Visibility: public export
ValidEnv : Context->Type
Totality: total
Visibility: public export
ValidClosed : Ty->Type
Totality: total
Visibility: public export
Closure : Termga->ValidEnvg->ValidCloseda
Totality: total
Visibility: public export
fstClosure : (t : Termga) -> (env : ValidEnvg) ->fst (Closuretenv) =Closuret (fstenv)
Totality: total
Visibility: public export
0getContext : ValidCloseda->Context
Totality: total
Visibility: public export
getEnv : (c : ValidCloseda) ->ValidEnv (getContextc)
Totality: total
Visibility: public export
getTerm : (c : ValidCloseda) ->Term (getContextc) a
Totality: total
Visibility: public export
etaValidClosed : (c : ValidCloseda) ->c=Closure (getTermc) (getEnvc)
Totality: total
Visibility: public export
lookup : ValidEnvg->Elemag->ValidCloseda
Totality: total
Visibility: public export
fstLookup : (env : ValidEnvg) -> (v : Elemag) ->fst (lookupenvv) =lookup (fstenv) v
Totality: total
Visibility: public export
Nil : ValidEnv []
Totality: total
Visibility: public export
(::) : ValidCloseda->ValidEnvg->ValidEnv (a::g)
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
IsValidEvalContext : EvalContextab->Type
Totality: total
Visibility: public export
ValidEvalContext : Ty->Ty->Type
Totality: total
Visibility: public export
Nil : ValidEvalContextaa
Totality: total
Visibility: public export
(::) : ValidCloseda->ValidEvalContextbc->ValidEvalContext (Arrab) c
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7
fstCons : (t : ValidCloseda) -> (ctx : ValidEvalContextbc) ->fst (t::ctx) =fstt::fstctx
Totality: total
Visibility: public export
dataView : ValidEvalContextab->Type
Totality: total
Visibility: public export
Constructors:
Nil : View []
(::) : (t : ValidCloseda) -> (ctx : ValidEvalContextbc) ->View (t::ctx)
irrelevantUnit : (t : ()) ->t= ()
Totality: total
Visibility: public export
etaPair : (p : (a, b)) ->p= (fstp, sndp)
Totality: total
Visibility: public export
view : (ctx : ValidEvalContextab) ->Viewctx
Totality: total
Visibility: public export
dataTrace : Termga->ValidEnvg->ValidEvalContextab->Type
Totality: total
Visibility: public export
Constructors:
Var : Trace (getTerm (lookupenvv)) (getEnv (lookupenvv)) ctx->Trace (Varv) envctx
App : Tracefenv (Closuretenv::ctx) ->Trace (f `App` t) envctx
Beta : Tracesc (arg::env) ctx->Trace (Lamsc) env (arg::ctx)
Done : Trace (Lamsc) env []
vvar : (tr : Trace (Varv) envctx) -> (tr' : Trace (getTerm (lookupenvv)) (getEnv (lookupenvv)) ctx**tr=Vartr')
Totality: total
Visibility: public export
vapp : (tr : Trace (f `App` t) envctx) -> (tr' : Tracefenv (Closuretenv::ctx) **tr= (tr' `App`))
Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 5
vlam0 : ctx= [] -> (tr : Trace (Lamsc) envctx) ->tr=Done
Totality: total
Visibility: public export
vlamS : ctx=arg::ctx'-> (tr : Trace (Lamsc) envctx) -> (tr' : Tracesc (arg::env) ctx'**tr=Betatr')
Totality: total
Visibility: public export
view : (t : Termga) -> (env : ValidEnvg) -> (ctx : ValidEvalContextab) -> (0tr : Tracetenvctx) ->Viewtr
Totality: total
Visibility: public export
refocus : (0_ : Tracetenvctx) ->Valueb
Totality: total
Visibility: public export
correctness : (ctx : ValidEvalContextab) -> (t : Termga) -> (env : ValidEnvg) -> (trold : Trace (refocus (fstctx) (Closuret (fstenv)))) -> (trnew : Tracetenvctx) ->refocustrnew=iteratetrold
Totality: total
Visibility: public export
trace : (ctx : ValidEvalContextab) -> (t : Termga) -> (env : ValidEnvg) ->Trace (refocus (fstctx) (Closuret (fstenv))) ->Tracetenvctx
Totality: total
Visibility: public export
termination : (t : Term [] a) ->Tracet [] []
Totality: total
Visibility: public export
evaluate : Term [] a->Valuea
Totality: total
Visibility: public export