diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/astmod.ml | 45 | ||||
| -rw-r--r-- | parsing/g_module.ml4 | 11 |
2 files changed, 45 insertions, 11 deletions
diff --git a/parsing/astmod.ml b/parsing/astmod.ml index acf0de62e..9c0915a4f 100644 --- a/parsing/astmod.ml +++ b/parsing/astmod.ml @@ -89,21 +89,46 @@ let lookup_modtype binders qid = with Not_found -> Nametab.locate_modtype qid -let transl_modtype binders = function - | Node(loc,"MODTYPEQID",qid_ast) -> begin match qid_ast with - | [Node (loc, "QUALID", astl)] -> - let qid = interp_qualid astl in begin +let transl_with_decl binders = function + | Node(loc,"WITHMODULE",[id_ast;qid_ast]) -> + let id = match id_ast with + Nvar(_,id) -> id + | _ -> anomaly "Identifier AST expected" + in + let qid = match qid_ast with + | Node (loc, "QUALID", astl) -> + interp_qualid astl + | _ -> anomaly "QUALID expected" + in + With_Module (id,lookup_module binders 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 + With_Definition (id,c) + | _ -> anomaly "Unexpected AST" + +let rec transl_modtype binders = 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) with | Not_found -> - Modops.error_not_a_modtype (*loc*) (string_of_qualid qid) - end - | _ -> anomaly "QUALID expected" - end - | _ -> anomaly "TODO: transl_modtype: I can handle qualid module types only" - + Modops.error_not_a_modtype (*loc*) (string_of_qualid qid) + end + | _ -> 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 + 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 = diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4 index 01e7256ef..56db0cb59 100644 --- a/parsing/g_module.ml4 +++ b/parsing/g_module.ml4 @@ -73,9 +73,18 @@ GEXTEND Gram ] ] ; + with_declaration: + [ [ "Definition"; id = ident; ":="; c = Constr.constr -> + <:ast< (WITHDEFINITION $id $c) >> + | IDENT "Module"; id = ident; ":="; qid = qualid -> + <:ast< (WITHMODULE $id $qid) >> + ] ] + ; + module_type: [ [ qid = qualid -> <:ast< (MODTYPEQID $qid) >> (* ... *) - ] ] + | mty = module_type; "with"; decl = with_declaration -> + <:ast< (MODTYPEWITH $mty $decl)>> ] ] ; END |