diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 476 |
1 files changed, 161 insertions, 315 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 90b1dd807..0ce4f3d4a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,4 +1,4 @@ -(***********************************************************************) +(***********************Sppc************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) (* \VV/ *************************************************************) @@ -9,8 +9,6 @@ (*i $Id$ i*) (*i*) -open Util -open Pp open Names (*i*) @@ -24,8 +22,7 @@ type sorts = val mk_Set : sorts val mk_Prop : sorts - -val print_sort : sorts -> std_ppcmds +val type_0 : sorts (*s The sorts family of CCI. *) @@ -36,38 +33,33 @@ val new_sort_in_family : sorts_family -> sorts (*s Useful types *) +(*s Existential variables *) type existential_key = int +(*s Case annotation *) type pattern_source = DefaultPat of int | RegularPat type case_style = PrintLet | PrintIf | PrintCases type case_printing = - inductive * identifier array * int - * case_style option * pattern_source array + { cnames : identifier array; + ind_nargs : int; (* number of real args of the inductive type *) + style : case_style option; + source : pattern_source array } (* the integer is the number of real args, needed for reduction *) -type case_info = int * case_printing - -(*s Concrete type for making pattern-matching. *) -module Polymorph : -sig -(* [constr array] is an instance matching definitional [named_context] in - the same order (i.e. last argument first) *) -type 'constr existential = existential_key * 'constr array -type ('constr, 'types) rec_declaration = - name array * 'types array * 'constr array -type ('constr, 'types) fixpoint = - (int array * int) * ('constr, 'types) rec_declaration -type ('constr, 'types) cofixpoint = - int * ('constr, 'types) rec_declaration - -(* [IsVar] is used for named variables and [IsRel] for variables as - de Bruijn indices. *) -end +type case_info = + { ci_ind : inductive; + ci_npar : int; + ci_pp_info : case_printing (* not interpreted by the kernel *) + } (*s*******************************************************************) (* The type of constructions *) type constr +(* [eq_constr a b] is true if [a] equals [b] modulo alpha, casts, + and application grouping *) +val eq_constr : constr -> constr -> bool + (* [types] is the same as [constr] but is intended to be used where a {\em type} in CCI sense is expected (Rem:plurial form since [type] is a reserved ML keyword) *) @@ -80,144 +72,79 @@ val type_app : (constr -> constr) -> types -> types val body_of_type : types -> constr -(*s A {\em declaration} has the form (name,body,type). It is either an - {\em assumption} if [body=None] or a {\em definition} if - [body=Some actualbody]. It is referred by {\em name} if [na] is an - identifier or by {\em relative index} if [na] is not an identifier - (in the latter case, [na] is of type [name] but just for printing - purpose *) - -type named_declaration = identifier * constr option * types -type rel_declaration = name * constr option * types - -type arity = rel_declaration list * sorts - (*s 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. *) -open Polymorph -type ('constr, 'types) kind_of_term = - | IsRel of int - | IsMeta of int - | IsVar of identifier - | IsSort of sorts - | IsCast of 'constr * 'constr - | IsProd of name * 'types * 'constr - | IsLambda of name * 'types * 'constr - | IsLetIn of name * 'constr * 'types * 'constr - | IsApp of 'constr * 'constr array - | IsEvar of 'constr existential - | IsConst of constant - | IsMutInd of inductive - | IsMutConstruct of constructor - | IsMutCase of case_info * 'constr * 'constr * 'constr array - | IsFix of ('constr, 'types) fixpoint - | IsCoFix of ('constr, 'types) cofixpoint - -type existential = existential_key * constr array -type rec_declaration = name array * types array * constr array -type fixpoint = (int array * int) * rec_declaration -type cofixpoint = int * rec_declaration - -(* User view of [constr]. For [IsApp], it is ensured there is at - least one argument and the function is not itself an applicative - term *) - -val kind_of_term : constr -> (constr, types) kind_of_term - (*s Term constructors. *) (* Constructs a DeBrujin index *) val mkRel : int -> constr -(* Constructs an existential variable named "?n" *) -val mkMeta : int -> constr - (* Constructs a Variable *) val mkVar : identifier -> constr -(* Construct a type *) +(* Constructs an metavariable named "?n" *) +val mkMeta : int -> constr + +(* Constructs an existential variable *) +type existential = existential_key * constr array +val mkEvar : existential -> constr + +(* Construct a sort *) val mkSort : sorts -> constr val mkProp : constr -val mkSet : constr +val mkSet : constr val mkType : Univ.universe -> constr -val prop : sorts -val spec : sorts -(*val types : sorts *) -val type_0 : sorts - -(* Construct an implicit (see implicit arguments in the RefMan). - Used for extraction *) -val mkImplicit : constr -val implicit_sort : sorts -(* Constructs the term $t_1::t2$, i.e. the term $t_1$ casted with the +(* 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 * constr -> constr +val mkCast : constr * types -> constr -(* Constructs the product $(x:t_1)t_2$ *) -val mkProd : name * types * constr -> constr -val mkNamedProd : identifier -> constr -> constr -> constr -val mkProd_string : string -> constr -> constr -> constr - -(* Constructs the product $(x:t_1)t_2$ *) -val mkLetIn : name * constr * types * constr -> constr -val mkNamedLetIn : identifier -> constr -> constr -> constr -> constr - -(* Constructs either [(x:t)c] or [[x=b:t]c] *) -val mkProd_or_LetIn : rel_declaration -> constr -> constr -val mkNamedProd_or_LetIn : named_declaration -> constr -> constr - -(* Constructs either [[x:t]c] or [[x=b:t]c] *) -val mkLambda_or_LetIn : rel_declaration -> constr -> constr -val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr - -(* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) -val mkProd_wo_LetIn : rel_declaration -> constr -> constr -val mkNamedProd_wo_LetIn : named_declaration -> constr -> constr - -(* non-dependant product $t_1 \rightarrow t_2$ *) -val mkArrow : constr -> constr -> constr +(* Constructs the product [(x:t1)t2] *) +val mkProd : name * types * types -> constr +val mkNamedProd : identifier -> types -> types -> constr +(* non-dependant product $t_1 \rightarrow t_2$, an alias for + [(_:t1)t2]. Beware $t_2$ is NOT lifted. + Eg: A |- A->A is built by [(mkArrow (mkRel 0) (mkRel 1))] *) +val mkArrow : types -> types -> constr (* Constructs the abstraction $[x:t_1]t_2$ *) val mkLambda : name * types * constr -> constr -val mkNamedLambda : identifier -> constr -> constr -> constr +val mkNamedLambda : identifier -> types -> constr -> constr -(* [mkLambda_string s t c] constructs $[s:t]c$ *) -val mkLambda_string : string -> constr -> constr -> constr +(* Constructs the product [let x = t1 : t2 in t3] *) +val mkLetIn : name * constr * types * constr -> constr +val mkNamedLetIn : identifier -> 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 mkAppA : constr array -> constr (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) val mkConst : constant -> constr -(* Constructs an existential variable *) -val mkEvar : existential -> constr +(* Inductive types *) (* Constructs the ith (co)inductive type of the block named sp *) (* The array of terms correspond to the variables introduced in the section *) -val mkMutInd : inductive -> constr +val mkInd : inductive -> constr (* Constructs the jth constructor of the ith (co)inductive type of the block named sp. The array of terms correspond to the variables introduced in the section *) -val mkMutConstruct : constructor -> constr +val mkConstruct : constructor -> constr (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) -val mkMutCaseL : case_info * constr * constr * constr list -> constr -val mkMutCase : case_info * constr * constr * constr array -> constr +val mkCase : case_info * constr * constr * constr array -> constr (* If [recindxs = [|i1,...in|]] + [funnames = [|f1,.....fn|]] [typarray = [|t1,...tn|]] - [funnames = [f1,.....fn]] - [bodies = [b1,.....bn]] - then [ mkFix ((recindxs,i),typarray, funnames, bodies) ] + [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 @@ -225,12 +152,14 @@ val mkMutCase : case_info * constr * constr * constr array -> constr ... with fn [ctxn] = bn.] - \noindent where the lenght of the $j$th context is $ij$. + \noindent where the length of the $j$th context is $ij$. *) +type rec_declaration = name array * types array * constr array +type fixpoint = (int array * int) * rec_declaration val mkFix : fixpoint -> constr -(* If [typarray = [|t1,...tn|]] - [funnames = [f1,.....fn]] +(* If [funnames = [|f1,.....fn|]] + [typarray = [|t1,...tn|]] [bodies = [b1,.....bn]] \par\noindent then [mkCoFix (i, (typsarray, funnames, bodies))] constructs the ith function of the block @@ -240,22 +169,73 @@ val mkFix : fixpoint -> constr ... with fn = bn.] *) +type cofixpoint = int * rec_declaration val mkCoFix : cofixpoint -> constr + +(*s 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 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 identifier + | Meta of int + | Evar of 'constr pexistential + | Sort of sorts + | Cast of 'constr * 'constr + | Prod of name * 'types * 'types + | Lambda of name * 'types * 'constr + | LetIn of name * 'constr * 'types * 'constr + | App of 'constr * 'constr array + | Const of constant + | Ind of inductive + | Construct of constructor + | Case of case_info * 'constr * 'constr * 'constr array + | Fix of ('constr, 'types) pfixpoint + | CoFix of ('constr, 'types) pcofixpoint + +(* 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_of_term : constr -> (constr, types) kind_of_term + +(*s Simple term case analysis. *) + +val isRel : constr -> bool +val isVar : constr -> bool +val isMeta : constr -> bool +val isSort : constr -> bool +val isCast : constr -> bool +val isApp : constr -> bool +val isConst : constr -> bool +val isConstruct : 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 -> bool + (*s Term destructors. Destructor operations are partial functions and raise [invalid_arg "dest*"] if the term has not the expected form. *) -(* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *) -val destArity : constr -> arity -val isArity : constr -> bool - (* Destructs a DeBrujin index *) val destRel : constr -> int (* Destructs an existential variable *) val destMeta : constr -> int -val isMeta : constr -> bool (* Destructs a variable *) val destVar : constr -> identifier @@ -263,68 +243,35 @@ val destVar : constr -> identifier (* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *) val destSort : constr -> sorts -val is_Prop : constr -> bool -val is_Set : constr -> bool -val isprop : constr -> bool -val is_Type : constr -> bool -val iskind : constr -> bool -val isSort : constr -> bool - -val isType : sorts -> bool -val is_small : sorts -> bool (* true for \textsf{Prop} and \textsf{Set} *) (* Destructs a casted term *) -val destCast : constr -> constr * constr -val isCast : constr -> bool - -(* Removes recursively the casts around a term i.e. - [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : constr -> constr - -(* Apply a function letting Casted types in place *) -val under_casts : (constr -> constr) -> constr -> constr - -(* Tests if a de Bruijn index *) -val isRel : constr -> bool - -(* Tests if a variable *) -val isVar : constr -> bool +val destCast : constr -> constr * types (* Destructs the product $(x:t_1)t_2$ *) -val destProd : constr -> name * constr * constr -val hd_of_prod : constr -> constr -(*i -val hd_is_constructor : constr -> bool -i*) +val destProd : types -> name * types * types (* Destructs the abstraction $[x:t_1]t_2$ *) -val destLambda : constr -> name * constr * constr +val destLambda : constr -> name * types * constr (* Destructs the let $[x:=b:t_1]t_2$ *) -val destLetIn : constr -> name * constr * constr * constr +val destLetIn : constr -> name * constr * types * constr (* Destructs an application *) -val isApp : constr -> bool -(*i -val hd_app : constr -> constr -val args_app : constr -> constr array -i*) val destApplication : constr -> constr * constr array +(* ... removing casts *) +val decompose_app : constr -> constr * constr list (* Destructs a constant *) val destConst : constr -> constant -val isConst : constr -> bool (* Destructs an existential variable *) -val destEvar : constr -> existential_key * constr array -val num_of_evar : constr -> existential_key +val destEvar : constr -> existential (* Destructs a (co)inductive type *) -val destMutInd : constr -> inductive +val destInd : constr -> inductive (* Destructs a constructor *) -val destMutConstruct : constr -> constructor -val isMutConstruct : constr -> bool +val destConstruct : constr -> constructor (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) val destCase : constr -> case_info * constr * constr * constr array @@ -340,6 +287,30 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint + +(*s A {\em declaration} has the form (name,body,type). It is either an + {\em assumption} if [body=None] or a {\em definition} if + [body=Some actualbody]. It is referred by {\em name} if [na] is an + identifier or by {\em relative index} if [na] is not an identifier + (in the latter case, [na] is of type [name] but just for printing + purpose *) + +type named_declaration = identifier * constr option * types +type rel_declaration = name * constr option * types + +val map_named_declaration : + (constr -> constr) -> named_declaration -> named_declaration + +(* Constructs either [(x:t)c] or [[x=b:t]c] *) +val mkProd_or_LetIn : rel_declaration -> types -> constr +val mkNamedProd_or_LetIn : named_declaration -> types -> constr +val mkNamedProd_wo_LetIn : named_declaration -> types -> constr + +(* Constructs either [[x:t]c] or [[x=b:t]c] *) +val mkLambda_or_LetIn : rel_declaration -> constr -> constr +val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr + + (*s Other term constructors. *) val abs_implicit : constr -> constr @@ -361,14 +332,6 @@ val prodn : int -> (name * constr) list -> constr -> constr where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *) val lamn : int -> (name * constr) list -> constr -> constr -(* [prod_it b l] = $(x_1:T_1)..(x_n:T_n)b$ - where $l = [(x_n,T_n);\dots;(x_1,T_1)]$ *) -val prod_it : constr -> (name * constr) list -> constr - -(* [lam_it b l] = $[x_1:T_1]..[x_n:T_n]b$ - where $l = [(x_n,T_n);\dots;(x_1,T_1)]$ *) -val lam_it : constr -> (name * constr) list -> constr - (* [to_lambda n l] = $[x_1:T_1]...[x_n:T_n](x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$ where $l = (x_1:T_1)...(x_n:T_n)(x_{n+1}:T_{n+1})...(x_{n+j}:T_{n+j})T$ *) @@ -381,6 +344,11 @@ val prod_applist : constr -> constr list -> constr (*s Other term destructors. *) +(* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *) +type arity = rel_declaration list * sorts +val destArity : constr -> arity +val isArity : constr -> bool + (* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product. It includes also local definitions *) @@ -408,20 +376,16 @@ val nb_prod : constr -> int (* flattens application lists *) val collapse_appl : constr -> constr -val decomp_app : constr -> constr * constr list - -(*s Misc functions on terms, sorts and conversion problems. *) -(* Level comparison for information extraction : Prop <= Type *) -val same_kind : constr -> constr -> bool -val le_kind : constr -> constr -> bool -val le_kind_implicit : constr -> constr -> bool +(* Removes recursively the casts around a term i.e. + [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) +val strip_outer_cast : constr -> constr -val sort_hdchar : sorts -> string +(* Apply a function letting Casted types in place *) +val under_casts : (constr -> constr) -> constr -> constr -(* Generic functions *) -val free_rels : constr -> Intset.t +(*s Occur checks *) (* [closed0 M] is true iff [M] is a (deBruijn) closed term *) val closed0 : constr -> bool @@ -439,6 +403,8 @@ val noccur_between : int -> int -> constr -> bool context) (for existential variables, it is necessarily the case) *) val noccur_with_meta : int -> int -> constr -> bool +(*s Relocation and substitution *) + (* [liftn n k c] lifts by [n] indexes above [k] in [c] *) val liftn : int -> int -> constr -> constr @@ -469,91 +435,6 @@ val subst_vars : identifier list -> constr -> constr if two names are identical, the one of least indice is keeped *) val substn_vars : int -> identifier list -> constr -> constr -(* [rel_list n m] and [rel_vect n m] compute [[Rel (n+m);...;Rel(n+1)]] *) -val rel_vect : int -> int -> constr array -val rel_list : int -> int -> constr list - -(*s [extended_rel_vect n hyps] and [extended_rel_list n hyps] - generalizes [rel_vect] when local definitions may occur in parameters *) -val extended_rel_vect : int -> rel_declaration list -> constr array -val extended_rel_list : int -> rel_declaration list -> constr list - -(*s Occur check functions. *) - -val occur_meta : constr -> bool - -(*i Returns the maximum of metas. Returns -1 if there is no meta i*) -(*i val max_occur_meta : constr -> int i*) - -val occur_existential : constr -> bool - -(* [(occur_const (s:section_path) c)] returns [true] if constant [s] occurs - in c, [false] otherwise *) -val occur_const : constant -> constr -> bool - -(* [(occur_evar ev c)] returns [true] if existential variable [ev] occurs - in c, [false] otherwise *) -val occur_evar : existential_key -> constr -> bool - -(* [dependent M N] is true iff M is eq\_constr with a subterm of N - M is appropriately lifted through abstractions of N *) -val dependent : constr -> constr -> bool - -(* strips head casts and flattens head applications *) -val strip_head_cast : constr -> constr -val eta_reduce_head : constr -> constr -val eq_constr : constr -> constr -> bool -val eta_eq_constr : constr -> constr -> bool - -(*s The following functions substitutes [what] by [Rel 1] in [where] *) -val subst_term : what:constr -> where:constr -> constr -val subst_term_occ : occs:int list -> what:constr -> where:constr -> constr -val subst_term_occ_decl : occs:int list -> what:constr -> - where:named_declaration -> named_declaration - -(* [replace_term c by_c in_t substitutes c by by_c in in_t *) -val replace_term : constr -> constr -> constr -> constr - -(* [subst_meta bl c] substitutes the metavar $i$ by $c_i$ in [c] - for each binding $(i,c_i)$ in [bl], - and raises [Not_found] if [c] contains a meta that is not in the - association list *) - -val subst_meta : (int * constr) list -> constr -> constr - -(*s Generic representation of constructions *) - -type fix_kind = RFix of (int array * int) | RCoFix of int - -type constr_operator = - | OpMeta of int - | OpSort of sorts - | OpRel of int | OpVar of identifier - | OpCast | OpProd of name | OpLambda of name | OpLetIn of name - | OpApp | OpConst of constant - | OpEvar of existential_key - | OpMutInd of inductive - | OpMutConstruct of constructor - | OpMutCase of case_info - | OpRec of fix_kind * name array - - -val splay_constr : constr -> constr_operator * constr array -val gather_constr : constr_operator * constr array -> constr -(*i -val splay_constr : ('a,'a)kind_of_term -> constr_operator * 'a array -val gather_constr : constr_operator * 'a array -> ('a,'a) kind_of_term -i*) -val splay_constr_with_binders : constr -> - constr_operator * rel_declaration list * constr array -val gather_constr_with_binders : - constr_operator * rel_declaration list * constr array - -> constr - -val generic_fold_left : - ('a -> constr -> 'a) -> 'a -> rel_declaration list - -> constr array -> 'a - (*s Functionals working on the immediate subterm of a construction *) (* [fold_constr f acc c] folds [f] on the immediate subterms of [c] @@ -572,21 +453,6 @@ val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -(* [iter_constr 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 : (constr -> unit) -> constr -> unit - -(* [iter_constr_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_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit - (* [map_constr 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 *) @@ -602,34 +468,14 @@ val map_constr : (constr -> constr) -> constr -> constr val map_constr_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr -(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate - subterms of [c]; it carries an extra data [l] (typically a name - list) which is processed by [g na] (which typically cons [na] to - [l]) at each binder traversal (with name [na]); it is not recursive - and the order with which subterms are processed is not specified *) - -val map_constr_with_named_binders : - (name -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr - -(* [map_constr_with_binders_left_to_right 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; the subterms are processed from left - to right according to the usual representation of the constructions - (this may matter if [f] does a side-effect); it is not recursive *) - -val map_constr_with_binders_left_to_right : - ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr - -(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate - subterms of [c]; it carries an extra data [l] (typically a name - list) which is processed by [g na] (which typically cons [na] to - [l]) at each binder traversal (with name [na]); it is not recursive - and the order with which subterms are processed is not specified *) +(* [iter_constr_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 map_constr_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) -> - 'a -> constr -> constr +val iter_constr_with_binders : + ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit (* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare the immediate subterms of [c1] of [c2] if needed; Cast's, binders @@ -637,7 +483,7 @@ val map_constr_with_full_binders : val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool -(*s Hash-consing functions for constr. *) +(*********************************************************************) val hcons_constr: (section_path -> section_path) * |