optimizations extraction

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

5 files changed, 57 insertions, 29 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index c99d270ca8..e9a21c0d31 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -108,6 +108,9 @@ end
 
 module Pp = Ocaml.Make(ToplevelParams)
 
+let pp_ast a = Pp.pp_ast (normalize a)
+let pp_decl a = Pp.pp_decl (normalize_decl a)
+
 open Vernacinterp
 
 let extract_reference r =
@@ -115,7 +118,7 @@ let extract_reference r =
     (if is_ml_extraction r then
        [< 'sTR "User defined extraction:"; 'sPC; 'sTR (find_ml_extraction r) >]
      else
-       Pp.pp_decl (extract_declaration r))
+       pp_decl (extract_declaration r))
 
 let _ = 
   vinterp_add "Extraction"
@@ -132,7 +135,7 @@ let _ =
 		| _ ->
 		    match extract_constr (Global.env()) [] c with
 		      | Emltype (t,_,_) -> mSGNL (Pp.pp_type t)
-		      | Emlterm a -> mSGNL (Pp.pp_ast a))
+		      | Emlterm a -> mSGNL (pp_ast a))
        | _ -> assert false)
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
@@ -159,7 +162,7 @@ let _ =
   vinterp_add "ExtractionRec"
     (fun vl () ->
        let rl' = decl_of_refs (refs_of_vargl vl) in
-       List.iter (fun d -> mSGNL (Pp.pp_decl d)) rl')
+       List.iter (fun d -> mSGNL (pp_decl d)) rl')
 
 (*s Extraction parameters. *)
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 29941f617e..1c95e4b045 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -824,7 +824,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, t))
+	 | Emlterm t -> Dglob (r, uncurrify_ast t))
   | IndRef (sp,_) -> extract_inductive_declaration sp
   | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
   | VarRef _ -> assert false
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 358097c3b8..06a0963410 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -141,28 +141,57 @@ let nb_occur a =
   in 
   count 1 a; !cpt
 
-(*s Beta-reduction *)
+(*s Beta-iota reduction *)
 
-let rec betared_ast = function
+let constructor_index = function
+  | ConstructRef (_,j) -> pred j
+  | _ -> assert false
+
+let rec normalize = function
   | MLapp (f, []) ->
-      betared_ast f
+      normalize f
   | MLapp (f, a) ->
-      let f' = betared_ast f 
-      and a' = List.map betared_ast a in
+      let f' = normalize f 
+      and a' = List.map normalize a in
       (match f' with
+	 (* beta redex *)
 	 | MLlam (id,t) -> 
 	     (match nb_occur t with
-		| 0 -> betared_ast (MLapp (ml_pop t, List.tl a'))
-		| 1 -> betared_ast (MLapp (ml_subst (List.hd a') t,List.tl a'))
+		| 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', 
-				betared_ast (MLapp (t, List.tl a'))))
+				normalize (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')))
+	 (* application of a case: we push arguments inside *)
+	 | MLcase (e,br) ->
+	     let br' = 
+	       Array.map 
+      	       	 (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'')))) 
+		 br 
+	     in
+      	     normalize (MLcase (e,br'))
 	 | _ ->
 	     MLapp (f',a'))
+  | MLcase (e,br) ->
+      (match normalize e with
+	 (* iota redex *)
+	 | 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))
+	 | e' -> 
+	     MLcase (e', Array.map (fun (n,l,t) -> (n,l,normalize t)) br))
   | a -> 
-      ast_map betared_ast a
+      ast_map normalize a
     
-let betared_decl = function
- | Dglob (id, a) -> Dglob (id, betared_ast a)
+let normalize_decl = function
+ | Dglob (id, a) -> Dglob (id, normalize a)
  | d -> d
 
 (*s [uncurrify] uncurrifies the applications of constructors. *)
@@ -231,8 +260,6 @@ let subst_glob_decl r m = function
   | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
-let normalize = betared_ast
-
 let expansion_test r t = false
 
 let expand prm r t = 
@@ -248,13 +275,15 @@ let rec optimize prm = function
       []
   | (Dtype _ | Dabbrev _) as d :: l -> 
       d :: (optimize prm l)
+  | Dglob (_, MLprop) :: l ->
+      optimize prm l
   (*i
   | Dglob(id,(MLexn _ as t)) as d :: l ->
       let l' = List.map (expand (id,t)) l in optimize prm l'
   i*)	    
-  | [ Dglob(r,t) ] ->
+  | [ Dglob (r,t) ] ->
       let t' = normalize t in [ Dglob(r,t') ]
-  | Dglob(r,t) as d :: l ->
+  | Dglob (r,t) as d :: l ->
       let t' = normalize t in
       if expand prm r t' then begin
 	warning_expansion r;
@@ -264,7 +293,7 @@ let rec optimize prm = function
 	else
 	  optimize prm l'
       end else 
-	(Dglob(r,t')) :: (optimize prm l)
+	(Dglob (r,t')) :: (optimize prm l)
 
 (*s Table for direct ML extractions. *)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 768695e0a8..ca4268e3be 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -33,16 +33,16 @@ val ml_lift : int -> ml_ast -> ml_ast
 
 val ml_subst : ml_ast -> ml_ast -> ml_ast
 
-(*s Some transformations of ML terms. [betared_ast] and [betared_ecl] reduce
+(*s Some transformations of ML terms. [normalize] and [normalize_decl] reduce
     all beta redexes (when the argument does not occur, it is just
     thrown away; when it occurs exactly once it is substituted; otherwise
-    a let in redex is created for clarity) *)
+    a let in redex is created for clarity) and iota redexes, plus some other
+    optimizations. *)
 
-val betared_ast : ml_ast -> ml_ast
-val betared_decl : ml_decl -> ml_decl
+val normalize : ml_ast -> ml_ast
+val normalize_decl : ml_decl -> ml_decl
 
 val uncurrify_ast : ml_ast -> ml_ast
-val uncurrify_decl : ml_decl -> ml_decl
 
 (*s Optimization. *)
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index b143615cf5..d6390d6333 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -350,8 +350,6 @@ let pp_decl = function
 	       pp_function (empty_env ()) (pp_global r) a; 'fNL >]
 
 let pp_type = pp_type false
-let pp_ast a = pp_ast (betared_ast (uncurrify_ast a))
-let pp_decl d = pp_decl (betared_decl (uncurrify_decl d))
 
 end
 
@@ -445,8 +443,6 @@ let ocaml_preamble () =
      'sTR "let arity = ()"; 'fNL; 'fNL >]
 
 let extract_to_file f prm decls =
-  let decls = List.map 
-		(fun d -> betared_decl (uncurrify_decl d)) decls in
   let decls = optimize prm decls in
   let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in
   let cout = open_out f in