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