diff options
| -rw-r--r-- | interp/topconstr.ml | 5 | ||||
| -rw-r--r-- | interp/topconstr.mli | 5 | ||||
| -rw-r--r-- | library/declaremods.ml | 320 | ||||
| -rw-r--r-- | library/declaremods.mli | 13 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 31 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 20 | ||||
| -rw-r--r-- | plugins/interface/ascent.mli | 2 | ||||
| -rw-r--r-- | plugins/interface/vtp.ml | 6 | ||||
| -rw-r--r-- | plugins/interface/xlate.ml | 21 | ||||
| -rw-r--r-- | theories/Structures/DecidableType2.v | 35 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 19 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 6 |
12 files changed, 252 insertions, 231 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 12ce52d1b..a6b4b1b0a 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1001,7 +1001,6 @@ type with_declaration_ast = | CWith_Module of identifier list located * qualid located | CWith_Definition of identifier list located * constr_expr - type module_ast = | CMEident of qualid located | CMEapply of module_ast * module_ast @@ -1015,6 +1014,10 @@ type include_ast = | CIMTE of module_type_ast * module_type_ast list | CIME of module_ast * module_ast list +type 'a module_signature = + | Enforce of 'a (* ... : T *) + | Check of 'a list (* ... <: T1 <: T2, possibly empty *) + let loc_of_notation f loc (args,_) ntn = if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc) else snd (Util.unloc (f (List.hd args))) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 1b6514a65..1c0b207ea 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -245,7 +245,6 @@ type with_declaration_ast = | CWith_Module of identifier list located * qualid located | CWith_Definition of identifier list located * constr_expr - type module_ast = | CMEident of qualid located | CMEapply of module_ast * module_ast @@ -259,5 +258,9 @@ type include_ast = | CIMTE of module_type_ast * module_type_ast list | CIME of module_ast * module_ast list +type 'a module_signature = + | Enforce of 'a (* ... : T *) + | Check of 'a list (* ... <: T1 <: T2, possibly empty *) + val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int diff --git a/library/declaremods.ml b/library/declaremods.ml index 42d3652aa..0ed617a0b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -77,10 +77,10 @@ let modtab_objects = (* currently started interactive module (if any) - its arguments (if it is a functor) and declared output type *) -let openmod_info = - ref ((MPfile(initial_dir),[],None,None) - : module_path * mod_bound_id list * module_struct_entry option - * module_type_body option) +let openmod_info = + ref ((MPfile(initial_dir),[],None,[]) + : module_path * mod_bound_id list * module_struct_entry option + * module_type_body list) (* The library_cache here is needed to avoid recalculations of substituted modules object during "reloading" of libraries *) @@ -101,7 +101,7 @@ let _ = Summary.declare_summary "MODULE-INFO" modtab_substobjs := MPmap.empty; modtab_objects := MPmap.empty; openmod_info := ((MPfile(initial_dir), - [],None,None)); + [],None,[])); library_cache := Dirmap.empty) } (* auxiliary functions to transform full_path and kernel_name given @@ -118,17 +118,58 @@ let dir_of_sp sp = let dir,id = repr_path sp in add_dirpath_suffix dir id +(* Subtyping checks *) + +let check_sub mtb sub_mtb_l = + (* The constraints are checked and forgot immediately : *) + ignore (List.fold_right + (fun sub_mtb env -> + Environ.add_constraints + (Subtyping.check_subtypes env mtb sub_mtb) env) + sub_mtb_l (Global.env())) (* 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 = + a subtype of all signatures in [sub_mtb_l]. Uses only the global + environment. *) + +let check_subtypes mp sub_mtb_l = let env = Global.env () in let mb = Environ.lookup_module mp env in let mtb = Modops.module_type_of_module env None mb in - let _ = Environ.add_constraints - (Subtyping.check_subtypes env mtb sub_mtb) - in - () (* The constraints are checked and forgot immediately! *) + check_sub mtb sub_mtb_l + +(* Same for module type [mp] *) + +let check_subtypes_mt mp sub_mtb_l = + check_sub (Environ.lookup_modtype mp (Global.env())) sub_mtb_l + +(* Create a functor type entry *) + +let funct_entry args m = + List.fold_right + (fun (arg_id,arg_t) mte -> MSEfunctor (arg_id,arg_t,mte)) + args m + +(* Prepare the module type list for check of subtypes *) + +let build_subtypes interp_modtype mp args mtys = + List.map + (fun m -> + let mte = interp_modtype (Global.env()) m in + let mtb = Mod_typing.translate_module_type (Global.env()) mp mte in + let funct_mtb = + List.fold_right + (fun (arg_id,arg_t) mte -> + let arg_t = + Mod_typing.translate_module_type (Global.env()) + (MPbound arg_id) arg_t + in + SEBfunctor(arg_id,arg_t,mte)) + args mtb.typ_expr + in + { mtb with typ_expr = funct_mtb }) + mtys + (* These functions register the visibility of the module and iterates through its components. They are called by plenty module functions *) @@ -266,7 +307,7 @@ let modtypetab = (* currently started interactive module type. We remember its arguments if it is a functor type *) let openmodtype_info = - ref ([] : mod_bound_id list) + ref ([],[] : mod_bound_id list * module_type_body list) let _ = Summary.declare_summary "MODTYPE-INFO" { Summary.freeze_function = (fun () -> @@ -276,30 +317,35 @@ let _ = Summary.declare_summary "MODTYPE-INFO" openmodtype_info := snd ft); Summary.init_function = (fun () -> modtypetab := MPmap.empty; - openmodtype_info := []) } + openmodtype_info := [],[]) } + +let cache_modtype ((sp,kn),(entry,modtypeobjs,sub_mty_l)) = + let mp = mp_of_kn kn in -let cache_modtype ((sp,kn),(entry,modtypeobjs)) = let _ = match entry with | None -> anomaly "You must not recache interactive module types!" | Some mte -> - let mp = Global.add_modtype (basename sp) mte in - if mp <>mp_of_kn kn then + if mp <> Global.add_modtype (basename sp) mte then anomaly "Kernel and Library names do not match" in + (* Using declare_modtype should lead here, where we check + that any given subtyping is indeed accurate *) + check_subtypes_mt mp sub_mty_l; + if Nametab.exists_modtype sp then errorlabstrm "cache_modtype" (pr_path sp ++ str " already exists") ; - Nametab.push_modtype (Nametab.Until 1) sp (mp_of_kn kn); + Nametab.push_modtype (Nametab.Until 1) sp mp; - modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab + modtypetab := MPmap.add mp modtypeobjs !modtypetab -let load_modtype i ((sp,kn),(entry,modtypeobjs)) = +let load_modtype i ((sp,kn),(entry,modtypeobjs,_)) = check_empty "load_modtype" entry; if Nametab.exists_modtype sp then @@ -311,7 +357,7 @@ let load_modtype i ((sp,kn),(entry,modtypeobjs)) = modtypetab := MPmap.add (mp_of_kn kn) modtypeobjs !modtypetab -let open_modtype i ((sp,kn),(entry,_)) = +let open_modtype i ((sp,kn),(entry,_,_)) = check_empty "open_modtype" entry; if @@ -323,13 +369,13 @@ let open_modtype i ((sp,kn),(entry,_)) = Nametab.push_modtype (Nametab.Exactly i) sp (mp_of_kn kn) -let subst_modtype (subst,(entry,(mbids,mp,objs))) = +let subst_modtype (subst,(entry,(mbids,mp,objs),_)) = check_empty "subst_modtype" entry; - (entry,(mbids,subst_mp subst mp,subst_objects subst objs)) + (entry,(mbids,subst_mp subst mp,subst_objects subst objs),[]) -let classify_modtype (_,substobjs) = - Substitute (None,substobjs) +let classify_modtype (_,substobjs,_) = + Substitute (None,substobjs,[]) let (in_modtype,_) = @@ -448,36 +494,19 @@ let intern_args interp_modtype (idl,arg) = (mbid,mty)) dirs mbids -let start_module interp_modtype export id args res_o = - let fs = Summary.freeze_summaries () in +let start_module_ interp_modtype export id args res fs = let mp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - let res_entry_o, sub_body_o = match res_o with - None -> None, None - | Some (res, restricted) -> - (* we translate the module here to catch errors as early as possible *) + let res_entry_o, sub_body_l = match res with + | Topconstr.Enforce res -> let mte = interp_modtype (Global.env()) res in - if restricted then - let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in - Some mte, None - else - let mtb = Mod_typing.translate_module_type (Global.env()) - mp mte in - let funct_mtb = - List.fold_right - (fun (arg_id,arg_t) mte -> - let arg_t = Mod_typing.translate_module_type (Global.env()) - (MPbound arg_id) arg_t - in - SEBfunctor(arg_id,arg_t,mte)) - arg_entries mtb.typ_expr - in - None, Some {mtb with - typ_expr = funct_mtb} + let _ = Mod_typing.translate_struct_type_entry (Global.env()) mte in + Some mte, [] + | Topconstr.Check resl -> + None, build_subtypes interp_modtype mp arg_entries resl in - let mbids = List.map fst arg_entries in - openmod_info:=(mp,mbids,res_entry_o,sub_body_o); + openmod_info:=(mp,mbids,res_entry_o,sub_body_l); let prefix = Lib.start_module export id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModule prefix); Lib.add_frozen_state (); mp @@ -486,7 +515,7 @@ let start_module interp_modtype export id args res_o = let end_module () = let oldoname,oldprefix,fs,lib_stack = Lib.end_module () in - let mp,mbids, res_o, sub_o = !openmod_info in + let mp,mbids, res_o, sub_l = !openmod_info in let substitute, keep, special = Lib.classify_segment lib_stack in let mp_from,substobjs, keep, special = try @@ -514,10 +543,7 @@ let end_module () = let id = basename (fst oldoname) in let mp,resolver = Global.end_module fs id res_o in - begin match sub_o with - None -> () - | Some sub_mtb -> check_subtypes mp sub_mtb - end; + check_subtypes mp sub_l; (* we substitute objects if the module is sealed by a signature (ie. mp_from != None *) @@ -581,7 +607,7 @@ let register_library dir cenv objs digest = let start_library dir = let mp = Global.start_library dir in - openmod_info:=mp,[],None,None; + openmod_info:=mp,[],None,[]; Lib.start_compilation dir mp; Lib.add_frozen_state () @@ -630,14 +656,13 @@ let import_module export mp = (************************************************************************) (* module types *) -let start_modtype interp_modtype id args = - let fs = Summary.freeze_summaries () in +let start_modtype_ interp_modtype id args mtys fs = let mp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - + let sub_mty_l = build_subtypes interp_modtype mp arg_entries mtys in let mbids = List.map fst arg_entries in - openmodtype_info := mbids; + openmodtype_info := mbids, sub_mty_l; let prefix = Lib.start_modtype id mp fs in Nametab.push_dir (Nametab.Until 1) (fst prefix) (DirOpenModtype prefix); Lib.add_frozen_state (); mp @@ -647,11 +672,12 @@ let end_modtype () = let oldoname,prefix,fs,lib_stack = Lib.end_modtype () in let id = basename (fst oldoname) in let substitute, _, special = Lib.classify_segment lib_stack in - let mbids = !openmodtype_info in + let mbids, sub_mty_l = !openmodtype_info in let mp = Global.end_modtype fs id in - let modtypeobjs = mbids, mp, substitute in - let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs)]) in - + let modtypeobjs = mbids, mp, substitute in + check_subtypes_mt mp sub_mty_l; + let oname = Lib.add_leaves id (special@[in_modtype (None, modtypeobjs,[])]) + in if fst oname <> fst oldoname then anomaly "Section paths generated on start_ and end_modtype do not match"; @@ -663,32 +689,23 @@ let end_modtype () = mp -let declare_modtype_real interp_modtype id args mty = - let fs = Summary.freeze_summaries () in - - try +let declare_modtype_ interp_modtype id args mtys mty fs = let mmp = Global.start_modtype id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - - let base_mty = interp_modtype (Global.env()) mty in - let entry = - List.fold_right - (fun (arg_id,arg_t) mte -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries - base_mty - in + let entry = funct_entry arg_entries (interp_modtype (Global.env()) mty) in + (* NB: check of subtyping will be done in cache_modtype *) + let sub_mty_l = build_subtypes interp_modtype mmp arg_entries mtys in let (mbids,mp_from,objs) = get_modtype_substobjs (Global.env()) mmp entry in - (* Undo the simulated interactive building of the module type *) - (* and declare the module type as a whole *) + (* Undo the simulated interactive building of the module type *) + (* and declare the module type as a whole *) let substobjs = (mbids,mmp, - subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) in - Summary.unfreeze_summaries fs; - ignore (add_leaf id (in_modtype (Some entry, substobjs))); - mmp - with e -> - (* Something wrong: undo the whole process *) - Summary.unfreeze_summaries fs; raise e + subst_objects (map_mp mp_from mmp empty_delta_resolver) objs) + in + Summary.unfreeze_summaries fs; + ignore (add_leaf id (in_modtype (Some entry, substobjs, sub_mty_l))); + mmp + (* Small function to avoid module typing during substobjs retrivial *) let rec get_objs_module_application env = function @@ -824,36 +841,16 @@ let rec update_include (mbids,mp,objs) = in (mbids,mp,replace_include objs) -let declare_module_real interp_modtype interp_modexpr id args mty_o mexpr_o = - - let fs = Summary.freeze_summaries () in - - try +let declare_module_ interp_modtype interp_modexpr id args res mexpr_o fs = let mmp = Global.start_module id in let arg_entries = List.concat (List.map (intern_args interp_modtype) args) in - let mty_entry_o, mty_sub_o = match mty_o with - None -> None, None - | (Some (mty, true)) -> - Some (List.fold_right - (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 -> MSEfunctor(arg_id,arg_t,mte)) - arg_entries - (interp_modtype (Global.env()) mty)) + let funct f m = funct_entry arg_entries (f (Global.env ()) m) in + let mty_entry_o, mty_sub_l = match res with + | Topconstr.Enforce mty -> Some (funct interp_modtype mty), [] + | Topconstr.Check mtys -> None, List.map (funct interp_modtype) mtys in - let mexpr_entry_o = match mexpr_o with - None -> None - | Some mexpr -> - Some (List.fold_right - (fun (mbid,mte) me -> MSEfunctor(mbid,mte,me)) - arg_entries - (interp_modexpr (Global.env()) mexpr)) in + let mexpr_entry_o = Option.map (funct interp_modexpr) mexpr_o in let entry = {mod_entry_type = mty_entry_o; mod_entry_expr = mexpr_entry_o } @@ -866,30 +863,23 @@ let declare_module_real interp_modtype interp_modexpr id args mty_o mexpr_o = | _ -> anomaly "declare_module: No type, no body ..." in let (mbids,mp_from,objs) = update_include substobjs 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 mp_env,resolver = Global.add_module id entry in - let _ = if mp_env <> mp then - anomaly "Kernel and Library names do not match"; - match mty_sub_o with - | None -> () - | Some sub_mte -> - let sub_mtb = Mod_typing.translate_module_type - env mp sub_mte in - check_subtypes mp_env sub_mtb - in - let substobjs = (mbids,mp_env, - subst_objects(map_mp mp_from mp_env resolver) objs) in - ignore (add_leaf - id - (in_module (Some (entry, mty_sub_o), substobjs))); - mmp - - with e -> - (* Something wrong: undo the whole process *) - Summary.unfreeze_summaries fs; raise e + (* 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 mp_env,resolver = Global.add_module id entry in + + if mp_env <> mp then anomaly "Kernel and Library names do not match"; + + let subs = List.map (Mod_typing.translate_module_type env mp) mty_sub_l in + check_subtypes mp subs; + + let substobjs = (mbids,mp_env, + subst_objects(map_mp mp_from mp_env resolver) objs) in + ignore (add_leaf + id + (in_module (Some (entry), substobjs))); + mmp let declare_one_include interp_struct me_ast is_mod is_self = @@ -937,33 +927,53 @@ let declare_one_include interp_struct me_ast is_mod is_self = (in_include ((me,is_mod), substobjs))) -let declare_include interp_struct me_ast me_asts is_mod is_self = +let declare_include_ interp_struct me_ast me_asts is_mod is_self = + declare_one_include interp_struct me_ast is_mod is_self; + List.iter + (fun me -> declare_one_include interp_struct me is_mod true) + me_asts + +(** Versions of earlier functions taking care of the freeze/unfreeze + of summaries *) + +let protect_summaries f = let fs = Summary.freeze_summaries () in - try - declare_one_include interp_struct me_ast is_mod is_self; - List.iter - (fun me -> declare_one_include interp_struct me is_mod true) - me_asts + try f fs with e -> (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e +let declare_include interp_struct me_ast me_asts is_mod is_self = + protect_summaries + (fun _ -> declare_include_ interp_struct me_ast me_asts is_mod is_self) + +let declare_modtype interp_mt id args mtys mty_l = + let declare_mt fs = match mty_l with + | [] -> assert false + | [mty] -> declare_modtype_ interp_mt id args mtys mty fs + | mty :: mty_l -> + ignore (start_modtype_ interp_mt id args mtys fs); + declare_include_ interp_mt mty mty_l false false; + end_modtype () + in + protect_summaries declare_mt + +let start_modtype interp_modtype id args mtys = + protect_summaries (start_modtype_ interp_modtype id args mtys) + +let declare_module interp_mt interp_me id args mtys me_l = + let declare_me fs = match me_l with + | [] -> declare_module_ interp_mt interp_me id args mtys None fs + | [me] -> declare_module_ interp_mt interp_me id args mtys (Some me) fs + | me :: me_l -> + ignore (start_module_ interp_mt None id args mtys fs); + declare_include_ interp_me me me_l true false; + end_module () + in + protect_summaries declare_me -let declare_modtype interp_mt id args = function - | [] -> assert false - | [mty] -> declare_modtype_real interp_mt id args mty - | mty :: mty_l -> - ignore (start_modtype interp_mt id args); - declare_include interp_mt mty mty_l false false; - end_modtype () - -let declare_module interp_mt interp_me id args mty_o = function - | [] -> declare_module_real interp_mt interp_me id args mty_o None - | [me] -> declare_module_real interp_mt interp_me id args mty_o (Some me) - | me :: me_l -> - ignore (start_module interp_mt None id args mty_o); - declare_include interp_me me me_l true false; - end_module () +let start_module interp_modtype export id args res = + protect_summaries (start_module_ interp_modtype export id args res) (*s Iterators. *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 3d16a287f..f20be9cd0 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -37,14 +37,16 @@ open Lib *) val declare_module : - (env -> 'modtype -> module_struct_entry) -> (env -> 'modexpr -> module_struct_entry) -> + (env -> 'modtype -> module_struct_entry) -> + (env -> 'modexpr -> module_struct_entry) -> identifier -> - (identifier located list * 'modtype) list -> ('modtype * bool) option -> + (identifier located list * 'modtype) list -> + 'modtype Topconstr.module_signature -> 'modexpr list -> module_path val start_module : (env -> 'modtype -> module_struct_entry) -> bool option -> identifier -> (identifier located list * 'modtype) list -> - ('modtype * bool) option -> module_path + 'modtype Topconstr.module_signature -> module_path val end_module : unit -> module_path @@ -54,10 +56,11 @@ val end_module : unit -> module_path val declare_modtype : (env -> 'modtype -> module_struct_entry) -> identifier -> (identifier located list * 'modtype) list -> - 'modtype list -> module_path + 'modtype list -> 'modtype list -> module_path val start_modtype : (env -> 'modtype -> module_struct_entry) -> - identifier -> (identifier located list * 'modtype) list -> module_path + identifier -> (identifier located list * 'modtype) list -> + 'modtype list -> module_path val end_modtype : unit -> module_path diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 38ab689f5..56946ef27 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -388,17 +388,16 @@ GEXTEND Gram gallina_ext: [ [ (* Interactive module declaration *) IDENT "Module"; export = export_token; id = identref; - bl = LIST0 module_binder; mty_o = OPT of_module_type; - o = OPT is_module_expr -> - VernacDefineModule (export, id, bl, mty_o, - match o with None -> [] | Some l -> l) + bl = LIST0 module_binder; sign = of_module_type; + body = is_module_expr -> + VernacDefineModule (export, id, bl, sign, body) | IDENT "Module"; "Type"; id = identref; - bl = LIST0 module_binder; o = OPT is_module_type -> - VernacDeclareModuleType (id, bl, - match o with None -> [] | Some l -> l) + bl = LIST0 module_binder; sign = check_module_types; + body = is_module_type -> + VernacDeclareModuleType (id, bl, sign, body) | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref; bl = LIST0 module_binder; ":"; mty = module_type -> - VernacDeclareModule (export, id, bl, (mty,true)) + VernacDeclareModule (export, id, bl, mty) (* Section beginning *) | IDENT "Section"; id = identref -> VernacBeginSection id | IDENT "Chapter"; id = identref -> VernacBeginSection id @@ -433,15 +432,23 @@ GEXTEND Gram ext_module_expr: [ [ "<+"; mexpr = module_expr -> mexpr ] ] ; + check_module_type: + [ [ "<:"; mty = module_type -> mty ] ] + ; + check_module_types: + [ [ mtys = LIST0 check_module_type -> mtys ] ] + ; of_module_type: - [ [ ":"; mty = module_type -> (mty, true) - | "<:"; mty = module_type -> (mty, false) ] ] + [ [ ":"; mty = module_type -> Enforce mty + | mtys = check_module_types -> Check mtys ] ] ; is_module_type: - [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l) ] ] + [ [ ":="; mty = module_type ; l = LIST0 ext_module_type -> (mty::l) + | -> [] ] ] ; is_module_expr: - [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l) ] ] + [ [ ":="; mexpr = module_expr; l = LIST0 ext_module_expr -> (mexpr::l) + | -> [] ] ] ; (* Module binder *) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 4407ca6aa..190271159 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -253,9 +253,10 @@ and pr_module_expr = function 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 "<:") ++ - pr_module_type prc mty +let pr_of_module_type prc = function + | Enforce mty -> str ":" ++ pr_module_type prc mty + | Check mtys -> + prlist_strict (fun m -> str "<:" ++ pr_module_type prc m) mtys let pr_require_token = function | Some true -> str "Export " @@ -746,24 +747,25 @@ let rec pr_vernac = function hov 1 (str"Existing" ++ spc () ++ str"Class" ++ spc () ++ pr_lident id) (* Modules and Module Types *) - | VernacDefineModule (export,m,bl,ty,bd) -> + | VernacDefineModule (export,m,bl,tys,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_of_module_type pr_lconstr tys ++ (if bd = [] then mt () else str ":= ") ++ prlist_with_sep (fun () -> str " <+ ") pr_module_expr 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 ++ pr_lident id ++ b ++ - pr_of_module_type pr_lconstr m1) - | VernacDeclareModuleType (id,bl,m) -> + pr_module_type pr_lconstr m1) + | VernacDeclareModuleType (id,bl,tyl,m) -> let b = pr_module_binders_list bl pr_lconstr in + let pr_mt = pr_module_type pr_lconstr in hov 2 (str"Module Type " ++ pr_lident id ++ b ++ + prlist_strict (fun m -> str " <: " ++ pr_mt m) tyl ++ (if m = [] then mt () else str ":= ") ++ - prlist_with_sep (fun () -> str " <+ ") - (pr_module_type pr_lconstr) m) + prlist_with_sep (fun () -> str " <+ ") pr_mt m) | VernacInclude (b,CIMTE(mty,mtys)) -> let pr_mty = pr_module_type pr_lconstr in hov 2 (str"Include " ++ str (if b then "Self " else "") ++ str "Type " ++ diff --git a/plugins/interface/ascent.mli b/plugins/interface/ascent.mli index bc615f14e..bd82688d3 100644 --- a/plugins/interface/ascent.mli +++ b/plugins/interface/ascent.mli @@ -479,7 +479,7 @@ and ct_MODULE_TYPE = | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID_LIST * ct_ID and ct_MODULE_TYPE_CHECK = CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT - | CT_only_check of ct_MODULE_TYPE + | CT_only_check of ct_MODULE_TYPE list and ct_MODULE_TYPE_OPT = CT_coerce_ID_OPT_to_MODULE_TYPE_OPT of ct_ID_OPT | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT of ct_MODULE_TYPE diff --git a/plugins/interface/vtp.ml b/plugins/interface/vtp.ml index a84f9ea56..d71336150 100644 --- a/plugins/interface/vtp.ml +++ b/plugins/interface/vtp.ml @@ -1185,9 +1185,9 @@ and fMODULE_TYPE = function fNODE "module_type_with_mod" 3 and fMODULE_TYPE_CHECK = function | CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x -| CT_only_check(x1) -> - fMODULE_TYPE x1 ++ - fNODE "only_check" 1 +| CT_only_check(l) -> + (List.fold_left (++) (mt()) (List.map fMODULE_TYPE l)) ++ + fNODE "only_check" (List.length l) and fMODULE_TYPE_OPT = function | CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT x -> fMODULE_TYPE x diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 97ab9efc8..9ba1d6715 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -1617,14 +1617,13 @@ let xlate_module_binder_list (l:module_binder list) = CT_module_binder (CT_id_ne_list(fst, idl2), xlate_module_type mty)) l);; -let xlate_module_type_check_opt = function - None -> CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK - (CT_coerce_ID_OPT_to_MODULE_TYPE_OPT ctv_ID_OPT_NONE) - | Some(mty, true) -> CT_only_check(xlate_module_type mty) - | Some(mty, false) -> +let xlate_module_type_check = function + | Topconstr.Enforce mty -> CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK (CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT - (xlate_module_type mty));; + (xlate_module_type mty)) + | Topconstr.Check mtys -> + CT_only_check (List.map xlate_module_type mtys) let rec xlate_module_expr = function CMEident (_, qid) -> CT_coerce_ID_OPT_to_MODULE_EXPR @@ -2034,7 +2033,7 @@ let rec xlate_vernac = xlate_error"TODO: Local abbreviations and abbreviations with parameters" (* Modules and Module Types *) | VernacInclude (_) -> xlate_error "TODO : Include " - | VernacDeclareModuleType((_, id), bl, mty_o) -> + | VernacDeclareModuleType((_, id), bl, _, mty_o) -> CT_module_type_decl(xlate_ident id, xlate_module_binder_list bl, match mty_o with @@ -2045,18 +2044,18 @@ let rec xlate_vernac = CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT (xlate_module_type mty1) | _ -> failwith "TODO: Include Self") - | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) -> + | VernacDefineModule(_,(_, id), bl, mtys, mexpr_o) -> CT_module(xlate_ident id, xlate_module_binder_list bl, - xlate_module_type_check_opt mty_o, + xlate_module_type_check mtys, match mexpr_o with [] -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE | [m] -> xlate_module_expr m | _ -> failwith "TODO Include Self") - | VernacDeclareModule(_,(_, id), bl, mty_o) -> + | VernacDeclareModule(_,(_, id), bl, mty) -> CT_declare_module(xlate_ident id, xlate_module_binder_list bl, - xlate_module_type_check_opt (Some mty_o), + xlate_module_type_check (Topconstr.Enforce mty), CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE) | VernacRequire (impexp, spec, id::idl) -> let ct_impexp, ct_spec = get_require_flags impexp spec in diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index 111f45ca7..afc5b9122 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -62,25 +62,25 @@ Module Type EqualityType := BareEquality <+ IsEq. Module Type EqualityTypeOrig := BareEquality <+ IsEqOrig. -Module Type EqualityTypeBoth (* <: EqualityType <: EqualityTypeOrig *) +Module Type EqualityTypeBoth <: EqualityType <: EqualityTypeOrig := BareEquality <+ IsEq <+ IsEqOrig. -Module Type DecidableType (* <: EqualityType *) +Module Type DecidableType <: EqualityType := BareEquality <+ IsEq <+ HasEqDec. -Module Type DecidableTypeOrig (* <: EqualityTypeOrig *) +Module Type DecidableTypeOrig <: EqualityTypeOrig := BareEquality <+ IsEqOrig <+ HasEqDec. -Module Type DecidableTypeBoth (* <: DecidableType <: DecidableTypeOrig *) +Module Type DecidableTypeBoth <: DecidableType <: DecidableTypeOrig := EqualityTypeBoth <+ HasEqDec. -Module Type BooleanEqualityType (* <: EqualityType *) +Module Type BooleanEqualityType <: EqualityType := BareEquality <+ IsEq <+ HasEqBool. -Module Type BooleanDecidableType (* <: DecidableType <: BooleanEqualityType *) +Module Type BooleanDecidableType <: DecidableType <: BooleanEqualityType := BareEquality <+ IsEq <+ HasEqDec <+ HasEqBool. -Module Type DecidableTypeFull (* <: all previous interfaces *) +Module Type DecidableTypeFull <: DecidableTypeBoth <: BooleanDecidableType := BareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. @@ -146,7 +146,7 @@ Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType A particular case of [DecidableType] where the equality is the usual one of Coq. *) -Module Type UsualBareEquality. (* <: BareEquality *) +Module Type UsualBareEquality <: BareEquality. Parameter Inline t : Type. Definition eq := @eq t. End UsualBareEquality. @@ -161,26 +161,22 @@ Module UsualIsEqOrig (E:UsualBareEquality) <: IsEqOrig E. Definition eq_trans := @eq_trans E.t. End UsualIsEqOrig. -Module Type UsualEqualityType (* <: EqualityType *) +Module Type UsualEqualityType <: EqualityType := UsualBareEquality <+ IsEq. -Module Type UsualDecidableType (* <: DecidableType *) +Module Type UsualDecidableType <: DecidableType := UsualBareEquality <+ IsEq <+ HasEqDec. -Module Type UsualDecidableTypeBoth (* <: DecidableTypeBoth *) +Module Type UsualDecidableTypeBoth <: DecidableTypeBoth := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec. Module Type UsualBoolEq := UsualBareEquality <+ HasEqBool. -Module Type UsualDecidableTypeFull (* <: DecidableTypeFull *) +Module Type UsualDecidableTypeFull <: DecidableTypeFull := UsualBareEquality <+ IsEq <+ IsEqOrig <+ HasEqDec <+ HasEqBool. -(** a [UsualDecidableType] is in particular an [DecidableType]. *) - -Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. - -(** Some shortcuts for easily building a UsualDecidableType *) +(** Some shortcuts for easily building a [UsualDecidableType] *) Module Type MiniDecidableType. Parameter t : Type. @@ -188,12 +184,9 @@ Module Type MiniDecidableType. End MiniDecidableType. Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth. - Include M. Definition eq := @eq M.t. - Include Self UsualIsEq. - Include Self UsualIsEqOrig. + Include M <+ UsualIsEq <+ UsualIsEqOrig. End Make_UDT. Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull := M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec. - diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 76e7eb0b8..4fcd717bb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -446,7 +446,7 @@ let vernac_import export refl = List.iter import refl; Lib.add_frozen_state () -let vernac_declare_module export (loc, id) binders_ast mty_ast_o = +let vernac_declare_module export (loc, id) binders_ast mty_ast = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -460,7 +460,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o = else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_modtype Modintern.interp_modexpr - id binders_ast (Some mty_ast_o) [] + id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is declared"); @@ -514,7 +514,7 @@ let vernac_end_module export (loc,id as lid) = if_verbose message ("Module "^ string_of_id id ^" is defined") ; Option.iter (fun export -> vernac_import export [Ident lid]) export -let vernac_declare_module_type (loc,id) binders_ast mty_ast_l = +let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then error "Modules and Module Types are not allowed inside sections."; @@ -526,7 +526,8 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_l = (fun (export,idl,ty) (args,argsexport) -> (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast ([],[]) in - let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in + let mp = Declaremods.start_modtype + Modintern.interp_modtype id binders_ast mty_sign in Dumpglob.dump_moddef loc mp "modtype"; if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); @@ -545,7 +546,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_l = "and \"Import\" keywords from every functor argument.") else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_modtype - id binders_ast mty_ast_l in + id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") @@ -1329,10 +1330,10 @@ let interp c = match c with (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> vernac_declare_module export lid bl mtyo - | VernacDefineModule (export,lid,bl,mtyo,mexprl) -> - vernac_define_module export lid bl mtyo mexprl - | VernacDeclareModuleType (lid,bl,mtyo) -> - vernac_declare_module_type lid bl mtyo + | VernacDefineModule (export,lid,bl,mtys,mexprl) -> + vernac_define_module export lid bl mtys mexprl + | VernacDeclareModuleType (lid,bl,mtys,mtyo) -> + vernac_declare_module_type lid bl mtys mtyo | VernacInclude (is_self,in_asts) -> vernac_include is_self in_asts (* Gallina extensions *) diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index ccb850651..6148b98ae 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -259,11 +259,11 @@ type vernac_expr = (* Modules and Module Types *) | VernacDeclareModule of bool option * lident * - module_binder list * (module_type_ast * bool) + module_binder list * module_type_ast | VernacDefineModule of bool option * lident * - module_binder list * (module_type_ast * bool) option * module_ast list + module_binder list * module_type_ast module_signature * module_ast list | VernacDeclareModuleType of lident * - module_binder list * module_type_ast list + module_binder list * module_type_ast list * module_type_ast list | VernacInclude of bool * include_ast (* Solving *) |