extraction modulaire + environnement des Fix corrigé

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1505 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 46 insertions, 13 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 7a0ecd887..a5ec0a693 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -10,8 +10,11 @@ Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo" "extract_env.cmo".
 
 Grammar vernac vernac : ast :=
   extr_constr [ "Extraction" constrarg($c) "." ] -> 
-              [(Extraction $c)]
+              [ (Extraction $c) ]
 | extr_list   [ "Extraction" "-r" ne_qualidarg_list($l) "." ] ->
-              [(ExtractionRec ($LIST $l))]
+              [ (ExtractionRec ($LIST $l)) ]
 | extr_list   [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] ->
-              [(ExtractionFile $f ($LIST $l))].
+              [ (ExtractionFile $f ($LIST $l)) ]
+| extr_module [ "Extraction" "Module" identarg($m) "." ] ->
+              [ (ExtractionModule $m) ].
+
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index fa0ed7270..ac9fe6563 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -1,9 +1,10 @@
 
 open Pp
 open Term
+open Lib
+open Extraction
 open Miniml
 open Mlutil
-open Extraction
 
 (*s Topological sort of global CIC references. 
     We introduce graphs of global references; a graph is a map
@@ -140,7 +141,7 @@ let pp_decl d = Pp.pp_decl (betared_decl (uncurrify_decl d))
 open Vernacinterp
 
 let _ = 
-  vinterp_add "Extraction"
+  overwriting_vinterp_add "Extraction"
     (function 
        | [VARG_CONSTR ast] ->
 	   (fun () -> 
@@ -181,3 +182,28 @@ let _ =
        | VARG_STRING f :: vl ->
 	   (fun () -> Ocaml.extract_to_file f (decl_of_vargl vl))
        | _ -> assert false)
+
+(*s Extraction of a module. *)
+
+let extract_module m =
+  let seg = Library.module_segment (Some m) in
+  let get_reference = function
+    | sp, Leaf o ->
+	(match Libobject.object_tag o with
+	   | "CONSTANT" -> ConstRef sp
+	   | "INDUCTIVE" -> IndRef (sp,0)
+	   | _ -> failwith "caught")
+    | _ -> failwith "caught"
+  in
+  let rl = Util.map_succeed get_reference seg in
+  List.map extract_declaration rl
+
+let _ = 
+  vinterp_add "ExtractionModule"
+    (function 
+       | [VARG_IDENTIFIER m] ->
+	   (fun () -> 
+	      let m = Names.string_of_id m in
+	      let f = (String.uncapitalize m) ^ ".ml" in
+	      Ocaml.extract_to_file f (extract_module m))
+       | _ -> assert false)
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 1ff031f41..661cfef3d 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -218,7 +218,8 @@ let rec push_many_rels_ctx keep_prop env ctx = function
       (env, ctx)
 
 let fix_environment env ctx fl tl =
-  push_many_rels_ctx true env ctx (List.combine fl (Array.to_list tl))
+  let tl' = Array.mapi lift tl in
+  push_many_rels_ctx true env ctx (List.combine fl (Array.to_list tl'))
 
 (* Decomposition of a type beginning with at least n products when reduced *)
 
@@ -499,9 +500,10 @@ and extract_term_with_type env ctx c t =
 	       let (_,e) = extract_branch_aux 0 br.(0) in 	  
 	       Rmlterm e)
     | IsFix ((_,i),(ti,fi,ci)) ->
+	let n = Array.length ti in
 	let (env', ctx') = fix_environment env ctx fi ti in
-	let extract_fix_body c t = 
-	  match extract_constr_with_type env' ctx' c t with
+	let extract_fix_body c t =
+	  match extract_constr_with_type env' ctx' c (lift n t) with
 	    | Eprop -> MLprop 
 	    | Emltype _ -> MLarity
 	    | Emlterm a -> a
@@ -570,9 +572,8 @@ and signature_of_application env f t a =
   else 
     let f' = mkApp (f, Array.sub a 0 nbp) in 
     let a' = Array.sub a nbp (nargs-nbp) in 
-    let t' = Typing.type_of env Evd.empty t in
+    let t' = Typing.type_of env Evd.empty f' in
     s @ signature_of_application env f' t' a'
-
 	  
 
 (*s Extraction of a constr. *)
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index c218f9c31..8ad3f7556 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -32,8 +32,7 @@ type extraction_result =
 
 (*s Extraction functions. *)
 
-val extract_constr : 
-  env -> extraction_context -> constr -> extraction_result
+val extract_constr : env -> extraction_context -> constr -> extraction_result
 
 (*s ML declaration corresponding to a Coq reference. *)
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 86217971f..144891849 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -15,6 +15,7 @@ open Util
 open Names
 open Term
 open Miniml
+open Mlutil
 
 (*s Some utility functions. *)
 
@@ -364,6 +365,9 @@ end
 
 module Pp = Make(OcamlParams)
 
+let pp_ast a = Pp.pp_ast (betared_ast (uncurrify_ast a))
+let pp_decl d = Pp.pp_decl (betared_decl (uncurrify_decl d))
+
 let ocaml_preamble () =
   [< 'sTR "type prop = Prop"; 'fNL; 'fNL;
      'sTR "type arity = Arity"; 'fNL; 'fNL >]
@@ -374,7 +378,7 @@ let extract_to_file f decls =
   pP_with ft (hV 0 (ocaml_preamble ()));
   begin 
     try
-      List.iter (fun d -> mSGNL_with ft (Pp.pp_decl d)) decls
+      List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
     with e ->
       pp_flush_with ft (); close_out cout; raise e
   end;