dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

Improvements to grammar

Browse Source
This commit is contained in:
Steve Dunham
2024-11-09 21:39:45 -08:00
parent bb749a917a
commit 6abd97ee85
9 changed files with 80 additions and 80 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
TODO.md
View File

@@ -2,10 +2,10 @@
## TODO
- [x] forall / ∀ sugar
- [ ] Bad module name error has FC 0,0 instead of the module or name
- [x] Bad module name error has FC 0,0 instead of the module or name
- [x] I've made `{x}` be `{x : _}` instead of `{_ : x}`. Change this.
- [ ] Remove context lambdas when printing solutions (show names from context)
- build list of names and strip λ, then call pprint with names
- maybe build list of names and strip λ, then call pprint with names
- [ ] Check for shadowing when declaring dcon
- [ ] Require infix decl before declaring names (helps find bugs)
- [ ] sugar for typeclasses

6
playground/samples/Lists.newt
View File

@@ -44,7 +44,7 @@ data _≡_ : ∀ A . A -> A -> U where
Refl : ∀ A . {a : A} -> a ≡ a
-- If a ≡ b then b ≡ a
sym : {A : U} {a b : A} -> a ≡ b -> b ≡ a
sym : {A} {a b : A} -> a ≡ b -> b ≡ a
sym Refl = Refl
-- if a ≡ b and b ≡ c then a ≡ c
@@ -52,11 +52,11 @@ trans : {A : U} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
trans Refl x = x
-- This lets us replace a with b inside an expression if a ≡ b
replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
replace : ∀ A a b. (P : A -> U) -> a ≡ b -> P a -> P b
replace p Refl x = x
-- if a ≡ b then f a ≡ f b
cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
cong : ∀ A B a b. (f : A -> B) -> a ≡ b -> f a ≡ f b
-- if concatenate two lists, the length is the sum of the lengths
-- of the original lists

8
playground/samples/Tour.newt
View File

@@ -20,7 +20,7 @@
-/
-- One-line comments begin with two hypens
-- One-line comments begin with two hyphens
-- every file begins with a `module` declaration
-- it must match the filename
@@ -150,16 +150,16 @@ data Monad : (U -> U) -> U where
({a b : U} -> m a -> (a -> m b) -> m b) ->
Monad m
pure : ∀ m . {{_ : Monad m}} -> {a : U} -> a -> m a
pure : ∀ m. {{Monad m}} -> {a : U} -> a -> m a
pure {{MkMonad p _}} a = p a
-- we can declare multiple infix operators at once
infixl 1 _>>=_ _>>_
_>>=_ : ∀ m a b. {{_ : Monad m}} -> m a -> (a -> m b) -> m b
_>>=_ : ∀ m a b. {{Monad m}} -> m a -> (a -> m b) -> m b
_>>=_ {{MkMonad _ b}} ma amb = b ma amb
_>>_ : ∀ m a b. {{_ : Monad m}} -> m a -> m b -> m b
_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
ma >> mb = ma >>= (λ _ => mb)
-- That's our Monad typeclass, now let's make a List monad

17
playground/samples/Tree.newt
View File

@@ -16,8 +16,8 @@ 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
inl : {A B} -> A -> A + B
inr : {A B} -> B -> A + B
infix 4 _<=_
@@ -47,14 +47,14 @@ _ <<= 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
intv : {l u} (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 : _)
leaf : {l u} (lu : l <<= u) -> T23 l u Z
node2 : {l u h} (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 : _)
node3 : {l u h} (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)
@@ -71,9 +71,8 @@ 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))
insert : {l u h} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
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 (intv {_} {N y} x lx xy) tly of

42
playground/samples/TypeClass.newt
View File

@@ -3,35 +3,35 @@ module TypeClass
data Monad : (U -> U) -> U where
MkMonad : { M : U -> U } ->
(bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
(pure : {A : U} -> A -> M A) ->
(pure : ∀ A. A -> M A) ->
Monad M
infixl 1 _>>=_ _>>_
_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
_>>=_ {a} {b} {m} {{MkMonad bind' _}} ma amb = bind' {a} {b} ma amb
_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
_>>=_ {{MkMonad bind' _}} ma amb = bind' ma amb
_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
ma >> mb = mb
pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
pure {_} {_} {{MkMonad _ pure'}} a = pure' a
pure : ∀ m a. {{Monad m}} -> a -> m a
pure {{MkMonad _ pure'}} a = pure' a
data Either : U -> U -> U where
Left : {A B : U} -> A -> Either A B
Right : {A B : U} -> B -> Either A B
Left : ∀ A B. A -> Either A B
Right : ∀ A B. B -> Either A B
bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C
bindEither : ∀ A B C. (Either A B) -> (B -> Either A C) -> Either A C
bindEither (Left a) amb = Left a
bindEither (Right b) amb = amb b
EitherMonad : {A : U} -> Monad (Either A)
EitherMonad : ∀ A. Monad (Either A)
EitherMonad = MkMonad {Either A} bindEither Right
data Maybe : U -> U where
Just : {A : U} -> A -> Maybe A
Nothing : {A : U} -> Maybe A
Just : ∀ A. A -> Maybe A
Nothing : ∀ A. Maybe A
bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
bindMaybe : ∀ A B. Maybe A -> (A -> Maybe B) -> Maybe B
bindMaybe Nothing amb = Nothing
bindMaybe (Just a) amb = amb a
@@ -40,19 +40,19 @@ MaybeMonad = MkMonad bindMaybe Just
infixr 7 _::_
data List : U -> U where
Nil : {A : U} -> List A
_::_ : {A : U} -> A -> List A -> List A
Nil : ∀ A. List A
_::_ : ∀ A. A -> List A -> List A
infixl 7 _++_
_++_ : {A : U} -> List A -> List A -> List A
_++_ : ∀ A. List A -> List A -> List A
Nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
bindList : {A B : U} -> List A -> (A -> List B) -> List B
bindList : ∀ A B. List A -> (A -> List B) -> List B
bindList Nil f = Nil
bindList (x :: xs) f = f x ++ bindList xs f
singleton : {A : U} -> A -> List A
singleton : ∀ A. A -> List A
singleton a = a :: Nil
-- TODO need better error when the monad is not defined
@@ -61,7 +61,7 @@ ListMonad = MkMonad bindList singleton
infixr 1 _,_
data Pair : U -> U -> U where
_,_ : {A B : U} -> A -> B -> Pair A B
_,_ : ∀ A B. A -> B -> Pair A B
ptype Int
@@ -69,7 +69,7 @@ test : Maybe Int
test = pure 10
foo : Int -> Maybe Int
foo x = Just 42 >> Just x >>= (\ x => pure {_} {Maybe} 10)
foo x = Just 42 >> Just x >>= (\ x => pure 10)
bar : Int -> Maybe Int
bar x = do
@@ -77,7 +77,7 @@ bar x = do
z <- Just x
pure z
baz : {A B : U} -> List A -> List B -> List (Pair A B)
baz : ∀ A B. List A -> List B -> List (Pair A B)
baz xs ys = do
x <- xs
y <- ys

19
src/Lib/Parser.idr
View File

@@ -233,20 +233,23 @@ ebind = do
ibind : Parser (List (FC, String, Icit, Raw))
ibind = do
-- I've gone back and forth on this, but I think {m a b} is more useful than {Nat}
sym "{"
-- REVIEW - I have name required and type optional, which I think is the opposite of what I expect
names <- try (some (withPos varname) <* sym ":")
ty <- typeExpr
names <- (some (withPos varname))
ty <- optional (sym ":" *> typeExpr)
sym "}"
pure $ map (\(pos,name) => (pos, name, Implicit, ty)) names
pure $ map (\(pos,name) => (pos, name, Implicit, fromMaybe (RImplicit pos) ty)) names
abind : Parser (List (FC, String, Icit, Raw))
abind = do
-- for this, however, it would be nice to allow {{Monad A}}
sym "{{"
names <- try (some (withPos varname) <* sym ":")
name <- optional $ try (withPos varname <* sym ":")
ty <- typeExpr
sym "}}"
pure $ map (\(pos,name) => (pos, name, Auto, ty)) names
case name of
Just (pos,name) => pure [(pos, name, Auto, ty)]
Nothing => pure [(getFC ty, "_", Auto, ty)]
arrow : Parser Unit
arrow = sym "->" <|> sym "→"
@@ -371,8 +374,8 @@ parseDecl = parseMixfix <|> parsePType <|> parsePFunc <|> parseNorm <|> parseDat
export
parseModHeader : Parser String
parseModHeader = sameLevel (keyword "module") >> uident
parseModHeader : Parser (FC, String)
parseModHeader = sameLevel (keyword "module") >> withPos uident
export
parseImports : Parser (List Import)

4
src/Main.idr
View File

@@ -63,13 +63,13 @@ processModule base stk name = do
let Right toks = tokenise src
| Left err => fail (showError src err)
let Right (modName, ops, toks) := partialParse parseModHeader top.ops toks
let Right ((nameFC, modName), ops, toks) := partialParse parseModHeader top.ops toks
| Left err => fail (showError src err)
putStrLn "module \{modName}"
let True = name == modName
| _ => fail "ERROR at (0, 0): module name \{show modName} doesn't match file name \{show fn}"
| _ => fail "ERROR at \{show nameFC}: module name \{show modName} doesn't match file name \{show fn}"
let Right (imports, ops, toks) := partialParse parseImports ops toks
| Left err => fail (showError src err)

18
tests/black/Tree.newt
View File

@@ -16,8 +16,8 @@ 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
inl : {A B} -> A -> A + B
inr : {A B} -> B -> A + B
infix 4 _<=_
@@ -47,14 +47,14 @@ _ <<= 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
intv : {l u} (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 : _)
leaf : {l u} (lu : l <<= u) -> T23 l u Z
node2 : {l u h} (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 : _)
node3 : {l u h} (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)
@@ -71,10 +71,8 @@ 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
-- 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 : {l u h} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
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 (intv {_} {N y} x lx xy) tly of

42
tests/black/TypeClass.newt
View File

@@ -3,35 +3,35 @@ module TypeClass
data Monad : (U -> U) -> U where
MkMonad : { M : U -> U } ->
(bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
(pure : {A : U} -> A -> M A) ->
(pure : ∀ A. A -> M A) ->
Monad M
infixl 1 _>>=_ _>>_
_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
_>>=_ {a} {b} {m} {{MkMonad bind' _}} ma amb = bind' {a} {b} ma amb
_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
_>>=_ {{MkMonad bind' _}} ma amb = bind' ma amb
_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
ma >> mb = mb
pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
pure {_} {_} {{MkMonad _ pure'}} a = pure' a
pure : ∀ m a. {{Monad m}} -> a -> m a
pure {{MkMonad _ pure'}} a = pure' a
data Either : U -> U -> U where
Left : {A B : U} -> A -> Either A B
Right : {A B : U} -> B -> Either A B
Left : ∀ A B. A -> Either A B
Right : ∀ A B. B -> Either A B
bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C
bindEither : ∀ A B C. (Either A B) -> (B -> Either A C) -> Either A C
bindEither (Left a) amb = Left a
bindEither (Right b) amb = amb b
EitherMonad : {A : U} -> Monad (Either A)
EitherMonad : ∀ A. Monad (Either A)
EitherMonad = MkMonad {Either A} bindEither Right
data Maybe : U -> U where
Just : {A : U} -> A -> Maybe A
Nothing : {A : U} -> Maybe A
Just : ∀ A. A -> Maybe A
Nothing : ∀ A. Maybe A
bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
bindMaybe : ∀ A B. Maybe A -> (A -> Maybe B) -> Maybe B
bindMaybe Nothing amb = Nothing
bindMaybe (Just a) amb = amb a
@@ -40,19 +40,19 @@ MaybeMonad = MkMonad bindMaybe Just
infixr 7 _::_
data List : U -> U where
Nil : {A : U} -> List A
_::_ : {A : U} -> A -> List A -> List A
Nil : ∀ A. List A
_::_ : ∀ A. A -> List A -> List A
infixl 7 _++_
_++_ : {A : U} -> List A -> List A -> List A
_++_ : ∀ A. List A -> List A -> List A
Nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
bindList : {A B : U} -> List A -> (A -> List B) -> List B
bindList : ∀ A B. List A -> (A -> List B) -> List B
bindList Nil f = Nil
bindList (x :: xs) f = f x ++ bindList xs f
singleton : {A : U} -> A -> List A
singleton : ∀ A. A -> List A
singleton a = a :: Nil
-- TODO need better error when the monad is not defined
@@ -61,7 +61,7 @@ ListMonad = MkMonad bindList singleton
infixr 1 _,_
data Pair : U -> U -> U where
_,_ : {A B : U} -> A -> B -> Pair A B
_,_ : ∀ A B. A -> B -> Pair A B
ptype Int
@@ -69,7 +69,7 @@ test : Maybe Int
test = pure 10
foo : Int -> Maybe Int
foo x = Just 42 >> Just x >>= (\ x => pure {_} {Maybe} 10)
foo x = Just 42 >> Just x >>= (\ x => pure 10)
bar : Int -> Maybe Int
bar x = do
@@ -77,7 +77,7 @@ bar x = do
z <- Just x
pure z
baz : {A B : U} -> List A -> List B -> List (Pair A B)
baz : ∀ A B. List A -> List B -> List (Pair A B)
baz xs ys = do
x <- xs
y <- ys