addZero now works

distinguish two modes of unification
while pattern matching we return constraints on variables, and normally
we are more aggressive about evaluating when matching against a variable.
fixes to `let`
surface #check in vscode

newt/Combinatory.newt

@@ -26,8 +26,8 @@ Ctx : U
 Ctx = List Type
 
 data Ref : Type -> Ctx -> U where
-  Z : {σ : Type} {Γ : Ctx} -> Ref σ (σ :: Γ)
+  Here : {σ : Type} {Γ : Ctx} -> Ref σ (σ :: Γ)
-  S : {σ τ : Type} {Γ : Ctx} -> Ref σ Γ -> Ref σ (τ :: Γ)
+  There : {σ τ : Type} {Γ : Ctx} -> Ref σ Γ -> Ref σ (τ :: Γ)
 
 data Term : Ctx -> Type -> U where
   App : {Γ : Ctx} {σ τ : Type} -> Term Γ (σ ~> τ) -> Term Γ σ -> Term Γ τ
@@ -35,6 +35,35 @@ data Term : Ctx -> Type -> U where
   Var : {Γ : Ctx} {σ : Type} -> Ref σ Γ → Term Γ σ
 
 -- FIXME, I'm not getting an error for Nil, but it's shadowing Nil
+infixr 7 _:::_
 data Env : Ctx -> U where
   ENil : Env Nil
-  ECons : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ)
+  _:::_ : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ)
+
+-- TODO there is a problem here with coverage checking
+-- I suspect something is being split before it's ready
+
+-- lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
+-- lookup Z (x ::: y) = x
+-- lookup (S i) (x ::: env) = lookup i env
+
+
+-- lookup2 : {σ : Type} {Γ : Ctx} → Env Γ → Ref σ Γ → Val σ
+-- lookup2 (x ::: y) Here = x
+-- lookup2 (x ::: env) (There i) = lookup2 env i
+
+-- -- MixFix - this was ⟦_⟧
+-- eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
+-- eval (App t u) env = ? -- (eval t env) (eval u env)
+-- eval (Lam t) env = \ x => ? -- eval t (x ::: env)
+-- eval (Var i) env = lookup2 env i
+
+-- something really strange here, the arrow in the goal type is backwards...
+foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> ξ))
+foo {σ} {τ} {ξ} = ? -- \ x y => x
+
+-- data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
+--   -- S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x))
+--   K : {Γ : Ctx} {σ τ : Type} → Comb Γ (σ ~> τ ~> σ) (\ env => \ x => \ y => x)
+
+

newt/Debug.newt

@@ -0,0 +1,36 @@
+module Debug
+
+data Unit : U where
+  MkUnit : Unit
+
+infixr 7 _::_
+data List : U -> U where
+  Nil : {A : U} -> List A
+  _::_ : {A : U} -> A -> List A -> List A
+
+-- prj/menagerie/papers/combinatory
+
+infixr 6 _~>_
+data Type : U where
+  ι : Type
+  _~>_ : Type -> Type -> Type
+
+A : U
+A = Unit
+
+Val : Type -> U
+Val ι = A
+Val (x ~> y) = Val x -> Val y
+
+id : {a : U} -> a -> a
+id x = x
+
+-- can't get Val to expand here.
+#check (\ x => \ y => \ z => id (Val (x ~> y ~> z))) : Type -> Type -> Type -> U
+
+-- NOW something really strange here, the arrow in the goal type is backwards...
+-- I think case eval is broken.
+
+foo : {σ τ ξ : Type} → Val (σ ~> (τ ~> ξ))
+foo {σ} {τ} {ξ} = ? -- \ x y => x
+

src/Lib/Elab.idr

@@ -58,8 +58,8 @@ forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
   (Solved _ k t) => vappSpine t sp >>= forceMeta
 forceMeta x = pure x
 
-tryEval : String -> SnocList Val -> M (Maybe Val)
+tryEval : Val -> M (Maybe Val)
-tryEval k sp =
+tryEval (VRef fc k _ sp) =
   case lookup k !(get) of
       Just (MkEntry name ty (Fn tm)) => do
           vtm <- eval [] CBN tm
@@ -67,14 +67,14 @@ tryEval k sp =
             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
   (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp)
   (Solved _ k t) => vappSpine t sp >>= forceType
-forceType x@(VRef fc nm _ sp) = fromMaybe x <$> tryEval nm sp
+forceType x = fromMaybe x <$> tryEval x
-forceType x = pure x
 
 public export
 record UnifyResult where
@@ -88,6 +88,8 @@ Semigroup UnifyResult where
 Monoid UnifyResult where
   neutral = MkResult []
 
+data UnifyMode = Normal | Pattern
+
 -- We need to switch to SortedMap here
 export
 updateMeta : Context -> Nat -> (MetaEntry -> M MetaEntry) -> M ()
@@ -157,7 +159,7 @@ parameters (ctx: Context)
       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 name val body) =
-        pure $ Let fc name !(go ren lvl val) !(go (lvl :: ren) (S lvl) !(body $$ VVar fc lvl [<]))
+        pure $ Let fc name !(go ren lvl val) !(go (lvl :: ren) (S lvl) body)
 
 
   lams : Nat -> Tm -> Tm
@@ -167,7 +169,7 @@ parameters (ctx: Context)
 
 
   export
-  unify : (l : Nat) -> Val -> Val  -> M UnifyResult
+  unify : (l : Nat) -> UnifyMode -> Val -> Val  -> M UnifyResult
 
   export
   solve : (lvl : Nat) -> (k : Nat) -> SnocList Val -> Val -> M  ()
@@ -197,13 +199,13 @@ parameters (ctx: Context)
       MkMc fc ctx sp rhs => do
         val <- vappSpine soln sp
         debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}"
-        unify ctx.lvl val rhs
+        unify ctx.lvl Normal val rhs
 
-  unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val  -> M UnifyResult
+  unifySpine : Nat -> UnifyMode -> Bool -> SnocList Val -> SnocList Val  -> M UnifyResult
-  unifySpine l False _ _ = error emptyFC "unify failed at head" -- unreachable now
+  unifySpine l mode False _ _ = error emptyFC "unify failed at head" -- unreachable now
-  unifySpine l True [<] [<] = pure (MkResult [])
+  unifySpine l mode True [<] [<] = pure (MkResult [])
-  unifySpine l True (xs :< x) (ys :< y) = [| unify l x y <+> (unifySpine l True xs ys) |]
+  unifySpine l mode True (xs :< x) (ys :< y) = [| unify l mode x y <+> (unifySpine l mode True xs ys) |]
-  unifySpine l True _ _ = error emptyFC "meta spine length mismatch"
+  unifySpine l mode True _ _ = error emptyFC "meta spine length mismatch"
 
   lookupVar : Nat -> Maybe Val
   lookupVar k = let l = length ctx.env in
@@ -226,7 +228,7 @@ parameters (ctx: Context)
           pure t
   unlet x = pure x
 
-  unify l t u = do
+  unify l mode t u = do
     debug "Unify \{show ctx.lvl}"
     debug "  \{show l} \{show t}"
     debug "  =?= \{show u}"
@@ -240,32 +242,41 @@ parameters (ctx: Context)
 
       -- flex/flex
       (VMeta fc k sp,  VMeta fc' k' sp' ) =>
-        if k == k' then unifySpine l (k == k') sp sp'
+        if k == k' then unifySpine l mode (k == k') sp sp'
         -- TODO, might want to try the other way, too.
         else if length sp < length sp'
           then solve l k' sp' (VMeta fc k sp) >> pure neutral
           else solve l k sp (VMeta fc' k' sp') >> pure neutral
       (t,           VMeta fc' i' sp') => solve l i' sp' t >> pure neutral
       (VMeta fc i sp, t'           ) => solve l i sp t' >> pure neutral
-      (VPi fc _ _ a b, VPi fc' _ _ a' b') => [| unify l a a' <+> unify (S l) !(b $$ VVar emptyFC l [<]) !(b' $$ VVar emptyFC l [<]) |]
+      (VPi fc _ _ a b, VPi fc' _ _ a' b') => [| unify l mode a a' <+> unify (S l) mode !(b $$ VVar emptyFC l [<]) !(b' $$ VVar emptyFC l [<]) |]
       (VVar fc k sp,   (VVar fc' k' sp')  ) =>
-        if k == k' then unifySpine l (k == k') sp sp'
+        if k == k' then unifySpine l mode (k == k') sp sp'
         else if k < k' then pure $ MkResult [(k,u')] else pure $ MkResult [(k',t')]
 
-      -- attempt at building constraints
+      -- We only want to do this for LHS pattern vars, otherwise, try expanding
-      (VVar fc k [<], u) => pure $ MkResult[(k, u)]
+      (VVar fc k [<], u) => case mode of
-      (t, VVar fc k [<]) => pure $ MkResult[(k, t)]
+        Pattern => pure $ MkResult[(k, u)]
+        Normal => case !(tryEval u) of
+          Just v => unify l mode t' v
+          Nothing => error ctx.fc "Failed to unify \{show t'} and \{show u'}"
 
-      (VLam _ _ t,  VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
+      (t, VVar fc k [<]) => case mode of
+        Pattern => pure $ MkResult[(k, t)]
+        Normal => case !(tryEval t) of
+          Just v => unify l mode v u'
+          Nothing => error ctx.fc "Failed to unify \{show t'} and \{show u'}"
+
+      (VLam _ _ t,  VLam _ _ t') => unify (l + 1) mode !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
       (t,         VLam fc' _ t') => do
         debug "ETA \{show t}"
-        unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
+        unify (l + 1) mode !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
       (VLam fc _ t,  t'       ) => do
         debug "ETA' \{show t'}"
-        unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<])
+        unify (l + 1) mode !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<])
 
       -- REVIEW - consider separate value for DCon/TCon
-      (VRef fc k def sp,   VRef fc' k' def' sp'  ) =>
+      (VRef fc k def sp,  VRef fc' k' def' sp') =>
         -- This is a problem for cmp (S x) (S y) =?= cmp x y, when the
         -- same is an equation in cmp.
 
@@ -274,12 +285,12 @@ parameters (ctx: Context)
         --   unifySpine l (k == k') sp sp'
         -- else
           do
-          Nothing <- tryEval k sp
+          Nothing <- tryEval t'
-            | Just v => unify l v u'
+            | Just v => unify l mode v u'
-          Nothing <- tryEval k' sp'
+          Nothing <- tryEval u'
-            | Just v => unify l t' v
+            | Just v => unify l mode t' v
           if k == k'
-            then  unifySpine l (k == k') sp sp'
+            then unifySpine l mode (k == k') sp sp'
             else error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}"
 
       (VU _, VU _) => pure neutral
@@ -288,13 +299,13 @@ parameters (ctx: Context)
       (t,         VRef fc' k' def sp') => do
         debug "expand \{show t} =?= %ref \{k'}"
         case lookup k' !(get) of
-          Just (MkEntry name ty (Fn tm)) => unify l t !(vappSpine !(eval [] CBN tm) sp')
+          Just (MkEntry name ty (Fn tm)) => unify l mode t !(vappSpine !(eval [] CBN tm) sp')
           _ => 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 sp} =?= \{show u}"
         case lookup k !(get) of
-          Just (MkEntry name ty (Fn tm)) => unify l !(vappSpine !(eval [] CBN tm) sp) u
+          Just (MkEntry name ty (Fn tm)) => unify l mode !(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}"
 
       -- REVIEW I'd like to quote this back, but we have l that aren't in the environment.
@@ -312,7 +323,7 @@ parameters (ctx: Context)
 
 unifyCatch : FC -> Context -> Val -> Val -> M ()
 unifyCatch fc ctx ty' ty = do
-    res <- catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do
+    res <- catchError (unify ctx ctx.lvl Normal ty' ty) $ \(E x str) => do
       let names = toList $ map fst ctx.types
       debug "fail \{show ty'} \{show ty}"
       a <- quote ctx.lvl ty'
@@ -509,7 +520,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
   -- We get unification constraints from matching the data constructors
   -- codomain with the scrutinee type
   debug "unify dcon cod with scrut\n  \{show ty'}\n  \{show scty}"
-  Just res <- catchError {e = Error} (Just <$> unify ctx' (length ctx'.env) ty' scty)
+  Just res <- catchError {e = Error} (Just <$> unify ctx' (length ctx'.env) Pattern ty' scty)
               (\(E _ msg) => do
                   debug "SKIP \{dcName} because unify error \{msg}"
                   pure Nothing)
@@ -540,7 +551,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
         pure $ Just $ CaseCons dcName (map getName vars) tm
 
     _ => do
-        Right res <- tryError {e = Error} (unify ctx' (length ctx'.env) ty' scty)
+        Right res <- tryError {e = Error} (unify ctx' (length ctx'.env) Pattern ty' scty)
           | Left (E _ msg) => do
             debug "SKIP \{dcName} because unify error \{msg}"
             pure Nothing

src/Lib/Eval.idr

@@ -83,7 +83,7 @@ eval env mode (Meta fc i) =
         (Solved _ k t) => pure $ t
 eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t)
 eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b)
-eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) (MkClosure env u)
+eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) !(eval (VVar fc (length env) [<] :: env) mode 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
@@ -116,7 +116,7 @@ quote l (VMeta fc i sp) =
         (Solved _ k t) => quote l !(vappSpine t sp)
 quote l (VLam fc x t) = pure $ Lam fc x !(quote (S l) !(t $$ VVar emptyFC l [<]))
 quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<]))
-quote l (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) !(u $$ VVar emptyFC l [<]))
+quote l (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) u)
 quote l (VU fc) = pure (U fc)
 quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp
 quote l (VCase fc sc alts) = pure $ Case fc !(quote l sc) alts
@@ -128,6 +128,10 @@ export
 nf : Env -> Tm -> M Tm
 nf env t = quote (length env) !(eval env CBN t)
 
+export
+nfv : Env -> Tm -> M Tm
+nfv env t = quote (length env) !(eval env CBV t)
+
 export
 prvalCtx : {auto ctx : Context} -> Val -> M String
 prvalCtx v = pure $ pprint (toList $ map fst ctx.types) !(quote ctx.lvl v)

src/Lib/ProcessDecl.idr

@@ -165,7 +165,7 @@ processDecl (Def fc nm clauses) = do
       let names = (toList $ map fst ctx.types)
       -- I want to know which ones are defines. I should skip the `=` bit if they match, I'll need indices in here too.
       env <- for (zip ctx.env (toList ctx.types)) $ \(v, n, ty) => pure "  \{n} : \{pprint names !(quote ctx.lvl ty)} = \{pprint names !(quote ctx.lvl v)}"
-      let msg = "\{unlines (toList $ reverse env)}  -----------\n  goal \{pprint names ty'}"
+      let msg = "\{unlines (toList $ reverse env)}  -----------\n  \{pprint names ty'}\n  \{showTm ty'}"
       info fc "User Hole\n\{msg}"
     (Unsolved (l,c) k ctx ty kind cons) => do
       tm <- quote ctx.lvl !(forceMeta ty)
@@ -177,23 +177,29 @@ processDecl (Def fc nm clauses) = do
   modify $ setDef nm ty (Fn tm')
 
 processDecl (DCheck fc tm ty) = do
+  putStrLn "----- DCheck"
   top <- get
-  putStrLn "check \{show tm} at \{show ty}"
+
-  ty' <- check (mkCtx top.metas fc) tm (VU fc)
+  putStrLn "INFO at \{show fc}: check \{show tm} at \{show ty}"
-  putStrLn "got type \{pprint [] ty'}"
+  ty' <- check (mkCtx top.metas fc) ty (VU fc)
+  putStrLn "  got type \{pprint [] ty'}"
   vty <- eval [] CBN ty'
-  res <- check (mkCtx top.metas fc) ty vty
+  res <- check (mkCtx top.metas fc) tm vty
-  putStrLn "got \{pprint [] res}"
+  putStrLn "  got \{pprint [] res}"
   norm <- nf [] res
-  putStrLn "norm \{pprint [] norm}"
+  putStrLn "  NF \{pprint [] norm}"
-  putStrLn "NF "
+  norm <- nfv [] res
+  putStrLn "  NFV \{pprint [] norm}"
 
 processDecl (Data fc nm ty cons) = do
+  putStrLn "-----"
+  putStrLn "process data \{nm}"
   top <- get
   tyty <- check (mkCtx top.metas fc) ty (VU fc)
   modify $ setDef nm tyty Axiom
   cnames <- for cons $ \x => case x of
       (TypeSig fc names tm) => do
+          debug "check dcon \{show names} \{show tm}"
           dty <- check (mkCtx top.metas fc) tm (VU fc)
           debug "dty \{show names} is \{pprint [] dty}"
 

src/Lib/Tokenizer.idr

@@ -23,7 +23,7 @@ identMore : Lexer
 identMore = alphaNum <|> exact "." <|> exact "'" <|> exact "_"
 
 singleton : Lexer
-singleton = oneOf "()\\{}[],"
+singleton = oneOf "()\\{}[],?"
 
 quo : Recognise True
 quo = is '"'

src/Lib/Types.idr

@@ -142,6 +142,10 @@ Show Tm where
   show (Case _ sc alts) = "(Case \{show sc} \{show alts})"
   show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})"
 
+public export
+showTm : Tm -> String
+showTm = show
+
 -- I can't really show val because it's HOAS...
 
 -- TODO derive
@@ -228,7 +232,7 @@ data Val : Type where
   VMeta : FC -> (ix : Nat) -> (sp : SnocList Val) -> Val
   VLam : FC -> Name -> Closure -> Val
   VPi : FC -> Name -> Icit -> (a : Lazy Val) -> (b : Closure) -> Val
-  VLet : FC -> Name -> Val -> (b : Closure) -> Val
+  VLet : FC -> Name -> Val -> Val -> Val
   VU : FC -> Val
   VLit : FC -> Literal -> Val
 
@@ -242,6 +246,7 @@ getValFC (VLam fc _ _) = fc
 getValFC (VPi fc _ _ a b) = fc
 getValFC (VU fc) = fc
 getValFC (VLit fc _) = fc
+getValFC (VLet fc _ _ _) = fc
 
 
 public export
@@ -260,6 +265,7 @@ Show Val where
   show (VCase fc sc alts) = "(%case \{show sc} ...)"
   show (VU _) = "U"
   show (VLit _ lit) = show lit
+  show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}"
 
 -- Not used - I was going to change context to have a List Binder
 -- instead of env, types, bds

tests/black/CaseEval.newt

@@ -15,4 +15,7 @@ two : Eq (plus (S Z) (S Z)) (S (S Z))
 two = Refl
 
 three : Eq (plus (S Z) (S (S Z))) (plus (S (S Z)) (S Z))
-three = Refl {Nat} {S (S (S Z))}
+three = Refl
+
+addZero : {n : Nat} -> Eq (plus Z n) n
+addZero {n} = Refl