An automatic substitution of scope at functor application

 For Argument Scope, we now record types (more precisely classes cl_typ)
 in addition to scope list. After substitution (e.g. at functor application),
 the new types are used to search for corresponding concrete scopes.

 Currently, this automatic scope substitution of argument scope takes
 precedence (if successful) over scope declared in the functor (even
 by the user). On the opposite, the manual scope substitution
 (cf last commit introducing annotation [scope foo to bar])
 is done _after_ the automatic scope substitution.

 TODO: if this behavior is satisfactory, document it ...

 Note that Classops.find_class_type lose its env args since it was
 actually unused, and is now used for Notation.find_class

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

9 files changed, 92 insertions, 66 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 6be016c180..f0cdc49cda 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -444,27 +444,39 @@ let declare_class_scope sc cl =
 let find_class_scope cl =
   Gmap.find cl !class_scope_map
 
-let find_class t =
-  let t, _ = decompose_app (Reductionops.whd_betaiotazeta Evd.empty t) in
-  match kind_of_term t with
-    | Var id -> CL_SECVAR id
-    | Const sp -> CL_CONST sp
-    | Ind ind_sp -> CL_IND ind_sp
-    | Prod (_,_,_) -> CL_FUN
-    | Sort _ -> CL_SORT
-    |  _ -> raise Not_found
+let find_class_scope_opt = function
+  | None -> None
+  | Some cl -> try Some (find_class_scope cl) with Not_found -> None
+
+let find_class t = fst (find_class_type Evd.empty t)
 
 (**********************************************************************)
 (* Special scopes associated to arguments of a global reference *)
 
-let rec compute_arguments_scope t =
+let rec compute_arguments_classes t =
   match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with
     | Prod (_,t,u) ->
-	let sc =
-	  try Some (find_class_scope (find_class t)) with Not_found -> None in
-	sc :: compute_arguments_scope u
+	let cl = try Some (find_class t) with Not_found -> None in
+	cl :: compute_arguments_classes u
     | _ -> []
 
+let compute_arguments_scope_full t =
+  let cls = compute_arguments_classes t in
+  let scs = List.map find_class_scope_opt cls in
+  scs, cls
+
+let compute_arguments_scope t = fst (compute_arguments_scope_full t)
+
+(** 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 *)
+
+let rec merge_scope sc1 sc2 = match sc1, sc2 with
+  | [], _ -> sc2
+  | _, [] -> sc1
+  | Some sc :: sc1, _ :: sc2 -> Some sc :: merge_scope sc1 sc2
+  | None :: sc1, sco :: sc2 -> sco :: merge_scope sc1 sc2
+
 let arguments_scope = ref Refmap.empty
 
 type arguments_scope_discharge_request =
@@ -472,36 +484,39 @@ type arguments_scope_discharge_request =
   | ArgsScopeManual
   | ArgsScopeNoDischarge
 
-let load_arguments_scope _ (_,(_,r,scl)) =
+let load_arguments_scope _ (_,(_,r,scl,cls)) =
   List.iter (Option.iter check_scope) scl;
-  arguments_scope := Refmap.add r scl !arguments_scope
+  arguments_scope := Refmap.add r (scl,cls) !arguments_scope
 
 let cache_arguments_scope o =
   load_arguments_scope 1 o
 
-let subst_arguments_scope (subst,(req,r,scl)) =
+let subst_arguments_scope (subst,(req,r,scl,cls)) =
   let r' = fst (subst_global subst r) in
-  let scl' = list_smartmap (Option.smartmap Declaremods.subst_scope) scl in
-  (ArgsScopeNoDischarge,r',scl')
+  let cls' = list_smartmap (Option.smartmap (subst_cl_typ subst)) cls in
+  let scl' = merge_scope (List.map find_class_scope_opt cls') scl in
+  let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
+  (ArgsScopeNoDischarge,r',scl'',cls')
 
-let discharge_arguments_scope (_,(req,r,l)) =
+let discharge_arguments_scope (_,(req,r,l,_)) =
   if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
-  else Some (req,Lib.discharge_global r,l)
+  else Some (req,Lib.discharge_global r,l,[])
 
-let classify_arguments_scope (req,_,_ as obj) =
+let classify_arguments_scope (req,_,_,_ as obj) =
   if req = ArgsScopeNoDischarge then Dispose else Substitute obj
 
-let rebuild_arguments_scope (req,r,l) =
+let rebuild_arguments_scope (req,r,l,_) =
   match req with
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
-	(req,r,compute_arguments_scope (Global.type_of_global r))
+        let scs,cls = compute_arguments_scope_full (Global.type_of_global r) in
+	(req,r,scs,cls)
     | ArgsScopeManual ->
 	(* Add to the manually given scopes the one found automatically
            for the extra parameters of the section *)
-	let l' = compute_arguments_scope (Global.type_of_global r) in
+	let l',cls = compute_arguments_scope_full (Global.type_of_global r) in
 	let l1,_ = list_chop (List.length l' - List.length l) l' in
-	(req,r,l1@l)
+	(req,r,l1@l,cls)
 
 let inArgumentsScope =
   declare_object {(default_object "ARGUMENTS-SCOPE") with
@@ -514,21 +529,21 @@ let inArgumentsScope =
 
 let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
 
-let declare_arguments_scope_gen req r scl =
-  Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
+let declare_arguments_scope_gen req r (scl,cls) =
+  Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
 
 let declare_arguments_scope local ref scl =
   let req =
     if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
-  declare_arguments_scope_gen req ref scl
+  declare_arguments_scope_gen req ref (scl,[])
 
 let find_arguments_scope r =
-  try Refmap.find r !arguments_scope
+  try fst (Refmap.find r !arguments_scope)
   with Not_found -> []
 
 let declare_ref_arguments_scope ref =
   let t = Global.type_of_global ref in
-  declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope t)
+  declare_arguments_scope_gen ArgsScopeAuto ref (compute_arguments_scope_full t)
 
 
 (********************************)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 8205a6b2e8..42925a4c22 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -132,9 +132,9 @@ let coercion_info coe = Gmap.find coe !coercion_tab
 
 let coercion_exists coe = Gmap.mem coe !coercion_tab
 
-(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
+(* find_class_type : evar_map -> constr -> cl_typ * constr list *)
 
-let find_class_type env sigma t =
+let find_class_type sigma t =
   let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
   match kind_of_term t' with
     | Var id -> CL_SECVAR id, args
@@ -152,7 +152,7 @@ let subst_cl_typ subst ct = match ct with
   | CL_CONST kn ->
       let kn',t = subst_con subst kn in
 	if kn' == kn then ct else
-         fst (find_class_type (Global.env()) Evd.empty t)
+         fst (find_class_type Evd.empty t)
   | CL_IND (kn,i) ->
       let kn' = subst_ind subst kn in
 	if kn' == kn then ct else
@@ -167,12 +167,12 @@ let subst_coe_typ subst t = fst (subst_global subst t)
 let class_of env sigma t =
   let (t, n1, i, args) =
     try
-      let (cl,args) = find_class_type env sigma t in
+      let (cl,args) = find_class_type sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
-      let (cl, args) = find_class_type env sigma t in
+      let (cl, args) = find_class_type sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, args)
   in
@@ -180,7 +180,7 @@ let class_of env sigma t =
 
 let inductive_class_of ind = fst (class_info (CL_IND ind))
 
-let class_args_of env sigma c = snd (find_class_type env sigma c)
+let class_args_of env sigma c = snd (find_class_type sigma c)
 
 let string_of_class = function
   | CL_FUN -> "Funclass"
@@ -209,14 +209,14 @@ let lookup_path_to_sort_from_class s =
 
 let apply_on_class_of env sigma t cont =
   try
-    let (cl,args) = find_class_type env sigma t in
+    let (cl,args) = find_class_type sigma t in
     let (i, { cl_param = n1 } ) = class_info cl in
     if List.length args <> n1 then raise Not_found;
     t, cont i
   with Not_found ->
     (* Is it worth to be more incremental on the delta steps? *)
     let t = Tacred.hnf_constr env sigma t in
-    let (cl, args) = find_class_type env sigma t in
+    let (cl, args) = find_class_type sigma t in
     let (i, { cl_param = n1 } ) = class_info cl in
     if List.length args <> n1 then raise Not_found;
     t, cont i
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 3e6845f91d..66bb5c6c6a 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -50,7 +50,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 
 (** [find_class_type env sigma c] returns the head reference of [c] and its
    arguments *)
-val find_class_type : env -> evar_map -> types -> cl_typ * constr list
+val find_class_type : evar_map -> types -> cl_typ * constr list
 
 (** raises [Not_found] if not convertible to a class *)
 val class_of : env -> evar_map -> types -> types * cl_index
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 9748a43666..236c56b9f2 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -26,13 +26,17 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
 Delimit Scope bigZ_scope with bigZ.
 
-Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
- ZMake.Make BigN [scope abstract_scope to bigZ_scope]
- <+ ZTypeIsZAxioms [scope abstract_scope to bigZ_scope]
- <+ ZProp [no inline, scope abstract_scope to bigZ_scope]
- <+ HasEqBool2Dec [no inline, scope abstract_scope to bigZ_scope]
- <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigZ_scope]
- <+ MinMaxDecProperties [no inline, scope abstract_scope to bigZ_scope].
+Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder.
+ Include ZMake.Make BigN [scope abstract_scope to bigZ_scope].
+ Bind Scope bigZ_scope with t t_.
+ Include ZTypeIsZAxioms
+ <+ ZProp [no inline]
+ <+ HasEqBool2Dec [no inline]
+ <+ MinMaxLogicalProperties [no inline]
+ <+ MinMaxDecProperties [no inline].
+End BigZ.
+
+(** For precision concerning the above scope handling, see comment in BigN *)
 
 (** Notations about [BigZ] *)
 
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index fbb91ef7f2..3664180357 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -223,9 +223,8 @@ Definition eq := (@eq Z).
 
 (** Now the generic properties. *)
 
-Include ZProp [scope abstract_scope to Z_scope]
- <+ UsualMinMaxLogicalProperties [scope abstract_scope to Z_scope]
- <+ UsualMinMaxDecProperties [scope abstract_scope to Z_scope].
+Include ZProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End Z.
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 858c066581..d2c93bbfd1 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -28,13 +28,23 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
 
 Delimit Scope bigN_scope with bigN.
 
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
- NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope]
- <+ NTypeIsNAxioms [scope abstract_scope to bigN_scope]
- <+ NProp [no inline, scope abstract_scope to bigN_scope]
- <+ HasEqBool2Dec [no inline, scope abstract_scope to bigN_scope]
- <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigN_scope]
- <+ MinMaxDecProperties [no inline, scope abstract_scope to bigN_scope].
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder.
+ Include NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope].
+ Bind Scope bigN_scope with t t'.
+ Include NTypeIsNAxioms
+  <+ NProp [no inline]
+  <+ HasEqBool2Dec [no inline]
+  <+ MinMaxLogicalProperties [no inline]
+  <+ MinMaxDecProperties [no inline].
+End BigN.
+
+(** Nota concerning scopes : for the first Include, we cannot bind
+    the scope bigN_scope to a type that doesn't exists yet.
+    We hence need to explicitely declare the scope substitution.
+    For the next Include, the abstract type t (in scope abstract_scope)
+    gets substituted to concrete BigN.t (in scope bigN_scope),
+    and the corresponding argument scope are fixed automatically.
+*)
 
 (** Notations about [BigN] *)
 
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index cf284a2f19..bd59ef494b 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -234,9 +234,8 @@ Definition lor := Nor.
 Definition ldiff := Ndiff.
 Definition div2 := Ndiv2.
 
-Include NProp [scope abstract_scope to N_scope]
- <+ UsualMinMaxLogicalProperties [scope abstract_scope to N_scope]
- <+ UsualMinMaxDecProperties [scope abstract_scope to N_scope].
+Include NProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End N.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 4578851e27..0cf9ae4416 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -756,9 +756,8 @@ Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _.
 
 (** Generic Properties *)
 
-Include NProp [scope abstract_scope to nat_scope]
- <+ UsualMinMaxLogicalProperties [scope abstract_scope to nat_scope]
- <+ UsualMinMaxDecProperties [scope abstract_scope to nat_scope].
+Include NProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End Nat.
 
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 76d8750cb3..4e729f4460 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -124,7 +124,7 @@ let get_source lp source =
 	let (cl1,lv1) =
           match lp with
 	    | [] -> raise Not_found
-            | t1::_ -> find_class_type (Global.env()) Evd.empty t1
+            | t1::_ -> find_class_type Evd.empty t1
         in
 	(cl1,lv1,1)
     | Some cl ->
@@ -132,7 +132,7 @@ let get_source lp source =
 	  | [] -> raise Not_found
 	  | t1::lt ->
 	      try
-		let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in
+		let cl1,lv1 = find_class_type Evd.empty t1 in
 		if cl = cl1 then cl1,lv1,(List.length lt+1)
 		else raise Not_found
               with Not_found -> aux lt
@@ -142,7 +142,7 @@ let get_target t ind =
   if (ind > 1) then
     CL_FUN
   else
-    fst (find_class_type (Global.env()) Evd.empty t)
+    fst (find_class_type Evd.empty t)
 
 let prods_of t =
   let rec aux acc d = match kind_of_term d with
@@ -210,7 +210,7 @@ let build_id_coercion idf_opt source =
     match idf_opt with
       | Some idf -> idf
       | None ->
-	  let cl,_ = find_class_type (Global.env()) Evd.empty t in
+	  let cl,_ = find_class_type Evd.empty t in
 	  id_of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in