Require Import Io.System.All Io.All List ListString.All Ascii.
Import ListNotations C.Notations.
Definition j(line:LString.t):ascii:=match line with[_;x;y;_;z;_;_]=>if eqb x y then x else z|_=>"X"%char end.
Fixpoint q(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[j s]|_=>ret tt
end)in
q m
end.
Definition main:=Extraction.launch(fun _=>q 32).