(*
HX-2019-03-26:

The original code is available at
https://gist.github.com/ashalkhakov/c3577e97b20020fde31f84447fd1e056

I turned runCommand into a polymorphic function and
also made Command a linear datatype (i.e., dataviewtype)

*)

(*

inspired by this discussion:

https://groups.google.com/forum/#!topic/ats-lang-users/fICcWumT9RE

runnable over at glot.io:

https://glot.io/snippets/fapb07meuz

to build and run:

patscc -DATS_MEMALLOC_LIBC main.dats && a.out
*)
#include
"share/atspre_staload.hats"

%{

// NOTE: this is really from ATS2 prelude
// (newer version of prelude includes this)
extern
atstype_ptr
atspre_fileref_get_line_string_main2
(
  atstype_int bsz0
, atstype_ptr filp0
, atstype_ref nlen0 // int *nlen
)
{
//
  int bsz = bsz0 ;
  int ofs1 = 0, ofs2 = 0;
  int *nlen = (int*)nlen0;
  FILE *filp = (FILE*)filp0 ;
  char *buf1, *buf2, *pres ;
//
  buf1 = atspre_malloc_gc(bsz) ;
//
  while (1) {
    buf2 = buf1+ofs1 ;
    pres = fgets(buf2, bsz-ofs1, filp) ;
    if (!pres)
    {
      if (feof(filp))
      {
        *buf2 = '\0' ;
        *nlen = ofs1 ; return buf1 ;
      } else {
        atspre_mfree_gc(buf1) ;
        *nlen = -1 ; return (char*)0 ;
      } // end of [if]
    }
//
    ofs2 = strlen(buf2) ;
//
    if
    (ofs2 > 0) ofs1 += ofs2 ; else return buf1;
//
// HX: ofs1 > 0 holds at this point
// HX: the newline symbol needs to be trimmed:
//
    if(
    buf1[ofs1-1]=='\n'
    ) {
    buf1[ofs1-1] = '\0'; *nlen = ofs1-1 ; return buf1 ;
    } // end of [if]
//
// HX: there is room // so there are no more chars:
//
    if (ofs1+1 < bsz) { ( *nlen = ofs1 ) ; return buf1 ; }
//
// HX: there is no room // another call to [fgets] is needed:
//
    bsz *= 2 ;
    buf2 = buf1 ;
    buf1 = atspre_malloc_gc(bsz) ;
    memcpy(buf1, buf2, ofs1) ; atspre_mfree_gc(buf2) ;
  } // end of [while]
//
  return buf1 ; // HX: this is really deadcode
//
} // end of [atspre_fileref_get_line_string_main2]

%}

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

// well, this is untested and may be ignored.
// initially this block was introduced so that
// we might allocate the temporaries for "binds" on stack
%{^

#include <alloca.h>

#if __STDC_VERSION__ >= 201112L /* C11 */

#include <stdalign.h>

#define ALIGN_OF(type) (alignof(type))

#else /* not C11 */

#define ALIGN_OF(type) ((size_t)&((struct { char c; type d; } *)0)->d)

#endif

// using GCC "statement expressions"
#define ALLOCA_TYPE(type) ({ \
   const int align = ALIGN_OF(type); \
   const int n = sizeof(type); \
   void *p = alloca(n + align - 1); \
   (type *)(((UINT_PTR)p + (ALIGN_OF(type) - 1)) & ~(ALIGN_OF(type) - 1)); \
})

%}

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

// an abstract type of "commands"
absvtype
Command_vtype(a:vtype) = ptr
vtypedef Command(a:vtype) = Command_vtype(a)

// a command interpreter
// NOTE: it requires the user to provide a continuation
extern
fun
runCommand
{a:vtype}
(c:Command(a:vtype)): (a)

// the returned command will perform c1, then c2
extern
fun seq
(c1:Command(unit), c2: Command(unit)): Command(unit)

// a more powerful sequencing operator: this feeds the output of c1
// into c2
extern
fun
bind
{a:vtype}{b:vtype}
(c1:Command(a), c2: a -<cloptr1> Command(b)): Command(b)

// build a command that will provide us with input from  user
extern
fun cread (): Command(string)
// build a command to print a string to console
extern
fun cprint (s:string): Command(unit)

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

extern
fun
fgetstring
  (inp: FILEref): string

local

// the command sub-language
datavtype
Command(vtype) =
  | Nop(unit)
  | Read(string)
  | Print(unit) of string
  | Seq(unit) of (Command(unit), Command(unit))
  | {a,b:vtype} Bind(b) of (Command(a), a -<cloptr1> Command(b))

assume Command_vtype = Command

in // in of [local]

implement
cprint (s) = Print s
implement
cread () = Read ()
implement
seq(c1, c2) = Seq(c1, c2)
implement
bind{a}{b}(c1, fc2) = Bind(c1, fc2)

implement
fgetstring (inp) = let
//
var nlen: int // uninitialized
val line = fileref_get_line_string_main(inp, nlen)
prval () = lemma_strnptr_param(line)
//
in
  g0ofg1(strnptr2string(line))
end // end of [fgetstring]

implement
runCommand{a}(c) =
  case+ c of
  | ~Nop() => unit
  | ~Print(s) =>
    let val () = print (s) in unit end
  | ~Read() => fgetstring(stdin_ref)
  | ~Seq (c1, c2) =>
    let val _ = runCommand(c1) in runCommand(c2) end
  | ~Bind(c1, fc2) =>
    let
      val r1 = fc2(runCommand(c1))
    in
      cloptr_free($UNSAFE.castvwtp0{cloptr(void)}(fc2)); runCommand(r1)
    end

end // end of [local]
//
(* ****** ****** *)

extern
fun
test0 (): void
implement
test0 () = let
  val hello =
  let val h1 = cprint "hi" val h2 = cprint "hi" in seq (h1, h2) end // here. twice the effect!
  val hello = seq (hello, cprint "\n")
  val unit() = runCommand (hello)

  // a bigger program
  // (this one shows how the interpreter interacts with the command-building
  // process, which is our program)
  val greet = let
    val h = cprint "what is your name?\n"
    val g = cread ()
    val f = lam (name) =<cloptr1> seq (cprint "hello, ", seq (cprint name, cprint "\n"))
  in
    seq (h, bind (g, f))
  end
  val unit() = runCommand (greet)
in
  (*nop*)
end

implement
main0 () = test0 ()