1 (* Title: Tools/Code/code_haskell.ML
2 Author: Florian Haftmann, TU Muenchen
4 Serializer for Haskell.
7 signature CODE_HASKELL =
10 val setup: theory -> theory
13 structure Code_Haskell : CODE_HASKELL =
16 val target = "Haskell";
18 open Basic_Code_Thingol;
25 (** Haskell serializer **)
27 fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
28 reserved deresolve contr_classparam_typs deriving_show =
30 fun class_name class = case class_syntax class
31 of NONE => deresolve class
32 | SOME class => class;
33 fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
35 | constraints => enum "," "(" ")" (
37 str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
39 fun print_typforall tyvars vs = case map fst vs
41 | vnames => str "forall " :: Pretty.breaks
42 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
43 fun print_tyco_expr tyvars fxy (tyco, tys) =
44 brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
45 and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
46 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
47 | SOME (i, print) => print (print_typ tyvars) fxy tys)
48 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
49 fun print_typdecl tyvars (vs, tycoexpr) =
50 Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
51 fun print_typscheme tyvars (vs, ty) =
52 Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
53 fun print_term tyvars some_thm vars fxy (IConst c) =
54 print_app tyvars some_thm vars fxy (c, [])
55 | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
56 (case Code_Thingol.unfold_const_app t
57 of SOME app => print_app tyvars some_thm vars fxy app
60 print_term tyvars some_thm vars NOBR t1,
61 print_term tyvars some_thm vars BR t2
63 | print_term tyvars some_thm vars fxy (IVar NONE) =
65 | print_term tyvars some_thm vars fxy (IVar (SOME v)) =
66 (str o lookup_var vars) v
67 | print_term tyvars some_thm vars fxy (t as _ `|=> _) =
69 val (binds, t') = Code_Thingol.unfold_pat_abs t;
70 val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
71 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
72 | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
73 (case Code_Thingol.unfold_const_app t0
74 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
75 then print_case tyvars some_thm vars fxy cases
76 else print_app tyvars some_thm vars fxy c_ts
77 | NONE => print_case tyvars some_thm vars fxy cases)
78 and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) =
80 val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
81 fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
83 ((if annotate then put_annotation else I)
84 ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
86 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
87 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
88 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
90 val (binds, body) = Code_Thingol.unfold_let (ICase cases);
91 fun print_match ((pat, ty), t) vars =
93 |> print_bind tyvars some_thm BR pat
94 |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
95 val (ps, vars') = fold_map print_match binds vars;
96 in brackify_block fxy (str "let {")
98 (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
100 | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
102 fun print_select (pat, body) =
104 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
105 in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
106 in Pretty.block_enclose
107 (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
108 (map print_select clauses)
110 | print_case tyvars some_thm vars fxy ((_, []), _) =
111 (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
112 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
114 val tyvars = intro_vars (map fst vs) reserved;
117 (str o deresolve) name
118 :: map str (replicate n "_")
121 @@ (str o ML_Syntax.print_string
122 o Long_Name.base_name o Long_Name.qualifier) name
124 fun print_eqn ((ts, t), (some_thm, _)) =
126 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
129 (is_none o const_syntax) deresolve consts
130 |> intro_vars ((fold o Code_Thingol.fold_varnames)
131 (insert (op =)) ts []);
134 (str o deresolve) name
135 :: map (print_term tyvars some_thm vars BR) ts
137 @@ print_term tyvars some_thm vars NOBR t
143 (str o suffix " ::" o deresolve) name,
144 print_typscheme tyvars (vs, ty)
146 :: (case filter (snd o snd) raw_eqs
147 of [] => [print_err ((length o fst o Code_Thingol.unfold_fun) ty)]
148 | eqs => map print_eqn eqs)
151 | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
153 val tyvars = intro_vars (map fst vs) reserved;
157 print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
160 | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
162 val tyvars = intro_vars (map fst vs) reserved;
166 :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
168 :: (str o deresolve) co
169 :: print_typ tyvars BR ty
170 :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
173 | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
175 val tyvars = intro_vars (map fst vs) reserved;
176 fun print_co ((co, _), tys) =
179 :: map (print_typ tyvars BR) tys
184 :: print_typdecl tyvars (vs, (deresolve name, map (ITyVar o fst) vs))
187 :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
188 @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
191 | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
193 val tyvars = intro_vars [v] reserved;
194 fun print_classparam (classparam, ty) =
196 (str o deresolve) classparam,
198 print_typ tyvars NOBR ty
201 Pretty.block_enclose (
204 Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
205 str (deresolve name ^ " " ^ lookup_var tyvars v),
209 ) (map print_classparam classparams)
211 | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
213 val tyvars = intro_vars (map fst vs) reserved;
214 fun requires_args classparam = case const_syntax classparam
216 | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
217 | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
218 fun print_classparam_instance ((classparam, const), (thm, _)) =
219 case requires_args classparam
220 of NONE => semicolon [
221 (str o Long_Name.base_name o deresolve) classparam,
223 print_app tyvars (SOME thm) reserved NOBR (const, [])
227 val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
228 val (vs, rhs) = (apfst o map) fst
229 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
230 val s = if (is_some o const_syntax) c
231 then NONE else (SOME o Long_Name.base_name o deresolve) c;
233 |> intro_vars (map_filter I (s :: vs));
234 val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
235 (*dictionaries are not relevant at this late stage*)
238 print_term tyvars (SOME thm) vars NOBR lhs,
240 print_term tyvars (SOME thm) vars NOBR rhs
244 Pretty.block_enclose (
247 Pretty.block (print_typcontext tyvars vs),
248 str (class_name class ^ " "),
249 print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
253 ) (map print_classparam_instance classparam_instances)
257 fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
259 fun namify_fun upper base (nsp_fun, nsp_typ) =
261 val (base', nsp_fun') =
262 Name.variant (if upper then first_upper base else base) nsp_fun;
263 in (base', (nsp_fun', nsp_typ)) end;
264 fun namify_typ base (nsp_fun, nsp_typ) =
266 val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
267 in (base', (nsp_fun, nsp_typ')) end;
268 fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
269 | namify_stmt (Code_Thingol.Fun _) = namify_fun false
270 | namify_stmt (Code_Thingol.Datatype _) = namify_typ
271 | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
272 | namify_stmt (Code_Thingol.Class _) = namify_typ
273 | namify_stmt (Code_Thingol.Classrel _) = pair
274 | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
275 | namify_stmt (Code_Thingol.Classinst _) = pair;
276 fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
277 | select_stmt (Code_Thingol.Fun _) = true
278 | select_stmt (Code_Thingol.Datatype _) = true
279 | select_stmt (Code_Thingol.Datatypecons _) = false
280 | select_stmt (Code_Thingol.Class _) = true
281 | select_stmt (Code_Thingol.Classrel _) = false
282 | select_stmt (Code_Thingol.Classparam _) = false
283 | select_stmt (Code_Thingol.Classinst _) = true;
285 Code_Namespace.flat_program labelled_name
286 { module_alias = module_alias, module_prefix = module_prefix,
287 reserved = reserved, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
288 modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
291 fun serialize_haskell module_prefix string_classes { labelled_name, reserved_syms,
292 includes, module_alias, class_syntax, tyco_syntax, const_syntax } program =
296 val reserved = fold (insert (op =) o fst) includes reserved_syms;
297 val { deresolver, flat_program = haskell_program } = haskell_program_of_program
298 labelled_name module_alias module_prefix (Name.make_context reserved) program;
300 (* print statements *)
301 val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
302 fun deriving_show tyco =
304 fun deriv _ "fun" = false
305 | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
306 andalso (member (op =) tycos tyco
307 orelse case try (Graph.get_node program) tyco
308 of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
311 and deriv' tycos (tyco `%% tys) = deriv tycos tyco
312 andalso forall (deriv' tycos) tys
313 | deriv' _ (ITyVar _) = true
314 in deriv [] tyco end;
315 fun print_stmt deresolve = print_haskell_stmt labelled_name
316 class_syntax tyco_syntax const_syntax (make_vars reserved)
317 deresolve contr_classparam_typs
318 (if string_classes then deriving_show else K false);
321 val import_includes_ps =
322 map (fn (name, _) => str ("import qualified " ^ name ^ ";")) includes;
323 fun print_module_frame module_name ps =
324 (module_name, Pretty.chunks2 (
325 str ("module " ^ module_name ^ " where {")
329 fun print_module module_name (gr, imports) =
331 val deresolve = deresolver module_name
332 fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
333 val import_ps = import_includes_ps @ map (print_import o fst) imports;
334 fun print_stmt' gr name = case Graph.get_node gr name
336 | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
337 val body_ps = map_filter (print_stmt' gr) ((flat o rev o Graph.strong_conn) gr);
339 print_module_frame module_name
340 ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
344 fun write_module width (SOME destination) (module_name, content) =
346 val _ = File.check_dir destination;
347 val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
348 o separate "/" o Long_Name.explode) module_name;
349 val _ = Isabelle_System.mkdirs (Path.dir filepath);
351 (File.write filepath o format [] width o Pretty.chunks2)
352 [str "{-# LANGUAGE ScopedTypeVariables #-}", content]
354 | write_module width NONE (_, content) = writeln (format [] width content);
356 Code_Target.serialization
357 (fn width => fn destination => K () o map (write_module width destination))
358 (fn present => fn width => rpair (try (deresolver ""))
359 o format present width o Pretty.chunks o map snd)
360 (map (uncurry print_module_frame o apsnd single) includes
361 @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
362 ((flat o rev o Graph.strong_conn) haskell_program))
365 val serializer : Code_Target.serializer =
366 Code_Target.parse_args (Scan.optional (Args.$$$ "root" -- Args.colon |-- Args.name) ""
367 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
368 >> (fn (module_prefix, string_classes) =>
369 serialize_haskell module_prefix string_classes));
374 val s = ML_Syntax.print_char c;
375 in if s = "'" then "\\'" else s end;
376 fun numeral_haskell k = if k >= 0 then string_of_int k
377 else Library.enclose "(" ")" (signed_string_of_int k);
379 literal_char = Library.enclose "'" "'" o char_haskell,
380 literal_string = quote o translate_string char_haskell,
381 literal_numeral = numeral_haskell,
382 literal_positive_numeral = numeral_haskell,
383 literal_alternative_numeral = numeral_haskell,
384 literal_naive_numeral = numeral_haskell,
385 literal_list = enum "," "[" "]",
386 infix_cons = (5, ":")
390 (** optional monad syntax **)
392 fun pretty_haskell_monad c_bind =
394 fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
395 of SOME ((pat, ty), t') =>
396 SOME ((SOME ((pat, ty), true), t1), t')
398 fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
399 if c = c_bind_name then dest_bind t1 t2
401 | dest_monad _ t = case Code_Thingol.split_let t
402 of SOME (((pat, ty), tbind), t') =>
403 SOME ((SOME ((pat, ty), false), tbind), t')
405 fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
406 fun print_monad print_bind print_term (NONE, t) vars =
407 (semicolon [print_term vars NOBR t], vars)
408 | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
409 |> print_bind NOBR bind
410 |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
411 | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
412 |> print_bind NOBR bind
413 |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
414 fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
415 of SOME (bind, t') => let
416 val (binds, t'') = implode_monad c_bind' t'
417 val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
418 (bind :: binds) vars;
420 (brackify fxy o single o enclose "do { " " }" o Pretty.breaks)
421 (ps @| print_term vars' NOBR t'')
423 | NONE => brackify_infix (1, L) fxy
424 (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
425 in (2, ([c_bind], pretty)) end;
427 fun add_monad target' raw_c_bind thy =
429 val c_bind = Code.read_const thy raw_c_bind;
430 in if target = target' then
432 |> Code_Target.add_const_syntax target c_bind
433 (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
434 else error "Only Haskell target allows for monad syntax" end;
440 Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
441 Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
442 Toplevel.theory (add_monad target raw_bind))
446 Code_Target.add_target
447 (target, { serializer = serializer, literals = literals,
448 check = { env_var = "ISABELLE_GHC", make_destination = I,
449 make_command = fn module_name =>
450 "\"$ISABELLE_GHC\" -XRankNTypes -XScopedTypeVariables -odir build -hidir build -stubdir build -e \"\" " ^
451 module_name ^ ".hs" } })
452 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
453 brackify_infix (1, R) fxy (
454 print_typ (INFX (1, X)) ty1,
456 print_typ (INFX (1, R)) ty2
458 #> fold (Code_Target.add_reserved target) [
459 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
460 "import", "default", "forall", "let", "in", "class", "qualified", "data",
461 "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
463 #> fold (Code_Target.add_reserved target) [
464 "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
465 "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
466 "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
467 "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
468 "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
469 "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
470 "ExitSuccess", "False", "GT", "HeapOverflow",
471 "IOError", "IOException", "IllegalOperation",
472 "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
473 "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
474 "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
475 "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
476 "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
477 "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
478 "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
479 "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
480 "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
481 "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
482 "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
483 "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
484 "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
485 "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
486 "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
487 "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
488 "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
489 "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
490 "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
491 "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
492 "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
493 "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
494 "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
495 "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
496 "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
497 "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
498 "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
499 "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
500 "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
501 "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
502 "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
503 "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
504 "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
505 "sequence_", "show", "showChar", "showException", "showField", "showList",
506 "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
507 "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
508 "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
509 "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
510 "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
511 "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
512 ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);