From dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 25 Nov 2017 20:50:03 +0100 Subject: Notations: Adding modifiers to tell which kind of binder a constr can parse. Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}. --- CHANGES | 4 +- interp/constrintern.ml | 75 +++++++++++++++++++++++++--------- interp/notation.ml | 13 +++--- interp/notation_ops.ml | 28 +++++++++---- intf/extend.ml | 8 +++- intf/notation_term.ml | 9 +++- intf/vernacexpr.ml | 1 + parsing/g_vernac.ml4 | 16 +++++++- printing/ppvernac.ml | 15 ++++++- test-suite/output/Notations3.out | 2 - test-suite/output/Notations3.v | 2 - test-suite/success/Notations2.v | 19 ++++++++- vernac/metasyntax.ml | 88 ++++++++++++++++++++++++++-------------- 13 files changed, 203 insertions(+), 77 deletions(-) diff --git a/CHANGES b/CHANGES index 74e120a316..32a533d14f 100644 --- a/CHANGES +++ b/CHANGES @@ -12,7 +12,9 @@ Notations opened rather than to the latest notations defined independently of whether they are in an opened scope or not. - Notations can now refer to the syntactic category of patterns (as in - "fun 'pat =>" or "match p with pat => ... end"). + "fun 'pat =>" or "match p with pat => ... end"). Two variants are + available, depending on whether a single variable is considered as a + pattern or not. - Recursive notations now support ".." patterns with several occurrences of the recursive term or binder, possibly mixing terms and binders, possibly in reverse left-to-right order. diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 379d09e895..158ac24b2e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -549,6 +549,18 @@ let is_var store pat = | PatVar na -> store na; true | _ -> false +let out_var pat = + match pat.CAst.v with + | CPatAtom (Some (Ident (_,id))) -> Name id + | CPatAtom None -> Anonymous + | _ -> assert false + +let term_of_name = function + | Name id -> DAst.make (GVar id) + | Anonymous -> + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None)) + let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous | Name id -> @@ -564,13 +576,21 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam with Not_found -> try (* Trying to associate a pattern *) - let pat,scopes = Id.Map.find id binders in + let pat,(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in - let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in - let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na - | _ -> Some ((List.map snd ids,disjpat),id), snd na in - (renaming,env), pat, na + if onlyident then + (* Do not try to interpret a variable as a constructor *) + let na = out_var pat in + let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in + (renaming,env), None, na + else + (* Interpret as a pattern *) + let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + let pat, na = + match disjpat with + | [pat] when is_var store pat -> let na = get () in None, na + | _ -> Some ((List.map snd ids,disjpat),id), snd na in + (renaming,env), pat, na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -688,12 +708,15 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let gc = intern nenv c in (gc, Some c) in - let mk_env' (c, (tmp_scope, subscopes)) = + let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in - match disjpat with - | [pat] -> (glob_constr_of_cases_pattern pat, None) - | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc () + if onlyident then + let na = out_var c in term_of_name na, None + else + let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in + match disjpat with + | [pat] -> (glob_constr_of_cases_pattern pat, None) + | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc () in let terms = Id.Map.map mk_env terms in let binders = Id.Map.map mk_env' binders in @@ -744,15 +767,18 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = scopes = subscopes @ env.scopes} a with Not_found -> try - let pat,scopes = Id.Map.find id binders in + let pat,(onlyident,scopes) = Id.Map.find id binders in let env = set_env_scopes env scopes in (* We deactivate impls to avoid the check on hidden parameters *) (* and since we are only interested in the pattern as a term *) let env = reset_hidden_inductive_implicit_test env in - let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in - match disjpat with - | [pat] -> glob_constr_of_cases_pattern pat - | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") + if onlyident then + term_of_name (out_var pat) + else + let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + match disjpat with + | [pat] -> glob_constr_of_cases_pattern pat + | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try match binderopt with @@ -774,6 +800,10 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = into a substitution for interpretation and based on binding/constr distinction *) +let cases_pattern_of_name (loc,na) = + let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in + CAst.make ?loc (CPatAtom atom) + let split_by_type ids subst = let bind id scl l s = match l with @@ -785,12 +815,17 @@ 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 NtnParsedAsConstr -> + | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) -> + 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,(false,scl)) binders' in + (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') + | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent -> 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 + let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> - let binders,binders' = bind id scl binders binders' in + | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) -> + let onlyident = (x = NtnParsedAsIdent) in + let binders,binders' = bind id (onlyident,scl) binders binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') | NtnTypeConstrList -> let termlists,termlists' = bind id scl termlists termlists' in diff --git a/interp/notation.ml b/interp/notation.ml index 13ff960f64..ea7ef21b19 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -97,9 +97,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with | ETBigint, ETBigint -> true | ETBinder b1, ETBinder b2 -> b1 == b2 | ETConstr lev1, ETConstr lev2 -> eq lev1 lev2 -| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2 +| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2 +| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2 | ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2' -| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false +| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) = let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in @@ -626,10 +627,10 @@ 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 +| NtnParsedAsIdent, NtnParsedAsIdent -> true +| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 +| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2 +| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 44073c3b5e..c65f4785ef 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -671,12 +671,20 @@ let is_term_meta id metas = try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false with Not_found -> false +let is_onlybinding_strict_meta id metas = + try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsPattern true) -> true | _ -> false + with Not_found -> false + 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 +let is_onlybinding_pattern_like_meta isvar id metas = + try match Id.List.assoc id metas with + | _,NtnTypeBinder (NtnBinderParsedAsConstr + (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true + | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar) + | _ -> false with Not_found -> false let is_bindinglist_meta id metas = @@ -962,6 +970,8 @@ let match_opt f sigma t1 t2 = match (t1,t2) with | _ -> raise No_match let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with + | (na1,Name id2) when is_onlybinding_strict_meta id2 metas -> + raise No_match | (na1,Name id2) when is_onlybinding_meta id2 metas -> bind_binding_env alp sigma id2 [DAst.make (PatVar na1)] | (Name id1,Name id2) when is_term_meta id2 metas -> @@ -977,7 +987,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1 pat2 = match DAst.get pat1, DAst.get pat2 with - | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas -> + | PatVar _, PatVar (Name id2) when is_onlybinding_pattern_like_meta true id2 metas -> + bind_binding_env alp sigma id2 [pat1] + | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_env alp sigma id2 [pat1] | PatVar na1, PatVar na2 -> match_names metas acc na1 na2 | _, PatVar Anonymous when allow_catchall -> acc @@ -1093,7 +1105,9 @@ 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_pattern_like_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1 + | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match | 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 @@ -1232,7 +1246,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 = match_in u alp metas sigma b1 b2 | _ -> assert false) | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id - when is_gvar p e && is_onlybinding_pattern_like_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> + when is_gvar p e && is_onlybinding_pattern_like_meta false id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 -> (match get () with | [(_,(ids,disj_of_patl,b1))] -> let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in @@ -1276,13 +1290,13 @@ 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 NtnParsedAsConstr -> + | NtnTypeBinder (NtnBinderParsedAsConstr _) -> (match Id.List.assoc x binders with | [pat] -> let v = glob_constr_of_cases_pattern pat in ((v,scl)::terms',termlists',binders',binderlists') | _ -> raise No_match) - | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) -> + | 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/extend.ml b/intf/extend.ml index 813ed6dc6c..78f0aa1178 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -29,6 +29,11 @@ type production_level = | NextLevel | NumLevel of int +type constr_as_binder_kind = + | AsIdent + | AsIdentOrPattern + | AsStrictPattern + (** User-level types used to tell how to parse or interpret of the non-terminal *) type 'a constr_entry_key_gen = @@ -37,7 +42,8 @@ type 'a constr_entry_key_gen = | ETBigint | ETBinder of bool (* open list of binders if true, closed list of binders otherwise *) | ETConstr of 'a - | ETPattern of int option + | ETConstrAsBinder of constr_as_binder_kind * 'a + | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *) | ETOther of string * string (** Entries level (left-hand side of grammar rules) *) diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 0f4bfef600..86f5adbd78 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -61,7 +61,14 @@ 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_binder_source = + (* This accepts only pattern *) + (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *) + | NtnParsedAsPattern of bool + (* This accepts only ident *) + | NtnParsedAsIdent + (* This accepts ident, or pattern, or both *) + | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind type notation_var_instance_type = | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 8e0fe54c55..0b5009e26b 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -214,6 +214,7 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 009c1c19a6..cca1b29898 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1174,6 +1174,7 @@ GEXTEND Gram | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) + | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,lev) | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) ] ] ; @@ -1181,9 +1182,20 @@ GEXTEND Gram [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference | IDENT "bigint" -> ETBigint | IDENT "binder" -> ETBinder true - | IDENT "pattern" -> ETPattern None - | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (Some n) + | IDENT "constr"; n = OPT at_level; b = constr_as_binder_kind -> ETConstrAsBinder (b,n) + | IDENT "pattern" -> ETPattern (false,None) + | IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (false,Some n) + | IDENT "strict"; IDENT "pattern" -> ETPattern (true,None) + | IDENT "strict"; IDENT "pattern"; "at"; IDENT "level"; n = natural -> ETPattern (true,Some n) | IDENT "closed"; IDENT "binder" -> ETBinder false ] ] ; + at_level: + [ [ "at"; n = level -> n ] ] + ; + constr_as_binder_kind: + [ [ "as"; IDENT "ident" -> AsIdent + | "as"; IDENT "pattern" -> AsIdentOrPattern + | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ] + ; END diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 42329d03a7..2fc7843eda 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -97,13 +97,21 @@ open Decl_kinds | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level" + let pr_constr_as_binder_kind = function + | AsIdent -> keyword "as ident" + | AsIdentOrPattern -> keyword "as pattern" + | AsStrictPattern -> keyword "as strict pattern" + + let pr_strict b = if b then str "strict " else mt () + let pr_set_entry_type pr = function | ETName -> str"ident" | ETReference -> str"global" - | ETPattern None -> str"pattern" - | ETPattern (Some n) -> str"pattern" ++ spc () ++ pr_at_level (NumLevel n) + | ETPattern (b,None) -> pr_strict b ++ str"pattern" + | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n) | ETConstr lev -> str"constr" ++ pr lev | ETOther (_,e) -> str e + | ETConstrAsBinder (bk,lev) -> pr lev ++ spc () ++ pr_constr_as_binder_kind bk | ETBigint -> str "bigint" | ETBinder true -> str "binder" | ETBinder false -> str "closed binder" @@ -373,6 +381,9 @@ open Decl_kinds let pr_syntax_modifier = function | SetItemLevel (l,n) -> prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n + | SetItemLevelAsBinder (l,bk,n) -> + prlist_with_sep sep_v2 str l ++ + spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk | SetLevel n -> pr_at_level (NumLevel n) | SetAssoc LeftA -> keyword "left associativity" | SetAssoc RightA -> keyword "right associativity" diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 6d195b5122..3fd4c1c311 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -194,8 +194,6 @@ pair (prod nat (prod nat nat))) (prod (prod nat nat) nat) fun x : nat => if x is n .+ 1 then n else 1 : nat -> nat -{{{x, y}} : nat * nat | x + y = 0} - : Set exists2' {{x, y}}, x = 0 & y = 0 : Prop exists2 x : nat * nat, diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index b4ad4a7b3c..9ea218481e 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -341,8 +341,6 @@ Check fun x => if x is n.+1 then n else 1. (* Examples with binding patterns *) -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, diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 08d904cea0..7c2cf3ee52 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -98,12 +98,12 @@ Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200). (* 11. Notations with needed factorization of a recursive pattern *) (* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *) -Module A. +Module M11. Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..). Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..). Check [:: 1 ; 2 ; 3 ]. Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *) -End A. +End M11. (* 12. Preventively check that a variable which does not occur can be instantiated *) (* by any term. In particular, it should not be restricted to a binder *) @@ -111,3 +111,18 @@ Module M12. Notation "N ++ x" := (S x) (only parsing). Check 2 ++ 0. End M12. + +(* 13. Check that internal data about associativity are not used in comparing levels *) +Module M13. +Notation "x ;; z" := (x + z) + (at level 100, z at level 200, only parsing, right associativity). +Notation "x ;; z" := (x * z) + (at level 100, z at level 200, only parsing) : foo_scope. +End M13. + +(* 14. Check that a notation with a "ident" binder does not include a pattern *) +Module M14. +Notation "'myexists' x , p" := (ex (fun x => p)) + (at level 200, x ident, p at level 200, right associativity) : type_scope. +Check myexists I, I = 0. (* Should not be seen as a constructor *) +End M14. diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 44a7462dec..524c9b32b1 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -285,14 +285,17 @@ let prec_assoc = function | LeftA -> (E,L) | NonA -> (L,L) -let precedence_of_entry_type from = function - | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n - | ETConstr (NumLevel n,BorderProd (b,Some a)) -> +let precedence_of_position_and_level from = function + | NumLevel n, BorderProd (_,None) -> n, Prec n + | NumLevel n, BorderProd (b,Some a) -> n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp - | ETConstr (NumLevel n,InternalProd) -> n, Prec n - | ETConstr (NextLevel,_) -> from, L - | ETPattern n -> let n = match n with None -> 0 | Some n -> n in n, Prec n - | _ -> 0, E (* ?? *) + | NumLevel n, InternalProd -> n, Prec n + | NextLevel, _ -> from, L + +let precedence_of_entry_type from = function + | ETConstr x | ETConstrAsBinder (_,x) -> precedence_of_position_and_level from x + | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n + | _ -> 0, E (* should not matter *) (* Some breaking examples *) (* "x = y" : "x /1 = y" (breaks before any symbol) *) @@ -361,7 +364,7 @@ let unparsing_metavar i from typs = let x = List.nth typs (i-1) in let prec = snd (precedence_of_entry_type from x) in match x with - | ETConstr _ | ETReference | ETBigint -> + | ETConstr _ | ETConstrAsBinder _ | ETReference | ETBigint -> UnpMetaVar (i,prec) | ETPattern _ -> UnpBinderMetaVar (i,prec) @@ -596,7 +599,7 @@ let expand_list_rule typ tkl x n p ll = let is_constr_typ typ x etyps = match List.assoc x etyps with - | ETConstr typ' -> typ = typ' + | ETConstr typ' | ETConstrAsBinder (_,typ') -> typ = typ' | _ -> false let include_possible_similar_trailing_pattern typ etyps sl l = @@ -614,8 +617,8 @@ let prod_entry_type = function | ETReference -> ETProdReference | ETBigint -> ETProdBigint | ETBinder _ -> assert false (* See check_binder_type *) - | ETConstr p -> ETProdConstr p - | ETPattern n -> ETProdPattern (match n with None -> 0 | Some n -> n) + | ETConstr p | ETConstrAsBinder (_,p) -> ETProdConstr p + | ETPattern (_,n) -> ETProdPattern (match n with None -> 0 | Some n -> n) | ETOther (s,t) -> ETProdOther (s,t) let make_production etyps symbols = @@ -659,6 +662,7 @@ let rec find_symbols c_current c_next c_last = function let border = function | (_,ETConstr(_,BorderProd (_,a))) :: _ -> a + | (_,(ETConstrAsBinder(_,(_,BorderProd (_,a))))) :: _ -> a | _ -> None let recompute_assoc typs = @@ -679,7 +683,9 @@ let pr_arg_level from (lev,typ) = | (n,Prec m) when Int.equal m n -> str "at level " ++ int n | (n,_) -> str "Unknown level" in Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ - (match typ with ETConstr _ | ETPattern _ -> spc () ++ pplev lev | _ -> mt ()) + (match typ with + | ETConstr _ | ETConstrAsBinder _ | ETPattern _ -> spc () ++ pplev lev + | _ -> mt ()) let pr_level ntn (from,args,typs) = str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++ @@ -811,6 +817,8 @@ let interp_modifiers modl = let open NotationMods in interp { acc with etyps = (id,typ) :: acc.etyps; } l | SetItemLevel ([],n) :: l -> interp acc l + | SetItemLevelAsBinder ([],_,_) :: l -> + interp acc l | SetItemLevel (s::idl,n) :: l -> let id = Id.of_string s in if Id.List.mem_assoc id acc.etyps then @@ -818,8 +826,14 @@ let interp_modifiers modl = let open NotationMods in (str s ++ str " is already assigned to an entry or constr level."); let typ = ETConstr (Some n) in interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l) + | SetItemLevelAsBinder (s::idl,bk,n) :: l -> + let id = Id.of_string s in + if Id.List.mem_assoc id acc.etyps then + user_err ~hdr:"Metasyntax.interp_modifiers" + (str s ++ str " is already assigned to an entry or constr level."); + let typ = ETConstrAsBinder (bk,Some n) in + interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l) | SetLevel n :: l -> - interp { acc with level = Some n; } l | SetAssoc a :: l -> if not (Option.is_empty acc.assoc) then user_err Pp.(str "An associativity is given more than once."); @@ -886,9 +900,14 @@ let set_entry_type etyps (x,typ) = | ETConstr (Some n), (_,BorderProd (left,_)) -> ETConstr (n,BorderProd (left,None)) | ETConstr (Some n), (_,InternalProd) -> ETConstr (n,InternalProd) - | (ETPattern _ | ETName | ETBigint | ETOther _ | - ETReference | ETBinder _ as t), _ -> t + | ETConstrAsBinder (bk, Some n), (_,BorderProd (left,_)) -> + ETConstrAsBinder (bk, (n,BorderProd (left,None))) + | ETConstrAsBinder (bk, Some n), (_,InternalProd) -> + ETConstrAsBinder (bk, (n,InternalProd)) + | ETPattern (b,n), _ -> ETPattern (b,n) + | (ETName | ETBigint | ETReference | ETBinder _ | ETOther _ as x), _ -> x | ETConstr None, _ -> ETConstr typ + | ETConstrAsBinder (bk,None), _ -> ETConstrAsBinder (bk,typ) with Not_found -> ETConstr typ in (x,typ) @@ -909,7 +928,7 @@ let join_auxiliary_recursive_types recvars etyps = let internalization_type_of_entry_type = function | ETBinder _ -> NtnInternTypeOnlyBinder - | ETConstr _ | ETBigint | ETReference + | ETConstr _ | ETConstrAsBinder _ | ETBigint | ETReference | ETName | ETPattern _ | ETOther _ -> NtnInternTypeAny let set_internalization_type typs = @@ -923,10 +942,13 @@ let make_internalization_vars recvars mainvars typs = let make_interpretation_type isrec isonlybinding = function | ETConstr _ -> if isrec then NtnTypeConstrList else - if isonlybinding then NtnTypeBinder NtnParsedAsConstr (* Parsed as constr, but interpreted as binder *) + if isonlybinding then + (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *) + NtnTypeBinder (NtnBinderParsedAsConstr AsIdent) else NtnTypeConstr + | ETConstrAsBinder (bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk) | ETName -> NtnTypeBinder NtnParsedAsIdent - | ETPattern _ -> NtnTypeBinder NtnParsedAsPattern (* Parsed as ident/pattern, primarily interpreted as binder *) + | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *) | ETBigint | ETReference | ETOther _ -> NtnTypeConstr | ETBinder _ -> if isrec then NtnTypeBinderList @@ -982,6 +1004,7 @@ let is_not_printable onlyparse reversibility = function (warn_non_reversible_notation reversibility; true) else onlyparse + let find_precedence lev etyps symbols onlyprint = let first_symbol = let rec aux = function @@ -999,27 +1022,30 @@ let find_precedence lev etyps symbols onlyprint = match first_symbol with | None -> [],0 | Some (NonTerminal x) -> + let test () = + if onlyprint then + if Option.is_empty lev then + user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.") + else [],Option.get lev + else + user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in (try match List.assoc x etyps with - | ETConstr _ -> - if onlyprint then - if Option.is_empty lev then - user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.") - else [],Option.get lev - else - user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") - | ETName | ETBigint | ETReference -> + | ETConstr _ -> test () + | ETConstrAsBinder (_,Some _) -> test () + | (ETName | ETBigint | ETReference) -> begin match lev with | None -> ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0) | Some 0 -> ([],0) | _ -> - user_err Pp.(str "A notation starting with an atomic expression must be at level 0.") + user_err Pp.(str "A notation starting with an atomic expression must be at level 0.") end - | ETPattern _ | ETBinder _ | ETOther _ -> (* Give a default ? *) - if Option.is_empty lev then - user_err Pp.(str "Need an explicit level.") - else [],Option.get lev + | (ETPattern _ | ETBinder _ | ETOther _ | ETConstrAsBinder _) -> + (* Give a default ? *) + if Option.is_empty lev then + user_err Pp.(str "Need an explicit level.") + else [],Option.get lev with Not_found -> if Option.is_empty lev then user_err Pp.(str "A left-recursive notation must have an explicit level.") -- cgit v1.2.3