diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/modintern.ml | 36 | ||||
| -rw-r--r-- | interp/modintern.mli | 9 | ||||
| -rw-r--r-- | interp/topconstr.ml | 14 | ||||
| -rw-r--r-- | interp/topconstr.mli | 14 |
4 files changed, 45 insertions, 28 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index 041e32bf6..049745ca9 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -80,6 +80,16 @@ let lookup_modtype (loc,qid) = | Not_found -> Modops.error_not_a_modtype_loc loc (string_of_qualid qid) +let lookup_module_or_modtype (loc,qid) = + try + let mp = Nametab.locate_module qid in + Dumpglob.dump_modref loc mp "modtype"; (mp,true) + with Not_found -> try + let mp = Nametab.locate_modtype qid in + Dumpglob.dump_modref loc mp "mod"; (mp,false) + with Not_found -> + Modops.error_not_a_module_or_modtype_loc loc (string_of_qualid qid) + let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> With_Module (fqid,lookup_module qid) @@ -87,22 +97,38 @@ let transl_with_decl env = function With_Definition (fqid,interp_constr Evd.empty env c) let rec interp_modexpr env = function - | CMEident qid -> + | CMident qid -> MSEident (lookup_module qid) - | CMEapply (me1,me2) -> + | CMapply (me1,me2) -> let me1 = interp_modexpr env me1 in let me2 = interp_modexpr env me2 in MSEapply(me1,me2) + | CMwith _ -> Modops.error_with_in_module () + let rec interp_modtype env = function - | CMTEident qid -> + | CMident qid -> MSEident (lookup_modtype qid) - | CMTEapply (mty1,me) -> + | CMapply (mty1,me) -> let mty' = interp_modtype env mty1 in let me' = interp_modexpr env me in MSEapply(mty',me') - | CMTEwith (mty,decl) -> + | CMwith (mty,decl) -> let mty = interp_modtype env mty in let decl = transl_with_decl env decl in MSEwith(mty,decl) +let rec interp_modexpr_or_modtype env = function + | CMident qid -> + let (mp,ismod) = lookup_module_or_modtype qid in + (MSEident mp, ismod) + | CMapply (me1,me2) -> + let me1,ismod1 = interp_modexpr_or_modtype env me1 in + let me2,ismod2 = interp_modexpr_or_modtype env me2 in + if not ismod2 then Modops.error_application_to_module_type (); + (MSEapply (me1,me2), ismod1) + | CMwith (me,decl) -> + let me,ismod = interp_modexpr_or_modtype env me in + let decl = transl_with_decl env decl in + if ismod then Modops.error_with_in_module (); + (MSEwith(me,decl), ismod) diff --git a/interp/modintern.mli b/interp/modintern.mli index f39205d8b..e528b7af7 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -21,8 +21,15 @@ open Topconstr (* Module expressions and module types are interpreted relatively to eventual functor or funsig arguments. *) -val interp_modtype : env -> module_type_ast -> module_struct_entry +val interp_modtype : env -> module_ast -> module_struct_entry val interp_modexpr : env -> module_ast -> module_struct_entry +(* The following function tries to interprete an ast as a module, + and in case of failure, interpretes this ast as a module type. + The boolean is true for a module, false for a module type *) + +val interp_modexpr_or_modtype : env -> module_ast -> + module_struct_entry * bool + val lookup_module : qualid located -> module_path diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 155fd1c02..d93e1ab14 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1005,17 +1005,9 @@ type with_declaration_ast = | CWith_Definition of identifier list located * constr_expr 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 list - | CIME of module_ast list + | CMident of qualid located + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast type 'a module_signature = | Enforce of 'a (* ... : T *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 6e3951b2f..1b1698f95 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -242,17 +242,9 @@ type with_declaration_ast = | CWith_Definition of identifier list located * constr_expr 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 list - | CIME of module_ast list + | CMident of qualid located + | CMapply of module_ast * module_ast + | CMwith of module_ast * with_declaration_ast type 'a module_signature = | Enforce of 'a (* ... : T *) |