src/Tools/Code/code_ml.ML
author haftmann
Fri Dec 04 18:19:32 2009 +0100 (2009-12-04)
changeset 33992 bf22ff4f3d19
parent 33636 a9bb3f063773
child 34028 1e6206763036
permissions -rw-r--r--
signatures for generated code; tuned
     1 (*  Title:      Tools/code/code_ml.ML_
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Serializer for SML and OCaml.
     5 *)
     6 
     7 signature CODE_ML =
     8 sig
     9   val eval: string option -> string * (unit -> 'a) option Unsynchronized.ref
    10     -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    11   val target_Eval: string
    12   val setup: theory -> theory
    13 end;
    14 
    15 structure Code_ML : CODE_ML =
    16 struct
    17 
    18 open Basic_Code_Thingol;
    19 open Code_Printer;
    20 
    21 infixr 5 @@;
    22 infixr 5 @|;
    23 
    24 
    25 (** generic **)
    26 
    27 val target_SML = "SML";
    28 val target_OCaml = "OCaml";
    29 val target_Eval = "Eval";
    30 
    31 datatype ml_binding =
    32     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
    33   | ML_Instance of string * ((class * (string * (vname * sort) list))
    34         * ((class * (string * (string * dict list list))) list
    35       * ((string * const) * (thm * bool)) list));
    36 
    37 datatype ml_stmt =
    38     ML_Exc of string * (typscheme * int)
    39   | ML_Val of ml_binding
    40   | ML_Funs of ml_binding list * string list
    41   | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
    42   | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
    43 
    44 fun stmt_name_of_binding (ML_Function (name, _)) = name
    45   | stmt_name_of_binding (ML_Instance (name, _)) = name;
    46 
    47 fun stmt_names_of (ML_Exc (name, _)) = [name]
    48   | stmt_names_of (ML_Val binding) = [stmt_name_of_binding binding]
    49   | stmt_names_of (ML_Funs (bindings, _)) = map stmt_name_of_binding bindings
    50   | stmt_names_of (ML_Datas ds) = map fst ds
    51   | stmt_names_of (ML_Class (name, _)) = [name];
    52 
    53 fun print_product _ [] = NONE
    54   | print_product print [x] = SOME (print x)
    55   | print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs);
    56 
    57 fun print_tuple _ _ [] = NONE
    58   | print_tuple print fxy [x] = SOME (print fxy x)
    59   | print_tuple print _ xs = SOME (Pretty.list "(" ")" (map (print NOBR) xs));
    60 
    61 
    62 (** SML serializer **)
    63 
    64 fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
    65   let
    66     fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    67       | print_tyco_expr fxy (tyco, [ty]) =
    68           concat [print_typ BR ty, (str o deresolve) tyco]
    69       | print_tyco_expr fxy (tyco, tys) =
    70           concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    71     and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
    72          of NONE => print_tyco_expr fxy (tyco, tys)
    73           | SOME (i, print) => print print_typ fxy tys)
    74       | print_typ fxy (ITyVar v) = str ("'" ^ v);
    75     fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    76     fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" ""
    77       (map_filter (fn (v, sort) =>
    78         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    79     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
    80     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    81     fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
    82           brackify fxy ((str o deresolve) inst ::
    83             (if is_pseudo_fun inst then [str "()"]
    84             else map_filter (print_dicts is_pseudo_fun BR) dss))
    85       | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
    86           let
    87             val v_p = str (if k = 1 then first_upper v ^ "_"
    88               else first_upper v ^ string_of_int (i+1) ^ "_");
    89           in case classrels
    90            of [] => v_p
    91             | [classrel] => brackets [(str o deresolve) classrel, v_p]
    92             | classrels => brackets
    93                 [Pretty.enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
    94           end
    95     and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
    96     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    97       (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    98     fun print_term is_pseudo_fun thm vars fxy (IConst c) =
    99           print_app is_pseudo_fun thm vars fxy (c, [])
   100       | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
   101           str "_"
   102       | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   103           str (lookup_var vars v)
   104       | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
   105           (case Code_Thingol.unfold_const_app t
   106            of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
   107             | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
   108                 print_term is_pseudo_fun thm vars BR t2])
   109       | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
   110           let
   111             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   112             fun print_abs (pat, ty) =
   113               print_bind is_pseudo_fun thm NOBR pat
   114               #>> (fn p => concat [str "fn", p, str "=>"]);
   115             val (ps, vars') = fold_map print_abs binds vars;
   116           in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end
   117       | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
   118           (case Code_Thingol.unfold_const_app t0
   119            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   120                 then print_case is_pseudo_fun thm vars fxy cases
   121                 else print_app is_pseudo_fun thm vars fxy c_ts
   122             | NONE => print_case is_pseudo_fun thm vars fxy cases)
   123     and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
   124       if is_cons c then
   125         let val k = length tys in
   126           if k < 2 orelse length ts = k
   127           then (str o deresolve) c
   128             :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
   129           else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
   130         end
   131       else if is_pseudo_fun c
   132         then (str o deresolve) c @@ str "()"
   133       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   134         @ map (print_term is_pseudo_fun thm vars BR) ts
   135     and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   136       (print_term is_pseudo_fun) syntax_const thm vars
   137     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   138     and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
   139           let
   140             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   141             fun print_match ((pat, ty), t) vars =
   142               vars
   143               |> print_bind is_pseudo_fun thm NOBR pat
   144               |>> (fn p => semicolon [str "val", p, str "=",
   145                     print_term is_pseudo_fun thm vars NOBR t])
   146             val (ps, vars') = fold_map print_match binds vars;
   147           in
   148             Pretty.chunks [
   149               Pretty.block [str ("let"), Pretty.fbrk, Pretty.chunks ps],
   150               Pretty.block [str ("in"), Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body],
   151               str ("end")
   152             ]
   153           end
   154       | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
   155           let
   156             fun print_select delim (pat, body) =
   157               let
   158                 val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
   159               in
   160                 concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body]
   161               end;
   162           in
   163             brackets (
   164               str "case"
   165               :: print_term is_pseudo_fun thm vars NOBR t
   166               :: print_select "of" clause
   167               :: map (print_select "|") clauses
   168             )
   169           end
   170       | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
   171           (concat o map str) ["raise", "Fail", "\"empty case\""];
   172     fun print_val_decl print_typscheme (name, typscheme) = concat
   173       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   174     fun print_datatype_decl definer (tyco, (vs, cos)) =
   175       let
   176         fun print_co (co, []) = str (deresolve co)
   177           | print_co (co, tys) = concat [str (deresolve co), str "of",
   178               Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   179       in
   180         concat (
   181           str definer
   182           :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
   183           :: str "="
   184           :: separate (str "|") (map print_co cos)
   185         )
   186       end;
   187     fun print_def is_pseudo_fun needs_typ definer
   188           (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
   189           let
   190             fun print_eqn definer ((ts, t), (thm, _)) =
   191               let
   192                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   193                 val vars = reserved
   194                   |> intro_base_names
   195                        (is_none o syntax_const) deresolve consts
   196                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   197                        (insert (op =)) ts []);
   198                 val prolog = if needs_typ then
   199                   concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   200                     else Pretty.strs [definer, deresolve name];
   201               in
   202                 concat (
   203                   prolog
   204                   :: (if is_pseudo_fun name then [str "()"]
   205                       else print_dict_args vs
   206                         @ map (print_term is_pseudo_fun thm vars BR) ts)
   207                   @ str "="
   208                   @@ print_term is_pseudo_fun thm vars NOBR t
   209                 )
   210               end
   211             val shift = if null eqs then I else
   212               map (Pretty.block o single o Pretty.block o single);
   213           in pair
   214             (print_val_decl print_typscheme (name, vs_ty))
   215             ((Pretty.block o Pretty.fbreaks o shift) (
   216               print_eqn definer eq
   217               :: map (print_eqn "|") eqs
   218             ))
   219           end
   220       | print_def is_pseudo_fun _ definer
   221           (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
   222           let
   223             fun print_superinst (_, (classrel, dss)) =
   224               concat [
   225                 (str o Long_Name.base_name o deresolve) classrel,
   226                 str "=",
   227                 print_dict is_pseudo_fun NOBR (DictConst dss)
   228               ];
   229             fun print_classparam ((classparam, c_inst), (thm, _)) =
   230               concat [
   231                 (str o Long_Name.base_name o deresolve) classparam,
   232                 str "=",
   233                 print_app (K false) thm reserved NOBR (c_inst, [])
   234               ];
   235           in pair
   236             (print_val_decl print_dicttypscheme
   237               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   238             (concat (
   239               str definer
   240               :: (str o deresolve) inst
   241               :: (if is_pseudo_fun inst then [str "()"]
   242                   else print_dict_args vs)
   243               @ str "="
   244               :: Pretty.list "{" "}"
   245                 (map print_superinst superinsts @ map print_classparam classparams)
   246               :: str ":"
   247               @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   248             ))
   249           end;
   250     fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   251           [print_val_decl print_typscheme (name, vs_ty)]
   252           ((semicolon o map str) (
   253             (if n = 0 then "val" else "fun")
   254             :: deresolve name
   255             :: replicate n "_"
   256             @ "="
   257             :: "raise"
   258             :: "Fail"
   259             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   260           ))
   261       | print_stmt (ML_Val binding) =
   262           let
   263             val (sig_p, p) = print_def (K false) true "val" binding
   264           in pair
   265             [sig_p]
   266             (semicolon [p])
   267           end
   268       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   269           let
   270             val print_def' = print_def (member (op =) pseudo_funs) false;
   271             fun print_pseudo_fun name = concat [
   272                 str "val",
   273                 (str o deresolve) name,
   274                 str "=",
   275                 (str o deresolve) name,
   276                 str "();"
   277               ];
   278             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   279               (print_def' "fun" binding :: map (print_def' "and") bindings);
   280             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   281           in pair
   282             sig_ps
   283             (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps))
   284           end
   285      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   286           let
   287             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   288           in
   289             pair
   290             [concat [str "type", ty_p]]
   291             (concat [str "datatype", ty_p, str "=", str "EMPTY__"])
   292           end
   293      | print_stmt (ML_Datas (data :: datas)) = 
   294           let
   295             val sig_ps = print_datatype_decl "datatype" data
   296               :: map (print_datatype_decl "and") datas;
   297             val (ps, p) = split_last sig_ps;
   298           in pair
   299             sig_ps
   300             (Pretty.chunks (ps @| semicolon [p]))
   301           end
   302      | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
   303           let
   304             fun print_field s p = concat [str s, str ":", p];
   305             fun print_proj s p = semicolon
   306               (map str ["val", s, "=", "#" ^ s, ":"] @| p);
   307             fun print_superclass_decl (superclass, classrel) =
   308               print_val_decl print_dicttypscheme
   309                 (classrel, ([(v, [class])], (superclass, ITyVar v)));
   310             fun print_superclass_field (superclass, classrel) =
   311               print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
   312             fun print_superclass_proj (superclass, classrel) =
   313               print_proj (deresolve classrel)
   314                 (print_dicttypscheme ([(v, [class])], (superclass, ITyVar v)));
   315             fun print_classparam_decl (classparam, ty) =
   316               print_val_decl print_typscheme
   317                 (classparam, ([(v, [class])], ty));
   318             fun print_classparam_field (classparam, ty) =
   319               print_field (deresolve classparam) (print_typ NOBR ty);
   320             fun print_classparam_proj (classparam, ty) =
   321               print_proj (deresolve classparam)
   322                 (print_typscheme ([(v, [class])], ty));
   323           in pair
   324             (concat [str "type", print_dicttyp (class, ITyVar v)]
   325               :: map print_superclass_decl superclasses
   326               @ map print_classparam_decl classparams)
   327             (Pretty.chunks (
   328               concat [
   329                 str ("type '" ^ v),
   330                 (str o deresolve) class,
   331                 str "=",
   332                 Pretty.list "{" "};" (
   333                   map print_superclass_field superclasses
   334                   @ map print_classparam_field classparams
   335                 )
   336               ]
   337               :: map print_superclass_proj superclasses
   338               @ map print_classparam_proj classparams
   339             ))
   340           end;
   341   in print_stmt end;
   342 
   343 fun print_sml_module name some_decls body = Pretty.chunks2 (
   344     Pretty.chunks (
   345       str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   346       :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
   347       @| (if is_some some_decls then str "end = struct" else str "struct")
   348     )
   349     :: body
   350     @| str ("end; (*struct " ^ name ^ "*)")
   351   );
   352 
   353 val literals_sml = Literals {
   354   literal_char = prefix "#" o quote o ML_Syntax.print_char,
   355   literal_string = quote o translate_string ML_Syntax.print_char,
   356   literal_numeral = fn unbounded => fn k =>
   357     if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"
   358     else string_of_int k,
   359   literal_list = Pretty.list "[" "]",
   360   infix_cons = (7, "::")
   361 };
   362 
   363 
   364 (** OCaml serializer **)
   365 
   366 fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve =
   367   let
   368     fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
   369       | print_tyco_expr fxy (tyco, [ty]) =
   370           concat [print_typ BR ty, (str o deresolve) tyco]
   371       | print_tyco_expr fxy (tyco, tys) =
   372           concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
   373     and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
   374          of NONE => print_tyco_expr fxy (tyco, tys)
   375           | SOME (i, print) => print print_typ fxy tys)
   376       | print_typ fxy (ITyVar v) = str ("'" ^ v);
   377     fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
   378     fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" ""
   379       (map_filter (fn (v, sort) =>
   380         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
   381     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
   382     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
   383     fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
   384           brackify fxy ((str o deresolve) inst ::
   385             (if is_pseudo_fun inst then [str "()"]
   386             else map_filter (print_dicts is_pseudo_fun BR) dss))
   387       | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
   388           str (if k = 1 then "_" ^ first_upper v
   389             else "_" ^ first_upper v ^ string_of_int (i+1))
   390           |> fold_rev (fn classrel => fn p =>
   391                Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
   392     and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
   393     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
   394       (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
   395     fun print_term is_pseudo_fun thm vars fxy (IConst c) =
   396           print_app is_pseudo_fun thm vars fxy (c, [])
   397       | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
   398           str "_"
   399       | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
   400           str (lookup_var vars v)
   401       | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
   402           (case Code_Thingol.unfold_const_app t
   403            of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
   404             | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
   405                 print_term is_pseudo_fun thm vars BR t2])
   406       | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
   407           let
   408             val (binds, t') = Code_Thingol.unfold_pat_abs t;
   409             val (ps, vars') = fold_map (print_bind is_pseudo_fun thm BR o fst) binds vars;
   410           in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun thm vars' NOBR t') end
   411       | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
   412           (case Code_Thingol.unfold_const_app t0
   413            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   414                 then print_case is_pseudo_fun thm vars fxy cases
   415                 else print_app is_pseudo_fun thm vars fxy c_ts
   416             | NONE => print_case is_pseudo_fun thm vars fxy cases)
   417     and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
   418       if is_cons c then
   419         let val k = length tys in
   420           if length ts = k
   421           then (str o deresolve) c
   422             :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
   423           else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
   424         end
   425       else if is_pseudo_fun c
   426         then (str o deresolve) c @@ str "()"
   427       else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
   428         @ map (print_term is_pseudo_fun thm vars BR) ts
   429     and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
   430       (print_term is_pseudo_fun) syntax_const thm vars
   431     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
   432     and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
   433           let
   434             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   435             fun print_let ((pat, ty), t) vars =
   436               vars
   437               |> print_bind is_pseudo_fun thm NOBR pat
   438               |>> (fn p => concat
   439                   [str "let", p, str "=", print_term is_pseudo_fun thm vars NOBR t, str "in"])
   440             val (ps, vars') = fold_map print_let binds vars;
   441           in
   442             brackify_block fxy (Pretty.chunks ps) []
   443               (print_term is_pseudo_fun thm vars' NOBR body)
   444           end
   445       | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
   446           let
   447             fun print_select delim (pat, body) =
   448               let
   449                 val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
   450               in concat [str delim, p, str "->", print_term is_pseudo_fun thm vars' NOBR body] end;
   451           in
   452             brackets (
   453               str "match"
   454               :: print_term is_pseudo_fun thm vars NOBR t
   455               :: print_select "with" clause
   456               :: map (print_select "|") clauses
   457             )
   458           end
   459       | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
   460           (concat o map str) ["failwith", "\"empty case\""];
   461     fun print_val_decl print_typscheme (name, typscheme) = concat
   462       [str "val", str (deresolve name), str ":", print_typscheme typscheme];
   463     fun print_datatype_decl definer (tyco, (vs, cos)) =
   464       let
   465         fun print_co (co, []) = str (deresolve co)
   466           | print_co (co, tys) = concat [str (deresolve co), str "of",
   467               Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
   468       in
   469         concat (
   470           str definer
   471           :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
   472           :: str "="
   473           :: separate (str "|") (map print_co cos)
   474         )
   475       end;
   476     fun print_def is_pseudo_fun needs_typ definer
   477           (ML_Function (name, (vs_ty as (vs, ty), eqs))) =
   478           let
   479             fun print_eqn ((ts, t), (thm, _)) =
   480               let
   481                 val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   482                 val vars = reserved
   483                   |> intro_base_names
   484                       (is_none o syntax_const) deresolve consts
   485                   |> intro_vars ((fold o Code_Thingol.fold_varnames)
   486                       (insert (op =)) ts []);
   487               in concat [
   488                 (Pretty.block o Pretty.commas)
   489                   (map (print_term is_pseudo_fun thm vars NOBR) ts),
   490                 str "->",
   491                 print_term is_pseudo_fun thm vars NOBR t
   492               ] end;
   493             fun print_eqns is_pseudo [((ts, t), (thm, _))] =
   494                   let
   495                     val consts = fold Code_Thingol.add_constnames (t :: ts) [];
   496                     val vars = reserved
   497                       |> intro_base_names
   498                           (is_none o syntax_const) deresolve consts
   499                       |> intro_vars ((fold o Code_Thingol.fold_varnames)
   500                           (insert (op =)) ts []);
   501                   in
   502                     concat (
   503                       (if is_pseudo then [str "()"]
   504                         else map (print_term is_pseudo_fun thm vars BR) ts)
   505                       @ str "="
   506                       @@ print_term is_pseudo_fun thm vars NOBR t
   507                     )
   508                   end
   509               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
   510                   Pretty.block (
   511                     str "="
   512                     :: Pretty.brk 1
   513                     :: str "function"
   514                     :: Pretty.brk 1
   515                     :: print_eqn eq
   516                     :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   517                           o single o print_eqn) eqs
   518                   )
   519               | print_eqns _ (eqs as eq :: eqs') =
   520                   let
   521                     val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
   522                     val vars = reserved
   523                       |> intro_base_names
   524                           (is_none o syntax_const) deresolve consts;
   525                     val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
   526                   in
   527                     Pretty.block (
   528                       Pretty.breaks dummy_parms
   529                       @ Pretty.brk 1
   530                       :: str "="
   531                       :: Pretty.brk 1
   532                       :: str "match"
   533                       :: Pretty.brk 1
   534                       :: (Pretty.block o Pretty.commas) dummy_parms
   535                       :: Pretty.brk 1
   536                       :: str "with"
   537                       :: Pretty.brk 1
   538                       :: print_eqn eq
   539                       :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
   540                            o single o print_eqn) eqs'
   541                     )
   542                   end;
   543             val prolog = if needs_typ then
   544               concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty]
   545                 else Pretty.strs [definer, deresolve name];
   546           in pair
   547             (print_val_decl print_typscheme (name, vs_ty))
   548             (concat (
   549               prolog
   550               :: print_dict_args vs
   551               @| print_eqns (is_pseudo_fun name) eqs
   552             ))
   553           end
   554       | print_def is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) =
   555           let
   556             fun print_superinst (_, (classrel, dss)) =
   557               concat [
   558                 (str o deresolve) classrel,
   559                 str "=",
   560                 print_dict is_pseudo_fun NOBR (DictConst dss)
   561               ];
   562             fun print_classparam ((classparam, c_inst), (thm, _)) =
   563               concat [
   564                 (str o deresolve) classparam,
   565                 str "=",
   566                 print_app (K false) thm reserved NOBR (c_inst, [])
   567               ];
   568           in pair
   569             (print_val_decl print_dicttypscheme
   570               (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
   571             (concat (
   572               str definer
   573               :: (str o deresolve) inst
   574               :: print_dict_args vs
   575               @ str "="
   576               @@ brackets [
   577                 enum_default "()" ";" "{" "}" (map print_superinst superinsts
   578                   @ map print_classparam classparams),
   579                 str ":",
   580                 print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   581               ]
   582             ))
   583           end;
   584      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
   585           [print_val_decl print_typscheme (name, vs_ty)]
   586           ((doublesemicolon o map str) (
   587             "let"
   588             :: deresolve name
   589             :: replicate n "_"
   590             @ "="
   591             :: "failwith"
   592             @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name
   593           ))
   594       | print_stmt (ML_Val binding) =
   595           let
   596             val (sig_p, p) = print_def (K false) true "let" binding
   597           in pair
   598             [sig_p]
   599             (doublesemicolon [p])
   600           end
   601       | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) =
   602           let
   603             val print_def' = print_def (member (op =) pseudo_funs) false;
   604             fun print_pseudo_fun name = concat [
   605                 str "let",
   606                 (str o deresolve) name,
   607                 str "=",
   608                 (str o deresolve) name,
   609                 str "();;"
   610               ];
   611             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
   612               (print_def' "let rec" binding :: map (print_def' "and") bindings);
   613             val pseudo_ps = map print_pseudo_fun pseudo_funs;
   614           in pair
   615             sig_ps
   616             (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps))
   617           end
   618      | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   619           let
   620             val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   621           in
   622             pair
   623             [concat [str "type", ty_p]]
   624             (concat [str "type", ty_p, str "=", str "EMPTY__"])
   625           end
   626      | print_stmt (ML_Datas (data :: datas)) = 
   627           let
   628             val sig_ps = print_datatype_decl "type" data
   629               :: map (print_datatype_decl "and") datas;
   630             val (ps, p) = split_last sig_ps;
   631           in pair
   632             sig_ps
   633             (Pretty.chunks (ps @| doublesemicolon [p]))
   634           end
   635      | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) =
   636           let
   637             fun print_field s p = concat [str s, str ":", p];
   638             fun print_superclass_field (superclass, classrel) =
   639               print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v));
   640             fun print_classparam_decl (classparam, ty) =
   641               print_val_decl print_typscheme
   642                 (classparam, ([(v, [class])], ty));
   643             fun print_classparam_field (classparam, ty) =
   644               print_field (deresolve classparam) (print_typ NOBR ty);
   645             val w = "_" ^ first_upper v;
   646             fun print_classparam_proj (classparam, _) =
   647               (concat o map str) ["let", deresolve classparam, w, "=",
   648                 w ^ "." ^ deresolve classparam ^ ";;"];
   649             val type_decl_p = concat [
   650                 str ("type '" ^ v),
   651                 (str o deresolve) class,
   652                 str "=",
   653                 enum_default "unit" ";" "{" "}" (
   654                   map print_superclass_field superclasses
   655                   @ map print_classparam_field classparams
   656                 )
   657               ];
   658           in pair
   659             (type_decl_p :: map print_classparam_decl classparams)
   660             (Pretty.chunks (
   661               doublesemicolon [type_decl_p]
   662               :: map print_classparam_proj classparams
   663             ))
   664           end;
   665   in print_stmt end;
   666 
   667 fun print_ocaml_module name some_decls body = Pretty.chunks2 (
   668     Pretty.chunks (
   669       str ("module " ^ name ^ (if is_some some_decls then " : sig" else " ="))
   670       :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls
   671       @| (if is_some some_decls then str "end = struct" else str "struct")
   672     )
   673     :: body
   674     @| str ("end;; (*struct " ^ name ^ "*)")
   675   );
   676 
   677 val literals_ocaml = let
   678   fun chr i =
   679     let
   680       val xs = string_of_int i;
   681       val ys = replicate_string (3 - length (explode xs)) "0";
   682     in "\\" ^ ys ^ xs end;
   683   fun char_ocaml c =
   684     let
   685       val i = ord c;
   686       val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
   687         then chr i else c
   688     in s end;
   689   fun bignum_ocaml k = if k <= 1073741823
   690     then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
   691     else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
   692 in Literals {
   693   literal_char = enclose "'" "'" o char_ocaml,
   694   literal_string = quote o translate_string char_ocaml,
   695   literal_numeral = fn unbounded => fn k => if k >= 0 then
   696       if unbounded then bignum_ocaml k
   697       else string_of_int k
   698     else
   699       if unbounded then "(Big_int.minus_big_int " ^ bignum_ocaml (~ k) ^ ")"
   700       else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,
   701   literal_list = Pretty.enum ";" "[" "]",
   702   infix_cons = (6, "::")
   703 } end;
   704 
   705 
   706 
   707 (** SML/OCaml generic part **)
   708 
   709 local
   710 
   711 datatype ml_node =
   712     Dummy of string
   713   | Stmt of string * ml_stmt
   714   | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
   715 
   716 in
   717 
   718 fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
   719   let
   720     val module_alias = if is_some module_name then K module_name else raw_module_alias;
   721     val reserved = Name.make_context reserved;
   722     val empty_module = ((reserved, reserved), Graph.empty);
   723     fun map_node [] f = f
   724       | map_node (m::ms) f =
   725           Graph.default_node (m, Module (m, empty_module))
   726           #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
   727                Module (module_name, (nsp, map_node ms f nodes)));
   728     fun map_nsp_yield [] f (nsp, nodes) =
   729           let
   730             val (x, nsp') = f nsp
   731           in (x, (nsp', nodes)) end
   732       | map_nsp_yield (m::ms) f (nsp, nodes) =
   733           let
   734             val (x, nodes') =
   735               nodes
   736               |> Graph.default_node (m, Module (m, empty_module))
   737               |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 
   738                   let
   739                     val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
   740                   in (x, Module (d_module_name, nsp_nodes')) end)
   741           in (x, (nsp, nodes')) end;
   742     fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
   743       let
   744         val (x, nsp_fun') = f nsp_fun
   745       in (x, (nsp_fun', nsp_typ)) end;
   746     fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
   747       let
   748         val (x, nsp_typ') = f nsp_typ
   749       in (x, (nsp_fun, nsp_typ')) end;
   750     val mk_name_module = mk_name_module reserved NONE module_alias program;
   751     fun mk_name_stmt upper name nsp =
   752       let
   753         val (_, base) = dest_name name;
   754         val base' = if upper then first_upper base else base;
   755         val ([base''], nsp') = Name.variants [base'] nsp;
   756       in (base'', nsp') end;
   757     fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) =
   758           let
   759             val eqs = filter (snd o snd) raw_eqs;
   760             val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
   761                of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
   762                   then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE)
   763                   else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
   764                 | _ => (eqs, NONE)
   765               else (eqs, NONE)
   766           in (ML_Function (name, (tysm, eqs')), is_value) end
   767       | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) =
   768           (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE)
   769       | ml_binding_of_stmt (name, _) =
   770           error ("Binding block containing illegal statement: " ^ labelled_name name)
   771     fun add_fun (name, stmt) =
   772       let
   773         val (binding, some_value_name) = ml_binding_of_stmt (name, stmt);
   774         val ml_stmt = case binding
   775          of ML_Function (name, ((vs, ty), [])) =>
   776               ML_Exc (name, ((vs, ty),
   777                 (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty))
   778           | _ => case some_value_name
   779              of NONE => ML_Funs ([binding], [])
   780               | SOME (name, true) => ML_Funs ([binding], [name])
   781               | SOME (name, false) => ML_Val binding
   782       in
   783         map_nsp_fun_yield (mk_name_stmt false name)
   784         #>> (fn name' => ([name'], ml_stmt))
   785       end;
   786     fun add_funs stmts =
   787       let
   788         val ml_stmt = ML_Funs (map_split ml_binding_of_stmt stmts |> (apsnd o map_filter o Option.map) fst);
   789       in
   790         fold_map (fn (name, _) => map_nsp_fun_yield (mk_name_stmt false name)) stmts
   791         #>> rpair ml_stmt
   792       end;
   793     fun add_datatypes stmts =
   794       fold_map
   795         (fn (name, Code_Thingol.Datatype (_, stmt)) =>
   796               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   797           | (name, Code_Thingol.Datatypecons _) =>
   798               map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
   799           | (name, _) =>
   800               error ("Datatype block containing illegal statement: " ^ labelled_name name)
   801         ) stmts
   802       #>> (split_list #> apsnd (map_filter I
   803         #> (fn [] => error ("Datatype block without data statement: "
   804                   ^ (commas o map (labelled_name o fst)) stmts)
   805              | stmts => ML_Datas stmts)));
   806     fun add_class stmts =
   807       fold_map
   808         (fn (name, Code_Thingol.Class (_, stmt)) =>
   809               map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
   810           | (name, Code_Thingol.Classrel _) =>
   811               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   812           | (name, Code_Thingol.Classparam _) =>
   813               map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
   814           | (name, _) =>
   815               error ("Class block containing illegal statement: " ^ labelled_name name)
   816         ) stmts
   817       #>> (split_list #> apsnd (map_filter I
   818         #> (fn [] => error ("Class block without class statement: "
   819                   ^ (commas o map (labelled_name o fst)) stmts)
   820              | [stmt] => ML_Class stmt)));
   821     fun add_stmts ([stmt as (name, Code_Thingol.Fun _)]) =
   822           add_fun stmt
   823       | add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
   824           add_funs stmts
   825       | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
   826           add_datatypes stmts
   827       | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
   828           add_datatypes stmts
   829       | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
   830           add_class stmts
   831       | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
   832           add_class stmts
   833       | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
   834           add_class stmts
   835       | add_stmts ([stmt as (_, Code_Thingol.Classinst _)]) =
   836           add_fun stmt
   837       | add_stmts ((stmts as (_, Code_Thingol.Classinst _)::_)) =
   838           add_funs stmts
   839       | add_stmts stmts = error ("Illegal mutual dependencies: " ^
   840           (commas o map (labelled_name o fst)) stmts);
   841     fun add_stmts' stmts nsp_nodes =
   842       let
   843         val names as (name :: names') = map fst stmts;
   844         val deps =
   845           []
   846           |> fold (fold (insert (op =)) o Graph.imm_succs program) names
   847           |> subtract (op =) names;
   848         val (module_names, _) = (split_list o map dest_name) names;
   849         val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
   850           handle Empty =>
   851             error ("Different namespace prefixes for mutual dependencies:\n"
   852               ^ commas (map labelled_name names)
   853               ^ "\n"
   854               ^ commas module_names);
   855         val module_name_path = Long_Name.explode module_name;
   856         fun add_dep name name' =
   857           let
   858             val module_name' = (mk_name_module o fst o dest_name) name';
   859           in if module_name = module_name' then
   860             map_node module_name_path (Graph.add_edge (name, name'))
   861           else let
   862             val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
   863               (module_name_path, Long_Name.explode module_name');
   864           in
   865             map_node common
   866               (fn node => Graph.add_edge_acyclic (diff1, diff2) node
   867                 handle Graph.CYCLES _ => error ("Dependency "
   868                   ^ quote name ^ " -> " ^ quote name'
   869                   ^ " would result in module dependency cycle"))
   870           end end;
   871       in
   872         nsp_nodes
   873         |> map_nsp_yield module_name_path (add_stmts stmts)
   874         |-> (fn (base' :: bases', stmt') =>
   875            apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
   876               #> fold2 (fn name' => fn base' =>
   877                    Graph.new_node (name', (Dummy base'))) names' bases')))
   878         |> apsnd (fold (fn name => fold (add_dep name) deps) names)
   879         |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
   880       end;
   881     val (_, nodes) = empty_module
   882       |> fold add_stmts' (map (AList.make (Graph.get_node program))
   883           (rev (Graph.strong_conn program)));
   884     fun deresolver prefix name = 
   885       let
   886         val module_name = (fst o dest_name) name;
   887         val module_name' = (Long_Name.explode o mk_name_module) module_name;
   888         val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
   889         val stmt_name =
   890           nodes
   891           |> fold (fn name => fn node => case Graph.get_node node name
   892               of Module (_, (_, node)) => node) module_name'
   893           |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
   894                | Dummy stmt_name => stmt_name);
   895       in
   896         Long_Name.implode (remainder @ [stmt_name])
   897       end handle Graph.UNDEF _ =>
   898         error ("Unknown statement name: " ^ labelled_name name);
   899   in (deresolver, nodes) end;
   900 
   901 fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name
   902   reserved includes raw_module_alias _ syntax_tyco syntax_const program stmt_names destination =
   903   let
   904     val is_cons = Code_Thingol.is_cons program;
   905     val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
   906     val is_presentation = not (null presentation_stmt_names);
   907     val module_name = if is_presentation then SOME "Code" else raw_module_name;
   908     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
   909       reserved raw_module_alias program;
   910     val reserved = make_vars reserved;
   911     fun print_node prefix (Dummy _) =
   912           NONE
   913       | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso
   914           (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt
   915           then NONE
   916           else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt)
   917       | print_node prefix (Module (module_name, (_, nodes))) =
   918           let
   919             val (decls, body) = print_nodes (prefix @ [module_name]) nodes;
   920             val p = if is_presentation then Pretty.chunks2 body
   921               else print_module module_name (if with_signatures then SOME decls else NONE) body;
   922           in SOME ([], p) end
   923     and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes)
   924         o rev o flat o Graph.strong_conn) nodes
   925       |> split_list
   926       |> (fn (decls, body) => (flat decls, body))
   927     val stmt_names' = (map o try)
   928       (deresolver (if is_some module_name then the_list module_name else [])) stmt_names;
   929     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes));
   930   in
   931     Code_Target.mk_serialization target
   932       (case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty) | NONE => NONE)
   933       (fn NONE => Code_Target.code_writeln | SOME file => File.write file o Code_Target.code_of_pretty)
   934       (rpair stmt_names' o Code_Target.code_of_pretty) p destination
   935   end;
   936 
   937 end; (*local*)
   938 
   939 
   940 (** ML (system language) code for evaluation and instrumentalization **)
   941 
   942 val eval_struct_name = "Code"
   943 
   944 fun eval_code_of some_target with_struct thy =
   945   let
   946     val target = the_default target_Eval some_target;
   947     val serialize = if with_struct then fn _ => fn [] =>
   948         serialize_ml target_SML (SOME (K ())) print_sml_module print_sml_stmt (SOME eval_struct_name) true
   949       else fn _ => fn [] => 
   950         serialize_ml target_SML (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt (SOME eval_struct_name) true;
   951   in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end;
   952 
   953 
   954 (* evaluation *)
   955 
   956 fun eval some_target reff postproc thy t args =
   957   let
   958     val ctxt = ProofContext.init thy;
   959     fun evaluator naming program ((_, (_, ty)), t) deps =
   960       let
   961         val _ = if Code_Thingol.contains_dictvar t then
   962           error "Term to be evaluated contains free dictionaries" else ();
   963         val value_name = "Value.VALUE.value"
   964         val program' = program
   965           |> Graph.new_node (value_name,
   966               Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
   967           |> fold (curry Graph.add_edge value_name) deps;
   968         val (value_code, [SOME value_name']) = eval_code_of some_target false thy naming program' [value_name];
   969         val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
   970           ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
   971       in ML_Context.evaluate ctxt false reff sml_code end;
   972   in Code_Thingol.eval thy postproc evaluator t end;
   973 
   974 
   975 (* instrumentalization by antiquotation *)
   976 
   977 local
   978 
   979 structure CodeAntiqData = Proof_Data
   980 (
   981   type T = (string list * string list) * (bool * (string
   982     * (string * ((string * string) list * (string * string) list)) lazy));
   983   fun init _ = (([], []), (true, ("", Lazy.value ("", ([], [])))));
   984 );
   985 
   986 val is_first_occ = fst o snd o CodeAntiqData.get;
   987 
   988 fun delayed_code thy tycos consts () =
   989   let
   990     val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
   991     val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
   992     val (ml_code, target_names) = eval_code_of NONE true thy naming program (consts' @ tycos');
   993     val (consts'', tycos'') = chop (length consts') target_names;
   994     val consts_map = map2 (fn const => fn NONE =>
   995         error ("Constant " ^ (quote o Code.string_of_const thy) const
   996           ^ "\nhas a user-defined serialization")
   997       | SOME const'' => (const, const'')) consts consts''
   998     val tycos_map = map2 (fn tyco => fn NONE =>
   999         error ("Type " ^ (quote o Sign.extern_type thy) tyco
  1000           ^ "\nhas a user-defined serialization")
  1001       | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
  1002   in (ml_code, (tycos_map, consts_map)) end;
  1003 
  1004 fun register_code new_tycos new_consts ctxt =
  1005   let
  1006     val ((tycos, consts), (_, (struct_name, _))) = CodeAntiqData.get ctxt;
  1007     val tycos' = fold (insert (op =)) new_tycos tycos;
  1008     val consts' = fold (insert (op =)) new_consts consts;
  1009     val (struct_name', ctxt') = if struct_name = ""
  1010       then ML_Antiquote.variant eval_struct_name ctxt
  1011       else (struct_name, ctxt);
  1012     val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) tycos' consts');
  1013   in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end;
  1014 
  1015 fun register_const const = register_code [] [const];
  1016 
  1017 fun register_datatype tyco constrs = register_code [tyco] constrs;
  1018 
  1019 fun print_const const all_struct_name tycos_map consts_map =
  1020   (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
  1021 
  1022 fun print_datatype tyco constrs all_struct_name tycos_map consts_map =
  1023   let
  1024     val upperize = implode o nth_map 0 Symbol.to_ascii_upper o explode;
  1025     fun check_base name name'' =
  1026       if upperize (Long_Name.base_name name) = upperize name''
  1027       then () else error ("Name as printed " ^ quote name''
  1028         ^ "\ndiffers from logical base name " ^ quote (Long_Name.base_name name) ^ "; sorry.");
  1029     val tyco'' = (the o AList.lookup (op =) tycos_map) tyco;
  1030     val constrs'' = map (the o AList.lookup (op =) consts_map) constrs;
  1031     val _ = check_base tyco tyco'';
  1032     val _ = map2 check_base constrs constrs'';
  1033   in "datatype " ^ tyco'' ^ " = datatype " ^ Long_Name.append all_struct_name tyco'' end;
  1034 
  1035 fun print_code struct_name is_first print_it ctxt =
  1036   let
  1037     val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
  1038     val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code;
  1039     val ml_code = if is_first then ml_code
  1040       else "";
  1041     val all_struct_name = Long_Name.append struct_name struct_code_name;
  1042   in (ml_code, print_it all_struct_name tycos_map consts_map) end;
  1043 
  1044 in
  1045 
  1046 fun ml_code_antiq raw_const {struct_name, background} =
  1047   let
  1048     val const = Code.check_const (ProofContext.theory_of background) raw_const;
  1049     val is_first = is_first_occ background;
  1050     val background' = register_const const background;
  1051   in (print_code struct_name is_first (print_const const), background') end;
  1052 
  1053 fun ml_code_datatype_antiq (raw_tyco, raw_constrs) {struct_name, background} =
  1054   let
  1055     val thy = ProofContext.theory_of background;
  1056     val tyco = Sign.intern_type thy raw_tyco;
  1057     val constrs = map (Code.check_const thy) raw_constrs;
  1058     val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
  1059     val _ = if eq_set (op =) (constrs, constrs') then ()
  1060       else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")
  1061     val is_first = is_first_occ background;
  1062     val background' = register_datatype tyco constrs background;
  1063   in (print_code struct_name is_first (print_datatype tyco constrs), background') end;
  1064 
  1065 end; (*local*)
  1066 
  1067 
  1068 (** Isar setup **)
  1069 
  1070 val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
  1071 val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
  1072   (Args.tyname --| Scan.lift (Args.$$$ "=")
  1073     -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
  1074       >> ml_code_datatype_antiq);
  1075 
  1076 fun isar_seri_sml module_name =
  1077   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
  1078   >> (fn with_signatures => serialize_ml target_SML
  1079       (SOME (use_text ML_Env.local_context (1, "generated code") false))
  1080       print_sml_module print_sml_stmt module_name with_signatures));
  1081 
  1082 fun isar_seri_ocaml module_name =
  1083   Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
  1084   >> (fn with_signatures => serialize_ml target_OCaml NONE
  1085       print_ocaml_module print_ocaml_stmt module_name with_signatures));
  1086 
  1087 val setup =
  1088   Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
  1089   #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
  1090   #> Code_Target.extend_target (target_Eval, (target_SML, K I))
  1091   #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
  1092       brackify_infix (1, R) fxy [
  1093         print_typ (INFX (1, X)) ty1,
  1094         str "->",
  1095         print_typ (INFX (1, R)) ty2
  1096       ]))
  1097   #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
  1098       brackify_infix (1, R) fxy [
  1099         print_typ (INFX (1, X)) ty1,
  1100         str "->",
  1101         print_typ (INFX (1, R)) ty2
  1102       ]))
  1103   #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
  1104   #> fold (Code_Target.add_reserved target_SML)
  1105       ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
  1106   #> fold (Code_Target.add_reserved target_OCaml) [
  1107       "and", "as", "assert", "begin", "class",
  1108       "constraint", "do", "done", "downto", "else", "end", "exception",
  1109       "external", "false", "for", "fun", "function", "functor", "if",
  1110       "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
  1111       "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
  1112       "sig", "struct", "then", "to", "true", "try", "type", "val",
  1113       "virtual", "when", "while", "with"
  1114     ]
  1115   #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"];
  1116 
  1117 end; (*struct*)