most of Tree.newt working

newt/Tree.newt

@@ -45,7 +45,7 @@ _ <<= Top = Unit
 _ <<= _ = Void
 
 data Intv : Bnd -> Bnd -> U where
-  MkI : {l u : Bnd} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
+  intv : {l u : Bnd} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
 
 data T23 : Bnd -> Bnd -> Nat -> U where
   leaf : {l u : Bnd} {h : Nat} (lu : l <<= u) -> T23 l u Z
@@ -64,6 +64,14 @@ infixr 1 _**_
 data Sg : (A : U) -> (A -> U) -> U where
   _**_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
 
+
+-- Accidentally defined this as a separate data because I was
+-- guessing the def behind _*_. I get an unsolved meta below if
+-- I define in terms of Sg.
+
+-- _*_ : U -> U -> U
+-- A * B = Sg A (\ _ => B)
+
 data _*_ : (A B : U) -> U where
    _,_ : {A B : U} -> A -> B -> A * B
 
@@ -71,13 +79,28 @@ TooBig : Bnd -> Bnd -> Nat -> U
 TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
 
 insert : {h : Nat} {l u : Bnd} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
-insert (MkI x lx xu) (leaf lu) = ?
+-- Agda is yellow here, needs h = x on each leaf
-insert (MkI x lx xu) (node2 x1 t t1) = ?
+-- In Newt, we're getting an skolem escape error
-insert (MkI x lx xu) (node3 y z tly tyz tzu) = case cmp x y of
+insert (intv x lx xu) (leaf lu) = inl (x ** (leaf lx , leaf xu))
+insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of
   -- u := N y is not solved at this time
-  inl xy => case insert (MkI {_} {N y} x lx xy) tly of
+  inl xy => case insert (intv {_} {N y} x lx xy) tly of
-    -- NOW down to a non-linear issue now.
+    inl (z ** (tlz, tzy)) => inr (node3 z y tlz tzy tyu)
-    -- Possibly due to the meta being applied to an extra argument
+    inr tly' => inr (node2 y tly' tyu)
+  inr yx => case insert (intv {N y} x yx xu) tyu of
+    inl (z ** (tyz, tzu)) => inr (node3 y z tly tyz tzu)
+    inr tyu' => inr (node2 y tly tyu')
+insert (intv x lx xu) (node3 y z tly tyz tzu) = case cmp x y of
+  inl xy => case insert (intv {_} {N y} x lx xy) tly of
+    -- TODO Here a meta is applied to an extra argument, if we ignore that
+    -- constraint we get a better one later - _but_ we probably need to check
+    -- the constraint later.
     inl (v ** (tlv , tvy)) => inl (y ** (node2 v tlv tvy, node2 z tyz tzu))
-    inr x1 => ?
+    inr tly' => inr (node3 y z tly' tyz tzu)
-  inr x1 => ?
+  inr yx => case cmp x z of
+    inl xz => case insert (intv {N y} {N z} x yx xz) tyz of
+      inl (w ** (tyw , twz)) => inl (w ** (node2 y tly tyw, node2 z twz tzu))
+      inr tyz' => inr (node3 y z tly tyz' tzu)
+    inr zx => case insert (intv {N z} x zx xu) tzu of
+      inl (w ** (tzw, twu)) => inl (z ** (node2 y tly tyz, node2 w tzw twu))
+      inr tzu' => inr (node3 y z tly tyz tzu')

src/Lib/Elab.idr

@@ -136,15 +136,24 @@ parameters (ctx: Context)
   solve : Nat -> 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 <- lookupMeta m
+    meta@(Unsolved metaFC ix ctx ty) <- lookupMeta m
-    debug "meta \{show meta}"
+      | _ => error (getFC t) "Meta \{show m} already solved!"
-    ren <- invert l sp
+    let size = length $ filter (\x => x == Bound) $ toList ctx.bds
-    tm <- rename m ren l t
+    debug "\{show m} size is \{show size}"
-    let tm = lams (length sp) tm
+    if (length sp /= size) then do
-    top <- get
+        -- need INFO that works like debug.
-    soln <- eval [] CBN tm
+        -- FIXME we probably need to hold onto the constraint and recheck when we solve the meta?
-    solveMeta top m soln
+        info (getFC t) "meta \{show m} applied to \{show $ length sp} args insted of \{show size}"
-    pure ()
+        -- error (getFC t) "meta \{show m} applied to \{show $ length sp} args insted of \{show size}"
+      else do
+        debug "meta \{show meta}"
+        ren <- invert l sp
+        tm <- rename m ren l t
+        let tm = lams (length sp) tm
+        top <- get
+        soln <- eval [] CBN tm
+        solveMeta top m soln
+        pure ()
 
   trySolve : Nat -> Nat -> SnocList Val -> Val -> M ()
   trySolve l m sp t = do
@@ -210,8 +219,12 @@ parameters (ctx: Context)
       (t, VVar fc k [<]) => pure $ MkResult[(k, t)]
 
       (VLam _ _ t,  VLam _ _ t') => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
-      (t,         VLam fc' _ t') => unify (l + 1) !(t `vapp` VVar emptyFC l [<]) !(t' $$ VVar emptyFC l [<])
+      (t,         VLam fc' _ t') => do
-      (VLam fc _ t,  t'       ) => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<])
+        debug "ETA \{show t}"
+        unify (l + 1) !(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 [<])
 
       -- REVIEW - consider separate value for DCon/TCon
       (VRef fc k def sp,   VRef fc' k' def' sp'  ) =>

src/Lib/Types.idr

@@ -33,6 +33,13 @@ Show Icit where
 public export
 data BD = Bound | Defined
 
+public export
+Eq BD where
+  Bound == Bound = True
+  Defined == Defined = True
+  _ == _ = False
+
+
 Show BD where
   show Bound = "bnd"
   show Defined = "def"
@@ -219,6 +226,9 @@ getValFC (VU fc) = fc
 getValFC (VLit fc _) = fc
 
 
+public export
+HasFC Val where getFC = getValFC
+
 Show Closure
 
 covering export
@@ -450,6 +460,10 @@ debug x = do
   top <- get
   when top.verbose $ putStrLn x
 
+export
+info : FC -> String -> M ()
+info fc msg = putStrLn "INFO at \{show fc}: \{show msg}"
+
 ||| Version of debug that makes monadic computation lazy
 export
 debugM : M String -> M ()