More equality functions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 108 insertions, 0 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 6b45c8897..b9469bdf3 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -17,6 +17,18 @@ open Decl_kinds
 (***********************)
 (* For binders parsing *)
 
+let binding_kind_eq bk1 bk2 = match bk1, bk2 with
+| Explicit, Explicit -> true
+| Implicit, Implicit -> true
+| _ -> false
+
+let binder_kind_eq b1 b2 = match b1, b2 with
+| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
+| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) ->
+  binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 &&
+  (if b1 then b2 else not b2)
+| _ -> false
+
 let default_binder_kind = Default Explicit
 
 let names_of_local_assums bl =
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 63c0043c0..bd118bbce 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -24,6 +24,10 @@ val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
 
 val local_binders_loc : local_binder list -> Loc.t
 
+val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
+
+val binder_kind_eq : binder_kind -> binder_kind -> bool
+
 val default_binder_kind : binder_kind
 
 val mkIdentC : identifier -> constr_expr
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 83e4c4415..57de9da33 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1175,6 +1175,13 @@ let intern_ind_pattern genv env pat =
 (**********************************************************************)
 (* Utilities for application                                          *)
 
+let explicitation_eq ex1 ex2 = match ex1, ex2 with
+| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
+  Int.equal i1 i2 && Option.Misc.compare id_eq id1 id2
+| ExplByName id1, ExplByName id2 ->
+  id_eq id1 id2
+| _ -> false
+
 let merge_impargs l args =
   List.fold_right (fun a l ->
     match a with
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 28e7e2985..6e2c9e883 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -188,3 +188,8 @@ val parsing_explicit : bool ref
 
 (** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
+
+(** Nothing to do here *)
+
+val explicitation_eq : explicitation -> explicitation -> bool
+
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 9e3528cf4..1192423c2 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -36,6 +36,32 @@ type argument_type =
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
+let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
+| BoolArgType, BoolArgType -> true
+| IntArgType, IntArgType -> true
+| IntOrVarArgType, IntOrVarArgType -> true
+| StringArgType, StringArgType -> true
+| PreIdentArgType, PreIdentArgType -> true
+| IntroPatternArgType, IntroPatternArgType -> true
+| IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
+| VarArgType, VarArgType -> true
+| RefArgType, RefArgType -> true
+| SortArgType, SortArgType -> true
+| ConstrArgType, ConstrArgType -> true
+| ConstrMayEvalArgType, ConstrMayEvalArgType -> true
+| QuantHypArgType, QuantHypArgType -> true
+| OpenConstrArgType b1, OpenConstrArgType b2 -> (b1 : bool) == b2
+| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true
+| BindingsArgType, BindingsArgType -> true
+| RedExprArgType, RedExprArgType -> true
+| List0ArgType arg1, List0ArgType arg2 -> argument_type_eq arg1 arg2
+| List1ArgType arg1, List1ArgType arg2 -> argument_type_eq arg1 arg2
+| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2
+| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) ->
+  argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r
+| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2
+| _ -> false
+
 let loc_of_or_by_notation f = function
   | AN c -> f c
   | ByNotation (loc,s,_) -> loc
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 37a67eb3c..b8ed6f374 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -273,6 +273,8 @@ type argument_type =
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
+val argument_type_eq : argument_type -> argument_type -> bool
+
 val genarg_tag : 'a generic_argument -> argument_type
 
 val unquote : ('a,'co) abstract_argument_type -> argument_type
diff --git a/interp/notation.ml b/interp/notation.ml
index 58a6d0593..a3a6708eb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -75,6 +75,17 @@ let init_scope_map () =
 (**********************************************************************)
 (* Operations on scopes *)
 
+let parenRelation_eq t1 t2 = match t1, t2 with
+| L, L | E, E | Any, Any -> true
+| Prec l1, Prec l2 -> Int.equal l1 l2
+| _ -> false
+
+let level_eq (l1, t1) (l2, t2) =
+  let tolerability_eq (i1, r1) (i2, r2) =
+    Int.equal i1 i2 && parenRelation_eq r1 r2
+  in
+  Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+
 let declare_scope scope =
   try let _ = Gmap.find scope !scope_map in ()
   with Not_found ->
@@ -624,6 +635,14 @@ type symbol =
   | SProdList of identifier * symbol list
   | Break of int
 
+let rec symbol_eq s1 s2 = match s1, s2 with
+| Terminal s1, Terminal s2 -> String.equal s1 s2
+| NonTerminal id1, NonTerminal id2 -> id_eq id1 id2
+| SProdList (id1, l1), SProdList (id2, l2) ->
+  id_eq id1 id2 && List.equal symbol_eq l1 l2
+| Break i1, Break i2 -> Int.equal i1 i2
+| _ -> false
+
 let rec string_of_symbol = function
   | NonTerminal _ -> ["_"]
   | Terminal "_" -> ["'_'"]
diff --git a/interp/notation.mli b/interp/notation.mli
index 88574636f..5c8dbb40b 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -35,6 +35,8 @@ val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
 
+val level_eq : level -> level -> bool
+
 (** Check where a scope is opened or not in a scope list, or in
  * the current opened scopes *)
 val scope_is_open_in_scopes : scope_name -> scopes -> bool
@@ -171,6 +173,8 @@ type symbol =
   | SProdList of identifier * symbol list
   | Break of int
 
+val symbol_eq : symbol -> symbol -> bool
+
 val make_notation_key : symbol list -> notation
 val decompose_notation_key : notation -> symbol list
 
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index a4eab42d0..7da2a7faa 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -19,6 +19,9 @@ open Names
 type level = Expand | Level of int | Opaque
 let default = Level 0
 let transparent = default
+let is_transparent = function
+| Level 0 -> true
+| _ -> false
 
 type oracle = level Idmap.t * level Cmap.t
 
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index f875fabf2..2a6db4b4b 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -22,6 +22,9 @@ val oracle_order : bool -> 'a tableKey -> 'a tableKey -> bool
 type level = Expand | Level of int | Opaque
 val transparent : level
 
+(** Check whether a level is transparent *)
+val is_transparent : level -> bool
+
 val get_strategy : 'a tableKey -> level
 
 (** Sets the level of a constant.
diff --git a/lib/loc.ml b/lib/loc.ml
index 57c928bbc..e87ad132e 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -33,6 +33,8 @@ let ghost = {
   fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
   bp = 0; ep = 0; }
 
+let is_ghost loc = Pervasives.(=) loc ghost (** FIXME *)
+
 let merge loc1 loc2 =
   if loc1.bp < loc2.bp then
     if loc1.ep < loc2.ep then {
diff --git a/lib/loc.mli b/lib/loc.mli
index 0b6ba544d..c712cddd9 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -32,6 +32,9 @@ val make_loc : int * int -> t
 val ghost : t
 (** Dummy location *)
 
+val is_ghost : t -> bool
+(** Test whether the location is meaningful *)
+
 val merge : t -> t -> t
 
 val raise : t -> exn -> 'a
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 2f4707406..d8cfde590 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -53,6 +53,14 @@ let coe_info_typ_equal c1 c2 =
     c1.coe_is_identity == c2.coe_is_identity &&
     Int.equal c1.coe_param c2.coe_param
 
+let cl_typ_eq t1 t2 = match t1, t2 with
+| CL_SORT, CL_SORT -> true
+| CL_FUN, CL_FUN -> true
+| CL_SECVAR v1, CL_SECVAR v2 -> id_eq v1 v2
+| CL_CONST c1, CL_CONST c2 -> eq_constant c1 c2
+| CL_IND i1, CL_IND i2 -> eq_ind i1 i2
+| _ -> false
+
 type cl_index = int
 
 type coe_index = coe_info_typ
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 1cbacdfa6..82af9d418 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -22,6 +22,9 @@ type cl_typ =
   | CL_CONST of constant
   | CL_IND of inductive
 
+(** Equality over [cl_typ] *)
+val cl_typ_eq : cl_typ -> cl_typ -> bool
+
 val subst_cl_typ : substitution -> cl_typ -> cl_typ
 
 (** This is the type of infos for declared classes *)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 161243587..22f154795 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -40,6 +40,9 @@ let nowhere = { onhyps=Some[]; concl_occs=NoOccurrences }
 let onHyp h =
   { onhyps=Some[(AllOccurrences,h),InHyp]; concl_occs=NoOccurrences }
 
+let is_nowhere = function
+| { onhyps=Some[]; concl_occs=NoOccurrences } -> true
+| _ -> false
 
 (** Clause conversion functions, parametrized by a hyp enumeration function *)
 
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 15ab0c94b..bd4df6edd 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -28,6 +28,10 @@ val onConcl : 'a clause_expr
 val nowhere : 'a clause_expr
 val onHyp : 'a -> 'a clause_expr
 
+(** Tests *)
+
+val is_nowhere : 'a clause_expr -> bool
+
 (** Clause conversion functions, parametrized by a hyp enumeration function *)
 
 val simple_clause_of : (unit -> identifier list) -> clause -> simple_clause