aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml75
-rw-r--r--pretyping/classops.ml16
-rw-r--r--pretyping/classops.mli2
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v18
-rw-r--r--theories/Numbers/Integer/Binary/ZBinary.v5
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v24
-rw-r--r--theories/Numbers/Natural/Binary/NBinary.v5
-rw-r--r--theories/Numbers/Natural/Peano/NPeano.v5
-rw-r--r--toplevel/class.ml8
9 files changed, 92 insertions, 66 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index 6be016c18..f0cdc49cd 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 8205a6b2e..42925a4c2 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 3e6845f91..66bb5c6c6 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 9748a4366..236c56b9f 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 fbb91ef7f..366418035 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 858c06658..d2c93bbfd 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 cf284a2f1..bd59ef494 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 4578851e2..0cf9ae441 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 76d8750cb..4e729f446 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 07:14:49 +0000