blob: 69d2c9c376d358bde79293d57a47e6ec5ead7e30 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
import «Common»
namespace Day12
------------------------------------------------------------------------------------
inductive SpringState
| operational
| damaged
| unknown
structure SpringArrangement where
Mask : List SpringState
DamagedGroups : List Nat
inductive ParsingError
| unknownSymbolInLeftBlock : Char → ParsingError
| nonNumericSymbolInRightBlock : Substring → ParsingError
| invalidNumberOfBlockSeparators : Nat → ParsingError
| noInput : ParsingError
| missingLeftBlock : ParsingError
| missingRightBlock : ParsingError
instance : ToString ParsingError where
toString := λ
| .unknownSymbolInLeftBlock c => s!"Unkown character in left part of input: '{c}'. Expected '#', '.' or '?'."
| .nonNumericSymbolInRightBlock s => s!"The right block contained an unknown symbol. Expected ',' or numeric digits. Found {s}"
| .invalidNumberOfBlockSeparators n => s!"An input line has an unexpected number of whitespace characters. Expected 1, found {n}."
| .noInput => "The input file is empty."
| .missingLeftBlock => "The left block, which should contain a map of operational ('.') or damaged ('#') springs, or the question mark ('?') is empty."
| .missingRightBlock => "The right block, which should contain a comma-separted list of numbers, is empty."
def parse (input : String) : Except ParsingError SpringArrangement :=
let input := input.toSubstring.trim
let lines := input.splitOn "\n"
let lines := lines.filterMap λx ↦
let r : Substring := x.trim
(Function.const Unit r) <$> Option.ofBool !r.isEmpty
if lines.isEmpty then
Except.error ParsingError.noInput
else
let splitLines := lines.map (·.splitOn " ")
let invalidLines := splitLines.map List.length |> List.filter (· ≠ 2)
if h : !invalidLines.isEmpty then
Except.error $ ParsingError.invalidNumberOfBlockSeparators $ invalidLines.head (List.not_empty_iff_size_gt_zero.mp ((Bool.not_eq_true' _).mp h) |> List.ne_nil_of_length_pos)
else
--splitLines.mapM
sorry
where
parseLeftBlock : Substring → List SpringState → Except ParsingError (List SpringState) := λs p ↦
if s.isEmpty then
Except.ok p.reverse
else
match parseMaskChar s.front with
| .error e => .error e
| .ok v => parseLeftBlock (s.drop 1) $ v :: p
termination_by s => s.bsize
decreasing_by
simp_wf
rename_i h₁
apply Substring.drop_bsize_dec _ _ h₁ Nat.one_ne_zero
parseMaskChar : Char → Except ParsingError SpringState := λ
| '#' => .ok .damaged
| '?' => .ok .unknown
| '.' => .ok .operational
| c => Except.error $ .unknownSymbolInLeftBlock c
parseRightBlock : Substring → Except ParsingError (List Nat) := λs ↦
s.splitOn ","
|> List.mapM λs ↦ (Substring.toNat? s).toExcept (ParsingError.nonNumericSymbolInRightBlock s)
|
