From 34d131d524c0d532a8336690cf6b513e819157da Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 20 Aug 2013 08:22:45 +0000 Subject: Mod_typing : code cleanup git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16709 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/mod_typing.ml | 377 +++++++++++++++++++++++++-------------------------- 1 file changed, 181 insertions(+), 196 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index befa822ce..d5555c624 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -12,15 +12,12 @@ (* This module provides the main functions for type-checking module declarations *) -open Errors open Util open Names -open Univ open Declarations open Entries open Environ open Modops -open Subtyping open Mod_subst exception Not_path @@ -39,10 +36,16 @@ 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 Label.equal k k' && (is_modular b) == (m : bool) -> rev_before,b,after - | h::tail -> list_split_assoc km (h::rev_before) tail +(** Split a [structure_body] at some label corresponding to + a modular definition or not. *) + +let split_sign k m struc = + let rec split rev_before = function + | [] -> raise Not_found + | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) -> + List.rev rev_before,b,after + | h::tail -> split (h::rev_before) tail + in split [] struc let discr_resolver mtb = match mtb.typ_expr with | SEBstruct _ -> mtb.typ_delta @@ -50,184 +53,170 @@ let discr_resolver mtb = match mtb.typ_expr with let rec rebuild_mp mp l = match l with - []-> mp - | i::r -> rebuild_mp (MPdot(mp,i)) r - -let rec check_with env sign with_decl alg_sign mp equiv = - let sign,wd,equiv,cst= match with_decl with - | 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 - match alg_sign with - | None -> - sign, None, equiv, cst - | Some s -> - sign,Some (SEBwith(s, wd)),equiv,cst + | []-> mp + | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r + +let (+++) = Univ.union_constraints -and check_with_def env sign (idl,c) mp equiv = - let sig_b = match sign with +let rec 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 idl with + let lab,idl = match idl with | [] -> assert false - | id::idl -> id,idl + | id::idl -> Label.of_id id, idl in - let l = Label.of_id id in - try - let not_empty = match idl with [] -> false | _ :: _ -> true in - let rev_before,spec,after = list_split_assoc (l, not_empty) [] sig_b in - let before = List.rev rev_before in - let env' = Modops.add_signature mp before equiv env in - match idl with [] -> - (* Toplevel definition *) - let cb = match spec with - | SFBconst cb -> cb - | _ -> error_not_a_constant l - in - (* In the spirit of subtyping.check_constant, we accept - any implementations of parameters and opaques terms, - as long as they have the right type *) - let def,cst = match cb.const_body with - | Undef _ | OpaqueDef _ -> - let (j,cst1) = Typeops.infer env' c in - let typ = Typeops.type_of_constant_type env' cb.const_type in - let cst2 = Reduction.conv_leq env' j.uj_type typ in - let cst = union_constraints - (union_constraints - (Future.force cb.const_constraints) cst1) - cst2 - in - let def = Def (Lazyconstr.from_val j.uj_val) in - def,cst - | Def cs -> - let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in - let cst = union_constraints - (Future.force cb.const_constraints) cst1 in - let def = Def (Lazyconstr.from_val c) in - def,cst - in - let cb' = - { cb with - const_body = def; - const_body_code = - Cemitcodes.from_val (compile_constant_body env' def); - const_constraints = Future.from_val cst } - in - SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst - | _ -> - (* Definition inside a sub-module *) - let old = match spec with - | SFBmodule msb -> msb - | _ -> error_not_a_module (Label.to_string l) - in - begin - match old.mod_expr with - | None -> - let sign,cb,cst = - 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 - | Some msb -> - error_generative_module_expected l - end - with - | Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_incorrect_with_constraint l - -and check_with_mod env sign (idl,mp1) mp equiv = - let sig_b = match sign with - | SEBstruct(sig_b) ->sig_b + try + let modular = not (List.is_empty idl) in + let before,spec,after = split_sign lab modular sig_b in + let env' = Modops.add_signature mp before equiv env in + if List.is_empty idl then + (* Toplevel definition *) + let cb = match spec with + | SFBconst cb -> cb + | _ -> error_not_a_constant lab + in + (* In the spirit of subtyping.check_constant, we accept + any implementations of parameters and opaques terms, + as long as they have the right type *) + let def,cst = match cb.const_body with + | Undef _ | OpaqueDef _ -> + let j,cst1 = Typeops.infer env' c in + let typ = Typeops.type_of_constant_type env' cb.const_type in + let cst2 = Reduction.conv_leq env' j.uj_type typ in + let cst = Future.force cb.const_constraints +++ cst1 +++ cst2 in + let def = Def (Lazyconstr.from_val j.uj_val) in + def,cst + | Def cs -> + let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in + let cst = Future.force cb.const_constraints +++ cst1 in + let def = Def (Lazyconstr.from_val c) in + def,cst + in + let cb' = + { cb with + const_body = def; + const_body_code = Cemitcodes.from_val (compile_constant_body env' def); + const_constraints = Future.from_val cst } + in + SEBstruct(before@(lab,SFBconst(cb'))::after),cb',cst + else + (* Definition inside a sub-module *) + let mb = match spec with + | SFBmodule mb -> mb + | _ -> error_not_a_module (Label.to_string lab) + in + begin match mb.mod_expr with + | Some _ -> error_generative_module_expected lab + | None -> + let sign,cb,cst = + check_with_def env' mb.mod_type (idl,c) (MPdot(mp,lab)) mb.mod_delta + in + let mb' = { mb with + mod_type = sign; + mod_type_alg = None } + in + SEBstruct(before@(lab,SFBmodule mb')::after),cb,cst + end + with + | Not_found -> error_no_such_label lab + | Reduction.NotConvertible -> error_incorrect_with_constraint lab + +let rec 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 idl with + let lab,idl = match idl with | [] -> assert false - | id::idl -> id,idl + | id::idl -> Label.of_id id, idl in - let l = Label.of_id id in - try - let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in - let before = List.rev rev_before in - let env' = Modops.add_signature mp before equiv env in - match idl with [] -> - (* Toplevel module definition *) - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module (Label.to_string l) - in - let mb_mp1 = (lookup_module mp1 env) in - let mtb_mp1 = - module_type_of_module None mb_mp1 in - let cst = - match old.mod_expr with - None -> - begin - try union_constraints - (check_subtypes env' mtb_mp1 - (module_type_of_module None old)) - old.mod_constraints - with Failure _ -> error_incorrect_with_constraint (Label.of_id id) - end - | Some (SEBident(mp')) -> - check_modpath_equiv env' mp1 mp'; - old.mod_constraints - | _ -> error_generative_module_expected l - in - let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false - in - let new_spec = SFBmodule {new_mb with - mod_mp = MPdot(mp,l); - mod_expr = Some (SEBident mp1); - mod_constraints = cst} in - (* we propagate the new equality in the rest of the signature - with the identity substitution accompagned by the new resolver*) - 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 - | _ -> - (* Module definition of a sub-module *) - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module (Label.to_string l) - in - begin - match old.mod_expr with - None -> - let sign,equiv',cst = - 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; - mod_type_alg = None; - mod_delta = equiv'} - in - let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) equiv' in - SEBstruct(before@(l,new_spec)::subst_signature id_subst after), - new_equiv,cst - | Some (SEBident(mp')) -> - let mpnew = rebuild_mp mp' (List.map Label.of_id idl) in - check_modpath_equiv env' mpnew mp; - SEBstruct(before@(l,spec)::after) - ,equiv,empty_constraint - | _ -> - error_generative_module_expected l - end - with - Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_incorrect_with_constraint l - -and translate_module env mp inl me = + try + let before,spec,after = split_sign lab true sig_b in + let env' = Modops.add_signature mp before equiv env in + let old = match spec with + | SFBmodule mb -> mb + | _ -> error_not_a_module (Label.to_string lab) + in + if List.is_empty idl then + (* Toplevel module definition *) + let mb_mp1 = lookup_module mp1 env in + let mtb_mp1 = module_type_of_module None mb_mp1 in + let cst = match old.mod_expr with + | None -> + begin + try + let mtb_old = module_type_of_module None old in + Subtyping.check_subtypes env' mtb_mp1 mtb_old + +++ old.mod_constraints + with Failure _ -> error_incorrect_with_constraint lab + end + | Some (SEBident(mp')) -> + check_modpath_equiv env' mp1 mp'; + old.mod_constraints + | _ -> error_generative_module_expected lab + in + let mp' = MPdot (mp,lab) in + let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in + let new_mb' = {new_mb with + mod_mp = mp'; + mod_expr = Some (SEBident mp1); + mod_constraints = cst } + in + (* we propagate the new equality in the rest of the signature + with the identity substitution accompagned by the new resolver*) + let id_subst = map_mp mp' mp' new_mb.mod_delta in + SEBstruct(before@(lab,SFBmodule new_mb')::subst_signature id_subst after), + add_delta_resolver equiv new_mb.mod_delta,cst + else + (* Module definition of a sub-module *) + let mp' = MPdot (mp,lab) in + let old = match spec with + | SFBmodule msb -> msb + | _ -> error_not_a_module (Label.to_string lab) + in + begin match old.mod_expr with + | None -> + let sign,equiv',cst = + check_with_mod env' old.mod_type (idl,mp1) mp' old.mod_delta in + let new_equiv = add_delta_resolver equiv equiv' in + let new_mb = { old with + mod_type = sign; + mod_type_alg = None; + mod_delta = equiv'} + in + let id_subst = map_mp mp' mp' equiv' in + SEBstruct(before@(lab,SFBmodule new_mb)::subst_signature id_subst after), + new_equiv,cst + | Some (SEBident mp0) -> + let mpnew = rebuild_mp mp0 idl in + check_modpath_equiv env' mpnew mp; + SEBstruct(before@(lab,spec)::after),equiv,Univ.empty_constraint + | _ -> error_generative_module_expected lab + end + with + | Not_found -> error_no_such_label lab + | Reduction.NotConvertible -> error_incorrect_with_constraint lab + +let check_with env sign with_decl alg_sign mp equiv = + let sign,wd,equiv,cst= match with_decl with + | 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 + match alg_sign with + | None -> sign, None, equiv, cst + | Some s -> sign, Some (SEBwith(s, wd)), equiv, cst + +let rec translate_module env mp inl me = match me.mod_entry_expr, me.mod_entry_type with | None, None -> - anomaly ~label:"Mod_typing.translate_module" (Pp.str "empty type and expr in module entry") + Errors.anomaly ~label:"Mod_typing.translate_module" + (Pp.str "empty type and expr in module entry") | None, Some mte -> let mtb = translate_module_type env mp inl mte in { mod_mp = mp; @@ -243,14 +232,14 @@ and translate_module env mp inl me = let sign,alg1,resolver,cst2 = match me.mod_entry_type with | None -> - sign,None,resolver,empty_constraint + sign,None,resolver,Univ.empty_constraint | Some mte -> let mtb = translate_module_type env mp inl mte in - let cst = check_subtypes env + let cst = Subtyping.check_subtypes env {typ_mp = mp; typ_expr = sign; typ_expr_alg = None; - typ_constraints = empty_constraint; + typ_constraints = Univ.empty_constraint; typ_delta = resolver;} mtb in @@ -260,7 +249,7 @@ and translate_module env mp inl me = mod_type = sign; mod_expr = alg_implem; mod_type_alg = alg1; - mod_constraints = Univ.union_constraints cst1 cst2; + mod_constraints = cst1 +++ cst2; mod_delta = resolver; mod_retroknowledge = []} (* spiwack: not so sure about that. It may @@ -276,15 +265,14 @@ and translate_apply env inl ftrans mexpr mkalg = with Not_path -> error_application_to_not_path mexpr in let mtb = module_type_of_module None (lookup_module mp1 env) in - let cst2 = check_subtypes env mtb farg_b in + let cst2 = Subtyping.check_subtypes env mtb farg_b in let mp_delta = discr_resolver mtb in let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in - let subst = map_mbid farg_id mp1 mp_delta - in + let subst = map_mbid farg_id mp1 mp_delta in subst_struct_expr subst fbody_b, mkalg alg mp1 cst2, subst_codom_delta_resolver subst resolver, - Univ.union_constraints cst1 cst2 + cst1 +++ cst2 and translate_functor env inl arg_id arg_e trans mkalg = let mtb = translate_module_type env (MPbound arg_id) inl arg_e in @@ -294,7 +282,7 @@ and translate_functor env inl arg_id arg_e trans mkalg = SEBfunctor (arg_id, mtb, sign), mkalg alg arg_id mtb, resolver, - Univ.union_constraints cst mtb.typ_constraints + cst +++ mtb.typ_constraints and translate_struct_module_entry env mp inl = function | MSEident mp1 -> @@ -314,7 +302,7 @@ and translate_struct_module_entry env mp inl = function translate_struct_module_entry env mp inl mte in let sign,alg,resolve,cst2 = check_with env sign with_decl alg mp resolve in - sign,alg,resolve,Univ.union_constraints cst1 cst2 + sign,alg,resolve, cst1 +++ cst2 and translate_struct_type_entry env inl = function | MSEident mp1 -> @@ -331,7 +319,7 @@ and translate_struct_type_entry env inl = function let sign,alg,resolve,cst2 = check_with env sign with_decl alg (mp_from_mexpr mte) resolve in - sign,alg,resolve,Univ.union_constraints cst1 cst2 + sign,alg,resolve, cst1 +++ cst2 and translate_module_type env mp inl mte = let mp_from = mp_from_mexpr mte in @@ -415,16 +403,14 @@ let rec struct_expr_constraints cst = function structure_body | SEBapply (meb1,meb2,cst1) -> - struct_expr_constraints - (struct_expr_constraints (Univ.union_constraints cst1 cst) meb1) - meb2 + struct_expr_constraints (struct_expr_constraints (cst1 +++ cst) meb1) + meb2 | SEBwith(meb,With_definition_body(_,cb))-> - struct_expr_constraints - (Univ.union_constraints (Future.force cb.const_constraints) cst) meb + struct_expr_constraints ((Future.force cb.const_constraints) +++ cst) meb | SEBwith(meb,With_module_body(_,_))-> - struct_expr_constraints cst meb - -and struct_elem_constraints cst = function + struct_expr_constraints cst meb + +and struct_elem_constraints cst = function | SFBconst cb -> cst | SFBmind mib -> cst | SFBmodule mb -> module_constraints cst mb @@ -434,12 +420,11 @@ and module_constraints cst mb = let cst = match mb.mod_expr with | None -> cst | Some meb -> struct_expr_constraints cst meb in - let cst = - struct_expr_constraints cst mb.mod_type in - Univ.union_constraints mb.mod_constraints cst + let cst = struct_expr_constraints cst mb.mod_type in + mb.mod_constraints +++ cst and modtype_constraints cst mtb = - struct_expr_constraints (Univ.union_constraints mtb.typ_constraints cst) mtb.typ_expr + struct_expr_constraints (mtb.typ_constraints +++ cst) mtb.typ_expr let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint -- cgit v1.2.3