From 41a7563ad56b916f8bd4a6e505e51bbaf83b0e94 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 17 Oct 2024 21:54:11 -0700 Subject: [PATCH] Variant on Tree, try not to expand too much --- src/Lib/Elab.idr | 4 -- src/Lib/Prettier.idr | 2 +- src/Lib/ProcessDecl.idr | 7 +- src/Lib/Types.idr | 2 +- tests/{black => aside}/Test1.newt | 2 + tests/aside/Tree2.newt | 110 ++++++++++++++++++++++++++++++ 6 files changed, 118 insertions(+), 9 deletions(-) rename tests/{black => aside}/Test1.newt (68%) create mode 100644 tests/aside/Tree2.newt diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 0754cca..ec38e5b 100644 --- a/src/Lib/Elab.idr +++ b/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 diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr index 8900e14..c7f189e 100644 --- a/src/Lib/Prettier.idr +++ b/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)) diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 7630b59..987f0cc 100644 --- a/src/Lib/ProcessDecl.idr +++ b/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 diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 1de488f..6efb300 100644 --- a/src/Lib/Types.idr +++ b/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 diff --git a/tests/black/Test1.newt b/tests/aside/Test1.newt similarity index 68% rename from tests/black/Test1.newt rename to tests/aside/Test1.newt index d17e526..1afa501 100644 --- a/tests/black/Test1.newt +++ b/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 diff --git a/tests/aside/Tree2.newt b/tests/aside/Tree2.newt new file mode 100644 index 0000000..195af4a --- /dev/null +++ b/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')