From 71cf4f39f526237acb01d860539c3b03c2e45cf9 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 30 Nov 2024 15:51:06 -0800 Subject: [PATCH] Make $ special --- TODO.md | 2 +- aoc2023/Prelude.newt | 10 +- newt-vscode/syntaxes/newt.tmLanguage.json | 2 +- newt/Prelude.newt | 163 ++++++++++++++++++++-- playground/samples/Prelude.newt | 10 +- src/Lib/Parser.idr | 14 +- src/Lib/Tokenizer.idr | 1 + 7 files changed, 173 insertions(+), 29 deletions(-) diff --git a/TODO.md b/TODO.md index 76b1274..7e43f57 100644 --- a/TODO.md +++ b/TODO.md @@ -5,7 +5,7 @@ - [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it. - [x] deconstructing `let` (and do arrows) - [x] Fix string printing to be js instead of weird Idris strings -- [ ] make $ special +- [x] make $ special - Makes inference easier, cleaner output, and allows `foo $ \ x => ...` - remove hack from Elab.infer - [ ] Support @ on the LHS diff --git a/aoc2023/Prelude.newt b/aoc2023/Prelude.newt index 429791e..170179e 100644 --- a/aoc2023/Prelude.newt +++ b/aoc2023/Prelude.newt @@ -76,12 +76,10 @@ _<>>_ : ∀ a. SnocList a → List a → List a Lin <>> ys = ys (xs :< x) <>> ys = xs <>> x :: ys --- TODO this is special cased in some languages, maybe for easier --- inference? Figure out why. --- Currently very noisy in generated code (if nothing else, optimize it out?) -infixr 0 _$_ -_$_ : ∀ a b. (a -> b) -> a -> b -f $ a = f a +-- This is now handled by the parser, and LHS becomes `f a`. +-- infixr 0 _$_ +-- _$_ : ∀ a b. (a -> b) -> a -> b +-- f $ a = f a infixr 8 _×_ infixr 2 _,_ diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index 077ee80..05b9886 100644 --- a/newt-vscode/syntaxes/newt.tmLanguage.json +++ b/newt-vscode/syntaxes/newt.tmLanguage.json @@ -16,7 +16,7 @@ }, { "name": "keyword.newt", - "match": "\\b(data|where|do|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" + "match": "\\b(λ|=>|->|→|:=|\\$|data|where|do|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" }, { "name": "string.js", diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 7676fd4..170179e 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -1,5 +1,7 @@ module Prelude +id : ∀ a. a → a +id x = x data Bool : U where True False : Bool @@ -15,14 +17,27 @@ _||_ : Bool → Bool → Bool True || _ = True False || b = b +infixr 5 _&&_ +_&&_ : Bool → Bool → Bool +False && b = False +True && b = b + infixl 6 _==_ class Eq a where _==_ : a → a → Bool +infixl 6 _/=_ +_/=_ : ∀ a. {{Eq a}} → a → a → Bool +a /= b = not (a == b) + data Nat : U where Z : Nat S : Nat -> Nat +pred : Nat → Nat +pred Z = Z +pred (S k) = k + instance Eq Nat where Z == Z = True S n == S m = n == m @@ -61,19 +76,23 @@ _<>>_ : ∀ a. SnocList a → List a → List a Lin <>> ys = ys (xs :< x) <>> ys = xs <>> x :: ys --- TODO this is special cased in some languages, maybe for easier --- inference? Figure out why. --- Currently very noisy in generated code (if nothing else, optimize it out?) -infixr 0 _$_ -_$_ : ∀ a b. (a -> b) -> a -> b -f $ a = f a +-- This is now handled by the parser, and LHS becomes `f a`. +-- infixr 0 _$_ +-- _$_ : ∀ a b. (a -> b) -> a -> b +-- f $ a = f a infixr 8 _×_ infixr 2 _,_ data _×_ : U → U → U where _,_ : ∀ A B. A → B → A × B -infixl 6 _<_ +fst : ∀ a b. a × b → a +fst (a,b) = a + +snd : ∀ a b. a × b → b +snd (a,b) = b + +infixl 6 _<_ _<=_ class Ord a where _<_ : a → a → Bool @@ -82,6 +101,8 @@ instance Ord Nat where Z < S _ = True S n < S m = n < m +_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool +a <= b = a == b || a < b -- Monad class Monad (m : U → U) where @@ -95,6 +116,9 @@ ma >>= amb = bind ma amb _>>_ : {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b ma >> mb = mb +join : ∀ m. {{Monad m}} {0 a} → m (m a) → m a +join mma = mma >>= id + -- Equality infixl 1 _≡_ @@ -137,6 +161,14 @@ class Applicative (f : U → U) where return : {0 a} → a → f a _<*>_ : {0 a b} -> f (a → b) → f a → f b +class Traversable (t : U → U) where + traverse : {f : U → U} → {{appf : Applicative f}} → {a : U} → {b : U} → (a → f b) → t a → f (t b) + +instance Applicative Maybe where + return a = Just a + Nothing <*> _ = Nothing + Just f <*> fa = f <$> fa + infixr 2 _<|>_ class Alternative (m : U → U) where _<|>_ : {0 a} → m a → m a → m a @@ -167,7 +199,6 @@ instance Mul Nat where Z * _ = Z S n * m = m + n * m - infixl 7 _-_ class Sub a where _-_ : a → a → a @@ -189,6 +220,17 @@ pfunc sconcat : String → String → String := `(x,y) => x + y` instance Concat String where _++_ = sconcat + +pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? True : False` +instance Eq Int where + a == b = jsEq a b + +instance Eq String where + a == b = jsEq a b + +instance Eq Char where + a == b = jsEq a b + data Unit : U where MkUnit : Unit @@ -274,6 +316,21 @@ instance Monad List where bind Nil amb = Nil bind (x :: xs) amb = amb x ++ bind xs amb + + +-- This is traverse, but we haven't defined Traversable yet +mapA : ∀ m. {{Applicative m}} {0 a b} → (a → m b) → List a → m (List b) +mapA f Nil = return Nil +mapA f (x :: xs) = return _::_ <*> f x <*> mapA f xs + + +mapM : ∀ m. {{Monad m}} {0 a b} → (a → m b) → List a → m (List b) +mapM f Nil = pure Nil +mapM f (x :: xs) = do + b <- f x + bs <- mapM f xs + pure (b :: bs) + class HasIO (m : U -> U) where liftIO : ∀ a. IO a → m a @@ -306,9 +363,6 @@ instance Show Int where pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)` -infix 6 _<=_ -pfunc _<=_ uses (True False) : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False` - pfunc unpack : String -> List Char := `(s) => { let acc = Nil(Char) @@ -327,9 +381,15 @@ pfunc pack : List Char → String := `(cs) => { } ` -pfunc debugStr : ∀ a. a → String := `(_, obj) => { +pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => { const go = (obj) => { - if (obj?.tag) { + if (obj?.tag === '_::_') { + let stuff = listToArray(undefined,obj) + return '['+(stuff.map(go).join(', '))+']' + } + if (obj?.tag === 'S') { + return ''+natToInt(obj) + } else if (obj?.tag) { let rval = '('+obj.tag for(let i=0;;i++) { let key = 'h'+i @@ -398,3 +458,80 @@ span {a} f xs = go xs Nil go (x :: xs) left = if f x then go xs (x :: left) else (reverse left, x :: xs) + +instance Show Nat where + show n = show (natToInt n) + +enumerate : ∀ a. List a → List (Nat × a) +enumerate {a} xs = go Z xs + where + go : Nat → List a → List (Nat × a) + go k Nil = Nil + go k (x :: xs) = (k,x) :: go (S k) xs + +filter : ∀ a. (a → Bool) → List a → List a +filter pred Nil = Nil +filter pred (x :: xs) = if pred x then x :: filter pred xs else filter pred xs + +drop : ∀ a. Nat -> List a -> List a +drop _ Nil = Nil +drop Z xs = xs +drop (S k) (x :: xs) = drop k xs + +take : ∀ a. Nat -> List a -> List a +take Z xs = Nil +take _ Nil = Nil +take (S k) (x :: xs) = x :: take k xs + +getAt : ∀ a. Nat → List a → Maybe a +getAt _ Nil = Nothing +getAt Z (x :: xs) = Just x +getAt (S k) (x :: xs) = getAt k xs + +splitOn : ∀ a. {{Eq a}} → a → List a → List (List a) +splitOn {a} v xs = go Nil xs + where + go : List a → List a → List (List a) + go acc Nil = reverse acc :: Nil + go acc (x :: xs) = if x == v + then reverse acc :: go Nil xs + else go (x :: acc) xs + + +class Inhabited a where + default : a + +instance ∀ a. Inhabited (List a) where + default = Nil + +getAt! : ∀ a. {{Inhabited a}} → Nat → List a → a +getAt! _ Nil = default +getAt! Z (x :: xs) = x +getAt! (S k) (x :: xs) = getAt! k xs + + +instance ∀ a. Applicative (Either a) where + return b = Right b + Right x <*> Right y = Right (x y) + Left x <*> _ = Left x + Right x <*> Left y = Left y + +instance ∀ a. Monad (Either a) where + pure x = Right x + bind (Right x) mab = mab x + bind (Left x) mab = Left x + +instance Monad Maybe where + pure x = Just x + bind Nothing mab = Nothing + bind (Just x) mab = mab x + + +elem : ∀ a. {{Eq a}} → a → List a → Bool +elem v Nil = False +elem v (x :: xs) = if v == x then True else elem v xs + +-- TODO no empty value on my `Add`, I need a group.. +-- sum : ∀ a. {{Add a}} → List a → a +-- sum xs = foldl _+_ +pfunc trace uses (debugStr) : ∀ a. String -> a -> a := `(_, msg, a) => { console.log(msg,debugStr(_,a)); return a }` diff --git a/playground/samples/Prelude.newt b/playground/samples/Prelude.newt index 429791e..170179e 100644 --- a/playground/samples/Prelude.newt +++ b/playground/samples/Prelude.newt @@ -76,12 +76,10 @@ _<>>_ : ∀ a. SnocList a → List a → List a Lin <>> ys = ys (xs :< x) <>> ys = xs <>> x :: ys --- TODO this is special cased in some languages, maybe for easier --- inference? Figure out why. --- Currently very noisy in generated code (if nothing else, optimize it out?) -infixr 0 _$_ -_$_ : ∀ a b. (a -> b) -> a -> b -f $ a = f a +-- This is now handled by the parser, and LHS becomes `f a`. +-- infixr 0 _$_ +-- _$_ : ∀ a b. (a -> b) -> a -> b +-- f $ a = f a infixr 8 _×_ infixr 2 _,_ diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 23fec96..6fb04b0 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -296,8 +296,9 @@ ifThenElse = do c <- term pure $ RIf fc a b c --- This hits an idris codegen bug if parseOp is last and Lazy -term = caseExpr +term' : Parser Raw + +term' = caseExpr <|> caseLet <|> letExpr <|> lamExpr @@ -306,6 +307,15 @@ term = caseExpr -- Make this last for better error messages <|> parseOp +term = do + t <- term' + rest <- many ((,) <$> getPos <* keyword "$" <*> term') + pure $ apply t rest + where + apply : Raw -> List (FC,Raw) -> Raw + apply t [] = t + apply t ((fc,x) :: xs) = RApp fc t (apply x xs) Explicit + varname : Parser String varname = (ident <|> uident <|> keyword "_" *> pure "_") diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index d9d88d3..183d866 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -11,6 +11,7 @@ keywords = ["let", "in", "where", "case", "of", "data", "U", "do", "∀", "forall", "class", "instance", "if", "then", "else", + "$", "λ", "->", "→", ":", "=>", ":=", "=", "<-", "\\", "_", "|"] checkKW : String -> Token Kind