(*  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_abort: string -> theory -> theory;

  type serialization;

  type serializer;

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

  val extend_target: string * (string * (CodeThingol.program -> CodeThingol.program))

    -> theory -> theory;

  val assert_target: theory -> string -> string;

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

    -> CodeThingol.program -> string list -> serialization;

  val compile: serialization -> unit;

  val export: serialization -> unit;

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

  val string: string list -> serialization -> string;

  val code_of: theory -> string -> string -> string list -> string list -> string;

  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 shell_command: string (*theory name*) -> string (*cg expr*) -> unit;

  val setup: theory -> theory;

  val code_width: int ref;

  val ml_code_of: theory -> CodeThingol.program -> string list -> string * string list;

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 | Export | File of Path.T | String of string list;

type serialization = destination -> (string * string list) option;

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

fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);

fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";

fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;

(*FIXME why another code_setmp?*)

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

fun export f = (code_setmp f Export; ());

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

fun string cs f = fst (the (code_setmp f (String cs)));

fun stmt_names_of_destination (String stmts) = stmts

  | stmt_names_of_destination _ = [];

(** 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)

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

datatype name_syntax_table = NameSyntaxTable of {

  class: class_syntax Symtab.table,

  inst: unit Symtab.table,

  tyco: typ_syntax Symtab.table,

  const: term_syntax Symtab.table

};

(** theory data **)

val target_SML = "SML";

val target_OCaml = "OCaml";

val target_Haskell = "Haskell";

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 =

  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.program

  -> string list                        (*selected statements*)

  -> serialization;

datatype serializer_entry = Serializer of serializer

  | Extends of string * (CodeThingol.program -> CodeThingol.program);

datatype target = Target of {

  serial: serial,

  serializer: serializer_entry,

  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 strict 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 orelse not strict 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 true) (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;

val abort_allowed = snd o CodeTargetData.get;

fun assert_target thy target =

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

   of SOME data => target

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

fun put_target (target, seri) thy =

  let

    val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));

    val _ = case seri

     of Extends (super, _) => if defined_target super then ()

          else error ("Unknown code target language: " ^ quote super)

      | _ => ();

    val _ = if defined_target target

      then warning ("Overwriting existing target " ^ quote target)

      else ();

  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 add_target (target, seri) = put_target (target, Serializer seri);

fun extend_target (target, (super, modify)) =

  put_target (target, Extends (super, modify));

fun map_target_data target f thy =

  let

    val _ = assert_target thy target;

  in

    thy

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

  end;

fun map_reserved target =

  map_target_data target o apsnd o apfst o apfst;

fun map_includes target =

  map_target_data target o apsnd o apfst o apsnd;

fun map_name_syntax target =

  map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;

fun map_module_alias target =

  map_target_data target o apsnd o apsnd o apsnd;

fun invoke_serializer thy modify abortable serializer reserved includes 

    module_alias class inst tyco const module args program1 cs1 =

  let

    val program2 = modify program1;

    val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;

    val cs2 = subtract (op =) hidden cs1;

    val program3 = Graph.subgraph (not o member (op =) hidden) program2;

    val all_cs = Graph.all_succs program2 cs2;

    val program4 = Graph.subgraph (member (op =) all_cs) program3;

    val empty_funs = filter_out (member (op =) abortable)

      (CodeThingol.empty_funs program3);

    val _ = if null empty_funs then () else error ("No defining equations for "

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

  in

    serializer module args (CodeName.labelled_name thy) reserved includes

      (Symtab.lookup module_alias) (Symtab.lookup class)

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

      program4 cs2

  end;

fun mount_serializer thy alt_serializer target =

  let

    val (targets, abortable) = CodeTargetData.get thy;

    fun collapse_hierarchy target =

      let

        val data = case Symtab.lookup targets target

         of SOME data => data

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

      in case the_serializer data

       of Serializer _ => (I, data)

        | Extends (super, modify) => let

            val (modify', data') = collapse_hierarchy super

          in (modify' #> modify, merge_target false target (data', data)) end

      end;

    val (modify, data) = collapse_hierarchy target;

    val serializer = the_default (case the_serializer data

     of Serializer seri => seri) alt_serializer;

    val reserved = the_reserved data;

    val includes = Symtab.dest (the_includes data);

    val module_alias = the_module_alias data;

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

  in

    invoke_serializer thy modify abortable serializer reserved

      includes module_alias class inst tyco const

  end;

fun serialize thy = mount_serializer thy NONE;

fun parse_args f args =

  case Scan.read OuterLex.stopper f args

   of SOME x => x

    | NONE => error "Bad serializer arguments";

(** generic code combinators **)

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

fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);

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 thm 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 nerror thm "Illegal numeral expression: illegal bit"

      | dest_bit _ = nerror thm "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 nerror thm "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 _ = nerror thm "Illegal numeral expression: illegal term";

  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;

(* applications and bindings *)

fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat

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

  case syntax_const c

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

        nerror thm "Non-constructor in pattern"

        else brackify fxy (pr_app thm pat vars app)

    | SOME (i, pr) =>

        let

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

          fun pr' fxy ts = pr (pr_term thm pat) thm pat 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 thm pat vars BR) ts2)

          else pr_term thm pat vars fxy (CodeThingol.eta_expand k app)

        end;

fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) 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 thm true vars'' fxy) pat;

  in (pr_bind ((v', pat'), ty), vars'') 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_name_module reserved_names module_prefix module_alias program =

  let

    fun mk_alias name = case module_alias name

     of SOME name' => name'

      | NONE => name

          |> NameSpace.explode

          |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))

          |> NameSpace.implode;

    fun mk_prefix name = case module_prefix

     of SOME module_prefix => NameSpace.append module_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)

             program

  in the o Symtab.lookup tab end;

(** SML/OCaml serializer **)

datatype ml_stmt =

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

fun pr_sml_stmt syntax_tyco syntax_const labelled_name 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)) = 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_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 (CodeName.lookup_var vars v)

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

          (case CodeThingol.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') = CodeThingol.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 CodeThingol.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 (CodeThingol.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 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') = CodeThingol.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 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, ((vs, ty), [])) =

                  let

                    val vs_dict = filter_out (null o snd) vs;

                    val n = length vs_dict + (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 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 CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);

                        val vars = reserved_names

                          |> CodeName.intro_vars consts

                          |> CodeName.intro_vars ((fold o CodeThingol.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 = 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 ^ "*)")

  );

fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =

  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_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 (CodeName.lookup_var vars v)

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

          (case CodeThingol.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') = CodeThingol.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 CodeThingol.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 (CodeThingol.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 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') = CodeThingol.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' = CodeName.intro_vars fished3 vars;

      in map (CodeName.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 CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);

                val vars = reserved_names

                  |> 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 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 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), 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 CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);

                    val vars = reserved_names

                      |> CodeName.intro_vars consts

                      |> CodeName.intro_vars ((fold o CodeThingol.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 CodeThingol.fold_constnames)

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

                    val vars = reserved_names

                      |> CodeName.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 = "_" ^ first_upper v;

            fun pr_superclass_field (class, classrel) =

              (concat o map str) [