Variant on Tree, try not to expand too much

src/Lib/Elab.idr

@@ -69,10 +69,6 @@ tryEval k sp =
 
 -- Lennart needed more forcing for recursive nat,
 forceType : Val -> M Val
-forceType tm@(VRef fc nm def sp) =
-  case !(tryEval nm sp) of
-    Just tm => pure tm
-    _ => pure tm
 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

src/Lib/Prettier.idr

@@ -57,7 +57,7 @@ be acc w k ((i, Line) :: xs) = (be (acc :< LINE i) w i xs)
 be acc w k ((i, (Text s)) :: xs) = (be (acc :< TEXT s) w (k + length s) xs)
 be acc w k ((i, (Nest j x)) :: xs) = be acc w k ((i+j,x)::xs)
 be acc w k ((i, (Seq x y)) :: xs) = be acc w k ((i,x) :: (i,y) :: xs)
--- We're doing extra work here - the first branch should cut if it exhausts w before the first LINE
+-- We're doing extra work here - the first branch should cut if it exhausts w - k before the first LINE
 be acc w k ((i, (Alt x y)) :: xs) = acc <>> better w k (be [<] w k ((i,x)::xs))
                                                        (be [<] w k ((i,y)::xs))
 

src/Lib/ProcessDecl.idr

@@ -40,9 +40,10 @@ processDecl (TypeSig fc nm tm) = do
   putStrLn "TypeSig \{nm} \{show tm}"
   ty <- check (mkCtx top.metas fc) tm (VU fc)
   putStrLn "got \{pprint [] ty}"
-  ty' <- nf [] ty
-  putStrLn "nf \{pprint [] ty'}"
-  modify $ setDef nm ty' Axiom
+  -- I was doing this previously, but I don't want to over-expand VRefs
+  -- ty' <- nf [] ty
+  -- putStrLn "nf \{pprint [] ty'}"
+  modify $ setDef nm ty Axiom
 
 processDecl (PType fc nm ty) = do
   ctx <- get

src/Lib/Types.idr

@@ -462,7 +462,7 @@ debug x = do
 
 export
 info : FC -> String -> M ()
-info fc msg = putStrLn "INFO at \{show fc}: \{show msg}"
+info fc msg = putStrLn "INFO at \{show fc}: \{msg}"
 
 ||| Version of debug that makes monadic computation lazy
 export

tests/aside/Test1.newt

@@ -1,9 +1,11 @@
 module Test1
 
+-- This is not total
 nat : U
 nat = {C : U} -> C -> (nat -> C) -> C
 
 -- TESTCASE This was broken when I wasn't expanding Ref ty in check
 -- Also broken when I tried to put Def in VRef
+-- Broken if I don't `nf` the type of a function before putting in TopContext
 succ : nat -> nat
 succ = \n => \ z s => s n

tests/aside/Tree2.newt

@@ -0,0 +1,110 @@
+-- This needs to solve at a pi-type and the constraint has it applied..
+module Tree2
+
+-- https://youtu.be/v2yXrOkzt5w?t=3013
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Unit : U where
+  MkUnit : Unit
+
+data Void : U where
+
+infixl 4 _+_
+
+data _+_ : U -> U -> U where
+  inl : {A B : U} -> A -> A + B
+  inr : {A B : U} -> B -> A + B
+
+infix 4 _<=_
+
+_<=_ : Nat -> Nat -> U
+Z <= y = Unit
+S x <= Z = Void
+S x <= S y = x <= y
+
+cmp : (x y : Nat) -> (x <= y) + (y <= x)
+cmp Z y = inl MkUnit
+cmp (S z) Z = inr MkUnit
+cmp (S x) (S y) = cmp x y
+
+-- 53:21
+
+data Bnd : U where
+  Bot : Bnd
+  N : Nat -> Bnd
+  Top : Bnd
+
+infix 4 _<<=_
+
+_<<=_ : Bnd -> Bnd -> U
+Bot <<= _ = Unit
+N x <<= N y = x <= y
+_ <<= Top = Unit
+_ <<= _ = Void
+
+data Intv : Bnd -> Bnd -> U where
+  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
+  node2 : {l u : Bnd} {h : Nat} (x : _)
+    (tlx : T23 l (N x) h) (txu : T23 (N x) u h) ->
+    T23 l u (S h)
+  node3 : {l u : Bnd} {h : Nat} (x y : _)
+    (tlx : T23 l (N x) h) (txy : T23 (N x) (N y) h) (tyu : T23 (N y) u h) ->
+    T23 l u (S h)
+
+-- 56:
+
+infixl 5 _*_
+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.
+
+-- It's meta applied to too many args. I think the root issue is that
+-- _*_ gets expanded early and then \ _  => B a =?= ?meta a isn't solvable
+-- but if it was A * B =?= A * ?meta we could say A =?= A, B =?= ?meta without expanding
+
+_*_ : U -> U -> U
+A * B = Sg A (\ _ => B)
+
+-- data _*_ : (A B : U) -> U where
+--    _,_ : {A B : U} -> A -> B -> A * B
+
+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
+-- Agda is yellow here, needs h = x on each leaf
+-- The second arg to the second _,_ is unsolved and pi-typed
+insert (intv x lx xu) (leaf lu) = inl (x , (leaf {_} {_} {x} lx , leaf {_} {_} {x} 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 (intv {_} {N y} x lx xy) tly of
+    inl (z , (tlz , tzy)) => inr (node3 z y tlz tzy tyu)
+    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 tly' => inr (node3 y z tly' tyz tzu)
+  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')