# HG changeset patch
# User haftmann
# Date 1168003911 -3600
# Node ID 93f842eb51a8c8b47ed0c34f9c38307fb88e9e87
# Parent  6466a24dee5b283aa6d647e9f6c25cb4dcf23814
non-layout-sensitive syntax for Haskell

diff -r 6466a24dee5b -r 93f842eb51a8 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Jan 05 14:31:50 2007 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Jan 05 14:31:51 2007 +0100
@@ -30,7 +30,7 @@
   val eval_verbose: bool ref;
   val eval_term: theory -> CodegenThingol.code
     -> (string * 'a option ref) * CodegenThingol.iterm -> 'a;
-  val sml_code_width: int ref;
+  val code_width: int ref;
 end;
 
 structure CodegenSerializer: CODEGEN_SERIALIZER =
@@ -39,14 +39,17 @@
 open BasicCodegenThingol;
 val tracing = CodegenThingol.tracing;
 
-(** syntax **)
-
-(* basics *)
+(** basics **)
 
 infixr 5 @@;
 infixr 5 @|;
 fun x @@ y = [x, y];
 fun xs @| y = xs @ [y];
+val str = setmp print_mode [] Pretty.str;
+val concat = Pretty.block o Pretty.breaks;
+fun semicolon ps = Pretty.block [concat ps, str ";"];
+
+(** syntax **)
 
 datatype lrx = L | R | X;
 
@@ -55,6 +58,8 @@
   | NOBR
   | INFX of (int * lrx);
 
+val APP = INFX (~1, L);
+
 type 'a pretty_syntax = int * (fixity -> (fixity -> 'a -> Pretty.T)
   -> 'a list -> Pretty.T);
 
@@ -69,7 +74,9 @@
       pr < pr_ctxt
       orelse pr = pr_ctxt
         andalso eval_lrx lr lr_ctxt
+      orelse pr_ctxt = ~1
   | eval_fxy _ (INFX _) = false
+  | eval_fxy (INFX _) NOBR = false
   | eval_fxy _ _ = true;
 
 fun gen_brackify _ [p] = p
@@ -93,7 +100,7 @@
             pr fxy from_expr ts
           else if k < length ts
           then case chop k ts of (ts1, ts2) =>
-            brackify fxy (pr NOBR from_expr ts1 :: map (from_expr BR) ts2)
+            brackify fxy (pr APP from_expr ts1 :: map (from_expr BR) ts2)
           else from_expr fxy (CodegenThingol.eta_expand app k)
         end;
 
@@ -103,8 +110,6 @@
 
 (* user-defined syntax *)
 
-val str = setmp print_mode [] Pretty.str;
-
 datatype 'a mixfix =
     Arg of fixity
   | Pretty of Pretty.T;
@@ -244,7 +249,7 @@
 
 
 
-(** SML serializer **)
+(** SML/OCaml serializer **)
 
 datatype ml_def =
     MLFuns of (string * ((iterm list * iterm) list * typscheme)) list
@@ -335,7 +340,7 @@
                   let
                     val vars' = CodegenThingol.intro_vars [v] vars;
                   in
-                    ((Pretty.block o Pretty.breaks) [str "fn", str (CodegenThingol.lookup_var vars' v), str "=>"], vars')
+                    (concat [str "fn", str (CodegenThingol.lookup_var vars' v), str "=>"], vars')
                   end
               | pr ((v, SOME p), _) vars =
                   let
@@ -343,7 +348,7 @@
                     val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
                     val vars'' = CodegenThingol.intro_vars vs vars';
                   in
-                    ((Pretty.block o Pretty.breaks) [str "fn", str (CodegenThingol.lookup_var vars' v), str "as",
+                    (concat [str "fn", str (CodegenThingol.lookup_var vars' v), str "as",
                       pr_term vars'' NOBR p, str "=>"], vars'')
                   end;
             val (ps', vars') = fold_map pr ps vars;
@@ -366,7 +371,7 @@
                 val vars' = CodegenThingol.intro_vars vs vars;
               in
                 (Pretty.block [
-                  (Pretty.block o Pretty.breaks) [
+                  concat [
                     str "val",
                     pr_term vars' NOBR p,
                     str "=",
@@ -389,7 +394,7 @@
                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
                 val vars' = CodegenThingol.intro_vars vs vars;
               in
-                (Pretty.block o Pretty.breaks) [
+                concat [
                   str definer,
                   pr_term vars' NOBR p,
                   str "=>",
@@ -444,7 +449,7 @@
                       |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                            (insert (op =)) ts []);
                   in
-                    (Pretty.block o Pretty.breaks) (
+                    concat (
                       [str definer, (str o deresolv) name]
                       @ (if null ts andalso null vs
                            andalso not (ty = ITyVar "_")(*for evaluation*)
@@ -468,13 +473,13 @@
             fun pr_co (co, []) =
                   str (deresolv co)
               | pr_co (co, tys) =
-                  (Pretty.block o Pretty.breaks) [
+                  concat [
                     str (deresolv co),
                     str "of",
                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
                   ];
             fun pr_data definer (tyco, (vs, cos)) =
-              (Pretty.block o Pretty.breaks) (
+              concat (
                 str definer
                 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
                 :: str "="
@@ -486,16 +491,16 @@
           let
             val w = dictvar v;
             fun pr_superclass class =
-              (Pretty.block o Pretty.breaks o map str) [
+              (concat o map str) [
                 label class, ":", "'" ^ v, deresolv class
               ];
             fun pr_classop (classop, ty) =
-              (Pretty.block o Pretty.breaks) [
+              concat [
                 (*FIXME?*)
                 (str o mk_classop_name) classop, str ":", pr_typ NOBR ty
               ];
             fun pr_classop_fun (classop, _) =
-              (Pretty.block o Pretty.breaks) [
+              concat [
                 str "fun",
                 (str o deresolv) classop,
                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
@@ -505,7 +510,7 @@
               ];
           in
             Pretty.chunks (
-              (Pretty.block o Pretty.breaks) [
+              concat [
                 str ("type '" ^ v),
                 (str o deresolv) class,
                 str "=",
@@ -519,7 +524,7 @@
      | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
           let
             fun pr_superclass (superclass, superinst_iss) =
-              (Pretty.block o Pretty.breaks) [
+              concat [
                 (str o label) superclass,
                 str "=",
                 pr_insts NOBR [Instance superinst_iss]
@@ -533,14 +538,14 @@
                 val vars = keyword_vars
                   |> CodegenThingol.intro_vars consts;
               in
-                (Pretty.block o Pretty.breaks) [
+                concat [
                   (str o mk_classop_name) classop,
                   str "=",
                   pr_term vars NOBR t
                 ]
               end;
           in
-            (Pretty.block o Pretty.breaks) ([
+            concat ([
               str (if null arity then "val" else "fun"),
               (str o deresolv) inst ] @
               map pr_tyvar arity @ [
@@ -686,7 +691,7 @@
                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
                 val vars' = CodegenThingol.intro_vars vs vars;
               in
-                ((Pretty.block o Pretty.breaks) [
+                (concat [
                   str "let",
                   pr_term vars' NOBR p,
                   str "=",
@@ -705,7 +710,7 @@
                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
                 val vars' = CodegenThingol.intro_vars vs vars;
               in
-                (Pretty.block o Pretty.breaks) [
+                concat [
                   str definer,
                   pr_term vars' NOBR p,
                   str "->",
@@ -756,7 +761,7 @@
                   |> CodegenThingol.intro_vars consts
                   |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                       (insert (op =)) ts []);
-              in (Pretty.block o Pretty.breaks) [
+              in concat [
                 (Pretty.block o Pretty.commas) (map (pr_term vars NOBR) ts),
                 str "->",
                 pr_term vars NOBR t
@@ -772,7 +777,7 @@
                       |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                           (insert (op =)) ts []);
                   in
-                    (Pretty.block o Pretty.breaks) (
+                    concat (
                       map (pr_term vars BR) ts
                       @ str "="
                       @@ pr_term vars NOBR t
@@ -813,7 +818,7 @@
                     )
                   end;
             fun pr_funn definer (name, (eqs, (vs, ty))) =
-              (Pretty.block o Pretty.breaks) (
+              concat (
                 str definer
                 :: (str o deresolv) name
                 :: map_filter (fn (_, []) => NONE | v => SOME (pr_tyvar v)) vs
@@ -826,13 +831,13 @@
             fun pr_co (co, []) =
                   str (deresolv co)
               | pr_co (co, tys) =
-                  (Pretty.block o Pretty.breaks) [
+                  concat [
                     str (deresolv co),
                     str "of",
                     Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
                   ];
             fun pr_data definer (tyco, (vs, cos)) =
-              (Pretty.block o Pretty.breaks) (
+              concat (
                 str definer
                 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
                 :: str "="
@@ -844,15 +849,15 @@
           let
             val w = dictvar v;
             fun pr_superclass class =
-              (Pretty.block o Pretty.breaks o map str) [
+              (concat o map str) [
                 deresolv class, ":", "'" ^ v, deresolv class
               ];
             fun pr_classop (classop, ty) =
-              (Pretty.block o Pretty.breaks) [
+              concat [
                 (str o deresolv) classop, str ":", pr_typ NOBR ty
               ];
             fun pr_classop_fun (classop, _) =
-              (Pretty.block o Pretty.breaks) [
+              concat [
                 str "let",
                 (str o deresolv) classop,
                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
@@ -861,7 +866,7 @@
               ];
           in
             Pretty.chunks (
-              (Pretty.block o Pretty.breaks) [
+              concat [
                 str ("type '" ^ v),
                 (str o deresolv) class,
                 str "=",
@@ -875,7 +880,7 @@
      | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
           let
             fun pr_superclass (superclass, superinst_iss) =
-              (Pretty.block o Pretty.breaks) [
+              concat [
                 (str o deresolv) superclass,
                 str "=",
                 pr_insts NOBR [Instance superinst_iss]
@@ -889,14 +894,14 @@
                 val vars = keyword_vars
                   |> CodegenThingol.intro_vars consts;
               in
-                (Pretty.block o Pretty.breaks) [
+                concat [
                   (str o deresolv) classop,
                   str "=",
                   pr_term vars NOBR t
                 ]
               end;
           in
-            (Pretty.block o Pretty.breaks) (
+            concat (
               str "let"
               :: (str o deresolv) inst
               :: map pr_tyvar arity
@@ -920,7 +925,8 @@
     str ("end;; (*struct " ^ name ^ "*)")
   ]);
 
-val sml_code_width = ref 80;
+val code_width = ref 80;
+fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
 
 fun seri_ml pr_def pr_modl output reserved_user module_alias module_prolog
   (_ : string -> (string * (string -> string option)) option) tyco_syntax const_syntax code =
@@ -1084,9 +1090,9 @@
 
 val isar_seri_sml =
   let
-    fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
-    fun output_diag p = Pretty.writeln p;
-    fun output_internal p = use_text Output.ml_output false (Pretty.output p);
+    fun output_file file = File.write (Path.explode file) o code_output;
+    val output_diag = writeln o code_output;
+    val output_internal = use_text Output.ml_output false o code_output;
   in
     parse_args ((Args.$$$ "-" >> K output_diag
       || Args.$$$ "#" >> K output_internal
@@ -1096,8 +1102,8 @@
 
 val isar_seri_ocaml =
   let
-    fun output_file file p = File.write (Path.explode file) (Pretty.output p ^ "\n");
-    fun output_diag p = Pretty.writeln p;
+    fun output_file file = File.write (Path.explode file) o code_output;
+    val output_diag = writeln o code_output;
   in
     parse_args ((Args.$$$ "-" >> K output_diag
       || Args.name >> output_file)
@@ -1113,7 +1119,7 @@
      of NONE => deresolv class
       | SOME (class, _) => class;
     fun classop_name class classop = case class_syntax class
-     of NONE => (snd o dest_name) classop
+     of NONE => deresolv_here classop
       | SOME (_, classop_syntax) => case classop_syntax classop
          of NONE => (snd o dest_name) classop
           | SOME classop => classop
@@ -1166,7 +1172,7 @@
                     val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
                     val vars'' = CodegenThingol.intro_vars vs vars';
                   in
-                    ((Pretty.block o Pretty.breaks) [str (CodegenThingol.lookup_var vars' v),
+                    (concat [str (CodegenThingol.lookup_var vars' v),
                       str "@", pr_term vars'' BR p], vars'')
                   end
               | pr ((v, NONE), _) vars =
@@ -1202,17 +1208,19 @@
                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
                 val vars' = CodegenThingol.intro_vars vs vars;
               in
-                ((Pretty.block o Pretty.breaks) [
+                (semicolon [
                   pr_term vars' BR p,
                   str "=",
                   pr_term vars NOBR t
                 ], vars')
               end;
             val (binds, vars') = fold_map pr ts vars;
-          in Pretty.chunks [
-            [str "(let", Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,
-            [str "in ", pr_term vars' NOBR t, str ")"] |> Pretty.block
-          ] end
+          in
+            Pretty.block_enclose (
+              str "let {",
+              Pretty.block [str "} in ", pr_term vars' NOBR t]
+            ) binds
+          end
       | pr_term vars fxy (ICase ((td, _), bs)) =
           let
             fun pr (p, t) =
@@ -1220,19 +1228,17 @@
                 val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
                 val vars' = CodegenThingol.intro_vars vs vars;
               in
-                (Pretty.block o Pretty.breaks) [
+                semicolon [
                   pr_term vars' NOBR p,
                   str "->",
                   pr_term vars' NOBR t
                 ]
               end
           in
-            (Pretty.enclose "(" ")" o Pretty.breaks) [
-              str "case",
-              pr_term vars NOBR td,
-              str "of",
-              (Pretty.chunks o map pr) bs
-            ]
+            Pretty.block_enclose (
+              concat [str "(case", pr_term vars NOBR td, str "of", str "{"],
+              str "})"
+            ) (map pr bs)
           end
     and pr_app' vars ((c, _), ts) =
       (str o deresolv) c :: map (pr_term vars BR) ts
@@ -1252,10 +1258,11 @@
                   |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                        (insert (op =)) ts []);
               in
-                (Pretty.block o Pretty.breaks) (
+                semicolon (
                   (str o deresolv_here) name
                   :: map (pr_term vars BR) ts
-                  @ [str "=", pr_term vars NOBR t]
+                  @ str "="
+                  @@ pr_term vars NOBR t
                 )
               end;
           in
@@ -1263,7 +1270,8 @@
               Pretty.block [
                 (str o suffix " ::" o deresolv_here) name,
                 Pretty.brk 1,
-                pr_typscheme tyvars (vs, ty)
+                pr_typscheme tyvars (vs, ty),
+                str ";"
               ]
               :: map pr_eq eqs
             )
@@ -1272,62 +1280,57 @@
           let
             val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;
           in
-            (Pretty.block o Pretty.breaks) ([
-              str "newtype",
-              pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs)),
-              str "=",
-              (str o deresolv_here) co,
-              pr_typ tyvars BR ty
-            ] @ (if deriving_show name then [str "deriving (Read, Show)"] else []))
+            semicolon (
+              str "newtype"
+              :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
+              :: str "="
+              :: (str o deresolv_here) co
+              :: pr_typ tyvars BR ty
+              :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
+            )
           end
       | pr_def (name, CodegenThingol.Datatype (vs, co :: cos)) =
           let
             val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;
             fun pr_co (co, tys) =
-              (Pretty.block o Pretty.breaks) (
+              concat (
                 (str o deresolv_here) co
                 :: map (pr_typ tyvars BR) tys
               )
           in
-            (Pretty.block o Pretty.breaks) ((
+            semicolon (
               str "data"
               :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
               :: str "="
               :: pr_co co
               :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
-            ) @ (if deriving_show name then [str "deriving (Read, Show)"] else []))
+              @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
+            )
           end
       | pr_def (name, CodegenThingol.Class (superclasss, (v, classops))) =
           let
             val tyvars = CodegenThingol.intro_vars [v] keyword_vars;
             fun pr_classop (classop, ty) =
-              Pretty.block [
-                str (deresolv_here classop ^ " ::"),
-                Pretty.brk 1,
+              semicolon [
+                (str o classop_name name) classop,
+                str "::",
                 pr_typ tyvars NOBR ty
               ]
           in
-            Pretty.block [
-              str "class ",
-              pr_typparms tyvars [(v, superclasss)],
-              str (deresolv_here name ^ " " ^ CodegenThingol.lookup_var tyvars v),
-              str " where",
-              Pretty.fbrk,
-              Pretty.chunks (map pr_classop classops)
-            ]
+            Pretty.block_enclose (
+              Pretty.block [
+                str "class ",
+                pr_typparms tyvars [(v, superclasss)],
+                str (deresolv_here name ^ " " ^ CodegenThingol.lookup_var tyvars v),
+                str " where {"
+              ],
+              str "};"
+            ) (map pr_classop classops)
           end
       | pr_def (_, CodegenThingol.Classinst ((class, (tyco, vs)), (_, classop_defs))) =
           let
             val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;
-          in
-            Pretty.block [
-              str "instance ",
-              pr_typparms tyvars vs,
-              str (class_name class ^ " "),
-              pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
-              str " where",
-              Pretty.fbrk,
-              Pretty.chunks (map (fn (classop, t) =>
+            fun pr_instdef (classop, t) =
                 let
                   val consts = map_filter
                     (fn c => if (is_some o const_syntax) c
@@ -1336,14 +1339,23 @@
                   val vars = keyword_vars
                     |> CodegenThingol.intro_vars consts;
                 in
-                  (Pretty.block o Pretty.breaks) [
+                  semicolon [
                     (str o classop_name class) classop,
                     str "=",
                     pr_term vars NOBR t
                   ]
-                end
-              ) classop_defs)
-            ]
+                end;
+          in
+            Pretty.block_enclose (
+              Pretty.block [
+                str "instance ",
+                pr_typparms tyvars vs,
+                str (class_name class ^ " "),
+                pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
+                str " where {"
+              ],
+              str "};"
+            ) (map pr_instdef classop_defs)
           end;
   in pr_def def end;
 
@@ -1423,16 +1435,15 @@
       in deriv [] tyco end;
     fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax init_vars
       deresolv_here (if qualified then deresolv else deresolv_here) (if string_classes then deriving_show else K false);
-    fun write_module (SOME destination) modlname p =
+    fun write_module (SOME destination) modlname =
           let
             val filename = case modlname
              of "" => Path.explode "Main.hs"
               | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;
             val pathname = Path.append destination filename;
             val _ = File.mkdir (Path.dir pathname);
-          in File.write pathname (Pretty.setmp_margin 999999 Pretty.output p ^ "\n") end
-      | write_module NONE _ p =
-          writeln (Pretty.setmp_margin 999999 Pretty.output p ^ "\n");
+          in File.write pathname end
+      | write_module NONE _ = writeln;
     fun seri_module (modlname', (imports, (defs, _))) =
       let
         val imports' =
@@ -1447,19 +1458,24 @@
           |> has_duplicates (op =);
         val mk_import = str o (if qualified
           then prefix "import qualified "
-          else prefix "import ");
+          else prefix "import ") o suffix ";";
       in
         Pretty.chunks (
-          str ("module " ^ modlname' ^ " where")
+          str ("module " ^ modlname' ^ " where {")
+          :: str ""
           :: map mk_import imports'
-          @ (
-          (case module_prolog modlname'
-           of SOME prolog => [str "", prolog, str ""]
-            | NONE => [str ""])
-          @ separate (str "") (map_filter
+          @ str ""
+          :: separate (str "") ((case module_prolog modlname'
+             of SOME prolog => [prolog]
+              | NONE => [])
+          @ map_filter
             (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
-              | (_, (_, NONE)) => NONE) defs))
-        ) |> write_module destination modlname'
+              | (_, (_, NONE)) => NONE) defs)
+          @ str ""
+          @@ str "}"
+        )
+        |> code_output
+        |> write_module destination modlname'
       end;
   in Symtab.fold (fn modl => fn () => seri_module modl) code' () end;
 
@@ -1480,9 +1496,9 @@
   in
     []
     |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
-    |> separate (Pretty.str "")
-    |> Pretty.chunks
-    |> Pretty.writeln
+    |> Pretty.chunks2
+    |> code_output
+    |> writeln
   end;