1 (* Title: Tools/code/code_target.ML
3 Author: Florian Haftmann, TU Muenchen
5 Serializer from intermediate language ("Thin-gol")
6 to target languages (like SML or Haskell).
9 signature CODE_TARGET =
11 include BASIC_CODE_THINGOL;
13 val add_syntax_class: string -> class
14 -> (string * (string * string) list) option -> theory -> theory;
15 val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
16 val add_syntax_tycoP: string -> string -> OuterParse.token list
17 -> (theory -> theory) * OuterParse.token list;
18 val add_syntax_constP: string -> string -> OuterParse.token list
19 -> (theory -> theory) * OuterParse.token list;
21 val add_undefined: string -> string -> string -> theory -> theory;
22 val add_pretty_list: string -> string -> string -> theory -> theory;
23 val add_pretty_list_string: string -> string -> string
24 -> string -> string list -> theory -> theory;
25 val add_pretty_char: string -> string -> string list -> theory -> theory
26 val add_pretty_numeral: string -> bool -> string -> string -> string -> string
27 -> string -> string -> theory -> theory;
28 val add_pretty_ml_string: string -> string -> string list -> string
29 -> string -> string -> theory -> theory;
30 val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;
32 val allow_exception: string -> theory -> theory;
35 val add_serializer: string * serializer -> theory -> theory;
36 val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
37 -> (theory -> string -> string) -> string list option
38 -> CodeThingol.code -> unit;
39 val assert_serializer: theory -> string -> string;
41 val eval_verbose: bool ref;
42 val eval_invoke: theory -> (theory -> string -> string)
43 -> (string * (unit -> 'a) option ref) -> CodeThingol.code
44 -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
45 val code_width: int ref;
47 val setup: theory -> theory;
50 structure CodeTarget : CODE_TARGET =
53 open BasicCodeThingol;
60 fun xs @| y = xs @ [y];
61 val str = PrintMode.setmp [] Pretty.str;
62 val concat = Pretty.block o Pretty.breaks;
63 val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
64 fun semicolon ps = Pretty.block [concat ps, str ";"];
69 datatype lrx = L | R | X;
74 | INFX of (int * lrx);
76 val APP = INFX (~1, L);
78 fun eval_lrx L L = false
79 | eval_lrx R R = false
80 | eval_lrx _ _ = true;
82 fun eval_fxy NOBR NOBR = false
83 | eval_fxy BR NOBR = false
84 | eval_fxy NOBR BR = false
85 | eval_fxy (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
88 andalso eval_lrx lr lr_ctxt
90 | eval_fxy _ (INFX _) = false
91 | eval_fxy (INFX _) NOBR = false
92 | eval_fxy _ _ = true;
94 fun gen_brackify _ [p] = p
95 | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
96 | gen_brackify false (ps as _::_) = Pretty.block ps;
98 fun brackify fxy_ctxt ps =
99 gen_brackify (eval_fxy BR fxy_ctxt) (Pretty.breaks ps);
101 fun brackify_infix infx fxy_ctxt ps =
102 gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
104 type class_syntax = string * (string -> string option);
105 type typ_syntax = int * ((fixity -> itype -> Pretty.T)
106 -> fixity -> itype list -> Pretty.T);
107 type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
108 -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
111 (* user-defined syntax *)
115 | Pretty of Pretty.T;
117 fun mk_mixfix prep_arg (fixity_this, mfx) =
119 fun is_arg (Arg _) = true
121 val i = (length o filter is_arg) mfx;
124 | fillin pr (Arg fxy :: mfx) (a :: args) =
125 (pr fxy o prep_arg) a :: fillin pr mfx args
126 | fillin pr (Pretty p :: mfx) args =
127 p :: fillin pr mfx args
129 error ("Inconsistent mixfix: too many arguments")
131 error ("Inconsistent mixfix: too less arguments");
133 (i, fn pr => fn fixity_ctxt => fn args =>
134 gen_brackify (eval_fxy fixity_this fixity_ctxt) (fillin pr mfx args))
137 fun parse_infix prep_arg (x, i) s =
139 val l = case x of L => INFX (i, L) | _ => INFX (i, X);
140 val r = case x of R => INFX (i, R) | _ => INFX (i, X);
142 mk_mixfix prep_arg (INFX (i, x), [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
145 fun parse_mixfix prep_arg s =
147 val sym_any = Scan.one Symbol.is_regular;
148 val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
149 ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
150 || ($$ "_" >> K (Arg BR))
151 || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
154 || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
155 sym_any) >> (Pretty o str o implode)));
156 in case Scan.finite Symbol.stopper parse (Symbol.explode s)
157 of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
158 | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
159 | _ => Scan.!! (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
162 fun parse_args f args =
163 case Scan.read Args.stopper f args
165 | NONE => error "Bad serializer arguments";
168 (* generic serializer combinators *)
170 fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons
171 lhs vars fxy (app as ((c, (_, tys)), ts)) =
173 of NONE => if lhs andalso not (is_cons c) then
174 error ("non-constructor on left hand side of equation: " ^ labelled_name c)
175 else brackify fxy (pr_app' lhs vars app)
178 val k = if i < 0 then length tys else i;
179 fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
182 else if k < length ts
183 then case chop k ts of (ts1, ts2) =>
184 brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
185 else pr_term lhs vars fxy (CodeThingol.eta_expand app k)
188 fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars =
191 of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
193 val vars' = CodeName.intro_vars (the_list v) vars;
194 val vars'' = CodeName.intro_vars vs vars';
195 val v' = Option.map (CodeName.lookup_var vars') v;
196 val pat' = Option.map (pr_term true vars'' fxy) pat;
197 in (pr_bind' ((v', pat'), ty), vars'') end;
200 (* list, char, string, numeral and monad abstract syntax transformations *)
202 fun implode_list c_nil c_cons t =
204 fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
208 | dest_cons _ = NONE;
209 val (ts, t') = CodeThingol.unfoldr dest_cons t;
211 of IConst (c, _) => if c = c_nil then SOME ts else NONE
215 fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
217 fun idx c = find_index (curry (op =) c) c_nibbles;
218 fun decode ~1 _ = NONE
220 | decode n m = SOME (chr (n * 16 + m));
221 in decode (idx c1) (idx c2) end
222 | decode_char _ _ = NONE;
224 fun implode_string c_char c_nibbles mk_char mk_string ts =
226 fun implode_char (IConst (c, _) `$ t1 `$ t2) =
227 if c = c_char then decode_char c_nibbles (t1, t2) else NONE
228 | implode_char _ = NONE;
229 val ts' = map implode_char ts;
230 in if forall is_some ts'
231 then (SOME o str o mk_string o implode o map_filter I) ts'
235 fun implode_numeral c_bit0 c_bit1 c_pls c_min c_bit =
237 fun dest_bit (IConst (c, _)) = if c = c_bit0 then SOME 0
238 else if c = c_bit1 then SOME 1
241 fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
242 else if c = c_min then SOME ~1
244 | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
245 if c = c_bit then case (dest_numeral t1, dest_bit t2)
246 of (SOME n, SOME b) => SOME (2 * n + b)
249 | dest_numeral _ = NONE;
252 fun implode_monad c_mbind c_kbind t =
254 fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
256 then case CodeThingol.split_abs t2
257 of SOME (((v, pat), ty), t') => SOME ((SOME (((SOME v, pat), ty), true), t1), t')
260 then SOME ((NONE, t1), t2)
262 | dest_monad t = case CodeThingol.split_let t
263 of SOME (((pat, ty), tbind), t') => SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
265 in CodeThingol.unfoldr dest_monad t end;
268 (** name auxiliary **)
270 val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
271 val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
274 apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
276 fun mk_modl_name_tab init_names prefix module_alias code =
278 fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;
280 case module_alias name
281 of SOME name' => name'
282 | NONE => nsp_map (fn name => (the_single o fst)
283 (Name.variants [name] init_names)) name;
286 of SOME prefix => NameSpace.append prefix name
290 |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
291 o fst o dest_name o fst)
293 in fn name => (the o Symtab.lookup tab) name end;
297 (** SML/OCaml serializer **)
300 MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
301 | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
302 | MLClass of string * (vname * ((class * string) list * (string * itype) list))
303 | MLClassinst of string * ((class * (string * (vname * sort) list))
304 * ((class * (string * (string * dict list list))) list
305 * (string * const) list));
307 fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
309 val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
310 val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
311 fun pr_dicts fxy ds =
313 fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
314 | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
319 | pr_proj (ps as _ :: _) p =
320 brackets [Pretty.enum " o" "(" ")" ps, p];
321 fun pr_dictc fxy (DictConst (inst, dss)) =
322 brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
323 | pr_dictc fxy (DictVar (classrels, v)) =
324 pr_proj (map (str o deresolv) classrels) ((str o pr_dictvar) v)
327 | [d] => pr_dictc fxy d
328 | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
332 |> map (fn (v, sort) => map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)
333 |> map (pr_dicts BR);
334 fun pr_tycoexpr fxy (tyco, tys) =
336 val tyco' = (str o deresolv) tyco
337 in case map (pr_typ BR) tys
339 | [p] => Pretty.block [p, Pretty.brk 1, tyco']
340 | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
342 and pr_typ fxy (tyco `%% tys) =
343 (case tyco_syntax tyco
344 of NONE => pr_tycoexpr fxy (tyco, tys)
346 if not (i = length tys)
347 then error ("Number of argument mismatch in customary serialization: "
348 ^ (string_of_int o length) tys ^ " given, "
349 ^ string_of_int i ^ " expected")
350 else pr pr_typ fxy tys)
351 | pr_typ fxy (ITyVar v) =
353 fun pr_term lhs vars fxy (IConst c) =
354 pr_app lhs vars fxy (c, [])
355 | pr_term lhs vars fxy (IVar v) =
356 str (CodeName.lookup_var vars v)
357 | pr_term lhs vars fxy (t as t1 `$ t2) =
358 (case CodeThingol.unfold_const_app t
359 of SOME c_ts => pr_app lhs vars fxy c_ts
361 brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
362 | pr_term lhs vars fxy (t as _ `|-> _) =
364 val (binds, t') = CodeThingol.unfold_abs t;
365 fun pr ((v, pat), ty) =
366 pr_bind NOBR ((SOME v, pat), ty)
367 #>> (fn p => concat [str "fn", p, str "=>"]);
368 val (ps, vars') = fold_map pr binds vars;
369 in brackets (ps @ [pr_term lhs vars' NOBR t']) end
370 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
371 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
372 then pr_case vars fxy cases
373 else pr_app lhs vars fxy c_ts
374 | NONE => pr_case vars fxy cases)
375 and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
376 if is_cons c then let
379 (str o deresolv) c :: map (pr_term lhs vars BR) ts
380 else if k = length ts then
381 [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
382 else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else
384 :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts
385 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
386 and pr_bind' ((NONE, NONE), _) = str "_"
387 | pr_bind' ((SOME v, NONE), _) = str v
388 | pr_bind' ((NONE, SOME p), _) = p
389 | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
390 and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
391 and pr_case vars fxy (cases as ((_, [_]), _)) =
393 val (binds, t') = CodeThingol.unfold_let (ICase cases);
394 fun pr ((pat, ty), t) vars =
396 |> pr_bind NOBR ((NONE, SOME pat), ty)
397 |>> (fn p => semicolon [str "val", p, str "=", pr_term false vars NOBR t])
398 val (ps, vars') = fold_map pr binds vars;
401 [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
402 [str ("in"), Pretty.fbrk, pr_term false vars' NOBR t'] |> Pretty.block,
406 | pr_case vars fxy (((td, ty), b::bs), _) =
408 fun pr delim (pat, t) =
410 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
412 concat [str delim, p, str "=>", pr_term false vars' NOBR t]
415 (Pretty.enclose "(" ")" o single o brackify fxy) (
417 :: pr_term false vars NOBR td
422 | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
423 fun pr_def (MLFuns (funns as (funn :: funns'))) =
427 fun no_args _ ((ts, _) :: _) = length ts
428 | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;
430 | mk 0 vs = if (null o filter_out (null o snd)) vs then "val" else "fun"
432 fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)
433 | chk (_, ((vs, ty), eqs)) (SOME defi) =
434 if defi = mk (no_args ty eqs) vs then SOME defi
435 else error ("Mixing simultaneous vals and funs not implemented: "
436 ^ commas (map (labelled_name o fst) funns));
437 in the (fold chk funns NONE) end;
438 fun pr_funn definer (name, ((raw_vs, ty), [])) =
440 val vs = filter_out (null o snd) raw_vs;
441 val n = length vs + (length o fst o CodeThingol.unfold_fun) ty;
445 :: (str o deresolv) name
446 :: map str (replicate n "_")
450 :: (str o ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name
454 | pr_funn definer (name, ((raw_vs, ty), eqs as eq :: eqs')) =
456 val vs = filter_out (null o snd) raw_vs;
457 val shift = if null eqs' then I else
458 map (Pretty.block o single o Pretty.block o single);
459 fun pr_eq definer (ts, t) =
461 val consts = map_filter
462 (fn c => if (is_some o const_syntax) c
463 then NONE else (SOME o NameSpace.base o deresolv) c)
464 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
466 |> CodeName.intro_vars consts
467 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
468 (insert (op =)) ts []);
471 [str definer, (str o deresolv) name]
472 @ (if null ts andalso null vs
473 then [str ":", pr_typ NOBR ty]
476 @ map (pr_term true vars BR) ts)
477 @ [str "=", pr_term false vars NOBR t]
481 (Pretty.block o Pretty.fbreaks o shift) (
483 :: map (pr_eq "|") eqs'
486 val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
487 in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
488 | pr_def (MLDatas (datas as (data :: datas'))) =
496 Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
498 fun pr_data definer (tyco, (vs, [])) =
501 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
505 | pr_data definer (tyco, (vs, cos)) =
508 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
510 :: separate (str "|") (map pr_co cos)
512 val (ps, p) = split_last (pr_data "datatype" data :: map (pr_data "and") datas');
513 in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
514 | pr_def (MLClass (class, (v, (superclasses, classparams)))) =
516 val w = first_upper v ^ "_";
517 fun pr_superclass_field (class, classrel) =
519 pr_label_classrel classrel, ":", "'" ^ v, deresolv class
521 fun pr_classparam_field (classparam, ty) =
523 (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
525 fun pr_classparam_proj (classparam, _) =
528 (str o deresolv) classparam,
529 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
531 str ("#" ^ pr_label_classparam classparam),
534 fun pr_superclass_proj (_, classrel) =
537 (str o deresolv) classrel,
538 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
540 str ("#" ^ pr_label_classrel classrel),
547 (str o deresolv) class,
549 Pretty.enum "," "{" "};" (
550 map pr_superclass_field superclasses @ map pr_classparam_field classparams
553 :: map pr_superclass_proj superclasses
554 @ map pr_classparam_proj classparams
557 | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
559 fun pr_superclass (_, (classrel, dss)) =
561 (str o pr_label_classrel) classrel,
563 pr_dicts NOBR [DictConst dss]
565 fun pr_classparam (classparam, c_inst) =
567 (str o pr_label_classparam) classparam,
569 pr_app false init_syms NOBR (c_inst, [])
573 str (if null arity then "val" else "fun"),
574 (str o deresolv) inst ] @
577 Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classparam classparam_insts),
579 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
582 in pr_def ml_def end;
584 fun pr_sml_modl name content =
586 str ("structure " ^ name ^ " = "),
591 str ("end; (*struct " ^ name ^ "*)")
594 fun pr_ocaml tyco_syntax const_syntax labelled_name
595 init_syms deresolv is_cons ml_def =
597 fun pr_dicts fxy ds =
599 fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
600 | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
602 fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
603 fun pr_dictc fxy (DictConst (inst, dss)) =
604 brackify fxy ((str o deresolv) inst :: map (pr_dicts BR) dss)
605 | pr_dictc fxy (DictVar (classrels, v)) =
606 pr_proj (map deresolv classrels) ((str o pr_dictvar) v)
609 | [d] => pr_dictc fxy d
610 | _ :: _ => (Pretty.list "(" ")" o map (pr_dictc NOBR)) ds
614 |> map (fn (v, sort) => map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)
615 |> map (pr_dicts BR);
616 fun pr_tycoexpr fxy (tyco, tys) =
618 val tyco' = (str o deresolv) tyco
619 in case map (pr_typ BR) tys
621 | [p] => Pretty.block [p, Pretty.brk 1, tyco']
622 | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
624 and pr_typ fxy (tyco `%% tys) =
625 (case tyco_syntax tyco
626 of NONE => pr_tycoexpr fxy (tyco, tys)
628 if not (i = length tys)
629 then error ("Number of argument mismatch in customary serialization: "
630 ^ (string_of_int o length) tys ^ " given, "
631 ^ string_of_int i ^ " expected")
632 else pr pr_typ fxy tys)
633 | pr_typ fxy (ITyVar v) =
635 fun pr_term lhs vars fxy (IConst c) =
636 pr_app lhs vars fxy (c, [])
637 | pr_term lhs vars fxy (IVar v) =
638 str (CodeName.lookup_var vars v)
639 | pr_term lhs vars fxy (t as t1 `$ t2) =
640 (case CodeThingol.unfold_const_app t
641 of SOME c_ts => pr_app lhs vars fxy c_ts
643 brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
644 | pr_term lhs vars fxy (t as _ `|-> _) =
646 val (binds, t') = CodeThingol.unfold_abs t;
647 fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
648 val (ps, vars') = fold_map pr binds vars;
649 in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
650 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
651 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
652 then pr_case vars fxy cases
653 else pr_app lhs vars fxy c_ts
654 | NONE => pr_case vars fxy cases)
655 and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
657 if length tys = length ts
659 of [] => [(str o deresolv) c]
660 | [t] => [(str o deresolv) c, pr_term lhs vars BR t]
661 | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
662 else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))]
663 else (str o deresolv) c
664 :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts)
665 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
666 and pr_bind' ((NONE, NONE), _) = str "_"
667 | pr_bind' ((SOME v, NONE), _) = str v
668 | pr_bind' ((NONE, SOME p), _) = p
669 | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
670 and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
671 and pr_case vars fxy (cases as ((_, [_]), _)) =
673 val (binds, t') = CodeThingol.unfold_let (ICase cases);
674 fun pr ((pat, ty), t) vars =
676 |> pr_bind NOBR ((NONE, SOME pat), ty)
677 |>> (fn p => concat [str "let", p, str "=", pr_term false vars NOBR t, str "in"])
678 val (ps, vars') = fold_map pr binds vars;
679 in Pretty.chunks (ps @| pr_term false vars' NOBR t') end
680 | pr_case vars fxy (((td, ty), b::bs), _) =
682 fun pr delim (pat, t) =
684 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
685 in concat [str delim, p, str "->", pr_term false vars' NOBR t] end;
687 (Pretty.enclose "(" ")" o single o brackify fxy) (
689 :: pr_term false vars NOBR td
694 | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
695 fun pr_def (MLFuns (funns as funn :: funns')) =
697 fun fish_parm _ (w as SOME _) = w
698 | fish_parm (IVar v) NONE = SOME v
699 | fish_parm _ NONE = NONE;
700 fun fillup_parm _ (_, SOME v) = v
701 | fillup_parm x (i, NONE) = x ^ string_of_int i;
702 fun fish_parms vars eqs =
704 val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
705 val x = Name.variant (map_filter I fished1) "x";
706 val fished2 = map_index (fillup_parm x) fished1;
707 val (fished3, _) = Name.variants fished2 Name.context;
708 val vars' = CodeName.intro_vars fished3 vars;
709 in map (CodeName.lookup_var vars') fished3 end;
712 val consts = map_filter
713 (fn c => if (is_some o const_syntax) c
714 then NONE else (SOME o NameSpace.base o deresolv) c)
715 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
717 |> CodeName.intro_vars consts
718 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
719 (insert (op =)) ts []);
721 (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts),
723 pr_term false vars NOBR t
725 fun pr_eqs name ty [] =
727 val n = (length o fst o CodeThingol.unfold_fun) ty;
730 map str (replicate n "_")
733 @@ (str o ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name
736 | pr_eqs _ _ [(ts, t)] =
738 val consts = map_filter
739 (fn c => if (is_some o const_syntax) c
740 then NONE else (SOME o NameSpace.base o deresolv) c)
741 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
743 |> CodeName.intro_vars consts
744 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
745 (insert (op =)) ts []);
748 map (pr_term true vars BR) ts
750 @@ pr_term false vars NOBR t
753 | pr_eqs _ _ (eqs as (eq as ([_], _)) :: eqs') =
760 :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
762 | pr_eqs _ _ (eqs as eq :: eqs') =
764 val consts = map_filter
765 (fn c => if (is_some o const_syntax) c
766 then NONE else (SOME o NameSpace.base o deresolv) c)
767 ((fold o CodeThingol.fold_constnames) (insert (op =)) (map snd eqs) []);
769 |> CodeName.intro_vars consts;
770 val dummy_parms = (map str o fish_parms vars o map fst) eqs;
773 Pretty.breaks dummy_parms
779 :: (Pretty.block o Pretty.commas) dummy_parms
784 :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] o single o pr_eq) eqs'
787 fun pr_funn definer (name, ((vs, ty), eqs)) =
790 :: (str o deresolv) name
791 :: pr_tyvars (filter_out (null o snd) vs)
792 @| pr_eqs name ty eqs
794 val (ps, p) = split_last (pr_funn "let rec" funn :: map (pr_funn "and") funns');
795 in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
796 | pr_def (MLDatas (datas as (data :: datas'))) =
804 Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
806 fun pr_data definer (tyco, (vs, [])) =
809 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
813 | pr_data definer (tyco, (vs, cos)) =
816 :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
818 :: separate (str "|") (map pr_co cos)
820 val (ps, p) = split_last (pr_data "type" data :: map (pr_data "and") datas');
821 in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
822 | pr_def (MLClass (class, (v, (superclasses, classparams)))) =
824 val w = "_" ^ first_upper v;
825 fun pr_superclass_field (class, classrel) =
827 deresolv classrel, ":", "'" ^ v, deresolv class
829 fun pr_classparam_field (classparam, ty) =
831 (str o deresolv) classparam, str ":", pr_typ NOBR ty
833 fun pr_classparam_proj (classparam, _) =
836 (str o deresolv) classparam,
839 str (w ^ "." ^ deresolv classparam ^ ";;")
844 (str o deresolv) class,
846 Pretty.enum ";" "{" "};;" (
847 map pr_superclass_field superclasses @ map pr_classparam_field classparams
850 :: map pr_classparam_proj classparams
852 | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
854 fun pr_superclass (_, (classrel, dss)) =
856 (str o deresolv) classrel,
858 pr_dicts NOBR [DictConst dss]
860 fun pr_classparam_inst (classparam, c_inst) =
862 (str o deresolv) classparam,
864 pr_app false init_syms NOBR (c_inst, [])
869 :: (str o deresolv) inst
872 @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
873 Pretty.enum ";" "{" "}" (map pr_superclass superarities @ map pr_classparam_inst classparam_insts),
875 pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
879 in pr_def ml_def end;
881 fun pr_ocaml_modl name content =
883 str ("module " ^ name ^ " = "),
888 str ("end;; (*struct " ^ name ^ "*)")
891 val code_width = ref 80;
892 fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
894 fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog
895 (_ : string -> class_syntax option) tyco_syntax const_syntax code =
897 val module_alias = if is_some module then K module else raw_module_alias;
898 val is_cons = CodeThingol.is_cons code;
900 Def of string * ml_def option
901 | Module of string * ((Name.context * Name.context) * node Graph.T);
902 val init_names = Name.make_context reserved_syms;
903 val init_module = ((init_names, init_names), Graph.empty);
904 fun map_node [] f = f
905 | map_node (m::ms) f =
906 Graph.default_node (m, Module (m, init_module))
907 #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) => Module (dmodlname, (nsp, map_node ms f nodes)));
908 fun map_nsp_yield [] f (nsp, nodes) =
910 val (x, nsp') = f nsp
911 in (x, (nsp', nodes)) end
912 | map_nsp_yield (m::ms) f (nsp, nodes) =
916 |> Graph.default_node (m, Module (m, init_module))
917 |> Graph.map_node_yield m (fn Module (dmodlname, nsp_nodes) =>
919 val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
920 in (x, Module (dmodlname, nsp_nodes')) end)
921 in (x, (nsp, nodes')) end;
922 val init_syms = CodeName.make_vars reserved_syms;
923 val name_modl = mk_modl_name_tab init_names NONE module_alias code;
924 fun name_def upper name nsp =
926 val (_, base) = dest_name name;
927 val base' = if upper then first_upper base else base;
928 val ([base''], nsp') = Name.variants [base'] nsp;
929 in (base'', nsp') end;
930 fun map_nsp_fun f (nsp_fun, nsp_typ) =
932 val (x, nsp_fun') = f nsp_fun
933 in (x, (nsp_fun', nsp_typ)) end;
934 fun map_nsp_typ f (nsp_fun, nsp_typ) =
936 val (x, nsp_typ') = f nsp_typ
937 in (x, (nsp_fun, nsp_typ')) end;
940 (fn (name, CodeThingol.Fun info) =>
941 map_nsp_fun (name_def false name) >> (fn base => (base, (name, (apsnd o map) fst info)))
942 | (name, def) => error ("Function block containing illegal definition: " ^ labelled_name name)
944 >> (split_list #> apsnd MLFuns);
945 fun mk_datatype defs =
947 (fn (name, CodeThingol.Datatype info) =>
948 map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
949 | (name, CodeThingol.Datatypecons _) =>
950 map_nsp_fun (name_def true name) >> (fn base => (base, NONE))
951 | (name, def) => error ("Datatype block containing illegal definition: " ^ labelled_name name)
953 >> (split_list #> apsnd (map_filter I
954 #> (fn [] => error ("Datatype block without data definition: " ^ (commas o map (labelled_name o fst)) defs)
955 | infos => MLDatas infos)));
958 (fn (name, CodeThingol.Class info) =>
959 map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))
960 | (name, CodeThingol.Classrel _) =>
961 map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
962 | (name, CodeThingol.Classparam _) =>
963 map_nsp_fun (name_def false name) >> (fn base => (base, NONE))
964 | (name, def) => error ("Class block containing illegal definition: " ^ labelled_name name)
966 >> (split_list #> apsnd (map_filter I
967 #> (fn [] => error ("Class block without class definition: " ^ (commas o map (labelled_name o fst)) defs)
968 | [info] => MLClass info)));
969 fun mk_inst [(name, CodeThingol.Classinst info)] =
970 map_nsp_fun (name_def false name)
971 >> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst info)));
972 fun add_group mk defs nsp_nodes =
974 val names as (name :: names') = map fst defs;
977 |> fold (fold (insert (op =)) o Graph.imm_succs code) names
978 |> subtract (op =) names;
979 val (modls, _) = (split_list o map dest_name) names;
980 val modl' = (the_single o distinct (op =) o map name_modl) modls
982 error ("Different namespace prefixes for mutual dependencies:\n"
983 ^ commas (map labelled_name names)
985 ^ commas (map (NameSpace.qualifier o NameSpace.qualifier) names));
986 val modl_explode = NameSpace.explode modl';
987 fun add_dep name name'' =
989 val modl'' = (name_modl o fst o dest_name) name'';
990 in if modl' = modl'' then
991 map_node modl_explode
992 (Graph.add_edge (name, name''))
994 val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
995 (modl_explode, NameSpace.explode modl'');
998 (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
999 handle Graph.CYCLES _ => error ("Dependency "
1000 ^ quote name ^ " -> " ^ quote name''
1001 ^ " would result in module dependency cycle"))
1005 |> map_nsp_yield modl_explode (mk defs)
1006 |-> (fn (base' :: bases', def') =>
1007 apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def')))
1008 #> fold2 (fn name' => fn base' => Graph.new_node (name', (Def (base', NONE)))) names' bases')))
1009 |> apsnd (fold (fn name => fold (add_dep name) deps) names)
1010 |> apsnd (fold (map_node modl_explode o Graph.add_edge) (product names names))
1012 fun group_defs [(_, CodeThingol.Bot)] =
1014 | group_defs ((defs as (_, CodeThingol.Fun _)::_)) =
1015 add_group mk_funs defs
1016 | group_defs ((defs as (_, CodeThingol.Datatypecons _)::_)) =
1017 add_group mk_datatype defs
1018 | group_defs ((defs as (_, CodeThingol.Datatype _)::_)) =
1019 add_group mk_datatype defs
1020 | group_defs ((defs as (_, CodeThingol.Class _)::_)) =
1021 add_group mk_class defs
1022 | group_defs ((defs as (_, CodeThingol.Classrel _)::_)) =
1023 add_group mk_class defs
1024 | group_defs ((defs as (_, CodeThingol.Classparam _)::_)) =
1025 add_group mk_class defs
1026 | group_defs ((defs as [(_, CodeThingol.Classinst _)])) =
1027 add_group mk_inst defs
1028 | group_defs defs = error ("Illegal mutual dependencies: " ^
1029 (commas o map (labelled_name o fst)) defs)
1032 |> fold group_defs (map (AList.make (Graph.get_node code))
1033 (rev (Graph.strong_conn code)))
1034 fun deresolver prefix name =
1036 val modl = (fst o dest_name) name;
1037 val modl' = (NameSpace.explode o name_modl) modl;
1038 val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');
1041 |> fold (fn m => fn g => case Graph.get_node g m
1042 of Module (_, (_, g)) => g) modl'
1043 |> (fn g => case Graph.get_node g name of Def (defname, _) => defname);
1045 NameSpace.implode (remainder @ [defname'])
1046 end handle Graph.UNDEF _ =>
1047 error ("Unknown definition name: " ^ labelled_name name);
1048 fun the_prolog modlname = case module_prolog modlname
1050 | SOME p => [p, str ""];
1051 fun pr_node prefix (Def (_, NONE)) =
1053 | pr_node prefix (Def (_, SOME def)) =
1054 SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
1055 (deresolver prefix) is_cons def)
1056 | pr_node prefix (Module (dmodlname, (_, nodes))) =
1057 SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
1058 @ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
1059 o rev o flat o Graph.strong_conn) nodes)));
1060 val p = Pretty.chunks (the_prolog "" @ separate (str "") ((map_filter
1061 (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes))
1064 val eval_verbose = ref false;
1066 fun isar_seri_sml module file =
1068 val output = case file
1069 of NONE => use_text "generated code" Output.ml_output (!eval_verbose) o code_output
1070 | SOME "-" => PrintMode.setmp [] writeln o code_output
1071 | SOME file => File.write (Path.explode file) o code_output;
1073 parse_args (Scan.succeed ())
1074 #> (fn () => seri_ml pr_sml pr_sml_modl module output)
1077 fun isar_seri_ocaml module file =
1079 val output = case file
1080 of NONE => error "OCaml: no internal compilation"
1081 | SOME "-" => PrintMode.setmp [] writeln o code_output
1082 | SOME file => File.write (Path.explode file) o code_output;
1083 fun output_file file = File.write (Path.explode file) o code_output;
1084 val output_diag = PrintMode.setmp [] writeln o code_output;
1086 parse_args (Scan.succeed ())
1087 #> (fn () => seri_ml pr_ocaml pr_ocaml_modl module output)
1091 (** Haskell serializer **)
1095 fun pr_bind' ((NONE, NONE), _) = str "_"
1096 | pr_bind' ((SOME v, NONE), _) = str v
1097 | pr_bind' ((NONE, SOME p), _) = p
1098 | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p]
1100 val pr_bind_haskell = gen_pr_bind pr_bind';
1104 fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name
1105 init_syms deresolv_here deresolv is_cons deriving_show def =
1107 fun class_name class = case class_syntax class
1108 of NONE => deresolv class
1109 | SOME (class, _) => class;
1110 fun classparam_name class classparam = case class_syntax class
1111 of NONE => deresolv_here classparam
1112 | SOME (_, classparam_syntax) => case classparam_syntax classparam
1113 of NONE => (snd o dest_name) classparam
1114 | SOME classparam => classparam
1115 fun pr_typparms tyvars vs =
1116 case maps (fn (v, sort) => map (pair v) sort) vs
1118 | xs => Pretty.block [
1119 Pretty.enum "," "(" ")" (
1120 map (fn (v, class) => str
1121 (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) xs
1125 fun pr_tycoexpr tyvars fxy (tyco, tys) =
1126 brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
1127 and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
1128 (case tyco_syntax tyco
1130 pr_tycoexpr tyvars fxy (deresolv tyco, tys)
1132 if not (i = length tys)
1133 then error ("Number of argument mismatch in customary serialization: "
1134 ^ (string_of_int o length) tys ^ " given, "
1135 ^ string_of_int i ^ " expected")
1136 else pr (pr_typ tyvars) fxy tys)
1137 | pr_typ tyvars fxy (ITyVar v) =
1138 (str o CodeName.lookup_var tyvars) v;
1139 fun pr_typscheme_expr tyvars (vs, tycoexpr) =
1140 Pretty.block (pr_typparms tyvars vs @@ pr_tycoexpr tyvars NOBR tycoexpr);
1141 fun pr_typscheme tyvars (vs, ty) =
1142 Pretty.block (pr_typparms tyvars vs @@ pr_typ tyvars NOBR ty);
1143 fun pr_term lhs vars fxy (IConst c) =
1144 pr_app lhs vars fxy (c, [])
1145 | pr_term lhs vars fxy (t as (t1 `$ t2)) =
1146 (case CodeThingol.unfold_const_app t
1147 of SOME app => pr_app lhs vars fxy app
1150 pr_term lhs vars NOBR t1,
1151 pr_term lhs vars BR t2
1153 | pr_term lhs vars fxy (IVar v) =
1154 (str o CodeName.lookup_var vars) v
1155 | pr_term lhs vars fxy (t as _ `|-> _) =
1157 val (binds, t') = CodeThingol.unfold_abs t;
1158 fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
1159 val (ps, vars') = fold_map pr binds vars;
1160 in brackets (str "\\" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
1161 | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
1162 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
1163 then pr_case vars fxy cases
1164 else pr_app lhs vars fxy c_ts
1165 | NONE => pr_case vars fxy cases)
1166 and pr_app' lhs vars ((c, _), ts) =
1167 (str o deresolv) c :: map (pr_term lhs vars BR) ts
1168 and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
1169 and pr_bind fxy = pr_bind_haskell pr_term fxy
1170 and pr_case vars fxy (cases as ((_, [_]), _)) =
1172 val (binds, t) = CodeThingol.unfold_let (ICase cases);
1173 fun pr ((pat, ty), t) vars =
1175 |> pr_bind BR ((NONE, SOME pat), ty)
1176 |>> (fn p => semicolon [p, str "=", pr_term false vars NOBR t])
1177 val (ps, vars') = fold_map pr binds vars;
1179 Pretty.block_enclose (
1181 concat [str "}", str "in", pr_term false vars' NOBR t]
1184 | pr_case vars fxy (((td, ty), bs as _ :: _), _) =
1188 val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
1189 in semicolon [p, str "->", pr_term false vars' NOBR t] end;
1191 Pretty.block_enclose (
1192 concat [str "(case", pr_term false vars NOBR td, str "of", str "{"],
1196 | pr_case vars fxy ((_, []), _) = str "error \"empty case\"";
1197 fun pr_def (name, CodeThingol.Fun ((vs, ty), [])) =
1199 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1200 val n = (length o fst o CodeThingol.unfold_fun) ty;
1204 (str o suffix " ::" o deresolv_here) name,
1206 pr_typscheme tyvars (vs, ty),
1210 (str o deresolv_here) name
1211 :: map str (replicate n "_")
1214 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name
1218 | pr_def (name, CodeThingol.Fun ((vs, ty), eqs)) =
1220 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1221 fun pr_eq ((ts, t), _) =
1223 val consts = map_filter
1224 (fn c => if (is_some o const_syntax) c
1225 then NONE else (SOME o NameSpace.base o deresolv) c)
1226 ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
1227 val vars = init_syms
1228 |> CodeName.intro_vars consts
1229 |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
1230 (insert (op =)) ts []);
1233 (str o deresolv_here) name
1234 :: map (pr_term true vars BR) ts
1236 @@ pr_term false vars NOBR t
1242 (str o suffix " ::" o deresolv_here) name,
1244 pr_typscheme tyvars (vs, ty),
1250 | pr_def (name, CodeThingol.Datatype (vs, [])) =
1252 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1256 pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
1259 | pr_def (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
1261 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1265 :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
1267 :: (str o deresolv_here) co
1268 :: pr_typ tyvars BR ty
1269 :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
1272 | pr_def (name, CodeThingol.Datatype (vs, co :: cos)) =
1274 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1275 fun pr_co (co, tys) =
1277 (str o deresolv_here) co
1278 :: map (pr_typ tyvars BR) tys
1283 :: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
1286 :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
1287 @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
1290 | pr_def (name, CodeThingol.Class (v, (superclasses, classparams))) =
1292 val tyvars = CodeName.intro_vars [v] init_syms;
1293 fun pr_classparam (classparam, ty) =
1295 (str o classparam_name name) classparam,
1297 pr_typ tyvars NOBR ty
1300 Pretty.block_enclose (
1303 pr_typparms tyvars [(v, map fst superclasses)],
1304 str (deresolv_here name ^ " " ^ CodeName.lookup_var tyvars v),
1308 ) (map pr_classparam classparams)
1310 | pr_def (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
1312 val tyvars = CodeName.intro_vars (map fst vs) init_syms;
1313 fun pr_instdef ((classparam, c_inst), _) =
1315 (str o classparam_name class) classparam,
1317 pr_app false init_syms NOBR (c_inst, [])
1320 Pretty.block_enclose (
1323 pr_typparms tyvars vs,
1324 str (class_name class ^ " "),
1325 pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
1329 ) (map pr_instdef classparam_insts)
1333 fun pretty_haskell_monad c_mbind c_kbind =
1335 fun pretty pr vars fxy [(t, _)] =
1337 val pr_bind = pr_bind_haskell (K pr);
1338 fun pr_mbind (NONE, t) vars =
1339 (semicolon [pr vars NOBR t], vars)
1340 | pr_mbind (SOME (bind, true), t) vars = vars
1341 |> pr_bind NOBR bind
1342 |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
1343 | pr_mbind (SOME (bind, false), t) vars = vars
1344 |> pr_bind NOBR bind
1345 |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
1346 val (binds, t) = implode_monad c_mbind c_kbind t;
1347 val (ps, vars') = fold_map pr_mbind binds vars;
1348 fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p;
1349 in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
1354 fun seri_haskell module_prefix module destination string_classes labelled_name
1355 reserved_syms raw_module_alias module_prolog
1356 class_syntax tyco_syntax const_syntax code =
1358 val _ = Option.map File.check destination;
1359 val is_cons = CodeThingol.is_cons code;
1360 val module_alias = if is_some module then K module else raw_module_alias;
1361 val init_names = Name.make_context reserved_syms;
1362 val name_modl = mk_modl_name_tab init_names module_prefix module_alias code;
1363 fun add_def (name, (def, deps)) =
1365 val (modl, base) = dest_name name;
1366 fun name_def base = Name.variants [base] #>> the_single;
1367 fun add_fun upper (nsp_fun, nsp_typ) =
1369 val (base', nsp_fun') = name_def (if upper then first_upper base else base) nsp_fun
1370 in (base', (nsp_fun', nsp_typ)) end;
1371 fun add_typ (nsp_fun, nsp_typ) =
1373 val (base', nsp_typ') = name_def (first_upper base) nsp_typ
1374 in (base', (nsp_fun, nsp_typ')) end;
1377 of CodeThingol.Bot => pair base
1378 | CodeThingol.Fun _ => add_fun false
1379 | CodeThingol.Datatype _ => add_typ
1380 | CodeThingol.Datatypecons _ => add_fun true
1381 | CodeThingol.Class _ => add_typ
1382 | CodeThingol.Classrel _ => pair base
1383 | CodeThingol.Classparam _ => add_fun false
1384 | CodeThingol.Classinst _ => pair base;
1385 val modlname' = name_modl modl;
1388 of CodeThingol.Bot => I
1389 | CodeThingol.Datatypecons _ =>
1390 cons (name, ((NameSpace.append modlname' base', base'), NONE))
1391 | CodeThingol.Classrel _ => I
1392 | CodeThingol.Classparam _ =>
1393 cons (name, ((NameSpace.append modlname' base', base'), NONE))
1394 | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
1396 Symtab.map_default (modlname', ([], ([], (init_names, init_names))))
1397 (apfst (fold (insert (op = : string * string -> bool)) deps))
1398 #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
1399 #-> (fn (base', names) =>
1400 (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
1401 (add_def base' defs, names)))
1404 fold add_def (AList.make (fn name => (Graph.get_node code name, Graph.imm_succs code name))
1405 (Graph.strong_conn code |> flat)) Symtab.empty;
1406 val init_syms = CodeName.make_vars reserved_syms;
1408 (fst o fst o the o AList.lookup (op =) ((fst o snd o the
1409 o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
1410 handle Option => error ("Unknown definition name: " ^ labelled_name name);
1411 fun deresolv_here name =
1412 (snd o fst o the o AList.lookup (op =) ((fst o snd o the
1413 o Symtab.lookup code') ((name_modl o fst o dest_name) name))) name
1414 handle Option => error ("Unknown definition name: " ^ labelled_name name);
1415 fun deriving_show tyco =
1417 fun deriv _ "fun" = false
1418 | deriv tycos tyco = member (op =) tycos tyco orelse
1419 case the_default CodeThingol.Bot (try (Graph.get_node code) tyco)
1420 of CodeThingol.Bot => true
1421 | CodeThingol.Datatype (_, cs) => forall (deriv' (tyco :: tycos))
1423 and deriv' tycos (tyco `%% tys) = deriv tycos tyco
1424 andalso forall (deriv' tycos) tys
1425 | deriv' _ (ITyVar _) = true
1426 in deriv [] tyco end;
1427 fun seri_def qualified = pr_haskell class_syntax tyco_syntax
1428 const_syntax labelled_name init_syms
1429 deresolv_here (if qualified then deresolv else deresolv_here) is_cons
1430 (if string_classes then deriving_show else K false);
1431 fun write_module (SOME destination) modlname =
1433 val filename = case modlname
1434 of "" => Path.explode "Main.hs"
1435 | _ => (Path.ext "hs" o Path.explode o implode o separate "/" o NameSpace.explode) modlname;
1436 val pathname = Path.append destination filename;
1437 val _ = File.mkdir (Path.dir pathname);
1438 in File.write pathname end
1439 | write_module NONE _ = PrintMode.setmp [] writeln;
1440 fun seri_module (modlname', (imports, (defs, _))) =
1444 |> map (name_modl o fst o dest_name)
1446 |> remove (op =) modlname';
1448 imports @ map fst defs
1449 |> map_filter (try deresolv)
1450 |> map NameSpace.base
1451 |> has_duplicates (op =);
1452 val mk_import = str o (if qualified
1453 then prefix "import qualified "
1454 else prefix "import ") o suffix ";";
1457 str ("module " ^ modlname' ^ " where {")
1459 :: map mk_import imports'
1461 :: separate (str "") ((case module_prolog modlname'
1462 of SOME prolog => [prolog]
1465 (fn (name, (_, SOME def)) => SOME (seri_def qualified (name, def))
1466 | (_, (_, NONE)) => NONE) defs)
1471 |> write_module destination modlname'
1473 in Symtab.fold (fn modl => fn () => seri_module modl) code' () end;
1475 fun isar_seri_haskell module file =
1477 val destination = case file
1478 of NONE => error ("Haskell: no internal compilation")
1480 | SOME file => SOME (Path.explode file)
1482 parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
1483 -- Scan.optional (Args.$$$ "string_classes" >> K true) false
1484 >> (fn (module_prefix, string_classes) =>
1485 seri_haskell module_prefix module destination string_classes))
1489 (** diagnosis serializer **)
1491 fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
1493 val init_names = CodeName.make_vars [];
1494 fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
1495 brackify_infix (1, R) fxy [
1496 pr_typ (INFX (1, X)) ty1,
1498 pr_typ (INFX (1, R)) ty2
1501 val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
1504 |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
1507 |> PrintMode.setmp [] writeln
1514 datatype syntax_expr = SyntaxExpr of {
1515 class: (string * (string -> string option)) Symtab.table,
1516 inst: unit Symtab.table,
1517 tyco: typ_syntax Symtab.table,
1518 const: term_syntax Symtab.table
1521 fun mk_syntax_expr ((class, inst), (tyco, const)) =
1522 SyntaxExpr { class = class, inst = inst, tyco = tyco, const = const };
1523 fun map_syntax_expr f (SyntaxExpr { class, inst, tyco, const }) =
1524 mk_syntax_expr (f ((class, inst), (tyco, const)));
1525 fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
1526 SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
1528 (Symtab.join (K snd) (class1, class2),
1529 Symtab.join (K snd) (inst1, inst2)),
1530 (Symtab.join (K snd) (tyco1, tyco2),
1531 Symtab.join (K snd) (const1, const2))
1534 datatype syntax_modl = SyntaxModl of {
1535 alias: string Symtab.table,
1536 prolog: Pretty.T Symtab.table
1539 fun mk_syntax_modl (alias, prolog) =
1540 SyntaxModl { alias = alias, prolog = prolog };
1541 fun map_syntax_modl f (SyntaxModl { alias, prolog }) =
1542 mk_syntax_modl (f (alias, prolog));
1543 fun merge_syntax_modl (SyntaxModl { alias = alias1, prolog = prolog1 },
1544 SyntaxModl { alias = alias2, prolog = prolog2 }) =
1546 Symtab.join (K snd) (alias1, alias2),
1547 Symtab.join (K snd) (prolog1, prolog2)
1554 -> (string -> string)
1556 -> (string -> string option)
1557 -> (string -> Pretty.T option)
1558 -> (string -> class_syntax option)
1559 -> (string -> typ_syntax option)
1560 -> (string -> term_syntax option)
1561 -> CodeThingol.code -> unit;
1563 datatype target = Target of {
1565 serializer: serializer,
1566 reserved: string list,
1567 syntax_expr: syntax_expr,
1568 syntax_modl: syntax_modl
1571 fun mk_target (serial, ((serializer, reserved), (syntax_expr, syntax_modl))) =
1572 Target { serial = serial, reserved = reserved, serializer = serializer, syntax_expr = syntax_expr, syntax_modl = syntax_modl };
1573 fun map_target f ( Target { serial, serializer, reserved, syntax_expr, syntax_modl } ) =
1574 mk_target (f (serial, ((serializer, reserved), (syntax_expr, syntax_modl))));
1575 fun merge_target target (Target { serial = serial1, serializer = serializer, reserved = reserved1,
1576 syntax_expr = syntax_expr1, syntax_modl = syntax_modl1 },
1577 Target { serial = serial2, serializer = _, reserved = reserved2,
1578 syntax_expr = syntax_expr2, syntax_modl = syntax_modl2 }) =
1579 if serial1 = serial2 then
1580 mk_target (serial1, ((serializer, merge (op =) (reserved1, reserved2)),
1581 (merge_syntax_expr (syntax_expr1, syntax_expr2),
1582 merge_syntax_modl (syntax_modl1, syntax_modl2))
1585 error ("Incompatible serializers: " ^ quote target);
1587 structure CodeTargetData = TheoryDataFun
1589 type T = target Symtab.table * string list;
1590 val empty = (Symtab.empty, []);
1593 fun merge _ ((target1, exc1), (target2, exc2)) =
1594 (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2));
1597 fun the_serializer (Target { serializer, ... }) = serializer;
1598 fun the_reserved (Target { reserved, ... }) = reserved;
1599 fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
1600 fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x;
1602 fun assert_serializer thy target =
1603 case Symtab.lookup (fst (CodeTargetData.get thy)) target
1604 of SOME data => target
1605 | NONE => error ("Unknown code target language: " ^ quote target);
1607 fun add_serializer (target, seri) thy =
1609 val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target
1610 of SOME _ => warning ("overwriting existing serializer " ^ quote target)
1614 |> (CodeTargetData.map o apfst oo Symtab.map_default)
1615 (target, mk_target (serial (), ((seri, []),
1616 (mk_syntax_expr ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
1617 mk_syntax_modl (Symtab.empty, Symtab.empty)))))
1618 (map_target (fn (serial, ((_, keywords), syntax)) => (serial, ((seri, keywords), syntax))))
1621 fun map_seri_data target f thy =
1623 val _ = assert_serializer thy target;
1626 |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
1629 val target_SML = "SML";
1630 val target_OCaml = "OCaml";
1631 val target_Haskell = "Haskell";
1632 val target_diag = "diag";
1634 fun get_serializer thy target permissive module file args
1635 labelled_name = fn cs =>
1637 val (seris, exc) = CodeTargetData.get thy;
1638 val data = case Symtab.lookup seris target
1639 of SOME data => data
1640 | NONE => error ("Unknown code target language: " ^ quote target);
1641 val seri = the_serializer data;
1642 val reserved = the_reserved data;
1643 val { alias, prolog } = the_syntax_modl data;
1644 val { class, inst, tyco, const } = the_syntax_expr data;
1645 val project = if target = target_diag then I
1646 else CodeThingol.project_code permissive
1647 (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
1648 fun check_empty_funs code = case (filter_out (member (op =) exc)
1649 (CodeThingol.empty_funs code))
1651 | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
1655 #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
1656 (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
1659 fun eval_invoke thy labelled_name (ref_name, reff) code (t, ty) args =
1661 val _ = if CodeThingol.contains_dictvar t then
1662 error "Term to be evaluated constains free dictionaries" else ();
1663 val val_name = "Isabelle_Eval.EVAL.EVAL";
1664 val val_name' = "Isabelle_Eval.EVAL";
1665 val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
1666 val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
1670 seri (SOME [val_name]) code;
1671 use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
1672 ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_name'_args ^ "))");
1674 of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
1675 ^ " (reference probably has been shadowed)")
1680 |> CodeThingol.add_eval_def (val_name, (t, ty))
1686 (** optional pretty serialization **)
1690 val pretty : (string * {
1691 pretty_char: string -> string,
1692 pretty_string: string -> string,
1693 pretty_numeral: bool -> int -> string,
1694 pretty_list: Pretty.T list -> Pretty.T,
1695 infix_cons: int * string
1697 ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
1698 pretty_string = ML_Syntax.print_string,
1699 pretty_numeral = fn unbounded => fn k =>
1700 if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
1701 else string_of_int k,
1702 pretty_list = Pretty.enum "," "[" "]",
1703 infix_cons = (7, "::")}),
1704 ("OCaml", { pretty_char = fn c => enclose "'" "'"
1706 in if i < 32 orelse i = 39 orelse i = 92
1707 then prefix "\\" (string_of_int i)
1710 pretty_string = ML_Syntax.print_string,
1711 pretty_numeral = fn unbounded => fn k => if k >= 0 then
1713 "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
1714 else string_of_int k
1717 "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
1718 o string_of_int o op ~) k ^ ")"
1719 else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
1720 pretty_list = Pretty.enum ";" "[" "]",
1721 infix_cons = (6, "::")}),
1722 ("Haskell", { pretty_char = fn c => enclose "'" "'"
1724 in if i < 32 orelse i = 39 orelse i = 92
1725 then Library.prefix "\\" (string_of_int i)
1728 pretty_string = ML_Syntax.print_string,
1729 pretty_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
1730 else enclose "(" ")" (signed_string_of_int k),
1731 pretty_list = Pretty.enum "," "[" "]",
1732 infix_cons = (5, ":")})
1737 fun pr_pretty target = case AList.lookup (op =) pretty target
1739 | NONE => error ("Unknown code target language: " ^ quote target);
1741 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
1742 brackify_infix (target_fxy, R) fxy [
1743 pr (INFX (target_fxy, X)) t1,
1745 pr (INFX (target_fxy, R)) t2
1748 fun pretty_list c_nil c_cons target =
1750 val pretty_ops = pr_pretty target;
1751 val mk_list = #pretty_list pretty_ops;
1752 fun pretty pr vars fxy [(t1, _), (t2, _)] =
1753 case Option.map (cons t1) (implode_list c_nil c_cons t2)
1754 of SOME ts => mk_list (map (pr vars NOBR) ts)
1755 | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
1758 fun pretty_list_string c_nil c_cons c_char c_nibbles target =
1760 val pretty_ops = pr_pretty target;
1761 val mk_list = #pretty_list pretty_ops;
1762 val mk_char = #pretty_char pretty_ops;
1763 val mk_string = #pretty_string pretty_ops;
1764 fun pretty pr vars fxy [(t1, _), (t2, _)] =
1765 case Option.map (cons t1) (implode_list c_nil c_cons t2)
1766 of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts
1768 | NONE => mk_list (map (pr vars NOBR) ts)
1769 | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
1772 fun pretty_char c_char c_nibbles target =
1774 val mk_char = #pretty_char (pr_pretty target);
1775 fun pretty _ _ _ [(t1, _), (t2, _)] =
1776 case decode_char c_nibbles (t1, t2)
1777 of SOME c => (str o mk_char) c
1778 | NONE => error "Illegal character expression";
1781 fun pretty_numeral unbounded c_bit0 c_bit1 c_pls c_min c_bit target =
1783 val mk_numeral = #pretty_numeral (pr_pretty target);
1784 fun pretty _ _ _ [(t, _)] =
1785 case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
1786 of SOME k => (str o mk_numeral unbounded) k
1787 | NONE => error "Illegal numeral expression";
1790 fun pretty_ml_string c_char c_nibbles c_nil c_cons target =
1792 val pretty_ops = pr_pretty target;
1793 val mk_char = #pretty_char pretty_ops;
1794 val mk_string = #pretty_string pretty_ops;
1795 fun pretty pr vars fxy [(t, _)] =
1796 case implode_list c_nil c_cons t
1797 of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
1799 | NONE => error "Illegal ml_string expression")
1800 | NONE => error "Illegal ml_string expression";
1803 fun pretty_imperative_monad_bind bind' =
1805 fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
1806 | dest_abs (t, ty) =
1808 val vs = CodeThingol.fold_varnames cons t [];
1809 val v = Name.variant vs "x";
1810 val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
1811 in ((v, ty'), t `$ IVar v) end;
1812 fun tr_bind [(t1, _), (t2, ty2)] =
1814 val ((v, ty), t) = dest_abs (t2, ty2);
1815 in ICase (((t1, ty), [(IVar v, tr_bind' t)]), IVar "") end
1816 and tr_bind' (t as _ `$ _) = (case CodeThingol.unfold_app t
1817 of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
1818 then tr_bind [(x1, ty1), (x2, ty2)]
1822 fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);
1827 (** ML and Isar interface **)
1831 fun map_syntax_exprs target =
1832 map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
1833 fun map_syntax_modls target =
1834 map_seri_data target o apsnd o apsnd o apsnd o map_syntax_modl;
1835 fun map_reserveds target =
1836 map_seri_data target o apsnd o apfst o apsnd;
1838 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
1840 val class = prep_class thy raw_class;
1841 val class' = CodeName.class thy class;
1842 fun mk_classparam c = case AxClass.class_of_param thy c
1843 of SOME class'' => if class = class'' then CodeName.const thy c
1844 else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
1845 | NONE => error ("Not a class operation: " ^ quote c);
1846 fun mk_syntax_params raw_params = AList.lookup (op =)
1847 ((map o apfst) (mk_classparam o prep_const thy) raw_params);
1849 of SOME (syntax, raw_params) =>
1851 |> (map_syntax_exprs target o apfst o apfst)
1852 (Symtab.update (class', (syntax, mk_syntax_params raw_params)))
1855 |> (map_syntax_exprs target o apfst o apfst)
1856 (Symtab.delete_safe class')
1859 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
1861 val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
1864 |> (map_syntax_exprs target o apfst o apsnd)
1865 (Symtab.update (inst, ()))
1868 |> (map_syntax_exprs target o apfst o apsnd)
1869 (Symtab.delete_safe inst)
1872 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
1874 val tyco = prep_tyco thy raw_tyco;
1875 val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
1876 fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
1877 then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
1882 |> (map_syntax_exprs target o apsnd o apfst)
1883 (Symtab.update (tyco', check_args syntax))
1886 |> (map_syntax_exprs target o apsnd o apfst)
1887 (Symtab.delete_safe tyco')
1890 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
1892 val c = prep_const thy raw_c;
1893 val c' = CodeName.const thy c;
1894 fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
1895 then error ("Too many arguments in syntax for constant " ^ quote c)
1900 |> (map_syntax_exprs target o apsnd o apsnd)
1901 (Symtab.update (c', check_args syntax))
1904 |> (map_syntax_exprs target o apsnd o apsnd)
1905 (Symtab.delete_safe c')
1908 fun cert_class thy class =
1910 val _ = AxClass.get_definition thy class;
1913 fun read_class thy raw_class =
1915 val class = Sign.intern_class thy raw_class;
1916 val _ = AxClass.get_definition thy class;
1919 fun cert_tyco thy tyco =
1921 val _ = if Sign.declared_tyname thy tyco then ()
1922 else error ("No such type constructor: " ^ quote tyco);
1925 fun read_tyco thy raw_tyco =
1927 val tyco = Sign.intern_type thy raw_tyco;
1928 val _ = if Sign.declared_tyname thy tyco then ()
1929 else error ("No such type constructor: " ^ quote raw_tyco);
1932 fun no_bindings x = (Option.map o apsnd)
1933 (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
1935 fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy =
1937 val c_run' = prep_const thy c_run;
1938 val c_mbind' = prep_const thy c_mbind;
1939 val c_mbind'' = CodeName.const thy c_mbind';
1940 val c_kbind' = prep_const thy c_kbind;
1941 val c_kbind'' = CodeName.const thy c_kbind';
1942 val pr = pretty_haskell_monad c_mbind'' c_kbind''
1945 |> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr)
1946 |> gen_add_syntax_const (K I) target_Haskell c_mbind'
1947 (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
1948 |> gen_add_syntax_const (K I) target_Haskell c_kbind'
1949 (no_bindings (SOME (parse_infix fst (L, 1) ">>")))
1952 fun add_reserved target =
1954 fun add sym syms = if member (op =) syms sym
1955 then error ("Reserved symbol " ^ quote sym ^ " already declared")
1956 else insert (op =) sym syms
1957 in map_reserveds target o add end;
1959 fun add_modl_alias target =
1960 map_syntax_modls target o apfst o Symtab.update o apsnd CodeName.check_modulename;
1962 fun add_modl_prolog target =
1963 map_syntax_modls target o apsnd o
1964 (fn (modl, NONE) => Symtab.delete modl | (modl, SOME prolog) =>
1965 Symtab.update (modl, Pretty.str prolog));
1967 fun gen_allow_exception prep_cs raw_c thy =
1969 val c = prep_cs thy raw_c;
1970 val c' = CodeName.const thy c;
1971 in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
1973 fun zip_list (x::xs) f g =
1976 fold_map (fn x => g |-- f >> pair x) xs
1977 #-> (fn xys => pair ((x, y) :: xys)));
1979 structure P = OuterParse
1980 and K = OuterKeyword
1982 fun parse_multi_syntax parse_thing parse_syntax =
1983 P.and_list1 parse_thing
1984 #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
1985 (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
1987 val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
1989 fun parse_syntax prep_arg xs =
1991 ((P.$$$ infixK >> K X)
1992 || (P.$$$ infixlK >> K L)
1993 || (P.$$$ infixrK >> K R))
1994 -- P.nat >> parse_infix prep_arg
1995 || Scan.succeed (parse_mixfix prep_arg))
1997 >> (fn (parse, s) => parse s)) xs;
1999 val (code_classK, code_instanceK, code_typeK, code_constK, code_monadK,
2000 code_reservedK, code_modulenameK, code_moduleprologK, code_exceptionK) =
2001 ("code_class", "code_instance", "code_type", "code_const", "code_monad",
2002 "code_reserved", "code_modulename", "code_moduleprolog", "code_exception");
2006 val parse_syntax = parse_syntax;
2008 val add_syntax_class = gen_add_syntax_class cert_class (K I);
2009 val add_syntax_inst = gen_add_syntax_inst cert_class cert_tyco;
2010 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
2011 val add_syntax_const = gen_add_syntax_const (K I);
2012 val allow_exception = gen_allow_exception (K I);
2014 val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
2015 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
2016 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
2017 val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
2018 val allow_exception_cmd = gen_allow_exception CodeUnit.read_const;
2020 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
2021 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
2023 fun add_undefined target undef target_undefined thy =
2025 fun pr _ _ _ _ = str target_undefined;
2028 |> add_syntax_const target undef (SOME (~1, pr))
2031 fun add_pretty_list target nill cons thy =
2033 val nil' = CodeName.const thy nill;
2034 val cons' = CodeName.const thy cons;
2035 val pr = pretty_list nil' cons' target;
2038 |> add_syntax_const target cons (SOME pr)
2041 fun add_pretty_list_string target nill cons charr nibbles thy =
2043 val nil' = CodeName.const thy nill;
2044 val cons' = CodeName.const thy cons;
2045 val charr' = CodeName.const thy charr;
2046 val nibbles' = map (CodeName.const thy) nibbles;
2047 val pr = pretty_list_string nil' cons' charr' nibbles' target;
2050 |> add_syntax_const target cons (SOME pr)
2053 fun add_pretty_char target charr nibbles thy =
2055 val charr' = CodeName.const thy charr;
2056 val nibbles' = map (CodeName.const thy) nibbles;
2057 val pr = pretty_char charr' nibbles' target;
2060 |> add_syntax_const target charr (SOME pr)
2063 fun add_pretty_numeral target unbounded number_of b0 b1 pls min bit thy =
2065 val b0' = CodeName.const thy b0;
2066 val b1' = CodeName.const thy b1;
2067 val pls' = CodeName.const thy pls;
2068 val min' = CodeName.const thy min;
2069 val bit' = CodeName.const thy bit;
2070 val pr = pretty_numeral unbounded b0' b1' pls' min' bit' target;
2073 |> add_syntax_const target number_of (SOME pr)
2076 fun add_pretty_ml_string target charr nibbles nill cons str thy =
2078 val charr' = CodeName.const thy charr;
2079 val nibbles' = map (CodeName.const thy) nibbles;
2080 val nil' = CodeName.const thy nill;
2081 val cons' = CodeName.const thy cons;
2082 val pr = pretty_ml_string charr' nibbles' nil' cons' target;
2085 |> add_syntax_const target str (SOME pr)
2088 fun add_pretty_imperative_monad_bind target bind thy =
2089 add_syntax_const target bind (SOME (pretty_imperative_monad_bind
2090 (CodeName.const thy bind))) thy;
2092 val add_haskell_monad = gen_add_haskell_monad CodeUnit.read_const;
2095 val _ = OuterSyntax.keywords [infixK, infixlK, infixrK];
2098 OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
2099 parse_multi_syntax P.xname
2100 (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
2101 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) []))
2102 >> (Toplevel.theory oo fold) (fn (target, syns) =>
2103 fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
2107 OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
2108 parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
2109 ((P.minus >> K true) || Scan.succeed false)
2110 >> (Toplevel.theory oo fold) (fn (target, syns) =>
2111 fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
2115 OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
2116 parse_multi_syntax P.xname (parse_syntax I)
2117 >> (Toplevel.theory oo fold) (fn (target, syns) =>
2118 fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
2122 OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
2123 parse_multi_syntax P.term (parse_syntax fst)
2124 >> (Toplevel.theory oo fold) (fn (target, syns) =>
2125 fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
2129 OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl (
2130 P.term -- P.term -- P.term
2131 >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory
2132 (add_haskell_monad raw_run raw_mbind raw_kbind))
2136 OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl (
2137 P.name -- Scan.repeat1 P.name
2138 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
2142 OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
2143 P.name -- Scan.repeat1 (P.name -- P.name)
2144 >> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
2148 OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
2149 P.name -- Scan.repeat1 (P.name -- (P.text >> (fn "-" => NONE | s => SOME s)))
2150 >> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
2154 OuterSyntax.command code_exceptionK "permit exceptions for constant" K.thy_decl (
2155 Scan.repeat1 P.term >> (Toplevel.theory o fold allow_exception_cmd)
2159 (*including serializer defaults*)
2161 add_serializer (target_SML, isar_seri_sml)
2162 #> add_serializer (target_OCaml, isar_seri_ocaml)
2163 #> add_serializer (target_Haskell, isar_seri_haskell)
2164 #> add_serializer (target_diag, fn _=> fn _ => fn _ => seri_diagnosis)
2165 #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
2166 (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
2167 pr_typ (INFX (1, X)) ty1,
2169 pr_typ (INFX (1, R)) ty2
2171 #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
2172 (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
2173 pr_typ (INFX (1, X)) ty1,
2175 pr_typ (INFX (1, R)) ty2
2177 #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
2178 brackify_infix (1, R) fxy [
2179 pr_typ (INFX (1, X)) ty1,
2181 pr_typ (INFX (1, R)) ty2
2183 #> fold (add_reserved "SML") ML_Syntax.reserved_names
2184 #> fold (add_reserved "SML")
2185 ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
2186 #> fold (add_reserved "OCaml") [
2187 "and", "as", "assert", "begin", "class",
2188 "constraint", "do", "done", "downto", "else", "end", "exception",
2189 "external", "false", "for", "fun", "function", "functor", "if",
2190 "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
2191 "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
2192 "sig", "struct", "then", "to", "true", "try", "type", "val",
2193 "virtual", "when", "while", "with"
2195 #> fold (add_reserved "OCaml") ["failwith", "mod"]
2196 #> fold (add_reserved "Haskell") [
2197 "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
2198 "import", "default", "forall", "let", "in", "class", "qualified", "data",
2199 "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
2201 #> fold (add_reserved "Haskell") [
2202 "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
2203 "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
2204 "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
2205 "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
2206 "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
2207 "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
2208 "ExitSuccess", "False", "GT", "HeapOverflow",
2209 "IOError", "IOException", "IllegalOperation",
2210 "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
2211 "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
2212 "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
2213 "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
2214 "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
2215 "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
2216 "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
2217 "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
2218 "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
2219 "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
2220 "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
2221 "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
2222 "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
2223 "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
2224 "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
2225 "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
2226 "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
2227 "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
2228 "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
2229 "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
2230 "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
2231 "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
2232 "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
2233 "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
2234 "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
2235 "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
2236 "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
2237 "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
2238 "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
2239 "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
2240 "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
2241 "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
2242 "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
2243 "sequence_", "show", "showChar", "showException", "showField", "showList",
2244 "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
2245 "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
2246 "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
2247 "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
2248 "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
2249 "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
2250 ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);