diff options
Diffstat (limited to 'checker/closure.mli')
| -rw-r--r-- | checker/closure.mli | 32 |
1 files changed, 5 insertions, 27 deletions
diff --git a/checker/closure.mli b/checker/closure.mli index 12cee770..707a51f9 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: closure.mli 9902 2007-06-21 17:01:21Z herbelin $ i*) - (*i*) open Pp open Names @@ -32,6 +30,9 @@ type transparent_state = Idpred.t * Cpred.t val all_opaque : transparent_state val all_transparent : transparent_state +val is_transparent_variable : transparent_state -> variable -> bool +val is_transparent_constant : transparent_state -> constant -> bool + (* Sets of reduction kinds. *) module type RedFlagsSig = sig type reds @@ -51,33 +52,20 @@ module type RedFlagsSig = sig (* 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 @@ -86,7 +74,6 @@ type table_key = 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 (************************************************************************) @@ -132,23 +119,14 @@ type stack_member = 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 eta_expand_stack : stack -> stack (* 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 |