Idris2Doc : Language.IntrinsicTyping.Krivine
Index
Default
Alternative
Black & White
Definitions data Ty : Type
Totality : total Visibility : public export Constructors : Base : Ty
Arr : Ty -> Ty -> Ty
Context : Type
Totality : total Visibility : public export data Term : Context -> Ty -> Type
Totality : total Visibility : public export Constructors : Lam : Term (a :: g ) b -> Term g (Arr a b )
App : Term g (Arr a b ) -> Term g a -> Term g b
Var : Elem a g -> Term g a
data Closed : Ty -> Type
Totality : total Visibility : public export Constructors : Closure : Term g a -> Env g -> Closed a
ClApp : Closed (Arr a b ) -> Closed a -> Closed b
data Env : Context -> Type
Totality : total Visibility : public export Constructors : Nil : Env []
(::) : Closed a -> Env g -> Env (a :: g )
data IsValue : Closed g -> Type
Totality : total Visibility : public export Constructor : Lam : IsValue (Closure (Lam b ) env )
data Value : Ty -> Type
Totality : total Visibility : public export Constructor : Val : (c : Closed a ) -> IsValue c -> Value a
data Redex : Ty -> Type
Totality : total Visibility : public export Constructors : RVar : Elem a g -> Env g -> Redex a
RApp : Term g (Arr a b ) -> Term g a -> Env g -> Redex b
Beta : Term (a :: g ) b -> Env g -> Closed a -> Redex b
redex : Redex a -> Closed a
Totality : total Visibility : public export lookup : Env g -> Elem a g -> Closed a
Totality : total Visibility : public export contract : Redex a -> Closed a
Totality : total Visibility : public export data EvalContext : Ty -> Ty -> Type
Totality : total Visibility : public export Constructors : Nil : EvalContext inner inner
(::) : Closed a -> EvalContext inner outer -> EvalContext (Arr a inner ) outer
snoc : EvalContext inner (Arr dom outer ) -> Closed dom -> EvalContext inner outer
Totality : total Visibility : public export data SnocView : EvalContext inner outer -> Type
Totality : total Visibility : public export Constructors : Lin : SnocView []
(:<) : (ctx : EvalContext inner (Arr dom outer )) -> (t : Closed dom ) -> SnocView (snoc ctx t )
snocView : (ctx : EvalContext inner outer ) -> SnocView ctx
Totality : total Visibility : public export plug : EvalContext a b -> Closed a -> Closed b
Totality : total Visibility : public export 0 plugSnoc : (ctx : EvalContext a (Arr dom b )) -> (t : Closed dom ) -> (f : Closed a ) -> plug (snoc ctx t ) f = ClApp (plug ctx f ) t
Totality : total Visibility : public export data Decomposition : Closed a -> Type
Totality : total Visibility : public export Constructors : Val : (sc : Term (a :: g ) b ) -> (env : Env g ) -> Decomposition (Closure (Lam sc ) env )
Red : (r : Redex s ) -> (ctx : EvalContext s t ) -> Decomposition (plug ctx (redex r ))
load : (ctx : EvalContext a b ) -> (c : Closed a ) -> Decomposition (plug ctx c )
Totality : total Visibility : public export unload : (ctx : EvalContext (Arr a b ) outer ) -> (sc : Term (a :: g ) b ) -> (env : Env g ) -> Decomposition (plug ctx (Closure (Lam sc ) env ))
Totality : total Visibility : public export decompose : (c : Closed a ) -> Decomposition c
Totality : total Visibility : public export decomposePlug : (ctx : EvalContext a b ) -> (c : Closed a ) -> decompose (plug ctx c ) = load ctx c
Totality : total Visibility : public export recompose : Decomposition c -> Closed a
Totality : total Visibility : public export headReduce : Closed a -> Closed a
Totality : total Visibility : public export loadRedex : (ctx : EvalContext a b ) -> (r : Redex a ) -> load ctx (redex r ) = Red r ctx
Totality : total Visibility : public export headReducePlug : (ctx : EvalContext a b ) -> (r : Redex a ) -> headReduce (plug ctx (redex r )) = plug ctx (contract r )
Totality : total Visibility : public export headReduceClApp : (f : Closed (Arr a b )) -> Not (IsValue f ) -> (t : Closed a ) -> headReduce (ClApp f t ) = ClApp (headReduce f ) t
Totality : total Visibility : public export data Trace : Decomposition c -> Type
Totality : total Visibility : public export Constructors : Done : (sc : Term ({a:5061} :: {g:5060} ) {b:5059} ) -> (env : Env {g:5060} ) -> Trace (Val sc env )
Step : (ctx : EvalContext a b ) -> (r : Redex a ) -> Trace (decompose (plug ctx (contract r ))) -> Trace (Red r ctx )
iterate : (0 _ : Trace d ) -> Value a
Totality : total Visibility : public export Reducible : (a : Ty ) -> Closed a -> Type
Totality : total Visibility : public export data ReducibleEnv : Env g -> Type
Totality : total Visibility : public export Constructors : Nil : ReducibleEnv []
(::) : Reducible a t -> ReducibleEnv env -> ReducibleEnv (t :: env )
lookup : ReducibleEnv env -> (v : Elem a g ) -> Reducible a (lookup env v )
Totality : total Visibility : public export step : Trace (decompose (headReduce c )) -> Trace (decompose c )
Totality : total Visibility : public export expand : Reducible a (headReduce c ) -> Reducible a c
Totality : total Visibility : public export closure : (t : Term g a ) -> ReducibleEnv env -> Reducible a (Closure t env )
Totality : total Visibility : public export theorem : (c : Closed a ) -> Reducible a c
Totality : total Visibility : public export theoremEnv : (env : Env g ) -> ReducibleEnv env
Totality : total Visibility : public export termination : (c : Closed a ) -> Trace (decompose c )
Totality : total Visibility : public export evaluate : Closed a -> Value a
Totality : total Visibility : public export refocus : (ctx : EvalContext a b ) -> (c : Closed a ) -> Decomposition (plug ctx c )
Totality : total Visibility : public export refocusCorrect : (ctx : EvalContext a b ) -> (c : Closed a ) -> refocus ctx c = decompose (plug ctx c )
Totality : total Visibility : public export data Trace : Decomposition c -> Type
Totality : total Visibility : public export Constructors : Done : (0 sc : Term ({a:6073} :: {g:6072} ) {b:6071} ) -> (0 env : Env {g:6072} ) -> Trace (Val sc env )
Step : (0 ctx : EvalContext a b ) -> (0 r : Redex a ) -> Trace (refocus ctx (contract r )) -> Trace (Red r ctx )
trace : Trace d -> (0 _ : e = d ) -> Trace e
Totality : total Visibility : public export termination : (c : Closed a ) -> Trace (decompose c )
Totality : total Visibility : public export iterate : (0 _ : Trace d ) -> Value a
Totality : total Visibility : public export evaluate : Closed a -> Value a
Totality : total Visibility : public export IsValidEnv : Env g -> Type
Totality : total Visibility : public export IsValidClosed : Closed a -> Type
Totality : total Visibility : public export ValidEnv : Context -> Type
Totality : total Visibility : public export ValidClosed : Ty -> Type
Totality : total Visibility : public export Closure : Term g a -> ValidEnv g -> ValidClosed a
Totality : total Visibility : public export fstClosure : (t : Term g a ) -> (env : ValidEnv g ) -> fst (Closure t env ) = Closure t (fst env )
Totality : total Visibility : public export 0 getContext : ValidClosed a -> Context
Totality : total Visibility : public export getEnv : (c : ValidClosed a ) -> ValidEnv (getContext c )
Totality : total Visibility : public export getTerm : (c : ValidClosed a ) -> Term (getContext c ) a
Totality : total Visibility : public export etaValidClosed : (c : ValidClosed a ) -> c = Closure (getTerm c ) (getEnv c )
Totality : total Visibility : public export lookup : ValidEnv g -> Elem a g -> ValidClosed a
Totality : total Visibility : public export fstLookup : (env : ValidEnv g ) -> (v : Elem a g ) -> fst (lookup env v ) = lookup (fst env ) v
Totality : total Visibility : public export Nil : ValidEnv []
Totality : total Visibility : public export (::) : ValidClosed a -> ValidEnv g -> ValidEnv (a :: g )
Totality : total Visibility : public export Fixity Declaration : infixr operator, level 7 IsValidEvalContext : EvalContext a b -> Type
Totality : total Visibility : public export ValidEvalContext : Ty -> Ty -> Type
Totality : total Visibility : public export Nil : ValidEvalContext a a
Totality : total Visibility : public export (::) : ValidClosed a -> ValidEvalContext b c -> ValidEvalContext (Arr a b ) c
Totality : total Visibility : public export Fixity Declaration : infixr operator, level 7 fstCons : (t : ValidClosed a ) -> (ctx : ValidEvalContext b c ) -> fst (t :: ctx ) = fst t :: fst ctx
Totality : total Visibility : public export data View : ValidEvalContext a b -> Type
Totality : total Visibility : public export Constructors : Nil : View []
(::) : (t : ValidClosed a ) -> (ctx : ValidEvalContext b c ) -> View (t :: ctx )
irrelevantUnit : (t : ()) -> t = ()
Totality : total Visibility : public export etaPair : (p : (a , b )) -> p = (fst p , snd p )
Totality : total Visibility : public export view : (ctx : ValidEvalContext a b ) -> View ctx
Totality : total Visibility : public export data Trace : Term g a -> ValidEnv g -> ValidEvalContext a b -> Type
Totality : total Visibility : public export Constructors : Var : Trace (getTerm (lookup env v )) (getEnv (lookup env v )) ctx -> Trace (Var v ) env ctx
App : Trace f env (Closure t env :: ctx ) -> Trace (f `App ` t ) env ctx
Beta : Trace sc (arg :: env ) ctx -> Trace (Lam sc ) env (arg :: ctx )
Done : Trace (Lam sc ) env []
vvar : (tr : Trace (Var v ) env ctx ) -> (tr' : Trace (getTerm (lookup env v )) (getEnv (lookup env v )) ctx ** tr = Var tr' )
Totality : total Visibility : public export vapp : (tr : Trace (f `App ` t ) env ctx ) -> (tr' : Trace f env (Closure t env :: ctx ) ** tr = (tr' `App `))
Totality : total Visibility : public export Fixity Declaration : infixl operator, level 5 vlam0 : ctx = [] -> (tr : Trace (Lam sc ) env ctx ) -> tr = Done
Totality : total Visibility : public export vlamS : ctx = arg :: ctx' -> (tr : Trace (Lam sc ) env ctx ) -> (tr' : Trace sc (arg :: env ) ctx' ** tr = Beta tr' )
Totality : total Visibility : public export view : (t : Term g a ) -> (env : ValidEnv g ) -> (ctx : ValidEvalContext a b ) -> (0 tr : Trace t env ctx ) -> View tr
Totality : total Visibility : public export refocus : (0 _ : Trace t env ctx ) -> Value b
Totality : total Visibility : public export correctness : (ctx : ValidEvalContext a b ) -> (t : Term g a ) -> (env : ValidEnv g ) -> (trold : Trace (refocus (fst ctx ) (Closure t (fst env )))) -> (trnew : Trace t env ctx ) -> refocus trnew = iterate trold
Totality : total Visibility : public export trace : (ctx : ValidEvalContext a b ) -> (t : Term g a ) -> (env : ValidEnv g ) -> Trace (refocus (fst ctx ) (Closure t (fst env ))) -> Trace t env ctx
Totality : total Visibility : public export termination : (t : Term [] a ) -> Trace t [] []
Totality : total Visibility : public export evaluate : Term [] a -> Value a
Totality : total Visibility : public export Produced by Idris 2 version 0.7.0-2ff3231b5