diff options
| -rw-r--r-- | kernel/safe_typing.ml | 32 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
| -rw-r--r-- | library/declaremods.ml | 42 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 2 | ||||
| -rw-r--r-- | library/global.mli | 5 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 10 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 12 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
10 files changed, 92 insertions, 28 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index b0dc6dd8a..ef2ea800c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -431,13 +431,29 @@ let end_module l restype senv = let mtb = translate_module_type senv.env senv.modinfo.modpath me in - mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta + mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta in let senv = add_constraints cst senv in let mp_sup = senv.modinfo.modpath in + (* Include Self support *) + let rec compute_sign sign mb senv = + match sign with + | SEBfunctor(mbid,mtb,str) -> + let cst_sub = check_subtypes senv.env mb mtb in + let senv = add_constraints cst_sub senv in + let mpsup_delta = complete_inline_delta_resolver senv.env mp_sup + mbid mtb mb.typ_delta in + (compute_sign + (subst_struct_expr (map_mbid mbid mp_sup mpsup_delta) str) mb senv) + | str -> str,senv + in + let sign,senv = compute_sign sign {typ_mp = mp_sup; + typ_expr = SEBstruct (List.rev senv.revstruct); + typ_expr_alg = None; + typ_constraints = Constraint.empty; + typ_delta = senv.modinfo.resolver} senv in let str = match sign with - | SEBstruct(str_l) -> - str_l + | SEBstruct(str_l) -> str_l | _ -> error ("You cannot Include a high-order structure.") in let senv = @@ -683,7 +699,15 @@ let start_library dir senv = loads = []; local_retroknowledge = [] } - +let pack_module senv = + {mod_mp=senv.modinfo.modpath; + mod_expr=None; + mod_type= SEBstruct (List.rev senv.revstruct); + mod_type_alg=None; + mod_constraints=Constraint.empty; + mod_delta=senv.modinfo.resolver; + mod_retroknowledge=[]; + } let export senv dir = let modinfo = senv.modinfo in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index f011d42b7..169fd158d 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -89,8 +89,10 @@ val end_modtype : label -> safe_environment -> module_path * safe_environment val add_include : - module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment + module_struct_entry -> bool -> safe_environment -> + delta_resolver * safe_environment +val pack_module : safe_environment -> module_body val current_modpath : safe_environment -> module_path val delta_of_senv : safe_environment -> delta_resolver*delta_resolver diff --git a/library/declaremods.ml b/library/declaremods.ml index 68ce86b3a..c40e94c51 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -750,8 +750,6 @@ let rec get_module_substobjs env mp_from = function | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from mty | MSEwith (mty, With_Module (idl,mp)) -> assert false - - (* Include *) let rec subst_inc_expr subst me = @@ -769,7 +767,8 @@ let rec subst_inc_expr subst me = | MSEapply (me1,me2) -> MSEapply (subst_inc_expr subst me1, subst_inc_expr subst me2) - | _ -> anomaly "You cannot Include a high-order structure" + | MSEfunctor(mbid,me1,me2) -> + MSEfunctor (mbid, subst_inc_expr subst me1, subst_inc_expr subst me2) let lift_oname (sp,kn) = let mp,_,_ = Names.repr_kn kn in @@ -893,19 +892,49 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = Summary.unfreeze_summaries fs; raise e -let declare_include interp_struct me_ast is_mod = +let declare_include interp_struct me_ast is_mod is_self = let fs = Summary.freeze_summaries () in try let env = Global.env() in - let me = interp_struct env me_ast in + let me = interp_struct env me_ast in let mp1,_ = current_prefix () in - let (mbids,mp,objs)= + let compute_objs objs = function + | MSEident mp -> + let mb_mp = if is_mod then + Environ.lookup_module mp env else + Modops.module_body_of_type mp (Environ.lookup_modtype mp env) in + (match objs with + |([],_,_) -> objs + |(mbids,mp_self,objects) -> + let mb = Global.pack_module() in + let rec compute_subst mbids sign = + match mbids with + [] -> empty_subst + | mbid::mbids -> + let farg_id, farg_b, fbody_b = + Modops.destr_functor env sign in + let subst=compute_subst mbids fbody_b in + let mp_delta = + Modops.complete_inline_delta_resolver env mb.mod_mp + farg_id farg_b mb.mod_delta in + join (map_mbid mbid mb.mod_mp mp_delta) subst + in + let subst = compute_subst mbids mb_mp.mod_type in + ([],mp_self,subst_objects subst objects) + + ) + | _ -> objs + in + + let (mbids,mp,objs)= if is_mod then get_module_substobjs env mp1 me else get_modtype_substobjs env mp1 me in + let (mbids,mp,objs) = if is_self + then compute_objs (mbids,mp,objs) me else (mbids,mp,objs) in let id = current_mod_id() in let resolver = Global.add_include me is_mod in let substobjs = (mbids,mp1, @@ -916,7 +945,6 @@ let declare_include interp_struct me_ast is_mod = (* Something wrong: undo the whole process *) Summary.unfreeze_summaries fs; raise e - (*s Iterators. *) let iter_all_segments f = diff --git a/library/declaremods.mli b/library/declaremods.mli index 5cda0d28d..4a037b005 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -100,7 +100,7 @@ val import_module : bool -> module_path -> unit (* Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry) -> - 'struct_expr -> bool -> unit + 'struct_expr -> bool -> bool -> unit (*s [iter_all_segments] iterate over all segments, the modules' segments first and then the current segment. Modules are presented diff --git a/library/global.ml b/library/global.ml index 6d7942ec0..3129c1caf 100644 --- a/library/global.ml +++ b/library/global.ml @@ -108,6 +108,8 @@ let end_modtype fs id = global_env := newenv; kn +let pack_module () = + pack_module !global_env diff --git a/library/global.mli b/library/global.mli index 30bd04150..b7e788912 100644 --- a/library/global.mli +++ b/library/global.mli @@ -52,7 +52,8 @@ val add_mind : val add_module : identifier -> module_entry -> module_path * delta_resolver val add_modtype : identifier -> module_struct_entry -> module_path -val add_include : module_struct_entry -> bool -> delta_resolver +val add_include : + module_struct_entry -> bool -> delta_resolver val add_constraints : constraints -> unit @@ -74,7 +75,7 @@ val add_module_parameter : mod_bound_id -> module_struct_entry -> delta_resolver val start_modtype : identifier -> module_path val end_modtype : Summary.frozen -> identifier -> module_path - +val pack_module : unit -> module_body (* Queries *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3bc27965a..3a99b2473 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -413,8 +413,13 @@ GEXTEND Gram VernacRequireFrom (export, None, filename) | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) - | IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr)) - | IDENT "Include"; "Type"; expr = module_type -> VernacInclude(CIMTE(expr)) ] ] + | IDENT "Include"; expr = module_expr -> VernacInclude(false,CIME(expr)) + | IDENT "Include"; "Type"; expr = module_type -> + VernacInclude(false,CIMTE(expr)) + | IDENT "Include"; "Self"; expr = module_expr -> + VernacInclude(true,CIME(expr)) + | IDENT "Include"; "Self"; "Type"; expr = module_type -> + VernacInclude(true,CIMTE(expr)) ] ] ; export_token: [ [ IDENT "Import" -> Some false diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 9e7bd10e7..52ef1875f 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -761,15 +761,15 @@ let rec pr_vernac = function 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) - | VernacInclude (in_ast) -> + | VernacInclude (b,in_ast) -> begin match in_ast with | CIMTE mty -> - hov 2 (str"Include" ++ - (fun mt -> str " " ++ pr_module_type pr_lconstr mt) mty) + hov 2 (str"Include " ++ str (if b then "Self " else "") ++ + pr_module_type pr_lconstr mty) | CIME mexpr -> - hov 2 (str"Include" ++ - (fun me -> str " " ++ pr_module_expr me) mexpr) + hov 2 (str"Include " ++ str (if b then "Self " else "") ++ + pr_module_expr mexpr) end (* Solving *) | VernacSolve (i,tac,deftac) -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 60e38d97f..2008e5f01 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -555,11 +555,13 @@ let vernac_end_modtype (loc,id) = Dumpglob.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") -let vernac_include = function +let vernac_include is_self = function | CIMTE mty_ast -> - Declaremods.declare_include Modintern.interp_modtype mty_ast false + Declaremods.declare_include + Modintern.interp_modtype mty_ast false is_self | CIME mexpr_ast -> - Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true + Declaremods.declare_include + Modintern.interp_modexpr mexpr_ast true is_self (**********************) (* Gallina extensions *) @@ -1331,8 +1333,8 @@ let interp c = match c with vernac_define_module export lid bl mtyo mexpro | VernacDeclareModuleType (lid,bl,mtyo) -> vernac_declare_module_type lid bl mtyo - | VernacInclude (in_ast) -> - vernac_include in_ast + | VernacInclude (is_self,in_ast) -> + vernac_include is_self in_ast (* Gallina extensions *) | VernacBeginSection lid -> vernac_begin_section lid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 8a70e7626..366308bfa 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -264,7 +264,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 + | VernacInclude of bool * include_ast (* Solving *) |