aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/mod_typing.ml82
-rw-r--r--kernel/safe_typing.ml56
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/subtyping.ml74
5 files changed, 119 insertions, 99 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 5b800edeca..7cf74ba3cd 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -192,6 +192,10 @@ type structure_field_body =
| SFBmodule of module_body
| SFBmodtype of module_type_body
+(** NB: we may encounter now (at most) twice the same label in
+ a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
+ and once for an object ([SFBconst] or [SFBmind]) *)
+
and structure_body = (label * structure_field_body) list
and struct_expr_body =
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e2304f1194..4cb6fc2fd3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -36,10 +36,14 @@ let rec mp_from_mexpr = function
| MSEfunctor (_,_,expr) -> mp_from_mexpr expr
| MSEwith (expr,_) -> mp_from_mexpr expr
-let rec list_split_assoc k rev_before = function
+let is_modular = function
+ | SFBmodule _ | SFBmodtype _ -> true
+ | SFBconst _ | SFBmind _ -> false
+
+let rec list_split_assoc ((k,m) as km) rev_before = function
| [] -> raise Not_found
- | (k',b)::after when k=k' -> rev_before,b,after
- | h::tail -> list_split_assoc k (h::rev_before) tail
+ | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
+ | h::tail -> list_split_assoc km (h::rev_before) tail
let discr_resolver env mtb =
match mtb.typ_expr with
@@ -55,35 +59,34 @@ let rec rebuild_mp mp l =
let rec check_with env sign with_decl alg_sign mp equiv =
let sign,wd,equiv,cst= match with_decl with
- | With_Definition (id,_) ->
- let sign,cb,cst = check_with_aux_def env sign with_decl mp equiv in
- sign,With_definition_body(id,cb),equiv,cst
- | With_Module (id,mp1) ->
- let sign,equiv,cst =
- check_with_aux_mod env sign with_decl mp equiv in
- sign,With_module_body(id,mp1),equiv,cst in
+ | With_Definition (idl,c) ->
+ let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
+ sign,With_definition_body(idl,cb),equiv,cst
+ | With_Module (idl,mp1) ->
+ let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
+ sign,With_module_body(idl,mp1),equiv,cst
+ in
if alg_sign = None then
sign,None,equiv,cst
else
sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
-and check_with_aux_def env sign with_decl mp equiv =
+and check_with_def env sign (idl,c) mp equiv =
let sig_b = match sign with
| SEBstruct(sig_b) -> sig_b
| _ -> error_signature_expected sign
in
- let id,idl = match with_decl with
- | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
- | With_Definition ([],_) | With_Module ([],_) -> assert false
+ let id,idl = match idl with
+ | [] -> assert false
+ | id::idl -> id,idl
in
let l = label_of_id id in
try
- let rev_before,spec,after = list_split_assoc l [] sig_b in
+ let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
let before = List.rev rev_before in
let env' = Modops.add_signature mp before equiv env in
- match with_decl with
- | With_Definition ([],_) -> assert false
- | With_Definition ([id],c) ->
+ if idl = [] then
+ (* Toplevel definition *)
let cb = match spec with
| SFBconst cb -> cb
| _ -> error_not_a_constant l
@@ -116,8 +119,9 @@ and check_with_aux_def env sign with_decl mp equiv =
Cemitcodes.from_val (compile_constant_body env' def);
const_constraints = cst }
in
- SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
- | With_Definition (_::_,c) ->
+ SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
+ else
+ (* Definition inside a sub-module *)
let old = match spec with
| SFBmodule msb -> msb
| _ -> error_not_a_module (string_of_label l)
@@ -125,43 +129,36 @@ and check_with_aux_def env sign with_decl mp equiv =
begin
match old.mod_expr with
| None ->
- let new_with_decl = With_Definition (idl,c) in
let sign,cb,cst =
- check_with_aux_def env' old.mod_type new_with_decl
+ check_with_def env' old.mod_type (idl,c)
(MPdot(mp,l)) old.mod_delta in
let new_spec = SFBmodule({old with
mod_type = sign;
mod_type_alg = None}) in
- SEBstruct(before@((l,new_spec)::after)),cb,cst
+ SEBstruct(before@(l,new_spec)::after),cb,cst
| Some msb ->
error_generative_module_expected l
end
- | _ -> anomaly "Modtyping:incorrect use of with"
with
| Not_found -> error_no_such_label l
| Reduction.NotConvertible -> error_incorrect_with_constraint l
-and check_with_aux_mod env sign with_decl mp equiv =
+and check_with_mod env sign (idl,mp1) mp equiv =
let sig_b = match sign with
| SEBstruct(sig_b) ->sig_b
| _ -> error_signature_expected sign
in
- let id,idl = match with_decl with
- | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl
- | With_Definition ([],_) | With_Module ([],_) -> assert false
+ let id,idl = match idl with
+ | [] -> assert false
+ | id::idl -> id,idl
in
let l = label_of_id id in
try
- let rev_before,spec,after = list_split_assoc l [] sig_b in
+ let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
let before = List.rev rev_before in
- let rec mp_rec = function
- | [] -> mp
- | i::r -> MPdot(mp_rec r,label_of_id i)
- in
let env' = Modops.add_signature mp before equiv env in
- match with_decl with
- | With_Module ([],_) -> assert false
- | With_Module ([id], mp1) ->
+ if idl = [] then
+ (* Toplevel module definition *)
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module (string_of_label l)
@@ -195,7 +192,8 @@ and check_with_aux_mod env sign with_decl mp equiv =
let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
add_delta_resolver equiv new_mb.mod_delta,cst
- | With_Module (idc,mp1) ->
+ else
+ (* Module definition of a sub-module *)
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module (string_of_label l)
@@ -203,10 +201,9 @@ and check_with_aux_mod env sign with_decl mp equiv =
begin
match old.mod_expr with
None ->
- let new_with_decl = With_Module (idl,mp1) in
let sign,equiv',cst =
- check_with_aux_mod env'
- old.mod_type new_with_decl (MPdot(mp,l)) old.mod_delta in
+ check_with_mod env'
+ old.mod_type (idl,mp1) (MPdot(mp,l)) old.mod_delta in
let new_equiv = add_delta_resolver equiv equiv' in
let new_spec = SFBmodule {old with
mod_type = sign;
@@ -224,7 +221,6 @@ and check_with_aux_mod env sign with_decl mp equiv =
| _ ->
error_generative_module_expected l
end
- | _ -> anomaly "Modtyping:incorrect use of with"
with
Not_found -> error_no_such_label l
| Reduction.NotConvertible -> error_incorrect_with_constraint l
@@ -369,7 +365,7 @@ let rec add_struct_expr_constraints env = function
| SEBstruct (structure_body) ->
List.fold_left
- (fun env (l,item) -> add_struct_elem_constraints env item)
+ (fun env (_,item) -> add_struct_elem_constraints env item)
env
structure_body
@@ -414,7 +410,7 @@ let rec struct_expr_constraints cst = function
| SEBstruct (structure_body) ->
List.fold_left
- (fun cst (l,item) -> struct_elem_constraints cst item)
+ (fun cst (_,item) -> struct_elem_constraints cst item)
cst
structure_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e87bc9c1c1..94be2602e0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -102,7 +102,8 @@ type safe_environment =
{ old : safe_environment;
env : env;
modinfo : module_info;
- labset : Labset.t;
+ modlabels : Labset.t;
+ objlabels : Labset.t;
revstruct : structure_body;
univ : Univ.constraints;
engagement : engagement option;
@@ -110,13 +111,16 @@ type safe_environment =
loads : (module_path * module_body) list;
local_retroknowledge : Retroknowledge.action list}
-let exists_label l senv = Labset.mem l senv.labset
+let exists_modlabel l senv = Labset.mem l senv.modlabels
+let exists_objlabel l senv = Labset.mem l senv.objlabels
-let check_label l senv =
- if exists_label l senv then error_existing_label l
+let check_modlabel l senv =
+ if exists_modlabel l senv then error_existing_label l
+let check_objlabel l senv =
+ if exists_objlabel l senv then error_existing_label l
-let check_labels ls senv =
- Labset.iter (fun l -> check_label l senv) ls
+let check_objlabels ls senv =
+ Labset.iter (fun l -> check_objlabel l senv) ls
let labels_of_mib mib =
let add,get =
@@ -141,7 +145,8 @@ let rec empty_environment =
variant = NONE;
resolver = empty_delta_resolver;
resolver_of_param = empty_delta_resolver};
- labset = Labset.empty;
+ modlabels = Labset.empty;
+ objlabels = Labset.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -173,11 +178,15 @@ type generic_name =
| M
let add_field ((l,sfb) as field) gn senv =
- let labels = match sfb with
- | SFBmind mib -> labels_of_mib mib
- | _ -> Labset.singleton l
+ let mlabs,olabs = match sfb with
+ | SFBmind mib ->
+ let l = labels_of_mib mib in
+ check_objlabels l senv; (Labset.empty,l)
+ | SFBconst _ ->
+ check_objlabel l senv; (Labset.empty, Labset.singleton l)
+ | SFBmodule _ | SFBmodtype _ ->
+ check_modlabel l senv; (Labset.singleton l, Labset.empty)
in
- check_labels labels senv;
let senv = add_constraints (constraints_of_sfb sfb) senv in
let env' = match sfb, gn with
| SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -188,7 +197,8 @@ let add_field ((l,sfb) as field) gn senv =
in
{ senv with
env = env';
- labset = Labset.union labels senv.labset;
+ modlabels = Labset.union mlabs senv.modlabels;
+ objlabels = Labset.union olabs senv.objlabels;
revstruct = field :: senv.revstruct }
(* Applying a certain function to the resolver of a safe environment *)
@@ -321,7 +331,7 @@ let add_module l me inl senv =
(* Interactive modules *)
let start_module l senv =
- check_label l senv;
+ check_modlabel l senv;
let mp = MPdot(senv.modinfo.modpath, l) in
let modinfo = { modpath = mp;
label = l;
@@ -332,7 +342,8 @@ let start_module l senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- labset = Labset.empty;
+ modlabels = Labset.empty;
+ objlabels = Labset.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -416,7 +427,8 @@ let end_module l restype senv =
mp,resolver,{ old = oldsenv.old;
env = newenv;
modinfo = modinfo;
- labset = Labset.add l oldsenv.labset;
+ modlabels = Labset.add l oldsenv.modlabels;
+ objlabels = oldsenv.objlabels;
revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
univ = Univ.union_constraints senv'.univ oldsenv.univ;
(* engagement is propagated to the upper level *)
@@ -511,7 +523,8 @@ let add_module_parameter mbid mte inl senv =
variant = new_variant;
resolver_of_param = add_delta_resolver
resolver_of_param senv.modinfo.resolver_of_param};
- labset = senv.labset;
+ modlabels = senv.modlabels;
+ objlabels = senv.objlabels;
revstruct = [];
univ = senv.univ;
engagement = senv.engagement;
@@ -523,7 +536,7 @@ let add_module_parameter mbid mte inl senv =
(* Interactive module types *)
let start_modtype l senv =
- check_label l senv;
+ check_modlabel l senv;
let mp = MPdot(senv.modinfo.modpath, l) in
let modinfo = { modpath = mp;
label = l;
@@ -534,7 +547,8 @@ let start_modtype l senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- labset = Labset.empty;
+ modlabels = Labset.empty;
+ objlabels = Labset.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
@@ -585,7 +599,8 @@ let end_modtype l senv =
mp, { old = oldsenv.old;
env = newenv;
modinfo = oldsenv.modinfo;
- labset = Labset.add l oldsenv.labset;
+ modlabels = Labset.add l oldsenv.modlabels;
+ objlabels = oldsenv.objlabels;
revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
univ = Univ.union_constraints senv.univ oldsenv.univ;
engagement = senv.engagement;
@@ -644,7 +659,8 @@ let start_library dir senv =
mp, { old = senv;
env = senv.env;
modinfo = modinfo;
- labset = Labset.empty;
+ modlabels = Labset.empty;
+ objlabels = Labset.empty;
revstruct = [];
univ = Univ.empty_constraint;
engagement = None;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6f46a45be9..ad275d49ec 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -138,7 +138,7 @@ val typing : safe_environment -> constr -> judgment
(** {7 Query } *)
-val exists_label : label -> safe_environment -> bool
+val exists_objlabel : label -> safe_environment -> bool
(*spiwack: safe retroknowledge functionalities *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 9fb0454077..46734b30bd 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -33,15 +33,18 @@ type namedobject =
| Constant of constant_body
| IndType of inductive * mutual_inductive_body
| IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
| Module of module_body
| Modtype of module_type_body
(* adds above information about one mutual inductive: all types and
constructors *)
-let add_nameobjects_of_mib ln mib map =
- let add_nameobjects_of_one j oib map =
- let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+ let ind = make_mind mp empty_dirpath l in
+ let add_mip_nameobjects j oib map =
+ let ip = (ind,j) in
let map =
array_fold_right_i
(fun i id map ->
@@ -51,22 +54,33 @@ let add_nameobjects_of_mib ln mib map =
in
Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
in
- array_fold_right_i add_nameobjects_of_one mib.mind_packets map
+ array_fold_right_i add_mip_nameobjects mib.mind_packets map
+
+
+(* creates (namedobject/namedmodule) map for the whole signature *)
+
+type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
-(* creates namedobject map for the whole signature *)
+let get_obj mp map l =
+ try Labmap.find l map.objs
+ with Not_found -> error_no_such_label_sub l (string_of_mp mp)
-let make_label_map mp list =
+let get_mod mp map l =
+ try Labmap.find l map.mods
+ with Not_found -> error_no_such_label_sub l (string_of_mp mp)
+
+let make_labmap mp list =
let add_one (l,e) map =
- let add_map obj = Labmap.add l obj map in
match e with
- | SFBconst cb -> add_map (Constant cb)
- | SFBmind mib ->
- add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
- | SFBmodule mb -> add_map (Module mb)
- | SFBmodtype mtb -> add_map (Modtype mtb)
+ | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+ | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
+ | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
+ | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
in
- List.fold_right add_one list Labmap.empty
+ List.fold_right add_one list empty_labmap
+
let check_conv_error error why cst f env a1 a2 =
try
@@ -300,7 +314,6 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv NotConvertibleTypeField cst conv env ty1 ty2
- | _ -> error DefinitionFieldExpected
let rec check_modules cst env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module None msb1 in
@@ -309,33 +322,24 @@ let rec check_modules cst env msb1 msb2 subst1 subst2 =
cst
and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
- let map1 = make_label_map mp1 sig1 in
+ let map1 = make_labmap mp1 sig1 in
let check_one_body cst (l,spec2) =
- let info1 =
- try
- Labmap.find l map1
- with
- Not_found -> error_no_such_label_sub l
- (string_of_mp mp1)
- in
- match spec2 with
+ match spec2 with
| SFBconst cb2 ->
- check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2
+ check_constant cst env mp1 l (get_obj mp1 map1 l)
+ cb2 spec2 subst1 subst2
| SFBmind mib2 ->
- check_inductive cst env
- mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
+ check_inductive cst env mp1 l (get_obj mp1 map1 l)
+ mp2 mib2 spec2 subst1 subst2 reso1 reso2
| SFBmodule msb2 ->
- begin
- match info1 with
- | Module msb -> check_modules cst env msb msb2
- subst1 subst2
- | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
+ begin match get_mod mp1 map1 l with
+ | Module msb -> check_modules cst env msb msb2 subst1 subst2
+ | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
end
| SFBmodtype mtb2 ->
- let mtb1 =
- match info1 with
- | Modtype mtb -> mtb
- | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
+ let mtb1 = match get_mod mp1 map1 l with
+ | Modtype mtb -> mtb
+ | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
in
let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
(add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:32:58 +0000