This commit is contained in:
Nathan McCarty 2025-01-14 21:51:33 -05:00
parent 62510c6755
commit 9721602598

View file

@ -5,24 +5,168 @@ module Years.Y2015.Day8
import Control.Eff
import Data.Primitives.Interpolation
import Runner
-->
```idris
import Data.String
import Data.Vect
import Data.Either
```
<!-- idris
%default total
-->
## Parsing
Effect alias for a parser
```idris
Parser : List (Type -> Type)
Parser =
[Choose, State (List Char), Except String]
```
Get the next character from the state, modifying it in place
```idris
getNext : Eff Parser Char
getNext = do
chars <- get
case chars of
[] => throw "End of Input"
(x :: xs) => do
put xs
pure x
```
Parse a quote
```idris
quote : Eff Parser ()
quote = do
char <- getNext
if char == '"'
then pure ()
else throw "Expected quote, found: \{show char}"
```
Parse a char that's not a quote or an escape character
```idris
normal : Eff Parser Char
normal = do
char <- getNext
if any (char ==) (the (List _) ['\\', '"'])
then throw "Tried to parse a special character as normal \{show char}"
else pure char
```
Parse a hex digit
```idris
hexDigit : Eff Parser Int
hexDigit = do
char <- getNext
case toLower char of
'0' => pure 0x0
'1' => pure 0x1
'2' => pure 0x2
'3' => pure 0x3
'4' => pure 0x4
'5' => pure 0x5
'6' => pure 0x6
'7' => pure 0x7
'8' => pure 0x8
'9' => pure 0x9
'a' => pure 0xa
'b' => pure 0xb
'c' => pure 0xc
'd' => pure 0xd
'e' => pure 0xe
'f' => pure 0xf
_ => throw "Invalid hex digit: \{show char}"
```
Parse an escaped character
```idris
escaped : Eff Parser Char
escaped = do
escape <- getNext
if escape == '\\'
then do
first <- getNext
case first of
'\\' => pure '\\'
'"' => pure '"'
'x' => do
[x, y] : Vect _ Int <- sequence [hexDigit, hexDigit]
-- Fails to compile
-- pure . chr $ x * 0x10 + y
-- Compiles
pure . (const 'a') $ x * 0x10 + y
_ => throw "Invalid Escape Character: \{show first}"
else throw "Tried to parse non escape as escape \{show escape}"
```
Parse any non-quote character
```idris
character : Eff Parser Char
character = oneOfM (the (List _) [escaped, normal])
```
Run a parser until it runs out
```idris
parseMany : Eff Parser t -> Eff Parser (List t)
parseMany x = do
Just next <- lift $ catch (\_ => pure Nothing) (map Just x)
| _ => pure []
map (next ::) (parseMany x)
```
Parse any number of non-quote characters
```idris
characters : Eff Parser (List Char)
characters = parseMany character
```
Parse a quote delimited string
```idris
parseString : Eff Parser (List Char)
parseString = do
quote
xs <- characters
quote
pure xs
```
Run a parser
```idris
runParser : Eff Parser t -> String -> Maybe t
runParser m str =
map fst . head' . rights
. extract . runChoose {f = List} . runExcept . runState (unpack str)
$ m
```
## Part Functions
### Part 1
```idris
part1 : Eff (PartEff String) (Nat, ())
part1 : Eff (PartEff String) (Nat, List (List Char, List Char))
part1 = do
inputs <- map (lines . trim) $ askAt "input"
let outputs = map (map pack . runParser parseString) inputs
let pairs = zip inputs outputs
let debug_out = joinBy "\n" . map show $ pairs
putStrLn debug_out
?part1_rhs_1
```
<!-- idris