diff options
| author | Hugo Herbelin | 2016-07-17 09:34:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-17 09:37:53 +0200 |
| commit | d17237cfd3a67b9a93de98a23ae29869456d2028 (patch) | |
| tree | 5a323cfed9cee00a8dc23b1fac710bbe408c23aa /interp/notation_ops.ml | |
| parent | 91f44b164c5d9fa170a8faa7227aff08c1335861 (diff) | |
Fixing interpretation of notations w/ opposite instances of a recursive pattern.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ef363f5402..80c09745d8 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -237,6 +237,8 @@ let check_is_hole id = function GHole _ -> () | t -> strbrk "In recursive notation with binders, " ++ pr_id id ++ strbrk " is expected to come without type.") +let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' + let compare_recursive_parts found f (iterator,subc) = let diff = ref None in let terminator = ref None in @@ -284,7 +286,13 @@ let compare_recursive_parts found f (iterator,subc) = user_err_loc (subtract_loc loc1 loc2,"", str "Both ends of the recursive pattern are the same.") | Some (x,y,Some lassoc) -> - let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in + let newfound,x,y,lassoc = + if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) then + !found,x,y,lassoc + else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) then + !found,y,x,not lassoc + else + (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in let iterator = f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator else iterator) in @@ -357,8 +365,6 @@ let notation_constr_and_vars_of_glob_constr a = (* Side effect *) t, !found -let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' - let check_variables nenv (found,foundrec,foundrecbinding) = let recvars = nenv.ninterp_rec_vars in let fold _ y accu = Id.Set.add y accu in |