fact: Fixpoint parsePrimaryExp (steps:nat) (xs : list token) : optionE (aexp * list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => TRY ' (i, rest) <- parseIdentifier xs ;; SomeE (AId i, rest) OR TRY ' (n, rest) <- parseNumber xs ;; SomeE (ANum n, rest) OR ' (e, rest) <- firstExpect "(" (parseSumExp steps') xs ;; ' (u, rest') <- expect ")" rest ;; SomeE (e,rest') end with parseProductExp (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => ' (e, rest) <- parsePrimaryExp steps' xs ;; ' (es, rest') <- many (firstExpect "*" (parsePrimaryExp steps')) steps' rest ;; SomeE (fold_left AMult es e, rest') end with parseSumExp (steps:nat) (xs : list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => ' (e, rest) <- parseProductExp steps' xs ;; ' (es, rest') <- many (fun xs => TRY ' (e,rest') <- firstExpect "+" (parseProductExp steps') xs ;; SomeE ( (true, e), rest') OR ' (e, rest') <- firstExpect "-" (parseProductExp steps') xs ;; SomeE ( (false, e), rest')) steps' rest ;; SomeE (fold_left (fun e0 term => match term with | (true, e) => APlus e0 e | (false, e) => AMinus e0 e end) 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)