# 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 *)