Remove old aoc2023 directory
This commit is contained in:
4
TODO.md
4
TODO.md
@@ -228,10 +228,6 @@
|
||||
- This may need a little care. But I think I could collect all constructors that only match wildcards into a single case. This would lose any information from breaking out the individual, unnamed cases though.
|
||||
- There are cases where we have `_` and then `Foo` on the next line, but they should all get collected into the `Foo` case. I think I sorted all of this out for primitives.
|
||||
- [x] Case for primitives
|
||||
- [ ] aoc2023 translation
|
||||
- [x] day1
|
||||
- [x] day2 - day6
|
||||
- some "real world" examples
|
||||
- [x] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet
|
||||
- [x] unsolved meta errors repeat (need to freeze or only report at end)
|
||||
- [x] Sanitize JS idents, e.g. `_+_`
|
||||
|
||||
@@ -1,62 +0,0 @@
|
||||
module Day1
|
||||
|
||||
import Prelude
|
||||
import Node
|
||||
|
||||
digits1 : List Char -> List Int
|
||||
digits1 Nil = Nil
|
||||
digits1 (c :: cs) = let x = ord c in
|
||||
if 48 < x && x < 58
|
||||
then x - 48 :: digits1 cs
|
||||
else 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
|
||||
|
||||
runFile : String -> IO Unit
|
||||
runFile fn = do
|
||||
text <- readFile 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 = do
|
||||
runFile "aoc2023/day1/eg.txt"
|
||||
runFile "aoc2023/day1/eg2.txt"
|
||||
runFile "aoc2023/day1/input.txt"
|
||||
@@ -1,82 +0,0 @@
|
||||
module Day2
|
||||
|
||||
import Prelude
|
||||
import Node
|
||||
|
||||
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
|
||||
|
||||
-- FIXME implicit isn't being solved in time here.
|
||||
parseDraw : String -> Either String Draw
|
||||
parseDraw line =
|
||||
case mapM parseColor $ split line ", " of
|
||||
Right parts => Right $ foldl maxd (0,0,0) parts
|
||||
Left err => Left err
|
||||
|
||||
parseGame : String -> Either String Game
|
||||
parseGame line =
|
||||
let (a :: b :: Nil) = split line ": "
|
||||
| _ => Left $ "No colon in " ++ line in
|
||||
let ("Game" :: ns :: Nil) = split a " "
|
||||
| _ => Left $ "No Game" in
|
||||
let (Right parts) = mapM parseDraw $ split b "; "
|
||||
| Left err => Left err in
|
||||
Right $ MkGame (toInt ns) parts
|
||||
|
||||
part1 : List Game -> Int
|
||||
part1 Nil = 0
|
||||
part1 (MkGame n parts :: rest) =
|
||||
let total = foldl maxd (0,0,0) parts in
|
||||
if lte total (12,13,14)
|
||||
then n + part1 rest
|
||||
else part1 rest
|
||||
|
||||
part2 : List Game -> Int
|
||||
part2 Nil = 0
|
||||
part2 (MkGame n parts :: rest) =
|
||||
let (a,b,c) = foldl maxd (0,0,0) parts
|
||||
in a * b * c + part2 rest
|
||||
|
||||
run : String -> IO Unit
|
||||
run fn = do
|
||||
putStrLn fn
|
||||
text <- readFile fn
|
||||
let (Right games) = mapM {Either String} parseGame (split (trim text) "\n")
|
||||
| Left err => putStrLn $ "fail " ++ err
|
||||
putStrLn "part1"
|
||||
printLn (part1 games)
|
||||
putStrLn "part2"
|
||||
printLn (part2 games)
|
||||
|
||||
main : IO Unit
|
||||
main = do
|
||||
run "aoc2023/day2/eg.txt"
|
||||
run "aoc2023/day2/input.txt"
|
||||
@@ -1,104 +0,0 @@
|
||||
module Day3
|
||||
|
||||
import Prelude
|
||||
import Node
|
||||
import Aoc
|
||||
|
||||
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
|
||||
|
||||
|
||||
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"
|
||||
|
||||
@@ -1,63 +0,0 @@
|
||||
module Day4
|
||||
|
||||
import Prelude
|
||||
import Node
|
||||
|
||||
Round : U
|
||||
Round = List Int × List Int
|
||||
|
||||
parseRound : String → Maybe Round
|
||||
parseRound s =
|
||||
let (a :: b :: Nil) = split s ": " | _ => Nothing in
|
||||
let (l :: r :: Nil) = split b " | " | _ => Nothing in
|
||||
Just (nums l, nums r)
|
||||
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
|
||||
let (Just cards) = parse text
|
||||
| _ => putStrLn "fail"
|
||||
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"
|
||||
@@ -1,119 +0,0 @@
|
||||
module Day5
|
||||
|
||||
import Prelude
|
||||
import Node
|
||||
import Aoc
|
||||
|
||||
-- AoC lib?
|
||||
-- nums : String → List Int
|
||||
-- nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
|
||||
|
||||
data MapEntry : U where
|
||||
-- dest / src / len
|
||||
MkEntry : Int → Int → Int → MapEntry
|
||||
|
||||
src : MapEntry -> Int
|
||||
src (MkEntry d s l) = s
|
||||
|
||||
Map : U
|
||||
Map = List MapEntry
|
||||
|
||||
data Problem : U where
|
||||
MkProb : List Int → List Map → Problem
|
||||
|
||||
parseEntry : String → Either String MapEntry
|
||||
parseEntry part = case nums part of
|
||||
(dest :: src :: len :: Nil) => Right $ MkEntry dest src len
|
||||
_ => Left $ "Bad part " ++ part
|
||||
|
||||
parseMap : List String → Either String Map
|
||||
parseMap (_ :: parts) = mapM parseEntry parts
|
||||
parseMap x = Left $ "bad map " ++ debugStr x
|
||||
|
||||
parseFile : String → Either String Problem
|
||||
parseFile content = do
|
||||
let parts = split (trim content) "\n\n"
|
||||
-- TODO deconstructing let
|
||||
let (first :: rest) = parts
|
||||
| _ => Left "expected some parts"
|
||||
let (_ :: x :: Nil) = split first ": "
|
||||
| _ => Left $ "expected ': ' in " ++ first
|
||||
|
||||
let seeds = nums x
|
||||
maps <- mapA (λ part => parseMap (split part "\n")) rest
|
||||
Right $ MkProb seeds maps
|
||||
|
||||
applyEntry : Int → MapEntry → Int
|
||||
applyEntry n (MkEntry dest src len) =
|
||||
if src <= n && n < src + len then n + dest - src else n
|
||||
|
||||
applyMap : Int → Map → Int
|
||||
applyMap n Nil = n
|
||||
applyMap n (MkEntry dest src len :: es) =
|
||||
if src <= n && n < src + len then n + dest - src else applyMap n es
|
||||
|
||||
min : Int → Int → Int
|
||||
min x y = if x < y then x else y
|
||||
|
||||
part1 : Problem → IO Unit
|
||||
part1 (MkProb seeds maps) = do
|
||||
let loc = map (λ s => foldl applyMap s maps) seeds
|
||||
let part1 = foldl min 999999999 loc
|
||||
putStrLn $ "part1 " ++ show part1
|
||||
|
||||
Range : U
|
||||
Range = Int × Int
|
||||
|
||||
apply' : Range → List MapEntry → List Range
|
||||
apply' (r1, r2) x = case x of
|
||||
Nil => (r1, r2) :: Nil
|
||||
(MkEntry d s l) :: es =>
|
||||
if r2 + r1 <= s then (r1,r2) :: Nil -- map after range
|
||||
else if s + l <= r1 then apply' (r1, r2) es -- map before range
|
||||
-- take off any bare range on front
|
||||
else if r1 < s then
|
||||
(r1, s - r1) :: apply' (s, r2 + r1 - s) x
|
||||
else if s + l < r1 + r2 then
|
||||
let slack = r1 - s in
|
||||
(r1 + d - s, l - slack) :: apply' (r1 + l - slack, r2 + slack - l) x
|
||||
else
|
||||
(r1 + d - s, r2) :: Nil
|
||||
|
||||
|
||||
apply : List Range → List MapEntry → List Range
|
||||
apply ranges entries =
|
||||
let entries = qsort (\ a b => src a < src b) entries in
|
||||
join $ map (\ r => apply' r entries) ranges
|
||||
|
||||
mkRanges : List Int → Maybe (List Range)
|
||||
mkRanges (a :: b :: rs) = do
|
||||
rs <- mkRanges rs
|
||||
Just $ (a,b) :: rs
|
||||
mkRanges Nil = Just Nil
|
||||
mkRanges _ = Nothing
|
||||
|
||||
part2 : Problem → IO Unit
|
||||
part2 (MkProb seeds maps) = do
|
||||
let (Just ranges) = mkRanges seeds
|
||||
| Nothing => printLn "odd seeds!"
|
||||
let results = foldl apply ranges maps
|
||||
-- putStrLn $ debugStr results
|
||||
let answer = foldl min 99999999 $ map fst results
|
||||
putStrLn $ "part2 " ++ show answer
|
||||
|
||||
run : String -> IO Unit
|
||||
run fn = do
|
||||
putStrLn fn
|
||||
text <- readFile fn
|
||||
let (Right prob) = parseFile text
|
||||
| Left err => putStrLn err
|
||||
putStrLn $ debugStr prob
|
||||
part1 prob
|
||||
part2 prob
|
||||
|
||||
-- 35 / 46
|
||||
-- 282277027 / 11554135
|
||||
main : IO Unit
|
||||
main = do
|
||||
run "aoc2023/day5/eg.txt"
|
||||
run "aoc2023/day5/input.txt"
|
||||
@@ -1,74 +0,0 @@
|
||||
module Day6
|
||||
|
||||
import Prelude
|
||||
import Node
|
||||
import Aoc
|
||||
|
||||
Problem : U
|
||||
Problem = List (Int × Int)
|
||||
|
||||
pNums : String → Either String (List Int)
|
||||
pNums line =
|
||||
let (_ :: line :: Nil) = split line ": "
|
||||
| _ => Left "expected two parts" in
|
||||
Right $ nums line
|
||||
|
||||
parse : String → Either String Problem
|
||||
parse content = do
|
||||
let (a :: b :: Nil) = split (trim content) "\n"
|
||||
| _ => Left "expected two lines"
|
||||
times <- pNums a
|
||||
dists <- pNums b
|
||||
Right (zip times dists)
|
||||
|
||||
part1 : Problem → Int
|
||||
part1 prob = go 1 prob
|
||||
where
|
||||
run : Int -> Int -> Int → Int → Int
|
||||
run time dist t count =
|
||||
let count = if dist < t * (time - t) then count + 1 else count in
|
||||
if time == t then count
|
||||
else run time dist (t + 1) count
|
||||
|
||||
go : Int → Problem → Int
|
||||
go acc Nil = acc
|
||||
go acc ((time,dist) :: prob) = go (acc * run time dist 0 0) prob
|
||||
|
||||
part2 : Int × Int → IO Unit
|
||||
part2 (time,dist) = do
|
||||
let t = intToDouble time
|
||||
let d = intToDouble dist
|
||||
let x = sqrtDouble (t * t - intToDouble 4 * d)
|
||||
let start = (t - x) / intToDouble 2
|
||||
let stop = (t + x) / intToDouble 2
|
||||
let s = doubleToInt $ ceilDouble start
|
||||
let e = doubleToInt $ ceilDouble stop
|
||||
putStrLn $ "part2 " ++ show (e - s)
|
||||
|
||||
parse2 : String → Either String (Int × Int)
|
||||
parse2 content =
|
||||
let (a :: b :: Nil) = split (trim content) "\n"
|
||||
| _ => Left "too many parts" in
|
||||
let time = stringToInt $ pack $ filter isDigit $ unpack a
|
||||
dist = stringToInt $ pack $ filter isDigit $ unpack b
|
||||
in Right (time, dist)
|
||||
|
||||
run : String -> IO Unit
|
||||
run fn = do
|
||||
putStrLn fn
|
||||
text <- readFile fn
|
||||
let (Right prob) = parse text | Left err => putStrLn err
|
||||
putStrLn $ debugStr prob
|
||||
putStrLn $ "part1 " ++ show (part1 prob)
|
||||
let (Right prob) = parse2 text | Left err => putStrLn err
|
||||
part2 prob
|
||||
-- debugLog prob
|
||||
-- part2 prob
|
||||
|
||||
-- 288 / 71503
|
||||
-- 1413720 / 30565288
|
||||
|
||||
main : IO Unit
|
||||
main = do
|
||||
run "aoc2023/day6/eg.txt"
|
||||
run "aoc2023/day6/input.txt"
|
||||
162
aoc2023/Lib.newt
162
aoc2023/Lib.newt
@@ -1,162 +0,0 @@
|
||||
module Lib
|
||||
|
||||
-- Prelude
|
||||
data Unit : U where
|
||||
MkUnit : Unit
|
||||
|
||||
data Bool : U where
|
||||
True : Bool
|
||||
False : Bool
|
||||
|
||||
data Nat : U where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
data Maybe : U -> U where
|
||||
Just : {a : U} -> a -> Maybe a
|
||||
Nothing : {a : U} -> Maybe a
|
||||
|
||||
data Either : U -> U -> U where
|
||||
Left : {a b : U} -> a -> Either a b
|
||||
Right : {a b : U} -> b -> Either a b
|
||||
|
||||
|
||||
infixr 7 _::_
|
||||
data List : U -> U where
|
||||
Nil : {a : U} -> List a
|
||||
_::_ : {a : U} -> a -> List a -> List a
|
||||
|
||||
Cons : {a : U} -> a -> List a -> List a
|
||||
Cons x xs = x :: xs
|
||||
|
||||
-- TODO where clauses
|
||||
reverse' : {A : U} -> List A -> List A -> List A
|
||||
reverse' Nil acc = acc
|
||||
reverse' (x :: xs) acc = reverse' xs (x :: acc)
|
||||
|
||||
reverse : {A : U} -> List A -> List A
|
||||
reverse xs = reverse' xs Nil
|
||||
|
||||
length : {a : U} -> List a -> Nat
|
||||
length Nil = Z
|
||||
length (x :: xs) = S (length xs)
|
||||
|
||||
infixr 0 _,_
|
||||
|
||||
data Pair : U -> U -> U where
|
||||
_,_ : {a b : U} -> a -> b -> Pair a b
|
||||
|
||||
-- Idris says it special cases to deal with unification issues
|
||||
infixr 0 _$_
|
||||
|
||||
_$_ : {a b : U} -> (a -> b) -> a -> b
|
||||
f $ a = f a
|
||||
|
||||
-- JS Bridge
|
||||
|
||||
ptype Dummy
|
||||
|
||||
|
||||
ptype World
|
||||
data IO : U -> U where
|
||||
MkIO : {a : U} -> (World -> Pair World a) -> IO a
|
||||
|
||||
-- TODO unified Number for now
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
ptype Array : U -> U
|
||||
|
||||
pfunc arrayToList : {a : U} -> Array a -> List a := "
|
||||
(a, arr) => {
|
||||
let rval = Nil(a)
|
||||
for (let i = arr.length - 1; i >= 0; i--) {
|
||||
rval = Cons(a, arr[i], rval)
|
||||
}
|
||||
return rval
|
||||
}
|
||||
"
|
||||
|
||||
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 : {a : U} -> Array a -> Int := `(a,arr) => arr.length`
|
||||
pfunc aget : {a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
|
||||
pfunc aempty : {a : U} -> Unit -> Array a := `() => []`
|
||||
|
||||
pfunc getArgs : List String := `arrayToList(String, process.argv)`
|
||||
-- Maybe integrate promises?
|
||||
|
||||
|
||||
pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)`
|
||||
|
||||
pfunc _<_ : Int -> Int -> Bool := `(x,y) => (x < y) ? True : False`
|
||||
pfunc _<=_ : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False`
|
||||
pfunc _+_ : Int -> Int -> Int := `(x,y) => x + y`
|
||||
pfunc _-_ : Int -> Int -> Int := `(x,y) => x - y`
|
||||
pfunc _*_ : Int -> Int -> Int := `(x,y) => x * y`
|
||||
pfunc _/_ : Int -> Int -> Int := `(x,y) => x / y`
|
||||
|
||||
infix 6 _<_ _<=_
|
||||
infixl 8 _+_ _-_
|
||||
infixl 9 _*_ _/_
|
||||
|
||||
-- Ideally we'd have newt write the arrows for us to keep things correct
|
||||
-- We'd still have difficulty with callbacks...
|
||||
pfunc fs : Dummy := `require('fs')`
|
||||
pfunc readFile : (fn : String) -> String := `(fn) => fs.readFileSync(fn, 'utf8')`
|
||||
pfunc log : {a : U} -> a -> Dummy := `(a, obj) => console.log(obj)`
|
||||
|
||||
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 : String -> String -> List String := "(s, by) => {
|
||||
let parts = s.split(by)
|
||||
let rval = Nil(String)
|
||||
parts.reverse()
|
||||
parts.forEach(p => { rval = _$3A$3A_(List(String), p, rval) })
|
||||
return rval
|
||||
}"
|
||||
|
||||
pfunc slen : String -> Int := `s => s.length`
|
||||
pfunc sindex : String -> Int -> Char := `(s,i) => s[i]`
|
||||
|
||||
|
||||
infixl 7 _++_
|
||||
pfunc _++_ : String -> String -> String := `(a,b) => a + b`
|
||||
|
||||
|
||||
pfunc trace : {a : U} -> String -> a -> a := "(_, lab, a) => {
|
||||
console.log(lab,a)
|
||||
return a
|
||||
}"
|
||||
|
||||
pfunc unpack : String -> List Char
|
||||
:= "(s) => {
|
||||
let acc = Nil(Char)
|
||||
for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc)
|
||||
return acc
|
||||
}"
|
||||
|
||||
foldl : {A B : U} -> (B -> A -> B) -> B -> List A -> B
|
||||
foldl f acc Nil = acc
|
||||
foldl f acc (x :: xs) = foldl f (f acc x) xs
|
||||
|
||||
map : {A B : U} -> (A -> B) -> List A -> List B
|
||||
map f Nil = Nil
|
||||
map f (x :: xs) = f x :: map f xs
|
||||
|
||||
|
||||
infixl 9 _∘_
|
||||
_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
|
||||
(f ∘ g) x = f (g x)
|
||||
@@ -1,7 +0,0 @@
|
||||
module Node
|
||||
|
||||
import Prelude
|
||||
|
||||
pfunc fs : JSObject := `require('fs')`
|
||||
pfunc getArgs : List String := `arrayToList(String, process.argv)`
|
||||
pfunc readFile uses (MkIORes) : (fn : String) -> IO String := `(fn) => (w) => Prelude_MkIORes(require('fs').readFileSync(fn, 'utf8'), w)`
|
||||
@@ -1 +0,0 @@
|
||||
../src/Prelude.newt
|
||||
@@ -1,2 +0,0 @@
|
||||
|
||||
Attempts to port AOC2023 solutions from Lean4 to see how usable newt is.
|
||||
@@ -1,5 +0,0 @@
|
||||
1abc2
|
||||
pqr3stu8vwx
|
||||
a1b2c3d4e5f
|
||||
treb7uchet
|
||||
|
||||
@@ -1,7 +0,0 @@
|
||||
two1nine
|
||||
eightwothree
|
||||
abcone2threexyz
|
||||
xtwone3four
|
||||
4nineeightseven2
|
||||
zoneight234
|
||||
7pqrstsixteen
|
||||
File diff suppressed because it is too large
Load Diff
@@ -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
|
||||
@@ -1,10 +0,0 @@
|
||||
467..114..
|
||||
...*......
|
||||
..35..633.
|
||||
......#...
|
||||
617*......
|
||||
.....+.58.
|
||||
..592.....
|
||||
......755.
|
||||
...$.*....
|
||||
.664.598..
|
||||
@@ -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
|
||||
@@ -1,33 +0,0 @@
|
||||
seeds: 79 14 55 13
|
||||
|
||||
seed-to-soil map:
|
||||
50 98 2
|
||||
52 50 48
|
||||
|
||||
soil-to-fertilizer map:
|
||||
0 15 37
|
||||
37 52 2
|
||||
39 0 15
|
||||
|
||||
fertilizer-to-water map:
|
||||
49 53 8
|
||||
0 11 42
|
||||
42 0 7
|
||||
57 7 4
|
||||
|
||||
water-to-light map:
|
||||
88 18 7
|
||||
18 25 70
|
||||
|
||||
light-to-temperature map:
|
||||
45 77 23
|
||||
81 45 19
|
||||
68 64 13
|
||||
|
||||
temperature-to-humidity map:
|
||||
0 69 1
|
||||
1 0 69
|
||||
|
||||
humidity-to-location map:
|
||||
60 56 37
|
||||
56 93 4
|
||||
@@ -1,2 +0,0 @@
|
||||
Time: 7 15 30
|
||||
Distance: 9 40 200
|
||||
@@ -1 +0,0 @@
|
||||
../aoc2023/Node.newt
|
||||
7
aoc2024/Node.newt
Normal file
7
aoc2024/Node.newt
Normal file
@@ -0,0 +1,7 @@
|
||||
module Node
|
||||
|
||||
import Prelude
|
||||
|
||||
pfunc fs : JSObject := `require('fs')`
|
||||
pfunc getArgs : List String := `arrayToList(String, process.argv)`
|
||||
pfunc readFile uses (MkIORes) : (fn : String) -> IO String := `(fn) => (w) => Prelude_MkIORes(require('fs').readFileSync(fn, 'utf8'), w)`
|
||||
@@ -1 +0,0 @@
|
||||
../newt/SortedMap.newt
|
||||
203
aoc2024/SortedMap.newt
Normal file
203
aoc2024/SortedMap.newt
Normal file
@@ -0,0 +1,203 @@
|
||||
module SortedMap
|
||||
|
||||
import Prelude
|
||||
|
||||
-- TODO We'll want to replace Ord/Eq with (a → Ordering) (and rewrite most of our aoc solutions...)
|
||||
-- data Ordering : U where
|
||||
-- LT EQ GT : Ordering
|
||||
|
||||
data T23 : Nat -> U -> U -> U where
|
||||
Leaf : ∀ k v. k -> v -> T23 Z k v
|
||||
Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v
|
||||
Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v
|
||||
|
||||
lookupT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> T23 h k v -> Maybe (k × v)
|
||||
lookupT23 key (Leaf k v)= if k == key then Just (k,v) else Nothing
|
||||
lookupT23 key (Node2 t1 k1 t2) =
|
||||
if key <= k1 then lookupT23 key t1 else lookupT23 key t2
|
||||
lookupT23 key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1 then lookupT23 key t1
|
||||
else if key <= k2 then lookupT23 key t2
|
||||
else lookupT23 key t3
|
||||
|
||||
insertT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
|
||||
insertT23 key value (Leaf k v) =
|
||||
if key == k then Left (Leaf key value)
|
||||
else if key <= k then Right (Leaf key value, key, Leaf k v)
|
||||
else Right (Leaf k v, k, Leaf key value)
|
||||
insertT23 key value (Node2 t1 k1 t2) =
|
||||
if key <= k1 then
|
||||
case insertT23 key value t1 of
|
||||
Left t1' => Left (Node2 t1' k1 t2)
|
||||
Right (a,b,c) => Left (Node3 a b c k1 t2)
|
||||
else case insertT23 key value t2 of
|
||||
Left t2' => Left (Node2 t1 k1 t2')
|
||||
Right (a,b,c) => Left (Node3 t1 k1 a b c)
|
||||
insertT23 key value (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1 then
|
||||
case insertT23 key value t1 of
|
||||
Left t1' => Left (Node3 t1' k1 t2 k2 t3)
|
||||
Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
|
||||
else if key <= k2 then
|
||||
case insertT23 key value t2 of
|
||||
Left t2' => Left (Node3 t1 k1 t2' k2 t3)
|
||||
Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
|
||||
else
|
||||
case insertT23 key value t3 of
|
||||
Left t3' => Left (Node3 t1 k1 t2 k2 t3')
|
||||
Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
|
||||
|
||||
-- This is cribbed from Idris. Deleting nodes takes a bit of code.
|
||||
Hole : Nat → U → U → U
|
||||
Hole Z k v = Unit
|
||||
Hole (S n) k v = T23 n k v
|
||||
|
||||
Node4 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
Node4 t1 k1 t2 k2 t3 k3 t4 = Node2 (Node2 t1 k1 t2) k2 (Node2 t3 k3 t4)
|
||||
|
||||
Node5 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
Node5 a b c d e f g h i = Node2 (Node2 a b c) d (Node3 e f g h i)
|
||||
|
||||
Node6 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
Node6 a b c d e f g h i j k = Node2 (Node3 a b c d e) f (Node3 g h i j k)
|
||||
|
||||
Node7 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
Node7 a b c d e f g h i j k l m = Node3 (Node3 a b c d e) f (Node2 g h i) j (Node2 k l m)
|
||||
|
||||
merge1 : ∀ k v h. T23 h k v → k → T23 (S h) k v → k → T23 (S h) k v → T23 (S (S h)) k v
|
||||
merge1 a b (Node2 c d e) f (Node2 g h i) = Node5 a b c d e f g h i
|
||||
merge1 a b (Node2 c d e) f (Node3 g h i j k) = Node6 a b c d e f g h i j k
|
||||
merge1 a b (Node3 c d e f g) h (Node2 i j k) = Node6 a b c d e f g h i j k
|
||||
merge1 a b (Node3 c d e f g) h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
|
||||
|
||||
merge2 : ∀ k v h. T23 (S h) k v → k → T23 h k v → k → T23 (S h) k v → T23 (S (S h)) k v
|
||||
merge2 (Node2 a b c) d e f (Node2 g h i) = Node5 a b c d e f g h i
|
||||
merge2 (Node2 a b c) d e f (Node3 g h i j k) = Node6 a b c d e f g h i j k
|
||||
merge2 (Node3 a b c d e) f g h (Node2 i j k) = Node6 a b c d e f g h i j k
|
||||
merge2 (Node3 a b c d e) f g h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
|
||||
|
||||
merge3 : ∀ k v h. T23 (S h) k v → k → T23 (S h) k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
merge3 (Node2 a b c) d (Node2 e f g) h i = Node5 a b c d e f g h i
|
||||
merge3 (Node2 a b c) d (Node3 e f g h i) j k = Node6 a b c d e f g h i j k
|
||||
merge3 (Node3 a b c d e) f (Node2 g h i) j k = Node6 a b c d e f g h i j k
|
||||
merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l m
|
||||
|
||||
-- height is erased in the data everywhere but the top, but needed for case
|
||||
-- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this
|
||||
deleteT23 : ∀ k v. {{Ord k}} {{Eq k}} → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
|
||||
deleteT23 Z key (Leaf k v) = if k == key then Right MkUnit else Left (Leaf k v)
|
||||
deleteT23 (S Z) key (Node2 t1 k1 t2) =
|
||||
if key <= k1
|
||||
then case deleteT23 Z key t1 of
|
||||
Left t1 => Left (Node2 t1 k1 t2)
|
||||
Right _ => Right t2
|
||||
else case deleteT23 Z key t2 of
|
||||
Left t2 => Left (Node2 t1 k1 t2)
|
||||
Right MkUnit => Right t1
|
||||
deleteT23 (S Z) key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1
|
||||
then case deleteT23 _ key t1 of
|
||||
Left t1 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right MkUnit => Left (Node2 t2 k2 t3)
|
||||
else if key <= k2 then case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right _ => Left (Node2 t1 k1 t3)
|
||||
else case deleteT23 _ key t3 of
|
||||
Left t3 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right _ => Left (Node2 t1 k1 t2)
|
||||
deleteT23 (S (S h)) key (Node2 t1 k1 t2) =
|
||||
if key <= k1
|
||||
then case deleteT23 (S h) key t1 of
|
||||
Left t1 => Left (Node2 t1 k1 t2)
|
||||
Right t1 => case t2 of
|
||||
Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
|
||||
Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
|
||||
else case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node2 t1 k1 t2)
|
||||
Right t2 => case t1 of
|
||||
Node2 a b c => Right (Node3 a b c k1 t2)
|
||||
Node3 a b c d e => Left (Node4 a b c d e k1 t2)
|
||||
deleteT23 (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1
|
||||
then case deleteT23 _ key t1 of
|
||||
Left t1 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t1 => Left (merge1 t1 k1 t2 k2 t3)
|
||||
else if key <= k2 then case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t2 => Left (merge2 t1 k1 t2 k2 t3)
|
||||
else case deleteT23 _ key t3 of
|
||||
Left t3 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t3 => Left (merge3 t1 k1 t2 k2 t3)
|
||||
|
||||
treeLeft : ∀ h k v. T23 h k v → (k × v)
|
||||
treeLeft (Leaf k v) = (k, v)
|
||||
treeLeft (Node2 t1 _ _) = treeLeft t1
|
||||
treeLeft (Node3 t1 _ _ _ _) = treeLeft t1
|
||||
|
||||
treeRight : ∀ h k v. T23 h k v → (k × v)
|
||||
treeRight (Leaf k v) = (k, v)
|
||||
treeRight (Node2 _ _ t2) = treeRight t2
|
||||
treeRight (Node3 _ _ _ _ t3) = treeRight t3
|
||||
|
||||
|
||||
data SortedMap : U -> U -> U where
|
||||
EmptyMap : ∀ k v. SortedMap k v
|
||||
-- not erased so we know what happens in delete
|
||||
MapOf : ∀ k v. {h : Nat} → T23 h k v -> SortedMap k v
|
||||
|
||||
deleteMap : ∀ k v. {{Ord k}} {{Eq k}} → k → SortedMap k v → SortedMap k v
|
||||
deleteMap key EmptyMap = EmptyMap
|
||||
-- REVIEW if I split h separately in a nested case, it doesn't sort out Hole
|
||||
deleteMap key (MapOf {k} {v} {Z} tree) = case deleteT23 Z key tree of
|
||||
Left t => MapOf t
|
||||
Right t => EmptyMap
|
||||
deleteMap key (MapOf {k} {v} {S n} tree) = case deleteT23 (S n) key tree of
|
||||
Left t => MapOf t
|
||||
Right t => MapOf t
|
||||
|
||||
leftMost : ∀ k v. SortedMap k v → Maybe (k × v)
|
||||
leftMost EmptyMap = Nothing
|
||||
leftMost (MapOf m) = Just (treeLeft m)
|
||||
|
||||
rightMost : ∀ k v. SortedMap k v → Maybe (k × v)
|
||||
rightMost EmptyMap = Nothing
|
||||
rightMost (MapOf m) = Just (treeRight m)
|
||||
|
||||
-- TODO issue with metas and case if written as `do` block
|
||||
pop : ∀ k v. {{Eq k}} {{Ord k}} → SortedMap k v → Maybe ((k × v) × SortedMap k v)
|
||||
pop m = case leftMost m of
|
||||
Just (k,v) => Just ((k,v), deleteMap k m)
|
||||
Nothing => Nothing
|
||||
|
||||
lookupMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe (k × v)
|
||||
lookupMap k EmptyMap = Nothing
|
||||
lookupMap k (MapOf map) = lookupT23 k map
|
||||
|
||||
lookupMap' : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe v
|
||||
lookupMap' k EmptyMap = Nothing
|
||||
lookupMap' k (MapOf map) = snd <$> lookupT23 k map
|
||||
|
||||
|
||||
updateMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> v -> SortedMap k v -> SortedMap k v
|
||||
updateMap k v EmptyMap = MapOf $ Leaf k v
|
||||
updateMap k v (MapOf map) = case insertT23 k v map of
|
||||
Left map' => MapOf map'
|
||||
Right (a, b, c) => MapOf (Node2 a b c)
|
||||
|
||||
toList : ∀ k v. SortedMap k v → List (k × v)
|
||||
toList {k} {v} (MapOf smap) = reverse $ go smap Nil
|
||||
where
|
||||
go : ∀ h. T23 h k v → List (k × v) → List (k × v)
|
||||
go (Leaf k v) acc = (k, v) :: acc
|
||||
go (Node2 t1 k1 t2) acc = go t2 (go t1 acc)
|
||||
go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
|
||||
toList _ = Nil
|
||||
|
||||
foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b
|
||||
foldMap f m Nil = m
|
||||
foldMap f m ((a,b) :: xs) = case lookupMap a m of
|
||||
Nothing => foldMap f (updateMap a b m) xs
|
||||
Just (_, b') => foldMap f (updateMap a (f b' b) m) xs
|
||||
|
||||
listValues : ∀ k v. SortedMap k v → List v
|
||||
listValues sm = map snd $ toList sm
|
||||
@@ -1,203 +0,0 @@
|
||||
module SortedMap
|
||||
|
||||
import Prelude
|
||||
|
||||
-- TODO We'll want to replace Ord/Eq with (a → Ordering) (and rewrite most of our aoc solutions...)
|
||||
-- data Ordering : U where
|
||||
-- LT EQ GT : Ordering
|
||||
|
||||
data T23 : Nat -> U -> U -> U where
|
||||
Leaf : ∀ k v. k -> v -> T23 Z k v
|
||||
Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v
|
||||
Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v
|
||||
|
||||
lookupT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> T23 h k v -> Maybe (k × v)
|
||||
lookupT23 key (Leaf k v)= if k == key then Just (k,v) else Nothing
|
||||
lookupT23 key (Node2 t1 k1 t2) =
|
||||
if key <= k1 then lookupT23 key t1 else lookupT23 key t2
|
||||
lookupT23 key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1 then lookupT23 key t1
|
||||
else if key <= k2 then lookupT23 key t2
|
||||
else lookupT23 key t3
|
||||
|
||||
insertT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
|
||||
insertT23 key value (Leaf k v) =
|
||||
if key == k then Left (Leaf key value)
|
||||
else if key <= k then Right (Leaf key value, key, Leaf k v)
|
||||
else Right (Leaf k v, k, Leaf key value)
|
||||
insertT23 key value (Node2 t1 k1 t2) =
|
||||
if key <= k1 then
|
||||
case insertT23 key value t1 of
|
||||
Left t1' => Left (Node2 t1' k1 t2)
|
||||
Right (a,b,c) => Left (Node3 a b c k1 t2)
|
||||
else case insertT23 key value t2 of
|
||||
Left t2' => Left (Node2 t1 k1 t2')
|
||||
Right (a,b,c) => Left (Node3 t1 k1 a b c)
|
||||
insertT23 key value (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1 then
|
||||
case insertT23 key value t1 of
|
||||
Left t1' => Left (Node3 t1' k1 t2 k2 t3)
|
||||
Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
|
||||
else if key <= k2 then
|
||||
case insertT23 key value t2 of
|
||||
Left t2' => Left (Node3 t1 k1 t2' k2 t3)
|
||||
Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
|
||||
else
|
||||
case insertT23 key value t3 of
|
||||
Left t3' => Left (Node3 t1 k1 t2 k2 t3')
|
||||
Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
|
||||
|
||||
-- This is cribbed from Idris. Deleting nodes takes a bit of code.
|
||||
Hole : Nat → U → U → U
|
||||
Hole Z k v = Unit
|
||||
Hole (S n) k v = T23 n k v
|
||||
|
||||
Node4 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
Node4 t1 k1 t2 k2 t3 k3 t4 = Node2 (Node2 t1 k1 t2) k2 (Node2 t3 k3 t4)
|
||||
|
||||
Node5 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
Node5 a b c d e f g h i = Node2 (Node2 a b c) d (Node3 e f g h i)
|
||||
|
||||
Node6 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
Node6 a b c d e f g h i j k = Node2 (Node3 a b c d e) f (Node3 g h i j k)
|
||||
|
||||
Node7 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
Node7 a b c d e f g h i j k l m = Node3 (Node3 a b c d e) f (Node2 g h i) j (Node2 k l m)
|
||||
|
||||
merge1 : ∀ k v h. T23 h k v → k → T23 (S h) k v → k → T23 (S h) k v → T23 (S (S h)) k v
|
||||
merge1 a b (Node2 c d e) f (Node2 g h i) = Node5 a b c d e f g h i
|
||||
merge1 a b (Node2 c d e) f (Node3 g h i j k) = Node6 a b c d e f g h i j k
|
||||
merge1 a b (Node3 c d e f g) h (Node2 i j k) = Node6 a b c d e f g h i j k
|
||||
merge1 a b (Node3 c d e f g) h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
|
||||
|
||||
merge2 : ∀ k v h. T23 (S h) k v → k → T23 h k v → k → T23 (S h) k v → T23 (S (S h)) k v
|
||||
merge2 (Node2 a b c) d e f (Node2 g h i) = Node5 a b c d e f g h i
|
||||
merge2 (Node2 a b c) d e f (Node3 g h i j k) = Node6 a b c d e f g h i j k
|
||||
merge2 (Node3 a b c d e) f g h (Node2 i j k) = Node6 a b c d e f g h i j k
|
||||
merge2 (Node3 a b c d e) f g h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
|
||||
|
||||
merge3 : ∀ k v h. T23 (S h) k v → k → T23 (S h) k v → k → T23 h k v → T23 (S (S h)) k v
|
||||
merge3 (Node2 a b c) d (Node2 e f g) h i = Node5 a b c d e f g h i
|
||||
merge3 (Node2 a b c) d (Node3 e f g h i) j k = Node6 a b c d e f g h i j k
|
||||
merge3 (Node3 a b c d e) f (Node2 g h i) j k = Node6 a b c d e f g h i j k
|
||||
merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l m
|
||||
|
||||
-- height is erased in the data everywhere but the top, but needed for case
|
||||
-- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this
|
||||
deleteT23 : ∀ k v. {{Ord k}} {{Eq k}} → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
|
||||
deleteT23 Z key (Leaf k v) = if k == key then Right MkUnit else Left (Leaf k v)
|
||||
deleteT23 (S Z) key (Node2 t1 k1 t2) =
|
||||
if key <= k1
|
||||
then case deleteT23 Z key t1 of
|
||||
Left t1 => Left (Node2 t1 k1 t2)
|
||||
Right _ => Right t2
|
||||
else case deleteT23 Z key t2 of
|
||||
Left t2 => Left (Node2 t1 k1 t2)
|
||||
Right MkUnit => Right t1
|
||||
deleteT23 (S Z) key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1
|
||||
then case deleteT23 _ key t1 of
|
||||
Left t1 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right MkUnit => Left (Node2 t2 k2 t3)
|
||||
else if key <= k2 then case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right _ => Left (Node2 t1 k1 t3)
|
||||
else case deleteT23 _ key t3 of
|
||||
Left t3 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right _ => Left (Node2 t1 k1 t2)
|
||||
deleteT23 (S (S h)) key (Node2 t1 k1 t2) =
|
||||
if key <= k1
|
||||
then case deleteT23 (S h) key t1 of
|
||||
Left t1 => Left (Node2 t1 k1 t2)
|
||||
Right t1 => case t2 of
|
||||
Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
|
||||
Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
|
||||
else case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node2 t1 k1 t2)
|
||||
Right t2 => case t1 of
|
||||
Node2 a b c => Right (Node3 a b c k1 t2)
|
||||
Node3 a b c d e => Left (Node4 a b c d e k1 t2)
|
||||
deleteT23 (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
|
||||
if key <= k1
|
||||
then case deleteT23 _ key t1 of
|
||||
Left t1 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t1 => Left (merge1 t1 k1 t2 k2 t3)
|
||||
else if key <= k2 then case deleteT23 _ key t2 of
|
||||
Left t2 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t2 => Left (merge2 t1 k1 t2 k2 t3)
|
||||
else case deleteT23 _ key t3 of
|
||||
Left t3 => Left (Node3 t1 k1 t2 k2 t3)
|
||||
Right t3 => Left (merge3 t1 k1 t2 k2 t3)
|
||||
|
||||
treeLeft : ∀ h k v. T23 h k v → (k × v)
|
||||
treeLeft (Leaf k v) = (k, v)
|
||||
treeLeft (Node2 t1 _ _) = treeLeft t1
|
||||
treeLeft (Node3 t1 _ _ _ _) = treeLeft t1
|
||||
|
||||
treeRight : ∀ h k v. T23 h k v → (k × v)
|
||||
treeRight (Leaf k v) = (k, v)
|
||||
treeRight (Node2 _ _ t2) = treeRight t2
|
||||
treeRight (Node3 _ _ _ _ t3) = treeRight t3
|
||||
|
||||
|
||||
data SortedMap : U -> U -> U where
|
||||
EmptyMap : ∀ k v. SortedMap k v
|
||||
-- not erased so we know what happens in delete
|
||||
MapOf : ∀ k v. {h : Nat} → T23 h k v -> SortedMap k v
|
||||
|
||||
deleteMap : ∀ k v. {{Ord k}} {{Eq k}} → k → SortedMap k v → SortedMap k v
|
||||
deleteMap key EmptyMap = EmptyMap
|
||||
-- REVIEW if I split h separately in a nested case, it doesn't sort out Hole
|
||||
deleteMap key (MapOf {k} {v} {Z} tree) = case deleteT23 Z key tree of
|
||||
Left t => MapOf t
|
||||
Right t => EmptyMap
|
||||
deleteMap key (MapOf {k} {v} {S n} tree) = case deleteT23 (S n) key tree of
|
||||
Left t => MapOf t
|
||||
Right t => MapOf t
|
||||
|
||||
leftMost : ∀ k v. SortedMap k v → Maybe (k × v)
|
||||
leftMost EmptyMap = Nothing
|
||||
leftMost (MapOf m) = Just (treeLeft m)
|
||||
|
||||
rightMost : ∀ k v. SortedMap k v → Maybe (k × v)
|
||||
rightMost EmptyMap = Nothing
|
||||
rightMost (MapOf m) = Just (treeRight m)
|
||||
|
||||
-- TODO issue with metas and case if written as `do` block
|
||||
pop : ∀ k v. {{Eq k}} {{Ord k}} → SortedMap k v → Maybe ((k × v) × SortedMap k v)
|
||||
pop m = case leftMost m of
|
||||
Just (k,v) => Just ((k,v), deleteMap k m)
|
||||
Nothing => Nothing
|
||||
|
||||
lookupMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe (k × v)
|
||||
lookupMap k EmptyMap = Nothing
|
||||
lookupMap k (MapOf map) = lookupT23 k map
|
||||
|
||||
lookupMap' : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe v
|
||||
lookupMap' k EmptyMap = Nothing
|
||||
lookupMap' k (MapOf map) = snd <$> lookupT23 k map
|
||||
|
||||
|
||||
updateMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> v -> SortedMap k v -> SortedMap k v
|
||||
updateMap k v EmptyMap = MapOf $ Leaf k v
|
||||
updateMap k v (MapOf map) = case insertT23 k v map of
|
||||
Left map' => MapOf map'
|
||||
Right (a, b, c) => MapOf (Node2 a b c)
|
||||
|
||||
toList : ∀ k v. SortedMap k v → List (k × v)
|
||||
toList {k} {v} (MapOf smap) = reverse $ go smap Nil
|
||||
where
|
||||
go : ∀ h. T23 h k v → List (k × v) → List (k × v)
|
||||
go (Leaf k v) acc = (k, v) :: acc
|
||||
go (Node2 t1 k1 t2) acc = go t2 (go t1 acc)
|
||||
go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
|
||||
toList _ = Nil
|
||||
|
||||
foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b
|
||||
foldMap f m Nil = m
|
||||
foldMap f m ((a,b) :: xs) = case lookupMap a m of
|
||||
Nothing => foldMap f (updateMap a b m) xs
|
||||
Just (_, b') => foldMap f (updateMap a (f b' b) m) xs
|
||||
|
||||
listValues : ∀ k v. SortedMap k v → List v
|
||||
listValues sm = map snd $ toList sm
|
||||
10
pack.toml
10
pack.toml
@@ -1,10 +0,0 @@
|
||||
[custom.all.newt]
|
||||
type = "local"
|
||||
path = "."
|
||||
ipkg = "newt.ipkg"
|
||||
test = "test/test.ipkg"
|
||||
|
||||
[custom.all.newt-test]
|
||||
type = "local"
|
||||
path = "test"
|
||||
ipkg = "test.ipkg"
|
||||
@@ -87,8 +87,6 @@ any : ∀ a. (a → Bool) → List a → Bool
|
||||
any f Nil = False
|
||||
any f (x :: xs) = if f x then True else any f xs
|
||||
|
||||
-- NOW so we stuff quant and the args in here and sort it out later?
|
||||
|
||||
-- apply an expression at an arity to a list of args
|
||||
-- CAppRef will specify any missing args, for eta conversion later
|
||||
-- and any extra args get individual CApp.
|
||||
|
||||
Reference in New Issue
Block a user