diff --git a/Makefile b/Makefile
index c42c5ca62f..caa71e4e8f 100644
--- a/Makefile
+++ b/Makefile
@@ -91,7 +91,7 @@ DOCKERIZE =
 
 IMPLS = ada ada.2 awk bash basic bbc-basic c chuck clojure coffee common-lisp cpp crystal cs d dart \
 	elisp elixir elm erlang es6 factor fantom forth fsharp go groovy gnu-smalltalk \
-	guile haskell haxe hy io java js jq julia kotlin livescript logo lua make mal \
+	guile haskell haxe hy idris2 io java js jq julia kotlin livescript logo lua make mal \
 	matlab miniMAL nasm nim objc objpascal ocaml perl perl6 php picolisp pike plpgsql \
 	plsql powershell ps python python.2 r racket rexx rpython ruby rust scala scheme skew \
 	swift swift3 swift4 swift5 tcl ts vala vb vhdl vimscript wasm wren yorick xslt zig
@@ -217,6 +217,7 @@ guile_STEP_TO_PROG =         impls/guile/$($(1)).scm
 haskell_STEP_TO_PROG =       impls/haskell/$($(1))
 haxe_STEP_TO_PROG =          $(haxe_STEP_TO_PROG_$(haxe_MODE))
 hy_STEP_TO_PROG =            impls/hy/$($(1)).hy
+idris2_STEP_TO_PROG =        impls/idris2/build/exec/$($(1))
 io_STEP_TO_PROG =            impls/io/$($(1)).io
 java_STEP_TO_PROG =          impls/java/target/classes/mal/$($(1)).class
 js_STEP_TO_PROG =            impls/js/$($(1)).js
diff --git a/impls/idris2/.gitignore b/impls/idris2/.gitignore
new file mode 100644
index 0000000000..378eac25d3
--- /dev/null
+++ b/impls/idris2/.gitignore
@@ -0,0 +1 @@
+build
diff --git a/impls/idris2/Class.idr b/impls/idris2/Class.idr
new file mode 100644
index 0000000000..8c5a6015b3
--- /dev/null
+++ b/impls/idris2/Class.idr
@@ -0,0 +1,88 @@
+||| Typeclasses that describe types that correspond to Mal data
+module Class
+
+import Eval
+import Types
+
+export
+interface MalType a where
+  toMalAst : a -> AST
+  fromMalAst : AST -> Maybe a
+
+export
+implementation MalType AST where
+  toMalAst = id
+  fromMalAst = Just
+
+export
+implementation MalType () where
+  toMalAst () = Symbol "nil"
+  fromMalAst (Symbol "nil") = Just ()
+  fromMalAst _ = Nothing
+
+export
+implementation MalType Integer where
+  toMalAst = Number
+  fromMalAst (Number x) = Just x
+  fromMalAst _ = Nothing
+
+export
+implementation MalType String where
+  toMalAst = Str
+  fromMalAst (Str s) = Just s
+  fromMalAst _ = Nothing
+
+export
+implementation MalType Bool where
+  toMalAst True = Symbol "true"
+  toMalAst False = Symbol "false"
+  fromMalAst (Symbol "true") = Just True
+  fromMalAst (Symbol "false") = Just False
+  -- fromMalAst (Symbol "nil") = Just False -- Maybe?
+  fromMalAst _ = Nothing
+
+export
+implementation MalType (IORef AST) where
+  toMalAst = Atom
+  fromMalAst (Atom a) = Just a
+  fromMalAst _ = Nothing
+
+export
+implementation MalType a => MalType (List a) where
+  toMalAst = List False . map toMalAst
+  fromMalAst (List _ xs) = traverse fromMalAst xs
+  fromMalAst (Symbol "nil") = Just []
+  fromMalAst _ = Nothing
+
+export
+implementation MalType (SortedMap String AST) where
+  toMalAst = Map
+  fromMalAst (Map m) = Just m
+  fromMalAst (Symbol "nil") = Just empty
+  fromMalAst _ = Nothing
+
+export
+interface MalFunction a where
+  toMalFunc : a -> List AST -> MalM AST
+
+export
+implementation MalType a => MalFunction a where
+  toMalFunc x [] = pure $ toMalAst x
+  toMalFunc _ xs = do
+    traverse eval xs -- (+ 1 2 (println "hi")) should print hi
+    throwError $ Str "Too many arguments"
+
+export
+implementation MalType a => MalFunction (MalM a) where
+  toMalFunc x [] = map toMalAst x
+  toMalFunc _ xs = do
+    traverse eval xs
+    throwError $ Str "Too many arguments"
+
+export
+implementation (MalType a, MalFunction b) => MalFunction (a -> b) where
+  toMalFunc _ [] = throwError $ Str "Too few arguments"
+  toMalFunc f (x::xs) = do
+    Just x' <- map fromMalAst $ eval x
+      | Nothing => traverse_ eval xs *> throwError (Str "Wrong argument type")
+    toMalFunc (f x') xs
diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
new file mode 100644
index 0000000000..40b052bd65
--- /dev/null
+++ b/impls/idris2/Core.idr
@@ -0,0 +1,441 @@
+module Core
+
+import Control.Monad.Syntax
+import Data.List
+import Data.Maybe
+import Data.Strings
+import System
+import System.Clock
+import System.File
+
+import Class
+import Eval
+import Reader
+import Types
+
+liftIO' : MalType a => IO a -> MalM AST
+liftIO' = map toMalAst . MonadTrans.liftIO
+
+defBuiltin : List AST -> MalM AST
+defBuiltin [] = throwError $ Str "def!: too few arguments"
+defBuiltin [_] = throwError $ Str "def!: too few arguments"
+defBuiltin [Symbol n, x] = do
+  x' <- eval x
+  insert n x'
+  pure x'
+defBuiltin [_, _] = throwError $ Str "def!: expecting symbol"
+defBuiltin _ = throwError $ Str "def!: too many arguments"
+
+defmacroBuiltin : List AST -> MalM AST
+defmacroBuiltin [] = throwError $ Str "defmacro!: too few arguments"
+defmacroBuiltin [_] = throwError $ Str "defmacro!: too few arguments"
+defmacroBuiltin [Symbol n, x] = do
+  Func _ m <- eval x
+    | _ => throwError $ Str "defmacro!: expected a function"
+  let m' = Func True $ eval <=< local (record { evalFunc = don'tEval }) . m
+  insert n m'
+  pure m'
+defmacroBuiltin [_, _] = throwError $ Str "defmacro!: expecting symbol"
+defmacroBuiltin _ = throwError $ Str "defmacro!: too many arguments"
+
+letBuiltin : List AST -> MalM AST
+letBuiltin [] = throwError $ Str "let*: too few arguments"
+letBuiltin [_] = throwError $ Str "let*: too few arguments"
+letBuiltin [List _ defs, ans] = withLocalEnv $ go defs
+  where
+    go : List AST -> MalM AST
+    go [] = eval ans
+    go (Symbol n::x::rest) = do
+      x' <- eval x
+      insert n x'
+      go rest
+    go _ = throwError $ Str "let*: malformed arguments"
+letBuiltin [_, _] = throwError $ Str "let*: malformed arguments"
+letBuiltin _ = throwError $ Str "let*: too many arguments"
+
+doBuiltin : List AST -> MalM AST
+doBuiltin xs = do
+  Just x <- map last' $ traverse eval xs
+    | Nothing => throwError $ Str "do: too few arguments"
+  pure x
+
+ifBuiltin : List AST -> MalM AST
+ifBuiltin [] = throwError $ Str "if: too few arguments"
+ifBuiltin [_] = throwError $ Str "if: too few arguments"
+ifBuiltin [cond, tt] = do
+  cond' <- eval cond
+  if truthiness cond' then eval tt else pure $ Symbol "nil"
+ifBuiltin [cond, tt, ff] = do
+  cond' <- eval cond
+  if truthiness cond' then eval tt else eval ff
+ifBuiltin _ = throwError $ Str "if: too few arguments"
+
+fnBuiltin : List AST -> MalM AST
+fnBuiltin [List _ argNames, res] = do
+  argNames' <- traverse getSymbol argNames
+  parentEnv <- ask
+  pure $ Func False $ \args => do
+    args' <- traverse eval args
+    local (const parentEnv) $ withLocalEnv $ do
+      bindArgs argNames' args'
+      -- If it's a regular function, then it only runs during fullEval mode.
+      -- If it's a macro, we need to evaluate it even it macroexpand mode.
+      -- So fullEval is the right thing to do here.
+      fullEval res
+  where getSymbol : AST -> MalM String
+        getSymbol (Symbol n) = pure n
+        getSymbol _ = throwError $ Str "fn: malformed arguments"
+        bindArgs : List String -> List AST -> MalM ()
+        bindArgs [] [] = pure ()
+        bindArgs [] _ = throwError $ Str "too many arguments"
+        bindArgs ["&",n] xs = insert n $ List False xs
+        bindArgs _ [] = throwError $ Str "too few arguments"
+        bindArgs (n::ns) (x::xs) = do
+          insert n x
+          bindArgs ns xs
+fnBuiltin _ = throwError $ Str "fn: malformed arguments"
+
+readStringBuiltin : String -> MalM AST
+readStringBuiltin s =
+  case parseText s of
+       Right [] => pure $ Symbol "nil"
+       Right [ast] => pure ast
+       Right xs => pure $ List True xs
+       Left e => throwError $ Str $ "parse error: " ++ e
+
+slurpBuiltin : String -> MalM String
+slurpBuiltin file = do
+  res <- liftIO $ readFile file
+  case res of
+       Right contents => pure contents
+       Left _ => throwError $ Str $ "slurp: could not read file " ++ file
+
+atomBuiltin : AST -> MalM AST
+atomBuiltin = liftIO' . newIORef
+
+resetBuiltin : IORef AST -> AST -> MalM AST
+resetBuiltin r x = do
+  liftIO $ writeIORef r x
+  pure x
+
+derefBuiltin : IORef AST -> MalM AST
+derefBuiltin = MonadTrans.liftIO . readIORef
+
+swapBuiltin : List AST -> MalM AST
+swapBuiltin [] = throwError $ Str "swap!: too few arguments"
+swapBuiltin [_] = throwError $ Str "swap!: too few arguments"
+swapBuiltin (a::f::args) = do
+  (Atom x, Func _ f') <- [| MkPair (eval a) (eval f) |]
+    | _ => throwError $ Str "swap!: type error"
+  new <- f' (List False [Symbol "deref", Atom x]::args)
+  resetBuiltin x new
+
+consBuiltin : AST -> List AST -> List AST
+consBuiltin = (::)
+
+firstBuiltin : List AST -> AST
+firstBuiltin [] = Symbol "nil"
+firstBuiltin (x::_) = x
+
+restBuiltin : List AST -> List AST
+restBuiltin [] = []
+restBuiltin (_::xs) = xs
+
+concatBuiltin : List AST -> MalM AST
+concatBuiltin = map (List False) . go <=< traverse eval
+  where go : List AST -> MalM (List AST)
+        go (List _ l::ls) = map (l ++) $ go ls
+        go (_::_) = throwError $ Str "concat: expected list"
+        go [] = pure []
+
+quoteBuiltin : List AST -> MalM AST
+quoteBuiltin [x] = pure x
+quoteBuiltin _ = throwError $ Str "quote: wanted exactly one argument"
+
+quasiquoteBuiltin : List AST -> MalM AST
+quasiquoteBuiltin [x] = qq x
+  where expandSplice : AST -> MalM (List AST)
+        expandSplice (List False [Symbol "splice-unquote", x]) = do
+          x' <- eval x
+          case x' of
+               List _ xs => pure xs
+               _ => pure [x']
+        expandSplice x = pure [x]
+        qq : AST -> MalM AST
+        qq (Symbol x) = pure $ Symbol x
+        qq (Str s) = pure $ Str s
+        qq (Number x) = pure $ Number x
+        qq (Atom a) = pure $ Atom a
+        qq (List False [Symbol "unquote", a]) = eval a
+        qq (List _ xs) = do
+          xs' <- traverse qq xs
+          map (List False . concat) $ traverse expandSplice xs'
+        qq (Map m) = map Map $ traverse qq m
+        qq (Func m f) = pure $ Func m f
+quasiquoteBuiltin _ = throwError $ Str "quote: wanted exactly one argument"
+
+macroexpandBuiltin : List AST -> MalM AST
+macroexpandBuiltin [x] = local (record { evalFunc = macroexpand }) $ eval x
+macroexpandBuiltin _ = throwError $ Str "macroexpand: wanted exactly one argument"
+
+tryBuiltin : List AST -> MalM AST
+tryBuiltin [x] = eval x
+tryBuiltin [x, List False [Symbol "catch*", Symbol e, handler]] =
+  catchError (eval x) $ \err => withLocalEnv $ do
+    insert e err
+    eval handler
+tryBuiltin _ = throwError $ Str "try*: malformed arguments"
+
+typeofBuiltin : AST -> AST
+typeofBuiltin (Symbol _) = Keyword "symbol"
+typeofBuiltin (Str s) = Keyword $ if map fst (strUncons s) == Just '\xff' then "keyword" else "string"
+typeofBuiltin (Number _) = Keyword "number"
+typeofBuiltin (Atom _) = Keyword "atom"
+typeofBuiltin (List False _) = Keyword "list"
+typeofBuiltin (List True _) = Keyword "vector"
+typeofBuiltin (Map _) = Keyword "map"
+typeofBuiltin (Func False _) = Keyword "fn"
+typeofBuiltin (Func True _) = Keyword "macro"
+
+assocBuiltin : List AST -> MalM AST
+assocBuiltin = traverse eval >=> assoc
+  where go : SortedMap String AST -> List AST -> MalM (SortedMap String AST)
+        go m [] = pure m
+        go m [_] = throwError $ Str "odd number of arguments"
+        go m (Str k::v::rest) = go (insert k v m) rest
+        go m _ = throwError $ Str "expected a string or keyword"
+        assoc : List AST -> MalM AST
+        assoc [] = throwError $ Str "too few arguments"
+        assoc (Map m::rest) = map Map $ go m rest
+        assoc _ = throwError $ Str "expected a map"
+
+dissocBuiltin : List AST -> MalM AST
+dissocBuiltin = traverse eval >=> dissoc
+  where go : SortedMap String AST -> List AST -> MalM (SortedMap String AST)
+        go m [] = pure m
+        go m (Str k::rest) = go (delete k m) rest
+        go m _ = throwError $ Str "expecting a string or keyword"
+        dissoc : List AST -> MalM AST
+        dissoc [] = throwError $ Str "too few arguments"
+        dissoc (Map m::rest) = map Map $ go m rest
+        dissoc _ = throwError $ Str "expected a map"
+
+getBuiltin : SortedMap String AST -> String -> AST
+getBuiltin m k = fromMaybe (Symbol "nil") $ lookup k m
+
+containsBuiltin : SortedMap String AST -> String -> Bool
+containsBuiltin m k = isJust $ lookup k m
+
+timeBuiltin : MalM Integer
+timeBuiltin = do
+  MkClock s ns <- liftIO $ clockTime UTC
+  let ms = 1000 * s + ns `div` 1000000
+  pure ms
+
+conjBuiltin : List AST -> MalM AST
+conjBuiltin = conj <=< traverse eval
+  where conj : List AST -> MalM AST
+        conj (List False xs::rest) = pure $ List False $ foldl (flip (::)) xs rest
+        conj (List True xs::rest) = pure $ List True $ xs ++ rest
+        conj (_::_) = throwError $ Str "conj: expecting a list or a vector"
+        conj [] = throwError $ Str "conj: too few arguments"
+
+seqBuiltin : AST -> MalM AST
+seqBuiltin (Symbol "nil") = pure $ Symbol "nil"
+seqBuiltin (List _ []) = pure $ Symbol "nil"
+seqBuiltin (Str "") = pure $ Symbol "nil"
+seqBuiltin (List _ xs) = pure $ List False xs
+seqBuiltin (Str s) = case strUncons s of
+                          Just ('\xff', _) => throwError $ Str "seq: expecting a list, vector, or string"
+                          _ => pure $ List False $ map (Str . pack . pure) $ unpack s
+seqBuiltin _ = throwError $ Str "seq: expecting a list, vector, or string"
+
+readlineBuiltin : String -> MalM AST
+readlineBuiltin s =
+  case strUncons s of
+       Just ('\xff', _) => throwError $ Str "readline: expecing a string"
+       _ => liftIO $ do
+         False <- fEOF stdin
+           | True => putStr "\n" *> pure (Symbol "nil")
+         putStr s
+         map Str getLine
+
+prStr : List AST -> MalM AST
+prStr xs = do
+  xs' <- traverse eval xs
+  sxs <- liftIO $ traverse (toString True) xs'
+  pure $ Str $ fastAppend $ intersperse " " sxs
+str : List AST -> MalM AST
+str xs = do
+  xs' <- traverse eval xs
+  sxs <- liftIO $ traverse (toString False) xs'
+  pure $ Str $ fastAppend sxs
+prn : List AST -> MalM AST
+prn xs = do
+  xs' <- traverse eval xs
+  sxs <- liftIO $ traverse (toString True) xs'
+  liftIO' $ putStrLn $ fastAppend $ intersperse " " sxs
+println : List AST -> MalM AST
+println xs = do
+  xs' <- traverse eval xs
+  sxs <- liftIO $ traverse (toString False) xs'
+  liftIO' $ putStrLn $ fastAppend $ intersperse " " sxs
+
+baseEnv : SortedMap String AST
+baseEnv = fromList [
+  ("nil", Symbol "nil"),
+  ("true", Symbol "true"),
+  ("false", Symbol "false"),
+  ("*host-language*", Str "idris2"),
+  ("+", Func False $ toMalFunc $ (+) {ty=Integer}),
+  ("-", Func False $ toMalFunc $ (-) {ty=Integer}),
+  ("*", Func False $ toMalFunc $ (*) {ty=Integer}),
+  ("/", Func False $ toMalFunc $ div {ty=Integer}),
+  ("def!", Func False $ defBuiltin),
+  ("defmacro!", Func False $ defmacroBuiltin),
+  ("let*", Func False letBuiltin),
+  ("if", Func False ifBuiltin),
+  ("fn*", Func False fnBuiltin),
+  ("do", Func False doBuiltin),
+  ("list", Func False $ map (List False) . traverse eval),
+  ("vector", Func False $ map (List True) . traverse eval),
+  ("count", Func False $ toMalFunc $ the (List AST -> Integer) $ cast . List.length),
+  ("=", Func False $ toMalFunc $ (==) {ty=AST}),
+  (">", Func False $ toMalFunc $ (>) {ty=Integer}),
+  (">=", Func False $ toMalFunc $ (>=) {ty=Integer}),
+  ("<", Func False $ toMalFunc $ (<) {ty=Integer}),
+  ("<=", Func False $ toMalFunc $ (<=) {ty=Integer}),
+  -- TODO: implement in corelib
+  ("pr-str", Func False prStr),
+  ("str", Func False str),
+  ("prn", Func False prn),
+  ("println", Func False println),
+  ("read-string", Func False $ toMalFunc readStringBuiltin),
+  ("slurp", Func False $ toMalFunc slurpBuiltin),
+  ("eval", Func False $ toMalFunc $ withGlobalEnv . eval),
+  ("atom", Func False $ toMalFunc atomBuiltin),
+  ("deref", Func False $ toMalFunc derefBuiltin),
+  ("reset!", Func False $ toMalFunc resetBuiltin),
+  ("swap!", Func False swapBuiltin),
+  ("cons", Func False $ toMalFunc consBuiltin),
+  ("concat", Func False concatBuiltin),
+  ("first", Func False $ toMalFunc firstBuiltin),
+  ("rest", Func False $ toMalFunc restBuiltin),
+  ("quote", Func False quoteBuiltin),
+  ("quasiquote", Func False quasiquoteBuiltin),
+  ("macroexpand", Func False macroexpandBuiltin),
+  ("try*", Func False tryBuiltin),
+  ("throw", Func False $ toMalFunc $ the (AST -> MalM AST) throwError),
+  ("idris-typeof", Func False $ toMalFunc typeofBuiltin),
+  ("idris-str-to-keyword", Func False $ toMalFunc Keyword),
+  ("symbol", Func False $ toMalFunc Symbol),
+  ("assoc", Func False assocBuiltin),
+  ("dissoc", Func False dissocBuiltin),
+  ("keys", Func False $ toMalFunc $ the (SortedMap String AST -> List String) keys),
+  ("vals", Func False $ toMalFunc $ the (SortedMap String AST -> List AST) values),
+  ("get", Func False $ toMalFunc getBuiltin),
+  ("contains?", Func False $ toMalFunc containsBuiltin),
+  ("readline", Func False $ toMalFunc readlineBuiltin),
+  ("time-ms", Func False $ toMalFunc timeBuiltin),
+  ("conj", Func False conjBuiltin),
+  ("seq", Func False $ toMalFunc seqBuiltin),
+  ("meta", Func False $ const $ throwError $ Str "unimplemented"),
+  ("with-meta", Func False $ const $ throwError $ Str "unimplemented")
+]
+
+coreLib : String
+coreLib = "
+(def! empty? (fn* (l) (= (count l) 0)))
+(def! not (fn* (a) (if a false true)))
+(def! load-file (fn* (f) (eval (read-string (str \"(do \" (slurp f) \"\\nnil)\")))))
+(defmacro! cond
+  (fn* (& xs) (if (> (count xs) 0)
+        (list 'if (first xs)
+              (if (> (count xs) 1)
+                  (first (rest xs))
+                  (throw \"odd number of forms to cond\"))
+              (cons 'cond (rest (rest xs)))
+        )
+  ))
+)
+(def! nth (fn* (xs n)
+  (cond
+    (not (sequential? xs)) (throw \"expecting a list or vector\")
+    (if (< n 0) true (empty? xs)) (throw \"nth: index out of bounds\")
+    (= n 0) (first xs)
+    true (nth (rest xs) (- n 1))
+  )
+))
+(def! apply
+  (let*
+    ( init (fn* (l) (if (<= (count l) 1) () (cons (first l) (init (rest l)))))
+    , last (fn* (l) (if (<= (count l) 1) (first l) (last (rest l))))
+    )
+    (fn* (f & args)
+      (if (empty? args)
+          (throw \"apply: expected at least two arguments\")
+          (eval
+            (cons f
+              (map (fn* (x) (list 'quote x))
+                (concat (init args) (last args))))
+          )
+      )
+    )
+  )
+)
+(def! map
+  (fn* (f list)
+    (if (empty? list)
+        ()
+        (cons (f (first list)) (map f (rest list)))
+    )
+  )
+)
+(def! number? (fn* (x) (= (idris-typeof x) :number)))
+(def! string? (fn* (x) (= (idris-typeof x) :string)))
+(def! list? (fn* (x) (= (idris-typeof x) :list)))
+(def! vector? (fn* (x) (= (idris-typeof x) :vector)))
+(def! atom? (fn* (x) (= (idris-typeof x) :atom)))
+(def! map? (fn* (x) (= (idris-typeof x) :map)))
+(def! keyword? (fn* (x) (= (idris-typeof x) :keyword)))
+(def! nil? (fn* (x) (= x nil)))
+(def! true? (fn* (x) (= x true)))
+(def! false? (fn* (x) (= x false)))
+;; nil, true, and false are implemented as symbols, but (symbol? nil) == false
+(def! symbol? (fn* (x)
+  (if (= (idris-typeof x) :symbol)
+      (if (nil? x)
+          false
+          (if (true? x)
+              false
+              (if (false? x) false true)
+          )
+      )
+      false
+  )
+))
+(def! fn? (fn* (x) (= (idris-typeof x) :fn)))
+(def! macro? (fn* (x) (= (idris-typeof x) :macro)))
+(def! sequential? (fn* (x) (if (list? x) true (vector? x))))
+(def! keyword (fn* (x) (if (keyword? x) x (idris-str-to-keyword x))))
+(def! hash-map (fn* (& args) (eval `(assoc {} ~@args))))
+"
+
+public export
+getStartingEnv : IO Env
+getStartingEnv = do
+  args <- getArgs
+  let argv =
+    case args of
+         (_::_::rest) => List False $ map Str rest
+         _ => List False []
+  env <- map (\v => MkEnv fullEval [v]) $ newIORef $ insert "*ARGV*" argv baseEnv
+  res <- runExceptT $ flip runReaderT env $ do
+    defs <- either (throwError . Str) pure $ parseText coreLib
+    traverse_ eval defs
+  case res of
+       Right () => pure ()
+       Left e => do
+         se <- toString False e
+         putStrLn $ "CORELIB: error: " ++ se
+  pure env
diff --git a/impls/idris2/Dockerfile b/impls/idris2/Dockerfile
new file mode 100644
index 0000000000..b29dd36764
--- /dev/null
+++ b/impls/idris2/Dockerfile
@@ -0,0 +1,39 @@
+FROM ubuntu:focal
+MAINTAINER Joel Martin <github@martintribe.org>
+
+##########################################################
+# General requirements for testing or common across many
+# implementations
+##########################################################
+
+RUN apt-get -y update
+
+# Required for running tests
+RUN apt-get -y install make python
+
+# Some typical implementation and test requirements
+RUN apt-get -y install curl libreadline-dev libedit-dev
+
+RUN mkdir -p /mal
+WORKDIR /mal
+
+##########################################################
+# Specific implementation requirements
+##########################################################
+
+# Idris2 deps
+RUN apt-get -y install gcc chezscheme git
+
+# Install from source
+WORKDIR /idris2
+ENV PATH /idris2/bin:$PATH
+ENV LD_LIBRARY_PATH /idris2/lib:$LD_LIBRARY_PATH
+ENV SCHEME chezscheme
+RUN git clone https://github.com/idris-lang/Idris2.git \
+    && cd Idris2 \
+    && sed -i 's|^PREFIX.*|PREFIX = /idris2|' config.mk \
+    && make bootstrap \
+    && make install
+RUN chmod -R a+x /idris2/idris2-0.2.0
+
+WORKDIR /mal
diff --git a/impls/idris2/Eval.idr b/impls/idris2/Eval.idr
new file mode 100644
index 0000000000..039f111445
--- /dev/null
+++ b/impls/idris2/Eval.idr
@@ -0,0 +1,43 @@
+module Eval
+
+import Types
+import MonadTrans
+import Data.List
+
+-- Evaluate in the current eval mode.
+export
+eval : AST -> MalM AST
+eval x = do
+  e <- reader evalFunc
+  e x
+
+-- Run everything.
+export
+fullEval : AST -> MalM AST
+fullEval (Symbol n) = lookup n
+fullEval (Str s) = pure $ Str s
+fullEval (Number x) = pure $ Number x
+fullEval (Atom e) = pure $ Atom e
+fullEval (List False []) = pure $ List False []
+fullEval (List False (f::xs)) = do
+  Func _ f' <- fullEval f
+    | _ => throwError $ Str "tried to call something that's not a function"
+  f' xs
+fullEval (List True xs) = map (List True) $ traverse fullEval xs
+fullEval (Map m) = map Map $ traverse fullEval m
+fullEval (Func m f) = pure $ Func m f
+
+-- Run nothing.
+-- Macros are run in don'tEval mode so their arguments don't get evaluated.
+export
+don'tEval : AST -> MalM AST
+don'tEval = pure
+
+-- Only run macros.
+export
+macroexpand : AST -> MalM AST
+macroexpand (List False (Symbol n::xs)) = do
+  Func isMacro f <- lookup n
+    | _ => throwError $ Str "tried to call something that's not a function"
+  if isMacro then f xs else pure $ List False (Symbol n::xs)
+macroexpand x = pure x
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
new file mode 100644
index 0000000000..ee02a55485
--- /dev/null
+++ b/impls/idris2/Makefile
@@ -0,0 +1,17 @@
+SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr step3_env.idr \
+	   step4_if_fn_do.idr step5_tco.idr step6_file.idr step7_quote.idr \
+	   step8_macros.idr step9_try.idr stepA_mal.idr
+OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr Class.idr MonadTrans.idr
+BINS = $(SRCS:%.idr=build/exec/%)
+
+idris_args = -p contrib
+
+#####################
+
+all: $(BINS)
+
+$(BINS): build/exec/%: %.idr $(OTHER_SRCS)
+	idris2 $(idris_args) $< -o $(<:%.idr=%)
+
+clean:
+	rm -rf build
diff --git a/impls/idris2/MonadTrans.idr b/impls/idris2/MonadTrans.idr
new file mode 100644
index 0000000000..497d3b0507
--- /dev/null
+++ b/impls/idris2/MonadTrans.idr
@@ -0,0 +1,156 @@
+module MonadTrans
+
+import public Control.Monad.Trans
+import public Control.Monad.State
+
+-- Classes
+
+public export
+interface Monad m => MonadIO m where
+  liftIO : IO a -> m a
+
+public export
+implementation MonadIO IO where
+  liftIO = id
+
+public export
+implementation MonadIO m => MonadIO (StateT s m) where
+  liftIO x = ST $ \st => do
+    val <- liftIO x
+    pure (val, st)
+
+public export
+interface Monad m => MonadError e m | m where
+  throwError : e -> m a
+  catchError : m a -> (e -> m a) -> m a
+
+public export
+implementation MonadError e (Either e) where
+  throwError = Left
+  catchError (Left e) f = f e
+  catchError (Right x) f = Right x
+
+public export
+implementation MonadError () Maybe where
+  throwError () = Nothing
+  catchError Nothing f = f ()
+  catchError (Just x) f = Just x
+
+public export
+implementation MonadError e m => MonadError e (StateT s m) where
+  throwError e = lift $ throwError e
+  catchError (ST x) f = ST $ \st => catchError (x st) $ flip runStateT st . f
+
+public export
+interface Monad m => MonadReader r m | m where
+  ask : m r
+  local : (r -> r) -> m a -> m a
+  reader : (r -> a) -> m a
+
+-- public export
+-- implementation MonadReader r ((->) r) where
+--   ask = id
+--   local f g = g . f
+--   reader = id
+
+
+-- ExceptT
+
+public export
+record ExceptT (e : Type) (m : Type -> Type) (a : Type) where
+  constructor MkExceptT
+  runExceptT : m (Either e a)
+
+public export
+implementation Functor m => Functor (ExceptT e m) where
+  map f (MkExceptT x) = MkExceptT $ map (map f) x
+
+public export
+implementation Monad m => Applicative (ExceptT e m) where
+  pure = MkExceptT . pure . pure
+
+  (MkExceptT mf) <*> (MkExceptT mx) = MkExceptT $ do
+    Right f <- mf
+      | Left e => pure $ Left e
+    Right x <- mx
+      | Left e => pure $ Left e
+    pure $ Right $ f x
+
+public export
+implementation Monad m => Monad (ExceptT e m) where
+  (MkExceptT mx) >>= f = MkExceptT $ do
+    Right x <- mx
+      | Left e => pure $ Left e
+    runExceptT $ f x
+
+public export
+implementation MonadTrans (ExceptT e) where
+  lift x = MkExceptT $ map Right x
+
+public export
+implementation MonadState s m => MonadState s (ExceptT e m) where
+  get = lift get
+  put x = lift $ put x
+
+public export
+implementation Monad m => MonadError e (ExceptT e m) where
+  throwError = MkExceptT . pure . Left
+  catchError (MkExceptT mx) f = MkExceptT $ do
+    Left e <- mx
+      | Right x => pure $ Right x
+    runExceptT $ f e
+
+public export
+implementation MonadIO m => MonadIO (ExceptT e m) where
+  liftIO = MkExceptT . map Right . liftIO
+
+public export
+implementation MonadReader r m => MonadReader r (ExceptT e m) where
+  ask = lift ask
+  local f (MkExceptT x) = MkExceptT $ local f x
+  reader = lift . reader
+
+
+-- ReaderT
+
+public export
+record ReaderT (r : Type) (m : Type -> Type) (a : Type) where
+  constructor MkReaderT
+  runReaderT : r -> m a
+
+public export
+implementation Functor m => Functor (ReaderT r m) where
+  map f (MkReaderT g) = MkReaderT $ map f . g
+
+public export
+implementation Applicative m => Applicative (ReaderT r m) where
+  pure = MkReaderT . const . pure
+  MkReaderT f <*> MkReaderT x = MkReaderT $ \r => f r <*> x r
+
+public export
+implementation Monad m => Monad (ReaderT r m) where
+  MkReaderT x >>= f = MkReaderT $ \r => x r >>= flip runReaderT r . f
+
+public export
+implementation MonadTrans (ReaderT r) where
+  lift = MkReaderT . const
+
+public export
+implementation Monad m => MonadReader r (ReaderT r m) where
+  ask = MkReaderT pure
+  local f (MkReaderT x) = MkReaderT $ x . f
+  reader f = MkReaderT $ pure . f
+
+public export
+implementation MonadState s m => MonadState s (ReaderT r m) where
+  get = MkReaderT $ const get
+  put = MkReaderT . const . put
+
+public export
+implementation MonadError e m => MonadError e (ReaderT r m) where
+  throwError = MkReaderT . const . throwError
+  catchError (MkReaderT a) h = MkReaderT $ \r => catchError (a r) (flip runReaderT r . h)
+
+public export
+implementation MonadIO m => MonadIO (ReaderT r m) where
+  liftIO = MkReaderT . const . liftIO
diff --git a/impls/idris2/Reader.idr b/impls/idris2/Reader.idr
new file mode 100644
index 0000000000..cbfb8b8109
--- /dev/null
+++ b/impls/idris2/Reader.idr
@@ -0,0 +1,155 @@
+module Reader
+
+import Types
+
+import Control.Monad.Syntax
+import Data.List
+import Data.Strings
+import Text.Lexer
+import Text.Parser
+import Text.Token
+
+data TokenKind
+  = TSymbol
+  | TKeyword
+  | TNumber
+  | TString
+  | TOpenParen | TCloseParen
+  | TOpenBrace | TCloseBrace
+  | TOpenBracket | TCloseBracket
+  | TSigil
+  | TWhitespace
+
+implementation Eq TokenKind where
+  TSymbol == TSymbol = True
+  TKeyword == TKeyword = True
+  TNumber == TNumber = True
+  TString == TString = True
+  TOpenParen == TOpenParen = True
+  TCloseParen == TCloseParen = True
+  TOpenBrace == TOpenBrace = True
+  TCloseBrace == TCloseBrace = True
+  TOpenBracket == TOpenBracket = True
+  TCloseBracket == TCloseBracket = True
+  TWhitespace == TWhitespace = True
+  TSigil == TSigil = True
+  _ == _ = False
+
+unescape : List Char -> List Char
+unescape ('\\'::'\\'::rest) = '\\' :: unescape rest
+unescape ('\\'::'"'::rest) = '"' :: unescape rest
+unescape ('\\'::'n'::rest) = '\n' :: unescape rest
+unescape (c::rest) = c :: unescape rest
+unescape [] = []
+
+implementation Text.Token.TokenKind TokenKind where
+  TokType TSymbol = String
+  TokType TKeyword = String
+  TokType TNumber = Integer
+  TokType TString = String
+  TokType TSigil = String
+  TokType _ = ()
+
+  tokValue TSymbol x = x
+  tokValue TKeyword x = assert_total $ strTail x -- keywords always start with something
+  tokValue TNumber x = cast x
+  tokValue TString x = pack $ unescape $ unpack $ substr 1 (length x `minus` 2) x
+  tokValue TSigil x = x
+  tokValue TOpenParen _ = ()
+  tokValue TCloseParen _ = ()
+  tokValue TOpenBrace _ = ()
+  tokValue TCloseBrace _ = ()
+  tokValue TOpenBracket _ = ()
+  tokValue TCloseBracket _ = ()
+  tokValue TWhitespace _ = ()
+
+Token : Type
+Token = Text.Token.Token TokenKind
+-- Token = TokenData (Text.Token.Token TokenKind)
+
+%hide Text.Token.TokenKind
+%hide Text.Token.Token
+
+isIdentChar : Char -> Bool
+isIdentChar x = not $ isSpace x || (x `elem` unpack "[]{}()'\"`,;")
+
+tokenMap : TokenMap Token
+tokenMap = toTokenMap [
+  (some (space <|> is ','), TWhitespace),
+  (exact "~@", TSigil),
+  (oneOf "'`~^@", TSigil),
+  (is '(', TOpenParen), (is ')', TCloseParen),
+  (is '{', TOpenBrace), (is '}', TCloseBrace),
+  (is '[', TOpenBracket), (is ']', TCloseBracket),
+  (stringLit, TString),
+  (lineComment (is ';'), TWhitespace),
+  (intLit, TNumber),
+  (is ':' <+> some (pred isIdentChar), TKeyword),
+  (some (pred isIdentChar), TSymbol)
+  ]
+
+lexText : String -> Either String (List Token)
+lexText text =
+  case lex tokenMap text of
+       (toks, (_, _, "")) => Right $ map tok toks
+       (_, (row, col, _)) => Left $
+         "Lexer error at " ++ show row ++ ":" ++ show col ++ ": possibly unbalanced string"
+
+Parser : Type -> Type
+Parser = Grammar Token True
+
+mutual
+  stringGrammar : Parser String
+  stringGrammar = match TString <|> map (strCons '\xff') (match TKeyword)
+
+  listGrammar : Parser AST
+  listGrammar = match TOpenParen *> map (List False) (many grammar) <* match TCloseParen
+
+  vectorGrammar : Parser AST
+  vectorGrammar = match TOpenBracket *> map (List True) (many grammar) <* match TCloseBracket
+
+  mapGrammar : Parser AST
+  mapGrammar = match TOpenBrace *> map (Map . fromList) contents <* match TCloseBrace
+    where contents : Grammar Token False (List (String, AST))
+          contents = many [| MkPair stringGrammar grammar |]
+
+  sigilGrammar : Parser AST
+  sigilGrammar = assert_total $ match TSigil >>= sigilAction
+    where partial
+          sigilAction : String -> Parser AST
+          sigilAction "~@" = map (\x => List False [Symbol "splice-unquote", x]) grammar
+          sigilAction "'" = map (\x => List False [Symbol "quote", x]) grammar
+          sigilAction "`" = map (\x => List False [Symbol "quasiquote", x]) grammar
+          sigilAction "~" = map (\x => List False [Symbol "unquote", x]) grammar
+          sigilAction "@" = map (\x => List False [Symbol "deref", x]) grammar
+          sigilAction "^" = do
+            x <- grammar
+            y <- grammar
+            pure $ List False [Symbol "with-meta", y, x]
+
+  grammar : Parser AST
+  grammar = choice [
+    map Symbol $ match TSymbol,
+    map Str stringGrammar,
+    map Number $ match TNumber,
+    listGrammar,
+    vectorGrammar,
+    mapGrammar,
+    sigilGrammar
+    ]
+
+parseTokens : List Token -> Either String (List AST)
+parseTokens toks =
+  case parse (many grammar) toks of
+       Right (ast, []) => Right ast
+       Right (ast, rest) => Left $ "Parse error: possible unbalanced parentheses"
+       Left (Error msg _) => Left msg
+
+export
+parseText : String -> Either String (List AST)
+parseText = parseTokens . filter notWhitespace <=< lexText
+  where notWhitespace : Token -> Bool
+        notWhitespace t =
+          case kind t of
+               TWhitespace => False
+               _ => True
diff --git a/impls/idris2/Types.idr b/impls/idris2/Types.idr
new file mode 100644
index 0000000000..8126931640
--- /dev/null
+++ b/impls/idris2/Types.idr
@@ -0,0 +1,114 @@
+module Types
+
+import Control.Monad.State
+import public Data.IORef
+import Data.List
+import public Data.SortedMap
+import Data.Strings
+import public MonadTrans
+
+mutual
+  public export
+  data AST = Symbol String -- Identifiers
+           | Str String -- Includes keywords
+           | Number Integer
+           | Atom (IORef AST)
+           | List Bool (List AST) -- List False -> List, List True -> Vector
+           | Map (SortedMap String AST)
+           | Func Bool (List AST -> MalM AST)
+
+  public export
+  record Env where
+    constructor MkEnv
+    evalFunc : AST -> MalM AST
+    symbols : List (IORef (SortedMap String AST))
+
+  public export
+  MalM : Type -> Type
+  MalM = ReaderT Env (ExceptT AST IO)
+
+export
+toString : (readably : Bool) -> AST -> IO String
+toString b (Symbol s) = pure s
+toString b (Str s) =
+  case strUncons s of
+       Just ('\xff', rest) => pure $ strCons ':' rest
+       _ => pure $ if b then show s else s
+toString b (Number x) = pure $ show x
+toString b (Atom a) = do
+  x <- readIORef a
+  sx <- toString b x
+  pure $ "(atom " ++ sx ++ ")"
+toString b (List False xs) = do
+  sxs <- traverse (toString b) xs
+  pure $ "(" ++ unwords sxs ++ ")"
+toString b (List True xs) = do
+  sxs <- traverse (toString b) xs
+  pure $ "[" ++ unwords sxs ++ "]"
+toString b (Map m) = do
+  sm <- map concat $ traverse onePair $ SortedMap.toList m
+  pure $ "{" ++ unwords sm ++ "}"
+  where onePair : (String, AST) -> IO (List String)
+        onePair (k, v) = sequence [toString b (Str k), toString b v]
+toString b (Func False f) = pure "#<function>"
+toString b (Func True f) = pure "#<macro>"
+
+export
+implementation Eq AST where
+  Symbol x == Symbol y = x == y
+  Str x == Str y = x == y
+  Number x == Number y = x == y
+  List _ x == List _ y = x == y
+  Map x == Map y = SortedMap.toList x == SortedMap.toList y
+  Func _ _ == Func _ _ = False
+  _ == _ = False
+
+export
+truthiness : AST -> Bool
+truthiness (Symbol "false") = False
+truthiness (Symbol "nil") = False
+truthiness _ = True
+
+export
+Keyword : String -> AST
+Keyword = Str . strCons '\xff'
+
+export
+getEnv : MalM (IORef (SortedMap String AST))
+getEnv = do
+  env <- reader symbols
+  case env of
+       [] => throwError $ Str "Internal error: no environment"
+       e :: _ => pure e
+
+export
+withLocalEnv : MalM a -> MalM a
+withLocalEnv x = do
+  new <- liftIO $ newIORef empty
+  local (record {symbols $= (new::)}) x
+
+export
+withGlobalEnv : MalM a -> MalM a
+withGlobalEnv x = do
+  env <- reader symbols
+  evil <- reader evalFunc
+  case last' env of
+       Just ge => local (const $ MkEnv evil [ge]) x
+       Nothing => throwError $ Str "Internal error: no environment"
+
+export
+insert : String -> AST -> MalM ()
+insert n x = do
+  env <- getEnv
+  liftIO $ modifyIORef env $ insert n x
+
+export
+lookup : String -> MalM AST
+lookup n = reader symbols >>= go
+  where go : List (IORef (SortedMap String AST)) -> MalM AST
+        go [] = throwError $ Str $ "'" ++ n ++ "' not found"
+        go (e::es) = do
+          val <- map (lookup n) $ liftIO $ readIORef e
+          case val of
+               Just x => pure x
+               Nothing => go es
diff --git a/impls/idris2/run b/impls/idris2/run
new file mode 100755
index 0000000000..2d6ae43752
--- /dev/null
+++ b/impls/idris2/run
@@ -0,0 +1,2 @@
+#!/bin/bash
+exec $(dirname $0)/build/exec/${STEP:-stepA_mal} "${@}"
diff --git a/impls/idris2/step0_repl.idr b/impls/idris2/step0_repl.idr
new file mode 100644
index 0000000000..032d52f50e
--- /dev/null
+++ b/impls/idris2/step0_repl.idr
@@ -0,0 +1,24 @@
+import System.File
+
+read : String -> String
+read = id
+
+eval : String -> String
+eval = id
+
+print : String -> String
+print = id
+
+repl : a -> String -> (a -> String -> IO a) -> IO b
+repl state prompt f = do
+  putStr prompt
+  fflush stdout
+  input <- getLine
+  f state input
+  repl state prompt f
+
+main : IO ()
+main = repl () "user> " $ \state, input => do
+  let result = print $ eval $ read input
+  putStrLn result
+  pure ()
diff --git a/impls/idris2/step1_read_print.idr b/impls/idris2/step1_read_print.idr
new file mode 100644
index 0000000000..188f078941
--- /dev/null
+++ b/impls/idris2/step1_read_print.idr
@@ -0,0 +1,37 @@
+import System.File
+
+import Types
+import Reader
+
+read : String -> IO (Maybe AST)
+read s =
+  case parseText s of
+       Right [ast] => pure (Just ast)
+       Right _ => do
+         putStrLn "wack"
+         pure Nothing
+       Left e => do
+         putStrLn $ "parse error: " ++ e
+         pure Nothing
+
+eval : AST -> IO AST
+eval = pure
+
+repl : a -> String -> (a -> String -> IO a) -> IO ()
+repl state prompt f = do
+  putStr prompt
+  fflush stdout
+  input <- getLine
+  False <- fEOF stdin
+    | True => putStr "\n"
+  f state input
+  repl state prompt f
+
+main : IO ()
+main = repl () "user> " $ \state, input => do
+  Just ast <- read input
+    | Nothing => pure ()
+  result <- eval ast
+  str <- toString True result
+  putStrLn str
+  pure ()
diff --git a/impls/idris2/step2_eval.idr b/impls/idris2/step2_eval.idr
new file mode 100644
index 0000000000..a58c6b9da6
--- /dev/null
+++ b/impls/idris2/step2_eval.idr
@@ -0,0 +1,43 @@
+import System.File
+
+import Types
+import MonadTrans
+import Reader
+import Eval
+import Core
+
+read : String -> MalM (Maybe AST)
+read s =
+  case parseText s of
+       Right [ast] => pure (Just ast)
+       Right [] => pure Nothing
+       Right _ => throwError $ Str "wack" -- too many ast's
+       Left e => throwError $ Str $ "parse error: " ++ e
+
+runMalM : MalM () -> ReaderT Env IO ()
+runMalM x = MkReaderT $ \r => do
+  Right x <- runExceptT $ runReaderT x r
+    | Left e => do
+      se <- toString False e
+      putStrLn $ "error: " ++ se
+  pure x
+
+repl : r -> String -> (String -> ReaderT r IO ()) -> IO ()
+repl r prompt f = do
+  putStr prompt
+  fflush stdout
+  input <- getLine
+  False <- fEOF stdin
+    | True => putStr "\n"
+  runReaderT (f input) r
+  repl r prompt f
+
+main : IO ()
+main = do
+  startingEnv <- getStartingEnv
+  repl startingEnv "user> " $ \input => runMalM $ do
+    Just ast <- read input
+      | Nothing => pure ()
+    result <- eval ast
+    str <- MonadTrans.liftIO $ toString True result
+    MonadTrans.liftIO $ putStrLn str
diff --git a/impls/idris2/step3_env.idr b/impls/idris2/step3_env.idr
new file mode 120000
index 0000000000..5ec4d46d7c
--- /dev/null
+++ b/impls/idris2/step3_env.idr
@@ -0,0 +1 @@
+step2_eval.idr
\ No newline at end of file
diff --git a/impls/idris2/step4_if_fn_do.idr b/impls/idris2/step4_if_fn_do.idr
new file mode 120000
index 0000000000..712248ede6
--- /dev/null
+++ b/impls/idris2/step4_if_fn_do.idr
@@ -0,0 +1 @@
+step3_env.idr
\ No newline at end of file
diff --git a/impls/idris2/step5_tco.idr b/impls/idris2/step5_tco.idr
new file mode 120000
index 0000000000..add5fc57a7
--- /dev/null
+++ b/impls/idris2/step5_tco.idr
@@ -0,0 +1 @@
+step4_if_fn_do.idr
\ No newline at end of file
diff --git a/impls/idris2/step6_file.idr b/impls/idris2/step6_file.idr
new file mode 100644
index 0000000000..cad29f9125
--- /dev/null
+++ b/impls/idris2/step6_file.idr
@@ -0,0 +1,51 @@
+import System
+import System.File
+
+import Types
+import MonadTrans
+import Reader
+import Eval
+import Core
+
+read : String -> MalM (Maybe AST)
+read s =
+  case parseText s of
+       Right [ast] => pure (Just ast)
+       Right [] => pure Nothing
+       Right _ => throwError $ Str "wack" -- too many ast's
+       Left e => throwError $ Str $ "parse error: " ++ e
+
+runMalM : MalM a -> ReaderT Env IO ()
+runMalM x = MkReaderT $ \r => do
+  Right _ <- runExceptT $ runReaderT x r
+    | Left e => do
+      se <- toString False e
+      putStrLn $ "error: " ++ se
+  pure ()
+
+repl : r -> String -> (String -> ReaderT r IO ()) -> IO ()
+repl r prompt f = do
+  putStr prompt
+  fflush stdout
+  input <- getLine
+  False <- fEOF stdin
+    | True => putStr "\n"
+  runReaderT (f input) r
+  repl r prompt f
+
+doRepl : Env -> IO ()
+doRepl startingEnv = repl startingEnv "user> " $ \input => runMalM $ do
+  Just ast <- read input
+    | Nothing => pure ()
+  result <- eval ast
+  str <- MonadTrans.liftIO $ toString True result
+  MonadTrans.liftIO $ putStrLn str
+
+main : IO ()
+main = do
+  startingEnv <- getStartingEnv
+  args <- getArgs
+  case args of
+       (_::f::_) => flip runReaderT startingEnv $ runMalM $
+           eval $ List False [Symbol "load-file", Str f]
+       _ => doRepl startingEnv
diff --git a/impls/idris2/step7_quote.idr b/impls/idris2/step7_quote.idr
new file mode 120000
index 0000000000..d2418f36b2
--- /dev/null
+++ b/impls/idris2/step7_quote.idr
@@ -0,0 +1 @@
+step6_file.idr
\ No newline at end of file
diff --git a/impls/idris2/step8_macros.idr b/impls/idris2/step8_macros.idr
new file mode 120000
index 0000000000..b2d7804675
--- /dev/null
+++ b/impls/idris2/step8_macros.idr
@@ -0,0 +1 @@
+step7_quote.idr
\ No newline at end of file
diff --git a/impls/idris2/step9_try.idr b/impls/idris2/step9_try.idr
new file mode 120000
index 0000000000..281af9ad24
--- /dev/null
+++ b/impls/idris2/step9_try.idr
@@ -0,0 +1 @@
+step8_macros.idr
\ No newline at end of file
diff --git a/impls/idris2/stepA_mal.idr b/impls/idris2/stepA_mal.idr
new file mode 100644
index 0000000000..dec38e77f4
--- /dev/null
+++ b/impls/idris2/stepA_mal.idr
@@ -0,0 +1,57 @@
+import System
+import System.File
+
+import Types
+import MonadTrans
+import Reader
+import Eval
+import Core
+
+read : String -> MalM (Maybe AST)
+read s =
+  case parseText s of
+       Right [ast] => pure (Just ast)
+       Right [] => pure Nothing
+       Right _ => throwError $ Str "wack" -- too many ast's
+       Left e => throwError $ Str $ "parse error: " ++ e
+
+runMalM : MalM a -> ReaderT Env IO ()
+runMalM x = MkReaderT $ \r => do
+  Right _ <- runExceptT $ runReaderT x r
+    | Left e => do
+      se <- toString False e
+      putStrLn $ "error: " ++ se
+  pure ()
+
+repl : r -> String -> (String -> ReaderT r IO ()) -> IO ()
+repl r prompt f = do
+  putStr prompt
+  fflush stdout
+  input <- getLine
+  False <- fEOF stdin
+    | True => putStr "\n"
+  runReaderT (f input) r
+  repl r prompt f
+
+doRepl : Env -> IO ()
+doRepl startingEnv = do
+  flip runReaderT startingEnv $ runMalM $ do
+    Just x <- read "(println (str \"Mal [\" *host-language* \"]\"))"
+      | Nothing => pure ()
+    eval x
+    pure ()
+  repl startingEnv "user> " $ \input => runMalM $ do
+    Just ast <- read input
+      | Nothing => pure ()
+    result <- eval ast
+    str <- MonadTrans.liftIO $ toString True result
+    MonadTrans.liftIO $ putStrLn str
+
+main : IO ()
+main = do
+  startingEnv <- getStartingEnv
+  args <- getArgs
+  case args of
+       (_::f::_) => flip runReaderT startingEnv $ runMalM $
+           eval $ List False [Symbol "load-file", Str f]
+       _ => doRepl startingEnv