push

brainfuck.ipkg

@@ -0,0 +1,11 @@
+package brainfuck
+
+authors = "you"
+version = 0.1.0
+
+sourcedir = "src"
+main = Main
+executable = "brainfuck"
+
+depends = contrib
+

flake.nix

@@ -0,0 +1,51 @@
+{
+  description = "idris2 brainfuck interpreter";
+  inputs = {
+    nixpkgs.url     = "github:NixOS/nixpkgs/nixos-unstable";
+    flake-utils.url = "github:numtide/flake-utils";
+  };
+  outputs = { self, nixpkgs, flake-utils }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        pkgs = import nixpkgs { inherit system; };
+        brainfuck = pkgs.stdenv.mkDerivation {
+          pname   = "brainfuck";
+          version = "0.1.0";
+          src = ./.;
+          nativeBuildInputs = [ pkgs.idris2 ];
+          buildPhase = ''
+            idris2 --build brainfuck.ipkg
+          '';
+          installPhase = ''
+            mkdir -p $out/bin
+            cp -r build/exec/brainfuck_app $out/bin/brainfuck_app
+            cp build/exec/brainfuck $out/bin/brainfuck
+          '';
+          meta = with pkgs.lib; {
+            description = "A Brainfuck interpreter in Idris2";
+            license     = licenses.mit;
+            platforms   = platforms.unix;
+          };
+        };
+      in {
+        packages.default   = brainfuck;
+        packages.brainfuck = brainfuck;
+        apps.default = {
+          type    = "app";
+          program = "${brainfuck}/bin/brainfuck";
+        };
+        devShells.default = pkgs.mkShell {
+          packages = [
+            pkgs.idris2
+            pkgs.rlwrap
+            pkgs.nodePackages.nodemon
+          ];
+          shellHook = ''
+            echo "Idris2 brainfuck dev shell"
+            echo "  Build : idris2 --build brainfuck.ipkg"
+            echo "  Run   : ./build/exec/brainfuck <file.bf>"
+          '';
+        };
+      }
+    );
+}

hello.bf

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

src/Main.idr

@@ -0,0 +1,118 @@
+module Main
+
+import Data.List
+import Data.SortedMap
+import System
+import System.File
+
+record BFState where
+  constructor MkBFState
+  leftCells   : List Int
+  currentCell : Int
+  rightCells  : List Int
+
+BraceMap : Type
+BraceMap = SortedMap Int Int
+
+inits : BFState
+inits = MkBFState [] 0 (replicate 29999 0)
+
+mr : BFState -> BFState
+mr (MkBFState left cur right) =
+  case right of
+    []      => MkBFState (cur :: left) 0 []
+    (r::rs) => MkBFState (cur :: left) r rs
+
+moveLeft : BFState -> BFState
+moveLeft (MkBFState left cur right) =
+  case left of
+    []      => MkBFState [] 0 (cur :: right)
+    (l::ls) => MkBFState ls l (cur :: right)
+
+increment : BFState -> BFState
+increment st = { currentCell $= (+1) } st
+
+decrement : BFState -> BFState
+decrement st = { currentCell $= (\x => x - 1) } st
+
+buildBraceMap : List (Int, Char) -> List Int -> BraceMap -> BraceMap
+buildBraceMap [] _ bmap = bmap
+buildBraceMap ((i, c) :: rest) stack bmap =
+  case c of
+    '[' => buildBraceMap rest (i :: stack) bmap
+    ']' => case stack of
+             []        => buildBraceMap rest [] bmap
+             (s :: ss) =>
+               let bmap' = insert s i (insert i s bmap)
+               in buildBraceMap rest ss bmap'
+    _   => buildBraceMap rest stack bmap
+
+mbm : List Char -> BraceMap
+mbm code =
+  buildBraceMap (zip [0..(cast (length code) - 1)] code) [] empty
+
+cleanup : String -> List Char
+cleanup s = filter (\c => c `elem` (unpack ".,[]<>+-")) (unpack s)
+
+safeIndex : Int -> List a -> Maybe a
+safeIndex _ [] = Nothing
+safeIndex 0 (x :: xs) = Just x
+safeIndex n (x :: xs) =
+  if n < 0 then Nothing else safeIndex (n - 1) xs
+
+
+runStep : List Char -> BraceMap -> Int -> BFState -> IO (BFState, Int)
+runStep code bmap cp st =
+  case safeIndex cp code of
+    Nothing => pure (st, cp)
+    Just op =>
+      case op of
+        '>' => pure (mr st, cp + 1)
+        '<' => pure (moveLeft  st, cp + 1)
+        '+' => pure (increment st, cp + 1)
+        '-' => pure (decrement st, cp + 1)
+
+        '.' => do
+                 putChar (cast (currentCell st))
+                 pure (st, cp + 1)
+
+        ',' => do
+                 c <- getChar
+                 pure ({ currentCell := cast c } st, cp + 1)
+
+        '[' => if currentCell st == 0
+                 then case lookup cp bmap of
+                        Just target => pure (st, target + 1)
+                        Nothing     => pure (st, cp + 1)
+                 else pure (st, cp + 1)
+
+        ']' => if currentCell st /= 0
+                 then case lookup cp bmap of
+                        Just target => pure (st, target + 1)
+                        Nothing     => pure (st, cp + 1)
+                 else pure (st, cp + 1)
+
+        _   => pure (st, cp + 1)
+
+interpret : List Char -> BraceMap -> Int -> BFState -> IO ()
+interpret code bmap cp st =
+  if cp >= cast (length code)
+    then pure ()
+    else do
+      (st', cp') <- runStep code bmap cp st
+      interpret code bmap cp' st'
+
+
+main : IO ()
+main = do
+  args <- getArgs
+  case args of
+    (_ :: filename :: _) => do
+      result <- readFile filename
+      case result of
+        Left err   => putStrLn ("Error reading file: " ++ show err)
+        Right src  => do
+          let code  = cleanup src
+              bmap  = mbm code
+          interpret code bmap 0 inits
+    _ => putStrLn "Usage: brainfuck <filename.bf>"