diff options
Diffstat (limited to 'parsing/astmod.ml')
| -rw-r--r-- | parsing/astmod.ml | 69 |
1 files changed, 15 insertions, 54 deletions
diff --git a/parsing/astmod.ml b/parsing/astmod.ml index 9c0915a4f..cbb19fa0b 100644 --- a/parsing/astmod.ml +++ b/parsing/astmod.ml @@ -65,31 +65,13 @@ let lookup_qualid (modtype:bool) qid = and the basename. Searches Nametab otherwise. *) -let lookup_module binders qid = - try - let dir,id = repr_qualid qid in - (* dirpath in natural order *) - let idl = List.rev (id::repr_dirpath dir) in - let top_mp = MPbound (fst (List.assoc (List.hd idl) binders)) in - make_mp top_mp (List.tl idl) - with - Not_found -> Nametab.locate_module qid +let lookup_module qid = + Nametab.locate_module qid -let lookup_modtype binders qid = - try - let dir,id = repr_qualid qid in - (* dirpath in natural order *) - match List.rev (repr_dirpath dir) with - | hd::tl -> - let top_mp = MPbound (fst (List.assoc hd binders)) in - let mp = make_mp top_mp tl in - make_kn mp empty_dirpath (label_of_id id) - | [] -> raise Not_found - (* may-be a module, but not a module type!*) - with - Not_found -> Nametab.locate_modtype qid +let lookup_modtype qid = + Nametab.locate_modtype qid -let transl_with_decl binders = function +let transl_with_decl env = function | Node(loc,"WITHMODULE",[id_ast;qid_ast]) -> let id = match id_ast with Nvar(_,id) -> id @@ -100,22 +82,22 @@ let transl_with_decl binders = function interp_qualid astl | _ -> anomaly "QUALID expected" in - With_Module (id,lookup_module binders qid) + With_Module (id,lookup_module qid) | Node(loc,"WITHDEFINITION",[id_ast;cast]) -> let id = match id_ast with Nvar(_,id) -> id | _ -> anomaly "Identifier AST expected" in - let c = interp_constr Evd.empty (Global.env()) cast in + let c = interp_constr Evd.empty env cast in With_Definition (id,c) | _ -> anomaly "Unexpected AST" -let rec transl_modtype binders = function +let rec interp_modtype env = function | Node(loc,"MODTYPEQID",qid_ast) -> begin match qid_ast with | [Node (loc, "QUALID", astl)] -> let qid = interp_qualid astl in begin try - MTEident (lookup_modtype binders qid) + MTEident (lookup_modtype qid) with | Not_found -> Modops.error_not_a_modtype (*loc*) (string_of_qualid qid) @@ -123,32 +105,18 @@ let rec transl_modtype binders = function | _ -> anomaly "QUALID expected" end | Node(loc,"MODTYPEWITH",[mty_ast;decl_ast]) -> - let mty = transl_modtype binders mty_ast in - let decl = transl_with_decl binders decl_ast in + let mty = interp_modtype env mty_ast in + let decl = transl_with_decl env decl_ast in MTEwith(mty,decl) | _ -> anomaly "TODO: transl_modtype: I can handle qualid module types only" -let transl_binder binders (idl,mty_ast) = - let mte = transl_modtype binders mty_ast in - let add_one binders id = - if List.mem_assoc id binders then - error "Two identical module binders..." - else - let mbid = make_mbid (Lib.module_dp()) (string_of_id id) in - (id,(mbid,mte))::binders - in - List.fold_left add_one binders idl - -let transl_binders = List.fold_left transl_binder - - -let rec transl_modexpr binders = function +let rec interp_modexpr env = function | Node(loc,"MODEXPRQID",qid_ast) -> begin match qid_ast with | [Node (loc, "QUALID", astl)] -> let qid = interp_qualid astl in begin try - MEident (lookup_module binders qid) + MEident (lookup_module qid) with | Not_found -> Modops.error_not_a_module (*loc*) (string_of_qualid qid) @@ -156,17 +124,10 @@ let rec transl_modexpr binders = function | _ -> anomaly "QUALID expected" end | Node(_,"MODEXPRAPP",[ast1;ast2]) -> - let me1 = transl_modexpr binders ast1 in - let me2 = transl_modexpr binders ast2 in + let me1 = interp_modexpr env ast1 in + let me2 = interp_modexpr env ast2 in MEapply(me1,me2) | Node(_,"MODEXPRAPP",_) -> anomaly "transl_modexpr: MODEXPRAPP must have two arguments" | _ -> anomaly "transl_modexpr: I can handle MODEXPRQID or MODEXPRAPP only..." - -let interp_module_decl evd env args_ast mty_ast_o mexpr_ast_o = - let binders = transl_binders [] args_ast in - let mty_o = option_app (transl_modtype binders) mty_ast_o in - let mexpr_o = option_app (transl_modexpr binders) mexpr_ast_o in - (List.rev binders, mty_o, mexpr_o) - |