From f22d5b55021fcf5fb11fa9d4fce3a7b8d9bc532f Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 26 Mar 2012 16:03:12 +0000 Subject: Module names and constant/inductive names are now in two separate namespaces We now accept the following code: Definition E := 0. Module E. End E. Techically, we simply allow the same label to occur at most twice in a structure_body, which is a (label * structure_field_body) list). These two label occurences should not be at the same level of fields (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change. Drawback : no more simple List.assoc or equivalent should be performed on a structure_body ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/declarations.mli | 4 +++ kernel/mod_typing.ml | 82 +++++++++++++++++++++++-------------------------- kernel/safe_typing.ml | 56 +++++++++++++++++++++------------ kernel/safe_typing.mli | 2 +- kernel/subtyping.ml | 74 +++++++++++++++++++++++--------------------- 5 files changed, 119 insertions(+), 99 deletions(-) (limited to 'kernel') 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 -- cgit v1.2.3