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

try to fix missing Aoc.newt in playground

Browse Source
This commit is contained in:
Steve Dunham
2024-12-18 14:00:59 -08:00
parent 54b50f3761
commit 6e8727c784
14 changed files with 2 additions and 1138 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
TODO.md
View File

@@ -7,7 +7,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
- [x] for parse error, seek to col 0 token and process next decl - [x] for parse error, seek to col 0 token and process next decl
- [ ] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality) - [ ] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality)
- [ ] Keep a `compare` function on `SortedMap` (like lean) - [ ] Keep a `compare` function on `SortedMap` (like lean)
- [ ] keymap for monaco - [x] keymap for monaco
- [x] SortedMap.newt issue in `where` - [x] SortedMap.newt issue in `where`
- [x] fix "insufficient patterns", wire in M or Either String - [x] fix "insufficient patterns", wire in M or Either String
- [x] Matching _,_ when Maybe is expected should be an error - [x] Matching _,_ when Maybe is expected should be an error

71
playground/samples/aoc2023/Day1.newt
View File

@@ -1,71 +0,0 @@
module Day1
/-
I ported a couple of Advent of Code 2023 solutions from Lean4
as an early test case. Here I've adapted them to the web playground
by replacing `readFile` with an async `fetchText`.
-/
import Web
digits1 : List Char -> List Int
digits1 Nil = Nil
digits1 (c :: cs) = let x = ord c in
case x < 58 of
True => case 48 < x of
True => x - 48 :: digits1 cs
False => digits1 cs
False => digits1 cs
-- TODO I used @ patterns in Lean
digits2 : List Char -> List Int
digits2 xs = case xs of
('o' :: 'n' :: 'e' :: _) => 1 :: digits2 (tail xs)
('t' :: 'w' :: 'o' :: _) => 2 :: digits2 (tail xs)
('t' :: 'h' :: 'r' :: 'e' :: 'e' :: _) => 3 :: digits2 (tail xs)
('f' :: 'o' :: 'u' :: 'r' :: _) => 4 :: digits2 (tail xs)
('f' :: 'i' :: 'v' :: 'e' :: _) => 5 :: digits2 (tail xs)
('s' :: 'i' :: 'x' :: _) => 6 :: digits2 (tail xs)
('s' :: 'e' :: 'v' :: 'e' :: 'n' :: _) => 7 :: digits2 (tail xs)
('e' :: 'i' :: 'g' :: 'h' :: 't' :: _) => 8 :: digits2 (tail xs)
('n' :: 'i' :: 'n' :: 'e' :: _) => 9 :: digits2 (tail xs)
(c :: cs) => let x = ord c in
case x < 58 of
True => case 48 < x of
True => x - 48 :: digits2 cs
False => digits2 cs
False => digits2 cs
Nil => Nil
combine : List Int -> Int
combine Nil = 0
combine (x :: Nil) = x * 10 + x
combine (x :: y :: Nil) = x * 10 + y
combine (x :: y :: xs) = combine (x :: xs)
part1 : String -> (String -> List Int) -> Int
part1 text digits =
let lines = split (trim text) "\n" in
let nums = map combine $ map digits lines in
foldl _+_ 0 nums
#check digits1 ∘ unpack : String -> List Int
runFile : String -> Async Unit
runFile fn = do
text <- fetchText fn
putStrLn fn
putStrLn "part1"
putStrLn $ show (part1 text (digits1 ∘ unpack))
putStrLn "part2"
putStrLn $ show (part1 text (digits2 ∘ unpack))
putStrLn ""
-- Argument is a hack to keep it from running at startup. Need to add IO
main : IO Unit
main = runAsync (do
runFile "aoc2023/day1/eg.txt"
runFile "aoc2023/day1/eg2.txt"
-- runFile "aoc2023/day1/input.txt"
)

92
playground/samples/aoc2023/Day2.newt
View File

@@ -1,92 +0,0 @@
module Day2
/-
I ported a couple of Advent of Code 2023 solutions from Lean4
as an early test case. Here I've adapted them to the web playground
by replacing `readFile` with an async `fetchText`.
-/
import Web
Draw : U
Draw = Int × Int × Int
data Game : U where
MkGame : Int -> List Draw -> Game
-- Original had class and instance...
-- Add, Sub, Mul, Neg
max : Int -> Int -> Int
max x y = case x < y of
True => y
False => x
pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, ' ')`
pfunc toInt : String -> Int := `s => Number(s)`
maxd : Draw -> Draw -> Draw
maxd (a,b,c) (d,e,f) = (max a d, max b e, max c f)
lte : Draw -> Draw -> Bool
lte (a,b,c) (d,e,f) = a <= d && b <= e && c <= f
parseColor : String -> Either String Draw
parseColor line = case split line " " of
(n :: "red" :: Nil) => Right (toInt n,0,0)
(n :: "green" :: Nil) => Right (0,toInt n,0)
(n :: "blue" :: Nil) => Right (0,0,toInt n)
x => Left $ "Bad draw" ++ repr x
parseDraw : String -> Either String Draw
parseDraw line = case mapM {Either String} parseColor $ split line ", " of
Right parts => Right $ foldl maxd (0,0,0) parts
Left err => Left err
parseGame : String -> Either String Game
parseGame line =
-- Need the Idris | sugar...
case split line ": " of
-- this is splitting on the Nil instead of the a
(a :: b :: Nil) => case split a " " of
("Game" :: ns :: Nil) =>
let num = toInt ns in
case mapM {Either String} parseDraw $ split b "; " of
Right parts => Right $ MkGame num parts
Left err => Left err
_ => Left "No Game"
_ => Left $ "No colon in " ++ line
part1 : List Game -> Int
part1 Nil = 0
part1 (MkGame n parts :: rest) =
let total = foldl maxd (0,0,0) parts in
case lte total (12,13,14) of
True => n + part1 rest
False => part1 rest
part2 : List Game -> Int
part2 Nil = 0
part2 (MkGame n parts :: rest) =
case foldl maxd (0,0,0) parts of
(a,b,c) => a * b * c + part2 rest
-- readFile not in browser / playground
run : String -> Async Unit
run fn = do
text <- fetchText fn
case mapM {Either String} parseGame (split (trim text) "\n") of
Left err => putStrLn $ "fail " ++ err
Right games => do
putStrLn "part1"
printLn (part1 games)
putStrLn "part2"
printLn (part2 games)
main : IO Unit
main = runAsync (do
run "aoc2023/day2/eg.txt"
run "aoc2023/day2/input.txt"
)

115
playground/samples/aoc2023/Day3.newt
View File

@@ -1,115 +0,0 @@
module Day3
import Prelude
import Node
pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, ' ')`
maybe : ∀ a b. b → (a → b) → Maybe a → b
maybe def f Nothing = def
maybe def f (Just a) = f a
-- was 'structure' I could make a `record` that destructures to this..
data Number : U where
MkNumber : (start : Nat) -> (stop : Nat) → (value : Int) → Number
isDigit : Char -> Bool
isDigit '0' = True
isDigit '1' = True
isDigit '2' = True
isDigit '3' = True
isDigit '4' = True
isDigit '5' = True
isDigit '6' = True
isDigit '7' = True
isDigit '8' = True
isDigit '9' = True
isDigit _ = False
numbers : List Char -> List Number
numbers arr = go arr Z
where
go : List Char → Nat → List Number
go (c :: cs) start = if isDigit c
then case span isDigit (c :: cs) of
(front,back) => let stop = start + length front
in MkNumber start stop (stringToInt $ pack front) :: go back stop
else go cs (S start)
go Nil start = Nil
range : ∀ a. Nat -> Nat -> List a -> List a
range _ _ Nil = Nil
range _ Z _ = Nil
range Z (S k) (x :: xs) = x :: range Z k xs
range (S n) (S m) (x :: xs) = range n m xs
isPart : List (List Char) -> Nat -> Number -> Bool
isPart rows row (MkNumber start end _) =
checkRow (pred row) || checkRow row || checkRow (S row)
where
isThing : Char -> Bool
isThing c = not (isDigit c || c == '.')
checkRow : Nat -> Bool
checkRow r = case getAt r rows of
Nothing => False
Just chars => case filter isThing (range (pred start) (S end) chars) of
Nil => False
_ => True
getValue : Number -> Int
getValue (MkNumber _ _ v) = v
part1 : List (List Char) -> Int
part1 rows =
foldl (\ acc num => acc + getValue num) 0 $
join $ map (partNums rows) $ enumerate rows
where
partNums : List (List Char) -> (Nat × List Char) -> List Number
partNums grid (r, cs) =
filter (isPart grid r) $ (numbers cs)
gears : List (List Char) -> List Char -> Nat -> Int
gears rows row y =
let a = numbers (getAt! (pred y) rows)
b = numbers (getAt! y rows)
c = numbers (getAt! (S y) rows)
all = a ++ b ++ c
cands = map fst $ filter (_==_ '*' ∘ snd) (enumerate row)
in foldl _+_ 0 $ map (check all) cands
where
ratio : List Int → Int
ratio (a :: b :: Nil) = a * b
ratio _ = 0
match : Nat → Number → Bool
match y (MkNumber start stop value) = pred start <= y && y < S stop
check : List Number → Nat → Int
check nums y = ratio $ map getValue (filter (match y) nums)
part2 : List (List Char) -> Int
part2 rows =
foldl go 0 (enumerate rows)
where
go : Int → Nat × List Char → Int
go acc (y, row) = acc + gears rows row y
-- 4361 / 467835
-- 517021 / 81296995
run : String -> IO Unit
run fn = do
content <- readFile fn
let grid = (splitOn '\n' $ unpack $ trim content)
putStrLn fn
printLn (part1 grid)
printLn (part2 grid)
main : IO Unit
main = do
run "aoc2023/day3/eg.txt"
run "aoc2023/day3/input.txt"

67
playground/samples/aoc2023/Day4.newt
View File

@@ -1,67 +0,0 @@
module Day4
import Prelude
import Node
Round : U
Round = List Int × List Int
parseRound : String → Maybe Round
parseRound s =
case split s ": " of
(a :: b :: Nil) => case split b " | " of
(l :: r :: Nil) => Just (nums l, nums r)
_ => Nothing
_ => Nothing
where
-- Nat or Int here?
nums : String → List Int
-- catch - split returns empty strings that become zeros
nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
parse : String -> Maybe (List Round)
parse s = mapM parseRound (split (trim s) "\n")
pfunc pow : Int → Int → Int := `(x,y) => x ** y`
part1 : List Round → Int
part1 rounds = foldl _+_ 0 $ map score rounds
where
-- TODO we'll keep the math in Int land until we have magic Nat
score : Round → Int
score (a,b) = let count = natToInt $ length $ filter (\ n => elem n b) a
in if count == 0 then 0 else pow 2 (count - 1)
part2 : List Round → Int
part2 rounds = go 0 $ map (_,_ 1) rounds
where
mark : Int -> Nat → List (Int × Round) → List (Int × Round)
mark _ _ Nil = Nil
mark v Z rounds = rounds
mark v (S k) ((cnt, round) :: rounds) = (cnt + v, round) :: mark v k rounds
go : Int → List (Int × Round) → Int
go acc Nil = acc
go acc ((cnt, a, b) :: rounds) =
let n = length $ filter (\ n => elem n b) a
in go (acc + cnt) $ mark cnt n rounds
run : String -> IO Unit
run fn = do
putStrLn fn
text <- readFile fn
case parse text of
Nothing => putStrLn "fail"
Just cards => do
putStrLn "part1"
printLn (part1 cards)
putStrLn "part2"
printLn (part2 cards)
-- 13/30
-- 25004/14427616
main : IO Unit
main = do
run "aoc2023/day4/eg.txt"
run "aoc2023/day4/input.txt"

7
playground/samples/aoc2023/Node.newt
View File

@@ -1,7 +0,0 @@
module Node
import Prelude
pfunc fs : JSObject := `require('fs')`
pfunc getArgs : List String := `arrayToList(String, process.argv)`
pfunc readFile uses (fs) : (fn : String) -> IO String := `(fn) => (w) => MkIORes(Unit, fs.readFileSync(fn, 'utf8'), w)`

725
playground/samples/aoc2023/Prelude.newt
View File

@@ -1,725 +0,0 @@
module Prelude
id : ∀ a. a → a
id x = x
the : (a : U) → a → a
the _ a = a
data Bool : U where
True False : Bool
not : Bool → Bool
not True = False
not False = True
-- In Idris, this is lazy in the second arg, we're not doing
-- magic laziness for now, it's messy
infixr 4 _||_
_||_ : 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
x == y = False
data Maybe : U -> U where
Just : ∀ a. a -> Maybe a
Nothing : ∀ a. Maybe a
fromMaybe : ∀ a. a → Maybe a → a
fromMaybe a Nothing = a
fromMaybe _ (Just a) = a
data Either : U -> U -> U where
Left : {0 a b : U} -> a -> Either a b
Right : {0 a b : U} -> b -> Either a b
infixr 7 _::_
data List : U -> U where
Nil : ∀ A. List A
_::_ : ∀ A. A → List A → List A
length : ∀ a. List a → Nat
length Nil = Z
length (x :: xs) = S (length xs)
infixl 7 _:<_
data SnocList : U → U where
Lin : ∀ A. SnocList A
_:<_ : ∀ A. SnocList A → A → SnocList A
-- 'chips'
infixr 6 _<>>_
_<>>_ : ∀ a. SnocList a → List a → List a
Lin <>> ys = ys
(xs :< x) <>> ys = xs <>> x :: ys
-- 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
fst : ∀ a b. a × b → a
fst (a,b) = a
snd : ∀ a b. a × b → b
snd (a,b) = b
-- Monad
class Monad (m : U → U) where
bind : {0 a b} → m a → (a → m b) → m b
pure : {0 a} → a → m a
infixl 1 _>>=_ _>>_
_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
ma >>= amb = bind ma amb
_>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
ma >> mb = ma >>= (\ _ => mb)
join : ∀ m a. {{Monad m}} → m (m a) → m a
join mma = mma >>= id
-- Equality
infixl 1 _≡_
data _≡_ : {A : U} -> A -> A -> U where
Refl : {A : U} -> {a : A} -> a ≡ a
replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
replace p Refl x = x
cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
sym Refl = Refl
-- Functor
class Functor (m : U → U) where
map : {0 a b} → (a → b) → m a → m b
infixr 4 _<$>_
_<$>_ : {0 f} {{Functor f}} {0 a b} → (a → b) → f a → f b
f <$> ma = map f ma
instance Functor Maybe where
map f Nothing = Nothing
map f (Just a) = Just (f a)
instance Functor List where
map f Nil = Nil
map f (x :: xs) = f x :: map f xs
instance Functor SnocList where
map f Lin = Lin
map f (xs :< x) = map f xs :< f x
-- TODO this probably should depend on / entail Functor
infixl 3 _<*>_
class Applicative (f : U → U) where
-- appIsFunctor : Functor f
return : {0 a} → a → f a
_<*>_ : {0 a b} -> f (a → b) → f a → f b
class Traversable (t : U → U) where
traverse : ∀ f a b. {{Applicative f}} → (a → f b) → t a → f (t b)
instance Traversable List where
traverse f Nil = return Nil
traverse f (x :: xs) = return _::_ <*> f x <*> traverse f xs
for : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f (t b)
for stuff fun = traverse fun stuff
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
instance Alternative Maybe where
Nothing <|> x = x
Just x <|> _ = Just x
-- Semigroup
infixl 8 _<+>_
class Semigroup a where
_<+>_ : a → a → a
infixl 7 _+_
class Add a where
_+_ : a → a → a
infixl 8 _*_ _/_
class Mul a where
_*_ : a → a → a
class Div a where
_/_ : a → a → a
instance Add Nat where
Z + m = m
S n + m = S (n + m)
instance Mul Nat where
Z * _ = Z
S n * m = m + n * m
infixl 7 _-_
class Sub a where
_-_ : a → a → a
instance Sub Nat where
Z - m = Z
n - Z = n
S n - S m = n - m
infixr 7 _++_
class Concat a where
_++_ : a → a → a
ptype String
ptype Int
ptype Char
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`
pfunc jsLT 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
ptype Array : U → U
pfunc listToArray : {a : U} -> List a -> Array a := `
(a, l) => {
let rval = []
while (l.tag !== 'Nil') {
rval.push(l.h1)
l = l.h2
}
return rval
}
`
pfunc alen : {0 a : U} -> Array a -> Int := `(a,arr) => arr.length`
pfunc aget : {0 a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
pfunc aempty : {0 a : U} -> Unit -> Array a := `() => []`
pfunc arrayToList uses (Nil _::_) : {0 a} → Array a → List a := `(a,arr) => {
let rval = Nil(a)
for (let i = arr.length - 1;i >= 0; i--) {
rval = _$3A$3A_(a, arr[i], rval)
}
return rval
}`
-- for now I'll run this in JS
pfunc lines : String → List String := `(s) => arrayToList(s.split('\n'))`
pfunc p_strHead : (s : String) -> Char := `(s) => s[0]`
pfunc p_strTail : (s : String) -> String := `(s) => s[0]`
pfunc trim : String -> String := `s => s.trim()`
pfunc split uses (Nil _::_) : String -> String -> List String := `(s, by) => {
let parts = s.split(by)
let rval = Nil(String)
parts.reverse()
parts.forEach(p => { rval = _$3A$3A_(undefined, p, rval) })
return rval
}`
pfunc slen : String -> Int := `s => s.length`
pfunc sindex : String -> Int -> Char := `(s,i) => s[i]`
-- TODO represent Nat as number at runtime
pfunc natToInt : Nat -> Int := `(n) => {
let rval = 0
while (n.tag === 'S') {
n = n.h0
rval++
}
return rval
}`
pfunc intToNat uses (Z S) : Int -> Nat := `(n) => {
let rval = Z
for (;n>0;n--) rval = S(rval);
return rval;
}`
pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')`
pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))`
-- I don't want to use an empty type because it would be a proof of void
ptype World
data IORes : U -> U where
MkIORes : ∀ a. a -> World -> IORes a
IO : U -> U
IO a = World -> IORes a
instance Monad IO where
bind ma mab = \ w => case ma w of
MkIORes a w => mab a w
pure x = \ w => MkIORes x w
bindList : ∀ a b. List a → (a → List b) → List b
instance ∀ a. Concat (List a) where
Nil ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)
instance Monad List where
pure a = a :: Nil
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
instance HasIO IO where
liftIO a = a
pfunc primPutStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
console.log(s)
return MkIORes(undefined,MkUnit,w)
}`
putStrLn : ∀ io. {{HasIO io}} -> String -> io Unit
putStrLn s = liftIO (primPutStrLn s)
pfunc showInt : Int -> String := `(i) => String(i)`
class Show a where
show : a → String
instance Show String where
show a = a
instance Show Int where
show = showInt
pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)`
pfunc unpack uses (Nil _::_) : String -> List Char
:= `(s) => {
let acc = Nil(undefined)
for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(undefined, s[i], acc)
return acc
}`
pfunc pack : List Char → String := `(cs) => {
let rval = ''
while (cs.tag === '_::_') {
rval += cs.h1
cs = cs.h2
}
return rval
}
`
pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => {
const go = (obj) => {
if (obj === undefined) return "_"
if (obj.tag === '_,_') {
let rval = '('
while (obj?.tag === '_,_') {
rval += go(obj.h2) + ', '
obj = obj.h3
}
return rval + go(obj) + ')'
}
if (obj?.tag === '_::_' || obj?.tag === 'Nil') {
let stuff = listToArray(undefined,obj)
return '['+(stuff.map(go).join(', '))+']'
}
if (obj instanceof Array) {
return 'io['+(obj.map(go).join(', '))+']'
}
if (obj?.tag === 'S' || obj?.tag === 'Z') {
return ''+natToInt(obj)
} else if (obj?.tag) {
let rval = '('+obj.tag
for(let i=0;;i++) {
let key = 'h'+i
if (!(key in obj)) break
rval += ' ' + go(obj[key])
}
return rval+')'
} else {
return JSON.stringify(obj)
}
}
return go(obj)
}`
debugLog : ∀ a. a → IO Unit
debugLog a = putStrLn (debugStr a)
pfunc stringToInt : String → Int := `(s) => {
let rval = Number(s)
if (isNaN(rval)) throw new Error(s + " is NaN")
return rval
}`
foldl : ∀ A B. (B -> A -> B) -> B -> List A -> B
foldl f acc Nil = acc
foldl f acc (x :: xs) = foldl f (f acc x) xs
infixl 9 _∘_
_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
(f ∘ g) x = f (g x)
pfunc addInt : Int → Int → Int := `(x,y) => x + y`
pfunc mulInt : Int → Int → Int := `(x,y) => x * y`
pfunc divInt : Int → Int → Int := `(x,y) => x / y|0`
pfunc subInt : Int → Int → Int := `(x,y) => x - y`
pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? True : False`
instance Mul Int where
x * y = mulInt x y
instance Add Int where
x + y = addInt x y
instance Sub Int where
x - y = subInt x y
instance Div Int where
x / y = divInt x y
printLn : {m} {{HasIO m}} {a} {{Show a}} → a → m Unit
printLn a = putStrLn (show a)
-- opaque JSObject
ptype JSObject
reverse : ∀ a. List a → List a
reverse {a} = go Nil
where
go : List a → List a → List a
go acc Nil = acc
go acc (x :: xs) = go (x :: acc) xs
-- Like Idris1, but not idris2, we need {a} to put a in scope.
span : ∀ a. (a -> Bool) -> List a -> List a × List a
span {a} f xs = go xs Nil
where
go : List a -> List a -> List a × List a
go Nil left = (reverse left, 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 }`
mapMaybe : ∀ a b. (a → Maybe b) → List a → List b
mapMaybe f Nil = Nil
mapMaybe f (x :: xs) = case f x of
Just y => y :: mapMaybe f xs
Nothing => mapMaybe f xs
zip : ∀ a b. List a → List b → List (a × b)
zip (x :: xs) (y :: ys) = (x,y) :: zip xs ys
zip _ _ = Nil
-- TODO add double literals
ptype Double
pfunc intToDouble : Int → Double := `(x) => x`
pfunc doubleToInt : Double → Int := `(x) => x`
pfunc addDouble : Double → Double → Double := `(x,y) => x + y`
pfunc subDouble : Double → Double → Double := `(x,y) => x - y`
pfunc mulDouble : Double → Double → Double := `(x,y) => x * y`
pfunc divDouble : Double → Double → Double := `(x,y) => x / y`
pfunc sqrtDouble : Double → Double := `(x) => Math.sqrt(x)`
pfunc ceilDouble : Double → Double := `(x) => Math.ceil(x)`
instance Add Double where x + y = addDouble x y
instance Sub Double where x - y = subDouble x y
instance Mul Double where x * y = mulDouble x y
instance Div Double where x / y = divDouble x y
ptype IOArray : U → U
pfunc newArray uses (MkIORes) : ∀ a. Int → a → IO (IOArray a) :=
`(_, n, v) => (w) => MkIORes(undefined,Array(n).fill(v),w)`
pfunc arrayGet : ∀ a. IOArray a → Int → IO a := `(_, arr, ix) => w => MkIORes(undefined, arr[ix], w)`
pfunc arraySet uses (MkUnit) : ∀ a. IOArray a → Int → a → IO Unit := `(_, arr, ix, v) => w => {
arr[ix] = v
return MkIORes(undefined, MkUnit, w)
}`
pfunc arraySize uses (MkIORes) : ∀ a. IOArray a → IO Int := `(_, arr) => w => MkIORes(undefined, arr.length, w)`
pfunc ioArrayToList uses (Nil _::_ MkIORes) : {0 a} → IOArray a → IO (List a) := `(a,arr) => w => {
let rval = Nil(a)
for (let i = arr.length - 1;i >= 0; i--) {
rval = _$3A$3A_(a, arr[i], rval)
}
return MkIORes(undefined, rval, w)
}`
pfunc listToIOArray uses (MkIORes) : {0 a} → List a → IO (Array a) := `(a,list) => w => {
let rval = []
while (list.tag === '_::_') {
rval.push(list.h1)
list = list.h2
}
return MkIORes(undefined,rval,w)
}`
class Cast a b where
cast : a → b
instance Cast Nat Int where
cast = natToInt
instance Cast Int Double where
cast = intToDouble
instance Applicative IO where
return a = \ w => MkIORes a w
f <*> a = \ w =>
let (MkIORes f w) = trace "fw" $ f w in
let (MkIORes a w) = trace "aw" $ a w in
MkIORes (f a) w
class Bifunctor (f : U → U → U) where
bimap : ∀ a b c d. (a → c) → (b → d) → f a b → f c d
mapFst : ∀ a b c f. {{Bifunctor f}} → (a → c) → f a b → f c b
mapFst f ab = bimap f id ab
mapSnd : ∀ a b c f. {{Bifunctor f}} → (b → c) → f a b → f a c
mapSnd f ab = bimap id f ab
isNothing : ∀ a. Maybe a → Bool
isNothing Nothing = True
isNothing _ = False
instance Bifunctor _×_ where
bimap f g (a,b) = (f a, g b)
instance Functor IO where
map f a = bind a $ \ a => pure (f a)
uncurry : ∀ a b c. (a -> b -> c) -> (a × b) -> c
uncurry f (a,b) = f a b
-- TODO Idris has a tail recursive version of this
instance Applicative List where
return a = a :: Nil
Nil <*> _ = Nil
fs <*> ys = join $ map (\ f => map f ys) fs
tail : ∀ a. List a → List a
tail Nil = Nil
tail (x :: xs) = xs
--
infixl 6 _<_ _<=_
class Ord a where
-- isEq : Eq a
_<_ : a → a → Bool
_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
a <= b = a == b || a < b
search : ∀ cl. {{cl}} -> cl
search {{x}} = x
instance Ord Nat where
-- isEq = search
_ < Z = False
Z < S _ = True
S n < S m = n < m
instance Ord Int where
-- isEq = ?
x < y = ltInt x y
instance Ord Char where
x < y = jsLT x y
-- foo : ∀ a. {{Ord a}} -> a -> Bool
-- foo a = a == a
flip : ∀ a b c. (a → b → c) → (b → a → c)
flip f b a = f a b
partition : ∀ a. (a → Bool) → List a → List a × List a
partition {a} pred xs = go xs Nil Nil
where
go : List a → List a → List a → List a × List a
go Nil as bs = (as, bs)
go (x :: xs) as bs = if pred x
then go xs (x :: as) bs
else go xs as (x :: bs)
-- probably not super efficient, but it works
qsort : ∀ a. (a → a → Bool) → List a → List a
qsort lt Nil = Nil
qsort lt (x :: xs) = qsort lt (filter (λ y => not $ lt x y) xs) ++ x :: qsort lt (filter (lt x) xs)
ordNub : ∀ a. {{Eq a}} {{Ord a}} -> List a -> List a
ordNub {a} {{ordA}} xs = go $ qsort _<_ xs
where
go : List a → List a
go (a :: b :: xs) = if a == b then go (a :: xs) else a :: go (b :: xs)
go t = t
ite : ∀ a. Bool → a → a → a
ite c t e = if c then t else e
instance Ord String where
a < b = jsLT a b
instance Cast Int Nat where
cast n = intToNat n

26
playground/samples/aoc2023/Web.newt
View File

@@ -1,26 +0,0 @@
module Web
import Prelude
ptype Async : U -> U
pfunc resolve : ∀ a. a -> Async a := `(_, a) => Promise.resolve(a)`
pfunc andThen : ∀ a b. Async a -> (a -> Async b) -> Async b := `(A,B,a,ab) => a.then(ab)`
pfunc reject : ∀ a. String -> Async a := `(_, msg) => Promise.reject(msg)`
instance Monad Async where
bind = andThen
pure = resolve
-- It'd be nice to be able to declare operators and JS "projections"
pfunc fetchText : String -> Async String := `async (url) => {
let response = await fetch(url)
return response.text()
}`
pfunc liftAsync : ∀ a. IO a -> Async a := `(_, a) => Promise.resolve(a(undefined).h0)`
instance HasIO Async where
liftIO = liftAsync
runAsync : ∀ a. Async a -> IO Unit
runAsync foo = pure MkUnit

5
playground/samples/aoc2023/day1/eg.txt
View File

@@ -1,5 +0,0 @@
1abc2
pqr3stu8vwx
a1b2c3d4e5f
treb7uchet

7
playground/samples/aoc2023/day1/eg2.txt
View File

@@ -1,7 +0,0 @@
two1nine
eightwothree
abcone2threexyz
xtwone3four
4nineeightseven2
zoneight234
7pqrstsixteen

5
playground/samples/aoc2023/day2/eg.txt
View File

@@ -1,5 +0,0 @@
Game 1: 3 blue, 4 red; 1 red, 2 green, 6 blue; 2 green
Game 2: 1 blue, 2 green; 3 green, 4 blue, 1 red; 1 green, 1 blue
Game 3: 8 green, 6 blue, 20 red; 5 blue, 4 red, 13 green; 5 green, 1 red
Game 4: 1 green, 3 red, 6 blue; 3 green, 6 red; 3 green, 15 blue, 14 red
Game 5: 6 red, 1 blue, 3 green; 2 blue, 1 red, 2 green

10
playground/samples/aoc2023/day3/eg.txt
View File

@@ -1,10 +0,0 @@
467..114..
...*......
..35..633.
......#...
617*......
.....+.58.
..592.....
......755.
...$.*....
.664.598..

6
playground/samples/aoc2023/day4/eg.txt
View File

@@ -1,6 +0,0 @@
Card 1: 41 48 83 86 17 | 83 86 6 31 17 9 48 53
Card 2: 13 32 20 16 61 | 61 30 68 82 17 32 24 19
Card 3: 1 21 53 59 44 | 69 82 63 72 16 21 14 1
Card 4: 41 92 73 84 69 | 59 84 76 51 58 5 54 83
Card 5: 87 83 26 28 32 | 88 30 70 12 93 22 82 36
Card 6: 31 18 13 56 72 | 74 77 10 23 35 67 36 11

2
playground/samples/aoc2024/Aoc.newt
View File

@@ -1 +1 @@
../../../aoc2024/Aoc.newt ../../../aoc2023/Aoc.newt