More equality functions

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

8 files changed, 79 insertions, 0 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 6b45c88975..b9469bdf37 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 63c0043c0b..bd118bbce5 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 83e4c44152..57de9da33a 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 28e7e2985f..6e2c9e8832 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 9e3528cf41..1192423c2c 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 37a67eb3cd..b8ed6f3749 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 58a6d05938..a3a6708eb7 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 88574636fe..5c8dbb40bf 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