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 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 (tyco `%% tys) = (case tyco_syntax tyco
56 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
57 | SOME (_, 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 (tyco, vs) =
60 print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
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 const) =
64 print_app tyvars some_thm vars fxy (const, [])
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 case_expr) =
83 (case Code_Thingol.unfold_const_app (#primitive case_expr)
84 of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
85 then print_case tyvars some_thm vars fxy case_expr
86 else print_app tyvars some_thm vars fxy app
87 | NONE => print_case tyvars some_thm vars fxy case_expr)
88 and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
90 val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
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 { clauses = [], ... } =
102 (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
103 | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
105 val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
106 fun print_match ((pat, _), t) vars =
108 |> print_bind tyvars some_thm BR pat
109 |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
110 val (ps, vars') = fold_map print_match binds vars;
111 in brackify_block fxy (str "let {")
113 (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
115 | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
117 fun print_select (pat, body) =
119 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
120 in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
121 in Pretty.block_enclose
122 (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
123 (map print_select clauses)
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 vs reserved;
170 print_typdecl tyvars (deresolve name, vs)
173 | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
175 val tyvars = intro_vars vs reserved;
179 :: print_typdecl tyvars (deresolve name, 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 vs reserved;
189 fun print_co ((co, _), tys) =
192 :: map (print_typ tyvars BR) tys
197 :: print_typdecl tyvars (deresolve name, 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, inst_params, ... }) =
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 { name = c, dom, range, ... } = 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 { name = classparam, typargs = [],
248 dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
249 (*dictionaries are not relevant at this late stage,
250 and these consts never need type annotations for disambiguation *)
253 print_term tyvars (SOME thm) vars NOBR lhs,
255 print_term tyvars (SOME thm) vars NOBR rhs
259 Pretty.block_enclose (
262 Pretty.block (print_typcontext tyvars vs),
263 str (class_name class ^ " "),
264 print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
268 ) (map print_classparam_instance inst_params)
272 fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
274 fun namify_fun upper base (nsp_fun, nsp_typ) =
276 val (base', nsp_fun') =
277 Name.variant (if upper then first_upper base else base) nsp_fun;
278 in (base', (nsp_fun', nsp_typ)) end;
279 fun namify_typ base (nsp_fun, nsp_typ) =
281 val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
282 in (base', (nsp_fun, nsp_typ')) end;
283 fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
284 | namify_stmt (Code_Thingol.Fun _) = namify_fun false
285 | namify_stmt (Code_Thingol.Datatype _) = namify_typ
286 | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
287 | namify_stmt (Code_Thingol.Class _) = namify_typ
288 | namify_stmt (Code_Thingol.Classrel _) = pair
289 | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
290 | namify_stmt (Code_Thingol.Classinst _) = pair;
291 fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
292 | select_stmt (Code_Thingol.Fun _) = true
293 | select_stmt (Code_Thingol.Datatype _) = true
294 | select_stmt (Code_Thingol.Datatypecons _) = false
295 | select_stmt (Code_Thingol.Class _) = true
296 | select_stmt (Code_Thingol.Classrel _) = false
297 | select_stmt (Code_Thingol.Classparam _) = false
298 | select_stmt (Code_Thingol.Classinst _) = true;
300 Code_Namespace.flat_program labelled_name
301 { module_alias = module_alias, module_prefix = module_prefix,
302 reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
303 modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
306 fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
307 includes, module_alias, class_syntax, tyco_syntax, const_syntax } program =
311 val reserved = fold (insert (op =) o fst) includes reserved_syms;
312 val { deresolver, flat_program = haskell_program } = haskell_program_of_program
313 labelled_name module_alias module_prefix (Name.make_context reserved) program;
315 (* print statements *)
316 fun deriving_show tyco =
318 fun deriv _ "fun" = false
319 | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
320 andalso (member (op =) tycos tyco
321 orelse case try (Graph.get_node program) tyco
322 of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
325 and deriv' tycos (tyco `%% tys) = deriv tycos tyco
326 andalso forall (deriv' tycos) tys
327 | deriv' _ (ITyVar _) = true
328 in deriv [] tyco end;
329 fun print_stmt deresolve = print_haskell_stmt
330 class_syntax tyco_syntax const_syntax (make_vars reserved)
331 deresolve (if string_classes then deriving_show else K false);
334 val import_includes_ps =
335 map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes;
336 fun print_module_frame module_name ps =
337 (module_name, Pretty.chunks2 (
338 str ("module " ^ module_name ^ " where {")
342 fun print_module module_name (gr, imports) =
344 val deresolve = deresolver module_name
345 fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
346 val import_ps = import_includes_ps @ map (print_import o fst) imports;
347 fun print_stmt' gr name = case Graph.get_node gr name
349 | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
350 val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr);
352 print_module_frame module_name
353 ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
357 fun write_module width (SOME destination) (module_name, content) =
359 val _ = File.check_dir destination;
360 val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
361 o separate "/" o Long_Name.explode) module_name;
362 val _ = Isabelle_System.mkdirs (Path.dir filepath);
364 (File.write filepath o format [] width o Pretty.chunks2)
365 [str language_pragma, content]
367 | write_module width NONE (_, content) = writeln (format [] width content);
369 Code_Target.serialization
370 (fn width => fn destination => K () o map (write_module width destination))
371 (fn present => fn width => rpair (try (deresolver ""))
372 o format present width o Pretty.chunks o map snd)
373 (map (uncurry print_module_frame o apsnd single) includes
374 @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
375 ((flat o rev o Graph.strong_conn) haskell_program))
378 val serializer : Code_Target.serializer =
379 Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
380 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
381 >> (fn (module_prefix, string_classes) =>
382 serialize_haskell module_prefix string_classes));
387 val s = ML_Syntax.print_char c;
388 in if s = "'" then "\\'" else s end;
389 fun numeral_haskell k = if k >= 0 then string_of_int k
390 else Library.enclose "(" ")" (signed_string_of_int k);
392 literal_char = Library.enclose "'" "'" o char_haskell,
393 literal_string = quote o translate_string char_haskell,
394 literal_numeral = numeral_haskell,
395 literal_positive_numeral = numeral_haskell,
396 literal_alternative_numeral = numeral_haskell,
397 literal_naive_numeral = numeral_haskell,
398 literal_list = enum "," "[" "]",
399 infix_cons = (5, ":")
403 (** optional monad syntax **)
405 fun pretty_haskell_monad c_bind =
407 fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
408 of SOME ((pat, ty), t') =>
409 SOME ((SOME ((pat, ty), true), t1), t')
411 fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
412 if c = c_bind_name then dest_bind t1 t2
414 | dest_monad _ t = case Code_Thingol.split_let t
415 of SOME (((pat, ty), tbind), t') =>
416 SOME ((SOME ((pat, ty), false), tbind), t')
418 fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
419 fun print_monad print_bind print_term (NONE, t) vars =
420 (semicolon [print_term vars NOBR t], vars)
421 | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
422 |> print_bind NOBR bind
423 |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
424 | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
425 |> print_bind NOBR bind
426 |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
427 fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
428 of SOME (bind, t') => let
429 val (binds, t'') = implode_monad c_bind' t'
430 val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
431 (bind :: binds) vars;
433 (brackify fxy o single o enclose "do { " " }" o Pretty.breaks)
434 (ps @| print_term vars' NOBR t'')
436 | NONE => brackify_infix (1, L) fxy
437 (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
438 in (2, ([c_bind], pretty)) end;
440 fun add_monad target' raw_c_bind thy =
442 val c_bind = Code.read_const thy raw_c_bind;
443 in if target = target' then
445 |> Code_Target.add_const_syntax target c_bind
446 (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
447 else error "Only Haskell target allows for monad syntax" end;
453 Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
454 (Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
455 Toplevel.theory (add_monad target raw_bind)));
458 Code_Target.add_target
459 (target, { serializer = serializer, literals = literals,
460 check = { env_var = "ISABELLE_GHC", make_destination = I,
461 make_command = fn module_name =>
462 "\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^
463 module_name ^ ".hs" } })
464 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
465 brackify_infix (1, R) fxy (
466 print_typ (INFX (1, X)) ty1,
468 print_typ (INFX (1, R)) ty2
470 #> fold (Code_Target.add_reserved target) [
471 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
472 "import", "default", "forall", "let", "in", "class", "qualified", "data",
473 "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
475 #> fold (Code_Target.add_reserved target) [
476 "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
477 "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
478 "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
479 "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
480 "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
481 "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
482 "ExitSuccess", "False", "GT", "HeapOverflow",
483 "IOError", "IOException", "IllegalOperation",
484 "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
485 "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
486 "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
487 "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
488 "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
489 "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
490 "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
491 "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
492 "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
493 "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
494 "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
495 "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
496 "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
497 "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
498 "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
499 "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
500 "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
501 "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
502 "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
503 "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
504 "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
505 "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
506 "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
507 "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
508 "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
509 "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
510 "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
511 "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
512 "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
513 "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
514 "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
515 "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
516 "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
517 "sequence_", "show", "showChar", "showException", "showField", "showList",
518 "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
519 "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
520 "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
521 "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
522 "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
523 "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
524 ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);