fact: Fixpoint parseAtomicExp (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => DO (u,rest) <-- expect "true" xs; SomeE (BTrue,rest) OR DO (u,rest) <-- expect "false" xs; SomeE (BFalse,rest) OR DO (e,rest) <-- firstExpect "not" (parseAtomicExp steps') xs; SomeE (BNot e, rest) OR DO (e,rest) <-- firstExpect "(" (parseConjunctionExp steps') xs; (DO (u,rest') <== expect ")" rest; SomeE (e, rest')) OR DO (e, rest) <== parseProductExp steps' xs; (DO (e', rest') <-- firstExpect "==" (parseAExp steps') rest; SomeE (BEq e e', rest') OR DO (e', rest') <-- firstExpect "<=" (parseAExp steps') rest; SomeE (BLe e e', rest') OR NoneE "Expected '==' or '<=' after arithmetic expression") end with parseConjunctionExp (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => DO (e, rest) <== parseAtomicExp steps' xs ; DO (es, rest') <== many (firstExpect "&&" (parseAtomicExp steps')) steps' rest; SomeE (fold_left BAnd es e, rest') end.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.Arith.Arith Coq.Arith.EqNat Coq.Lists.List Maps Imp