diff options
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 8 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 15 | ||||
| -rw-r--r-- | intf/notation_term.ml | 5 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 3 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 7 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 5 |
7 files changed, 36 insertions, 11 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6a415a8e5..63cf66bdd 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -767,11 +767,11 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder true -> + | NtnTypeBinder NtnParsedAsConstr -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,scl) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder false -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> let binders,binders' = bind id scl binders binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeConstrList -> diff --git a/interp/notation.ml b/interp/notation.ml index e6186e08c..e2e769d2f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -622,9 +622,15 @@ let availability_of_prim_token n printer_scope local_scopes = let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 +let notation_binder_source_eq s1 s2 = match s1, s2 with + | NtnParsedAsConstr, NtnParsedAsConstr -> true + | NtnParsedAsIdent, NtnParsedAsIdent -> true + | NtnParsedAsPattern, NtnParsedAsPattern -> true + | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false + let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true -| NtnTypeBinder b1, NtnTypeBinder b2 -> b1 = (b2:bool) +| NtnTypeBinder s1, NtnTypeBinder s2 -> notation_binder_source_eq s1 s2 | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ec568823e..b7c1d84f1 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -667,6 +667,10 @@ let is_onlybinding_meta id metas = try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false with Not_found -> false +let is_onlybinding_pattern_like_meta id metas = + try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsConstr | NtnParsedAsPattern) -> true | _ -> false + with Not_found -> false + let is_bindinglist_meta id metas = try match Id.List.assoc id metas with _,NtnTypeBinderList -> true | _ -> false with Not_found -> false @@ -965,7 +969,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with let rec match_cases_pattern_binders metas (alp,sigma as acc) pat1 pat2 = match DAst.get pat1, DAst.get pat2 with - | _, PatVar (Name id2) when is_onlybinding_meta id2 metas -> + | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_env alp sigma id2 pat1 | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2) @@ -1084,7 +1088,8 @@ let rec match_ inner u alp metas sigma a1 a2 = match DAst.get a1, a2 with (* Matching notation variable *) | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1 - | r1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | r1, NVar id2 when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1 (* Matching recursive notations for terms *) @@ -1248,7 +1253,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in match_in u alp metas sigma b1 b2 | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(_,[cp],b1))]), Name id - when is_gvar p e && is_onlybinding_meta id metas && not (occur_glob_constr p b1) -> + when is_gvar p e && is_onlybinding_pattern_like_meta id metas && not (occur_glob_constr p b1) -> let alp,sigma = bind_binding_env alp sigma id cp in match_in u alp metas sigma b1 b2 | _, _, Name id when is_bindinglist_meta id metas && (not isprod || na1 != Anonymous)-> @@ -1276,10 +1281,10 @@ let match_notation_constr u c (metas,pat) = | NtnTypeConstr -> let term = try Id.List.assoc x terms with Not_found -> raise No_match in ((term, scl)::terms',termlists',binders',binderlists') - | NtnTypeBinder true -> + | NtnTypeBinder NtnParsedAsConstr -> let v = glob_constr_of_cases_pattern (Id.List.assoc x binders) in ((v,scl)::terms',termlists',binders',binderlists') - | NtnTypeBinder false -> + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists') diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 83cc454f4..0f4bfef60 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -60,8 +60,11 @@ type subscopes = tmp_scope_name option * scope_name list (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y, x carries the sequence of objects bound to the list x..y *) + +type notation_binder_source = NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern + type notation_var_instance_type = - | NtnTypeConstr | NtnTypeBinder of bool | NtnTypeConstrList | NtnTypeBinderList + | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList (** Type of variables when interpreting a constr_expr as a notation_constr: in a recursive pattern x..y, both x and y carry the individual type diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index fb2d375c2..7c47c0885 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -197,3 +197,6 @@ fun x : nat => if x is n .+ 1 then n else 1 : Set exists2' {{x, y}}, x = 0 & y = 0 : Prop +exists2 x : nat * nat, + let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 46e0c1b1b..ee6f0a09e 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -338,9 +338,16 @@ Check fun x => if x is n.+1 then n else 1. Check {(x,y)|x+y=0}. +Module D. Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q)) (at level 200, x pattern, p at level 200, right associativity, format "'[' 'exists2'' '/ ' x , '/ ' '[' p & '/' q ']' ']'") : type_scope. Check exists2' (x,y), x=0 & y=0. +End D. + +(* Ensuring for reparsability that printer of notations does not use a + pattern where only an ident could be reparsed *) + +Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y). diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 6ee0d6c82..e142f2ab8 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -962,9 +962,10 @@ let make_internalization_vars recvars mainvars typs = let make_interpretation_type isrec isonlybinding = function | ETConstr _ -> if isrec then NtnTypeConstrList else - if isonlybinding then NtnTypeBinder true (* Parsed as constr, but interpreted as binder *) + if isonlybinding then NtnTypeBinder NtnParsedAsConstr (* Parsed as constr, but interpreted as binder *) else NtnTypeConstr - | ETName | ETPattern _ -> NtnTypeBinder false (* Parsed as ident/pattern, primarily interpreted as binder *) + | ETName -> NtnTypeBinder NtnParsedAsIdent + | ETPattern _ -> NtnTypeBinder NtnParsedAsPattern (* Parsed as ident/pattern, primarily interpreted as binder *) | ETBigint | ETReference | ETOther _ -> NtnTypeConstr | ETBinder _ -> if isrec then NtnTypeBinderList |