From d1eb180aaeb1607f8179659d644e65dcd4ec3752 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 19 Mar 2022 10:38:17 -0700 Subject: [PATCH] test: add non mutually recursive version --- tests/lean/run/lex.lean | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/tests/lean/run/lex.lean b/tests/lean/run/lex.lean index b09e8e811d..62bb8a3d5b 100644 --- a/tests/lean/run/lex.lean +++ b/tests/lean/run/lex.lean @@ -22,7 +22,7 @@ inductive LexErr where def charDigit? (char : Char) : Option Nat := if char.isDigit then - some char.toNat + some (char.toNat - '0'.toNat) else none @@ -54,3 +54,35 @@ end #eval lex (m := Except LexErr) "123".iter #eval lex (m := Except LexErr) "1+23".iter #eval lex (m := Except LexErr) "1+23()".iter + +def Option.toList : Option α -> List α + | none => [] + | some x => [x] + +namespace NonMutual + +def lex [Monad m] [MonadExceptOf LexErr m] (current? : Option (List Char × Nat)) (it : String.Iterator) : m (List Token) := do + let currTok := fun + | (cs, n) => { text := {data := cs.reverse}, tok := Tok.num n } + if it.hasNext then + let emit (tok : Token) (xs : List Token) : List Token := + match current? with + | none => tok :: xs + | some numInfo => currTok numInfo :: tok :: xs; + match it.curr with + | '(' => return emit { text := "(", tok := Tok.lpar } (← lex none it.next) + | ')' => return emit { text := ")", tok := Tok.rpar } (← lex none it.next) + | '+' => return emit { text := "+", tok := Tok.plus } (← lex none it.next) + | other => + match charDigit? other with + | none => throw <| LexErr.unexpected other + | some d => match current? with + | none => lex (some ([other], d)) it.next + | some (tokTxt, soFar) => lex (other :: tokTxt, soFar * 10 + d) it.next + else + return current?.toList.map currTok + +#eval lex (m := Except LexErr) none "".iter +#eval lex (m := Except LexErr) none "123".iter +#eval lex (m := Except LexErr) none "1+23".iter +#eval lex (m := Except LexErr) none "1+23()".iter