Require Import Io.System.All.
Require Import Io.All.
Require Import List.
Require Import ListString.All.
Require Import Ascii.

Import ListNotations.
Import C.Notations.

Definition solve(line: LString.t): ascii :=
  match line with
  | [_; x; y; _; z; _; _] =>
      if eqb x y then x else z
  | _ => "X"%char
  end.

Fixpoint doTimes(n: nat) : C.t System.effect unit :=
  match n with
  | 0 => ret tt
  | S m => 
      let! line := read_line in
      do! (match line with
          | Some s => log [solve s]
          | _ => ret tt
          end) in
      doTimes m
  end.

Definition main := Extraction.launch (fun _ => doTimes 32).