changements de dernieres minutes pour la 8.1 beta:

- qualification correcte des noms en Haskell
- on imprime les types de toutes les fonctions en Haskell
- en Ocaml, les appels recursifs d'une f : 'a truc doivent 
 se faire avec les _meme_ parametres de types 'a. Exemple illegal: 
   let rec f = function [] -> 0 | l -> f [l];;
 On met maintenant des Obj.magic en conséquence. 
 En Haskell (avec typage fourni), ca passe. 



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

7 files changed, 80 insertions, 31 deletions

diff --git a/CHANGES b/CHANGES
index f6e75bfd37..f2d672233c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -98,9 +98,12 @@ Tactics
 
 Extraction
  
-- all type parts should now disappear instead of sometimes producing _ 
+- All type parts should now disappear instead of sometimes producing _ 
   (for instance in Map.empty).
-- TODO bug fixes...
+- Haskell extraction: types of functions are now printed, better 
+  unsafeCoerce mechanism, both for hugs and ghc
+- Scheme extraction improved, see http://www.pps.jussieu.fr/~letouzey/scheme
+- Many bug fixes
 
 Modules
 
@@ -124,7 +127,7 @@ Notations
 Libraries
 
 - New library on String and Ascii characters (contributed by L. Thery)
-- New library FSets+FMaps of finite sets and maps (TODO doc quelque part)
+- New library FSets+FMaps of finite sets and maps (TODO doc)
 - New library QArith on rational numbers
 - Small extension of Zmin.V, new Zmax.v, new Zminmax.v
 - Reworking of the files on classical logic and description principles
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index b6d9f2da76..6db146b1e5 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -290,7 +290,10 @@ module StdParams = struct
       else match lang () with 
 	| Scheme -> [s] (* no modular Scheme extraction... *)
 	| Toplevel -> [s] (* idem *)
-	| Haskell -> ls (* for the moment we always qualify in Haskell *)
+	| Haskell -> 
+	    if !modular then 
+	      ls (* for the moment we always qualify in modular Haskell *)
+	    else [s]
 	| Ocaml -> 
 	    try (* has [mp] something in common with one of those in [mpl] ? *)
 	      let pref = common_prefix_from_list mp mpl in 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 485b75b9f2..a6565aa872 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -35,6 +35,9 @@ exception I of inductive_info
    to avoid loops in [extract_inductive] *)
 let internal_call = ref KNset.empty
 
+(* A set of all fixpoint functions currently being extracted *)
+let current_fixpoints = ref ([] : constant list)
+
 let none = Evd.empty
 
 let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
@@ -574,12 +577,18 @@ and extract_cst_app env mle mlt kn args =
   (* First, the [ml_schema] of the constant, in expanded version. *) 
   let nb,t = record_constant_type env kn None in 
   let schema = nb, expand env t in 
+  (* Can we instantiate types variables for this constant ? *)
+  (* In Ocaml, inside the definition of this constant, the answer is no. *)
+  let instantiated = 
+    if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
+    else instantiation schema
+  in 
   (* Then the expected type of this constant. *)
-  let metas = List.map new_meta args in 
+  let a = new_meta () in 
   (* We compare stored and expected types in two steps. *)
   (* First, can [kn] be applied to all args ? *)
-  let a = new_meta () in 
-  let magic1 = needs_magic (type_recomp (metas, a), instantiation schema) in 
+  let metas = List.map new_meta args in 
+  let magic1 = needs_magic (type_recomp (metas, a), instantiated) in 
   (* Second, is the resulting type compatible with the expected type [mlt] ? *)
   let magic2 = needs_magic (a, mlt) in 
   (* The internal head receives a magic if [magic1] *)
@@ -789,8 +798,10 @@ let extract_fixpoint env vkn (fi,ti,ci) =
   let n = Array.length vkn in 
   let types = Array.make n (Tdummy Kother)
   and terms = Array.make n MLdummy in 
+  let kns = Array.to_list vkn in 
+  current_fixpoints := kns; 
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
-  let sub = List.rev_map mkConst (Array.to_list vkn) in 
+  let sub = List.rev_map mkConst kns in 
   for i = 0 to n-1 do 
     if sort_of env ti.(i) <> InProp then begin 
       let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 15270bbf2a..5b2ff86360 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -210,7 +210,7 @@ and pp_function env f t =
   (f ++ pr_binding (List.rev bl) ++
      str " =" ++ fnl () ++ str "  " ++
      hov 2 (pp_expr false env' [] t'))
-	
+
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_comment s = str "-- " ++ s ++ fnl ()
@@ -289,12 +289,16 @@ let pp_decl mpl =
 	    else str "=" ++ spc () ++ pp_type false l t
 	in 
 	hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl ()
-  | Dfix (rv, defs,_) ->
-      let ppv = Array.map pp_global rv in 
-      prlist_with_sep (fun () -> fnl () ++ fnl ())
-	(fun (pi,ti) -> pp_function (empty_env ()) pi ti)
-	(List.combine (Array.to_list ppv) (Array.to_list defs)) 
-      ++ fnl () ++ fnl ()
+  | Dfix (rv, defs, typs) ->
+      let max = Array.length rv in 
+      let rec iter i = 
+	if i = max then mt () 
+	else
+	  let e = pp_global rv.(i) in 
+	  e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () 
+	  ++ pp_function (empty_env ()) e defs.(i) ++ fnl () ++ fnl () 
+	  ++ iter (i+1)
+      in iter 0
   | Dterm (r, a, t) ->
       if is_inline_custom r then mt () 
       else 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 15d219e491..18629bcec4 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -343,13 +343,9 @@ and pp_pat env i pv =
 and pp_function env f t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars bl env in
-  let is_function pv =
-    let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
-    not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl)
-  in
   match t' with 
-    | MLcase(i,MLrel 1,pv) when i=Standard ->
-	if is_function pv then
+    | MLcase(i,MLrel 1,pv) when i=Standard -> 
+	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then 
 	  (f ++ pr_binding (List.rev (List.tl bl)) ++
        	     str " = function" ++ fnl () ++
 	     v 0 (str "  | " ++ pp_pat env' i pv))
@@ -358,7 +354,6 @@ and pp_function env f t =
              str " = match " ++
 	     pr_id (List.hd bl) ++ str " with" ++ fnl () ++
 	     v 0 (str "  | " ++ pp_pat env' i pv))
-	  
     | _ -> (f ++ pr_binding (List.rev bl) ++
 	      str " =" ++ fnl () ++ str "  " ++
 	      hov 2 (pp_expr false env' [] t'))
diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend
index 1ed9e24f2b..31d46eeb4f 100644
--- a/contrib/extraction/test/.depend
+++ b/contrib/extraction/test/.depend
@@ -242,6 +242,16 @@ theories/FSets/fSetProperties.cmx: theories/Init/specif.cmx \
     theories/FSets/fSetProperties.cmi 
 theories/FSets/fSets.cmo: theories/FSets/fSets.cmi 
 theories/FSets/fSets.cmx: theories/FSets/fSets.cmi 
+theories/FSets/fSetToFiniteSet.cmo: theories/Init/specif.cmi \
+    theories/Setoids/setoid.cmi theories/FSets/orderedTypeEx.cmi \
+    theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+    theories/FSets/fSetProperties.cmi theories/Init/datatypes.cmi \
+    theories/FSets/fSetToFiniteSet.cmi 
+theories/FSets/fSetToFiniteSet.cmx: theories/Init/specif.cmx \
+    theories/Setoids/setoid.cmx theories/FSets/orderedTypeEx.cmx \
+    theories/FSets/orderedType.cmx theories/Lists/list.cmx \
+    theories/FSets/fSetProperties.cmx theories/Init/datatypes.cmx \
+    theories/FSets/fSetToFiniteSet.cmi 
 theories/FSets/fSetWeakFacts.cmo: theories/Init/specif.cmi \
     theories/Setoids/setoid.cmi theories/FSets/fSetWeakInterface.cmi \
     theories/Init/datatypes.cmi theories/FSets/fSetWeakFacts.cmi 
@@ -440,14 +450,20 @@ theories/Lists/theoryList.cmx: theories/Init/specif.cmx \
     theories/Lists/theoryList.cmi 
 theories/Logic/berardi.cmo: theories/Logic/berardi.cmi 
 theories/Logic/berardi.cmx: theories/Logic/berardi.cmi 
-theories/Logic/choiceFacts.cmo: theories/Logic/choiceFacts.cmi 
-theories/Logic/choiceFacts.cmx: theories/Logic/choiceFacts.cmi 
+theories/Logic/choiceFacts.cmo: theories/Init/specif.cmi \
+    theories/Init/datatypes.cmi theories/Logic/choiceFacts.cmi 
+theories/Logic/choiceFacts.cmx: theories/Init/specif.cmx \
+    theories/Init/datatypes.cmx theories/Logic/choiceFacts.cmi 
 theories/Logic/classicalChoice.cmo: theories/Logic/classicalChoice.cmi 
 theories/Logic/classicalChoice.cmx: theories/Logic/classicalChoice.cmi 
-theories/Logic/classicalDescription.cmo: \
-    theories/Logic/classicalDescription.cmi 
-theories/Logic/classicalDescription.cmx: \
-    theories/Logic/classicalDescription.cmi 
+theories/Logic/classicalDescription.cmo: theories/Init/specif.cmi \
+    theories/Logic/choiceFacts.cmi theories/Logic/classicalDescription.cmi 
+theories/Logic/classicalDescription.cmx: theories/Init/specif.cmx \
+    theories/Logic/choiceFacts.cmx theories/Logic/classicalDescription.cmi 
+theories/Logic/classicalEpsilon.cmo: theories/Init/specif.cmi \
+    theories/Logic/choiceFacts.cmi theories/Logic/classicalEpsilon.cmi 
+theories/Logic/classicalEpsilon.cmx: theories/Init/specif.cmx \
+    theories/Logic/choiceFacts.cmx theories/Logic/classicalEpsilon.cmi 
 theories/Logic/classicalFacts.cmo: theories/Logic/classicalFacts.cmi 
 theories/Logic/classicalFacts.cmx: theories/Logic/classicalFacts.cmi 
 theories/Logic/classical.cmo: theories/Logic/classical.cmi 
@@ -464,10 +480,16 @@ theories/Logic/classical_Prop.cmx: theories/Logic/eqdepFacts.cmx \
     theories/Logic/classical_Prop.cmi 
 theories/Logic/classical_Type.cmo: theories/Logic/classical_Type.cmi 
 theories/Logic/classical_Type.cmx: theories/Logic/classical_Type.cmi 
+theories/Logic/classicalUniqueChoice.cmo: \
+    theories/Logic/classicalUniqueChoice.cmi 
+theories/Logic/classicalUniqueChoice.cmx: \
+    theories/Logic/classicalUniqueChoice.cmi 
 theories/Logic/decidable.cmo: theories/Logic/decidable.cmi 
 theories/Logic/decidable.cmx: theories/Logic/decidable.cmi 
-theories/Logic/diaconescu.cmo: theories/Logic/diaconescu.cmi 
-theories/Logic/diaconescu.cmx: theories/Logic/diaconescu.cmi 
+theories/Logic/diaconescu.cmo: theories/Init/specif.cmi \
+    theories/Logic/diaconescu.cmi 
+theories/Logic/diaconescu.cmx: theories/Init/specif.cmx \
+    theories/Logic/diaconescu.cmi 
 theories/Logic/eqdep_dec.cmo: theories/Init/specif.cmi \
     theories/Logic/eqdep_dec.cmi 
 theories/Logic/eqdep_dec.cmx: theories/Init/specif.cmx \
@@ -921,6 +943,10 @@ theories/FSets/fSetList.cmi: theories/Init/specif.cmi \
 theories/FSets/fSetProperties.cmi: theories/Init/specif.cmi \
     theories/Setoids/setoid.cmi theories/Lists/list.cmi \
     theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi 
+theories/FSets/fSetToFiniteSet.cmi: theories/Init/specif.cmi \
+    theories/Setoids/setoid.cmi theories/FSets/orderedTypeEx.cmi \
+    theories/FSets/orderedType.cmi theories/Lists/list.cmi \
+    theories/Init/datatypes.cmi 
 theories/FSets/fSetWeakFacts.cmi: theories/Init/specif.cmi \
     theories/Setoids/setoid.cmi theories/FSets/fSetWeakInterface.cmi \
     theories/Init/datatypes.cmi 
@@ -994,6 +1020,13 @@ theories/Lists/setoidList.cmi: theories/Init/specif.cmi \
 theories/Lists/streams.cmi: theories/Init/datatypes.cmi 
 theories/Lists/theoryList.cmi: theories/Init/specif.cmi \
     theories/Lists/list.cmi theories/Init/datatypes.cmi 
+theories/Logic/choiceFacts.cmi: theories/Init/specif.cmi \
+    theories/Init/datatypes.cmi 
+theories/Logic/classicalDescription.cmi: theories/Init/specif.cmi \
+    theories/Logic/choiceFacts.cmi 
+theories/Logic/classicalEpsilon.cmi: theories/Init/specif.cmi \
+    theories/Logic/choiceFacts.cmi 
+theories/Logic/diaconescu.cmi: theories/Init/specif.cmi 
 theories/Logic/eqdep_dec.cmi: theories/Init/specif.cmi 
 theories/NArith/binNat.cmi: theories/Init/specif.cmi \
     theories/Init/datatypes.cmi theories/NArith/binPos.cmi 
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 5f8a40f62b..65a5409039 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -10,7 +10,7 @@ AXIOMSVO:= \
 theories/Reals/% \
 theories/Num/%
 
-DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name .svn))
+DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -path \*.svn\*))
 
 INCL:= $(patsubst %,-I %,$(DIRS))