1 (* Title: Tools/Code/code_haskell.ML
2 Author: Florian Haftmann, TU Muenchen
4 Serializer for Haskell.
7 signature CODE_HASKELL =
9 val language_params: string
11 val setup: theory -> theory
14 structure Code_Haskell : CODE_HASKELL =
17 val target = "Haskell";
19 val language_extensions =
20 ["EmptyDataDecls", "RankNTypes", "ScopedTypeVariables"];
23 "{-# LANGUAGE " ^ commas language_extensions ^ " #-}";
26 space_implode " " (map (prefix "-X") language_extensions);
28 open Basic_Code_Thingol;
35 (** Haskell serializer **)
37 fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
38 reserved deresolve deriving_show =
40 fun class_name class = case class_syntax class
41 of NONE => deresolve class
42 | SOME class => class;
43 fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
45 | constraints => enum "," "(" ")" (
47 str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
49 fun print_typforall tyvars vs = case map fst vs
51 | vnames => str "forall " :: Pretty.breaks
52 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
53 fun print_tyco_expr tyvars fxy (tyco, tys) =
54 brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
55 and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
56 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
57 | SOME (i, print) => print (print_typ tyvars) fxy tys)
58 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
59 fun print_typdecl tyvars (vs, tycoexpr) =
60 Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
61 fun print_typscheme tyvars (vs, ty) =
62 Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
63 fun print_term tyvars some_thm vars fxy (IConst c) =
64 print_app tyvars some_thm vars fxy (c, [])
65 | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
66 (case Code_Thingol.unfold_const_app t
67 of SOME app => print_app tyvars some_thm vars fxy app
70 print_term tyvars some_thm vars NOBR t1,
71 print_term tyvars some_thm vars BR t2
73 | print_term tyvars some_thm vars fxy (IVar NONE) =
75 | print_term tyvars some_thm vars fxy (IVar (SOME v)) =
76 (str o lookup_var vars) v
77 | print_term tyvars some_thm vars fxy (t as _ `|=> _) =
79 val (binds, t') = Code_Thingol.unfold_pat_abs t;
80 val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
81 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
82 | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
83 (case Code_Thingol.unfold_const_app t0
84 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
85 then print_case tyvars some_thm vars fxy cases
86 else print_app tyvars some_thm vars fxy c_ts
87 | NONE => print_case tyvars some_thm vars fxy cases)
88 and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
90 val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
93 brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
97 printed_const :: map (print_term tyvars some_thm vars BR) ts
99 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
100 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
101 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
103 val (binds, body) = Code_Thingol.unfold_let (ICase cases);
104 fun print_match ((pat, ty), t) vars =
106 |> print_bind tyvars some_thm BR pat
107 |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
108 val (ps, vars') = fold_map print_match binds vars;
109 in brackify_block fxy (str "let {")
111 (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
113 | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
115 fun print_select (pat, body) =
117 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
118 in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
119 in Pretty.block_enclose
120 (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
121 (map print_select clauses)
123 | print_case tyvars some_thm vars fxy ((_, []), _) =
124 (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
125 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
127 val tyvars = intro_vars (map fst vs) reserved;
130 (str o deresolve) name
131 :: map str (replicate n "_")
134 @@ (str o ML_Syntax.print_string
135 o Long_Name.base_name o Long_Name.qualifier) name
137 fun print_eqn ((ts, t), (some_thm, _)) =
139 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
142 (is_none o const_syntax) deresolve consts
143 |> intro_vars ((fold o Code_Thingol.fold_varnames)
144 (insert (op =)) ts []);
147 (str o deresolve) name
148 :: map (print_term tyvars some_thm vars BR) ts
150 @@ print_term tyvars some_thm vars NOBR t
156 (str o suffix " ::" o deresolve) name,
157 print_typscheme tyvars (vs, ty)
159 :: (case filter (snd o snd) raw_eqs
160 of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
161 | eqs => map print_eqn eqs)
164 | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
166 val tyvars = intro_vars (map fst vs) reserved;
170 print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
173 | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
175 val tyvars = intro_vars (map fst vs) reserved;
179 :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
181 :: (str o deresolve) co
182 :: print_typ tyvars BR ty
183 :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
186 | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
188 val tyvars = intro_vars (map fst vs) reserved;
189 fun print_co ((co, _), tys) =
192 :: map (print_typ tyvars BR) tys
197 :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
200 :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
201 @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
204 | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
206 val tyvars = intro_vars [v] reserved;
207 fun print_classparam (classparam, ty) =
209 (str o deresolve) classparam,
211 print_typ tyvars NOBR ty
214 Pretty.block_enclose (
217 Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
218 str (deresolve name ^ " " ^ lookup_var tyvars v),
222 ) (map print_classparam classparams)
224 | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
226 val tyvars = intro_vars (map fst vs) reserved;
227 fun requires_args classparam = case const_syntax classparam
229 | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
230 | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
231 fun print_classparam_instance ((classparam, const), (thm, _)) =
232 case requires_args classparam
233 of NONE => semicolon [
234 (str o Long_Name.base_name o deresolve) classparam,
236 print_app tyvars (SOME thm) reserved NOBR (const, [])
240 val (c, ((_, tys), _)) = const;
241 val (vs, rhs) = (apfst o map) fst
242 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
243 val s = if (is_some o const_syntax) c
244 then NONE else (SOME o Long_Name.base_name o deresolve) c;
246 |> intro_vars (map_filter I (s :: vs));
247 val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
248 (*dictionaries are not relevant at this late stage,
249 and these consts never need type annotations for disambiguation *)
252 print_term tyvars (SOME thm) vars NOBR lhs,
254 print_term tyvars (SOME thm) vars NOBR rhs
258 Pretty.block_enclose (
261 Pretty.block (print_typcontext tyvars vs),
262 str (class_name class ^ " "),
263 print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
267 ) (map print_classparam_instance classparam_instances)
271 fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
273 fun namify_fun upper base (nsp_fun, nsp_typ) =
275 val (base', nsp_fun') =
276 Name.variant (if upper then first_upper base else base) nsp_fun;
277 in (base', (nsp_fun', nsp_typ)) end;
278 fun namify_typ base (nsp_fun, nsp_typ) =
280 val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
281 in (base', (nsp_fun, nsp_typ')) end;
282 fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
283 | namify_stmt (Code_Thingol.Fun _) = namify_fun false
284 | namify_stmt (Code_Thingol.Datatype _) = namify_typ
285 | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
286 | namify_stmt (Code_Thingol.Class _) = namify_typ
287 | namify_stmt (Code_Thingol.Classrel _) = pair
288 | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
289 | namify_stmt (Code_Thingol.Classinst _) = pair;
290 fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
291 | select_stmt (Code_Thingol.Fun _) = true
292 | select_stmt (Code_Thingol.Datatype _) = true
293 | select_stmt (Code_Thingol.Datatypecons _) = false
294 | select_stmt (Code_Thingol.Class _) = true
295 | select_stmt (Code_Thingol.Classrel _) = false
296 | select_stmt (Code_Thingol.Classparam _) = false
297 | select_stmt (Code_Thingol.Classinst _) = true;
299 Code_Namespace.flat_program labelled_name
300 { module_alias = module_alias, module_prefix = module_prefix,
301 reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
302 modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
305 fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
306 includes, module_alias, class_syntax, tyco_syntax, const_syntax } program =
310 val reserved = fold (insert (op =) o fst) includes reserved_syms;
311 val { deresolver, flat_program = haskell_program } = haskell_program_of_program
312 labelled_name module_alias module_prefix (Name.make_context reserved) program;
314 (* print statements *)
315 fun deriving_show tyco =
317 fun deriv _ "fun" = false
318 | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
319 andalso (member (op =) tycos tyco
320 orelse case try (Graph.get_node program) tyco
321 of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
324 and deriv' tycos (tyco `%% tys) = deriv tycos tyco
325 andalso forall (deriv' tycos) tys
326 | deriv' _ (ITyVar _) = true
327 in deriv [] tyco end;
328 fun print_stmt deresolve = print_haskell_stmt labelled_name
329 class_syntax tyco_syntax const_syntax (make_vars reserved)
330 deresolve (if string_classes then deriving_show else K false);
333 val import_includes_ps =
334 map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes;
335 fun print_module_frame module_name ps =
336 (module_name, Pretty.chunks2 (
337 str ("module " ^ module_name ^ " where {")
341 fun print_module module_name (gr, imports) =
343 val deresolve = deresolver module_name
344 fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
345 val import_ps = import_includes_ps @ map (print_import o fst) imports;
346 fun print_stmt' gr name = case Graph.get_node gr name
348 | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
349 val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr);
351 print_module_frame module_name
352 ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
356 fun write_module width (SOME destination) (module_name, content) =
358 val _ = File.check_dir destination;
359 val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
360 o separate "/" o Long_Name.explode) module_name;
361 val _ = Isabelle_System.mkdirs (Path.dir filepath);
363 (File.write filepath o format [] width o Pretty.chunks2)
364 [str language_pragma, content]
366 | write_module width NONE (_, content) = writeln (format [] width content);
368 Code_Target.serialization
369 (fn width => fn destination => K () o map (write_module width destination))
370 (fn present => fn width => rpair (try (deresolver ""))
371 o format present width o Pretty.chunks o map snd)
372 (map (uncurry print_module_frame o apsnd single) includes
373 @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
374 ((flat o rev o Graph.strong_conn) haskell_program))
377 val serializer : Code_Target.serializer =
378 Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
379 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
380 >> (fn (module_prefix, string_classes) =>
381 serialize_haskell module_prefix string_classes));
386 val s = ML_Syntax.print_char c;
387 in if s = "'" then "\\'" else s end;
388 fun numeral_haskell k = if k >= 0 then string_of_int k
389 else Library.enclose "(" ")" (signed_string_of_int k);
391 literal_char = Library.enclose "'" "'" o char_haskell,
392 literal_string = quote o translate_string char_haskell,
393 literal_numeral = numeral_haskell,
394 literal_positive_numeral = numeral_haskell,
395 literal_alternative_numeral = numeral_haskell,
396 literal_naive_numeral = numeral_haskell,
397 literal_list = enum "," "[" "]",
398 infix_cons = (5, ":")
402 (** optional monad syntax **)
404 fun pretty_haskell_monad c_bind =
406 fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
407 of SOME ((pat, ty), t') =>
408 SOME ((SOME ((pat, ty), true), t1), t')
410 fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
411 if c = c_bind_name then dest_bind t1 t2
413 | dest_monad _ t = case Code_Thingol.split_let t
414 of SOME (((pat, ty), tbind), t') =>
415 SOME ((SOME ((pat, ty), false), tbind), t')
417 fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
418 fun print_monad print_bind print_term (NONE, t) vars =
419 (semicolon [print_term vars NOBR t], vars)
420 | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
421 |> print_bind NOBR bind
422 |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
423 | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
424 |> print_bind NOBR bind
425 |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
426 fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
427 of SOME (bind, t') => let
428 val (binds, t'') = implode_monad c_bind' t'
429 val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
430 (bind :: binds) vars;
432 (brackify fxy o single o enclose "do { " " }" o Pretty.breaks)
433 (ps @| print_term vars' NOBR t'')
435 | NONE => brackify_infix (1, L) fxy
436 (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
437 in (2, ([c_bind], pretty)) end;
439 fun add_monad target' raw_c_bind thy =
441 val c_bind = Code.read_const thy raw_c_bind;
442 in if target = target' then
444 |> Code_Target.add_const_syntax target c_bind
445 (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
446 else error "Only Haskell target allows for monad syntax" end;
452 Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
453 (Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
454 Toplevel.theory (add_monad target raw_bind)));
457 Code_Target.add_target
458 (target, { serializer = serializer, literals = literals,
459 check = { env_var = "ISABELLE_GHC", make_destination = I,
460 make_command = fn module_name =>
461 "\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^
462 module_name ^ ".hs" } })
463 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
464 brackify_infix (1, R) fxy (
465 print_typ (INFX (1, X)) ty1,
467 print_typ (INFX (1, R)) ty2
469 #> fold (Code_Target.add_reserved target) [
470 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
471 "import", "default", "forall", "let", "in", "class", "qualified", "data",
472 "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
474 #> fold (Code_Target.add_reserved target) [
475 "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
476 "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
477 "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
478 "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
479 "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
480 "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
481 "ExitSuccess", "False", "GT", "HeapOverflow",
482 "IOError", "IOException", "IllegalOperation",
483 "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
484 "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
485 "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
486 "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
487 "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
488 "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
489 "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
490 "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
491 "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
492 "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
493 "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
494 "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
495 "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
496 "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
497 "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
498 "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
499 "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
500 "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
501 "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
502 "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
503 "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
504 "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
505 "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
506 "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
507 "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
508 "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
509 "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
510 "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
511 "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
512 "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
513 "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
514 "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
515 "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
516 "sequence_", "show", "showChar", "showException", "showField", "showList",
517 "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
518 "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
519 "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
520 "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
521 "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
522 "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
523 ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);