synchonization des tables d'extraction

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

3 files changed, 35 insertions, 14 deletions

diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 2680724a3..8f362e74b 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -5,4 +5,3 @@
 
  7. Eta expansion pour contourner typage Caml
 
- 8. Synchroniser Reset & les tables 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 2c723a078..0a0ec8029 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -20,6 +20,7 @@ open Instantiate
 open Miniml
 open Mlutil
 open Closure
+open Summary
 
 (*s Extraction results. *)
 
@@ -279,6 +280,21 @@ let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table
 let constant_table = 
   ref (Gmap.empty : (section_path, extraction_result) Gmap.t)
 
+(* Tables synchronization. *)
+
+let freeze () =
+  !inductive_extraction_table, !constructor_extraction_table, !constant_table
+
+let unfreeze (it,cst,ct) =
+  inductive_extraction_table := it;
+  constructor_extraction_table := cst;
+  constant_table := ct
+
+let _ = declare_summary "Extraction tables"
+	  { freeze_function = freeze;
+	    unfreeze_function = unfreeze;
+	    init_function = (fun () -> ());
+	    survive_section = true }
 
 (*s Extraction of a type. *)
 
@@ -338,10 +354,10 @@ and extract_type_rec_info env vl c args =
 	if is_arity env Evd.empty cty then
 	  (match extract_constant sp with 
 	     | Emltype (Miniml.Tarity,_,_) -> Tarity
-	       | Emltype (Miniml.Tprop,_,_) -> Tprop
-	       | Emltype (mlt, sc, vlc) ->  
-		   extract_type_app env vl (ConstRef sp,sc,vlc) args 
-	       | Emlterm _ -> assert false) 
+	     | Emltype (Miniml.Tprop,_,_) -> Tprop
+	     | Emltype (mlt, sc, vlc) ->  
+		 extract_type_app env vl (ConstRef sp,sc,vlc) args 
+	     | Emlterm _ -> assert false) 
 	else begin
 	  (* We can't keep as ML type abbreviation a CIC constant 
 	     which type is not an arity: we reduce this constant. *)
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index b4b6f30a6..b143615cf 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -163,6 +163,11 @@ let rec pp_type par t =
     de Bruijn variables. [args] is the list of collected arguments
     (already pretty-printed). *)
 
+let expr_needs_par = function
+  | MLlam _  -> true
+  | MLcase _ -> true
+  | _        -> false 
+
 let rec pp_expr par env args = 
   let apply st = match args with
     | [] -> st
@@ -186,10 +191,15 @@ let rec pp_expr par env args =
           apply [< 'sTR "("; st; 'sTR ")" >]
     | MLletin (id,a1,a2) ->
 	let id',env' = push_vars [id] env in
-	hOV 0 [< hOV 2 [< 'sTR "let "; pr_id (List.hd id'); 'sTR " ="; 'sPC;
-			  pp_expr false env [] a1; 'sPC; 'sTR "in" >];
-		 'sPC;
-		 pp_expr false env' [] a2 >] 
+	let par' = par || args <> [] in
+	let par2 = not par' && expr_needs_par a2 in
+	apply 
+	  (hOV 0 [< open_par par';
+		    hOV 2 [< 'sTR "let "; pr_id (List.hd id'); 'sTR " ="; 'sPC;
+			     pp_expr false env [] a1; 'sPC; 'sTR "in" >];
+		    'sPC;
+		    pp_expr par2 env' [] a2;
+		    close_par par' >])
     | MLglob r -> 
 	apply (pp_global r)
     | MLcons (r,_,[]) ->
@@ -226,11 +236,7 @@ let rec pp_expr par env args =
 and pp_pat env pv = 
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev ids) env in
-    let par = match t with
-      | MLlam _  -> true
-      | MLcase _ -> true
-      | _        -> false 
-    in
+    let par = expr_needs_par t in
     hOV 2 [< pp_global name;
 	     begin match ids with 
 	       | [] -> [< >]