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