(*  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 * (CodeUnit.const * 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 -> string * typ -> string -> string -> string

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

  val add_pretty_ml_string: string -> string -> string list -> string

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

  val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;

  type serializer;

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

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

    -> (theory -> string -> string) -> string list option -> CodeThingol.code -> unit;

  val assert_serializer: theory -> string -> string;

  val eval_verbose: bool ref;

  val eval_term: theory -> (theory -> string -> string) -> CodeThingol.code

    -> (string * 'a option ref) * CodeThingol.iterm -> string list -> 'a;

  val 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.with_default Pretty.str;

val concat = Pretty.block o Pretty.breaks;

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

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

(** syntax **)

datatype lrx = L | R | X;

datatype fixity =

    BR

  | NOBR

  | INFX of (int * lrx);

val APP = INFX (~1, L);

fun eval_lrx L L = false

  | eval_lrx R R = false

  | eval_lrx _ _ = true;

fun eval_fxy NOBR NOBR = false

  | eval_fxy BR NOBR = false

  | eval_fxy NOBR BR = false

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

      pr < pr_ctxt

      orelse pr = pr_ctxt

        andalso eval_lrx lr lr_ctxt

      orelse pr_ctxt = ~1

  | eval_fxy _ (INFX _) = false

  | eval_fxy (INFX _) NOBR = false

  | eval_fxy _ _ = 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 ps =

  gen_brackify (eval_fxy BR fxy_ctxt) (Pretty.breaks ps);

fun brackify_infix infx fxy_ctxt ps =

  gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);

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);

(* user-defined syntax *)

datatype 'a mixfix =

    Arg of fixity

  | Pretty of Pretty.T;

fun mk_mixfix prep_arg (fixity_this, mfx) =

  let

    fun is_arg (Arg _) = true

      | is_arg _ = false;

    val i = (length o filter is_arg) mfx;

    fun fillin _ [] [] =

          []

      | fillin pr (Arg fxy :: mfx) (a :: args) =

          (pr fxy o prep_arg) a :: fillin pr mfx args

      | fillin pr (Pretty p :: mfx) args =

          p :: fillin pr mfx args

      | fillin _ [] _ =

          error ("Inconsistent mixfix: too many arguments")

      | fillin _ _ [] =

          error ("Inconsistent mixfix: too less arguments");

  in

    (i, fn pr => fn fixity_ctxt => fn args =>

      gen_brackify (eval_fxy fixity_this fixity_ctxt) (fillin pr mfx args))

  end;

fun parse_infix prep_arg (x, i) s =

  let

    val l = case x of L => INFX (i, L) | _ => INFX (i, X);

    val r = case x of R => INFX (i, R) | _ => INFX (i, X);

  in

    mk_mixfix prep_arg (INFX (i, x), [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])

  end;

fun parse_mixfix prep_arg s =

  let

    val sym_any = Scan.one Symbol.is_regular;

    val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (

         ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))

      || ($$ "_" >> K (Arg BR))

      || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))

      || (Scan.repeat1

           (   $$ "'" |-- sym_any

            || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")

                 sym_any) >> (Pretty o str o implode)));

  in case Scan.finite Symbol.stopper parse (Symbol.explode s)

   of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)

    | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)

    | _ => Scan.!! (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()

  end;

fun parse_args f args =

  case Scan.read Args.stopper f args

   of SOME x => x

    | NONE => error "Bad serializer arguments";

(* generic serializer combinators *)

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 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 c_bit0 c_bit1 c_pls c_min c_bit =

  let

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

          else if c = c_bit1 then SOME 1

          else NONE

      | dest_bit _ = NONE;

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

          else if c = c_min then SOME (IntInf.fromInt ~1)

          else NONE

      | dest_numeral (IConst (c, _) `$ t1 `$ t2) =

          if c = c_bit then case (dest_numeral t1, dest_bit t2)

           of (SOME n, SOME b) => SOME (IntInf.fromInt 2 * n + IntInf.fromInt b)

            | _ => NONE

          else NONE

      | dest_numeral _ = NONE;

  in dest_numeral end;

fun implode_monad c_mbind c_kbind t =

  let

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

          if c = c_mbind

            then case CodeThingol.split_abs t2

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

              | NONE => NONE

          else if c = c_kbind

            then SOME ((NONE, t1), t2)

            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 * ((iterm list * iterm) list * typscheme)) list

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

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

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

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

      * (string * iterm) 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_classop = 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 false) 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 mk [] [] = "val"

                  | mk (_::_) _ = "fun"

                  | mk [] vs = if (null o filter_out (null o snd)) vs then "val" else "fun";

                fun chk (_, ((ts, _) :: _, (vs, _))) NONE = SOME (mk ts vs)

                  | chk (_, ((ts, _) :: _, (vs, _))) (SOME defi) =

                      if defi = mk ts 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, (eqs as eq::eqs', (raw_vs, ty))) =

              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

                           andalso not (ty = ITyVar "_")(*for evaluation*)

                         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, (superclasses, (v, classops)))) =

          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_classop_field (classop, ty) =

              concat [

                (str o pr_label_classop) classop, str ":", pr_typ NOBR ty

              ];

            fun pr_classop_proj (classop, _) =

              semicolon [

                str "fun",

                (str o deresolv) classop,

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

                str "=",

                str ("#" ^ pr_label_classop classop),

                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_classop_field classops

                )

              ]

              :: map pr_superclass_proj superclasses

              @ map pr_classop_proj classops

            )

          end

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

          let

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

              concat [

                (str o pr_label_classrel) classrel,

                str "=",

                pr_dicts NOBR [DictConst dss]

              ];

            fun pr_classop (classop, 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)

                    (CodeThingol.fold_constnames (insert (op =)) t []);

                val vars = CodeName.intro_vars consts init_syms;

              in

                concat [

                  (str o pr_label_classop) classop,

                  str "=",

                  pr_term false vars NOBR t

                ]

              end;

          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_classop classop_defs),

              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 false) 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 raw_fished = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);

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

                val fished = map_index (fillup_parm x) raw_fished;

                val vars' = CodeName.intro_vars fished vars;

              in map (CodeName.lookup_var vars') fished 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 [(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, (eqs, (vs, ty))) =

              concat (

                str definer

                :: (str o deresolv) name

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

                @| pr_eqs 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, (superclasses, (v, classops)))) =

          let

            val w = "_" ^ first_upper v;

            fun pr_superclass_field (class, classrel) =

              (concat o map str) [

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

              ];

            fun pr_classop_field (classop, ty) =

              concat [

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

              ];

            fun pr_classop_proj (classop, _) =

              concat [

                str "let",

                (str o deresolv) classop,

                str w,

                str "=",

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

              ];

          in Pretty.chunks (

            concat [

              str ("type '" ^ v),

              (str o deresolv) class,

              str "=",

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

                map pr_superclass_field superclasses @ map pr_classop_field classops

              )

            ]

            :: map pr_classop_proj classops

          ) end

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

          let

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

              concat [

                (str o deresolv) classrel,

                str "=",

                pr_dicts NOBR [DictConst dss]

              ];

            fun pr_classop_def (classop, 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)

                    (CodeThingol.fold_constnames (insert (op =)) t []);

                val vars = CodeName.intro_vars consts init_syms;

              in

                concat [

                  (str o deresolv) classop,

                  str "=",

                  pr_term false vars NOBR t

                ]

              end;

          in

            concat (

              str "let"

              :: (str o deresolv) inst

              :: pr_tyvars arity

              @ str "="

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

                Pretty.enum ";" "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),

                str ":",

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

              ]

            )

          end;

  in pr_def ml_def end;

fun pr_ocaml_modl name content =

  Pretty.chunks ([

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

    str "struct",

    str ""

  ] @ content @ [

    str "",

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

  ]);

val code_width = ref 80;

fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";

fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog

  (_ : string -> class_syntax option) tyco_syntax const_syntax code =

  let

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

    val is_cons = CodeThingol.is_cons code;

    datatype node =

        Def of string * ml_def option

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

    val init_names = Name.make_context reserved_syms;

    val init_module = ((init_names, init_names), Graph.empty);

    fun map_node [] f = f

      | map_node (m::ms) f =

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

          #> Graph.map_node m (fn (Module (dmodlname, (nsp, nodes))) => Module (dmodlname, (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, init_module))

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

                  let

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

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

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

    val init_syms = CodeName.make_vars reserved_syms;

    val name_modl = mk_modl_name_tab init_names NONE module_alias code;

    fun name_def upper name nsp =

      let

        val (_, base) = dest_name name;

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

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

      in (base'', nsp') end;

    fun map_nsp_fun f (nsp_fun, nsp_typ) =

      let

        val (x, nsp_fun') = f nsp_fun

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

    fun map_nsp_typ f (nsp_fun, nsp_typ) =

      let

        val (x, nsp_typ') = f nsp_typ

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

    fun mk_funs defs =

      fold_map

        (fn (name, CodeThingol.Fun info) =>

              map_nsp_fun (name_def false name) >> (fn base => (base, (name, info)))

          | (name, def) => error ("Function block containing illegal definition: " ^ labelled_name name)

        ) defs

      >> (split_list #> apsnd MLFuns);

    fun mk_datatype defs =

      fold_map

        (fn (name, CodeThingol.Datatype info) =>

              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))

          | (name, CodeThingol.Datatypecons _) =>

              map_nsp_fun (name_def true name) >> (fn base => (base, NONE))

          | (name, def) => error ("Datatype block containing illegal definition: " ^ labelled_name name)

        ) defs

      >> (split_list #> apsnd (map_filter I

        #> (fn [] => error ("Datatype block without data definition: " ^ (commas o map (labelled_name o fst)) defs)

             | infos => MLDatas infos)));

    fun mk_class defs =

      fold_map

        (fn (name, CodeThingol.Class info) =>

              map_nsp_typ (name_def false name) >> (fn base => (base, SOME (name, info)))

          | (name, CodeThingol.Classrel _) =>

              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))

          | (name, CodeThingol.Classop _) =>

              map_nsp_fun (name_def false name) >> (fn base => (base, NONE))

          | (name, def) => error ("Class block containing illegal definition: " ^ labelled_name name)

        ) defs

      >> (split_list #> apsnd (map_filter I

        #> (fn [] => error ("Class block without class definition: " ^ (commas o map (labelled_name o fst)) defs)

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

    fun mk_inst [(name, CodeThingol.Classinst info)] =

      map_nsp_fun (name_def false name)

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

    fun add_group mk defs nsp_nodes =

      let

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

        val deps =

          []

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

          |> subtract (op =) names;

        val (modls, _) = (split_list o map dest_name) names;

        val modl' = (the_single o distinct (op =) o map name_modl) modls

          handle Empty =>

            error ("Illegal mutual dependencies: " ^ commas (map labelled_name names));

        val modl_explode = NameSpace.explode modl';

        fun add_dep name name'' =

          let

            val modl'' = (name_modl o fst o dest_name) name'';

          in if modl' = modl'' then

            map_node modl_explode

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

          else let

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

              (modl_explode, NameSpace.explode modl'');

          in

            map_node common

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

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

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

                  ^ " would result in module dependency cycle"))

          end end;

      in

        nsp_nodes

        |> map_nsp_yield modl_explode (mk defs)

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

           apsnd (map_node modl_explode (Graph.new_node (name, (Def (base', SOME def')))

              #> fold2 (fn name' => fn base' => Graph.new_node (name', (Def (base', NONE)))) names' bases')))

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

        |> apsnd (fold (map_node modl_explode o Graph.add_edge) (product names names))

      end;

    fun group_defs [(_, CodeThingol.Bot)] =

          I

      | group_defs ((defs as (_, CodeThingol.Fun _)::_)) =