From 37bf242325b087afd6fbe4947a551ae24f5fedbd Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Mon, 29 Jun 2020 15:08:01 -0400
Subject: [PATCH 01/17] Idris2: step 0 and 1

---
 Makefile                          |   4 +-
 impls/idris2/.gitignore           |   1 +
 impls/idris2/AST.idr              |  36 +++++++
 impls/idris2/Makefile             |  15 +++
 impls/idris2/Reader.idr           | 153 ++++++++++++++++++++++++++++++
 impls/idris2/run                  |   2 +
 impls/idris2/step0_repl.idr       |  24 +++++
 impls/idris2/step1_read_print.idr |  36 +++++++
 8 files changed, 270 insertions(+), 1 deletion(-)
 create mode 100644 impls/idris2/.gitignore
 create mode 100644 impls/idris2/AST.idr
 create mode 100644 impls/idris2/Makefile
 create mode 100644 impls/idris2/Reader.idr
 create mode 100755 impls/idris2/run
 create mode 100644 impls/idris2/step0_repl.idr
 create mode 100644 impls/idris2/step1_read_print.idr

diff --git a/Makefile b/Makefile
index c42c5ca62f..ccd2d73937 100644
--- a/Makefile
+++ b/Makefile
@@ -94,7 +94,8 @@ IMPLS = ada ada.2 awk bash basic bbc-basic c chuck clojure coffee common-lisp cp
 	guile haskell haxe hy 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
+	swift swift3 swift4 swift5 tcl ts vala vb vhdl vimscript wasm wren yorick xslt zig \
+	idris2
 
 EXTENSION = .mal
 
@@ -270,6 +271,7 @@ wren_STEP_TO_PROG =          impls/wren/$($(1)).wren
 yorick_STEP_TO_PROG =        impls/yorick/$($(1)).i
 xslt_STEP_TO_PROG =          impls/xslt/$($(1))
 zig_STEP_TO_PROG =           impls/zig/$($(1))
+idris2_STEP_TO_PROG =        impls/idris2/build/exec/$($(1))
 
 #
 # General settings and utility functions
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/AST.idr b/impls/idris2/AST.idr
new file mode 100644
index 0000000000..a178eed75f
--- /dev/null
+++ b/impls/idris2/AST.idr
@@ -0,0 +1,36 @@
+module AST
+
+import Data.SortedMap
+import Data.Strings
+
+public export
+data AST = Symbol String -- Identifiers
+         | Str String -- Includes keywords
+         | Quasiquote AST
+         | Quote AST
+         | Unquote AST
+         | SpliceUnquote AST
+         | Deref AST
+         | WithMeta AST AST
+         | Number Integer
+         | List (List AST)
+         | Vector (List AST)
+         | Map (SortedMap String AST)
+
+export
+implementation Show AST where
+  show (Symbol s) = s
+  show (Str s) =
+    case strUncons s of
+         Just ('\xff', rest) => strCons ':' rest
+         _ => show s
+  show (Quasiquote x) = "(quasiquote " ++ show x ++ ")"
+  show (Quote x) = "(quote " ++ show x ++ ")"
+  show (Unquote x) = "(unquote " ++ show x ++ ")"
+  show (SpliceUnquote x) = "(splice-unquote " ++ show x ++ ")"
+  show (Deref x) = "(deref " ++ show x ++ ")"
+  show (WithMeta a b) = "(with-meta " ++ show a ++ " " ++ show b ++ ")"
+  show (Number x) = show x
+  show (List xs) = "(" ++ unwords (map show xs) ++ ")"
+  show (Vector xs) = "[" ++ unwords (map show xs) ++ "]"
+  show (Map m) = "{" ++ unwords (concatMap (\(a, b) => [show (Str a), show b]) $ toList m) ++ "}"
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
new file mode 100644
index 0000000000..33ef5ffaee
--- /dev/null
+++ b/impls/idris2/Makefile
@@ -0,0 +1,15 @@
+SRCS = step0_repl.idr step1_read_print.idr
+OTHER_SRCS = AST.idr Reader.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/Reader.idr b/impls/idris2/Reader.idr
new file mode 100644
index 0000000000..3751f0a504
--- /dev/null
+++ b/impls/idris2/Reader.idr
@@ -0,0 +1,153 @@
+module Reader
+
+import AST
+
+import Control.Monad.Syntax
+import Data.List
+import Data.SortedMap
+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 (many grammar) <* match TCloseParen
+
+  vectorGrammar : Parser AST
+  vectorGrammar = match TOpenBracket *> map Vector (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 SpliceUnquote grammar
+          sigilAction "'" = map Quote grammar
+          sigilAction "`" = map Quasiquote grammar
+          sigilAction "~" = map Unquote grammar
+          sigilAction "@" = map Deref grammar
+          sigilAction "^" = flip WithMeta <$> grammar <*> grammar
+
+  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" ++ show ast
+       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/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..dca06d96c9
--- /dev/null
+++ b/impls/idris2/step1_read_print.idr
@@ -0,0 +1,36 @@
+import System.File
+
+import AST
+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
+  printLn result
+  pure ()

From 9300fcc4fed5a87ec4e723431c3e5040f1c44418 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Tue, 30 Jun 2020 03:09:39 -0400
Subject: [PATCH 02/17] Idris2: step 2: eval

---
 impls/idris2/AST.idr              |  36 -----------
 impls/idris2/Eval.idr             |  38 +++++++++++
 impls/idris2/Makefile             |   4 +-
 impls/idris2/MonadTrans.idr       |  90 ++++++++++++++++++++++++++
 impls/idris2/Reader.idr           |   5 +-
 impls/idris2/Types.idr            | 104 ++++++++++++++++++++++++++++++
 impls/idris2/step1_read_print.idr |   2 +-
 impls/idris2/step2_eval.idr       |  39 +++++++++++
 8 files changed, 276 insertions(+), 42 deletions(-)
 delete mode 100644 impls/idris2/AST.idr
 create mode 100644 impls/idris2/Eval.idr
 create mode 100644 impls/idris2/MonadTrans.idr
 create mode 100644 impls/idris2/Types.idr
 create mode 100644 impls/idris2/step2_eval.idr

diff --git a/impls/idris2/AST.idr b/impls/idris2/AST.idr
deleted file mode 100644
index a178eed75f..0000000000
--- a/impls/idris2/AST.idr
+++ /dev/null
@@ -1,36 +0,0 @@
-module AST
-
-import Data.SortedMap
-import Data.Strings
-
-public export
-data AST = Symbol String -- Identifiers
-         | Str String -- Includes keywords
-         | Quasiquote AST
-         | Quote AST
-         | Unquote AST
-         | SpliceUnquote AST
-         | Deref AST
-         | WithMeta AST AST
-         | Number Integer
-         | List (List AST)
-         | Vector (List AST)
-         | Map (SortedMap String AST)
-
-export
-implementation Show AST where
-  show (Symbol s) = s
-  show (Str s) =
-    case strUncons s of
-         Just ('\xff', rest) => strCons ':' rest
-         _ => show s
-  show (Quasiquote x) = "(quasiquote " ++ show x ++ ")"
-  show (Quote x) = "(quote " ++ show x ++ ")"
-  show (Unquote x) = "(unquote " ++ show x ++ ")"
-  show (SpliceUnquote x) = "(splice-unquote " ++ show x ++ ")"
-  show (Deref x) = "(deref " ++ show x ++ ")"
-  show (WithMeta a b) = "(with-meta " ++ show a ++ " " ++ show b ++ ")"
-  show (Number x) = show x
-  show (List xs) = "(" ++ unwords (map show xs) ++ ")"
-  show (Vector xs) = "[" ++ unwords (map show xs) ++ "]"
-  show (Map m) = "{" ++ unwords (concatMap (\(a, b) => [show (Str a), show b]) $ toList m) ++ "}"
diff --git a/impls/idris2/Eval.idr b/impls/idris2/Eval.idr
new file mode 100644
index 0000000000..ec62d535de
--- /dev/null
+++ b/impls/idris2/Eval.idr
@@ -0,0 +1,38 @@
+module Eval
+
+import Types
+import MonadTrans
+
+public export
+eval : AST -> MalM AST
+eval (Symbol n) = do
+  Just x <- gets (lookup n)
+    | Nothing => throwError $ Str $ "unrecognized ident " ++ n
+  pure x
+eval (Str s) = pure $ Str s
+eval (Number x) = pure $ Number x
+eval (Quasiquote x) = pure x -- TODO
+eval (Quote x) = pure x -- TODO
+eval (Unquote x) = pure x -- TODO
+eval (SpliceUnquote x) = pure x -- TODO
+eval (Deref x) = pure x -- TODO
+eval (WithMeta a b) = pure $ WithMeta a b -- TODO
+eval (List []) = pure $ List []
+eval (List xs) = do
+  Func f'::xs' <- traverse eval xs
+    | _ => throwError $ Str "tried to call something that's not a function"
+  f' xs'
+eval (Vector xs) = map Vector $ traverse eval xs
+eval (Map m) = map Map $ traverse eval m
+eval (Func f) = pure $ Func f
+
+-- Builtins
+
+public export
+startingEnv : Env
+startingEnv = fromList [
+  ("+", Func $ toMalFunc ((+) {ty=Integer})),
+  ("-", Func $ toMalFunc ((-) {ty=Integer})),
+  ("*", Func $ toMalFunc ((*) {ty=Integer})),
+  ("/", Func $ toMalFunc (div {ty=Integer}))
+]
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index 33ef5ffaee..50005a5dce 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,5 +1,5 @@
-SRCS = step0_repl.idr step1_read_print.idr
-OTHER_SRCS = AST.idr Reader.idr
+SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr
+OTHER_SRCS = Types.idr Reader.idr Eval.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
 idris_args = -p contrib
diff --git a/impls/idris2/MonadTrans.idr b/impls/idris2/MonadTrans.idr
new file mode 100644
index 0000000000..4c0035b568
--- /dev/null
+++ b/impls/idris2/MonadTrans.idr
@@ -0,0 +1,90 @@
+module MonadTrans
+
+import public Control.Monad.Trans
+import public Control.Monad.State
+
+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
+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 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 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
+
+-- This module would just be ExceptT, but until the Idris 2 stdlib has a
+-- working IO typeclass, we gotta roll our own.
+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 (ExceptT e m) where
+  liftIO = MkExceptT . map Right . liftIO
+
+public export
+implementation MonadIO m => MonadIO (StateT s m) where
+  liftIO x = ST $ \st => do
+    val <- liftIO x
+    pure (val, st)
diff --git a/impls/idris2/Reader.idr b/impls/idris2/Reader.idr
index 3751f0a504..b7d33266d5 100644
--- a/impls/idris2/Reader.idr
+++ b/impls/idris2/Reader.idr
@@ -1,10 +1,9 @@
 module Reader
 
-import AST
+import Types
 
 import Control.Monad.Syntax
 import Data.List
-import Data.SortedMap
 import Data.Strings
 import Text.Lexer
 import Text.Parser
@@ -140,7 +139,7 @@ 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" ++ show ast
+       Right (ast, rest) => Left $ "Parse error: possible unbalanced parentheses"
        Left (Error msg _) => Left msg
 
 export
diff --git a/impls/idris2/Types.idr b/impls/idris2/Types.idr
new file mode 100644
index 0000000000..6350db4a0d
--- /dev/null
+++ b/impls/idris2/Types.idr
@@ -0,0 +1,104 @@
+module Types
+
+import Control.Monad.State
+import public Data.SortedMap
+import Data.Strings
+import MonadTrans
+
+mutual
+  public export
+  data AST = Symbol String -- Identifiers
+           | Str String -- Includes keywords
+           | Number Integer
+           | Quasiquote AST
+           | Quote AST
+           | Unquote AST
+           | SpliceUnquote AST
+           | Deref AST
+           | WithMeta AST AST
+           | List (List AST)
+           | Vector (List AST)
+           | Map (SortedMap String AST)
+           | Func (List AST -> MalM AST)
+
+  public export
+  Env : Type
+  Env = SortedMap String AST
+
+  public export
+  MalM : Type -> Type
+  MalM = StateT Env (ExceptT AST IO)
+
+export
+implementation Show AST where
+  show (Symbol s) = s
+  show (Str s) =
+    case strUncons s of
+         Just ('\xff', rest) => strCons ':' rest
+         _ => show s
+  show (Quasiquote x) = "(quasiquote " ++ show x ++ ")"
+  show (Quote x) = "(quote " ++ show x ++ ")"
+  show (Unquote x) = "(unquote " ++ show x ++ ")"
+  show (SpliceUnquote x) = "(splice-unquote " ++ show x ++ ")"
+  show (Deref x) = "(deref " ++ show x ++ ")"
+  show (WithMeta a b) = "(with-meta " ++ show a ++ " " ++ show b ++ ")"
+  show (Number x) = show x
+  show (List xs) = "(" ++ unwords (map show xs) ++ ")"
+  show (Vector xs) = "[" ++ unwords (map show xs) ++ "]"
+  show (Map m) = "{" ++ unwords (concatMap (\(a, b) => [show (Str a), show b]) $ toList m) ++ "}"
+  show (Func f) = "<function>"
+
+public export
+interface MalType a where
+  toMalAst : a -> AST
+  fromMalAst : AST -> Maybe a
+
+public export
+implementation MalType AST where
+  toMalAst = id
+  fromMalAst = Just
+
+public export
+implementation MalType Integer where
+  toMalAst = Number
+  fromMalAst (Number x) = Just x
+  fromMalAst _ = Nothing
+
+public export
+implementation MalType String where
+  toMalAst = Str
+  fromMalAst (Str s) = Just s
+  fromMalAst _ = Nothing
+
+public export
+implementation MalType a => MalType (List a) where
+  toMalAst = Vector . map toMalAst -- Should this be List or Vector?
+  fromMalAst (List xs) = traverse fromMalAst xs
+  fromMalAst _ = Nothing
+
+public export
+implementation MalType a => MalType (SortedMap String a) where
+  toMalAst = Map . map toMalAst
+  fromMalAst (Map m) = traverse fromMalAst m
+  fromMalAst _ = Nothing
+
+public export
+interface MalFunction a where
+  toMalFunc : a -> List AST -> MalM AST
+
+public export
+implementation MalType a => MalFunction a where
+  toMalFunc x [] = pure $ toMalAst x
+  toMalFunc _ _ = throwError $ Str "Too many arguments"
+
+public export
+implementation MalType a => MalFunction (MalM a) where
+  toMalFunc x [] = map toMalAst x
+  toMalFunc _ _ = throwError $ Str "Too many arguments"
+
+public export
+implementation (MalType a, MalFunction b) => MalFunction (a -> b) where
+  toMalFunc _ [] = throwError $ Str "Too few arguments"
+  toMalFunc f (x::xs) = case fromMalAst x of
+                             Just x' => toMalFunc (f x') xs
+                             Nothing => throwError $ Str "Wrong argument type"
diff --git a/impls/idris2/step1_read_print.idr b/impls/idris2/step1_read_print.idr
index dca06d96c9..e7d9f3d8a5 100644
--- a/impls/idris2/step1_read_print.idr
+++ b/impls/idris2/step1_read_print.idr
@@ -1,6 +1,6 @@
 import System.File
 
-import AST
+import Types
 import Reader
 
 read : String -> IO (Maybe AST)
diff --git a/impls/idris2/step2_eval.idr b/impls/idris2/step2_eval.idr
new file mode 100644
index 0000000000..9dba1ccdb7
--- /dev/null
+++ b/impls/idris2/step2_eval.idr
@@ -0,0 +1,39 @@
+import System.File
+
+import Types
+import MonadTrans
+import Reader
+import Eval
+
+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 () -> StateT Env IO ()
+runMalM x = ST $ \st => do
+  Left e <- runExceptT $ runStateT x st
+    | Right x => pure x
+  putStr "error: "
+  printLn e
+  pure ((), st)
+
+repl : a -> String -> (String -> StateT a IO ()) -> IO ()
+repl state prompt f = do
+  putStr prompt
+  fflush stdout
+  input <- getLine
+  False <- fEOF stdin
+    | True => putStr "\n"
+  ((), state') <- runStateT (f input) state
+  repl state' prompt f
+
+main : IO ()
+main = repl startingEnv "user> " $ \input => runMalM $ do
+  Just ast <- read input
+    | Nothing => pure ()
+  result <- eval ast
+  MonadTrans.liftIO $ printLn result

From 575fb0c515835a2d9de6fc081b942adcfe27ba80 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Tue, 30 Jun 2020 17:24:23 -0400
Subject: [PATCH 03/17] Idris2: step 3

---
 impls/idris2/Eval.idr       | 123 ++++++++++++++++++++++++++++++----
 impls/idris2/Makefile       |   2 +-
 impls/idris2/MonadTrans.idr | 130 +++++++++++++++++++++++++++---------
 impls/idris2/Types.idr      |  84 +++++++++--------------
 impls/idris2/step2_eval.idr |  32 ++++-----
 impls/idris2/step3_env.idr  |  39 +++++++++++
 6 files changed, 296 insertions(+), 114 deletions(-)
 create mode 100644 impls/idris2/step3_env.idr

diff --git a/impls/idris2/Eval.idr b/impls/idris2/Eval.idr
index ec62d535de..c2efba9da0 100644
--- a/impls/idris2/Eval.idr
+++ b/impls/idris2/Eval.idr
@@ -5,12 +5,11 @@ import MonadTrans
 
 public export
 eval : AST -> MalM AST
-eval (Symbol n) = do
-  Just x <- gets (lookup n)
-    | Nothing => throwError $ Str $ "unrecognized ident " ++ n
-  pure x
+eval (Symbol n) = lookup n
 eval (Str s) = pure $ Str s
 eval (Number x) = pure $ Number x
+eval (Boolean b) = pure $ Boolean b
+eval Nil = pure Nil
 eval (Quasiquote x) = pure x -- TODO
 eval (Quote x) = pure x -- TODO
 eval (Unquote x) = pure x -- TODO
@@ -18,21 +17,117 @@ eval (SpliceUnquote x) = pure x -- TODO
 eval (Deref x) = pure x -- TODO
 eval (WithMeta a b) = pure $ WithMeta a b -- TODO
 eval (List []) = pure $ List []
-eval (List xs) = do
-  Func f'::xs' <- traverse eval xs
+eval (List (f::xs)) = do
+  Func f' <- eval f
     | _ => throwError $ Str "tried to call something that's not a function"
-  f' xs'
+  f' xs
 eval (Vector xs) = map Vector $ traverse eval xs
 eval (Map m) = map Map $ traverse eval m
 eval (Func f) = pure $ Func f
 
 -- Builtins
+public export
+interface MalType a where
+  toMalAst : a -> AST
+  fromMalAst : AST -> Maybe a
+
+public export
+implementation MalType AST where
+  toMalAst = id
+  fromMalAst = Just
+
+public export
+implementation MalType Integer where
+  toMalAst = Number
+  fromMalAst (Number x) = Just x
+  fromMalAst _ = Nothing
+
+public export
+implementation MalType String where
+  toMalAst = Str
+  fromMalAst (Str s) = Just s
+  fromMalAst _ = Nothing
+
+public export
+implementation MalType a => MalType (List a) where
+  toMalAst = Vector . map toMalAst -- Should this be List or Vector?
+  fromMalAst (List xs) = traverse fromMalAst xs
+  fromMalAst _ = Nothing
+
+public export
+implementation MalType a => MalType (SortedMap String a) where
+  toMalAst = Map . map toMalAst
+  fromMalAst (Map m) = traverse fromMalAst m
+  fromMalAst _ = Nothing
+
+public export
+interface MalFunction a where
+  toMalFunc : a -> List AST -> MalM AST
+
+public 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"
+
+public export
+implementation MalType a => MalFunction (MalM a) where
+  toMalFunc x [] = map toMalAst x
+  toMalFunc _ xs = do
+    traverse eval xs
+    throwError $ Str "Too many arguments"
+
+public 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
+
+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"
+
+letBuiltin : List AST -> MalM AST
+letBuiltin [] = throwError $ Str "let*: too few arguments"
+letBuiltin [_] = throwError $ Str "let*: too few arguments"
+letBuiltin [defs, ans] = do
+  defs' <- the (MalM _) $ case defs of
+    List xs => pure xs
+    Vector xs => pure xs
+    _ => throwError $ Str "let*: expecting vector or list"
+  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*: too many arguments"
 
 public export
-startingEnv : Env
-startingEnv = fromList [
-  ("+", Func $ toMalFunc ((+) {ty=Integer})),
-  ("-", Func $ toMalFunc ((-) {ty=Integer})),
-  ("*", Func $ toMalFunc ((*) {ty=Integer})),
-  ("/", Func $ toMalFunc (div {ty=Integer}))
-]
+getStartingEnv : IO Env
+getStartingEnv = map pure $ newIORef startingEnv
+  where
+    startingEnv : SortedMap String AST
+    startingEnv = fromList [
+      ("nil", Nil),
+      ("true", Boolean True),
+      ("false", Boolean True),
+      ("+", Func $ toMalFunc ((+) {ty=Integer})),
+      ("-", Func $ toMalFunc ((-) {ty=Integer})),
+      ("*", Func $ toMalFunc ((*) {ty=Integer})),
+      ("/", Func $ toMalFunc (div {ty=Integer})),
+      ("def!", Func defBuiltin),
+      ("let*", Func letBuiltin)
+    ]
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index 50005a5dce..be85bffc00 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,4 +1,4 @@
-SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr
+SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr step3_env.idr
 OTHER_SRCS = Types.idr Reader.idr Eval.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
diff --git a/impls/idris2/MonadTrans.idr b/impls/idris2/MonadTrans.idr
index 4c0035b568..497d3b0507 100644
--- a/impls/idris2/MonadTrans.idr
+++ b/impls/idris2/MonadTrans.idr
@@ -3,6 +3,59 @@ 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
@@ -39,23 +92,6 @@ implementation MonadState s m => MonadState s (ExceptT e m) where
   get = lift get
   put x = lift $ put x
 
-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 Monad m => MonadError e (ExceptT e m) where
   throwError = MkExceptT . pure . Left
@@ -65,26 +101,56 @@ implementation Monad m => MonadError e (ExceptT e m) where
     runExceptT $ f e
 
 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
+implementation MonadIO m => MonadIO (ExceptT e m) where
+  liftIO = MkExceptT . map Right . liftIO
 
--- This module would just be ExceptT, but until the Idris 2 stdlib has a
--- working IO typeclass, we gotta roll our own.
 public export
-interface Monad m => MonadIO m where
-  liftIO : IO a -> m a
+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
-implementation MonadIO IO where
-  liftIO = id
+record ReaderT (r : Type) (m : Type -> Type) (a : Type) where
+  constructor MkReaderT
+  runReaderT : r -> m a
 
 public export
-implementation MonadIO m => MonadIO (ExceptT e m) where
-  liftIO = MkExceptT . map Right . liftIO
+implementation Functor m => Functor (ReaderT r m) where
+  map f (MkReaderT g) = MkReaderT $ map f . g
 
 public export
-implementation MonadIO m => MonadIO (StateT s m) where
-  liftIO x = ST $ \st => do
-    val <- liftIO x
-    pure (val, st)
+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/Types.idr b/impls/idris2/Types.idr
index 6350db4a0d..a0b8f7e5eb 100644
--- a/impls/idris2/Types.idr
+++ b/impls/idris2/Types.idr
@@ -1,15 +1,18 @@
 module Types
 
 import Control.Monad.State
+import public Data.IORef
 import public Data.SortedMap
 import Data.Strings
-import MonadTrans
+import public MonadTrans
 
 mutual
   public export
   data AST = Symbol String -- Identifiers
            | Str String -- Includes keywords
            | Number Integer
+           | Boolean Bool
+           | Nil
            | Quasiquote AST
            | Quote AST
            | Unquote AST
@@ -23,11 +26,11 @@ mutual
 
   public export
   Env : Type
-  Env = SortedMap String AST
+  Env = List (IORef (SortedMap String AST))
 
   public export
   MalM : Type -> Type
-  MalM = StateT Env (ExceptT AST IO)
+  MalM = ReaderT Env (ExceptT AST IO)
 
 export
 implementation Show AST where
@@ -36,69 +39,48 @@ implementation Show AST where
     case strUncons s of
          Just ('\xff', rest) => strCons ':' rest
          _ => show s
+  show (Number x) = show x
+  show (Boolean True) = "true"
+  show (Boolean False) = "false"
+  show Nil = "nil"
   show (Quasiquote x) = "(quasiquote " ++ show x ++ ")"
   show (Quote x) = "(quote " ++ show x ++ ")"
   show (Unquote x) = "(unquote " ++ show x ++ ")"
   show (SpliceUnquote x) = "(splice-unquote " ++ show x ++ ")"
   show (Deref x) = "(deref " ++ show x ++ ")"
   show (WithMeta a b) = "(with-meta " ++ show a ++ " " ++ show b ++ ")"
-  show (Number x) = show x
   show (List xs) = "(" ++ unwords (map show xs) ++ ")"
   show (Vector xs) = "[" ++ unwords (map show xs) ++ "]"
   show (Map m) = "{" ++ unwords (concatMap (\(a, b) => [show (Str a), show b]) $ toList m) ++ "}"
   show (Func f) = "<function>"
 
 public export
-interface MalType a where
-  toMalAst : a -> AST
-  fromMalAst : AST -> Maybe a
-
-public export
-implementation MalType AST where
-  toMalAst = id
-  fromMalAst = Just
-
-public export
-implementation MalType Integer where
-  toMalAst = Number
-  fromMalAst (Number x) = Just x
-  fromMalAst _ = Nothing
-
-public export
-implementation MalType String where
-  toMalAst = Str
-  fromMalAst (Str s) = Just s
-  fromMalAst _ = Nothing
-
-public export
-implementation MalType a => MalType (List a) where
-  toMalAst = Vector . map toMalAst -- Should this be List or Vector?
-  fromMalAst (List xs) = traverse fromMalAst xs
-  fromMalAst _ = Nothing
-
-public export
-implementation MalType a => MalType (SortedMap String a) where
-  toMalAst = Map . map toMalAst
-  fromMalAst (Map m) = traverse fromMalAst m
-  fromMalAst _ = Nothing
-
-public export
-interface MalFunction a where
-  toMalFunc : a -> List AST -> MalM AST
+getEnv : MalM (IORef (SortedMap String AST))
+getEnv = do
+  env <- ask
+  case env of
+       [] => throwError $ Str "Internal error: no environment"
+       e :: _ => pure e
 
 public export
-implementation MalType a => MalFunction a where
-  toMalFunc x [] = pure $ toMalAst x
-  toMalFunc _ _ = throwError $ Str "Too many arguments"
+withLocalEnv : MalM a -> MalM a
+withLocalEnv x = do
+  new <- liftIO $ newIORef empty
+  local (new::) x
 
 public export
-implementation MalType a => MalFunction (MalM a) where
-  toMalFunc x [] = map toMalAst x
-  toMalFunc _ _ = throwError $ Str "Too many arguments"
+insert : String -> AST -> MalM ()
+insert n x = do
+  env <- getEnv
+  liftIO $ modifyIORef env $ insert n x
 
 public export
-implementation (MalType a, MalFunction b) => MalFunction (a -> b) where
-  toMalFunc _ [] = throwError $ Str "Too few arguments"
-  toMalFunc f (x::xs) = case fromMalAst x of
-                             Just x' => toMalFunc (f x') xs
-                             Nothing => throwError $ Str "Wrong argument type"
+lookup : String -> MalM AST
+lookup n = ask >>= go
+  where go : Env -> MalM AST
+        go [] = throwError $ Str $ "Symbol " ++ 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/step2_eval.idr b/impls/idris2/step2_eval.idr
index 9dba1ccdb7..3f7e43c09c 100644
--- a/impls/idris2/step2_eval.idr
+++ b/impls/idris2/step2_eval.idr
@@ -13,27 +13,27 @@ read s =
        Right _ => throwError $ Str "wack" -- too many ast's
        Left e => throwError $ Str $ "parse error: " ++ e
 
-runMalM : MalM () -> StateT Env IO ()
-runMalM x = ST $ \st => do
-  Left e <- runExceptT $ runStateT x st
-    | Right x => pure x
-  putStr "error: "
-  printLn e
-  pure ((), st)
+runMalM : MalM () -> ReaderT Env IO ()
+runMalM x = MkReaderT $ \r => do
+  Right x <- runExceptT $ runReaderT x r
+    | Left e => putStrLn $ "error: " ++ show e
+  pure x
 
-repl : a -> String -> (String -> StateT a IO ()) -> IO ()
-repl state prompt f = do
+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"
-  ((), state') <- runStateT (f input) state
-  repl state' prompt f
+  runReaderT (f input) r
+  repl r prompt f
 
 main : IO ()
-main = repl startingEnv "user> " $ \input => runMalM $ do
-  Just ast <- read input
-    | Nothing => pure ()
-  result <- eval ast
-  MonadTrans.liftIO $ printLn result
+main = do 
+  startingEnv <- getStartingEnv
+  repl startingEnv "user> " $ \input => runMalM $ do
+    Just ast <- read input
+      | Nothing => pure ()
+    result <- eval ast
+    MonadTrans.liftIO $ printLn result
diff --git a/impls/idris2/step3_env.idr b/impls/idris2/step3_env.idr
new file mode 100644
index 0000000000..3f7e43c09c
--- /dev/null
+++ b/impls/idris2/step3_env.idr
@@ -0,0 +1,39 @@
+import System.File
+
+import Types
+import MonadTrans
+import Reader
+import Eval
+
+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 => putStrLn $ "error: " ++ show e
+  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
+    MonadTrans.liftIO $ printLn result

From 92f4b302fdc21b83b670cdb12ff32f25420304ed Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Tue, 30 Jun 2020 21:03:22 -0400
Subject: [PATCH 04/17] Idris2: step 4

---
 impls/idris2/Core.idr           | 217 ++++++++++++++++++++++++++++++++
 impls/idris2/Eval.idr           | 114 +----------------
 impls/idris2/Makefile           |   4 +-
 impls/idris2/Reader.idr         |   4 +-
 impls/idris2/Types.idr          |  77 ++++++++----
 impls/idris2/step2_eval.idr     |   1 +
 impls/idris2/step3_env.idr      |   1 +
 impls/idris2/step4_if_fn_do.idr |  40 ++++++
 8 files changed, 319 insertions(+), 139 deletions(-)
 create mode 100644 impls/idris2/Core.idr
 create mode 100644 impls/idris2/step4_if_fn_do.idr

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
new file mode 100644
index 0000000000..df35a7148c
--- /dev/null
+++ b/impls/idris2/Core.idr
@@ -0,0 +1,217 @@
+module Core
+
+import Control.Monad.Syntax
+import Data.List
+import Data.Strings
+import Eval
+import Reader
+import Types
+
+-- Builtins
+interface MalType a where
+  toMalAst : a -> AST
+  fromMalAst : AST -> Maybe a
+
+implementation MalType AST where
+  toMalAst = id
+  fromMalAst = Just
+
+implementation MalType () where
+  toMalAst () = Nil
+  fromMalAst Nil = Just ()
+  fromMalAst _ = Nothing
+
+implementation MalType Integer where
+  toMalAst = Number
+  fromMalAst (Number x) = Just x
+  fromMalAst _ = Nothing
+
+implementation MalType Int where
+  toMalAst = Number . cast
+  fromMalAst (Number x) = Just $ cast x
+  fromMalAst _ = Nothing
+
+implementation MalType String where
+  toMalAst = Str
+  fromMalAst (Str s) = Just s
+  fromMalAst _ = Nothing
+
+implementation MalType Bool where
+  toMalAst = Boolean
+  fromMalAst (Boolean b) = Just b
+  fromMalAst _ = Nothing
+
+implementation MalType a => MalType (List a) where
+  toMalAst = List True . map toMalAst -- Should this be List or Vector?
+  fromMalAst (List _ xs) = traverse fromMalAst xs
+  fromMalAst Nil = Just []
+  fromMalAst _ = Nothing
+
+implementation MalType a => MalType (SortedMap String a) where
+  toMalAst = Map . map toMalAst
+  fromMalAst (Map m) = traverse fromMalAst m
+  fromMalAst _ = Nothing
+
+interface MalFunction a where
+  toMalFunc : a -> List AST -> MalM AST
+
+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"
+
+implementation MalType a => MalFunction (MalM a) where
+  toMalFunc x [] = map toMalAst x
+  toMalFunc _ xs = do
+    traverse eval xs
+    throwError $ Str "Too many arguments"
+
+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
+
+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"
+
+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 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 $ \args => do
+    args' <- traverse eval args
+    local (const parentEnv) $ withLocalEnv $ do
+      bindArgs argNames' args'
+      eval 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"
+
+isList : AST -> Bool
+isList (List False _) = True
+isList _ = False
+
+isVector : AST -> Bool
+isVector (List True _) = True
+isVector _ = False
+
+-- Specialized on MalM to help type inference
+liftIO' : MalType a => IO a -> MalM AST
+liftIO' = map toMalAst . MonadTrans.liftIO
+
+prStr : List AST -> MalM AST
+prStr xs = do
+  xs' <- traverse eval xs
+  pure $ Str $ fastAppend $ intersperse " " $ map (toString True) xs'
+str : List AST -> MalM AST
+str xs = do
+  xs' <- traverse eval xs
+  pure $ Str $ fastAppend $ map (toString False) xs'
+prn : List AST -> MalM AST
+prn xs = do
+  xs' <- traverse eval xs
+  liftIO' $ putStrLn $ fastAppend $ intersperse " " $ map (toString True) xs'
+println : List AST -> MalM AST
+println xs = do
+  xs' <- traverse eval xs
+  liftIO' $ putStrLn $ fastAppend $ intersperse " " $ map (toString False) xs'
+
+baseEnv : SortedMap String AST
+baseEnv = fromList [
+  ("nil", Nil),
+  ("true", Boolean True),
+  ("false", Boolean False),
+  ("+", Func $ toMalFunc $ (+) {ty=Integer}),
+  ("-", Func $ toMalFunc $ (-) {ty=Integer}),
+  ("*", Func $ toMalFunc $ (*) {ty=Integer}),
+  ("/", Func $ toMalFunc $ div {ty=Integer}),
+  ("def!", Func defBuiltin),
+  ("let*", Func letBuiltin),
+  ("if", Func ifBuiltin),
+  ("fn*", Func fnBuiltin),
+  ("do", Func doBuiltin),
+  ("list", Func $ map (List False) . traverse eval),
+  ("list?", Func $ toMalFunc isList),
+  ("vector", Func $ map (List True) . traverse eval),
+  ("vector?", Func $ toMalFunc isVector),
+  ("count", Func $ toMalFunc $ the (List AST -> Integer) $ cast . List.length),
+  ("=", Func $ toMalFunc $ (==) {ty=AST}),
+  (">", Func $ toMalFunc $ (>) {ty=Integer}),
+  (">=", Func $ toMalFunc $ (>=) {ty=Integer}),
+  ("<", Func $ toMalFunc $ (<) {ty=Integer}),
+  ("<=", Func $ toMalFunc $ (<=) {ty=Integer}),
+  -- TODO: implement in corelib when varargs is done
+  ("pr-str", Func prStr),
+  ("str", Func str),
+  ("prn", Func prn),
+  ("println", Func println)
+]
+
+coreLib : String
+coreLib = "
+(def! empty? (fn* (l) (= (count l) 0)))
+(def! not (fn* (a) (if a false true)))
+"
+
+public export
+getStartingEnv : IO Env
+getStartingEnv = do
+  env <- map pure $ newIORef baseEnv
+  res <- runExceptT $ flip runReaderT env $ do
+    defs <- either (throwError . Str . ("parse error: "++)) pure $ parseText coreLib
+    traverse_ eval defs
+  case res of
+       Right () => pure ()
+       Left e => putStrLn $ "CORELIB: error: " ++ toString False e
+  pure env
diff --git a/impls/idris2/Eval.idr b/impls/idris2/Eval.idr
index c2efba9da0..80c5570f16 100644
--- a/impls/idris2/Eval.idr
+++ b/impls/idris2/Eval.idr
@@ -2,6 +2,7 @@ module Eval
 
 import Types
 import MonadTrans
+import Data.List
 
 public export
 eval : AST -> MalM AST
@@ -16,118 +17,11 @@ eval (Unquote x) = pure x -- TODO
 eval (SpliceUnquote x) = pure x -- TODO
 eval (Deref x) = pure x -- TODO
 eval (WithMeta a b) = pure $ WithMeta a b -- TODO
-eval (List []) = pure $ List []
-eval (List (f::xs)) = do
+eval (List False []) = pure $ List False []
+eval (List False (f::xs)) = do
   Func f' <- eval f
     | _ => throwError $ Str "tried to call something that's not a function"
   f' xs
-eval (Vector xs) = map Vector $ traverse eval xs
+eval (List True xs) = map (List True) $ traverse eval xs
 eval (Map m) = map Map $ traverse eval m
 eval (Func f) = pure $ Func f
-
--- Builtins
-public export
-interface MalType a where
-  toMalAst : a -> AST
-  fromMalAst : AST -> Maybe a
-
-public export
-implementation MalType AST where
-  toMalAst = id
-  fromMalAst = Just
-
-public export
-implementation MalType Integer where
-  toMalAst = Number
-  fromMalAst (Number x) = Just x
-  fromMalAst _ = Nothing
-
-public export
-implementation MalType String where
-  toMalAst = Str
-  fromMalAst (Str s) = Just s
-  fromMalAst _ = Nothing
-
-public export
-implementation MalType a => MalType (List a) where
-  toMalAst = Vector . map toMalAst -- Should this be List or Vector?
-  fromMalAst (List xs) = traverse fromMalAst xs
-  fromMalAst _ = Nothing
-
-public export
-implementation MalType a => MalType (SortedMap String a) where
-  toMalAst = Map . map toMalAst
-  fromMalAst (Map m) = traverse fromMalAst m
-  fromMalAst _ = Nothing
-
-public export
-interface MalFunction a where
-  toMalFunc : a -> List AST -> MalM AST
-
-public 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"
-
-public export
-implementation MalType a => MalFunction (MalM a) where
-  toMalFunc x [] = map toMalAst x
-  toMalFunc _ xs = do
-    traverse eval xs
-    throwError $ Str "Too many arguments"
-
-public 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
-
-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"
-
-letBuiltin : List AST -> MalM AST
-letBuiltin [] = throwError $ Str "let*: too few arguments"
-letBuiltin [_] = throwError $ Str "let*: too few arguments"
-letBuiltin [defs, ans] = do
-  defs' <- the (MalM _) $ case defs of
-    List xs => pure xs
-    Vector xs => pure xs
-    _ => throwError $ Str "let*: expecting vector or list"
-  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*: too many arguments"
-
-public export
-getStartingEnv : IO Env
-getStartingEnv = map pure $ newIORef startingEnv
-  where
-    startingEnv : SortedMap String AST
-    startingEnv = fromList [
-      ("nil", Nil),
-      ("true", Boolean True),
-      ("false", Boolean True),
-      ("+", Func $ toMalFunc ((+) {ty=Integer})),
-      ("-", Func $ toMalFunc ((-) {ty=Integer})),
-      ("*", Func $ toMalFunc ((*) {ty=Integer})),
-      ("/", Func $ toMalFunc (div {ty=Integer})),
-      ("def!", Func defBuiltin),
-      ("let*", Func letBuiltin)
-    ]
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index be85bffc00..45bee92a5f 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,5 +1,5 @@
-SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr step3_env.idr
-OTHER_SRCS = Types.idr Reader.idr Eval.idr MonadTrans.idr
+SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr step3_env.idr step4_if_fn_do.idr
+OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
 idris_args = -p contrib
diff --git a/impls/idris2/Reader.idr b/impls/idris2/Reader.idr
index b7d33266d5..e633f7ebba 100644
--- a/impls/idris2/Reader.idr
+++ b/impls/idris2/Reader.idr
@@ -103,10 +103,10 @@ mutual
   stringGrammar = match TString <|> map (strCons '\xff') (match TKeyword)
 
   listGrammar : Parser AST
-  listGrammar = match TOpenParen *> map List (many grammar) <* match TCloseParen
+  listGrammar = match TOpenParen *> map (List False) (many grammar) <* match TCloseParen
 
   vectorGrammar : Parser AST
-  vectorGrammar = match TOpenBracket *> map Vector (many grammar) <* match TCloseBracket
+  vectorGrammar = match TOpenBracket *> map (List True) (many grammar) <* match TCloseBracket
 
   mapGrammar : Parser AST
   mapGrammar = match TOpenBrace *> map (Map . fromList) contents <* match TCloseBrace
diff --git a/impls/idris2/Types.idr b/impls/idris2/Types.idr
index a0b8f7e5eb..7c01aab220 100644
--- a/impls/idris2/Types.idr
+++ b/impls/idris2/Types.idr
@@ -19,8 +19,7 @@ mutual
            | SpliceUnquote AST
            | Deref AST
            | WithMeta AST AST
-           | List (List AST)
-           | Vector (List AST)
+           | List Bool (List AST) -- List False -> List, List True -> Vector
            | Map (SortedMap String AST)
            | Func (List AST -> MalM AST)
 
@@ -32,29 +31,57 @@ mutual
   MalM : Type -> Type
   MalM = ReaderT Env (ExceptT AST IO)
 
+export
+toString : (readably : Bool) -> AST -> String
+toString b (Symbol s) = s
+toString b (Str s) =
+  case strUncons s of
+       Just ('\xff', rest) => strCons ':' rest
+       _ => if b then show s else s
+toString b (Number x) = show x
+toString b (Boolean True) = "true"
+toString b (Boolean False) = "false"
+toString b Nil = "nil"
+toString b (Quasiquote x) = "(quasiquote " ++ toString b x ++ ")"
+toString b (Quote x) = "(quote " ++ toString b x ++ ")"
+toString b (Unquote x) = "(unquote " ++ toString b x ++ ")"
+toString b (SpliceUnquote x) = "(splice-unquote " ++ toString b x ++ ")"
+toString b (Deref x) = "(deref " ++ toString b x ++ ")"
+toString b (WithMeta x y) = "(with-meta " ++ toString b x ++ " " ++ toString b y ++ ")"
+toString b (List False xs) = "(" ++ unwords (map (toString b) xs) ++ ")"
+toString b (List True xs) = "[" ++ unwords (map (toString b) xs) ++ "]"
+toString b (Map m) = "{" ++ unwords (concatMap (\(x, y) => [toString b (Str x), toString b y]) $ toList m) ++ "}"
+toString b (Func f) = "#<function>"
+
 export
 implementation Show AST where
-  show (Symbol s) = s
-  show (Str s) =
-    case strUncons s of
-         Just ('\xff', rest) => strCons ':' rest
-         _ => show s
-  show (Number x) = show x
-  show (Boolean True) = "true"
-  show (Boolean False) = "false"
-  show Nil = "nil"
-  show (Quasiquote x) = "(quasiquote " ++ show x ++ ")"
-  show (Quote x) = "(quote " ++ show x ++ ")"
-  show (Unquote x) = "(unquote " ++ show x ++ ")"
-  show (SpliceUnquote x) = "(splice-unquote " ++ show x ++ ")"
-  show (Deref x) = "(deref " ++ show x ++ ")"
-  show (WithMeta a b) = "(with-meta " ++ show a ++ " " ++ show b ++ ")"
-  show (List xs) = "(" ++ unwords (map show xs) ++ ")"
-  show (Vector xs) = "[" ++ unwords (map show xs) ++ "]"
-  show (Map m) = "{" ++ unwords (concatMap (\(a, b) => [show (Str a), show b]) $ toList m) ++ "}"
-  show (Func f) = "<function>"
+  show = toString True
+
+export
+implementation Eq AST where
+  Symbol x == Symbol y = x == y
+  Str x == Str y = x == y
+  Number x == Number y = x == y
+  Boolean x == Boolean y = x == y
+  Nil == Nil = True
+  Quasiquote x == Quasiquote y = x == y
+  Quote x == Quote y = x == y
+  Unquote x == Unquote y = x == y
+  SpliceUnquote x == SpliceUnquote y = x == y
+  Deref x == Deref y = x == y
+  WithMeta a b == WithMeta x y = a == x && b == y
+  List _ x == List _ y = x == y
+  Map x == Map y = toList x == toList y
+  Func _ == Func _ = False
+  _ == _ = False
+ 
+export
+truthiness : AST -> Bool
+truthiness Nil = False
+truthiness (Boolean False) = False
+truthiness _ = True
 
-public export
+export
 getEnv : MalM (IORef (SortedMap String AST))
 getEnv = do
   env <- ask
@@ -62,19 +89,19 @@ getEnv = do
        [] => throwError $ Str "Internal error: no environment"
        e :: _ => pure e
 
-public export
+export
 withLocalEnv : MalM a -> MalM a
 withLocalEnv x = do
   new <- liftIO $ newIORef empty
   local (new::) x
 
-public export
+export
 insert : String -> AST -> MalM ()
 insert n x = do
   env <- getEnv
   liftIO $ modifyIORef env $ insert n x
 
-public export
+export
 lookup : String -> MalM AST
 lookup n = ask >>= go
   where go : Env -> MalM AST
diff --git a/impls/idris2/step2_eval.idr b/impls/idris2/step2_eval.idr
index 3f7e43c09c..f1589e7061 100644
--- a/impls/idris2/step2_eval.idr
+++ b/impls/idris2/step2_eval.idr
@@ -4,6 +4,7 @@ import Types
 import MonadTrans
 import Reader
 import Eval
+import Core
 
 read : String -> MalM (Maybe AST)
 read s =
diff --git a/impls/idris2/step3_env.idr b/impls/idris2/step3_env.idr
index 3f7e43c09c..f1589e7061 100644
--- a/impls/idris2/step3_env.idr
+++ b/impls/idris2/step3_env.idr
@@ -4,6 +4,7 @@ import Types
 import MonadTrans
 import Reader
 import Eval
+import Core
 
 read : String -> MalM (Maybe AST)
 read s =
diff --git a/impls/idris2/step4_if_fn_do.idr b/impls/idris2/step4_if_fn_do.idr
new file mode 100644
index 0000000000..f1589e7061
--- /dev/null
+++ b/impls/idris2/step4_if_fn_do.idr
@@ -0,0 +1,40 @@
+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 => putStrLn $ "error: " ++ show e
+  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
+    MonadTrans.liftIO $ printLn result

From 91c6e70d9ff7385e4d496c3c7e15d1f8057fb4cf Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Tue, 30 Jun 2020 21:12:26 -0400
Subject: [PATCH 05/17] Idris2: step 5 -- hell yeah TCO already works

---
 impls/idris2/Makefile      |  3 ++-
 impls/idris2/step5_tco.idr | 40 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 impls/idris2/step5_tco.idr

diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index 45bee92a5f..747d276735 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,4 +1,5 @@
-SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr step3_env.idr step4_if_fn_do.idr
+SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr step3_env.idr \
+	   step4_if_fn_do.idr step5_tco.idr
 OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
diff --git a/impls/idris2/step5_tco.idr b/impls/idris2/step5_tco.idr
new file mode 100644
index 0000000000..f1589e7061
--- /dev/null
+++ b/impls/idris2/step5_tco.idr
@@ -0,0 +1,40 @@
+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 => putStrLn $ "error: " ++ show e
+  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
+    MonadTrans.liftIO $ printLn result

From 15572cf2164470c2f92135057c73eb1c2681606a Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Wed, 1 Jul 2020 01:25:24 -0400
Subject: [PATCH 06/17] Idris2: step 6

---
 impls/idris2/Core.idr             | 109 +++++++++++++++++++++++-------
 impls/idris2/Eval.idr             |   8 +--
 impls/idris2/Makefile             |   2 +-
 impls/idris2/Reader.idr           |  10 +--
 impls/idris2/Types.idr            |  92 ++++++++++++++-----------
 impls/idris2/step1_read_print.idr |   3 +-
 impls/idris2/step2_eval.idr       |   7 +-
 impls/idris2/step3_env.idr        |  41 +----------
 impls/idris2/step4_if_fn_do.idr   |  41 +----------
 impls/idris2/step5_tco.idr        |  41 +----------
 impls/idris2/step6_file.idr       |  51 ++++++++++++++
 11 files changed, 205 insertions(+), 200 deletions(-)
 mode change 100644 => 120000 impls/idris2/step3_env.idr
 mode change 100644 => 120000 impls/idris2/step4_if_fn_do.idr
 mode change 100644 => 120000 impls/idris2/step5_tco.idr
 create mode 100644 impls/idris2/step6_file.idr

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
index df35a7148c..6119253805 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -3,6 +3,9 @@ module Core
 import Control.Monad.Syntax
 import Data.List
 import Data.Strings
+import System
+import System.File
+
 import Eval
 import Reader
 import Types
@@ -17,8 +20,8 @@ implementation MalType AST where
   fromMalAst = Just
 
 implementation MalType () where
-  toMalAst () = Nil
-  fromMalAst Nil = Just ()
+  toMalAst () = Symbol "nil"
+  fromMalAst (Symbol "nil") = Just ()
   fromMalAst _ = Nothing
 
 implementation MalType Integer where
@@ -37,14 +40,22 @@ implementation MalType String where
   fromMalAst _ = Nothing
 
 implementation MalType Bool where
-  toMalAst = Boolean
-  fromMalAst (Boolean b) = Just b
+  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
+
+implementation MalType (IORef AST) where
+  toMalAst = Atom
+  fromMalAst (Atom a) = Just a
   fromMalAst _ = Nothing
 
 implementation MalType a => MalType (List a) where
   toMalAst = List True . map toMalAst -- Should this be List or Vector?
   fromMalAst (List _ xs) = traverse fromMalAst xs
-  fromMalAst Nil = Just []
+  fromMalAst (Symbol "nil") = Just []
   fromMalAst _ = Nothing
 
 implementation MalType a => MalType (SortedMap String a) where
@@ -74,6 +85,10 @@ implementation (MalType a, MalFunction b) => MalFunction (a -> b) where
       | Nothing => traverse_ eval xs *> throwError (Str "Wrong argument type")
     toMalFunc (f x') xs
 
+-- Specialized on MalM to help type inference
+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"
@@ -110,7 +125,7 @@ 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 Nil
+  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
@@ -138,40 +153,68 @@ fnBuiltin [List _ argNames, res] = do
           bindArgs ns xs
 fnBuiltin _ = throwError $ Str "fn: malformed arguments"
 
-isList : AST -> Bool
-isList (List False _) = True
-isList _ = False
+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
 
-isVector : AST -> Bool
-isVector (List True _) = True
-isVector _ = False
+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
 
--- Specialized on MalM to help type inference
-liftIO' : MalType a => IO a -> MalM AST
-liftIO' = map toMalAst . MonadTrans.liftIO
+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 xs = do
+  Atom x::Func f::args <- traverse eval xs
+    | _ => throwError $ Str "swap!: type error"
+  old <- liftIO $ readIORef x
+  new <- f (old::args)
+  resetBuiltin x new
 
 prStr : List AST -> MalM AST
 prStr xs = do
   xs' <- traverse eval xs
-  pure $ Str $ fastAppend $ intersperse " " $ map (toString True) xs'
+  sxs <- liftIO $ traverse (toString True) xs'
+  pure $ Str $ fastAppend $ intersperse " " sxs
 str : List AST -> MalM AST
 str xs = do
   xs' <- traverse eval xs
-  pure $ Str $ fastAppend $ map (toString False) xs'
+  sxs <- liftIO $ traverse (toString False) xs'
+  pure $ Str $ fastAppend sxs
 prn : List AST -> MalM AST
 prn xs = do
   xs' <- traverse eval xs
-  liftIO' $ putStrLn $ fastAppend $ intersperse " " $ map (toString True) xs'
+  sxs <- liftIO $ traverse (toString True) xs'
+  liftIO' $ putStrLn $ fastAppend $ intersperse " " sxs
 println : List AST -> MalM AST
 println xs = do
   xs' <- traverse eval xs
-  liftIO' $ putStrLn $ fastAppend $ intersperse " " $ map (toString False) xs'
+  sxs <- liftIO $ traverse (toString False) xs'
+  liftIO' $ putStrLn $ fastAppend $ intersperse " " sxs
 
 baseEnv : SortedMap String AST
 baseEnv = fromList [
-  ("nil", Nil),
-  ("true", Boolean True),
-  ("false", Boolean False),
+  ("nil", Symbol "nil"),
+  ("true", Symbol "true"),
+  ("false", Symbol "false"),
   ("+", Func $ toMalFunc $ (+) {ty=Integer}),
   ("-", Func $ toMalFunc $ (-) {ty=Integer}),
   ("*", Func $ toMalFunc $ (*) {ty=Integer}),
@@ -195,23 +238,39 @@ baseEnv = fromList [
   ("pr-str", Func prStr),
   ("str", Func str),
   ("prn", Func prn),
-  ("println", Func println)
+  ("println", Func println),
+  ("read-string", Func $ toMalFunc readStringBuiltin),
+  ("slurp", Func $ toMalFunc slurpBuiltin),
+  ("eval", Func $ toMalFunc $ withGlobalEnv . eval),
+  ("atom", Func $ toMalFunc atomBuiltin),
+  ("atom?", Func $ toMalFunc isAtom),
+  ("deref", Func $ toMalFunc derefBuiltin),
+  ("reset!", Func $ toMalFunc resetBuiltin),
+  ("swap!", Func swapBuiltin)
 ]
 
 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)\")))))
 "
 
 public export
 getStartingEnv : IO Env
 getStartingEnv = do
-  env <- map pure $ newIORef baseEnv
+  args <- getArgs
+  let argv =
+    case args of
+         (_::_::rest) => List False $ map Str rest
+         _ => List False []
+  env <- map pure $ newIORef $ insert "*ARGV*" argv baseEnv
   res <- runExceptT $ flip runReaderT env $ do
     defs <- either (throwError . Str . ("parse error: "++)) pure $ parseText coreLib
     traverse_ eval defs
   case res of
        Right () => pure ()
-       Left e => putStrLn $ "CORELIB: error: " ++ toString False e
+       Left e => do
+         se <- toString False e
+         putStrLn $ "CORELIB: error: " ++ se
   pure env
diff --git a/impls/idris2/Eval.idr b/impls/idris2/Eval.idr
index 80c5570f16..6137e4f64f 100644
--- a/impls/idris2/Eval.idr
+++ b/impls/idris2/Eval.idr
@@ -9,13 +9,7 @@ eval : AST -> MalM AST
 eval (Symbol n) = lookup n
 eval (Str s) = pure $ Str s
 eval (Number x) = pure $ Number x
-eval (Boolean b) = pure $ Boolean b
-eval Nil = pure Nil
-eval (Quasiquote x) = pure x -- TODO
-eval (Quote x) = pure x -- TODO
-eval (Unquote x) = pure x -- TODO
-eval (SpliceUnquote x) = pure x -- TODO
-eval (Deref x) = pure x -- TODO
+eval (Atom e) = pure $ Atom e
 eval (WithMeta a b) = pure $ WithMeta a b -- TODO
 eval (List False []) = pure $ List False []
 eval (List False (f::xs)) = do
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index 747d276735..4b1cb0c704 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,5 +1,5 @@
 SRCS = step0_repl.idr step1_read_print.idr step2_eval.idr step3_env.idr \
-	   step4_if_fn_do.idr step5_tco.idr
+	   step4_if_fn_do.idr step5_tco.idr step6_file.idr
 OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
diff --git a/impls/idris2/Reader.idr b/impls/idris2/Reader.idr
index e633f7ebba..8442ad8d70 100644
--- a/impls/idris2/Reader.idr
+++ b/impls/idris2/Reader.idr
@@ -117,11 +117,11 @@ mutual
   sigilGrammar = assert_total $ match TSigil >>= sigilAction
     where partial
           sigilAction : String -> Parser AST
-          sigilAction "~@" = map SpliceUnquote grammar
-          sigilAction "'" = map Quote grammar
-          sigilAction "`" = map Quasiquote grammar
-          sigilAction "~" = map Unquote grammar
-          sigilAction "@" = map Deref grammar
+          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 "^" = flip WithMeta <$> grammar <*> grammar
 
   grammar : Parser AST
diff --git a/impls/idris2/Types.idr b/impls/idris2/Types.idr
index 7c01aab220..d233045069 100644
--- a/impls/idris2/Types.idr
+++ b/impls/idris2/Types.idr
@@ -2,6 +2,7 @@ module Types
 
 import Control.Monad.State
 import public Data.IORef
+import Data.List
 import public Data.SortedMap
 import Data.Strings
 import public MonadTrans
@@ -11,13 +12,7 @@ mutual
   data AST = Symbol String -- Identifiers
            | Str String -- Includes keywords
            | Number Integer
-           | Boolean Bool
-           | Nil
-           | Quasiquote AST
-           | Quote AST
-           | Unquote AST
-           | SpliceUnquote AST
-           | Deref AST
+           | Atom (IORef AST)
            | WithMeta AST AST
            | List Bool (List AST) -- List False -> List, List True -> Vector
            | Map (SortedMap String AST)
@@ -32,55 +27,66 @@ mutual
   MalM = ReaderT Env (ExceptT AST IO)
 
 export
-toString : (readably : Bool) -> AST -> String
-toString b (Symbol s) = s
+toString : (readably : Bool) -> AST -> IO String
+toString b (Symbol s) = pure s
 toString b (Str s) =
   case strUncons s of
-       Just ('\xff', rest) => strCons ':' rest
-       _ => if b then show s else s
-toString b (Number x) = show x
-toString b (Boolean True) = "true"
-toString b (Boolean False) = "false"
-toString b Nil = "nil"
-toString b (Quasiquote x) = "(quasiquote " ++ toString b x ++ ")"
-toString b (Quote x) = "(quote " ++ toString b x ++ ")"
-toString b (Unquote x) = "(unquote " ++ toString b x ++ ")"
-toString b (SpliceUnquote x) = "(splice-unquote " ++ toString b x ++ ")"
-toString b (Deref x) = "(deref " ++ toString b x ++ ")"
-toString b (WithMeta x y) = "(with-meta " ++ toString b x ++ " " ++ toString b y ++ ")"
-toString b (List False xs) = "(" ++ unwords (map (toString b) xs) ++ ")"
-toString b (List True xs) = "[" ++ unwords (map (toString b) xs) ++ "]"
-toString b (Map m) = "{" ++ unwords (concatMap (\(x, y) => [toString b (Str x), toString b y]) $ toList m) ++ "}"
-toString b (Func f) = "#<function>"
-
-export
-implementation Show AST where
-  show = toString True
+       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 (WithMeta x y) = do
+  sx <- toString b x
+  sy <- toString b y
+  pure $ "(with-meta " ++ sx ++ " " ++ sy ++ ")"
+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 f) = pure "#<function>"
 
 export
 implementation Eq AST where
   Symbol x == Symbol y = x == y
   Str x == Str y = x == y
   Number x == Number y = x == y
-  Boolean x == Boolean y = x == y
-  Nil == Nil = True
-  Quasiquote x == Quasiquote y = x == y
-  Quote x == Quote y = x == y
-  Unquote x == Unquote y = x == y
-  SpliceUnquote x == SpliceUnquote y = x == y
-  Deref x == Deref y = x == y
   WithMeta a b == WithMeta x y = a == x && b == y
   List _ x == List _ y = x == y
-  Map x == Map y = toList x == toList y
+  Map x == Map y = SortedMap.toList x == SortedMap.toList y
   Func _ == Func _ = False
   _ == _ = False
  
 export
 truthiness : AST -> Bool
-truthiness Nil = False
-truthiness (Boolean False) = False
+truthiness (Symbol "false") = False
+truthiness (Symbol "nil") = False
 truthiness _ = True
 
+export
+isList : AST -> Bool
+isList (List False _) = True
+isList _ = False
+
+export
+isVector : AST -> Bool
+isVector (List True _) = True
+isVector _ = False
+
+export
+isAtom : AST -> Bool
+isAtom (Atom _) = True
+isAtom _ = False
+
 export
 getEnv : MalM (IORef (SortedMap String AST))
 getEnv = do
@@ -95,6 +101,14 @@ withLocalEnv x = do
   new <- liftIO $ newIORef empty
   local (new::) x
 
+export
+withGlobalEnv : MalM a -> MalM a
+withGlobalEnv x = do
+  env <- ask
+  case last' env of
+       Just ge => local (const [ge]) x
+       Nothing => throwError $ Str "Internal error: no environment"
+
 export
 insert : String -> AST -> MalM ()
 insert n x = do
diff --git a/impls/idris2/step1_read_print.idr b/impls/idris2/step1_read_print.idr
index e7d9f3d8a5..188f078941 100644
--- a/impls/idris2/step1_read_print.idr
+++ b/impls/idris2/step1_read_print.idr
@@ -32,5 +32,6 @@ main = repl () "user> " $ \state, input => do
   Just ast <- read input
     | Nothing => pure ()
   result <- eval ast
-  printLn result
+  str <- toString True result
+  putStrLn str
   pure ()
diff --git a/impls/idris2/step2_eval.idr b/impls/idris2/step2_eval.idr
index f1589e7061..1a41b951be 100644
--- a/impls/idris2/step2_eval.idr
+++ b/impls/idris2/step2_eval.idr
@@ -17,7 +17,9 @@ read s =
 runMalM : MalM () -> ReaderT Env IO ()
 runMalM x = MkReaderT $ \r => do
   Right x <- runExceptT $ runReaderT x r
-    | Left e => putStrLn $ "error: " ++ show e
+    | Left e => do
+      se <- toString False e
+      putStrLn $ "error: " ++ se
   pure x
 
 repl : r -> String -> (String -> ReaderT r IO ()) -> IO ()
@@ -37,4 +39,5 @@ main = do
     Just ast <- read input
       | Nothing => pure ()
     result <- eval ast
-    MonadTrans.liftIO $ printLn result
+    str <- MonadTrans.liftIO $ toString True result
+    MonadTrans.liftIO $ putStrLn str
diff --git a/impls/idris2/step3_env.idr b/impls/idris2/step3_env.idr
deleted file mode 100644
index f1589e7061..0000000000
--- a/impls/idris2/step3_env.idr
+++ /dev/null
@@ -1,40 +0,0 @@
-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 => putStrLn $ "error: " ++ show e
-  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
-    MonadTrans.liftIO $ printLn result
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
deleted file mode 100644
index f1589e7061..0000000000
--- a/impls/idris2/step4_if_fn_do.idr
+++ /dev/null
@@ -1,40 +0,0 @@
-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 => putStrLn $ "error: " ++ show e
-  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
-    MonadTrans.liftIO $ printLn result
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
deleted file mode 100644
index f1589e7061..0000000000
--- a/impls/idris2/step5_tco.idr
+++ /dev/null
@@ -1,40 +0,0 @@
-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 => putStrLn $ "error: " ++ show e
-  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
-    MonadTrans.liftIO $ printLn result
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..4474604184
--- /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

From 68b75435a5979adfee73c7dab17c202433532cae Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Wed, 1 Jul 2020 02:18:22 -0400
Subject: [PATCH 07/17] Idris2: step 7

---
 impls/idris2/Core.idr        | 45 ++++++++++++++++++++++++++++++++++--
 impls/idris2/Makefile        |  2 +-
 impls/idris2/step7_quote.idr |  1 +
 3 files changed, 45 insertions(+), 3 deletions(-)
 create mode 120000 impls/idris2/step7_quote.idr

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
index 6119253805..6af229d8da 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -53,7 +53,7 @@ implementation MalType (IORef AST) where
   fromMalAst _ = Nothing
 
 implementation MalType a => MalType (List a) where
-  toMalAst = List True . map toMalAst -- Should this be List or Vector?
+  toMalAst = List False . map toMalAst
   fromMalAst (List _ xs) = traverse fromMalAst xs
   fromMalAst (Symbol "nil") = Just []
   fromMalAst _ = Nothing
@@ -189,6 +189,43 @@ swapBuiltin xs = do
   new <- f (old::args)
   resetBuiltin x new
 
+consBuiltin : AST -> List AST -> List AST
+consBuiltin = (::)
+
+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 (WithMeta a b) = pure $ WithMeta a b -- TODO
+        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 f) = pure $ Func f
+quasiquoteBuiltin _ = throwError $ Str "quote: wanted exactly one argument"
+
 prStr : List AST -> MalM AST
 prStr xs = do
   xs' <- traverse eval xs
@@ -246,7 +283,11 @@ baseEnv = fromList [
   ("atom?", Func $ toMalFunc isAtom),
   ("deref", Func $ toMalFunc derefBuiltin),
   ("reset!", Func $ toMalFunc resetBuiltin),
-  ("swap!", Func swapBuiltin)
+  ("swap!", Func swapBuiltin),
+  ("cons", Func $ toMalFunc consBuiltin),
+  ("concat", Func concatBuiltin),
+  ("quote", Func quoteBuiltin),
+  ("quasiquote", Func quasiquoteBuiltin)
 ]
 
 coreLib : String
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index 4b1cb0c704..49c0fedc0d 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,5 +1,5 @@
 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
+	   step4_if_fn_do.idr step5_tco.idr step6_file.idr step7_quote.idr
 OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
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

From 9866462fba7c590df90c8daa3cdceed05b107588 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Wed, 1 Jul 2020 15:16:28 -0400
Subject: [PATCH 08/17] Idris2: step 8

---
 impls/idris2/Core.idr         | 140 ++++++++++++++++++++++++----------
 impls/idris2/Eval.idr         |  47 +++++++++---
 impls/idris2/Makefile         |   3 +-
 impls/idris2/Types.idr        |  26 ++++---
 impls/idris2/step8_macros.idr |   1 +
 5 files changed, 152 insertions(+), 65 deletions(-)
 create mode 120000 impls/idris2/step8_macros.idr

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
index 6af229d8da..ac5dd3c80e 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -34,6 +34,14 @@ implementation MalType Int where
   fromMalAst (Number x) = Just $ cast x
   fromMalAst _ = Nothing
 
+implementation MalType Nat where
+  toMalAst = Number . cast
+  fromMalAst (Number x) = toNat x 0
+    where toNat : Integer -> Nat -> Maybe Nat
+          toNat 0 acc = Just acc
+          toNat n acc = if n < 0 then Nothing else toNat (n - 1) (S acc)
+  fromMalAst _ = Nothing
+
 implementation MalType String where
   toMalAst = Str
   fromMalAst (Str s) = Just s
@@ -99,6 +107,20 @@ defBuiltin [Symbol n, x] = do
 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"
+  -- Really wish it was fn* and macro*, not def! and defmacro!, so it would be
+  -- possible to use native functions without hacky quoting or a is_macro flag
+  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"
@@ -135,11 +157,14 @@ fnBuiltin : List AST -> MalM AST
 fnBuiltin [List _ argNames, res] = do
   argNames' <- traverse getSymbol argNames
   parentEnv <- ask
-  pure $ Func $ \args => do
+  pure $ Func False $ \args => do
     args' <- traverse eval args
     local (const parentEnv) $ withLocalEnv $ do
       bindArgs argNames' args'
-      eval res
+      -- 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"
@@ -183,7 +208,7 @@ swapBuiltin : List AST -> MalM AST
 swapBuiltin [] = throwError $ Str "swap!: too few arguments"
 swapBuiltin [_] = throwError $ Str "swap!: too few arguments"
 swapBuiltin xs = do
-  Atom x::Func f::args <- traverse eval xs
+  Atom x::Func _ f::args <- traverse eval xs
     | _ => throwError $ Str "swap!: type error"
   old <- liftIO $ readIORef x
   new <- f (old::args)
@@ -192,6 +217,20 @@ swapBuiltin xs = do
 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
+
+-- TODO: move to corelib
+nthBuiltin : List AST -> Nat -> MalM AST
+nthBuiltin (x::_) 0 = pure x
+nthBuiltin (_::xs) (S n) = nthBuiltin xs n
+nthBuiltin [] _ = throwError $ Str "nth: index out of bounds"
+
 concatBuiltin : List AST -> MalM AST
 concatBuiltin = map (List False) . go <=< traverse eval
   where go : List AST -> MalM (List AST)
@@ -223,9 +262,13 @@ quasiquoteBuiltin [x] = qq x
           xs' <- traverse qq xs
           map (List False . concat) $ traverse expandSplice xs'
         qq (Map m) = map Map $ traverse qq m
-        qq (Func f) = pure $ Func f
+        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"
+
 prStr : List AST -> MalM AST
 prStr xs = do
   xs' <- traverse eval xs
@@ -252,42 +295,47 @@ baseEnv = fromList [
   ("nil", Symbol "nil"),
   ("true", Symbol "true"),
   ("false", Symbol "false"),
-  ("+", Func $ toMalFunc $ (+) {ty=Integer}),
-  ("-", Func $ toMalFunc $ (-) {ty=Integer}),
-  ("*", Func $ toMalFunc $ (*) {ty=Integer}),
-  ("/", Func $ toMalFunc $ div {ty=Integer}),
-  ("def!", Func defBuiltin),
-  ("let*", Func letBuiltin),
-  ("if", Func ifBuiltin),
-  ("fn*", Func fnBuiltin),
-  ("do", Func doBuiltin),
-  ("list", Func $ map (List False) . traverse eval),
-  ("list?", Func $ toMalFunc isList),
-  ("vector", Func $ map (List True) . traverse eval),
-  ("vector?", Func $ toMalFunc isVector),
-  ("count", Func $ toMalFunc $ the (List AST -> Integer) $ cast . List.length),
-  ("=", Func $ toMalFunc $ (==) {ty=AST}),
-  (">", Func $ toMalFunc $ (>) {ty=Integer}),
-  (">=", Func $ toMalFunc $ (>=) {ty=Integer}),
-  ("<", Func $ toMalFunc $ (<) {ty=Integer}),
-  ("<=", Func $ toMalFunc $ (<=) {ty=Integer}),
-  -- TODO: implement in corelib when varargs is done
-  ("pr-str", Func prStr),
-  ("str", Func str),
-  ("prn", Func prn),
-  ("println", Func println),
-  ("read-string", Func $ toMalFunc readStringBuiltin),
-  ("slurp", Func $ toMalFunc slurpBuiltin),
-  ("eval", Func $ toMalFunc $ withGlobalEnv . eval),
-  ("atom", Func $ toMalFunc atomBuiltin),
-  ("atom?", Func $ toMalFunc isAtom),
-  ("deref", Func $ toMalFunc derefBuiltin),
-  ("reset!", Func $ toMalFunc resetBuiltin),
-  ("swap!", Func swapBuiltin),
-  ("cons", Func $ toMalFunc consBuiltin),
-  ("concat", Func concatBuiltin),
-  ("quote", Func quoteBuiltin),
-  ("quasiquote", Func quasiquoteBuiltin)
+  ("+", 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),
+  ("list?", Func False $ toMalFunc isList),
+  ("vector", Func False $ map (List True) . traverse eval),
+  ("vector?", Func False $ toMalFunc isVector),
+  ("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),
+  ("atom?", Func False $ toMalFunc isAtom),
+  ("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),
+  ("nth", Func False $ toMalFunc nthBuiltin),
+  ("quote", Func False quoteBuiltin),
+  ("quasiquote", Func False quasiquoteBuiltin),
+  ("macroexpand", Func False macroexpandBuiltin)
 ]
 
 coreLib : String
@@ -295,6 +343,16 @@ 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) 
+                  (nth xs 1)
+                  (throw \"odd number of forms to cond\"))
+              (cons 'cond (rest (rest xs)))
+        )
+  ))
+)
 "
 
 public export
@@ -305,7 +363,7 @@ getStartingEnv = do
     case args of
          (_::_::rest) => List False $ map Str rest
          _ => List False []
-  env <- map pure $ newIORef $ insert "*ARGV*" argv baseEnv
+  env <- map (\v => MkEnv fullEval [v]) $ newIORef $ insert "*ARGV*" argv baseEnv
   res <- runExceptT $ flip runReaderT env $ do
     defs <- either (throwError . Str . ("parse error: "++)) pure $ parseText coreLib
     traverse_ eval defs
diff --git a/impls/idris2/Eval.idr b/impls/idris2/Eval.idr
index 6137e4f64f..fd187c24f2 100644
--- a/impls/idris2/Eval.idr
+++ b/impls/idris2/Eval.idr
@@ -4,18 +4,41 @@ import Types
 import MonadTrans
 import Data.List
 
-public export
+-- Evaluate in the current eval mode.
+export
 eval : AST -> MalM AST
-eval (Symbol n) = lookup n
-eval (Str s) = pure $ Str s
-eval (Number x) = pure $ Number x
-eval (Atom e) = pure $ Atom e
-eval (WithMeta a b) = pure $ WithMeta a b -- TODO
-eval (List False []) = pure $ List False []
-eval (List False (f::xs)) = do
-  Func f' <- eval f
+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 (WithMeta a b) = pure $ WithMeta a b -- TODO
+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
-eval (List True xs) = map (List True) $ traverse eval xs
-eval (Map m) = map Map $ traverse eval m
-eval (Func f) = pure $ Func f
+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
index 49c0fedc0d..d983932865 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,5 +1,6 @@
 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
+	   step4_if_fn_do.idr step5_tco.idr step6_file.idr step7_quote.idr \
+	   step8_macros.idr
 OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
diff --git a/impls/idris2/Types.idr b/impls/idris2/Types.idr
index d233045069..eba35f11c5 100644
--- a/impls/idris2/Types.idr
+++ b/impls/idris2/Types.idr
@@ -16,11 +16,13 @@ mutual
            | WithMeta AST AST
            | List Bool (List AST) -- List False -> List, List True -> Vector
            | Map (SortedMap String AST)
-           | Func (List AST -> MalM AST)
+           | Func Bool (List AST -> MalM AST)
 
   public export
-  Env : Type
-  Env = List (IORef (SortedMap String AST))
+  record Env where
+    constructor MkEnv
+    evalFunc : AST -> MalM AST
+    symbols : List (IORef (SortedMap String AST))
 
   public export
   MalM : Type -> Type
@@ -53,7 +55,8 @@ toString b (Map m) = do
   pure $ "{" ++ unwords sm ++ "}"
   where onePair : (String, AST) -> IO (List String)
         onePair (k, v) = sequence [toString b (Str k), toString b v]
-toString b (Func f) = pure "#<function>"
+toString b (Func False f) = pure "#<function>"
+toString b (Func True f) = pure "#<macro>"
 
 export
 implementation Eq AST where
@@ -63,7 +66,7 @@ implementation Eq AST where
   WithMeta a b == WithMeta x y = a == x && b == y
   List _ x == List _ y = x == y
   Map x == Map y = SortedMap.toList x == SortedMap.toList y
-  Func _ == Func _ = False
+  Func _ _ == Func _ _ = False
   _ == _ = False
  
 export
@@ -90,7 +93,7 @@ isAtom _ = False
 export
 getEnv : MalM (IORef (SortedMap String AST))
 getEnv = do
-  env <- ask
+  env <- reader symbols
   case env of
        [] => throwError $ Str "Internal error: no environment"
        e :: _ => pure e
@@ -99,14 +102,15 @@ export
 withLocalEnv : MalM a -> MalM a
 withLocalEnv x = do
   new <- liftIO $ newIORef empty
-  local (new::) x
+  local (record {symbols $= (new::)}) x
 
 export
 withGlobalEnv : MalM a -> MalM a
 withGlobalEnv x = do
-  env <- ask
+  env <- reader symbols
+  evil <- reader evalFunc
   case last' env of
-       Just ge => local (const [ge]) x
+       Just ge => local (const $ MkEnv evil [ge]) x
        Nothing => throwError $ Str "Internal error: no environment"
 
 export
@@ -117,8 +121,8 @@ insert n x = do
 
 export
 lookup : String -> MalM AST
-lookup n = ask >>= go
-  where go : Env -> MalM AST
+lookup n = reader symbols >>= go
+  where go : List (IORef (SortedMap String AST)) -> MalM AST
         go [] = throwError $ Str $ "Symbol " ++ n ++ " not found"
         go (e::es) = do
           val <- map (lookup n) $ liftIO $ readIORef e
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

From d372d1a98c3c3c7c9cf4da3e4aca9c0109f8d886 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 01:00:57 -0400
Subject: [PATCH 09/17] Idris2: step 9

---
 impls/idris2/Core.idr       | 160 ++++++++++++++++++++++++++++--------
 impls/idris2/Makefile       |   2 +-
 impls/idris2/Types.idr      |  19 +----
 impls/idris2/step2_eval.idr |   2 +-
 impls/idris2/step6_file.idr |   2 +-
 impls/idris2/step9_try.idr  |   1 +
 6 files changed, 135 insertions(+), 51 deletions(-)
 create mode 120000 impls/idris2/step9_try.idr

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
index ac5dd3c80e..26abbdc138 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -2,6 +2,7 @@ module Core
 
 import Control.Monad.Syntax
 import Data.List
+import Data.Maybe
 import Data.Strings
 import System
 import System.File
@@ -29,19 +30,6 @@ implementation MalType Integer where
   fromMalAst (Number x) = Just x
   fromMalAst _ = Nothing
 
-implementation MalType Int where
-  toMalAst = Number . cast
-  fromMalAst (Number x) = Just $ cast x
-  fromMalAst _ = Nothing
-
-implementation MalType Nat where
-  toMalAst = Number . cast
-  fromMalAst (Number x) = toNat x 0
-    where toNat : Integer -> Nat -> Maybe Nat
-          toNat 0 acc = Just acc
-          toNat n acc = if n < 0 then Nothing else toNat (n - 1) (S acc)
-  fromMalAst _ = Nothing
-
 implementation MalType String where
   toMalAst = Str
   fromMalAst (Str s) = Just s
@@ -66,9 +54,10 @@ implementation MalType a => MalType (List a) where
   fromMalAst (Symbol "nil") = Just []
   fromMalAst _ = Nothing
 
-implementation MalType a => MalType (SortedMap String a) where
-  toMalAst = Map . map toMalAst
-  fromMalAst (Map m) = traverse fromMalAst m
+implementation MalType (SortedMap String AST) where
+  toMalAst = Map
+  fromMalAst (Map m) = Just m
+  fromMalAst (Symbol "nil") = Just empty
   fromMalAst _ = Nothing
 
 interface MalFunction a where
@@ -113,8 +102,6 @@ defmacroBuiltin [_] = throwError $ Str "defmacro!: too few arguments"
 defmacroBuiltin [Symbol n, x] = do
   Func _ m <- eval x
     | _ => throwError $ Str "defmacro!: expected a function"
-  -- Really wish it was fn* and macro*, not def! and defmacro!, so it would be
-  -- possible to use native functions without hacky quoting or a is_macro flag
   let m' = Func True $ eval <=< local (record { evalFunc = don'tEval }) . m
   insert n m'
   pure m'
@@ -225,12 +212,6 @@ restBuiltin : List AST -> List AST
 restBuiltin [] = []
 restBuiltin (_::xs) = xs
 
--- TODO: move to corelib
-nthBuiltin : List AST -> Nat -> MalM AST
-nthBuiltin (x::_) 0 = pure x
-nthBuiltin (_::xs) (S n) = nthBuiltin xs n
-nthBuiltin [] _ = throwError $ Str "nth: index out of bounds"
-
 concatBuiltin : List AST -> MalM AST
 concatBuiltin = map (List False) . go <=< traverse eval
   where go : List AST -> MalM (List AST)
@@ -269,6 +250,55 @@ 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 (WithMeta _ _) = Symbol "nil" -- TODO
+typeofBuiltin (List False _) = Keyword "list"
+typeofBuiltin (List True _) = Keyword "vector"
+typeofBuiltin (Map _) = Keyword "map"
+typeofBuiltin (Func False _) = Keyword "func"
+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
+
 prStr : List AST -> MalM AST
 prStr xs = do
   xs' <- traverse eval xs
@@ -306,9 +336,7 @@ baseEnv = fromList [
   ("fn*", Func False fnBuiltin),
   ("do", Func False doBuiltin),
   ("list", Func False $ map (List False) . traverse eval),
-  ("list?", Func False $ toMalFunc isList),
   ("vector", Func False $ map (List True) . traverse eval),
-  ("vector?", Func False $ toMalFunc isVector),
   ("count", Func False $ toMalFunc $ the (List AST -> Integer) $ cast . List.length),
   ("=", Func False $ toMalFunc $ (==) {ty=AST}),
   (">", Func False $ toMalFunc $ (>) {ty=Integer}),
@@ -324,7 +352,6 @@ baseEnv = fromList [
   ("slurp", Func False $ toMalFunc slurpBuiltin),
   ("eval", Func False $ toMalFunc $ withGlobalEnv . eval),
   ("atom", Func False $ toMalFunc atomBuiltin),
-  ("atom?", Func False $ toMalFunc isAtom),
   ("deref", Func False $ toMalFunc derefBuiltin),
   ("reset!", Func False $ toMalFunc resetBuiltin),
   ("swap!", Func False swapBuiltin),
@@ -332,10 +359,20 @@ baseEnv = fromList [
   ("concat", Func False concatBuiltin),
   ("first", Func False $ toMalFunc firstBuiltin),
   ("rest", Func False $ toMalFunc restBuiltin),
-  ("nth", Func False $ toMalFunc nthBuiltin),
   ("quote", Func False quoteBuiltin),
   ("quasiquote", Func False quasiquoteBuiltin),
-  ("macroexpand", Func False macroexpandBuiltin)
+  ("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)
 ]
 
 coreLib : String
@@ -343,16 +380,73 @@ 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) 
+(defmacro! cond
+  (fn* (& xs) (if (> (count xs) 0)
         (list 'if (first xs)
-              (if (> (count xs) 1) 
-                  (nth xs 1)
+              (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! 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! 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
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index d983932865..d68e587c44 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,6 +1,6 @@
 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
+	   step8_macros.idr step9_try.idr
 OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
diff --git a/impls/idris2/Types.idr b/impls/idris2/Types.idr
index eba35f11c5..90c4d5b81b 100644
--- a/impls/idris2/Types.idr
+++ b/impls/idris2/Types.idr
@@ -68,7 +68,7 @@ implementation Eq AST where
   Map x == Map y = SortedMap.toList x == SortedMap.toList y
   Func _ _ == Func _ _ = False
   _ == _ = False
- 
+
 export
 truthiness : AST -> Bool
 truthiness (Symbol "false") = False
@@ -76,19 +76,8 @@ truthiness (Symbol "nil") = False
 truthiness _ = True
 
 export
-isList : AST -> Bool
-isList (List False _) = True
-isList _ = False
-
-export
-isVector : AST -> Bool
-isVector (List True _) = True
-isVector _ = False
-
-export
-isAtom : AST -> Bool
-isAtom (Atom _) = True
-isAtom _ = False
+Keyword : String -> AST
+Keyword = Str . strCons '\xff'
 
 export
 getEnv : MalM (IORef (SortedMap String AST))
@@ -123,7 +112,7 @@ export
 lookup : String -> MalM AST
 lookup n = reader symbols >>= go
   where go : List (IORef (SortedMap String AST)) -> MalM AST
-        go [] = throwError $ Str $ "Symbol " ++ n ++ " not found"
+        go [] = throwError $ Str $ "'" ++ n ++ "' not found"
         go (e::es) = do
           val <- map (lookup n) $ liftIO $ readIORef e
           case val of
diff --git a/impls/idris2/step2_eval.idr b/impls/idris2/step2_eval.idr
index 1a41b951be..a58c6b9da6 100644
--- a/impls/idris2/step2_eval.idr
+++ b/impls/idris2/step2_eval.idr
@@ -33,7 +33,7 @@ repl r prompt f = do
   repl r prompt f
 
 main : IO ()
-main = do 
+main = do
   startingEnv <- getStartingEnv
   repl startingEnv "user> " $ \input => runMalM $ do
     Just ast <- read input
diff --git a/impls/idris2/step6_file.idr b/impls/idris2/step6_file.idr
index 4474604184..cad29f9125 100644
--- a/impls/idris2/step6_file.idr
+++ b/impls/idris2/step6_file.idr
@@ -42,7 +42,7 @@ doRepl startingEnv = repl startingEnv "user> " $ \input => runMalM $ do
   MonadTrans.liftIO $ putStrLn str
 
 main : IO ()
-main = do 
+main = do
   startingEnv <- getStartingEnv
   args <- getArgs
   case args of
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

From 946e3eafe04e93e21c7ab0973c5c7facab2331f8 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 01:57:12 -0400
Subject: [PATCH 10/17] Idris2: step A

---
 impls/idris2/Core.idr      | 60 +++++++++++++++++++++++++++++++++-----
 impls/idris2/Makefile      |  2 +-
 impls/idris2/stepA_mal.idr | 57 ++++++++++++++++++++++++++++++++++++
 3 files changed, 111 insertions(+), 8 deletions(-)
 create mode 100644 impls/idris2/stepA_mal.idr

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
index 26abbdc138..8d4643af17 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -5,6 +5,7 @@ import Data.List
 import Data.Maybe
 import Data.Strings
 import System
+import System.Clock
 import System.File
 
 import Eval
@@ -194,11 +195,13 @@ derefBuiltin = MonadTrans.liftIO . readIORef
 swapBuiltin : List AST -> MalM AST
 swapBuiltin [] = throwError $ Str "swap!: too few arguments"
 swapBuiltin [_] = throwError $ Str "swap!: too few arguments"
-swapBuiltin xs = do
-  Atom x::Func _ f::args <- traverse eval xs
-    | _ => throwError $ Str "swap!: type error"
+swapBuiltin (a::f::args) = do
+  Atom x <- eval a
+    | _ => throwError $ Str "swap!: expecting atom"
+  Func _ f' <- eval f
+    | _ => throwError $ Str "swap!: expecting function"
   old <- liftIO $ readIORef x
-  new <- f (old::args)
+  new <- f' (old::args)
   resetBuiltin x new
 
 consBuiltin : AST -> List AST -> List AST
@@ -267,7 +270,7 @@ typeofBuiltin (WithMeta _ _) = Symbol "nil" -- TODO
 typeofBuiltin (List False _) = Keyword "list"
 typeofBuiltin (List True _) = Keyword "vector"
 typeofBuiltin (Map _) = Keyword "map"
-typeofBuiltin (Func False _) = Keyword "func"
+typeofBuiltin (Func False _) = Keyword "fn"
 typeofBuiltin (Func True _) = Keyword "macro"
 
 assocBuiltin : List AST -> MalM AST
@@ -299,6 +302,38 @@ 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 String
+readlineBuiltin s =
+  case strUncons s of
+       Just ('\xff', _) => throwError $ Str "readline: expecing a string"
+       _ => liftIO $ do
+         putStr s
+         getLine
+
 prStr : List AST -> MalM AST
 prStr xs = do
   xs' <- traverse eval xs
@@ -325,6 +360,7 @@ 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}),
@@ -372,7 +408,13 @@ baseEnv = fromList [
   ("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)
+  ("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
@@ -423,6 +465,8 @@ coreLib = "
     )
   )
 )
+(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)))
@@ -444,6 +488,8 @@ coreLib = "
       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))))
@@ -459,7 +505,7 @@ getStartingEnv = do
          _ => List False []
   env <- map (\v => MkEnv fullEval [v]) $ newIORef $ insert "*ARGV*" argv baseEnv
   res <- runExceptT $ flip runReaderT env $ do
-    defs <- either (throwError . Str . ("parse error: "++)) pure $ parseText coreLib
+    defs <- either (throwError . Str) pure $ parseText coreLib
     traverse_ eval defs
   case res of
        Right () => pure ()
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index d68e587c44..a5c75d586d 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,6 +1,6 @@
 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
+	   step8_macros.idr step9_try.idr stepA_mal.idr
 OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
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

From 13de766d32ebe71eec4fb74f04cbc2eaf267f62c Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 02:01:57 -0400
Subject: [PATCH 11/17] Idris2: fix nth

---
 impls/idris2/Core.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
index 8d4643af17..7401545e79 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -437,7 +437,7 @@ coreLib = "
     (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))
+    true (nth (rest xs) (- n 1))
   )
 ))
 (def! apply

From 59ca50d2a9c988107d10dd03fb03c2de2eb495b0 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 02:49:40 -0400
Subject: [PATCH 12/17] Idris2: fix swap!

---
 impls/idris2/Core.idr | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
index 7401545e79..7047f23840 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -196,12 +196,9 @@ 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 <- eval a
-    | _ => throwError $ Str "swap!: expecting atom"
-  Func _ f' <- eval f
-    | _ => throwError $ Str "swap!: expecting function"
-  old <- liftIO $ readIORef x
-  new <- f' (old::args)
+  (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

From 6e9cadcafcae2aa681d32f058243924aa7cbb990 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 03:27:12 -0400
Subject: [PATCH 13/17] Idris2: some cleanup

---
 impls/idris2/Class.idr  | 88 +++++++++++++++++++++++++++++++++++++++++
 impls/idris2/Core.idr   | 75 +----------------------------------
 impls/idris2/Eval.idr   |  1 -
 impls/idris2/Makefile   |  2 +-
 impls/idris2/Reader.idr |  5 ++-
 impls/idris2/Types.idr  |  6 ---
 6 files changed, 94 insertions(+), 83 deletions(-)
 create mode 100644 impls/idris2/Class.idr

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
index 7047f23840..75c39a3bee 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -8,82 +8,11 @@ import System
 import System.Clock
 import System.File
 
+import Class
 import Eval
 import Reader
 import Types
 
--- Builtins
-interface MalType a where
-  toMalAst : a -> AST
-  fromMalAst : AST -> Maybe a
-
-implementation MalType AST where
-  toMalAst = id
-  fromMalAst = Just
-
-implementation MalType () where
-  toMalAst () = Symbol "nil"
-  fromMalAst (Symbol "nil") = Just ()
-  fromMalAst _ = Nothing
-
-implementation MalType Integer where
-  toMalAst = Number
-  fromMalAst (Number x) = Just x
-  fromMalAst _ = Nothing
-
-implementation MalType String where
-  toMalAst = Str
-  fromMalAst (Str s) = Just s
-  fromMalAst _ = Nothing
-
-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
-
-implementation MalType (IORef AST) where
-  toMalAst = Atom
-  fromMalAst (Atom a) = Just a
-  fromMalAst _ = Nothing
-
-implementation MalType a => MalType (List a) where
-  toMalAst = List False . map toMalAst
-  fromMalAst (List _ xs) = traverse fromMalAst xs
-  fromMalAst (Symbol "nil") = Just []
-  fromMalAst _ = Nothing
-
-implementation MalType (SortedMap String AST) where
-  toMalAst = Map
-  fromMalAst (Map m) = Just m
-  fromMalAst (Symbol "nil") = Just empty
-  fromMalAst _ = Nothing
-
-interface MalFunction a where
-  toMalFunc : a -> List AST -> MalM AST
-
-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"
-
-implementation MalType a => MalFunction (MalM a) where
-  toMalFunc x [] = map toMalAst x
-  toMalFunc _ xs = do
-    traverse eval xs
-    throwError $ Str "Too many arguments"
-
-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
-
--- Specialized on MalM to help type inference
 liftIO' : MalType a => IO a -> MalM AST
 liftIO' = map toMalAst . MonadTrans.liftIO
 
@@ -237,7 +166,6 @@ quasiquoteBuiltin [x] = qq x
         qq (Str s) = pure $ Str s
         qq (Number x) = pure $ Number x
         qq (Atom a) = pure $ Atom a
-        qq (WithMeta a b) = pure $ WithMeta a b -- TODO
         qq (List False [Symbol "unquote", a]) = eval a
         qq (List _ xs) = do
           xs' <- traverse qq xs
@@ -263,7 +191,6 @@ 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 (WithMeta _ _) = Symbol "nil" -- TODO
 typeofBuiltin (List False _) = Keyword "list"
 typeofBuiltin (List True _) = Keyword "vector"
 typeofBuiltin (Map _) = Keyword "map"
diff --git a/impls/idris2/Eval.idr b/impls/idris2/Eval.idr
index fd187c24f2..039f111445 100644
--- a/impls/idris2/Eval.idr
+++ b/impls/idris2/Eval.idr
@@ -18,7 +18,6 @@ fullEval (Symbol n) = lookup n
 fullEval (Str s) = pure $ Str s
 fullEval (Number x) = pure $ Number x
 fullEval (Atom e) = pure $ Atom e
-fullEval (WithMeta a b) = pure $ WithMeta a b -- TODO
 fullEval (List False []) = pure $ List False []
 fullEval (List False (f::xs)) = do
   Func _ f' <- fullEval f
diff --git a/impls/idris2/Makefile b/impls/idris2/Makefile
index a5c75d586d..ee02a55485 100644
--- a/impls/idris2/Makefile
+++ b/impls/idris2/Makefile
@@ -1,7 +1,7 @@
 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 MonadTrans.idr
+OTHER_SRCS = Types.idr Reader.idr Eval.idr Core.idr Class.idr MonadTrans.idr
 BINS = $(SRCS:%.idr=build/exec/%)
 
 idris_args = -p contrib
diff --git a/impls/idris2/Reader.idr b/impls/idris2/Reader.idr
index 8442ad8d70..cbfb8b8109 100644
--- a/impls/idris2/Reader.idr
+++ b/impls/idris2/Reader.idr
@@ -122,7 +122,10 @@ mutual
           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 "^" = flip WithMeta <$> grammar <*> grammar
+          sigilAction "^" = do
+            x <- grammar
+            y <- grammar
+            pure $ List False [Symbol "with-meta", y, x]
 
   grammar : Parser AST
   grammar = choice [
diff --git a/impls/idris2/Types.idr b/impls/idris2/Types.idr
index 90c4d5b81b..8126931640 100644
--- a/impls/idris2/Types.idr
+++ b/impls/idris2/Types.idr
@@ -13,7 +13,6 @@ mutual
            | Str String -- Includes keywords
            | Number Integer
            | Atom (IORef AST)
-           | WithMeta AST AST
            | List Bool (List AST) -- List False -> List, List True -> Vector
            | Map (SortedMap String AST)
            | Func Bool (List AST -> MalM AST)
@@ -40,10 +39,6 @@ toString b (Atom a) = do
   x <- readIORef a
   sx <- toString b x
   pure $ "(atom " ++ sx ++ ")"
-toString b (WithMeta x y) = do
-  sx <- toString b x
-  sy <- toString b y
-  pure $ "(with-meta " ++ sx ++ " " ++ sy ++ ")"
 toString b (List False xs) = do
   sxs <- traverse (toString b) xs
   pure $ "(" ++ unwords sxs ++ ")"
@@ -63,7 +58,6 @@ implementation Eq AST where
   Symbol x == Symbol y = x == y
   Str x == Str y = x == y
   Number x == Number y = x == y
-  WithMeta a b == WithMeta x y = a == x && b == y
   List _ x == List _ y = x == y
   Map x == Map y = SortedMap.toList x == SortedMap.toList y
   Func _ _ == Func _ _ = False

From 4812148417af48e4c13d0751abbd26b37e8029e4 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 16:57:46 -0400
Subject: [PATCH 14/17] Idris2: add Dockerfile

---
 impls/idris2/Dockerfile | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 impls/idris2/Dockerfile

diff --git a/impls/idris2/Dockerfile b/impls/idris2/Dockerfile
new file mode 100644
index 0000000000..147466c957
--- /dev/null
+++ b/impls/idris2/Dockerfile
@@ -0,0 +1,36 @@
+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
+##########################################################
+
+ENV HOME /mal
+ENV PATH /mal/.idris2/bin:$PATH
+ENV LD_LIBRARY_PATH /mal/.idris2/lib:$LD_LIBRARY_PATH
+
+# Idris2 deps
+RUN apt-get -y install gcc chezscheme git
+
+# Install from source
+ENV SCHEME chezscheme
+RUN git clone https://github.com/idris-lang/Idris2.git \
+    && cd Idris2 \
+    && make bootstrap \
+    && make install

From 485b566bca2647ec64cf1ac193f8db8750d3077f Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 20:06:32 -0400
Subject: [PATCH 15/17] Idris2: fix Dockerfile

---
 impls/idris2/Dockerfile | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/impls/idris2/Dockerfile b/impls/idris2/Dockerfile
index 147466c957..b29dd36764 100644
--- a/impls/idris2/Dockerfile
+++ b/impls/idris2/Dockerfile
@@ -21,16 +21,19 @@ WORKDIR /mal
 # Specific implementation requirements
 ##########################################################
 
-ENV HOME /mal
-ENV PATH /mal/.idris2/bin:$PATH
-ENV LD_LIBRARY_PATH /mal/.idris2/lib:$LD_LIBRARY_PATH
-
 # 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

From bb1fd58fd4aad6b9368e979505c7bfbdcb56002a Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 20:34:02 -0400
Subject: [PATCH 16/17] Put idris in its appropriate alphabetical location in
 the Makefile

---
 Makefile | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index ccd2d73937..caa71e4e8f 100644
--- a/Makefile
+++ b/Makefile
@@ -91,11 +91,10 @@ 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 \
-	idris2
+	swift swift3 swift4 swift5 tcl ts vala vb vhdl vimscript wasm wren yorick xslt zig
 
 EXTENSION = .mal
 
@@ -218,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
@@ -271,7 +271,6 @@ wren_STEP_TO_PROG =          impls/wren/$($(1)).wren
 yorick_STEP_TO_PROG =        impls/yorick/$($(1)).i
 xslt_STEP_TO_PROG =          impls/xslt/$($(1))
 zig_STEP_TO_PROG =           impls/zig/$($(1))
-idris2_STEP_TO_PROG =        impls/idris2/build/exec/$($(1))
 
 #
 # General settings and utility functions

From b4691504000528aff0ed4ade94ddf5b74194d2a7 Mon Sep 17 00:00:00 2001
From: Mark Barbone <mark.l.barbone@gmail.com>
Date: Thu, 2 Jul 2020 23:48:08 -0400
Subject: [PATCH 17/17] Idris2: make readline handle EOF better

---
 impls/idris2/Core.idr | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/impls/idris2/Core.idr b/impls/idris2/Core.idr
index 75c39a3bee..40b052bd65 100644
--- a/impls/idris2/Core.idr
+++ b/impls/idris2/Core.idr
@@ -250,13 +250,15 @@ seqBuiltin (Str s) = case strUncons s of
                           _ => pure $ List False $ map (Str . pack . pure) $ unpack s
 seqBuiltin _ = throwError $ Str "seq: expecting a list, vector, or string"
 
-readlineBuiltin : String -> MalM 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
-         getLine
+         map Str getLine
 
 prStr : List AST -> MalM AST
 prStr xs = do