From dec694c91c32fcd4dfe947b5f07bef6cd4df9cae Mon Sep 17 00:00:00 2001 From: Matt Russell Date: Tue, 3 Dec 2024 08:35:51 +0000 Subject: [PATCH] day3 part 1 --- Aoc2024/Day03/Examples.lean | 2 +- Aoc2024/Day03/Main.lean | 4 ++-- Aoc2024/Day03/Solve.lean | 25 ++++++++++++++++++++++--- Aoc2024/Day03/inputs/example.txt | 1 + Aoc2024/Day03/inputs/input.txt | 6 ++++++ Aoc2024/Utils.lean | 5 +++++ lake-manifest.json | 28 ++++++++++++++++++++++++---- lakefile.toml | 4 ++-- lean-toolchain | 2 +- 9 files changed, 64 insertions(+), 13 deletions(-) diff --git a/Aoc2024/Day03/Examples.lean b/Aoc2024/Day03/Examples.lean index 1effa2a..372afb4 100644 --- a/Aoc2024/Day03/Examples.lean +++ b/Aoc2024/Day03/Examples.lean @@ -1,2 +1,2 @@ def exampleInput := -"..." +"xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5))" diff --git a/Aoc2024/Day03/Main.lean b/Aoc2024/Day03/Main.lean index 686f617..2d03a06 100644 --- a/Aoc2024/Day03/Main.lean +++ b/Aoc2024/Day03/Main.lean @@ -4,8 +4,8 @@ import Aoc2024.CustomMonadLift def solve (name: String) (inputPath: String) : IO Unit := do IO.println name let input <- IO.FS.readFile inputPath - IO.println s!"Part 1: {<- parseAndSolvePart1 input}" - IO.println s!"Part 2: {<- parseAndSolvePart2 input}" + IO.println s!"Part 1: {solvePart1 input}" + -- IO.println s!"Part 2: {<- parseAndSolvePart2 input}" def main : IO Unit := do IO.println "Day 03" diff --git a/Aoc2024/Day03/Solve.lean b/Aoc2024/Day03/Solve.lean index 4175b2f..4b8906d 100644 --- a/Aoc2024/Day03/Solve.lean +++ b/Aoc2024/Day03/Solve.lean @@ -1,12 +1,31 @@ import Aoc2024.Utils import Aoc2024.Day03.Examples import Aoc2024.Day03.Parser +import Regex +open Regex (Match Captures) -private def solvePart1 (things : List Int) : Int := sorry +def mulRegex := regex% r"mul\((\d+),(\d+)\)" -def parseAndSolvePart1 (s : String): Except String Int := parseThings s |>.map solvePart1 +def matchToNat (m : Match) : Option Nat := m.toNat? --- #guard parseAndSolvePart1 exampleInput == Except.ok 2 +def optMatchToNat (m : Option Match) : Option Nat := m >>= matchToNat + +def matchesToNatPair (ms : Array (Option Match)): Option (Nat × Nat) := + match ms.toList with + | [some m1, some m2] => Prod.mk <$> matchToNat m1 <*> matchToNat m2 + | _ => none + +def capturesToNatPair (captures: Captures) : Option (Nat × Nat) := + matchesToNatPair captures.groups + +def findMatches (s : String) : List (Nat × Nat) := + Regex.all_captures s mulRegex |>.toList |>.bind (fun captures => captures |> capturesToNatPair |> Option.toList) + +#guard findMatches "mul(1,2) mul(3,4)" = [(1, 2), (3, 4)] + +def solvePart1 (s : String) : Int := findMatches s |>.sumBy (fun (n1, n2) => n1 * n2) + +#guard solvePart1 exampleInput = 161 private def solvePart2 (things : List Int) : Int := sorry diff --git a/Aoc2024/Day03/inputs/example.txt b/Aoc2024/Day03/inputs/example.txt index e69de29..2e1a90a 100644 --- a/Aoc2024/Day03/inputs/example.txt +++ b/Aoc2024/Day03/inputs/example.txt @@ -0,0 +1 @@ +xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5)) \ No newline at end of file diff --git a/Aoc2024/Day03/inputs/input.txt b/Aoc2024/Day03/inputs/input.txt index e69de29..36b0331 100644 --- a/Aoc2024/Day03/inputs/input.txt +++ b/Aoc2024/Day03/inputs/input.txt @@ -0,0 +1,6 @@ +[#from())when()/}+%mul(982,733)mul(700,428)}}don't(){:,$+mul(395,45)[; what()!mul(328,373)?!, <-)mul(139,254)^>#)*,[,&when()mul(719,688)-@,from()-@mul(616,640)from()!~{[' mul(666,309)(mul(889,261){select();why())<(/mul(364,750)>:+(:/mul(911,969)mul(360,631)~select() )$>mul(692,527)^mul(823,512)!]{where():&;,how()don't()'?,*where()<[>!mul(345,427))~ do()((how()@mul(394,662)[mul(903,277)why()~from()mul(249,126)>?/-what()'when()from()[who()mul(823,356)$mul(257,129),%*what()+]when()(mul(571,713)+why()]#([mul(230,759)'%^}$]mul(978,804)%>~!{-&don't() &'how() why()why(379,123)mul(816,166)}from(576,921) ?/when()?when()mul(946,526)/*mul(321,352)> where()'^ select(925,337)>[mul(233,433)^mul(247,132)select(){[ ]!~ mul(104,931)why()&-+)~:}#,}-$>&mul(412,598)*who()where();@why()do()mul(814,674)%where(){;~mul(654,224)/(what()][^how(190,339)#mul(690,95)&}what()*[mul(821,149) :-who()from()~mul(279,247);)mul(66,274)who()$)why()@where(395,477)~:/~mul(442,748)*when()from()'who()}]^~%mul(130,259)}why()<})how(){^mul(768,298)>{-+when(366,794):-mul(489,845)*mul(442,721)-$[ {)mul(283,227)@how()[where()>mul(862,708)'who()?*!where(){mul(182,377)#^mul-[;select()^-!mul(472,672)'select()mul(117,275))$where()$('select(),$(mul(409,378)where()where()?'mul(448,267)]!,:&;what()%>what(265,341)mul(916,448)~when()/!/ ;how()mul(849,877)what()*?do()mul(851,406)~/%~mul(480,848)from(607,219)who()@~mul(803,80)don't(){*how()%{!where()select()mul(482,344),]/mul(702,892)how()@)']mul(552,653))&<^,^+#mul(13,654) /?:mul&from()what()mul(247,264)<$'{*^how();;mul(453,796)&+select(338,67)mul(201,343)>select()) /who()mul(360,411)what()why()@mul(657,810):/}&$:+-^what()do()what()'select()where()mul(129,10)$#where()!]select(),}how()~mul(545,776)@%*how()who(){mul(25,979)mul(448,493)what()'^>do()why()# & mul(56,384) +?why()mul(56,627):-?+-what()from()(}mul(55,437)(*%&$do()#{$don't()&mul(246,928)&%)#%,'#select()how()mul(943,775)*,!mul*/'(who()where())mul(719,941)?, >-^/mul(778,355)%what()mul(920,978)@when()do()/how()'when()-mul(671,550)!what()>[!mul(644,99)'who(308,220)'$({mul(919,375select()don't()'what()mul(714,919)<;#-{!{mul(541,507)(*what()%why()mul(692,759)$mul(716,287)!]>^mul(665,820);who()mul(489,645)@~(why()?$^%select()mul(815,720)@mul(143,726)-(!-what()where(){#mul(320,590)!:)+{@{*+]mul(140,659)mul(935,172)mul(329,759))'}~~'[when()+mul(771,773)'!*}*select()<}-mul(205,139)when()'$*/{mul(666,493)mul(54,372)$,#$what()@{:}[mul(824,679)from()}mul(918,54)@;>@!mul(227,267)~];what()mul(327,164)%,}mul(154,571)]^mul(97,247))mul(219,849)select()mul(279,307)how(),*?*&$#?)!}~#+mul(214,556)?~(mul(947,774)($^(>#-/@'mul(680,458)>*what(378,770)~- '?where()mul(757,805)+[?#select():-mul(607,982)(?*{!-$>,mul(934,196)when()how()where()%]^^&%mul(879,438)where()}?what()&*why()why()mul(563,458) don't()select(823,614)!*')where()where(),mul(621,647)~{$ ??why()mul(258{ ]who()>-]don't()/!&mul(783,70)~select(),mul(601,782)where()@mul(132,385)[mul(639,263{ ?why():}{&mul(424,281)-*>+who()!how()where(729,42)mul(579,859){+why()mul(826,812)&($#mul(28,383)]-from()&mul(274,484)^select()mul(662,327)+when()from()#[]who()mul(481,190)^^:>+mul(656,796)?[,]]?mul(195,147)select()]>mul(405,286)?%}#-where()$why(753,135)^mul(207,366)!why()when(245,871)*#mul(834,202):]how(511,578)who() @+mul(860,487)mul(766,862)why()^$from()#%$]mul(458,470)why()mul(852,979)mul(983,451)select(505,117)!:don't()]$]#[,<}mul(822select() ]! ;%,mul(384,20)>what()*;-+mul(309,125)'from()how()who()-when()select()when() ?mul(326,51)when()@:mul(493,525)~select()/?^&mul(235,832'@when()}mul(657,540)@>,from()!mul(959,593)don't()>/how()~]&:{mul*;>}~mul(305,904)mul(906,489)&mul(315,569)([from()~mul(565,343)@<^select()mul(48,333)mul(787,786)$ #(}mul(953,78):/?why(230,166)*who():(~what()mul(252,932)[when()^*:when():mul(200'+'~}what()mul(829,705)from(590,812)>mul(130,990where()(from()^mul(281,313) @mul(809,672)*why() what(),(+mul(478,222)^&who()?*!mul(576,270) +,^how()mul(48,786)?^~<(<*from()don't()what()}mul(392,859))(why())select()mul(277,939)%mul(504,200)+who()from()why()/:~ $mul(187,846)who(907,944)mul(688,788+>mul(530,75)>when()what(),!who(761,680){;,#mul}~(/why()mul(891,102)@/^mul(803,887)'when()*from()/%%>&mul(89,939) who()when(){mulwhat()where()from(462,595)%mul(502,530)^]?'-mul(250,294)mul(605,766)(&>[mul(603,805)mul(137,182)mul(423,943)when(901,398) )mul(288,661)mul(625,873)-who()what()why()+#>}mul(241,604):(]~>&:mul(467,489)/&}[?>mul(53,380)'&[when()&~$?mul(302,961)from()*when()}select()mul(882,764) ,?%what()mul(204,978)when())who()mul(353,772)what();+>-mul(770,681);select()@mul(769,770)^select()when()mul(111,749)$&+?,?mul(633,686)]what()-why()mul(665how()[what()>mul(293,891)mul(442,313)!+where()$*mul(943,306;}%%select() mul(725,505)$why()['select()mul(922,245)~mul(800,759),mul(151,956)!mul mul(93,438)mul(387,185)[who(477,260)}>}[don't()![what()?]what()!(how()mul(554,415)](#mul(383,957)mul(454,823{:<;mul(385,442)<<-where()]select())mul(596,203)mul(402,933)[ &+mul(73,911)mul(308,100)()<%/]how()! $mul(114,356)how()$who():{$~when()mul(932,798)':!%<,@where()&mul(432,183)]when(489,492):,+how()who()mul(452,30)mul(605,245)how()why()@,who()where(941,116)/?mul(71[where()^&when()mul(241,487)mul(668,60)mul(117,107)}[mul(115,580)~why()}:$+>{:mul(158,892)select()?^)%^where()*who()mul(959,22))##~#?}mul(149,724)'when()from())??select()' mul(303,721)where())*mul(558,172)mul(263,92)mul(238,242)'!why()where(229,547),do()why()who(),~'+mul(942,451)why()what()mul(734,792)select(); what()+,;}'mul(474,602)+mul(22,992)?what()?when()mul(13,956)'!}#;what()mul(943,628)*'mul(766,222)~(how()!mul(415,153)+^when()select()#what()how()(mul(954,996)~mul(677,121)/why()~who()-~mul(585,596)$':where(): who()%select()mul(615,102)[when();where()why()mul(514,759)where()]mul(655,965)[mul(159,259)/where()why():{mul(575,955)@%what()<,@select()!mul(483,798)>mul(739,11)where()from()}^#mul(893,732)mul(94,603)#who(21,133)why()^?'#what()mul(505,569);%mul(179/mul(438,58)$#:who(){{%when()!)mul(23,492from(){[what()!?)(;(mul(635,75)*@#how()*@when();}who()#!/usr/bin/perlwhy()/(#*what()mulwhat()from()select()*;%mul(975,209)when():how()+{mul(892,132) +mul(852,368)%:mul(114,988)@}-from()->+mul{how()^;$}&:-mul(985,558)how()%select()){%(:; mul(288,312){;where()'how()mul(336,716)/{(,;mul(409,530)why()$where()how()';where()%]mul(701*mul(961,243)>?$}[what(195,143)^mul(61,76)>>select()~when()why()$;mul(743,240)+~from()what()/{&when()why()!mul(347,105 what()mul(617,589) /@#%;?from()^*mul(330,309)[';?,&[%mul(370,215)!~[#when()>who()&mul(547,103)~when()&mul(965,253)from()*$-+*mul(589,893)mul(324,608select()[why()&-~>[how()why()?don't()#;@how(429,486)mul(184,79)#@^':}$]-mul(693,137)where()[who(696,367)mul(500,973)where()~^mul(706,585)}!%~mul(388,864)/why() mul(64,438)&!-who()%*$from()from()&mul(715,860)why()where()]%!:when()?^mul(60,506)*!-why()}^mul(364,578)mul(213,857)#when()mul(944,88)what()mul(929,686)>>mul(521;how()/~,)^don't():{~~ >]'mul(181,275)?how()%/$}{where())mul(849,549)}what()^ -mul(377,304)(select()who()mul(144,3)---~*when()/}mul{/;where() mul(820,531)'who()who()+'what()mul(447,768)?&;;/;what()mul(242,291)<]select()why()mul(103,796)from()<(who()how()mul(131,237) mul(317/mul(265,348)])!;mul(635,160)why()#/)~who()$mul(779,125)from()mul(584,45),!from()&where()@?mul(225,920)^'select()+~mul(545,219/~~-+*;&'mul(758,66)]~(mul(190,720)mul(721,95)~!/]]@>who()from()mul(835,210)mul(854,651),( , where()+@[mul(420,440)['}>}-mul(78,899)where()@%from()^mul(969,326)from(273,316)(what()]don't()mul(926,149)select(557,597))*,#who()mul(500,899)mul(784^:when()mul(246,886)/:why()mul(566,809)#{^@how()what(14,517)why()how(717,279)'mul(618,578)~mul(377,565);[^@+how();mul(971why()what()>#$$why()mul(340,80)%do()<:^?<$;mul(270,501)+$mul(123,33)who()#]mul(210,880)##;~@ ,when(321,532)how()-mul(774,259)mul(134,769)mul(530,259)when()how(),-*mul(824 [> from()?'how()$?mul(659,212)/mul(349,292)([}who()>@#@who()mul(301,677)~}#&+how(33,836)mul(756,809)@)who()what()^&mul(340,355)why()*mul(895,908)#$,!]?~mul(947,581) when()mul(812,612))~:,!>mul(784,307)>%select()&select()mul(465,327)when();>>/where()mul(198,33)%%what()select()?^,@how()mul(569,675)~;+where()'>@how()what()mul(405,231){?mul(773,340)why()what(431,691);from()%~@([mul(775,613+[);!mul(575,541)why()!@mul(765,267)?where(462,577)%+),&%'mul})'mul(206,338))+don't()<<{mul(577,346)mul(364,159);:*~@:+!;mul(572,192)mul(979,469)why();>mul(245,149)where()+mul(379,423)!:)mul(929,482)#^don't()[,%mul(165,905) what()where()how(){@mul(409,95)select()>#who()#mul(765,311)+where()when()mul(342,342);where()$(%;/mul(950,988),from()%~/mul(276,267)(>[)+[-when();%mul(339,489)/?when()-~%>what()from(572,199)mul(675,192)how()mul(809,602)[~>*don't()*]#}mul(485,278)}]mul(625,974)why(510,506)from()^>from()mul(274,178)#$,;select()mul(937,671)do()(:{?'!from() }mul(819,952)}:^when()%%$mul(408,89)mul(614$:#@[);$mul(66,163)+$mul(449,71)#why()(who()select()]how(421,129)mul(253,770) who(781,473)]mul(634,363)$when()*how() &mul(445,296)how()%>;'what()/,when()mul,>where()##mul(855,89)*select()}why()*select(59,18)<[mul(587,594@$?*where()mul(156,269)[]/mul(253,48)[]?where()*;mul(439,325)@who()who())*?when()#>from()mul(957,103)mul(199,630<(%where(220,646))!mul(924,669)~/{why(){mul(691,638)*mul(432,319)!]:'-?#from()mul(682,628)where()])why()#mul(103,731)'why()>what()$when()mul(709,983)select(655,64),)when()where()!>why()from(905,517)where()mul(278,204)<^%:select()what()mul(948,388): /(;;[what(965,999)@&mul(128,610):]~-how()$mul(752,530)who()'^what()!>!why()mul(486,916)$how(604,686)?@mul(322,302)?[>)mul(773,589)+!?~{/from()mul(461,456)why()~do()+how()-&%*mul(356,968)mul(961,828)(]:?;mul(765,321)& -mul(642,428)'what() why()how()-mul(78,233),]@!(?how()*from()mul(802,766)when()mul(674,430)from()+mul(187,741)]from()& %]}select(61,271)*(mul(699-'<$~?mul(442,143)#select()>when():mul(754,355)where()how()]%@< :]mul(952,528)}from(726,679)*~{), what():mul(747,103)!:'+)mul(761,566?,)^#why()}/,mul(713,786)mul(763,306)how()]>-how()+$mul(854,759)~:@from()[#mul(451,677) &->what()?what()mul(688,574)):{-['{mul(680,919)$^~where(393,389));-{where()mul(422,657)from()why(939,633)why()/mul(401,912what()<:%!;>![where()what()mul(262,821)>~*how()~mul(469,992)(+;how()mul(562,853) +mul(596,121)$}why(),who()mul(644~!;()what()mul(414,217):select():@}![];mul(963,916)mul(698,955)mul(887,587)+ mul(664,770)],who()'@,do()++$mul(375,153)}!^~#mul(189,464{:-?# mul(260,699)} -~how():?)who()mul(655,375)why()what()[do()~why()}who():mul(79,366)[$?@select()mul(594,21)(where()!-()select()who()mul(184,709)((?&what()what():when()(from()mul(538,963)~%,mul(638,808)why():mul(865,350)when(){>why()when(644,413){mul(437,972) +<,mul(953,93)>mul(920,599)>mul(81,578)select()}select(),what()?mul*select()mul(269,16)mul(990,699)mul(169,956)where()/$where()[@**{mul(236,175)%$%?$mul(560,233)mul(667,378)-~why();#'{-::mul(744,229)[%}@^^)do()where()-?why()&],::$mul(613,151)((}{>;mul(324,709)],]where()#~?mul(504,448)$where(801,178)}where(),%<*mul(441;/*mul(623,742)#?@how()@mul(447,481)'when()mul(546,493)&$how()+mul(75,277);<;(mul(339,191)mul(460,916) select()~:mul(655,210)$(#&who()}!mul(402,964)?!;how()[>mul(384,443),mul(715,435):}${mul(683,756)who()!'where()mul(349,78)*from()?';- >why()$don't()<'/what()-[:;where()who()mul(846,294)mul(382,709) [?@>mul(27,363)%!when()when()~:mul(620,721)[how()! do()mul(729,333)%!mul(822,111)%select()mul(984,174)?how()#' {where()$*mul(126,855)}-$)mul(347,402),+where()mul(542,243){-do()@{&mul(585,736) ^,mul(930,849)%where()]mul(750,188)what()<*(mul(76,528)~+who()*$:when()mul(474,368)$; : {mul(168,683)when()':'*from()(:-mul(857,78){)-mul(776,53)mul(920,130)!<))+why()!do()select()}mul(329,472)mul(507,107)mul(539,64)&^@?mul(716,635)>%~>how()#mul(68,519)-+;*mul(891,188)[where()what()what()?why()#!#mul(985,567)^{mul(429,918)how()do()mul(285,28)#who())&mul(754,541)select())mul(988,728)?/+mul(644,517)^[<&>why()why()mul(529,314);,-select(),what()mul(952,786)+select(); why()mul(503,655) {[-%]; !+mul(317,344))~{*,&$mul(367,12)mul(84,895)who(177,299)*!~]$+ diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean index e302306..2045331 100644 --- a/Aoc2024/Utils.lean +++ b/Aoc2024/Utils.lean @@ -47,6 +47,8 @@ def sepBy (p : Parser α) (sep : Parser β) : Parser (List α) := namespace List + def sum (xs: List Int) : Int := xs.foldl .add 0 + def sumBy (f : α → Int) (xs : List α) : Int := xs.foldl (λ acc x => acc + f x) 0 def toSet {α:Type} [BEq α] [Hashable α] (xs: List α) : HashSet α := @@ -57,6 +59,9 @@ namespace List end List +#guard [].sum = 0 +#guard [1, 2, 3].sum = 6 + #guard [1, 2, 3].sumBy (λ x => x * x) = 14 #guard [].differences == [] diff --git a/lake-manifest.json b/lake-manifest.json index 33a8db1..0e69cd3 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,15 +1,35 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/batteries", + [{"url": "https://github.com/fgdorais/lean4-unicode-basic.git", "type": "git", "subDir": null, - "scope": "leanprover-community", - "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83", + "scope": "", + "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "v1.1.0", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "", + "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18", "name": "batteries", "manifestFile": "lake-manifest.json", + "inputRev": "v4.13.0", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/bergmannjg/regex", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b42eb7a7b1338cb18873fc1e5a985600026c2f56", + "name": "Regex", + "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": false, - "configFile": "lakefile.toml"}], + "configFile": "lakefile.lean"}], "name": "aoc2024", "lakeDir": ".lake"} diff --git a/lakefile.toml b/lakefile.toml index 5bf8f1b..14269de 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -22,6 +22,6 @@ name = "dayXX" root = "Aoc2024.DayXX.Main" [[require]] -name = "batteries" -scope = "leanprover-community" +name = "Regex" +git = "https://github.com/bergmannjg/regex" rev = "main" \ No newline at end of file diff --git a/lean-toolchain b/lean-toolchain index 3450f2d..e0676e0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0-rc1 \ No newline at end of file +leanprover/lean4:v4.13.0 \ No newline at end of file