src/Pure/Tools/codegen_serializer.ML

--- a/src/Pure/Tools/codegen_serializer.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -14,13 +14,13 @@
       -> OuterParse.token list ->
       ((string -> string option)
         * (string -> CodegenThingol.itype pretty_syntax option)
-        * (string -> CodegenThingol.iexpr pretty_syntax option)
+        * (string -> CodegenThingol.iterm pretty_syntax option)
       -> string list * string list option
       -> CodegenThingol.module -> unit)
       * OuterParse.token list;
   val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
     ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
-  val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;
+  val pretty_list: string -> string -> int * string -> CodegenThingol.iterm pretty_syntax;
   val serializers: {
     ml: string * (string * string * (string -> bool) -> serializer),
     haskell: string * (string * string list -> serializer)
@@ -28,7 +28,7 @@
   val mk_flat_ml_resolver: string list -> string -> string;
   val ml_fun_datatype: string * string * (string -> bool)
     -> ((string -> CodegenThingol.itype pretty_syntax option)
-        * (string -> CodegenThingol.iexpr pretty_syntax option))
+        * (string -> CodegenThingol.iterm pretty_syntax option))
     -> (string -> string)
     -> ((string * CodegenThingol.funn) list -> Pretty.T)
         * ((string * CodegenThingol.datatyp) list -> Pretty.T);
@@ -198,7 +198,7 @@
     -> OuterParse.token list ->
     ((string -> string option)
       * (string -> itype pretty_syntax option)
-      * (string -> iexpr pretty_syntax option)
+      * (string -> iterm pretty_syntax option)
     -> string list * string list option
     -> CodegenThingol.module -> unit)
     * OuterParse.token list;
@@ -289,6 +289,12 @@
           | _ => SOME)
        | _ => Scan.fail ());
 
+fun parse_stdout serializer =
+  OuterParse.name
+  >> (fn "_" => serializer
+        (fn "" => (fn p => (Pretty.writeln p; NONE))
+          | _ => SOME)
+       | _ => Scan.fail ());
 
 (* list serializer *)
 
@@ -329,9 +335,9 @@
   type src = string;
   val ord = string_ord;
   fun mk reserved_ml (name, 0) =
-        (CodegenTheorems.proper_name o NameSpace.base) name
+        (CodegenThingol.proper_name o NameSpace.base) name
     | mk reserved_ml (name, i) =
-        (CodegenTheorems.proper_name o NameSpace.base) name ^ replicate_string i "'";
+        (CodegenThingol.proper_name o NameSpace.base) name ^ replicate_string i "'";
   fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
   fun maybe_unique _ _ = NONE;
   fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
@@ -458,13 +464,15 @@
                   ml_from_expr NOBR e1,
                   ml_from_expr BR e2
                 ])
-      | ml_from_expr fxy ((v, ty) `|-> e) =
-          brackify BR [
-            str "fn",
-            typify ty (str v),
-            str "=>",
-            ml_from_expr NOBR e
-          ]
+      | ml_from_expr fxy (e as _ `|-> _) =
+          let
+            val (es, be) = CodegenThingol.unfold_abs e;
+            fun mk_abs (e, ty) = (Pretty.block o Pretty.breaks) [
+                str "fn",
+                typify ty (ml_from_expr NOBR e),
+                str "=>"
+              ];
+          in brackify BR (map mk_abs es @ [ml_from_expr NOBR be]) end
       | ml_from_expr fxy (INum (n, _)) =
           brackify BR [
             (str o IntInf.toString) n,
@@ -475,16 +483,9 @@
           (str o prefix "#" o quote)
             (let val i = (Char.ord o the o Char.fromString) c
               in if i < 32 
-                then prefix "\\" c
+                then prefix "\\" (string_of_int i)
                 else c
               end)
-      | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
-          brackify BR [
-            str "fn",
-            typify vty (ml_from_expr NOBR ve),
-            str "=>",
-            ml_from_expr NOBR be
-          ]
       | ml_from_expr fxy (e as ICase ((_, [_]), _)) =
           let
             val (ves, be) = CodegenThingol.unfold_let e;
@@ -519,7 +520,7 @@
             @ [str ")"]
           ) end
       | ml_from_expr _ e =
-          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iexpr) e)
+          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
     and ml_mk_app f es =
       if is_cons f andalso length es > 1 then
         [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
@@ -553,7 +554,6 @@
           let
             fun no_eta (_::_, _) = I
               | no_eta (_, _ `|-> _) = I
-              | no_eta (_, IAbs (_, _)) = I
               | no_eta ([], e) = K false;
             fun has_tyvars (_ `%% tys) =
                   exists has_tyvars tys
@@ -816,6 +816,7 @@
   in
     parse_multi
     || parse_internal serializer
+    || parse_stdout serializer
     || parse_single_file serializer
   end;
 
@@ -910,20 +911,9 @@
           (str o enclose "'" "'")
             (let val i = (Char.ord o the o Char.fromString) c
               in if i < 32 
-                then Library.prefix "\\" c
+                then Library.prefix "\\" (string_of_int i)
                 else c
               end)
-      | hs_from_expr fxy (e as IAbs _) =
-          let
-            val (es, e) = CodegenThingol.unfold_abs e
-          in
-            brackify BR (
-              str "\\"
-              :: map (hs_from_expr BR o fst) es @ [
-              str "->",
-              hs_from_expr NOBR e
-            ])
-          end
       | hs_from_expr fxy (e as ICase ((_, [_]), _)) =
           let
             val (ps, body) = CodegenThingol.unfold_let e;