diff options
Diffstat (limited to 'kernel/constr.mli')
| -rw-r--r-- | kernel/constr.mli | 140 |
1 files changed, 121 insertions, 19 deletions
diff --git a/kernel/constr.mli b/kernel/constr.mli index 76dbf55309..19ffa8fe30 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -13,20 +13,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 *) @@ -80,14 +82,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,10 +113,10 @@ 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 *) @@ -180,7 +182,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 = @@ -201,14 +203,14 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | 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 * 'univs) (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + | 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. *) @@ -225,6 +227,110 @@ 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 +(** {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 * 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 *) val equal : constr -> constr -> bool @@ -302,7 +408,7 @@ 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 + instances (the first boolean tells if they belong to a Constant.t), [s] to compare sorts; Cast's, binders name and Cases annotations are not taken into account *) @@ -335,7 +441,7 @@ val compare_head_gen_with : (** [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 *) @@ -344,7 +450,7 @@ val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) (constr -> constr -> bool) -> (constr -> constr -> bool) -> constr -> constr -> bool - + (** {6 Hashconsing} *) val hash : constr -> int @@ -353,7 +459,3 @@ val case_info_hash : case_info -> int (*********************************************************************) val hcons : constr -> constr - -(**************************************) - -type values |