diff options
| -rw-r--r-- | interp/constrintern.ml | 33 | ||||
| -rw-r--r-- | intf/constrexpr.mli | 2 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 3 | ||||
| -rw-r--r-- | test-suite/success/Notations2.v | 110 |
4 files changed, 80 insertions, 68 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b62df8dfff..fa38695705 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -918,7 +918,7 @@ let chop_params_pattern loc ind args with_letin = args let find_constructor loc add_params ref = - let cstr = match ref with + let (ind,_ as cstr) = match ref with | ConstructRef cstr -> cstr | IndRef _ -> let error = str "There is an inductive name deep in a \"in\" clause." in @@ -927,15 +927,15 @@ let find_constructor loc add_params ref = let error = str "This reference is not a constructor." in user_err_loc (loc, "find_constructor", error) in - cstr, (function (ind,_ as c) -> match add_params with - |Some nb_args -> + cstr, match add_params with + | Some nb_args -> let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealdecls c) + if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr) then Inductiveops.inductive_nparamdecls ind else Inductiveops.inductive_nparams ind in List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))]) - |None -> []) cstr + | None -> [] let find_pattern_variable = function | Ident (loc,id) -> id @@ -1099,16 +1099,17 @@ let drop_notations_pattern looked_for = let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with | NRef g -> + (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; let () = assert (List.is_empty vars) in let (_,argscs) = find_remaining_scopes [] pats g in Some (g, [], List.map2 (in_pat_sc env) argscs pats) - | NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *) + | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *) test_kind top g; let () = assert (List.is_empty vars) in - let (argscs,_) = find_remaining_scopes pats [] g in - Some (g, List.map2 (in_pat_sc env) argscs pats, []) + Some (g, List.map (in_pat false env) pats, []) | NApp (NRef g,args) -> + (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments loc; @@ -1146,12 +1147,18 @@ let drop_notations_pattern looked_for = | Some (a,b,c) -> RCPatCstr(loc, a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, r, Some expl_pl, pl) -> + | CPatCstr (loc, r, Some expl_pl, pl) -> let g = try locate (snd (qualid_of_reference r)) with Not_found -> raise (InternalizationError (loc,NotAConstructor r)) in - let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in - RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl) + if expl_pl == [] then + (* Convention: (@r) deactivates all further implicit arguments and scopes *) + RCPatCstr (loc, g, List.map (in_pat false env) pl, []) + else + (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) + (* but not scopes in expl_pl *) + let (argscs1,_) = find_remaining_scopes expl_pl pl g in + RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl @ List.map (in_pat false env) pl, []) | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[]) when Bigint.is_strictly_pos p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) @@ -1203,8 +1210,8 @@ let drop_notations_pattern looked_for = ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in RCPatCstr (loc, g, - List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl, - List.map2 (in_pat_sc env) argscs2 args) + List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl @ + List.map (in_pat false env) args, []) | NList (x,_,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err_loc (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index f5855a971e..efd5129b66 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -40,7 +40,7 @@ type raw_cases_pattern_expr = | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t | RCPatCstr of Loc.t * Globnames.global_reference * raw_cases_pattern_expr list * raw_cases_pattern_expr list - (** [CPatCstr (_, c, l1, l2)] represents (@c l1) l2 *) + (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *) | RCPatAtom of Loc.t * Id.t option | RCPatOr of Loc.t * raw_cases_pattern_expr list diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index b11204cbc5..7e470e8445 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -380,6 +380,9 @@ GEXTEND Gram [ p = pattern; lp = LIST1 NEXT -> (match p with | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp) + | CPatCstr (_, r, None, l2) -> Errors.user_err_loc + (cases_pattern_expr_loc p, "compound_pattern", + Pp.str "Nested applications not supported.") | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp) | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp) | _ -> Errors.user_err_loc diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index ac41819f56..9505a56e3f 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -1,40 +1,33 @@ (* This file is giving some examples about how implicit arguments and - scopes are (inconsistently) treated when using abbreviations or - notations, in terms or patterns, or when using @ and parentheses in - terms and patterns *) - -(* One compromise would be that: - - Neither abbreviations nor notations break implicit arguments and - scopes unless the head constant is with @ and surrounded with parentheses. - + This would change 3. terms and patterns to behave like 4. terms, - with former behavior possible by using instead (@pair' _ x%nat) - or (pair' x%nat). - + This would change 4. patterns to behave like 4. terms, introducing the - possibibility to have the deactivation in patterns, as it is in terms, - by using (@pair'). - + This would change 5. terms to behave like 5. patterns, introducing the - possibibility to have the activation behavior in terms, as it with - abbreviations, using either (@(pair') _ x%nat) or (pair' _ x). - + This would change 6. patterns to behave like 6. terms, introducing the - possibibility to have the deactivation behavior in patterns, as it with - abbreviations in terms, using either (@(pair') _ x%nat) or (pair' _ x). - - "(foo args)" directly in terms would still deactivation implicit - arguments and scopes for further arguments, as of today. - - "(@foo args)" directly in terms would deactivate implicit arguments and scopes - in args as of today, but not for further arguments, on the contrary of today - - "((@foo) args)" directly in terms would deactivate implicit - arguments and scopes in args and for further arguments, as it is today - - Then, in both terms and patterns: - - "(@foo args)" in an abbreviation or notation would behave the same as - "(@foo args)" when expanded, i.e. with deactivation of implicit arguments - and scopes only for args, but not for further arguments. - - "((@foo) args)" in an abbreviation or notation would behave the same as - "((@foo) args)" when expanded, i.e. with deactivation of implicit arguments and scopes. - - "(foo args)" in an abbreviation or notation would behave the same as - "foo args" when expanded, i.e. with no change on implicit arguments and scopes. + scopes are treated when using abbreviations or notations, in terms + or patterns, or when using @ and parentheses in terms and patterns. + +The convention is: + +Constant foo with implicit arguments and scopes used in a term or a pattern: + + foo do not deactivate further arguments and scopes + @foo deactivates further arguments and scopes + (foo x) deactivates further arguments and scopes + (@foo x) deactivates further arguments and scopes + +Notations binding to foo: + +# := foo do not deactivate further arguments and scopes +# := @foo deactivates further arguments and scopes +# x := foo x deactivates further arguments and scopes +# x := @foo x deactivates further arguments and scopes + +Abbreviations binding to foo: + +f := foo do not deactivate further arguments and scopes +f := @foo deactivates further arguments and scopes +f x := foo x do not deactivate further arguments and scopes +f x := @foo x do not deactivate further arguments and scopes *) +(* One checks that abbreviations and notations in patterns now behave like in terms *) + Inductive prod' A : Type -> Type := | pair' (a:A) B (b:B) (c:bool) : prod' A B. Arguments pair' [A] a%bool_scope [B] b%bool_scope c%bool_scope. @@ -46,14 +39,13 @@ Check pair' 0 0 0 : prod' bool bool. Check (pair' 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *) Check c1 0 0 0 : prod' bool bool. Check fun x : prod' bool bool => match x with c1 0 y 0 => 2 | _ => 1 end. -Check fun x : prod' bool bool => match x with (pair' 0) y 0 => 2 | _ => 1 end. (* Inconsistent with terms *) (* 2. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) Notation c2 x := (@pair' _ x). Check (@pair' _ 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *) Check c2 0 0 0 : prod' bool bool. Check fun A (x : prod' bool A) => match x with c2 0 y 0 => 2 | _ => 1 end. -Check fun A (x : prod' bool A) => match x with (@pair' _ 0) y 0 => 2 | _ => 1 end. (* Inconsistent with terms *) +Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ => 1 end. (* 3. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) Notation c3 x := ((@pair') _ x). @@ -61,30 +53,40 @@ Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking impl Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *) Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *) Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end. -(* Check fun A (x :prod' nat A) => match x with ((@pair') _ 0) y 0 => 2 | _ => 1 end.*) (* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) -(* unless an atomic @ is given, in terms but not in patterns *) +(* unless an atomic @ is given *) Notation c4 := (@pair'). Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. -Check c4 _ 0 _ 0 0%bool : prod' nat nat. (* all 0 are in nat_scope: would there be incompatibilities to change that? *) -Check fun A (x :prod' bool A) => match x with c4 _ 0 _ y 0 => 2 | _ => 1 end. (* Inconsistent with terms: both 0 are in bool_scope *) -Check fun A (x :prod' nat A) => match x with (@pair') _ 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: the implicit arguments and scopes are not deactivated *) +Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end. +Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end. (* 5. Notations stop further implicit arguments to be inserted and scopes to be used *) -(* in terms but not in patterns *) -Notation "% x" := (pair' x) (at level 0, x at level 0). +Notation "# x" := (pair' x) (at level 0, x at level 1). Check pair' 0 0 0 : prod' bool bool. -Check % 0 _ 0 0%bool : prod' bool nat. (* last two 0 are in nat_scope *) -Check fun A (x :prod' bool A) => match x with % 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: both 0 are in bool_scope *) -Check fun A (x :prod' bool A) => match x with pair' 0 y 0 => 2 | _ => 1 end. +Check # 0 _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end. (* 6. Notations stop further implicit arguments to be inserted and scopes to be used *) -(* in terms but not in patterns *) -Notation "% x" := ((@pair') _ x%nat) (at level 0, x at level 0). -Check (@pair') _ 0 _ 0%bool 0%bool : prod' nat bool. -Check ((@pair') _ 0) _ 0%bool 0%bool : prod' nat bool. -Check % 0 _ 0 0%bool : prod' nat nat. (* last two 0 are in nat_scope *) -Check fun A (x :prod' nat A) => match x with % 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: last 0 is in bool_scope, and implicit is not given *) -Check fun A (x :prod' bool A) => match x with (@pair') 0 y 0 => 2 | _ => 1 end. (* inconsistent with terms: the implicit arguments and scopes are not deactivated *) -Check fun A (x :prod' nat A) => match x with ((@pair') _) 0 y 0 => 2 | _ => 1 end. +Notation "## x" := ((@pair') _ x) (at level 0, x at level 1). +Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. +Check ## 0%bool _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end. + +(* 7. Notations stop further implicit arguments to be inserted and scopes to be used *) +Notation "###" := (@pair') (at level 0). +Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check ### _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with ### _ 0%bool _ y 0%bool => 2 | _ => 1 end. + +(* 8. Notations w/o @ preserves implicit arguments and scopes *) +Notation "####" := pair' (at level 0). +Check #### 0 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. + +(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *) +Notation "##### x" := (pair' x) (at level 0, x at level 1). +Check ##### 0 _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. |