fact: Fixpoint parseSimpleCommand (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => DO (u, rest) <-- expect "SKIP" xs; SomeE (SKIP, rest) OR DO (e,rest) <-- firstExpect "IF" (parseBExp steps') xs; DO (c,rest') <== firstExpect "THEN" (parseSequencedCommand steps') rest; DO (c',rest'') <== firstExpect "ELSE" (parseSequencedCommand steps') rest'; DO (u,rest''') <== expect "END" rest''; SomeE(IFB e THEN c ELSE c' FI, rest''') OR DO (e,rest) <-- firstExpect "WHILE" (parseBExp steps') xs; DO (c,rest') <== firstExpect "DO" (parseSequencedCommand steps') rest; DO (u,rest'') <== expect "END" rest'; SomeE(WHILE e DO c END, rest'') OR DO (i, rest) <== parseIdentifier xs; DO (e, rest') <== firstExpect ":=" (parseAExp steps') rest; SomeE(i ::= e, rest') end with parseSequencedCommand (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => DO (c, rest) <== parseSimpleCommand steps' xs; DO (c', rest') <-- firstExpect ";" (parseSequencedCommand steps') rest; SomeE(c ;; c', rest') OR SomeE(c, rest) end.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.Arith.Arith Coq.Arith.EqNat Coq.Lists.List Maps Imp