diff options
Diffstat (limited to 'kernel/closure.mli')
-rw-r--r-- | kernel/closure.mli | 65 |
1 files changed, 32 insertions, 33 deletions
diff --git a/kernel/closure.mli b/kernel/closure.mli index 706a089e..feec8395 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: closure.mli 7639 2005-12-02 10:01:15Z gregoire $ i*) +(*i $Id: closure.mli 8793 2006-05-05 17:41:41Z barras $ i*) (*i*) open Pp @@ -91,33 +91,6 @@ 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 -val zip_term : ('a -> constr) -> constr -> 'a stack -> constr - -(************************************************************************) (*s Lazy reduction. *) (* [fconstr] is the type of frozen constr *) @@ -146,17 +119,43 @@ type fterm = | FCLOS of constr * fconstr subs | FLOCKED +(************************************************************************) +(*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 stack_member = + | Zapp of fconstr array + | Zcase of case_info * fconstr * fconstr array + | Zfix of fconstr * stack + | Zshift of int + | Zupdate of fconstr + +and stack = stack_member list + +val empty_stack : stack +val append_stack : fconstr array -> stack -> stack + +val decomp_stack : stack -> (fconstr * stack) option +val array_of_stack : stack -> fconstr array +val stack_assign : stack -> int -> fconstr -> stack +val stack_args_size : stack -> int +val stack_tail : int -> stack -> stack +val stack_nth : stack -> int -> fconstr +val zip_term : (fconstr -> constr) -> constr -> stack -> constr + (* 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 +(* mk_atom: prevents a term from being evaluated *) +val mk_atom : constr -> fconstr + val fterm_of : fconstr -> fterm val term_of_fconstr : fconstr -> constr val destFLambda : (fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr -(* mk_atom: prevents a term from being evaluated *) -val mk_atom : constr -> fconstr (* Global and local constant cache *) type clos_infos @@ -173,7 +172,7 @@ 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 + clos_infos -> fconstr -> stack -> fconstr * stack (* Conversion auxiliary functions to do step by step normalisation *) @@ -195,8 +194,8 @@ 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 kni: clos_infos -> fconstr -> stack -> fconstr * stack +val knr: clos_infos -> fconstr -> stack -> fconstr * stack val kl : clos_infos -> fconstr -> constr val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr |