summaryrefslogtreecommitdiff
path: root/pretyping/glob_term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/glob_term.mli')
-rw-r--r--pretyping/glob_term.mli167
1 files changed, 167 insertions, 0 deletions
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
new file mode 100644
index 00000000..798a960f
--- /dev/null
+++ b/pretyping/glob_term.mli
@@ -0,0 +1,167 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <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 *)
+(************************************************************************)
+
+(**Untyped intermediate terms, after constr_expr and before constr
+
+ Resolution of names, insertion of implicit arguments placeholder,
+ and notations are done, but coercions, inference of implicit
+ arguments and pattern-matching compilation are not. *)
+
+open Util
+open Names
+open Sign
+open Term
+open Libnames
+open Nametab
+
+(** The kind of patterns that occurs in "match ... with ... end"
+
+ locs here refers to the ident's location, not whole pat *)
+type cases_pattern =
+ | PatVar of loc * name
+ | PatCstr of loc * constructor * cases_pattern list * name
+ (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
+
+val cases_pattern_loc : cases_pattern -> loc
+
+type patvar = identifier
+
+type glob_sort = GProp of Term.contents | GType of Univ.universe option
+
+type binding_kind = Lib.binding_kind = Explicit | Implicit
+
+type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
+
+type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
+
+type 'a bindings =
+ | ImplicitBindings of 'a list
+ | ExplicitBindings of 'a explicit_bindings
+ | NoBindings
+
+type 'a with_bindings = 'a * 'a bindings
+
+type 'a cast_type =
+ | CastConv of cast_kind * 'a
+ | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
+
+type glob_constr =
+ | GRef of (loc * global_reference)
+ | GVar of (loc * identifier)
+ | GEvar of loc * existential_key * glob_constr list option
+ | GPatVar of loc * (bool * patvar) (** Used for patterns only *)
+ | GApp of loc * glob_constr * glob_constr list
+ | GLambda of loc * name * binding_kind * glob_constr * glob_constr
+ | GProd of loc * name * binding_kind * glob_constr * glob_constr
+ | GLetIn of loc * name * glob_constr * glob_constr
+ | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses
+ (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in
+ [MatchStyle]) *)
+
+ | GLetTuple of loc * name list * (name * glob_constr option) *
+ glob_constr * glob_constr
+ | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr
+ | GRec of loc * fix_kind * identifier array * glob_decl list array *
+ glob_constr array * glob_constr array
+ | GSort of loc * glob_sort
+ | GHole of (loc * Evd.hole_kind)
+ | GCast of loc * glob_constr * glob_constr cast_type
+
+and glob_decl = name * binding_kind * glob_constr option * glob_constr
+
+and fix_recursion_order = GStructRec | GWfRec of glob_constr | GMeasureRec of glob_constr * glob_constr option
+
+and fix_kind =
+ | GFix of ((int option * fix_recursion_order) array * int)
+ | GCoFix of int
+
+and predicate_pattern =
+ name * (loc * inductive * int * name list) option
+ (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)], [k]
+ is the number of parameter of [I]. *)
+
+and tomatch_tuple = (glob_constr * predicate_pattern)
+
+and tomatch_tuples = tomatch_tuple list
+
+and cases_clause = (loc * identifier list * cases_pattern list * glob_constr)
+(** [(p,il,cl,t)] = "|'cl' as 'il' => 't'" *)
+
+and cases_clauses = cases_clause list
+
+val cases_predicate_names : tomatch_tuples -> name list
+
+(* Apply one argument to a glob_constr *)
+val mkGApp : loc -> glob_constr -> glob_constr -> glob_constr
+
+val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr
+
+(* Ensure traversal from left to right *)
+val map_glob_constr_left_to_right :
+ (glob_constr -> glob_constr) -> glob_constr -> glob_constr
+
+(*
+val map_glob_constr_with_binders_loc : loc ->
+ (identifier -> 'a -> identifier * 'a) ->
+ ('a -> glob_constr -> glob_constr) -> 'a -> glob_constr -> glob_constr
+*)
+
+val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
+val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
+val occur_glob_constr : identifier -> glob_constr -> bool
+val free_glob_vars : glob_constr -> identifier list
+val loc_of_glob_constr : glob_constr -> loc
+
+(** Conversion from glob_constr to cases pattern, if possible
+
+ Take the current alias as parameter,
+ @raise Not_found if translation is impossible *)
+val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern
+
+val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr
+
+(** {6 Reduction expressions} *)
+
+type 'a glob_red_flag = {
+ rBeta : bool;
+ rIota : bool;
+ rZeta : bool;
+ rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
+ rConst : 'a list
+}
+
+val all_flags : 'a glob_red_flag
+
+type 'a or_var = ArgArg of 'a | ArgVar of identifier located
+
+type occurrences_expr = bool * int or_var list
+
+val all_occurrences_expr_but : int or_var list -> occurrences_expr
+val no_occurrences_expr_but : int or_var list -> occurrences_expr
+val all_occurrences_expr : occurrences_expr
+val no_occurrences_expr : occurrences_expr
+
+type 'a with_occurrences = occurrences_expr * 'a
+
+type ('a,'b,'c) red_expr_gen =
+ | Red of bool
+ | Hnf
+ | Simpl of 'c with_occurrences option
+ | Cbv of 'b glob_red_flag
+ | Lazy of 'b glob_red_flag
+ | Unfold of 'b with_occurrences list
+ | Fold of 'a list
+ | Pattern of 'a with_occurrences list
+ | ExtraRedExpr of string
+ | CbvVm
+
+type ('a,'b,'c) may_eval =
+ | ConstrTerm of 'a
+ | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
+ | ConstrContext of (loc * identifier) * 'a
+ | ConstrTypeOf of 'a