summaryrefslogtreecommitdiff
path: root/checker/closure.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /checker/closure.mli
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'checker/closure.mli')
-rw-r--r--checker/closure.mli32
1 files changed, 5 insertions, 27 deletions
diff --git a/checker/closure.mli b/checker/closure.mli
index 12cee770..428197fa 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-2012 *)
(* \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