fact: Fixpoint parsePrimaryExp (steps:nat) (xs : list token) : optionE (aexp * list token) := match steps with | 0 => NoneE "Too many recursive calls" | S steps' => DO (i, rest) <-- parseIdentifier xs ; SomeE (AId i, rest) OR DO (n, rest) <-- parseNumber xs ; SomeE (ANum n, rest) OR (DO (e, rest) <== firstExpect "(" (parseSumExp steps') xs; DO (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' => DO (e, rest) <== parsePrimaryExp steps' xs ; DO (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' => DO (e, rest) <== parseProductExp steps' xs ; DO (es, rest') <== many (fun xs => DO (e,rest') <-- firstExpect "+" (parseProductExp steps') xs; SomeE ( (true, e), rest') OR DO (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.Arith.EqNat Coq.Lists.List Maps Imp