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, ((_, (function_typs, body_typ)), annotate)), ts) =
90 val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
91 fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
93 ((if annotate then put_annotation else I)
94 ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
96 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
97 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
98 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
100 val (binds, body) = Code_Thingol.unfold_let (ICase cases);
101 fun print_match ((pat, ty), t) vars =
103 |> print_bind tyvars some_thm BR pat
104 |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
105 val (ps, vars') = fold_map print_match binds vars;
106 in brackify_block fxy (str "let {")
108 (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
110 | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
112 fun print_select (pat, body) =
114 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
115 in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
116 in Pretty.block_enclose
117 (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
118 (map print_select clauses)
120 | print_case tyvars some_thm vars fxy ((_, []), _) =
121 (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
122 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
124 val tyvars = intro_vars (map fst vs) reserved;
127 (str o deresolve) name
128 :: map str (replicate n "_")
131 @@ (str o ML_Syntax.print_string
132 o Long_Name.base_name o Long_Name.qualifier) name
134 fun print_eqn ((ts, t), (some_thm, _)) =
136 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
139 (is_none o const_syntax) deresolve consts
140 |> intro_vars ((fold o Code_Thingol.fold_varnames)
141 (insert (op =)) ts []);
144 (str o deresolve) name
145 :: map (print_term tyvars some_thm vars BR) ts
147 @@ print_term tyvars some_thm vars NOBR t
153 (str o suffix " ::" o deresolve) name,
154 print_typscheme tyvars (vs, ty)
156 :: (case filter (snd o snd) raw_eqs
157 of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
158 | eqs => map print_eqn eqs)
161 | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
163 val tyvars = intro_vars (map fst vs) reserved;
167 print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
170 | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
172 val tyvars = intro_vars (map fst vs) reserved;
176 :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
178 :: (str o deresolve) co
179 :: print_typ tyvars BR ty
180 :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
183 | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
185 val tyvars = intro_vars (map fst vs) reserved;
186 fun print_co ((co, _), tys) =
189 :: map (print_typ tyvars BR) tys
194 :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
197 :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
198 @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
201 | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
203 val tyvars = intro_vars [v] reserved;
204 fun print_classparam (classparam, ty) =
206 (str o deresolve) classparam,
208 print_typ tyvars NOBR ty
211 Pretty.block_enclose (
214 Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
215 str (deresolve name ^ " " ^ lookup_var tyvars v),
219 ) (map print_classparam classparams)
221 | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
223 val tyvars = intro_vars (map fst vs) reserved;
224 fun requires_args classparam = case const_syntax classparam
226 | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
227 | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
228 fun print_classparam_instance ((classparam, const), (thm, _)) =
229 case requires_args classparam
230 of NONE => semicolon [
231 (str o Long_Name.base_name o deresolve) classparam,
233 print_app tyvars (SOME thm) reserved NOBR (const, [])
237 val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
238 val (vs, rhs) = (apfst o map) fst
239 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
240 val s = if (is_some o const_syntax) c
241 then NONE else (SOME o Long_Name.base_name o deresolve) c;
243 |> intro_vars (map_filter I (s :: vs));
244 val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
245 (*dictionaries are not relevant at this late stage*)
248 print_term tyvars (SOME thm) vars NOBR lhs,
250 print_term tyvars (SOME thm) vars NOBR rhs
254 Pretty.block_enclose (
257 Pretty.block (print_typcontext tyvars vs),
258 str (class_name class ^ " "),
259 print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
263 ) (map print_classparam_instance classparam_instances)
267 fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
269 fun namify_fun upper base (nsp_fun, nsp_typ) =
271 val (base', nsp_fun') =
272 Name.variant (if upper then first_upper base else base) nsp_fun;
273 in (base', (nsp_fun', nsp_typ)) end;
274 fun namify_typ base (nsp_fun, nsp_typ) =
276 val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
277 in (base', (nsp_fun, nsp_typ')) end;
278 fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
279 | namify_stmt (Code_Thingol.Fun _) = namify_fun false
280 | namify_stmt (Code_Thingol.Datatype _) = namify_typ
281 | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
282 | namify_stmt (Code_Thingol.Class _) = namify_typ
283 | namify_stmt (Code_Thingol.Classrel _) = pair
284 | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
285 | namify_stmt (Code_Thingol.Classinst _) = pair;
286 fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
287 | select_stmt (Code_Thingol.Fun _) = true
288 | select_stmt (Code_Thingol.Datatype _) = true
289 | select_stmt (Code_Thingol.Datatypecons _) = false
290 | select_stmt (Code_Thingol.Class _) = true
291 | select_stmt (Code_Thingol.Classrel _) = false
292 | select_stmt (Code_Thingol.Classparam _) = false
293 | select_stmt (Code_Thingol.Classinst _) = true;
295 Code_Namespace.flat_program labelled_name
296 { module_alias = module_alias, module_prefix = module_prefix,
297 reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
298 modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
301 fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
302 includes, module_alias, class_syntax, tyco_syntax, const_syntax } program =
306 val reserved = fold (insert (op =) o fst) includes reserved_syms;
307 val { deresolver, flat_program = haskell_program } = haskell_program_of_program
308 labelled_name module_alias module_prefix (Name.make_context reserved) program;
310 (* print statements *)
311 fun deriving_show tyco =
313 fun deriv _ "fun" = false
314 | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
315 andalso (member (op =) tycos tyco
316 orelse case try (Graph.get_node program) tyco
317 of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
320 and deriv' tycos (tyco `%% tys) = deriv tycos tyco
321 andalso forall (deriv' tycos) tys
322 | deriv' _ (ITyVar _) = true
323 in deriv [] tyco end;
324 fun print_stmt deresolve = print_haskell_stmt labelled_name
325 class_syntax tyco_syntax const_syntax (make_vars reserved)
327 (if string_classes then deriving_show else K false);
330 val import_includes_ps =
331 map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes;
332 fun print_module_frame module_name ps =
333 (module_name, Pretty.chunks2 (
334 str ("module " ^ module_name ^ " where {")
338 fun print_module module_name (gr, imports) =
340 val deresolve = deresolver module_name
341 fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
342 val import_ps = import_includes_ps @ map (print_import o fst) imports;
343 fun print_stmt' gr name = case Graph.get_node gr name
345 | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
346 val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr);
348 print_module_frame module_name
349 ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
353 fun write_module width (SOME destination) (module_name, content) =
355 val _ = File.check_dir destination;
356 val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
357 o separate "/" o Long_Name.explode) module_name;
358 val _ = Isabelle_System.mkdirs (Path.dir filepath);
360 (File.write filepath o format [] width o Pretty.chunks2)
361 [str language_pragma, content]
363 | write_module width NONE (_, content) = writeln (format [] width content);
365 Code_Target.serialization
366 (fn width => fn destination => K () o map (write_module width destination))
367 (fn present => fn width => rpair (try (deresolver ""))
368 o format present width o Pretty.chunks o map snd)
369 (map (uncurry print_module_frame o apsnd single) includes
370 @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
371 ((flat o rev o Graph.strong_conn) haskell_program))
374 val serializer : Code_Target.serializer =
375 Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
376 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
377 >> (fn (module_prefix, string_classes) =>
378 serialize_haskell module_prefix string_classes));
383 val s = ML_Syntax.print_char c;
384 in if s = "'" then "\\'" else s end;
385 fun numeral_haskell k = if k >= 0 then string_of_int k
386 else Library.enclose "(" ")" (signed_string_of_int k);
388 literal_char = Library.enclose "'" "'" o char_haskell,
389 literal_string = quote o translate_string char_haskell,
390 literal_numeral = numeral_haskell,
391 literal_positive_numeral = numeral_haskell,
392 literal_alternative_numeral = numeral_haskell,
393 literal_naive_numeral = numeral_haskell,
394 literal_list = enum "," "[" "]",
395 infix_cons = (5, ":")
399 (** optional monad syntax **)
401 fun pretty_haskell_monad c_bind =
403 fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
404 of SOME ((pat, ty), t') =>
405 SOME ((SOME ((pat, ty), true), t1), t')
407 fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
408 if c = c_bind_name then dest_bind t1 t2
410 | dest_monad _ t = case Code_Thingol.split_let t
411 of SOME (((pat, ty), tbind), t') =>
412 SOME ((SOME ((pat, ty), false), tbind), t')
414 fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
415 fun print_monad print_bind print_term (NONE, t) vars =
416 (semicolon [print_term vars NOBR t], vars)
417 | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
418 |> print_bind NOBR bind
419 |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
420 | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
421 |> print_bind NOBR bind
422 |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
423 fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
424 of SOME (bind, t') => let
425 val (binds, t'') = implode_monad c_bind' t'
426 val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
427 (bind :: binds) vars;
429 (brackify fxy o single o enclose "do { " " }" o Pretty.breaks)
430 (ps @| print_term vars' NOBR t'')
432 | NONE => brackify_infix (1, L) fxy
433 (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
434 in (2, ([c_bind], pretty)) end;
436 fun add_monad target' raw_c_bind thy =
438 val c_bind = Code.read_const thy raw_c_bind;
439 in if target = target' then
441 |> Code_Target.add_const_syntax target c_bind
442 (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
443 else error "Only Haskell target allows for monad syntax" end;
449 Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
450 Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
451 Toplevel.theory (add_monad target raw_bind))
455 Code_Target.add_target
456 (target, { serializer = serializer, literals = literals,
457 check = { env_var = "ISABELLE_GHC", make_destination = I,
458 make_command = fn module_name =>
459 "\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^
460 module_name ^ ".hs" } })
461 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
462 brackify_infix (1, R) fxy (
463 print_typ (INFX (1, X)) ty1,
465 print_typ (INFX (1, R)) ty2
467 #> fold (Code_Target.add_reserved target) [
468 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
469 "import", "default", "forall", "let", "in", "class", "qualified", "data",
470 "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
472 #> fold (Code_Target.add_reserved target) [
473 "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
474 "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
475 "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
476 "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
477 "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
478 "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
479 "ExitSuccess", "False", "GT", "HeapOverflow",
480 "IOError", "IOException", "IllegalOperation",
481 "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
482 "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
483 "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
484 "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
485 "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
486 "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
487 "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
488 "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
489 "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
490 "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
491 "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
492 "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
493 "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
494 "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
495 "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
496 "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
497 "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
498 "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
499 "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
500 "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
501 "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
502 "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
503 "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
504 "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
505 "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
506 "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
507 "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
508 "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
509 "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
510 "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
511 "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
512 "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
513 "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
514 "sequence_", "show", "showChar", "showException", "showField", "showList",
515 "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
516 "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
517 "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
518 "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
519 "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
520 "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
521 ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);