fact: Fixpoint parseSimpleCommand (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => TRY ' (u, rest) <- expect "skip" xs ;; SomeE (<{skip}>, rest) OR TRY ' (e,rest) <- firstExpect "if" (parseBExp steps') xs ;; ' (c,rest') <- firstExpect "then" (parseSequencedCommand steps') rest ;; ' (c',rest'') <- firstExpect "else" (parseSequencedCommand steps') rest' ;; ' (tt,rest''') <- expect "end" rest'' ;; SomeE(<{if e then c else c' end}>, rest''') OR TRY ' (e,rest) <- firstExpect "while" (parseBExp steps') xs ;; ' (c,rest') <- firstExpect "do" (parseSequencedCommand steps') rest ;; ' (u,rest'') <- expect "end" rest' ;; SomeE(<{while e do c end}>, rest'') OR TRY ' (i, rest) <- parseIdentifier xs ;; ' (e, rest') <- firstExpect ":=" (parseAExp steps') rest ;; SomeE (<{i := e}>, rest') OR NoneE "Expecting a command" end with parseSequencedCommand (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => ' (c, rest) <- parseSimpleCommand steps' xs ;; TRY ' (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(Init.Nat) Coq(Arith.EqNat) Coq(Lists.List) LF(Maps Imp)