diff --git a/.github/workflows/ci-idris2.yml b/.github/workflows/ci-idris2.yml
index 5aef38215..84b4e9ebd 100644
--- a/.github/workflows/ci-idris2.yml
+++ b/.github/workflows/ci-idris2.yml
@@ -33,7 +33,7 @@ on:
       - '.github/workflows/ci-super-linter.yml'
 
 env:
-  IDRIS2_VERSION: 0.4.0 # For previous-version build
+  IDRIS2_VERSION: 0.5.0 # For previous-version build
 
 jobs:
 
@@ -542,4 +542,4 @@ jobs:
       - name: Build Frex
         run: |
           make
-          make test
\ No newline at end of file
+          make test
diff --git a/CHANGELOG.md b/CHANGELOG.md
index f00b7efa9..d20295ff4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,15 @@
 # Changelog
 
+## [Next version]
+
+### REPL changes
+
+* New experimental Scheme based evaluator (only available if compiled via
+  Chez scheme or Racket). To access this at the REPL, set the evaluator mode to
+  the scheme based evaluator with `:set eval scheme`.
+* New option `evaltiming` to time how long an evaluation takes at the REPL,
+  set with `:set evaltiming`.
+
 ## v0.5.0
 
 ### Language changes
diff --git a/Release/CHECKLIST b/Release/CHECKLIST
index 9d5ce0327..dd7828cd8 100644
--- a/Release/CHECKLIST
+++ b/Release/CHECKLIST
@@ -4,6 +4,7 @@
 [ ] Change version number in idris2api.ipkg
 [ ] Change version number in flake.nix
 [ ] Change version number in test pkg010 (TODO: make this step unnecessary!)
+[ ] Make sure INSTALL.md gives the correct minimum Idris version
 [ ] Update bootstrap chez and racket
 [ ] Remove __collect_safe from generated chez (to avoid need for chez >9.5)
 [ ] Tag on github with version number (in the form vX.Y.Z)
diff --git a/idris2api.ipkg b/idris2api.ipkg
index 9b043f8dd..f72482482 100644
--- a/idris2api.ipkg
+++ b/idris2api.ipkg
@@ -71,6 +71,7 @@ modules =
     Core.Ord,
     Core.Primitives,
     Core.Reflect,
+    Core.SchemeEval,
     Core.Termination,
     Core.Transform,
     Core.TT,
@@ -79,6 +80,12 @@ modules =
     Core.UnifyState,
     Core.Value,
 
+    Core.SchemeEval.Builtins,
+    Core.SchemeEval.Compile,
+    Core.SchemeEval.Evaluate,
+    Core.SchemeEval.Quote,
+    Core.SchemeEval.ToScheme,
+
     IdrisPaths,
 
     Idris.CommandLine,
@@ -175,6 +182,7 @@ modules =
     Libraries.Utils.Hex,
     Libraries.Utils.Octal,
     Libraries.Utils.Path,
+    Libraries.Utils.Scheme,
     Libraries.Utils.Shunting,
     Libraries.Utils.String,
     Libraries.Utils.Term,
diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr
index 0f0dd5943..750707202 100644
--- a/src/Compiler/Common.idr
+++ b/src/Compiler/Common.idr
@@ -19,6 +19,7 @@ import Core.TTC
 import Libraries.Data.IOArray
 import Libraries.Data.SortedMap
 import Libraries.Utils.Path
+import Libraries.Utils.Scheme
 
 import Data.List
 import Data.List1
@@ -146,7 +147,7 @@ getMinimalDef (Coded ns bin)
              = MkGlobalDef fc name (Erased fc False) [] [] [] [] mul
                            [] Public (MkTotality Unchecked IsCovering)
                            [] Nothing refsR False False True
-                           None cdef []
+                           None cdef Nothing [] Nothing
          pure (def, Just (ns, bin))
 
 -- ||| Recursively get all calls in a function definition
diff --git a/src/Compiler/Inline.idr b/src/Compiler/Inline.idr
index 11d4d1888..587e9d953 100644
--- a/src/Compiler/Inline.idr
+++ b/src/Compiler/Inline.idr
@@ -523,7 +523,9 @@ addArityHash n
          Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
          let Just cexpr =  compexpr def             | Nothing => pure ()
          let MkFun args _ = cexpr                   | _ => pure ()
-         addHash (n, length args)
+         case visibility def of
+              Private => pure ()
+              _ => addHash (n, length args)
 
 export
 compileAndInlineAll : {auto c : Ref Ctxt Defs} ->
diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 79e07025b..305e27a3a 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -12,6 +12,7 @@ import public Core.Options.Log
 import public Core.TT
 
 import Libraries.Utils.Binary
+import Libraries.Utils.Scheme
 
 import Data.Fin
 import Libraries.Data.IOArray
@@ -312,7 +313,9 @@ newDef fc n rig vars ty vis def
         , linearChecked = False
         , definition = def
         , compexpr = Nothing
+        , namedcompexpr = Nothing
         , sizeChange = []
+        , schemeExpr = Nothing
         }
 
 -- Rewrite rules, applied after type checking, for runtime code only
@@ -745,6 +748,7 @@ record Defs where
      -- timeout should be thrown
   warnings : List Warning
      -- ^ as yet unreported warnings
+  schemeEvalLoaded : Bool
 
 -- Label for context references
 export
@@ -792,6 +796,7 @@ initDefs
            , timings = empty
            , timer = Nothing
            , warnings = []
+           , schemeEvalLoaded = False
            }
 
 -- Reset the context, except for the options
@@ -1011,7 +1016,9 @@ addBuiltin n ty tot op
          , linearChecked = True
          , definition = Builtin op
          , compexpr = Nothing
+         , namedcompexpr = Nothing
          , sizeChange = []
+         , schemeExpr = Nothing
          }
 
 export
@@ -1023,7 +1030,8 @@ updateDef n fdef
              | Nothing => pure ()
          case fdef (definition gdef) of
               Nothing => pure ()
-              Just def' => ignore $ addDef n (record { definition = def' } gdef)
+              Just def' => ignore $ addDef n (record { definition = def',
+                                                       schemeExpr = Nothing } gdef)
 
 export
 updateTy : {auto c : Ref Ctxt Defs} ->
diff --git a/src/Core/Context/Context.idr b/src/Core/Context/Context.idr
index 2bff99d4a..745812f5f 100644
--- a/src/Core/Context/Context.idr
+++ b/src/Core/Context/Context.idr
@@ -20,6 +20,7 @@ import Libraries.Data.IOArray
 import Libraries.Data.NameMap
 import Libraries.Data.UserNameMap
 import Libraries.Utils.Binary
+import Libraries.Utils.Scheme
 
 public export
 data Ref : (l : label) -> Type -> Type where
@@ -278,6 +279,17 @@ export
 Eq SCCall where
   x == y = fnCall x == fnCall y && fnArgs x == fnArgs y
 
+public export
+data SchemeMode
+        = EvalAll -- evaluate everything
+        | BlockExport -- compile 'export' names in other modules as blocked
+
+export
+Eq SchemeMode where
+   EvalAll == EvalAll = True
+   BlockExport == BlockExport = True
+   _ == _ = False
+
 public export
 record GlobalDef where
   constructor MkGlobalDef
@@ -306,7 +318,9 @@ record GlobalDef where
   linearChecked : Bool -- Flag whether we've already checked its linearity
   definition : Def
   compexpr : Maybe CDef
+  namedcompexpr : Maybe NamedDef
   sizeChange : List SCCall
+  schemeExpr : Maybe (SchemeMode, SchemeObj Write)
 
 export
 gDefKindedName : GlobalDef -> KindedName
diff --git a/src/Core/SchemeEval.idr b/src/Core/SchemeEval.idr
new file mode 100644
index 000000000..b31089d63
--- /dev/null
+++ b/src/Core/SchemeEval.idr
@@ -0,0 +1,88 @@
+module Core.SchemeEval
+
+-- Top level interface to the scheme based evaluator
+-- Drops back to the default slow evaluator if scheme isn't available
+
+import Core.Context
+import Core.Context.Log
+import Core.Core
+import Core.Env
+import Core.Normalise
+import public Core.SchemeEval.Compile
+import public Core.SchemeEval.Evaluate
+import public Core.SchemeEval.Quote
+import public Core.SchemeEval.ToScheme
+import Core.TT
+
+import Libraries.Data.NameMap
+import Libraries.Utils.Scheme
+
+{-
+
+Summary:
+
+SObj vars
+   ...is a scheme object with the scheme representation of the result
+   of evaluating a term vars
+
+SNF vars
+   ...corresponds to NF vars, and is an inspectable version of the above.
+   Evaluation is call by value, but there has not yet been any evaluation
+   under lambdas
+
+'Evaluate.seval' gets you an SObj from a Term
+   - this involves compiling all the relevant definitions to scheme code
+   first. We make a note of what we've compiled to scheme so we don't have
+   to do it more than once.
+`Evaluate.toSNF` gets you an SNF from an SObj
+`Quote.quote` gets you back to a Term from an SNF
+
+`snf` gets you directly to an SNF from a Term
+`snormalise` packages up the whole process
+
+All of this works only on a back end which can call scheme directly, and
+with the relevant support files (currently: Chez)
+
+-}
+
+snormaliseMode : {auto c : Ref Ctxt Defs} ->
+                 {vars : _} ->
+                 SchemeMode -> Env Term vars -> Term vars -> Core (Term vars)
+snormaliseMode mode env tm
+    = do defs <- get Ctxt
+         True <- initialiseSchemeEval
+             | _ => normalise defs env tm
+         sval <- seval mode env tm
+         quoteObj sval
+
+export
+snormalise : {auto c : Ref Ctxt Defs} ->
+             {vars : _} ->
+             Env Term vars -> Term vars -> Core (Term vars)
+snormalise = snormaliseMode BlockExport
+
+export
+snormaliseAll : {auto c : Ref Ctxt Defs} ->
+                {vars : _} ->
+                Env Term vars -> Term vars -> Core (Term vars)
+snormaliseAll = snormaliseMode EvalAll
+
+export
+snf : {auto c : Ref Ctxt Defs} ->
+      {vars : _} ->
+      Env Term vars -> Term vars -> Core (SNF vars)
+snf env tm
+    = do True <- initialiseSchemeEval
+             | _ => throw (InternalError "Scheme evaluator not available")
+         sval <- seval BlockExport env tm
+         toSNF sval
+
+export
+snfAll : {auto c : Ref Ctxt Defs} ->
+         {vars : _} ->
+         Env Term vars -> Term vars -> Core (SNF vars)
+snfAll env tm
+    = do True <- initialiseSchemeEval
+             | _ => throw (InternalError "Scheme evaluator not available")
+         sval <- seval EvalAll env tm
+         toSNF sval
diff --git a/src/Core/SchemeEval/Builtins.idr b/src/Core/SchemeEval/Builtins.idr
new file mode 100644
index 000000000..cbced1ab9
--- /dev/null
+++ b/src/Core/SchemeEval/Builtins.idr
@@ -0,0 +1,314 @@
+module Core.SchemeEval.Builtins
+
+import Core.Context
+import Core.SchemeEval.ToScheme
+import Core.TT
+
+import Data.Vect
+import Libraries.Utils.Scheme
+
+-- Integers are wrapped, so unwrap then wrap again
+add : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+add (Just (Signed (P n))) x y = Apply (Var "ct-s+") [x, y, toScheme (n-1)]
+add (Just (Unsigned n)) x y = Apply (Var "ct-u+") [x, y, toScheme n]
+add _ x y = Apply (Var "ct+") [x, y]
+
+sub : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+sub (Just (Signed (P n))) x y = Apply (Var "ct-s-") [x, y, toScheme (n-1)]
+sub (Just (Unsigned n)) x y = Apply (Var "ct-u-") [x, y, toScheme n]
+sub _ x y = Apply (Var "ct-") [x, y]
+
+mul : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+mul (Just (Signed (P n))) x y = Apply (Var "ct-s*") [x, y, toScheme (n-1)]
+mul (Just (Unsigned n)) x y = Apply (Var "ct-u*") [x, y, toScheme n]
+mul _ x y = Apply (Var "ct*") [x, y]
+
+div : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+div (Just (Signed Unlimited)) x y = Apply (Var "ct/") [x, y]
+div (Just (Signed (P n))) x y = Apply (Var "ct-s/") [x, y, toScheme (n-1)]
+div (Just (Unsigned n)) x y = Apply (Var "ct-u/") [x, y, toScheme n]
+div _ x y = Apply (Var "ct/") [x, y]
+
+mod : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+mod x y = Apply (Var "ct-mod") [x, y]
+
+shl : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+shl (Just (Signed (P n))) x y = Apply (Var "ct-bits-shl-signed") [x, y, toScheme (n-1)]
+shl (Just (Unsigned n)) x y = Apply (Var "ct-bits-shl") [x, y, toScheme n]
+shl _ x y = Apply (Var "ct-shl") [x, y]
+
+shr : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+shr _ x y = Apply (Var "ct-shr") [x, y]
+
+-- Doubles don't need wrapping, since there's only one double type
+addDbl : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+addDbl x y = Apply (Var "+") [x, y]
+
+subDbl : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+subDbl x y = Apply (Var "-") [x, y]
+
+mulDbl : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+mulDbl x y = Apply (Var "*") [x, y]
+
+divDbl : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+divDbl x y = Apply (Var "/") [x, y]
+
+-- Check necessary arguments are in canonical form before applying the
+-- operator, otherwise return the blocked form
+-- Current assumption is that all primitives that we can evaluate at
+-- compile time work on constants, if they do anything in Scheme at all.
+canonical : SchemeObj Write ->
+            Vect n (SchemeObj Write) -> SchemeObj Write -> SchemeObj Write
+canonical blk [] body = body
+canonical blk (n :: ns) body
+   = If (Apply (Var "ct-isConstant") [n]) (canonical blk ns body) blk
+
+-- Return blocked application if a partial operator is given an input
+-- on which it's undefined
+testPartial : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+testPartial blk res
+    = Let "p-0" res $
+          (If (Apply (Var "ct-isConstant") [Var "p-0"])
+              (Var "p-0")
+              blk)
+
+unaryOp : SchemeObj Write -> String ->
+          SchemeObj Write -> SchemeObj Write
+unaryOp blk op x = canonical blk [x] $ Apply (Var op) [x]
+
+binOp : SchemeObj Write -> String ->
+        SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+binOp blk op x y = canonical blk [x, y] $ Apply (Var op) [x, y]
+
+ternaryOp : SchemeObj Write -> String ->
+            SchemeObj Write -> SchemeObj Write -> SchemeObj Write ->
+            SchemeObj Write
+ternaryOp blk op x y z = canonical blk [x, y, z] $ Apply (Var op) [x, y, z]
+
+int : SchemeObj Write -> SchemeObj Write
+int obj = Vector (-100) [obj]
+
+int8 : SchemeObj Write -> SchemeObj Write
+int8 obj = Vector (-101) [obj]
+
+int16 : SchemeObj Write -> SchemeObj Write
+int16 obj = Vector (-102) [obj]
+
+int32 : SchemeObj Write -> SchemeObj Write
+int32 obj = Vector (-103) [obj]
+
+int64 : SchemeObj Write -> SchemeObj Write
+int64 obj = Vector (-104) [obj]
+
+integer : SchemeObj Write -> SchemeObj Write
+integer obj = Vector (-105) [obj]
+
+bits8 : SchemeObj Write -> SchemeObj Write
+bits8 obj = Vector (-106) [obj]
+
+bits16 : SchemeObj Write -> SchemeObj Write
+bits16 obj = Vector (-107) [obj]
+
+bits32 : SchemeObj Write -> SchemeObj Write
+bits32 obj = Vector (-108) [obj]
+
+bits64 : SchemeObj Write -> SchemeObj Write
+bits64 obj = Vector (-109) [obj]
+
+wrap : IntKind -> SchemeObj Write -> SchemeObj Write
+wrap (Signed Unlimited) = integer
+wrap (Signed (P 8)) = int8
+wrap (Signed (P 16)) = int16
+wrap (Signed (P 32)) = int32
+wrap (Signed (P 64)) = int64
+wrap (Unsigned 8) = bits8
+wrap (Unsigned 16) = bits16
+wrap (Unsigned 32) = bits32
+wrap (Unsigned 64) = bits64
+wrap _ = integer
+
+-- Result has to be wrapped in Int, which is Vector (-100)
+boolOp : SchemeObj Write -> String ->
+         SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+boolOp blk op x y
+    = canonical blk [x, y] $
+         int $
+             Apply (Var "or")
+                [Apply (Var "and") [Apply (Var op) [x, y],
+                                    IntegerVal 1],
+                 IntegerVal 0]
+
+applyIntCast : IntKind -> IntKind -> SchemeObj Write -> SchemeObj Write
+applyIntCast _ (Signed Unlimited) x = x
+applyIntCast (Signed m) k@(Signed (P n)) x
+    = if P n >= m
+         then x
+         else wrap k $ Apply (Var "ct-toSignedInt") [x, toScheme (n - 1)]
+applyIntCast (Unsigned m) k@(Signed (P n)) x
+    = if n > m
+         then x
+         else wrap k $ Apply (Var "ct-toSignedInt") [x, toScheme (n - 1)]
+applyIntCast (Signed _) k@(Unsigned n) x
+    = wrap k $ Apply (Var "ct-toUnsignedInt") [x, toScheme n]
+applyIntCast (Unsigned m) (Unsigned n) x
+    = if n >= m
+         then x
+         else Apply (Var "ct-toUnsignedInt") [x, toScheme n]
+
+applyCast : SchemeObj Write ->
+            Constant -> Constant ->
+            SchemeObj Write -> SchemeObj Write
+applyCast blk CharType to x
+    = canonical blk [x] $
+        case intKind to of
+           Nothing =>
+              case to of
+                   StringType => Apply (Var "string") [x]
+                   _ => blk
+           Just (Signed Unlimited) => integer $ Apply (Var "char->integer") [x]
+           Just k@(Signed (P n)) => wrap k $ Apply (Var "ct-cast-char-boundedInt") [x, toScheme (n - 1)]
+           Just k@(Unsigned n) => wrap k $ Apply (Var "ct-cast-char-boundedUInt") [x, toScheme n]
+applyCast blk from CharType x
+    = canonical blk [x] $
+        case intKind from of
+           Nothing => blk
+           Just k => Apply (Var "ct-cast-int-char") [x]
+applyCast blk StringType to x
+    = canonical blk [x] $
+        case intKind to of
+           Nothing => case to of
+                           DoubleType => Apply (Var "ct-cast-string-double") [x]
+                           _ => blk
+           Just (Signed Unlimited) => integer $ Apply (Var "ct-cast-string-int") [x]
+           Just k@(Signed (P n)) => wrap k $ Apply (Var "ct-cast-string-boundedInt") [x, toScheme (n - 1)]
+           Just k@(Unsigned n) => wrap k $ Apply (Var "ct-cast-string-boundedUInt") [x, toScheme n]
+applyCast blk from StringType x
+    = canonical blk [x] $
+        case intKind from of
+           Nothing => case from of
+                           DoubleType => Apply (Var "number->string") [x]
+                           _ => blk
+           Just k => Apply (Var "ct-cast-number-string") [x]
+applyCast blk DoubleType to x
+    = canonical blk [x] $
+        case intKind to of
+           Nothing => case to of
+                           StringType => Apply (Var "number->string") [x]
+                           _ => blk
+           Just (Signed Unlimited) => integer $ Apply (Var "ct-exact-truncate") [x]
+           Just k@(Signed (P n)) => wrap k $ Apply (Var "ct-exact-truncate-boundedInt") [x, toScheme (n - 1)]
+           Just k@(Unsigned n) => wrap k $ Apply (Var "ct-exact-truncate-boundedUInt") [x, toScheme n]
+applyCast blk from DoubleType x
+    = canonical blk [x] $
+        case intKind from of
+           Nothing => case from of
+                           StringType => Apply (Var "ct-cast-string-double") [x]
+                           _ => blk
+           Just k => Apply (Var "ct-int-double") [x]
+applyCast blk from to x
+    = canonical blk [x] $
+        case (intKind from, intKind to) of
+           (Just f, Just t) => applyIntCast f t x
+           _ => blk
+
+applyOp : SchemeObj Write -> -- if we don't have arguments in canonical form
+          PrimFn n -> Vect n (SchemeObj Write) ->
+          SchemeObj Write
+applyOp blk (Add DoubleType) [x, y] = binOp blk "+" x y
+applyOp blk (Sub DoubleType) [x, y] = binOp blk "-" x y
+applyOp blk (Mul DoubleType) [x, y] = binOp blk "*" x y
+applyOp blk (Div DoubleType) [x, y] = binOp blk "/" x y
+applyOp blk (Neg DoubleType) [x] = unaryOp blk "-" x
+applyOp blk (Add ty) [x, y] = canonical blk [x, y] $ add (intKind ty) x y
+applyOp blk (Sub ty) [x, y] = canonical blk [x, y] $ sub (intKind ty) x y
+applyOp blk (Mul ty) [x, y] = canonical blk [x, y] $ mul (intKind ty) x y
+applyOp blk (Div ty) [x, y] = canonical blk [x, y] $ div (intKind ty) x y
+applyOp blk (Mod ty) [x, y] = canonical blk [x, y] $ mod x y
+applyOp blk (Neg ty) [x] = canonical blk [x] $ Apply (Var "ct-neg") [x]
+applyOp blk (ShiftL ty) [x, y] = canonical blk [x, y] $ shl (intKind ty) x y
+applyOp blk (ShiftR ty) [x, y] = canonical blk [x, y] $ shr (intKind ty) x y
+applyOp blk (BAnd ty) [x, y] = binOp blk "ct-and" x y
+applyOp blk (BOr ty) [x, y] = binOp blk "ct-or" x y
+applyOp blk (BXOr ty) [x, y] = binOp blk "ct-xor" x y
+applyOp blk (LT CharType) [x, y] = boolOp blk "char<?" x y
+applyOp blk (LTE CharType) [x, y] = boolOp blk "char<=?" x y
+applyOp blk (EQ CharType) [x, y] = boolOp blk "char=?" x y
+applyOp blk (GTE CharType) [x, y] = boolOp blk "char>=?" x y
+applyOp blk (GT CharType) [x, y] = boolOp blk "char>?" x y
+applyOp blk (LT StringType) [x, y] = boolOp blk "string<?" x y
+applyOp blk (LTE StringType) [x, y] = boolOp blk "string<=?" x y
+applyOp blk (EQ StringType) [x, y] = boolOp blk "string=?" x y
+applyOp blk (GTE StringType) [x, y] = boolOp blk "string>=?" x y
+applyOp blk (GT StringType) [x, y] = boolOp blk "string>?" x y
+applyOp blk (LT DoubleType) [x, y] = boolOp blk "<" x y
+applyOp blk (LTE DoubleType) [x, y] = boolOp blk "<=" x y
+applyOp blk (EQ DoubleType) [x, y] = boolOp blk "=" x y
+applyOp blk (GTE DoubleType) [x, y] = boolOp blk ">=" x y
+applyOp blk (GT DoubleType) [x, y] = boolOp blk ">" x y
+applyOp blk (LT ty) [x, y] = boolOp blk "ct<" x y
+applyOp blk (LTE ty) [x, y] = boolOp blk "ct<=" x y
+applyOp blk (EQ ty) [x, y] = boolOp blk "ct=" x y
+applyOp blk (GTE ty) [x, y] = boolOp blk "ct>=" x y
+applyOp blk (GT ty) [x, y] = boolOp blk "ct>" x y
+applyOp blk StrLength [x]
+    = canonical blk [x] $ Vector (-100) [Apply (Var "string-length") [x]]
+applyOp blk StrHead [x]
+    = canonical blk [x] $ Apply (Var "string-ref")
+                                [x, IntegerVal 0]
+applyOp blk StrTail [x]
+    = canonical blk [x] $ Apply (Var "substring")
+                                [x, IntegerVal 1,
+                                 Apply (Var "string-length") [x]]
+applyOp blk StrIndex [x, y]
+    = canonical blk [x, y] $ testPartial blk $
+         Apply (Var "ct-string-ref") [x, y]
+applyOp blk StrCons [x, y]
+    = canonical blk [x, y] $ Apply (Var "ct-string-cons") [x, y]
+applyOp blk StrAppend [x, y]
+    = canonical blk [x, y] $ Apply (Var "string-append") [x, y]
+applyOp blk StrReverse [x]
+    = canonical blk [x] $ Apply (Var "ct-string-reverse") [x]
+applyOp blk StrSubstr [x, y, z]
+    = canonical blk [x, y, z] $ Apply (Var "ct-string-substr") [x]
+
+applyOp blk DoubleExp [x] = unaryOp blk "flexp" x
+applyOp blk DoubleLog [x] = unaryOp blk "fllog" x
+applyOp blk DoublePow [x, y] = binOp blk "expt" x y
+applyOp blk DoubleSin [x] = unaryOp blk "flsin" x
+applyOp blk DoubleCos [x] = unaryOp blk "flcos" x
+applyOp blk DoubleTan [x] = unaryOp blk "fltan" x
+applyOp blk DoubleASin [x] = unaryOp blk "flasin" x
+applyOp blk DoubleACos [x] = unaryOp blk "flacos" x
+applyOp blk DoubleATan [x] = unaryOp blk "flatan" x
+applyOp blk DoubleSqrt [x] = unaryOp blk "flsqrt" x
+applyOp blk DoubleFloor [x] = unaryOp blk "flfloor" x
+applyOp blk DoubleCeiling [x] = unaryOp blk "flceiling" x
+
+applyOp blk (Cast from to) [x] = applyCast blk from to x
+applyOp blk BelieveMe [_, _, x] = x
+applyOp blk Crash [_, msg] = blk
+
+mkArgList : Int -> (n : Nat) -> Vect n String
+mkArgList i Z = []
+mkArgList i (S k) = ("x-" ++ show i) :: mkArgList (i + 1) k
+
+export
+compileBuiltin : {farity : Nat} ->
+                Name -> PrimFn farity -> SchemeObj Write
+compileBuiltin nm fn
+    = let args = mkArgList 0 farity in
+          bindArgs args [] args
+  where
+    makeBlockedApp : Vect n String -> SchemeObj Write
+    makeBlockedApp args = Vector (-2) [toScheme nm, vars args]
+      where
+        vars : forall n . Vect n String -> SchemeObj Write
+        vars [] = Null
+        vars (x :: xs) = Cons (Var x) (vars xs)
+
+    bindArgs : Vect n String -> Vect n' String ->
+               Vect farity String -> SchemeObj Write
+    bindArgs [] done args = applyOp (makeBlockedApp args) fn (map Var args)
+    bindArgs (x :: xs) done args
+        = Vector (-9) [makeBlockedApp (reverse done),
+                       Lambda [x] (bindArgs xs (x :: done) args)]
diff --git a/src/Core/SchemeEval/Compile.idr b/src/Core/SchemeEval/Compile.idr
new file mode 100644
index 000000000..cfb5e72fe
--- /dev/null
+++ b/src/Core/SchemeEval/Compile.idr
@@ -0,0 +1,608 @@
+module Core.SchemeEval.Compile
+
+{- TODO:
+
+- Make a decent set of test cases
+- Option to keep vs discard FCs for faster quoting where we don't need FC
+
+Advanced TODO (possibly not worth it...):
+- Write a conversion check
+- Extend unification to use SObj; include SObj in Glued
+
+-}
+
+import Algebra.ZeroOneOmega
+
+import Core.CaseTree
+import Core.Context
+import Core.Core
+import Core.Directory
+import Core.SchemeEval.Builtins
+import Core.SchemeEval.ToScheme
+import Core.TT
+
+import Data.List
+
+import Libraries.Utils.Scheme
+import System.Info
+
+schString : String -> String
+schString s = concatMap okchar (unpack s)
+  where
+    okchar : Char -> String
+    okchar c = if isAlphaNum c || c =='_'
+                  then cast c
+                  else "C-" ++ show (cast {to=Int} c)
+
+schVarUN : UserName -> String
+schVarUN (Basic n) = schString n
+schVarUN (Field n) = "rf--" ++ schString n
+schVarUN Underscore = "_US_"
+
+schVarName : Name -> String
+schVarName (NS ns (UN n))
+   = schString (showNSWithSep "-" ns) ++ "-" ++ schVarUN n
+schVarName (NS ns n) = schString (showNSWithSep "-" ns) ++ "-" ++ schVarName n
+schVarName (UN n) = "u--" ++ schVarUN n
+schVarName (MN n i) = schString n ++ "-" ++ show i
+schVarName (PV n d) = "pat--" ++ schVarName n
+schVarName (DN _ n) = schVarName n
+schVarName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schVarName n
+schVarName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
+schVarName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y
+schVarName (Resolved i) = "fn--" ++ show i
+
+schName : Name -> String
+schName n = "ct-" ++ schVarName n
+
+export
+data Sym : Type where
+
+export
+nextName : Ref Sym Integer => Core Integer
+nextName
+    = do n <- get Sym
+         put Sym (n + 1)
+         pure n
+
+public export
+data SVar = Bound String | Free String
+
+Show SVar where
+  show (Bound x) = x
+  show (Free x) = "'" ++ x
+
+export
+getName : SVar -> String
+getName (Bound x) = x
+getName (Free x) = x
+
+public export
+data SchVars : List Name -> Type where
+     Nil : SchVars []
+     (::) : SVar -> SchVars ns -> SchVars (n :: ns)
+
+Show (SchVars ns) where
+  show xs = show (toList xs)
+    where
+      toList : forall ns . SchVars ns -> List String
+      toList [] = []
+      toList (Bound x :: xs) = x :: toList xs
+      toList (Free x :: xs) = "'x" :: toList xs
+
+getSchVar : {idx : _} -> (0 _ : IsVar n idx vars) -> SchVars vars -> String
+getSchVar First (Bound x :: xs) = x
+getSchVar First (Free x :: xs) = "'" ++ x
+getSchVar (Later p) (x :: xs) = getSchVar p xs
+
+{-
+
+Encoding of NF -> Scheme
+
+Maybe consider putting this back into a logical order, rather than the order
+I implemented them in...
+
+vector (tag>=0) name args == data constructor
+vector (-10) (name, arity) (args as list) == blocked meta application
+                   (needs to be same arity as block app, for ct-addArg)
+vector (-11) symbol (args as list) == blocked local application
+vector (-1) ... == type constructor
+vector (-2) name (args as list) == blocked application
+vector (-3) ... == Pi binder
+vector (-4) ... == delay arg
+vector (-5) ... == force arg
+vector (-6) = Erased
+vector (-7) = Type
+vector (-8) ... = Lambda
+vector (-9) blockedapp proc = Top level lambda (from a PMDef, so not expanded)
+vector (-12) ... = PVar binding
+vector (-13) ... = PVTy binding
+vector (-14) ... = PLet binding
+vector (-15) ... = Delayed
+
+vector (-100 onwards) ... = constants
+-}
+
+blockedAppWith : Name -> List (SchemeObj Write) -> SchemeObj Write
+blockedAppWith n args = Vector (-2) [toScheme n, vars args]
+  where
+    vars : List (SchemeObj Write) -> SchemeObj Write
+    vars [] = Null
+    vars (x :: xs) = Cons x (vars xs)
+
+blockedMetaApp : Name -> SchemeObj Write
+blockedMetaApp n
+    = Lambda ["arity-0"] (Vector (-10) [Cons (toScheme n) (Var "arity-0"),
+                                        Null])
+
+unload : SchemeObj Write -> List (SchemeObj Write) -> SchemeObj Write
+unload f [] = f
+unload f (a :: as) = unload (Apply (Var "ct-app") [f, a]) as
+
+compileConstant : FC -> Constant -> SchemeObj Write
+compileConstant fc (I x) = Vector (-100) [IntegerVal (cast x)]
+compileConstant fc (I8 x) = Vector (-101) [IntegerVal (cast x)]
+compileConstant fc (I16 x) = Vector (-102) [IntegerVal (cast x)]
+compileConstant fc (I32 x) = Vector (-103) [IntegerVal (cast x)]
+compileConstant fc (I64 x) = Vector (-104) [IntegerVal (cast x)]
+compileConstant fc (BI x) = Vector (-105) [IntegerVal x]
+compileConstant fc (B8 x) = Vector (-106) [IntegerVal (cast x)]
+compileConstant fc (B16 x) = Vector (-107) [IntegerVal (cast x)]
+compileConstant fc (B32 x) = Vector (-108) [IntegerVal (cast x)]
+compileConstant fc (B64 x) = Vector (-109) [IntegerVal (cast x)]
+compileConstant fc (Str x) = StringVal x
+compileConstant fc (Ch x) = CharVal x
+compileConstant fc (Db x) = FloatVal x
+-- Constant types get compiled as TyCon names, for matching purposes
+compileConstant fc t
+    = Vector (-1) [IntegerVal (cast (constTag t)),
+                   StringVal (show t),
+                   toScheme (UN (Basic (show t))),
+                   toScheme fc]
+
+compileStk : Ref Sym Integer =>
+             {auto c : Ref Ctxt Defs} ->
+             SchVars vars -> List (SchemeObj Write) -> Term vars ->
+             Core (SchemeObj Write)
+
+compilePiInfo : Ref Sym Integer =>
+                {auto c : Ref Ctxt Defs} ->
+                SchVars vars -> PiInfo (Term vars) ->
+                Core (PiInfo (SchemeObj Write))
+compilePiInfo svs Implicit = pure Implicit
+compilePiInfo svs Explicit = pure Explicit
+compilePiInfo svs AutoImplicit = pure AutoImplicit
+compilePiInfo svs (DefImplicit t)
+    = do t' <- compileStk svs [] t
+         pure (DefImplicit t')
+
+compileStk svs stk (Local fc isLet idx p)
+    = pure $ unload (Var (getSchVar p svs)) stk
+-- We are assuming that the bound name is a valid scheme symbol. We should
+-- only see this when inventing temporary names during quoting
+compileStk svs stk (Ref fc Bound name)
+    = pure $ unload (Symbol (show name)) stk
+compileStk svs stk (Ref fc (DataCon t a) name)
+    = if length stk == a -- inline it if it's fully applied
+         then pure $ Vector (cast t)
+                       (toScheme !(toResolvedNames name) ::
+                        toScheme fc :: stk)
+         else pure $ unload (Apply (Var (schName name)) []) stk
+compileStk svs stk (Ref fc (TyCon t a) name)
+    = if length stk == a -- inline it if it's fully applied
+         then pure $ Vector (-1)
+                       (IntegerVal (cast t) ::
+                        StringVal (show name) ::
+                        toScheme !(toResolvedNames name) ::
+                        toScheme fc :: stk)
+         else pure $ unload (Apply (Var (schName name)) []) stk
+compileStk svs stk (Ref fc x name)
+    = pure $ unload (Apply (Var (schName name)) []) stk
+compileStk svs stk (Meta fc name i xs)
+    = do xs' <- traverse (compileStk svs stk) xs
+         -- we encode the arity as first argument to the hole definition, which
+         -- helps in readback, so we have to apply the hole function to the
+         -- length of xs to be able to restore the Meta properly
+         pure $ unload (Apply (Var (schName name)) [])
+                       (IntegerVal (cast (length xs)) :: stk ++ xs')
+compileStk svs stk (Bind fc x (Let _ _ val _) scope)
+    = do i <- nextName
+         let x' = schVarName x ++ "-" ++ show i
+         val' <- compileStk svs [] val
+         sc' <- compileStk (Bound x' :: svs) [] scope
+         pure $ unload (Let x' val' sc') stk
+compileStk svs stk (Bind fc x (Pi _ rig p ty) scope)
+    = do i <- nextName
+         let x' = schVarName x ++ "-" ++ show i
+         ty' <- compileStk svs [] ty
+         sc' <- compileStk (Bound x' :: svs) [] scope
+         p' <- compilePiInfo svs p
+         pure $ Vector (-3) [Lambda [x'] sc', toScheme rig, toSchemePi p',
+                                              ty', toScheme x]
+compileStk svs stk (Bind fc x (PVar _ rig p ty) scope)
+    = do i <- nextName
+         let x' = schVarName x ++ "-" ++ show i
+         ty' <- compileStk svs [] ty
+         sc' <- compileStk (Bound x' :: svs) [] scope
+         p' <- compilePiInfo svs p
+         pure $ Vector (-12) [Lambda [x'] sc', toScheme rig, toSchemePi p',
+                                               ty', toScheme x]
+compileStk svs stk (Bind fc x (PVTy _ rig ty) scope)
+    = do i <- nextName
+         let x' = schVarName x ++ "-" ++ show i
+         ty' <- compileStk svs [] ty
+         sc' <- compileStk (Bound x' :: svs) [] scope
+         pure $ Vector (-13) [Lambda [x'] sc', toScheme rig, ty', toScheme x]
+compileStk svs stk (Bind fc x (PLet _ rig val ty) scope) -- we only see this on LHS
+    = do i <- nextName
+         let x' = schVarName x ++ "-" ++ show i
+         val' <- compileStk svs [] val
+         ty' <- compileStk svs [] ty
+         sc' <- compileStk (Bound x' :: svs) [] scope
+         pure $ Vector (-14) [Lambda [x'] sc', toScheme rig, val', ty', toScheme x]
+compileStk svs [] (Bind fc x (Lam _ rig p ty) scope)
+    = do i <- nextName
+         let x' = schVarName x ++ "-" ++ show i
+         ty' <- compileStk svs [] ty
+         sc' <- compileStk (Bound x' :: svs) [] scope
+         p' <- compilePiInfo svs p
+         pure $ Vector (-8) [Lambda [x'] sc', toScheme rig, toSchemePi p',
+                                              ty', toScheme x]
+compileStk svs (s :: stk) (Bind fc x (Lam _ _ _ _) scope)
+    = do i <- nextName
+         let x' = schVarName x ++ "-" ++ show i
+         sc' <- compileStk (Bound x' :: svs) stk scope
+         pure $ Apply (Lambda [x'] sc') [s]
+compileStk svs stk (App fc fn arg)
+    = compileStk svs (!(compileStk svs [] arg) :: stk) fn
+-- We're only using this evaluator for REPL and typechecking, not for
+-- tidying up definitions or LHSs, so we'll always remove As patterns
+compileStk svs stk (As fc x as pat) = compileStk svs stk pat
+compileStk svs stk (TDelayed fc r ty)
+    = do ty' <- compileStk svs stk ty
+         pure $ Vector (-15) [toScheme r, ty']
+compileStk svs stk (TDelay fc r ty arg)
+    = do ty' <- compileStk svs [] ty
+         arg' <- compileStk svs [] arg
+         pure $ Vector (-4) [toScheme r, toScheme fc,
+                             Lambda [] ty', Lambda [] arg']
+compileStk svs stk (TForce fc x tm)
+    = do tm' <- compileStk svs [] tm
+         pure $ Apply (Var "ct-doForce")
+                      [tm',
+                      Vector (-5) [toScheme x, toScheme fc, Lambda [] tm']]
+compileStk svs stk (PrimVal fc c) = pure $ compileConstant fc c
+compileStk svs stk (Erased fc imp) = pure $ Vector (-6) [toScheme fc, toScheme imp]
+compileStk svs stk (TType fc) = pure $ Vector (-7) [toScheme fc]
+
+export
+compile : Ref Sym Integer =>
+          {auto c : Ref Ctxt Defs} ->
+          SchVars vars -> Term vars -> Core (SchemeObj Write)
+compile vars tm = compileStk vars [] tm
+
+getArgName : Ref Sym Integer =>
+             Core Name
+getArgName
+    = do i <- nextName
+         pure (MN "carg" (cast i))
+
+extend : Ref Sym Integer =>
+         (args : List Name) -> SchVars vars ->
+         Core (List Name, SchVars (args ++ vars))
+extend [] svs = pure ([], svs)
+extend (arg :: args) svs
+    = do n <- getArgName
+         (args', svs') <- extend args svs
+         pure (n :: args', Bound (schVarName n) :: svs')
+
+compileCase : Ref Sym Integer =>
+              {auto c : Ref Ctxt Defs} ->
+              (blocked : SchemeObj Write) ->
+              SchVars vars -> CaseTree vars -> Core (SchemeObj Write)
+compileCase blk svs (Case idx p scTy xs)
+    = case !(caseType xs) of
+           CON => toSchemeConCases idx p xs
+           TYCON => toSchemeTyConCases idx p xs
+           DELAY => toSchemeDelayCases idx p xs
+           CONST => toSchemeConstCases idx p xs
+  where
+    data CaseType = CON | TYCON | DELAY | CONST
+
+    caseType : List (CaseAlt vs) -> Core CaseType
+    caseType [] = pure CON
+    caseType (ConCase x tag args y :: xs)
+        = do defs <- get Ctxt
+             Just gdef <- lookupCtxtExact x (gamma defs)
+                  | Nothing => pure TYCON -- primitive type match
+             case definition gdef of
+                  DCon{} => pure CON
+                  TCon{} => pure TYCON
+                  _ => pure CON -- or maybe throw?
+    caseType (DelayCase ty arg x :: xs) = pure DELAY
+    caseType (ConstCase x y :: xs) = pure CONST
+    caseType (DefaultCase x :: xs) = caseType xs
+
+    makeDefault : List (CaseAlt vars) -> Core (SchemeObj Write)
+    makeDefault [] = pure blk
+    makeDefault (DefaultCase sc :: xs) = compileCase blk svs sc
+    makeDefault (_ :: xs) = makeDefault xs
+
+    toSchemeConCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->
+                       List (CaseAlt vars) -> Core (SchemeObj Write)
+    toSchemeConCases idx p alts
+        = do let var = getSchVar p svs
+             alts' <- traverse (makeAlt var) alts
+             let caseblock
+                    = Case (Apply (Var "vector-ref") [Var var, IntegerVal 0])
+                           (mapMaybe id alts')
+                           (Just !(makeDefault alts))
+             pure $ If (Apply (Var "ct-isDataCon") [Var var])
+                       caseblock
+                       blk
+      where
+        project : Int -> String -> List Name ->
+                  SchemeObj Write -> SchemeObj Write
+        project i var [] body = body
+        project i var (n :: ns) body
+            = Let (schVarName n)
+                  (Apply (Var "vector-ref") [Var var, IntegerVal (cast i)])
+                  (project (i + 1) var ns body)
+
+        bindArgs : String -> (args : List Name) -> CaseTree (args ++ vars) ->
+                   Core (SchemeObj Write)
+        bindArgs var args sc
+            = do (bind, svs') <- extend args svs
+                 project 3 var bind <$> compileCase blk svs' sc
+
+        makeAlt : String -> CaseAlt vars ->
+                  Core (Maybe (SchemeObj Write, SchemeObj Write))
+        makeAlt var (ConCase n t args sc)
+            = pure $ Just (IntegerVal (cast t), !(bindArgs var args sc))
+        -- TODO: Matching on types, including ->
+        makeAlt var _ = pure Nothing
+
+    toSchemeTyConCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->
+                         List (CaseAlt vars) -> Core (SchemeObj Write)
+    toSchemeTyConCases idx p alts
+        = do let var = getSchVar p svs
+             alts' <- traverse (makeAlt var) alts
+             caseblock <- addPiMatch var alts
+                      -- work on the name, so the 2nd arg
+                            (Case (Apply (Var "vector-ref") [Var var, IntegerVal 2])
+                               (mapMaybe id alts')
+                               (Just !(makeDefault alts)))
+             pure $ If (Apply (Var "ct-isTypeMatchable") [Var var])
+                       caseblock
+                       blk
+      where
+        project : Int -> String -> List Name ->
+                  SchemeObj Write -> SchemeObj Write
+        project i var [] body = body
+        project i var (n :: ns) body
+            = Let (schVarName n)
+                  (Apply (Var "vector-ref") [Var var, IntegerVal (cast i)])
+                  (project (i + 1) var ns body)
+
+        bindArgs : String -> (args : List Name) -> CaseTree (args ++ vars) ->
+                   Core (SchemeObj Write)
+        bindArgs var args sc
+            = do (bind, svs') <- extend args svs
+                 project 5 var bind <$> compileCase blk svs' sc
+
+        makeAlt : String -> CaseAlt vars ->
+                  Core (Maybe (SchemeObj Write, SchemeObj Write))
+        makeAlt var (ConCase (UN (Basic "->")) t [_, _] sc)
+            = pure Nothing -- do this in 'addPiMatch' below, since the
+                           -- representation is different
+        makeAlt var (ConCase n t args sc)
+            = pure $ Just (StringVal (show n), !(bindArgs var args sc))
+        makeAlt var _ = pure Nothing
+
+        addPiMatch : String -> List (CaseAlt vars) -> SchemeObj Write ->
+                     Core (SchemeObj Write)
+        addPiMatch var [] def = pure def
+        -- t is a function type, and conveniently the scope of a pi
+        -- binding is represented as a function. Lucky us! So we just need
+        -- to extract it then evaluate the scope
+        addPiMatch var (ConCase (UN (Basic "->")) _ [s, t] sc :: _) def
+            = do sn <- getArgName
+                 tn <- getArgName
+                 let svs' = Bound (schVarName sn) ::
+                              Bound (schVarName tn) :: svs
+                 sc' <- compileCase blk svs' sc
+                 pure $ If (Apply (Var "ct-isPi") [Var var])
+                           (Let (schVarName sn) (Apply (Var "vector-ref") [Var var, IntegerVal 4]) $
+                            Let (schVarName tn) (Apply (Var "vector-ref") [Var var, IntegerVal 1]) $
+                            sc')
+                           def
+        addPiMatch var (x :: xs) def = addPiMatch var xs def
+
+    toSchemeConstCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->
+                         List (CaseAlt vars) -> Core (SchemeObj Write)
+    toSchemeConstCases x p alts
+        = do let var = getSchVar p svs
+             alts' <- traverse (makeAlt var) alts
+             let caseblock
+                    = Cond (mapMaybe id alts')
+                           (Just !(makeDefault alts))
+             pure $ If (Apply (Var "ct-isConstant") [Var var])
+                       caseblock
+                       blk
+     where
+        makeAlt : String -> CaseAlt vars ->
+                  Core (Maybe (SchemeObj Write, SchemeObj Write))
+        makeAlt var (ConstCase c sc)
+            = do sc' <- compileCase blk svs sc
+                 pure (Just (Apply (Var "equal?")
+                               [Var var, compileConstant emptyFC c], sc'))
+        makeAlt var _ = pure Nothing
+
+    toSchemeDelayCases : (idx : Nat) -> (0 p : IsVar n idx vars) ->
+                         List (CaseAlt vars) -> Core (SchemeObj Write)
+    -- there will only ever be one, or a default case
+    toSchemeDelayCases idx p (DelayCase ty arg sc :: rest)
+        = do let var = getSchVar p svs
+             tyn <- getArgName
+             argn <- getArgName
+             let svs' = Bound (schVarName tyn) ::
+                          Bound (schVarName argn) :: svs
+             sc' <- compileCase blk svs' sc
+             pure $ If (Apply (Var "ct-isDelay") [Var var])
+                       (Let (schVarName tyn)
+                           (Apply (Apply (Var "vector-ref") [Var var, IntegerVal 3]) []) $
+                        Let (schVarName argn)
+                           (Apply (Apply (Var "vector-ref") [Var var, IntegerVal 4]) []) $
+                         sc')
+                       blk
+    toSchemeDelayCases idx p (_ :: rest) = toSchemeDelayCases idx p rest
+    toSchemeDelayCases idx p _ = pure Null
+
+compileCase blk vars (STerm _ tm) = compile vars tm
+compileCase blk vars _ = pure blk
+
+varObjs : SchVars ns -> List (SchemeObj Write)
+varObjs [] = []
+varObjs (x :: xs) = Var (show x) :: varObjs xs
+
+mkArgs : (ns : List Name) -> Core (SchVars ns)
+mkArgs [] = pure []
+mkArgs (x :: xs)
+    = pure $ Bound (schVarName x) :: !(mkArgs xs)
+
+bindArgs : Name ->
+           (todo : SchVars ns) ->
+           (done : List (SchemeObj Write)) ->
+           SchemeObj Write -> SchemeObj Write
+bindArgs n [] done body = body
+bindArgs n (x :: xs) done body
+    = Vector (-9) [blockedAppWith n (reverse done),
+                   Lambda [show x]
+                      (bindArgs n xs (Var (show x) :: done) body)]
+
+compileBody : {auto c : Ref Ctxt Defs} ->
+              Bool -> -- okay to reduce (if False, block)
+              Name -> Def -> Core (SchemeObj Write)
+compileBody _ n None = pure $ blockedAppWith n []
+compileBody redok n (PMDef pminfo args treeCT treeRT pats)
+    = do i <- newRef Sym 0
+         argvs <- mkArgs args
+         let blk = blockedAppWith n (varObjs argvs)
+         body <- compileCase blk argvs treeCT
+         let body' = if redok
+                        then If (Apply (Var "ct-isBlockAll") []) blk body
+                        else blk
+         -- If it arose from a hole, we need to take an extra argument for
+         -- the arity since that's what Meta gets applied to
+         case holeInfo pminfo of
+              NotHole => pure (bindArgs n argvs [] body')
+              SolvedHole _ => pure (Lambda ["h-0"] (bindArgs n argvs [] body'))
+compileBody _ n (ExternDef arity) = pure $ blockedAppWith n []
+compileBody _ n (ForeignDef arity xs) = pure $ blockedAppWith n []
+compileBody _ n (Builtin x) = pure $ compileBuiltin n x
+compileBody _ n (DCon tag Z newtypeArg)
+    = pure $ Vector (cast tag) [toScheme !(toResolvedNames n), toScheme emptyFC]
+compileBody _ n (DCon tag arity newtypeArg)
+    = do let args = mkArgNs 0 arity
+         argvs <- mkArgs args
+         let body
+               = Vector (cast tag)
+                        (toScheme n :: toScheme emptyFC ::
+                             map (Var . schVarName) args)
+         pure (bindArgs n argvs [] body)
+  where
+    mkArgNs : Int -> Nat -> List Name
+    mkArgNs i Z = []
+    mkArgNs i (S k) = MN "arg" i :: mkArgNs (i+1) k
+compileBody _ n (TCon tag Z parampos detpos flags mutwith datacons detagabbleBy)
+    = pure $ Vector (-1) [IntegerVal (cast tag), StringVal (show n),
+                          toScheme n, toScheme emptyFC]
+compileBody _ n (TCon tag arity parampos detpos flags mutwith datacons detagabbleBy)
+    = do let args = mkArgNs 0 arity
+         argvs <- mkArgs args
+         let body
+               = Vector (-1)
+                        (IntegerVal (cast tag) ::
+                         StringVal (show n) ::
+                          toScheme n :: toScheme emptyFC ::
+                            map (Var . schVarName) args)
+         pure (bindArgs n argvs [] body)
+  where
+    mkArgNs : Int -> Nat -> List Name
+    mkArgNs i Z = []
+    mkArgNs i (S k) = MN "arg" i :: mkArgNs (i+1) k
+compileBody _ n (Hole numlocs x) = pure $ blockedMetaApp n
+compileBody _ n (BySearch x maxdepth defining) = pure $ blockedMetaApp n
+compileBody _ n (Guess guess envbind constraints) = pure $ blockedMetaApp n
+compileBody _ n ImpBind = pure $ blockedMetaApp n
+compileBody _ n Delayed = pure $ blockedMetaApp n
+
+export
+compileDef : {auto c : Ref Ctxt Defs} -> SchemeMode -> Name -> Core ()
+compileDef mode n_in
+    = do n <- toFullNames n_in -- this is handy for readability of generated names
+                     -- we used resolved names for blocked names, though, as
+                     -- that's a bit better for performance
+         defs <- get Ctxt
+         Just def <- lookupCtxtExact n (gamma defs)
+              | Nothing => throw (UndefinedName emptyFC n)
+
+         let True = case schemeExpr def of
+                         Nothing => True
+                         Just (cmode, def) => cmode /= mode
+               | _ => pure () -- already done
+         -- If we're in BlockExport mode, check whether the name is
+         -- available for reduction.
+         let redok = mode == EvalAll ||
+                       reducibleInAny (currentNS defs :: nestedNS defs)
+                                      (fullname def)
+                                      (visibility def)
+         -- 'n' is used in compileBody for generating names for readback,
+         -- and reading back resolved names is quicker because it's just
+         -- an integer
+         b <- compileBody redok !(toResolvedNames n) !(toFullNames (definition def))
+         let schdef = Define (schName n) b
+
+         -- Add the new definition to the current scheme runtime
+         Just obj <- coreLift $ evalSchemeObj schdef
+              | Nothing => throw (InternalError ("Compiling " ++ show n ++ " failed"))
+
+         -- Record that this one is done
+         ignore $ addDef n (record { schemeExpr = Just (mode, schdef) } def)
+
+initEvalWith : {auto c : Ref Ctxt Defs} ->
+               String -> Core Bool
+initEvalWith "chez"
+    = do defs <- get Ctxt
+         if defs.schemeEvalLoaded
+            then pure True
+            else
+             catch (do f <- readDataFile "chez/ct-support.ss"
+                       Just _ <- coreLift $ evalSchemeStr $ "(begin " ++ f ++ ")"
+                            | Nothing => pure False
+                       put Ctxt (record { schemeEvalLoaded = True } defs)
+                       pure True)
+                (\err => pure False)
+initEvalWith "racket"
+    = do defs <- get Ctxt
+         if defs.schemeEvalLoaded
+            then pure True
+            else
+             catch (do f <- readDataFile "racket/ct-support.rkt"
+                       Just _ <- coreLift $ evalSchemeStr $ "(begin " ++ f ++ ")"
+                            | Nothing => pure False
+                       put Ctxt (record { schemeEvalLoaded = True } defs)
+                       pure True)
+                (\err => do coreLift $ printLn err
+                            pure False)
+initEvalWith _ = pure False -- only works on Chez for now
+
+-- Initialise the internal functions we need to build/extend blocked
+-- applications
+-- These are in a support file, chez/support.ss. Returns True if loading
+-- and processing succeeds. If it fails, which it probably will during a
+-- bootstrap build at least, we can fall back to the default evaluator.
+export
+initialiseSchemeEval : {auto c : Ref Ctxt Defs} ->
+                       Core Bool
+initialiseSchemeEval = initEvalWith codegen
diff --git a/src/Core/SchemeEval/Evaluate.idr b/src/Core/SchemeEval/Evaluate.idr
new file mode 100644
index 000000000..70460a80f
--- /dev/null
+++ b/src/Core/SchemeEval/Evaluate.idr
@@ -0,0 +1,691 @@
+module Core.SchemeEval.Evaluate
+
+import Core.Context
+import Core.Context.Log
+import Core.Core
+import Core.Env
+import Core.SchemeEval.Compile
+import Core.SchemeEval.ToScheme
+import Core.TT
+
+import Libraries.Data.NameMap
+import Libraries.Utils.Scheme
+
+public export
+data SObj : List Name -> Type where
+     MkSObj : ForeignObj -> SchVars vars -> SObj vars
+
+-- Values, which we read off evaluated scheme objects.
+-- Unfortunately we can't quite get away with using Core.Value.NF because
+-- of the different representation of closures. Also, we're call by value
+-- when going via scheme, so this structure is a little bit simpler (not
+-- recording a LocalEnv for example).
+mutual
+  public export
+  data SHead : List Name -> Type where
+       SLocal : (idx : Nat) -> (0 p : IsVar nm idx vars) -> SHead vars
+       SRef : NameType -> Name -> SHead vars
+       SMeta : Name -> Int -> List (Core (SNF vars)) -> SHead vars
+
+  public export
+  data SNF : List Name -> Type where
+       SBind    : FC -> (x : Name) -> Binder (SNF vars) ->
+                  (SObj vars -> Core (SNF vars)) -> SNF vars
+       SApp     : FC -> SHead vars -> List (Core (SNF vars)) -> SNF vars
+       SDCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->
+                  List (Core (SNF vars)) -> SNF vars
+       STCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->
+                  List (Core (SNF vars)) -> SNF vars
+       SDelayed : FC -> LazyReason -> SNF vars -> SNF vars
+       SDelay   : FC -> LazyReason -> Core (SNF vars) -> Core (SNF vars) ->
+                  SNF vars
+       SForce   : FC -> LazyReason -> SNF vars -> SNF vars
+       SPrimVal : FC -> Constant -> SNF vars
+       SErased  : FC -> (imp : Bool) -> SNF vars
+       SType    : FC -> SNF vars
+
+getAllNames : {auto c : Ref Ctxt Defs} ->
+              NameMap () -> List Name -> Core (NameMap ())
+getAllNames done [] = pure done
+getAllNames done (x :: xs)
+    = do let Nothing = lookup x done
+             | _ => getAllNames done xs
+         defs <- get Ctxt
+         Just gdef <- lookupCtxtExact x (gamma defs)
+             | _ => getAllNames done xs
+         getAllNames (insert x () done) (xs ++ keys (refersTo gdef))
+
+-- Evaluate a term via scheme. This will throw if the backend doesn't
+-- support scheme evaluation, so callers should have checked first and fall
+-- back to the internal (slow!) evaluator if initialisation fails.
+export
+seval : {auto c : Ref Ctxt Defs} ->
+        SchemeMode -> Env Term vars -> Term vars -> Core (SObj vars)
+seval mode env tm
+    = do -- Check the evaluator is initialised. This will fail if the backend
+         -- doesn't support scheme evaluation.
+         True <- logTimeWhen False "Scheme eval" initialiseSchemeEval
+              | False => throw (InternalError "Loading scheme support failed")
+
+         -- make sure all the names in the term are compiled
+         -- We need to recheck in advance, since definitions might have changed
+         -- since we last evaluated a name, and we might have evaluated the
+         -- name in a different mode
+         let ms = getRefs (MN "" 0) tm
+         let rs = addMetas ms tm
+         names <- getAllNames empty (keys rs)
+         traverse_ (compileDef mode) (keys names)
+
+         i <- newRef Sym 0
+         (bind, schEnv) <- mkEnv env id
+         stm <- compile schEnv !(toFullNames tm)
+         Just res <- coreLift $ evalSchemeObj (bind stm)
+              | Nothing => throw (InternalError "Compiling expression failed")
+         pure (MkSObj res schEnv)
+  where
+    mkEnv : forall vars . Ref Sym Integer =>
+            Env Term vars ->
+            (SchemeObj Write -> SchemeObj Write) ->
+            Core (SchemeObj Write -> SchemeObj Write, SchVars vars)
+    mkEnv [] k = pure (k, [])
+    mkEnv (Let fc c val ty :: es) k
+        = do i <- nextName
+             (bind, vs) <- mkEnv es k
+             val' <- compile vs val
+             let n = "let-var-" ++ show i
+             pure (\x => Let n val' (bind x), Bound n :: vs)
+    mkEnv (_ :: es) k
+        = do i <- nextName
+             (bind, vs) <- mkEnv es k
+             pure (bind, Free ("free-" ++ show i) :: vs)
+
+invalid : Core (Term vs)
+invalid = pure (Erased emptyFC False)
+
+invalidS : Core (SNF vs)
+invalidS = pure (SErased emptyFC False)
+
+getArgList : ForeignObj -> List ForeignObj
+getArgList obj
+    = if isPair obj
+         then unsafeFst obj :: getArgList (unsafeSnd obj)
+         else []
+
+mutual
+  -- We don't use decodeObj because then we have to traverse the term twice.
+  -- Instead, decode the ForeignObj directly, which is uglier but faster.
+  quoteVector : Ref Sym Integer =>
+                Ref Ctxt Defs =>
+                SchVars (outer ++ vars) ->
+                Integer -> List ForeignObj ->
+                Core (Term (outer ++ vars))
+  quoteVector svs (-2) [_, fname_in, args_in] -- Blocked app
+      = do let Just fname = fromScheme (decodeObj fname_in)
+                    | _ => invalid
+           let argList = getArgList args_in
+           args <- traverse (quote' svs) argList
+           pure (apply emptyFC (Ref emptyFC Func fname) args)
+  quoteVector svs (-10) [_, fn_arity, args_in] -- Blocked meta app
+      = do let Just (fname, arity_in) = the (Maybe (Name, Integer)) $
+                                            fromScheme (decodeObj fn_arity)
+                    | _ => invalid
+           let arity : Nat = cast arity_in
+           let argList = getArgList args_in
+           args <- traverse (quote' svs) argList
+           defs <- get Ctxt
+           fnameF <- toFullNames fname
+           (idx, _) <- getPosition fname (gamma defs)
+           pure (apply emptyFC (Meta emptyFC fnameF idx (take arity args))
+                               (drop arity args))
+  quoteVector svs (-11) [_, loc_in, args_in] -- Blocked local var application
+      = do loc <- quote' svs loc_in
+           let argList = getArgList args_in
+           args <- traverse (quote' svs) argList
+           pure (apply emptyFC loc args)
+  quoteVector svs (-1) (_ :: tag_in :: strtag :: cname_in :: fc_in :: args_in) -- TyCon
+      = do let Just cname = fromScheme (decodeObj cname_in)
+                    | Nothing => invalid
+           let Just tag = the (Maybe Integer) $ fromScheme (decodeObj tag_in)
+                    | Nothing => invalid
+           let fc = emptyFC -- case fromScheme (decodeObj fc_in) of
+--                            Just fc => fc
+--                            _ => emptyFC
+           args <- traverse (quote' svs) args_in
+           pure (apply fc (Ref fc (TyCon (cast tag) (length args)) cname)
+                           args)
+  quoteVector svs (-15) [_, r_in, ty_in] -- Delayed
+      = do ty <- quote' svs ty_in
+           let r = case fromScheme (decodeObj r_in) of
+                        Just r => r
+                        _ => LUnknown
+           pure (TDelayed emptyFC r ty)
+  quoteVector svs (-4) [_, r_in, fc_in, ty_in, tm_in] -- Delay
+      = do -- Block further reduction under tm_in
+           Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #t)"
+                | Nothing => invalid
+           let Procedure tmproc = decodeObj tm_in
+                | _ => invalid
+           let Procedure typroc = decodeObj ty_in
+                | _ => invalid
+           tm <- quote' svs (unsafeForce tmproc)
+           ty <- quote' svs (unsafeForce typroc)
+           -- Turn blocking off again
+           Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #f)"
+                | Nothing => invalid
+           let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           let r = case fromScheme (decodeObj r_in) of
+                        Just r => r
+                        _ => LUnknown
+           pure (TDelay fc r ty tm)
+  quoteVector svs (-5) [_, r_in, fc_in, tm_in] -- Force
+      = do -- The thing we were trying to force was stuck. Corresponding to
+           -- Core.Normalise, reduce it anyway here (so no ct-blockAll like above)
+           tm <- quote' svs tm_in
+           let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           let r = case fromScheme (decodeObj r_in) of
+                        Just r => r
+                        _ => LUnknown
+           pure (TForce fc r tm)
+  quoteVector svs (-6) [_, fc_in, imp_in] -- Erased
+      = do let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           let imp = case fromScheme (decodeObj imp_in) of
+                          Just imp => imp
+                          _ => False
+           pure (Erased fc imp)
+  quoteVector svs (-7) [_, fc_in] -- Type
+      = do let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           pure (TType fc)
+  quoteVector svs (-8) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Lambda
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- quote' svs ty_in
+           pi <- quotePiInfo svs pi_in
+           quoteBinder svs Lam proc_in rig pi ty name
+  quoteVector svs (-3) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Pi
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- quote' svs ty_in
+           pi <- quotePiInfo svs pi_in
+           quoteBinder svs Pi proc_in rig pi ty name
+  quoteVector svs (-12) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- PVar
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- quote' svs ty_in
+           pi <- quotePiInfo svs pi_in
+           quoteBinder svs PVar proc_in rig pi ty name
+  quoteVector svs (-13) [_, proc_in, rig_in, ty_in, name_in] -- PVTy
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- quote' svs ty_in
+           quoteBinder svs (\fc, r, p, t => PVTy fc r t) proc_in rig Explicit ty name
+  quoteVector svs (-14) [_, proc_in, rig_in, val_in, ty_in, name_in] -- PLet
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- quote' svs ty_in
+           val <- quote' svs val_in
+           quotePLet svs proc_in rig val ty name
+  quoteVector svs (-9) [_, blocked, _] -- Blocked top level lambda
+      = quote' svs blocked
+  quoteVector svs (-100) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (I x')
+  quoteVector svs (-101) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (I8 x')
+  quoteVector svs (-102) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (I16 x')
+  quoteVector svs (-103) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (I32 x')
+  quoteVector svs (-104) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (I64 x')
+  quoteVector svs (-105) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (BI x')
+  quoteVector svs (-106) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (B8 x')
+  quoteVector svs (-107) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (B16 x')
+  quoteVector svs (-108) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (B32 x')
+  quoteVector svs (-109) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalid
+           pure $ PrimVal emptyFC (B64 x')
+  quoteVector svs tag (_ :: cname_in :: fc_in :: args_in) -- DataCon
+      = if tag >= 0
+           then do
+             let Just cname = fromScheme (decodeObj cname_in)
+                    | Nothing => invalid
+             let fc = emptyFC -- case fromScheme (decodeObj fc_in) of
+--                            Just fc => fc
+--                            _ => emptyFC
+             args <- traverse (quote' svs) args_in
+             pure (apply fc (Ref fc (DataCon (cast tag) (length args)) cname)
+                            args)
+           else invalid
+  quoteVector _ _ _ = invalid
+
+  quotePiInfo : Ref Sym Integer =>
+                Ref Ctxt Defs =>
+                SchVars (outer ++ vars) ->
+                ForeignObj ->
+                Core (PiInfo (Term (outer ++ vars)))
+  quotePiInfo svs obj
+      = if isInteger obj
+           then case unsafeGetInteger obj of
+                     0 => pure Implicit
+                     1 => pure Explicit
+                     2 => pure AutoImplicit
+                     _ => pure Explicit
+           else if isBox obj
+                   then do t' <- quote' svs (unsafeUnbox obj)
+                           pure (DefImplicit t')
+           else pure Explicit
+
+  quoteBinder : Ref Sym Integer =>
+                Ref Ctxt Defs =>
+                SchVars (outer ++ vars) ->
+                (forall ty . FC -> RigCount -> PiInfo ty -> ty -> Binder ty) ->
+                ForeignObj -> -- body of binder, represented as a function
+                RigCount ->
+                PiInfo (Term (outer ++ vars)) ->
+                Term (outer ++ vars) -> -- decoded type
+                Name -> -- bound name
+                Core (Term (outer ++ vars))
+  quoteBinder svs binder proc_in r pi ty name
+      = do let Procedure proc = decodeObj proc_in
+                    | _ => invalid
+           i <- nextName
+           let n = show name ++ "-" ++ show i
+           let sc = unsafeApply proc (makeSymbol n)
+           sc' <- quote' {outer = name :: outer} (Bound n :: svs) sc
+           pure (Bind emptyFC name
+                      (binder emptyFC r pi ty)
+                      sc')
+
+  quotePLet : Ref Sym Integer =>
+              Ref Ctxt Defs =>
+              SchVars (outer ++ vars) ->
+              ForeignObj -> -- body of binder, represented as a function
+              RigCount ->
+              Term (outer ++ vars) -> -- decoded type
+              Term (outer ++ vars) -> -- decoded value
+              Name -> -- bound name
+              Core (Term (outer ++ vars))
+  quotePLet svs proc_in r val ty name
+      = do let Procedure proc = decodeObj proc_in
+                    | _ => invalid
+           i <- nextName
+           let n = show name ++ "-" ++ show i
+           let sc = unsafeApply proc (makeSymbol n)
+           sc' <- quote' {outer = name :: outer} (Bound n :: svs) sc
+           pure (Bind emptyFC name
+                      (PLet emptyFC r val ty)
+                      sc')
+
+  quote' : Ref Sym Integer =>
+           Ref Ctxt Defs =>
+           SchVars (outer ++ vars) -> ForeignObj ->
+           Core (Term (outer ++ vars))
+  quote' svs obj
+      = if isVector obj
+           then quoteVector svs (unsafeGetInteger (unsafeVectorRef obj 0))
+                                (unsafeVectorToList obj)
+        else if isProcedure obj then quoteBinder svs Lam obj top
+                                              Explicit
+                                              (Erased emptyFC False)
+                                              (UN (Basic "x"))
+        else if isSymbol obj then pure $ findName svs (unsafeReadSymbol obj)
+        else if isFloat obj then pure $ PrimVal emptyFC (Db (unsafeGetFloat obj))
+        else if isInteger obj then pure $ PrimVal emptyFC (I (cast (unsafeGetInteger obj)))
+        else if isString obj then pure $ PrimVal emptyFC (Str (unsafeGetString obj))
+        else if isChar obj then pure $ PrimVal emptyFC (Ch (unsafeGetChar obj))
+        else invalid
+    where
+      findName : forall vars . SchVars vars -> String -> Term vars
+      findName [] n = Ref emptyFC Func (UN (Basic n))
+      findName (x :: xs) n
+          = if getName x == n
+               then Local emptyFC Nothing _ First
+               else let Local fc loc _ p = findName xs n
+                           | _ => Ref emptyFC Func (UN (Basic n)) in
+                        Local fc loc _ (Later p)
+
+      readVector : Integer -> Integer -> ForeignObj -> List ForeignObj
+      readVector len i obj
+          = if len == i
+               then []
+               else unsafeVectorRef obj i :: readVector len (i + 1) obj
+
+-- Quote a scheme value directly back to a Term, without making an SNF
+-- in between. This is what we want if we're just looking for a normal
+-- form immediately (so, evaluating under binders)
+export
+quoteObj : {auto c : Ref Ctxt Defs} ->
+           SObj vars -> Core (Term vars)
+quoteObj (MkSObj val schEnv)
+    = do i <- newRef Sym 0
+         quote' {outer = []} schEnv val
+
+mutual
+  snfVector : Ref Ctxt Defs =>
+              SchVars vars ->
+              Integer -> List ForeignObj ->
+              Core (SNF vars)
+  snfVector svs (-2) [_, fname_in, args_in] -- Blocked application
+      = do let Just fname = fromScheme (decodeObj fname_in)
+                    | _ => invalidS
+           let args = map (snf' svs) (getArgList args_in)
+           pure (SApp emptyFC (SRef Func fname) args)
+  snfVector svs (-10) [_, fn_arity, args_in] -- Block meta app
+      = do let Just (fname, arity_in) = the (Maybe (Name, Integer)) $
+                                            fromScheme (decodeObj fn_arity)
+                    | _ => invalidS
+           let arity : Nat = cast arity_in
+           let args = map (snf' svs) (getArgList args_in)
+           defs <- get Ctxt
+           fnameF <- toFullNames fname
+           (idx, _) <- getPosition fnameF (gamma defs)
+           pure (SApp emptyFC (SMeta fnameF idx (take arity args))
+                               (drop arity args))
+  snfVector svs (-11) [_, loc_in, args_in] -- Blocked local var application
+      = do SApp fc loc args <- snf' svs loc_in
+                | _ => invalidS
+           let args' = map (snf' svs) (getArgList args_in)
+           pure (SApp fc loc (args ++ args'))
+  snfVector svs (-1) (_ :: tag_in :: strtag :: cname_in :: fc_in :: args_in) -- TyCon
+      = do let Just cname = fromScheme (decodeObj cname_in)
+                    | Nothing => invalidS
+           let Just tag = the (Maybe Integer) $ fromScheme (decodeObj tag_in)
+                    | Nothing => invalidS
+           let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           let args = map (snf' svs) args_in
+           pure (STCon fc cname (cast tag) (length args) args)
+  snfVector svs (-15) [_, r_in, ty_in] -- Delayed
+      = do ty <- snf' svs ty_in
+           let r = case fromScheme (decodeObj r_in) of
+                        Just r => r
+                        _ => LUnknown
+           pure (SDelayed emptyFC r ty)
+  snfVector svs (-4) [_, r_in, fc_in, ty_in, tm_in] -- Delay
+      = do let Procedure tmproc = decodeObj tm_in
+                | _ => invalidS
+           let Procedure typroc = decodeObj ty_in
+                | _ => invalidS
+           -- Block further reduction under tm_in
+           let tm = do Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #t)"
+                            | Nothing => invalidS
+                       res <- snf' svs (unsafeForce tmproc)
+                       Just _ <- coreLift $ evalSchemeStr "(ct-setBlockAll #f)"
+                            | Nothing => invalidS
+                       pure res
+           let ty = snf' svs (unsafeForce typroc)
+           let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           let r = case fromScheme (decodeObj r_in) of
+                        Just r => r
+                        _ => LUnknown
+           pure (SDelay fc r ty tm)
+  snfVector svs (-5) [_, r_in, fc_in, tm_in] -- Force
+      = do -- The thing we were trying to force was stuck. Corresponding to
+           -- Core.Normalise, reduce it anyway here (so no ct-blockAll like above)
+           tm <- snf' svs tm_in
+           let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           let r = case fromScheme (decodeObj r_in) of
+                        Just r => r
+                        _ => LUnknown
+           pure (SForce fc r tm)
+  snfVector svs (-6) [_, fc_in, imp_in] -- Erased
+      = do let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           let imp = case fromScheme (decodeObj imp_in) of
+                          Just imp => imp
+                          _ => False
+           pure (SErased fc imp)
+  snfVector svs (-7) [_, fc_in] -- Type
+      = do let fc = case fromScheme (decodeObj fc_in) of
+                         Just fc => fc
+                         _ => emptyFC
+           pure (SType fc)
+  snfVector svs (-8) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Lambda
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- snf' svs ty_in
+           pi <- snfPiInfo svs pi_in
+           snfBinder svs Lam proc_in rig pi ty name
+  snfVector svs (-3) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- Pi
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- snf' svs ty_in
+           pi <- snfPiInfo svs pi_in
+           snfBinder svs Pi proc_in rig pi ty name
+  snfVector svs (-12) [_, proc_in, rig_in, pi_in, ty_in, name_in] -- PVar
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- snf' svs ty_in
+           pi <- snfPiInfo svs pi_in
+           snfBinder svs PVar proc_in rig pi ty name
+  snfVector svs (-13) [_, proc_in, rig_in, ty_in, name_in] -- PVTy
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- snf' svs ty_in
+           snfBinder svs (\fc, r, p, t => PVTy fc r t) proc_in rig Explicit ty name
+  snfVector svs (-14) [_, proc_in, rig_in, val_in, ty_in, name_in] -- PLet
+      = do let name = case fromScheme (decodeObj name_in) of
+                           Nothing => UN (Basic "x")
+                           Just n' => n'
+           let rig = case fromScheme (decodeObj rig_in) of
+                          Nothing => top
+                          Just r => r
+           ty <- snf' svs ty_in
+           val <- snf' svs val_in
+           snfPLet svs proc_in rig val ty name
+  snfVector svs (-9) [_, blocked, _] -- Blocked top level lambda
+      = snf' svs blocked
+
+  -- constants here
+  snfVector svs (-100) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (I x')
+  snfVector svs (-101) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (I8 x')
+  snfVector svs (-102) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (I16 x')
+  snfVector svs (-103) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (I32 x')
+  snfVector svs (-104) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (I64 x')
+  snfVector svs (-105) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (BI x')
+  snfVector svs (-106) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (B8 x')
+  snfVector svs (-107) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (B16 x')
+  snfVector svs (-108) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (B32 x')
+  snfVector svs (-109) [_, x]
+      = do let Just x' = fromScheme (decodeObj x)
+                 | Nothing => invalidS
+           pure $ SPrimVal emptyFC (B64 x')
+
+  snfVector svs tag (_ :: cname_in :: fc_in :: args_in) -- DataCon
+      = if tag >= 0
+           then do
+             let Just cname = fromScheme (decodeObj cname_in)
+                    | Nothing => invalidS
+             let fc = case fromScheme (decodeObj fc_in) of
+                           Just fc => fc
+                           _ => emptyFC
+             let args = map (snf' svs) args_in
+             pure (SDCon fc cname (cast tag) (length args) args)
+           else invalidS
+  snfVector _ _ _ = invalidS
+
+  snfPiInfo : Ref Ctxt Defs =>
+              SchVars vars ->
+              ForeignObj ->
+              Core (PiInfo (SNF vars))
+  snfPiInfo svs obj
+      = if isInteger obj
+           then case unsafeGetInteger obj of
+                     0 => pure Implicit
+                     1 => pure Explicit
+                     2 => pure AutoImplicit
+                     _ => pure Explicit
+           else if isBox obj
+                   then do t' <- snf' svs (unsafeUnbox obj)
+                           pure (DefImplicit t')
+           else pure Explicit
+
+  snfBinder : Ref Ctxt Defs =>
+              SchVars vars ->
+              (forall ty . FC -> RigCount -> PiInfo ty -> ty -> Binder ty) ->
+              ForeignObj -> -- body of binder, represented as a function
+              RigCount ->
+              PiInfo (SNF vars) ->
+              SNF vars -> -- decoded type
+              Name -> -- bound name
+              Core (SNF vars)
+  snfBinder svs binder proc_in r pi ty name
+      = do let Procedure proc = decodeObj proc_in
+                    | _ => invalidS
+           pure (SBind emptyFC name (binder emptyFC r pi ty)
+                       (\tm => do let MkSObj arg _ = tm
+                                  let sc = unsafeApply proc arg
+                                  snf' svs sc))
+
+  snfPLet : Ref Ctxt Defs =>
+            SchVars vars ->
+            ForeignObj -> -- body of binder, represented as a function
+            RigCount ->
+            SNF vars -> -- decoded type
+            SNF vars -> -- decoded value
+            Name -> -- bound name
+            Core (SNF vars)
+  snfPLet svs proc_in r val ty name
+      = do let Procedure proc = decodeObj proc_in
+                    | _ => invalidS
+           pure (SBind emptyFC name (PLet emptyFC r val ty)
+                       (\tm => do let MkSObj arg _ = tm
+                                  let sc = unsafeApply proc arg
+                                  snf' svs sc))
+
+  snf' : Ref Ctxt Defs =>
+         SchVars vars -> ForeignObj ->
+         Core (SNF vars)
+  snf' svs obj
+      = if isVector obj
+           then snfVector svs (unsafeGetInteger (unsafeVectorRef obj 0))
+                              (unsafeVectorToList obj)
+           else if isProcedure obj then snfBinder svs Lam obj top
+                                                 Explicit
+                                                 (SErased emptyFC False)
+                                                 (UN (Basic "x"))
+           else if isSymbol obj then pure $ findName svs (unsafeReadSymbol obj)
+           else if isFloat obj then pure $ SPrimVal emptyFC (Db (unsafeGetFloat obj))
+           else if isInteger obj then pure $ SPrimVal emptyFC (I (cast (unsafeGetInteger obj)))
+           else if isString obj then pure $ SPrimVal emptyFC (Str (unsafeGetString obj))
+           else if isChar obj then pure $ SPrimVal emptyFC (Ch (unsafeGetChar obj))
+           else invalidS
+    where
+      findName : forall vars . SchVars vars -> String -> SNF vars
+      findName [] n = SApp emptyFC (SRef Func (UN (Basic n))) []
+      findName (x :: xs) n
+          = if getName x == n
+               then SApp emptyFC (SLocal _ First) []
+               else let SApp fc (SLocal _ p) args = findName xs n
+                           | _ => SApp emptyFC (SRef Func (UN (Basic n))) [] in
+                        SApp fc (SLocal _ (Later p)) []
+
+      readVector : Integer -> Integer -> ForeignObj -> List ForeignObj
+      readVector len i obj
+          = if len == i
+               then []
+               else unsafeVectorRef obj i :: readVector len (i + 1) obj
+
+export
+toSNF : Ref Ctxt Defs =>
+        SObj vars -> Core (SNF vars)
+toSNF (MkSObj val schEnv) = snf' schEnv val
diff --git a/src/Core/SchemeEval/Quote.idr b/src/Core/SchemeEval/Quote.idr
new file mode 100644
index 000000000..ce3764fd6
--- /dev/null
+++ b/src/Core/SchemeEval/Quote.idr
@@ -0,0 +1,143 @@
+module Core.SchemeEval.Quote
+
+import Core.Context
+import Core.Context.Log
+import Core.Core
+import Core.Env
+import Core.SchemeEval.Compile
+import Core.SchemeEval.Evaluate
+import Core.TT
+
+import Libraries.Data.NameMap
+import Libraries.Utils.Scheme
+
+mutual
+  quoteArgs : {auto c : Ref Ctxt Defs} ->
+              {bound, free : _} ->
+              Ref Sym Integer -> Bounds bound ->
+              Env Term free -> List (Core (SNF free)) ->
+              Core (List (Term (bound ++ free)))
+  quoteArgs q bound env args
+      = traverse (\arg => do arg' <- arg
+                             quoteGen q bound env arg') args
+
+  quotePi : {auto c : Ref Ctxt Defs} ->
+            {bound, free : _} ->
+            Ref Sym Integer -> Bounds bound ->
+            Env Term free -> PiInfo (SNF free) ->
+            Core (PiInfo (Term (bound ++ free)))
+  quotePi q bound env Explicit = pure Explicit
+  quotePi q bound env Implicit = pure Implicit
+  quotePi q bound env AutoImplicit = pure AutoImplicit
+  quotePi q bound env (DefImplicit t)
+      = do t' <- quoteGen q bound env t
+           pure (DefImplicit t')
+
+  quoteBinder : {auto c : Ref Ctxt Defs} ->
+                {bound, free : _} ->
+                Ref Sym Integer -> Bounds bound ->
+                Env Term free -> Binder (SNF free) ->
+                Core (Binder (Term (bound ++ free)))
+  quoteBinder q bound env (Lam fc r p ty)
+     = do ty' <- quoteGen q bound env ty
+          p' <- quotePi q bound env p
+          pure (Lam fc r p' ty')
+  quoteBinder q bound env (Let fc r val ty)
+     = do ty' <- quoteGen q bound env ty
+          val' <- quoteGen q bound env val
+          pure (Let fc r val' ty')
+  quoteBinder q bound env (Pi fc r p ty)
+     = do ty' <- quoteGen q bound env ty
+          p' <- quotePi q bound env p
+          pure (Pi fc r p' ty')
+  quoteBinder q bound env (PVar fc r p ty)
+     = do ty' <- quoteGen q bound env ty
+          p' <- quotePi q bound env p
+          pure (PVar fc r p' ty')
+  quoteBinder q bound env (PLet fc r val ty)
+     = do ty' <- quoteGen q bound env ty
+          val' <- quoteGen q bound env val
+          pure (PLet fc r val' ty')
+  quoteBinder q bound env (PVTy fc r ty)
+     = do ty' <- quoteGen q bound env ty
+          pure (PVTy fc r ty')
+
+  quoteHead : {auto c : Ref Ctxt Defs} ->
+              {bound, free : _} ->
+              Ref Sym Integer ->
+              FC -> Bounds bound -> Env Term free -> SHead free ->
+              Core (Term (bound ++ free))
+  quoteHead {bound} q fc bounds env (SLocal idx prf)
+      = let MkVar prf' = addLater bound prf in
+            pure (Local fc Nothing _ prf')
+    where
+      addLater : {idx : _} ->
+                 (ys : List Name) -> (0 p : IsVar n idx xs) ->
+                 Var (ys ++ xs)
+      addLater [] isv = MkVar isv
+      addLater (x :: xs) isv
+          = let MkVar isv' = addLater xs isv in
+                MkVar (Later isv')
+  quoteHead q fc bounds env (SRef nt n)
+      = pure $ case findName bounds of
+             Just (MkVar p) => Local fc Nothing _ (varExtend p)
+             Nothing => Ref fc nt n
+    where
+      findName : Bounds bound' -> Maybe (Var bound')
+      findName None = Nothing
+      findName (Add x n' ns)
+          = if n == n'
+               then Just (MkVar First)
+               else do MkVar p <-findName ns
+                       Just (MkVar (Later p))
+  quoteHead q fc bounds env (SMeta n i args)
+      = do args' <- quoteArgs q bounds env args
+           pure $ Meta fc n i args'
+
+  quoteGen : {auto c : Ref Ctxt Defs} ->
+             {bound, vars : _} ->
+             Ref Sym Integer -> Bounds bound ->
+             Env Term vars -> SNF vars -> Core (Term (bound ++ vars))
+  quoteGen q bound env (SBind fc n b sc)
+      = do i <- get Sym
+           put Sym (i + 1)
+           let var = UN (Basic ("b-" ++ show (fromInteger i)))
+           -- Ref Bound gets turned directly into a symbol by seval, which
+           -- we can then read back when quoting the scope
+           arg <- seval EvalAll env (Ref fc Bound var)
+           sc' <- quoteGen q (Add n var bound) env !(sc arg)
+           b' <- quoteBinder q bound env b
+           pure (Bind fc n b' sc')
+  quoteGen q bound env (SApp fc f args)
+      = do f' <- quoteHead q fc bound env f
+           args' <- quoteArgs q bound env args
+           pure $ apply fc f' args'
+  quoteGen q bound env (SDCon fc n t ar args)
+      = do args' <- quoteArgs q bound env args
+           pure $ apply fc (Ref fc (DataCon t ar) n) args'
+  quoteGen q bound env (STCon fc n t ar args)
+      = do args' <- quoteArgs q bound env args
+           pure $ apply fc (Ref fc (TyCon t ar) n) args'
+  quoteGen q bound env (SDelayed fc r arg)
+      = do argQ <- quoteGen q bound env arg
+           pure (TDelayed fc r argQ)
+  quoteGen q bound env (SDelay fc r ty arg)
+      = do argQ <- quoteGen q bound env !arg
+           tyQ <- quoteGen q bound env !ty
+           pure (TDelay fc r tyQ argQ)
+  quoteGen q bound env (SForce fc r arg)
+      = case arg of
+             SDelay fc _ _ arg => quoteGen q bound env !arg
+             _ => do arg' <- quoteGen q bound env arg
+                     pure $ (TForce fc r arg')
+  quoteGen q bound env (SPrimVal fc c) = pure $ PrimVal fc c
+  quoteGen q bound env (SErased fc i) = pure $ Erased fc i
+  quoteGen q bound env (SType fc) = pure $ TType fc
+
+export
+quote : {auto c : Ref Ctxt Defs} ->
+        {vars : _} ->
+        Env Term vars -> SNF vars -> Core (Term vars)
+quote env tm
+    = do q <- newRef Sym 0
+         quoteGen q None env tm
diff --git a/src/Core/SchemeEval/ToScheme.idr b/src/Core/SchemeEval/ToScheme.idr
new file mode 100644
index 000000000..ab4297bba
--- /dev/null
+++ b/src/Core/SchemeEval/ToScheme.idr
@@ -0,0 +1,110 @@
+module Core.SchemeEval.ToScheme
+
+import Core.TT
+import Libraries.Utils.Scheme
+
+export
+Scheme Namespace where
+  toScheme x = toScheme (unsafeUnfoldNamespace x)
+  fromScheme x = Just $ unsafeFoldNamespace !(fromScheme x)
+
+export
+Scheme UserName where
+  toScheme (Basic str) = toScheme str
+  toScheme (Field str) = Vector 5 [toScheme str]
+  toScheme Underscore = Vector 9 []
+
+  fromScheme (Vector 5 [x]) = pure $ Field !(fromScheme x)
+  fromScheme (Vector 9 []) = pure Underscore
+  fromScheme (StringVal x) = pure (Basic x)
+  fromScheme _ = Nothing
+
+export
+Scheme Name where
+  toScheme (NS x y) = Vector 0 [toScheme x, toScheme y]
+  toScheme (UN x) = toScheme x
+  toScheme (MN x y) = Vector 2 [toScheme x, toScheme y]
+  toScheme (PV x y) = Vector 3 [toScheme x, toScheme y]
+  toScheme (DN x y) = Vector 4 [toScheme x, toScheme y]
+  toScheme (Nested x y) = Vector 6 [toScheme x, toScheme y]
+  toScheme (CaseBlock x y) = Vector 7 [toScheme x, toScheme y]
+  toScheme (WithBlock x y) = Vector 8 [toScheme x, toScheme y]
+  toScheme (Resolved x) = toScheme x -- we'll see this most often
+
+  fromScheme (Vector 0 [x, y])
+      = pure $ NS !(fromScheme x) !(fromScheme y)
+  fromScheme (Vector 2 [x, y])
+      = pure $ MN !(fromScheme x) !(fromScheme y)
+  fromScheme (Vector 3 [x, y])
+      = pure $ PV !(fromScheme x) !(fromScheme y)
+  fromScheme (Vector 4 [x, y])
+      = pure $ DN !(fromScheme x) !(fromScheme y)
+  fromScheme (Vector 5 [x, y])
+      = pure $ UN (Field !(fromScheme x))
+  fromScheme (Vector 6 [x, y])
+      = pure $ Nested !(fromScheme x) !(fromScheme y)
+  fromScheme (Vector 7 [x, y])
+      = pure $ CaseBlock !(fromScheme x) !(fromScheme y)
+  fromScheme (Vector 8 [x, y])
+      = pure $ WithBlock !(fromScheme x) !(fromScheme y)
+  fromScheme (Vector 9 [])
+      = pure $ UN Underscore
+  fromScheme (IntegerVal x)
+      = pure $ Resolved (cast x)
+  fromScheme (StringVal x)
+      = pure $ UN (Basic x)
+  fromScheme _ = Nothing
+
+export
+Scheme ModuleIdent where
+  toScheme ns = toScheme (miAsNamespace ns)
+  fromScheme s = Just $ nsAsModuleIdent !(fromScheme s)
+
+export
+Scheme OriginDesc where
+  toScheme (PhysicalIdrSrc ident) = Vector 0 [toScheme ident]
+  toScheme (PhysicalPkgSrc fname) = Vector 1 [toScheme fname]
+  toScheme (Virtual ident) = Null
+
+  fromScheme (Vector 0 [i]) = Just (PhysicalIdrSrc !(fromScheme i))
+  fromScheme (Vector 1 [i]) = Just (PhysicalPkgSrc !(fromScheme i))
+  fromScheme (Vector _ _) = Nothing
+  fromScheme _ = Just (Virtual Interactive)
+
+export
+Scheme FC where
+  toScheme (MkFC d s e) = Vector 0 [toScheme d, toScheme s, toScheme e]
+  toScheme (MkVirtualFC d s e) = Vector 1 [toScheme d, toScheme s, toScheme e]
+  toScheme EmptyFC = Null
+
+  fromScheme _ = Just EmptyFC
+
+export
+Scheme LazyReason where
+  toScheme LInf = IntegerVal 0
+  toScheme LLazy = IntegerVal 1
+  toScheme LUnknown = IntegerVal 2
+
+  fromScheme (IntegerVal 0) = Just LInf
+  fromScheme (IntegerVal 1) = Just LLazy
+  fromScheme _ = Just LUnknown
+
+export
+Scheme RigCount where
+  toScheme x
+      = if isErased x then IntegerVal 0
+        else if isLinear x then IntegerVal 1
+        else IntegerVal 2
+
+  fromScheme (IntegerVal 0) = Just erased
+  fromScheme (IntegerVal 1) = Just linear
+  fromScheme _ = Just top
+
+export
+toSchemePi : PiInfo (SchemeObj Write) -> SchemeObj Write
+toSchemePi Implicit = IntegerVal 0
+toSchemePi Explicit = IntegerVal 1
+toSchemePi AutoImplicit = IntegerVal 2
+toSchemePi (DefImplicit s) = Box s
+
+
diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr
index e9b544977..2e164fc30 100644
--- a/src/Core/TTC.idr
+++ b/src/Core/TTC.idr
@@ -18,6 +18,7 @@ import Libraries.Data.IOArray
 import Data.Vect
 
 import Libraries.Utils.Binary
+import Libraries.Utils.Scheme
 
 %default covering
 
@@ -1115,10 +1116,10 @@ TTC GlobalDef where
                       sc <- fromBuf b
                       pure (MkGlobalDef loc name ty eargs seargs specargs iargs
                                         mul vars vis
-                                        tot fl refs refsR inv c True def cdef sc)
+                                        tot fl refs refsR inv c True def cdef Nothing sc Nothing)
               else pure (MkGlobalDef loc name (Erased loc False) [] [] [] []
                                      mul [] Public unchecked [] refs refsR
-                                     False False True def cdef [])
+                                     False False True def cdef Nothing [] Nothing)
 
 export
 TTC Transform where
diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr
index 026570195..1567e9060 100644
--- a/src/Idris/IDEMode/REPL.idr
+++ b/src/Idris/IDEMode/REPL.idr
@@ -311,6 +311,7 @@ SExpable REPLEval where
   toSExp EvalTC = SymbolAtom "typecheck"
   toSExp NormaliseAll = SymbolAtom "normalise"
   toSExp Execute = SymbolAtom "execute"
+  toSExp Scheme = SymbolAtom "scheme"
 
 SExpable REPLOpt where
   toSExp (ShowImplicits impl) = SExpList [ SymbolAtom "show-implicits", toSExp impl ]
@@ -320,6 +321,7 @@ SExpable REPLOpt where
   toSExp (Editor editor) = SExpList [ SymbolAtom "editor", toSExp editor ]
   toSExp (CG str) = SExpList [ SymbolAtom "cg", toSExp str ]
   toSExp (Profile p) = SExpList [ SymbolAtom "profile", toSExp p ]
+  toSExp (EvalTiming p) = SExpList [ SymbolAtom "evaltiming", toSExp p ]
 
 
 displayIDEResult : {auto c : Ref Ctxt Defs} ->
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 1399ae347..8459d2424 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1755,17 +1755,23 @@ parseMode
           pure EvalTC
    <|> do exactIdent "normalise"
           pure NormaliseAll
+   <|> do exactIdent "default"
+          pure NormaliseAll
+   <|> do exactIdent "normal"
+          pure NormaliseAll
    <|> do exactIdent "normalize" -- oh alright then
           pure NormaliseAll
    <|> do exactIdent "execute"
           pure Execute
    <|> do exactIdent "exec"
           pure Execute
+   <|> do exactIdent "scheme"
+          pure Scheme
 
 setVarOption : Rule REPLOpt
 setVarOption
     = do exactIdent "eval"
-         mode <- parseMode
+         mode <- option NormaliseAll parseMode
          pure (EvalMode mode)
   <|> do exactIdent "editor"
          e <- unqualifiedName
@@ -1784,6 +1790,8 @@ setOption set
          pure (ShowTypes set)
   <|> do exactIdent "profile"
          pure (Profile set)
+  <|> do exactIdent "evaltiming"
+         pure (EvalTiming set)
   <|> if set then setVarOption else fatalError "Unrecognised option"
 
 replCmd : List String -> Rule ()
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index 9dca29730..d2d33be53 100644
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@@ -28,6 +28,8 @@ import Core.Termination
 import Core.Unify
 import Core.Value
 
+import Core.SchemeEval
+
 import Parser.Unlit
 
 import Idris.Desugar
@@ -198,6 +200,8 @@ setOpt (CG e)
 setOpt (Profile t)
     = do pp <- getSession
          setSession (record { profile = t } pp)
+setOpt (EvalTiming t)
+    = setEvalTiming t
 
 getOptions : {auto c : Ref Ctxt Defs} ->
          {auto o : Ref ROpts REPLOpts} ->
@@ -590,7 +594,8 @@ execExp ctm
               | Nothing =>
                    do iputStrLn (reflow "No such code generator available")
                       pure CompilationFailed
-         execute cg tm_erased
+         logTimeWhen !getEvalTiming "Execution" $
+           execute cg tm_erased
          pure $ Executed ctm
 
 
@@ -731,9 +736,17 @@ process (Eval itm)
          let emode = evalMode opts
          case emode of
             Execute => do ignore (execExp itm); pure (Executed itm)
+            Scheme =>
+              do defs <- get Ctxt
+                 (tm `WithType` ty) <- inferAndElab InExpr itm
+                 qtm <- logTimeWhen !getEvalTiming "Evaluation" $
+                           (do nf <- snfAll [] tm
+                               quote [] nf)
+                 itm <- logTimeWhen False "resugar" $ resugar [] qtm
+                 pure (Evaluated itm Nothing)
             _ =>
-              do
-                 (ntm `WithType` ty) <- inferAndNormalize emode itm
+              do (ntm `WithType` ty) <- logTimeWhen !getEvalTiming "Evaluation" $
+                                           inferAndNormalize emode itm
                  itm <- resugar [] ntm
                  defs <- get Ctxt
                  opts <- get ROpts
@@ -1039,6 +1052,7 @@ mutual
       prompt EvalTC = "[tc] "
       prompt NormaliseAll = ""
       prompt Execute = "[exec] "
+      prompt Scheme = "[scheme] "
 
   export
   handleMissing' : MissedResult -> String
diff --git a/src/Idris/REPL/Opts.idr b/src/Idris/REPL/Opts.idr
index f3efb0e48..c49e899aa 100644
--- a/src/Idris/REPL/Opts.idr
+++ b/src/Idris/REPL/Opts.idr
@@ -44,6 +44,7 @@ record REPLOpts where
   constructor MkREPLOpts
   showTypes : Bool
   evalMode : REPLEval
+  evalTiming : Bool
   mainfile : Maybe String
   literateStyle : Maybe LiterateStyle
   source : String
@@ -70,6 +71,7 @@ defaultOpts fname outmode cgs
     = MkREPLOpts
         { showTypes = False
         , evalMode = NormaliseAll
+        , evalTiming = False
         , mainfile = fname
         , literateStyle = litStyle fname
         , source = ""
@@ -207,3 +209,15 @@ export
 setSynHighlightOn : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
 setSynHighlightOn b = do opts <- get ROpts
                          put ROpts (record { synHighlightOn = b } opts)
+
+export
+getEvalTiming : {auto o : Ref ROpts REPLOpts} -> Core Bool
+getEvalTiming
+    = do opts <- get ROpts
+         pure (evalTiming opts)
+
+export
+setEvalTiming : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
+setEvalTiming b
+    = do opts <- get ROpts
+         put ROpts (record { evalTiming = b } opts)
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index 77f96802c..03b7fc0bb 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -518,18 +518,21 @@ data REPLEval : Type where
      EvalTC : REPLEval -- Evaluate as if part of the typechecker
      NormaliseAll : REPLEval -- Normalise everything (default)
      Execute : REPLEval -- Evaluate then pass to an executer
+     Scheme : REPLEval -- Use the scheme evaluator
 
 export
 Show REPLEval where
   show EvalTC = "typecheck"
   show NormaliseAll = "normalise"
   show Execute = "execute"
+  show Scheme = "scheme"
 
 export
 Pretty REPLEval where
   pretty EvalTC = pretty "typecheck"
   pretty NormaliseAll = pretty "normalise"
   pretty Execute = pretty "execute"
+  pretty Scheme = pretty "scheme"
 
 public export
 data REPLOpt : Type where
@@ -540,6 +543,7 @@ data REPLOpt : Type where
      Editor : String -> REPLOpt
      CG : String -> REPLOpt
      Profile : Bool -> REPLOpt
+     EvalTiming : Bool -> REPLOpt
 
 export
 Show REPLOpt where
@@ -550,6 +554,7 @@ Show REPLOpt where
   show (Editor editor) = "editor = " ++ show editor
   show (CG str) = "cg = " ++ str
   show (Profile p) = "profile = " ++ show p
+  show (EvalTiming p) = "evaltiming = " ++ show p
 
 export
 Pretty REPLOpt where
@@ -560,6 +565,7 @@ Pretty REPLOpt where
   pretty (Editor editor) = pretty "editor" <++> equals <++> pretty editor
   pretty (CG str) = pretty "cg" <++> equals <++> pretty str
   pretty (Profile p) = pretty "profile" <++> equals <++> pretty p
+  pretty (EvalTiming p) = pretty "evaltiming" <++> equals <++> pretty p
 
 public export
 data EditCmd : Type where
diff --git a/src/Libraries/Utils/Scheme.idr b/src/Libraries/Utils/Scheme.idr
new file mode 100644
index 000000000..1823ff637
--- /dev/null
+++ b/src/Libraries/Utils/Scheme.idr
@@ -0,0 +1,360 @@
+module Libraries.Utils.Scheme
+
+export
+data ForeignObj : Type where [external]
+
+%foreign "scheme:blodwen-eval-scheme"
+prim__evalScheme : String -> ForeignObj
+
+%foreign "scheme:blodwen-eval-okay"
+prim__evalOkay : ForeignObj -> Int
+
+%foreign "scheme:blodwen-get-eval-result"
+prim__evalResult : ForeignObj -> ForeignObj
+
+%foreign "scheme:blodwen-debug-scheme"
+prim__debugScheme : ForeignObj -> PrimIO ()
+
+%foreign "scheme:blodwen-is-number"
+prim_isNumber : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-integer"
+prim_isInteger : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-float"
+prim_isFloat : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-char"
+prim_isChar : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-string"
+prim_isString : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-procedure"
+prim_isProcedure : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-symbol"
+prim_isSymbol : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-nil"
+prim_isNil : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-pair"
+prim_isPair : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-vector"
+prim_isVector : ForeignObj -> Int
+
+%foreign "scheme:blodwen-is-box"
+prim_isBox : ForeignObj -> Int
+
+export
+isNumber : ForeignObj -> Bool
+isNumber x = prim_isNumber x == 1
+
+export
+isInteger : ForeignObj -> Bool
+isInteger x = prim_isInteger x == 1
+
+export
+isFloat : ForeignObj -> Bool
+isFloat x = prim_isFloat x == 1
+
+export
+isChar : ForeignObj -> Bool
+isChar x = prim_isChar x == 1
+
+export
+isString : ForeignObj -> Bool
+isString x = prim_isString x == 1
+
+export
+isProcedure : ForeignObj -> Bool
+isProcedure x = prim_isProcedure x == 1
+
+export
+isSymbol : ForeignObj -> Bool
+isSymbol x = prim_isSymbol x == 1
+
+export
+isNil : ForeignObj -> Bool
+isNil x = prim_isNil x == 1
+
+export
+isPair : ForeignObj -> Bool
+isPair x = prim_isPair x == 1
+
+export
+isVector : ForeignObj -> Bool
+isVector x = prim_isVector x == 1
+
+export
+isBox : ForeignObj -> Bool
+isBox x = prim_isBox x == 1
+
+-- The below are all 'unsafe' because they rely on having done the relevant
+-- check above first
+%foreign "scheme:blodwen-id"
+export
+unsafeGetInteger : ForeignObj -> Integer
+
+%foreign "scheme:blodwen-id"
+export
+unsafeGetString : ForeignObj -> String
+
+%foreign "scheme:blodwen-id"
+export
+unsafeGetFloat : ForeignObj -> Double
+
+%foreign "scheme:blodwen-id"
+export
+unsafeGetChar : ForeignObj -> Char
+
+%foreign "scheme:car"
+export
+unsafeFst : ForeignObj -> ForeignObj
+
+%foreign "scheme:cdr"
+export
+unsafeSnd : ForeignObj -> ForeignObj
+
+%foreign "scheme:blodwen-apply"
+export
+unsafeApply : ForeignObj -> ForeignObj -> ForeignObj
+
+%foreign "scheme:blodwen-force"
+export
+unsafeForce : ForeignObj -> ForeignObj
+
+%foreign "scheme:blodwen-vector-ref"
+export
+unsafeVectorRef : ForeignObj -> Integer -> ForeignObj
+
+%foreign "scheme:blodwen-unbox"
+export
+unsafeUnbox : ForeignObj -> ForeignObj
+
+%foreign "scheme:blodwen-vector-length"
+export
+unsafeVectorLength : ForeignObj -> Integer
+
+%foreign "scheme:blodwen-vector-list"
+export
+unsafeVectorToList : ForeignObj -> List ForeignObj
+
+%foreign "scheme:blodwen-make-symbol"
+export
+makeSymbol : String -> ForeignObj
+
+%foreign "scheme:blodwen-read-symbol"
+export
+unsafeReadSymbol : ForeignObj -> String
+
+export
+evalSchemeStr : String -> IO (Maybe ForeignObj)
+evalSchemeStr exp
+    = let obj = prim__evalScheme exp in
+          if prim__evalOkay obj == 1
+             then pure $ Just (prim__evalResult obj)
+             else pure Nothing
+
+export
+debugScheme : ForeignObj -> IO ()
+debugScheme obj = primIO $ prim__debugScheme obj
+
+public export
+data Direction = Write | Readback
+
+public export
+data SchemeObj : Direction -> Type where
+     Null : SchemeObj t
+     Cons : SchemeObj t -> SchemeObj t -> SchemeObj t
+     IntegerVal : Integer -> SchemeObj t
+     FloatVal : Double -> SchemeObj t
+     StringVal : String -> SchemeObj t
+     CharVal : Char -> SchemeObj t
+     Symbol : String -> SchemeObj t
+     Box : SchemeObj t -> SchemeObj t
+     Vector : Integer -> List (SchemeObj t) -> SchemeObj t
+        -- ^ this is convenient for us since all our vectors start with a
+        -- tag, but not for a general library
+
+     Procedure : ForeignObj -> SchemeObj Readback
+
+     Define : String -> SchemeObj Write -> SchemeObj Write
+     Var : String -> SchemeObj Write
+     Lambda : List String -> SchemeObj Write -> SchemeObj Write
+     Let : String -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
+     If : SchemeObj Write -> SchemeObj Write -> SchemeObj Write ->
+          SchemeObj Write
+     Case : SchemeObj Write ->
+            List (SchemeObj Write, SchemeObj Write) ->
+            Maybe (SchemeObj Write) ->
+            SchemeObj Write
+     Cond : List (SchemeObj Write, SchemeObj Write) ->
+            Maybe (SchemeObj Write) ->
+            SchemeObj Write
+     Apply : SchemeObj Write -> List (SchemeObj Write) -> SchemeObj Write
+
+export
+evalSchemeObj : SchemeObj Write -> IO (Maybe ForeignObj)
+evalSchemeObj obj
+    = do let str = toString obj
+         evalSchemeStr str
+  where
+    showSep : String -> List String -> String
+    showSep sep [] = ""
+    showSep sep [x] = x
+    showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
+
+    toString : SchemeObj Write -> String
+    toString Null = "'()"
+    toString (Cons x y) = "(cons " ++ toString x ++ " " ++ toString y ++ ")"
+    toString (IntegerVal x) = show x
+    toString (FloatVal x) = show x
+    toString (StringVal x) = show x
+    toString (CharVal x)
+       = if (the Int (cast x) >= 32 && the Int (cast x) < 127)
+            then "#\\" ++ cast x
+            else "(integer->char " ++ show (the Int (cast x)) ++ ")"
+    toString (Symbol x) = "'" ++ x
+    toString (Vector i xs) = "(vector " ++ show i ++ " " ++ showSep " " (map toString xs) ++ ")"
+    toString (Box x) = "(box " ++ toString x ++ ")"
+    toString (Define x body) = "(define (" ++ x ++ ") " ++ toString body ++ ")"
+    toString (Var x) = x
+    toString (Lambda xs x)
+        = "(lambda (" ++ showSep " " xs ++ ") " ++ toString x ++ ")"
+    toString (Let var val x)
+        = "(let ((" ++ var ++ " " ++ toString val ++ ")) " ++ toString x ++ ")"
+    toString (If x t e)
+        = "(if " ++ toString x ++ " " ++ toString t ++ " " ++ toString e ++ ")"
+    toString (Case x alts def)
+        = "(case " ++ toString x ++ " " ++
+              showSep " " (map showAlt alts) ++
+              showDef def ++ ")"
+      where
+        showAlt : (SchemeObj Write, SchemeObj Write) -> String
+        showAlt (opt, go)
+           = "((" ++ toString opt ++ ") " ++ toString go ++ ")"
+
+        showDef : Maybe (SchemeObj Write) -> String
+        showDef Nothing = ""
+        showDef (Just e) = " (else " ++ toString e ++ ")"
+    toString (Cond alts def)
+        = "(cond " ++
+              showSep " " (map showAlt alts) ++
+              showDef def ++ ")"
+      where
+        showAlt : (SchemeObj Write, SchemeObj Write) -> String
+        showAlt (opt, go)
+           = "(" ++ toString opt ++ " " ++ toString go ++ ")"
+
+        showDef : Maybe (SchemeObj Write) -> String
+        showDef Nothing = ""
+        showDef (Just e) = " (else " ++ toString e ++ ")"
+    toString (Apply x xs)
+        = "(" ++ toString x ++ " " ++ showSep " " (map toString xs) ++ ")"
+
+export
+decodeObj : ForeignObj -> SchemeObj Readback
+decodeObj obj
+    = if isInteger obj then IntegerVal (unsafeGetInteger obj)
+      else if isVector obj then Vector (unsafeGetInteger (unsafeVectorRef obj 0))
+                                       (readVector (unsafeVectorLength obj) 1 obj)
+      else if isPair obj then Cons (decodeObj (unsafeFst obj))
+                                   (decodeObj (unsafeSnd obj))
+      else if isFloat obj then FloatVal (unsafeGetFloat obj)
+      else if isString obj then StringVal (unsafeGetString obj)
+      else if isChar obj then CharVal (unsafeGetChar obj)
+      else if isSymbol obj then Symbol (unsafeReadSymbol obj)
+      else if isProcedure obj then Procedure obj
+      else if isBox obj then Box (decodeObj (unsafeUnbox obj))
+      else Null
+  where
+    readVector : Integer -> Integer -> ForeignObj -> List (SchemeObj Readback)
+    readVector len i obj
+        = if len == i
+             then []
+             else decodeObj (unsafeVectorRef obj i) ::
+                     readVector len (i + 1) obj
+
+public export
+interface Scheme a where
+  toScheme : a -> SchemeObj Write
+  fromScheme : SchemeObj Readback -> Maybe a
+
+export
+evalScheme : Scheme a => a -> IO (Maybe ForeignObj)
+evalScheme = evalSchemeObj . toScheme
+
+export
+decode : Scheme a => ForeignObj -> Maybe a
+decode = fromScheme . decodeObj
+
+export
+Scheme Integer where
+  toScheme x = IntegerVal x
+
+  fromScheme (IntegerVal x) = Just x
+  fromScheme _ = Nothing
+
+export
+Scheme Int where
+  toScheme x = IntegerVal (cast x)
+
+  fromScheme (IntegerVal x) = Just (cast x)
+  fromScheme _ = Nothing
+
+export
+Scheme String where
+  toScheme x = StringVal x
+
+  fromScheme (StringVal x) = Just x
+  fromScheme _ = Nothing
+
+export
+Scheme Double where
+  toScheme x = FloatVal x
+
+  fromScheme (FloatVal x) = Just x
+  fromScheme _ = Nothing
+
+export
+Scheme Char where
+  toScheme x = CharVal x
+
+  fromScheme (CharVal x) = Just x
+  fromScheme _ = Nothing
+
+export
+Scheme Bool where
+  toScheme False = IntegerVal 0
+  toScheme True = IntegerVal 1
+
+  fromScheme (IntegerVal 0) = Just False
+  fromScheme (IntegerVal 1) = Just True
+  fromScheme _ = Nothing
+
+export
+Scheme a => Scheme (List a) where
+  toScheme [] = Null
+  toScheme (x :: xs) = Cons (toScheme x) (toScheme xs)
+
+  fromScheme Null = Just []
+  fromScheme (Cons x xs) = Just $ !(fromScheme x) :: !(fromScheme xs)
+  fromScheme _ = Nothing
+
+export
+(Scheme a, Scheme b) => Scheme (a, b) where
+  toScheme (x, y) = Cons (toScheme x) (toScheme y)
+  fromScheme (Cons x y) = Just (!(fromScheme x), !(fromScheme y))
+  fromScheme _ = Nothing
+
+export
+Scheme a => Scheme (Maybe a) where
+  toScheme Nothing = Null
+  toScheme (Just x) = Box (toScheme x)
+
+  fromScheme Null = Just Nothing
+  fromScheme (Box x) = Just $ Just !(fromScheme x)
+  fromScheme _ = Nothing
diff --git a/support/chez/ct-support.ss b/support/chez/ct-support.ss
new file mode 100644
index 000000000..1b47f51dc
--- /dev/null
+++ b/support/chez/ct-support.ss
@@ -0,0 +1,297 @@
+; Block all reductions (e.g. needed when quoting under a 'delay')
+(define ct-blockAll
+  (make-thread-parameter #f))
+
+(define (ct-isBlockAll)
+  (ct-blockAll))
+
+(define (ct-setBlockAll x)
+  (ct-blockAll x))
+
+; Check encodings of normal forms
+(define (ct-isDataCon val)
+  (and (vector? val) (>= (vector-ref val 0) 0)))
+(define (ct-isConstant val)
+  (or (number? val) (string? val) (char? val)
+      (and (vector? val) (<= (vector-ref val 0) -100))))
+(define (ct-isTypeCon val)
+  (and (vector? val) (= (vector-ref val 0) -1)))
+(define (ct-isBlocked val)
+  (and (vector? val) (= (vector-ref val 0) -2)))
+(define (ct-isPi val)
+  (and (vector? val) (= (vector-ref val 0) -3)))
+(define (ct-isTypeMatchable val)
+  (or (ct-isTypeCon val) (ct-isPi val)))
+(define (ct-isDelay val)
+  (and (vector? val) (= (vector-ref val 0) -4)))
+(define (ct-isForce val)
+  (and (vector? val) (= (vector-ref val 0) -5)))
+(define (ct-isErased val)
+  (and (vector? val) (= (vector-ref val 0) -6)))
+(define (ct-isType val)
+  (and (vector? val) (= (vector-ref val 0) -7)))
+(define (ct-isLambda val)
+  (and (vector? val) (= (vector-ref val 0) -8)))
+(define (ct-isTopLambda val)
+  (and (vector? val) (= (vector-ref val 0) -9)))
+
+; A function might be a blocked application, which is represented as
+; a vector (-1, name, args), so make a new vector extending args
+; (or a meta, which is a vector (-10, name, args))
+(define (ct-addArg f a)
+    (if (vector? f)
+        (vector (vector-ref f 0) (vector-ref f 1)
+             (append (vector-ref f 2) (list a)))
+        (vector -11 f (list a))))
+
+; to apply a function, either run it if it is a function, or add
+; a blocked argument if it's stuck
+(define (ct-app f a)
+   (cond
+     [(ct-isTopLambda f) ((vector-ref f 2) a)]
+     [(ct-isLambda f) ((vector-ref f 1) a)]
+     [(procedure? f) (f a)]
+     [else (ct-addArg f a)]))
+
+; force a delayed evaluation
+(define (ct-doForce arg default)
+    (if (ct-isDelay arg)
+        ((vector-ref arg 4))
+        default))
+
+; primitives
+(define ct-toSignedInt
+  (lambda (x bits)
+    (if (logbit? bits x)
+        (logor x (ash (- 1) bits))
+        (logand x (- (ash 1 bits) 1)))))
+
+(define ct-toUnsignedInt
+  (lambda (x bits)
+    (modulo x (ash 1 bits))))
+
+(define ct-u+ (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toUnsignedInt (+ xval yval) bits)))))
+(define ct-u- (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toUnsignedInt (- xval yval) bits)))))
+(define ct-u* (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toUnsignedInt (* xval yval) bits)))))
+(define ct-u/ (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toUnsignedInt (quotient xval yval) bits)))))
+
+(define ct-s+ (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (+ xval yval) bits)))))
+(define ct-s- (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (- xval yval) bits)))))
+(define ct-s* (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (* xval yval) bits)))))
+(define ct-s/ (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (quotient xval yval) bits)))))
+
+(define ct+ (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (+ xval yval)))))
+(define ct- (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (- xval yval)))))
+(define ct* (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (* xval yval)))))
+(define ct/ (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (quotient xval yval)))))
+
+(define ct-mod (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (remainder xval yval)))))
+
+(define ct-neg (lambda (x)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))]
+          (vector tag (- xval)))))
+
+(define ct-bits-shl-signed (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (shl xval yval) bits)))))
+(define ct-bits-shl (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (remainder (ash xval yval) (ash 1 bits))))))
+(define ct-shl (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ash xval yval)))))
+
+(define ct-shr (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ash xval (- yval))))))
+
+(define ct-and (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (logand xval yval)))))
+(define ct-or (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (logor xval yval)))))
+(define ct-xor (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (logxor xval yval)))))
+
+(define ct-string-ref (lambda (x i)
+    (let [(ival (vector-ref i 1))]
+         (if (and (>= ival 0) (< ival (string-length x)))
+             (string-ref x ival)
+             '()))))
+(define ct-string-cons (lambda (x y) (string-append (string x) y)))
+(define ct-string-reverse (lambda (x)
+  (list->string (reverse (string->list x)))))
+(define (ct-string-substr offin lenin s)
+    (let* [(off (vector-ref offin 1))
+           (len (vector-ref lenin 1))
+           (l (string-length s))
+           (b (max 0 off))
+           (x (max 0 len))
+           (end (min l (+ b x)))]
+          (if (> b l)
+              ""
+              (substring s b end))))
+
+; Don't wrap the result for bool results, we do that in Builtins.idr
+(define ct< (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (< xval yval))))
+(define ct<= (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (<= xval yval))))
+(define ct= (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (= xval yval))))
+(define ct>= (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (>= xval yval))))
+(define ct> (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (> xval yval))))
+
+; casts
+; when targetting integers, we add the Vector on the Idris side
+
+(define ct-cast-num
+  (lambda (x)
+    (if (number? x) x 0)))
+(define destroy-prefix
+  (lambda (x)
+    (cond
+      ((equal? x "") "")
+      ((equal? (string-ref x 0) #\#) "")
+      (else x))))
+
+(define ct-cast-string-double
+  (lambda (x)
+    (cast-num (string->number (destroy-prefix x)))))
+
+(define ct-cast-char-boundedInt
+  (lambda (x y)
+    (ct-toSignedInt (char->integer x) y)))
+
+(define ct-cast-char-boundedUInt
+  (lambda (x y)
+    (ct-toUnsignedInt (char->integer x) y)))
+
+(define ct-cast-int-char
+  (lambda (xin)
+    (let [(x (vector-ref xin 1))]
+      (if (or
+          (and (>= x 0) (<= x #xd7ff))
+          (and (>= x #xe000) (<= x #x10ffff)))
+        (integer->char x)
+        (integer->char 0)))))
+
+(define ct-cast-string-int
+  (lambda (x)
+    (exact-truncate (cast-num (string->number (destroy-prefix x))))))
+
+(define ct-cast-string-boundedInt
+  (lambda (x y)
+    (blodwen-toSignedInt (cast-string-int x) y)))
+
+(define ct-cast-string-boundedUInt
+  (lambda (x y)
+    (blodwen-toUnsignedInt (cast-string-int x) y)))
+
+(define ct-cast-number-string
+  (lambda (xin)
+    (let [(x (vector-ref xin 1))]
+      (number->string x))))
+
+(define ct-exact-truncate
+  (lambda (x)
+    (inexact->exact (truncate x))))
+
+(define ct-exact-truncate-boundedInt
+  (lambda (x y)
+    (ct-toSignedInt (exact-truncate x) y)))
+
+(define ct-exact-truncate-boundedUInt
+  (lambda (x y)
+    (ct-toUnsignedInt (exact-truncate x) y)))
+
+(define ct-int-double
+  (lambda (xin)
+    (let [(x (vector-ref xin 1))]
+      (exact->inexact x))))
diff --git a/support/chez/support.ss b/support/chez/support.ss
index 82aaab901..ea6528a8e 100644
--- a/support/chez/support.ss
+++ b/support/chez/support.ss
@@ -499,7 +499,10 @@
 ; read a scheme string and evaluate it, returning 'Just result' on success
 ; TODO: catch exception!
 (define (blodwen-eval-scheme str)
-  (box (eval (read (open-input-string str))))) ; box == Just
+  (guard
+     (x [#t '()]) ; Nothing on failure
+     (box (eval (read (open-input-string str)))))
+  ); box == Just
 
 (define (blodwen-eval-okay obj)
   (if (null? obj)
diff --git a/support/racket/ct-support.rkt b/support/racket/ct-support.rkt
new file mode 100644
index 000000000..d6bd518c0
--- /dev/null
+++ b/support/racket/ct-support.rkt
@@ -0,0 +1,297 @@
+; Block all reductions (e.g. needed when quoting under a 'delay')
+(define ct-blockAll
+  (make-thread-cell #f))
+
+(define (ct-isBlockAll)
+  (thread-cell-ref ct-blockAll))
+
+(define (ct-setBlockAll x)
+  (thread-cell-set! ct-blockAll x))
+
+; Check encodings of normal forms
+(define (ct-isDataCon val)
+  (and (vector? val) (>= (vector-ref val 0) 0)))
+(define (ct-isConstant val)
+  (or (number? val) (string? val) (char? val)
+      (and (vector? val) (<= (vector-ref val 0) -100))))
+(define (ct-isTypeCon val)
+  (and (vector? val) (= (vector-ref val 0) -1)))
+(define (ct-isBlocked val)
+  (and (vector? val) (= (vector-ref val 0) -2)))
+(define (ct-isPi val)
+  (and (vector? val) (= (vector-ref val 0) -3)))
+(define (ct-isTypeMatchable val)
+  (or (ct-isTypeCon val) (ct-isPi val)))
+(define (ct-isDelay val)
+  (and (vector? val) (= (vector-ref val 0) -4)))
+(define (ct-isForce val)
+  (and (vector? val) (= (vector-ref val 0) -5)))
+(define (ct-isErased val)
+  (and (vector? val) (= (vector-ref val 0) -6)))
+(define (ct-isType val)
+  (and (vector? val) (= (vector-ref val 0) -7)))
+(define (ct-isLambda val)
+  (and (vector? val) (= (vector-ref val 0) -8)))
+(define (ct-isTopLambda val)
+  (and (vector? val) (= (vector-ref val 0) -9)))
+
+; A function might be a blocked application, which is represented as
+; a vector (-1, name, args), so make a new vector extending args
+; (or a meta, which is a vector (-10, name, args))
+(define (ct-addArg f a)
+    (if (vector? f)
+        (vector (vector-ref f 0) (vector-ref f 1)
+             (append (vector-ref f 2) (list a)))
+        (vector -11 f (list a))))
+
+; to apply a function, either run it if it is a function, or add
+; a blocked argument if it's stuck
+(define (ct-app f a)
+   (cond
+     [(ct-isTopLambda f) ((vector-ref f 2) a)]
+     [(ct-isLambda f) ((vector-ref f 1) a)]
+     [(procedure? f) (f a)]
+     [else (ct-addArg f a)]))
+
+; force a delayed evaluation
+(define (ct-doForce arg default)
+    (if (ct-isDelay arg)
+        ((vector-ref arg 4))
+        default))
+
+; primitives
+(define ct-toSignedInt
+  (lambda (x bits)
+    (if (logbit? bits x)
+        (logor x (ash (- 1) bits))
+        (logand x (- (ash 1 bits) 1)))))
+
+(define ct-toUnsignedInt
+  (lambda (x bits)
+    (modulo x (ash 1 bits))))
+
+(define ct-u+ (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toUnsignedInt (+ xval yval) bits)))))
+(define ct-u- (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toUnsignedInt (- xval yval) bits)))))
+(define ct-u* (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toUnsignedInt (* xval yval) bits)))))
+(define ct-u/ (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toUnsignedInt (quotient xval yval) bits)))))
+
+(define ct-s+ (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (+ xval yval) bits)))))
+(define ct-s- (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (- xval yval) bits)))))
+(define ct-s* (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (* xval yval) bits)))))
+(define ct-s/ (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (quotient xval yval) bits)))))
+
+(define ct+ (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (+ xval yval)))))
+(define ct- (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (- xval yval)))))
+(define ct* (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (* xval yval)))))
+(define ct/ (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (quotient xval yval)))))
+
+(define ct-mod (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (remainder xval yval)))))
+
+(define ct-neg (lambda (x)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))]
+          (vector tag (- xval)))))
+
+(define ct-bits-shl-signed (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ct-toSignedInt (shl xval yval) bits)))))
+(define ct-bits-shl (lambda (x y bits)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (remainder (ash xval yval) (ash 1 bits))))))
+(define ct-shl (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ash xval yval)))))
+
+(define ct-shr (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (ash xval (- yval))))))
+
+(define ct-and (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (logand xval yval)))))
+(define ct-or (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (logor xval yval)))))
+(define ct-xor (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (vector tag (logxor xval yval)))))
+
+(define ct-string-ref (lambda (x i)
+    (let [(ival (vector-ref i 1))]
+         (if (and (>= ival 0) (< ival (string-length x)))
+             (string-ref x ival)
+             '()))))
+(define ct-string-cons (lambda (x y) (string-append (string x) y)))
+(define ct-string-reverse (lambda (x)
+  (list->string (reverse (string->list x)))))
+(define (ct-string-substr offin lenin s)
+    (let* [(off (vector-ref offin 1))
+           (len (vector-ref lenin 1))
+           (l (string-length s))
+           (b (max 0 off))
+           (x (max 0 len))
+           (end (min l (+ b x)))]
+          (if (> b l)
+              ""
+              (substring s b end))))
+
+; Don't wrap the result for bool results, we do that in Builtins.idr
+(define ct< (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (< xval yval))))
+(define ct<= (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (<= xval yval))))
+(define ct= (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (= xval yval))))
+(define ct>= (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (>= xval yval))))
+(define ct> (lambda (x y)
+    (let [(tag (vector-ref x 0))
+          (xval (vector-ref x 1))
+          (yval (vector-ref y 1))]
+          (> xval yval))))
+
+; casts
+; when targetting integers, we add the Vector on the Idris side
+
+(define ct-cast-num
+  (lambda (x)
+    (if (number? x) x 0)))
+(define destroy-prefix
+  (lambda (x)
+    (cond
+      ((equal? x "") "")
+      ((equal? (string-ref x 0) #\#) "")
+      (else x))))
+
+(define ct-cast-string-double
+  (lambda (x)
+    (cast-num (string->number (destroy-prefix x)))))
+
+(define ct-cast-char-boundedInt
+  (lambda (x y)
+    (ct-toSignedInt (char->integer x) y)))
+
+(define ct-cast-char-boundedUInt
+  (lambda (x y)
+    (ct-toUnsignedInt (char->integer x) y)))
+
+(define ct-cast-int-char
+  (lambda (xin)
+    (let [(x (vector-ref xin 1))]
+      (if (or
+          (and (>= x 0) (<= x #xd7ff))
+          (and (>= x #xe000) (<= x #x10ffff)))
+        (integer->char x)
+        (integer->char 0)))))
+
+(define ct-cast-string-int
+  (lambda (x)
+    (exact-truncate (cast-num (string->number (destroy-prefix x))))))
+
+(define ct-cast-string-boundedInt
+  (lambda (x y)
+    (blodwen-toSignedInt (cast-string-int x) y)))
+
+(define ct-cast-string-boundedUInt
+  (lambda (x y)
+    (blodwen-toUnsignedInt (cast-string-int x) y)))
+
+(define ct-cast-number-string
+  (lambda (xin)
+    (let [(x (vector-ref xin 1))]
+      (number->string x))))
+
+(define ct-exact-truncate
+  (lambda (x)
+    (inexact->exact (truncate x))))
+
+(define ct-exact-truncate-boundedInt
+  (lambda (x y)
+    (ct-toSignedInt (exact-truncate x) y)))
+
+(define ct-exact-truncate-boundedUInt
+  (lambda (x y)
+    (ct-toUnsignedInt (exact-truncate x) y)))
+
+(define ct-int-double
+  (lambda (xin)
+    (let [(x (vector-ref xin 1))]
+      (exact->inexact x))))
diff --git a/support/racket/support.rkt b/support/racket/support.rkt
index 921b08e37..b8c58e302 100644
--- a/support/racket/support.rkt
+++ b/support/racket/support.rkt
@@ -490,7 +490,9 @@
 ; read a scheme string and evaluate it, returning 'Just result' on success
 ; TODO: catch exception!
 (define (blodwen-eval-scheme str)
-  (box (eval (read (open-input-string str)) ns))) ; box == Just
+  (with-handlers ([exn:fail? (lambda (x) '())]) ; Nothing on failure
+     (box (eval (read (open-input-string str)) ns))) ; box == Just
+)
 
 (define (blodwen-eval-okay obj)
   (if (null? obj)
diff --git a/tests/Main.idr b/tests/Main.idr
index 07709affd..19b915090 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -180,6 +180,13 @@ idrisTestsTotality = MkTestPool "Totality checking" [] Nothing
        "total011", "total012"
       ]
 
+-- This will only work with an Idris compiled via Chez or Racket, but at
+-- least for the moment we're not officially supporting self hosting any
+-- other way. If we do, we'll need to have a way to disable these.
+idrisTestsSchemeEval : TestPool
+idrisTestsSchemeEval = MkTestPool "Scheme Evaluator" [] Nothing
+     ["schemeeval001", "schemeeval002", "schemeeval003", "schemeeval004"]
+
 idrisTests : TestPool
 idrisTests = MkTestPool "Misc" [] Nothing
        -- Documentation strings
@@ -320,6 +327,7 @@ main = runner $
   , testPaths "idris2" idrisTestsBuiltin
   , testPaths "idris2" idrisTestsEvaluator
   , testPaths "idris2" idrisTestsTotality
+  , testPaths "idris2" idrisTestsSchemeEval
   , testPaths "idris2" idrisTests
   , !typeddTests
   , !ideModeTests
diff --git a/tests/idris2/schemeeval001/expected b/tests/idris2/schemeeval001/expected
new file mode 100644
index 000000000..e88288353
--- /dev/null
+++ b/tests/idris2/schemeeval001/expected
@@ -0,0 +1,5 @@
+Main> [scheme] Main> \x, y => plus x y
+[scheme] Main> \x, y => plus y x
+[scheme] Main> \x => S (S (plus x x))
+[scheme] Main> \x => plus x (S (S x))
+[scheme] Main> Bye for now!
diff --git a/tests/idris2/schemeeval001/input b/tests/idris2/schemeeval001/input
new file mode 100644
index 000000000..9f0d3faae
--- /dev/null
+++ b/tests/idris2/schemeeval001/input
@@ -0,0 +1,6 @@
+:set eval scheme
+\x, y => plus x y
+\x : Nat, y => y + x
+\x => plus (S (S x)) x
+\x => plus x (S (S x))
+:q
diff --git a/tests/idris2/schemeeval001/run b/tests/idris2/schemeeval001/run
new file mode 100755
index 000000000..47008ffee
--- /dev/null
+++ b/tests/idris2/schemeeval001/run
@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner < input
+
diff --git a/tests/idris2/schemeeval002/expected b/tests/idris2/schemeeval002/expected
new file mode 100644
index 000000000..e292dc48e
--- /dev/null
+++ b/tests/idris2/schemeeval002/expected
@@ -0,0 +1,3 @@
+Main> [scheme] Main> [scheme] Main> 700000
+[scheme] Main> 0.30000000000000004
+[scheme] Main> Bye for now!
diff --git a/tests/idris2/schemeeval002/input b/tests/idris2/schemeeval002/input
new file mode 100644
index 000000000..004bde086
--- /dev/null
+++ b/tests/idris2/schemeeval002/input
@@ -0,0 +1,5 @@
+:set eval scheme
+-- Partly a performance test, partly to test primitives
+natToInteger (plus (integerToNat 300000) (integerToNat 400000))
+the Double 0.1+0.2
+:q
diff --git a/tests/idris2/schemeeval002/run b/tests/idris2/schemeeval002/run
new file mode 100755
index 000000000..47008ffee
--- /dev/null
+++ b/tests/idris2/schemeeval002/run
@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner < input
+
diff --git a/tests/idris2/schemeeval003/expected b/tests/idris2/schemeeval003/expected
new file mode 100644
index 000000000..fc0cd676c
--- /dev/null
+++ b/tests/idris2/schemeeval003/expected
@@ -0,0 +1,3 @@
+Main> [scheme] Main> 1 :: Delay (countFrom (1 + 1) (\{arg:0} => prim__add_Integer 1 arg))
+[scheme] Main> [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
+[scheme] Main> Bye for now!
diff --git a/tests/idris2/schemeeval003/input b/tests/idris2/schemeeval003/input
new file mode 100644
index 000000000..ff53b2d15
--- /dev/null
+++ b/tests/idris2/schemeeval003/input
@@ -0,0 +1,4 @@
+:set eval scheme
+[1..]
+take 10 [1..]
+:q
diff --git a/tests/idris2/schemeeval003/run b/tests/idris2/schemeeval003/run
new file mode 100755
index 000000000..47008ffee
--- /dev/null
+++ b/tests/idris2/schemeeval003/run
@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner < input
+
diff --git a/tests/idris2/schemeeval004/expected b/tests/idris2/schemeeval004/expected
new file mode 100644
index 000000000..d33358d4b
--- /dev/null
+++ b/tests/idris2/schemeeval004/expected
@@ -0,0 +1,5 @@
+1/1: Building list (list.idr)
+Main> [scheme] Main> False :: (False :: (False :: (False :: (False :: (False :: (False :: (False :: (False :: (False :: ?help)))))))))
+[scheme] Main> S (S (S (S (S (S (S (S (S (S (length ?help))))))))))
+[scheme] Main> True
+[scheme] Main> Bye for now!
diff --git a/tests/idris2/schemeeval004/input b/tests/idris2/schemeeval004/input
new file mode 100644
index 000000000..1182cd215
--- /dev/null
+++ b/tests/idris2/schemeeval004/input
@@ -0,0 +1,5 @@
+:set eval scheme
+mkList False 10
+length (mkList False 10)
+isEven (length (replicate 200000 False))
+:q
diff --git a/tests/idris2/schemeeval004/list.idr b/tests/idris2/schemeeval004/list.idr
new file mode 100644
index 000000000..d9e0b5d58
--- /dev/null
+++ b/tests/idris2/schemeeval004/list.idr
@@ -0,0 +1,11 @@
+import Data.List
+
+mkList : a -> Nat -> List a
+mkList x Z = ?help
+mkList x (S k) = x :: mkList x k
+
+-- For a performance test: make sure we evaluate the full list, and get
+-- a result that we don't have to work hard to render
+isEven : Nat -> Bool
+isEven Z = True
+isEven (S k) = not (isEven k)
diff --git a/tests/idris2/schemeeval004/run b/tests/idris2/schemeeval004/run
new file mode 100755
index 000000000..24353950f
--- /dev/null
+++ b/tests/idris2/schemeeval004/run
@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner list.idr < input
+