Extraction: less eta in calls to global functions, better optimization phase

 - we saturate the normalize function : as long as
    (kill_dummy + simpl) isn't a nop, we do it again.
 - generalize_case allowed on all types of theories/Init/*.v
   instead of only bool,sumbool,sumor. NB: this optim cannot
   be performed on any type, it might produce untyped code.
 - common_branch allowed on match with one branch: in this
   situation it indicates whether the match can be removed or not.

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

3 files changed, 58 insertions, 51 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 667f2e91a0..e7c2e23f7d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -142,6 +142,12 @@ let rec sign_kind = function
 	| SafeLogicalSig | EmptySig ->
 	    if k = Kother then UnsafeLogicalSig else SafeLogicalSig
 
+(* Removing the final [Keep] in a signature *)
+
+let rec no_final_keeps = function
+  | [] -> []
+  | k :: s -> let s' = k :: no_final_keeps s in if s' = [Keep] then [] else s'
+
 (*S Management of type variable contexts. *)
 
 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]
@@ -595,19 +601,18 @@ and extract_app env mle mlt mk_head args =
   let metas = List.map new_meta args in
   let type_head = type_recomp (metas, mlt) in
   let mlargs = List.map2 (extract_maybe_term env mle) metas args in
-  if mlargs = [] then mk_head type_head else MLapp (mk_head type_head, mlargs)
+  mlapp (mk_head type_head) mlargs
 
 (*s Auxiliary function used to extract arguments of constant or constructor. *)
 
 and make_mlargs env e s args typs =
-  let l = ref s in
-  let keep () = match !l with [] -> true | b :: s -> l:=s; b=Keep in
   let rec f = function
-    | [], [] -> []
-    | a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt))
-    | _::la, _::lt -> f (la,lt)
+    | [], [], _ -> []
+    | a::la, t::lt, [] -> extract_maybe_term env e t a :: (f (la,lt,[]))
+    | a::la, t::lt, Keep::s -> extract_maybe_term env e t a :: (f (la,lt,s))
+    | _::la, _::lt, _::s -> f (la,lt,s)
     | _ -> assert false
-  in f (args,typs)
+  in f (args,typs,s)
 
 (*s Extraction of a constant applied to arguments. *)
 
@@ -632,9 +637,11 @@ and extract_cst_app env mle mlt kn args =
   (* The internal head receives a magic if [magic1] *)
   let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
   (* Now, the extraction of the arguments. *)
-  let s = type2signature env (snd schema) in
+  let s_full = type2signature env (snd schema) in
+  let s = no_final_keeps s_full in
   let ls = List.length s in
   let la = List.length args in
+  (* The ml arguments, already expunged from known logical ones *)
   let mla = make_mlargs env mle s args metas in
   let mla =
     if not magic1 then
@@ -645,32 +652,27 @@ and extract_cst_app env mle mlt kn args =
       with _ -> mla
     else mla
   in
+  (* For strict languages, purely logical signatures with at least
+     one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
+     accordingly. *)
+  let optdummy = match sign_kind s_full with
+    | UnsafeLogicalSig when lang () <> Haskell -> [MLdummy]
+    | _ -> []
+  in
   (* Different situations depending of the number of arguments: *)
-  match sign_kind s with
-    | EmptySig -> put_magic_if magic2 head
-    | NonLogicalSig ->
-	if la >= ls || List.for_all ((=) Keep) s
-	then
-	  put_magic_if (magic2 && not magic1) (MLapp (head, mla))
-	else
-	  (* Non-pure function partially applied. We complete via eta. *)
-	  let ls' = ls-la in
-	  let s' = list_lastn ls' s in
-	  let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
-	  put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s')
-    | UnsafeLogicalSig when lang () <> Haskell ->
-	(* For strict languages, purely logical signatures with at least
-	   one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
-	   accordingly. *)
-	if la >= ls
-	then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla))
-	else put_magic_if magic2 (dummy_lams head (ls-la-1))
-    | _ ->
-	(* s is made only of [Kill Ktype], or we have a lazy target language *)
-	if la >= ls
-	then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
-	else put_magic_if magic2 (dummy_lams head (ls-la))
-
+  if la >= ls
+  then
+    (* Enough args, cleanup already done in [mla], we only add the
+       additionnal dummy if needed. *)
+    put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla))
+  else
+    (* Partially applied function with some logical arg missing.
+       We complete via eta and expunge logical args. *)
+    let ls' = ls-la in
+    let s' = list_skipn la s in
+    let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
+    let e = anonym_or_dummy_lams (mlapp head mla) s' in
+    put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
 
 (*s Extraction of an inductive constructor applied to arguments. *)
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 268011444f..37e5e6a617 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -341,6 +341,8 @@ let type_expunge env t =
 
 (*S Generic functions over ML ast terms. *)
 
+let mlapp f a = if a = [] then f else MLapp (f,a)
+
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
    of the number of bingings crossed before reaching the [MLrel]. *)
 
@@ -662,22 +664,19 @@ let check_and_generalize (r0,l,c) =
 (* CAVEAT: this optimization breaks typing in some special case. example:
    [type 'x a = A]. Then [let f = function A -> A] has type ['x a -> 'y a],
    which is incompatible with the type of [let f x = x].
-   By default, we brutally disable this optim except for some known types:
-   [bool], [sumbool], [sumor] *)
+   By default, we brutally disable this optim except for the known types
+   in theories/Init/*.v *)
 
-let generalizable_list =
-  let datatypes = MPfile (dirpath_of_string "Coq.Init.Datatypes")
-  and specif = MPfile (dirpath_of_string "Coq.Init.Specif")
-  in
-  [ make_mind datatypes empty_dirpath (mk_label "bool");
-    make_mind specif empty_dirpath (mk_label "sumbool");
-    make_mind specif empty_dirpath (mk_label "sumor") ]
+let generalizable_mind m =
+  match mind_modpath m with
+    | MPfile dir -> is_dirpath_prefix_of (dirpath_of_string "Coq.Init") dir
+    | _ -> false
 
 let check_generalizable_case unsafe br =
   if not unsafe then
     (match br.(0) with
      | ConstructRef ((kn,_),_), _, _ ->
-	 if not (List.mem kn generalizable_list) then raise Impossible
+	 if not (generalizable_mind kn) then raise Impossible
      | _ -> assert false);
   let f = check_and_generalize br.(0) in
   for i = 1 to Array.length br - 1 do
@@ -704,7 +703,7 @@ let common_branches br =
   let best = ref [] in
   Hashtbl.iter
     (fun _ l -> if List.length l > List.length !best then best := l) tab;
-  if List.length !best < 2 then [] else !best
+  if Array.length br >= 2 && List.length !best < 2 then [] else !best
 
 (*s If all branches are functions, try to permut the case and the functions. *)
 
@@ -778,10 +777,8 @@ let is_atomic = function
 (* Some beta-iota reductions + simplifications. *)
 
 let rec simpl o = function
-  | MLapp (f, []) ->
-      simpl o f
-  | MLapp (f, a) ->
-      simpl_app o (List.map (simpl o) a) (simpl o f)
+  | MLapp (f, []) -> simpl o f
+  | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f)
   | MLcase (i,e,br) ->
       let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
       simpl_case o i br (simpl o e)
@@ -803,6 +800,8 @@ let rec simpl o = function
       else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
   | a -> ast_map (simpl o) a
 
+(* invariant : list [a] of arguments is non-empty *)
+
 and simpl_app o a = function
   | MLapp (f',a') -> simpl_app o (a'@a) f'
   | MLlam (Dummy,t) ->
@@ -831,6 +830,8 @@ and simpl_app o a = function
 	(* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
+(* Invariant : all empty matches should now be [MLexn] *)
+
 and simpl_case o i br e =
   if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
     simpl o (iota_gen br e)
@@ -842,7 +843,7 @@ and simpl_case o i br e =
     with Impossible ->
       (* Detect common branches *)
       let common_br = if not o.opt_case_cst then [] else common_branches br in
-      if List.length common_br = Array.length br && br <> [||] then
+      if List.length common_br = Array.length br then
 	let (_,ids,t) = br.(0) in ast_lift (-List.length ids) t
       else
 	let new_i = (fst i, common_br) in
@@ -1018,8 +1019,10 @@ and kill_dummy_fix i c =
 
 let normalize a =
   let o = optims () in
-  let a = simpl o a in
-  if o.opt_kill_dum then kill_dummy a else a
+  let rec norm a =
+    let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
+    if a = a' then a else norm a'
+  in norm a
 
 (*S Special treatment of fixpoint for pretty-printing purpose. *)
 
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 7fd8006a59..0366c4ba78 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -87,6 +87,7 @@ val tmp_id : ml_ident -> ml_ident
 
 val collect_lams : ml_ast -> ml_ident list * ml_ast
 val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast
+val remove_n_lams : int -> ml_ast -> ml_ast
 val nb_lams : ml_ast -> int
 
 val dummy_lams : ml_ast -> int -> ml_ast
@@ -96,6 +97,7 @@ val eta_args_sign : int -> signature -> ml_ast list
 
 (*s Utility functions over ML terms. *)
 
+val mlapp : ml_ast -> ml_ast list -> ml_ast
 val ast_map : (ml_ast -> ml_ast) -> ml_ast -> ml_ast
 val ast_map_lift : (int -> ml_ast -> ml_ast) -> int -> ml_ast -> ml_ast
 val ast_iter : (ml_ast -> unit) -> ml_ast -> unit