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