Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * 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 Rocq, namely kernel terms, as well as a handful of generic manipulation functions. *)
open Names
(** {6 Simply type aliases } *)type pconstant = Constant.t UVars.puniversestype pinductive = inductive UVars.puniversestype pconstructor = constructor UVars.puniverses
(** {6 Existential variables } *)type metavariable = int
(** {6 Case annotation } *)type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle
type case_printing = { style : case_style }
(* INVARIANT: * - Array.length ci_cstr_ndecls = Array.length ci_cstr_nargs * - forall (i : 0 .. pred (Array.length ci_cstr_ndecls)), * ci_cstr_ndecls.(i) >= ci_cstr_nargs.(i) *)type case_info = { ci_ind : inductive; (* inductive type to which belongs the value that is being matched *) ci_npar : int; (* number of parameters of the above inductive type *) ci_cstr_ndecls : int array; (* For each constructor, the corresponding integer determines the number of values that can be bound in a match-construct. NOTE: parameters of the inductive type are therefore excluded from the count *) ci_cstr_nargs : int array; (* for each constructor, the corresponding integers determines the number of values that can be applied to the constructor, in addition to the parameters of the related inductive type NOTE: "lets" are therefore excluded from the count NOTE: parameters of the inductive type are also excluded from the count *) ci_pp_info : case_printing (* not interpreted by the kernel *) }
(** {6 The type of constructions } *)
type ttype constr = t(** [types] is the same as [constr] but is intended to be used for documentation to indicate that such or such function specifically works with {e types} (i.e. terms of type a sort). (Rem:plurial form since [type] is a reserved ML keyword) *)
type types = constr
(** {5 Functions for dealing with constr terms. } The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with previous ones. *)
(** {6 Term constructors. } *)
(** Constructs a de Bruijn index (DB indices begin at 1) *)val mkRel : int -> constr
(** Constructs a Variable *)val mkVar : Id.t -> constr
(** Constructs a machine integer *)val mkInt : Uint63.t -> constr
(** Constructs an array *)val mkArray : UVars.Instance.t * constr array * constr * types -> constr
(** Constructs a machine float number *)val mkFloat : Float64.t -> constr
(** Constructs a machine string. *)val mkString : Pstring.t -> constr
(** Constructs an patvar named "?n" *)val mkMeta : metavariable -> constr
(** Constructs an existential variable *)type existential = Evar.t * constr SList.tval mkEvar : existential -> constr
(** Construct a sort *)val mkSort : Sorts.t -> typesval mkSProp : typesval mkProp : typesval mkSet : typesval mkType : Univ.Universe.t -> types
(** This defines the strategy to use for verifiying a Cast *)type cast_kind = VMcast | NATIVEcast | DEFAULTcast
(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the type t{_ 2} (that means t2 is declared as the type of t1). *)val mkCast : constr * cast_kind * constr -> constr
type 'a binder_annot = ('a,Sorts.relevance) Context.pbinder_annot
(** Constructs the product [(x:t1)t2] *)val mkProd : Name.t binder_annot * types * types -> types
(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *)val mkLambda : Name.t binder_annot * types * constr -> constr
(** Constructs the product [let x = t1 : t2 in t3] *)val mkLetIn : Name.t binder_annot * constr * types * constr -> constr
(** [mkApp (f, [|t1; ...; tN|]] constructs the application {%html:(f t<sub>1</sub> ... t<sub>n</sub>)%} {%latex:$(f~t_1\dots f_n)$%}. *)val mkApp : constr * constr array -> constr
val map_puniverses : ('a -> 'b) -> 'a UVars.puniverses -> 'b UVars.puniverses
(** Constructs a Constant.t *)val mkConstU : pconstant -> constr
(** Constructs a projection application *)val mkProj : (Projection.t * Sorts.relevance * constr) -> constr
(** Inductive types *)
(** Constructs the ith (co)inductive type of the block named kn *)val mkIndU : pinductive -> constr
(** Constructs the jth constructor of the ith (co)inductive type of the block named kn. *)val mkConstructU : pconstructor -> constrval mkConstructUi : pinductive * int -> constr
(** Make a constant, inductive, constructor or variable. *)val mkRef : GlobRef.t UVars.puniverses -> constr
module UnsafeMonomorphic : sig val mkConst : Constant.t -> constr val mkInd : inductive -> constr val mkConstruct : constructor -> constrend
(** Constructs a destructor of inductive type.
[mkCase ci params p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] presented as describe in [ci].
[p] structure is [args x |- "return clause"]
[ac]{^ ith} element is ith constructor case presented as {e construct_args |- case_term } *)
type ('constr,'r) pcase_branch = (Name.t,'r) Context.pbinder_annot array * 'constr(** Names bound by matching the constructor for this branch. *)
type ('types,'r) pcase_return = ((Name.t,'r) Context.pbinder_annot array * 'types) * 'r(** Names of the indices + name of self *)
type 'constr pcase_invert = | NoInvert (** Normal reduction: match when the scrutinee is a constructor. *)
| CaseInvert of { indices : 'constr array; } (** SProp to non SProp only: No constructors or reduce when the indices match those of the unique constructor. *)
type ('constr, 'types, 'univs, 'r) pcase = case_info * 'univs * 'constr array * ('types,'r) pcase_return * 'constr pcase_invert * 'constr * ('constr,'r) pcase_branch array
type case_invert = constr pcase_inverttype case_return = (types, Sorts.relevance) pcase_returntype case_branch = (constr, Sorts.relevance) pcase_branchtype case = (constr, types, UVars.Instance.t, Sorts.relevance) pcase
val mkCase : case -> constr
(** If [recindxs = [|i1,...in|]] [funnames = [|f1,.....fn|]] [typarray = [|t1,...tn|]] [bodies = [|b1,.....bn|]] then [mkFix ((recindxs,i), funnames, typarray, bodies) ] constructs the {% $ %}i{% $ %}th function of the block (counting from 0)
[Fixpoint f1 [ctx1] = b1 with f2 [ctx2] = b2 ... with fn [ctxn] = bn.]
where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.*)type ('constr, 'types, 'r) prec_declaration = (Name.t, 'r) Context.pbinder_annot array * 'types array * 'constr arraytype ('constr, 'types, 'r) pfixpoint = (int array * int) * ('constr, 'types, 'r) 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, 'r) pcofixpoint = int * ('constr, 'types, 'r) prec_declaration(** The component [int] tells which component of the block of cofixpoint is returned *)
type rec_declaration = (constr, types, Sorts.relevance) prec_declaration
type fixpoint = (constr, types, Sorts.relevance) pfixpointval mkFix : fixpoint -> constr
(** If [funnames = [|f1,.....fn|]] [typarray = [|t1,...tn|]] [bodies = [b1,.....bn]] then [mkCoFix (i, (funnames, typarray, bodies))] constructs the ith function of the block
[CoFixpoint f1 = b1 with f2 = b2 ... with fn = bn.] *)type cofixpoint = (constr, types, Sorts.relevance) pcofixpointval mkCoFix : cofixpoint -> constr
(** {6 Concrete type for making pattern-matching. } *)
(** [constr list] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *)type 'constr pexistential = Evar.t * 'constr SList.t
type ('constr, 'types, 'sort, 'univs, 'r) 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 'sort | Cast of 'constr * cast_kind * 'types | Prod of (Name.t,'r) Context.pbinder_annot * 'types * 'types (** Concrete syntax ["forall A:B,C"] is represented as [Prod (A,B,C)]. *) | Lambda of (Name.t,'r) Context.pbinder_annot * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) | LetIn of (Name.t,'r) Context.pbinder_annot * '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.t * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem], or [Symbol] 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 * 'univs * 'constr array * ('types,'r) pcase_return * 'constr pcase_invert * 'constr * ('constr,'r) pcase_branch array (** [Case (ci,u,params,p,iv,c,brs)] is a [match c return p with brs] expression. [c] lives in inductive [ci.ci_ind] at universe instance [u] and parameters [params]. If this match has case inversion (ie match on a 1 constructor SProp inductive with proof relevant return type) the indices are in [iv].
The names in [p] are the names of the bound indices and inductive value (ie the [in] and [as] clauses).
The names in the [brs] are the names of the variables bound in the respective branch. *) | Fix of ('constr, 'types, 'r) pfixpoint | CoFix of ('constr, 'types, 'r) pcofixpoint | Proj of Projection.t * 'r * 'constr (** The relevance is the relevance of the whole term *) | Int of Uint63.t | Float of Float64.t | String of Pstring.t | Array of 'univs * 'constr array * 'constr * 'types (** [Array (u,vals,def,t)] is an array of [vals] in type [t] with default value [def]. [u] is a universe containing [t]. *)
(** 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, Sorts.t, UVars.Instance.t, Sorts.relevance) kind_of_termval of_kind : (constr, types, Sorts.t, UVars.Instance.t, Sorts.relevance) kind_of_term -> constr
val kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term) -> ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term)
val kind_nocast : constr -> (constr, types, Sorts.t, UVars.Instance.t, Sorts.relevance) kind_of_term
(** {6 Simple case analysis} *)val isRel : constr -> boolval isRelN : int -> constr -> boolval isVar : constr -> boolval isVarId : Id.t -> constr -> boolval isRef : constr -> boolval isInd : constr -> boolval isEvar : constr -> boolval isMeta : constr -> boolval isEvar_or_Meta : constr -> boolval isSort : constr -> boolval isCast : constr -> boolval isApp : constr -> boolval isLambda : constr -> boolval isLetIn : constr -> boolval isProd : constr -> boolval isConst : constr -> boolval isConstruct : constr -> boolval isFix : constr -> boolval isCoFix : constr -> boolval isCase : constr -> boolval isProj : constr -> bool
val is_Prop : constr -> boolval is_Set : constr -> boolval isprop : constr -> boolval is_Type : constr -> boolval iskind : constr -> 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 [Prop], whether [isprop] recognizes both [Prop] and [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 binder_annot * types * types
(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)val destLambda : constr -> Name.t binder_annot * types * constr
(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)val destLetIn : constr -> Name.t binder_annot * 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_list : constr -> constr * constr list
(** Same as [decompose_app], but returns an array. *)val decompose_app : constr -> constr * constr array
(** Destructs a constant *)val destConst : constr -> Constant.t UVars.puniverses
(** Destructs an existential variable *)val destEvar : constr -> existential
(** Destructs a (co)inductive type *)val destInd : constr -> inductive UVars.puniverses
(** Destructs a constructor *)val destConstruct : constr -> constructor UVars.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 argsreturn 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
(** Destructs a projection *)val destProj : constr -> Projection.t * Sorts.relevance * 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
val destRef : constr -> GlobRef.t UVars.puniverses
(** {6 Equality} *)
(** [equal a b] is true if [a] equals [b] modulo alpha, casts, and application grouping *)val equal : constr -> constr -> bool
(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, application grouping and the universe equalities in [u]. *)val eq_constr_univs : UGraph.t -> constr -> constr -> bool
(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo alpha, casts, application grouping and the universe inequalities in [u]. *)val leq_constr_univs : UGraph.t -> constr -> constr -> bool
(** {6 Extension of Context with declarations on constr} *)
type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pttype named_declaration = (constr, types, Sorts.relevance) Context.Named.Declaration.pttype rel_context = rel_declaration listtype named_context = named_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_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_branch array -> case_branch 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_return -> case_return
(** [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_branch array -> case_branch 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_return -> case_return
(** {6 Functionals working on the immediate subterm of a construction } *)
(** [fold f acc c] folds [f] on the immediate subterms of [c] starting from [acc] and proceeding from left to right according to the usual representation of the constructions; it is not recursive *)
val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
val fold_invert : ('a -> 'b -> 'a) -> 'a -> 'b pcase_invert -> 'a
(** [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
val map_invert : ('a -> 'a) -> 'a pcase_invert -> 'a pcase_invert
(** Like {!map}, but also has an additional accumulator. *)
val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
val fold_map_invert : ('a -> 'b -> 'a * 'b) -> 'a -> 'b pcase_invert -> 'a * 'b pcase_invert
(** [map_with_binders g f n c] maps [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 map_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
(** [iter f c] iters [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *)
val iter : (constr -> unit) -> constr -> unit
val iter_invert : ('a -> unit) -> 'a pcase_invert -> 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 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 constr_compare_fn = int -> 'constr -> 'constr -> bool
(** 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 'univs instance_compare_fn = (GlobRef.t * int) option -> 'univs -> 'univs -> bool
val compare_head_gen_leq_with : ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term) -> ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term) -> 'univs instance_compare_fn -> ('sort -> 'sort -> bool) -> ('v pexistential -> 'v pexistential -> bool) -> 'v constr_compare_fn -> 'v constr_compare_fn -> 'v constr_compare_fn
val eq_invert : ('a -> 'a -> bool) -> 'a pcase_invert -> 'a pcase_invert -> bool
(** {6 Hashconsing} *)
(*********************************************************************)
module GenHCons(C:sig type t val kind : t -> (t, t, Sorts.t, UVars.Instance.t, Sorts.relevance) kind_of_term val self : t -> constr val refcount : t -> int
val via_hconstr : bool
module Tbl : sig val find_opt : t -> (int * constr) option val add : t -> int * constr -> unit end end) : sig val hcons : C.t -> int * constrend
val hcons : constr Hashcons.f
val hasheq_kind : (_ kind_of_term as 'k) -> 'k -> bool(** Checks physical equality of every immediate element (goes inside tuples and arrays) *)
val debug_print : constr -> Pp.tval debug_print_fix : ('a -> Pp.t) -> ('a, 'a, 'r) pfixpoint -> Pp.t
val mkConst : Constant.t -> constr[@@deprecated "(8.18) Use [mkConstU] or if truly needed [UnsafeMonomorphic.mkConst]"]
val mkInd : inductive -> constr[@@deprecated "(8.18) Use [mkIndU] or if truly needed [UnsafeMonomorphic.mkInd]"]
val mkConstruct : constructor -> constr[@@deprecated "(8.18) Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct]"]
val hcons_annot : Name.t binder_annot Hashcons.f
val hcons_caseinfo : case_info Hashcons.f
val hash_cast_kind : cast_kind -> int