Compare commits
No commits in common. "3394aedba178120f38dfae04d2804f3e780f1c4b" and "6f26c62b0cf30c133f3a90a5116dff486a6a1a21" have entirely different histories.
3394aedba1
...
6f26c62b0c
2 changed files with 4 additions and 42 deletions
|
@ -13,7 +13,7 @@ PartEff err =
|
||||||
||| Model solving a single day
|
||| Model solving a single day
|
||||||
public export
|
public export
|
||||||
record Day where
|
record Day where
|
||||||
constructor MkDay
|
constructor Both
|
||||||
day : Nat
|
day : Nat
|
||||||
{0 out1, out2, err1, err2 : Type}
|
{0 out1, out2, err1, err2 : Type}
|
||||||
{auto showOut1 : Show out1}
|
{auto showOut1 : Show out1}
|
||||||
|
@ -31,16 +31,7 @@ namespace Day
|
||||||
(day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
|
(day : Nat) -> (part1 : Eff (PartEff err) (out, ctx'))
|
||||||
-> Day
|
-> Day
|
||||||
First day part1 =
|
First day part1 =
|
||||||
MkDay day part1 Nothing {out2 = ()} {err2 = ()}
|
Both day part1 Nothing {out2 = ()} {err2 = ()}
|
||||||
|
|
||||||
||| Constructor for a day with both parts ready to run
|
|
||||||
public export
|
|
||||||
Both : Show o1 => Show o2 => Show e1 => Show e2 =>
|
|
||||||
(day : Nat) -> (part1 : Eff (PartEff e1) (o1, ctx')) ->
|
|
||||||
(part2 :ctx' -> Eff (PartEff e2) o2)
|
|
||||||
-> Day
|
|
||||||
Both day part1 part2 =
|
|
||||||
MkDay day part1 (Just part2)
|
|
||||||
|
|
||||||
||| Freshness criteria for days
|
||| Freshness criteria for days
|
||||||
|||
|
|||
|
||||||
|
|
|
@ -4,37 +4,8 @@ import Control.Eff
|
||||||
|
|
||||||
import Runner
|
import Runner
|
||||||
|
|
||||||
%default total
|
part1 : Eff (PartEff String) ((), ())
|
||||||
|
|
||||||
trackFloor : (start : Integer) -> (xs : List Char) -> Integer
|
|
||||||
trackFloor start [] = start
|
|
||||||
trackFloor start ('(' :: xs) = trackFloor (start + 1) xs
|
|
||||||
trackFloor start (')' :: xs) = trackFloor (start - 1) xs
|
|
||||||
trackFloor start (x :: xs) = trackFloor start xs
|
|
||||||
|
|
||||||
findBasement : (position : Nat) -> (currentFloor : Integer) -> (xs : List Char)
|
|
||||||
-> Nat
|
|
||||||
findBasement position currentFloor [] = position
|
|
||||||
findBasement position currentFloor ('(' :: xs) =
|
|
||||||
findBasement (position + 1) (currentFloor + 1) xs
|
|
||||||
findBasement position currentFloor (')' :: xs) =
|
|
||||||
if currentFloor <= 0
|
|
||||||
then position
|
|
||||||
else findBasement (position + 1) (currentFloor - 1) xs
|
|
||||||
findBasement position currentFloor (x :: xs) =
|
|
||||||
findBasement (position + 1) currentFloor xs
|
|
||||||
|
|
||||||
part1 : Eff (PartEff String) (Integer, ())
|
|
||||||
part1 = do
|
|
||||||
input <- map unpack $ askAt "input"
|
|
||||||
let output = trackFloor 0 input
|
|
||||||
pure (output, ())
|
|
||||||
|
|
||||||
part2 : () -> Eff (PartEff String) Nat
|
|
||||||
part2 x = do
|
|
||||||
input <- map unpack $ askAt "input"
|
|
||||||
pure $ findBasement 1 0 input
|
|
||||||
|
|
||||||
export
|
export
|
||||||
day1 : Day
|
day1 : Day
|
||||||
day1 = Both 1 part1 part2
|
day1 = First 1 part1
|
||||||
|
|
Loading…
Add table
Reference in a new issue