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:5049} :: {g:5048} ) {b:5047} ) -> (env : Env {g:5048} ) -> 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:6061} :: {g:6060} ) {b:6059} ) -> (0 env : Env {g:6060} ) -> 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.8.0-8c970f1ba