Extraction: unfolds the let-in created by Program when handling "match"

 This leads to code closer to the original input of the user,
 and moreover some more dummy __ may be removed this way.

 To avoid unfolding by mistake user's variables, we change
 the name of these generated let-in into "program_branch_NN" instead
 of "branch_NN"

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

1 files changed, 18 insertions, 1 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 03b62f836..d8b7d364f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -799,6 +799,23 @@ let is_atomic = function
 
 let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
 
+(** Program creates a let-in named "program_branch_NN" for each branch of match.
+    Unfolding them leads to more natural code (and more dummy removal) *)
+
+let is_program_branch = function
+  | Id id ->
+    let s = string_of_id id in
+    let br = "program_branch_" in
+    let n = String.length br in
+    (try
+       ignore (int_of_string (String.sub s n (String.length s - n)));
+       String.sub s 0 n = br
+     with _ -> false)
+  | Tmp _ | Dummy -> false
+
+let expand_linear_let o id e =
+   o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e
+
 (*S The main simplification function. *)
 
 (* Some beta-iota reductions + simplifications. *)
@@ -815,7 +832,7 @@ let rec simpl o = function
       if
 	(is_atomic c) || (is_atomic e) ||
 	(let n = nb_occur_match e in
-	 (n = 0 || (n=1 && (is_tmp id || is_imm_apply e || o.opt_lin_let))))
+	 (n = 0 || (n=1 && expand_linear_let o id e)))
       then
 	simpl o (ast_subst c e)
       else