diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /interp/modintern.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'interp/modintern.ml')
-rw-r--r-- | interp/modintern.ml | 103 |
1 files changed, 103 insertions, 0 deletions
diff --git a/interp/modintern.ml b/interp/modintern.ml new file mode 100644 index 00000000..0929119c --- /dev/null +++ b/interp/modintern.ml @@ -0,0 +1,103 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: modintern.ml,v 1.2.2.1 2004/07/16 19:30:22 herbelin Exp $ *) + +open Pp +open Util +open Names +open Entries +open Libnames +open Topconstr +open Constrintern + +let rec make_mp mp = function + [] -> mp + | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl + +(* +(* Since module components are not put in the nametab we try to locate +the module prefix *) +exception BadRef + +let lookup_qualid (modtype:bool) qid = + let rec make_mp mp = function + [] -> mp + | h::tl -> make_mp (MPdot(mp, label_of_id h)) tl + in + let rec find_module_prefix dir n = + if n<0 then raise Not_found; + let dir',dir'' = list_chop n dir in + let id',dir''' = + match dir'' with + | hd::tl -> hd,tl + | _ -> anomaly "This list should not be empty!" + in + let qid' = make_qualid dir' id' in + try + match Nametab.locate qid' with + | ModRef mp -> mp,dir''' + | _ -> raise BadRef + with + Not_found -> find_module_prefix dir (pred n) + in + try Nametab.locate qid + with Not_found -> + let (dir,id) = repr_qualid qid in + let pref_mp,dir' = find_module_prefix dir (List.length dir - 1) in + let mp = + List.fold_left (fun mp id -> MPdot (mp, label_of_id id)) pref_mp dir' + in + if modtype then + ModTypeRef (make_ln mp (label_of_id id)) + else + ModRef (MPdot (mp,label_of_id id)) + +*) + +(* Search for the head of [qid] in [binders]. + If found, returns the module_path/kernel_name created from the dirpath + and the basename. Searches Nametab otherwise. +*) + +let lookup_module (loc,qid) = + try + Nametab.locate_module qid + with + | Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid) + +let lookup_modtype (loc,qid) = + try + Nametab.locate_modtype qid + with + | Not_found -> + Modops.error_not_a_modtype_loc loc (string_of_qualid qid) + +let transl_with_decl env = function + | CWith_Module ((_,id),qid) -> + With_Module (id,lookup_module qid) + | CWith_Definition ((_,id),c) -> + With_Definition (id,interp_constr Evd.empty env c) + +let rec interp_modtype env = function + | CMTEident qid -> + MTEident (lookup_modtype qid) + | CMTEwith (mty,decl) -> + let mty = interp_modtype env mty in + let decl = transl_with_decl env decl in + MTEwith(mty,decl) + + +let rec interp_modexpr env = function + | CMEident qid -> + MEident (lookup_module qid) + | CMEapply (me1,me2) -> + let me1 = interp_modexpr env me1 in + let me2 = interp_modexpr env me2 in + MEapply(me1,me2) + |