diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /kernel/constr.mli | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'kernel/constr.mli')
-rw-r--r-- | kernel/constr.mli | 313 |
1 files changed, 313 insertions, 0 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli new file mode 100644 index 00000000..5d11511b --- /dev/null +++ b/kernel/constr.mli @@ -0,0 +1,313 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names + +(** {6 Value under universe substitution } *) +type 'a puniverses = 'a Univ.puniverses + +(** {6 Simply type aliases } *) +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses + +(** {6 Existential variables } *) +type existential_key = Evar.t + +(** {6 Existential variables } *) +type metavariable = int + +(** {6 Case annotation } *) +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 *) + cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *) + style : case_style } + +(** the integer is the number of real args, needed for reduction *) +type case_info = + { ci_ind : inductive; + ci_npar : int; + ci_cstr_ndecls : int array; (* number of pattern vars of each constructor (with let's)*) + ci_cstr_nargs : int array; (* number of pattern vars of each constructor (w/o let's) *) + ci_pp_info : case_printing (** not interpreted by the kernel *) + } + +(** {6 The type of constructions } *) + +type t +type 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 DeBrujin index (DB indices begin at 1) *) +val mkRel : int -> constr + +(** Constructs a Variable *) +val mkVar : Id.t -> constr + +(** Constructs an patvar named "?n" *) +val mkMeta : metavariable -> constr + +(** Constructs an existential variable *) +type existential = existential_key * 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 + + +(** This defines the strategy to use for verifiying a Cast *) +type cast_kind = VMcast | NATIVEcast | DEFAULTcast | REVERTcast + +(** 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 + +(** Constructs the product [(x:t1)t2] *) +val mkProd : Name.t * types * types -> types + +(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *) +val mkLambda : Name.t * types * constr -> constr + +(** Constructs the product [let x = t1 : t2 in t3] *) +val mkLetIn : Name.t * constr * types * constr -> constr + +(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application + {% $(f~t_1~\dots~t_n)$ %}. *) +val mkApp : constr * constr array -> constr + +val map_puniverses : ('a -> 'b) -> 'a puniverses -> 'b puniverses + +(** Constructs a constant *) +val mkConst : constant -> constr +val mkConstU : pconstant -> constr + +(** Constructs a projection application *) +val mkProj : (projection * constr) -> constr + +(** Inductive types *) + +(** Constructs the ith (co)inductive type of the block named kn *) +val mkInd : inductive -> constr +val mkIndU : pinductive -> constr + +(** Constructs the jth constructor of the ith (co)inductive type of the + block named kn. *) +val mkConstruct : constructor -> constr +val mkConstructU : pconstructor -> constr +val mkConstructUi : pinductive * int -> 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] + presented as describe in [ci]. + + [p] stucture is [fun args x -> "return clause"] + + [ac]{^ ith} element is ith constructor case presented as + {e lambda construct_args (without params). case_term } *) +val mkCase : case_info * constr * constr * constr array -> 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 rec_declaration = Name.t array * types array * constr array +type fixpoint = (int array * int) * rec_declaration +val 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 = int * rec_declaration +val mkCoFix : cofixpoint -> constr + + +(** {6 Concrete type for making pattern-matching. } *) + +(** [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, '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) kind_of_term = + | Rel of int + | Var of Id.t + | Meta of metavariable + | Evar of 'constr pexistential + | Sort of Sorts.t + | Cast of 'constr * cast_kind * 'types + | Prod of Name.t * 'types * 'types + | Lambda of Name.t * 'types * 'constr + | LetIn of Name.t * 'constr * 'types * 'constr + | App of 'constr * 'constr array + | Const of constant puniverses + | Ind of inductive puniverses + | Construct of constructor puniverses + | Case of case_info * 'constr * 'constr * 'constr array + | Fix of ('constr, 'types) pfixpoint + | CoFix of ('constr, 'types) pcofixpoint + | Proj of projection * '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 + +(** [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 : constr Univ.check_function + +(** [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 : constr Univ.check_function + +(** [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_infer : Univ.universes -> constr -> constr -> bool Univ.constrained + +(** [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_infer : Univ.universes -> constr -> constr -> bool Univ.constrained + +(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and ignoring universe instances. *) +val eq_constr_nounivs : constr -> constr -> bool + +(** Total ordering compatible with [equal] *) +val compare : constr -> constr -> int + +(** {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 + +(** [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 + +(** Like {!map}, but also has an additional accumulator. *) + +val fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr + +(** [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 + +(** [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 + +(** [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 + +(** [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 *) + +val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) -> + (Sorts.t -> Sorts.t -> bool) -> + (constr -> constr -> bool) -> + constr -> constr -> bool + +(** [compare_head_gen_leq u s sle 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), + [s] to compare sorts for equality and [sle] 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) -> + (Sorts.t -> Sorts.t -> bool) -> + (Sorts.t -> Sorts.t -> bool) -> + (constr -> constr -> bool) -> + (constr -> constr -> bool) -> + constr -> constr -> bool + +(** {6 Hashconsing} *) + +val hash : constr -> int +val case_info_hash : case_info -> int + +(*********************************************************************) + +val hcons : constr -> constr + +(**************************************) + +type values |