Last active
August 7, 2019 13:50
-
-
Save ashalkhakov/c3577e97b20020fde31f84447fd1e056 to your computer and use it in GitHub Desktop.
IO monad in ATS
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* | |
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