diff options
-rw-r--r-- | CHANGES | 4 | ||||
-rw-r--r-- | plugins/extraction/common.ml | 7 | ||||
-rw-r--r-- | plugins/extraction/common.mli | 6 | ||||
-rw-r--r-- | plugins/extraction/extract_env.ml | 21 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 57 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 20 |
6 files changed, 69 insertions, 46 deletions
@@ -73,6 +73,10 @@ Internal infrastructure - Support of cross-compilation via mingw toward Windows, contact P. Letouzey for more informations. +Extraction + +- The pretty-printer for Haskell now produces layout-independant code + Changes from V8.2 to V8.3 ========================= diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 61e2f8c28..ad2f40063 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -41,6 +41,13 @@ let pr_binding = function | [] -> mt () | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l +(** By default, in module Format, you can do horizontal placing of blocks + even if they include newlines, as long as the number of chars in the + blocks are less that a line length. To avoid this awkward situation, + we attach a big virtual size to [fnl] newlines. *) + +let fnl () = stras (1000000,"") ++ fnl () + let fnl2 () = fnl () ++ fnl () let space_if = function true -> str " " | false -> mt () diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 0abb47c22..7fc3279af 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -12,6 +12,12 @@ open Miniml open Mlutil open Pp +(** By default, in module Format, you can do horizontal placing of blocks + even if they include newlines, as long as the number of chars in the + blocks are less that a line length. To avoid this awkward situation, + we attach a big virtual size to [fnl] newlines. *) + +val fnl : unit -> std_ppcmds val fnl2 : unit -> std_ppcmds val space_if : bool -> std_ppcmds diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 1218dd80c..8a812664f 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -395,13 +395,20 @@ let print_one_decl struc mp decl = (*s Extraction of a ml struct to a file. *) let formatter dry file = - if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) - else match file with - | None -> !Pp_control.std_ft - | Some cout -> - let ft = Pp_control.with_output_to cout in - Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ()); - ft + let ft = + if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) + else Pp_control.with_output_to (Option.default stdout file) + in + (* We never want to see ellipsis ... in extracted code *) + Format.pp_set_max_boxes ft max_int; + (* We reuse the width information given via "Set Printing Width" *) + (match Pp_control.get_margin () with + | None -> () + | Some i -> + Format.pp_set_margin ft i; + Format.pp_set_max_indent ft (i-10)); + (* note: max_indent should be < margin above, otherwise it's ignored *) + ft let print_structure_to_file (fn,si,mo) dry struc = let d = descr () in 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))) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index e4a145586..543cec6e5 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -292,7 +292,7 @@ let rec pp_expr par env args = (try pp_ifthenelse par' env expr pv with Not_found -> v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ - str " | " ++ pp_pat env info pv)))) + 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 @@ -356,19 +356,19 @@ and pp_pat env info pv = prvecti (fun i x -> if Intset.mem i factor_set then mt () else let s1,s2 = pp_one_pat env info x in - hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ - if i = last && Intset.is_empty factor_set then mt () else - fnl () ++ str " | ") pv + hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++ + if i = last && Intset.is_empty factor_set then mt () else 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) + hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + hov 2 (pp_expr par env' [] factor_br)) | BranchCst _ -> - hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br) + hv 2 (str "| _ ->" ++ spc () ++ hov 2 (pp_expr par env [] factor_br)) | BranchNone -> mt () and pp_function env t = @@ -380,11 +380,11 @@ and pp_function env t = if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' i pv) + v 0 (pp_pat env' i pv) else pr_binding (List.rev bl) ++ str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' i pv) + v 0 (pp_pat env' i pv) | _ -> pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ @@ -440,7 +440,7 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps = let pl = rename_tvars keywords pl in let pp_constructor i typs = (if i=0 then mt () else fnl ()) ++ - hov 5 (str " | " ++ cnames.(i) ++ + hov 3 (str "| " ++ cnames.(i) ++ (if typs = [] then mt () else str " of ") ++ prlist_with_sep (fun () -> spc () ++ str "* ") (pp_type true pl) typs) |