diff options
| -rw-r--r-- | interp/notation_ops.ml | 25 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 8 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 12 |
3 files changed, 43 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 2fa8903c4..ef363f540 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -284,7 +284,7 @@ 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 = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in let iterator = f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator else iterator) in @@ -614,6 +614,9 @@ let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v = (* TODO: handle the case of multiple occs in different scopes *) ((var,v)::terms,onlybinders,termlists,binderlists) +let add_termlist_env (terms,onlybinders,termlists,binderlists) var vl = + (terms,onlybinders,(var,vl)::termlists,binderlists) + let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v = (* TODO: handle the case of multiple occs in different scopes *) (terms,(var,v)::onlybinders,termlists,binderlists) @@ -642,6 +645,24 @@ let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = else raise No_match with Not_found -> add_env alp sigma var v +let bind_termlist_env (terms,onlybinders,termlists,binderlists as sigma) var vl = + try + let vl' = Id.List.assoc var termlists in + let unify_term v v' = + match v, v' with + | GHole _, _ -> v' + | _, GHole _ -> v + | _, _ -> if glob_constr_eq v v' then v' else raise No_match in + let rec unify vl vl' = + match vl, vl' with + | [], [] -> [] + | v :: vl, v' :: vl' -> unify_term v v' :: unify vl vl' + | _ -> raise No_match in + let vl = unify vl vl' in + let sigma = (terms,onlybinders,Id.List.remove_assoc var termlists,binderlists) in + add_termlist_env sigma var vl + with Not_found -> add_termlist_env sigma var vl + let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = try let v' = Id.List.assoc var onlybinders in @@ -823,7 +844,7 @@ let match_alist match_fun metas sigma rest x iter termin lassoc = (* registered for binders *) bind_bindinglist_as_term_env sigma x (if lassoc then l else List.rev l) else - (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) + bind_termlist_env sigma x (if lassoc then l else List.rev l) let does_not_come_from_already_eta_expanded_var = (* This is hack to avoid looping on a rule with rhs of the form *) diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out new file mode 100644 index 000000000..b3d2580ac --- /dev/null +++ b/test-suite/output/Notations3.out @@ -0,0 +1,8 @@ +[<0, 2 >] + : nat * nat * (nat * nat) +[<0, 2 >] + : nat * nat * (nat * nat) +(0, 2, (2, 2)) + : nat * nat * (nat * nat) +pair (pair O (S (S O))) (pair (S (S O)) O) + : prod (prod nat nat) (prod nat nat) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v new file mode 100644 index 000000000..32d70ac18 --- /dev/null +++ b/test-suite/output/Notations3.v @@ -0,0 +1,12 @@ +(**********************************************************************) +(* Check printing of notations with several instances of a recursive pattern *) +(* Was wrong but I could not trigger a problem due to the collision between *) +(* different instances of ".." *) + +Notation "[< x , y , .. , z >]" := (pair (.. (pair x y) ..) z,pair y ( .. (pair z x) ..)). +Check [<0,2>]. +Check ((0,2),(2,0)). +Check ((0,2),(2,2)). +Unset Printing Notations. +Check [<0,2>]. +Set Printing Notations. |