cosmetics: after an extract inductive to bool, let's use if then else

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

1 files changed, 23 insertions, 5 deletions

diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 8ba07ab0b..4dd829e5e 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -142,10 +142,15 @@ let rec pp_type par vl t =
     de Bruijn variables. [args] is the list of collected arguments
     (already pretty-printed). *)
 
+let is_ifthenelse = function 
+  | [|(r1,[],_);(r2,[],_)|] -> 
+       (find_custom r1 = "true") && (find_custom r2 = "false") 
+  | _ -> false
+
 let expr_needs_par = function
   | MLlam _  -> true
   | MLcase (_,_,[|_|]) -> false 
-  | MLcase _ -> true
+  | MLcase (_,_,pv) -> not (is_ifthenelse pv)
   | _        -> false 
 
 
@@ -238,11 +243,13 @@ let rec pp_expr par env args =
 			(hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) 
 			 ++ spc () ++ str "in") ++ 
 		      spc () ++ hov 0 s2)))
-	   else
-	     apply
+	   else 
+ 	     apply
       	       (pp_par par' 
-      		  (v 0 (str "match " ++ expr ++ str " with" ++
-			fnl () ++ str "  | " ++ pp_pat env (i,factors) pv))))
+		  (try pp_ifthenelse par' env expr pv 
+		   with Not_found -> 
+		     v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
+			  str "  | " ++ pp_pat env (i,factors) pv))))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -264,6 +271,17 @@ and pp_record_pat (projs, args) =
      (List.combine projs args) ++
    str " }"
 
+and pp_ifthenelse par env expr pv = match pv with 
+  | [|(tru,[],the);(fal,[],els)|] when 
+      (find_custom tru = "true") && (find_custom fal = "false")
+      -> 
+      hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++ 
+            hov 2 (str "then " ++
+		   hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++ 
+	    hov 2 (str "else " ++
+	           hov 2 (pp_expr (expr_needs_par els) env [] els)))
+  | _ -> raise Not_found
+
 and pp_one_pat env i (r,ids,t) = 
   let ids,env' = push_vars (List.rev ids) env in
   let expr = pp_expr (expr_needs_par t) env' [] t in