1 (* Title: Tools/Code/code_ml.ML
2 Author: Florian Haftmann, TU Muenchen
4 Serializer for SML and OCaml.
10 val target_OCaml: string
11 val evaluation_code_of: theory -> string -> string
12 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
13 val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
14 -> Code_Printer.fixity -> 'a list -> Pretty.T option
15 val setup: theory -> theory
18 structure Code_ML : CODE_ML =
21 open Basic_Code_Thingol;
30 val target_SML = "SML";
31 val target_OCaml = "OCaml";
34 ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
35 | ML_Instance of string * ((class * (string * (vname * sort) list))
36 * ((class * (string * (string * dict list list))) list
37 * (((string * const) * (thm * bool)) list * ((string * const) * (thm * bool)) list)));
40 ML_Exc of string * (typscheme * int)
41 | ML_Val of ml_binding
42 | ML_Funs of ml_binding list * string list
43 | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
44 | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
46 fun stmt_name_of_binding (ML_Function (name, _)) = name
47 | stmt_name_of_binding (ML_Instance (name, _)) = name;
49 fun stmt_names_of (ML_Exc (name, _)) = [name]
50 | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]
51 | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings
52 | stmt_names_of (ML_Datas ds) = map fst ds
53 | stmt_names_of (ML_Class (name, _)) = [name];
55 fun print_product _ [] = NONE
56 | print_product print [x] = SOME (print x)
57 | print_product print xs = (SOME o enum " *" "" "") (map print xs);
59 fun print_tuple _ _ [] = NONE
60 | print_tuple print fxy [x] = SOME (print fxy x)
61 | print_tuple print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
64 (** SML serializer **)
66 fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
68 fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
69 | print_tyco_expr fxy (tyco, [ty]) =
70 concat [print_typ BR ty, (str o deresolve) tyco]
71 | print_tyco_expr fxy (tyco, tys) =
72 concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
73 and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
74 of NONE => print_tyco_expr fxy (tyco, tys)
75 | SOME (i, print) => print print_typ fxy tys)
76 | print_typ fxy (ITyVar v) = str ("'" ^ v);
77 fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
78 fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
79 (map_filter (fn (v, sort) =>
80 (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
81 fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
82 fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
83 fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
84 brackify fxy ((str o deresolve) inst ::
85 (if is_pseudo_fun inst then [str "()"]
86 else map_filter (print_dicts is_pseudo_fun BR) dss))
87 | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
89 val v_p = str (if k = 1 then first_upper v ^ "_"
90 else first_upper v ^ string_of_int (i+1) ^ "_");
93 | [classrel] => brackets [(str o deresolve) classrel, v_p]
94 | classrels => brackets
95 [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
97 and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
98 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
99 (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
100 fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
101 print_app is_pseudo_fun some_thm vars fxy (c, [])
102 | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
104 | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
105 str (lookup_var vars v)
106 | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
107 (case Code_Thingol.unfold_const_app t
108 of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
109 | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
110 print_term is_pseudo_fun some_thm vars BR t2])
111 | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
113 val (binds, t') = Code_Thingol.unfold_pat_abs t;
114 fun print_abs (pat, ty) =
115 print_bind is_pseudo_fun some_thm NOBR pat
116 #>> (fn p => concat [str "fn", p, str "=>"]);
117 val (ps, vars') = fold_map print_abs binds vars;
118 in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
119 | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
120 (case Code_Thingol.unfold_const_app t0
121 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
122 then print_case is_pseudo_fun some_thm vars fxy cases
123 else print_app is_pseudo_fun some_thm vars fxy c_ts
124 | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
125 and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
127 let val k = length function_typs in
128 if k < 2 orelse length ts = k
129 then (str o deresolve) c
130 :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
131 else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
133 else if is_pseudo_fun c
134 then (str o deresolve) c @@ str "()"
135 else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
136 @ map (print_term is_pseudo_fun some_thm vars BR) ts
137 and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
138 (print_term is_pseudo_fun) syntax_const some_thm vars
139 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
140 and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
142 val (binds, body) = Code_Thingol.unfold_let (ICase cases);
143 fun print_match ((pat, ty), t) vars =
145 |> print_bind is_pseudo_fun some_thm NOBR pat
146 |>> (fn p => semicolon [str "val", p, str "=",
147 print_term is_pseudo_fun some_thm vars NOBR t])
148 val (ps, vars') = fold_map print_match binds vars;
151 Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
152 Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
156 | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
158 fun print_select delim (pat, body) =
160 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
162 concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
167 :: print_term is_pseudo_fun some_thm vars NOBR t
168 :: print_select "of" clause
169 :: map (print_select "|") clauses
172 | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
173 (concat o map str) ["raise", "Fail", "\"empty case\""];
174 fun print_val_decl print_typscheme (name, typscheme) = concat
175 [str "val", str (deresolve name), str ":", print_typscheme typscheme];
176 fun print_datatype_decl definer (tyco, (vs, cos)) =
178 fun print_co ((co, _), []) = str (deresolve co)
179 | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
180 enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
184 :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
186 :: separate (str "|") (map print_co cos)
189 fun print_def is_pseudo_fun needs_typ definer
190 (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
192 fun print_eqn definer ((ts, t), (some_thm, _)) =
194 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
197 (is_none o syntax_const) deresolve consts
198 |> intro_vars ((fold o Code_Thingol.fold_varnames)
199 (insert (op =)) ts []);
200 val prolog = if needs_typ then
201 concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
202 else (concat o map str) [definer, deresolve name];
206 :: (if is_pseudo_fun name then [str "()"]
207 else print_dict_args vs
208 @ map (print_term is_pseudo_fun some_thm vars BR) ts)
210 @@ print_term is_pseudo_fun some_thm vars NOBR t
213 val shift = if null eqs then I else
214 map (Pretty.block o single o Pretty.block o single);
216 (print_val_decl print_typscheme (name, vs_ty))
217 ((Pretty.block o Pretty.fbreaks o shift) (
219 :: map (print_eqn "|") eqs
222 | print_def is_pseudo_fun _ definer
223 (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
225 fun print_super_instance (_, (classrel, dss)) =
227 (str o Long_Name.base_name o deresolve) classrel,
229 print_dict is_pseudo_fun NOBR (DictConst dss)
231 fun print_classparam_instance ((classparam, const), (thm, _)) =
233 (str o Long_Name.base_name o deresolve) classparam,
235 print_app (K false) (SOME thm) reserved NOBR (const, [])
238 (print_val_decl print_dicttypscheme
239 (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
242 :: (str o deresolve) inst
243 :: (if is_pseudo_fun inst then [str "()"]
244 else print_dict_args vs)
247 (map print_super_instance super_instances
248 @ map print_classparam_instance classparam_instances)
250 @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
253 fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
254 [print_val_decl print_typscheme (name, vs_ty)]
255 ((semicolon o map str) (
256 (if n = 0 then "val" else "fun")
262 @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
264 | print_stmt (ML_Val binding) =
266 val (sig_p, p) = print_def (K false) true "val" binding
271 | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
273 val print_def' = print_def (member (op =) pseudo_funs) false;
274 fun print_pseudo_fun name = concat [
276 (str o deresolve) name,
278 (str o deresolve) name,
281 val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
282 (print_def' "fun" binding :: map (print_def' "and") bindings);
283 val pseudo_ps = map print_pseudo_fun pseudo_funs;
286 (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
288 | print_stmt (ML_Datas [(tyco, (vs, []))]) =
290 val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
293 [concat [str "type", ty_p]]
294 (concat [str "datatype", ty_p, str "=", str "EMPTY__"])
296 | print_stmt (ML_Datas (data :: datas)) =
298 val sig_ps = print_datatype_decl "datatype" data
299 :: map (print_datatype_decl "and") datas;
300 val (ps, p) = split_last sig_ps;
303 (Pretty.chunks (ps @| semicolon [p]))
305 | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
307 fun print_field s p = concat [str s, str ":", p];
308 fun print_proj s p = semicolon
309 (map str ["val", s, "=", "#" ^ s, ":"] @| p);
310 fun print_super_class_decl (super_class, classrel) =
311 print_val_decl print_dicttypscheme
312 (classrel, ([(v, [class])], (super_class, ITyVar v)));
313 fun print_super_class_field (super_class, classrel) =
314 print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
315 fun print_super_class_proj (super_class, classrel) =
316 print_proj (deresolve classrel)
317 (print_dicttypscheme ([(v, [class])], (super_class, ITyVar v)));
318 fun print_classparam_decl (classparam, ty) =
319 print_val_decl print_typscheme
320 (classparam, ([(v, [class])], ty));
321 fun print_classparam_field (classparam, ty) =
322 print_field (deresolve classparam) (print_typ NOBR ty);
323 fun print_classparam_proj (classparam, ty) =
324 print_proj (deresolve classparam)
325 (print_typscheme ([(v, [class])], ty));
327 (concat [str "type", print_dicttyp (class, ITyVar v)]
328 :: map print_super_class_decl super_classes
329 @ map print_classparam_decl classparams)
333 (str o deresolve) class,
336 map print_super_class_field super_classes
337 @ map print_classparam_field classparams
340 :: map print_super_class_proj super_classes
341 @ map print_classparam_proj classparams
346 fun print_sml_module name some_decls body = if name = ""
347 then Pretty.chunks2 body
348 else Pretty.chunks2 (
350 str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
351 :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
352 @| (if is_some some_decls then str "end = struct" else str "struct")
355 @| str ("end; (*struct " ^ name ^ "*)")
358 val literals_sml = Literals {
359 literal_char = prefix "#" o quote o ML_Syntax.print_char,
360 literal_string = quote o translate_string ML_Syntax.print_char,
361 literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
362 literal_positive_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
363 literal_alternative_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
364 literal_naive_numeral = string_of_int,
365 literal_list = enum "," "[" "]",
366 infix_cons = (7, "::")
370 (** OCaml serializer **)
372 fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
374 fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
375 | print_tyco_expr fxy (tyco, [ty]) =
376 concat [print_typ BR ty, (str o deresolve) tyco]
377 | print_tyco_expr fxy (tyco, tys) =
378 concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
379 and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
380 of NONE => print_tyco_expr fxy (tyco, tys)
381 | SOME (i, print) => print print_typ fxy tys)
382 | print_typ fxy (ITyVar v) = str ("'" ^ v);
383 fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
384 fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
385 (map_filter (fn (v, sort) =>
386 (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
387 fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
388 fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
389 fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
390 brackify fxy ((str o deresolve) inst ::
391 (if is_pseudo_fun inst then [str "()"]
392 else map_filter (print_dicts is_pseudo_fun BR) dss))
393 | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
394 str (if k = 1 then "_" ^ first_upper v
395 else "_" ^ first_upper v ^ string_of_int (i+1))
396 |> fold_rev (fn classrel => fn p =>
397 Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
398 and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
399 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
400 (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
401 fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
402 print_app is_pseudo_fun some_thm vars fxy (c, [])
403 | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
405 | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
406 str (lookup_var vars v)
407 | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
408 (case Code_Thingol.unfold_const_app t
409 of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
410 | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
411 print_term is_pseudo_fun some_thm vars BR t2])
412 | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
414 val (binds, t') = Code_Thingol.unfold_pat_abs t;
415 val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
416 in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
417 | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
418 (case Code_Thingol.unfold_const_app t0
419 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
420 then print_case is_pseudo_fun some_thm vars fxy cases
421 else print_app is_pseudo_fun some_thm vars fxy c_ts
422 | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
423 and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
425 let val k = length tys in
427 then (str o deresolve) c
428 :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
429 else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
431 else if is_pseudo_fun c
432 then (str o deresolve) c @@ str "()"
433 else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
434 @ map (print_term is_pseudo_fun some_thm vars BR) ts
435 and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
436 (print_term is_pseudo_fun) syntax_const some_thm vars
437 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
438 and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
440 val (binds, body) = Code_Thingol.unfold_let (ICase cases);
441 fun print_let ((pat, ty), t) vars =
443 |> print_bind is_pseudo_fun some_thm NOBR pat
445 [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
446 val (ps, vars') = fold_map print_let binds vars;
448 brackify_block fxy (Pretty.chunks ps) []
449 (print_term is_pseudo_fun some_thm vars' NOBR body)
451 | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
453 fun print_select delim (pat, body) =
455 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
456 in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
460 :: print_term is_pseudo_fun some_thm vars NOBR t
461 :: print_select "with" clause
462 :: map (print_select "|") clauses
465 | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
466 (concat o map str) ["failwith", "\"empty case\""];
467 fun print_val_decl print_typscheme (name, typscheme) = concat
468 [str "val", str (deresolve name), str ":", print_typscheme typscheme];
469 fun print_datatype_decl definer (tyco, (vs, cos)) =
471 fun print_co ((co, _), []) = str (deresolve co)
472 | print_co ((co, _), tys) = concat [str (deresolve co), str "of",
473 enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
477 :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
479 :: separate (str "|") (map print_co cos)
482 fun print_def is_pseudo_fun needs_typ definer
483 (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
485 fun print_eqn ((ts, t), (some_thm, _)) =
487 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
489 |> intro_vars ((fold o Code_Thingol.fold_varnames)
490 (insert (op =)) ts []);
492 (Pretty.block o commas)
493 (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
495 print_term is_pseudo_fun some_thm vars NOBR t
497 fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
499 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
502 (is_none o syntax_const) deresolve consts
503 |> intro_vars ((fold o Code_Thingol.fold_varnames)
504 (insert (op =)) ts []);
507 (if is_pseudo then [str "()"]
508 else map (print_term is_pseudo_fun some_thm vars BR) ts)
510 @@ print_term is_pseudo_fun some_thm vars NOBR t
513 | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
520 :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
521 o single o print_eqn) eqs
523 | print_eqns _ (eqs as eq :: eqs') =
525 val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
528 (is_none o syntax_const) deresolve consts;
529 val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
532 Pretty.breaks dummy_parms
538 :: (Pretty.block o commas) dummy_parms
543 :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
544 o single o print_eqn) eqs'
547 val prolog = if needs_typ then
548 concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
549 else (concat o map str) [definer, deresolve name];
551 (print_val_decl print_typscheme (name, vs_ty))
554 :: print_dict_args vs
555 @| print_eqns (is_pseudo_fun name) eqs
558 | print_def is_pseudo_fun _ definer
559 (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
561 fun print_super_instance (_, (classrel, dss)) =
563 (str o deresolve) classrel,
565 print_dict is_pseudo_fun NOBR (DictConst dss)
567 fun print_classparam_instance ((classparam, const), (thm, _)) =
569 (str o deresolve) classparam,
571 print_app (K false) (SOME thm) reserved NOBR (const, [])
574 (print_val_decl print_dicttypscheme
575 (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
578 :: (str o deresolve) inst
579 :: print_dict_args vs
582 enum_default "()" ";" "{" "}" (map print_super_instance super_instances
583 @ map print_classparam_instance classparam_instances),
585 print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
589 fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
590 [print_val_decl print_typscheme (name, vs_ty)]
591 ((doublesemicolon o map str) (
597 @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
599 | print_stmt (ML_Val binding) =
601 val (sig_p, p) = print_def (K false) true "let" binding
604 (doublesemicolon [p])
606 | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
608 val print_def' = print_def (member (op =) pseudo_funs) false;
609 fun print_pseudo_fun name = concat [
611 (str o deresolve) name,
613 (str o deresolve) name,
616 val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
617 (print_def' "let rec" binding :: map (print_def' "and") bindings);
618 val pseudo_ps = map print_pseudo_fun pseudo_funs;
621 (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
623 | print_stmt (ML_Datas [(tyco, (vs, []))]) =
625 val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
628 [concat [str "type", ty_p]]
629 (concat [str "type", ty_p, str "=", str "EMPTY__"])
631 | print_stmt (ML_Datas (data :: datas)) =
633 val sig_ps = print_datatype_decl "type" data
634 :: map (print_datatype_decl "and") datas;
635 val (ps, p) = split_last sig_ps;
638 (Pretty.chunks (ps @| doublesemicolon [p]))
640 | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
642 fun print_field s p = concat [str s, str ":", p];
643 fun print_super_class_field (super_class, classrel) =
644 print_field (deresolve classrel) (print_dicttyp (super_class, ITyVar v));
645 fun print_classparam_decl (classparam, ty) =
646 print_val_decl print_typscheme
647 (classparam, ([(v, [class])], ty));
648 fun print_classparam_field (classparam, ty) =
649 print_field (deresolve classparam) (print_typ NOBR ty);
650 val w = "_" ^ first_upper v;
651 fun print_classparam_proj (classparam, _) =
652 (concat o map str) ["let", deresolve classparam, w, "=",
653 w ^ "." ^ deresolve classparam ^ ";;"];
654 val type_decl_p = concat [
656 (str o deresolve) class,
658 enum_default "unit" ";" "{" "}" (
659 map print_super_class_field super_classes
660 @ map print_classparam_field classparams
664 (type_decl_p :: map print_classparam_decl classparams)
666 doublesemicolon [type_decl_p]
667 :: map print_classparam_proj classparams
672 fun print_ocaml_module name some_decls body = if name = ""
673 then Pretty.chunks2 body
674 else Pretty.chunks2 (
676 str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
677 :: (the_list o Option.map (indent 2 o Pretty.chunks)) some_decls
678 @| (if is_some some_decls then str "end = struct" else str "struct")
681 @| str ("end;; (*struct " ^ name ^ "*)")
684 val literals_ocaml = let
687 val xs = string_of_int i;
688 val ys = replicate_string (3 - length (explode xs)) "0";
689 in "\\" ^ ys ^ xs end;
693 val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
696 fun numeral_ocaml k = if k < 0
697 then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
698 else if k <= 1073741823
699 then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
700 else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
702 literal_char = Library.enclose "'" "'" o char_ocaml,
703 literal_string = quote o translate_string char_ocaml,
704 literal_numeral = numeral_ocaml,
705 literal_positive_numeral = numeral_ocaml,
706 literal_alternative_numeral = numeral_ocaml,
707 literal_naive_numeral = numeral_ocaml,
708 literal_list = enum ";" "[" "]",
709 infix_cons = (6, "::")
714 (** SML/OCaml generic part **)
720 | Stmt of string * ml_stmt
721 | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
725 fun ml_node_of_program labelled_name module_name reserved module_alias program =
727 val reserved = Name.make_context reserved;
728 val empty_module = ((reserved, reserved), Graph.empty);
729 fun map_node [] f = f
730 | map_node (m::ms) f =
731 Graph.default_node (m, Module (m, empty_module))
732 #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
733 Module (module_name, (nsp, map_node ms f nodes)));
734 fun map_nsp_yield [] f (nsp, nodes) =
736 val (x, nsp') = f nsp
737 in (x, (nsp', nodes)) end
738 | map_nsp_yield (m::ms) f (nsp, nodes) =
742 |> Graph.default_node (m, Module (m, empty_module))
743 |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) =>
745 val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
746 in (x, Module (d_module_name, nsp_nodes')) end)
747 in (x, (nsp, nodes')) end;
748 fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
750 val (x, nsp_fun') = f nsp_fun
751 in (x, (nsp_fun', nsp_typ)) end;
752 fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
754 val (x, nsp_typ') = f nsp_typ
755 in (x, (nsp_fun, nsp_typ')) end;
756 val mk_name_module = mk_name_module reserved NONE module_alias program;
757 fun mk_name_stmt upper name nsp =
759 val (_, base) = dest_name name;
760 val base' = if upper then first_upper base else base;
761 val ([base''], nsp') = Name.variants [base'] nsp;
762 in (base'', nsp') end;
765 |> fold (fold (insert (op =)) o Graph.imm_succs program) names
766 |> subtract (op =) names
767 |> filter_out (Code_Thingol.is_case o Graph.get_node program);
768 fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, ((tysm as (vs, ty), raw_eqs), _))) =
770 val eqs = filter (snd o snd) raw_eqs;
771 val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
772 of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
773 then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
774 else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
777 in (ML_Function (name, (tysm, eqs')), is_value) end
778 | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
779 (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
780 | ml_binding_of_stmt (name, _) =
781 error ("Binding block containing illegal statement: " ^ labelled_name name)
782 fun add_fun (name, stmt) =
784 val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
785 val ml_stmt = case binding
786 of ML_Function (name, ((vs, ty), [])) =>
787 ML_Exc (name, ((vs, ty),
788 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
789 | _ => case some_value_name
790 of NONE => ML_Funs ([binding], [])
791 | SOME (name, true) => ML_Funs ([binding], [name])
792 | SOME (name, false) => ML_Val binding
794 map_nsp_fun_yield (mk_name_stmt false name)
795 #>> (fn name' => ([name'], ml_stmt))
799 val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
801 fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
804 fun add_datatypes stmts =
806 (fn (name, Code_Thingol.Datatype (_, stmt)) =>
807 map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
808 | (name, Code_Thingol.Datatypecons _) =>
809 map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
811 error ("Datatype block containing illegal statement: " ^ labelled_name name)
813 #>> (split_list #> apsnd (map_filter I
814 #> (fn [] => error ("Datatype block without data statement: "
815 ^ (Library.commas o map (labelled_name o fst)) stmts)
816 | stmts => ML_Datas stmts)));
817 fun add_class stmts =
819 (fn (name, Code_Thingol.Class (_, stmt)) =>
820 map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
821 | (name, Code_Thingol.Classrel _) =>
822 map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
823 | (name, Code_Thingol.Classparam _) =>
824 map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
826 error ("Class block containing illegal statement: " ^ labelled_name name)
828 #>> (split_list #> apsnd (map_filter I
829 #> (fn [] => error ("Class block without class statement: "
830 ^ (Library.commas o map (labelled_name o fst)) stmts)
831 | [stmt] => ML_Class stmt)));
832 fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
834 | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
836 | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
838 | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
840 | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
842 | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
844 | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
846 | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
848 | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
850 | add_stmts stmts = error ("Illegal mutual dependencies: " ^
851 (Library.commas o map (labelled_name o fst)) stmts);
852 fun add_stmts' stmts nsp_nodes =
854 val names as (name :: names') = map fst stmts;
855 val deps = deps_of names;
856 val (module_names, _) = (split_list o map dest_name) names;
857 val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
859 error ("Different namespace prefixes for mutual dependencies:\n"
860 ^ Library.commas (map labelled_name names)
862 ^ Library.commas module_names);
863 val module_name_path = Long_Name.explode module_name;
864 fun add_dep name name' =
866 val module_name' = (mk_name_module o fst o dest_name) name';
867 in if module_name = module_name' then
868 map_node module_name_path (Graph.add_edge (name, name'))
870 val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
871 (module_name_path, Long_Name.explode module_name');
874 (fn node => Graph.add_edge_acyclic (diff1, diff2) node
875 handle Graph.CYCLES _ => error ("Dependency "
876 ^ quote name ^ " -> " ^ quote name'
877 ^ " would result in module dependency cycle"))
881 |> map_nsp_yield module_name_path (add_stmts stmts)
882 |-> (fn (base' :: bases', stmt') =>
883 apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
884 #> fold2 (fn name' => fn base' =>
885 Graph.new_node (name', (Dummy base'))) names' bases')))
886 |> apsnd (fold (fn name => fold (add_dep name) deps) names)
887 |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
889 val stmts = map (AList.make (Graph.get_node program)) (rev (Graph.strong_conn program))
890 |> filter_out (fn [(_, stmt)] => Code_Thingol.is_case stmt | _ => false);
891 val (_, nodes) = fold add_stmts' stmts empty_module;
892 fun deresolver prefix name =
894 val module_name = (fst o dest_name) name;
895 val module_name' = (Long_Name.explode o mk_name_module) module_name;
896 val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
899 |> fold (fn name => fn node => case Graph.get_node node name
900 of Module (_, (_, node)) => node) module_name'
901 |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
902 | Dummy stmt_name => stmt_name);
904 Long_Name.implode (remainder @ [stmt_name])
905 end handle Graph.UNDEF _ =>
906 error ("Unknown statement name: " ^ labelled_name name);
907 in (deresolver, nodes) end;
909 fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
910 reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
911 (stmt_names, presentation_stmt_names) =
913 val is_cons = Code_Thingol.is_cons program;
914 val is_presentation = not (null presentation_stmt_names);
915 val (deresolver, nodes) = ml_node_of_program labelled_name module_name
916 reserved module_alias program;
917 val reserved = make_vars reserved;
918 fun print_node prefix (Dummy _) =
920 | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
921 (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
923 else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt)
924 | print_node prefix (Module (module_name, (_, nodes))) =
926 val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
927 val p = if is_presentation then Pretty.chunks2 body
928 else print_module module_name (if with_signatures then SOME decls else NONE) body;
930 and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
931 o rev o flat o Graph.strong_conn) nodes
933 |> (fn (decls, body) => (flat decls, body))
934 val stmt_names' = (map o try)
935 (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
936 val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
938 Code_Target.mk_serialization target
939 (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
940 (rpair stmt_names' o code_of_pretty) p
946 (** for instrumentalization **)
948 fun evaluation_code_of thy target struct_name =
949 Code_Target.serialize_custom thy (target, fn module_name => fn [] =>
950 serialize_ml target print_sml_module print_sml_stmt module_name true) (SOME struct_name);
955 fun isar_serializer_sml module_name =
956 Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
957 >> (fn with_signatures => serialize_ml target_SML
958 print_sml_module print_sml_stmt module_name with_signatures));
960 fun isar_serializer_ocaml module_name =
961 Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
962 >> (fn with_signatures => serialize_ml target_OCaml
963 print_ocaml_module print_ocaml_stmt module_name with_signatures));
966 Code_Target.add_target
967 (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
968 check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
969 make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } })
970 #> Code_Target.add_target
971 (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
972 check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
973 make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } })
974 #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
975 brackify_infix (1, R) fxy (
976 print_typ (INFX (1, X)) ty1,
978 print_typ (INFX (1, R)) ty2
980 #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
981 brackify_infix (1, R) fxy (
982 print_typ (INFX (1, X)) ty1,
984 print_typ (INFX (1, R)) ty2
986 #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
987 #> fold (Code_Target.add_reserved target_SML)
988 ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
989 "Fail", "div", "mod" (*standard infixes*), "IntInf"]
990 #> fold (Code_Target.add_reserved target_OCaml) [
991 "and", "as", "assert", "begin", "class",
992 "constraint", "do", "done", "downto", "else", "end", "exception",
993 "external", "false", "for", "fun", "function", "functor", "if",
994 "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
995 "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
996 "sig", "struct", "then", "to", "true", "try", "type", "val",
997 "virtual", "when", "while", "with"
999 #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod", "Big_int"];