aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend26
-rw-r--r--kernel/declarations.ml8
-rw-r--r--kernel/declarations.mli8
-rw-r--r--kernel/entries.ml5
-rw-r--r--kernel/entries.mli5
-rw-r--r--kernel/mod_typing.ml99
-rw-r--r--kernel/modops.ml34
-rw-r--r--kernel/modops.mli6
-rw-r--r--kernel/safe_typing.ml16
-rw-r--r--kernel/subtyping.ml9
-rw-r--r--library/declaremods.ml25
-rw-r--r--parsing/astmod.ml45
-rw-r--r--parsing/g_module.ml411
13 files changed, 228 insertions, 69 deletions
diff --git a/.depend b/.depend
index 56b4a4da0..134bad870 100644
--- a/.depend
+++ b/.depend
@@ -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 07:45:57 +0000