diff options
author | 2016-09-28 15:29:58 +0200 | |
---|---|---|
committer | 2016-09-28 16:14:11 +0200 | |
commit | dfadb394640b3d09eb6134b73d0f3e931bd70af1 (patch) | |
tree | b7f0bba04890b0c905f06829d97d98642168b38f /interp/notation_ops.ml | |
parent | 8e0f29cb69f06b64d74b18b09fb6a717034f1140 (diff) |
Warning about similar notations now up to alpha-conversion.
This allows to define on purpose the very same notation in different
files, as currently the notations for *, +, - in Nat.v and Peano.v
(with the first one using variables n and m and the second one using
the default variables used by Infix, namely x and y).
This makes also the "notation-overridden" warning less enigmatic
facing two notations which are the same up to the choice of names.
Diffstat (limited to 'interp/notation_ops.ml')
-rw-r--r-- | interp/notation_ops.ml | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1f29a2948..cc81a0091 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -47,62 +47,62 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GHole _ | GSort _ | GLetIn _), _ -> false -let rec eq_notation_constr t1 t2 = match t1, t2 with +let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NRef gr1, NRef gr2 -> eq_gr gr1 gr2 -| NVar id1, NVar id2 -> Id.equal id1 id2 +| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2) | NApp (t1, a1), NApp (t2, a2) -> - eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 + (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) 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 + Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) 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 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NProd (na1, t1, u1), NProd (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) 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 + Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 | NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) 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 + (eq_notation_constr vars) 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 + (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 in - Option.equal eq_notation_constr o1 o2 && + Option.equal (eq_notation_constr vars) 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 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> - eq_notation_constr t1 t2 && + (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr u1 u2 && - eq_notation_constr r1 r2 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) u1 u2 && + (eq_notation_constr vars) 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 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) 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 + Array.equal (eq_notation_constr vars) us1 us2 && + Array.equal (eq_notation_constr vars) rs1 rs2 | NSort s1, NSort s2 -> Miscops.glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> - eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 + (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ | NRec _ | NSort _ | NCast _), _ -> false |