expand scrutinee in eval

playground/samples/Tour.newt

@@ -16,7 +16,7 @@
   on hover.  I'm emitting INFO for solved metas.
 
   The Day1.newt and Day2.newt are last year's advent of code, translated
-  from Lean.  You need to visit `Lib.newt` to get it to the worker.
+  from Lean.
 
 -/
 

src/Lib/Elab.idr

@@ -58,17 +58,6 @@ forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
   (Solved _ k t) => vappSpine t sp >>= forceMeta
 forceMeta x = pure x
 
-tryEval : Val -> M (Maybe Val)
-tryEval (VRef fc k _ sp) =
-  case lookup k !(get) of
-      Just (MkEntry name ty (Fn tm)) => do
-          vtm <- eval [] CBN tm
-          case !(vappSpine vtm sp) of
-            VCase{} => pure Nothing
-            v => pure $ Just v
-      _ => pure Nothing
-tryEval _ = pure Nothing
-
 -- Force far enough to compare types
 forceType : Val -> M Val
 forceType (VMeta fc ix sp) = case !(lookupMeta ix) of

src/Lib/Eval.idr

@@ -4,6 +4,7 @@ module Lib.Eval
 import Lib.Parser.Impl
 import Lib.Prettier
 import Lib.Types
+import Lib.TopContext
 import Control.Monad.Error.Interface
 
 import Data.IORef
@@ -44,6 +45,18 @@ vappSpine : Val -> SnocList Val -> M Val
 vappSpine t [<] = pure t
 vappSpine t (xs :< x) = vapp !(vappSpine t xs) x
 
+export
+tryEval : Val -> M (Maybe Val)
+tryEval (VRef fc k _ sp) =
+  case lookup k !(get) of
+      Just (MkEntry name ty (Fn tm)) => do
+          vtm <- eval [] CBN tm
+          case !(vappSpine vtm sp) of
+            VCase{} => pure Nothing
+            v => pure $ Just v
+      _ => pure Nothing
+tryEval _ = pure Nothing
+
 evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val)
 evalCase env mode sc@(VRef _ nm _ sp) (cc@(CaseCons name nms t) :: xs) =
   if nm == name
@@ -94,11 +107,12 @@ eval env mode (Bnd fc i) = case getAt i env of
   Nothing => error' "Bad deBruin index \{show i}"
 eval env mode (Lit fc lit) = pure $ VLit fc lit
 
-eval env mode tm@(Case fc sc alts) =
+eval env mode tm@(Case fc sc alts) = do
-  case !(evalCase env mode !(eval env mode sc) alts) of
+  -- TODO we need to be able to tell eval to expand aggressively here.
-    Just v => pure v
+  sc' <- eval env mode sc
-    Nothing => pure $ fromMaybe (VCase fc !(eval env mode sc) alts)
+  let sc' = fromMaybe sc' !(tryEval sc')
-                                !(evalCase env mode !(eval env mode sc) alts)
+  pure $ fromMaybe (VCase fc !(eval env mode sc) alts)
+                             !(evalCase env mode sc' alts)
 
 export
 quote : (lvl : Nat) -> Val -> M Tm