ManifoldMarketCompletion.lean

def read (s : String) : List (Option (Nat ⊕ Nat)) :=
s.data.map fun
| '(' => .some <| .inl 0
| '{' => .some <| .inl 1
| '[' => .some <| .inl 2
| '<' => .some <| .inl 3
| ')' => .some <| .inr 0
| '}' => .some <| .inr 1
| ']' => .some <| .inr 2
| '>' => .some <| .inr 3
| '?' => none
| _ => panic!"invalid string"

/-- `count n buffer remainder` is the number of possibilities. `n` is the count so far, `buffer` is
  the opening parentheses we've already read but haven't resolved yet,
  `remainder` is the remainder of the string.
  `none` marks an arbitrary opening parenthesis (in the buffer) or an arbitrary parenthesis
  (in the remainder). -/
def count : Nat → List (Option Nat) → List (Option (Nat ⊕ Nat)) → Nat
| n, [], [] => n
| _, _,  [] => 0
| n, l,  none :: xs =>
  (if l.length < xs.length then
    count n (none::l) xs -- ? is read as an opening parenthesis
  else 0) +
  (if let some v := l.head? then
    if v.isSome then -- ? is read as an closing parenthesis
      count n l.tail! xs
    else
      count (4 * n) l.tail! xs
  else
    0)
| n, l,  (.some (.inl k) :: xs) => count n (k::l) xs
| n, l,  (.some (.inr k) :: xs) =>
  if let some v := l.head? then
    if v.getD k == k then
      count n l.tail! xs
    else
      0
  else
    0

def answer (s : String) := count 1 [] (read s)

#eval answer "?<????????????)??]???????}??" -- 360217313280