Skip to content

Instantly share code, notes, and snippets.

@ashalkhakov
Last active August 7, 2019 13:50
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save ashalkhakov/c3577e97b20020fde31f84447fd1e056 to your computer and use it in GitHub Desktop.
Save ashalkhakov/c3577e97b20020fde31f84447fd1e056 to your computer and use it in GitHub Desktop.
IO monad in ATS
(*
HX-2019-03-26-2:
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)
AS-2019-03-26:
This version by HX also does a pre-allocation of 'bind' temporaries,
hence it supports unboxed result and intermediate types in Command.
Very nifty.
*)
(*
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:vt@ype) = ptr
vtypedef Command(a:vt@ype) = Command_vtype(a)
// a command interpreter
// NOTE: it requires the user to provide a continuation
extern
fun
{a:vt@ype}
runCommand
(cmd:Command(a)): a
extern
fun
runCommand2
{a:vt@ype}
(cmd:Command(a), &a? >> a): void
implement
{a}
runCommand(cmd) =
let var r0: a in runCommand2(cmd, r0); r0 end
// 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
{a:vt@ype}
{b:vt@ype}
bind
( 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
fun
{a:vt@ype}
assign(r0: &a? >> a, x0: a): void = (r0 := x0)
local
extern
fun
runCommand
{a:vt@ype}
(c:Command(a:vt@ype), &a? >> a): void
datavtype
Command(vt@ype) =
| Nop(unit)
| Read(string)
| Print(unit) of string
| Seq(unit) of (Command(unit), Command(unit))
| {a,b:vt@ype} Bind(b) of (Command(a), (&a >> a?) -<cloptr1> Command(b), a?)
assume Command_vtype = Command
in // in of [local]
implement
cprint (s) = Print s
implement
cread () = Read ()
implement
seq(c1, c2) = Seq(c1, c2)
implement
{a}{b}
bind(c1, fc2) =
Bind(c1, fc2, $UNSAFE.castvwtp0{a?}(0))
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
runCommand2{a}
(cmd, r0) =
case+ cmd of
| ~Nop() =>
assign<unit>(r0, unit)
| ~Print(s) =>
let
val () = print (s)
in assign<unit>(r0, unit) end
| ~Read() =>
let
val x0 =
fgetstring(stdin_ref)
in
assign<string>(r0, x0)
end
| ~Seq (c1, c2) =>
(runCommand2(c1, r0); runCommand2(c2, r0))
| @Bind(c1, fc2, r1) =>
let
val () =
runCommand2(c1, r1)
val fc2 = fc2
val cmd2 = fc2(r1)
in
free@(cmd); cloptr_free($UNSAFE.castvwtp0{cloptr(void)}(fc2)); runCommand2(cmd2, r0)
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: &string): Command(unit) =<cloptr1>
let val name = name in seq (cprint "hello, ", seq (cprint name, cprint "\n")) end
in
seq (h, bind (g, f))
end
val unit() = runCommand (greet)
in
(*nop*)
end
implement
main0 () = test0 ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment