diff options
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 228 |
1 files changed, 182 insertions, 46 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 98c0eaa28d..f2cedcdabb 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -13,20 +13,12 @@ open Names -(** {6 Value under universe substitution } *) -type 'a puniverses = 'a Univ.puniverses -[@@ocaml.deprecated "use Univ.puniverses"] - (** {6 Simply type aliases } *) type pconstant = Constant.t Univ.puniverses type pinductive = inductive Univ.puniverses type pconstructor = constructor Univ.puniverses (** {6 Existential variables } *) -type existential_key = Evar.t -[@@ocaml.deprecated "use Evar.t"] - -(** {6 Existential variables } *) type metavariable = int (** {6 Case annotation } *) @@ -122,7 +114,7 @@ val mkConst : Constant.t -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) -val mkProj : (projection * constr) -> constr +val mkProj : (Projection.t * constr) -> constr (** Inductive types *) @@ -136,6 +128,9 @@ val mkConstruct : constructor -> constr val mkConstructU : pconstructor -> constr val mkConstructUi : pinductive * int -> constr +(** Make a constant, inductive, constructor or variable. *) +val mkRef : GlobRef.t Univ.puniverses -> constr + (** Constructs a destructor of inductive type. [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] @@ -161,8 +156,26 @@ val mkCase : case_info * constr * constr * constr array -> constr where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) -type rec_declaration = Name.t array * types array * constr array -type fixpoint = (int array * int) * rec_declaration +type ('constr, 'types) prec_declaration = + Name.t array * 'types array * 'constr array +type ('constr, 'types) pfixpoint = + (int array * int) * ('constr, 'types) prec_declaration + (* The array of [int]'s tells for each component of the array of + mutual fixpoints the number of lambdas to skip before finding the + recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) + (v:=u) (w:I) {struct w}"), telling to skip x and z and that w is + the recursive argument); + The second component [int] tells which component of the block is + returned *) + +type ('constr, 'types) pcofixpoint = + int * ('constr, 'types) prec_declaration + (* The component [int] tells which component of the block of + cofixpoint is returned *) + +type rec_declaration = (constr, types) prec_declaration + +type fixpoint = (constr, types) pfixpoint val mkFix : fixpoint -> constr (** If [funnames = [|f1,.....fn|]] @@ -176,7 +189,7 @@ val mkFix : fixpoint -> constr ... with fn = bn.] *) -type cofixpoint = int * rec_declaration +type cofixpoint = (constr, types) pcofixpoint val mkCoFix : cofixpoint -> constr @@ -185,12 +198,6 @@ val mkCoFix : cofixpoint -> constr (** [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) type 'constr pexistential = Evar.t * 'constr array -type ('constr, 'types) prec_declaration = - Name.t array * 'types array * 'constr array -type ('constr, 'types) pfixpoint = - (int array * int) * ('constr, 'types) prec_declaration -type ('constr, 'types) pcofixpoint = - int * ('constr, 'types) prec_declaration type ('constr, 'types, 'sort, 'univs) kind_of_term = | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) @@ -220,7 +227,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative @@ -229,6 +236,11 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = val kind : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term val of_kind : (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -> constr +val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) + +val kind_nocast : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term + (** {6 Simple case analysis} *) val isRel : constr -> bool val isRelN : int -> constr -> bool @@ -273,8 +285,8 @@ val destMeta : constr -> metavariable (** Destructs a variable *) val destVar : constr -> Id.t -(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether - [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) +(** Destructs a sort. [is_Prop] recognizes the sort [Prop], whether + [isprop] recognizes both [Prop] and [Set]. *) val destSort : constr -> Sorts.t (** Destructs a casted term *) @@ -318,7 +330,7 @@ where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array (** Destructs a projection *) -val destProj : constr -> projection * constr +val destProj : constr -> Projection.t * constr (** Destructs the {% $ %}i{% $ %}th function of the block [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} @@ -331,6 +343,8 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint +val destRef : constr -> GlobRef.t Univ.puniverses + (** {6 Equality} *) (** [equal a b] is true if [a] equals [b] modulo alpha, casts, @@ -360,6 +374,105 @@ val eq_constr_nounivs : constr -> constr -> bool (** Total ordering compatible with [equal] *) val compare : constr -> constr -> int +(** {6 Extension of Context with declarations on constr} *) + +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_declaration = (constr, types) Context.Named.Declaration.pt +type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt +type rel_context = rel_declaration list +type named_context = named_declaration list +type compacted_context = compacted_declaration list + +(** {6 Relocation and substitution } *) + +(** [exliftn el c] lifts [c] with lifting [el] *) +val exliftn : Esubst.lift -> constr -> constr + +(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *) +val liftn : int -> int -> constr -> constr + +(** [lift n c] lifts by [n] the positive indexes in [c] *) +val lift : int -> constr -> constr + +(** {6 Functionals working on expressions canonically abstracted over + a local context (possibly with let-ins)} *) + +(** [map_under_context f l c] maps [f] on the immediate subterms of a + term abstracted over a context of length [n] (local definitions + are counted) *) + +val map_under_context : (constr -> constr) -> int -> constr -> constr + +(** [map_branches f br] maps [f] on the immediate subterms of an array + of "match" branches [br] in canonical eta-let-expanded form; it is + not recursive and the order with which subterms are processed is + not specified; it preserves sharing; the immediate subterms are the + types and possibly terms occurring in the context of each branch as + well as the body of each branch *) + +val map_branches : (constr -> constr) -> case_info -> constr array -> constr array + +(** [map_return_predicate f p] maps [f] on the immediate subterms of a + return predicate of a "match" in canonical eta-let-expanded form; + it is not recursive and the order with which subterms are processed + is not specified; it preserves sharing; the immediate subterms are + the types and possibly terms occurring in the context of each + branch as well as the body of the predicate *) + +val map_return_predicate : (constr -> constr) -> case_info -> constr -> constr + +(** [map_under_context_with_binders g f n l c] maps [f] on the + immediate subterms of a term abstracted over a context of length + [n] (local definitions are counted); it preserves sharing; it + carries an extra data [n] (typically a lift index) which is + processed by [g] (which typically add 1 to [n]) at each binder + traversal *) + +val map_under_context_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr + +(** [map_branches_with_binders f br] maps [f] on the immediate + subterms of an array of "match" branches [br] in canonical + eta-let-expanded form; it carries an extra data [n] (typically a + lift index) which is processed by [g] (which typically adds 1 to + [n]) at each binder traversal; it is not recursive and the order + with which subterms are processed is not specified; it preserves + sharing; the immediate subterms are the types and possibly terms + occurring in the context of the branch as well as the body of the + branch *) + +val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array + +(** [map_return_predicate_with_binders f p] maps [f] on the immediate + subterms of a return predicate of a "match" in canonical + eta-let-expanded form; it carries an extra data [n] (typically a + lift index) which is processed by [g] (which typically adds 1 to + [n]) at each binder traversal; it is not recursive and the order + with which subterms are processed is not specified; it preserves + sharing; the immediate subterms are the types and possibly terms + occurring in the context of each branch as well as the body of the + predicate *) + +val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr + +(** [map_under_context_with_full_binders g f n l c] is similar to + [map_under_context_with_binders] except that [g] takes also a full + binder as argument and that only the number of binders (and not + their signature) is required *) + +val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr + +(** [map_branches_with_full_binders g f l br] is equivalent to + [map_branches_with_binders] but using + [map_under_context_with_full_binders] *) + +val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array + +(** [map_return_predicate_with_full_binders g f l p] is equivalent to + [map_return_predicate_with_binders] but using + [map_under_context_with_full_binders] *) + +val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr + (** {6 Functionals working on the immediate subterm of a construction } *) (** [fold f acc c] folds [f] on the immediate subterms of [c] @@ -368,12 +481,23 @@ val compare : constr -> constr -> int val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a +val fold_with_full_binders : + (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b + (** [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) val map : (constr -> constr) -> constr -> constr +(** [map_user_view f c] maps [f] on the immediate subterms of [c]; it + differs from [map f c] in that the typing context and body of the + return predicate and of the branches of a [match] are considered as + immediate subterm of a [match] *) + +val map_user_view : (constr -> constr) -> constr -> constr + (** Like {!map}, but also has an additional accumulator. *) val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr @@ -402,50 +526,59 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit -type constr_compare_fn = int -> constr -> constr -> bool +(** [iter_with_binders g f n c] iters [f n] on the immediate + subterms of [c]; it carries an extra data [n] (typically a lift + index) which is processed by [g] (which typically add 1 to [n]) at + each binder traversal; it is not recursive and the order with which + subterms are processed is not specified *) + +val fold_constr_with_binders : + ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b + +type 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head : constr_compare_fn -> constr_compare_fn +val compare_head : constr constr_compare_fn -> constr constr_compare_fn (** Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .*) -type instance_compare_fn = global_reference -> int -> - Univ.Instance.t -> Univ.Instance.t -> bool +type 'univs instance_compare_fn = GlobRef.t -> int -> + 'univs -> 'univs -> bool (** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed, [u] to compare universe instances, [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen : instance_compare_fn -> +val compare_head_gen : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn val compare_head_gen_leq_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2] like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2]) is used,rather than {!kind}, to expose the immediate subterms of [c1] (resp. [c2]). *) val compare_head_gen_with : - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> - instance_compare_fn -> - (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + ('v -> ('v, 'v, 'sort, 'univs) kind_of_term) -> + 'univs instance_compare_fn -> + ('sort -> 'sort -> bool) -> + 'v constr_compare_fn -> + 'v constr_compare_fn (** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] for @@ -454,11 +587,11 @@ val compare_head_gen_with : [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen_leq : instance_compare_fn -> +val compare_head_gen_leq : Univ.Instance.t instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - constr_compare_fn -> - constr_compare_fn -> - constr_compare_fn + constr constr_compare_fn -> + constr constr_compare_fn -> + constr constr_compare_fn (** {6 Hashconsing} *) @@ -468,3 +601,6 @@ val case_info_hash : case_info -> int (*********************************************************************) val hcons : constr -> constr + +val debug_print : constr -> Pp.t +val debug_print_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t |