Fix issue where top level is expanded, but stuck on Case

newt/Tree.newt

@@ -56,7 +56,7 @@ data T23 : Bnd -> Bnd -> Nat -> U where
     (tlx : T23 l (N x) h) (txy : T23 (N x) (N y) h) (tyu : T23 (N y) u h) ->
     T23 l u (S h)
 
--- -- 56:
+-- 56:
 
 infixl 5 _*_
 infixl 1 _,_

src/Lib/Elab.idr

@@ -230,7 +230,7 @@ parameters (ctx: Context)
           _ => error ctx.fc "unify failed \{show t'} =?= \{show u'} [no Fn]\n  env is \{show ctx.env} \{show $ map fst ctx.types}"
 
       (VRef fc k def sp, u) => do
-        debug "expand %ref \{k} =?= \{show u}"
+        debug "expand %ref \{k} \{show sp} =?= \{show u}"
         case lookup k !(get) of
           Just (MkEntry name ty (Fn tm)) => unify l !(vappSpine !(eval [] CBN tm) sp) u
           _ => error ctx.fc "unify failed \{show t'} [no Fn] =?= \{show u'}\n  env is \{show ctx.env} \{show $ map fst ctx.types}"
@@ -690,9 +690,10 @@ check ctx tm ty = case (tm, !(forceType ty)) of
   (t@(RLam fc nm icit tm), ty) =>
             error fc "Expected pi type, got \{!(prvalCtx ty)}"
 
+  -- NOW Test1.newt passes with Explicit, TestCase4.newt passes with Implicit
   (tm, ty@(VPi fc nm' Implicit a b)) => do
     let names = toList $ map fst ctx.types
-    debug "XXX edge add implicit lambda to \{show tm}"
+    debug "XXX edge add implicit lambda {\{nm'} : \{show a}} to \{show tm} "
     let var = VVar fc (length ctx.env) [<]
     ty' <- b $$ var
     debugM $ pure "XXX ty' is \{!(prvalCtx {ctx=(extend ctx nm' a)} ty')}"

src/Lib/Eval.idr

@@ -72,10 +72,25 @@ bind v env = v :: env
 --   - Applications headed by top-level variables are lazy.
 --   - Any other function application is call-by-value during evaluation.
 
--- TODO - probably want to figure out gluing and handle constructors
+-- TODO maybe add glueing
+
+-- So this is a tricky bit - I don't want to expand top level functions
+-- if I can't get past the case tree.  Kovacs' eval doesn't have the spine
+-- when it starts applying. So I'll collect a spine as soon as I see an App
+-- Try to apply the Ref, and fall back to vappSpine.
+evalSpine : Env -> Mode -> Tm -> List Val -> M Val
+evalSpine env mode (App _ t u) sp = evalSpine env mode t (!(eval env mode u) :: sp)
+evalSpine env mode (Ref fc nm (Fn tm)) sp = do
+  v <- eval env mode tm
+  let sp' = [<] <>< sp
+  case !(vappSpine v sp') of
+    (VCase x sc xs) => pure $ VRef fc nm (Fn tm) sp'
+    v => pure v
+evalSpine env mode tm sp = vappSpine !(eval env mode tm) ([<] <>< sp)
+
 eval env mode (Ref _ x (Fn tm)) = eval env mode tm
 eval env mode (Ref fc x def) = pure $ VRef fc x def [<]
-eval env mode (App _ t u) = vapp !(eval env mode t) !(eval env mode u)
+eval env mode (App _ t u) = evalSpine env mode t [!(eval env mode u)]
 eval env mode (U fc) = pure (VU fc)
 eval env mode (Meta fc i) =
   case !(lookupMeta i) of