diff options
| author | barras | 2003-08-05 17:16:58 +0000 |
|---|---|---|
| committer | barras | 2003-08-05 17:16:58 +0000 |
| commit | ef14e67d209edf4581223c6de4c38a79e4831940 (patch) | |
| tree | 7012a9b32a16a14b765c03e76e4f32415f55ec86 /kernel/closure.mli | |
| parent | 8235d977028498a99d8c3c097f6fd2094298f3ff (diff) | |
Improved reduction machine with closure: should use less memory
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 19 |
1 files changed, 9 insertions, 10 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 4442e49f9f..8c80324238 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -133,26 +133,23 @@ type fconstr type fterm = | FRel of int - | FAtom of constr + | 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 (int array * int) * (name array * fconstr array * fconstr array) - * constr array * fconstr subs - | FCoFix of int * (name array * fconstr array * fconstr array) - * constr array * fconstr subs + | FFix of fixpoint * fconstr subs + | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array - | FLambda of name * fconstr * fconstr * constr * fconstr subs - | FProd of name * fconstr * fconstr * constr * fconstr subs - | FLetIn of name * fconstr * fconstr * fconstr * constr * fconstr subs + | 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 *) @@ -160,6 +157,8 @@ type fterm = 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 @@ -200,7 +199,7 @@ val mk_clos_deep : 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 -> fconstr +val kl : clos_infos -> fconstr -> constr val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr |