Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.

Du coup MLcons avec 2 args seulement.
Ne reclame pas de realiser axioms sur Prop.
Optimizations=true par default pour Extraction Module.
Simplifications naives des letin.
Merge_app avant normalisation.
Booleen expansion_test pour l'optimisation, avec test de strictness.


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

8 files changed, 172 insertions, 89 deletions

diff --git a/contrib/extraction/BUGS b/contrib/extraction/BUGS
index 8b13789179..7f3f59c190 100644
--- a/contrib/extraction/BUGS
+++ b/contrib/extraction/BUGS
@@ -1 +1,2 @@
-
+It's not a bug, it's a lack of feature !!
+Cf TODO.
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 8f362e74b2..27069ffdce 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -5,3 +5,11 @@
 
  7. Eta expansion pour contourner typage Caml
 
+ 9. Doc!! (exemples)
+
+ 10. Recommenter extraction.ml
+
+ 11. tester contribs
+	
+ 12. garantir typage Caml => magic + cast.
+
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index e9a21c0d31..2095541b0b 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -62,7 +62,7 @@ and visit_ast eenv a =
     | MLapp (a,l) -> visit a; List.iter visit l
     | MLlam (_,a) -> visit a
     | MLletin (_,a,b) -> visit a; visit b
-    | MLcons (r,_,l) -> visit_reference eenv r; List.iter visit l
+    | MLcons (r,l) -> visit_reference eenv r; List.iter visit l
     | MLcase (a,br) -> 
 	visit a; Array.iter (fun (r,_,a) -> visit_reference eenv r; visit a) br
     | MLfix (_,_,l) -> List.iter visit l
@@ -171,10 +171,10 @@ let interp_options keep modular = function
       { optimization = false; modular = modular; 
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | [VARG_STRING "nooption"] ->
-      { optimization = not modular; modular = modular;
+      { optimization = true; modular = modular;
 	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
   | VARG_STRING "expand" :: l ->
-      { optimization = not modular; modular = modular;
+      { optimization = true; modular = modular;
 	to_keep = refs_set_of_list keep; 
 	to_expand = refs_set_of_list (refs_of_vargl l) }
   | _ -> 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 1c95e4b045..e068842579 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -519,7 +519,7 @@ and extract_term_info_with_type env ctx c t =
 		    | [var]->var
 		    | _ -> assert false
 		else
-		  MLcons (ConstructRef cp, List.length rels, rels)
+		  MLcons (ConstructRef cp, rels)
 	    | (Info,NotArity) :: l -> 
 		MLlam (id_of_name Anonymous, abstract (i :: rels) (succ i) l)
 	    | (Logic,NotArity) :: l ->
@@ -667,18 +667,21 @@ and extract_constant sp =
   try
     Gmap.find sp !constant_table
   with Not_found ->
+    let env = Global.env() in    
     let cb = Global.lookup_constant sp in
     let typ = cb.const_type in
-    let body = match cb.const_body with 
-      | Some c -> c 
-      | None -> axiom_message sp
-    in
-    let env = Global.env() in
-    let e = extract_constr_with_type env [] body typ in
-    let e = eta_expanse e (extract_type env typ) in
-    constant_table := Gmap.add sp e !constant_table;
-    e
-    
+    match cb.const_body with
+      | None ->
+          (match v_of_arity env typ with
+             | (Info,_) -> axiom_message sp
+             | (Logic,Arity) -> Emltype (Miniml.Tarity,[],[])
+             | (Logic,NotArity) -> Emlterm MLprop)
+      | Some body ->
+          let e = extract_constr_with_type env [] body typ in
+          let e = eta_expanse e (extract_type env typ) in
+          constant_table := Gmap.add sp e !constant_table;
+          e
+
 (*s Extraction of an inductive. *)
     
 and extract_inductive ((sp,_) as i) =
@@ -824,7 +827,7 @@ let extract_declaration r = match r with
   | ConstRef sp -> 
       (match extract_constant sp with
 	 | Emltype (mlt, s, vl) -> Dabbrev (r, List.rev vl, mlt)
-	 | Emlterm t -> Dglob (r, uncurrify_ast t))
+	 | Emlterm t -> Dglob (r, t))
   | IndRef (sp,_) -> extract_inductive_declaration sp
   | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
   | VarRef _ -> assert false
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 12702e38ce..88f757f387 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -37,7 +37,7 @@ type ml_ast =
   | MLlam   of identifier * ml_ast
   | MLletin of identifier * ml_ast * ml_ast
   | MLglob  of global_reference
-  | MLcons  of global_reference * int * ml_ast list
+  | MLcons  of global_reference * ml_ast list
   | MLcase  of ml_ast * (global_reference * identifier list * ml_ast) array
   | MLfix   of int * identifier list * ml_ast list
   | MLexn   of identifier
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 06a0963410..23e105f574 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -22,7 +22,7 @@ open Miniml
 let anonymous = id_of_string "x"
 let prop_name = id_of_string "_"
 
-(* In an ML type, update the arguments to all inductive types [(sp,_)] *)		  
+(*s In an ML type, update the arguments to all inductive types [(sp,_)] *)		  
 
 let rec update_args sp vl = function  
   | Tapp ( Tglob r :: l ) -> 
@@ -40,7 +40,7 @@ let rec occurs k = function
   | MLrel i -> i = k
   | MLapp(t,argl) -> (occurs k t) || (occurs_list k argl)
   | MLlam(_,t) -> occurs (k + 1) t
-  | MLcons(_,_,argl) -> occurs_list k argl
+  | MLcons(_,argl) -> occurs_list k argl
   | MLcase(t,pv) -> 
       (occurs k t) ||
       (array_exists
@@ -56,7 +56,7 @@ let rec ast_map f = function
   | MLapp (a,al) -> MLapp (f a, List.map f al)
   | MLlam (id,a) -> MLlam (id, f a)
   | MLletin (id,a,b) -> MLletin (id, f a, f b)
-  | MLcons (c,n,al) -> MLcons (c, n, List.map f al)
+  | MLcons (c,al) -> MLcons (c, List.map f al)
   | MLcase (a,eqv) -> MLcase (f a, Array.map (ast_map_eqn f) eqv)
   | MLfix (fi,ids,al) -> MLfix (fi, ids, List.map f al)
   | MLcast (a,t) -> MLcast (f a, t)
@@ -120,6 +120,17 @@ let rec ml_subst v =
   in 
   subst 1 v
 
+(*s simplification of any [MLapp (MLapp (_,_),_)] *)
+
+let rec merge_app a = match a with 
+  | MLapp (f,l) -> 
+      let f' = merge_app f in 
+      let l' = List.map merge_app l in 
+      (match f' with 
+	 | MLapp (f'',l'') -> MLapp (f'',l'' @ l')
+	 | _ -> MLapp (f', l'))
+  | _ -> ast_map merge_app a
+
 (*s Number of occurences of [Rel 1] in [a]. *)
 
 let nb_occur a =
@@ -134,36 +145,44 @@ let nb_occur a =
     | MLfix (_,ids,cl) -> 
 	let k = List.length ids in List.iter (count (n + k)) cl
     | MLapp (a,l) -> count n a; List.iter (count n) l
-    | MLcons (_,_,l) ->  List.iter (count n) l
+    | MLcons (_,l) ->  List.iter (count n) l
     | MLmagic a -> count n a
     | MLcast (a,_) -> count n a
     | MLprop | MLexn _ | MLglob _ | MLarity -> ()
   in 
   count 1 a; !cpt
 
-(*s Beta-iota reduction *)
+
+(*s Beta-iota reduction + simplifications*)
 
 let constructor_index = function
   | ConstructRef (_,j) -> pred j
   | _ -> assert false
 
-let rec normalize = function
+let is_atomic = function 
+  | MLrel _ 
+  | MLglob _ 
+  | MLexn _
+  | MLprop | MLarity -> true
+  | _ -> false
+
+let rec betaiota = function
   | MLapp (f, []) ->
-      normalize f
+      betaiota f
   | MLapp (f, a) ->
-      let f' = normalize f 
-      and a' = List.map normalize a in
+      let f' = betaiota f 
+      and a' = List.map betaiota a in
       (match f' with
 	 (* beta redex *)
 	 | MLlam (id,t) -> 
 	     (match nb_occur t with
-		| 0 -> normalize (MLapp (ml_pop t, List.tl a'))
-		| 1 -> normalize (MLapp (ml_subst (List.hd a') t,List.tl a'))
-		| _ -> MLletin (id, List.hd a', 
-				normalize (MLapp (t, List.tl a'))))
+		| 0 -> betaiota (MLapp (ml_pop t, List.tl a'))
+		| 1 -> betaiota (MLapp (ml_subst (List.hd a') t,List.tl a'))
+		| _ -> betaiota (MLletin (id, List.hd a', 
+					  MLapp (t, List.tl a'))))
 	 (* application of a let in: we push arguments inside *)
 	 | MLletin (id,e1,e2) ->
-	     MLletin (id, e1, normalize (MLapp (e2, List.map (ml_lift 1) a')))
+	     MLletin (id, e1, betaiota (MLapp (e2, List.map (ml_lift 1) a')))
 	 (* application of a case: we push arguments inside *)
 	 | MLcase (e,br) ->
 	     let br' = 
@@ -171,72 +190,33 @@ let rec normalize = function
       	       	 (fun (n,l,t) -> 
 		    let k = List.length l in
 		    let a'' = List.map (ml_lift k) a' in
-      	       	    (n, l, normalize (MLapp (t,a'')))) 
+      	       	    (n, l, betaiota (MLapp (t,a'')))) 
 		 br 
 	     in
-      	     normalize (MLcase (e,br'))
+      	     betaiota (MLcase (e,br'))
 	 | _ ->
 	     MLapp (f',a'))
   | MLcase (e,br) ->
-      (match normalize e with
+      (match betaiota e with
 	 (* iota redex *)
-	 | MLcons (r,_,a) ->
+	 | MLcons (r,a) ->
 	     let j = constructor_index r in
 	     let (_,ids,c) = br.(j) in
 	     let c' = List.fold_right (fun id t -> MLlam (id,t)) ids c in
-	     normalize (MLapp (c',a))
+	     betaiota (MLapp (c',a))
 	 | e' -> 
-	     MLcase (e', Array.map (fun (n,l,t) -> (n,l,normalize t)) br))
+	     MLcase (e', Array.map (fun (n,l,t) -> (n,l,betaiota t)) br))
+  | MLletin(i,c,e) when (is_atomic c) || (nb_occur e <= 1) -> 
+      betaiota (ml_subst c e)
   | a -> 
-      ast_map normalize a
+      ast_map betaiota a
     
+let normalize a = betaiota (merge_app a)
+
 let normalize_decl = function
  | Dglob (id, a) -> Dglob (id, normalize a)
  | d -> d
 
-(*s [uncurrify] uncurrifies the applications of constructors. *)
-
-let rec is_constructor_app = function
-  | MLcons _ -> true
-  | MLapp (a,_) -> is_constructor_app a
-  | _ -> false
-
-let rec decomp_app = function
-  | MLapp (f,args) -> 
-      let (c,n,args') = decomp_app f in (c, n, args' @ args)
-  | MLcons (c,n,args) ->
-      (c,n,args)
-  | _ ->
-      assert false
-
-let rec n_lam n a =
-  if n = 0 then a else MLlam (anonymous, n_lam (pred n) a)
-
-let eta_expanse c n args =
-  let dif = n - List.length args in
-  assert (dif >= 0);
-  if dif > 0 then
-    let rels = List.rev_map (fun n -> MLrel n) (interval 1 dif) in
-    n_lam dif (MLcons (c, n, (List.map (ml_lift dif) args) @ rels))
-  else
-    MLcons (c,n,args)
-
-let rec uncurrify_ast a = match a with
-  | MLapp (f,_) when is_constructor_app f -> 
-      let (c,n,args) = decomp_app a in
-      let args' = List.map uncurrify_ast args in
-      eta_expanse c n args'
-  | MLcons (c,n,args) ->
-      let args' = List.map uncurrify_ast args in
-      eta_expanse c n args'
-  | _ -> 
-      ast_map uncurrify_ast a
-
-let uncurrify_decl = function
- | Dglob (id, a) -> Dglob (id, uncurrify_ast a)
- | d -> d
-
-
 (*s Optimization. *)
 
 module Refset = 
@@ -260,11 +240,104 @@ let subst_glob_decl r m = function
   | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
-let expansion_test r t = false
+(* Utilites functions used for the decision of expansion *)
+
+let rec ml_size = function
+    MLapp(t,l)     -> (List.length l) + (ml_size t) + (ml_size_list l)
+  | MLlam(_,t)     -> 1 + (ml_size t)
+  | MLcons(_,l)  -> ml_size_list l
+  | MLcase(t,pv)   -> 1 + (ml_size t) + (array_fold_right_from 0 
+					   (fun (_,_,t) a -> a+(ml_size t)) pv 0)
+  | MLfix(_,_,f) -> ml_size_list f
+  | MLletin (_,_,t) -> ml_size t
+  | MLcast (t,_) -> ml_size t
+  | MLmagic t -> ml_size t
+  | _              -> 0
+and ml_size_list l = List.fold_left (fun a t -> a+(ml_size t)) 0 l
+
+let is_fix = function MLfix _ -> true | _ -> false
+
+let rec is_constr = function
+    MLcons _   -> true
+  | MLlam(_,t) -> is_constr t
+  | _          -> false
+
+
+exception Toplevel
+
+let rec lift n l = List.map (fun x->x+n) l
+
+let rec pop n l = List.map 
+		    (fun x -> if (x-n<0) then raise Toplevel else x-n) l 
+
+let rec non_stricts add cand = function 
+  | MLlam (id,t) -> 
+      let cand = lift 1 cand in
+      let cand = if add then 1::cand else cand in
+      pop 1 (non_stricts add cand t)
+  | MLrel n ->  List.filter (fun x->(x<>n)) cand  
+  | MLapp (MLrel n, _) -> List.filter (fun x->(x<>n)) cand
+  | MLapp (t,l)-> 
+      let cand = non_stricts false cand t in 
+      List.fold_left (non_stricts false) cand l 
+  | MLcons (_,l) -> List.fold_left (non_stricts false) cand l
+  | MLletin (_,t1,t2) -> 
+      let cand = non_stricts false cand t1 in 
+      pop 1 (non_stricts add (lift 1 cand) t2)
+  | MLfix (_,i,f)-> 
+      let n = List.length i in
+      let cand = lift n cand in 
+      let cand = List.fold_left (non_stricts false) cand f in 
+      pop n cand
+  | MLcase (t,v) -> 
+      let cand = non_stricts false cand t in 
+      array_fold_left_from 0 
+	(fun c (_,i,t)-> 
+	   let n = List.length i in 
+	   let cand = lift n cand in 
+	   let cand = pop n (non_stricts add cand t) in
+	   Sort.merge (<=) cand c)
+	[] v
+  | MLcast (t,_) -> non_stricts add cand t
+  | MLmagic t -> non_stricts add cand t
+  | _ -> cand
+
+let is_not_strict t = 
+  try let _ = non_stricts true [] t in false
+  with 
+    | Toplevel -> true
+
+
+(* [expansion_test] answers the following question: 
+   If we could expand [t] (the user said nothing special), 
+   should we expand ? 
+   
+   We don't expand fixpoints, but always inductive constructors.
+   Last case of expansion is a term not to big with at least one 
+   non-strict variable (i.e. a variable that may not be evaluated). *)
+
+let expansion_test t = 
+  (not (is_fix t))
+  &&
+  ((is_constr t) 
+  ||
+   ((ml_size t < 10)
+    &&
+    (is_not_strict t)))
+
+(* If the user doesn't say he wants to keep [t], we expand in two cases:
+   \begin{itemize}
+   \item the user explicitly requests it 
+   \item [expansion_test] answers that the expansion is a good idea, and 
+   we are free to act (no [noopt] given as argument)
+   \end{itemize} *)
 
 let expand prm r t = 
-  (not (Refset.mem r prm.to_keep)) &&
-  (Refset.mem r prm.to_expand || (prm.optimization && expansion_test r t))
+  (not (Refset.mem r prm.to_keep)) (* if user DOES want to keep it *)
+  &&
+  (Refset.mem r prm.to_expand (* if user DOES want to expand it *) 
+  || 
+   (prm.optimization && expansion_test t)) 
 
 let warning_expansion r = 
   wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index ca4268e3be..0602567cb7 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -42,8 +42,6 @@ val ml_subst : ml_ast -> ml_ast -> ml_ast
 val normalize : ml_ast -> ml_ast
 val normalize_decl : ml_decl -> ml_decl
 
-val uncurrify_ast : ml_ast -> ml_ast
-
 (*s Optimization. *)
 
 module Refset : Set.S with type elt = global_reference
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index d6390d6333..e53f5371db 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -202,12 +202,12 @@ let rec pp_expr par env args =
 		    close_par par' >])
     | MLglob r -> 
 	apply (pp_global r)
-    | MLcons (r,_,[]) ->
+    | MLcons (r,[]) ->
 	pp_global r
-    | MLcons (r,_,[a]) ->
+    | MLcons (r,[a]) ->
 	[< open_par par; pp_global r; 'sPC;
 	   pp_expr true env [] a; close_par par >]
-    | MLcons (r,_,args') ->
+    | MLcons (r,args') ->
 	[< open_par par; pp_global r; 'sPC;
 	   pp_tuple (pp_expr true env []) args'; close_par par >]
     | MLcase (t, pv) ->