diff --git a/aoc2024/Day13.newt b/aoc2024/Day13.newt new file mode 100644 index 0000000..0702ade --- /dev/null +++ b/aoc2024/Day13.newt @@ -0,0 +1,102 @@ +module Day13 + +import Prelude +import Node +import Aoc +import Parser + + +Point : U +Point = Int × Int + +instance Add Point where + (a,b) + (c,d) = (a + c, b + d) + +instance Sub Point where + (a,b) - (c,d) = (a - c, b - d) + +instance Ord Point where + (a,b) < (c,d) = a < c || a == c && b < d + +instance Eq Point where + (a,b) == (c,d) = a == c && b == d + + +token : String → Parser Unit +token str = string str >> ws + + +data Machine : U where + MkMachine : Point → Point → Point → Machine + +-- need Either parser.. +parseButton : Parser Point +parseButton = do + token "Button" + any + token ":" + token "X+" + x <- number + token "," + token "Y+" + y <- number + match '\n' + pure (x,y) + +parsePrize : Parser Point +parsePrize = do + token "Prize:" + token "X=" + x <- number + token "," + token "Y=" + y <- number + match '\n' + pure (x,y) + +pMachine : Parser Machine +pMachine = MkMachine <$> parseButton <*> parseButton <*> parsePrize <* many (match '\n') + +-- TODO should be a proper primitive, so we can have literals (also need Double) +ptype BigInt +pfunc itobi : Int → BigInt := `(x) => BigInt(x)` +pfunc addbi : BigInt → BigInt → BigInt := `(a,b) => a + b` +pfunc subbi : BigInt → BigInt → BigInt := `(a,b) => a - b` +pfunc mulbi : BigInt → BigInt → BigInt := `(a,b) => a * b` +pfunc divbi : BigInt → BigInt → BigInt := `(a,b) => a / b` + +instance Mul BigInt where a * b = mulbi a b +instance Div BigInt where a / b = divbi a b +instance Add BigInt where a + b = addbi a b +instance Sub BigInt where a - b = subbi a b +instance Cast Int BigInt where cast x = itobi x +instance Eq BigInt where a == b = jsEq a b +instance Show BigInt where show = jsShow +instance Ord BigInt where a < b = jsLT a b + +calcCost : BigInt → Machine → Maybe BigInt +calcCost extra (MkMachine (ax, ay) (bx, by) (px, py)) = + let px = itobi px + extra + py = itobi py + extra + b = (px * itobi ay - py * itobi ax) / (itobi ay * itobi bx - itobi by * itobi ax) + a = (px - itobi bx * b) / itobi ax + in if a * itobi ax + b * itobi bx == px && a * itobi ay + b * itobi by == py + then Just (a * itobi 3 + b) else Nothing + +run : String -> IO Unit +run fn = do + putStrLn fn + text <- readFile fn + let (Right (machines,_)) = some pMachine $ unpack text | _ => putStrLn "Parse Error" + + let extra = itobi 0 + let p1 = foldl _+_ (itobi 0) $ mapMaybe (calcCost extra) machines + putStrLn $ "part1 " ++ show p1 + let extra = itobi 10000000 * itobi 1000000 + let p2 = foldl _+_ (itobi 0) $ mapMaybe (calcCost extra) machines + putStrLn $ "part2 " ++ show p2 + +main : IO Unit +main = do + run "aoc2024/day13/eg.txt" + run "aoc2024/day13/input.txt" diff --git a/aoc2024/Parser.newt b/aoc2024/Parser.newt new file mode 100644 index 0000000..8b73092 --- /dev/null +++ b/aoc2024/Parser.newt @@ -0,0 +1,69 @@ +module Parser + +import Prelude +import Aoc + +Parser : U → U +Parser a = List Char → Either String (a × List Char) + +instance Monad Parser where + pure a = \ cs => Right (a, cs) + bind ma mab = \ cs => ma cs >>= uncurry mab + +instance Alternative Parser where + pa <|> pb = \ cs => case pa cs of + Left msg => pb cs + res => res + +instance Functor Parser where + map f pa = \ cs => case pa cs of + Left msg => Left msg + Right (a, cs) => Right (f a, cs) + +instance Applicative Parser where + return a = pure a + pa <*> pb = pa >>= (\ f => map f pb) + + +fail : ∀ a. String -> Parser a +fail msg = \ cs => Left msg + +-- TODO, case builder isn't expanding Parser Unit to count lambdas +eof : Parser Unit +eof = \ cs => case cs of + Nil => Right (MkUnit, Nil) + _ => Left "expected eof" + +satisfy : (Char → Bool) → Parser Char +satisfy pred = λ cs => case cs of + Nil => Left "unexpected EOF" + (c :: cs) => if pred c then Right (c, cs) else Left ("did not expect " ++ show c) + +match : Char → Parser Char +match d = satisfy (_==_ d) + +any : Parser Char +any = satisfy (λ _ => True) + +some many : ∀ a. Parser a → Parser (List a) +many p = some p <|> pure Nil +some p = do + v <- p + vs <- many p + pure (v :: vs) + +string : String → Parser Unit +string str = go (unpack str) + where + go : List Char → Parser Unit + go Nil = pure MkUnit + go (c :: cs) = match c >> go cs + +number : Parser Int +number = stringToInt ∘ pack <$> some (satisfy isDigit) + -- do + -- digs <- some (satisfy isDigit) + -- pure $ stringToInt $ pack digs + +ws : Parser Unit +ws = many (match ' ') >> pure MkUnit diff --git a/aoc2024/day13/eg.txt b/aoc2024/day13/eg.txt new file mode 100644 index 0000000..912f482 --- /dev/null +++ b/aoc2024/day13/eg.txt @@ -0,0 +1,15 @@ +Button A: X+94, Y+34 +Button B: X+22, Y+67 +Prize: X=8400, Y=5400 + +Button A: X+26, Y+66 +Button B: X+67, Y+21 +Prize: X=12748, Y=12176 + +Button A: X+17, Y+86 +Button B: X+84, Y+37 +Prize: X=7870, Y=6450 + +Button A: X+69, Y+23 +Button B: X+27, Y+71 +Prize: X=18641, Y=10279 diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 2427780..9425e05 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -158,12 +158,18 @@ instance Functor SnocList where map f (xs :< x) = map f xs :< f x -- TODO this probably should depend on / entail Functor -infixl 3 _<*>_ +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 +const : ∀ a b. a → b → a +const a b = a + +_<*_ : ∀ f a b. {{Applicative f}} → f a → f b → f a +fa <* fb = return const <*> fa <*> fb + class Traversable (t : U → U) where traverse : ∀ f a b. {{Applicative f}} → (a → f b) → t a → f (t b) @@ -236,7 +242,7 @@ instance Concat String where 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` - +pfunc jsShow : ∀ a . a → String := `(_,a) => ''+a` instance Eq Int where a == b = jsEq a b @@ -246,6 +252,7 @@ instance Eq String where instance Eq Char where a == b = jsEq a b + data Unit : U where MkUnit : Unit @@ -401,6 +408,7 @@ pfunc pack : List Char → String := `(cs) => { pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => { const go = (obj) => { if (obj === undefined) return "_" + if (typeof obj == 'bigint') return ''+obj if (obj.tag === '_,_') { let rval = '(' while (obj?.tag === '_,_') { @@ -729,3 +737,6 @@ instance Ord String where instance Cast Int Nat where cast n = intToNat n + +instance Show Char where + show c = jsShow c diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 1a6b722..39d5693 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -175,7 +175,7 @@ keywords : List String keywords = [ "var", "true", "false", "let", "case", "switch", "if", "then", "else", "String", "function", "void", "undefined", "null", "await", "async", "return", "const", - "Number", "default", "for", "while", "Function", "Array" + "Number", "default", "for", "while", "Function", "Array", "BigInt" ] ||| escape identifiers for js