diff options
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 238 |
1 files changed, 188 insertions, 50 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 42d298e3..c1d1f988 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the most important datatype of Coq, namely kernel terms, @@ -13,20 +15,22 @@ 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 puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses +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 } *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle +type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) type case_printing = { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *) @@ -70,7 +74,7 @@ type types = constr (** {6 Term constructors. } *) -(** Constructs a DeBrujin index (DB indices begin at 1) *) +(** Constructs a de Bruijn index (DB indices begin at 1) *) val mkRel : int -> constr (** Constructs a Variable *) @@ -80,14 +84,14 @@ val mkVar : Id.t -> constr val mkMeta : metavariable -> constr (** Constructs an existential variable *) -type existential = existential_key * constr array +type existential = Evar.t * constr array val mkEvar : existential -> constr (** Construct a sort *) val mkSort : Sorts.t -> types val mkProp : types val mkSet : types -val mkType : Univ.universe -> types +val mkType : Univ.Universe.t -> types (** This defines the strategy to use for verifiying a Cast *) @@ -111,14 +115,14 @@ val mkLetIn : Name.t * constr * types * constr -> constr {%latex:$(f~t_1\dots f_n)$%}. *) val mkApp : constr * constr array -> constr -val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses +val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses -(** Constructs a constant *) -val mkConst : constant -> constr +(** Constructs a Constant.t *) +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 *) @@ -180,7 +184,7 @@ 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 = existential_key * 'constr array +type 'constr pexistential = Evar.t * 'constr array type ('constr, 'types) prec_declaration = Name.t array * 'types array * 'constr array type ('constr, 'types) pfixpoint = @@ -188,33 +192,146 @@ type ('constr, 'types) pfixpoint = type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration -type ('constr, 'types) kind_of_term = - | Rel of int - | Var of Id.t +type ('constr, 'types, 'sort, 'univs) kind_of_term = + | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) + + | Var of Id.t (** Gallina-variable that was introduced by Vernacular-command that extends + the local context of the currently open section + (i.e. [Variable] or [Let]). *) + | Meta of metavariable | Evar of 'constr pexistential - | Sort of Sorts.t + | Sort of 'sort | Cast of 'constr * cast_kind * 'types | Prod of Name.t * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) - | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *) + | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:C := B in D"] is represented as [LetIn (A,B,C,D)]. *) | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])]. + The {!mkApp} constructor also enforces the following invariant: - [F] itself is not {!App} - and [[|P1;..;Pn|]] is not empty. *) - | Const of constant puniverses - | Ind of inductive puniverses - | Construct of constructor puniverses + + | Const of (Constant.t * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *) + + | Ind of (inductive * 'univs) (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) + | Construct of (constructor * 'univs) (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | 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 term *) -val kind : constr -> (constr, types) 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 + +(** {6 Simple case analysis} *) +val isRel : constr -> bool +val isRelN : int -> constr -> bool +val isVar : constr -> bool +val isVarId : Id.t -> constr -> bool +val isInd : constr -> bool +val isEvar : constr -> bool +val isMeta : constr -> bool +val isEvar_or_Meta : constr -> bool +val isSort : constr -> bool +val isCast : constr -> bool +val isApp : constr -> bool +val isLambda : constr -> bool +val isLetIn : constr -> bool +val isProd : constr -> bool +val isConst : constr -> bool +val isConstruct : constr -> bool +val isFix : constr -> bool +val isCoFix : constr -> bool +val isCase : constr -> bool +val isProj : constr -> bool + +val is_Prop : constr -> bool +val is_Set : constr -> bool +val isprop : constr -> bool +val is_Type : constr -> bool +val iskind : constr -> bool +val is_small : Sorts.t -> bool + +(** {6 Term destructors } *) +(** Destructor operations are partial functions and + @raise DestKO if the term has not the expected form. *) + +exception DestKO + +(** Destructs a de Bruijn index *) +val destRel : constr -> int + +(** Destructs an existential variable *) +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{% }%}. *) +val destSort : constr -> Sorts.t + +(** Destructs a casted term *) +val destCast : constr -> constr * cast_kind * constr + +(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) +val destProd : types -> Name.t * types * types + +(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) +val destLambda : constr -> Name.t * types * constr + +(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) +val destLetIn : constr -> Name.t * constr * types * constr + +(** Destructs an application *) +val destApp : constr -> constr * constr array + +(** Decompose any term as an applicative term; the list of args can be empty *) +val decompose_app : constr -> constr * constr list + +(** Same as [decompose_app], but returns an array. *) +val decompose_appvect : constr -> constr * constr array + +(** Destructs a constant *) +val destConst : constr -> Constant.t Univ.puniverses + +(** Destructs an existential variable *) +val destEvar : constr -> existential + +(** Destructs a (co)inductive type *) +val destInd : constr -> inductive Univ.puniverses + +(** Destructs a constructor *) +val destConstruct : constr -> constructor Univ.puniverses + +(** Destructs a [match c as x in I args return P with ... | +Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args +return P in t1], or [if c then t1 else t2]) +@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] +where [info] is pretty-printing information *) +val destCase : constr -> case_info * constr * constr * constr array + +(** Destructs a projection *) +val destProj : constr -> Projection.t * constr + +(** Destructs the {% $ %}i{% $ %}th function of the block + [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} + with f{_ 2} ctx{_ 2} = b{_ 2} + ... + with f{_ n} ctx{_ n} = b{_ n}], + where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. +*) +val destFix : constr -> fixpoint + +val destCoFix : constr -> cofixpoint + +(** {6 Equality} *) (** [equal a b] is true if [a] equals [b] modulo alpha, casts, and application grouping *) @@ -285,48 +402,73 @@ val iter : (constr -> unit) -> constr -> unit val iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit +(** [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_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 -> constr -> bool) -> constr -> constr -> bool +val compare_head : constr_compare_fn -> 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 -(** [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 (the first boolean tells if they belong to a constant), [s] to - compare sorts; Cast's, binders name and Cases annotations are not taken - into account *) +(** [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 -> + (Sorts.t -> Sorts.t -> bool) -> + constr_compare_fn -> + constr_compare_fn -val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> +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 -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + constr_compare_fn -> + 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) kind_of_term) -> - (constr -> (constr,types) kind_of_term) -> - (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + (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 -> constr -> bool) -> - constr -> constr -> bool + constr_compare_fn -> + 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 conversion, [fle] for cumulativity, [u] to compare universe - instances (the first boolean tells if they belong to a constant), + instances (the first boolean tells if they belong to a Constant.t), [s] to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account *) -val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> +val compare_head_gen_leq : instance_compare_fn -> (Sorts.t -> Sorts.t -> bool) -> - (constr -> constr -> bool) -> - (constr -> constr -> bool) -> - constr -> constr -> bool - + constr_compare_fn -> + constr_compare_fn -> + constr_compare_fn + (** {6 Hashconsing} *) val hash : constr -> int @@ -335,7 +477,3 @@ val case_info_hash : case_info -> int (*********************************************************************) val hcons : constr -> constr - -(**************************************) - -type values |