32 infixr 5 @@; |
32 infixr 5 @@; |
33 infixr 5 @|; |
33 infixr 5 @|; |
34 |
34 |
35 |
35 |
36 (** Haskell serializer **) |
36 (** Haskell serializer **) |
|
37 |
|
38 val print_haskell_string = |
|
39 let |
|
40 fun char c = |
|
41 let |
|
42 val _ = if Symbol.is_ascii c then () |
|
43 else error "non-ASCII byte in Haskell string literal"; |
|
44 val s = ML_Syntax.print_char c; |
|
45 in if s = "'" then "\\'" else s end; |
|
46 in quote o translate_string char end; |
37 |
47 |
38 fun print_haskell_stmt class_syntax tyco_syntax const_syntax |
48 fun print_haskell_stmt class_syntax tyco_syntax const_syntax |
39 reserved deresolve deriving_show = |
49 reserved deresolve deriving_show = |
40 let |
50 let |
41 val deresolve_const = deresolve o Constant; |
51 val deresolve_const = deresolve o Constant; |
132 (semicolon o map str) ( |
142 (semicolon o map str) ( |
133 deresolve_const const |
143 deresolve_const const |
134 :: replicate n "_" |
144 :: replicate n "_" |
135 @ "=" |
145 @ "=" |
136 :: "error" |
146 :: "error" |
137 @@ ML_Syntax.print_string const |
147 @@ print_haskell_string const |
138 ); |
148 ); |
139 fun print_eqn ((ts, t), (some_thm, _)) = |
149 fun print_eqn ((ts, t), (some_thm, _)) = |
140 let |
150 let |
141 val vars = reserved |
151 val vars = reserved |
142 |> intro_base_names_for (is_none o const_syntax) |
152 |> intro_base_names_for (is_none o const_syntax) |
424 >> (fn (module_prefix, string_classes) => |
434 >> (fn (module_prefix, string_classes) => |
425 serialize_haskell module_prefix string_classes)); |
435 serialize_haskell module_prefix string_classes)); |
426 |
436 |
427 fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int; |
437 fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int; |
428 |
438 |
429 val literals = let |
439 val literals = Literals { |
430 fun char_haskell c = |
440 literal_string = print_haskell_string, |
431 let |
|
432 val s = ML_Syntax.print_char c; |
|
433 in if s = "'" then "\\'" else s end; |
|
434 in Literals { |
|
435 literal_char = Library.enclose "'" "'" o char_haskell, |
|
436 literal_string = quote o translate_string char_haskell, |
|
437 literal_numeral = print_numeral "Integer", |
441 literal_numeral = print_numeral "Integer", |
438 literal_list = enum "," "[" "]", |
442 literal_list = enum "," "[" "]", |
439 infix_cons = (5, ":") |
443 infix_cons = (5, ":") |
440 } end; |
444 }; |
441 |
445 |
442 |
446 |
443 (** optional monad syntax **) |
447 (** optional monad syntax **) |
444 |
448 |
445 fun pretty_haskell_monad c_bind = |
449 fun pretty_haskell_monad c_bind = |