maj CHANGES extraction + bug extraction & _

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

6 files changed, 186 insertions, 15 deletions

diff --git a/CHANGES b/CHANGES
index 623ded3eae..d978702e9d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,15 @@ Tactics
 - Slight improvement in naming strategy for NewInduction/NewDestruct
 - Intuition/Tauto do not perform useless unfolding and work up to conversion
 
+Extraction
+
+See contrib/extraction/CHANGES or documentation. In brief: 
+- Syntax changes: there are no more options inside the extraction commands. 
+  New commands for customization and options have been introduced instead. 
+- More optimizations on extracted code. 
+- Extraction tests are now embbeded in 14 user contributions. 
+
+
 Standard library
 
 - In [Relations], Rstar.v and Newman.v now axiom-free. 
diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES
index e1f5f194cd..f14db4fa1a 100644
--- a/contrib/extraction/CHANGES
+++ b/contrib/extraction/CHANGES
@@ -1,3 +1,160 @@
+7.1 -> 7.2 :
+
+* Syntax changes, see Documentation for more details: 
+
+Set/Unset Extraction Optimize. 
+
+Default is Set. This control all optimizations made on the ML terms 
+(mostly reduction of dummy beta/iota redexes, but also simplications on 
+Cases, etc). Put this option to Unset if you what a ML term as close as 
+possible to the Coq term.
+
+Set/Unset Extraction AutoInline. 
+
+Default in Set, so by default, the extraction mechanism feels free to 
+inline the bodies of some defined constants, according to some heuristics 
+like size of bodies, useness of some arguments, etc. Those heuristics are 
+not always perfect, you may want to disable this feature, do it by Unset. 
+
+Extraction Inline toto foo. 
+Extraction NoInline titi faa bor. 
+
+In addition to the automatic inline feature, you can now tell precisely to 
+inline some more constants by the Extraction Inline command. Conversely, 
+you can forbid the inlining of some specific constants by automatic inlining. 
+Those two commands enable a precise control of what is inlined and what is not. 
+
+Print Extraction Inline. 
+
+Sum up the current state of the table recording the custom inlings 
+(Extraction (No)Inline). 
+
+Reset Extraction Inline. 
+
+Put the table recording the custom inlings back to empty. 
+
+As a consequence, there is no more need for options inside the commands of 
+extraction: 
+
+Extraction foo. 
+Recursive Extraction foo bar. 
+Extraction "file" foo bar. 
+Extraction Module Mymodule. 
+Recursive Extraction Module Mymodule. 
+
+New: The last syntax extracts the module Mymodule and all the modules 
+it depends on. 
+
+You can also try the Haskell versions (not tested yet): 
+
+Haskell Extraction foo.
+Haskell Recursive Extraction foo bar.
+Haskell Extraction "file" foo bar.
+Haskell Extraction Module Mymodule.
+Haskell Recursive Extraction Module Mymodule.
+
+And there's still the realization syntax: 
+
+Extract Constant coq_bla => "caml_bla".
+Extract Inlined Constant coq_bla => "caml_bla".
+Extract Inductive myinductive => mycamlind [my_caml_constr1 ... ].
+
+Note that now, the Extract Inlined Constant command is sugar for an Extract 
+Constant followed by a Extraction Inline. So be careful with 
+Reset Extraction Inline. 
+
+ 
+
+* Lot of works around optimization of produced code. Should make code more 
+readable. 
+
+- fixpoint definitions : there should be no more stupid printings like 
+
+let foo x = 
+  let rec f x = 
+    .... (f y) ....
+  in f x
+
+but rather 
+
+let rec foo x = 
+  .... (foo y) .... 
+
+- generalized iota (in particular iota and permutation cases/cases):
+
+A generalized iota redex is a "Cases e of ...." where e is ok. 
+And the recursive predicate "ok" is given by:  
+e is ok if e is a Constructor or a Cases where all branches are ok.
+In the case of generalized iota redex, it might be good idea to reduce it, 
+so we do it. 
+Example: 
+
+match (match t with 
+         O -> Left
+       | S n -> match n with 
+                  O -> Right 
+                | S m -> Left) with 
+ Left -> blabla 
+| Right -> bloblo
+
+After simplification, that gives: 
+
+match t with 
+  O -> blabla
+| S n -> match n with 
+          O -> bloblo
+        | S n -> blabla
+
+As shown on the example, code duplication can occur. In practice 
+it seems not to happen frequently. 
+
+- "constant" case:
+In V7.1 we used to simplify cases where all branches are the same. 
+In V7.2 we can simplify in addition terms like 
+	cases e of 
+	  C1 x y -> f (C x y)
+	| C2 z -> f (C2 z) 
+If x y z don't occur in f, we can produce (f e). 
+
+- permutation cases/fun: 
+extracted code has frequenty functions in branches of cases: 
+
+let foo x = match x with 
+   O -> fun _ -> .... 
+ | S y -> fun _ -> .... 
+
+the optimization consist in lifting the common "fun _ ->", and that gives
+ 
+let foo x _ = match x with 
+   O -> .....
+ | S y -> ....
+ 
+
+* Some bug corrections (many thanks in particular to Michel Levy). 
+
+* Testing in coq contributions: 
+If you are interested in extraction, you can look at the extraction tests 
+I'have put in the following coq contributions 
+
+Bordeaux/Additions			computation of fibonacci(2000)
+Bordeaux/EXCEPTIONS			multiplication using exception.
+Bordeaux/SearchTrees			list -> binary tree. maximum.
+Dyade/BDDS				boolean tautology checker.
+Lyon/CIRCUITS				multiplication via a modelization of a circuit.
+Lyon/FIRING-SQUAD			print the states of the firing squad.
+Marseille/CIRCUITS			compares integers via a modelization of a circuit. 
+Nancy/FOUnify				unification of two first-orderde deux termes.
+Rocq/ARITH/Chinese			computation of the chinese remaindering.  
+Rocq/COC				small coc typechecker. (test by B. Barras, not by me)
+Rocq/HIGMAN				run the proof on one example. 
+Rocq/GRAPHS				linear constraints checker in Z. 
+Sophia-Antipolis/Stalmarck		boolean tautology checker.
+Suresnes/BDD				boolean tautology checker.
+
+Just do "make" in those contributions, the extraction test is integrated. 
+More tests will follow on more contributions.
+
+
 
 7.0 -> 7.1 : mostly bug corrections. No theoretical problems dealed with.
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 4db7ce6227..1f12662870 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -205,7 +205,7 @@ let sign_of_arity env c =
 let vl_of_lbinders = 
   lbinders_fold 
     (fun n _ v a -> 
-       if v = info_arity then (next_ident_away (id_of_name n) a)::a else a) []
+       if v = info_arity then (next_ident_away (id_of_name n) (prop_name::a))::a else a) []
   
 let vl_of_arity env c = vl_of_lbinders env (List.rev (fst (decompose_prod c)))
 	 
@@ -357,7 +357,7 @@ and extract_type_rec_info env c vl args =
     | Const sp when args = [] && is_ml_extraction (ConstRef sp) ->
 	Tmltype (Tglob (ConstRef sp), vl)
     | Const sp when is_axiom sp -> 
-	let id = next_ident_away (basename sp) vl in 
+	let id = next_ident_away (basename sp) (prop_name::vl) in 
 	Tmltype (Tvar id,  id :: vl)
     | Const sp ->
 	let t = constant_type env sp in 
@@ -379,7 +379,7 @@ and extract_type_rec_info env c vl args =
 	       extract_type_app env (IndRef spi,si,vli) vl args 
 	   |Iprop -> assert false (* Cf. initial tests *))
     | Case _ | Fix _ | CoFix _ ->
-	let id = next_ident_away flexible_name vl in
+	let id = next_ident_away flexible_name (prop_name::vl) in
 	Tmltype (Tvar id,  id :: vl)
 	  (* Type without counterpart in ML: we generate a 
 	     new flexible type variable. *) 
@@ -398,7 +398,7 @@ and extract_prod_lam env (n,t,d) vl flag =
     | (Info, Arity), _ -> 
 	(* We rename before the [push_rel], to be sure that the corresponding*)
 	(* [lookup_rel] will be correct. *)
-	let id' = next_ident_away (id_of_name n) vl in 
+	let id' = next_ident_away (id_of_name n) (prop_name::vl) in 
 	let env' = push_rel_assum (Name id', t) env in
 	extract_type_rec_info env' d (id'::vl) []
     | (Logic, Arity), _ | _, Lam ->
@@ -454,7 +454,7 @@ and extract_type_app env (r,sc,vlc) vl args =
   assert (nvlargs >= 0);
   let vl'' = 
     List.fold_right 
-      (fun id l -> (next_ident_away id l) :: l) 
+      (fun id l -> (next_ident_away id (prop_name::l)) :: l) 
       (list_firstn nvlargs vlc) vl'
   in
   (* We complete the list of arguments of [c] by variables *)
@@ -542,25 +542,26 @@ and extract_term_info_wt env ctx c t =
    match kind_of_term c with
      | Lambda (n, t, d) ->
 	 let v = v_of_t env t in 
-	 let env' = push_rel_assum (n,t) env in
+	 let id = next_ident_away (id_of_name n) [prop_name] in 
+	 let env' = push_rel_assum (Name id,t) env in
 	 let ctx' = (snd v = NotArity) :: ctx in
 	 let d' = extract_term_info env' ctx' d in
 	 (* If [d] was of type an arity, [c] too would be so *)
 	 (match v with
 	    | _,Arity -> d'
             | Logic,NotArity -> MLlam (prop_name, d')
-            | Info,NotArity -> MLlam (id_of_name n, d'))
+            | Info,NotArity -> MLlam (id, d'))
      | LetIn (n, c1, t1, c2) ->
 	 let v = v_of_t env t1 in
-	 let env' = push_rel (n,Some c1,t1) env in
+	 let id = next_ident_away (id_of_name n) [prop_name] in 
+	 let env' = push_rel (Name id,Some c1,t1) env in
 	 (match v with
 	    | (Info, NotArity) -> 
 		let c1' = extract_term_info_wt env ctx c1 t1 in
 		let c2' = extract_term_info env' (true :: ctx) c2 in
 		(* If [c2] was of type an arity, [c] too would be so *)
-		MLletin (id_of_name n,c1',c2')
-	    | _ ->
-		extract_term_info env' (false :: ctx) c2)
+		MLletin (id,c1',c2')
+	    | _ -> extract_term_info env' (false :: ctx) c2)
      | Rel n ->
 	 MLrel (renum_db ctx n)
      | Const sp ->
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index fcba0fcb55..cda6e4a9c9 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -102,7 +102,9 @@ let rec pp_expr par env args =
   in
   function
     | MLrel n -> 
-	apply (pr_id (get_db_name n env))
+	let id = get_db_name n env in 
+	apply (if string_of_id id = "_" then str "prop" else pr_id id)
+	  (* HACK, should disappear soon *)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 53408461f5..98c2317ec2 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -28,7 +28,7 @@ exception Impossible
 let anonymous = id_of_string "x"
 let prop_name = id_of_string "_"
 
-let no_prop_name = 
+let prop_name_to_anonymous = 
   List.map (fun i -> if i=prop_name then anonymous else i)
 
 (*s In an ML type, update the arguments to all inductive types [(sp,_)] *)  
@@ -383,7 +383,7 @@ and simplify_case o br e =
 	  check_constant_case br 
 	with Impossible ->
 	  if (is_atomic e) then (* Swap the case and the lam if possible *)
-	    let ids = no_prop_name (permut_case_fun br []) in 
+	    let ids = prop_name_to_anonymous (permut_case_fun br []) in 
 	    let n = List.length ids in 
 	    if n = 0 then MLcase (e, br) 
 	    else named_lams (MLcase (ml_lift n e, br)) ids
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 6705b8a4b1..42cd5a54bc 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -175,7 +175,9 @@ let rec pp_expr par env args =
   in
   function
     | MLrel n -> 
-	apply (pr_id (get_db_name n env))
+	let id = get_db_name n env in 
+	apply (if string_of_id id = "_" then str "prop" else pr_id id)
+	  (* HACK, should disappear soon *)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f