More equality functions

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

1 files changed, 19 insertions, 0 deletions

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 "_" -> ["'_'"]