Experimental Scheme based evaluator (#1956)

This is for compiled evaluation at compile-time, for full normalisation. You can try it by setting the evaluation mode to scheme (that is, :set eval scheme at the REPL). It's certainly an order of magnitude faster than the standard evaluator, based on my playing around with it, although still quite a bit slower than compilation for various reasons, including:

* It has to evaluate under binders, and therefore deal with blocked symbols
* It has to maintain enough information to be able to read back a Term from the evaluated scheme object, which means retaining things like types and other metadata
* We can't do a lot of the optimisations we'd do for runtime evaluation particularly setting things up so we don't need to do arity checking

Also added a new option evaltiming (set with :set evaltiming) to display how long evaluation itself takes, which is handy for checking performance.

I also don't think we should aim to replace the standard evaluator, in general, at least not for a while, because that will involve rewriting a lot of things and working out how to make it work as Call By Name (which is clearly possible, but fiddly).

Still, it's going to be interesting to experiment with it! I think it will be a good idea to use it for elaborator reflection and type providers when we eventually get around to implementing them.

Original commit details:

* Add ability to evaluate open terms via Scheme

Still lots of polish and more formal testing to do here before we can
use it in practice, but you can still use ':scheme <term>' at the REPL
to evaluate an expression by compiling to scheme then reading back the
result.

Also added 'evaltiming' option at the REPL, which, when set, displays
how long normalisaton takes (doesn't count resugaring, just the
normalisation step).

* Add scheme evaluation mode

Different when evaluating everything, vs only evaluating visible things.
We want the latter when type checking, the former at the REPL.

* Bring support.rkt up to date

A couple of missing things required for interfacing with scheme objects

* More Scheme readback machinery

We need these things in the next version so that the next-but-one
version can have a scheme evaluator!

* Add top level interface to scheme based normaliser

Also check it's available - currently chez only - and revert to the
default slow normaliser if it's not.

* Bring Context up to date with changes in main

* Now need Idris 0.5.0 to build

* Add SNF type for scheme values

This will allow us to incrementally evaluate under lambdas, which will
be useful for elaborator reflection and type providers.

* Add Quote for scheme evaluator

So, we can now get a weak head normal form, and evaluate the scope of
a binder when we have an argument to plug in, or just quote back the
whole thing.

* Add new 'scheme' evaluator mode at the REPL

Replacing the temporary 'TmpScheme', this is a better way to try out the
scheme based evaluator

* Fix name generation for new UN format

* Add scheme evaluator support to Racket

* Add another scheme eval test

With metavariables this time

* evaltiming now times execution too

This was handy for finding out the difference between the scheme based
evaluator and compilation. Compilation was something like 20 times
faster in my little test, so that'd be about 4-500 times faster than the
standard evaluator. Ouch!

* Fix whitespace errors

* Error handling when trying to evaluate Scheme

.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:
 

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

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)

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,

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

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} ->

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} ->

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

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

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)]

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

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

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

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
+
+

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

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} ->

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 ()

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

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)

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

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

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))))

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)

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))))

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)

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

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!

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

tests/idris2/schemeeval001/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner < input
+

tests/idris2/schemeeval002/expected

@@ -0,0 +1,3 @@
+Main> [scheme] Main> [scheme] Main> 700000
+[scheme] Main> 0.30000000000000004
+[scheme] Main> Bye for now!

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

tests/idris2/schemeeval002/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner < input
+

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!

tests/idris2/schemeeval003/input

@@ -0,0 +1,4 @@
+:set eval scheme
+[1..]
+take 10 [1..]
+:q

tests/idris2/schemeeval003/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner < input
+

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!

tests/idris2/schemeeval004/input

@@ -0,0 +1,5 @@
+:set eval scheme
+mkList False 10
+length (mkList False 10)
+isEven (length (replicate 200000 False))
+:q

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)

tests/idris2/schemeeval004/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner list.idr < input
+