diff options
author | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-19 18:21:04 +0000 |
---|---|---|
committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-19 18:21:04 +0000 |
commit | 04dfb014ae67e1446aba386913131e18e6bbe41f (patch) | |
tree | f36c281209313783b176473117f910f3818dd658 | |
parent | f0591d4fdf4a39c53ee690fc7285b592161406de (diff) |
La notation 'with'. L'interpretation - version preliminaire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend | 26 | ||||
-rw-r--r-- | kernel/declarations.ml | 8 | ||||
-rw-r--r-- | kernel/declarations.mli | 8 | ||||
-rw-r--r-- | kernel/entries.ml | 5 | ||||
-rw-r--r-- | kernel/entries.mli | 5 | ||||
-rw-r--r-- | kernel/mod_typing.ml | 99 | ||||
-rw-r--r-- | kernel/modops.ml | 34 | ||||
-rw-r--r-- | kernel/modops.mli | 6 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 16 | ||||
-rw-r--r-- | kernel/subtyping.ml | 9 | ||||
-rw-r--r-- | library/declaremods.ml | 25 | ||||
-rw-r--r-- | parsing/astmod.ml | 45 | ||||
-rw-r--r-- | parsing/g_module.ml4 | 11 |
13 files changed, 228 insertions, 69 deletions
@@ -448,19 +448,19 @@ kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/names.cmi kernel/term.cmi lib/util.cmi \ - kernel/modops.cmi + kernel/environ.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi \ + lib/util.cmi kernel/modops.cmi kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ - kernel/environ.cmx kernel/names.cmx kernel/term.cmx lib/util.cmx \ - kernel/modops.cmi + kernel/environ.cmx kernel/names.cmx kernel/term.cmx kernel/univ.cmx \ + lib/util.cmx kernel/modops.cmi kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \ - kernel/subtyping.cmi kernel/term_typing.cmi kernel/univ.cmi lib/util.cmi \ - kernel/mod_typing.cmi + kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \ + kernel/typeops.cmi kernel/univ.cmi lib/util.cmi kernel/mod_typing.cmi kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \ kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \ - kernel/subtyping.cmx kernel/term_typing.cmx kernel/univ.cmx lib/util.cmx \ - kernel/mod_typing.cmi + kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \ + kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \ kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \ @@ -674,11 +674,13 @@ parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx parsing/genarg.cmx \ library/libnames.cmx kernel/names.cmx lib/pp.cmx proofs/tacexpr.cmx \ lib/util.cmx parsing/ast.cmi parsing/astmod.cmo: parsing/astterm.cmi parsing/coqast.cmi kernel/entries.cmi \ - library/lib.cmi library/libnames.cmi kernel/modops.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi lib/util.cmi parsing/astmod.cmi + pretyping/evd.cmi library/global.cmi library/lib.cmi library/libnames.cmi \ + kernel/modops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + lib/util.cmi parsing/astmod.cmi parsing/astmod.cmx: parsing/astterm.cmx parsing/coqast.cmx kernel/entries.cmx \ - library/lib.cmx library/libnames.cmx kernel/modops.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx lib/util.cmx parsing/astmod.cmi + pretyping/evd.cmx library/global.cmx library/lib.cmx library/libnames.cmx \ + kernel/modops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + lib/util.cmx parsing/astmod.cmi parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ lib/dyn.cmi kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ library/global.cmi library/impargs.cmi library/libnames.cmi \ diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 8b1170597..05989bc82 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -148,7 +148,8 @@ and module_expr_body = | MEBapply of module_expr_body * module_expr_body * constraints -and module_specification_body = module_type_body * module_path option +and module_specification_body = + module_type_body * module_path option * constraints and structure_elem_body = | SEBconst of constant_body @@ -160,6 +161,7 @@ and module_structure_body = (label * structure_elem_body) list and module_body = { mod_expr : module_expr_body option; - mod_user_type : (module_type_body * constraints) option; + mod_user_type : module_type_body option; mod_type : module_type_body; - mod_equiv : module_path option } + mod_equiv : module_path option; + mod_constraints : constraints } diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 574cb04fa..eeec64875 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -107,7 +107,8 @@ and module_expr_body = | MEBapply of module_expr_body * module_expr_body * constraints -and module_specification_body = module_type_body * module_path option +and module_specification_body = + module_type_body * module_path option * constraints and structure_elem_body = | SEBconst of constant_body @@ -119,9 +120,10 @@ and module_structure_body = (label * structure_elem_body) list and module_body = { mod_expr : module_expr_body option; - mod_user_type : (module_type_body * constraints) option; + mod_user_type : module_type_body option; mod_type : module_type_body; - mod_equiv : module_path option } + mod_equiv : module_path option; + mod_constraints : constraints } diff --git a/kernel/entries.ml b/kernel/entries.ml index 4d86d6d2c..edba6e608 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -78,10 +78,13 @@ and module_type_entry = MTEident of kernel_name | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry | MTEsig of mod_self_id * module_signature_entry + | MTEwith of module_type_entry * with_declaration and module_signature_entry = (label * specification_entry) list - +and with_declaration = + With_Module of identifier * module_path + | With_Definition of identifier * constr and module_expr = MEident of module_path diff --git a/kernel/entries.mli b/kernel/entries.mli index 4d86d6d2c..edba6e608 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -78,10 +78,13 @@ and module_type_entry = MTEident of kernel_name | MTEfunsig of mod_bound_id * module_type_entry * module_type_entry | MTEsig of mod_self_id * module_signature_entry + | MTEwith of module_type_entry * with_declaration and module_signature_entry = (label * specification_entry) list - +and with_declaration = + With_Module of identifier * module_path + | With_Definition of identifier * constr and module_expr = MEident of module_path diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 1eb74ffef..2c00fe52e 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -24,6 +24,15 @@ let path_of_mexpr = function | MEident mb -> mb | _ -> raise Not_path +let rec replace_first p k = function + | [] -> [] + | h::t when p h -> k::t + | h::t -> h::(replace_first p k t) + +let rec list_split_assoc k rev_before = function + | [] -> raise Not_found + | (k',b)::after when k=k' -> rev_before,b,after + | h::tail -> list_split_assoc k (h::rev_before) tail let rec list_fold_map2 f e = function | [] -> (e,[],[]) @@ -47,6 +56,70 @@ let rec translate_modtype env mte = | MTEsig (msid,sig_e) -> let str_b,sig_b = translate_entry_list env msid false sig_e in MTBsig (msid,sig_b) + | MTEwith (mte, with_decl) -> + let mtb = translate_modtype env mte in + merge_with env mtb with_decl + +and merge_with env mtb with_decl = + let msid,sig_b = match (Modops.scrape_modtype env mtb) with + | MTBsig(msid,sig_b) -> msid,sig_b + | _ -> error_signature_expected mtb + in + let id = match with_decl with + | With_Definition (id,_) | With_Module (id,_) -> id + in + let l = label_of_id id in + try + let rev_before,spec,after = list_split_assoc l [] sig_b in + let before = List.rev rev_before in + let env' = Modops.add_signature (MPself msid) before env in + let new_spec = match with_decl with + | With_Definition (id,c) -> + let cb = match spec with + SPBconst cb -> cb + | _ -> error_not_a_constant l + in + begin + match cb.const_body with + | None -> + let (j,cst1) = Typeops.infer env' c in + let cst2 = + Reduction.conv_leq env' j.uj_type cb.const_type in + let cst = + Constraint.union + (Constraint.union cb.const_constraints cst1) + cst2 + in + SPBconst {cb with + const_body = Some j.uj_val; + const_constraints = cst} + | Some b -> + let cst1 = Reduction.conv env' c b in + let cst = Constraint.union cb.const_constraints cst1 in + SPBconst {cb with + const_body = Some c; + const_constraints = cst} + end + | With_Module (id, mp) -> + let (oldmtb,oldequiv,oldcst) = match spec with + SPBmodule (mtb,equiv,cst) -> (mtb,equiv,cst) + | _ -> error_not_a_module (string_of_label l) + in + let mtb = type_modpath env' mp in + let cst = check_subtypes env' mtb oldmtb in + let equiv = + match oldequiv with + | None -> Some mp + | Some mp' -> + check_modpath_equiv env' mp mp'; + Some mp + in + SPBmodule (mtb, equiv, Constraint.union oldcst cst) + in + MTBsig(msid, before@(l,new_spec)::after) + with + Not_found -> error_no_such_label l + | Reduction.NotConvertible -> error_with_incorrect l and translate_entry_list env msid is_definition sig_e = let mp = MPself msid in @@ -61,7 +134,7 @@ and translate_entry_list env msid is_definition sig_e = add_mind kn mib env, (l, SEBmind mib), (l, SPBmind mib) | SPEmodule me -> let mb = translate_module env is_definition me in - let mspec = mb.mod_type, mb.mod_equiv in + let mspec = mb.mod_type, mb.mod_equiv, mb.mod_constraints in let mp' = MPdot (mp,l) in add_module mp' mb env, (l, SEBmodule mb), (l, SPBmodule mspec) | SPEmodtype mte -> @@ -82,9 +155,10 @@ and translate_module env is_definition me = | None, Some mte -> let mtb = translate_modtype env mte in { mod_expr = None; - mod_user_type = Some (mtb, Constraint.empty); + mod_user_type = Some mtb; mod_type = mtb; - mod_equiv = None } + mod_equiv = None; + mod_constraints = Constraint.empty } | Some mexpr, _ -> let meq_o = (* do we have a transparent module ? *) try (* TODO: transparent field in module_entry *) @@ -104,17 +178,18 @@ and translate_module env is_definition me = in MEBident mp, type_modpath env mp in - let mtb,mod_user_type = + let mtb, mod_user_type, cst = match me.mod_entry_type with - | None -> mtb1, None + | None -> mtb1, None, Constraint.empty | Some mte -> let mtb2 = translate_modtype env mte in - mtb2, Some (mtb2, check_subtypes env mtb1 mtb2) + mtb2, Some mtb2, check_subtypes env mtb1 mtb2 in { mod_type = mtb; mod_user_type = mod_user_type; mod_expr = Some meb; - mod_equiv = meq_o } + mod_equiv = meq_o; + mod_constraints = cst } (* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *) and translate_mexpr env mexpr = match mexpr with @@ -180,12 +255,7 @@ and add_module_constraints env mb = | None -> env | Some meb -> add_module_expr_constraints env meb in - let env = match mb.mod_user_type with - | None -> env - | Some (mtb,cst) -> - Environ.add_constraints cst (add_modtype_constraints env mtb) - in - env + Environ.add_constraints mb.mod_constraints env and add_modtype_constraints env = function | MTBident _ -> env @@ -202,7 +272,8 @@ and add_modtype_constraints env = function and add_sig_elem_constraints env = function | SPBconst cb -> Environ.add_constraints cb.const_constraints env | SPBmind mib -> Environ.add_constraints mib.mind_constraints env - | SPBmodule (mtb,_) -> add_modtype_constraints env mtb + | SPBmodule (mtb,_,cst) -> + add_modtype_constraints (Environ.add_constraints cst env) mtb | SPBmodtype mtb -> add_modtype_constraints env mtb diff --git a/kernel/modops.ml b/kernel/modops.ml index ea8a2c4e2..d4338f0fb 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -11,6 +11,7 @@ (*i*) open Util open Names +open Univ open Term open Declarations open Environ @@ -41,6 +42,9 @@ let error_incompatible_labels l l' = let error_result_must_be_signature mtb = error "The result module type must be a signature" +let error_signature_expected mtb = + error "Signature expected" + let error_no_module_to_end _ = error "No open module to end" @@ -53,25 +57,33 @@ let error_not_a_modtype s = let error_not_a_module s = error ("\""^s^"\" is not a module") +let error_not_a_constant l = + error ("\""^(string_of_label l)^"\" is not a constant") + +let error_with_incorrect l = + error ("Incorrect constraint for label \""^(string_of_label l)^"\"") let rec scrape_modtype env = function | MTBident kn -> scrape_modtype env (lookup_modtype kn env) | mtb -> mtb -let module_body_of_spec spec = - { mod_type = fst spec; - mod_equiv = snd spec; - mod_expr = None; - mod_user_type = None} +let module_body_of_spec (mty,mpo,cst) = + { mod_type = mty; + mod_equiv = mpo; + mod_expr = None; + mod_user_type = None; + mod_constraints = cst} let module_body_of_type mtb = { mod_type = mtb; mod_equiv = None; mod_expr = None; - mod_user_type = None} + mod_user_type = None; + mod_constraints = Constraint.empty} + -let module_spec_of_body mb = mb.mod_type, mb.mod_equiv +let module_spec_of_body mb = mb.mod_type, mb.mod_equiv, mb.mod_constraints let destr_functor = function | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) @@ -114,11 +126,11 @@ and subst_signature sub sign = in List.map (fun (l,b) -> (l,subst_body b)) sign -and subst_module sub (mtb,mpo as mb) = +and subst_module sub (mtb,mpo,cst as mb) = let mtb' = subst_modtype sub mtb in let mpo' = option_smartmap (subst_mp sub) mpo in if mtb'==mtb && mpo'==mpo then mb else - (mtb',mpo') + (mtb',mpo',cst) let subst_signature_msid msid mp = subst_signature (map_msid msid mp) @@ -161,13 +173,13 @@ let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with | MTBident _ -> anomaly "scrape_modtype does not work!" | MTBfunsig _ -> mtb | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp) -and strengthen_mod env mp (mtb,mpo) = +and strengthen_mod env mp (mtb,mpo,cst) = let mtb' = strengthen_mtb env mp mtb in let mpo' = match mpo with | Some _ -> mpo | None -> Some mp in - (mtb',mpo') + (mtb',mpo',cst) and strengthen_sig env msid sign mp = match sign with | [] -> [] | (l,SPBconst cb) :: rest -> diff --git a/kernel/modops.mli b/kernel/modops.mli index 7cd22c57c..68f8ea38a 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -74,6 +74,8 @@ val error_no_such_label : label -> 'a val error_result_must_be_signature : module_type_body -> 'a +val error_signature_expected : module_type_body -> 'a + val error_no_module_to_end : unit -> 'a val error_no_modtype_to_end : unit -> 'a @@ -81,3 +83,7 @@ val error_no_modtype_to_end : unit -> 'a val error_not_a_modtype : string -> 'a val error_not_a_module : string -> 'a + +val error_not_a_constant : label -> 'a + +val error_with_incorrect : label -> 'a diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 909b12704..22d45861e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -262,13 +262,13 @@ let end_module l senv = params in let auto_tb = MTBsig (modinfo.msid, List.rev senv.revsign) in - let mtb, mod_user_type = + let mtb, mod_user_type, cst = match restype with - | None -> functorize_type auto_tb, None + | None -> functorize_type auto_tb, None, Constraint.empty | Some res_tb -> - let cnstrs = check_subtypes senv.env auto_tb res_tb in + let cst = check_subtypes senv.env auto_tb res_tb in let mtb = functorize_type res_tb in - mtb, Some (mtb, cnstrs) + mtb, Some mtb, cst in let mexpr = List.fold_right @@ -280,9 +280,10 @@ let end_module l senv = { mod_expr = Some mexpr; mod_user_type = mod_user_type; mod_type = mtb; - mod_equiv = None } + mod_equiv = None; + mod_constraints = cst } in - let mspec = mtb , None in + let mspec = mtb, None, Constraint.empty in let mp = MPdot (oldsenv.modinfo.modpath, l) in let newenv = oldsenv.env in let newenv = @@ -438,7 +439,8 @@ let export senv dir = { mod_expr = Some (MEBstruct (modinfo.msid, List.rev senv.revstruct)); mod_type = MTBsig (modinfo.msid, List.rev senv.revsign); mod_user_type = None; - mod_equiv = None } + mod_equiv = None; + mod_constraints = Constraint.empty } in modinfo.msid, (dir,mb,senv.imports) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index f62725c70..fa024b7f2 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -182,12 +182,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 = c2 *) -let rec check_modules cst env msid1 l msb1 msb2 = +let rec check_modules cst env msid1 l + (mtb1,mpo1,cst1 as msb1) (mtb2,mpo2,cst2 as msb2) = let mp = (MPdot(MPself msid1,l)) in - let mty1 = strengthen env (fst msb1) mp in - let cst = check_modtypes cst env mty1 (fst msb2) false in + let mty1 = strengthen env mtb1 mp in + let cst = check_modtypes cst env mty1 mtb2 false in begin - match (snd msb1), (snd msb2) with + match mpo1, mpo2 with | _, None -> () | None, Some mp2 -> check_modpath_equiv env mp mp2 diff --git a/library/declaremods.ml b/library/declaremods.ml index 89a826c92..28817ebe4 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -350,6 +350,20 @@ let (in_modtype,out_modtype) = +let replace_module_object id (subst, mbids, msid, lib_stack) modobjs = + if mbids<>[] then + error "Unexpected functor objects" + else + let rec replace_id = function + | [] -> [] + | (id',obj)::tail when id = id' -> + if object_tag obj = "MODULE" then + (id, in_module (None,modobjs,None))::tail + else error "MODULE expected!" + | lobj::tail -> lobj::replace_id tail + in + (subst, mbids, msid, replace_id lib_stack) + let abstract_substobjs mbids1 (subst, mbids2, msid, lib_stack) = (subst, mbids1@mbids2, msid, lib_stack) @@ -359,8 +373,13 @@ let rec get_modtype_substobjs = function | MTEfunsig (mbid,_,mte) -> let (subst, mbids, msid, objs) = get_modtype_substobjs mte in (subst, mbid::mbids, msid, objs) - | MTEsig (msid,_) -> (empty_subst, [], msid, []) - (* this is plainly wrong, but it is hard to do otherwise... *) + | MTEwith (mty, With_Definition _) -> get_modtype_substobjs mty + | MTEwith (mty, With_Module (id,mp)) -> + let substobjs = get_modtype_substobjs mty in + let modobjs = MPmap.find mp !modtab_substobjs in + replace_module_object id substobjs modobjs + | MTEsig (msid,_) -> + todo "Anonymous module types"; (empty_subst, [], msid, []) (* push names of bound modules (and their components) to Nametab *) (* add objects associated to them *) @@ -428,6 +447,8 @@ let end_module id = | Some (MTEsig (msid,_)) -> todo "Anonymous signatures not supported"; empty_subst, mbids, msid, [] + | Some (MTEwith _ as mty) -> + abstract_substobjs mbids (get_modtype_substobjs mty) | Some (MTEfunsig _) -> anomaly "Funsig cannot be here..." in 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 |