src/Pure/Tools/codegen_serializer.ML

code generator: case expressions, improved name resolving

(*  Title:      Pure/Tools/codegen_serializer.ML
    ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen

Serializer from intermediate language ("Thin-gol") to
target languages (like ML or Haskell).
*)

signature CODEGEN_SERIALIZER =
sig
  type primitives;
  val empty_prims: primitives;
  val add_prim: string * (string * string list) -> primitives -> primitives;
  val merge_prims: primitives * primitives -> primitives;
  val has_prim: primitives -> string -> bool;
  val mk_prims: primitives -> string;

  type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
    -> (string list * Pretty.T) option;
  type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
    -> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
  type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;

  val ml_from_thingol: string list list -> string -> serializer;
end;

structure CodegenSerializer: CODEGEN_SERIALIZER =
struct

open CodegenThingol;


(** target language primitives **)

type primitives = string Graph.T;

val empty_prims = Graph.empty;

fun add_prim (f, (def, deps)) prims =
  prims
  |> Graph.new_node (f, def)
  |> fold (fn dep => Graph.add_edge (f, dep)) deps;

val merge_prims = Graph.merge (op =) : primitives * primitives -> primitives;

val has_prim : primitives -> string -> bool = can o Graph.get_node;

fun get_prims prims defs =
  defs
  |> filter (can (Graph.get_node prims))
  |> `I
  ||> Graph.all_succs prims
  ||> (fn gr => Graph.subgraph gr prims)
  ||> Graph.strong_conn
  ||> rev
  ||> Library.flat
  ||> map (Graph.get_node prims)
  ||> separate ""
  ||> cat_lines
  ||> suffix "\n";

fun mk_prims prims = get_prims prims (Graph.keys prims) |> snd;


(** generic serialization **)

type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
  -> (string list * Pretty.T) option;
type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
  -> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;

datatype lrx = L | R | X;

datatype brack =
    BR
  | NOBR
  | INFX of (int * lrx);

fun eval_lrx L L = false
  | eval_lrx R R = false
  | eval_lrx _ _ = true;

fun eval_br BR _ = true
  | eval_br NOBR _ = false
  | eval_br (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
      pr1 > pr2
      orelse pr1 = pr2
      andalso eval_lrx lr1 lr2
  | eval_br (INFX _) _ = false;

fun eval_br_postfix BR _ = false
  | eval_br_postfix NOBR _ = false
  | eval_br_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
      pr1 > pr2
      orelse pr1 = pr2
      andalso eval_lrx lr1 lr2
  | eval_br_postfix (INFX _) _ = false;

fun brackify _ [p] = p
  | brackify true (ps as _::_) = Pretty.enclose "(" ")" (Pretty.breaks ps)
  | brackify false (ps as _::_) = Pretty.block (Pretty.breaks ps);

fun postify [] f = [f]
  | postify [p] f = [p, Pretty.brk 1, f]
  | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f];

fun praetify [] f = [f]
  | praetify [p] f = [f, Pretty.str " of ", p]


(** ML serializer **)

local

fun ml_validator prims name =
  let
    fun replace_invalid c =
      if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
      andalso not (NameSpace.separator = c)
      then c
      else "_"
    fun suffix_it name =
      name
      |> member (op =) ThmDatabase.ml_reserved ? suffix "'"
      |> member (op =) CodegenThingol.prims ? suffix "'"
      |> has_prim prims ? suffix "'"
      |> (fn name' => if name = name' then name else suffix_it name')
  in
    name
    |> translate_string replace_invalid
    |> suffix_it
    |> (fn name' => if name = name' then NONE else SOME name')
  end;

val ml_label_uniq = translate_string (fn "'" => "''" | "." => "'" | c => c);

fun ml_from_defs styco sconst resolv ds =
  let
    fun chunk_defs ps = 
      let
        val (p_init, p_last) = split_last ps
      in
        Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])])
    end;
    fun ml_from_typ br (IType ("Pair", [t1, t2])) =
          brackify (eval_br_postfix br (INFX (2, L))) [
            ml_from_typ (INFX (2, X)) t1,
            Pretty.str "*",
            ml_from_typ (INFX (2, X)) t2
          ]
      | ml_from_typ br (IType ("Bool", [])) =
          Pretty.str "bool"
      | ml_from_typ br (IType ("Integer", [])) =
          Pretty.str "IntInf.int"
      | ml_from_typ br (IType ("List", [ty])) =
          postify ([ml_from_typ BR ty]) (Pretty.str "list")
          |> Pretty.block
      | ml_from_typ br (IType (tyco, typs)) =
          let
            val tyargs = (map (ml_from_typ BR) typs)
          in
            case styco tyco tyargs (ml_from_typ BR)
             of NONE =>
                  postify tyargs ((Pretty.str o resolv) tyco)
                  |> Pretty.block
              | SOME ([], p) =>
                  p
              | SOME (_, p) =>
                  error ("cannot serialize partial type application to ML, while serializing "
                    ^ quote (tyco ^ " " ^ Pretty.output (Pretty.list "(" ")" tyargs)))
          end
      | ml_from_typ br (IFun (t1, t2)) =
          brackify (eval_br_postfix br (INFX (1, R))) [
            ml_from_typ (INFX (1, X)) t1,
            Pretty.str "->",
            ml_from_typ (INFX (1, R)) t2
          ]
      | ml_from_typ _ (IVarT (v, [])) =
          Pretty.str ("'" ^ v)
      | ml_from_typ _ (IVarT (_, sort)) =
          "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
      | ml_from_typ _ (IDictT fs) =
          (Pretty.enclose "{" "}" o Pretty.breaks) (
            map (fn (f, ty) =>
              Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_typ NOBR ty]) fs
          );
    fun ml_from_pat br (ICons (("True", []), _)) =
          Pretty.str "true"
      | ml_from_pat br (ICons (("False", []), _)) =
          Pretty.str "false"
      | ml_from_pat br (ICons (("Pair", ps), _)) =
          ps
          |> map (ml_from_pat NOBR)
          |> Pretty.list "(" ")"
      | ml_from_pat br (ICons (("Nil", []), _)) =
          Pretty.str "[]"
      | ml_from_pat br (p as ICons (("Cons", _), _)) =
          let
            fun dest_cons (ICons (("Cons", [ICons (("Pair", [p1, p2]), _)]), _)) = SOME (p1, p2)
              | dest_cons p = NONE
          in
            case unfoldr dest_cons p
             of (ps, (ICons (("Nil", []), _))) =>
                  ps
                  |> map (ml_from_pat NOBR)
                  |> Pretty.list "[" "]"
              | (ps, p) =>
                  (ps @ [p])
                  |> map (ml_from_pat (INFX (5, X)))
                  |> separate (Pretty.str "::")
                  |> brackify (eval_br br (INFX (5, R)))
          end
      | ml_from_pat br (ICons ((f, ps), ty)) =
          ps
          |> map (ml_from_pat BR)
          |> cons ((Pretty.str o resolv) f)
          |> brackify (eval_br br BR)
      | ml_from_pat br (IVarP (v, IType ("Integer", []))) =
          Pretty.str ("(" ^ v ^ ":IntInf.int)")
      | ml_from_pat br (IVarP (v, _)) =
          Pretty.str v;
    fun ml_from_iexpr br (e as (IApp (IConst ("Cons", _), _))) =
          let
            fun dest_cons (IApp (IConst ("Cons", _),
                  IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2)
              | dest_cons p = NONE
          in
            case unfoldr dest_cons e
             of (es, (IConst ("Nil", _))) =>
                  es
                  |> map (ml_from_iexpr NOBR) 
                  |> Pretty.list "[" "]"
              | (es, e) =>
                  (es @ [e])
                  |> map (ml_from_iexpr (INFX (5, X)))
                  |> separate (Pretty.str "::")
                  |> brackify (eval_br br (INFX (5, R)))
          end
      | ml_from_iexpr br (e as IApp (e1, e2)) =
          (case (unfold_app e)
           of (e as (IConst (f, _)), es) =>
                ml_from_app br (f, es)
            | _ => 
                brackify (eval_br br BR) [
                  ml_from_iexpr NOBR e1,
                  ml_from_iexpr BR e2
                ])
      | ml_from_iexpr br (e as IConst (f, _)) =
          ml_from_app br (f, [])
      | ml_from_iexpr br (IVarE (v, _)) =
          Pretty.str v
      | ml_from_iexpr br (IAbs ((v, _), e)) =
          brackify (eval_br br BR) [
            Pretty.str ("fn " ^ v ^ " =>"),
            ml_from_iexpr BR e
          ]
      | ml_from_iexpr br (e as ICase (_, [_])) =
          let
            val (ps, e) = unfold_let e;
            fun mk_val (p, e) = Pretty.block [
                Pretty.str "val ",
                ml_from_pat BR p,
                Pretty.str " =",
                Pretty.brk 1,
                ml_from_iexpr NOBR e,
                Pretty.str ";"
              ]
          in Pretty.chunks [
            [Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
            [Pretty.str ("in"), Pretty.fbrk, ml_from_iexpr NOBR e] |> Pretty.block,
            Pretty.str ("end")
          ] end
      | ml_from_iexpr br (ICase (e, c::cs)) =
          let
            fun mk_clause definer (p, e) =
              Pretty.block [
                Pretty.str definer,
                ml_from_pat NOBR p,
                Pretty.str " =>",
                Pretty.brk 1,
                ml_from_iexpr NOBR e
              ]
          in brackify (eval_br br BR) (
            Pretty.str "case"
            :: ml_from_iexpr NOBR e
            :: mk_clause "of " c
            :: map (mk_clause "| ") cs
          ) end
      | ml_from_iexpr br (IInst _) =
          error "cannot serialize poly instant to ML"
      | ml_from_iexpr br (IDictE fs) =
          (Pretty.enclose "{" "}" o Pretty.breaks) (
            map (fn (f, e) =>
              Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_iexpr NOBR e]) fs
          )
      | ml_from_iexpr br (ILookup (ls, v)) =
          brackify (eval_br br BR) [
            Pretty.str "(",
            ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e) |> Pretty.str,
            Pretty.str ")",
            Pretty.str " ",
            Pretty.str v
          ]
    and mk_app_p br p args =
      brackify (eval_br br BR)
        (p :: map (ml_from_iexpr BR) args)
    and ml_from_app br ("Nil", []) =
          Pretty.str "[]"
      | ml_from_app br ("True", []) =
          Pretty.str "true"
      | ml_from_app br ("False", []) =
          Pretty.str "false"
      | ml_from_app br ("primeq", [e1, e2]) =
          brackify (eval_br br (INFX (4, L))) [
            ml_from_iexpr (INFX (4, L)) e1,
            Pretty.str "=",
            ml_from_iexpr (INFX (4, X)) e2
          ]
      | ml_from_app br ("Pair", [e1, e2]) =
          Pretty.list "(" ")" [
            ml_from_iexpr NOBR e1,
            ml_from_iexpr NOBR e2
          ]
      | ml_from_app br ("and", [e1, e2]) =
          brackify (eval_br br (INFX (~1, L))) [
            ml_from_iexpr (INFX (~1, L)) e1,
            Pretty.str "andalso",
            ml_from_iexpr (INFX (~1, X)) e2
          ]
      | ml_from_app br ("or", [e1, e2]) =
          brackify (eval_br br (INFX (~2, L))) [
            ml_from_iexpr (INFX (~2, L)) e1,
            Pretty.str "orelse",
            ml_from_iexpr (INFX (~2, X)) e2
          ]
      | ml_from_app br ("if", [b, e1, e2]) =
          brackify (eval_br br BR) [
            Pretty.str "if",
            ml_from_iexpr BR b,
            Pretty.str "then",
            ml_from_iexpr BR e1,
            Pretty.str "else",
            ml_from_iexpr BR e2
          ]
      | ml_from_app br ("add", [e1, e2]) =
          brackify (eval_br br (INFX (6, L))) [
            ml_from_iexpr (INFX (6, L)) e1,
            Pretty.str "+",
            ml_from_iexpr (INFX (6, X)) e2
          ]
      | ml_from_app br ("mult", [e1, e2]) =
          brackify (eval_br br (INFX (7, L))) [
            ml_from_iexpr (INFX (7, L)) e1,
            Pretty.str "+",
            ml_from_iexpr (INFX (7, X)) e2
          ]
      | ml_from_app br ("lt", [e1, e2]) =
          brackify (eval_br br (INFX (4, L))) [
            ml_from_iexpr (INFX (4, L)) e1,
            Pretty.str "<",
            ml_from_iexpr (INFX (4, X)) e2
          ]
      | ml_from_app br ("le", [e1, e2]) =
          brackify (eval_br br (INFX (7, L))) [
            ml_from_iexpr (INFX (4, L)) e1,
            Pretty.str "<=",
            ml_from_iexpr (INFX (4, X)) e2
          ]
      | ml_from_app br ("minus", es) =
          mk_app_p br (Pretty.str "~") es
      | ml_from_app br ("wfrec", es) =
          mk_app_p br (Pretty.str "wfrec") es
      | ml_from_app br (f, es) =
          let
            val args = map (ml_from_iexpr BR) es
            val brackify' = K (eval_br br BR) ? (single #> Pretty.enclose "(" ")")
          in
            case sconst f args (ml_from_iexpr BR)
             of NONE =>
                  brackify (eval_br br BR) (Pretty.str (resolv f) :: args)
              | SOME (_, p) =>
                  brackify' p
          end;
    fun ml_from_funs (ds as d::ds_tl) =
      let
        fun mk_definer [] = "val"
          | mk_definer _ = "fun"
        fun check_args (_, Fun ((pats, _)::_, _)) NONE =
              SOME (mk_definer pats)
          | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) =
              if mk_definer pats = definer
              then SOME definer
              else error ("mixing simultaneous vals and funs not implemented")
          | check_args _ _ =
              error ("function definition block containing other definitions than functions")
        val definer = the (fold check_args ds NONE);
        fun mk_eq definer f ty (pats, expr) =
          let
            val lhs = [Pretty.str (definer ^ " " ^ f)]
                       @ (if null pats
                          then [Pretty.str ":", ml_from_typ NOBR ty]
                          else map (ml_from_pat BR) pats)
            val rhs = [Pretty.str "=", ml_from_iexpr NOBR expr]
          in
            Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
          end
        fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) =
          let
            val (pats_hd::pats_tl) = (fst o split_list) eqs;
            val _ = fold (fn x => fn y => (x ~~ y; y)) pats_tl pats_hd;
              (*check for equal length of argument lists*)
            val shift = if null eq_tl then I else map (Pretty.block o single);
          in (Pretty.block o Pretty.fbreaks o shift) (
               mk_eq definer f ty eq
               :: map (mk_eq "|" f ty) eq_tl
             )
          end
      in
        chunk_defs (
          mk_fun definer d
          :: map (mk_fun "and") ds_tl
        )
      end;
    fun ml_from_datatypes ds =
      let
        fun check_typ_dup ty xs =
          if AList.defined (op =) xs ty
          then error ("double datatype definition: " ^ quote ty)
          else xs
        fun check_typ_miss ty xs =
          if AList.defined (op =) xs ty
          then xs
          else error ("missing datatype definition: " ^ quote ty)
        fun group (name, Datatype (vs, _, _)) ts =
              (map (fn (_, []) => () | _ => error "can't serialize sort constrained datatype declaration to ML") vs;
              ts
              |> apsnd (check_typ_dup name)
              |> apsnd (AList.update (op =) (name, (vs, []))))
          | group (_, Datatypecons (_, _::_::_)) _ =
              error ("Datatype constructor containing more than one parameter")
          | group (name, Datatypecons (ty, tys)) ts =
              ts
              |> apfst (AList.default (op =) (resolv ty, []))
              |> apfst (AList.map_entry (op =) (resolv ty) (cons (name, tys)))
          | group _ _ =
              error ("Datatype block containing other statements than datatype or constructor definitions")
        fun group_cons (ty, co) ts =
          ts
          |> check_typ_miss ty
          |> AList.map_entry (op =) ty (rpair co o fst)
        fun mk_datatypes (ds as d::ds_tl) =
          let
            fun mk_cons (co, typs) =
              (Pretty.block oo praetify)
                (map (ml_from_typ NOBR) typs)
                (Pretty.str (resolv co))
            fun mk_datatype definer (t, (vs, cs)) =
              Pretty.block (
                [Pretty.str definer]
                @ postify (map (ml_from_typ BR o IVarT) vs)
                    (Pretty.str t)
                @ [Pretty.str " =",
                  Pretty.brk 1]
                @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
              )
          in
            chunk_defs (
              mk_datatype "datatype " d
              :: map (mk_datatype "and ") ds_tl
            )
          end;
      in
        ([], [])
        |> fold group ds
        |-> (fn cons => fold group_cons cons)
        |> mk_datatypes
      end;
    fun ml_from_def (name, Typesyn (vs, ty)) =
        (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
         Pretty.block (
          Pretty.str "type "
          :: postify (map (Pretty.str o fst) vs) (Pretty.str name)
          @ [Pretty.str " =",
          Pretty.brk 1,
          ml_from_typ NOBR ty,
          Pretty.str ";"
        ]))
      | ml_from_def (name, Nop) =
          if exists (fn query => (is_some o query) name)
            [(fn name => styco name [] (ml_from_typ NOBR)),
             (fn name => sconst name [] (ml_from_iexpr NOBR))]
          then Pretty.str ""
          else error ("empty statement during serialization: " ^ quote name)
      | ml_from_def (name, Class _) =
          error ("can't serialize class declaration " ^ quote name ^ " to ML")
      | ml_from_def (name, Classinst _) =
          error ("can't serialize instance declaration " ^ quote name ^ " to ML")
  in case (snd o hd) ds
   of Fun _ => ml_from_funs ds
    | Datatypecons _ => ml_from_datatypes ds
    | Datatype _ => ml_from_datatypes ds
    | _ => (case ds of [d] => ml_from_def d)
  end;

in

fun ml_from_thingol nspgrp name_root styco sconst prims select module =
  let
    fun ml_from_module (name, ps) =
      Pretty.chunks ([
        Pretty.str ("structure " ^ name ^ " = "),
        Pretty.str "struct",
        Pretty.str ""
      ] @ separate (Pretty.str "") ps @ [
        Pretty.str "",
        Pretty.str ("end; (* struct " ^ name ^ " *)")
      ]);
    fun eta_expander "Pair" = 2
      | eta_expander "Cons" = 2
      | eta_expander "primeq" = 2
      | eta_expander "and" = 2
      | eta_expander "or" = 2
      | eta_expander "if" = 3
      | eta_expander "add" = 2
      | eta_expander "mult" = 2
      | eta_expander "lt" = 2
      | eta_expander "le" = 2
      | eta_expander s =
          if NameSpace.is_qualified s
          then case get_def module s
            of Datatypecons (_ , tys) =>
                if length tys >= 2 then length tys else 0
             | _ =>
              (case sconst s [] (K (Pretty.str ""))
               of NONE => 0
                | SOME (xs, _) => length xs)
          else 0
  in 
    module
    |> debug 12 (Pretty.output o pretty_module)
    |> debug 3 (fn _ => "connecting datatypes and classdecls...")
    |> connect_datatypes_clsdecls
    |> debug 3 (fn _ => "selecting submodule...")
    |> (if is_some select then (partof o the) select else I)
    |> debug 3 (fn _ => "eta-expanding...")
    |> eta_expand eta_expander
    |> debug 3 (fn _ => "eta-expanding polydefs...")
    |> eta_expand_poly
    |> debug 12 (Pretty.output o pretty_module)
    |> debug 3 (fn _ => "tupelizing datatypes...")
    |> tupelize_cons
    |> debug 3 (fn _ => "eliminating classes...")
    |> eliminate_classes
    |> debug 3 (fn _ => "generating...")
    |> serialize (ml_from_defs styco sconst) ml_from_module (ml_validator prims) nspgrp name_root
  end;

fun ml_from_thingol' nspgrp name_root =
  Scan.optional (
    OuterParse.$$$ "(" |-- OuterParse.list1 OuterParse.text --| OuterParse.$$$ ")"
  ) []
    >> (fn _ => ml_from_thingol nspgrp name_root);

(* ML infix precedence
   7 / * div mod
   6 + - ^
   5 :: @
   4 = <> < > <= >=
   3 := o *)

end; (* local *)

end; (* struct *)