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

2 files changed, 45 insertions, 11 deletions

diff --git a/parsing/astmod.ml b/parsing/astmod.ml
index acf0de62e1..9c0915a4f7 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 01e7256efa..56db0cb590 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