summaryrefslogtreecommitdiff
path: root/pretyping/rawterm.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /pretyping/rawterm.mli
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'pretyping/rawterm.mli')
-rw-r--r--pretyping/rawterm.mli35
1 files changed, 14 insertions, 21 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index eecee8b0..b2b70bc9 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: rawterm.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id$ i*)
(*i*)
open Util
@@ -46,7 +46,7 @@ type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
-type 'a bindings =
+type 'a bindings =
| ImplicitBindings of 'a list
| ExplicitBindings of 'a explicit_bindings
| NoBindings
@@ -57,7 +57,7 @@ type 'a cast_type =
| CastConv of cast_kind * 'a
| CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
-type rawconstr =
+type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
| REvar of loc * existential_key * rawconstr list option
@@ -67,7 +67,7 @@ type rawconstr =
| RProd of loc * name * binding_kind * rawconstr * rawconstr
| RLetIn of loc * name * rawconstr * rawconstr
| RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
- | RLetTuple of loc * name list * (name * rawconstr option) *
+ | RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
| RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
| RRec of loc * fix_kind * identifier array * rawdecl list array *
@@ -79,7 +79,7 @@ type rawconstr =
and rawdecl = name * binding_kind * rawconstr option * rawconstr
-and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option
and fix_kind =
| RFix of ((int option * fix_recursion_order) array * int)
@@ -98,21 +98,14 @@ and cases_clauses = cases_clause list
val cases_predicate_names : tomatch_tuples -> name list
-(*i - if PRec (_, names, arities, bodies) is in env then arities are
- typed in env too and bodies are typed in env enriched by the
- arities incrementally lifted
-
- [On pourrait plutot mettre les arités aves le type qu'elles auront
- dans le contexte servant à typer les body ???]
-
- - boolean in POldCase means it is recursive
- - option in PHole tell if the "?" was apparent or has been implicitely added
-i*)
-
val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
+(** Ensure traversal from left to right *)
+val map_rawconstr_left_to_right :
+ (rawconstr -> rawconstr) -> rawconstr -> rawconstr
+
(*i
-val map_rawconstr_with_binders_loc : loc ->
+val map_rawconstr_with_binders_loc : loc ->
(identifier -> 'a -> identifier * 'a) ->
('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
i*)
@@ -155,10 +148,10 @@ val no_occurrences_expr : occurrences_expr
type 'a with_occurrences = occurrences_expr * 'a
-type ('a,'b) red_expr_gen =
+type ('a,'b,'c) red_expr_gen =
| Red of bool
| Hnf
- | Simpl of 'a with_occurrences option
+ | Simpl of 'c with_occurrences option
| Cbv of 'b raw_red_flag
| Lazy of 'b raw_red_flag
| Unfold of 'b with_occurrences list
@@ -167,8 +160,8 @@ type ('a,'b) red_expr_gen =
| ExtraRedExpr of string
| CbvVm
-type ('a,'b) may_eval =
+type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
- | ConstrEval of ('a,'b) red_expr_gen * 'a
+ | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
| ConstrContext of (loc * identifier) * 'a
| ConstrTypeOf of 'a