summaryrefslogtreecommitdiff
path: root/kernel/closure.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /kernel/closure.mli
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'kernel/closure.mli')
-rw-r--r--kernel/closure.mli207
1 files changed, 207 insertions, 0 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli
new file mode 100644
index 00000000..e58b91eb
--- /dev/null
+++ b/kernel/closure.mli
@@ -0,0 +1,207 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: closure.mli,v 1.42.2.1 2004/07/16 19:30:24 herbelin Exp $ i*)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Environ
+open Esubst
+(*i*)
+
+(* Flags for profiling reductions. *)
+val stats : bool ref
+val share : bool ref
+
+val with_stats: 'a Lazy.t -> 'a
+
+(*s Delta implies all consts (both global (= by
+ [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
+ Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
+ a LetIn expression is Letin reduction *)
+
+type transparent_state = Idpred.t * KNpred.t
+
+val all_opaque : transparent_state
+val all_transparent : transparent_state
+
+(* Sets of reduction kinds. *)
+module type RedFlagsSig = sig
+ type reds
+ type red_kind
+
+ (* The different kind of reduction *)
+ (* Const/Var means the reference as argument should be unfolded *)
+ (* Constbut/Varbut means all references except the ones as argument
+ of Constbut/Varbut should be unfolded (there may be several such
+ Constbut/Varbut *)
+ val fBETA : red_kind
+ val fDELTA : red_kind
+ val fIOTA : red_kind
+ val fZETA : red_kind
+ val fCONST : constant -> red_kind
+ val fVAR : identifier -> red_kind
+
+ (* No reduction at all *)
+ val no_red : reds
+
+ (* Adds a reduction kind to a set *)
+ val red_add : reds -> red_kind -> reds
+
+ (* Removes a reduction kind to a set *)
+ val red_sub : reds -> red_kind -> reds
+
+ (* Adds a reduction kind to a set *)
+ val red_add_transparent : reds -> transparent_state -> reds
+
+ (* Build a reduction set from scratch = iter [red_add] on [no_red] *)
+ val mkflags : red_kind list -> reds
+
+ (* Tests if a reduction kind is set *)
+ val red_set : reds -> red_kind -> bool
+
+ (* Gives the constant list *)
+ val red_get_const : reds -> bool * evaluable_global_reference list
+end
+
+module RedFlags : RedFlagsSig
+open RedFlags
+
+val beta : reds
+val betaiota : reds
+val betadeltaiota : reds
+val betaiotazeta : reds
+val betadeltaiotanolet : reds
+
+val unfold_red : evaluable_global_reference -> reds
+
+(************************************************************************)
+
+type table_key =
+ | ConstKey of constant
+ | VarKey of identifier
+ | FarRelKey of int
+ (* FarRel: index in the [rel_context] part of {\em initial} environment *)
+
+type 'a infos
+val ref_value_cache: 'a infos -> table_key -> 'a option
+val info_flags: 'a infos -> reds
+val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
+
+(************************************************************************)
+(*s A [stack] is a context of arguments, arguments are pushed by
+ [append_stack] one array at a time but popped with [decomp_stack]
+ one by one *)
+
+type 'a stack_member =
+ | Zapp of 'a list
+ | Zcase of case_info * 'a * 'a array
+ | Zfix of 'a * 'a stack
+ | Zshift of int
+ | Zupdate of 'a
+
+and 'a stack = 'a stack_member list
+
+val empty_stack : 'a stack
+val append_stack : 'a array -> 'a stack -> 'a stack
+
+val decomp_stack : 'a stack -> ('a * 'a stack) option
+val list_of_stack : 'a stack -> 'a list
+val array_of_stack : 'a stack -> 'a array
+val stack_assign : 'a stack -> int -> 'a -> 'a stack
+val stack_args_size : 'a stack -> int
+val app_stack : constr * constr stack -> constr
+val stack_tail : int -> 'a stack -> 'a stack
+val stack_nth : 'a stack -> int -> 'a
+
+(************************************************************************)
+(*s Lazy reduction. *)
+
+(* [fconstr] is the type of frozen constr *)
+
+type fconstr
+
+(* [fconstr] can be accessed by using the function [fterm_of] and by
+ matching on type [fterm] *)
+
+type fterm =
+ | FRel of int
+ | FAtom of constr (* Metas and Sorts *)
+ | FCast of fconstr * fconstr
+ | FFlex of table_key
+ | FInd of inductive
+ | FConstruct of constructor
+ | FApp of fconstr * fconstr array
+ | FFix of fixpoint * fconstr subs
+ | FCoFix of cofixpoint * fconstr subs
+ | FCases of case_info * fconstr * fconstr * fconstr array
+ | FLambda of int * (name * constr) list * constr * fconstr subs
+ | FProd of name * fconstr * fconstr
+ | FLetIn of name * fconstr * fconstr * constr * fconstr subs
+ | FEvar of existential_key * fconstr array
+ | FLIFT of int * fconstr
+ | FCLOS of constr * fconstr subs
+ | FLOCKED
+
+(* To lazy reduce a constr, create a [clos_infos] with
+ [create_clos_infos], inject the term to reduce with [inject]; then use
+ a reduction function *)
+
+val inject : constr -> fconstr
+val fterm_of : fconstr -> fterm
+val term_of_fconstr : fconstr -> constr
+val destFLambda :
+ (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
+
+(* Global and local constant cache *)
+type clos_infos
+val create_clos_infos : reds -> env -> clos_infos
+
+(* Reduction function *)
+
+(* [norm_val] is for strong normalization *)
+val norm_val : clos_infos -> fconstr -> constr
+
+(* [whd_val] is for weak head normalization *)
+val whd_val : clos_infos -> fconstr -> constr
+
+(* [whd_stack] performs weak head normalization in a given stack. It
+ stops whenever a reduction is blocked. *)
+val whd_stack :
+ clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+
+(* Conversion auxiliary functions to do step by step normalisation *)
+
+(* [unfold_reference] unfolds references in a [fconstr] *)
+val unfold_reference : clos_infos -> table_key -> fconstr option
+
+(* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
+val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
+
+(************************************************************************)
+(*i This is for lazy debug *)
+
+val lift_fconstr : int -> fconstr -> fconstr
+val lift_fconstr_vect : int -> fconstr array -> fconstr array
+
+val mk_clos : fconstr subs -> constr -> fconstr
+val mk_clos_vect : fconstr subs -> constr array -> fconstr array
+val mk_clos_deep :
+ (fconstr subs -> constr -> fconstr) ->
+ fconstr subs -> constr -> fconstr
+
+val kni: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+val knr: clos_infos -> fconstr -> fconstr stack -> fconstr * fconstr stack
+val kl : clos_infos -> fconstr -> constr
+
+val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
+val optimise_closure : fconstr subs -> constr -> fconstr subs * constr
+
+(* End of cbn debug section i*)