From 66d0087acb9457cd6a390ee33e68925a24fbdae7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 4 Mar 2011 16:18:42 +0000 Subject: Extraction: improved indentation of extracted code (fix #2497) For Haskell, we still try to provide readable indentation, but we now avoid relying on this indentation for correctness. Instead, we use layout-independant syntax with { } when necessary (after "case of" and "let"). It is much safer this way, even if the syntax gets a bit more cumbersome. For people allergic to {;}, they can most of the time do a tr -d "{;}" without changing the meaning of the program. Be careful nonetheless: since "case of" is now delimited, some parenthesis that used to be mandatory are now removed. Note also that the initial "module ... where" is still without { }: even when Format goes crazy it doesn't tamper with column 0. Other modifications: - Using "Set Printing Width" now affects uniformly the extraction pretty-printers. You can set a greater value than the default 78 before extracting a program that you know to be "really deep". - In ocaml (and also a bit in Haskell), we now try to avoid abusing of 2-char-right-indentation. For instance | is now aligned with the "m" of match. This way, max_indent will be reached less frequently. - As soon as a pretty-print box contains an explicit newline, we set its virtual size to a big number, in order to prevent this box to be part of some horizontal arrangement. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13870 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/haskell.ml | 57 +++++++++++++++++++++---------------------- 1 file changed, 28 insertions(+), 29 deletions(-) (limited to 'plugins/extraction/haskell.ml') diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 32362d32c..6cad5d294 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -104,7 +104,7 @@ let rec pp_type par vl t = let expr_needs_par = function | MLlam _ -> true - | MLcase _ -> true + | MLcase _ -> false (* now that we use the case ... of { ... } syntax *) | _ -> false @@ -127,14 +127,14 @@ let rec pp_expr par env args = let pp_id = pr_id (List.hd i) and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in - hv 0 - (apply - (pp_par par' - (hv 0 - (hov 5 - (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ - spc () ++ str "in") ++ - spc () ++ hov 0 pp_a2))) + let pp_def = + str "let {" ++ cut () ++ + hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}") + in + apply + (pp_par par' + (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2))) | MLglob r -> apply (pp_global Term r) | MLcons (_,r,[]) -> @@ -159,8 +159,8 @@ let rec pp_expr par env args = ++ pp_expr true env [] t))) | MLcase (info,t, pv) -> apply (pp_par par' - (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ - fnl () ++ str " " ++ pp_pat env info pv))) + (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++ + fnl () ++ pp_pat env info 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 @@ -177,12 +177,11 @@ and pp_pat env info pv = let pp_one_pat (name,ids,t) = let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in let par = expr_needs_par t in - hov 2 (pp_global Cons name ++ + hov 2 (str " " ++ pp_global Cons name ++ (match ids with | [] -> mt () | _ -> (str " " ++ - prlist_with_sep - (fun () -> (spc ())) pr_id (List.rev ids))) ++ + prlist_with_sep spc pr_id (List.rev ids))) ++ str " ->" ++ spc () ++ pp_expr par env' [] t) in let factor_br, factor_set = try match info.m_same with @@ -199,18 +198,18 @@ and pp_pat env info pv = prvecti (fun i x -> if Intset.mem i factor_set then mt () else (pp_one_pat pv.(i) ++ - if i = last && Intset.is_empty factor_set then mt () else - fnl () ++ str " ")) pv + if i = last && Intset.is_empty factor_set then str "}" else + (str ";" ++ fnl ()))) pv ++ if Intset.is_empty factor_set then mt () else let par = expr_needs_par factor_br in match info.m_same with | BranchFun _ -> let ids, env' = push_vars [anonymous_name] env in - hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - pp_expr par env' [] factor_br) + hov 2 (str " " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br ++ str "}") | BranchCst _ -> - hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br) + hov 2 (str " _ ->" ++ spc () ++ pp_expr par env [] factor_br ++ str "}") | BranchNone -> mt () (*s names of the functions ([ids]) are already pushed in [env], @@ -219,12 +218,12 @@ and pp_pat env info pv = and pp_fix par env i (ids,bl) args = pp_par par (v 0 - (v 2 (str "let" ++ fnl () ++ - prvect_with_sep fnl + (v 1 (str "let {" ++ fnl () ++ + prvect_with_sep (fun () -> str ";" ++ fnl ()) (fun (fi,ti) -> pp_function env (pr_id fi) ti) - (array_map2 (fun a b -> a,b) ids bl)) ++ - fnl () ++ - hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) + (array_map2 (fun a b -> a,b) ids bl) ++ + str "}") ++ + fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args)) and pp_function env f t = let bl,t' = collect_lams t in @@ -263,12 +262,12 @@ let pp_one_ind ip pl cv = (fun () -> (str " ")) (pp_type true pl) l)) in str (if Array.length cv = 0 then "type " else "data ") ++ - pp_global Type (IndRef ip) ++ str " " ++ - prlist_with_sep (fun () -> str " ") pr_lower_id pl ++ - (if pl = [] then mt () else str " ") ++ - if Array.length cv = 0 then str "= () -- empty inductive" + pp_global Type (IndRef ip) ++ + prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++ + if Array.length cv = 0 then str " () -- empty inductive" else - (v 0 (str "= " ++ + (fnl () ++ str " " ++ + v 0 (str " " ++ prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv))) -- cgit v1.2.3