Merge PR coq#6134: Interpreting a casted term in the scope bound to i…

…ts type if any

Reviewed-by: proux01
Ack-by: jfehrle
Co-authored-by: proux01 <[email protected]>

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 <https://github.com/coq/coq/pull/6134>`_,
+  fixes `#14959 <https://github.com/coq/coq/issues/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).

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 <LocalInterpretationRulesForNotations>` to
+:n:`@type` then :n:`@term10` is interpreted in that scope.
+
 .. _gallina-definitions:
 
 Top-level definitions

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 <type-cast>` :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

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

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

interp/constrextern.ml

@@ -1062,7 +1062,10 @@ 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 scl = Notation.compute_glob_type_scope c' in
+    let c' = extern_typ scopes vars c' in
+    let c = extern true (fst scopes,(scl, snd (snd scopes))) vars c in
+    CCast (c, k, c')
 
   | GInt i ->
      extern_prim_token_delimiter_if_required

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.");
@@ -2390,8 +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 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 (intern env 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)
     )

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
 

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

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

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
 

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

test-suite/output/NNumberSyntax.v

@@ -10,40 +10,40 @@ 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.
 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.