diff options
Diffstat (limited to 'interp/modintern.ml')
| -rw-r--r-- | interp/modintern.ml | 100 |
1 files changed, 79 insertions, 21 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml index f53d1796..a13560c0 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: modintern.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -16,6 +14,54 @@ open Libnames open Topconstr open Constrintern +type module_internalization_error = + | NotAModuleNorModtype of string + | IncorrectWithInModule + | IncorrectModuleApplication + +exception ModuleInternalizationError of module_internalization_error + +(* +val error_declaration_not_path : module_struct_entry -> 'a + +val error_not_a_functor : module_struct_entry -> 'a + +val error_not_equal : module_path -> module_path -> 'a + +val error_result_must_be_signature : unit -> 'a + +oval error_not_a_modtype_loc : loc -> string -> 'a + +val error_not_a_module_loc : loc -> string -> 'a + +val error_not_a_module_or_modtype_loc : loc -> string -> 'a + +val error_with_in_module : unit -> 'a + +val error_application_to_module_type : unit -> 'a +*) + +let error_result_must_be_signature () = + error "The result module type must be a signature." + +let error_not_a_modtype_loc loc s = + Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModuleType s)) + +let error_not_a_module_loc loc s = + Compat.Loc.raise loc (Modops.ModuleTypingError (Modops.NotAModule s)) + +let error_not_a_module_nor_modtype_loc loc s = + Compat.Loc.raise loc (ModuleInternalizationError (NotAModuleNorModtype s)) + +let error_incorrect_with_in_module loc = + Compat.Loc.raise loc (ModuleInternalizationError IncorrectWithInModule) + +let error_application_to_module_type loc = + Compat.Loc.raise loc (ModuleInternalizationError IncorrectModuleApplication) + + + + let rec make_mp mp = function [] -> mp | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl @@ -70,7 +116,7 @@ let lookup_module (loc,qid) = let mp = Nametab.locate_module qid in Dumpglob.dump_modref loc mp "modtype"; mp with - | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid) + | Not_found -> error_not_a_module_loc loc (string_of_qualid qid) let lookup_modtype (loc,qid) = try @@ -78,7 +124,7 @@ let lookup_modtype (loc,qid) = Dumpglob.dump_modref loc mp "mod"; mp with | Not_found -> - Modops.error_not_a_modtype_loc loc (string_of_qualid qid) + error_not_a_modtype_loc loc (string_of_qualid qid) let lookup_module_or_modtype (loc,qid) = try @@ -88,7 +134,7 @@ let lookup_module_or_modtype (loc,qid) = 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) + error_not_a_module_nor_modtype_loc loc (string_of_qualid qid) let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> @@ -96,24 +142,35 @@ let transl_with_decl env = function | CWith_Definition ((_,fqid),c) -> With_Definition (fqid,interp_constr Evd.empty env c) +let loc_of_module = function + | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc + +let check_module_argument_is_path me' = function + | CMident _ -> () + | (CMapply (loc,_,_) | CMwith (loc,_,_)) -> + Compat.Loc.raise loc + (Modops.ModuleTypingError (Modops.ApplicationToNotPath me')) + let rec interp_modexpr env = function | CMident qid -> MSEident (lookup_module qid) - | 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 () + | CMapply (_,me1,me2) -> + let me1' = interp_modexpr env me1 in + let me2' = interp_modexpr env me2 in + check_module_argument_is_path me2' me2; + MSEapply(me1',me2') + | CMwith (loc,_,_) -> error_incorrect_with_in_module loc let rec interp_modtype env = function | CMident qid -> MSEident (lookup_modtype qid) - | CMapply (mty1,me) -> + | CMapply (_,mty1,me) -> let mty' = interp_modtype env mty1 in let me' = interp_modexpr env me in - MSEapply(mty',me') - | CMwith (mty,decl) -> + check_module_argument_is_path me' me; + MSEapply(mty',me') + | CMwith (_,mty,decl) -> let mty = interp_modtype env mty in let decl = transl_with_decl env decl in MSEwith(mty,decl) @@ -122,13 +179,14 @@ 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) -> + | CMapply (_,me1,me2) -> + let me1',ismod1 = interp_modexpr_or_modtype env me1 in + let me2',ismod2 = interp_modexpr_or_modtype env me2 in + check_module_argument_is_path me2' me2; + if not ismod2 then error_application_to_module_type (loc_of_module me2); + (MSEapply (me1',me2'), ismod1) + | CMwith (loc,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 (); + if ismod then error_incorrect_with_in_module loc; (MSEwith(me,decl), ismod) |