(*  Title:      Tools/code/code_ml.ML

    ID:         $Id$

    Author:     Florian Haftmann, TU Muenchen

Serializer for SML and OCaml.

*)

signature CODE_ML =

sig

  val eval_conv: string * (unit -> thm) option ref

    -> theory -> cterm -> string list -> thm;

  val eval_term: string * (unit -> 'a) option ref

    -> theory -> term -> string list -> 'a;

  val setup: theory -> theory

end;

structure Code_ML : CODE_ML =

struct

open Basic_Code_Thingol;

open Code_Printer;

infixr 5 @@;

infixr 5 @|;

val target_SML = "SML";

val target_OCaml = "OCaml";

datatype ml_stmt =

    MLFuns of (string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)) list

  | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list

  | MLClass of string * (vname * ((class * string) list * (string * itype) list))

  | MLClassinst of string * ((class * (string * (vname * sort) list))

        * ((class * (string * (string * dict list list))) list

      * ((string * const) * (thm * bool)) list));

fun stmt_names_of (MLFuns fs) = map fst fs

  | stmt_names_of (MLDatas ds) = map fst ds

  | stmt_names_of (MLClass (c, _)) = [c]

  | stmt_names_of (MLClassinst (i, _)) = [i];

(** SML serailizer **)

fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =

  let

    val pr_label_classrel = translate_string (fn "." => "__" | c => c)

      o NameSpace.qualifier;

    val pr_label_classparam = NameSpace.base o NameSpace.qualifier;

    fun pr_dicts fxy ds =

      let

        fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"

          | pr_dictvar (v, (i, _)) = Code_Name.first_upper v ^ string_of_int (i+1) ^ "_";

        fun pr_proj [] p =

              p

          | pr_proj [p'] p =

              brackets [p', p]

          | pr_proj (ps as _ :: _) p =

              brackets [Pretty.enum " o" "(" ")" ps, p];

        fun pr_dict fxy (DictConst (inst, dss)) =

              brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)

          | pr_dict fxy (DictVar (classrels, v)) =

              pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)

      in case ds

       of [] => str "()"

        | [d] => pr_dict fxy d

        | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds

      end;

    fun pr_tyvar_dicts vs =

      vs

      |> map (fn (v, sort) => map_index (fn (i, _) =>

           DictVar ([], (v, (i, length sort)))) sort)

      |> map (pr_dicts BR);

    fun pr_tycoexpr fxy (tyco, tys) =

      let

        val tyco' = (str o deresolve) tyco

      in case map (pr_typ BR) tys

       of [] => tyco'

        | [p] => Pretty.block [p, Pretty.brk 1, tyco']

        | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']

      end

    and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco

         of NONE => pr_tycoexpr fxy (tyco, tys)

          | SOME (i, pr) => pr pr_typ fxy tys)

      | pr_typ fxy (ITyVar v) = str ("'" ^ v);

    fun pr_term thm pat vars fxy (IConst c) =

          pr_app thm pat vars fxy (c, [])

      | pr_term thm pat vars fxy (IVar v) =

          str (Code_Name.lookup_var vars v)

      | pr_term thm pat vars fxy (t as t1 `$ t2) =

          (case Code_Thingol.unfold_const_app t

           of SOME c_ts => pr_app thm pat vars fxy c_ts

            | NONE =>

                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])

      | pr_term thm pat vars fxy (t as _ `|-> _) =

          let

            val (binds, t') = Code_Thingol.unfold_abs t;

            fun pr ((v, pat), ty) =

              pr_bind thm NOBR ((SOME v, pat), ty)

              #>> (fn p => concat [str "fn", p, str "=>"]);

            val (ps, vars') = fold_map pr binds vars;

          in brackets (ps @ [pr_term thm pat vars' NOBR t']) end

      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =

          (case Code_Thingol.unfold_const_app t0

           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)

                then pr_case thm vars fxy cases

                else pr_app thm pat vars fxy c_ts

            | NONE => pr_case thm vars fxy cases)

    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =

      if is_cons c then let

        val k = length tys

      in if k < 2 then 

        (str o deresolve) c :: map (pr_term thm pat vars BR) ts

      else if k = length ts then

        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]

      else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else

        (str o deresolve) c

          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts

    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars

    and pr_bind' ((NONE, NONE), _) = str "_"

      | pr_bind' ((SOME v, NONE), _) = str v

      | pr_bind' ((NONE, SOME p), _) = p

      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]

    and pr_bind thm = gen_pr_bind pr_bind' pr_term thm

    and pr_case thm vars fxy (cases as ((_, [_]), _)) =

          let

            val (binds, t') = Code_Thingol.unfold_let (ICase cases);

            fun pr ((pat, ty), t) vars =

              vars

              |> pr_bind thm NOBR ((NONE, SOME pat), ty)

              |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])

            val (ps, vars') = fold_map pr binds vars;

          in

            Pretty.chunks [

              [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,

              [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,

              str ("end")

            ]

          end

      | pr_case thm vars fxy (((td, ty), b::bs), _) =

          let

            fun pr delim (pat, t) =

              let

                val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;

              in

                concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]

              end;

          in

            (Pretty.enclose "(" ")" o single o brackify fxy) (

              str "case"

              :: pr_term thm false vars NOBR td

              :: pr "of" b

              :: map (pr "|") bs

            )

          end

      | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";

    fun pr_stmt (MLFuns (funns as (funn :: funns'))) =

          let

            val definer =

              let

                fun no_args _ (((ts, _), _) :: _) = length ts

                  | no_args ty [] = (length o fst o Code_Thingol.unfold_fun) ty;

                fun mk 0 [] = "val"

                  | mk 0 vs = if (null o filter_out (null o snd)) vs

                      then "val" else "fun"

                  | mk k _ = "fun";

                fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)

                  | chk (_, ((vs, ty), eqs)) (SOME defi) =

                      if defi = mk (no_args ty eqs) vs then SOME defi

                      else error ("Mixing simultaneous vals and funs not implemented: "

                        ^ commas (map (labelled_name o fst) funns));

              in the (fold chk funns NONE) end;

            fun pr_funn definer (name, ((vs, ty), [])) =

                  let

                    val vs_dict = filter_out (null o snd) vs;

                    val n = length vs_dict + (length o fst o Code_Thingol.unfold_fun) ty;

                    val exc_str =

                      (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;

                  in

                    concat (

                      str definer

                      :: (str o deresolve) name

                      :: map str (replicate n "_")

                      @ str "="

                      :: str "raise"

                      :: str "(Fail"

                      @@ str (exc_str ^ ")")

                    )

                  end

              | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =

                  let

                    val vs_dict = filter_out (null o snd) vs;

                    val shift = if null eqs' then I else

                      map (Pretty.block o single o Pretty.block o single);

                    fun pr_eq definer ((ts, t), (thm, _)) =

                      let

                        val consts = map_filter

                          (fn c => if (is_some o syntax_const) c

                            then NONE else (SOME o NameSpace.base o deresolve) c)

                            ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);

                        val vars = reserved_names

                          |> Code_Name.intro_vars consts

                          |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)

                               (insert (op =)) ts []);

                      in

                        concat (

                          [str definer, (str o deresolve) name]

                          @ (if null ts andalso null vs_dict

                             then [str ":", pr_typ NOBR ty]

                             else

                               pr_tyvar_dicts vs_dict

                               @ map (pr_term thm true vars BR) ts)

                       @ [str "=", pr_term thm false vars NOBR t]

                        )

                      end

                  in

                    (Pretty.block o Pretty.fbreaks o shift) (

                      pr_eq definer eq

                      :: map (pr_eq "|") eqs'

                    )

                  end;

            val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');

          in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end

     | pr_stmt (MLDatas (datas as (data :: datas'))) =

          let

            fun pr_co (co, []) =

                  str (deresolve co)

              | pr_co (co, tys) =

                  concat [

                    str (deresolve co),

                    str "of",

                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)

                  ];

            fun pr_data definer (tyco, (vs, [])) =

                  concat (

                    str definer

                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

                    :: str "="

                    @@ str "EMPTY__" 

                  )

              | pr_data definer (tyco, (vs, cos)) =

                  concat (

                    str definer

                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

                    :: str "="

                    :: separate (str "|") (map pr_co cos)

                  );

            val (ps, p) = split_last

              (pr_data "datatype" data :: map (pr_data "and") datas');

          in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end

     | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =

          let

            val w = Code_Name.first_upper v ^ "_";

            fun pr_superclass_field (class, classrel) =

              (concat o map str) [

                pr_label_classrel classrel, ":", "'" ^ v, deresolve class

              ];

            fun pr_classparam_field (classparam, ty) =

              concat [

                (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty

              ];

            fun pr_classparam_proj (classparam, _) =

              semicolon [

                str "fun",

                (str o deresolve) classparam,

                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],

                str "=",

                str ("#" ^ pr_label_classparam classparam),

                str w

              ];

            fun pr_superclass_proj (_, classrel) =

              semicolon [

                str "fun",

                (str o deresolve) classrel,

                Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],

                str "=",

                str ("#" ^ pr_label_classrel classrel),

                str w

              ];

          in

            Pretty.chunks (

              concat [

                str ("type '" ^ v),

                (str o deresolve) class,

                str "=",

                Pretty.enum "," "{" "};" (

                  map pr_superclass_field superclasses @ map pr_classparam_field classparams

                )

              ]

              :: map pr_superclass_proj superclasses

              @ map pr_classparam_proj classparams

            )

          end

     | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =

          let

            fun pr_superclass (_, (classrel, dss)) =

              concat [

                (str o pr_label_classrel) classrel,

                str "=",

                pr_dicts NOBR [DictConst dss]

              ];

            fun pr_classparam ((classparam, c_inst), (thm, _)) =

              concat [

                (str o pr_label_classparam) classparam,

                str "=",

                pr_app thm false reserved_names NOBR (c_inst, [])

              ];

          in

            semicolon ([

              str (if null arity then "val" else "fun"),

              (str o deresolve) inst ] @

              pr_tyvar_dicts arity @ [

              str "=",

              Pretty.enum "," "{" "}"

                (map pr_superclass superarities @ map pr_classparam classparam_insts),

              str ":",

              pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])

            ])

          end;

  in pr_stmt end;

fun pr_sml_module name content =

  Pretty.chunks (

    str ("structure " ^ name ^ " = ")

    :: str "struct"

    :: str ""

    :: content

    @ str ""

    @@ str ("end; (*struct " ^ name ^ "*)")

  );

val literals_sml = Literals {

  literal_char = prefix "#" o quote o ML_Syntax.print_char,

  literal_string = quote o translate_string ML_Syntax.print_char,

  literal_numeral = fn unbounded => fn k =>

    if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)"

    else string_of_int k,

  literal_list = Pretty.enum "," "[" "]",

  infix_cons = (7, "::")

};

(** OCaml serializer **)

fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =

  let

    fun pr_dicts fxy ds =

      let

        fun pr_dictvar (v, (_, 1)) = "_" ^ Code_Name.first_upper v

          | pr_dictvar (v, (i, _)) = "_" ^ Code_Name.first_upper v ^ string_of_int (i+1);

        fun pr_proj ps p =

          fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p

        fun pr_dict fxy (DictConst (inst, dss)) =

              brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)

          | pr_dict fxy (DictVar (classrels, v)) =

              pr_proj (map deresolve classrels) ((str o pr_dictvar) v)

      in case ds

       of [] => str "()"

        | [d] => pr_dict fxy d

        | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds

      end;

    fun pr_tyvar_dicts vs =

      vs

      |> map (fn (v, sort) => map_index (fn (i, _) =>

           DictVar ([], (v, (i, length sort)))) sort)

      |> map (pr_dicts BR);

    fun pr_tycoexpr fxy (tyco, tys) =

      let

        val tyco' = (str o deresolve) tyco

      in case map (pr_typ BR) tys

       of [] => tyco'

        | [p] => Pretty.block [p, Pretty.brk 1, tyco']

        | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']

      end

    and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco

         of NONE => pr_tycoexpr fxy (tyco, tys)

          | SOME (i, pr) => pr pr_typ fxy tys)

      | pr_typ fxy (ITyVar v) = str ("'" ^ v);

    fun pr_term thm pat vars fxy (IConst c) =

          pr_app thm pat vars fxy (c, [])

      | pr_term thm pat vars fxy (IVar v) =

          str (Code_Name.lookup_var vars v)

      | pr_term thm pat vars fxy (t as t1 `$ t2) =

          (case Code_Thingol.unfold_const_app t

           of SOME c_ts => pr_app thm pat vars fxy c_ts

            | NONE =>

                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])

      | pr_term thm pat vars fxy (t as _ `|-> _) =

          let

            val (binds, t') = Code_Thingol.unfold_abs t;

            fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);

            val (ps, vars') = fold_map pr binds vars;

          in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end

      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0

           of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)

                then pr_case thm vars fxy cases

                else pr_app thm pat vars fxy c_ts

            | NONE => pr_case thm vars fxy cases)

    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =

      if is_cons c then

        if length tys = length ts

        then case ts

         of [] => [(str o deresolve) c]

          | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]

          | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"

                    (map (pr_term thm pat vars NOBR) ts)]

        else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]

      else (str o deresolve) c

        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)

    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars

    and pr_bind' ((NONE, NONE), _) = str "_"

      | pr_bind' ((SOME v, NONE), _) = str v

      | pr_bind' ((NONE, SOME p), _) = p

      | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]

    and pr_bind thm = gen_pr_bind pr_bind' pr_term thm

    and pr_case thm vars fxy (cases as ((_, [_]), _)) =

          let

            val (binds, t') = Code_Thingol.unfold_let (ICase cases);

            fun pr ((pat, ty), t) vars =

              vars

              |> pr_bind thm NOBR ((NONE, SOME pat), ty)

              |>> (fn p => concat

                  [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])

            val (ps, vars') = fold_map pr binds vars;

          in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end

      | pr_case thm vars fxy (((td, ty), b::bs), _) =

          let

            fun pr delim (pat, t) =

              let

                val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;

              in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;

          in

            (Pretty.enclose "(" ")" o single o brackify fxy) (

              str "match"

              :: pr_term thm false vars NOBR td

              :: pr "with" b

              :: map (pr "|") bs

            )

          end

      | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";

    fun fish_params vars eqs =

      let

        fun fish_param _ (w as SOME _) = w

          | fish_param (IVar v) NONE = SOME v

          | fish_param _ NONE = NONE;

        fun fillup_param _ (_, SOME v) = v

          | fillup_param x (i, NONE) = x ^ string_of_int i;

        val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);

        val x = Name.variant (map_filter I fished1) "x";

        val fished2 = map_index (fillup_param x) fished1;

        val (fished3, _) = Name.variants fished2 Name.context;

        val vars' = Code_Name.intro_vars fished3 vars;

      in map (Code_Name.lookup_var vars') fished3 end;

    fun pr_stmt (MLFuns (funns as funn :: funns')) =

          let

            fun pr_eq ((ts, t), (thm, _)) =

              let

                val consts = map_filter

                  (fn c => if (is_some o syntax_const) c

                    then NONE else (SOME o NameSpace.base o deresolve) c)

                    ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);

                val vars = reserved_names

                  |> Code_Name.intro_vars consts

                  |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)

                      (insert (op =)) ts []);

              in concat [

                (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),

                str "->",

                pr_term thm false vars NOBR t

              ] end;

            fun pr_eqs name ty [] =

                  let

                    val n = (length o fst o Code_Thingol.unfold_fun) ty;

                    val exc_str =

                      (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;

                  in

                    concat (

                      map str (replicate n "_")

                      @ str "="

                      :: str "failwith"

                      @@ str exc_str

                    )

                  end

              | pr_eqs _ _ [((ts, t), (thm, _))] =

                  let

                    val consts = map_filter

                      (fn c => if (is_some o syntax_const) c

                        then NONE else (SOME o NameSpace.base o deresolve) c)

                        ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);

                    val vars = reserved_names

                      |> Code_Name.intro_vars consts

                      |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)

                          (insert (op =)) ts []);

                  in

                    concat (

                      map (pr_term thm true vars BR) ts

                      @ str "="

                      @@ pr_term thm false vars NOBR t

                    )

                  end

              | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =

                  Pretty.block (

                    str "="

                    :: Pretty.brk 1

                    :: str "function"

                    :: Pretty.brk 1

                    :: pr_eq eq

                    :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]

                          o single o pr_eq) eqs'

                  )

              | pr_eqs _ _ (eqs as eq :: eqs') =

                  let

                    val consts = map_filter

                      (fn c => if (is_some o syntax_const) c

                        then NONE else (SOME o NameSpace.base o deresolve) c)

                        ((fold o Code_Thingol.fold_constnames)

                          (insert (op =)) (map (snd o fst) eqs) []);

                    val vars = reserved_names

                      |> Code_Name.intro_vars consts;

                    val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;

                  in

                    Pretty.block (

                      Pretty.breaks dummy_parms

                      @ Pretty.brk 1

                      :: str "="

                      :: Pretty.brk 1

                      :: str "match"

                      :: Pretty.brk 1

                      :: (Pretty.block o Pretty.commas) dummy_parms

                      :: Pretty.brk 1

                      :: str "with"

                      :: Pretty.brk 1

                      :: pr_eq eq

                      :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]

                           o single o pr_eq) eqs'

                    )

                  end;

            fun pr_funn definer (name, ((vs, ty), eqs)) =

              concat (

                str definer

                :: (str o deresolve) name

                :: pr_tyvar_dicts (filter_out (null o snd) vs)

                @| pr_eqs name ty eqs

              );

            val (ps, p) = split_last

              (pr_funn "let rec" funn :: map (pr_funn "and") funns');

          in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end

     | pr_stmt (MLDatas (datas as (data :: datas'))) =

          let

            fun pr_co (co, []) =

                  str (deresolve co)

              | pr_co (co, tys) =

                  concat [

                    str (deresolve co),

                    str "of",

                    Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)

                  ];

            fun pr_data definer (tyco, (vs, [])) =

                  concat (

                    str definer

                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

                    :: str "="

                    @@ str "EMPTY_"

                  )

              | pr_data definer (tyco, (vs, cos)) =

                  concat (

                    str definer

                    :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)

                    :: str "="

                    :: separate (str "|") (map pr_co cos)

                  );

            val (ps, p) = split_last

              (pr_data "type" data :: map (pr_data "and") datas');

          in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end

     | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =

          let

            val w = "_" ^ Code_Name.first_upper v;

            fun pr_superclass_field (class, classrel) =

              (concat o map str) [

                deresolve classrel, ":", "'" ^ v, deresolve class

              ];

            fun pr_classparam_field (classparam, ty) =

              concat [

                (str o deresolve) classparam, str ":", pr_typ NOBR ty

              ];

            fun pr_classparam_proj (classparam, _) =

              concat [

                str "let",

                (str o deresolve) classparam,

                str w,

                str "=",

                str (w ^ "." ^ deresolve classparam ^ ";;")

              ];

          in Pretty.chunks (

            concat [

              str ("type '" ^ v),

              (str o deresolve) class,

              str "=",

              enum_default "();;" ";" "{" "};;" (

                map pr_superclass_field superclasses

                @ map pr_classparam_field classparams

              )

            ]

            :: map pr_classparam_proj classparams

          ) end

     | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =

          let

            fun pr_superclass (_, (classrel, dss)) =

              concat [

                (str o deresolve) classrel,

                str "=",

                pr_dicts NOBR [DictConst dss]

              ];

            fun pr_classparam_inst ((classparam, c_inst), (thm, _)) =

              concat [

                (str o deresolve) classparam,

                str "=",

                pr_app thm false reserved_names NOBR (c_inst, [])

              ];

          in

            concat (

              str "let"

              :: (str o deresolve) inst

              :: pr_tyvar_dicts arity

              @ str "="

              @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [

                enum_default "()" ";" "{" "}" (map pr_superclass superarities

                  @ map pr_classparam_inst classparam_insts),

                str ":",

                pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])

              ]

            )

          end;

  in pr_stmt end;

fun pr_ocaml_module name content =

  Pretty.chunks (

    str ("module " ^ name ^ " = ")

    :: str "struct"

    :: str ""

    :: content

    @ str ""

    @@ str ("end;; (*struct " ^ name ^ "*)")

  );

val literals_ocaml = let

  fun chr i =

    let

      val xs = string_of_int i;

      val ys = replicate_string (3 - length (explode xs)) "0";

    in "\\" ^ ys ^ xs end;

  fun char_ocaml c =

    let

      val i = ord c;

      val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126

        then chr i else c

    in s end;

in Literals {

  literal_char = enclose "'" "'" o char_ocaml,

  literal_string = quote o translate_string char_ocaml,

  literal_numeral = fn unbounded => fn k => if k >= 0 then

      if unbounded then

        "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"

      else string_of_int k

    else

      if unbounded then

        "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"

          o string_of_int o op ~) k ^ ")"

      else (enclose "(" ")" o prefix "-" o string_of_int o op ~) k,

  literal_list = Pretty.enum ";" "[" "]",

  infix_cons = (6, "::")

} end;

(** SML/OCaml generic part **)

local

datatype ml_node =

    Dummy of string

  | Stmt of string * ml_stmt

  | Module of string * ((Name.context * Name.context) * ml_node Graph.T);

in

fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =

  let

    val module_alias = if is_some module_name then K module_name else raw_module_alias;

    val reserved_names = Name.make_context reserved_names;

    val empty_module = ((reserved_names, reserved_names), Graph.empty);

    fun map_node [] f = f

      | map_node (m::ms) f =

          Graph.default_node (m, Module (m, empty_module))

          #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>

               Module (module_name, (nsp, map_node ms f nodes)));

    fun map_nsp_yield [] f (nsp, nodes) =

          let

            val (x, nsp') = f nsp

          in (x, (nsp', nodes)) end

      | map_nsp_yield (m::ms) f (nsp, nodes) =

          let

            val (x, nodes') =

              nodes

              |> Graph.default_node (m, Module (m, empty_module))

              |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) => 

                  let

                    val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes

                  in (x, Module (d_module_name, nsp_nodes')) end)

          in (x, (nsp, nodes')) end;

    fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =

      let

        val (x, nsp_fun') = f nsp_fun

      in (x, (nsp_fun', nsp_typ)) end;

    fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =

      let

        val (x, nsp_typ') = f nsp_typ

      in (x, (nsp_fun, nsp_typ')) end;

    val mk_name_module = Code_Name.mk_name_module reserved_names NONE module_alias program;

    fun mk_name_stmt upper name nsp =

      let

        val (_, base) = Code_Name.dest_name name;

        val base' = if upper then Code_Name.first_upper base else base;

        val ([base''], nsp') = Name.variants [base'] nsp;

      in (base'', nsp') end;

    fun add_funs stmts =

      fold_map

        (fn (name, Code_Thingol.Fun (_, stmt)) =>

              map_nsp_fun_yield (mk_name_stmt false name) #>>

                rpair (name, stmt |> apsnd (filter (snd o snd)))

          | (name, _) =>

              error ("Function block containing illegal statement: " ^ labelled_name name)

        ) stmts

      #>> (split_list #> apsnd MLFuns);

    fun add_datatypes stmts =

      fold_map

        (fn (name, Code_Thingol.Datatype (_, stmt)) =>

              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))

          | (name, Code_Thingol.Datatypecons _) =>

              map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE

          | (name, _) =>

              error ("Datatype block containing illegal statement: " ^ labelled_name name)

        ) stmts

      #>> (split_list #> apsnd (map_filter I

        #> (fn [] => error ("Datatype block without data statement: "

                  ^ (commas o map (labelled_name o fst)) stmts)

             | stmts => MLDatas stmts)));

    fun add_class stmts =

      fold_map

        (fn (name, Code_Thingol.Class (_, stmt)) =>

              map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))

          | (name, Code_Thingol.Classrel _) =>

              map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE

          | (name, Code_Thingol.Classparam _) =>

              map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE

          | (name, _) =>

              error ("Class block containing illegal statement: " ^ labelled_name name)

        ) stmts

      #>> (split_list #> apsnd (map_filter I

        #> (fn [] => error ("Class block without class statement: "

                  ^ (commas o map (labelled_name o fst)) stmts)

             | [stmt] => MLClass stmt)));

    fun add_inst [(name, Code_Thingol.Classinst stmt)] =

      map_nsp_fun_yield (mk_name_stmt false name)

      #>> (fn base => ([base], MLClassinst (name, stmt)));

    fun add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =

          add_funs stmts

      | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =

          add_datatypes stmts

      | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =

          add_datatypes stmts

      | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =

          add_class stmts

      | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =

          add_class stmts

      | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =

          add_class stmts

      | add_stmts ((stmts as [(_, Code_Thingol.Classinst _)])) =

          add_inst stmts

      | add_stmts stmts = error ("Illegal mutual dependencies: " ^

          (commas o map (labelled_name o fst)) stmts);

    fun add_stmts' stmts nsp_nodes =

      let

        val names as (name :: names') = map fst stmts;

        val deps =

          []

          |> fold (fold (insert (op =)) o Graph.imm_succs program) names

          |> subtract (op =) names;

        val (module_names, _) = (split_list o map Code_Name.dest_name) names;

        val module_name = (the_single o distinct (op =) o map mk_name_module) module_names

          handle Empty =>

            error ("Different namespace prefixes for mutual dependencies:\n"

              ^ commas (map labelled_name names)

              ^ "\n"

              ^ commas module_names);

        val module_name_path = NameSpace.explode module_name;

        fun add_dep name name' =

          let

            val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';

          in if module_name = module_name' then

            map_node module_name_path (Graph.add_edge (name, name'))

          else let

            val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)

              (module_name_path, NameSpace.explode module_name');

          in

            map_node common

              (fn node => Graph.add_edge_acyclic (diff1, diff2) node

                handle Graph.CYCLES _ => error ("Dependency "

                  ^ quote name ^ " -> " ^ quote name'

                  ^ " would result in module dependency cycle"))

          end end;

      in

        nsp_nodes

        |> map_nsp_yield module_name_path (add_stmts stmts)

        |-> (fn (base' :: bases', stmt') =>

           apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))

              #> fold2 (fn name' => fn base' =>

                   Graph.new_node (name', (Dummy base'))) names' bases')))

        |> apsnd (fold (fn name => fold (add_dep name) deps) names)

        |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)

      end;

    val (_, nodes) = empty_module

      |> fold add_stmts' (map (AList.make (Graph.get_node program))

          (rev (Graph.strong_conn program)));

    fun deresolver prefix name = 

      let

        val module_name = (fst o Code_Name.dest_name) name;

        val module_name' = (NameSpace.explode o mk_name_module) module_name;

        val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');

        val stmt_name =

          nodes

          |> fold (fn name => fn node => case Graph.get_node node name

              of Module (_, (_, node)) => node) module_name'

          |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name

               | Dummy stmt_name => stmt_name);

      in

        NameSpace.implode (remainder @ [stmt_name])

      end handle Graph.UNDEF _ =>

        error ("Unknown statement name: " ^ labelled_name name);

  in (deresolver, nodes) end;

fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias

  _ syntax_tyco syntax_const naming program cs destination =

  let

    val is_cons = Code_Thingol.is_cons program;

    val stmt_names = Code_Target.stmt_names_of_destination destination;

    val module_name = if null stmt_names then raw_module_name else SOME "Code";

    val (deresolver, nodes) = ml_node_of_program labelled_name module_name

      reserved_names raw_module_alias program;

    val reserved_names = Code_Name.make_vars reserved_names;

    fun pr_node prefix (Dummy _) =

          NONE

      | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse

          (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME

            (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names

              (deresolver prefix) is_cons stmt)

          else NONE

      | pr_node prefix (Module (module_name, (_, nodes))) =

          separate (str "")

            ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)

              o rev o flat o Graph.strong_conn) nodes)

          |> (if null stmt_names then pr_module module_name else Pretty.chunks)

          |> SOME;

    val cs' = (map o try)

      (deresolver (if is_some module_name then the_list module_name else [])) cs;

    val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter

      (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));

  in

    Code_Target.mk_serialization target

      (case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty) | NONE => NONE)

      (fn NONE => Code_Target.code_writeln | SOME file => File.write file o Code_Target.code_of_pretty)

      (rpair cs' o Code_Target.code_of_pretty) p destination

  end;

end; (*local*)

(** ML (system language) code for evaluation and instrumentalization **)

fun ml_code_of thy = Code_Target.serialize_custom thy (target_SML,

    (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""),

  literals_sml));

(* evaluation *)

fun eval eval'' term_of reff thy ct args =

  let

    val ctxt = ProofContext.init thy;

    val _ = if null (term_frees (term_of ct)) then () else error ("Term "

      ^ quote (Syntax.string_of_term_global thy (term_of ct))

      ^ " to be evaluated contains free variables");

    fun eval' naming program ((vs, ty), t) deps =

      let

        val _ = if Code_Thingol.contains_dictvar t then

          error "Term to be evaluated constains free dictionaries" else ();

        val value_name = "Value.VALUE.value"

        val program' = program

          |> Graph.new_node (value_name,

              Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))

          |> fold (curry Graph.add_edge value_name) deps;

        val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];

        val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'

          ^ space_implode " " (map (enclose "(" ")") args) ^ " end";

      in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;

  in eval'' thy (fn t => (t, eval')) ct end;

fun eval_conv reff = eval Code_Thingol.eval_conv Thm.term_of reff;

fun eval_term reff = eval Code_Thingol.eval_term I reff;

(* instrumentalization by antiquotation *)

local

structure CodeAntiqData = ProofDataFun

(

  type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));

  fun init _ = ([], (true, ("", Lazy.value ("", []))));

);

val is_first_occ = fst o snd o CodeAntiqData.get;

fun delayed_code thy consts () =

  let

    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;

    val (ml_code, consts'') = ml_code_of thy naming program consts';

    val const_tab = map2 (fn const => fn NONE =>

      error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const

        ^ "\nhas a user-defined serialization")

      | SOME const' => (const, const')) consts consts''

  in (ml_code, const_tab) end;

fun register_const const ctxt =

  let

    val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;

    val consts' = insert (op =) const consts;

    val (struct_name', ctxt') = if struct_name = ""

      then ML_Antiquote.variant "Code" ctxt

      else (struct_name, ctxt);

    val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) consts');

  in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;

fun print_code struct_name is_first const ctxt =

  let

    val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;

    val (raw_ml_code, consts_map) = Lazy.force acc_code;

    val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)

      ((the o AList.lookup (op =) consts_map) const);

    val ml_code = if is_first then "\nstructure " ^ struct_code_name

        ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"

      else "";

  in (ml_code, const'') end;

in

fun ml_code_antiq raw_const {struct_name, background} =

  let

    val const = Code_Unit.check_const (ProofContext.theory_of background) raw_const;

    val is_first = is_first_occ background;

    val background' = register_const const background;

  in (print_code struct_name is_first const, background') end;

end; (*local*)

(** Isar setup **)

val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);

fun isar_seri_sml module_name =

  Code_Target.parse_args (Scan.succeed ())

  #> (fn () => serialize_ml target_SML

      (SOME (use_text ML_Context.name_space (1, "generated code") Output.ml_output false))

      pr_sml_module pr_sml_stmt module_name);

fun isar_seri_ocaml module_name =

  Code_Target.parse_args (Scan.succeed ())

  #> (fn () => serialize_ml target_OCaml NONE

      pr_ocaml_module pr_ocaml_stmt module_name);

val setup =

  Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))

  #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))

  #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>

      brackify_infix (1, R) fxy [

        pr_typ (INFX (1, X)) ty1,

        str "->",

        pr_typ (INFX (1, R)) ty2

      ]))

  #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>

      brackify_infix (1, R) fxy [

        pr_typ (INFX (1, X)) ty1,