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