fix env (should have used an index...)

newt/DepEq.newt

@@ -0,0 +1,73 @@
+module DepEq
+
+-- https://mathstodon.xyz/@MartinEscardo/114751459092567654
+-- see also https://martinescardo.github.io/dependent-equality-lecture/DependentEquality.html
+
+infixr 5 _≡_
+infixl 6 _+_
+infixl 6 _++_
+infixr 7 _::_
+infixr 5 _≡⟨_⟩_
+
+data _≡_ : ∀ a. a → a → U where
+  Refl : ∀ a. {x : a} → x ≡ x
+
+cong : ∀ X Y. (f : X → Y) → {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
+cong f Refl = Refl
+
+data ℕ : U where
+  S : ℕ → ℕ
+  Z : ℕ
+
+_+_ : ℕ → ℕ → ℕ
+Z + m = m
+S k + m = S (k + m)
+
++-assoc : (l m n : ℕ ) → l + (m + n) ≡ (l + m) + n
++-assoc Z m n = Refl
++-assoc (S k) m n = cong S (+-assoc k m n)
+
+
+
+_≡⟨_⟩_ : {0 A : U} → {0 B : A → U } →  {0 x₀ x₁ : A} → B x₀ → x₀ ≡ x₁ → B x₁ → U
+b₀ ≡⟨ Refl ⟩ b₁ = b₀ ≡ b₁
+
+congd : {0 A : U} → {0 B : A → U} → (f : (a : A) → B a) → {0 a₀ a₁ : A} →
+        (p : a₀ ≡ a₁) →
+        _≡⟨_⟩_ {_} {B} (f a₀) p (f a₁)
+congd f Refl = Refl
+
+data Vect : U → ℕ → U where
+  Nil : ∀ a. Vect a Z
+  _::_ : ∀ a n . a → Vect a n → Vect a (S n)
+
+_++_ : ∀ a n m. Vect a n → Vect a m → Vect a (n + m)
+Nil ++ ys = ys
+(x :: xs) ++ ys = x :: (xs ++ ys)
+
+-- REVIEW - make sure we're freezing metas at the end of a typesig / def
+cong-cons : ∀ a n m.  (x : a) → {xs : Vect a n} → {ys : Vect a m} → (p : n ≡ m) →
+            _≡⟨_⟩_ {_} {Vect a} xs p ys → _≡⟨_⟩_ {_} {Vect a} (x :: xs) (cong S p) (x :: ys)
+-- This is failing because the type doesn't reduce.  We need to process arg2 first, after determining that
+-- TODO the type of the second argument is not useful to split until the first one is split
+-- need to check the type when we decide to split on an argument
+-- cong-cons _ Refl Refl = ?
+
+-- and this one was having some trouble on the RHS, which turned out to `cong`
+-- being undefined.
+cong-cons _ Refl x = case x of Refl => Refl
+
+-- Idris' complaint about B is more readable:
+
+-- Error: While processing type of appAssoc. Can't solve constraint
+-- between: Vec ?a ((?l + ?n) + ?m) and ?b ((?l + ?n) + ?m).
+
+++-assoc : ∀ a l n m. (xs : Vect a l) → (ys : Vect a n) → (zs : Vect a m) →
+           -- TODO newt + idris have trouble sorting out B
+           _≡⟨_⟩_ {_} {Vect a} (xs ++ (ys ++ zs)) (+-assoc l n m) ((xs ++ ys) ++ zs)
+++-assoc Nil ys zs = Refl
+-- TODO need rhs hole to look more like this in newt:
+-- hole : DepEq (x :: (xs ++ (ys ++ zs))) (cong S (plusAssoc k n m)) (x :: ((xs ++ ys) ++ zs))
+++-assoc {a} {S k} {n} {m} (x :: xs) ys zs = cong-cons x (+-assoc k n m) (++-assoc xs ys zs)
+
+

src/Lib/Elab.newt

@@ -54,7 +54,7 @@ dumpCtx : Context -> M String
 dumpCtx ctx = do
   let names = (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 ctx.types) $ \case
+  env <- for (reverse $ zip ctx.env ctx.types) $ \case
     (v, n, ty) => do
       sty <- vprint ctx ty
       sv <- vprint ctx v
@@ -697,7 +697,7 @@ getConstructors ctx scfc (VRef fc nm _) = do
       top <- getTop
       case lookup nm top of
         (Just (MkEntry _ name type (TCon _ names) _)) => pure names
-        _ => error scfc "Not a type constructor \{show nm}"
+        _ => error scfc "Not a type constructor: \{show nm}"
     lookupDCon : QName -> M (QName × Int × Tm)
     lookupDCon nm = do
       top <- getTop

src/Lib/Eval.newt

@@ -74,7 +74,7 @@ tryEval env (VRef fc k sp) = do
         catchError (
             do
             debug $ \ _ =>  "app \{show name} to \{show sp}"
-            vtm <- eval Nil CBN tm
+            vtm <- eval env CBN tm
             debug $ \ _ =>  "tm is \{render 90 $ pprint Nil tm}"
             val <- vappSpine vtm sp
             case val of
@@ -86,7 +86,9 @@ tryEval env (VRef fc k sp) = do
               VLetRec _ _ _ _ _ => pure Nothing
               v => pure $ Just v)
             (\ _ => pure Nothing)
-      _ => pure Nothing
+      _ => do
+        debug $ \ _ => "tryEval blocked on undefined \{show k}"
+        pure Nothing
 tryEval _ _ = pure Nothing
 
 

src/Lib/Types.newt

@@ -178,6 +178,7 @@ pprint' p names (Bnd _ k) = case getAt (cast k) names of
 pprint' p names (Ref _ str) = text (show str)
 pprint' p names (Meta _ k) = text "?m:\{show k}"
 pprint' p names (Lam _ nm icit quant t) = parens 0 p $ nest 2 $ text "\\ \{show quant}\{nm} =>" <+/> pprint' 0 (nm :: names) t
+-- FIXME - we've lost icity, so we implict app as normal
 pprint' p names (App _ t u) = parens 0 p $ pprint' 0 names t <+> pprint' 1 names u
 pprint' p names (UU _) = text "U"
 pprint' p names (Pi _ nm Auto rig t u) = parens 0 p $

src/Main.newt

@@ -162,7 +162,7 @@ processModule importFC base stk qn@(QN ns nm) = do
     importHints (listValues mod.modDefs)
 
   log 1 $ \ _ => "process Decls"
-  traverse (tryProcessDecl ns) (collectDecl decls)
+  traverse (tryProcessDecl src ns) (collectDecl decls)
 
   -- update modules with result, leave the rest of context in case this is top file
   top <- getTop
@@ -178,14 +178,16 @@ processModule importFC base stk qn@(QN ns nm) = do
 
   (Nil) <- liftIO {M} $ readIORef top.errors
     | errors => do
-        traverse (putStrLn ∘ showError src) errors
+        -- we're now showing errors when they occur, so they're next to debug messages
+        -- traverse (putStrLn ∘ showError src) errors
         exitFailure "Compile failed"
   logMetas $ reverse $ listValues top.metaCtx.metas
   pure src
   where
-    tryProcessDecl : List String -> Decl -> M Unit
-    tryProcessDecl ns decl = do
+    tryProcessDecl : String -> List String → Decl -> M Unit
+    tryProcessDecl src ns decl = do
       (Left err) <- tryError $ processDecl ns decl | _ => pure MkUnit
+      putStrLn $ showError src err
       addError err
 
 -- unwind the module part of the path name