diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/assumptions.ml | 67 | ||||
| -rw-r--r-- | library/declaremods.ml | 133 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/global.mli | 2 |
4 files changed, 94 insertions, 110 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index 2418f0648..b1f133ac3 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -67,6 +67,23 @@ let rec search_cst_label lab = function | (l, SFBconst cb) :: _ when Label.equal l lab -> cb | _ :: fields -> search_cst_label lab fields +(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But: + a) I don't see currently what should be used instead + b) this shouldn't be critical for Print Assumption. At worse some + constants will have a canonical name which is non-canonical, + leading to failures in [Global.lookup_constant], but our own + [lookup_constant] should work. +*) + +let rec fields_of_functor f subs mp0 args = function + |NoFunctor a -> f subs mp0 args a + |MoreFunctor (mbid,_,e) -> + match args with + | [] -> assert false (* we should only encounter applied functors *) + | mpa :: args -> + let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in + fields_of_functor f subs mp0 args e + let rec lookup_module_in_impl mp = try Global.lookup_module mp with Not_found -> @@ -93,43 +110,29 @@ and fields_of_mp mp = if mp_eq inner_mp mp then subs else add_mp inner_mp mp mb.mod_delta subs in - Modops.subst_signature subs fields + Modops.subst_structure subs fields -and fields_of_mb subs mb args = - let seb = match mb.mod_expr with - | None -> mb.mod_type (* cf. Declare Module *) - | Some seb -> seb - in - fields_of_seb subs mb.mod_mp seb args +and fields_of_mb subs mb args = match mb.mod_expr with + |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr + |Struct sign -> fields_of_signature subs mb.mod_mp args sign + |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type -(* TODO: using [empty_delta_resolver] below in [fields_of_seb] - is probably slightly incorrect. But: - a) I don't see currently what should be used instead - b) this shouldn't be critical for Print Assumption. At worse some - constants will have a canonical name which is non-canonical, - leading to failures in [Global.lookup_constant], but our own - [lookup_constant] should work. -*) +(** The Abstract case above corresponds to [Declare Module] *) -and fields_of_seb subs mp0 seb args = match seb with - | SEBstruct l -> - let () = assert (List.is_empty args) in - l, mp0, subs - | SEBident mp -> +and fields_of_signature x = + fields_of_functor + (fun subs mp0 args struc -> + assert (List.is_empty args); + (struc, mp0, subs)) x + +and fields_of_expr subs mp0 args = function + |MEident mp -> let mb = lookup_module_in_impl (subst_mp subs mp) in fields_of_mb subs mb args - | SEBapply (seb1,seb2,_) -> - (match seb2 with - | SEBident mp2 -> fields_of_seb subs mp0 seb1 (mp2::args) - | _ -> assert false) (* only legal application is to module names *) - | SEBfunctor (mbid,mtb,seb) -> - (match args with - | [] -> assert false (* we should only encounter applied functors *) - | mpa :: args -> - let subs = add_mbid mbid mpa empty_delta_resolver subs in - fields_of_seb subs mp0 seb args) - | SEBwith _ -> assert false (* should not appear in a mod_expr - or mod_type field *) + |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1 + |MEwith _ -> assert false (* no 'with' in [mod_expr] *) + +and fields_of_expression x = fields_of_functor fields_of_expr x let lookup_constant_in_impl cst fallback = try diff --git a/library/declaremods.ml b/library/declaremods.ml index 5c0700606..8d332b7df 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -336,15 +336,14 @@ let () = ModSubstObjs.set_missing_handler handle_missing_substobjs (** Turn a chain of [MSEapply] into the head module_path and the list of module_path parameters (deepest param coming first). - Currently, right part of [MSEapply] must be [MSEident], - and left part must be either [MSEident] or another [MSEapply]. *) + The left part of a [MSEapply] must be either [MSEident] or + another [MSEapply]. *) let get_applications mexpr = let rec get params = function - | MSEident mp -> mp, params - | MSEapply (fexpr, MSEident mp) -> get (mp::params) fexpr - | MSEapply (_,mexpr) -> Modops.error_application_to_not_path mexpr - | _ -> error "Application of a non-functor." + | MEident mp -> mp, params + | MEapply (fexpr, mp) -> get (mp::params) fexpr + | MEwith _ -> error "Non-atomic functor application." in get [] mexpr (** Create the substitution corresponding to some functor applications *) @@ -357,10 +356,10 @@ let rec compute_subst env mbids sign mp_l inl = let farg_id, farg_b, fbody_b = Modops.destr_functor sign in let mb = Environ.lookup_module mp env in let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in - let resolver = match mb.mod_type with - | SEBstruct _ -> - Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta - | _ -> empty_delta_resolver (* case of a functor *) + let resolver = + if Modops.is_functor mb.mod_type then empty_delta_resolver + else + Modops.inline_delta_resolver env inl mp farg_id farg_b mb.mod_delta in mbid_left,join (map_mbid mbid mp resolver) subst @@ -386,25 +385,21 @@ let type_of_mod mp env = function |false -> (Environ.lookup_modtype mp env).typ_expr let rec get_module_path = function - |MSEident mp -> mp - |MSEfunctor (_,_,me) -> get_module_path me - |MSEwith (me,_) -> get_module_path me - |MSEapply _ as me -> fst (get_applications me) + |MEident mp -> mp + |MEwith (me,_) -> get_module_path me + |MEapply (me,_) -> get_module_path me (** Substitutive objects of a module expression (or module type) *) let rec get_module_sobjs is_mod env inl = function - |MSEident mp -> + |MEident mp -> begin match ModSubstObjs.get mp with |(mbids,Objs _) when not (ModPath.is_bound mp) -> (mbids,Ref (mp, empty_subst)) (* we create an alias *) |sobjs -> sobjs end - |MSEfunctor (mbid,_,mexpr) -> - let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in - (mbid::mbids, aobjs) - |MSEwith (mty, With_Definition _) -> get_module_sobjs is_mod env inl mty - |MSEwith (mty, With_Module (idl,mp1)) -> + |MEwith (mty, WithDef _) -> get_module_sobjs is_mod env inl mty + |MEwith (mty, WithMod (idl,mp1)) -> assert (not is_mod); let sobjs0 = get_module_sobjs is_mod env inl mty in assert (sobjs_no_functor sobjs0); @@ -413,35 +408,27 @@ let rec get_module_sobjs is_mod env inl = function let objs0 = expand_sobjs sobjs0 in let objs1 = expand_sobjs (ModSubstObjs.get mp1) in ([], Objs (replace_module_object idl mp0 objs0 mp1 objs1)) - |MSEapply _ as me -> + |MEapply _ as me -> let mp1, mp_l = get_applications me in - let mbids, aobjs = get_module_sobjs is_mod env inl (MSEident mp1) in + let mbids, aobjs = get_module_sobjs is_mod env inl (MEident mp1) in let typ = type_of_mod mp1 env is_mod in let mbids_left,subst = compute_subst env mbids typ mp_l inl in (mbids_left, subst_aobjs subst aobjs) +let get_functor_sobjs is_mod env inl (params,mexpr) = + let (mbids, aobjs) = get_module_sobjs is_mod env inl mexpr in + (List.map fst params @ mbids, aobjs) + (** {6 Handling of module parameters} *) (** For printing modules, [process_module_binding] adds names of bound module (and its components) to Nametab. It also loads - objects associated to it. It may raise a [Failure] when the - bound module hasn't an atomic type. *) - -let rec seb2mse = function - | SEBident mp -> MSEident mp - | SEBapply (s,s',_) -> MSEapply(seb2mse s, seb2mse s') - | SEBwith (s,With_module_body (l,mp)) -> MSEwith(seb2mse s,With_Module(l,mp)) - | SEBwith (s,With_definition_body(l,cb)) -> - (match cb.const_body with - | Def c -> MSEwith(seb2mse s,With_Definition(l,Lazyconstr.force c)) - | _ -> assert false) - | _ -> failwith "seb2mse: received a non-atomic seb" - -let process_module_binding mbid seb = + objects associated to it. *) + +let process_module_binding mbid me = let dir = DirPath.make [MBId.to_id mbid] in let mp = MPbound mbid in - let me = seb2mse seb in let sobjs = get_module_sobjs false (Global.env()) (default_inline ()) me in let subst = map_mp (get_module_path me) mp empty_delta_resolver in let sobjs = subst_sobjs subst sobjs in @@ -468,7 +455,7 @@ let intern_arg interp_modast acc (idl,(typ,ann)) = let resolver = Global.add_module_parameter mbid mty inl in let sobjs = subst_sobjs (map_mp mp0 mp resolver) sobjs in do_module false Lib.load_objects 1 dir mp sobjs []; - (mbid,(mty,inl))::acc) + (mbid,mty,inl)::acc) acc idl (** Process a list of declarations of functor parameters @@ -504,7 +491,7 @@ let check_subtypes mp sub_mtb_l = let mb = try Global.lookup_module mp with Not_found -> assert false in - let mtb = Modops.module_type_of_module None mb in + let mtb = Modops.module_type_of_module mb in check_sub mtb sub_mtb_l (** Same for module type [mp] *) @@ -515,24 +502,21 @@ let check_subtypes_mt mp sub_mtb_l = in check_sub mtb sub_mtb_l -(** Create a functor entry. +(** Create a params entry. In [args], the youngest module param now comes first. *) -let mk_funct_entry args entry0 = - List.fold_left - (fun entry (arg_id,(arg_t,_)) -> - MSEfunctor (arg_id,arg_t,entry)) - entry0 args +let mk_params_entry args = + List.rev_map (fun (mbid,arg_t,_) -> (mbid,arg_t)) args (** Create a functor type struct. In [args], the youngest module param now comes first. *) let mk_funct_type env args seb0 = List.fold_left - (fun seb (arg_id,(arg_t,arg_inl)) -> + (fun seb (arg_id,arg_t,arg_inl) -> let mp = MPbound arg_id in - let arg_t = Mod_typing.translate_module_type env mp arg_inl arg_t in - SEBfunctor(arg_id,arg_t,seb)) + let arg_t = Mod_typing.translate_modtype env mp arg_inl ([],arg_t) in + MoreFunctor(arg_id,arg_t,seb)) seb0 args (** Prepare the module type list for check of subtypes *) @@ -542,7 +526,7 @@ let build_subtypes interp_modast env mp args mtys = (fun (m,ann) -> let inl = inl2intopt ann in let mte,_ = interp_modast env ModType m in - let mtb = Mod_typing.translate_module_type env mp inl mte in + let mtb = Mod_typing.translate_modtype env mp inl ([],mte) in { mtb with typ_expr = mk_funct_type env args mtb.typ_expr }) mtys @@ -583,7 +567,8 @@ let start_module interp_modast export id args res fs = | Enforce (res,ann) -> let inl = inl2intopt ann in let mte,_ = interp_modast env ModType res in - let _ = Mod_typing.translate_struct_type_entry env inl mte in + (* We check immediately that mte is well-formed *) + let _ = Mod_typing.translate_mse env None inl mte in Some (mte,inl), [] | Check resl -> None, build_subtypes interp_modast env mp arg_entries_r resl @@ -636,32 +621,31 @@ let declare_module interp_modast id args res mexpr_o fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_module id in - let arg_entries_r = intern_args interp_modast args - in + let arg_entries_r = intern_args interp_modast args in + let params = mk_params_entry arg_entries_r in let env = Global.env () in - let mk_entry k m = mk_funct_entry arg_entries_r (fst (interp_modast env k m)) - in let mty_entry_o, subs, inl_res = match res with | Enforce (mty,ann) -> - Some (mk_entry ModType mty), [], inl2intopt ann + Some (fst (interp_modast env ModType mty)), [], inl2intopt ann | Check mtys -> None, build_subtypes interp_modast env mp arg_entries_r mtys, default_inline () in let mexpr_entry_o, inl_expr = match mexpr_o with | None -> None, default_inline () - | Some (mexpr,ann) -> Some (mk_entry Module mexpr), inl2intopt ann + | Some (mexpr,ann) -> + Some (fst (interp_modast env Module mexpr)), inl2intopt ann in - let entry = - {mod_entry_type = mty_entry_o; - mod_entry_expr = mexpr_entry_o } + let entry = match mexpr_entry_o, mty_entry_o with + | None, None -> assert false (* No body, no type ... *) + | None, Some typ -> MType (params, typ) + | Some body, otyp -> MExpr (params, body, otyp) in let sobjs, mp0 = match entry with - | {mod_entry_type = Some mte} -> - get_module_sobjs false env inl_res mte, get_module_path mte - | {mod_entry_expr = Some me} -> - get_module_sobjs true env inl_expr me, get_module_path me - | _ -> assert false (* No type, no body ... *) + | MType (_,mte) | MExpr (_,_,Some mte) -> + get_functor_sobjs false env inl_res (params,mte), get_module_path mte + | MExpr (_,me,None) -> + get_functor_sobjs true env inl_expr (params,me), get_module_path me in (* Undo the simulated interactive building of the module and declare the module as a whole *) @@ -720,16 +704,13 @@ let declare_modtype interp_modast id args mtys (mty,ann) fs = (* We simulate the beginning of an interactive module, then we adds the module parameters to the global env. *) let mp = Global.start_modtype id in - let arg_entries_r = intern_args interp_modast args - in + let arg_entries_r = intern_args interp_modast args in + let params = mk_params_entry arg_entries_r in let env = Global.env () in - let entry,_ = interp_modast env ModType mty in - let entry = mk_funct_entry arg_entries_r entry in - + let entry = params, fst (interp_modast env ModType mty) in let sub_mty_l = build_subtypes interp_modast env mp arg_entries_r mtys in - - let sobjs = get_module_sobjs false env inl entry in - let subst = map_mp (get_module_path entry) mp empty_delta_resolver in + let sobjs = get_functor_sobjs false env inl entry in + let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in let sobjs = subst_sobjs subst sobjs in (* Undo the simulated interactive building of the module type @@ -767,17 +748,17 @@ let rec include_subst env mp reso mbids sign inline = match mbids with let rec decompose_functor mpl typ = match mpl, typ with | [], _ -> typ - | _::mpl, SEBfunctor(_,_,str) -> decompose_functor mpl str + | _::mpl, MoreFunctor(_,_,str) -> decompose_functor mpl str | _ -> error "Application of a functor with too much arguments." exception NoIncludeSelf let type_of_incl env is_mod = function - |MSEident mp -> type_of_mod mp env is_mod - |MSEapply _ as me -> + |MEident mp -> type_of_mod mp env is_mod + |MEapply _ as me -> let mp0, mp_l = get_applications me in decompose_functor mp_l (type_of_mod mp0 env is_mod) - |_ -> raise NoIncludeSelf + |MEwith _ -> raise NoIncludeSelf let declare_one_include interp_modast (me_ast,annot) = let env = Global.env() in diff --git a/library/declaremods.mli b/library/declaremods.mli index f18ed2807..89bcccef3 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -118,4 +118,4 @@ val debug_print_modtab : unit -> Pp.std_ppcmds bound module hasn't an atomic type. *) val process_module_binding : - MBId.t -> Declarations.struct_expr_body -> unit + MBId.t -> Declarations.module_alg_expr -> unit diff --git a/library/global.mli b/library/global.mli index 1bc745bb7..c62f51e16 100644 --- a/library/global.mli +++ b/library/global.mli @@ -46,7 +46,7 @@ val add_module : Id.t -> Entries.module_entry -> Declarations.inline -> module_path * Mod_subst.delta_resolver val add_modtype : - Id.t -> Entries.module_struct_entry -> Declarations.inline -> module_path + Id.t -> Entries.module_type_entry -> Declarations.inline -> module_path val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver |