# HG changeset patch
# User haftmann
# Date 1133885500 -3600
# Node ID 3126d01e9e359d1f2f166314eab54ddd297139a1
# Parent  a2c9506b62a792aa383cc27679b3ea438858a7e8
improved serialization of classes to haskell

diff -r a2c9506b62a7 -r 3126d01e9e35 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Tue Dec 06 16:07:25 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Tue Dec 06 17:11:40 2005 +0100
@@ -88,6 +88,13 @@
 fun devarify_term t = (fst o Type.freeze_thaw) t;
 fun devarify_type ty = (fst o Type.freeze_thaw_type) ty;
 
+fun newline_correct s =
+  s
+  |> space_explode "\n"
+  |> map (implode o (fn [] => []
+                      | (" "::xs) => xs
+                      | xs => xs) o explode)
+  |> space_implode "\n";
 
 (* code generator instantiation, part 1 *)
 
@@ -1159,7 +1166,7 @@
 
 (* syntax *)
 
-fun gen_add_syntax_tyco prep_tyco prep_mfx prep_primname serial_name ((raw_tyco, raw_mfx), primdef) thy =
+fun gen_add_syntax_tyco prep_tyco prep_mfx prep_primname prep_primdef serial_name ((raw_tyco, raw_mfx), primdef) thy =
   let
     val tyco = prep_tyco thy raw_tyco;
     val _ = if member (op =) prims tyco
@@ -1167,7 +1174,7 @@
       else ()
     fun add_primdef NONE = I
       | add_primdef (SOME (name, (def, deps))) =
-          CodegenSerializer.add_prim (prep_primname thy tyco name, (def, deps))
+          CodegenSerializer.add_prim (prep_primname thy tyco name, (prep_primdef def, deps))
   in
     thy
     |> prep_mfx raw_mfx
@@ -1183,7 +1190,7 @@
           logic_data)))
   end;
 
-val add_syntax_tyco_i = gen_add_syntax_tyco (K I) pair ((K o K) I);
+val add_syntax_tyco_i = gen_add_syntax_tyco (K I) pair ((K o K) I) I;
 val add_syntax_tyco =
   let
     fun mk_name _ _ (SOME name) = name
@@ -1208,10 +1215,10 @@
       end;
   in
     gen_add_syntax_tyco (fn thy => idf_of_tname thy o Sign.intern_type thy)
-      prep_mfx mk_name
+      prep_mfx mk_name (newline_correct o Symbol.strip_blanks)
   end;
 
-fun gen_add_syntax_const prep_const prep_mfx prep_primname serial_name ((raw_f, raw_mfx), primdef) thy =
+fun gen_add_syntax_const prep_const prep_mfx prep_primname prep_primdef serial_name ((raw_f, raw_mfx), primdef) thy =
   let
     val f = prep_const thy raw_f;
     val _ = if member (op =) prims f
@@ -1219,7 +1226,7 @@
       else ()
     fun add_primdef NONE = I
       | add_primdef (SOME (name, (def, deps))) =
-          CodegenSerializer.add_prim (prep_primname thy f name, (def, deps))
+          CodegenSerializer.add_prim (prep_primname thy f name, (prep_primdef def, deps))
   in
     thy
     |> prep_mfx raw_mfx
@@ -1235,7 +1242,7 @@
           logic_data)))
   end;
 
-val add_syntax_const_i = gen_add_syntax_const (K I) pair ((K o K) I);
+val add_syntax_const_i = gen_add_syntax_const (K I) pair ((K o K) I) I;
 val add_syntax_const =
   let
     fun prep_const thy (raw_f, raw_ty) =
@@ -1268,7 +1275,7 @@
         |-> (fn es => pair (Codegen.replace_quotes es proto_mfx))
       end;
   in
-    gen_add_syntax_const prep_const prep_mfx mk_name
+    gen_add_syntax_const prep_const prep_mfx mk_name (newline_correct o Symbol.strip_blanks)
   end;
 
 
diff -r a2c9506b62a7 -r 3126d01e9e35 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Dec 06 16:07:25 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Dec 06 17:11:40 2005 +0100
@@ -644,7 +644,7 @@
     |> eliminate_classes
     |> debug 3 (fn _ => "generating...")
     |> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
-    |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
+    |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
   end;
 
 fun ml_from_thingol' nspgrp name_root =
@@ -664,8 +664,6 @@
 
 local
 
-val bslash = "\\";
-
 fun haskell_from_defs tyco_syntax const_syntax is_cons resolv defs =
   let
     val resolv = fn s =>
@@ -822,7 +820,7 @@
             val (vs, body) = unfold_abs e
           in
             brackify (eval_br br BR) (
-              Pretty.str bslash
+              Pretty.str "\\"
               :: map (Pretty.str o lower_first o fst) vs @ [
               Pretty.str "->",
               haskell_from_expr NOBR body
@@ -958,7 +956,6 @@
       end;
     fun haskell_from_classes defs =
       let
-        val _ = writeln ("IDS: " ^ (commas o map fst) defs)
         fun mk_member (f, ty) =
           Pretty.block [
             Pretty.str (f ^ " ::"),
@@ -1092,7 +1089,7 @@
     |> eta_expand eta_expander
     |> debug 3 (fn _ => "generating...")
     |> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root
-    |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
+    |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
   end;
 
 end; (* local *)
diff -r a2c9506b62a7 -r 3126d01e9e35 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Tue Dec 06 16:07:25 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Dec 06 17:11:40 2005 +0100
@@ -1311,8 +1311,8 @@
       | seri prfx ds =
           s_def (resolver prfx) (map (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds)
   in
-    setmp print_mode [] s_module (name_root, (map (seri [])
-      ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))
+    setmp print_mode [] (fn _ => s_module (name_root, (map (seri [])
+      ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))) ()
   end;
 
 end; (* struct *)