Taking into account the type of a definition (if it exists), and the

type in "cast" to activate the temporary interpretation scope.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7

interp/constrintern.ml

@@ -296,6 +296,12 @@ let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
 
 let reset_tmp_scope env = {env with tmp_scope = None}
 
+let set_scope env = function
+  | CastConv (GSort _) -> set_type_scope env
+  | CastConv (GRef (_,ref) | GApp (_,GRef (_,ref),_)) ->
+      {env with tmp_scope = compute_scope_of_global ref}
+  | _ -> env
+
 let rec it_mkGProd loc2 env body =
   match env with
       (loc1, (na, bk, _, t)) :: tl -> it_mkGProd loc2 tl (GProd (Loc.merge loc1 loc2, na, bk, t, body))
@@ -1441,7 +1447,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CSort (loc, s) ->
 	GSort(loc,s)
     | CCast (loc, c1, c2) ->
-	GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2)
+        let c2 = Miscops.map_cast_type (intern_type env) c2 in
+        let env' = set_scope env c2 in
+	GCast (loc,intern env' c1, c2)
 
   and intern_type env = intern (set_type_scope env)
 
@@ -1599,19 +1607,23 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Idset.empty
 
-let intern_gen isarity sigma env
+let scope_of_type_kind = function
+  | IsType -> Some Notation.type_scope
+  | OfType (Some typ) -> compute_type_scope typ
+  | OfType None -> None
+
+let intern_gen kind sigma env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
-  let tmp_scope =
-    if isarity then Some Notation.type_scope else None in
-    internalize sigma env {ids = extract_ids env; unb = false;
-			   tmp_scope = tmp_scope; scopes = [];
-			  impls = impls}
-      allow_patvar (ltacvars, []) c
+  let tmp_scope = scope_of_type_kind kind in
+  internalize sigma env {ids = extract_ids env; unb = false;
+		         tmp_scope = tmp_scope; scopes = [];
+			 impls = impls}
+    allow_patvar (ltacvars, []) c
 
-let intern_constr sigma env c = intern_gen false sigma env c
+let intern_constr sigma env c = intern_gen (OfType None) sigma env c
 
-let intern_type sigma env c = intern_gen true sigma env c
+let intern_type sigma env c = intern_gen IsType sigma env c
 
 let intern_pattern globalenv patt =
   try
@@ -1629,7 +1641,7 @@ let intern_pattern globalenv patt =
 let interp_gen kind sigma env
                ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
-  let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in
+  let c = intern_gen kind ~impls ~allow_patvar ~ltacvars sigma env c in
     understand_gen kind sigma env c
 
 let interp_constr sigma env c =
@@ -1645,7 +1657,7 @@ let interp_open_constr sigma env c =
   understand_tcc sigma env (intern_constr sigma env c)
 
 let interp_open_constr_patvar sigma env c =
-  let raw = intern_gen false sigma env c ~allow_patvar:true in
+  let raw = intern_gen (OfType None) sigma env c ~allow_patvar:true in
   let sigma = ref sigma in
   let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in
   let rec patvar_to_evar r = match r with
@@ -1673,7 +1685,7 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true)
     | Some evdref -> evdref
   in
   let istype = kind = IsType in
-  let c = intern_gen istype ~impls !evdref env c in
+  let c = intern_gen kind ~impls !evdref env c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:istype c in
     understand_tcc_evars ~fail_evar evdref env kind c, imps
 
@@ -1688,7 +1700,7 @@ let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=empty_intern
   interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c
 
 let interp_constr_evars_gen evdref env ?(impls=empty_internalization_env) kind c =
-  let c = intern_gen (kind=IsType) ~impls !evdref env c in
+  let c = intern_gen kind ~impls !evdref env c in
     understand_tcc_evars evdref env kind c
 
 let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c typ =
@@ -1700,7 +1712,8 @@ let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
-  let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
+  let c = intern_gen (if as_type then IsType else OfType None)
+            ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_glob_constr c
 
 let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
@@ -1722,12 +1735,12 @@ let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
 (* Interpret binders and contexts  *)
 
 let interp_binder sigma env na t =
-  let t = intern_gen true sigma env t in
+  let t = intern_gen IsType sigma env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
   understand_type sigma env t'
 
 let interp_binder_evars evdref env na t =
-  let t = intern_gen true !evdref env t in
+  let t = intern_gen IsType !evdref env t in
   let t' = locate_if_isevar (loc_of_glob_constr t) na t in
   understand_tcc_evars evdref env IsType t'
 

interp/constrintern.mli

@@ -78,7 +78,7 @@ val intern_constr : evar_map -> env -> constr_expr -> glob_constr
 
 val intern_type : evar_map -> env -> constr_expr -> glob_constr
 
-val intern_gen : bool -> evar_map -> env ->
+val intern_gen : typing_constraint -> evar_map -> env ->
   ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> glob_constr
 

interp/notation.ml

@@ -513,6 +513,12 @@ let compute_arguments_scope_full t =
 
 let compute_arguments_scope t = fst (compute_arguments_scope_full t)
 
+let compute_type_scope t =
+  find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None)
+
+let compute_scope_of_global ref =
+  find_scope_class_opt (Some (ScopeRef ref))
+
 (** When merging scope list, we give priority to the first one (computed
     by substitution), using the second one (user given or earlier automatic)
     as fallback *)

interp/notation.mli

@@ -160,6 +160,8 @@ val declare_scope_class : scope_name -> scope_class -> unit
 val declare_ref_arguments_scope : global_reference -> unit
 
 val compute_arguments_scope : Term.types -> scope_name option list
+val compute_type_scope : Term.types -> scope_name option
+val compute_scope_of_global : global_reference -> scope_name option
 
 (** Building notation key *)
 

plugins/funind/indfun.ml

@@ -133,7 +133,7 @@ let rec abstract_glob_constr c = function
         (abstract_glob_constr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
-  Constrintern.intern_gen false sigma env ~impls
+  Constrintern.intern_gen (Pretyping.OfType None) sigma env ~impls
     ~allow_patvar:false  ~ltacvars:([],[]) c
 
 (*

tactics/tacintern.ml

@@ -347,8 +347,9 @@ let intern_binding_name ist x =
 
 let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
+  let scope = if isarity then Pretyping.IsType else Pretyping.OfType None in
   let c' =
-    warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
+    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
   in
   (c',if !strict_check then None else Some c)
 

tactics/tacinterp.ml

@@ -465,7 +465,7 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
        intros/lettac/inversion hypothesis names *)
   | Some c ->
       let ltacdata = (List.map fst ltacvars,unbndltacvars) in
-      intern_gen (kind = IsType) ~allow_patvar ~ltacvars:ltacdata sigma env c
+      intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
   in
   let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
   let evdc =

test-suite/success/Scopes.v

@@ -13,3 +13,11 @@ Record B := { f :> Z -> Z }.
 Variable a:B.
 Arguments Scope a [Z_scope].
 Check a 0.
+
+(* Check that casts activate scopes if ever possible *)
+
+Inductive U := A.
+Bind Scope u with U.
+Notation "'ε'" := A : u.
+Definition c := ε : U.
+Check ε : U

toplevel/metasyntax.ml

@@ -313,10 +313,10 @@ let rec find_pattern nt xl = function
       find_pattern nt (x::xl) (l,l')
   | [], NonTerminal x' :: l' ->
       (out_nt nt,x',List.rev xl),l'
-  | _, Terminal s :: _ | Terminal s :: _, _ ->
-      error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
   | _, Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
+  | _, Terminal s :: _ | Terminal s :: _, _ ->
+      error ("The token \""^s^"\" occurs on one side of \"..\" but not on the other side.")
   | _, [] ->
       error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
   | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->

toplevel/record.ml

@@ -26,7 +26,7 @@ open Constrexpr_ops
 (********** definition d'un record (structure) **************)
 
 let interp_evars evdref env impls k typ =
-  let typ' = intern_gen true ~impls !evdref env typ in
+  let typ' = intern_gen Pretyping.IsType ~impls !evdref env typ in
   let imps = Implicit_quantifiers.implicits_of_glob_constr typ' in
     imps, Pretyping.understand_tcc_evars evdref env k typ'