(*  Title:      Tools/code/code_target.ML

    ID:         $Id$

    Author:     Florian Haftmann, TU Muenchen

Serializer from intermediate language ("Thin-gol")

to target languages (like SML or Haskell).

*)

signature CODE_TARGET =

sig

  include BASIC_CODE_THINGOL;

  val add_syntax_class: string -> class

    -> (string * (string * string) list) option -> theory -> theory;

  val add_syntax_inst: string -> string * class -> bool -> theory -> theory;

  val add_syntax_tycoP: string -> string -> OuterParse.token list

    -> (theory -> theory) * OuterParse.token list;

  val add_syntax_constP: string -> string -> OuterParse.token list

    -> (theory -> theory) * OuterParse.token list;

  val add_undefined: string -> string -> string -> theory -> theory;

  val add_pretty_list: string -> string -> string -> theory -> theory;

  val add_pretty_list_string: string -> string -> string

    -> string -> string list -> theory -> theory;

  val add_pretty_char: string -> string -> string list -> theory -> theory

  val add_pretty_numeral: string -> bool -> bool -> string -> string -> string

    -> string -> string -> theory -> theory;

  val add_pretty_message: string -> string -> string list -> string

    -> string -> string -> theory -> theory;

  val allow_exception: string -> theory -> theory;

  type serialization;

  type serializer;

  val add_serializer: string * serializer -> theory -> theory;

  val assert_serializer: theory -> string -> string;

  val serialize: theory -> string -> bool -> string option -> Args.T list

    -> CodeThingol.code -> string list option -> serialization;

  val compile: serialization -> unit;

  val write: serialization -> unit;

  val file: Path.T -> serialization -> unit;

  val string: serialization -> string;

  val sml_of: theory -> CodeThingol.code -> string list -> string;

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

    -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;

  val target_code_width: int ref;

  val setup: theory -> theory;

end;

structure CodeTarget : CODE_TARGET =

struct

open BasicCodeThingol;

(** basics **)

infixr 5 @@;

infixr 5 @|;

fun x @@ y = [x, y];

fun xs @| y = xs @ [y];

val str = PrintMode.setmp [] Pretty.str;

val concat = Pretty.block o Pretty.breaks;

val brackets = Pretty.enclose "(" ")" o Pretty.breaks;

fun semicolon ps = Pretty.block [concat ps, str ";"];

fun enum_default default sep opn cls [] = str default

  | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;

datatype destination = Compile | Write | File of Path.T | String;

type serialization = destination -> string option;

val target_code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)

fun target_code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!target_code_width) f);

fun target_code_of_pretty p = target_code_setmp Pretty.string_of p ^ "\n";

fun target_code_writeln p = Pretty.setmp_margin (!target_code_width) Pretty.writeln p;

(*FIXME why another target_code_setmp?*)

fun compile f = (target_code_setmp f Compile; ());

fun write f = (target_code_setmp f Write; ());

fun file p f = (target_code_setmp f (File p); ());

fun string f = the (target_code_setmp f String);

(** generic syntax **)

datatype lrx = L | R | X;

datatype fixity =

    BR

  | NOBR

  | INFX of (int * lrx);

val APP = INFX (~1, L);

fun fixity_lrx L L = false

  | fixity_lrx R R = false

  | fixity_lrx _ _ = true;

fun fixity NOBR _ = false

  | fixity _ NOBR = false

  | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =

      pr < pr_ctxt

      orelse pr = pr_ctxt

        andalso fixity_lrx lr lr_ctxt

      orelse pr_ctxt = ~1

  | fixity BR (INFX _) = false

  | fixity _ _ = true;

fun gen_brackify _ [p] = p

  | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps

  | gen_brackify false (ps as _::_) = Pretty.block ps;

fun brackify fxy_ctxt =

  gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;

fun brackify_infix infx fxy_ctxt =

  gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;

type class_syntax = string * (string -> string option);

type typ_syntax = int * ((fixity -> itype -> Pretty.T)

  -> fixity -> itype list -> Pretty.T);

type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)

  -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);

(** theory data **)

val target_diag = "diag";

val target_SML = "SML";

val target_OCaml = "OCaml";

val target_Haskell = "Haskell";

datatype name_syntax_table = NameSyntaxTable of {

  class: (string * (string -> string option)) Symtab.table,

  inst: unit Symtab.table,

  tyco: typ_syntax Symtab.table,

  const: term_syntax Symtab.table

};

fun mk_name_syntax_table ((class, inst), (tyco, const)) =

  NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };

fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =

  mk_name_syntax_table (f ((class, inst), (tyco, const)));

fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },

    NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =

  mk_name_syntax_table (

    (Symtab.join (K snd) (class1, class2),

       Symtab.join (K snd) (inst1, inst2)),

    (Symtab.join (K snd) (tyco1, tyco2),

       Symtab.join (K snd) (const1, const2))

  );

type serializer = (*FIXME order of arguments*)

  string option                         (*module name*)

  -> Args.T list                        (*arguments*)

  -> (string -> string)                 (*labelled_name*)

  -> string list                        (*reserved symbols*)

  -> (string * Pretty.T) list           (*includes*)

  -> (string -> string option)          (*module aliasses*)

  -> (string -> class_syntax option)

  -> (string -> typ_syntax option)

  -> (string -> term_syntax option)

  -> CodeThingol.code                   (*program*)

  -> string list                        (*selected statements*)

  -> serialization;

datatype target = Target of {

  serial: serial,

  serializer: serializer,

  reserved: string list,

  includes: Pretty.T Symtab.table,

  name_syntax_table: name_syntax_table,

  module_alias: string Symtab.table

};

fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =

  Target { serial = serial, serializer = serializer, reserved = reserved, 

    includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };

fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =

  mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));

fun merge_target target (Target { serial = serial1, serializer = serializer,

  reserved = reserved1, includes = includes1,

  name_syntax_table = name_syntax_table1, module_alias = module_alias1 },

    Target { serial = serial2, serializer = _,

      reserved = reserved2, includes = includes2,

      name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =

  if serial1 = serial2 then

    mk_target ((serial1, serializer),

      ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),

        (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),

          Symtab.join (K snd) (module_alias1, module_alias2))

    ))

  else

    error ("Incompatible serializers: " ^ quote target);

structure CodeTargetData = TheoryDataFun

(

  type T = target Symtab.table * string list;

  val empty = (Symtab.empty, []);

  val copy = I;

  val extend = I;

  fun merge _ ((target1, exc1) : T, (target2, exc2)) =

    (Symtab.join merge_target (target1, target2), Library.merge (op =) (exc1, exc2));

);

fun the_serializer (Target { serializer, ... }) = serializer;

fun the_reserved (Target { reserved, ... }) = reserved;

fun the_includes (Target { includes, ... }) = includes;

fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;

fun the_module_alias (Target { module_alias , ... }) = module_alias;

fun assert_serializer thy target =

  case Symtab.lookup (fst (CodeTargetData.get thy)) target

   of SOME data => target

    | NONE => error ("Unknown code target language: " ^ quote target);

fun add_serializer (target, seri) thy =

  let

    val _ = case Symtab.lookup (fst (CodeTargetData.get thy)) target

     of SOME _ => warning ("Overwriting existing serializer " ^ quote target)

      | NONE => ();

  in

    thy

    |> (CodeTargetData.map o apfst oo Symtab.map_default)

          (target, mk_target ((serial (), seri), (([], Symtab.empty),

            (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),

              Symtab.empty))))

          ((map_target o apfst o apsnd o K) seri)

  end;

fun map_seri_data target f thy =

  let

    val _ = assert_serializer thy target;

  in

    thy

    |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f

  end;

fun map_adaptions target =

  map_seri_data target o apsnd o apfst;

fun map_name_syntax target =

  map_seri_data target o apsnd o apsnd o apfst o map_name_syntax_table;

fun map_module_alias target =

  map_seri_data target o apsnd o apsnd o apsnd;

fun get_serializer get_seri thy target permissive =

  let

    val (seris, exc) = CodeTargetData.get thy;

    val data = case Symtab.lookup seris target

     of SOME data => data

      | NONE => error ("Unknown code target language: " ^ quote target);

    val seri = get_seri data;

    val reserved = the_reserved data;

    val includes = Symtab.dest (the_includes data);

    val alias = the_module_alias data;

    val { class, inst, tyco, const } = the_name_syntax data;

    val project = if target = target_diag then K I

      else CodeThingol.project_code permissive

        (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const);

    fun check_empty_funs code = case filter_out (member (op =) exc)

        (CodeThingol.empty_funs code)

     of [] => code

      | names => error ("No defining equations for "

          ^ commas (map (CodeName.labelled_name thy) names));

  in fn module => fn args => fn code => fn cs =>

    seri module args (CodeName.labelled_name thy) reserved includes

      (Symtab.lookup alias) (Symtab.lookup class)

      (Symtab.lookup tyco) (Symtab.lookup const)

        ((check_empty_funs o project cs) code) (these cs)

  end;

val serialize = get_serializer the_serializer;

fun parse_args f args =

  case Scan.read Args.stopper f args

   of SOME x => x

    | NONE => error "Bad serializer arguments";

(** generic output combinators **)

(* applications and bindings *)

fun gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons

      lhs vars fxy (app as ((c, (_, tys)), ts)) =

  case const_syntax c

   of NONE => if lhs andalso not (is_cons c) then

          error ("Non-constructor on left hand side of equation: " ^ labelled_name c)

        else brackify fxy (pr_app' lhs vars app)

    | SOME (i, pr) =>

        let

          val k = if i < 0 then length tys else i;

          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);

        in if k = length ts

          then pr' fxy ts

        else if k < length ts

          then case chop k ts of (ts1, ts2) =>

            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)

          else pr_term lhs vars fxy (CodeThingol.eta_expand app k)

        end;

fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars =

  let

    val vs = case pat

     of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []

      | NONE => [];

    val vars' = CodeName.intro_vars (the_list v) vars;

    val vars'' = CodeName.intro_vars vs vars';

    val v' = Option.map (CodeName.lookup_var vars') v;

    val pat' = Option.map (pr_term true vars'' fxy) pat;

  in (pr_bind' ((v', pat'), ty), vars'') end;

(* list, char, string, numeral and monad abstract syntax transformations *)

fun implode_list c_nil c_cons t =

  let

    fun dest_cons (IConst (c, _) `$ t1 `$ t2) =

          if c = c_cons

          then SOME (t1, t2)

          else NONE

      | dest_cons _ = NONE;

    val (ts, t') = CodeThingol.unfoldr dest_cons t;

  in case t'

   of IConst (c, _) => if c = c_nil then SOME ts else NONE

    | _ => NONE

  end;

fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =

      let

        fun idx c = find_index (curry (op =) c) c_nibbles;

        fun decode ~1 _ = NONE

          | decode _ ~1 = NONE

          | decode n m = SOME (chr (n * 16 + m));

      in decode (idx c1) (idx c2) end

  | decode_char _ _ = NONE;

fun implode_string c_char c_nibbles mk_char mk_string ts =

  let

    fun implode_char (IConst (c, _) `$ t1 `$ t2) =

          if c = c_char then decode_char c_nibbles (t1, t2) else NONE

      | implode_char _ = NONE;

    val ts' = map implode_char ts;

  in if forall is_some ts'

    then (SOME o str o mk_string o implode o map_filter I) ts'

    else NONE

  end;

fun implode_numeral negative c_pls c_min c_bit0 c_bit1 =

  let

    fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0

          else if c = c_bit1 then 1

          else error "Illegal numeral expression: illegal bit"

      | dest_bit _ = error "Illegal numeral expression: illegal bit";

    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0

          else if c = c_min then

            if negative then SOME ~1 else NONE

          else error "Illegal numeral expression: illegal leading digit"

      | dest_numeral (t1 `$ t2) =

          let val (n, b) = (dest_numeral t2, dest_bit t1)

          in case n of SOME n => SOME (2 * n + b) | NONE => NONE end

      | dest_numeral _ = error "Illegal numeral expression: illegal constant";

  in dest_numeral #> the_default 0 end;

fun implode_monad c_bind t =

  let

    fun dest_monad (IConst (c, _) `$ t1 `$ t2) =

          if c = c_bind

            then case CodeThingol.split_abs t2

             of SOME (((v, pat), ty), t') =>

                  SOME ((SOME (((SOME v, pat), ty), true), t1), t')

              | NONE => NONE

            else NONE

      | dest_monad t = case CodeThingol.split_let t

           of SOME (((pat, ty), tbind), t') =>

                SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')

            | NONE => NONE;

  in CodeThingol.unfoldr dest_monad t end;

(* name auxiliary *)

val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;

val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;

val dest_name =

  apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;

fun mk_modl_name_tab init_names prefix module_alias code =

  let

    fun nsp_map f = NameSpace.explode #> map f #> NameSpace.implode;

    fun mk_alias name =

     case module_alias name

      of SOME name' => name'

       | NONE => nsp_map (fn name => (the_single o fst)

            (Name.variants [name] init_names)) name;

    fun mk_prefix name =

      case prefix

       of SOME prefix => NameSpace.append prefix name

        | NONE => name;

    val tab =

      Symtab.empty

      |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))

           o fst o dest_name o fst)

             code

  in fn name => (the o Symtab.lookup tab) name end;

(** SML/OCaml serializer **)

datatype ml_def =

    MLFuns of (string * (typscheme * (iterm list * iterm) 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) list));

fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =

  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)) = first_upper v ^ "_"

          | pr_dictvar (v, (i, _)) = 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_dictc fxy (DictConst (inst, dss)) =

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

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

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

      in case ds

       of [] => str "()"

        | [d] => pr_dictc fxy d

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

      end;

    fun pr_tyvars 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 deresolv) 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 tyco_syntax tyco

           of NONE => pr_tycoexpr fxy (tyco, tys)

            | SOME (i, pr) =>

                if not (i = length tys)

                then error ("Number of argument mismatch in customary serialization: "

                  ^ (string_of_int o length) tys ^ " given, "

                  ^ string_of_int i ^ " expected")

                else pr pr_typ fxy tys)

      | pr_typ fxy (ITyVar v) =

          str ("'" ^ v);

    fun pr_term lhs vars fxy (IConst c) =

          pr_app lhs vars fxy (c, [])

      | pr_term lhs vars fxy (IVar v) =

          str (CodeName.lookup_var vars v)

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

          (case CodeThingol.unfold_const_app t

           of SOME c_ts => pr_app lhs vars fxy c_ts

            | NONE =>

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

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

          let

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

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

              pr_bind 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 lhs vars' NOBR t']) end

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

          (case CodeThingol.unfold_const_app t0

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

                then pr_case vars fxy cases

                else pr_app lhs vars fxy c_ts

            | NONE => pr_case vars fxy cases)

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

      if is_cons c then let

        val k = length tys

      in if k < 2 then 

        (str o deresolv) c :: map (pr_term lhs vars BR) ts

      else if k = length ts then

        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]

      else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else

        (str o deresolv) c

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

    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax

      labelled_name is_cons lhs 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 fxy = gen_pr_bind pr_bind' pr_term fxy

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

          let

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

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

              vars

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

              |>> (fn p => semicolon [str "val", p, str "=", pr_term 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 false vars' NOBR t'] |> Pretty.block,

              str ("end")

            ]

          end

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

          let

            fun pr delim (pat, t) =

              let

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

              in

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

              end;

          in

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

              str "case"

              :: pr_term false vars NOBR td

              :: pr "of" b

              :: map (pr "|") bs

            )

          end

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

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

          let

            val definer =

              let

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

                  | no_args ty [] = (length o fst o CodeThingol.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, ((raw_vs, ty), [])) =

                  let

                    val vs = filter_out (null o snd) raw_vs;

                    val n = length vs + (length o fst o CodeThingol.unfold_fun) ty;

                    val exc_str =

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

                  in

                    concat (

                      str definer

                      :: (str o deresolv) name

                      :: map str (replicate n "_")

                      @ str "="

                      :: str "raise"

                      :: str "(Fail"

                      :: str exc_str

                      @@ str ")"

                    )

                  end

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

                  let

                    val vs = filter_out (null o snd) raw_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) =

                      let

                        val consts = map_filter

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

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

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

                        val vars = init_syms

                          |> CodeName.intro_vars consts

                          |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)

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

                      in

                        concat (

                          [str definer, (str o deresolv) name]

                          @ (if null ts andalso null vs

                             then [str ":", pr_typ NOBR ty]

                             else

                               pr_tyvars vs

                               @ map (pr_term true vars BR) ts)

                       @ [str "=", pr_term 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_def (MLDatas (datas as (data :: datas'))) =

          let

            fun pr_co (co, []) =

                  str (deresolv co)

              | pr_co (co, tys) =

                  concat [

                    str (deresolv 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_def (MLClass (class, (v, (superclasses, classparams)))) =

          let

            val w = first_upper v ^ "_";

            fun pr_superclass_field (class, classrel) =

              (concat o map str) [

                pr_label_classrel classrel, ":", "'" ^ v, deresolv 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 deresolv) classparam,

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

                str "=",

                str ("#" ^ pr_label_classparam classparam),

                str w

              ];

            fun pr_superclass_proj (_, classrel) =

              semicolon [

                str "fun",

                (str o deresolv) classrel,

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

                str "=",

                str ("#" ^ pr_label_classrel classrel),

                str w

              ];

          in

            Pretty.chunks (

              concat [

                str ("type '" ^ v),

                (str o deresolv) 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_def (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) =

              concat [

                (str o pr_label_classparam) classparam,

                str "=",

                pr_app false init_syms NOBR (c_inst, [])

              ];

          in

            semicolon ([

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

              (str o deresolv) inst ] @

              pr_tyvars 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_def ml_def end;

fun pr_sml_modl name content =

  Pretty.chunks ([

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

    str "struct",

    str ""

  ] @ content @ [

    str "",

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

  ]);

fun pr_ocaml tyco_syntax const_syntax labelled_name

    init_syms deresolv is_cons ml_def =

  let

    fun pr_dicts fxy ds =

      let

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

          | pr_dictvar (v, (i, _)) = "_" ^ 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_dictc fxy (DictConst (inst, dss)) =

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

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

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

      in case ds

       of [] => str "()"

        | [d] => pr_dictc fxy d

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

      end;

    fun pr_tyvars 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 deresolv) 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 tyco_syntax tyco

           of NONE => pr_tycoexpr fxy (tyco, tys)

            | SOME (i, pr) =>

                if not (i = length tys)

                then error ("Number of argument mismatch in customary serialization: "

                  ^ (string_of_int o length) tys ^ " given, "

                  ^ string_of_int i ^ " expected")

                else pr pr_typ fxy tys)

      | pr_typ fxy (ITyVar v) =

          str ("'" ^ v);

    fun pr_term lhs vars fxy (IConst c) =

          pr_app lhs vars fxy (c, [])

      | pr_term lhs vars fxy (IVar v) =

          str (CodeName.lookup_var vars v)

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

          (case CodeThingol.unfold_const_app t

           of SOME c_ts => pr_app lhs vars fxy c_ts

            | NONE =>

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

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

          let

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

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

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

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

      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0

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

                then pr_case vars fxy cases

                else pr_app lhs vars fxy c_ts

            | NONE => pr_case vars fxy cases)

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

      if is_cons c then

        if length tys = length ts

        then case ts

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

          | [t] => [(str o deresolv) c, pr_term lhs vars BR t]

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

                    (map (pr_term lhs vars NOBR) ts)]

        else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))]

      else (str o deresolv) c

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

    and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax

      labelled_name is_cons lhs 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 fxy = gen_pr_bind pr_bind' pr_term fxy

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

          let

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

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

              vars

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

              |>> (fn p => concat

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

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

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

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

          let

            fun pr delim (pat, t) =

              let

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

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

          in

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

              str "match"

              :: pr_term false vars NOBR td

              :: pr "with" b

              :: map (pr "|") bs

            )

          end

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

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

          let

            fun fish_parm _ (w as SOME _) = w

              | fish_parm (IVar v) NONE = SOME v

              | fish_parm _ NONE = NONE;

            fun fillup_parm _ (_, SOME v) = v

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

            fun fish_parms vars eqs =

              let

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

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

                val fished2 = map_index (fillup_parm x) fished1;

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

                val vars' = CodeName.intro_vars fished3 vars;

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

            fun pr_eq (ts, t) =

              let

                val consts = map_filter

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

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

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

                val vars = init_syms

                  |> CodeName.intro_vars consts

                  |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)

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

              in concat [

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

                str "->",

                pr_term false vars NOBR t

              ] end;

            fun pr_eqs name ty [] =

                  let

                    val n = (length o fst o CodeThingol.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)] =

                  let

                    val consts = map_filter

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

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

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

                    val vars = init_syms

                      |> CodeName.intro_vars consts

                      |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)

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

                  in

                    concat (

                      map (pr_term true vars BR) ts

                      @ str "="

                      @@ pr_term 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 const_syntax) c

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

                        ((fold o CodeThingol.fold_constnames)

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

                    val vars = init_syms

                      |> CodeName.intro_vars consts;

                    val dummy_parms = (map str o fish_parms vars o map 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 deresolv) name

                :: pr_tyvars (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_def (MLDatas (datas as (data :: datas'))) =

          let

            fun pr_co (co, []) =

                  str (deresolv co)

              | pr_co (co, tys) =

                  concat [

                    str (deresolv 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_def (MLClass (class, (v, (superclasses, classparams)))) =

          let

            val w = "_" ^ first_upper v;

            fun pr_superclass_field (class, classrel) =

              (concat o map str) [

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

              ];

            fun pr_classparam_field (classparam, ty) =

              concat [

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

              ];

            fun pr_classparam_proj (classparam, _) =

              concat [

                str "let",

                (str o deresolv) classparam,

                str w,

                str "=",

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

              ];

          in Pretty.chunks (

            concat [

              str ("type '" ^ v),

              (str o deresolv) class,

              str "=",

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

                map pr_superclass_field superclasses

                @ map pr_classparam_field classparams

              )

            ]

            :: map pr_classparam_proj classparams

          ) end

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

          let

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

              concat [

                (str o deresolv) classrel,

                str "=",

                pr_dicts NOBR [DictConst dss]

              ];