diff --git a/Aoc.lean b/Aoc.lean deleted file mode 100644 index f7027a9..0000000 --- a/Aoc.lean +++ /dev/null @@ -1,3 +0,0 @@ --- This module serves as the root of the `Aoc` library. --- Import modules here that should be built as part of the library. -import Aoc.Basic \ No newline at end of file diff --git a/Aoc/1/Basic.lean b/Aoc/1/Basic.lean deleted file mode 100644 index bec6648..0000000 --- a/Aoc/1/Basic.lean +++ /dev/null @@ -1,30 +0,0 @@ -def rawFile := IO.FS.readFile "Aoc/1/input.txt" - -def parseRaw (rawFile: IO String): IO (List (Int × Int)) := do - let raw ← rawFile - let splitted := raw.splitOn "\n" - let listOfTwoElementList := List.map (λ x => x.splitOn " ") splitted - let dropped := List.dropLast listOfTwoElementList - let pairs := List.map (λ x => ((List.get! x 0).toInt!, (List.get! x 1).toInt!)) dropped - pure pairs - -set_option maxRecDepth 10000 -#eval parseRaw rawFile - -def input: List (Int × Int) := [(3, 4), (4, 3), (2, 5), (1, 3), (3, 9), (3, 3)] - -def transpose (input: List (Int × Int)) := input.foldl (fun (acc1, acc2) (x, y) => (acc1.append [x], acc2.append [y]) ) ([], []) - -def solve (input) := transpose input - |> (λ (a, b) => (List.mergeSort a, List.mergeSort b)) - |> (λ (a, b) => a.zip b) - |> (λ l => l.map (λ (x, y) => (x - y).natAbs)) - |> List.foldl Nat.add 0 - -def solveIO (inputIO: IO (List (Int × Int))) : IO Nat := do - let input ← inputIO - pure $ solve input - -#eval solveIO $ pure [(3, 4), (4, 3), (2, 5), (1, 3), (3, 9), (3, 3)] - -#eval solveIO $ parseRaw rawFile diff --git a/Aoc/Day1/Solution.lean b/Aoc/Day1/Solution.lean new file mode 100644 index 0000000..f3d4edf --- /dev/null +++ b/Aoc/Day1/Solution.lean @@ -0,0 +1,33 @@ +instance : Monad List where + pure := List.singleton + bind := List.flatMap + +def List.sequence {m α} [Monad m] (lst: List (m α)) : m (List α) := List.mapM id lst + +def parse (raw : String) : Option (List (Int × Int)) := + raw.splitOn "\n" + |> List.map (String.splitOn · " ") + |> List.map (List.map String.toInt?) + |> List.map List.sequence + |> List.filter Option.isSome + |> List.sequence + |> Option.map (List.map (λ x => match x with | [a, b] => some (a, b) | _ => none)) + |> Option.map List.sequence + |> Option.join + +def solve (input: List (Int × Int)) : Nat := + input.unzip + |> λ (a, b) => List.map (λ (x, y) => (x - y).natAbs) (a.mergeSort.zip b.mergeSort) + |> List.sum + +def fakeRawInput: String := "3 4\n4 3\n2 5\n1 3\n3 9\n3 3" +#eval solve <$> parse fakeRawInput + +def fakeParsedInput: List (Int × Int) := [(3, 4), (4, 3), (2, 5), (1, 3), (3, 9), (3, 3)] +#eval solve fakeParsedInput + +def parseAndSolve : String → Option Nat := + Option.map solve ∘ parse + +def rawInput := IO.FS.readFile "Aoc/Day1/input.txt" +#eval parseAndSolve <$> rawInput diff --git a/Aoc/1/input.txt b/Aoc/Day1/input.txt similarity index 100% rename from Aoc/1/input.txt rename to Aoc/Day1/input.txt diff --git a/Main.lean b/Main.lean deleted file mode 100644 index 73eb7c6..0000000 --- a/Main.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Aoc - -def main : IO Unit := - IO.println s!"Hello, {hello}!"