fixes to eval

.gitignore

@@ -6,7 +6,7 @@ build/
 *.bak
 *.agda
 *.agdai
-/*.js
+/newt*.js
 input.txt
 node_modules
 mkday.py

Makefile

@@ -29,7 +29,7 @@ newt.so: newt.ss prim.ss
 	chez --script scripts/compile-chez.ss
 
 newt2.ss: newt.so
-	chez --program newt.ss src/Main.newt -o newt2.ss
+	time chez --program newt.so src/Main.newt -o newt2.ss
 
 test: newt.js
 	scripts/test

src/Lib/Elab.newt

@@ -138,7 +138,6 @@ findMatches ctx ty ((name, type) :: xs) = do
       debug $ \ _ => "TRY \{show name} : \{rpprint Nil type} for \{show ty}"
       -- This check is solving metas, so we save mc below in case we want this solution
       let (QN ns nm) = name
-      let (cod, tele) = splitTele type
       setMetaMode CheckFirst
       tm <- check ctx (RVar fc nm) ty
       debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}"
@@ -344,19 +343,9 @@ rename meta ren lvl (VPi fc n icit rig ty tm) = do
   pure (Pi fc n icit rig ty' scope')
 rename meta ren lvl (VU fc) = pure (UU fc)
 rename meta ren lvl (VErased fc) = pure (Erased fc)
--- for now, we don't do solutions with case in them.
+-- for now, we don't do solutions with case, let, letrec in them
-rename meta ren lvl (VCase fc sc alts) = error fc "Case in solution"
+-- If we we need this, follow the model of VLam
-rename meta ren lvl (VLit fc lit) = pure (Lit fc lit)
+rename meta ren lvl tm = error (getFC tm) "Unhandled term in `rename`: \{show tm}"
-rename meta ren lvl (VLet fc name val body) = do
-  val' <- rename meta ren lvl val
-  body' <- rename meta (lvl :: ren) (1 + lvl) body
-  pure $ Let fc name val' body'
--- these probably shouldn't show up in solutions...
-rename meta ren lvl (VLetRec fc name ty val body) = do
-  ty' <- rename meta ren lvl ty
-  val' <- rename meta (lvl :: ren) (1 + lvl) val
-  body' <- rename meta (lvl :: ren) (1 + lvl) body
-  pure $ LetRec fc name ty' val' body'
 
 lams : Nat -> List String -> Tm -> Tm
 lams Z _ tm = tm
@@ -749,7 +738,6 @@ substVal k v tm = go tm
   where
     go : Val -> Val
     go (VVar fc j sp) = if j == k then v else (VVar fc j (map go sp))
-    go (VLet fc nm a b) = VLet fc nm (go a) b
     go (VPi fc nm icit rig a b) = VPi fc nm icit rig (go a) b
     go (VMeta fc ix sp) = VMeta fc ix (map go sp)
     go (VRef fc nm sp) = VRef fc nm (map go sp)

src/Lib/Eval.newt

@@ -9,6 +9,7 @@ import Lib.TopContext
 import Data.IORef
 import Data.SnocList
 import Data.SortedMap
+import Lib.Error
 
 eval : Env -> Tm -> M Val
 
@@ -27,6 +28,7 @@ vapp (VLam _ _ _ _ t) u = t $$ u
 vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u)
 vapp (VRef fc nm sp) u = pure $ VRef fc nm (sp :< u)
 vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u)
+-- not really impossible, could be a stuck VCase.
 vapp t u = error' "impossible in vapp \{show t} to \{show u}\n"
 
 vappSpine : Val -> SnocList Val -> M Val
@@ -69,8 +71,9 @@ tryEval env (VRef fc k sp) = do
             vtm <- eval env tm
             debug $ \ _ =>  "tm is \{render 90 $ pprint Nil tm}"
             val <- vappSpine vtm sp
+            -- These are considered "stuck" and we back out to the nearest name application
             case val of
-              VCase _ _ _ => pure Nothing
+              VCase _ _ _ _ => pure Nothing
               VLam _ _ _ _ _ => pure Nothing
               -- For now? There is a spot in Compile.newt that has
               -- two applications of fresh that is getting unfolded even
@@ -78,7 +81,7 @@ tryEval env (VRef fc k sp) = do
               -- coming out of a let and is instantly applied
               VLetRec _ _ _ _ _ => pure Nothing
               v => pure $ Just v)
-            (\ _ => pure Nothing)
+            (const $ pure Nothing)
       _ => do
         debug $ \ _ => "tryEval blocked on undefined \{show k}"
         pure Nothing
@@ -98,7 +101,7 @@ forceType env x = do
     | _ => pure x
   forceType env x'
 
--- for cases applied to a value
+-- Handles cases applied to a value, return Nothing if stuck
 -- TODO this does not handle CaseLit
 evalCase : Env -> Val -> List CaseAlt -> M (Maybe Val)
 evalCase env sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do
@@ -112,40 +115,19 @@ evalCase env sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do
       -- bail for a stuck function
       _ => pure Nothing
   where
+    -- put constructor args into scope
     pushArgs : Env -> List Val -> List String -> M (Maybe Val)
     pushArgs env (arg :: args) (nm :: nms) = pushArgs (arg :: env) args nms
-    pushArgs env args Nil = do
+    pushArgs env Nil Nil = Just <$> eval env t
-      t' <- eval env t
+    pushArgs env args Nil = fatalError "Extra args \{show args}"
-      Just <$> vappSpine t' (Lin <>< args)
     pushArgs env Nil rest = pure Nothing
--- REVIEW - this is handled in the caller already
+
-evalCase env sc@(VVar fc k sp) alts = case lookupVar env k of
-    Just tt@(VVar fc' k' sp') => do
-        debug $ \ _ =>  "lookup \{show k} is \{show tt}"
-        if k' == k
-          then pure Nothing
-          else do
-            val <- vappSpine (VVar fc' k' sp') sp
-            evalCase env val alts
-    Just t => do
-      val <- vappSpine t sp
-      evalCase env val alts
-    Nothing => do
-        debug $ \ _ =>  "lookup \{show k} is Nothing in env \{show env}"
-        pure Nothing
 evalCase env sc (CaseDefault u :: xs) = Just <$> eval env u
 evalCase env sc cc = do
   debug $ \ _ =>  "CASE BAIL sc \{show sc} vs " -- \{show cc}"
   debug $ \ _ =>  "env is \{show env}"
   pure Nothing
 
--- neutral alts
-evalAlt : Env → CaseAlt → M VCaseAlt
-evalAlt env (CaseDefault tm) = VCaseDefault <$> eval env tm
-evalAlt env (CaseLit lit tm) = VCaseLit lit <$> eval env tm
--- in the cons case, we're binding args
-evalAlt env (CaseCons nm args tm) = pure $ VCaseCons nm args env tm
-
 -- So smalltt says:
 --   Smalltt has the following approach:
 --   - Top-level and local definitions are lazy.
@@ -173,13 +155,19 @@ eval env (Pi fc x icit rig a b) = do
   pure $ VPi fc x icit rig a' (MkClosure env b)
 eval env (Let fc nm t u) = do
   t' <- eval env t
-  u' <- eval (VVar fc (length' env) Lin :: env) u
+  --
-  pure $ VLet fc nm t' u'
+  if True
+    then pure $ VLet fc nm t' (MkClosure env u)
+    else eval (t' :: env) u
 eval env (LetRec fc nm ty t u) = do
-  ty' <- eval env ty
+  -- Used for `where`, we'd probably need to treat this like Lam.
-  t' <- eval (VVar fc (length' env) Lin :: env) t
+  error fc "eval letrec"
-  u' <- eval (VVar fc (length' env) Lin :: env) u
+  -- I think we need to handle this like lam/let, disabled for now.
-  pure $ VLetRec fc nm ty' t' u'
+  -- It should be gone by the time we hit inlining, we'll see if it arises in other cases
+  -- ty' <- eval env ty
+  -- t' <- eval (VVar fc (length' env) Lin :: env) t
+  -- u' <- eval (VVar fc (length' env) Lin :: env) u
+  -- pure $ VLetRec fc nm ty' t' u'
 -- Here, we assume env has everything. We push levels onto it during type checking.
 -- I think we could pass in an l and assume everything outside env is free and
 -- translate to a level
@@ -191,15 +179,13 @@ eval env (Lit fc lit) = pure $ VLit fc lit
 eval env tm@(Case fc sc alts) = do
   -- TODO we need to be able to tell eval to expand aggressively here.
   sc' <- eval env sc
-  sc' <- unlet env sc' -- try to expand lets from pattern matching
+  -- inline metas and do beta reduction at head
-  -- possibly too aggressive?
   sc' <- forceType env sc'
   Nothing <- evalCase env sc' alts
     | Just v => pure v
 
   vsc <- eval env sc
-  alts' <- traverse (evalAlt env) alts
+  pure $ VCase fc vsc env alts
-  pure $ VCase fc vsc alts'
 
 quote : (lvl : Int) -> Val -> M Tm
 
@@ -210,10 +196,14 @@ quoteSp lvl t (xs :< x) = do
   x' <- quote lvl x
   pure $ App emptyFC t' x'
 
-quoteAlt : Int → VCaseAlt → M CaseAlt
+normAlt : Env → Int → CaseAlt → M CaseAlt
-quoteAlt l (VCaseDefault val) = CaseDefault <$> quote l val
+normAlt env l (CaseDefault tm) = do
-quoteAlt l (VCaseLit lit val) = CaseLit lit <$> quote l val
+   val <- eval env tm
-quoteAlt l (VCaseCons nm args env tm) = do
+   CaseDefault <$> quote l val
+normAlt env l (CaseLit lit tm) = do
+   val <- eval env tm
+   CaseLit lit <$> quote l val
+normAlt env l (CaseCons nm args tm) = do
   val <- eval (mkenv l env args) tm
   tm <- quote (length' args + l) val
   pure $ CaseCons nm args tm
@@ -224,7 +214,7 @@ quoteAlt l (VCaseCons nm args env tm) = do
 
 quote l (VVar fc k sp) = if k < l
   then quoteSp l (Bnd fc (lvl2ix l k )) sp -- level to index
-  else error fc "Bad index in quote \{show k} depth \{show l}"
+  else error fc "Bad level in quote \{show k} depth \{show l}"
 quote l (VMeta fc i sp) = do
   meta <- lookupMeta i
   case meta of
@@ -241,6 +231,7 @@ quote l (VPi fc x icit rig a b) = do
   pure $ Pi fc x icit rig a' tm
 quote l (VLet fc nm t u) = do
   t' <- quote l t
+  u <- u $$ VVar fc l Lin
   u' <- quote (1 + l) u
   pure $ Let fc nm t' u'
 quote l (VLetRec fc nm ty t u) = do
@@ -250,10 +241,11 @@ quote l (VLetRec fc nm ty t u) = do
   pure $ LetRec fc nm ty' t' u'
 quote l (VU fc) = pure (UU fc)
 quote l (VRef fc n sp) = quoteSp l (Ref fc n) sp
-quote l (VCase fc sc valts) = do
+quote l (VCase fc sc env alts) = do
   sc' <- quote l sc
-  alts <- traverse (quoteAlt l) valts
+  alts' <- traverse (normAlt env l) alts
-  pure $ Case fc sc' alts
+  pure $ Case fc sc' alts'
+
 quote l (VLit fc lit) = pure $ Lit fc lit
 quote l (VErased fc) = pure $ Erased fc
 
@@ -268,7 +260,6 @@ prvalCtx {{ctx}} v = do
   tm <- quote ctx.lvl v
   pure $ render 90 $ pprint (map fst ctx.types) tm
 
-
 -- 'zonk' is substituting metas _and_ doing inlining
 
 -- It is a flavor of eval, maybe we could combine them with some flags
@@ -309,23 +300,37 @@ zonkApp top l env t@(Meta fc k) sp = do
   meta <- lookupMeta k
   case meta of
     (Solved _ j v) => do
+      debug $ \ _ => "zonk for \{show k} env \{show env}"
+      debug $ \ _ => "spine \{show sp}"
       sp' <- traverse (eval env) sp
-      debug $ \ _ =>  "zonk \{show k} -> \{show v} spine \{show sp'}"
+      debug $ \ _ =>  "zonk meta \{show k} -> \{show v} spine \{show sp'}"
       foo <- vappSpine v (Lin <>< sp')
       debug $ \ _ =>  "-> result is \{show foo}"
-      tweakFC fc <$> quote l foo
+      if length' env /= l
+        then fatalError "MM2 \{show l} /= \{show $ length' env}"
+        else pure MkUnit
+      res <- tweakFC fc <$> quote l foo
+      debug $ \ _ => "quoted \{show res}"
+      pure res
     _ => pure $ appSpine t sp
 zonkApp top l env t sp = do
+  debug $ \ _ => "zonk2 for \{show t} env \{show env}"
+  debug $ \ _ => "spine \{show sp}"
   t' <- zonk top l env t
   -- inlining
   let (Just tm) = inlineDef t' | _ => pure $ appSpine t' sp
   sp' <- traverse (eval env) sp
   vtm <- eval env tm
   catchError (do
-    foo <- vappSpine vtm (Lin <>< sp')
+    debug $ \ _ =>  "zonk will app \{show t'} @ \{show sp} ~> \{show vtm} @ \{show sp'}"
-    t' <- quote l foo
+    res <- vappSpine vtm (Lin <>< sp')
-    zonk top l env t')
+    debug $ \_ => "result is \{show res}"
-    (\_ => pure $ appSpine t' sp)
+    t' <- quote l res
+    x <- zonk top l env t'
+    pure x)
+    (\err => do
+      debug $ \_ => "result err \{showError "" err}"
+      pure $ appSpine t' sp)
   where
     -- lookup name and return Def if flagged inline
     inlineDef : Tm → Maybe Tm

src/Lib/ProcessDecl.newt

@@ -310,6 +310,7 @@ processInstance ns instfc ty decls = do
   vdcty@(VPi _ nm icit rig a b) <- eval Nil dcty
     | x => error (getFC x) "dcty not Pi"
   debug $ \ _ => "dcty \{render 90 $ pprint Nil dcty}"
+  -- let (_,args) = funArgs codomain
 
   debug $ \ _ => "traverse \{show $ map show args}"
   -- This is a little painful because we're reverse engineering the
@@ -546,9 +547,6 @@ processRecord ns recordFC (nameFC, nm) tele cname decls = do
     processFields : Raw → Raw → List (String × Raw) → List (FC × String × Raw) → M Unit
     processFields _ _ _ Nil = pure MkUnit
     processFields autoPat tail deps ((fc,name,ty) :: rest) = do
-      -- TODO dependency isn't handled yet
-      -- we'll need to replace stuff like `len` with `len self`.
-
       let funType = substRaw deps $ teleToPi (impTele tele) $ RPi fc (BI fc "$self" Explicit Many) tail ty
 
       -- `.fieldName`

src/Lib/Types.newt

@@ -23,7 +23,10 @@ derive Show BD
 
 data Quant = Zero | Many
 derive Eq Quant
-derive Show Quant
+
+instance Show Quant where
+  show Zero = "0 "
+  show Many = ""
 
 -- We could make this polymorphic and use for environment...
 
@@ -169,20 +172,15 @@ Val : U
 Closure : U
 Env : U
 
-data VCaseAlt : U where
-  -- Like a Closure, but with a lot of args
-  VCaseCons : (name : QName) -> (args : List String) -> Env -> Tm ->  VCaseAlt
-  VCaseLit : Literal -> Val -> VCaseAlt
-  VCaseDefault : Val -> VCaseAlt
-
 data Val : U where
   VVar : FC -> (k : Int) -> (sp : SnocList Val) -> Val
   VRef : FC -> (nm : QName) -> (sp : SnocList Val) -> Val
-  VCase : FC -> (sc : Val) -> List VCaseAlt -> Val
+  VCase : FC -> (sc : Val) -> Env -> List CaseAlt -> Val
   VMeta : FC -> QName -> (sp : SnocList Val) -> Val
   VLam : FC -> Name -> Icit -> Quant -> Closure -> Val
   VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val
-  VLet : FC -> Name -> Val -> Val -> Val
+  -- not substing let, like idris
+  VLet : FC -> Name -> Val -> Closure -> Val
   VLetRec : FC -> Name -> Val -> Val -> Val -> Val
   VU : FC -> Val
   VErased : FC -> Val
@@ -196,7 +194,7 @@ data Closure = MkClosure Env Tm
 getValFC : Val -> FC
 getValFC (VVar fc _ _) = fc
 getValFC (VRef fc _ _) = fc
-getValFC (VCase fc _ _) = fc
+getValFC (VCase fc _ _ _) = fc
 getValFC (VMeta fc _ _) = fc
 getValFC (VLam fc _ _ _ _) = fc
 getValFC (VPi fc _ _ _ a b) = fc
@@ -220,15 +218,10 @@ instance Show Val where
   show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show  x}}. \{showClosure  y})"
   show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show  x}). \{showClosure  y})"
   show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show  x}}}. \{showClosure  y})"
-  show (VCase fc sc alts) = "(%case \{show sc} \{unwords $ map showAlt alts})"
+  show (VCase fc sc env alts) = "(%case \{show sc} \{unwords $ map show alts})"
-    where
-      showAlt : VCaseAlt → String
-      showAlt (VCaseDefault v) = "(%cdef \{show v})"
-      showAlt (VCaseLit lit v) = "(%clit \{show v})"
-      showAlt (VCaseCons nm args env v) = "(%ccon \{show nm} \{unwords $ map show args} [\{show $ length env} env] \{show v}"
   show (VU _) = "U"
   show (VLit _ lit) = show lit
-  show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}"
+  show (VLet _ nm a (MkClosure env b)) = "(%let \{show nm} = \{show a} in \{show b}"
   show (VLetRec _ nm ty a b) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}"
   show (VErased _) = "ERASED"
 
@@ -269,7 +262,10 @@ record MetaContext where
 
 derive Eq MetaMode
 
-data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon | TrueCon | FalseCon | NilCon | ConsCon
+data ConInfo = NormalCon
+             | SuccCon | ZeroCon
+             | EnumCon | TrueCon | FalseCon
+             | NilCon | ConsCon
 
 derive Eq ConInfo