(*------------------------------------------------------------------*)
(* Translation from the Rosetta Code VM to an ATS program. *)

#include "share/atspre_staload.hats"

#define NIL list_nil ()
#define ::  list_cons

exception Exc_premature_end of string
exception Exc_illegal_null_char of string
exception Exc_illegal_char of string
exception Exc_illegal_opcode of string
exception Exc_internal_error of string

typedef character = int
typedef reader =
  @{
    inpf = FILEref,
    queue = List0 character
  }

typedef instruction =
  @{
    address = uint,
    opcode = string,
    pushval = int,
    index = uint,
    reladdr = int
  }

typedef continuation = List1 string

macdef c2i = char2int0
macdef newline outf = fprintln! ,(outf)

(*------------------------------------------------------------------*)

fn
character_code (c : character) : int =
  c

fn
character_is_newline (c : character) : bool =
  character_code c = c2i '\n'

fn
character_is_digit (c : character) : bool =
  isdigit (character_code c)

fn
character_is_minus_or_digit (c : character) : bool =
  character_code c = c2i '-' || isdigit (character_code c)

fn
character_is_alpha (c : character) : bool =
  isalpha (character_code c)

fn
character_is_space (c : character) : bool =
  isspace (character_code c)

fn
addr2kont_uint (addr : uint) : string =
  strptr2string (string_append ("kont", tostring_val<uint> addr))

fn
addr2kont_int (addr : int) : string =
  addr2kont_uint (g0i2u addr)

overload addr2kont with addr2kont_uint
overload addr2kont with addr2kont_int

fn
jmp2kont (instr : instruction) : string =
  addr2kont (g0u2i instr.address + instr.reladdr + 1)

fn
skip_nothing (instr : instruction) : string =
  addr2kont (instr.address + 1U)

fn
skip_immed (instr : instruction) : string =
  addr2kont (instr.address + 5U)

fn
index2var (instr : instruction) : string =
  strptr2string
    (string_append ("var", tostring_val<uint> (instr.index)))

fn
character_list_to_string
          (lst    : List0 character,
           caller : string)
    : string =
  let
    implement
    list_map$fopr<character><charNZ> c =
      let
        val ch = int2char0 (character_code c)
        val ch = g1ofg0 ch
      in
        if ch = '\0' then
          $raise (Exc_illegal_null_char caller)
        else
          ch
      end
    val lst = list_vt2t (list_map<character><charNZ> lst)
  in
    strnptr2string (string_implode lst)
  end

fn
get_character (rd : &reader) : character =
  case+ rd.queue of
  | hd :: tl =>
    begin
      rd := @{inpf = rd.inpf, queue = tl};
      hd
    end
  | NIL => fileref_getc (rd.inpf)

fn
unget_character (rd : &reader,
                 c  : character) : void =
  rd := @{inpf = rd.inpf,
          queue = list_append (rd.queue, c :: NIL)}

fn
skip_until (rd   : &reader,
            pred : character -<cloref1> bool) : character =
  let
    fun
    loop (rd : &reader) : int =
      let
        val c = get_character rd
      in
        if pred c then
          c
        else if c < 0 then
          $raise (Exc_premature_end "skip_until")
        else
          loop rd
      end
  in
    loop rd
  end

fn
read_unsigned (rd : &reader) : uint =
  let
    fun
    loop (rd  : &reader,
          num : uint) : uint =
      let
        val c = get_character rd
      in
        if character_is_digit c then
          let
            val digit = character_code c - c2i ('0')
          in
            loop (rd, (10U * num) + g0i2u digit)
          end
        else
          begin
            unget_character (rd, c);
            num
          end
      end
  in
    loop (rd, 0U)
  end

fn
read_signed (rd : &reader) : int =
  let
    val c = get_character rd
  in
    if character_code c = '-' then
      let
        val num = read_unsigned rd
      in
        ~(g0u2i num)
      end
    else
      let
        val () = unget_character (rd, c)
        val num = read_unsigned rd
      in
        g0u2i num
      end
  end

fn
read_header (rd : &reader) : @(uint, uint) =
  let
    val c = skip_until (rd, lam c => character_is_digit c)
    val () = unget_character (rd, c)
    val data_size = read_unsigned rd
    val c = skip_until (rd, lam c => character_is_digit c)
    val () = unget_character (rd, c)
    val strings_size = read_unsigned rd
    val _ = skip_until (rd, lam c => character_is_newline c)
  in
    @(data_size, strings_size)
  end

fn
read_string (rd : &reader) : string =
  let
    fun
    loop (rd  : &reader,
          lst : List1 character) : List1 character =
      let
        val c = get_character rd
      in
        if character_code c < 0 then
          $raise (Exc_premature_end "read_string")
        else if character_code c = c2i '"' then
          c :: lst
        else
          loop (rd, c :: lst)
      end

    val c = skip_until (rd, lam c => character_code c = c2i '"')
    val lst = list_vt2t (list_reverse (loop (rd, c :: NIL)))
    val _ = skip_until (rd, lam c => character_code c = c2i '\n')
  in
    character_list_to_string (lst, "read_string")
  end

fn
read_strings_pool
          (rd           : &reader,
           strings_size : uint)
    : List0 string =
  let
    fun
    loop (rd    : &reader,
          count : uint,
          pool  : List0 string) : List0 string =
      if count = 0 then
        pool
      else
        let
          val s = read_string rd
        in
          loop (rd, pred count, s :: pool)
        end
  in
    list_vt2t (list_reverse (loop (rd, strings_size, NIL)))
  end

fn
read_opcode (rd : &reader) : string =
  let
    fun
    loop (rd  : &reader,
          lst : List0 character) : List0 character =
      let
        val c = get_character rd
        val code = character_code c
      in
        if code < 0 then
          $raise (Exc_premature_end "read_opcode")
        else if isalpha code then
          loop (rd, c :: lst)
        else
          begin
            unget_character (rd, c);
            list_vt2t (list_reverse lst)
          end
      end
  in
    character_list_to_string (loop (rd, NIL), "read_opcode")
  end

fn
read_args (rd    : &reader,
           instr : &instruction) : void =
  if instr.opcode = "push" then
    let
      val c = skip_until (rd, lam c => character_is_minus_or_digit c)
      val () = unget_character (rd, c)
      val pushval = read_signed rd
      val _ = skip_until (rd, lam c => character_is_newline c)
    in
      instr := @{address = instr.address,
                 opcode = instr.opcode,
                 pushval = pushval,
                 index = 0U,
                 reladdr = 0}
    end
  else if instr.opcode = "fetch" || instr.opcode = "store" then
    let
      val _ = skip_until (rd, lam c => character_code c = c2i '\[')
      val c = skip_until (rd, lam c => character_is_digit c)
      val () = unget_character (rd, c)
      val index = read_unsigned rd
      val _ = skip_until (rd, lam c => character_is_newline c)
    in
      instr := @{address = instr.address,
                 opcode = instr.opcode,
                 pushval = 0,
                 index = index,
                 reladdr = 0}
    end
  else if instr.opcode = "jmp" || instr.opcode = "jz" then
    let
      val _ = skip_until (rd, lam c => character_code c = c2i '\(')
      val c = skip_until (rd, lam c => character_is_minus_or_digit c)
      val () = unget_character (rd, c)
      val relative_addr = read_signed rd
      val _ = skip_until (rd, lam c => character_is_newline c)
    in
      instr := @{address = instr.address,
                 opcode = instr.opcode,
                 pushval = 0,
                 index = 0U,
                 reladdr = relative_addr}
    end

fn
read_instruc (rd : &reader) : instruction =
  let
    val c = skip_until (rd, lam c => character_is_digit c)
    val () = unget_character (rd, c)
    val address = read_unsigned rd
    val c = skip_until (rd, lam c => character_is_alpha c)
    val () = unget_character (rd, c)
    val opcode = read_opcode rd
    var instr = @{address = address,
                  opcode = opcode,
                  pushval = 0,
                  index = 0U,
                  reladdr = 0} : instruction
    val () = read_args (rd, instr)
  in
    instr
  end

fn
read_instructions (rd : &reader) : List0 instruction =
  let
    fun
    loop (rd  : &reader,
          lst : List0 instruction) : List0 instruction =
      let
        val c = skip_until (rd, lam c => ~character_is_space c)
      in
        if c < 0 then
          lst
        else if ~character_is_digit c then
          $raise (Exc_illegal_char "read_instructions")
        else
          let
            val () = unget_character (rd, c)
            val instr = read_instruc rd
          in
            loop (rd, instr :: lst)
          end
      end
  in
    list_vt2t (list_reverse (loop (rd, NIL)))
  end

(*------------------------------------------------------------------*)

fn
write_kont_body_ats_style
          (outf : FILEref,
           args : List0 string) : void =
  case+ args of
  | NIL =>
    $raise (Exc_internal_error "write_kont_body_ats_style")
  | hd :: tl =>
    let
      fun
      loop (args      : List0 string,
            separator : string) : void =
        case+ args of
        | NIL => ()
        | hd :: tl =>
          begin
            fprint! (outf, separator, hd);
            loop (tl, ", ")
          end
    in
      fprint! (outf, hd, " (");
      loop (tl, "");
      fprint! (outf, ")");
    end

fn
instruc2args_simple (instr : instruction) : List0 string =
  instr.opcode :: skip_nothing instr :: NIL

fn
instruc2args_unary
          (instr     : instruction,
           operation : string)
    : List0 string =
  "unary" :: operation :: skip_nothing instr :: NIL

fn
instruc2args_binary
          (instr     : instruction,
           operation : string)
    : List0 string =
  "binary" :: operation :: skip_nothing instr :: NIL

fn
instruc2args_store_fetch (instr : instruction) : List0 string =
  instr.opcode :: index2var instr :: skip_immed instr :: NIL

fn
instruc2args_push (instr : instruction) : List0 string =
  let
    val pushval = tostring_val<int> instr.pushval
  in
    instr.opcode :: pushval :: skip_immed instr :: NIL
  end

fn
instruc2args_jmp (instr : instruction) : List0 string =
  instr.opcode :: jmp2kont instr :: NIL

fn
instruc2args_jz (instr : instruction) : List0 string =
  instr.opcode :: jmp2kont instr :: skip_immed instr :: NIL

fn
instruc2args_halt (instr : instruction) : List0 string =
  instr.opcode :: NIL

fn
instruc2args (instr : instruction) : List0 string =
  case instr.opcode of
  | "push" => instruc2args_push instr
  | "jmp" => instruc2args_jmp instr
  | "jz" => instruc2args_jz instr
  | "store" => instruc2args_store_fetch instr
  | "fetch" => instruc2args_store_fetch instr
  | "prtc" => instruc2args_simple instr
  | "prti" => instruc2args_simple instr
  | "prts" => instruc2args_simple instr
  | "neg" => instruc2args_unary (instr, "g0int_neg")
  | "not" => instruc2args_unary (instr, "logical_not")
  | "add" => instruc2args_binary (instr, "g0int_add")
  | "sub" => instruc2args_binary (instr, "g0int_sub")
  | "mul" => instruc2args_binary (instr, "g0int_mul")
  | "div" => instruc2args_binary (instr, "g0int_div")
  | "mod" => instruc2args_binary (instr, "g0int_mod")
  | "and" => instruc2args_binary (instr, "logical_and")
  | "or" => instruc2args_binary (instr, "logical_or")
  | "lt" => instruc2args_binary (instr, "binary_lt")
  | "le" => instruc2args_binary (instr, "binary_le")
  | "gt" => instruc2args_binary (instr, "binary_gt")
  | "ge" => instruc2args_binary (instr, "binary_ge")
  | "eq" => instruc2args_binary (instr, "binary_eq")
  | "ne" => instruc2args_binary (instr, "binary_ne")
  | "halt" => instruc2args_halt instr
  | _ => $raise (Exc_illegal_opcode "instruc2args")

fn
vm2cps (instructions : List0 instruction)
    : List0 continuation =
  let
    fun
    loop (instructions : List0 instruction,
          continuations   : List0 continuation)
        : List0 continuation =
      case+ instructions of
      | NIL => continuations
      | hd :: tl =>
        let
          val addr = tostring_val<uint> hd.address
          val name = strptr2string (string_append ("kont", addr))
          val kont = name :: instruc2args hd
        in
          loop (tl, kont :: continuations)
        end
  in
    list_vt2t (list_reverse (loop (instructions, NIL)))
  end

(*------------------------------------------------------------------*)

fn
write_ats_stack (outf      : FILEref,
             stack_max : uint) : void =
  begin
    fprintln! (outf, "val stack = arrszref_make_elt<int> (",
               "g0u2u ", stack_max, "U, 0)");
    fprintln! (outf, "val stack_ptr : ref uint = ref 0U");
  end

fn
write_ats_named_variables
          (outf      : FILEref,
           data_size : uint)
    : void =
  let
    fun
    loop (i : uint) : void =
      if i <> data_size then
        begin
          fprintln! (outf, "val var", i, " : ref int = ref 0");
          loop (succ i)
        end
  in
    loop (0U)
  end

fn
write_ats_strings_pool
          (outf : FILEref,
           pool : List0 string)
    : void =
  let
    fun
    loop (i : uint, pool : List0 string) : void =
      case+ pool of
      | hd :: tl =>
        begin
          fprintln! (outf, "val () = strings[", i, "] := ", hd);
          loop (succ i, tl)
        end
      | NIL => ()

    val n = length pool
  in
    fprintln! (outf, "val strings = arrszref_make_elt<string> ",
               "(i2sz ", max (n, 1), ", \"\")");
    if isneqz n then
      loop (0U, pool)
  end

fn
write_ats_procedures
          (outf  : FILEref,
           konts : List0 continuation) : void =
  begin
    fprint! (outf, "fnx ");
    fprint! (outf, "start_here () : void = ");
    case+ konts of
    | NIL => fprintln! (outf, " ()")
    | hd :: _ =>
      let
        fun
        loop (konts : List0 continuation) : void =
          case+ konts of
          | NIL => ()
          | hd :: tl =>
            let
              val+ kontname :: arguments = hd
            in
              fprint! (outf, "and ");
              fprint! (outf, kontname, " () : void = ");
              write_kont_body_ats_style (outf, arguments);
              newline outf;
              loop tl
            end
      in
        fprintln! (outf, "kont0 ()");
        loop konts
      end
  end

fn
write_ats_macros (outf : FILEref) : void =
  fprint! (outf,
"macdef logical_not (x) =
  if iseqz ,(x) then 1 else 0

macdef logical_and (x, y) =
  if (isneqz ,(x)) * (isneqz ,(y)) then 1 else 0

macdef logical_or (x, y) =
  if (isneqz ,(x)) + (isneqz ,(y)) then 1 else 0

macdef binary_lt (x, y) =
  if ,(x) < ,(y) then 1 else 0

macdef binary_le (x, y) =
  if ,(x) <= ,(y) then 1 else 0

macdef binary_gt (x, y) =
  if ,(x) > ,(y) then 1 else 0

macdef binary_ge (x, y) =
  if ,(x) >= ,(y) then 1 else 0

macdef binary_eq (x, y) =
  if ,(x) = ,(y) then 1 else 0

macdef binary_ne (x, y) =
  if ,(x) <> ,(y) then 1 else 0

macdef unary (operation, kont) =
  let
    val sp = pred !stack_ptr
  in
    stack[sp] := ,(operation) (stack[sp]);
    ,(kont) ()
  end

macdef binary (operation, kont) =
  let
    val sp2 = pred !stack_ptr
    val sp1 = pred sp2
  in
    stack[sp1] := ,(operation) (stack[sp1], stack[sp2]);
    !stack_ptr := sp2;
    ,(kont) ()
  end

macdef jmp (kont) =
  ,(kont) ()

macdef jz (kont_if, kont_else) =
  let
    val sp = pred !stack_ptr;
  in
    !stack_ptr := sp;
    if iseqz stack[sp] then
      ,(kont_if) ()
    else
      ,(kont_else) ()
  end

macdef push (pushval, kont) =
  let
    val sp = !stack_ptr
  in
    stack[sp] := ,(pushval);
    !stack_ptr := succ sp;
    ,(kont) ()
  end

macdef store (variable, kont) =
  let
    val sp = pred !stack_ptr
  in
    !stack_ptr := sp;
    !,(variable) := stack[sp];
    ,(kont) ()
  end

macdef fetch (variable, kont) =
  let
    val sp = !stack_ptr
  in
    stack[sp] := !,(variable);
    !stack_ptr := succ sp;
    ,(kont) ()
  end

macdef prtc (kont) =
  let
    val sp = pred !stack_ptr
  in
    print! (int2char0 stack[sp]);
    !stack_ptr := sp;
    ,(kont) ()
  end

macdef prti (kont) =
  let
    val sp = pred !stack_ptr
  in
    print! (stack[sp]);
    !stack_ptr := sp;
    ,(kont) ()
  end

macdef prts (kont) =
  let
    val sp = pred !stack_ptr
  in
    print! (strings[stack[sp]]);
    !stack_ptr := sp;
    ,(kont) ()
  end

macdef halt () = ()
")

fn
compile2ats (rd        : &reader,
             outf      : FILEref,
             stack_max : uint) : void =
  let
    val @(data_size, strings_size) = read_header rd
    val strings_pool = read_strings_pool (rd, strings_size)
    val instructions = read_instructions rd
    val continuations = vm2cps instructions
  in
    fprintln! (outf, "#include \"share/atspre_staload.hats\"");
    newline outf;
    write_ats_stack (outf, stack_max);
    newline outf;
    write_ats_named_variables (outf, data_size);
    newline outf;
    write_ats_strings_pool (outf, strings_pool);
    newline outf;
    write_ats_macros outf;
    newline outf;
    write_ats_procedures (outf, continuations);
    newline outf;
    fprintln! (outf, "implement main0 () = start_here ()")
  end

(*------------------------------------------------------------------*)

implement
main0 () =
  let
    var rd : reader = @{inpf = stdin_ref, queue = NIL}
  in
    compile2ats (rd, stdout_ref, 1000U)
  end

(*------------------------------------------------------------------*)