commit f40862fc1e9b7f587db63b11b2651dc15e01e8f2 Author: Kiana Sheibani Date: Mon Dec 2 06:06:11 2024 -0500 feat: part 1-1 diff --git a/.envrc b/.envrc new file mode 100644 index 0000000..b9238c3 --- /dev/null +++ b/.envrc @@ -0,0 +1,3 @@ +#!/usr/bin/env bash + +use flake diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..8b7a5e0 --- /dev/null +++ b/.gitignore @@ -0,0 +1,7 @@ +*.ibc +*.o + +.direnv/ + +build/ +*.*~ diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..712386e --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2024 Kiana Sheibani + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg new file mode 100644 index 0000000..37257e6 --- /dev/null +++ b/advent-of-code-2024.ipkg @@ -0,0 +1,18 @@ +package advent-of-code-2024 +version = 0.0 + +brief = "Advent of Code 2024" + +authors = "Kiana Sheibani" +license = "MIT" + +sourcedir = "src" + +langversion >= 0.6.0 + +executable = advent-of-code-2024 +main = Main +modules = Main, Utils, AllDays, + Data.Problem, + Day1.Part1 + diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..ce5e263 --- /dev/null +++ b/flake.lock @@ -0,0 +1,98 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1731533236, + "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "idris": { + "inputs": { + "flake-utils": [ + "flake-utils" + ], + "idris-emacs-src": "idris-emacs-src", + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1733093802, + "narHash": "sha256-bUjIOLocDumq6XdJ5mAuS4t3SMht9JKVYZ88BSQSiGs=", + "owner": "idris-lang", + "repo": "Idris2", + "rev": "d176ab4108a42cd8423466a0e2450e17cc693b7c", + "type": "github" + }, + "original": { + "owner": "idris-lang", + "repo": "Idris2", + "type": "github" + } + }, + "idris-emacs-src": { + "flake": false, + "locked": { + "lastModified": 1666078909, + "narHash": "sha256-oYNHFIpcrFfPb4sXJwEBFKeH+PB4AGCrAFrfBrSTCeo=", + "owner": "redfish64", + "repo": "idris2-mode", + "rev": "3bcb52a65c488f31c99d20f235f6050418a84c9d", + "type": "github" + }, + "original": { + "owner": "redfish64", + "repo": "idris2-mode", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1719371271, + "narHash": "sha256-G3tm/ttP6PxnrrpCYIi4VBpJdGrwqr2pqRKuZlvTg2s=", + "owner": "NixOS", + "repo": "nixpkgs", + "rev": "267d115a04e93a3487d3c2c26e3af5704a0144cc", + "type": "github" + }, + "original": { + "owner": "NixOS", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "idris": "idris" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..f25ee8f --- /dev/null +++ b/flake.nix @@ -0,0 +1,30 @@ +{ + description = "Advent of Code 2024 in Idris2"; + + inputs.flake-utils.url = "github:numtide/flake-utils"; + inputs.idris = { + url = "github:idris-lang/Idris2"; + inputs.flake-utils.follows = "flake-utils"; + }; + + outputs = { self, idris, flake-utils }: + flake-utils.lib.eachDefaultSystem (system: + let + npkgs = import idris.inputs.nixpkgs { inherit system; }; + idrisPkgs = idris.packages.${system}; + buildIdris = idris.buildIdris.${system}; + pkgs = buildIdris { + ipkgName = "advent-of-code-2024"; + src = ./.; + idrisLibraries = []; + }; + in { + packages.default = pkgs.executable; + devShell = npkgs.mkShell { + buildInputs = [ idrisPkgs.idris2 npkgs.rlwrap ]; + shellHook = '' + alias idris2="rlwrap -s 1000 idris2 --no-banner" + ''; + }; + }); +} diff --git a/src/AllDays.idr b/src/AllDays.idr new file mode 100644 index 0000000..01e67ea --- /dev/null +++ b/src/AllDays.idr @@ -0,0 +1,3 @@ +module AllDays + +import public Day1.Part1 diff --git a/src/Data/Problem.idr b/src/Data/Problem.idr new file mode 100644 index 0000000..f1a70d0 --- /dev/null +++ b/src/Data/Problem.idr @@ -0,0 +1,88 @@ +module Data.Problem + +import Data.List1 +import Data.String +import Data.Maybe +import Data.SortedMap +import Language.Reflection + +%language ElabReflection +%default total + + +public export +data Part = Part1 | Part2 + +public export +Eq Part where + Part1 == Part1 = True + Part1 == Part2 = False + Part2 == Part2 = True + Part2 == Part1 = False + +public export +Ord Part where + compare Part1 Part1 = EQ + compare Part1 Part2 = LT + compare Part2 Part2 = EQ + compare Part2 Part1 = GT + +public export +record Problem where + constructor Pr + day : Nat + part : Part + +public export +Eq Problem where + Pr d1 p1 == Pr d2 p2 = d1 == d2 && p1 == p2 + +public export +Ord Problem where + compare (Pr d1 p1) (Pr d2 p2) = compare d1 d2 <+> compare p1 p2 + + +public export +partNat : Part -> Nat +partNat Part1 = 1 +partNat Part2 = 2 + +public export +parsePart : String -> Maybe Part +parsePart "1" = Just Part1 +parsePart "2" = Just Part2 +parsePart _ = Nothing + +public export +parseProblem : String -> Maybe Problem +parseProblem str = + let (day ::: [part]) = split (=='-') str + | _ => Nothing + dayInt = parseInteger day + dayNat = cast <$> filter (> 0) dayInt + in Pr <$> dayNat <*> parsePart part + + +||| Generate a list of all problems given the latest problem solved. +public export +allProblems : (latest : Problem) -> List Problem +allProblems (Pr day' part') = do + day <- [1..day'] + part <- filter (<= part') [Part1, Part2] + pure $ Pr day part + +--- REFLECTION + +public export +fetchSolution : Problem -> Elab (String -> String) +fetchSolution (Pr day part) = do + let name = + NS (MkNS ["Part" ++ show (partNat part), + "Day" ++ show day]) `{solution} + check `(\s => show (~(IVar EmptyFC name) s)) + <|> fail "\{show name} does not exist as a valid solution" + +public export +fetchAllSols : (latest : Problem) -> Elab (SortedMap Problem (String -> String)) +fetchAllSols pr = + fromList <$> traverse (\p => (p,) <$> fetchSolution p) (allProblems pr) diff --git a/src/Day1/Part1.idr b/src/Day1/Part1.idr new file mode 100644 index 0000000..6c82365 --- /dev/null +++ b/src/Day1/Part1.idr @@ -0,0 +1,39 @@ +module Day1.Part1 + +import Data.List +import Data.List1 +import Data.String +import Data.Maybe +import Utils + +%default total + + +--- PARSING + +parseLine : String -> Maybe (Nat, Nat) +parseLine str = + let [n1,n2] = filter (/="") $ forget $ split (==' ') str + | _ => Nothing + in (,) <$> parseNat n1 <*> parseNat n2 + +parseInput : String -> Maybe (List Nat, List Nat) +parseInput = map unzip . traverse (parseLine) . lines + + +--- UTILS + +distance : Nat -> Nat -> Nat +distance x y = + cast $ abs $ natToInteger x - natToInteger y + + +--- SOLUTION + +export +solution : String -> Maybe Nat +solution input = do + (list1, list2) <- parseInput input + let list1 = sort list1 + list2 = sort list2 + pure $ sum $ zipWith distance list1 list2 diff --git a/src/Main.idr b/src/Main.idr new file mode 100644 index 0000000..9cc0eb4 --- /dev/null +++ b/src/Main.idr @@ -0,0 +1,46 @@ +module Main + +import Data.List1 +import Data.Maybe +import Data.String +import Data.SortedMap +import Data.SortedMap.Dependent +import Data.Problem + +import Language.Reflection + +import AllDays + +%language ElabReflection + + +||| The latest problem that has been solved. +-- NOTE: UPDATE AFTER EACH SOLUTION +latest : Problem +latest = Pr 1 Part1 + + +solMap : SortedMap Problem (String -> String) +solMap = %runElab fetchAllSols latest + +getInput : IO String +getInput = go "" + where + go : String -> IO String + go str = do + line <- getLine + if trim line == "\\" + then pure str + else go (str ++ "\n" ++ line) + +main : IO () +main = do + putStr "Solution: " + Just pr <- parseProblem <$> getLine + | Nothing => putStrLn "Invalid solution ID" + let Just func = lookup pr solMap + | Nothing => putStrLn "This part is not implemented yet!" + + putStrLn "Input (end with \\):" + input <- trim <$> getInput + putStrLn $ func input diff --git a/src/Utils.idr b/src/Utils.idr new file mode 100644 index 0000000..fa8e9b9 --- /dev/null +++ b/src/Utils.idr @@ -0,0 +1,10 @@ +module Utils + +import Data.Maybe +import Data.String + +%default total + +export +parseNat : String -> Maybe Nat +parseNat = map cast . filter (> 0) . parseInteger