(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(*                              Hongwei Xi                             *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Anairiats - Unleashing the Potential of Types!
**
** Copyright (C) 2002-2008 Hongwei Xi, Boston University
**
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
** 
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
** 
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
// Start Time: April 2008
//
(* ****** ****** *)

%{^
#include "libc/CATS/time.cats" // only needed for ATS/Geizella
%} // end of [%{^]

(* ****** ****** *)

staload TM = "libc_sats_time.sats"

(* ****** ****** *)

staload Deb = "ats_debug.sats"
staload Err = "ats_error.sats"
staload Fil = "ats_filename.sats"
typedef fil_t = $Fil.filename_t
staload Glo = "ats_global.sats"
staload Lst = "ats_list.sats"
staload Syn = "ats_syntax.sats"

(* ****** ****** *)

staload "ats_staexp2.sats"
staload "ats_dynexp2.sats"

(* ****** ****** *)

staload SDC = "ats_stadyncst2.sats"
staload TR2Env = "ats_trans2_env.sats"

(* ****** ****** *)

staload "ats_hiexp.sats"
staload "ats_trans4.sats"
staload "ats_ccomp.sats"
staload "ats_ccomp_env.sats"

(* ****** ****** *)

stadef fmlte = file_mode_lte

(* ****** ****** *)

fn prerr_interror () = prerr "INTERNAL ERROR (ats_ccomp_main)"

(* ****** ****** *)

fn emit_time_stamp {m:file_mode}
  (pf: fmlte (m, w) | out: &FILE m): void = let
  var time: $TM.time_t = $TM.time_get ()
  val (pfopt | p_tm) = $TM.localtime (time)
in
//
if p_tm > null then let
  prval Some_v @(pf1, fpf1) = pfopt
  val tm_min = $TM.tm_get_min (!p_tm)
  val tm_hour = $TM.tm_get_hour (!p_tm)
  val tm_mday = $TM.tm_get_mday (!p_tm)
  val tm_mon = 1 + $TM.tm_get_mon (!p_tm)
  val tm_year = 1900 + $TM.tm_get_year (!p_tm)
  prval () = fpf1 (pf1)
in
  fprint1_string (pf | out, "/*\n");
  fprint1_string (pf | out, "**\n");
  fprint1_string (pf | out,
    "** The C code is generated by ATS/Anairiats\n"
  );
  fprint1_string (pf | out, "** The compilation time is: ");
  fprintf1_exn (pf | out
  , "%i-%i-%i: %2ih:%2im\n"
  , @(tm_year, tm_mon, tm_mday, tm_hour, tm_min)
  );
  fprint1_string (pf | out, "**\n");
  fprint1_string (pf | out, "*/\n\n");
end else let
  prval None_v () = pfopt
in
  // nothing
end (* end of [if] *)
//
end // end of [emit_time_stamp]

(* ****** ****** *)

fn emit_include_header {m:file_mode}
  (pf: fmlte (m, w) | out: &FILE m): void = let
  val () = fprint1_string (pf | out, "/* include some .h files */\n")
  val () = fprint1_string (pf | out, "#ifndef _ATS_HEADER_NONE\n")
  val () = fprint1_string (pf | out, "#include \"ats_config.h\"\n")
  val () = fprint1_string (pf | out, "#include \"ats_basics.h\"\n")
  val () = fprint1_string (pf | out, "#include \"ats_types.h\"\n")
  val () = fprint1_string (pf | out, "#include \"ats_exception.h\"\n")
  val () = fprint1_string (pf | out, "#include \"ats_memory.h\"\n")
  val () = fprint1_string (pf | out, "#endif /* _ATS_HEADER_NONE */\n")
  val () = fprint1_char (pf | out, '\n')
in
  // empty
end // end of [emit_include_header]

(* ****** ****** *)

fn emit_include_cats {m:file_mode}
  (pf: fmlte (m, w) | out: &FILE m): void = let
  val () = fprint1_string (pf | out, "/* include some .cats files */\n")
  val () = fprint1_string (pf | out, "#ifndef _ATS_PRELUDE_NONE\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/array.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/basics.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/bool.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/byte.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/char.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/float.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/integer.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/integer_fixed.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/integer_ptr.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/lazy.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/lazy_vt.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/pointer.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/printf.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/reference.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/sizetype.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/string.cats\"\n")
  // common data structures
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/array.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/list.cats\"\n")
  val () = fprint1_string (pf | out, "#include \"prelude/CATS/option.cats\"\n")
  val () = fprint1_string (pf | out, "#endif /* _ATS_PRELUDE_NONE */\n")
in
  // empty
end // end of [emit_include_cats]

(* ****** ****** *)

fn atarray_name_test
  (name: string): bool = let
  val name = string1_of_string name
in
  if string_is_at_end (name, 0) then false else
    eq_char_char (string_get_char_at (name, 0), '\[')
  // end of [if]
end // end of [atarray_name_test]

fn fprint_atarray_name {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, name: string
) : void = let
  fun aux {n,i:nat | i <= n}
    (out: &FILE m, name: string n, i: size_t i)
    : void = begin
    if string_is_at_end (name, i) then ()
    else let
      val c = name[i]
    in
      if c <> ']' then begin
        fprint1_char (pf | out, c); aux (out, name, i+1)
      end
    end // end of [if]
  end // end of [aux]
  val name = string1_of_string name
in
  if string_is_at_end (name, 0) then () else aux (out, name, 1)
end // end of [fprint_atarray_name]

fn emit_typdef_rec {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, lnames: labstrlst
) : void = let
  fun aux (out: &FILE m, lnames: labstrlst)
    : void = begin case+ lnames of
    | LABSTRLSTcons (l, name, lnames) => let
        val () = case+ 0 of
        | _ when atarray_name_test name => let
            val () = fprint_atarray_name (pf | out, name)
            val () = fprint1_string (pf | out, " atslab_")
            val () = emit_label (pf | out, l)
            val () = fprint1_string (pf | out, "[] ;\n")
          in
            // empty
          end
        | _ => let
            val () = fprint1_string (pf | out, name)
            val () = fprint1_string (pf | out, " atslab_")
            val () = emit_label (pf | out, l)
            val () = fprint1_string (pf | out, " ;\n")
          in
            // empty
          end
      in
        aux (out, lnames)
      end
    | LABSTRLSTnil () => ()
  end // end of [aux]
in
  fprint1_string (pf | out, "typedef struct {\n");
  aux (out, lnames);
  fprint1_string (pf | out, "}")
end // end of [emit_typdef_rec]

fn emit_typdef_sum
  {m:file_mode} (
    pf: fmlte (m, w)
  | out: &FILE m
  , tag: int
  , names: strlst
  ) : void = let
  fun aux (out: &FILE m, i: int, names: strlst)
    : void = begin case+ names of
    | list_cons (name, names) => let
        val () = fprint1_string (pf | out, name);
        val () = fprintf1_exn (pf | out, " atslab_%i", @(i))
        val () = fprint1_string (pf | out, " ;\n")
      in
        aux (out, i+1, names)
      end // end of [list_cons]
    | list_nil () => ()
  end // end of [aux]
in
  case+ tag of
  | _ when tag = 0 => begin
      fprint1_string (pf | out, "typedef struct {\n");
      aux (out, 0, names);
      fprint1_string (pf | out, "}")
    end
  | _ when tag = 1 => begin
      fprint1_string (pf | out, "typedef struct {\n");
      fprint1_string (pf | out, "int tag ;\n");
      aux (out, 0, names);
      fprint1_string (pf | out, "}")
    end
  | _ when tag = ~1 => begin
      fprint1_string (pf | out, "typedef struct {\n");
      fprint1_string (pf | out, "int tag ;\n");
      fprint1_string (pf | out, "char *name ;\n");
      aux (out, 0, names);
      fprint1_string (pf | out, "}")
    end
  | _ => begin
      prerr_interror ();
      prerr ": aux_sum_con: tag = "; prerr tag; prerr_newline ();
      $Err.abort {void} ()
    end // end of [_]
end // end of [emit_typdef_sum]

fn emit_typdeflst_free {m:file_mode} (
    pf: fmlte (m, w) | out: &FILE m, tds: typdeflst
  ) : int = let
  fun aux (out: &FILE m, i: int, tds: typdeflst)
    : int = begin case+ tds of
    | ~TYPDEFLSTcons (tk, name_def, tds) => let
        val () = if i > 0 then fprint1_char (pf | out, '\n')
        val () = case+ tk of
        | TYPKEYrec lnames => begin
            emit_typdef_rec (pf | out, lnames);
            fprintf1_exn (pf | out, " %s ;\n", @(name_def));
          end
        | TYPKEYsum (tag, names) => begin
            emit_typdef_sum (pf | out, tag, names);
            fprintf1_exn (pf | out, " %s ;\n", @(name_def));
          end
        | TYPKEYuni lnames => ()
      in
        aux (out, i+1, tds)
      end // end of [TYPDEFLSTcons]
    | ~TYPDEFLSTnil () => i
  end // end of [aux]
in
  aux (out, 0, tds)
end // end of [emit_typdeflst_free]

(* ****** ****** *)

fn emit_datcstlst
  {m:file_mode} (
    pf: fmlte (m, w)
  | out: &FILE m
  , s2cs: !datcstlst
  ) : int = let
//
  fun aux_conlst
    (out: &FILE m, d2cs: d2conlst)
    : void = begin case+ d2cs of
    | D2CONLSTcons (d2c, d2cs) => let
        val () = fprint1_string (pf | out, "ATSglobal(ats_sum_type, ")
        val () = emit_d2con (pf | out, d2c)
        val () = fprint1_string (pf | out, ") ;\n")
      in
        aux_conlst (out, d2cs)
      end
    | D2CONLSTnil () => ()
  end // end of [aux_conlst]
//
  fn aux_cst
    (out: &FILE m, s2c: s2cst_t)
    : void = begin case+ s2cst_conlst_get (s2c) of
    | Some d2cs => aux_conlst (out, d2cs) | None () => ()
  end // end of [aux_cst]
//
  fun aux
    (out: &FILE m, i: int, s2cs: !datcstlst): int = begin
    case+ s2cs of
    | DATCSTLSTcons (s2c, !s2cs1) => let
        val () = aux_cst (out, s2c); val n = aux (out, i+1, !s2cs1)
      in
        fold@ (s2cs); n
      end
    | DATCSTLSTnil () => (fold@ (s2cs); i)
  end // end of [aux]
//
in
  aux (out, 0, s2cs)
end // end of [emit_datcstlst]

(* ****** ****** *)

fn emit_exnconlst
  {m:file_mode} (
    pf: fmlte (m, w)
  | out: &FILE m
  , d2cs: !exnconlst
  ) : int = let
  fun aux (
      out: &FILE m
    , i: int
    , d2cs: !exnconlst
    ) : int = begin case+ d2cs of
    | EXNCONLSTcons (d2c, !d2cs1) => let
        val () = fprint1_string (pf | out, "ATSglobal(ats_exn_type, ")
        val () = emit_d2con (pf | out, d2c)
        val () = fprint1_string (pf | out, ") ;\n")
        val n = aux (out, i+1, !d2cs1);
      in
        fold@ (d2cs); n
      end
    | EXNCONLSTnil () => (fold@ d2cs; i)
  end // end of [aux]
in
  aux (out, 0, d2cs)
end // end of [emit_exnconlst]

(* ****** ****** *)

fn emit_free_glocstlst
  {m:file_mode} (
    pf: fmlte (m, w)
  | out: &FILE m
  , xs: glocstlst
  ) : int = let
  fun aux (
    out: &FILE m, i: int, xs: glocstlst
  ) : int = begin case+ xs of
    | ~GLOCSTLSTcons_clo (d2c, xs) => let
        val () = fprint1_string (pf | out, "ATSglobal(ats_clo_ptr_type, ")
        val () = emit_d2cst (pf | out, d2c)
        val () = fprint1_string (pf | out, ") ;\n")
      in
        aux (out, i+1, xs)
      end // end of [GLOCSTLSTcons_clo]
    | ~GLOCSTLSTcons_fun (d2c, xs) => let
        val () = fprint1_string (pf | out, "ATSglobal(ats_fun_ptr_type, ")
        val () = emit_d2cst (pf | out, d2c)
        val () = fprint1_string (pf | out, ") ;\n")
      in
        aux (out, i+1, xs)
      end // end of [GLOCSTLSTcons_fun]
    | ~GLOCSTLSTcons_val (d2c, vp, xs) => let
        val () = fprint1_string (pf | out, "ATSglobal(")
        val () = emit_hityp (pf | out, vp.valprim_typ)
        val () = fprint1_string (pf | out, ", ")
        val () = emit_d2cst (pf | out, d2c)
        val () = fprint1_string (pf | out, ") ;\n")
      in
        aux (out, i+1, xs)
      end // end of [GLOCSTLSTcons_val]
    | ~GLOCSTLSTnil () => i // end of [GLOCSTLSTnil]
  end // end of [aux]
in
  aux (out, 0, xs)
end // end of [emit_free_glocstlst]

(* ****** ****** *)

fn _emit_dynconset
  {m:file_mode} {l:addr} (
    pf_mod: fmlte (m, w)
  , pf_fil: !FILE m @ l
  | p_l: ptr l
  , d2cs: dynconset_t
  ) : int = let
  var i: int = 0
  viewdef V = (FILE m @ l, int @ i)
  dataviewtype ENV2
    (l:addr, i:addr) = ENV2con (l, i) of (ptr l, ptr i)
  // end of [ENV2]
  viewtypedef VT = ENV2 (l, i)
  fn f_con (pf: !V | d2c: d2con_t, env: !VT): void = let
    prval @(pf_fil, pf_int) = pf
    val+ ENV2con (p_l, p_i)= env
    val i = !p_i; val () = (!p_i := i + 1)
    val () = fprint1_string (pf_mod | !p_l, "ATSextern_val(")
    val () = (case+ 0 of
      | _ when d2con_is_exn d2c => begin
          fprint1_string (pf_mod | !p_l, "ats_exn_type, ")
        end
      | _ => begin
          fprint1_string (pf_mod | !p_l, "ats_sum_type, ")
        end // end of [_]
    ) : void // end of [val]
    val () = emit_d2con (pf_mod | !p_l, d2c)
    val () = fprint1_string (pf_mod | !p_l, ") ;\n")
  in
    pf := @(pf_fil, pf_int); fold@ env
  end
  val env = ENV2con (p_l, &i)
  prval pf = @(pf_fil, view@ i)
  val () = dynconset_foreach_main {V} {VT} (pf | d2cs, f_con, env)
  prval () = (pf_fil := pf.0; view@ i := pf.1)
  val+ ~ENV2con (_, _) = env
in
  i // the number of dynamic constructors
end // end of [_emit_dynconset]

fn emit_dynconset {m:file_mode}
  (pf: fmlte (m, w) | out: &FILE m, d2cs: dynconset_t): int =
  _emit_dynconset (pf, view@ out | &out, d2cs)

(* ****** ****** *)

#define HITARGSEP ", "

(* ****** ****** *)

fn emit_d2cst_dec
  {m:file_mode} // for a non-proof constant
  (pf: fmlte (m, w)| out: &FILE m, d2c: d2cst_t): void = let
  val hit0 = d2cst_hityp_get_some (d2c); val hit1 = hityp_decode (hit0)
//
  macdef f_isprf_mac () = begin
    fprint1_string (pf | out, "ATSextern_prf(");
    emit_d2cst (pf | out, d2c);
    fprint1_string (pf | out, ") ;\n")
  end // end of [macdef]  
//
  macdef f_isfun_FUNCLOclo_mac
    (hits_arg, hit_res) = let
(*
    val hits_arg = hityplst_encode ,(hits_arg)
    val hit_res = hityp_encode ,(hit_res)
*)
   in
     fprint1_string (pf | out, "ATSextern_val(");
     fprint1_string (pf | out, "ats_ptr_type, "); // HX: is [ats_clo_ptr_type]
     emit_d2cst (pf | out, d2c);
     fprint1_string (pf | out, ") ;\n");
   end // end of [macdef]
//
  macdef f_isfun_FUNCLOfun_mac
    (hits_arg, hit_res) = let
(*
    val hits_arg = hityplst_encode ,(hits_arg)
    val hit_res = hityp_encode ,(hit_res)
*)
  in
    case+ 0 of
    | _ when d2cst_is_fun d2c => let
        val hits_arg = hityplst_encode ,(hits_arg)
        val hit_res = hityp_encode ,(hit_res)
      in
        fprint1_string (pf | out, "extern\n");
        emit_hityp (pf | out, hit_res);
        fprint1_char (pf | out, ' ');
        emit_d2cst (pf | out, d2c);
        fprint1_string (pf | out, " (");
        emit_hityplst_sep (pf | out, hits_arg, HITARGSEP);
        fprint1_string (pf | out, ") ;\n")
       end // end of [_ when ...]
     | _ when d2cst_is_castfn d2c => () // casting function
     | _ => begin // function value
         fprint1_string (pf | out, "ATSextern_val(");
         fprint1_string (pf | out, "ats_ptr_type, "); // HX: is [ats_fun_ptr_type]
         emit_d2cst (pf | out, d2c);
         fprint1_string (pf | out, ") ;\n");
       end // end of [_]
    // end of [case]
  end // end of [macdef]
//
  macdef f_isnotfun_mac () = () where {
    val () = fprint1_string (pf | out, "ATSextern_val(")
    val () = emit_hityp (pf | out, hit0)
    val () = fprint1_string (pf | out, ", ")
    val () = emit_d2cst (pf | out, d2c)
    val () = fprint1_string (pf | out, ") ;\n")
  } // end of [_]
//
in // in of [let]
//
  case+ 0 of
  | _ when d2cst_is_proof d2c => ()
  | _ when d2cst_is_extmac d2c => ()
  | _ => begin case+ hit1.hityp_node of
    | HITfun (fc, hits_arg, hit_res) => begin case+ fc of
      | $Syn.FUNCLOclo _ => f_isfun_FUNCLOclo_mac (hits_arg, hit_res)
      | $Syn.FUNCLOfun _ => f_isfun_FUNCLOfun_mac (hits_arg, hit_res)
      end // end of [HITfun]
    | _ => f_isnotfun_mac ()
    end // end of [_]
//
end // end of [emit_d2cst_dec]

fn emit_d2cst_dec_prfck {m:file_mode} // for terminating constants
  (pf: fmlte (m, w)| out: &FILE m, d2c: d2cst_t): void = let
//
  val hit0 = d2cst_hityp_get_some (d2c); val hit1 = hityp_decode (hit0)
//
  macdef f_isprf_mac () = begin
    fprint1_string (pf | out, "extern\n");
    emit_hityp (pf | out, hityp_t_void);
    fprint1_char (pf | out, ' ');
    emit_d2cst (pf | out, d2c);
    fprint1_string (pf | out, "_prfck (");
    fprint1_string (pf | out, ") ;\n")
  end // end of [macdef]
//
in
//
  case+ 0 of
  | _ when d2cst_is_praxi d2c => ()
  | _ when d2cst_is_prfun d2c => f_isprf_mac ()
  | _ when d2cst_is_prval d2c => f_isprf_mac ()
  | _ => () // needs some fixing later
//
end // end of [emit_d2cst_dec]

(* ****** ****** *)

fn _emit_dyncstset_proc
  {m:file_mode} {l:addr} (
    pf_mod: fmlte (m, w), pf_fil: !FILE m @ l
  | p_l: ptr l, d2cs: dyncstset_t
  , proc: (fmlte (m, w) | &FILE m, d2cst_t) -> void
  ) : int = let
  var i: int = 0
  viewdef V = (FILE m @ l, int @ i)
  typedef fun_type (m:file_mode) =
    (fmlte (m, w) | &FILE m, d2cst_t) -> void
  dataviewtype ENV3 (m: file_mode, l:addr, i:addr) =
    ENV3con (m, l, i) of (ptr l, ptr i, fun_type m)
  viewtypedef VT = ENV3 (m, l, i)
  fn f_cst (pf: !V | d2c: d2cst_t, env: !VT): void = let
    prval @(pf_fil, pf_int) = pf
    val+ ENV3con (p_l, p_i, proc)= env
    val i = !p_i; val () = (!p_i := i + 1)
    val () = proc (pf_mod | !p_l, d2c)
  in
    pf := @(pf_fil, pf_int); fold@ env
  end // end of [f_cst]
  fn f_cst_if (pf: !V | d2c: d2cst_t, env: !VT): void = begin
    case+ d2cst_decarg_get (d2c) of
    | list_cons _ => () | list_nil _ => f_cst (pf | d2c, env)
  end // end of [f_cst_if]
  val env = ENV3con (p_l, &i, proc)
  prval pf = @(pf_fil, view@ i)
  val () = dyncstset_foreach_main {V} {VT} (pf | d2cs, f_cst_if, env)
  prval () = (pf_fil := pf.0; view@ i := pf.1)
  val+ ~ENV3con (_, _, _) = env
in
  i // the number of dynamic constructors
end // end of [_emit_dyncstset]

fn emit_dyncstset {m:file_mode}
  (pf: fmlte (m, w) | out: &FILE m, d2cs: dyncstset_t): int =
  _emit_dyncstset_proc (pf, view@ out | &out, d2cs, emit_d2cst_dec)
// end of [emit_dyncstset]

fn emit_dyncstset_prfck {m:file_mode}
  (pf: fmlte (m, w) | out: &FILE m, d2cs: dyncstset_t): int =
  _emit_dyncstset_proc (pf, view@ out | &out, d2cs, emit_d2cst_dec_prfck)
// end of [emit_dyncstset_prfck]

(* ****** ****** *)

fn emit_instrlst_vt {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, inss: !instrlst_vt
) : void = let
//
  fun aux
    (out: &FILE m, i: int, inss: !instrlst_vt)
    : int = begin case+ inss of
    | list_vt_cons (ins, !inss1) => let
        val () = if i > 0 then fprint1_char (pf | out, '\n')
        val () = emit_instr (pf | out, ins)
        val n = aux (out, i+1, !inss1)
      in
        fold@ (inss); n
      end
    | list_vt_nil () => (fold@ inss; i)
  end // end of [aux]
//
  val n = aux (out, 0, inss)
  val () = if n > 0 then fprint_newline (pf | out)
//
in
  // empty
end // end of [emit_instrlst_vt]

(* ****** ****** *)

fun emit_funentry_lablst
  {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, fls0: !funlablst_vt
) : void = begin case+ fls0 of
  | list_vt_cons (fl, !fls) => let
      val prfck = funlab_prfck_get fl
      val entry = funlab_entry_get_some fl
      val () = if prfck > 0 then
        fprint1_string (pf | out, "#ifdef _ATS_PROOFCHECK\n")
      // end of [if]
      val () = emit_funentry (pf | out, entry)
      val () = fprint1_string (pf | out, "\n")
      val () = if prfck > 0 then
        fprint1_string (pf | out, "#endif /* _ATS_PROOFCHECK */\n")
      // end of [if]
      val () = fprint1_string (pf | out, "\n")
      val () = emit_funentry_lablst (pf | out, !fls)
    in
      fold@ (fls0)
    end
  | list_vt_nil () => fold@ (fls0)
end // end of [emit_funentry_lablst]

fun emit_funentry_lablst_prototype
  {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, i: int, fls0: !funlablst_vt
) : int = begin case+ fls0 of
  | list_vt_cons (fl, !fls) => let
      val entry = funlab_entry_get_some fl
      val () = emit_funentry_prototype (pf | out, entry)
      val n = emit_funentry_lablst_prototype (pf | out, i+1, !fls)
    in
      fold@ (fls0); n
    end (* end of [list_vt_cons] *)
  | list_vt_nil () => (fold@ (fls0); i)
end // end of [emit_funentry_lablst_prototype]

(* ****** ****** *)

fun instrlst_vt_tmpvarmap_gen
  (inss0: !instrlst_vt): tmpvarmap_vt = let
  fun aux (m: &tmpvarmap_vt, inss0: !instrlst_vt)
    : void = begin case+ inss0 of
    | list_vt_cons (ins, !inss) => let
        val () = instr_tmpvarmap_add (m, ins); val () = aux (m, !inss)
      in
        fold@ inss0
      end
    | list_vt_nil () => fold@ inss0
  end // end of [aux]
  var m = tmpvarmap_nil ()
in
  aux (m, inss0); m
end // end of [instrlst_vt_tmpvarmap_gen]

(* ****** ****** *)

fn emit_extvallst_dec
  {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, exts: !extvallst
) : int = let
  fun aux (out: &FILE m, i: int, exts: !extvallst)
    : int = begin case+ exts of
    | EXTVALLSTcons (name, vp, !exts_rest) => let
        val () = emit_hityp (pf | out, vp.valprim_typ)
        val () = fprintf1_exn (pf | out, " %s ;\n", @(name))
        val n = aux (out, i+1, !exts_rest)
      in
        fold@ exts; n
      end
    | EXTVALLSTnil () => (fold@ exts; i)
  end // end of [aux]
in
  aux (out, 0, exts)
end // end of [emit_extvallst_dec]

fn emit_extvallst_markroot
  {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, exts: !extvallst
) : int = let
  fun aux (out: &FILE m, i: int, exts: !extvallst)
    : int = begin case+ exts of
    | EXTVALLSTcons (name, vp, !exts_rest) => let
        val () = fprint1_string (pf | out, "ATS_GC_MARKROOT (&")
        val () = fprint1_string (pf | out, name)
        val () = fprint1_string (pf | out, ", sizeof(")
        val () = emit_hityp (pf | out, vp.valprim_typ)
        val () = fprint1_string (pf | out, ")) ;\n")
        val n = aux (out, i+1, !exts_rest)
      in
        fold@ exts; n
      end
    | EXTVALLSTnil () => (fold@ exts; i)
  end // end of [aux]
in
  aux (out, 0, exts)
end // end of [emit_extvallst_markroot]

(* ****** ****** *)

fun emit_stafile_extcode
  {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, fil: fil_t
) : void = let
  val fil_sym = $Fil.filename_full_sym (fil)
  val od2cs = $TR2Env.d2eclst_namespace_find (fil_sym)
  val d2cs = (case+ od2cs of
    | ~Some_vt (d2cs) => d2cs | ~None_vt () => begin
        prerr_interror ();
        prerr ": emit_stafile_extcode: fil = "; $Fil.prerr_filename fil;
        prerr_newline ();
        $Err.abort {d2eclst} ()
      end // end of [None_vt]
  ) : d2eclst
  fun aux
    (out: &FILE m, d2cs: d2eclst): void =
    case+ d2cs of
    | list_cons (d2c, d2cs) => let
        val () = (case+ d2c.d2ec_node of
          | D2Cextcode (pos, code) => begin
              if (pos >= 0) then () else fprint1_string (pf | out, code)
            end // end of [D2Cextcode]
          | D2Cstaload (_qua, fil, _loaded, _loadflag, _d2cs) =>
              emit_stafile_extcode (pf | out, fil) // end of [D2Cstaload]
          | _ => ()
        ) : void // end of [val]
      in
        aux (out, d2cs)
      end // end of [list_cons]
    | list_nil () => ()
  // end of [aux]
in
  aux (out, d2cs)
end // end of [emit_stafile_extcode]

fun emit_stafilelst_extcode
  {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, fils: !stafilelst
) : void = begin case+ fils of
  | STAFILELSTcons (fil, loadflag, !fils_rest) => let
     val () = emit_stafile_extcode (pf | out, fil)
     val () = emit_stafilelst_extcode (pf | out, !fils_rest)
   in
     fold@ fils
   end // end of [STAFILELSTcons]
  | STAFILELSTnil () => fold@ fils
end (* end of [emit_stafilelst_extcode] *)

(* ****** ****** *)

fn emit_staload
  {m:file_mode} (
    pf: fmlte (m, w)
  | out: &FILE m, fil: fil_t
  , stafils: stafilelst, s2cs: !datcstlst, d2cs: !exnconlst
) : void = let
//
  fun aux_staload_dec (
    out: &FILE m, fils: !stafilelst
  ) : void = begin case+ fils of
    | STAFILELSTcons (fil, loadflag, !fils_rest) => let
        val () =
          if (loadflag = 0) then fprint1_string (pf | out, "// ")
        // end of [val]
        val () = fprint1_string (pf | out, "extern ")
        val () = fprint1_string (pf | out, "ats_void_type ")
        val () = emit_filename (pf | out, fil)
        val () = fprint1_string (pf | out, "__staload (void) ;\n")
        val () = aux_staload_dec (out, !fils_rest)
      in
        fold@ fils
      end // end of [STAFILELSTcons]
    | STAFILELSTnil () => fold@ fils
  end // end of [ats_staload_dec]
//
  fun aux_staload_app (
    out: &FILE m, fils: !stafilelst
  ) : void = begin case+ fils of
    | STAFILELSTcons (fil, loadflag, !fils_rest) => let
        val () =
          if (loadflag = 0) then fprint1_string (pf | out, "// ")
        // end of [val]
        val () = emit_filename (pf | out, fil)
        val () = fprint1_string (pf | out, "__staload () ;\n")
        val () = aux_staload_app (out, !fils_rest)
      in
        fold@ fils
      end // end of [STAFILELSTcons]
    | STAFILELSTnil () => fold@ fils
  end // end of [ats_staload_app]
//
  fun aux_staload_datcstlst
    (out: &FILE m, s2cs: !datcstlst): int = let
    fun aux_conlst (out: &FILE m, d2cs: d2conlst)
      : void = begin case+ d2cs of
      | D2CONLSTcons (d2c, d2cs) => let
          val () = begin // only needed for a constructor with no arguments!
            if d2con_arity_real_get d2c > 0 then fprint1_string (pf | out, "// ")
          end // end of [val]
          val () = emit_d2con (pf | out, d2c);
          val tag = d2con_tag_get d2c
          val () = fprintf1_exn (pf | out, ".tag = %i ;\n", @(tag))
        in
          aux_conlst (out, d2cs)
        end // end of [D2CONLSTcons]
      | D2CONLSTnil () => ()
    end // end of [aux_conlst]
    fn aux_cst (out: &FILE m, s2c: s2cst_t)
      : void = begin case+ s2cst_conlst_get (s2c) of
      | Some d2cs => aux_conlst (out, d2cs) | None () => ()
    end // end of [aux_cst]
    fun aux (out: &FILE m, i: int, s2cs: !datcstlst): int = begin
      case+ s2cs of
      | DATCSTLSTcons (s2c, !s2cs1) => let
          val () = aux_cst (out, s2c); val n = aux (out, i+1, !s2cs1)
        in
          fold@ s2cs; n
        end
      | DATCSTLSTnil () => (fold@ s2cs; i)
    end // end of [aux]
  in
    aux (out, 0, s2cs)
  end // end of [aux_staload_datcstlst]
//
  fun aux_staload_exnconlst
    (out: &FILE m, d2cs: !exnconlst): int = let
    fun aux (out: &FILE m, i: int, d2cs: !exnconlst): int = begin
      case+ d2cs of
      | EXNCONLSTcons (d2c, !d2cs1) => let
          val () = emit_d2con (pf | out, d2c)
          val () = fprint1_string (
            pf | out, ".tag = ats_exception_con_tag_new () ;\n"
          ) // end of [fprint1_string]
          val () = emit_d2con (pf | out, d2c)
          val () = fprint1_string (pf | out, ".name = \"")
(*
          val () = $Fil.fprint1_string_filename (pf | out, d2con_fil_get d2c)
          val () = fprint1_string (pf | out, "::")
          val () = fprint1_string_d2con (pf | out, d2c)
*)
          val () = emit_d2con (pf | out, d2c)
          val () = fprint1_string (pf | out, "\" ;\n")
          val n = aux (out, i+1, !d2cs1)
        in
          fold@ d2cs; n
        end // end of [EXNCONLSTcons]
      | EXNCONLSTnil () => (fold@ d2cs; i)
    end // end of [aux]
  in
    aux (out, 0, d2cs)
  end // end of [aux_staload_exnconlst]
(*  
  // *_staload function should always be defined!
  val () = fprint1_string (pf | out, "#ifndef _ATS_STALOADFUN_NONE\n")
*)
  val () = aux_staload_dec (out, stafils)
//
  val () = fprint1_string (pf | out, "static int ")
  val () = emit_filename (pf | out, fil)
  val () = fprint1_string (pf | out, "__staload_flag = 0 ;\n\n")
  val () = fprint1_string (pf | out, "ats_void_type\n")
  val () = emit_filename (pf | out, fil)
  val () = fprint1_string (pf | out, "__staload () {\n")
  val () = fprint1_string (pf | out, "if (");
  val () = emit_filename (pf | out, fil)
  val () = fprint1_string (pf | out, "__staload_flag) return ;\n")
  val () = emit_filename (pf | out, fil)
  val () = fprint1_string (pf | out, "__staload_flag = 1 ;\n")
//
  val () = aux_staload_app (out, stafils)
//
  val () = stafilelst_free (stafils)
//
  val _(*int*) = aux_staload_datcstlst (out, s2cs)
  val _(*int*) = aux_staload_exnconlst (out, d2cs)
//
  val () = fprint1_string (pf | out, "return ;\n")
  val () = fprint1_string (pf | out, "} /* staload function */\n")
(*
  val () = fprint1_string (pf | out, "#endif /* [_ATS_STALOADFUN_NONE] */\n\n")
*)
in
  // empty
end // end of [emit_staload]

(* ****** ****** *)

fn emit_dynload
  {m:file_mode} (
    pf: fmlte (m, w)
  | out: &FILE m
  , dynloadflag: int
  , fil: fil_t
  , res: !instrlst_vt
  , tmps: !tmpvarmap_vt
  , exts: !extvallst
  ) : void = let
//
  // code for dynamic loading
  val dynfils = the_dynfilelst_get ()
  val () = aux_dynload_dec (out, dynfils) where {
    fun aux_dynload_dec
      (out: &FILE m, fils: !dynfilelst): void = case+ fils of
      | DYNFILELSTcons (fil, !fils_rest) => let
          val () = fprint1_string (pf | out, "int ")
          val () = emit_filename (pf | out, fil)
          val () = fprint1_string (pf | out, "__dynload_flag = 0 ;\n")
          val () = fprint1_string (pf | out, "extern\n")
          val () = fprint1_string (pf | out, "ats_void_type ")
          val () = emit_filename (pf | out, fil)
          val () = fprint1_string (pf | out, "__dynload (void) ;\n")
          val () = aux_dynload_dec (out, !fils_rest)
        in
          fold@ fils
        end // end of [DYNFILELSTcons]
      | DYNFILELSTnil () => fold@ fils
    // end of [aux_dynload_dec]
  } // end of [where]
  val () = dynfilelst_free (dynfils)
//
  val () = fprint1_string
    (pf | out, "// (external) dynload flag declaration\n")
  // end of [val]
//
  val () = let
    val () = if dynloadflag = 0 then fprint1_string (pf | out, "// ")
    val () = fprint1_string (pf | out, "extern\n")
    val () = if dynloadflag = 0 then fprint1_string (pf | out, "// ")
    val () = fprint1_string (pf | out, "int ")
    val () = emit_filename (pf | out, fil)
    val () = fprint1_string (pf | out, "__dynload_flag ;\n\n")
  in
    // empty
  end // end of [val]
//
  val () = fprint1_string (pf | out, "ats_void_type\n")
  val () = emit_filename (pf | out, fil)
  val () = fprint1_string (pf | out, "__dynload () {\n")
//
  val () = let
    val () =
      if dynloadflag = 0 then fprint1_string (pf | out, "// ")
    val () = emit_filename (pf | out, fil)
    val () = fprint1_string (pf | out, "__dynload_flag = 1 ;\n")
  in
    // empty
  end // end of [val]
//
  // code for static loading
  val () = emit_filename (pf | out, fil)
  val () = fprint1_string (pf | out, "__staload () ;\n")
//
  // code for termination checking
  val () = fprint1_string (pf | out, "#ifdef _ATS_PROOFCHECK\n")
  stavar l_out: addr; val p_out: ptr l_out = &out
  val () = dyncstset_foreach_main {FILE m @ l_out} {ptr l_out}
    (view@ out | the_dyncstset_get (), f, p_out) where {
    fn f (pf_out: !FILE m @ l_out | d2c: d2cst_t, p_out: !ptr l_out): void = let
      val () = begin case+ 0 of
        | _ when d2cst_is_praxi (d2c) => ()
        | _ when d2cst_is_prfun (d2c) => begin
            emit_d2cst (pf | !p_out, d2c); fprint1_string (pf | !p_out, "_prfck () ;\n")
          end // end of [_]
        | _ when d2cst_is_prval (d2c) => begin
            emit_d2cst (pf | !p_out, d2c); fprint1_string (pf | !p_out, "_prfck () ;\n")
          end // end of [_]
        | _ => () // should nonproof terminating functions be checked as well?
      end // end of [val]
    in
      // empty
    end // end of [f]
  } // end of [where]
  val () = fprint1_string (pf | out, "#endif /* _ATS_PROOFCHECK */\n")
//
  // code marking GC roots
  val () = fprint1_string
    (pf | out, "\n/* marking static variables for GC */\n")
  val _(*n*) = emit_tmpvarmap_markroot (pf | out, tmps)
  val () = fprint1_string
    (pf | out, "\n/* marking external values for GC */\n")
  val _(*n*) = emit_extvallst_markroot (pf | out, exts)
//
  val () = fprint1_string
    (pf | out, "\n/* code for dynamic loading */\n")
  val () = emit_instrlst_vt (pf | out, res)
//
  val () = fprint1_string (pf | out, "return ;\n")
  val () = fprint1_string (pf | out, "} /* end of [dynload function] */\n\n")
//
  // this is used for explicit dynamic loading
  val () = let
    val name = $Glo.atsopt_dynloadfun_name_get () // ATS_DYNLOADFUN_NAME
  in
    case+ 0 of
    | _ when stropt_is_some name => let
        val name = stropt_unsome name
        val () = fprintf1_exn (pf | out, "ats_void_type %s () {\n", @(name))
        val () = emit_filename (pf | out, fil)
        val () = fprint1_string (pf | out, "__dynload () ; return ;\n}\n\n")
      in
        // empty
      end // end of [_ when ...]
    | _ => () // end of [_]
  end // end of [val]
//
in
  // empty
end // end of [emit_dynload]

(* ****** ****** *)

fn emit_extypelst_free
  {m:file_mode} (
  pf: fmlte (m, w) | out: &FILE m, ets: extypelst
) : int = let
  fun aux (out: &FILE m, i: int, ets: extypelst): int =
    case+ ets of
    | ~EXTYPELSTcons (name, hit_def, ets) => let
        val hit_def = hityp_decode hit_def
        val HITNAM (knd, name_def) = hit_def.hityp_name
        val () = fprintf1_exn (pf | out, "typedef %s ", @(name_def))
        val () = if knd > 0 then fprint1_char (pf | out, '*')
        val () = fprintf1_exn (pf | out, "%s ;\n", @(name))
      in
        aux (out, i + 1, ets)
      end
    | ~EXTYPELSTnil () => i
in
  aux (out, 0, ets)
end // end of [emit_extypelst_free]

(* ****** ****** *)

fn emit_extcodelst
  {m:file_mode} (
    pf: fmlte (m, w)
  | out: &FILE m
  , pos0: int (* top(0), mid(1), bot(2) *)
  , xs0: &extcodelst
  ) : int = let
//
  fn test (
     pos0: int, pos: int
  ) : bool =
    case+ 0 of
    | _ when pos0 = 0 => pos <= 0 (* pos = ~1 or pos = 0 *)
    | _ when pos0 = 1 => pos = 1
    | _ => true // pos = 2
  (* end of [test] *)
//
  fun aux_main (
      out: &FILE m
    , pos0: int
    , xs0: &extcodelst
    , i: &int
    ) : void = begin case+ xs0 of
    | EXTCODELSTcons
        (loc, pos, code, !p_xs) => let
      in
        if test (pos0, pos) then let
//
          val gline = $Deb.gline_flag_get ()
          val () = if gline >= 1 then
            $Loc.fprint_line_pragma (pf | out, loc)
          // end of [val]
//
          val () = fprint1_string (pf | out, code)
          val xs = !p_xs; val () = free@ (xs0); val () = xs0 := xs
          val () = i := i + 1
        in
          aux_main (out, pos0, xs0, i)
        end else let
          val () = aux_main (out, pos0, !p_xs, i)
          val () = fold@ (xs0)
        in
          // nothing
        end (* end of [if] *)
      end // end of [EXTCODELSTcons]
    | EXTCODELSTnil () => fold@ (xs0)
  end // end of [aux]
//
  var i: int = 0
//
in
  aux_main (out, pos0, xs0, i); i
end // end of [emit_extcodelst]

(* ****** ****** *)

fn main_void_is_implemented (): bool = let
  val d2c = $SDC.d2cstref_cst_get ($SDC.Ats_main_void)
in
  case+ the_topcstctx_find (d2c) of
  | ~Some_vt _ => true | ~None_vt () => false
end // end of [main_void_is_implemented]

fn main_argc_argv_is_implemented (): bool = let
  val d2c = $SDC.d2cstref_cst_get ($SDC.Ats_main_argc_argv)
in
  case+ the_topcstctx_find (d2c) of
  | ~Some_vt _ => true | ~None_vt () => false
end // end of [main_argc_argv_is_implemented]

fn main_dummy_is_implemented (): bool = let
  val d2c = $SDC.d2cstref_cst_get ($SDC.Ats_main_dummy)
in
  case+ the_topcstctx_find (d2c) of
  | ~Some_vt _ => true | ~None_vt () => false
end // end of [main_dummy_is_implemented]

(* ****** ****** *)

#define MAINATS_NONE ~1
#define MAINATS_VOID 0
#define MAINATS_ARGC_ARGV 1
#define MAINATS_DUMMY 2

fn mainatsknd_get (): int = let
  val is_main_void = main_void_is_implemented ()
  val is_main_argc_argv = main_argc_argv_is_implemented ()
in
  if is_main_void then begin
    if not (is_main_argc_argv) then MAINATS_VOID else let
      val () = prerr "error(ccomp)"
      val () = prerr ": it is not allowed to implement both [main_void] and [main_argc_argv]"
      val () = prerr_newline ()
    in
      $Err.abort {int} ()
    end // end of [if]
  end else begin
    if is_main_argc_argv then MAINATS_ARGC_ARGV else begin
      if main_dummy_is_implemented () then MAINATS_DUMMY else MAINATS_NONE
    end // end of [if]
  end (* end of [if] *)
end // end of [main_is_implemented]

(* ****** ****** *)

implement ccomp_main {m}
  (pf | flag, out, fil, hids) = let
  var res: instrlst_vt = list_vt_nil ()
  val () = ccomp_declst (res, hids)
  val () = the_dynctx_free ()
  val fls: funlablst_vt = funentry_lablst_get ()
  val res = $Lst.list_vt_reverse (res)
//
  val () = emit_time_stamp (pf | out)
  val () = emit_include_header (pf | out)
  val () = if flag > 0 then emit_include_cats (pf | out)
//
  val stafils = the_stafilelst_get ()
  val () = () where {
    val () = fprint1_string
      (pf | out, "/* prologue from statically loaded files */\n")
    val () = emit_stafilelst_extcode (pf | out, stafils)
  } // end of [val]
//
  var extcodes = the_extcodelst_get ()
  val () = fprint1_string (pf | out, "/* external codes at top */\n")
  val n = emit_extcodelst (pf | out, 0(*top*), extcodes)
  val () = if n > 0 then fprint1_char (pf | out, '\n')
//
  val () = let // type definitions
    val () = fprint1_string (pf | out, "/* type definitions */\n")
    val n = emit_typdeflst_free (pf | out, typdeflst_get ())
  in
    if n > 0 then fprint1_char (pf | out, '\n')
  end // end of [val]
//
  val () = let // external type definitions
    val () = fprint1_string (pf | out, "/* external typedefs */\n")
    val ets = the_extypelst_get ()
    val n = emit_extypelst_free (pf | out, ets)
  in
    if n > 0 then fprint1_char (pf | out, '\n')
  end // end of [val]
//
  val () = if (flag > 0) then let // declaration for dynamic constructors
    val () = fprint1_string
      (pf | out, "/* external dynamic constructor declarations */\n")
    val n = emit_dynconset (pf | out, the_dynconset_get ())
  in
    if n > 0 then fprint1_char (pf | out, '\n')
  end  // end of [val]
//
  val () = if (flag > 0) then let // declaration for dynamic constants
    val () = begin
      fprint1_string (pf | out, "/* external dynamic constant declarations */\n")
    end // end of [val]
    val n = emit_dyncstset (pf | out, the_dyncstset_get ())
  in
    if n > 0 then fprint1_char (pf | out, '\n')
  end // end of [val]
//
  val () = if (flag > 0) then let // declaration for dynamic terminating constants
    val () = fprint1_string
      (pf | out, "/* external dynamic terminating constant declarations */\n")
    val () = fprint1_string (pf | out, "#ifdef _ATS_PROOFCHECK\n")
    val n = emit_dyncstset_prfck (pf | out, the_dyncstset_get ())
    val () = if n = 0 then fprint1_string (pf | out, "/* empty */\n")
    val () = fprint1_string (pf | out, "#endif /* _ATS_PROOFCHECK */\n\n")
  in
    // empty
  end // end of [val]
//
  val datcsts = the_datcstlst_get ()
  val () = let
    val () = fprint1_string (pf | out, "/* sum constructor declarations */\n")
    val n = emit_datcstlst (pf | out, datcsts)
  in
    if n > 0 then fprint1_char (pf | out, '\n')
  end // end of [val]
//
  val exncons = the_exnconlst_get ()
  val () = let
    val () = fprint1_string (pf | out, "/* exn constructor declarations */\n")
    val n = emit_exnconlst (pf | out, exncons)
  in
    if n > 0 then fprint1_char (pf | out, '\n')
  end // end of [val]
//
  val () = if (flag > 0) then let
(*
** HX: declaring implemented non-functional constants
*)
    val glocstlst = the_glocstlst_get ()
    val () = fprint1_string
      (pf | out, "/* global dynamic (non-functional) constant declarations */\n")
    val n = emit_free_glocstlst (pf | out, glocstlst)
  in
    if n > 0 then fprint1_char (pf | out, '\n')
  end // end of [if] // end of [val]
//
  val () = if (flag > 0) then let
    val () = begin
      fprint1_string (pf | out, "/* internal function declarations */\n")
    end
    val n = emit_funentry_lablst_prototype (pf | out, 0, fls)
    val () = if n > 0 then fprint1_char (pf | out, '\n')
  in
    // empty
  end // end of [val]
//
  val tmps_static = instrlst_vt_tmpvarmap_gen (res)
//
  val () = if (flag > 0) then let // static variable declarations
    val () = begin
      fprint1_string (pf | out, "/* static temporary variable declarations */\n")
    end // end of [val]
    val n = emit_tmpvarmap_dec_static (pf | out, tmps_static)
    val () = if n > 0 then fprint1_char (pf | out, '\n')
  in
    // empty
  end // end of [if] // end of [val]
//
  val extvals = the_extvallst_get ()
//
  val () = if (flag > 0) then let // external variable declarations
    val () = begin
      fprint1_string (pf | out, "/* external value variable declarations */\n\n")
    end // end of [val]
    val n = emit_extvallst_dec (pf | out, extvals)
    val () = if n > 0 then fprint1_char (pf | out, '\n')
  in
    // empty
  end // end of [if] // end of [val]
//
  val fls = (
    if (flag > 0) then let
      val () = fprint1_string (pf | out, "/* function implementations */\n\n")
      val () = emit_funentry_lablst (pf | out, fls)
    in
      fls
    end else begin
      fls
    end // end of [if]
  ) : funlablst_vt
//
  val () = let
    val () = fprint1_string (pf | out, "/* static load function */\n\n")
    val () = emit_staload (pf | out, fil, stafils, datcsts, exncons)
  in
    // empty
  end // end of [val]
//
  val mainatsknd = mainatsknd_get ()
//
(*
  val () = begin
    print "ccomp_main: mainatsknd = "; print mainatsknd; print_newline ()
  end // end of [val]
*)
//
  val res = (
    if flag > 0 then let // defining the dynload function
      val dynloadflag =
        (if mainatsknd >= 0 then 0 else $Glo.atsopt_dynloadflag_get ()): int
      val () = fprint1_string (pf | out, "/* dynamic load function */\n\n")
      val () = emit_dynload
        (pf | out, dynloadflag, fil, res, tmps_static, extvals)
    in
      res
    end else begin
      res
    end // end of [if]
  ) : instrlst_vt
//
  val () = $Lst.list_vt_free__boxed (res)
  val () = tmpvarmap_free (tmps_static)
  val () = extvallst_free (extvals)
//
  val () = begin case+ 0 of
    | _ when mainatsknd >= 0 => begin
        emit_mainfun (pf | out, fil); fprint1_char (pf | out, '\n')
      end // end of [_ when ...]
    | _ => () // end of [_]
  end // end of [val]
//
  val () = $Lst.list_vt_free__boxed (fls)
//
  val () = fprint1_string (pf | out, "/* external codes at mid */\n")
  val n = emit_extcodelst (pf | out, 1(*mid*), extcodes)
  val () = if n > 0 then fprint1_char (pf | out, '\n')
  val () = fprint1_string (pf | out, "/* external codes at bot */\n")
  val n = emit_extcodelst (pf | out, 2(*bot*), extcodes)
  val () = if n > 0 then fprint1_char (pf | out, '\n')
//
  val () = datcstlst_free (datcsts)
  val () = exnconlst_free (exncons)
  val () = extcodelst_free (extcodes)
//
in
  // empty
end // end of [ccomp_main]

(* ****** ****** *)

(* end of [ats_ccomp_main.dats] *)