From 63fd32c98aa0646b8a2bf87e66d4ff9bdf1c0da7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 25 Sep 2023 16:10:56 +0200 Subject: [PATCH 1/7] Remove useless casts in test-suite Since those are output tests, the type will be tested in the output anyway. --- test-suite/output/NNumberSyntax.out | 54 +++++++------- test-suite/output/NNumberSyntax.v | 54 +++++++------- test-suite/output/PosSyntax.out | 40 +++++------ test-suite/output/PosSyntax.v | 58 +++++++-------- test-suite/output/ZNumberSyntax.out | 108 ++++++++++++++-------------- test-suite/output/ZNumberSyntax.v | 108 ++++++++++++++-------------- 6 files changed, 211 insertions(+), 211 deletions(-) diff --git a/test-suite/output/NNumberSyntax.out b/test-suite/output/NNumberSyntax.out index 970bf5574051..163b30a3ced2 100644 --- a/test-suite/output/NNumberSyntax.out +++ b/test-suite/output/NNumberSyntax.out @@ -20,25 +20,25 @@ fun x : positive => (N.pos x~0 + 0)%N : N N.of_nat 0 = 0%N : Prop -0%N : N +0%N : N -1%N : N +1%N : N -2%N : N +2%N : N -255%N : N +255%N : N -255%N : N +255%N : N -0%N : N +0%N : N -1%N : N +1%N : N -2%N : N +2%N : N -255%N : N +255%N : N -255%N : N +255%N : N 0x2a : N @@ -48,39 +48,39 @@ N.of_nat 0 = 0%N : N 0x0 : N -0x0 : N +0x0 : N -0x1 : N +0x1 : N -0x2 : N +0x2 : N -0xff : N +0xff : N -0xff : N +0xff : N -0x0 : N +0x0 : N -0x0 : N +0x0 : N -0x1 : N +0x1 : N -0x2 : N +0x2 : N -0xff : N +0xff : N -0xff : N +0xff : N -0x0 : N +0x0 : N -0x0 : N +0x0 : N -0x1 : N +0x1 : N -0x2 : N +0x2 : N -0xff : N +0xff : N -0xff : N +0xff : N (0 + N.of_nat 11)%N : N diff --git a/test-suite/output/NNumberSyntax.v b/test-suite/output/NNumberSyntax.v index 34aebdd40647..be19ad96c89c 100644 --- a/test-suite/output/NNumberSyntax.v +++ b/test-suite/output/NNumberSyntax.v @@ -10,16 +10,16 @@ Check (fun x : positive => (Npos (xO x) + 0)%N). Check (N.of_nat 0 + 1)%N. Check (0 + N.of_nat (0 + 0))%N. Check (N.of_nat 0 = 0%N). -Check 0x00%N : N. -Check 0x01%N : N. -Check 0x02%N : N. -Check 0xff%N : N. -Check 0xFF%N : N. -Check 0x00%xN : N. -Check 0x01%xN : N. -Check 0x02%xN : N. -Check 0xff%xN : N. -Check 0xFF%xN : N. +Check 0x00%N. +Check 0x01%N. +Check 0x02%N. +Check 0xff%N. +Check 0xFF%N. +Check 0x00%xN. +Check 0x01%xN. +Check 0x02%xN. +Check 0xff%xN. +Check 0xFF%xN. (* Check hexadecimal printing *) Open Scope hex_N_scope. @@ -27,23 +27,23 @@ Check 42%N. Check 0%N. Check 42%xN. Check 0%xN. -Check 0x00%N : N. -Check 0x01%N : N. -Check 0x02%N : N. -Check 0xff%N : N. -Check 0xFF%N : N. -Check 0x0%xN : N. -Check 0x00%xN : N. -Check 0x01%xN : N. -Check 0x02%xN : N. -Check 0xff%xN : N. -Check 0xFF%xN : N. -Check 0x0 : N. -Check 0x00 : N. -Check 0x01 : N. -Check 0x02 : N. -Check 0xff : N. -Check 0xFF : N. +Check 0x00%N. +Check 0x01%N. +Check 0x02%N. +Check 0xff%N. +Check 0xFF%N. +Check 0x0%xN. +Check 0x00%xN. +Check 0x01%xN. +Check 0x02%xN. +Check 0xff%xN. +Check 0xFF%xN. +Check 0x0. +Check 0x00. +Check 0x01. +Check 0x02. +Check 0xff. +Check 0xFF. Close Scope hex_N_scope. Require Import Arith. diff --git a/test-suite/output/PosSyntax.out b/test-suite/output/PosSyntax.out index 346046f8f332..fd6528d8d627 100644 --- a/test-suite/output/PosSyntax.out +++ b/test-suite/output/PosSyntax.out @@ -29,21 +29,21 @@ Cannot interpret this number as a value of type positive File "./output/PosSyntax.v", line 15, characters 11-15: The command has indeed failed with message: Cannot interpret this number as a value of type positive -1%positive : positive +1%positive : positive -2%positive : positive +2%positive : positive -255%positive : positive +255%positive : positive -255%positive : positive +255%positive : positive -1%positive : positive +1%positive : positive -2%positive : positive +2%positive : positive -255%positive : positive +255%positive : positive -255%positive : positive +255%positive : positive 0x2a : positive @@ -55,13 +55,13 @@ Cannot interpret this number as a value of type positive File "./output/PosSyntax.v", line 30, characters 11-15: The command has indeed failed with message: Cannot interpret this number as a value of type positive -0x1 : positive +0x1 : positive -0x2 : positive +0x2 : positive -0xff : positive +0xff : positive -0xff : positive +0xff : positive File "./output/PosSyntax.v", line 35, characters 11-14: The command has indeed failed with message: @@ -69,13 +69,13 @@ Cannot interpret this number as a value of type positive File "./output/PosSyntax.v", line 36, characters 11-15: The command has indeed failed with message: Cannot interpret this number as a value of type positive -0x1 : positive +0x1 : positive -0x2 : positive +0x2 : positive -0xff : positive +0xff : positive -0xff : positive +0xff : positive File "./output/PosSyntax.v", line 41, characters 11-14: The command has indeed failed with message: @@ -83,13 +83,13 @@ Cannot interpret this number as a value of type positive File "./output/PosSyntax.v", line 42, characters 11-15: The command has indeed failed with message: Cannot interpret this number as a value of type positive -0x1 : positive +0x1 : positive -0x2 : positive +0x2 : positive -0xff : positive +0xff : positive -0xff : positive +0xff : positive (1 + Pos.of_nat 11)%positive : positive diff --git a/test-suite/output/PosSyntax.v b/test-suite/output/PosSyntax.v index 9537c600309b..dca787d08d6c 100644 --- a/test-suite/output/PosSyntax.v +++ b/test-suite/output/PosSyntax.v @@ -10,40 +10,40 @@ Check (fun x : positive => (xO x + 1)%positive). Check (Pos.of_nat 0 + 1)%positive. Check (1 + Pos.of_nat (0 + 0))%positive. Check (Pos.of_nat 1 = 1%positive). -Fail Check 0%positive : positive. -Fail Check 0x0%positive : positive. -Fail Check 0x00%positive : positive. -Check 0x01%positive : positive. -Check 0x02%positive : positive. -Check 0xff%positive : positive. -Check 0xFF%positive : positive. -Check 0x01%xpositive : positive. -Check 0x02%xpositive : positive. -Check 0xff%xpositive : positive. -Check 0xFF%xpositive : positive. +Fail Check 0%positive. +Fail Check 0x0%positive. +Fail Check 0x00%positive. +Check 0x01%positive. +Check 0x02%positive. +Check 0xff%positive. +Check 0xFF%positive. +Check 0x01%xpositive. +Check 0x02%xpositive. +Check 0xff%xpositive. +Check 0xFF%xpositive. (* Check hexadecimal printing *) Open Scope hex_positive_scope. Check 42%positive. Check 1%positive. -Fail Check 0x0%positive : positive. -Fail Check 0x00%positive : positive. -Check 0x01%positive : positive. -Check 0x02%positive : positive. -Check 0xff%positive : positive. -Check 0xFF%positive : positive. -Fail Check 0x0 : positive. -Fail Check 0x00 : positive. -Check 0x01 : positive. -Check 0x02 : positive. -Check 0xff : positive. -Check 0xFF : positive. -Fail Check 0x0%xpositive : positive. -Fail Check 0x00%xpositive : positive. -Check 0x01%xpositive : positive. -Check 0x02%xpositive : positive. -Check 0xff%xpositive : positive. -Check 0xFF%xpositive : positive. +Fail Check 0x0%positive. +Fail Check 0x00%positive. +Check 0x01%positive. +Check 0x02%positive. +Check 0xff%positive. +Check 0xFF%positive. +Fail Check 0x0. +Fail Check 0x00. +Check 0x01. +Check 0x02. +Check 0xff. +Check 0xFF. +Fail Check 0x0%xpositive. +Fail Check 0x00%xpositive. +Check 0x01%xpositive. +Check 0x02%xpositive. +Check 0xff%xpositive. +Check 0xFF%xpositive. Close Scope hex_positive_scope. Require Import Arith. diff --git a/test-suite/output/ZNumberSyntax.out b/test-suite/output/ZNumberSyntax.out index 908f6a63f608..f2719ba76496 100644 --- a/test-suite/output/ZNumberSyntax.out +++ b/test-suite/output/ZNumberSyntax.out @@ -24,53 +24,53 @@ fun x : positive => (- Z.pos x~0 + 0)%Z : Z Z.of_nat 0 = 0%Z : Prop -0%Z : Z +0%Z : Z -0%Z : Z +0%Z : Z -1%Z : Z +1%Z : Z -2%Z : Z +2%Z : Z -255%Z : Z +255%Z : Z -255%Z : Z +255%Z : Z -(- 0)%Z : Z +(- 0)%Z : Z -(- 0)%Z : Z +(- 0)%Z : Z -(-1)%Z : Z +(-1)%Z : Z -(-2)%Z : Z +(-2)%Z : Z -(-255)%Z : Z +(-255)%Z : Z -(-255)%Z : Z +(-255)%Z : Z -0%Z : Z +0%Z : Z -0%Z : Z +0%Z : Z -1%Z : Z +1%Z : Z -2%Z : Z +2%Z : Z -255%Z : Z +255%Z : Z -255%Z : Z +255%Z : Z -(- 0)%Z : Z +(- 0)%Z : Z -(- 0)%Z : Z +(- 0)%Z : Z -(-1)%Z : Z +(-1)%Z : Z -(-2)%Z : Z +(-2)%Z : Z -(-255)%Z : Z +(-255)%Z : Z -(-255)%Z : Z +(-255)%Z : Z 0x2a : Z @@ -84,65 +84,65 @@ Z.of_nat 0 = 0%Z : Z 0x0 : Z -0x0 : Z +0x0 : Z -0x0 : Z +0x0 : Z -0x1 : Z +0x1 : Z -0x2 : Z +0x2 : Z -0xff : Z +0xff : Z -0xff : Z +0xff : Z -(- 0)%Z : Z +(- 0)%Z : Z -(- 0)%Z : Z +(- 0)%Z : Z --0x1 : Z +-0x1 : Z --0x2 : Z +-0x2 : Z --0xff : Z +-0xff : Z --0xff : Z +-0xff : Z -0x0 : Z +0x0 : Z -0x0 : Z +0x0 : Z -0x1 : Z +0x1 : Z -0x2 : Z +0x2 : Z -0xff : Z +0xff : Z -0xff : Z +0xff : Z -0x0 : Z +0x0 : Z -0x0 : Z +0x0 : Z -0x1 : Z +0x1 : Z -0x2 : Z +0x2 : Z -0xff : Z +0xff : Z -0xff : Z +0xff : Z -(- 0)%Z : Z +(- 0)%Z : Z -(- 0)%Z : Z +(- 0)%Z : Z --0x1 : Z +-0x1 : Z --0x2 : Z +-0x2 : Z --0xff : Z +-0xff : Z --0xff : Z +-0xff : Z (0 + Z.of_nat 11)%Z : Z diff --git a/test-suite/output/ZNumberSyntax.v b/test-suite/output/ZNumberSyntax.v index 8bef1bb01ab5..395849e34cf6 100644 --- a/test-suite/output/ZNumberSyntax.v +++ b/test-suite/output/ZNumberSyntax.v @@ -12,30 +12,30 @@ Check (fun x : positive => (- Zpos (xO x) + 0)%Z). Check (Z.of_nat 0 + 1)%Z. Check (0 + Z.of_nat (0 + 0))%Z. Check (Z.of_nat 0 = 0%Z). -Check 0x0%Z : Z. -Check 0x00%Z : Z. -Check 0x01%Z : Z. -Check 0x02%Z : Z. -Check 0xff%Z : Z. -Check 0xFF%Z : Z. -Check (-0x0)%Z : Z. -Check (-0x00)%Z : Z. -Check (-0x01)%Z : Z. -Check (-0x02)%Z : Z. -Check (-0xff)%Z : Z. -Check (-0xFF)%Z : Z. -Check 0x0%xZ : Z. -Check 0x00%xZ : Z. -Check 0x01%xZ : Z. -Check 0x02%xZ : Z. -Check 0xff%xZ : Z. -Check 0xFF%xZ : Z. -Check (-0x0)%xZ%Z : Z. -Check (-0x00)%xZ%Z : Z. -Check (-0x01)%xZ : Z. -Check (-0x02)%xZ : Z. -Check (-0xff)%xZ : Z. -Check (-0xFF)%xZ : Z. +Check 0x0%Z. +Check 0x00%Z. +Check 0x01%Z. +Check 0x02%Z. +Check 0xff%Z. +Check 0xFF%Z. +Check (-0x0)%Z. +Check (-0x00)%Z. +Check (-0x01)%Z. +Check (-0x02)%Z. +Check (-0xff)%Z. +Check (-0xFF)%Z. +Check 0x0%xZ. +Check 0x00%xZ. +Check 0x01%xZ. +Check 0x02%xZ. +Check 0xff%xZ. +Check 0xFF%xZ. +Check (-0x0)%xZ%Z. +Check (-0x00)%xZ%Z. +Check (-0x01)%xZ. +Check (-0x02)%xZ. +Check (-0xff)%xZ. +Check (-0xFF)%xZ. (* Check hexadecimal printing *) Open Scope hex_Z_scope. @@ -45,36 +45,36 @@ Check 0%Z. Check 42%xZ. Check (-42)%xZ. Check 0%xZ. -Check 0x0%Z : Z. -Check 0x00%Z : Z. -Check 0x01%Z : Z. -Check 0x02%Z : Z. -Check 0xff%Z : Z. -Check 0xFF%Z : Z. -Check (-0x0)%Z : Z. -Check (-0x00)%Z : Z. -Check (-0x01)%Z : Z. -Check (-0x02)%Z : Z. -Check (-0xff)%Z : Z. -Check (-0xFF)%Z : Z. -Check 0x0 : Z. -Check 0x00 : Z. -Check 0x01 : Z. -Check 0x02 : Z. -Check 0xff : Z. -Check 0xFF : Z. -Check 0x0%xZ : Z. -Check 0x00%xZ : Z. -Check 0x01%xZ : Z. -Check 0x02%xZ : Z. -Check 0xff%xZ : Z. -Check 0xFF%xZ : Z. -Check (-0x0)%xZ%Z : Z. -Check (-0x00)%xZ%Z : Z. -Check (-0x01)%xZ : Z. -Check (-0x02)%xZ : Z. -Check (-0xff)%xZ : Z. -Check (-0xFF)%xZ : Z. +Check 0x0%Z. +Check 0x00%Z. +Check 0x01%Z. +Check 0x02%Z. +Check 0xff%Z. +Check 0xFF%Z. +Check (-0x0)%Z. +Check (-0x00)%Z. +Check (-0x01)%Z. +Check (-0x02)%Z. +Check (-0xff)%Z. +Check (-0xFF)%Z. +Check 0x0. +Check 0x00. +Check 0x01. +Check 0x02. +Check 0xff. +Check 0xFF. +Check 0x0%xZ. +Check 0x00%xZ. +Check 0x01%xZ. +Check 0x02%xZ. +Check 0xff%xZ. +Check 0xFF%xZ. +Check (-0x0)%xZ%Z. +Check (-0x00)%xZ%Z. +Check (-0x01)%xZ. +Check (-0x02)%xZ. +Check (-0xff)%xZ. +Check (-0xFF)%xZ. Close Scope hex_Z_scope. (* Submitted by Pierre Casteran *) From a37e2359c4b51cb46447499f33fd7b8d521ed9e9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 9 Nov 2017 14:13:54 +0100 Subject: [PATCH 2/7] Forcing use of type_scope when casting with a sort (see issue #6077). --- interp/constrexpr_ops.ml | 3 +++ interp/constrexpr_ops.mli | 4 ++++ interp/constrextern.ml | 4 +++- interp/constrintern.ml | 3 ++- test-suite/output/TermSyntax.out | 2 ++ test-suite/output/TermSyntax.v | 2 ++ 6 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 test-suite/output/TermSyntax.out create mode 100644 test-suite/output/TermSyntax.v diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index bd640e90db18..6394979dea96 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -684,3 +684,6 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function | CArray _ -> CErrors.user_err ?loc (str "Arrays in patterns not supported.")) c + +let isCSort a = + match a.CAst.v with Constrexpr.CSort _ -> true | _ -> false diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index f86f71fc8f6c..9daa6817d185 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -113,6 +113,8 @@ val map_constr_expr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) -> 'a -> constr_expr -> constr_expr +(** {6 Miscellaneous}*) + val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr @@ -127,5 +129,7 @@ val split_at_annot : local_binder_expr list -> lident option -> local_binder_exp val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> notation -> (int * int) list val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -> (int * int) list +val isCSort : constr_expr -> bool + (** For cases pattern parsing errors *) val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a diff --git a/interp/constrextern.ml b/interp/constrextern.ml index be2f46a280fa..5d5ad120d6c6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1062,7 +1062,9 @@ let rec extern inctx ?impargs scopes vars r = | GGenarg arg -> CGenargGlob arg | GCast (c, k, c') -> - CCast (sub_extern true scopes vars c, k, extern_typ scopes vars c') + let c' = extern_typ scopes vars c' in + let c = if isCSort c' then extern_typ scopes vars c else sub_extern true scopes vars c in + CCast (c, k, c') | GInt i -> extern_prim_token_delimiter_if_required diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 542dc5f588d8..53d083aad21e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2390,8 +2390,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = DAst.make ?loc @@ GSort (intern_sort ~local_univs:env.local_univs s) | CCast (c1, k, c2) -> + let c1 = if isCSort c2 then intern_type env c1 else intern env c1 in DAst.make ?loc @@ - GCast (intern env c1, k, intern_type (slide_binders env) c2) + GCast (c1, k, intern_type (slide_binders env) c2) | CArray(u,t,def,ty) -> DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty) ) diff --git a/test-suite/output/TermSyntax.out b/test-suite/output/TermSyntax.out new file mode 100644 index 000000000000..e023e17f22a4 --- /dev/null +++ b/test-suite/output/TermSyntax.out @@ -0,0 +1,2 @@ +nat * nat : Type + : Type diff --git a/test-suite/output/TermSyntax.v b/test-suite/output/TermSyntax.v new file mode 100644 index 000000000000..1abbc4c3265a --- /dev/null +++ b/test-suite/output/TermSyntax.v @@ -0,0 +1,2 @@ +(* Check Type cast setting type_scope *) +Check nat * nat : Type. From 65c7c58eb2ec719b35760fa7e9958e4b057a8aee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 9 Nov 2017 14:31:52 +0100 Subject: [PATCH 3/7] Dropping two cast notations whose effect is done at in/externalization time. Note that the feature implemented natively is different from the one implemented by the two deleted cast notations to a sort as the latters are "only parsing" while the native implementation is also for printing. --- theories/ssr/ssreflect.v | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index 43634d60d854..889ef8221fdd 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -101,7 +101,6 @@ Export SsrSyntax. Local Notation CoqGenericIf c vT vF := (if c then vT else vF) (only parsing). Local Notation CoqGenericDependentIf c x R vT vF := (if c as x return R then vT else vF) (only parsing). -Local Notation CoqCast x T := (x : T) (only parsing). (** Reserve notation that introduced in this file. **) Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200, @@ -111,9 +110,6 @@ Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200, Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200, c, R, vT, vF at level 200, x name). -Reserved Notation "T : 'Type'" (at level 100, format "T : 'Type'"). -Reserved Notation "P : 'Prop'" (at level 100, format "P : 'Prop'"). - Reserved Notation "[ 'the' sT 'of' v 'by' f ]" (at level 0, format "[ 'the' sT 'of' v 'by' f ]"). Reserved Notation "[ 'the' sT 'of' v ]" (at level 0, @@ -182,14 +178,6 @@ Declare Scope form_scope. Delimit Scope form_scope with FORM. Open Scope form_scope. -(** - Allow the casual use of notations like nat * nat for explicit Type - declarations. Note that (nat * nat : Type) is NOT equivalent to - (nat * nat)%%type, whose inferred type is legacy type "Set". **) -Notation "T : 'Type'" := (CoqCast T%type Type) (only parsing) : core_scope. -(** Allow similarly Prop annotation for, e.g., rewrite multirules. **) -Notation "P : 'Prop'" := (CoqCast P%type Prop) (only parsing) : core_scope. - (** Constants for abstract: and #[#: name #]# intro pattern **) Definition abstract_lock := unit. Definition abstract_key := tt. From 571bb80464ea0e055e6ff67cedd7f8eaa1a84efa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 9 Nov 2017 23:30:47 +0100 Subject: [PATCH 4/7] Exporting functions to compute the scope class of a glob constr. --- interp/notation.ml | 3 +++ interp/notation.mli | 1 + pretyping/coercionops.ml | 11 +++++++++++ pretyping/coercionops.mli | 2 ++ 4 files changed, 17 insertions(+) diff --git a/interp/notation.ml b/interp/notation.ml index fe7a4af85a6a..d40070b3e86b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1841,6 +1841,9 @@ let compute_type_scope env sigma t = let current_type_scope_names () = find_scope_class_opt !scope_class_map (Some CL_SORT) +let compute_glob_type_scope t = + find_scope_class_opt !scope_class_map (try Some (find_class_glob_type t) with Not_found -> None) + let scope_class_of_class (x : cl_typ) : scope_class = x diff --git a/interp/notation.mli b/interp/notation.mli index 0941f7d62a22..e8ecb75a2dab 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -308,6 +308,7 @@ val declare_ref_arguments_scope : GlobRef.t -> unit val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name list list val compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name list +val compute_glob_type_scope : 'a Glob_term.glob_constr_g -> scope_name list (** Get the current scopes bound to Sortclass *) val current_type_scope_names : unit -> scope_name list diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml index 4ef24725ef79..9e3f59a1c3ea 100644 --- a/pretyping/coercionops.ml +++ b/pretyping/coercionops.ml @@ -176,6 +176,17 @@ let find_class_type env sigma t = | Sort _ -> CL_SORT, EInstance.empty, [] | _ -> raise Not_found +let class_of_global_reference = function + | GlobRef.VarRef id -> CL_SECVAR id + | GlobRef.ConstRef kn -> CL_CONST kn + | GlobRef.IndRef ind -> CL_IND ind + | GlobRef.ConstructRef _ -> raise Not_found + +let find_class_glob_type c = match DAst.get c with + | Glob_term.GRef (ref,_) -> class_of_global_reference ref + | Glob_term.GProd _ -> CL_FUN + | Glob_term.GSort _ -> CL_SORT + | _ -> raise Not_found let subst_cl_typ env subst ct = match ct with CL_SORT diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli index a65d7b806719..3693abfe137e 100644 --- a/pretyping/coercionops.mli +++ b/pretyping/coercionops.mli @@ -61,6 +61,8 @@ val class_nparams : cl_typ -> int its universe instance and its arguments *) val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list +val find_class_glob_type : 'a Glob_term.glob_constr_g -> cl_typ + (** raises [Not_found] if not convertible to a class *) val class_of : env -> evar_map -> types -> types * cl_typ From 232c29d4c23d6f83f622fb6cd9af74cabf9a8c08 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 9 Nov 2017 23:31:35 +0100 Subject: [PATCH 5/7] Interpreting a casted term in the scope bound to its type if any. This extends interpreting in type_scope a term casted by a sort. See discussion at issue #6077. --- interp/constrextern.ml | 3 ++- interp/constrintern.ml | 7 +++++-- test-suite/output/TermSyntax.out | 4 ++++ test-suite/output/TermSyntax.v | 5 ++++- 4 files changed, 15 insertions(+), 4 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 5d5ad120d6c6..574ef56a5c67 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1062,8 +1062,9 @@ let rec extern inctx ?impargs scopes vars r = | GGenarg arg -> CGenargGlob arg | GCast (c, k, c') -> + let scl = Notation.compute_glob_type_scope c' in let c' = extern_typ scopes vars c' in - let c = if isCSort c' then extern_typ scopes vars c else sub_extern true scopes vars c in + let c = extern true (fst scopes,(scl, snd (snd scopes))) vars c in CCast (c, k, c') | GInt i -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 53d083aad21e..abf9eb0ba54c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2390,9 +2390,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = DAst.make ?loc @@ GSort (intern_sort ~local_univs:env.local_univs s) | CCast (c1, k, c2) -> - let c1 = if isCSort c2 then intern_type env c1 else intern env c1 in + let c2 = intern_type (slide_binders env) c2 in + let sc = Notation.compute_glob_type_scope c2 in + let env' = {env with tmp_scope = sc @ env.tmp_scope} in + let c1 = intern env' c1 in DAst.make ?loc @@ - GCast (c1, k, intern_type (slide_binders env) c2) + GCast (c1, k, c2) | CArray(u,t,def,ty) -> DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty) ) diff --git a/test-suite/output/TermSyntax.out b/test-suite/output/TermSyntax.out index e023e17f22a4..f000a6e0861b 100644 --- a/test-suite/output/TermSyntax.out +++ b/test-suite/output/TermSyntax.out @@ -1,2 +1,6 @@ nat * nat : Type : Type +0 * 0 : nat + : nat +0 * 0 : Z + : Z diff --git a/test-suite/output/TermSyntax.v b/test-suite/output/TermSyntax.v index 1abbc4c3265a..b28b5cd84ea0 100644 --- a/test-suite/output/TermSyntax.v +++ b/test-suite/output/TermSyntax.v @@ -1,2 +1,5 @@ -(* Check Type cast setting type_scope *) +(* Check cast setting scopes *) Check nat * nat : Type. +Check 0 * 0 : nat. +Require Import ZArith. +Check 0 * 0 : Z. From 9af0a3261bc7fb6ab974c333640f3155d8c4ea57 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 9 Nov 2017 23:36:04 +0100 Subject: [PATCH 6/7] Interpreting a casted pattern in the scope bound to its type if any. See discussion at issue #6077. Works only when part of a recursive notation with binders yet, and not for printing. --- interp/constrintern.ml | 8 ++++---- test-suite/output/TermSyntax.out | 5 +++++ test-suite/output/TermSyntax.v | 8 ++++++++ 3 files changed, 17 insertions(+), 4 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index abf9eb0ba54c..7944d41c401f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -594,11 +594,11 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = (na,term,ty)) let intern_cases_pattern_as_binder intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) = - let p,t = match p with - | CPatCast (p, t) -> (p, Some t) - | _ -> (pv, None) in + let p,t,tmp_scope = match p with + | CPatCast (p, t) -> (p, Some t, (* Redone later, not nice: *) Notation.compute_glob_type_scope (intern (set_type_scope env) t)) + | _ -> (pv, None, []) in let il,disjpat = - let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (env_for_pattern (reset_tmp_scope env)) p in + let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (env_for_pattern {env with tmp_scope}) p in let substl,disjpat = List.split subst_disjpat in if not (List.for_all (fun subst -> Id.Map.equal Id.equal subst Id.Map.empty) substl) then user_err ?loc (str "Unsupported nested \"as\" clause."); diff --git a/test-suite/output/TermSyntax.out b/test-suite/output/TermSyntax.out index f000a6e0861b..c17b2729f50e 100644 --- a/test-suite/output/TermSyntax.out +++ b/test-suite/output/TermSyntax.out @@ -4,3 +4,8 @@ nat * nat : Type : nat 0 * 0 : Z : Z +File "./output/TermSyntax.v", line 11, characters 16-21: +The command has indeed failed with message: +Unknown interpretation for notation "{ _ ; _ }". +λ '(exist _ x _), x + : b → bool diff --git a/test-suite/output/TermSyntax.v b/test-suite/output/TermSyntax.v index b28b5cd84ea0..8860dc786856 100644 --- a/test-suite/output/TermSyntax.v +++ b/test-suite/output/TermSyntax.v @@ -3,3 +3,11 @@ Check nat * nat : Type. Check 0 * 0 : nat. Require Import ZArith. Check 0 * 0 : Z. + +Declare Scope b_scope. +Definition b := {x:bool|x=true}. +Notation "{ x ; y }" := (exist _ x y) : b_scope. +Require Import Utf8. +Fail Check λ '({x;y}:b), x. +Bind Scope b_scope with b. +Check λ '({x;y}:b), x. From 3ed759015416da61ac115549fd2c71c107d29484 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 27 Sep 2023 16:45:22 +0200 Subject: [PATCH 7/7] Add documentation --- .../03-notations/6134-master+type-scope-cast.rst | 10 ++++++++++ doc/sphinx/language/core/definitions.rst | 3 +++ doc/sphinx/user-extensions/syntax-extensions.rst | 11 +++++++++++ 3 files changed, 24 insertions(+) create mode 100644 doc/changelog/03-notations/6134-master+type-scope-cast.rst diff --git a/doc/changelog/03-notations/6134-master+type-scope-cast.rst b/doc/changelog/03-notations/6134-master+type-scope-cast.rst new file mode 100644 index 000000000000..cdf386c05ac6 --- /dev/null +++ b/doc/changelog/03-notations/6134-master+type-scope-cast.rst @@ -0,0 +1,10 @@ +- **Changed:** + In casts like :g:`term : t` where :g:`t` is bound to some + scope :g:`t_scope`, via :cmd:`Bind Scope`, the :g:`term` is now + interpreted in scope :g:`t_scope`. In particular when :g:`t` + is :g:`Type` the :g:`term` is interpreted in :g:`type_scope` + and when :g:`t` is a product the :g:`term` is interpreted + in :g:`fun_scope` + (`#6134 `_, + fixes `#14959 `_, + by Hugo Herbelin, reviewed by Maxime Dénès, Jim Fehrle, Emilio Gallego, Gaëtan Gilbert, Jason Gross, Pierre-Marie Pédrot, Pierre Roux, Bas Spitters and Théo Zimmermann). diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index a2c36af41223..89638ae45b07 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -57,6 +57,9 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`) :n:`@type` without leaving a trace in the produced value. This is a :gdef:`volatile cast`. +If a scope is :ref:`bound ` to +:n:`@type` then :n:`@term10` is interpreted in that scope. + .. _gallina-definitions: Top-level definitions diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index c14b4c61c7c4..302b04aa410d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1590,6 +1590,9 @@ Binding types or coercion classes to notation scopes then :g:`a` of type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted in scope ``scope``. + In explicit :ref:`casts ` :n:`@term : @coercion_class`, the :n:`term` + is interpreted in the :token:`scope_name` associated with :n:`@coercion_class`. + This command supports the :attr:`local`, :attr:`global`, :attr:`add_top` and :attr:`add_bottom` attributes. @@ -1652,6 +1655,14 @@ Binding types or coercion classes to notation scopes About f. + Bindings are also used in casts. + + .. coqtop:: all + + Close Scope F_scope. + Check #. + Check # : bool. + .. note:: Such stacks of scopes can be handy to share notations between multiple types. For instance, the scope ``T_scope`` above could contain many generic notations used for both the