suite des modifs concernant les optimisations divers

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

5 files changed, 124 insertions, 115 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 23264fb075..974a47a59d 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -244,10 +244,6 @@ let decompose_lam_eta n env c =
     let e = applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in
     (rb, e)
 
-let rec abstract_n n a = 
-  if n = 0 then a else MLlam (anonymous, ml_lift 1 (abstract_n (n-1) a))
-
-
 
 (*s Error message when extraction ends on an axiom. *)
 
@@ -573,7 +569,7 @@ and abstract_constructor cp  =
     | (_,Arity) :: l -> 
 	abstract rels i l
   in
-  abstract_n n (abstract [] 1 s)
+  anonym_lams (ml_lift n (abstract [] 1 s)) n
 
 (* Extraction of a case *)
 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 28c0612c96..f3d64fceee 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -103,7 +103,7 @@ let rec pp_expr par env args =
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
     | MLlam _ as a -> 
-      	let fl,a' = collect_lambda a in
+      	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
 	let st = [< pp_abst (List.rev fl); pp_expr false env' [] a' >] in
 	if args = [] then
@@ -194,7 +194,7 @@ and pp_fix par env in_p (ids,bl) args =
      close_par par >]
 
 and pp_function env f t =
-  let bl,t' = collect_lambda t in
+  let bl,t' = collect_lams t in
   let bl,env' = push_vars bl env in
   [< f; pr_binding (List.rev bl);
      'sTR " ="; 'fNL; 'sTR "  ";
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index b047b10038..27c971c65c 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -81,8 +81,8 @@ let rec occurs_itvl k k' = function
   | MLcase(t,pv) -> 
       (occurs_itvl k k' t) ||
       (array_exists
-	 (fun (_,l,t') -> 
-	    let n = List.length l in occurs_itvl (k + n) (k' + n) t') pv)
+         (fun (_,l,t') -> 
+            let n = List.length l in occurs_itvl (k + n) (k' + n) t') pv)
   | MLfix(_,l,cl) -> 
       let n = Array.length l in occurs_itvl_vect (k + n) (k' + n) cl
   | MLcast(t,_) -> occurs_itvl k k' t
@@ -119,14 +119,14 @@ let ml_liftn k n c =
     | MLrel i as c -> if i < n then c else MLrel (i+k)
     | MLlam (id,t) -> MLlam (id, liftrec (n+1) t)
     | MLletin (id,a,b) -> MLletin (id, liftrec n a, liftrec (n+1) b)
-    | MLcase (t,pl) -> 
+    | MLcase (t,pv) -> 
 	MLcase (liftrec n t,
       	       	Array.map (fun (id,idl,p) -> 
 			     let k = List.length idl in
-			     (id, idl, liftrec (n+k) p)) pl)
-    | MLfix (n0,idl,pl) -> 
+			     (id, idl, liftrec (k+n) p)) pv)
+    | MLfix (n0,idl,pv) -> 
 	MLfix (n0,idl,
-	       let k = Array.length idl in Array.map (liftrec (n+k)) pl)
+	       let k = Array.length idl in Array.map (liftrec (k+n)) pv)
     | a -> ast_map (liftrec n) a
   in 
   if k = 0 then c else liftrec n c
@@ -196,6 +196,48 @@ let nb_occur a =
   in 
   count 1 a; !cpt
 
+(*s The two following functions test and create [MLrel n;...;MLrel 1] *)
+
+let rec test_eta_args n = function 
+  | [] -> n=0
+  | a :: q -> (a = (MLrel n)) && (test_eta_args (pred n) q)
+
+let rec make_eta_args n = 
+  if n = 0 then [] else (MLrel n)::(make_eta_args (pred n))
+  
+(*s [generalize_check k k' i] return true if there is a [(Rel j)] 
+   in [t] with [k<=i<=k'] *)
+
+exception Impossible
+
+let check_and_generalize (r0,l,c) = 
+  let nargs = List.length l in 
+  let rec genrec k k' = function 
+    | MLrel i as c -> 
+	if i<k then c 
+	else if i>k' then MLrel (i-nargs+1) 
+	else raise Impossible
+    | MLcons(r,args) when r=r0 -> 
+	if (test_eta_args nargs args) then MLrel k
+	else raise Impossible
+    | MLlam(id,t) -> MLlam(id,genrec (k + 1) (k' + 1) t)
+    | MLletin(id,t,t') -> MLletin(id,(genrec k k' t),(genrec (k+1) (k'+1) t'))
+    | MLcase(t,pv) -> 
+	MLcase(genrec k k' t,
+	       Array.map (fun (id,idl,t') -> 
+			    let n = List.length idl in 
+			    (id,idl,genrec (k+n) (k'+n) t')) pv)
+    | MLfix(n0,idl,pv) -> 
+	MLfix(n0,idl,
+	      let n = Array.length idl in Array.map (genrec (k+n) (k'+n)) pv)
+    | a -> ast_map (genrec k k') a
+  in genrec 1 nargs c  
+
+let check_case br = 
+  let f = check_and_generalize br.(0) in 
+  for i = 1 to Array.length br - 1 do 
+    if check_and_generalize br.(i) <> f then raise Impossible 
+  done; f
 
 (*s Some Beta-iota reductions + simplifications*)
 
@@ -207,38 +249,6 @@ let is_atomic = function
   | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity -> true
   | _ -> false
 
-exception Impossible
-
-let check_identity_case br = 
-  let rec check_list k = function 
-    | [] -> ()
-    | t :: q -> 
-	if t <> MLrel k then raise Impossible;
-	check_list (k-1) q
-  in
-  let check_one_branch (r,l,t) = 
-    match t with 
-      | MLcons (r',l') -> 
-	  if r<>r' then raise Impossible;
-	  check_list (List.length l) l'
-      | _ -> raise Impossible
-  in 
-  Array.iter check_one_branch br
-
-
-let check_constant_case br = 
-  let (_,l,t) = br.(0) in
-  let n = List.length l in 
-  if occurs_itvl 1 n t then raise Impossible; 
-  let cst = ml_lift (-n) t in 
-  for i = 1 to Array.length br - 1 do 
-    let (_,l,t) = br.(i) in
-    let n = List.length l in
-    if (occurs_itvl 1 n t) || (cst <> (ml_lift (-n) t)) 
-    then raise Impossible
-  done; cst
- 
-
 let all_constr br = 
   try 
     Array.iter 
@@ -250,7 +260,6 @@ let all_constr br =
     true
   with Impossible -> false
   
-
 let normalize a = 
   let o = optim() in 
   let rec simplify = function
@@ -308,10 +317,10 @@ let normalize a =
 	   | e' -> 
 	       let br' = Array.map (fun (n,l,t) -> (n,l,simplify t)) br in 
 	       if o then
-		 try check_identity_case br'; e' 
-		 with Impossible -> 
-		   try check_constant_case br' 
-		   with Impossible -> MLcase (e', br')
+		 try 
+		   let f = check_case br' in 
+		   simplify (MLapp (MLlam (anonymous,f),[e']))
+		 with Impossible -> MLcase (e', br')
 	       else MLcase (e', br'))
     | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> 
 	(* expansion of a letin in special cases *)
@@ -325,72 +334,65 @@ let normalize a =
 	ast_map simplify a 
   in simplify (merge_app a)
 
-(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
+let normalize_decl = function
+ | Dglob (id, a) -> Dglob (id, normalize a)
+ | d -> d
+
+(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
     the list [idn;...;id1] and the term [t]. *)
 
-let collect_lambda = 
+let collect_lams = 
   let rec collect acc = function
     | MLlam(id,t) -> collect (id::acc) t
     | x           -> acc,x
   in 
   collect []
 
-let rec pass_n_lambda n = function 
-  | MLlam(_,t)-> pass_n_lambda (n-1) t
-  | _ -> raise Impossible
+(* [named_abstract] does the converse of [collect_lambda] *)
 
-let rec test_eta n = function 
-  | [] -> n=0
-  | a :: q -> (a = (MLrel n)) && (test_eta (pred n) q)
-
-let rec make_args n = 
-  if n = 0 then [] else (MLrel n)::(make_args (pred n))
-  
-(* this abstract is written without lift on purpose *)
-let rec abstract ids a = match ids with
+let rec named_lams a = function 
   | [] -> a 
-  | id :: l -> abstract l (MLlam(id,a))
+  | id :: ids -> named_lams (MLlam(id,a)) ids
+
+let rec anonym_lams a = function 
+  | 0 -> a 
+  | n -> anonym_lams (MLlam(anonymous,a)) (pred n)
+
+(*s special treatment of non-mutual fixpoint for pretty-printing purpose *)
 
 let optimize_fix a = 
   if not (optim()) then a 
   else
-    let lams,b = collect_lambda a in 
-    let n = List.length lams in 
+    let ids,a' = collect_lams a in 
+    let n = List.length ids in 
     if n = 0 then a 
     else  
-      (match b with 
+      (match a' with 
 	 | MLfix(_,[|f|],[|c|]) ->
-	     let new_f = MLapp (MLrel (n+1),make_args n) in 
-	     let new_c = abstract lams (ml_subst new_f c)
+	     let new_f = MLapp (MLrel (n+1),make_eta_args n) in 
+	     let new_c = named_lams (ml_subst new_f c) ids
 	     in MLfix(0,[|f|],[|new_c|])
-	 | MLapp(b,ids) ->
-	     (match b with 
-		| MLfix(_,[|_|],[|_|]) when (test_eta n ids)-> b
-		| MLfix(_,[|f|],[|c|]) -> a
-(* TODO: tenir compte des occurrences des ids 
+	 | MLapp(a',args) ->
+	     (match a' with 
+		| MLfix(_,[|_|],[|_|]) when (test_eta_args n args)-> a'
+		| MLfix(_,[|f|],[|c|]) -> 
 		    (try 
+		      let m = List.length args in 
 		      let v = Array.make n 0 in 
-		      let m = List.length ids in 
-		      list_iter_i (fun i t -> 
-				     (match t with 
-					  MLrel j when v.(j-1)=0 -> v.(j-1)<-(succ i)
-					| _ -> raise Impossible)) ids;
-		      let args = array_fold_left_i
-				   (fun i accum j -> 
-				      let r = if j=0 then (succ i)+m else j 
-				      in (MLrel r) :: accum) [] v in
-		      let new_f = 
-			abstract (List.map (fun _ ->anonymous) ids)
-			  (MLapp (MLrel (m+n+1),args)) in  
-		      let new_c = abstract lams (normalize (ml_subst new_f c))
+		      for i=0 to (n-1) do v.(i)<-i done;
+		      let aux i = function 
+			  MLrel j when v.(j-1)>=0 -> v.(j-1)<-(-i-1)
+			| _ -> raise Impossible
+		      in
+		      list_iter_i aux args; 
+		      let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
+		      let new_f = anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in  
+		      let new_c = named_lams (normalize (MLapp ((ml_subst new_f c),args))) ids
 		      in MLfix(0,[|f|],[|new_c|])
 		    with Impossible -> a) 
-*)		| _ -> a)
+		| _ -> a)
 	 | _ -> a)
 
-let normalize_decl = function
- | Dglob (id, a) -> Dglob (id, normalize a)
- | d -> d
 
 (*s Utility functions used for the decision of expansion *)
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 2c5a586acf..3771151b42 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -42,15 +42,22 @@ val ml_subst : ml_ast -> ml_ast -> ml_ast
 val subst_glob_ast : global_reference -> ml_ast -> ml_ast -> ml_ast
 
 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
-    the list [id1;...;idn] and the term [t]. *)
+    the list [idn;...;id1] and the term [t]. *)
+
+val collect_lams : ml_ast -> identifier list * ml_ast
+
+(* [named_abstract] is the converse of [collect_lambda]. *)
+
+val named_lams : ml_ast -> identifier list -> ml_ast
+
+val anonym_lams : ml_ast -> int -> ml_ast
 
-val collect_lambda : ml_ast -> identifier list * ml_ast
 
 (*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) and iota redexes, plus some other
-    optimizations. *)
+    optimizations. *)  (* TO UPDATE *)
 
 val normalize : ml_ast -> ml_ast
 val normalize_decl : ml_decl -> ml_decl
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1a7d151fb3..4470e00ac6 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -158,6 +158,7 @@ let expr_needs_par = function
   | _        -> false 
 
 let rec pp_expr par env args = 
+  let par' = args <> [] || par in 
   let apply st = match args with
     | [] -> st
     | _  -> hOV 2 [< open_par par; st; 'sPC;
@@ -171,16 +172,12 @@ let rec pp_expr par env args =
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
     | MLlam _ as a -> 
-      	let fl,a' = collect_lambda a in
+      	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
 	let st = [< pp_abst (List.rev fl); pp_expr false env' [] a' >] in
-	if args = [] then
-          [< open_par par; st; close_par par >]
-        else
-          apply [< 'sTR "("; st; 'sTR ")" >]
+	[< open_par par'; st; close_par par' >]
     | MLletin (id,a1,a2) ->
 	let id',env' = push_vars [id] env in
-	let par' = par || args <> [] in
 	let par2 = not par' && expr_needs_par a2 in
 	apply 
 	  (hOV 0 [< open_par par';
@@ -199,12 +196,20 @@ let rec pp_expr par env args =
     | MLcons (r,args') ->
 	[< open_par par; pp_global r; 'sPC;
 	   pp_tuple (pp_expr true env []) args'; close_par par >]
+    | MLcase (t,[|x|])->
+	apply 
+	  (hOV 0 [< open_par par'; 'sTR "let ";  
+		    pp_one_pat 
+		      [< 'sTR " ="; 'sPC;
+			 pp_expr false env [] t; 'sPC; 'sTR "in" >] 
+		      env x;
+		    close_par par' >])
     | MLcase (t, pv) ->
       	apply
-      	  [< if args <> [] then [< 'sTR "(" >]  else open_par par;
+      	  [< open_par par';
       	     v 0 [< 'sTR "match "; pp_expr false env [] t; 'sTR " with";
 		    'fNL; 'sTR "  "; pp_pat env pv >];
-	     if args <> [] then [< 'sTR ")" >] else close_par par >]
+	     close_par par' >]
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
@@ -222,18 +227,17 @@ let rec pp_expr par env args =
 	[< open_par true; 'sTR "Obj.magic"; 'sPC; 
 	   pp_expr false env args a; close_par true >]
 
+and pp_one_pat s env (r,ids,t) = 
+  let ids,env' = push_vars (List.rev ids) env in
+  let par = expr_needs_par t in
+  [< pp_global r; 
+     if ids = [] then [< >] 
+     else [< 'sTR " "; pp_boxed_tuple pr_id (List.rev ids) >];
+     s; 'sPC; pp_expr par env' [] t >]
+  
 and pp_pat env pv = 
-  let pp_one_pat (name,ids,t) =
-    let ids,env' = push_vars (List.rev ids) env in
-    let par = expr_needs_par t in
-    hOV 2 [< pp_global name;
-	     begin match ids with 
-	       | [] -> [< >]
-	       | _  -> [< 'sTR " "; pp_boxed_tuple pr_id (List.rev ids) >]
-	     end;
-	     'sTR " ->"; 'sPC; pp_expr par env' [] t >]
-  in 
-  [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
+  [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) 
+       (fun x -> hOV 2 (pp_one_pat (string " ->") env x)) pv >]
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
@@ -260,7 +264,7 @@ and pp_fix par env in_p (ids,bl) args =
      close_par par >]
 
 and pp_function env f t =
-  let bl,t' = collect_lambda t in
+  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