diff options
author | 2008-01-20 00:31:17 +0000 | |
---|---|---|
committer | 2008-01-20 00:31:17 +0000 | |
commit | c07bea7dd60b77d963e8382dabfe886210b6f176 (patch) | |
tree | 15da49c140c8315e2e995305ccdf7dc7700fe360 /contrib/extraction/ocaml.ml | |
parent | c2e3d63ca60b27abb5398ecbc8ebcaf8fb925206 (diff) |
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
Diffstat (limited to 'contrib/extraction/ocaml.ml')
-rw-r--r-- | contrib/extraction/ocaml.ml | 28 |
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 |