diff options
| -rw-r--r-- | doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 1 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 34 | ||||
| -rw-r--r-- | interp/notation.mli | 3 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 3 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 6 | ||||
| -rw-r--r-- | interp/syntax_def.mli | 2 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 11 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13078.v | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13131.v | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13178.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/opened/bug_3395.v | 232 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_13241_1.v | 1 | ||||
| -rw-r--r-- | test-suite/output/ErrorLocation_13241_2.v | 1 | ||||
| -rw-r--r-- | test-suite/output/prim_array.out | 9 | ||||
| -rw-r--r-- | test-suite/output/prim_array.v | 10 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 29 |
18 files changed, 104 insertions, 266 deletions
diff --git a/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst b/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst new file mode 100644 index 0000000000..fb12c91729 --- /dev/null +++ b/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 <https://github.com/coq/coq/pull/13092>`_, + fixes `#13078 <https://github.com/coq/coq/issues/13078>`_, + by Hugo Herbelin). diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 29877e1b32..f8c0e23696 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -86,6 +86,7 @@ Setting properties of a function's arguments the parameter name used in the function definition). Unless `rename` is specified, the list of :n:`@name`\s must be a prefix of the formal parameters, including all implicit arguments. `_` can be used to skip over a formal parameter. + The construct :n:`@name {? % @scope }` declares :n:`@name` as non-implicit if `clear implicits` is specified or at least one other name is declared implicit in the same list of :n:`@name`\s. :token:`scope` can be either a scope name or its delimiting key. See :ref:`binding_to_scope`. `clear implicits` diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 2853eef5c5..ee07fb6ed1 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -114,8 +114,8 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp ungeneralizable loc id) vars; vars -let rec make_fresh ids env x = - if is_freevar ids env x then x else make_fresh ids env (Nameops.increment_subscript x) +let make_fresh ids env x = + Namegen.next_ident_away_from x (fun x -> not (is_freevar ids env x)) let next_name_away_from na avoid = match na with diff --git a/interp/notation.ml b/interp/notation.ml index 269e20c16e..c150ae7abb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -341,22 +341,27 @@ type notation_rule = interp_rule * interpretation * notation_applicative_status let notation_rule_eq (rule1,pat1,s1 as x1) (rule2,pat2,s2 as x2) = x1 == x2 || (rule1 = rule2 && interpretation_eq pat1 pat2 && s1 = s2) +let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) = + (* No need in principle to compare also_cases as it is inferred *) + also_cases1 = also_cases2 && notation_rule_eq rule1 rule2 + let keymap_add key interp map = let old = try KeyMap.find key map with Not_found -> [] in (* In case of re-import, no need to keep the previous copy *) - let old = try List.remove_first (notation_rule_eq interp) old with Not_found -> old in + let old = try List.remove_first (also_cases_notation_rule_eq interp) old with Not_found -> old in KeyMap.add key (interp :: old) map let keymap_remove key interp map = let old = try KeyMap.find key map with Not_found -> [] in - KeyMap.add key (List.remove_first (notation_rule_eq interp) old) map + KeyMap.add key (List.remove_first (also_cases_notation_rule_eq interp) old) map let keymap_find key map = try KeyMap.find key map with Not_found -> [] (* Scopes table : interpretation -> scope_name *) -let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) +(* Boolean = for cases pattern also *) +let notations_key_table = ref (KeyMap.empty : (bool * notation_rule) list KeyMap.t) let glob_prim_constr_key c = match DAst.get c with | GRef (ref, _) -> Some (canonical_gr ref) @@ -1333,13 +1338,13 @@ let check_printing_override (scopt,ntn) data parsingdata printingdata = exists) printingdata in parsing_update, exists -let remove_uninterpretation rule (metas,c as pat) = +let remove_uninterpretation rule also_in_cases_pattern (metas,c as pat) = let (key,n) = notation_constr_key c in - notations_key_table := keymap_remove key (rule,pat,n) !notations_key_table + notations_key_table := keymap_remove key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table -let declare_uninterpretation rule (metas,c as pat) = +let declare_uninterpretation ?(also_in_cases_pattern=true) rule (metas,c as pat) = let (key,n) = notation_constr_key c in - notations_key_table := keymap_add key (rule,pat,n) !notations_key_table + notations_key_table := keymap_add key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table let update_notation_data (scopt,ntn) use data table = let (parsingdata,printingdata) = @@ -1448,14 +1453,17 @@ let interp_notation ?loc ntn local_scopes = (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") let uninterp_notations c = - List.map_append (fun key -> keymap_find key !notations_key_table) + List.map_append (fun key -> List.map snd (keymap_find key !notations_key_table)) (glob_constr_keys c) +let filter_also_for_pattern = + List.map_filter (function (true,x) -> Some x | _ -> None) + let uninterp_cases_pattern_notations c = - keymap_find (cases_pattern_key c) !notations_key_table + filter_also_for_pattern (keymap_find (cases_pattern_key c) !notations_key_table) let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table + filter_also_for_pattern (keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table) let has_active_parsing_rule_in_scope ntn sc = try @@ -1615,7 +1623,7 @@ type entry_coercion_kind = | IsEntryGlobal of string * int | IsEntryIdent of string * int -let declare_notation (scopt,ntn) pat df ~use coe deprecation = +let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecation = (* Register the interpretation *) let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in let sc = find_scope scope in @@ -1630,10 +1638,10 @@ let declare_notation (scopt,ntn) pat df ~use coe deprecation = scope_map := String.Map.add scope sc !scope_map; (* Update the uninterpretation cache *) begin match printing_update with - | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) pat + | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat | None -> () end; - if not exists && use <> OnlyParsing then declare_uninterpretation (NotationRule (scopt,ntn)) pat; + if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat; (* Register visibility of lonely notations *) if not exists then begin match scopt with | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack diff --git a/interp/notation.mli b/interp/notation.mli index d744ff41d9..4d6d640a2d 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -234,7 +234,7 @@ type notation_use = | OnlyParsing | ParsingAndPrinting -val declare_uninterpretation : interp_rule -> interpretation -> unit +val declare_uninterpretation : ?also_in_cases_pattern:bool -> interp_rule -> interpretation -> unit type entry_coercion_kind = | IsEntryCoercion of notation_entry_level @@ -243,6 +243,7 @@ type entry_coercion_kind = val declare_notation : notation_with_optional_scope * notation -> interpretation -> notation_location -> use:notation_use -> + also_in_cases_pattern:bool -> entry_coercion_kind option -> Deprecation.t option -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index fe874cd01d..24b5dfce29 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1436,9 +1436,8 @@ let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists') - | NtnTypeBinder _ -> assert false | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists') - | NtnTypeBinderList -> assert false) + | NtnTypeBinder _ | NtnTypeBinderList -> anomaly (str "Unexpected binder in pattern notation.")) metas ([],[]) let match_notation_constr_cases_pattern c (metas,pat) = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index bd3e234a91..f3ad3546ff 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -22,6 +22,7 @@ type syndef = { syndef_pattern : interpretation; syndef_onlyparsing : bool; syndef_deprecation : Deprecation.t option; + syndef_also_in_cases_pattern : bool; } let syntax_table = @@ -52,7 +53,7 @@ let open_syntax_constant i ((sp,kn),(_local,syndef)) = if not syndef.syndef_onlyparsing then (* Redeclare it to be used as (short) name in case an other (distfix) notation was declared in between *) - Notation.declare_uninterpretation (Notation.SynDefRule kn) pat + Notation.declare_uninterpretation ~also_in_cases_pattern:syndef.syndef_also_in_cases_pattern (Notation.SynDefRule kn) pat end let cache_syntax_constant d = @@ -81,11 +82,12 @@ let in_syntax_constant : (bool * syndef) -> obj = subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } -let declare_syntactic_definition ~local deprecation id ~onlyparsing pat = +let declare_syntactic_definition ~local ?(also_in_cases_pattern=true) deprecation id ~onlyparsing pat = let syndef = { syndef_pattern = pat; syndef_onlyparsing = onlyparsing; syndef_deprecation = deprecation; + syndef_also_in_cases_pattern = also_in_cases_pattern; } in let _ = add_leaf id (in_syntax_constant (local,syndef)) in () diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 66a3132f2a..31f685152c 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -13,7 +13,7 @@ open Notation_term (** Syntactic definitions. *) -val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t -> +val declare_syntactic_definition : local:bool -> ?also_in_cases_pattern:bool -> Deprecation.t option -> Id.t -> onlyparsing:bool -> interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8da1d636f0..45d0e39ed6 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -681,13 +681,10 @@ let tag_var = tag Tag.variable | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (LevelLe ldelim) a), ldelim) | CArray(u, t,def,ty) -> - let pp = ref (str " |"++ spc () ++ pr mt ltop def - ++ pr_opt_type_spc (pr mt) ty ++ str " |]" ++ pr_universe_instance u) in - for i = Array.length t - 1 downto 1 do - pp := str ";" ++ pr mt ltop t.(i) ++ !pp - done; - pp := pr mt ltop t.(0) ++ !pp; - hov 0 (str "[|" ++ !pp), 0 + hov 0 (str "[| " ++ prvect_with_sep (fun () -> str "; ") (pr mt ltop) t ++ + (if not (Array.is_empty t) then str " " else mt()) ++ + str "|" ++ spc() ++ pr mt ltop def ++ pr_opt_type_spc (pr mt) ty ++ + str " |]" ++ pr_universe_instance u), 0 in let loc = constr_loc a in pr_with_comments ?loc diff --git a/test-suite/bugs/closed/bug_13078.v b/test-suite/bugs/closed/bug_13078.v new file mode 100644 index 0000000000..ec04408fd1 --- /dev/null +++ b/test-suite/bugs/closed/bug_13078.v @@ -0,0 +1,10 @@ +(* Check that rules with patterns are not registered for cases patterns *) +Module PrintingTest. +Declare Custom Entry test. +Notation "& x" := (Some x) (in custom test at level 0, x pattern). +Check fun x => match x with | None => None | Some tt => Some tt end. +Notation "& x" := (Some x) (at level 0, x pattern). +Check fun x => match x with | None => None | Some tt => Some tt end. +End PrintingTest. + +Fail Notation "x &" := (Some x) (at level 0, x pattern). diff --git a/test-suite/bugs/closed/bug_13131.v b/test-suite/bugs/closed/bug_13131.v new file mode 100644 index 0000000000..b358ae3ecc --- /dev/null +++ b/test-suite/bugs/closed/bug_13131.v @@ -0,0 +1,6 @@ +Set Mangle Names. + +Class A := {}. + +Lemma foo `{A} : A. +Proof. Fail exact H. assumption. Qed. diff --git a/test-suite/bugs/closed/bug_13178.v b/test-suite/bugs/closed/bug_13178.v new file mode 100644 index 0000000000..d9c516c362 --- /dev/null +++ b/test-suite/bugs/closed/bug_13178.v @@ -0,0 +1,3 @@ +Primitive array := #array_type. + +Check [| | 0 |]. diff --git a/test-suite/bugs/opened/bug_3395.v b/test-suite/bugs/opened/bug_3395.v deleted file mode 100644 index 70b3a48a06..0000000000 --- a/test-suite/bugs/opened/bug_3395.v +++ /dev/null @@ -1,232 +0,0 @@ -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) -Generalizable All Variables. -Set Implicit Arguments. - -Arguments fst {_ _} _. -Arguments snd {_ _} _. - -Axiom cheat : forall {T}, T. - -Reserved Notation "g 'o' f" (at level 40, left associativity). - -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. -Arguments idpath {A a} , [A] a. -Notation "x = y" := (paths x y) : type_scope. - -Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x - := match p with idpath => idpath end. - -Delimit Scope morphism_scope with morphism. -Delimit Scope category_scope with category. -Delimit Scope object_scope with object. -Record PreCategory (object : Type) := - Build_PreCategory' { - object :> Type := object; - morphism : object -> object -> Type; - identity : forall x, morphism x x; - compose : forall s d d', - morphism d d' - -> morphism s d - -> morphism s d' - where "f 'o' g" := (compose f g); - associativity : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - (m3 o m2) o m1 = m3 o (m2 o m1); - associativity_sym : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - m3 o (m2 o m1) = (m3 o m2) o m1; - left_identity : forall a b (f : morphism a b), identity b o f = f; - right_identity : forall a b (f : morphism a b), f o identity a = f; - identity_identity : forall x, identity x o identity x = identity x - }. -Bind Scope category_scope with PreCategory. -Arguments PreCategory {_}. -Arguments identity {_} [!C%category] x%object : rename. - -Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. - -Infix "o" := compose : morphism_scope. - -Delimit Scope functor_scope with functor. -Local Open Scope morphism_scope. -Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := - { - object_of :> C -> D; - morphism_of : forall s d, morphism C s d - -> morphism D (object_of s) (object_of d); - composition_of : forall s d d' - (m1 : morphism C s d) (m2: morphism C d d'), - morphism_of _ _ (m2 o m1) - = (morphism_of _ _ m2) o (morphism_of _ _ m1); - identity_of : forall x, morphism_of _ _ (identity x) - = identity (object_of x) - }. -Bind Scope functor_scope with Functor. - -Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. - -Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. - -Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := - { - morphism_inverse : morphism C d s; - left_inverse : morphism_inverse o m = identity _; - right_inverse : m o morphism_inverse = identity _ - }. - -Definition opposite `(C : @PreCategory objC) : PreCategory - := @Build_PreCategory' - C - (fun s d => morphism C d s) - (identity (C := C)) - (fun _ _ _ m1 m2 => m2 o m1) - (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) - (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) - (fun _ _ => @right_identity _ _ _ _) - (fun _ _ => @left_identity _ _ _ _) - (@identity_identity _ C). - -Notation "C ^op" := (opposite C) (at level 3) : category_scope. - -Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). - refine (@Build_PreCategory' - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) - * morphism D (snd s) (snd d))%type) - (fun x => (identity (fst x), identity (snd x))) - (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) - _ - _ - _ - _ - _); admit. -Defined. -Infix "*" := prod : category_scope. - -Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E - := Build_Functor - C E - (fun c => G (F c)) - (fun _ _ m => morphism_of G (morphism_of F m)) - cheat - cheat. - -Infix "o" := compose_functor : functor_scope. - -Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := - Build_NaturalTransformation' { - components_of :> forall c, morphism D (F c) (G c); - commutes : forall s d (m : morphism C s d), - components_of d o F _1 m = G _1 m o components_of s; - - commutes_sym : forall s d (m : C.(morphism) s d), - G _1 m o components_of s = components_of d o F _1 m - }. -Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory - := @Build_PreCategory' (Functor C D) - (@NaturalTransformation _ C _ D) - cheat - cheat - cheat - cheat - cheat - cheat - cheat. - -Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op - := Build_Functor (C^op) (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). - -Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op - := Build_Functor C (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). -Notation "F ^op" := (opposite_functor F) : functor_scope. - -Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. -Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C - := Build_Functor (C * D) C - (@fst _ _) - (fun _ _ => @fst _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). - -Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D - := Build_Functor (C * D) D - (@snd _ _) - (fun _ _ => @snd _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). -Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') -: Functor C (D * D') - := Build_Functor - C (D * D') - (fun c => (F c, F' c)) - (fun s d m => (F _1 m, F' _1 m))%morphism - cheat - cheat. -Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') - := (prod_functor (F o fst) (F' o snd))%functor. -Notation cat_of obj := - (@Build_PreCategory' obj - (fun x y => forall _ : x, y) - (fun _ x => x) - (fun _ _ _ f g x => f (g x))%core - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ => idpath)). - -Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) - := Build_Functor _ _ cheat cheat cheat cheat. - -Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) -: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) - := Build_NaturalTransformation' _ _ cheat cheat cheat. - -Class IsFullyFaithful `(F : @Functor objC C objD D) - := is_fully_faithful - : forall x y : C, - IsIsomorphism (induced_hom_natural_transformation F (x, y)). - -Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) - := cheat. - -Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) - := (((coyoneda A^op)^op'L)^op'L)%functor. -Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). -Admitted. - -Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda. - Time let t := (type of CYE) in - let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) - Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). - Time let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) -Fail Timeout 2 Defined. -Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) - -Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda; simpl in *. - Fail Timeout 1 exact CYE. - Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) -Abort. diff --git a/test-suite/output/ErrorLocation_13241_1.v b/test-suite/output/ErrorLocation_13241_1.v index ff92085133..3102b13fb8 100644 --- a/test-suite/output/ErrorLocation_13241_1.v +++ b/test-suite/output/ErrorLocation_13241_1.v @@ -2,3 +2,4 @@ Ltac a := intro. Ltac b := a. Goal True. b. +Abort. diff --git a/test-suite/output/ErrorLocation_13241_2.v b/test-suite/output/ErrorLocation_13241_2.v index 280d4a3506..b82f36ed6f 100644 --- a/test-suite/output/ErrorLocation_13241_2.v +++ b/test-suite/output/ErrorLocation_13241_2.v @@ -2,3 +2,4 @@ Ltac a _ := intro. Ltac b := a (). Goal True. b. +Abort. diff --git a/test-suite/output/prim_array.out b/test-suite/output/prim_array.out new file mode 100644 index 0000000000..6c12153ab9 --- /dev/null +++ b/test-suite/output/prim_array.out @@ -0,0 +1,9 @@ +[| | 0 : nat |] + : array nat +[| 1; 2; 3 | 0 : nat |] + : array nat +[| | 0 : nat |]@{Set} + : array@{Set} nat +[| bool; list nat | nat : Set |]@{prim_array.4} + : array@{prim_array.4} Set +(* {prim_array.4} |= Set < prim_array.4 *) diff --git a/test-suite/output/prim_array.v b/test-suite/output/prim_array.v new file mode 100644 index 0000000000..a82f6a16f1 --- /dev/null +++ b/test-suite/output/prim_array.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Check [| | 0 |]. + +Check [| 1; 2; 3 | 0 |]. + +Set Printing Universes. +Check [| | 0 |]. + +Check [| bool; list nat | nat |]. diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 185abcf35b..8477870cb4 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1042,6 +1042,13 @@ let interp_non_syntax_modifiers mods = in List.fold_left (fun st modif -> Option.bind st @@ set modif) (Some (false,false,InConstrEntry)) mods +(* Check if an interpretation can be used for printing a cases printing *) +let has_no_binders_type = + List.for_all (fun (_,(_,typ)) -> + match typ with + | NtnTypeBinder _ | NtnTypeBinderList -> false + | NtnTypeConstr | NtnTypeConstrList -> true) + (* Compute precedences from modifiers (or find default ones) *) let set_entry_type from n etyps (x,typ) = @@ -1226,6 +1233,9 @@ let find_precedence custom lev etyps symbols onlyprint = | _ -> user_err Pp.(str "A notation starting with an atomic expression must be at level 0.") end + | (ETPattern _ | ETBinder _), InConstrEntry when not onlyprint -> + (* Don't know exactly if we can make sense of this case *) + user_err Pp.(str "Binders or patterns not supported in leftmost position.") | (ETPattern _ | ETBinder _ | ETConstr _), _ -> (* Give a default ? *) if Option.is_empty lev then @@ -1416,6 +1426,7 @@ type notation_obj = { notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; notobj_specific_pp_rules : syntax_printing_extension option; + notobj_also_in_cases_pattern : bool; } let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = @@ -1438,9 +1449,10 @@ let open_notation i (_, nobj) = let pat = nobj.notobj_interp in let deprecation = nobj.notobj_deprecation in let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in + let also_in_cases_pattern = nobj.notobj_also_in_cases_pattern in (* Declare the notation *) (match nobj.notobj_use with - | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation + | Some use -> Notation.declare_notation (scope,ntn) pat df ~use ~also_in_cases_pattern nobj.notobj_coercion deprecation | None -> ()); (* Declare specific format if any *) (match nobj.notobj_specific_pp_rules with @@ -1621,19 +1633,21 @@ let add_notation_in_scope ~local deprecation df env c mods scope = let (acvars, ac, reversibility) = interp_notation_constr env nenv c in let interp = make_interpretation_vars sd.recvars (pi2 sd.level) acvars (fst sd.pa_syntax_data) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in + let vars = List.map_filter map i_vars in (* Order of elements is important here! *) + let also_in_cases_pattern = has_no_binders_type vars in let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in let notation, location = sd.info in let use = make_use true onlyparse sd.only_printing in let notation = { notobj_local = local; notobj_scope = scope; - notobj_interp = (List.map_filter map i_vars, ac); - (* Order is important here! *) notobj_use = use; + notobj_interp = (vars, ac); notobj_coercion = coe; notobj_deprecation = sd.deprecation; notobj_notation = (notation, location); notobj_specific_pp_rules = sy_pp_rules; + notobj_also_in_cases_pattern = also_in_cases_pattern; } in (* Ready to change the global state *) List.iter (fun f -> f ()) sd.msgs; @@ -1665,18 +1679,20 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization let plevel = match level with Some (from,level,l) -> level | None (* numeral: irrelevant )*) -> 0 in let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in + let vars = List.map_filter map i_vars in (* Order of elements is important here! *) + let also_in_cases_pattern = has_no_binders_type vars in let onlyparse,coe = printability level i_typs onlyparse reversibility ac in let use = make_use false onlyparse onlyprint in let notation = { notobj_local = local; notobj_scope = scope; - notobj_interp = (List.map_filter map i_vars, ac); - (* Order is important here! *) notobj_use = use; + notobj_interp = (vars, ac); notobj_coercion = coe; notobj_deprecation = deprecation; notobj_notation = df'; notobj_specific_pp_rules = pp_sy; + notobj_also_in_cases_pattern = also_in_cases_pattern; } in Lib.add_anonymous_leaf (inNotation notation); df' @@ -1850,8 +1866,9 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] 0 acvars (List.map in_pat vars) in let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in + let also_in_cases_pattern = has_no_binders_type vars in let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in - Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat) + Syntax_def.declare_syntactic_definition ~local ~also_in_cases_pattern deprecation ident ~onlyparsing (vars,pat) (**********************************************************************) (* Declaration of custom entry *) |