Fixing equality of notation_constrs. Fixes bug #4136.

4 files changed, 87 insertions, 1 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 6040c33a5e..f498761344 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -516,12 +516,30 @@ let availability_of_prim_token n printer_scope local_scopes =
 
 (* Miscellaneous *)
 
+let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
+
+let ntpe_eq t1 t2 = match t1, t2 with
+| NtnTypeConstr, NtnTypeConstr -> true
+| NtnTypeConstrList, NtnTypeConstrList -> true
+| NtnTypeBinderList, NtnTypeBinderList -> true
+| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false
+
+
+let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) =
+  Id.equal id1 id2 &&
+  pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 &&
+  ntpe_eq tp1 tp2
+
+let interpretation_eq (vars1, t1) (vars2, t2) =
+  List.equal vars_eq vars1 vars2 &&
+  Notation_ops.eq_notation_constr t1 t2
+
 let exists_notation_in_scope scopt ntn r =
   let scope = match scopt with Some s -> s | None -> default_scope in
   try
     let sc = String.Map.find scope !scope_map in
     let (r',_) = String.Map.find ntn sc.notations in
-    Pervasives.(=) r' r (** FIXME *)
+    interpretation_eq r' r
   with Not_found -> false
 
 let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c91c781591..2762dc0b8d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -170,6 +170,69 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
 
 let rec eq_glob_constr t1 t2 = compare_glob_constr eq_glob_constr (fun _ -> ()) t1 t2
 
+let rec eq_notation_constr t1 t2 = match t1, t2 with
+| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NVar id1, NVar id2 -> Id.equal id1 id2
+| NApp (t1, a1), NApp (t2, a2) ->
+  eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2
+| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
+| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
+  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2 && b1 == b2
+| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) ->
+  Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2
+| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) ->
+  Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2
+| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *)
+  let eqpat (p1, t1) (p2, t2) =
+    List.equal cases_pattern_eq p1 p2 &&
+    eq_notation_constr t1 t2
+  in
+  let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
+    let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
+    eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
+  in
+  Option.equal eq_notation_constr o1 o2 &&
+  List.equal eqf r1 r2 &&
+  List.equal eqpat p1 p2
+| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
+  List.equal Name.equal nas1 nas2 &&
+  Name.equal na1 na2 &&
+  Option.equal eq_notation_constr o1 o2 &&
+  eq_notation_constr t1 t2 &&
+  eq_notation_constr u1 u2
+| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+  eq_notation_constr t1 t2 &&
+  Name.equal na1 na2 &&
+  Option.equal eq_notation_constr o1 o2 &&
+  eq_notation_constr u1 u2 &&
+  eq_notation_constr r1 r2
+| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *)
+  let eq (na1, o1, t1) (na2, o2, t2) =
+    Name.equal na1 na2 &&
+    Option.equal eq_notation_constr o1 o2 &&
+    eq_notation_constr t1 t2
+  in
+  Array.equal Id.equal ids1 ids2 &&
+  Array.equal (List.equal eq) ts1 ts2 &&
+  Array.equal eq_notation_constr us1 us2 &&
+  Array.equal eq_notation_constr rs1 rs2
+| NSort s1, NSort s2 ->
+  Miscops.glob_sort_eq s1 s2
+| NPatVar p1, NPatVar p2 ->
+  Id.equal p1 p2
+| NCast (t1, c1), NCast (t2, c2) ->
+  eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2
+| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+  | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
+  | NRec _ | NSort _ | NPatVar _ | NCast _), _ -> false
+
+
 let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
 
 let check_is_hole id = function GHole _ -> () | t ->
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 7283ed6f12..c6770deea2 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -25,6 +25,8 @@ val ldots_var : Id.t
 (** FIXME: nothing to do here *)
 val eq_glob_constr : glob_constr -> glob_constr -> bool
 
+val eq_notation_constr : notation_constr -> notation_constr -> bool
+
 (** Re-interpret a notation as a [glob_constr], taking care of binders     *)
 
 val glob_constr_of_notation_constr_with_binders : Loc.t ->
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 67f3cb4169..e514fd529e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,9 @@ open Glob_term
 
 val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
 
+val cast_type_eq : ('a -> 'a -> bool) ->
+  'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+
 val glob_constr_eq : glob_constr -> glob_constr -> bool
 
 (** Operations on [glob_constr] *)