contrib/gavinz: brainfxxk interpreter example

contrib/gavinz/brainfxxk/.gitignore

@@ -0,0 +1,4 @@
+BUILD/*.js
+BUILD/JS/*.js
+lib/*.js
+UTIL/*.js

contrib/gavinz/brainfxxk/DATS/brainfxxk.dats

@@ -0,0 +1,109 @@
+#staload _ = "prelude/DATS/gdbg000.dats"
+#include "srcgen2/prelude/HATS/prelude_dats.hats"
+#include "srcgen2/prelude/HATS/prelude_JS_dats.hats"
+#include "srcgen2/prelude/HATS/prelude_NODE_dats.hats"
+
+#staload "contrib/gavinz/xatslib/SATS/proc000.sats"
+#staload "contrib/gavinz/xatslib/SATS/file000.sats"
+
+val UCHARMAX = 255
+val TAPESIZE = 4096
+(*
+#define UCHARMAX 255
+#define TAPE_SIZE 4096 // not supported
+*)
+
+#typedef cell = uint
+#typedef mptr = uint
+// #typedef mstate = a1rf(uint, 4096)
+
+excptcon Overflow of ()
+excptcon Underflow of ()
+excptcon RBNotFound of ()
+excptcon LBNotFound of ()
+
+fun max(x, y) = if x >= y then x else y
+
+fun interp {pl:nat} (prog: strn): void = let
+  val proglen: int(pl) = (strn_length prog)
+  and state: a1rf(int) = a1rf_make_ncpy(TAPESIZE, 0)
+
+  fun find_match_rb 
+    {pn:nat | pn < pl} 
+    (start: int(pn)): [px: nat | pn < px && px < pl] int(px) = let
+      fun loop 
+        (idx: int, acc: int): int = 
+          if idx >= proglen
+          then $raise RBNotFound()
+          else (
+            case+ 0 of
+            | _ when (prog[idx] = '[') => loop (idx + 1, acc + 1)
+            | _ when (prog[idx] = ']') => if acc = 1 then idx else loop (idx + 1, acc - 1)
+            | _ => loop (idx + 1, acc)
+          )
+  in
+    loop (start + 1, 1)
+  end
+
+  fun find_match_lb 
+    {pn:nat | pn < pl} 
+    (start: int(pn)): [px: nat | px < pn] int(px) = let
+      fun loop 
+        (idx: int, acc: int): int = 
+          if idx = (-1)
+          then $raise LBNotFound()
+          else (
+            case+ 0  of
+            | _ when (prog[idx] = '[') => if acc = 1 then idx else loop (idx - 1, acc - 1)
+            | _ when (prog[idx] = ']') => loop (idx - 1, acc + 1)
+            | _ => loop (idx - 1, acc)
+          )
+  in
+    loop (start - 1, 1)
+  end
+
+  fun loop {pn:nat| pn <= pl + 1} (pc: int(pn), ptr: int): void =
+    if pc >= proglen
+    then ()
+    else
+      let
+        val cur = state[ptr]
+      in
+        case+ 0 of
+        | _ when prog[pc] = '+' => 
+          (state[ptr] := (if cur = UCHARMAX then 0 else cur + 1); loop (pc + 1, ptr))
+        | _ when prog[pc] = '-' =>
+          (state[ptr] := (if cur = 0 then UCHARMAX else (cur - 1)); loop (pc + 1, ptr))
+        | _ when prog[pc] = '<' =>
+          if ptr = 0
+          then $raise Underflow()
+          else loop (pc + 1, ptr - 1)
+        | _ when prog[pc] = '>' =>
+          if ptr + 1 = TAPESIZE
+          then $raise Overflow()
+          else loop (pc + 1, ptr + 1)
+        | _ when prog[pc] = '.' => (prints(char(cur)); loop (pc + 1, ptr))
+        (* TODO: implement getchar() in JS *)
+        | _ when prog[pc] = ',' => (state[ptr] := 255; loop (pc + 1, ptr))
+        | _ when prog[pc] = '[' => 
+          if cur = 0
+          then loop (find_match_rb pc, ptr)
+          else loop (pc + 1, ptr)
+        | _ when prog[pc] = ']' =>
+          if cur != 0
+          then loop (find_match_lb pc, ptr)
+          else loop (pc + 1, ptr)
+        | _ => loop (pc + 1, ptr)
+      end
+
+in
+  loop(0, 0)
+end
+
+val input_path: strn = argv_get()[2]
+
+val () = prints("Interpreting: ", input_path, "\n")
+
+val input_program: strn = read_file(input_path)
+
+val () = interp(input_program)

contrib/gavinz/brainfxxk/Makefile

@@ -0,0 +1,49 @@
+CAT=cat
+ECHO=echo
+BUN=bun
+NODE=node
+
+XATS2JS=$(XATSHOME)/srcgen2/xats2js/srcgenx/UTIL/xats2js_jsemit00_dats.js
+SRCGEN2_XSHARED=$(XATSHOME)/srcgen2/xats2js/srcgenx/xshared/runtime
+GAVINZ_XATSLIB=$(XATSHOME)/contrib/gavinz/xatslib/BUILD/xatslib.js
+
+# Directories
+DATS_DIR := DATS
+BUILD_DIR := BUILD
+BUILD_JS_DIR := $(BUILD_DIR)/JS
+
+# Find all .dats files and generate corresponding .js filenames
+DATS_FILES := $(wildcard $(DATS_DIR)/*.dats)
+JS_FILES := $(patsubst $(DATS_DIR)/%.dats,$(BUILD_JS_DIR)/%_dats.js,$(DATS_FILES))
+MAIN := $(BUILD_DIR)/main.js
+
+# Main target to build all files
+all: builddirs $(JS_FILES)
+
+# Make sure build directory exists
+builddirs:
+	mkdir -pv $(BUILD_DIR)
+	mkdir -pv $(BUILD_JS_DIR)
+
+# Rule to compile .dats to .js
+$(BUILD_JS_DIR)/%_dats.js: $(DATS_DIR)/%.dats
+	$(BUN) run $(XATS2JS) $< > $@
+
+# Group all JS files into one runnable file
+main: $(JS_FILES)
+	$(ECHO) "// " `date` > $(MAIN)
+	$(CAT) $(SRCGEN2_XSHARED)/xats2js_js1emit.js >> $(MAIN)
+	$(CAT) $(SRCGEN2_XSHARED)/xats2js_prelude.js >> $(MAIN)
+	$(CAT) $(SRCGEN2_XSHARED)/xats2js_xatslib.js >> $(MAIN)
+	$(CAT) $(SRCGEN2_XSHARED)/xats2js_prelude_node.js >> $(MAIN)
+	$(CAT) $(GAVINZ_XATSLIB) >> $(MAIN)
+	$(CAT) $^ >> $(MAIN)
+
+run: $(MAIN)
+	$(BUN) run $(MAIN)
+
+# Clean target
+clean:
+	rm -rf $(BUILD_DIR)
+
+.PHONY: all clean run

contrib/gavinz/brainfxxk/README.md

@@ -0,0 +1,22 @@
+An interpreter for brainfxxk written in ATS3.
+
+## Instructions to Run
+
+The following assumes you're in the root directory of the
+git repository, NOT in
+`contrib/gavinz/brainfxxk`.
+
+1. `make -f Makefile_overall` to compile ATS3
+   compilers and prelude.
+
+2. `make -C contrib/gavinz/xatslib` to compile my `xatslib` which provides
+   additional functions
+   that are
+   not yet merged into `prelude`.
+
+3. `make -C contrib/gavinz/brainfxxk` to compile the brainfxxk interpreter.
+
+4. `bun run contrib/gavinz/brainfxxk/BUILD/main.js <input-file>` to interpret a
+   brainfxxk program. For example,
+   `bun run contrib/gavinz/brainfxxk/BUILD/main.js
+   contrib/gavinz/brainfxxk/hello.bf`

contrib/gavinz/brainfxxk/hello.bf

@@ -0,0 +1 @@
+++++++++[>++++[>++>+++>+++>+<<<<-]>+>+>->>+[<]<-]>>.>---.+++++++..+++.>>.<-.<.+++.------.--------.>>+.>++.

contrib/gavinz/xatslib/.gitignore

@@ -0,0 +1,4 @@
+BUILD/*.js
+BUILD/JS/*.js
+lib/*.js
+UTIL/*.js

contrib/gavinz/xatslib/CATS/JS/char000.cats

@@ -0,0 +1,5 @@
+function XATS2JS_char_make_int(code)
+{
+  // We store chars as an int
+  return code
+}

contrib/gavinz/xatslib/CATS/JS/file000.cats

@@ -0,0 +1,5 @@
+function XATS2JS_NODE_readFileSync(path)
+{
+  const fs = require("fs")
+  return fs.readFileSync(path, "utf8")
+}

contrib/gavinz/xatslib/CATS/JS/proc000.cats

@@ -0,0 +1,4 @@
+function XATS2JS_NODE_argv_get()
+{
+  return process.argv;
+}

contrib/gavinz/xatslib/DATS/JS/char000.dats

@@ -0,0 +1,13 @@
+#impltmp <(*tmp*)> char_make_sint (code: sint): char =
+	XATS2JS_char_make_int(code)
+    where
+    {
+      #extern fun XATS2JS_char_make_int(code: sint): char = $extnam()
+    }
+
+#impltmp <(*tmp*)> char_make_uint (code: uint): char =
+  (XATS2JS_char_make_int(code))
+    where
+    {
+      #extern fun XATS2JS_char_make_int(code: uint): char = $extnam()
+    }

contrib/gavinz/xatslib/DATS/JS/file000.dats

@@ -0,0 +1,6 @@
+fun read_file(path: strn): strn =
+  XATS2JS_NODE_readFileSync(path)
+    where
+    {
+      #extern fun XATS2JS_NODE_readFileSync(strn): strn = $extnam()
+    }

contrib/gavinz/xatslib/DATS/JS/proc000.dats

@@ -0,0 +1,6 @@
+fun argv_get(): a1rf(strn) =
+  XATS2JS_NODE_argv_get()
+	  where
+    {
+      #extern fun XATS2JS_NODE_argv_get(): a1rf(strn) = $extnam()
+    }

contrib/gavinz/xatslib/Makefile

@@ -0,0 +1,49 @@
+CAT=cat
+ECHO=echo
+BUN=bun
+NODE=node
+
+XATS2JS=$(XATSHOME)/srcgen2/xats2js/srcgenx/UTIL/xats2js_jsemit00_dats.js
+SRCGEN2_XSHARED=$(XATSHOME)/srcgen2/xats2js/srcgenx/xshared/runtime
+
+# Directories
+DATS_DIR := DATS
+DATS_JS_DIR := $(DATS_DIR)/JS
+CATS_DIR := CATS
+BUILD_DIR := BUILD
+BUILD_JS_DIR := $(BUILD_DIR)/JS
+
+# Find all .dats files and generate corresponding .js filenames
+DATS_FILES    := $(wildcard $(DATS_DIR)/*.dats)
+DATS_JS_FILES := $(wildcard $(DATS_DIR)/JS/*.dats)
+CATS_JS_FILES := $(wildcard $(CATS_DIR)/JS/*.cats)
+
+JS_OUTPUTS := $(patsubst $(DATS_DIR)/%.dats,$(BUILD_JS_DIR)/%_dats.js,$(DATS_FILES)) \
+						  $(patsubst $(DATS_JS_DIR)/%.dats,$(BUILD_JS_DIR)/JS/%_dats.js,$(DATS_JS_FILES))
+
+# Main target to build all files
+all: builddir xatslib
+
+# Make sure build directory exists
+builddir:
+	mkdir -pv $(BUILD_DIR)
+	mkdir -pv $(BUILD_JS_DIR)
+	mkdir -pv $(BUILD_JS_DIR)/JS
+
+# Rule to compile .dats to .js
+$(BUILD_JS_DIR)/%_dats.js: $(DATS_DIR)/%.dats
+	$(BUN) run $(XATS2JS) $< > $@
+
+$(BUILD_JS_DIR)/JS/%_dats.js: $(DATS_DIR)/JS/%.dats
+	$(BUN) run $(XATS2JS) $< > $@
+
+# Group all JS files into one runnable file
+xatslib: $(CATS_JS_FILES) $(JS_OUTPUTS)
+	$(ECHO) "// gavinz/xatslib generated on " `date` > $(BUILD_DIR)/xatslib.js
+	$(CAT) $^ >> $(BUILD_DIR)/xatslib.js
+
+# Clean target
+clean:
+	rm -rf $(BUILD_DIR)
+
+.PHONY: all clean

contrib/gavinz/xatslib/SATS/file000.sats

@@ -0,0 +1 @@
+fun read_file(strn): strn

contrib/gavinz/xatslib/SATS/proc000.sats

@@ -0,0 +1 @@
+fun argv_get(): a1rf(strn)

flake.nix

@@ -0,0 +1 @@
+contrib/gavinz/flake.nix