From e6502abeedc6d09185594ccc79ba989f1e6d43d5 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 30 Oct 2024 08:21:33 -0700 Subject: [PATCH] update docs and a test --- README.md | 5 +- tests/aside/Tree2.newt | 110 ----------------------------------------- tests/black/Tree.newt | 32 +++++------- 3 files changed, 15 insertions(+), 132 deletions(-) delete mode 100644 tests/aside/Tree2.newt diff --git a/README.md b/README.md index 92b33fc..652e7f6 100644 --- a/README.md +++ b/README.md @@ -19,7 +19,7 @@ The repository is tagging `.newt` files as Agda to convince github to highlight There is a `Makefile` that builds both chez and javascript versions. They end up in `build/exec` as usual. I've also added a `pack.toml`, so `pack build` also works. -There is a vscode extension in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `build/exec/newt` to exist in the workspace. +There is a vscode extension in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `build/exec/newt` to exist in the workspace. And `make test` will run a few black box tests. Currently it simply checks return codes, since the output is in flux. ## Overview @@ -52,8 +52,7 @@ Following kovacs, I'm putting `VVar` into context env when I go under binders. T ## Autos -Newt has primitive auto implicits. As a first pass, higher order ones, like monad, will not - +Newt has primitive auto implicits. They are denoted by double braces `{{}}` as in Agda. Newt will search for a function that returns a type in the same family, only has implicit and auto-implicit arguments, and unifies (satisfying any relevant constraints). ## Issues diff --git a/tests/aside/Tree2.newt b/tests/aside/Tree2.newt deleted file mode 100644 index 195af4a..0000000 --- a/tests/aside/Tree2.newt +++ /dev/null @@ -1,110 +0,0 @@ --- 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') diff --git a/tests/black/Tree.newt b/tests/black/Tree.newt index 9346e37..2594a8e 100644 --- a/tests/black/Tree.newt +++ b/tests/black/Tree.newt @@ -1,6 +1,8 @@ module Tree --- https://youtu.be/v2yXrOkzt5w?t=3013 +-- adapted from Conor McBride's 2-3 tree example +-- youtube video: https://youtu.be/v2yXrOkzt5w?t=3013 + data Nat : U where Z : Nat @@ -60,43 +62,35 @@ data T23 : Bnd -> Bnd -> Nat -> U where infixl 5 _*_ infixr 1 _,_ -infixr 1 _**_ data Sg : (A : U) -> (A -> U) -> U where - _**_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B + _,_ : {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 +_*_ : U -> U -> U +A * B = Sg 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 -insert (intv x lx xu) (leaf lu) = inl (x ** (leaf {_} {_} {x} lx , leaf {_} {_} {x} xu)) +-- 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) + 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) + 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 - inl (v ** (tlv , tvy)) => inl (y ** (node2 v tlv tvy, node2 z tyz tzu)) + 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)) + 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)) + inl (w , (tzw , twu)) => inl (z , (node2 y tly tyz , node2 w tzw twu)) inr tzu' => inr (node3 y z tly tyz tzu')