fact: Fixpoint parseAtomicExp (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => TRY ' (u,rest) <- expect "true" xs ;; SomeE (BTrue,rest) OR TRY ' (u,rest) <- expect "false" xs ;; SomeE (BFalse,rest) OR TRY ' (e,rest) <- firstExpect "~" (parseAtomicExp steps') xs ;; SomeE (BNot e, rest) OR TRY ' (e,rest) <- firstExpect "(" (parseConjunctionExp steps') xs ;; ' (u,rest') <- expect ")" rest ;; SomeE (e, rest') OR ' (e, rest) <- parseProductExp steps' xs ;; TRY ' (e', rest') <- firstExpect "=" (parseAExp steps') rest ;; SomeE (BEq e e', rest') OR TRY ' (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' => ' (e, rest) <- parseAtomicExp steps' xs ;; ' (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(Init.Nat) Coq(Arith.EqNat) Coq(Lists.List) LF(Maps Imp)