diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-01 12:18:37 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-01 12:18:37 +0000 |
| commit | 7acb63cad5f92c2618f99ca2a812a465092a523f (patch) | |
| tree | b673bec4833d608f314c132ff85a0ffc5eab1e0f | |
| parent | 9b913feb3532c15aad771f914627a7a82743e625 (diff) | |
Beaoucoup de changements dans la representation interne des modules.
kernel:
-declaration.ml
unification des representations pour les modules et modules types.
(type struct_expr_body)
-mod_typing.ml
le typage des modules est separe de l'evaluation des modules
-modops.ml
nouvelle fonction qui pour toutes expressions de structure calcule
sa forme evaluee.(eval_struct)
-safe_typing.ml
ajout du support du nouvel operateur Include.(add_include).
library:
-declaremods.ml
nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
les alias via la nametab.
parsing:
-g_vernac.ml4:
nouvelles regles pour le support des Includes et pour l'application des signatures
fonctorielles.
extraction:
Adaptation a la nouvelle representation des modules et support de l'operateur with.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
46 files changed, 1410 insertions, 849 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 855990d25..7a6d42428 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -289,6 +289,7 @@ let modfstlev_rename l = else (add_modfstlev id []; s) + (*s Creating renaming for a [module_path] *) let rec mp_create_renaming mp = @@ -358,14 +359,14 @@ let create_modular_renamings struc = (* 3) determines the potential clashes *) let needs_qualify k r = let mp = modpath_of_r r in - if (is_modfile mp) && mp <> current_module && - (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules) - then add_static_clash r + if (is_modfile mp) && mp <> current_module && + (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules) + then add_static_clash r in - Refset.iter (needs_qualify Type) ty; - Refset.iter (needs_qualify Term) tr; - Refset.iter (needs_qualify Cons) co; - List.rev opened_modules + Refset.iter (needs_qualify Type) ty; + Refset.iter (needs_qualify Term) tr; + Refset.iter (needs_qualify Cons) co; + List.rev opened_modules (*s Initial renamings creation, for monolithic extraction. *) @@ -479,3 +480,16 @@ let pp_module mp = error_module_clash base_s else dottify ls + +(*i + (* DO NOT REMOVE: used when making names resolution *) + let cout = open_out (f^".ren") in + let ft = Pp_control.with_output_to cout in + Hashtbl.iter + (fun r id -> + if short_module r = !current_module then + msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r))) + renamings; + pp_flush_with ft (); + close_out cout; +i*) diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 2aca56f9b..701b71a4a 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -31,16 +31,17 @@ let toplevel_env () = | (_,kn), Lib.Leaf o -> let mp,_,l = repr_kn kn in let seb = match Libobject.object_tag o with - | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn)) - | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn) - | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l))) - | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn) + | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn)) + | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn) + | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l))) + | "MODULE TYPE" -> + SFBmodtype (fst (Global.lookup_modtype (MPdot (mp,l)))) | _ -> failwith "caught" in l,seb | _ -> failwith "caught" in match current_toplevel () with - | MPself msid -> MEBstruct (msid, List.rev (map_succeed get_reference seg)) + | MPself msid -> SEBstruct (msid, List.rev (map_succeed get_reference seg)) | _ -> assert false let environment_until dir_opt = @@ -132,7 +133,7 @@ let factor_fix env l cb msb = list_iter_i (fun j -> function - | (l,SEBconst cb') -> + | (l,SFBconst cb') -> if check <> check_fix env cb' (j+1) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; @@ -141,7 +142,7 @@ let factor_fix env l cb msb = let rec extract_msig env mp = function | [] -> [] - | (l,SPBconst cb) :: msig -> + | (l,SFBconst cb) :: msig -> let kn = make_con mp empty_dirpath l in let s = extract_constant_spec env kn cb in if logical_spec s then extract_msig env mp msig @@ -149,7 +150,7 @@ let rec extract_msig env mp = function Visit.add_spec_deps s; (l,Spec s) :: (extract_msig env mp msig) end - | (l,SPBmind cb) :: msig -> + | (l,SFBmind cb) :: msig -> let kn = make_kn mp empty_dirpath l in let s = Sind (kn, extract_inductive env kn) in if logical_spec s then extract_msig env mp msig @@ -157,26 +158,42 @@ let rec extract_msig env mp = function Visit.add_spec_deps s; (l,Spec s) :: (extract_msig env mp msig) end - | (l,SPBmodule {msb_modtype=mtb}) :: msig -> - (l,Smodule (extract_mtb env mtb)) :: (extract_msig env mp msig) - | (l,SPBmodtype mtb) :: msig -> + | (l,SFBmodule mb) :: msig -> + (l,Smodule (extract_mtb env (Modops.type_of_mb env mb))) :: + (extract_msig env mp msig) + | (l,SFBmodtype mtb) :: msig -> (l,Smodtype (extract_mtb env mtb)) :: (extract_msig env mp msig) -and extract_mtb env = function - | MTBident kn -> Visit.add_kn kn; MTident kn - | MTBfunsig (mbid, mtb, mtb') -> + +and extract_mtb env = function + | SEBident kn -> Visit.add_mp kn; MTident kn + | SEBwith(mtb',With_definition_body(idl,cb))-> + begin + let mtb''= extract_mtb env mtb' in + match extract_with_type env cb with (* cb peut contenir des kn *) + None -> mtb'' + | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ)) + end + | SEBwith(mtb',With_module_body(idl,mp,_))-> + Visit.add_mp mp; + MTwith(extract_mtb env mtb',ML_With_module(idl,mp)) + | SEBfunctor (mbid, mtb, mtb') -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MTfunsig (mbid, extract_mtb env mtb, - extract_mtb env' mtb') - | MTBsig (msid, msig) -> + MTfunsig (mbid, extract_mtb env mtb, + extract_mtb env' mtb') + | SEBstruct (msid, msig) -> let mp = MPself msid in let env' = Modops.add_signature mp msig env in - MTsig (msid, extract_msig env' mp msig) + MTsig (msid, extract_msig env' mp msig) + | mtb -> + let mtb' = Modops.eval_struct env mtb in + extract_mtb env mtb' + let rec extract_msb env mp all = function | [] -> [] - | (l,SEBconst cb) :: msb -> + | (l,SFBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in let vc = Array.map (make_con mp empty_dirpath) vl in @@ -196,7 +213,7 @@ let rec extract_msb env mp all = function if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) - | (l,SEBmind mib) :: msb -> + | (l,SFBmind mib) :: msb -> let ms = extract_msb env mp all msb in let kn = make_kn mp empty_dirpath l in let b = Visit.needed_kn kn in @@ -205,50 +222,52 @@ let rec extract_msb env mp all = function if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms - | (l,SEBmodule mb) :: msb -> + | (l,SFBmodule mb) :: msb -> let ms = extract_msb env mp all msb in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then (l,SEmodule (extract_module env mp true mb)) :: ms else ms - | (l,SEBmodtype mtb) :: msb -> + | (l,SFBmodtype mtb) :: msb -> let ms = extract_msb env mp all msb in - let kn = make_kn mp empty_dirpath l in - if all || Visit.needed_kn kn then + let mp = MPdot (mp,l) in + if all || Visit.needed_mp mp then (l,SEmodtype (extract_mtb env mtb)) :: ms else ms and extract_meb env mpo all = function - | MEBident mp -> + | SEBident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; Visit.add_mp mp; MEident mp - | MEBapply (meb, meb',_) -> + | SEBapply (meb, meb',_) -> MEapply (extract_meb env None true meb, extract_meb env None true meb') - | MEBfunctor (mbid, mtb, meb) -> + | SEBfunctor (mbid, mtb, meb) -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in MEfunctor (mbid, extract_mtb env mtb, extract_meb env' None true meb) - | MEBstruct (msid, msb) -> + | SEBstruct (msid, msb) -> let mp,msb = match mpo with | None -> MPself msid, msb | Some mp -> mp, subst_msb (map_msid msid mp) msb in let env' = add_structure mp msb env in MEstruct (msid, extract_msb env' mp all msb) + | SEBwith (_,_) -> anomaly "Not avaible yet" and extract_module env mp all mb = (* [mb.mod_expr <> None ], since we look at modules from outside. *) (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) let meb = Option.get mb.mod_expr in - let mtb = match mb.mod_user_type with None -> mb.mod_type | Some mt -> mt in + let mtb = match mb.mod_type with None -> (Modops.type_of_mb env mb) | Some mt -> mt in (* Because of the "with" construct, the module type can be [MTBsig] with *) (* a msid different from the one of the module. Here is the patch. *) - let mtb = replicate_msid meb mtb in + let mtb = replicate_msid meb mtb in { ml_mod_expr = extract_meb env (Some mp) all meb; ml_mod_type = extract_mtb env mtb } + let unpack = function MEstruct (_,sel) -> sel | _ -> assert false let mono_environment refs mpl = @@ -446,8 +465,3 @@ let extraction_library is_rec m = in print struc; reset () - - - - - diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 27687ae1c..b7be86bff 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -876,6 +876,20 @@ let extract_constant_spec env kn cb = let t = snd (record_constant_type env kn (Some typ)) in Sval (r, type_expunge env t) +let extract_with_type env cb = + let typ = Typeops.type_of_constant_type env cb.const_type in + match flag_of_type env typ with + | (_ , Default) -> None + | (Logic, TypeScheme) ->Some ([],Tdummy Ktype) + | (Info, TypeScheme) -> + let s,vl = type_sign_vl env typ in + (match cb.const_body with + | None -> assert false + | Some body -> + let db = db_from_sign s in + let t = extract_type_scheme env db (force body) (List.length s) + in Some ( vl, t) ) + let extract_inductive env kn = let ind = extract_ind env kn in add_recursors env kn; @@ -903,9 +917,3 @@ let logical_spec = function | Sval (_,Tdummy _) -> true | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false - - - - - - diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index cb0600d05..343d2b69a 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -21,6 +21,8 @@ val extract_constant : env -> constant -> constant_body -> ml_decl val extract_constant_spec : env -> constant -> constant_body -> ml_spec +val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option + val extract_fixpoint : env -> constant array -> (constr, types) prec_declaration -> ml_decl diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index ef963cc90..3add72d8b 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -126,9 +126,14 @@ type ml_specif = | Smodtype of ml_module_type and ml_module_type = - | MTident of kernel_name + | MTident of module_path | MTfunsig of mod_bound_id * ml_module_type * ml_module_type | MTsig of mod_self_id * ml_module_sig + | MTwith of ml_module_type * ml_with_declaration + +and ml_with_declaration = + | ML_With_type of identifier list * identifier list * ml_type + | ML_With_module of identifier list * module_path and ml_module_sig = (label * ml_specif) list diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 79ba0ebc5..5c3f84822 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -28,49 +28,52 @@ let add_structure mp msb env = let kn = make_kn mp empty_dirpath l in let con = make_con mp empty_dirpath l in match elem with - | SEBconst cb -> Environ.add_constant con cb env - | SEBmind mib -> Environ.add_mind kn mib env - | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env - | SEBmodtype mtb -> Environ.add_modtype kn mtb env + | SFBconst cb -> Environ.add_constant con cb env + | SFBmind mib -> Environ.add_mind kn mib env + | SFBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env + | SFBmodtype mtb -> Environ.add_modtype (MPdot (mp,l)) (mtb,None) env in List.fold_left add_one env msb (*s Apply a module path substitution on a module. Build on the [Modops.subst_modtype] model. *) let rec subst_module sub mb = - let mtb' = Modops.subst_modtype sub mb.mod_type + let mtb' = Option.smartmap (Modops.subst_modtype sub) mb.mod_type and meb' = Option.smartmap (subst_meb sub) mb.mod_expr - and mtb'' = Option.smartmap (Modops.subst_modtype sub) mb.mod_user_type and mpo' = Option.smartmap (subst_mp sub) mb.mod_equiv in - if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && - (mtb''==mb.mod_user_type) && (mpo'==mb.mod_equiv) + if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && (mpo'==mb.mod_equiv) then mb else { mod_expr= meb'; mod_type=mtb'; - mod_user_type=mtb''; mod_equiv=mpo'; mod_constraints=mb.mod_constraints; mod_retroknowledge=[] } (* spiwack: since I'm lazy and it's unused at this point. I forget about retroknowledge, - this may need a change later *) + this may need a change later *) and subst_meb sub = function - | MEBident mp -> MEBident (subst_mp sub mp) - | MEBfunctor (mbid, mtb, meb) -> + | SEBident mp -> SEBident (subst_mp sub mp) + | SEBfunctor (mbid, mtb, meb) -> assert (not (occur_mbid mbid sub)); - MEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb) - | MEBstruct (msid, msb) -> + SEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb) + | SEBstruct (msid, msb) -> assert (not (occur_msid msid sub)); - MEBstruct (msid, subst_msb sub msb) - | MEBapply (meb, meb', c) -> - MEBapply (subst_meb sub meb, subst_meb sub meb', c) + SEBstruct (msid, subst_msb sub msb) + | SEBapply (meb, meb', c) -> + SEBapply (subst_meb sub meb, subst_meb sub meb', c) + | SEBwith (meb,With_module_body(id,mp,cst))-> + SEBwith(subst_meb sub meb, + With_module_body(id,Mod_subst.subst_mp sub mp,cst)) + | SEBwith (meb,With_definition_body(id,cb))-> + SEBwith(subst_meb sub meb, + With_definition_body(id,Declarations.subst_const_body sub cb)) and subst_msb sub msb = let subst_body = function - | SEBconst cb -> SEBconst (subst_const_body sub cb) - | SEBmind mib -> SEBmind (subst_mind sub mib) - | SEBmodule mb -> SEBmodule (subst_module sub mb) - | SEBmodtype mtb -> SEBmodtype (Modops.subst_modtype sub mtb) + | SFBconst cb -> SFBconst (subst_const_body sub cb) + | SFBmind mib -> SFBmind (subst_mind sub mib) + | SFBmodule mb -> SFBmodule (subst_module sub mb) + | SFBmodtype mtb -> SFBmodtype (Modops.subst_modtype sub mtb) in List.map (fun (l,b) -> (l,subst_body b)) msb (*s Change a msid in a module type, to follow a module expr. @@ -78,16 +81,29 @@ and subst_msb sub msb = [MTBsig] with a msid different from the one of the module. *) let rec replicate_msid meb mtb = match meb,mtb with - | MEBfunctor (_, _, meb), MTBfunsig (mbid, mtb1, mtb2) -> + | SEBfunctor (_, _, meb), SEBfunctor (mbid, mtb1, mtb2) -> let mtb' = replicate_msid meb mtb2 in - if mtb' == mtb2 then mtb else MTBfunsig (mbid, mtb1, mtb') - | MEBstruct (msid, _), MTBsig (msid1, msig) when msid <> msid1 -> + if mtb' == mtb2 then mtb else SEBfunctor (mbid, mtb1, mtb') + | SEBstruct (msid, _), SEBstruct (msid1, msig) when msid <> msid1 -> let msig' = Modops.subst_signature_msid msid1 (MPself msid) msig in - if msig' == msig then MTBsig (msid, msig) else MTBsig (msid, msig') + if msig' == msig then SEBstruct (msid, msig) else SEBstruct (msid, msig') | _ -> mtb (*S Functions upon ML modules. *) - +let rec msid_of_mt = function + | MTident mp -> begin + match Modops.eval_struct (Global.env()) (SEBident mp) with + | SEBstruct(msid,_) -> MPself msid + | _ -> anomaly "Extraction:the With can'tbe applied to a funsig" + end + | MTwith(mt,_)-> msid_of_mt mt + | _ -> anomaly "Extraction:the With operator isn't applied to a name" + +let make_mp_with mp idl = + let idl_rev = List.rev idl in + let idl' = List.rev (List.tl idl_rev) in + (List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) + mp idl') (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -95,6 +111,16 @@ let struct_iter do_decl do_spec s = let rec mt_iter = function | MTident _ -> () | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' + | MTwith (mt,ML_With_type(idl,l,t))-> + let mp_mt = msid_of_mt mt in + let mp = make_mp_with mp_mt idl in + let gr = ConstRef ( + (make_con mp empty_dirpath + (label_of_id ( + List.hd (List.rev idl))))) in + mt_iter mt;do_decl + (Dtype(gr,l,t)) + | MTwith (mt,_)->mt_iter mt | MTsig (_, sign) -> List.iter spec_iter sign and spec_iter = function | (_,Spec s) -> do_spec s diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index c89590daa..8d0f3e923 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -20,18 +20,18 @@ open Mod_subst (* Add _all_ direct subobjects of a module, not only those exported. Build on the [Modops.add_signature] model. *) -val add_structure : module_path -> module_structure_body -> env -> env +val add_structure : module_path -> structure_body -> env -> env (* Apply a module path substitution on a module. Build on the [Modops.subst_modtype] model. *) val subst_module : substitution -> module_body -> module_body -val subst_meb : substitution -> module_expr_body -> module_expr_body -val subst_msb : substitution -> module_structure_body -> module_structure_body +val subst_meb : substitution -> struct_expr_body -> struct_expr_body +val subst_msb : substitution -> structure_body -> structure_body (* Change a msid in a module type, to follow a module expr. *) -val replicate_msid : module_expr_body -> module_type_body -> module_type_body +val replicate_msid : struct_expr_body -> struct_expr_body -> struct_expr_body (*s Functions upon ML modules. *) diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 1ed82090a..16859a9c1 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -20,6 +20,26 @@ open Miniml open Mlutil open Modutil open Common +open Declarations + + +(*s Some utility functions. *) + +let rec msid_of_mt = function + | MTident mp -> begin + match Modops.eval_struct (Global.env()) (SEBident mp) with + | SEBstruct(msid,_) -> MPself msid + | _ -> anomaly "Extraction:the With can'tbe applied to a funsig" + end + | MTwith(mt,_)-> msid_of_mt mt + | _ -> anomaly "Extraction:the With operator isn't applied to a name" + +let make_mp_with mp idl = + let idl_rev = List.rev idl in + let idl' = List.rev (List.tl idl_rev) in + (List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) + mp idl') + let pp_tvar id = let s = string_of_id id in @@ -585,7 +605,7 @@ let rec pp_specif = function and pp_module_type ol = function | MTident kn -> - let mp,_,l = repr_kn kn in pp_modname (MPdot (mp,l)) + pp_modname kn | MTfunsig (mbid, mt, mt') -> let name = pp_modname (MPbound mbid) in let typ = pp_module_type None mt in @@ -600,10 +620,41 @@ and pp_module_type ol = function pop_visible (); str "sig " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ - fnl () ++ str "end" - + fnl () ++ str "end" + | MTwith(mt,ML_With_type(idl,vl,typ)) -> + let l = rename_tvars keywords vl in + let ids = pp_parameters l in + let mp_mt = msid_of_mt mt in + let mp = make_mp_with mp_mt idl in + let gr = ConstRef ( + (make_con mp empty_dirpath + (label_of_id ( + List.hd (List.rev idl))))) in + push_visible mp_mt; + let s = pp_module_type None mt ++ + str " with type " ++ + pp_global Type gr ++ + ids in + pop_visible(); + s ++ str "=" ++ spc () ++ + pp_type false vl typ + | MTwith(mt,ML_With_module(idl,mp)) -> + let mp_mt=msid_of_mt mt in + push_visible mp_mt; + let s = + pp_module_type None mt ++ + str " with module " ++ + (pp_modname + (List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) + mp_mt idl)) + ++ str " = " + in + pop_visible (); + s ++ (pp_modname mp) + + let is_short = function MEident _ | MEapply _ -> true | _ -> false - + let rec pp_structure_elem = function | (l,SEdecl d) -> (try diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c261d57e9..0fbfa39b7 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1574,7 +1574,9 @@ let rec xlate_module_type = function | CWith_Module((_, idl), (_, qid)) -> CT_module_type_with_mod(mty1, CT_id_list (List.map xlate_ident idl), - CT_ident (xlate_qualid qid)));; + CT_ident (xlate_qualid qid))) + | CMTEapply (_,_) -> xlate_error "TODO: Funsig application";; + let xlate_module_binder_list (l:module_binder list) = CT_module_binder_list @@ -1967,7 +1969,8 @@ let rec xlate_vernac = | VernacSyntacticDefinition (id, c, true, _) -> xlate_error "TODO: Local abbreviations" (* Modules and Module Types *) - | VernacDeclareModuleType((_, id), bl, mty_o) -> + | VernacInclude (_) -> xlate_error "TODO : Include " + | VernacDeclareModuleType((_, id), bl, mty_o) -> CT_module_type_decl(xlate_ident id, xlate_module_binder_list bl, match mty_o with diff --git a/interp/modintern.ml b/interp/modintern.ml index f077bea93..68978080b 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -64,7 +64,6 @@ let lookup_qualid (modtype:bool) qid = If found, returns the module_path/kernel_name created from the dirpath and the basename. Searches Nametab otherwise. *) - let lookup_module (loc,qid) = try Nametab.locate_module qid @@ -84,20 +83,23 @@ let transl_with_decl env = function | CWith_Definition ((_,fqid),c) -> With_Definition (fqid,interp_constr Evd.empty env c) -let rec interp_modtype env = function - | CMTEident qid -> - MTEident (lookup_modtype qid) - | CMTEwith (mty,decl) -> - let mty = interp_modtype env mty in - let decl = transl_with_decl env decl in - MTEwith(mty,decl) - - let rec interp_modexpr env = function | CMEident qid -> - MEident (lookup_module qid) + MSEident (lookup_module qid) | CMEapply (me1,me2) -> let me1 = interp_modexpr env me1 in let me2 = interp_modexpr env me2 in - MEapply(me1,me2) + MSEapply(me1,me2) + +let rec interp_modtype env = function + | CMTEident qid -> + MSEident (lookup_modtype qid) + | CMTEapply (mty1,me) -> + let mty' = interp_modtype env mty1 in + let me' = interp_modexpr env me in + MSEapply(mty',me') + | CMTEwith (mty,decl) -> + let mty = interp_modtype env mty in + let decl = transl_with_decl env decl in + MSEwith(mty,decl) diff --git a/interp/modintern.mli b/interp/modintern.mli index a8676c793..1f27e3c18 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -12,13 +12,17 @@ open Declarations open Environ open Entries +open Util +open Libnames +open Names open Topconstr (*i*) (* Module expressions and module types are interpreted relatively to eventual functor or funsig arguments. *) -val interp_modtype : env -> module_type_ast -> module_type_entry +val interp_modtype : env -> module_type_ast -> module_struct_entry -val interp_modexpr : env -> module_ast -> module_expr +val interp_modexpr : env -> module_ast -> module_struct_entry +val lookup_module : qualid located -> module_path diff --git a/interp/topconstr.ml b/interp/topconstr.ml index accccdeee..c9a33c7eb 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -887,10 +887,16 @@ type with_declaration_ast = | CWith_Module of identifier list located * qualid located | CWith_Definition of identifier list located * constr_expr -type module_type_ast = - | CMTEident of qualid located - | CMTEwith of module_type_ast * with_declaration_ast type module_ast = | CMEident of qualid located | CMEapply of module_ast * module_ast + +type module_type_ast = + | CMTEident of qualid located + | CMTEapply of module_type_ast * module_ast + | CMTEwith of module_type_ast * with_declaration_ast + +type include_ast = + | CIMTE of module_type_ast + | CIME of module_ast diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 6bfbcf07f..26805aa13 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -224,10 +224,17 @@ type with_declaration_ast = | CWith_Module of identifier list located * qualid located | CWith_Definition of identifier list located * constr_expr -type module_type_ast = - | CMTEident of qualid located - | CMTEwith of module_type_ast * with_declaration_ast type module_ast = | CMEident of qualid located | CMEapply of module_ast * module_ast + +type module_type_ast = + | CMTEident of qualid located + | CMTEapply of module_type_ast * module_ast + | CMTEwith of module_type_ast * with_declaration_ast + +type include_ast = + | CIMTE of module_type_ast + | CIME of module_ast + diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 4a5893de8..63c690d48 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -247,44 +247,31 @@ let subst_mind sub mib = (*s Modules: signature component specifications, module types, and module declarations *) -type specification_body = - | SPBconst of constant_body - | SPBmind of mutual_inductive_body - | SPBmodule of module_specification_body - | SPBmodtype of module_type_body - -and module_signature_body = (label * specification_body) list - -and module_type_body = - | MTBident of kernel_name - | MTBfunsig of mod_bound_id * module_type_body * module_type_body - | MTBsig of mod_self_id * module_signature_body - -and module_specification_body = - { msb_modtype : module_type_body; - msb_equiv : module_path option; - msb_constraints : constraints } - -type structure_elem_body = - | SEBconst of constant_body - | SEBmind of mutual_inductive_body - | SEBmodule of module_body - | SEBmodtype of module_type_body - -and module_structure_body = (label * structure_elem_body) list - -and module_expr_body = - | MEBident of module_path - | MEBfunctor of mod_bound_id * module_type_body * module_expr_body - | MEBstruct of mod_self_id * module_structure_body - | MEBapply of module_expr_body * module_expr_body +type structure_field_body = + | SFBconst of constant_body + | SFBmind of mutual_inductive_body + | SFBmodule of module_body + | SFBmodtype of struct_expr_body + +and structure_body = (label * structure_field_body) list + +and struct_expr_body = + | SEBident of module_path + | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body + | SEBstruct of mod_self_id * structure_body + | SEBapply of struct_expr_body * struct_expr_body * constraints + | SEBwith of struct_expr_body * with_declaration_body +and with_declaration_body = + With_module_body of identifier list * module_path * constraints + | With_definition_body of identifier list * constant_body + and module_body = - { mod_expr : module_expr_body option; - mod_user_type : module_type_body option; - mod_type : module_type_body; + { mod_expr : struct_expr_body option; + mod_type : struct_expr_body option; mod_equiv : module_path option; mod_constraints : constraints; mod_retroknowledge : Retroknowledge.action list} +type module_type_body = struct_expr_body * module_path option diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 2f32d8639..544cea246 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -177,51 +177,32 @@ val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body (*s Modules: signature component specifications, module types, and module declarations *) -type specification_body = - | SPBconst of constant_body - | SPBmind of mutual_inductive_body - | SPBmodule of module_specification_body - | SPBmodtype of module_type_body - -and module_signature_body = (label * specification_body) list - -and module_type_body = - | MTBident of kernel_name - | MTBfunsig of mod_bound_id * module_type_body * module_type_body - | MTBsig of mod_self_id * module_signature_body - -and module_specification_body = - { msb_modtype : module_type_body; - msb_equiv : module_path option; - msb_constraints : constraints } - (* [type_of](equiv) <: modtype (if given) - + substyping of past [With_Module] mergers *) - - -type structure_elem_body = - | SEBconst of constant_body - | SEBmind of mutual_inductive_body - | SEBmodule of module_body - | SEBmodtype of module_type_body - -and module_structure_body = (label * structure_elem_body) list - -and module_expr_body = - | MEBident of module_path - | MEBfunctor of mod_bound_id * module_type_body * module_expr_body - | MEBstruct of mod_self_id * module_structure_body - | MEBapply of module_expr_body * module_expr_body (* (F A) *) - * constraints (* [type_of](A) <: [input_type_of](F) *) +type structure_field_body = + | SFBconst of constant_body + | SFBmind of mutual_inductive_body + | SFBmodule of module_body + | SFBmodtype of struct_expr_body + +and structure_body = (label * structure_field_body) list + +and struct_expr_body = + | SEBident of module_path + | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body + | SEBstruct of mod_self_id * structure_body + | SEBapply of struct_expr_body * struct_expr_body + * constraints + | SEBwith of struct_expr_body * with_declaration_body + +and with_declaration_body = + With_module_body of identifier list * module_path * constraints + | With_definition_body of identifier list * constant_body and module_body = - { mod_expr : module_expr_body option; - mod_user_type : module_type_body option; - mod_type : module_type_body; + { mod_expr : struct_expr_body option; + mod_type : struct_expr_body option; mod_equiv : module_path option; mod_constraints : constraints; mod_retroknowledge : Retroknowledge.action list} - (* [type_of(mod_expr)] <: [mod_user_type] (if given) *) - (* if equiv given then constraints are empty *) - +type module_type_body = struct_expr_body * module_path option diff --git a/kernel/entries.ml b/kernel/entries.ml index 17da967c2..89e444a74 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -74,28 +74,22 @@ type specification_entry = SPEconst of constant_entry | SPEmind of mutual_inductive_entry | SPEmodule of module_entry - | SPEmodtype of module_type_entry + | SPEmodtype of module_struct_entry -and module_type_entry = - MTEident of kernel_name - | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry - | MTEwith of module_type_entry * with_declaration - -and module_signature_entry = (label * specification_entry) list +and module_struct_entry = + MSEident of module_path + | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry + | MSEwith of module_struct_entry * with_declaration + | MSEapply of module_struct_entry * module_struct_entry and with_declaration = With_Module of identifier list * module_path | With_Definition of identifier list * constr -and module_expr = - MEident of module_path - | MEfunctor of mod_bound_id * module_type_entry * module_expr - | MEapply of module_expr * module_expr - and module_structure = (label * specification_entry) list - and module_entry = - { mod_entry_type : module_type_entry option; - mod_entry_expr : module_expr option} + { mod_entry_type : module_struct_entry option; + mod_entry_expr : module_struct_entry option} + diff --git a/kernel/entries.mli b/kernel/entries.mli index 56ea852da..b757032f8 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -73,28 +73,22 @@ type specification_entry = SPEconst of constant_entry | SPEmind of mutual_inductive_entry | SPEmodule of module_entry - | SPEmodtype of module_type_entry + | SPEmodtype of module_struct_entry -and module_type_entry = - MTEident of kernel_name - | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry - | MTEwith of module_type_entry * with_declaration - -and module_signature_entry = (label * specification_entry) list +and module_struct_entry = + MSEident of module_path + | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry + | MSEwith of module_struct_entry * with_declaration + | MSEapply of module_struct_entry * module_struct_entry and with_declaration = With_Module of identifier list * module_path | With_Definition of identifier list * constr -and module_expr = - MEident of module_path - | MEfunctor of mod_bound_id * module_type_entry * module_expr - | MEapply of module_expr * module_expr - and module_structure = (label * specification_entry) list - and module_entry = - { mod_entry_type : module_type_entry option; - mod_entry_expr : module_expr option} + { mod_entry_type : module_struct_entry option; + mod_entry_expr : module_struct_entry option} + diff --git a/kernel/environ.ml b/kernel/environ.ml index c2ec6ea7e..b1290452a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -160,7 +160,7 @@ let add_constant kn cs env = (* constant_type gives the type of a constant *) let constant_type env kn = let cb = lookup_constant kn env in - cb.const_type + cb.const_type type const_evaluation_result = NoBody | Opaque @@ -273,7 +273,7 @@ let keep_hyps env needed = (* Modules *) let add_modtype ln mtb env = - let new_modtypes = KNmap.add ln mtb env.env_globals.env_modtypes in + let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in let new_globals = { env.env_globals with env_modtypes = new_modtypes } in @@ -290,7 +290,8 @@ let lookup_module mp env = MPmap.find mp env.env_globals.env_modules let lookup_modtype ln env = - KNmap.find ln env.env_globals.env_modtypes + MPmap.find ln env.env_globals.env_modtypes + (*s Judgments. *) diff --git a/kernel/environ.mli b/kernel/environ.mli index bfbb5dd3c..10e962674 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -146,13 +146,13 @@ val scrape_mind : env -> mutual_inductive -> mutual_inductive (************************************************************************) (*s Modules *) -val add_modtype : kernel_name -> module_type_body -> env -> env +val add_modtype : module_path -> module_type_body -> env -> env (* [shallow_add_module] does not add module components *) val shallow_add_module : module_path -> module_body -> env -> env val lookup_module : module_path -> env -> module_body -val lookup_modtype : kernel_name -> env -> module_type_body +val lookup_modtype : module_path -> env -> module_type_body (************************************************************************) (*s Universe constraints *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 93d01f12a..201835c10 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -22,14 +22,9 @@ open Mod_subst exception Not_path let path_of_mexpr = function - | MEident mb -> mb + | MSEident mb -> mb | _ -> raise Not_path -let rec replace_first p k = function - | [] -> [] - | h::t when p h -> k::t - | h::t -> h::(replace_first p k t) - let rec list_split_assoc k rev_before = function | [] -> raise Not_found | (k',b)::after when k=k' -> rev_before,b,after @@ -42,25 +37,88 @@ let rec list_fold_map2 f e = function let e'',t1',t2' = list_fold_map2 f e' t in e'',h1'::t1',h2'::t2' -let type_modpath env mp = - strengthen env (lookup_module mp env).mod_type mp +let rec check_with env mtb with_decl = + match with_decl with + | With_Definition (id,_) -> + let cb = check_with_aux_def env mtb with_decl in + SEBwith(mtb,With_definition_body(id,cb)) + | With_Module (id,mp) -> + let cst = check_with_aux_mod env mtb with_decl in + SEBwith(mtb,With_module_body(id,mp,cst)) -let rec translate_modtype env mte = - match mte with - | MTEident ln -> MTBident ln - | MTEfunsig (arg_id,arg_e,body_e) -> - let arg_b = translate_modtype env arg_e in - let env' = - add_module (MPbound arg_id) (module_body_of_type arg_b) env in - let body_b = translate_modtype env' body_e in - MTBfunsig (arg_id,arg_b,body_b) - | MTEwith (mte, with_decl) -> - let mtb = translate_modtype env mte in - merge_with env mtb with_decl +and check_with_aux_def env mtb with_decl = + let msid,sig_b = match (eval_struct env mtb) with + | SEBstruct(msid,sig_b) -> + msid,sig_b + | _ -> error_signature_expected mtb + in + let id,idl = match with_decl with + | With_Definition (id::idl,_) | With_Module (id::idl,_) -> id,idl + | With_Definition ([],_) | With_Module ([],_) -> assert false + in + let l = label_of_id id in + try + let rev_before,spec,after = list_split_assoc l [] sig_b in + let before = List.rev rev_before in + let env' = Modops.add_signature (MPself msid) before env in + match with_decl with + | With_Definition ([],_) -> assert false + | With_Definition ([id],c) -> + let cb = match spec with + SFBconst cb -> cb + | _ -> error_not_a_constant l + in + begin + match cb.const_body with + | None -> + 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 = + Constraint.union + (Constraint.union cb.const_constraints cst1) + cst2 in + let body = Some (Declarations.from_val j.uj_val) in + let cb' = {cb with + const_body = body; + const_body_code = Cemitcodes.from_val + (compile_constant_body env' body false false); + const_constraints = cst} in + cb' + | Some b -> + let cst1 = Reduction.conv env' c (Declarations.force b) in + let cst = Constraint.union cb.const_constraints cst1 in + let body = Some (Declarations.from_val c) in + let cb' = {cb with + const_body = body; + const_body_code = Cemitcodes.from_val + (compile_constant_body env' body false false); + const_constraints = cst} in + cb' + end + | With_Definition (_::_,_) -> + let old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module (string_of_label l) + in + begin + match old.mod_equiv with + | None -> + let new_with_decl = match with_decl with + With_Definition (_,c) -> With_Definition (idl,c) + | With_Module (_,c) -> With_Module (idl,c) in + check_with_aux_def env' (type_of_mb env old) new_with_decl + | Some mp -> + error_a_generative_module_expected l + end + | _ -> anomaly "Modtyping:incorrect use of with" + with + Not_found -> error_no_such_label l + | Reduction.NotConvertible -> error_with_incorrect l -and merge_with env mtb with_decl = - let msid,sig_b = match (Modops.scrape_modtype env mtb) with - | MTBsig(msid,sig_b) -> let msid'=(refresh_msid msid) in +and check_with_aux_mod env mtb with_decl = + let msid,sig_b = match (eval_struct env mtb) with + | SEBstruct(msid,sig_b) ->let msid'=(refresh_msid msid) in msid',(subst_signature_msid msid (MPself(msid')) sig_b) | _ -> error_signature_expected mtb in @@ -73,107 +131,58 @@ and merge_with env mtb with_decl = let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in let env' = Modops.add_signature (MPself msid) before env in - let new_spec = match with_decl with - | With_Definition ([],_) - | With_Module ([],_) -> assert false - | With_Definition ([id],c) -> - let cb = match spec with - SPBconst cb -> cb - | _ -> error_not_a_constant l - in - begin - match cb.const_body with - | None -> - 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 = - Constraint.union - (Constraint.union cb.const_constraints cst1) - cst2 in - let body = Some (Declarations.from_val j.uj_val) in - SPBconst {cb with - const_body = body; - const_body_code = Cemitcodes.from_val - (compile_constant_body env' body false false); - const_constraints = cst} - | Some b -> - let cst1 = Reduction.conv env' c (Declarations.force b) in - let cst = Constraint.union cb.const_constraints cst1 in - let body = Some (Declarations.from_val c) in - SPBconst {cb with - const_body = body; - const_body_code = Cemitcodes.from_val - (compile_constant_body env' body false false); - const_constraints = cst} - end -(* and what about msid's ????? Don't they clash ? *) - | With_Module ([id], mp) -> - let old = match spec with - SPBmodule msb -> msb - | _ -> error_not_a_module (string_of_label l) - in - let mtb = type_modpath env' mp in - let cst = - try check_subtypes env' mtb old.msb_modtype + match with_decl with + | With_Module ([],_) -> assert false + | With_Module ([id], mp) -> + let old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module (string_of_label l) + in + let mtb' = eval_struct env' (SEBident mp) in + let cst = + try check_subtypes env' mtb' (type_of_mb env old) with Failure _ -> error_with_incorrect (label_of_id id) in - let equiv = - match old.msb_equiv with + let _ = + match old.mod_equiv with | None -> Some mp | Some mp' -> check_modpath_equiv env' mp mp'; Some mp - in - let msb = - {msb_modtype = mtb; - msb_equiv = equiv; - msb_constraints = Constraint.union old.msb_constraints cst } - in - SPBmodule msb - | With_Definition (_::_,_) + in + cst | With_Module (_::_,_) -> let old = match spec with - SPBmodule msb -> msb + SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) in begin - match old.msb_equiv with - None -> - let new_with_decl = match with_decl with - With_Definition (_,c) -> With_Definition (idl,c) - | With_Module (_,c) -> With_Module (idl,c) in - let modtype = - merge_with env' old.msb_modtype new_with_decl in - let msb = - {msb_modtype = modtype; - msb_equiv = None; - msb_constraints = old.msb_constraints } - in - SPBmodule msb - | Some mp -> - error_a_generative_module_expected l + match old.mod_equiv with + None -> + let new_with_decl = match with_decl with + With_Definition (_,c) -> With_Definition (idl,c) + | With_Module (_,c) -> With_Module (idl,c) in + check_with_aux_mod env' (type_of_mb env old) new_with_decl + | Some mp -> + error_a_generative_module_expected l end - in - MTBsig(msid, before@(l,new_spec)::after) + | _ -> anomaly "Modtyping:incorrect use of with" with Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l - - -and translate_module env me = + +and translate_module env me = match me.mod_entry_expr, me.mod_entry_type with | None, None -> anomaly "Mod_typing.translate_module: empty type and expr in module entry" | None, Some mte -> - let mtb = translate_modtype env mte in + let mtb = translate_struct_entry env mte in { mod_expr = None; - mod_user_type = Some mtb; - mod_type = mtb; + mod_type = Some mtb; mod_equiv = None; - mod_constraints = Constraint.empty; - mod_retroknowledge = [] } + mod_constraints = Constraint.empty; + mod_retroknowledge = []} | Some mexpr, _ -> - let meq_o = (* do we have a transparent module ? *) + let meq_o = try (* TODO: transparent field in module_entry *) match me.mod_entry_type with | None -> Some (path_of_mexpr mexpr) @@ -181,17 +190,17 @@ and translate_module env me = with | Not_path -> None in - let meb,mtb1 = translate_mexpr env mexpr in - let mtb, mod_user_type, cst = + let meb = translate_struct_entry env mexpr in + let mod_typ, cst = match me.mod_entry_type with - | None -> mtb1, None, Constraint.empty + | None -> None, Constraint.empty | Some mte -> - let mtb2 = translate_modtype env mte in - let cst = check_subtypes env mtb1 mtb2 in - mtb2, Some mtb2, cst + let mtb1 = translate_struct_entry env mte in + let cst = check_subtypes env (eval_struct env meb) + mtb1 in + Some mtb1, cst in - { mod_type = mtb; - mod_user_type = mod_user_type; + { mod_type = mod_typ; mod_expr = Some meb; mod_equiv = meq_o; mod_constraints = cst; @@ -200,96 +209,78 @@ and translate_module env me = If it does, I don't really know how to fix the bug.*) -(* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *) -and translate_mexpr env mexpr = match mexpr with - | MEident mp -> - MEBident mp, - type_modpath env mp - | MEfunctor (arg_id, arg_e, body_expr) -> - let arg_b = translate_modtype env arg_e in + +and translate_struct_entry env mse = match mse with + | MSEident mp -> + SEBident mp + | MSEfunctor (arg_id, arg_e, body_expr) -> + let arg_b = translate_struct_entry env arg_e in let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in - let (body_b,body_tb) = translate_mexpr env' body_expr in - MEBfunctor (arg_id, arg_b, body_b), - MTBfunsig (arg_id, arg_b, body_tb) - | MEapply (fexpr,mexpr) -> - let feb,ftb = translate_mexpr env fexpr in - let ftb = scrape_modtype env ftb in - let farg_id, farg_b, fbody_b = destr_functor ftb in - let meb,mtb = translate_mexpr env mexpr in - let cst = check_subtypes env mtb farg_b in - let mp = + let body_b = translate_struct_entry env' body_expr in + SEBfunctor (arg_id, arg_b, body_b) + | MSEapply (fexpr,mexpr) -> + let feb = translate_struct_entry env fexpr in + let feb'= eval_struct env feb + in + let farg_id, farg_b, fbody_b = destr_functor env feb' in + let _ = try path_of_mexpr mexpr with | Not_path -> error_application_to_not_path mexpr - (* place for nondep_supertype *) - in - let resolve = Modops.resolver_of_environment farg_id farg_b mp env in - MEBapply(feb,meb,cst), - (* This is the place where the functor formal parameter is - substituted by the given argument to compute the type of the - functor application. *) - subst_modtype - (map_mbid farg_id mp (Some resolve)) fbody_b - + (* place for nondep_supertype *) in + let meb= translate_struct_entry env mexpr in + let cst = check_subtypes env (eval_struct env meb) farg_b in + SEBapply(feb,meb,cst) + | MSEwith(mte, with_decl) -> + let mtb = translate_struct_entry env mte in + let mtb' = check_with env mtb with_decl in + mtb' -let translate_module env me = translate_module env me -let rec add_module_expr_constraints env = function - | MEBident _ -> env +let rec add_struct_expr_constraints env = function + | SEBident _ -> env - | MEBfunctor (_,mtb,meb) -> - add_module_expr_constraints (add_modtype_constraints env mtb) meb + | SEBfunctor (_,mtb,meb) -> + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb - | MEBstruct (_,mod_struct_body) -> + | SEBstruct (_,structure_body) -> List.fold_left (fun env (l,item) -> add_struct_elem_constraints env item) env - mod_struct_body + structure_body - | MEBapply (meb1,meb2,cst) -> + | SEBapply (meb1,meb2,cst) -> Environ.add_constraints cst - (add_module_expr_constraints - (add_module_expr_constraints env meb1) + (add_struct_expr_constraints + (add_struct_expr_constraints env meb1) meb2) - + | SEBwith(meb,With_definition_body(_,cb))-> + Environ.add_constraints cb.const_constraints + (add_struct_expr_constraints env meb) + | SEBwith(meb,With_module_body(_,_,cst))-> + Environ.add_constraints cst + (add_struct_expr_constraints env meb) + and add_struct_elem_constraints env = function - | SEBconst cb -> Environ.add_constraints cb.const_constraints env - | SEBmind mib -> Environ.add_constraints mib.mind_constraints env - | SEBmodule mb -> add_module_constraints env mb - | SEBmodtype mtb -> add_modtype_constraints env mtb + | SFBconst cb -> Environ.add_constraints cb.const_constraints env + | SFBmind mib -> Environ.add_constraints mib.mind_constraints env + | SFBmodule mb -> add_module_constraints env mb + | SFBmodtype mtb -> add_modtype_constraints env mtb and add_module_constraints env mb = - (* if there is a body, the mb.mod_type is either inferred from the - body and hence uninteresting or equal to the non-empty - user_mod_type *) let env = match mb.mod_expr with - | None -> add_modtype_constraints env mb.mod_type - | Some meb -> add_module_expr_constraints env meb + | None -> env + | Some meb -> add_struct_expr_constraints env meb in - let env = match mb.mod_user_type with + let env = match mb.mod_type with | None -> env - | Some mtb -> add_modtype_constraints env mtb + | Some mtb -> + add_modtype_constraints env mtb in Environ.add_constraints mb.mod_constraints env -and add_modtype_constraints env = function - | MTBident _ -> env - | MTBfunsig (_,mtb1,mtb2) -> - add_modtype_constraints - (add_modtype_constraints env mtb1) - mtb2 - | MTBsig (_,mod_sig_body) -> - List.fold_left - (fun env (l,item) -> add_sig_elem_constraints env item) - env - mod_sig_body - -and add_sig_elem_constraints env = function - | SPBconst cb -> Environ.add_constraints cb.const_constraints env - | SPBmind mib -> Environ.add_constraints mib.mind_constraints env - | SPBmodule {msb_modtype=mtb; msb_constraints=cst} -> - add_modtype_constraints (Environ.add_constraints cst env) mtb - | SPBmodtype mtb -> add_modtype_constraints env mtb - - +and add_modtype_constraints env mtb = + add_struct_expr_constraints env mtb + diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 702e79ecc..124cb89c4 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -15,13 +15,13 @@ open Entries (*i*) -val translate_modtype : env -> module_type_entry -> module_type_body - val translate_module : env -> module_entry -> module_body -val translate_mexpr : env -> module_expr -> module_expr_body * module_type_body +val translate_struct_entry : env -> module_struct_entry -> struct_expr_body -val add_modtype_constraints : env -> module_type_body -> env +val add_modtype_constraints : env -> struct_expr_body -> env val add_module_constraints : env -> module_body -> env + + diff --git a/kernel/modops.ml b/kernel/modops.ml index 135a37747..c5b8e15b5 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -83,43 +83,36 @@ let error_local_context lo = let error_no_such_label_sub l l1 l2 = - error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing (or invisible) in "^l1^".") + error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing in "^l1^".") -let rec scrape_modtype env = function - | MTBident kn -> scrape_modtype env (lookup_modtype kn env) - | mtb -> mtb + + +let rec list_split_assoc k 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 + +let path_of_seb = function + | SEBident mb -> mb + | _ -> anomaly "Modops: evaluation failed." + + +let destr_functor env mtb = + match mtb with + | SEBfunctor (arg_id,arg_t,body_t) -> + (arg_id,arg_t,body_t) + | _ -> error_not_a_functor mtb (* the constraints are not important here *) -let module_body_of_spec msb = - { mod_type = msb.msb_modtype; - mod_equiv = msb.msb_equiv; - mod_expr = None; - mod_user_type = None; - mod_constraints = Constraint.empty; - mod_retroknowledge = []} let module_body_of_type mtb = - { mod_type = mtb; + { mod_type = Some mtb; mod_equiv = None; mod_expr = None; - mod_user_type = None; mod_constraints = Constraint.empty; mod_retroknowledge = []} -(* the constraints are not important here *) -let module_spec_of_body mb = - { msb_modtype = mb.mod_type; - msb_equiv = mb.mod_equiv; - msb_constraints = Constraint.empty} - - - -let destr_functor = function - | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) - | mtb -> error_not_a_functor mtb - - let rec check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else let mb1 = lookup_module mp1 env in @@ -131,47 +124,62 @@ let rec check_modpath_equiv env mp1 mp2 = | Some mp2' -> check_modpath_equiv env mp2' mp1) | Some mp1' -> check_modpath_equiv env mp2 mp1' +let subst_with_body sub = function + | With_module_body(id,mp,cst) -> + With_module_body(id,subst_mp sub mp,cst) + | With_definition_body(id,cb) -> + With_definition_body( id,subst_const_body sub cb) -let rec subst_modtype sub = function - (* This is the case in which I am substituting a whole module. - For instance "Module M(X). Module N := X. End M". When I apply - M to M' I must substitute M' for X in "Module N := X". *) - | MTBident ln -> MTBident (subst_kn sub ln) - | MTBfunsig (arg_id, arg_b, body_b) -> - MTBfunsig (arg_id, - subst_modtype sub arg_b, - subst_modtype sub body_b) - | MTBsig (sid1, msb) -> - MTBsig (sid1, subst_signature sub msb) - -and subst_signature sub sign = +let rec subst_modtype sub mtb = + subst_struct_expr sub mtb + +and subst_structure sub sign = let subst_body = function - SPBconst cb -> - SPBconst (subst_const_body sub cb) - | SPBmind mib -> - SPBmind (subst_mind sub mib) - | SPBmodule mb -> - SPBmodule (subst_module sub mb) - | SPBmodtype mtb -> - SPBmodtype (subst_modtype sub mtb) + SFBconst cb -> + SFBconst (subst_const_body sub cb) + | SFBmind mib -> + SFBmind (subst_mind sub mib) + | SFBmodule mb -> + SFBmodule (subst_module sub mb) + | SFBmodtype mtb -> + SFBmodtype (subst_modtype sub mtb) in List.map (fun (l,b) -> (l,subst_body b)) sign and subst_module sub mb = - let mtb' = subst_modtype sub mb.msb_modtype in + let mtb' = Option.smartmap (subst_modtype sub) mb.mod_type in (* This is similar to the previous case. In this case we have a module M in a signature that is knows to be equivalent to a module M' (because the signature is "K with Module M := M'") and we are substituting M' with some M''. *) - let mpo' = Option.smartmap (subst_mp sub) mb.msb_equiv in - if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else - { msb_modtype=mtb'; - msb_equiv=mpo'; - msb_constraints=mb.msb_constraints} + let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in + let mpo' = Option.smartmap (subst_mp sub) mb.mod_equiv in + if mtb'==mb.mod_type && mpo'==mb.mod_equiv && mb.mod_expr == me' + then mb else + { mod_expr = me'; + mod_type=mtb'; + mod_equiv=mpo'; + mod_constraints=mb.mod_constraints; + mod_retroknowledge=mb.mod_retroknowledge} + + +and subst_struct_expr sub = function + | SEBident mp -> SEBident (subst_mp sub mp) + | SEBfunctor (msid, mtb, meb') -> + SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb') + | SEBstruct (msid,str)-> + SEBstruct(msid, subst_structure sub str) + | SEBapply (meb1,meb2,cst)-> + SEBapply(subst_struct_expr sub meb1, + subst_struct_expr sub meb2, + cst) + | SEBwith (meb,wdb)-> + SEBwith(subst_struct_expr sub meb, + subst_with_body sub wdb) + let subst_signature_msid msid mp = - subst_signature (map_msid msid mp) - + subst_structure (map_msid msid mp) (* spiwack: here comes the function which takes care of importing the retroknowledge declared in the library *) @@ -198,43 +206,150 @@ let add_retroknowledge msid mp = imports 10 000 retroknowledge registration.*) List.fold_right subst_and_perform lclrk env -(* we assume that the substitution of "mp" into "msid" is already done -(or unnecessary) *) -let rec add_signature mp sign env = + + +let strengthen_const env mp l cb = + match cb.const_opaque, cb.const_body with + | false, Some _ -> cb + | true, Some _ + | _, None -> + let const = mkConst (make_con mp empty_dirpath l) in + let const_subs = Some (Declarations.from_val const) in + {cb with + const_body = const_subs; + const_opaque = false; + const_body_code = Cemitcodes.from_val + (compile_constant_body env const_subs false false) + } + +let strengthen_mind env mp l mib = match mib.mind_equiv with + | Some _ -> mib + | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)} + + +let rec eval_struct env = function + | SEBident mp -> + begin + match (lookup_modtype mp env) with + mtb,None -> eval_struct env mtb + | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb) + end + | SEBapply (seb1,seb2,_) -> + let svb1 = eval_struct env seb1 in + let farg_id, farg_b, fbody_b = destr_functor env svb1 in + let mp = path_of_seb seb2 in + let resolve = resolver_of_environment farg_id farg_b mp env in + eval_struct env (subst_modtype + (map_mbid farg_id mp (Some resolve)) fbody_b) + | SEBwith (mtb,wdb) -> merge_with env mtb wdb + | mtb -> mtb + +and type_of_mb env mb = + match mb.mod_type,mb.mod_expr with + None,Some b -> eval_struct env b + | Some t, _ -> eval_struct env t + | _,_ -> anomaly + "Modops: empty type and empty expr" + +and merge_with env mtb with_decl = + let msid,sig_b = match (eval_struct env mtb) with + | SEBstruct(msid,sig_b) -> msid,sig_b + | _ -> error_signature_expected mtb + in + let id,idl = match with_decl with + | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) -> id,idl + | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false + in + let l = label_of_id id in + try + let rev_before,spec,after = list_split_assoc l [] sig_b in + let before = List.rev rev_before in + let new_spec = match with_decl with + | With_definition_body ([],_) + | With_module_body ([],_,_) -> assert false + | With_definition_body ([id],c) -> + SFBconst c + | With_module_body ([id], mp,cst) -> + let old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module (string_of_label l) + in + let mtb' = eval_struct env (SEBident mp) in + let msb = + {mod_expr = Some (SEBident mp); + mod_type = Some mtb'; + mod_equiv = Some mp; + mod_constraints = cst; + mod_retroknowledge = old.mod_retroknowledge } + in + (SFBmodule msb) + | With_definition_body (_::_,_) + | With_module_body (_::_,_,_) -> + let old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module (string_of_label l) + in + let new_with_decl = match with_decl with + With_definition_body (_,c) -> With_definition_body (idl,c) + | With_module_body (_,c,cst) -> With_module_body (idl,c,cst) in + let modtype = + merge_with env (type_of_mb env old) new_with_decl in + let msb = + { mod_expr = None; + mod_type = Some modtype; + mod_equiv = None; + mod_constraints = old.mod_constraints; + mod_retroknowledge = old.mod_retroknowledge} + in + (SFBmodule msb) + in + SEBstruct(msid, before@(l,new_spec)::after) + with + Not_found -> error_no_such_label l + +and add_signature mp sign env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in let con = make_con mp empty_dirpath l in match elem with - | SPBconst cb -> Environ.add_constant con cb env - | SPBmind mib -> Environ.add_mind kn mib env - | SPBmodule mb -> - add_module (MPdot (mp,l)) (module_body_of_spec mb) env + | SFBconst cb -> Environ.add_constant con cb env + | SFBmind mib -> Environ.add_mind kn mib env + | SFBmodule mb -> + add_module (MPdot (mp,l)) mb env (* adds components as well *) - | SPBmodtype mtb -> Environ.add_modtype kn mtb env + | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) + (mtb,None) env in List.fold_left add_one env sign - and add_module mp mb env = let env = Environ.shallow_add_module mp mb env in - match scrape_modtype env mb.mod_type with - | MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBsig (msid,sign) -> + let env = match mb.mod_type,mb.mod_expr with + | Some mt, _ -> + Environ.add_modtype mp (mt,Some mp) env + | None, Some me -> + Environ.add_modtype mp (me,Some mp) env + | _,_ -> anomaly "Modops:Empty expr and type" in + let mod_typ = type_of_mb env mb in + match mod_typ with + | SEBstruct (msid,sign) -> add_retroknowledge msid mp (mb.mod_retroknowledge) (add_signature mp (subst_signature_msid msid mp sign) env) - | MTBfunsig _ -> env + | SEBfunctor _ -> env + | _ -> anomaly "Modops:the evaluation of the structure failed " + -let rec constants_of_specification env mp sign = +and constants_of_specification env mp sign = let aux (env,res) (l,elem) = match elem with - | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res - | SPBmind _ -> env,res - | SPBmodule mb -> - let new_env = add_module (MPdot (mp,l)) (module_body_of_spec mb) env in + | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res + | SFBmind _ -> env,res + | SFBmodule mb -> + let new_env = add_module (MPdot (mp,l)) mb env in new_env,(constants_of_modtype env (MPdot (mp,l)) - (module_body_of_spec mb).mod_type) @ res - | SPBmodtype mtb -> + (type_of_mb env mb)) @ res + | SFBmodtype mtb -> (* module type dans un module type. Il faut au moins mettre mtb dans l'environnement (avec le bon kn pour pouvoir continuer aller deplier les modules utilisant ce @@ -250,21 +365,22 @@ let rec constants_of_specification env mp sign = si on ne rajoute pas T2 dans l'environement de typage on va exploser au moment du Declare Module *) - let new_env = Environ.add_modtype (make_kn mp empty_dirpath l) mtb env in + let new_env = Environ.add_modtype (MPdot(mp,l)) (mtb,None) env in new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res in snd (List.fold_left aux (env,[]) sign) and constants_of_modtype env mp modtype = - match scrape_modtype env modtype with - MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBsig (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | MTBfunsig _ -> [] - -(* returns a resolver for kn that maps mbid to mp *) -let resolver_of_environment mbid modtype mp env = + match (eval_struct env modtype) with + SEBstruct (msid,sign) -> + constants_of_specification env mp + (subst_signature_msid msid mp sign) + | SEBfunctor _ -> [] + | _ -> anomaly "Modops:the evaluation of the structure failed " + +(* returns a resolver for kn that maps mbid to mp. We only keep + constants that have the inline flag *) +and resolver_of_environment mbid modtype mp env = let constants = constants_of_modtype env (MPbound mbid) modtype in let rec make_resolve = function | [] -> [] @@ -284,65 +400,56 @@ let resolver_of_environment mbid modtype mp env = let resolve = make_resolve constants in Mod_subst.make_resolver resolve -let strengthen_const env mp l cb = - match cb.const_opaque, cb.const_body with - | false, Some _ -> cb - | true, Some _ - | _, None -> - let const = mkConst (make_con mp empty_dirpath l) in - let const_subs = Some (Declarations.from_val const) in - {cb with - const_body = const_subs; - const_opaque = false; - const_body_code = Cemitcodes.from_val - (compile_constant_body env const_subs false false) - } - -let strengthen_mind env mp l mib = match mib.mind_equiv with - | Some _ -> mib - | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)} -let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with - | MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBfunsig _ -> mtb - | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp) - -and strengthen_mod env mp msb = - { msb_modtype = strengthen_mtb env mp msb.msb_modtype; - msb_equiv = begin match msb.msb_equiv with - | Some _ -> msb.msb_equiv - | None -> Some mp - end ; - msb_constraints = msb.msb_constraints; } - +and strengthen_mtb env mp mtb = + let mtb1 = eval_struct env mtb in + match mtb1 with + | SEBfunctor _ -> mtb1 + | SEBstruct (msid,sign) -> + SEBstruct (msid,strengthen_sig env msid sign mp) + | _ -> anomaly "Modops:the evaluation of the structure failed " + +and strengthen_mod env mp mb = + let mod_typ = type_of_mb env mb in + { mod_expr = mb.mod_expr; + mod_type = Some (strengthen_mtb env mp mod_typ); + mod_equiv = begin match mb.mod_equiv with + | Some _ -> mb.mod_equiv + | None -> Some mp + end ; + mod_constraints = mb.mod_constraints; + mod_retroknowledge = mb.mod_retroknowledge} + and strengthen_sig env msid sign mp = match sign with | [] -> [] - | (l,SPBconst cb) :: rest -> - let item' = l,SPBconst (strengthen_const env mp l cb) in + | (l,SFBconst cb) :: rest -> + let item' = l,SFBconst (strengthen_const env mp l cb) in let rest' = strengthen_sig env msid rest mp in item'::rest' - | (l,SPBmind mib) :: rest -> - let item' = l,SPBmind (strengthen_mind env mp l mib) in + | (l,SFBmind mib) :: rest -> + let item' = l,SFBmind (strengthen_mind env mp l mib) in let rest' = strengthen_sig env msid rest mp in item'::rest' - | (l,SPBmodule mb) :: rest -> + | (l,SFBmodule mb) :: rest -> let mp' = MPdot (mp,l) in - let item' = l,SPBmodule (strengthen_mod env mp' mb) in + let item' = l,SFBmodule (strengthen_mod env mp' mb) in let env' = add_module (MPdot (MPself msid,l)) - (module_body_of_spec mb) - env + mb + env in let rest' = strengthen_sig env' msid rest mp in item'::rest' - | (l,SPBmodtype mty as item) :: rest -> + | (l,SFBmodtype mty as item) :: rest -> let env' = add_modtype - (make_kn (MPself msid) empty_dirpath l) - mty + (MPdot((MPself msid),l)) + (mty,None) env in let rest' = strengthen_sig env' msid rest mp in item::rest' + let strengthen env mtb mp = strengthen_mtb env mp mtb + diff --git a/kernel/modops.mli b/kernel/modops.mli index d7cdb59ac..3cb8e47bb 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -20,55 +20,52 @@ open Mod_subst (* Various operations on modules and module types *) -(* recursively unfold MTBdent module types *) -val scrape_modtype : env -> module_type_body -> module_type_body - (* make the environment entry out of type *) -val module_body_of_type : module_type_body -> module_body - -val module_body_of_spec : module_specification_body -> module_body - -val module_spec_of_body : module_body -> module_specification_body +val module_body_of_type : struct_expr_body -> module_body val destr_functor : - module_type_body -> mod_bound_id * module_type_body * module_type_body + env -> struct_expr_body -> mod_bound_id * struct_expr_body * struct_expr_body - -val subst_modtype : substitution -> module_type_body -> module_type_body +val subst_modtype : substitution -> struct_expr_body -> struct_expr_body val subst_signature_msid : mod_self_id -> module_path -> - module_signature_body -> module_signature_body + structure_body -> structure_body + +(* Evaluation functions *) +val eval_struct : env -> struct_expr_body -> struct_expr_body + +val type_of_mb : env -> module_body -> struct_expr_body (* [add_signature mp sign env] assumes that the substitution [msid] $\mapsto$ [mp] has already been performed (or is not necessary, like when [mp = MPself msid]) *) val add_signature : - module_path -> module_signature_body -> env -> env + module_path -> structure_body -> env -> env (* adds a module and its components, but not the constraints *) val add_module : - module_path -> module_body -> env -> env + module_path -> module_body -> env -> env val check_modpath_equiv : env -> module_path -> module_path -> unit -val strengthen : env -> module_type_body -> module_path -> module_type_body +val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body val error_existing_label : label -> 'a -val error_declaration_not_path : module_expr -> 'a +val error_declaration_not_path : module_struct_entry -> 'a -val error_application_to_not_path : module_expr -> 'a +val error_application_to_not_path : module_struct_entry -> 'a -val error_not_a_functor : module_expr -> 'a +val error_not_a_functor : module_struct_entry -> 'a val error_incompatible_modtypes : - module_type_body -> module_type_body -> 'a + struct_expr_body -> struct_expr_body -> 'a val error_not_equal : module_path -> module_path -> 'a -val error_not_match : label -> specification_body -> 'a +val error_not_match : label -> structure_field_body -> 'a val error_incompatible_labels : label -> label -> 'a @@ -76,7 +73,7 @@ val error_no_such_label : label -> 'a val error_result_must_be_signature : unit -> 'a -val error_signature_expected : module_type_body -> 'a +val error_signature_expected : struct_expr_body -> 'a val error_no_module_to_end : unit -> 'a @@ -99,4 +96,4 @@ val error_local_context : label option -> 'a val error_no_such_label_sub : label->string->string->'a val resolver_of_environment : - mod_bound_id -> module_type_body -> module_path -> env -> resolver + mod_bound_id -> struct_expr_body -> module_path -> env -> resolver diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 4f2498dc3..2b41e5a36 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -26,7 +26,7 @@ type globals = { env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body KNmap.t } + env_modtypes : module_type_body MPmap.t } type stratification = { env_universes : universes; @@ -60,7 +60,7 @@ let empty_env = { env_constants = Cmap.empty; env_inductives = KNmap.empty; env_modules = MPmap.empty; - env_modtypes = KNmap.empty }; + env_modtypes = MPmap.empty }; env_named_context = empty_named_context; env_named_vals = []; env_rel_context = empty_rel_context; diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 511f56e65..b6d83b918 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -26,7 +26,7 @@ type globals = { env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body KNmap.t } + env_modtypes : module_type_body MPmap.t } type stratification = { env_universes : universes; diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f7f6a980d..368879713 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -28,8 +28,8 @@ open Mod_typing type modvariant = | NONE - | SIG of (* funsig params *) (mod_bound_id * module_type_body) list - | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list + | SIG of (* funsig params *) (mod_bound_id * struct_expr_body) list + | STRUCT of (* functor params *) (mod_bound_id * struct_expr_body) list | LIBRARY of dir_path type module_info = @@ -54,8 +54,7 @@ type safe_environment = env : env; modinfo : module_info; labset : Labset.t; - revsign : module_signature_body; - revstruct : module_structure_body; + revstruct : structure_body; univ : Univ.constraints; engagement : engagement option; imports : library_info list; @@ -84,7 +83,6 @@ let rec empty_environment = label = mk_label "_"; variant = NONE}; labset = Labset.empty; - revsign = []; revstruct = []; univ = Univ.Constraint.empty; engagement = None; @@ -214,8 +212,7 @@ let add_constant dir l decl senv = env = env''; modinfo = senv.modinfo; labset = Labset.add l senv.labset; - revsign = (l,SPBconst cb)::senv.revsign; - revstruct = (l,SEBconst cb)::senv.revstruct; + revstruct = (l,SFBconst cb)::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; @@ -244,8 +241,7 @@ let add_mind dir l mie senv = env = env''; modinfo = senv.modinfo; labset = Labset.add l senv.labset; (* TODO: the same as above *) - revsign = (l,SPBmind mib)::senv.revsign; - revstruct = (l,SEBmind mib)::senv.revstruct; + revstruct = (l,SFBmind mib)::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; @@ -257,16 +253,15 @@ let add_mind dir l mie senv = let add_modtype l mte senv = check_label l senv.labset; - let mtb = translate_modtype senv.env mte in + let mtb = translate_struct_entry senv.env mte in let env' = add_modtype_constraints senv.env mtb in - let kn = make_kn senv.modinfo.modpath empty_dirpath l in - let env'' = Environ.add_modtype kn mtb env' in - kn, { old = senv.old; + let mp = MPdot(senv.modinfo.modpath, l) in + let env'' = Environ.add_modtype mp (mtb,None) env' in + mp, { old = senv.old; env = env''; modinfo = senv.modinfo; labset = Labset.add l senv.labset; - revsign = (l,SPBmodtype mtb)::senv.revsign; - revstruct = (l,SEBmodtype mtb)::senv.revstruct; + revstruct = (l,SFBmodtype mtb)::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; @@ -285,15 +280,13 @@ let full_add_module mp mb env = let add_module l me senv = check_label l senv.labset; let mb = translate_module senv.env me in - let mspec = module_spec_of_body mb in let mp = MPdot(senv.modinfo.modpath, l) in let env' = full_add_module mp mb senv.env in mp, { old = senv.old; env = env'; modinfo = senv.modinfo; labset = Labset.add l senv.labset; - revsign = (l,SPBmodule mspec)::senv.revsign; - revstruct = (l,SEBmodule mb)::senv.revstruct; + revstruct = (l,SFBmodule mb)::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; @@ -317,7 +310,6 @@ let start_module l senv = env = senv.env; modinfo = modinfo; labset = Labset.empty; - revsign = []; revstruct = []; univ = Univ.Constraint.empty; engagement = None; @@ -329,7 +321,7 @@ let start_module l senv = let end_module l restype senv = let oldsenv = senv.old in let modinfo = senv.modinfo in - let restype = Option.map (translate_modtype senv.env) restype in + let restype = Option.map (translate_struct_entry senv.env) restype in let params = match modinfo.variant with | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () @@ -337,40 +329,32 @@ let end_module l restype senv = in if l <> modinfo.label then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_local_context None; - let functorize_type tb = + let functorize_struct tb = List.fold_left - (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb)) + (fun mtb (arg_id,arg_b) -> + SEBfunctor(arg_id,arg_b,mtb)) tb params in - let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in - let mtb, mod_user_type, cst = + let auto_tb = + SEBstruct (modinfo.msid, List.rev senv.revstruct) + in + let mod_typ, cst = match restype with - | None -> functorize_type auto_tb, None, Constraint.empty + | None -> None, Constraint.empty | Some res_tb -> let cst = check_subtypes senv.env auto_tb res_tb in - let mtb = functorize_type res_tb in - mtb, Some mtb, cst + let mtb = functorize_struct res_tb in + Some mtb, cst in + let mexpr = functorize_struct auto_tb in let cst = Constraint.union cst senv.univ in - let mexpr = - List.fold_left - (fun mtb (arg_id,arg_b) -> MEBfunctor (arg_id,arg_b,mtb)) - (MEBstruct (modinfo.msid, List.rev senv.revstruct)) - params - in let mb = { mod_expr = Some mexpr; - mod_user_type = mod_user_type; - mod_type = mtb; + mod_type = mod_typ; mod_equiv = None; mod_constraints = cst; - mod_retroknowledge = senv.local_retroknowledge} - in - let mspec = - { msb_modtype = mtb; - msb_equiv = None; - msb_constraints = Constraint.empty } + mod_retroknowledge = senv.local_retroknowledge } in let mp = MPdot (oldsenv.modinfo.modpath, l) in let newenv = oldsenv.env in @@ -388,8 +372,7 @@ let end_module l restype senv = env = newenv; modinfo = oldsenv.modinfo; labset = Labset.add l oldsenv.labset; - revsign = (l,SPBmodule mspec)::oldsenv.revsign; - revstruct = (l,SEBmodule mb)::oldsenv.revstruct; + revstruct = (l,SFBmodule mb)::oldsenv.revstruct; univ = oldsenv.univ; (* engagement is propagated to the upper level *) engagement = senv.engagement; @@ -398,12 +381,85 @@ let end_module l restype senv = local_retroknowledge = senv.local_retroknowledge@oldsenv.local_retroknowledge } +(* Include for module and module type*) + let add_include me senv = + let struct_expr = translate_struct_entry senv.env me in + let senv = { senv with env = add_modtype_constraints senv.env struct_expr } in + let msid,str = match (eval_struct senv.env struct_expr) with + | SEBstruct(msid,str_l) -> msid,str_l + | _ -> error ("You cannot Include a higher-order Module or Module Type" ) + in + let mp_sup = senv.modinfo.modpath in + let str1 = subst_signature_msid msid mp_sup str in + let add senv (l,elem) = + check_label l senv.labset; + match elem with + | SFBconst cb -> + let con = make_con mp_sup empty_dirpath l in + let env' = Environ.add_constraints cb.const_constraints senv.env in + let env'' = Environ.add_constant con cb env' in + { old = senv.old; + env = env''; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revstruct = (l,SFBconst cb)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; + imports = senv.imports; + loads = senv.loads ; + local_retroknowledge = senv.local_retroknowledge } + + | SFBmind mib -> + let kn = make_kn mp_sup empty_dirpath l in + let env' = Environ.add_constraints mib.mind_constraints senv.env in + let env'' = Environ.add_mind kn mib env' in + { old = senv.old; + env = env''; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revstruct = (l,SFBmind mib)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; + imports = senv.imports; + loads = senv.loads; + local_retroknowledge = senv.local_retroknowledge } + + | SFBmodule mb -> + let mp = MPdot(senv.modinfo.modpath, l) in + let env' = full_add_module mp mb senv.env in + { old = senv.old; + env = env'; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revstruct = (l,SFBmodule mb)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; + imports = senv.imports; + loads = senv.loads; + local_retroknowledge = senv.local_retroknowledge } + | SFBmodtype mtb -> + let env' = add_modtype_constraints senv.env mtb in + let mp = MPdot(senv.modinfo.modpath, l) in + let env'' = Environ.add_modtype mp (mtb,None) env' in + { old = senv.old; + env = env''; + modinfo = senv.modinfo; + labset = Labset.add l senv.labset; + revstruct = (l,SFBmodtype mtb)::senv.revstruct; + univ = senv.univ; + engagement = senv.engagement; + imports = senv.imports; + loads = senv.loads; + local_retroknowledge = senv.local_retroknowledge } + in + List.fold_left add senv str1 + (* Adding parameters to modules or module types *) let add_module_parameter mbid mte senv = - if senv.revsign <> [] or senv.revstruct <> [] or senv.loads <> [] then + if senv.revstruct <> [] or senv.loads <> [] then anomaly "Cannot add a module parameter to a non empty module"; - let mtb = translate_modtype senv.env mte in + let mtb = translate_struct_entry senv.env mte in let env = full_add_module (MPbound mbid) (module_body_of_type mtb) senv.env in let new_variant = match senv.modinfo.variant with @@ -416,7 +472,6 @@ let add_module_parameter mbid mte senv = env = env; modinfo = { senv.modinfo with variant = new_variant }; labset = senv.labset; - revsign = []; revstruct = []; univ = senv.univ; engagement = senv.engagement; @@ -441,12 +496,11 @@ let start_modtype l senv = env = senv.env; modinfo = modinfo; labset = Labset.empty; - revsign = []; revstruct = []; univ = Univ.Constraint.empty; engagement = None; imports = senv.imports; - loads = []; + loads = [] ; (* spiwack: not 100% sure, but I think it should be like that *) local_retroknowledge = []} @@ -460,14 +514,17 @@ let end_modtype l senv = in if l <> modinfo.label then error_incompatible_labels l modinfo.label; if not (empty_context senv.env) then error_local_context None; - let res_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in + let auto_tb = + SEBstruct (modinfo.msid, List.rev senv.revstruct) + in let mtb = List.fold_left - (fun mtb (arg_id,arg_b) -> MTBfunsig (arg_id,arg_b,mtb)) - res_tb + (fun mtb (arg_id,arg_b) -> + SEBfunctor(arg_id,arg_b,mtb)) + auto_tb params in - let kn = make_kn oldsenv.modinfo.modpath empty_dirpath l in + let mp = MPdot (oldsenv.modinfo.modpath, l) in let newenv = oldsenv.env in (* since universes constraints cannot be stored in the modtype, they are propagated to the upper level *) @@ -483,14 +540,13 @@ let end_modtype l senv = add_modtype_constraints newenv mtb in let newenv = - Environ.add_modtype kn mtb newenv + Environ.add_modtype mp (mtb,None) newenv in - kn, { old = oldsenv.old; + mp, { old = oldsenv.old; env = newenv; modinfo = oldsenv.modinfo; labset = Labset.add l oldsenv.labset; - revsign = (l,SPBmodtype mtb)::oldsenv.revsign; - revstruct = (l,SEBmodtype mtb)::oldsenv.revstruct; + revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct; univ = Univ.Constraint.union senv.univ oldsenv.univ; engagement = senv.engagement; imports = senv.imports; @@ -532,7 +588,7 @@ type compiled_library = [start_library] was called *) let is_empty senv = - senv.revsign = [] && + senv.revstruct = [] && senv.modinfo.msid = initial_msid && senv.modinfo.variant = NONE @@ -557,7 +613,6 @@ let start_library dir senv = env = senv.env; modinfo = modinfo; labset = Labset.empty; - revsign = []; revstruct = []; univ = Univ.Constraint.empty; engagement = None; @@ -567,7 +622,6 @@ let start_library dir senv = - let export senv dir = let modinfo = senv.modinfo in begin @@ -581,9 +635,8 @@ let export senv dir = (*if senv.modinfo.params <> [] || senv.modinfo.restype <> None then (* error_export_simple *) (); *) let mb = - { mod_expr = Some (MEBstruct (modinfo.msid, List.rev senv.revstruct)); - mod_type = MTBsig (modinfo.msid, List.rev senv.revsign); - mod_user_type = None; + { mod_expr = Some (SEBstruct (modinfo.msid, List.rev senv.revstruct)); + mod_type = None; mod_equiv = None; mod_constraints = senv.univ; mod_retroknowledge = senv.local_retroknowledge} @@ -630,48 +683,31 @@ let import (dp,mb,depends,engmt) digest senv = (* Remove the body of opaque constants in modules *) - -let rec lighten_module mb = + let rec lighten_module mb = { mb with mod_expr = Option.map lighten_modexpr mb.mod_expr; - mod_type = lighten_modtype mb.mod_type; - mod_user_type = Option.map lighten_modtype mb.mod_user_type } - -and lighten_modtype = function - | MTBident kn as x -> x - | MTBfunsig (mbid,mtb1,mtb2) -> - MTBfunsig (mbid, lighten_modtype mtb1, lighten_modtype mtb2) - | MTBsig (msid,sign) -> MTBsig (msid, lighten_sig sign) - -and lighten_modspec ms = - { ms with msb_modtype = lighten_modtype ms.msb_modtype } - -and lighten_sig sign = - let lighten_spec (l,spec) = (l,match spec with - | SPBconst ({const_opaque=true} as x) -> SPBconst {x with const_body=None} - | (SPBconst _ | SPBmind _) as x -> x - | SPBmodule m -> SPBmodule (lighten_modspec m) - | SPBmodtype m -> SPBmodtype (lighten_modtype m)) - in - List.map lighten_spec sign - + mod_type = Option.map lighten_modexpr mb.mod_type; + } + and lighten_struct struc = let lighten_body (l,body) = (l,match body with - | SEBconst ({const_opaque=true} as x) -> SEBconst {x with const_body=None} - | (SEBconst _ | SEBmind _) as x -> x - | SEBmodule m -> SEBmodule (lighten_module m) - | SEBmodtype m -> SEBmodtype (lighten_modtype m)) + | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None} + | (SFBconst _ | SFBmind _) as x -> x + | SFBmodule m -> SFBmodule (lighten_module m) + | SFBmodtype m -> SFBmodtype (lighten_modexpr m)) in List.map lighten_body struc and lighten_modexpr = function - | MEBfunctor (mbid,mty,mexpr) -> - MEBfunctor (mbid,lighten_modtype mty,lighten_modexpr mexpr) - | MEBident mp as x -> x - | MEBstruct (msid, struc) -> - MEBstruct (msid, lighten_struct struc) - | MEBapply (mexpr,marg,u) -> - MEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) + | SEBfunctor (mbid,mty,mexpr) -> + SEBfunctor (mbid,lighten_modexpr mty,lighten_modexpr mexpr) + | SEBident mp as x -> x + | SEBstruct (msid, struc) -> + SEBstruct (msid, lighten_struct struc) + | SEBapply (mexpr,marg,u) -> + SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) + | SEBwith (seb,wdcl) -> + SEBwith (lighten_modexpr seb,wdcl) let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index fe028c073..e764312b5 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -59,8 +59,8 @@ val add_module : (* Adding a module type *) val add_modtype : - label -> module_type_entry -> safe_environment - -> kernel_name * safe_environment + label -> module_struct_entry -> safe_environment + -> module_path * safe_environment (* Adding universe constraints *) val add_constraints : @@ -73,20 +73,21 @@ val set_engagement : engagement -> safe_environment -> safe_environment (*s Interactive module functions *) val start_module : label -> safe_environment -> module_path * safe_environment - val end_module : - label -> module_type_entry option + label -> module_struct_entry option -> safe_environment -> module_path * safe_environment val add_module_parameter : - mod_bound_id -> module_type_entry -> safe_environment -> safe_environment + mod_bound_id -> module_struct_entry -> safe_environment -> safe_environment val start_modtype : label -> safe_environment -> module_path * safe_environment val end_modtype : - label -> safe_environment -> kernel_name * safe_environment + label -> safe_environment -> module_path * safe_environment +val add_include : + module_struct_entry -> safe_environment -> safe_environment val current_modpath : safe_environment -> module_path val current_msid : safe_environment -> mod_self_id diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index a9403a5e3..3db187a0b 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -27,13 +27,12 @@ open Entries (* This local type is used to subtype a constant with a constructor or an inductive type. It can also be useful to allow reorderings in inductive types *) - type namedobject = | Constant of constant_body | IndType of inductive * mutual_inductive_body | IndConstr of constructor * mutual_inductive_body - | Module of module_specification_body - | Modtype of module_type_body + | Module of module_body + | Modtype of struct_expr_body (* adds above information about one mutual inductive: all types and constructors *) @@ -59,11 +58,11 @@ let make_label_map mp list = let add_one (l,e) map = let add_map obj = Labmap.add l obj map in match e with - | SPBconst cb -> add_map (Constant cb) - | SPBmind mib -> + | SFBconst cb -> add_map (Constant cb) + | SFBmind mib -> add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map - | SPBmodule mb -> add_map (Module mb) - | SPBmodtype mtb -> add_map (Modtype mtb) + | SFBmodule mb -> add_map (Module mb) + | SFBmodtype mtb -> add_map (Modtype mtb) in List.fold_right add_one list Labmap.empty @@ -290,10 +289,10 @@ let check_constant cst env msid1 l info1 cb2 spec2 = let rec check_modules cst env msid1 l msb1 msb2 = let mp = (MPdot(MPself msid1,l)) in - let mty1 = strengthen env msb1.msb_modtype mp in - let cst = check_modtypes cst env mty1 msb2.msb_modtype false in - begin - match msb1.msb_equiv, msb2.msb_equiv with + let mty1 = strengthen env (type_of_mb env msb1) mp in + let cst = check_modtypes cst env mty1 (type_of_mb env msb2) false in + begin + match msb1.mod_equiv, msb2.mod_equiv with | _, None -> () | None, Some mp2 -> check_modpath_equiv env mp mp2 @@ -316,18 +315,18 @@ and check_signatures cst env (msid1,sig1) (msid2,sig2') = Not_found -> error_no_such_label_sub l (string_of_msid msid1) (string_of_msid msid2) in match spec2 with - | SPBconst cb2 -> + | SFBconst cb2 -> check_constant cst env msid1 l info1 cb2 spec2 - | SPBmind mib2 -> + | SFBmind mib2 -> check_inductive cst env msid1 l info1 mib2 spec2 - | SPBmodule msb2 -> + | SFBmodule msb2 -> let msb1 = match info1 with | Module msb -> msb | _ -> error_not_match l spec2 in check_modules cst env msid1 l msb1 msb2 - | SPBmodtype mtb2 -> + | SFBmodtype mtb2 -> let mtb1 = match info1 with | Modtype mtb -> mtb @@ -339,19 +338,19 @@ and check_signatures cst env (msid1,sig1) (msid2,sig2') = and check_modtypes cst env mtb1 mtb2 equiv = if mtb1==mtb2 then cst else (* just in case :) *) - let mtb1' = scrape_modtype env mtb1 in - let mtb2' = scrape_modtype env mtb2 in + let mtb1' = eval_struct env mtb1 in + let mtb2' = eval_struct env mtb2 in if mtb1'==mtb2' then cst else match mtb1', mtb2' with - | MTBsig (msid1,list1), - MTBsig (msid2,list2) -> + | SEBstruct (msid1,list1), + SEBstruct (msid2,list2) -> let cst = check_signatures cst env (msid1,list1) (msid2,list2) in if equiv then check_signatures cst env (msid2,list2) (msid1,list1) else cst - | MTBfunsig (arg_id1,arg_t1,body_t1), - MTBfunsig (arg_id2,arg_t2,body_t2) -> + | SEBfunctor (arg_id1,arg_t1,body_t1), + SEBfunctor (arg_id2,arg_t2,body_t2) -> let cst = check_modtypes cst env arg_t2 arg_t1 equiv in (* contravariant *) let env = @@ -365,8 +364,6 @@ and check_modtypes cst env mtb1 mtb2 equiv = body_t1 in check_modtypes cst env body_t1' body_t2 equiv - | MTBident _ , _ -> anomaly "Subtyping: scrape failed" - | _ , MTBident _ -> anomaly "Subtyping: scrape failed" | _ , _ -> error_incompatible_modtypes mtb1 mtb2 let check_subtypes env sup super = diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index c0b1ee5d3..d7288fc06 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -14,6 +14,6 @@ open Declarations open Environ (*i*) -val check_subtypes : env -> module_type_body -> module_type_body -> constraints +val check_subtypes : env -> struct_expr_body -> struct_expr_body -> constraints diff --git a/library/declaremods.ml b/library/declaremods.ml index 29e8012fe..8cfd7e1ae 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -78,8 +78,8 @@ let modtab_objects = (* currently started interactive module (if any) - its arguments (if it is a functor) and declared output type *) let openmod_info = - ref (([],None,None) : mod_bound_id list * module_type_entry option - * module_type_body option) + ref (([],None,None) : mod_bound_id list * module_struct_entry option + * struct_expr_body option) let _ = Summary.declare_summary "MODULE-INFO" { Summary.freeze_function = (fun () -> @@ -122,23 +122,19 @@ let msid_of_prefix (_,(mp,sec)) = anomaly ("Non-empty section in module name!" ^ string_of_mp mp ^ "." ^ string_of_dirpath sec) -(* Check that a module type is not functorial *) - -let rec check_sig env = function - | MTBident kn -> check_sig env (Environ.lookup_modtype kn env) - | MTBsig _ -> () - | MTBfunsig _ -> Modops.error_result_must_be_signature () - -let rec check_sig_entry env = function - | MTEident kn -> check_sig env (Environ.lookup_modtype kn env) - | MTEfunsig _ -> Modops.error_result_must_be_signature () - | MTEwith (mte,_) -> check_sig_entry env mte +let rec scrape_alias mp = + match (Environ.lookup_module mp + (Global.env())) with + | {mod_expr = Some (SEBident mp1); + mod_type = None} -> scrape_alias mp1 + | _ -> mp + (* This function checks if the type calculated for the module [mp] is a subtype of [sub_mtb]. Uses only the global environment. *) let check_subtypes mp sub_mtb = let env = Global.env () in - let mtb = (Environ.lookup_module mp env).mod_type in + let mtb = Modops.eval_struct env (SEBident mp) in let _ = Environ.add_constraints (Subtyping.check_subtypes env mtb sub_mtb) in @@ -176,6 +172,35 @@ let do_module exists what iter_objects i dir mp substobjs objects = | None -> () + +let do_module_alias exists what iter_objects i dir mp alias substobjs objects = + let prefix = (dir,(alias,empty_dirpath)) in + let dirinfo = DirModule (dir,(mp,empty_dirpath)) in + let vis = + if exists then + if + try Nametab.locate_dir (qualid_of_dirpath dir) = dirinfo + with Not_found -> false + then + Nametab.Exactly i + else + errorlabstrm (what^"_module") + (pr_dirpath dir ++ str " should already exist!") + else + if Nametab.exists_dir dir then + errorlabstrm (what^"_module") (pr_dirpath dir ++ str " already exists") + else + Nametab.Until i + in + Nametab.push_dir vis dir dirinfo; + modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs; + match objects with + Some seg -> + modtab_objects := MPmap.add mp (prefix,seg) !modtab_objects; + iter_objects (i+1) prefix seg + | None -> () + + let conv_names_do_module exists what iter_objects i (sp,kn) substobjs substituted = let dir,mp = dir_of_sp sp, mp_of_kn kn in @@ -193,7 +218,8 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = | Some (me,sub_mte_o) -> let sub_mtb_o = match sub_mte_o with None -> None - | Some mte -> Some (Mod_typing.translate_modtype (Global.env()) mte) + | Some mte -> Some (Mod_typing.translate_struct_entry + (Global.env()) mte) in let mp = Global.add_module (basename sp) me in @@ -203,12 +229,40 @@ let cache_module ((sp,kn as oname),(entry,substobjs,substituted)) = match sub_mtb_o with None -> () | Some sub_mtb -> -check_subtypes mp sub_mtb + check_subtypes mp sub_mtb in conv_names_do_module false "cache" load_objects 1 oname substobjs substituted +let cache_module_alias ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias = match entry with + | None -> + anomaly "You must not recache interactive modules!" + | Some (me,sub_mte_o) -> + let sub_mtb_o = match sub_mte_o with + None -> None + | Some mte -> Some (Mod_typing.translate_struct_entry + (Global.env()) mte) + in + + let mp' = Global.add_module (basename sp) me in + if mp' <> mp_of_kn kn then + anomaly "Kernel and Library names do not match"; + + let _ = match sub_mtb_o with + None -> () + | Some sub_mtb -> + check_subtypes mp' sub_mtb in + match me with + | {mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "cache module alias" + in + do_module_alias false "cache" load_objects 1 dir mp alias substobjs substituted + + (* TODO: This check is not essential *) let check_empty s = function | None -> () @@ -224,12 +278,40 @@ let load_module i (oname,(entry,substobjs,substituted)) = check_empty "load_module" entry; conv_names_do_module false "load" load_objects i oname substobjs substituted +let load_module_alias i ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias= + match entry with + | Some (me,_)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "tata" + end + | None -> anomaly "toujours" + in + do_module_alias false "load" load_objects i dir mp alias substobjs substituted let open_module i (oname,(entry,substobjs,substituted)) = (* TODO: This check is not essential *) check_empty "open_module" entry; conv_names_do_module true "open" open_objects i oname substobjs substituted +let open_module_alias i ((sp,kn),(entry,substobjs,substituted)) = + let dir,mp,alias= + match entry with + | Some (me,_)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + dir_of_sp sp,mp_of_kn kn,scrape_alias mp + | _ -> anomaly "tata" + end + | None -> anomaly "toujours" + in + do_module_alias true "open" open_objects i dir mp alias substobjs substituted let subst_substobjs dir mp (subst,mbids,msid,objs) = match mbids with @@ -252,10 +334,36 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) = in (None,substobjs,substituted) +let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = + let dir,mp = dir_of_sp sp, mp_of_kn kn in + let (sub,mbids,msid,objs) = substobjs in + let subst' = join sub subst in + (* substitutive_objects get the new substitution *) + let substobjs = (subst',mbids,msid,objs) in + (* if we are not a functor - calculate substitued. + We add "msid |-> mp" to the substitution *) + let substituted = subst_substobjs dir mp substobjs in + match entry with + | Some (me,sub)-> + begin + match me with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)} -> + (Some ({mod_entry_type = None; + mod_entry_expr = + Some (MSEident (subst_mp subst' mp))},sub), + substobjs,substituted) + + | _ -> anomaly "tata" + end + | None -> anomaly "toujours" let classify_module (_,(_,substobjs,_)) = Substitute (None,substobjs,None) +let classify_module_alias (_,(entry,substobjs,_)) = + Substitute (entry,substobjs,None) + let (in_module,out_module) = declare_object {(default_object "MODULE") with cache_function = cache_module; @@ -265,6 +373,14 @@ let (in_module,out_module) = classify_function = classify_module; export_function = (fun _ -> anomaly "No modules in sections!") } +let (in_module_alias,out_module_alias) = + declare_object {(default_object "MODULE ALIAS") with + cache_function = cache_module_alias; + load_function = load_module_alias; + open_function = open_module_alias; + subst_function = subst_module_alias; + classify_function = classify_module_alias; + export_function = (fun _ -> anomaly "No modules in sections!") } let cache_keep _ = anomaly "This module should not be cached!" @@ -298,7 +414,7 @@ let (in_modkeep,out_modkeep) = The module M gets its objects from SIG *) let modtypetab = - ref (KNmap.empty : substitutive_objects KNmap.t) + ref (MPmap.empty : substitutive_objects MPmap.t) (* currently started interactive module type. We remember its arguments if it is a functor type *) @@ -312,22 +428,20 @@ let _ = Summary.declare_summary "MODTYPE-INFO" modtypetab := fst ft; openmodtype_info := snd ft); Summary.init_function = (fun () -> - modtypetab := KNmap.empty; + modtypetab := MPmap.empty; openmodtype_info := []); Summary.survive_module = false; Summary.survive_section = true } - - let cache_modtype ((sp,kn),(entry,modtypeobjs)) = let _ = match entry with | None -> anomaly "You must not recache interactive module types!" | Some mte -> - let kn' = Global.add_modtype (basename sp) mte in - if kn' <> kn then + let mp = Global.add_modtype (basename sp) mte in + if mp <>mp_of_kn kn then anomaly "Kernel and Library names do not match" in @@ -335,9 +449,9 @@ let cache_modtype ((sp,kn),(entry,modtypeobjs)) = errorlabstrm "cache_modtype" (pr_sp sp ++ str " already exists") ; - Nametab.push_modtype (Nametab.Until 1) sp kn; + Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn); - modtypetab := KNmap.add kn modtypeobjs !modtypetab + modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab let load_modtype i ((sp,kn),(entry,modtypeobjs)) = @@ -347,23 +461,22 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) = errorlabstrm "cache_modtype" (pr_sp sp ++ str " already exists") ; - Nametab.push_modtype (Nametab.Until i) sp kn; + Nametab.push_modtype (Nametab.Until i) sp (mp_of_kn kn); - modtypetab := KNmap.add kn modtypeobjs !modtypetab + modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab let open_modtype i ((sp,kn),(entry,_)) = check_empty "open_modtype" entry; if - try Nametab.locate_modtype (qualid_of_sp sp) <> kn + try Nametab.locate_modtype (qualid_of_sp sp) <> (mp_of_kn kn) with Not_found -> true then errorlabstrm ("open_modtype") (pr_sp sp ++ str " should already exist!"); - Nametab.push_modtype (Nametab.Exactly i) sp kn - + Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) let subst_modtype (_,subst,(entry,(subs,mbids,msid,objs))) = check_empty "subst_modtype" entry; @@ -385,7 +498,7 @@ let (in_modtype,out_modtype) = -let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs = +let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs mp = if mbids<>[] then error "Unexpected functor objects" else @@ -394,10 +507,13 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs = | id::idl,(id',obj)::tail when id = id' -> if object_tag obj = "MODULE" then (match idl with - [] -> (id, in_module (None,modobjs,None))::tail + [] -> (id, in_module_alias (Some + ({mod_entry_type = None; + mod_entry_expr = Some (MSEident mp)},None) + ,modobjs,None))::tail | _ -> let (_,substobjs,_) = out_module obj in - let substobjs' = replace_module_object idl substobjs modobjs in + let substobjs' = replace_module_object idl substobjs modobjs mp in (id, in_module (None,substobjs',None))::tail ) else error "MODULE expected!" @@ -408,17 +524,34 @@ let rec replace_module_object idl (subst, mbids, msid, lib_stack) modobjs = let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) = (subst, mbids1@mbids2, msid, lib_stack) - -let rec get_modtype_substobjs = function - MTEident ln -> KNmap.find ln !modtypetab - | MTEfunsig (mbid,_,mte) -> - let (subst, mbids, msid, objs) = get_modtype_substobjs mte in +let rec get_modtype_substobjs env = function + MSEident ln -> MPmap.find ln !modtypetab + | MSEfunctor (mbid,_,mte) -> + let (subst, mbids, msid, objs) = get_modtype_substobjs env mte in (subst, mbid::mbids, msid, objs) - | MTEwith (mty, With_Definition _) -> get_modtype_substobjs mty - | MTEwith (mty, With_Module (idl,mp)) -> - let substobjs = get_modtype_substobjs mty in + | MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty + | MSEwith (mty, With_Module (idl,mp)) -> + let substobjs = get_modtype_substobjs env mty in let modobjs = MPmap.find mp !modtab_substobjs in - replace_module_object idl substobjs modobjs + replace_module_object idl substobjs modobjs mp + | MSEapply (mexpr, MSEident mp) -> + let ftb = Mod_typing.translate_struct_entry env mexpr in + let farg_id, farg_b, fbody_b = Modops.destr_functor env + (Modops.eval_struct env ftb) in + let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in + (match mbids with + | mbid::mbids -> + let resolve = + Modops.resolver_of_environment farg_id farg_b mp env in + (* application outside the kernel, only for substitutive + objects (that are all non-logical objects) *) + (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs) + | [] -> match mexpr with + | MSEident _ -> error "Application of a non-functor" + | _ -> error "Application of a functor with too few arguments") + | MSEapply (_,mexpr) -> + Modops.error_application_to_not_path mexpr + (* push names of bound modules (and their components) to Nametab *) (* add objects associated to them *) @@ -426,13 +559,14 @@ let process_module_bindings argids args = let process_arg id (mbid,mty) = let dir = make_dirpath [id] in let mp = MPbound mbid in - let substobjs = get_modtype_substobjs mty in + let substobjs = get_modtype_substobjs (Global.env()) mty in let substituted = subst_substobjs dir mp substobjs in do_module false "start" load_objects 1 dir mp substobjs substituted in List.iter2 process_arg argids args - +(* Dead code *) +(* let replace_module mtb id mb = todo "replace module after with"; mtb let rec get_some_body mty env = match mty with @@ -441,14 +575,15 @@ let rec get_some_body mty env = match mty with | MTEwith (mty,With_Definition _) -> get_some_body mty env | MTEwith (mty,With_Module (id,mp)) -> replace_module (get_some_body mty env) id (Environ.lookup_module mp env) - +*) +(* Dead code *) let intern_args interp_modtype (idl,arg) = let lib_dir = Lib.library_dp() in let mbids = List.map (fun (_,id) -> make_mbid lib_dir (string_of_id id)) idl in let mty = interp_modtype (Global.env()) arg in let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in - let substobjs = get_modtype_substobjs mty in + let substobjs = get_modtype_substobjs (Global.env()) mty in List.map2 (fun dir mbid -> Global.add_module_parameter mbid mty; @@ -457,7 +592,6 @@ let intern_args interp_modtype (idl,arg) = do_module false "interp" load_objects 1 dir mp substobjs substituted; (mbid,mty)) dirs mbids - let start_module interp_modtype export id args res_o = let fs = Summary.freeze_summaries () in @@ -469,23 +603,22 @@ let start_module interp_modtype export id args res_o = | Some (res, restricted) -> (* we translate the module here to catch errors as early as possible *) let mte = interp_modtype (Global.env()) res in - check_sig_entry (Global.env()) mte; if restricted then Some mte, None else - let mtb = Mod_typing.translate_modtype (Global.env()) mte in + let mtb = Mod_typing.translate_struct_entry (Global.env()) mte in let sub_mtb = List.fold_right (fun (arg_id,arg_t) mte -> - let arg_t = Mod_typing.translate_modtype (Global.env()) arg_t - in MTBfunsig(arg_id,arg_t,mte)) + let arg_t = Mod_typing.translate_struct_entry (Global.env()) arg_t + in SEBfunctor(arg_id,arg_t,mte)) arg_entries mtb in None, Some sub_mtb in let mbids = List.map fst arg_entries in - openmod_info:=(mbids,res_entry_o,sub_body_o); + openmod_info:=(mbids,res_entry_o,sub_body_o); let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); Lib.add_frozen_state () @@ -511,12 +644,14 @@ let end_module id = match res_o with | None -> (empty_subst, mbids, msid, substitute), keep, special - | Some (MTEident ln) -> - abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], [] - | Some (MTEwith _ as mty) -> - abstract_substobjs mbids (get_modtype_substobjs mty), [], [] - | Some (MTEfunsig _) -> + | Some (MSEident ln) -> + abstract_substobjs mbids (MPmap.find ln (!modtypetab)), [], [] + | Some (MSEwith _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] + | Some (MSEfunctor _) -> anomaly "Funsig cannot be here..." + | Some (MSEapply _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs (Global.env()) mty), [], [] with Not_found -> anomaly "Module objects not found..." in @@ -636,7 +771,6 @@ let import_module export mp = (************************************************************************) (* module types *) - let start_modtype interp_modtype id args = let fs = Summary.freeze_summaries () in @@ -667,7 +801,7 @@ let end_modtype id = if fst oname <> fst oldoname then anomaly "Section paths generated on start_ and end_modtype do not match"; - if snd oname <> ln then + if (mp_of_kn (snd oname)) <> ln then anomaly "Kernel and Library names do not match"; @@ -684,11 +818,11 @@ let declare_modtype interp_modtype id args mty = let base_mty = interp_modtype (Global.env()) mty in let entry = List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries base_mty in - let substobjs = get_modtype_substobjs entry in + let substobjs = get_modtype_substobjs (Global.env()) entry in (* Undo the simulated interactive building of the module type *) (* and declare the module type as a whole *) Summary.unfreeze_summaries fs; @@ -700,14 +834,14 @@ let declare_modtype interp_modtype id args mty = let rec get_module_substobjs env = function - | MEident mp -> MPmap.find mp !modtab_substobjs - | MEfunctor (mbid,mty,mexpr) -> + | MSEident mp -> MPmap.find mp !modtab_substobjs + | MSEfunctor (mbid,mty,mexpr) -> let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (subst, mbid::mbids, msid, objs) - | MEapply (mexpr, MEident mp) -> - let feb,ftb = Mod_typing.translate_mexpr env mexpr in - let ftb = Modops.scrape_modtype env ftb in - let farg_id, farg_b, fbody_b = Modops.destr_functor ftb in + | MSEapply (mexpr, MSEident mp) -> + let ftb = Mod_typing.translate_struct_entry env mexpr in + let farg_id, farg_b, fbody_b = Modops.destr_functor env + (Modops.eval_struct env ftb) in let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> @@ -717,11 +851,15 @@ let rec get_module_substobjs env = function objects (that are all non-logical objects) *) (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs) | [] -> match mexpr with - | MEident _ -> error "Application of a non-functor" + | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") - | MEapply (_,mexpr) -> + | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr - + | MSEwith (mty, With_Definition _) -> get_module_substobjs env mty + | MSEwith (mty, With_Module (idl,mp)) -> + let substobjs = get_module_substobjs env mty in + let modobjs = MPmap.find mp !modtab_substobjs in + replace_module_object idl substobjs modobjs mp let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = @@ -735,14 +873,14 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = None -> None, None | (Some (mty, true)) -> Some (List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries (interp_modtype (Global.env()) mty)), None | (Some (mty, false)) -> None, Some (List.fold_right - (fun (arg_id,arg_t) mte -> MTEfunsig(arg_id,arg_t,mte)) + (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) arg_entries (interp_modtype (Global.env()) mty)) in @@ -750,7 +888,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = None -> None | Some mexpr -> Some (List.fold_right - (fun (mbid,mte) me -> MEfunctor(mbid,mte,me)) + (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) arg_entries (interp_modexpr (Global.env()) mexpr)) in @@ -761,29 +899,136 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let env = Global.env() in let substobjs = match entry with - | {mod_entry_type = Some mte} -> get_modtype_substobjs mte + | {mod_entry_type = Some mte} -> get_modtype_substobjs env mte | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr | _ -> anomaly "declare_module: No type, no body ..." in - (* Undo the simulated interactive building of the module *) (* and declare the module as a whole *) Summary.unfreeze_summaries fs; - - let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in - let substituted = subst_substobjs dir mp substobjs in - - ignore (add_leaf - id - (in_module (Some (entry, mty_sub_o), substobjs, substituted))) - + match entry with + |{mod_entry_type = None; + mod_entry_expr = Some (MSEident mp) } -> + let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let substituted = subst_substobjs dir mp substobjs in + ignore (add_leaf + id + (in_module_alias (Some (entry, mty_sub_o), substobjs, substituted))) + | _ -> + let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in + let substituted = subst_substobjs dir mp substobjs in + ignore (add_leaf + id + (in_module (Some (entry, mty_sub_o), substobjs, substituted))) + with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e +(* Include *) + +let rec subst_inc_expr subst me = + match me with + | MSEident mp -> MSEident (subst_mp subst mp) + | MSEwith (me,With_Module(idl,mp)) -> + MSEwith (subst_inc_expr subst me, + With_Module(idl,subst_mp subst mp)) + | MSEwith (me,With_Definition(idl,const))-> + let const1 = Mod_subst.from_val const in + let force = Mod_subst.force subst_mps in + MSEwith (subst_inc_expr subst me, + With_Definition(idl,force (subst_substituted + subst const1))) + | MSEapply (me1,me2) -> + MSEapply (subst_inc_expr subst me1, + subst_inc_expr subst me2) + | _ -> anomaly "You cannot Include a high-order structure" + +let lift_oname (sp,kn) = + let mp,_,_ = Names.repr_kn kn in + let dir,_ = Libnames.repr_path sp in + (dir,mp) + +let cache_include (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + Global.add_include me; + match substituted with + Some seg -> + load_objects 1 prefix seg; + open_objects 1 prefix seg; + | None -> () + +let load_include i (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + match substituted with + Some seg -> + if is_mod then + load_objects i prefix seg + else + if i = 1 then + load_objects i prefix seg + | None -> () -(*s Iterators. *) +let open_include i (oname,((me,is_mod),substobjs,substituted)) = + let dir,mp1 = lift_oname oname in + let prefix = (dir,(mp1,empty_dirpath)) in + match substituted with + Some seg -> + if is_mod then + open_objects i prefix seg + else + if i = 1 then + open_objects i prefix seg + | None -> () +let subst_include (oname,subst,((me,is_mod),substobj,_)) = + let dir,mp1 = lift_oname oname in + let (sub,mbids,msid,objs) = substobj in + let subst' = join sub subst in + let substobjs = (subst',mbids,msid,objs) in + let substituted = subst_substobjs dir mp1 substobjs in + ((subst_inc_expr subst' me,is_mod),substobjs,substituted) + +let classify_include (_,((me,is_mod),substobjs,_)) = + Substitute ((me,is_mod),substobjs,None) + +let (in_include,out_include) = + declare_object {(default_object "INCLUDE") with + cache_function = cache_include; + load_function = load_include; + open_function = open_include; + subst_function = subst_include; + classify_function = classify_include; + export_function = (fun _ -> anomaly "No modules in section!") } + +let declare_include interp_struct me_ast is_mod = + + let fs = Summary.freeze_summaries () in + + try + let env = Global.env() in + let me = interp_struct env me_ast in + let substobjs = + if is_mod then + get_module_substobjs env me + else + get_modtype_substobjs env me in + let mp1,_ = current_prefix () in + let dir = dir_of_sp (Lib.path_of_include()) in + let substituted = subst_substobjs dir mp1 substobjs in + let id = current_mod_id() in + + ignore (add_leaf id + (in_include ((me,is_mod), substobjs, substituted))) + with e -> + (* Something wrong: undo the whole process *) + Summary.unfreeze_summaries fs; raise e + + +(*s Iterators. *) + let iter_all_segments f = let _ = MPmap.iter diff --git a/library/declaremods.mli b/library/declaremods.mli index 2a491b4a6..717fddf79 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -37,12 +37,12 @@ open Lib *) val declare_module : - (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) -> + (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> 'modexpr option -> unit -val start_module : (env -> 'modtype -> module_type_entry) -> +val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> ('modtype * bool) option -> unit @@ -52,10 +52,10 @@ val end_module : identifier -> unit (*s Module types *) -val declare_modtype : (env -> 'modtype -> module_type_entry) -> +val declare_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit -val start_modtype : (env -> 'modtype -> module_type_entry) -> +val start_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> unit val end_modtype : identifier -> unit @@ -95,6 +95,10 @@ val really_import_module : module_path -> unit val import_module : bool -> module_path -> unit +(* Include *) + +val declare_include : (env -> 'struct_expr -> module_struct_entry) -> + 'struct_expr -> bool -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented @@ -110,4 +114,5 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (* For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * module_type_entry) list -> unit + (mod_bound_id * module_struct_entry) list -> unit + diff --git a/library/global.ml b/library/global.ml index 0ee5533f3..4de4029b2 100644 --- a/library/global.ml +++ b/library/global.ml @@ -73,6 +73,8 @@ let add_constraints c = global_env := add_constraints c !global_env let set_engagement c = global_env := set_engagement c !global_env +let add_include me = global_env := add_include me !global_env + let start_module id = let l = label_of_id id in let mp,newenv = start_module l !global_env in diff --git a/library/global.mli b/library/global.mli index 8633dba76..71617f5a1 100644 --- a/library/global.mli +++ b/library/global.mli @@ -50,7 +50,7 @@ val add_mind : dir_path -> identifier -> mutual_inductive_entry -> kernel_name val add_module : identifier -> module_entry -> module_path -val add_modtype : identifier -> module_type_entry -> kernel_name +val add_modtype : identifier -> module_struct_entry -> module_path val add_constraints : constraints -> unit @@ -64,13 +64,14 @@ val set_engagement : engagement -> unit of the started module / module type *) val start_module : identifier -> module_path -val end_module : identifier -> module_type_entry option -> module_path +val end_module : identifier -> module_struct_entry option -> module_path -val add_module_parameter : mod_bound_id -> module_type_entry -> unit +val add_module_parameter : mod_bound_id -> module_struct_entry -> unit val start_modtype : identifier -> module_path -val end_modtype : identifier -> kernel_name +val end_modtype : identifier -> module_path +val add_include : module_struct_entry -> unit (* Queries *) val lookup_named : variable -> named_declaration @@ -78,7 +79,7 @@ val lookup_constant : constant -> constant_body val lookup_inductive : inductive -> mutual_inductive_body * one_inductive_body val lookup_mind : mutual_inductive -> mutual_inductive_body val lookup_module : module_path -> module_body -val lookup_modtype : kernel_name -> module_type_body +val lookup_modtype : module_path -> module_type_body (* Compiled modules *) val start_library : dir_path -> module_path diff --git a/library/lib.ml b/library/lib.ml index 8fff32e1a..de2047dbd 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -98,11 +98,15 @@ let library_dp () = module path and relative section path *) let path_prefix = ref initial_prefix - let cwd () = fst !path_prefix let make_path id = Libnames.make_path (cwd ()) id +let path_of_include () = + let dir = Names.repr_dirpath (cwd ()) in + let new_dir = List.tl dir in + let id = List.hd dir in + Libnames.make_path (Names.make_dirpath new_dir) id let current_prefix () = snd !path_prefix @@ -236,12 +240,25 @@ let add_frozen_state () = (* Modules. *) + let is_something_opened = function (_,OpenedSection _) -> true | (_,OpenedModule _) -> true | (_,OpenedModtype _) -> true | _ -> false + +let current_mod_id () = + try match find_entry_p is_something_opened with + | oname,OpenedModule (_,_,nametab) -> + basename (fst oname) + | oname,OpenedModtype (_,nametab) -> + basename (fst oname) + | _ -> error "you are not in a module" + with Not_found -> + error "no opened modules" + + let start_module export id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in let prefix = dir,(mp,empty_dirpath) in @@ -586,7 +603,8 @@ let reset_name (loc,id) = let is_mod_node = function | OpenedModule _ | OpenedModtype _ | OpenedSection _ | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true - | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + || t = "MODULE ALIAS" | _ -> false (* Reset on a module or section name in order to bypass constants with diff --git a/library/lib.mli b/library/lib.mli index f13ff82ae..570685585 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -88,6 +88,7 @@ val contents_after : object_name option -> library_segment (* User-side names *) val cwd : unit -> dir_path val make_path : identifier -> section_path +val path_of_include : unit -> section_path (* Kernel-side names *) val current_prefix : unit -> module_path * dir_path @@ -101,7 +102,7 @@ val sections_depth : unit -> int (* Are we inside an opened module type *) val is_modtype : unit -> bool val is_module : unit -> bool - +val current_mod_id : unit -> module_ident (* Returns the most recent OpenedThing node *) val what_is_opened : unit -> object_name * node diff --git a/library/nametab.ml b/library/nametab.ml index 9aab07cac..536c9605a 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -263,9 +263,11 @@ type ccitab = extended_global_reference SpTab.t let the_ccitab = ref (SpTab.empty : ccitab) type kntab = kernel_name SpTab.t -let the_modtypetab = ref (SpTab.empty : kntab) let the_tactictab = ref (SpTab.empty : kntab) +type mptab = module_path SpTab.t +let the_modtypetab = ref (SpTab.empty : mptab) + type objtab = unit SpTab.t let the_objtab = ref (SpTab.empty : objtab) @@ -299,8 +301,10 @@ let the_globrevtab = ref (Globrevtab.empty : globrevtab) type mprevtab = dir_path MPmap.t let the_modrevtab = ref (MPmap.empty : mprevtab) +type mptrevtab = section_path MPmap.t +let the_modtyperevtab = ref (MPmap.empty : mptrevtab) + type knrevtab = section_path KNmap.t -let the_modtyperevtab = ref (KNmap.empty : knrevtab) let the_tacticrevtab = ref (KNmap.empty : knrevtab) @@ -328,7 +332,7 @@ let push = push_cci let push_modtype vis sp kn = the_modtypetab := SpTab.push vis sp kn !the_modtypetab; - the_modtyperevtab := KNmap.add kn sp !the_modtyperevtab + the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab (* This is for tactic definition names *) @@ -483,7 +487,7 @@ let shortest_qualid_of_module mp = DirTab.shortest_qualid Idset.empty dir !the_dirtab let shortest_qualid_of_modtype kn = - let sp = KNmap.find kn !the_modtyperevtab in + let sp = MPmap.find kn !the_modtyperevtab in SpTab.shortest_qualid Idset.empty sp !the_modtypetab let shortest_qualid_of_tactic kn = @@ -504,6 +508,7 @@ let inductive_of_reference r = user_err_loc (loc_of_reference r,"global_inductive", pr_reference r ++ spc () ++ str "is not an inductive type") + (********************************************************************) (********************************************************************) @@ -520,10 +525,11 @@ let init () = the_tactictab := SpTab.empty; the_globrevtab := Globrevtab.empty; the_modrevtab := MPmap.empty; - the_modtyperevtab := KNmap.empty; + the_modtyperevtab := MPmap.empty; the_tacticrevtab := KNmap.empty + let freeze () = !the_ccitab, !the_dirtab, diff --git a/library/nametab.mli b/library/nametab.mli index 66de6a708..eab86db1d 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -73,7 +73,7 @@ type visibility = Until of int | Exactly of int val push : visibility -> section_path -> global_reference -> unit val push_syntactic_definition : visibility -> section_path -> kernel_name -> unit -val push_modtype : visibility -> section_path -> kernel_name -> unit +val push_modtype : visibility -> section_path -> module_path -> unit val push_dir : visibility -> dir_path -> global_dir_reference -> unit val push_object : visibility -> section_path -> unit val push_tactic : visibility -> section_path -> kernel_name -> unit @@ -106,7 +106,7 @@ val locate_obj : qualid -> section_path val locate_constant : qualid -> constant val locate_mind : qualid -> mutual_inductive val locate_section : qualid -> dir_path -val locate_modtype : qualid -> kernel_name +val locate_modtype : qualid -> module_path val locate_syntactic_definition : qualid -> kernel_name type ltac_constant = kernel_name @@ -161,7 +161,7 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds Coq.A.B.x that denotes the same object. *) val shortest_qualid_of_module : module_path -> qualid -val shortest_qualid_of_modtype : kernel_name -> qualid +val shortest_qualid_of_modtype : module_path -> qualid (* diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index dd9dbb8e6..2ffa30526 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -384,7 +384,9 @@ GEXTEND Gram filename = ne_string -> VernacRequireFrom (export, specif, filename) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) - | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) ] ] + | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) + | IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr)) + | IDENT "Include"; IDENT "Type"; expr = module_type -> VernacInclude(CIMTE(expr)) ] ] ; export_token: [ [ IDENT "Import" -> Some false @@ -415,12 +417,13 @@ GEXTEND Gram (* Module expressions *) module_expr: - [ [ qid = qualid -> CMEident qid - | me1 = module_expr; me2 = module_expr -> CMEapply (me1,me2) - | "("; me = module_expr; ")" -> me -(* ... *) + [ [ me = module_expr_atom -> me + | me1 = module_expr; me2 = module_expr_atom -> CMEapply (me1,me2) ] ] ; + module_expr_atom: + [ [ qid = qualid -> CMEident qid | "("; me = module_expr; ")" -> me ] ] + ; with_declaration: [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> CWith_Definition (fqid,c) @@ -431,8 +434,9 @@ GEXTEND Gram module_type: [ [ qid = qualid -> CMTEident qid (* ... *) - | mty = module_type; "with"; decl = with_declaration -> - CMTEwith (mty,decl) ] ] + | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) + | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl) + ] ] ; END diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 96b2a7167..7e7ea7c56 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -222,6 +222,18 @@ let rec pr_module_type pr_c = function let m = pr_module_type pr_c mty in let p = pr_with_declaration pr_c decl in m ++ spc() ++ str"with" ++ spc() ++ p + | CMTEapply (fexpr,mexpr)-> + let f = pr_module_type pr_c fexpr in + let m = pr_module_expr mexpr in + f ++ spc () ++ m + +and pr_module_expr = function + | CMEident qid -> pr_located pr_qualid qid + | CMEapply (me1,(CMEident _ as me2)) -> + pr_module_expr me1 ++ spc() ++ pr_module_expr me2 + | CMEapply (me1,me2) -> + pr_module_expr me1 ++ spc() ++ + hov 1 (str"(" ++ pr_module_expr me2 ++ str")") let pr_of_module_type prc (mty,b) = str (if b then ":" else "<:") ++ @@ -254,14 +266,6 @@ let pr_module_binders l pr_c = let pr_module_binders_list l pr_c = pr_module_binders l pr_c -let rec pr_module_expr = function - | CMEident qid -> pr_located pr_qualid qid - | CMEapply (me1,(CMEident _ as me2)) -> - pr_module_expr me1 ++ spc() ++ pr_module_expr me2 - | CMEapply (me1,me2) -> - pr_module_expr me1 ++ spc() ++ - hov 1 (str"(" ++ pr_module_expr me2 ++ str")") - let pr_type_option pr_c = function | CHole (loc, k) -> mt() | _ as c -> brk(0,2) ++ str":" ++ pr_c c @@ -721,19 +725,28 @@ let rec pr_vernac = function | VernacDefineModule (export,m,bl,ty,bd) -> let b = pr_module_binders_list bl pr_lconstr in hov 2 (str"Module" ++ spc() ++ pr_require_token export ++ - pr_lident m ++ b ++ - pr_opt (pr_of_module_type pr_lconstr) ty ++ - pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd) + pr_lident m ++ b ++ + pr_opt (pr_of_module_type pr_lconstr) ty ++ + pr_opt (fun me -> str ":= " ++ pr_module_expr me) bd) | VernacDeclareModule (export,id,bl,m1) -> let b = pr_module_binders_list bl pr_lconstr in - hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++ + hov 2 (str"Declare Module" ++ spc() ++ pr_require_token export ++ pr_lident id ++ b ++ pr_of_module_type pr_lconstr m1) | VernacDeclareModuleType (id,bl,m) -> let b = pr_module_binders_list bl pr_lconstr in - hov 2 (str"Module Type " ++ pr_lident id ++ b ++ - pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m) - + hov 2 (str"Module Type " ++ pr_lident id ++ b ++ + pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m) + | VernacInclude (in_ast) -> + begin + match in_ast with + | CIMTE mty -> + hov 2 (str"Include" ++ + (fun mt -> str " " ++ pr_module_type pr_lconstr mt) mty) + | CIME mexpr -> + hov 2 (str"Include" ++ + (fun me -> str " " ++ pr_module_expr me) mexpr) + end (* Solving *) | VernacSolve (i,tac,deftac) -> (if i = 1 then mt() else int i ++ str ": ") ++ diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 6fe4d80d4..6712af8b9 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -39,7 +39,7 @@ type object_pr = { print_section_variable : variable -> std_ppcmds; print_syntactic_def : kernel_name -> std_ppcmds; print_module : bool -> Names.module_path -> std_ppcmds; - print_modtype : kernel_name -> std_ppcmds; + print_modtype : module_path -> std_ppcmds; print_named_decl : identifier * constr option * types -> std_ppcmds; print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; @@ -175,7 +175,7 @@ type logical_name = | Term of global_reference | Dir of global_dir_reference | Syntactic of kernel_name - | ModuleType of qualid * kernel_name + | ModuleType of qualid * module_path | Undefined of qualid let locate_any_name ref = @@ -421,7 +421,8 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = let (mp,_,l) = repr_kn kn in Some (print_module with_values (MPdot (mp,l))) | (_,"MODULE TYPE") -> - Some (print_modtype kn) + let (mp,_,l) = repr_kn kn in + Some (print_modtype (MPdot (mp,l))) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None (* To deal with forgotten cases... *) @@ -560,7 +561,9 @@ let print_full_pure_context () = print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | "MODULE TYPE" -> (* TODO: make it reparsable *) - print_modtype kn ++ str "." ++ fnl () ++ fnl () + (* TODO: make it reparsable *) + let (mp,_,l) = repr_kn kn in + print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _ -> mt () in prec rest ++ pp | _::rest -> prec rest diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 35e23d923..c6478376d 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -74,7 +74,7 @@ type object_pr = { print_section_variable : variable -> std_ppcmds; print_syntactic_def : kernel_name -> std_ppcmds; print_module : bool -> Names.module_path -> std_ppcmds; - print_modtype : kernel_name -> std_ppcmds; + print_modtype : module_path -> std_ppcmds; print_named_decl : identifier * constr option * types -> std_ppcmds; print_leaf_entry : bool -> Libnames.object_name * Libobject.obj -> Pp.std_ppcmds; print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; diff --git a/parsing/printmod.ml b/parsing/printmod.ml index aaf4a662b..69c596093 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -42,11 +42,13 @@ let print_kn locals kn = pr_qualid qid with Not_found -> - let (mp,_,l) = repr_kn kn in - print_local_modpath locals mp ++ str"." ++ pr_lab l + try + print_local_modpath locals kn + with + Not_found -> print_modpath locals kn let rec flatten_app mexpr l = match mexpr with - | MEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l) + | SEBapply (mexpr,marg,_) -> flatten_app mexpr (marg::l) | mexpr -> mexpr::l let rec print_module name locals with_body mb = @@ -57,58 +59,80 @@ let rec print_module name locals with_body mb = spc () ++ str ":= " ++ print_modexpr locals mexpr | Some mp, _, _ -> str " == " ++ print_modpath locals mp in - hv 2 (str "Module " ++ name ++ spc () ++ str": " ++ - print_modtype locals mb.mod_type ++ body) - -and print_modtype locals mty = match mty with - | MTBident kn -> print_kn locals kn - | MTBfunsig (mbid,mtb1,mtb2) -> -(* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env - in *) - let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in - hov 2 (str "Funsig" ++ spc () ++ str "(" ++ - pr_id (id_of_mbid mbid) ++ str " : " ++ print_modtype locals mtb1 ++ - str ")" ++ spc() ++ print_modtype locals' mtb2) - | MTBsig (msid,sign) -> + let modtype = match mb.mod_type with + None -> str "" + | Some t -> str": " ++ + print_modtype locals t + in + hv 2 (str "Module " ++ name ++ spc () ++ modtype ++ body) + +and print_modtype locals mty = + match mty with + | SEBident kn -> print_kn locals kn + | SEBfunctor (mbid,mtb1,mtb2) -> + (* let env' = Modops.add_module (MPbid mbid) + (Modops.body_of_type mtb) env + in *) + let locals' = (mbid, get_new_id locals (id_of_mbid mbid)) + ::locals in + hov 2 (str "Funsig" ++ spc () ++ str "(" ++ + pr_id (id_of_mbid mbid) ++ str " : " ++ + print_modtype locals mtb1 ++ + str ")" ++ spc() ++ print_modtype locals' mtb2) + | SEBstruct (msid,sign) -> hv 2 (str "Sig" ++ spc () ++ print_sig locals msid sign ++ brk (1,-2) ++ str "End") + | SEBapply (mexpr,marg,_) -> + let lapp = flatten_app mexpr [marg] in + let fapp = List.hd lapp in + let mapp = List.tl lapp in + hov 3 (str"(" ++ (print_modtype locals fapp) ++ spc () ++ + prlist_with_sep spc (print_modexpr locals) mapp ++ str")") + | SEBwith(seb,With_definition_body(idl,cb))-> + let s = (String.concat "." (List.map string_of_id idl)) in + hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ + str "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) + | SEBwith(seb,With_module_body(idl,mp,_))-> + let s =(String.concat "." (List.map string_of_id idl)) in + hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ + str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) and print_sig locals msid sign = let print_spec (l,spec) = (match spec with - | SPBconst {const_body=Some _; const_opaque=false} -> str "Definition " - | SPBconst {const_body=None} - | SPBconst {const_opaque=true} -> str "Parameter " - | SPBmind _ -> str "Inductive " - | SPBmodule _ -> str "Module " - | SPBmodtype _ -> str "Module Type ") ++ str (string_of_label l) + | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition " + | SFBconst {const_body=None} + | SFBconst {const_opaque=true} -> str "Parameter " + | SFBmind _ -> str "Inductive " + | SFBmodule _ -> str "Module " + | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_spec sign and print_struct locals msid struc = let print_body (l,body) = (match body with - | SEBconst {const_body=Some _; const_opaque=false} -> str "Definition " - | SEBconst {const_body=Some _; const_opaque=true} -> str "Theorem " - | SEBconst {const_body=None} -> str "Parameter " - | SEBmind _ -> str "Inductive " - | SEBmodule _ -> str "Module " - | SEBmodtype _ -> str "Module Type ") ++ str (string_of_label l) + | SFBconst {const_body=Some _; const_opaque=false} -> str "Definition " + | SFBconst {const_body=Some _; const_opaque=true} -> str "Theorem " + | SFBconst {const_body=None} -> str "Parameter " + | SFBmind _ -> str "Inductive " + | SFBmodule _ -> str "Module " + | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_body struc and print_modexpr locals mexpr = match mexpr with - | MEBident mp -> print_modpath locals mp - | MEBfunctor (mbid,mty,mexpr) -> + | SEBident mp -> print_modpath locals mp + | SEBfunctor (mbid,mty,mexpr) -> (* let env' = Modops.add_module (MPbid mbid) (Modops.body_of_type mtb) env in *) let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in hov 2 (str "Functor" ++ spc() ++ str"[" ++ pr_id(id_of_mbid mbid) ++ str ":" ++ print_modtype locals mty ++ str "]" ++ spc () ++ print_modexpr locals' mexpr) - | MEBstruct (msid, struc) -> + | SEBstruct (msid, struc) -> hv 2 (str "Struct" ++ spc () ++ print_struct locals msid struc ++ brk (1,-2) ++ str "End") - | MEBapply (mexpr,marg,_) -> + | SEBapply (mexpr,marg,_) -> let lapp = flatten_app mexpr [marg] in hov 3 (str"(" ++ prlist_with_sep spc (print_modexpr locals) lapp ++ str")") - + | SEBwith (_,_)-> anomaly "Not avaible yet" let rec printable_body dir = @@ -128,6 +152,8 @@ let print_module with_body mp = print_module name [] with_body (Global.lookup_module mp) ++ fnl () let print_modtype kn = + let mtb = match Global.lookup_modtype kn with + | mtb,_ -> mtb in let name = print_kn [] kn in - str "Module Type " ++ name ++ str " = " ++ - print_modtype [] (Global.lookup_modtype kn) ++ fnl () + str "Module Type " ++ name ++ str " = " ++ + print_modtype [] mtb ++ fnl () diff --git a/parsing/printmod.mli b/parsing/printmod.mli index 2df0581c4..a3a16e8ec 100644 --- a/parsing/printmod.mli +++ b/parsing/printmod.mli @@ -14,4 +14,4 @@ val printable_body : dir_path -> bool val print_module : bool -> module_path -> std_ppcmds -val print_modtype : kernel_name -> std_ppcmds +val print_modtype : module_path -> std_ppcmds diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index f94ed6423..009d7fc35 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,7 +1,7 @@ -TrM.A = M.A +TrM.A = N.A : Set -OpM.A = M.A +OpM.A = N.A : Set -TrM.B = M.B +TrM.B = N.B : Set *** [ OpM.B : Set ] diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fed36d004..ec60cc52e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -470,10 +470,17 @@ let vernac_end_modtype id = if_verbose message ("Module Type "^ string_of_id id ^" is defined") - +let vernac_include = function + | CIMTE mty_ast -> + Declaremods.declare_include Modintern.interp_modtype mty_ast false + | CIME mexpr_ast -> + Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true + + + (**********************) (* Gallina extensions *) - + let vernac_record struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) @@ -1198,7 +1205,8 @@ let interp c = match c with vernac_define_module export id bl mtyo mexpro | VernacDeclareModuleType ((_,id),bl,mtyo) -> vernac_declare_module_type id bl mtyo - + | VernacInclude (in_ast) -> + vernac_include in_ast (* Gallina extensions *) | VernacBeginSection (_,id) -> vernac_begin_section id diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 3571b121b..cf7fb72c6 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -249,6 +249,7 @@ type vernac_expr = module_binder list * (module_type_ast * bool) option * module_ast option | VernacDeclareModuleType of lident * module_binder list * module_type_ast option + | VernacInclude of include_ast (* Solving *) |