1 + 1 = 2

.gitignore

@@ -2,3 +2,6 @@ build/
 *.*~ATTIC
 \#*
 *~
+*.log
+*.agda
+*.agdai

TODO.md

@@ -6,7 +6,7 @@ I may be done with `U` - I keep typing `Type`.
 - [ ] consider making meta application implicit in term, so its more readable when printed
   - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people
     leave that implicit for efficiency. I think it would also make printing more readable.
-- [ ] eval for case (see order.newt)
+- [x] eval for case (see order.newt)
 - [ ] dynamic pattern unification (add test case first)
 - [x] switch from commit/mustWork to checking progress
 - [x] type constructors are no longer generated?  And seem to have 0 arity.

newt-vscode/LICENSE

@@ -0,0 +1,24 @@
+This is free and unencumbered software released into the public domain.
+
+Anyone is free to copy, modify, publish, use, compile, sell, or
+distribute this software, either in source code form or as a compiled
+binary, for any purpose, commercial or non-commercial, and by any
+means.
+
+In jurisdictions that recognize copyright laws, the author or authors
+of this software dedicate any and all copyright interest in the
+software to the public domain. We make this dedication for the benefit
+of the public at large and to the detriment of our heirs and
+successors. We intend this dedication to be an overt act of
+relinquishment in perpetuity of all present and future rights to this
+software under copyright law.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
+OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
+ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+OTHER DEALINGS IN THE SOFTWARE.
+
+For more information, please refer to <https://unlicense.org>

newt/order.newt

@@ -14,6 +14,7 @@ data Pair : U -> U -> U where
 infix 1 _,_
 
 foo : Pair Nat Nat
+-- vscode plugin issue: Without the space the info is rendered on Z...
 foo = (Z , S Z)
 
 -- So I was going to force a (a + b, a) =?= (3,0) unification problem
@@ -24,6 +25,12 @@ data Eq : {A : U} -> A -> A -> U where
 -- but hold up here.  This doesn't solve either.
 -- Oh, because I can't reduce case.
 -- And the FC is useless.
+-- these go into caseeval.newt test
 two : Eq (plus Z (S (S Z))) (S (S Z))
-two = Refl {Nat} {S (S Z)}
+two = Refl
 
+two' : Eq (plus (S Z) (S Z)) (S (S Z))
+two' = Refl {Nat} {S (S Z)}
+
+three : Eq (plus (S Z) (S (S Z))) (plus (S (S Z)) (S Z))
+three = Refl {Nat} {S (S (S Z))}

src/Lib/Elab.idr

@@ -192,11 +192,22 @@ parameters (ctx: Context)
       (VVar fc k sp, u) => pure $ MkResult[(k, u)]
       (t, VVar fc k sp) => pure $ MkResult[(k, t)]
 
+      -- 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 error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}"
+        else case lookup k !(get) of
+          Just (MkEntry name ty (Fn tm)) => do
+            vtm <- eval [] CBN tm
+            v <- vappSpine vtm sp
+            unify l v u'
+          _ => case lookup k' !(get) of
+            Just (MkEntry name ty (Fn tm)) => do
+              vtm <- eval [] CBN tm
+              v <- vappSpine vtm sp'
+              unify l t' v
+            _ => error fc "vref mismatch \{show k} \{show k'} -- \{show sp} \{show sp'}"
 
       (VU _, VU _) => pure neutral
       -- Lennart.newt cursed type references itself

src/Lib/Eval.idr

@@ -9,6 +9,7 @@ import Control.Monad.Error.Interface
 import Data.IORef
 import Data.Fin
 import Data.List
+import Data.SnocList
 import Data.Vect
 import Data.SortedMap
 
@@ -43,23 +44,19 @@ vappSpine : Val -> SnocList Val -> M Val
 vappSpine t [<] = pure t
 vappSpine t (xs :< x) = vapp !(vappSpine t xs) x
 
--- So we need:
--- - a Neutral case statement
--- - split out data / type constructors from VRef application
--- - should we sort out what the case tree really looks like first?
-
--- Technically I don't need this now, as a neutral would be fine.
-
-evalAlt : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val)
--- FIXME spine length? Should this be VRef or do we specialize?
-evalAlt env mode (VRef _ nm y sp) ((CaseCons name args t) :: xs) =
+evalCase : Env -> Mode -> Val -> List CaseAlt -> M (Maybe Val)
+evalCase env mode sc@(VRef _ nm y sp) (cc@(CaseCons name nms t) :: xs) =
   if nm == name
-    -- Here we bind the args and push on. Do we have enough? Too many?
-    then ?evalAlt_success
-    -- here we need to know if we've got a mismatched constructor or some function app
-    else ?evalAlt_what
-evalAlt env mode sc (CaseDefault u :: xs) = pure $ Just !(eval (sc :: env) mode u)
-evalAlt env mode sc _ = pure Nothing -- stuck
+    then go env sp nms
+    else evalCase env mode sc xs
+  where
+    go : Env -> SnocList Val -> List String -> M (Maybe Val)
+    go env (args :< arg) (nm :: nms) = go (arg :: env) args nms
+    go env args [] = Just <$> vappSpine !(eval env mode t) args
+    go env [<] rest = pure Nothing
+
+evalCase env mode sc (CaseDefault u :: xs) = pure $ Just !(eval (sc :: env) mode u)
+evalCase env mode sc _ = pure Nothing
 
 bind : Val -> Env -> Env
 bind v env = v :: env
@@ -71,9 +68,6 @@ bind v env = v :: env
 --   - Applications headed by top-level variables are lazy.
 --   - Any other function application is call-by-value during evaluation.
 
--- Do we want a def in here instead?  We'll need DCon/TCon eventually
--- I need to be aggressive about reduction, I guess. I'll figure it out
--- later, maybe need lazy glued values.
 -- TODO - probably want to figure out gluing and handle constructors
 eval env mode (Ref _ x (Fn tm)) = eval env mode tm
 eval env mode (Ref fc x def) = pure $ VRef fc x def [<]
@@ -94,9 +88,11 @@ 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
 
--- We need a neutral and some code to run the case tree
-
-eval env mode tm@(Case fc sc alts) = pure $ VCase fc !(eval env mode sc) alts
+eval env mode tm@(Case fc sc alts) =
+  case !(evalCase env mode !(eval env mode sc) alts) of
+    Just v => pure v
+    Nothing => pure $ fromMaybe (VCase fc !(eval env mode sc) alts)
+                                !(evalCase env mode !(eval env mode sc) alts)
 
 export
 quote : (lvl : Nat) -> Val -> M Tm

tests/black/caseeval.newt

@@ -0,0 +1,18 @@
+module CaseEval
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+plus Z y = y
+plus (S x) y = S (plus x y)
+
+data Eq : {A : U} -> A -> A -> U where
+  Refl : {A : U} -> {x : A} -> Eq x x
+
+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))}