1 (* Title: Pure/Tools/codegen_serializer.ML
3 Author: Florian Haftmann, TU Muenchen
5 Serializer from intermediate language ("Thin-gol") to
6 target languages (like ML or Haskell).
9 signature CODEGEN_SERIALIZER =
11 type 'a pretty_syntax;
14 -> (string -> CodegenThingol.itype pretty_syntax option)
15 * (string -> CodegenThingol.iexpr pretty_syntax option)
18 -> CodegenThingol.module
19 -> unit -> Pretty.T * unit;
20 val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
21 ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
22 val parse_targetdef: (string -> string) -> string -> string;
24 ml: string * (string * string * string -> serializer),
25 haskell: string * (string -> serializer)
29 structure CodegenSerializer: CODEGEN_SERIALIZER =
32 open CodegenThingolOp;
41 (** generic serialization **)
45 datatype lrx = L | R | X;
50 | INFX of (int * lrx);
58 type 'a pretty_syntax = (int * int) * (fixity -> (fixity -> 'a -> Pretty.T) -> 'a list -> Pretty.T);
60 fun eval_lrx L L = false
61 | eval_lrx R R = false
62 | eval_lrx _ _ = true;
64 fun eval_fxy BR _ = true
65 | eval_fxy NOBR _ = false
66 | eval_fxy (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
69 andalso eval_lrx lr1 lr2
70 | eval_fxy (INFX _) _ = false;
72 val str = setmp print_mode [] Pretty.str;
74 fun brackify _ [p] = p
75 | brackify true (ps as _::_) = Pretty.enclose "(" ")" (Pretty.breaks ps)
76 | brackify false (ps as _::_) = Pretty.block (Pretty.breaks ps);
78 fun from_app mk_app from_expr const_syntax fxy (f, es) =
81 brackify (eval_fxy fxy BR) (mk_app f es)
82 | mk (SOME ((i, k), pr)) es =
84 val (es1, es2) = splitAt (i, es);
86 brackify (eval_fxy fxy BR) (pr fxy from_expr es1 :: map (from_expr BR) es2)
88 in mk (const_syntax f) es end;
90 fun fillin_mixfix fxy_this ms fxy pr args =
92 fun brackify true = Pretty.enclose "(" ")"
93 | brackify false = Pretty.block;
96 | fillin (Arg fxy :: ms) (a :: args) =
97 pr fxy a :: fillin ms args
98 | fillin (Ignore :: ms) args =
100 | fillin (Pretty p :: ms) args =
102 | fillin (Quote q :: ms) args =
103 pr BR q :: fillin ms args;
104 in brackify true (fillin ms args) (* (eval_fxy fxy_this fxy) *) end;
107 (* user-defined syntax *)
109 val (atomK, infixK, infixlK, infixrK) =
110 ("atom", "infix", "infixl", "infixr");
111 val _ = OuterSyntax.add_keywords ["atom", "infix", "infixl", "infixr"];
113 fun parse_infix (fixity as INFX (i, x)) s =
115 val l = case x of L => fixity
117 val r = case x of R => fixity
120 pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
123 fun parse_mixfix reader s ctxt =
125 fun sym s = Scan.lift ($$ s);
126 fun lift_reader ctxt s =
129 |-> (fn x => pair (Quote x));
130 val sym_any = Scan.lift (Scan.one Symbol.not_eof);
131 val parse = Scan.repeat (
132 (sym "_" -- sym "_" >> K (Arg NOBR))
133 || (sym "_" >> K (Arg BR))
134 || (sym "?" >> K Ignore)
135 || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
136 || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
137 ( $$ "'" |-- Scan.one Symbol.not_eof
138 || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
139 $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))
141 ( sym "'" |-- sym_any
142 || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*")
143 sym_any) >> (Pretty o str o implode)));
144 in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s)
145 of (p, (ctxt, [])) => (p, ctxt)
146 | _ => error ("Malformed mixfix annotation: " ^ quote s)
149 fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- (
150 OuterParse.$$$ infixK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
151 || OuterParse.$$$ infixlK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
152 || OuterParse.$$$ infixrK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
153 || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
154 || pair (parse_mixfix reader, BR)
155 ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
157 fun parse_syntax reader =
159 fun is_arg (Arg _) = true
160 | is_arg Ignore = true
164 val i = length (List.filter is_arg mfx)
165 in ((i, i), fillin_mixfix fixity mfx) end;
167 parse_syntax_proto reader
168 #-> (fn (mfx_reader, fixity) : ('Z -> 'Y mixfix list * 'Z) * fixity =>
169 pair (mfx_reader #-> (fn mfx => pair (mk fixity mfx)))
173 fun newline_correct s =
175 |> Symbol.strip_blanks
176 |> space_explode "\n"
177 |> map (implode o (fn [] => []
179 | xs => xs) o explode)
180 |> space_implode "\n";
182 fun parse_named_quote resolv s =
183 case Scan.finite Symbol.stopper (Scan.repeat (
185 || ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
186 --| $$ "`" >> (resolv o implode))
188 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> implode
189 ) >> implode) (Symbol.explode s)
191 | (p, ss) => error ("Malformed definition: " ^ quote p ^ " - " ^ commas ss);
193 fun parse_targetdef resolv = parse_named_quote resolv o newline_correct;
196 (* abstract serializer *)
200 -> (string -> CodegenThingol.itype pretty_syntax option)
201 * (string -> CodegenThingol.iexpr pretty_syntax option)
203 -> string list option
204 -> CodegenThingol.module
205 -> unit -> Pretty.T * unit;
207 fun abstract_serializer preprocess (from_defs, from_module, validator)
208 (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) postprocess select module =
210 fun from_prim (name, prim) =
211 case AList.lookup (op =) prim target
212 of NONE => error ("no primitive definition for " ^ quote name)
216 |> debug 3 (fn _ => "selecting submodule...")
217 |> (if is_some select then (partof o the) select else I)
218 |> tap (Pretty.writeln o pretty_deps)
219 |> debug 3 (fn _ => "preprocessing...")
221 |> debug 3 (fn _ => "serializing...")
222 |> serialize (from_defs (from_prim, (tyco_syntax, const_syntax)))
223 from_module validator nspgrp name_root
227 fun abstract_validator keywords name =
229 fun replace_invalid c =
230 if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
231 andalso not (NameSpace.separator = c)
236 |> member (op =) keywords ? suffix "'"
237 |> (fn name' => if name = name' then name else suffix_it name')
240 |> translate_string replace_invalid
242 |> (fn name' => if name = name' then NONE else SOME name')
245 fun postprocess_single_file path p =
246 File.write (Path.unpack path) (Pretty.output p ^ "\n");
248 fun parse_single_file serializer =
249 OuterParse.name >> (fn path => serializer (postprocess_single_file path));
253 (** ML serializer **)
257 fun ml_from_defs (is_cons, needs_type)
258 (from_prim, (tyco_syntax, const_syntax)) resolv defs =
262 val (p_init, p_last) = split_last ps
264 Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
266 fun ml_from_label s =
268 val s' = NameSpace.unpack s;
270 NameSpace.pack (Library.drop (length s' - 2, s'))
271 |> translate_string (fn "_" => "__" | "." => "_" | c => c)
274 | postify [p] f = Pretty.block [p, Pretty.brk 1, f]
275 | postify (ps as _::_) f = Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, f];
276 fun ml_from_type fxy (IType (tyco, tys)) =
277 (case tyco_syntax tyco
279 postify (map (ml_from_type BR) tys) ((str o resolv) tyco)
280 | SOME ((i, k), pr) =>
281 if not (i <= length tys andalso length tys <= k)
282 then error ("number of argument mismatch in customary serialization: "
283 ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
285 else pr fxy ml_from_type tys)
286 | ml_from_type fxy (IFun (t1, t2)) =
288 fun eval_fxy_postfix BR _ = false
289 | eval_fxy_postfix NOBR _ = false
290 | eval_fxy_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
293 andalso eval_lrx lr1 lr2
294 | eval_fxy_postfix (INFX _) _ = false;
296 brackify (eval_fxy_postfix fxy (INFX (1, R))) [
297 ml_from_type (INFX (1, X)) t1,
299 ml_from_type (INFX (1, R)) t2
302 | ml_from_type _ (IVarT (v, [])) =
304 | ml_from_type _ (IVarT (_, sort)) =
305 "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
306 | ml_from_type _ (IDictT fs) =
307 Pretty.gen_list "," "{" "}" (
309 Pretty.block [str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs
311 fun ml_from_pat fxy (ICons ((f, ps), ty)) =
313 of NONE => if length ps <= 1
316 |> map (ml_from_pat BR)
317 |> cons ((str o resolv) f)
318 |> brackify (eval_fxy fxy BR)
321 |> map (ml_from_pat BR)
322 |> Pretty.gen_list "," "(" ")"
324 |> cons ((str o resolv) f)
325 |> brackify (eval_fxy fxy BR)
326 | SOME ((i, k), pr) =>
327 if not (i <= length ps andalso length ps <= k)
328 then error ("number of argument mismatch in customary serialization: "
329 ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
331 else pr fxy ml_from_expr (map iexpr_of_ipat ps))
332 | ml_from_pat fxy (IVarP (v, ty)) =
335 brackify (eval_fxy fxy BR) [
342 and ml_from_expr fxy (e as IApp (e1, e2)) =
344 of (e as (IConst (f, _)), es) =>
345 ml_from_app fxy (f, es)
347 brackify (eval_fxy fxy BR) [
348 ml_from_expr NOBR e1,
351 | ml_from_expr fxy (e as IConst (f, _)) =
352 ml_from_app fxy (f, [])
353 | ml_from_expr fxy (IVarE (v, _)) =
355 | ml_from_expr fxy (IAbs ((v, _), e)) =
356 brackify (eval_fxy fxy BR) [
357 str ("fn " ^ v ^ " =>"),
360 | ml_from_expr fxy (e as ICase (_, [_])) =
362 val (ps, e) = unfold_let e;
363 fun mk_val (p, e) = Pretty.block [
372 [str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
373 [str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
376 | ml_from_expr fxy (ICase (e, c::cs)) =
378 fun mk_clause definer (p, e) =
386 in brackify (eval_fxy fxy BR) (
388 :: ml_from_expr NOBR e
390 :: map (mk_clause "| ") cs
392 | ml_from_expr fxy (IInst _) =
393 error "cannot serialize poly instant to ML"
394 | ml_from_expr fxy (IDictE fs) =
395 Pretty.gen_list "," "{" "}" (
397 Pretty.block [str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs
399 | ml_from_expr fxy (ILookup ([], v)) =
401 | ml_from_expr fxy (ILookup ([l], v)) =
402 brackify (eval_fxy fxy BR) [
403 str ("#" ^ (ml_from_label l)),
406 | ml_from_expr fxy (ILookup (ls, v)) =
407 brackify (eval_fxy fxy BR) [
409 ^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e))
414 error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
416 if is_cons f andalso length es > 1
418 [(str o resolv) f, Pretty.gen_list " *" "(" ")" (map (ml_from_expr BR) es)]
420 (str o resolv) f :: map (ml_from_expr BR) es
421 and ml_from_app fxy =
422 from_app ml_mk_app ml_from_expr const_syntax fxy;
423 fun ml_from_funs (ds as d::ds_tl) =
425 fun mk_definer [] = "val"
426 | mk_definer _ = "fun";
427 fun check_args (_, Fun ((pats, _)::_, _)) NONE =
428 SOME (mk_definer pats)
429 | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) =
430 if mk_definer pats = definer
432 else error ("mixing simultaneous vals and funs not implemented")
434 error ("function definition block containing other definitions than functions")
435 val definer = the (fold check_args ds NONE);
436 fun mk_eq definer f ty (pats, expr) =
438 val lhs = [str (definer ^ " " ^ f)]
440 then [str ":", ml_from_type NOBR ty]
441 else map (ml_from_pat BR) pats)
442 val rhs = [str "=", ml_from_expr NOBR expr]
444 Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
446 fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) =
448 val (pats_hd::pats_tl) = (fst o split_list) eqs;
449 val shift = if null eq_tl then I else map (Pretty.block o single);
450 in (Pretty.block o Pretty.fbreaks o shift) (
451 mk_eq definer f ty eq
452 :: map (mk_eq "|" f ty) eq_tl
458 :: map (mk_fun "and") ds_tl
461 fun ml_from_datatypes defs =
463 val defs' = List.mapPartial
464 (fn (name, Datatype info) => SOME (name, info)
465 | (name, Datatypecons _) => NONE
466 | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def)
468 fun mk_cons (co, []) =
470 | mk_cons (co, tys) =
475 :: separate (Pretty.block [str " *", Pretty.brk 1]) (map (ml_from_type NOBR) tys)
477 fun mk_datatype definer (t, ((vs, cs), _)) =
480 :: ml_from_type NOBR (t `%% map IVarT vs)
483 :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons cs)
489 mk_datatype "datatype " d
490 :: map (mk_datatype "and ") ds_tl
494 fun ml_from_def (name, Undef) =
495 error ("empty definition during serialization: " ^ quote name)
496 | ml_from_def (name, Prim prim) =
497 from_prim (name, prim)
498 | ml_from_def (name, Typesyn (vs, ty)) =
499 (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
502 ml_from_type NOBR (name `%% map IVarT vs),
505 ml_from_type NOBR ty,
509 | ml_from_def (name, Class _) =
510 error ("can't serialize class declaration " ^ quote name ^ " to ML")
511 | ml_from_def (_, Classmember _) =
513 | ml_from_def (name, Classinst _) =
514 error ("can't serialize instance declaration " ^ quote name ^ " to ML")
515 in (writeln ("ML defs " ^ (commas o map fst) defs); case defs
516 of (_, Fun _)::_ => ml_from_funs defs
517 | (_, Datatypecons _)::_ => ml_from_datatypes defs
518 | (_, Datatype _)::_ => ml_from_datatypes defs
519 | [def] => ml_from_def def)
524 fun ml_from_thingol target (nsp_dtcon, nsp_class, int_tyco)
525 nspgrp (tyco_syntax, const_syntax) name_root select module =
527 val reserved_ml = ThmDatabase.ml_reserved @ [
528 "bool", "int", "list", "true", "false"
530 fun ml_from_module _ (name, ps) () =
532 str ("structure " ^ name ^ " = "),
535 ] @ separate (str "") ps @ [
537 str ("end; (* struct " ^ name ^ " *)")
539 fun needs_type (IType (tyco, _)) =
540 has_nsp tyco nsp_class
541 orelse tyco = int_tyco
542 | needs_type (IDictT _) =
546 fun is_cons c = has_nsp c nsp_dtcon;
549 of SOME ((i, _), _) => i
550 | _ => if has_nsp s nsp_dtcon
551 then case get_def module s
552 of Datatypecons dtname => case get_def module dtname
553 of Datatype ((_, cs), _) =>
554 let val l = AList.lookup (op =) cs s |> the |> length
555 in if l >= 2 then l else 0 end
557 fun preprocess module =
559 |> tap (Pretty.writeln o pretty_deps)
560 |> debug 3 (fn _ => "eta-expanding...")
561 |> eta_expand eta_expander
562 |> debug 3 (fn _ => "eta-expanding polydefs...")
564 |> debug 3 (fn _ => "eliminating classes...")
567 abstract_serializer preprocess (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml)
568 (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module
575 fun haskell_from_defs is_cons (from_prim, (tyco_syntax, const_syntax)) resolv defs =
579 val (pr, b) = split_last (NameSpace.unpack s);
580 val (c::cs) = String.explode b;
581 in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
584 val (pr, b) = split_last (NameSpace.unpack s);
585 val (c::cs) = String.explode b;
586 in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
589 val (prfix, base) = (split_last o NameSpace.unpack o resolv) s
591 NameSpace.pack (map upper_first prfix @ [base])
594 if NameSpace.is_qualified f
597 then (upper_first o resolv) f
598 else (lower_first o resolv) f
601 fun haskell_from_sctxt vs =
603 fun from_sctxt [] = str ""
606 |> map (fn (v, cls) => str ((upper_first o resolv) cls ^ " " ^ lower_first v))
607 |> Pretty.gen_list "," "(" ")"
608 |> (fn p => Pretty.block [p, str " => "])
611 |> map (fn (v, sort) => map (pair v) sort)
615 fun haskell_from_type fxy ty =
617 fun from_itype fxy (IType (tyco, tys)) sctxt =
618 (case tyco_syntax tyco
621 |> fold_map (from_itype BR) tys
622 |-> (fn tyargs => pair (brackify (eval_fxy fxy BR) ((str o upper_first o resolv) tyco :: tyargs)))
623 | SOME ((i, k), pr) =>
624 if not (i <= length tys andalso length tys <= k)
625 then error ("number of argument mismatch in customary serialization: "
626 ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
628 else (pr fxy haskell_from_type tys, sctxt))
629 | from_itype fxy (IFun (t1, t2)) sctxt =
631 |> from_itype (INFX (1, X)) t1
632 ||>> from_itype (INFX (1, R)) t2
633 |-> (fn (p1, p2) => pair (
634 brackify (eval_fxy fxy (INFX (1, R))) [
640 | from_itype fxy (IVarT (v, [])) sctxt =
642 |> pair ((str o lower_first) v)
643 | from_itype fxy (IVarT (v, sort)) sctxt =
645 |> AList.default (op =) (v, [])
646 |> AList.map_entry (op =) v (fold (insert (op =)) sort)
647 |> pair ((str o lower_first) v)
648 | from_itype fxy (IDictT _) _ =
649 error "cannot serialize dictionary type to haskell"
653 ||> haskell_from_sctxt
654 |> (fn (pty, pctxt) => Pretty.block [pctxt, pty])
656 fun haskell_from_pat fxy (ICons ((f, ps), _)) =
660 |> map (haskell_from_pat BR)
661 |> cons ((str o resolv_const) f)
662 |> brackify (eval_fxy fxy BR)
663 | SOME ((i, k), pr) =>
664 if not (i <= length ps andalso length ps <= k)
665 then error ("number of argument mismatch in customary serialization: "
666 ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
668 else pr fxy haskell_from_expr (map iexpr_of_ipat ps))
669 | haskell_from_pat fxy (IVarP (v, _)) =
670 (str o lower_first) v
671 and haskell_from_expr fxy (e as IApp (e1, e2)) =
673 of (e as (IConst (f, _)), es) =>
674 haskell_from_app fxy (f, es)
676 brackify (eval_fxy fxy BR) [
677 haskell_from_expr NOBR e1,
678 haskell_from_expr BR e2
680 | haskell_from_expr fxy (e as IConst (f, _)) =
681 haskell_from_app fxy (f, [])
682 | haskell_from_expr fxy (IVarE (v, _)) =
683 (str o lower_first) v
684 | haskell_from_expr fxy (e as IAbs _) =
686 val (vs, body) = unfold_abs e
688 brackify (eval_fxy fxy BR) (
690 :: map (str o lower_first o fst) vs @ [
692 haskell_from_expr NOBR body
695 | haskell_from_expr fxy (e as ICase (_, [_])) =
697 val (ps, body) = unfold_let e;
698 fun mk_bind (p, e) = Pretty.block [
699 haskell_from_pat BR p,
702 haskell_from_expr NOBR e
705 [str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
706 [str ("in "), haskell_from_expr NOBR body] |> Pretty.block
708 | haskell_from_expr fxy (ICase (e, c::cs)) =
710 fun mk_clause definer (p, e) =
713 haskell_from_pat NOBR p,
716 haskell_from_expr NOBR e
718 in brackify (eval_fxy fxy BR) (
720 :: haskell_from_expr NOBR e
722 :: map (mk_clause "| ") cs
724 | haskell_from_expr fxy (IInst (e, _)) =
725 haskell_from_expr fxy e
726 | haskell_from_expr fxy (IDictE _) =
727 error "cannot serialize dictionary expression to haskell"
728 | haskell_from_expr fxy (ILookup _) =
729 error "cannot serialize lookup expression to haskell"
730 and haskell_mk_app f es =
731 (str o resolv_const) f :: map (haskell_from_expr BR) es
732 and haskell_from_app fxy =
733 from_app haskell_mk_app haskell_from_expr const_syntax fxy;
734 fun haskell_from_def (name, Undef) =
735 error ("empty statement during serialization: " ^ quote name)
736 | haskell_from_def (name, Prim prim) =
737 from_prim (name, prim)
738 | haskell_from_def (name, Fun (eqs, (_, ty))) =
740 fun from_eq name (args, rhs) =
742 str (lower_first name),
743 Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args),
747 haskell_from_expr NOBR rhs
752 str (lower_first name ^ " ::"),
754 haskell_from_type NOBR ty
756 Pretty.chunks (map (from_eq name) eqs)
759 | haskell_from_def (name, Typesyn (vs, ty)) =
762 haskell_from_sctxt vs,
763 str (upper_first name),
764 Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vs),
767 haskell_from_type NOBR ty
769 | haskell_from_def (name, Datatype ((vars, constrs), _)) =
771 fun mk_cons (co, tys) =
772 (Pretty.block o Pretty.breaks) (
773 str ((upper_first o resolv) co)
774 :: map (haskell_from_type NOBR) tys
779 :: haskell_from_sctxt vars
780 :: str (upper_first name)
781 :: Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vars)
784 :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
787 | haskell_from_def (_, Datatypecons _) =
789 | haskell_from_def (name, Class ((supclasss, (v, membrs)), _)) =
791 fun mk_member (m, (_, ty)) =
793 str (resolv m ^ " ::"),
795 haskell_from_type NOBR ty
800 haskell_from_sctxt (map (fn class => (v, [class])) supclasss),
801 str ((upper_first name) ^ " " ^ v),
804 Pretty.chunks (map mk_member membrs)
807 | haskell_from_def (name, Classmember _) =
809 | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), memdefs)) =
812 haskell_from_sctxt arity,
813 str ((upper_first o resolv) clsname),
815 haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)),
818 Pretty.chunks (map (fn (m, funn) => haskell_from_def (m, Fun funn) |> the) memdefs)
821 case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs
823 | l => (SOME o Pretty.chunks o separate (str "")) l
828 fun haskell_from_thingol target nsp_dtcon
829 nspgrp (tyco_syntax, const_syntax) name_root select module =
831 val reserved_haskell = [
832 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
833 "import", "default", "forall", "let", "in", "class", "qualified", "data",
834 "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
836 "Bool", "fst", "snd", "Integer", "True", "False", "negate"
840 val (pr, b) = split_last (NameSpace.unpack s);
841 val (c::cs) = String.explode b;
842 in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
843 fun haskell_from_module _ (name, ps) () =
845 str ("module " ^ (upper_first name) ^ " where"),
848 Pretty.chunks (separate (str "") ps)
850 fun is_cons c = has_nsp c nsp_dtcon;
853 |> Option.map (fst o fst)
855 fun preprocess module =
857 |> tap (Pretty.writeln o pretty_deps)
858 |> debug 3 (fn _ => "eta-expanding...")
859 |> eta_expand eta_expander
861 abstract_serializer preprocess (haskell_from_defs is_cons, haskell_from_module, abstract_validator reserved_haskell)
862 (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module
868 (** lookup record **)
872 fun seri s f = (s, f s);
874 ml = seri "ml" ml_from_thingol,
875 haskell = seri "haskell" haskell_from_thingol