Make eval less aggressive about substitution

README.md

@@ -12,10 +12,12 @@ The goal is to have inductive types, pattern matching, compile to javascript, an
 self hosted. Ideally I could build a little browser "playground" to compile, view
 output, and run code.
 
+The repository is tagging `.newt` files as Agda to convince github to highlight them.
+
 ## Building
 
 There is a `Makefile` that builds both chez and javascript versions.  They end up in
-`build/exec` as usual.  I've also added a `pack.toml`, so `pack build`
+`build/exec` as usual.  I've also added a `pack.toml`, so `pack build` also works.
 
 There is a vscode extension in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `build/exec/newt` to exist in the workspace.
 
@@ -48,6 +50,11 @@ from `Tm` to `Val`. I think I'll need a way to eval a VCase during unification,
 
 Following kovacs, I'm putting `VVar` into context env when I go under binders. This avoids substitution.
 
+## Autos
+
+Newt has primitive auto implicits. As a first pass, higher order ones, like monad, will not
+
+
 ## Issues
 
 - I should do some erasure of values unused at runtime

TODO.md

@@ -1,6 +1,14 @@
 
 ## TODO
 
+NOW - two things
+
+1. I broke Tree.newt by removing some over-aggressive reduction.  I need to
+make it happen during unification. Not sure if I have all of the bits to vappspine there.
+
+2. Need to collect constraints and re-run, I think that may get me to
+typeclasses
+
 - [x] Remember operators from imports
 - [ ] Default cases for non-primitives (currently gets expanded to all constructors)
 - [x] Case for primitives

newt/TypeClass.newt

@@ -26,34 +26,42 @@ data Either : U -> U -> U where
   Left : {A B : U} -> A -> Either A B
   Right : {A B : U} -> B -> Either A B
 
-EitherMonad : {A : U} -> Monad (Either A)
-EitherMonad = MkMonad {Either A} (\ ma amb =>
---                     ^ Need this for scrut type to be non-meta
-  case ma of
-    Left a => Left a
-    Right b => amb b)
+bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C
+bindEither (Left a) amb = Left a
+bindEither (Right b) amb = amb b
+
+EitherMonad : {A : U} -> Monad (Either A)
+EitherMonad = MkMonad {Either A} bindEither
+
+bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
+bindMaybe Nothing amb = Nothing
+bindMaybe (Just a) amb = amb a
+
+-- I think it was picking up the Maybe before I made it less aggressive about eval
 
--- [instance]
 MaybeMonad : Monad Maybe
--- Agda case lambda might be nice..
--- The {Maybe} isn't solved in type for the case
-MaybeMonad = MkMonad {Maybe} (\ {A} ma amb =>
-  case ma of
-      Nothing => Nothing
-      -- It doesn't discover pat$5 is A during pattern matching
-      -- oh, but var 0 value is var5
-      Just a => amb a)
+MaybeMonad = MkMonad {Maybe} bindMaybe
 
 -- So the idea here is to have some implicits that are solved by search
 
-_>>=_ : {a b : U} -> {m : U -> U} -> {x : Monad m} -> (m a) -> (a -> m b) -> m b
-_>>=_ {a} {b} {m} {MkMonad bind'}  ma amb = bind' {a} {b} ma amb
+-- Error here is from foo, with a bad FC. I think it might be showing up during search.
+_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
+_>>=_ {a} {b} {m} {{MkMonad bind'}}  ma amb = bind' {a} {b} ma amb
 
 infixl 1 _>>=_
 
 ptype Int
 
--- For now, we may try to solve this at creation time, but it's possible postpone is needed
+-- It's bailing on MaybeMonad and picking up Either?
+
+foo : Int -> Maybe Int
+foo x = (Just x) >>= (\ x  => Just 10)
+
+-- NOW
+
+-- Older notes below, but this is _close_, we're doing something like agda, and we're getting the right solution
+-- It's over-expanded, and there is an unsolved meta that I think the solution would unlock. (Need to collect and
+-- retry constraints)
 
 -- *SOLVE meta 6 sp [< (%var 0 [< ]), (%meta 4 [< (%var 0 [< ])])] val (%ref Maybe [< (%meta 9 [< (%var 0 [< ]), (%var 1 [< ])])])
 
@@ -81,8 +89,7 @@ ptype Int
 -- Agda seems complicated, minting fresh metas for bits of potential solutions (which
 -- may be tossed if the solution is ruled out.)
 
-foo : Int -> Maybe Int
-foo x = _>>=_ {_} {_} {_} {_} (Just x) (\ x  => Just 10)
+
 --                         ^
 /-
 So, agda style we'd guess ?m8 is MonadMaybe or MonadEither - agda's "maybe" case

src/Lib/Elab.idr

@@ -125,13 +125,15 @@ parameters (ctx: Context)
         -- REVIEW is this the right fc?
         then error fc "meta occurs check"
         else goSpine ren lvl (Meta fc ix) sp
-      go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar emptyFC lvl [<])))
+      go ren lvl (VLam fc n t) = pure (Lam fc n !(go (lvl :: ren) (S lvl) !(t $$ VVar fc lvl [<])))
       go ren lvl (VPi fc n icit ty tm) = pure (Pi fc n icit !(go ren lvl ty) !(go (lvl :: ren) (S lvl) !(tm $$ VVar emptyFC lvl [<])))
       go ren lvl (VU fc) = pure (U fc)
       -- for now, we don't do solutions with case in them.
       go ren lvl (VCase fc sc alts) = error fc "Case in solution"
       go ren lvl (VLit fc lit) = pure (Lit fc lit)
-      go ren lvl (VLet fc {}) = error fc "rename Let not implemented"
+      go ren lvl (VLet fc name val body) =
+        pure $ Let fc name !(go ren lvl val) !(go (lvl :: ren) (S lvl) !(body $$ VVar fc lvl [<]))
+
 
   lams : Nat -> Tm -> Tm
   lams 0 tm = tm
@@ -141,9 +143,9 @@ parameters (ctx: Context)
   export
   solve : (lvl : Nat) -> (k : Nat) -> SnocList Val -> Val -> M  ()
   solve l m sp t = do
-    debug "solve \{show m} lvl \{show l} sp \{show sp} is \{show t}"
-    meta@(Unsolved metaFC ix ctx ty _) <- lookupMeta m
+    meta@(Unsolved metaFC ix ctx ty kind) <- lookupMeta m
       | _ => error (getFC t) "Meta \{show m} already solved!"
+    debug "SOLVE \{show m} \{show kind} lvl \{show l} sp \{show sp} is \{show t}"
     let size = length $ filter (\x => x == Bound) $ toList ctx.bds
     debug "\{show m} size is \{show size}"
     if (length sp /= size) then do
@@ -234,15 +236,21 @@ parameters (ctx: Context)
 
       -- REVIEW - consider separate value for DCon/TCon
       (VRef fc k def sp,   VRef fc' k' def' sp'  ) =>
-        if k == k' then do
-          debug "unify \{show l} spine at \{k} \{show sp} \{show sp'}"
-          unifySpine l (k == k') sp sp'
-        else do
+        -- This is a problem for cmp (S x) (S y) =?= cmp x y, when the
+        -- same is an equation in cmp.
+
+        -- if k == k' then do
+        --   debug "unify \{show l} spine at \{k} \{show sp} \{show sp'}"
+        --   unifySpine l (k == k') sp sp'
+        -- else
+          do
           Nothing <- tryEval k sp
             | Just v => unify l v u'
           Nothing <- tryEval k' sp'
             | Just v => unify l t' v
-          error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}"
+          if k == k'
+            then  unifySpine l (k == k') sp sp'
+            else error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}"
 
       (VU _, VU _) => pure neutral
       -- Lennart.newt cursed type references itself
@@ -745,8 +753,8 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints [] expr) :: cs) ty) = do
 
   case pat of
     PatCon _ _ _ _ => do
-      -- expand vars that may be solved
-      scty' <- unlet ctx scty
+      -- expand vars that may be solved, eval top level functions
+      scty' <- unlet ctx scty >>= forceType
       debug "EXP \{show scty} -> \{show scty'}"
       -- this is per the paper, but it would be nice to coalesce
       -- default cases

src/Lib/Eval.idr

@@ -74,24 +74,8 @@ bind v env = v :: env
 
 -- 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)
-
--- This is too aggressive...
--- 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) = evalSpine env mode t [!(eval env mode u)]
+eval env mode (App _ t u) = vapp !(eval 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

src/Lib/ProcessDecl.idr

@@ -22,10 +22,6 @@ isCandidate (VRef _ nm _ _) (Ref fc nm' def) = nm == nm'
 isCandidate ty (App fc t u) = isCandidate ty t
 isCandidate _ _ = False
 
-    -- go : List Binder -> Tm -> (Tm, List Binder)
-    -- go ts (Pi fc nm icit t u) = go (MkBind fc nm icit t :: ts) u
-    -- go ts tm = (tm, reverse ts)
-
 
 -- This is a crude first pass
 -- TODO consider ctx
@@ -44,10 +40,11 @@ findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do
       debug "TRY \{name} : \{pprint [] type} for \{show ty}"
       tm <- check (mkCtx  top.metas fc) (RVar fc name) ty
       debug "Found \{pprint [] tm} for \{show ty}"
-      (tm ::) <$> findMatches ty xs)
-    (\ _ => do
       writeIORef top.metas mc
-      debug "No match \{show ty} \{pprint [] type}"
+      (tm ::) <$> findMatches ty xs)
+    (\ err => do
+      debug "No match \{show ty} \{pprint [] type} \{showError "" err}"
+      writeIORef top.metas mc
       findMatches ty xs)
 findMatches ty (y :: xs) = findMatches ty xs