Evaluating an expression provided as a string

Stream: lean4

[Jeremy Tan]

I want to define a function that parses arithmetic expressions provided as strings, and returns the value of the expression as a rational number if the string can be parsed, and 0 otherwise. The code below doesn't work (evaluate% comes from #new members > ✔ Evaluating code string @ 💬):

import Mathlib

open Lean Parser Elab Tactic Meta

/-- Turn a string into an expression, similar to Python's `eval`. -/
elab "evaluate%" code:str : term <= expectedType => do
  let .ok stx := Parser.runParserCategory (← getEnv) `term code.getString |
    throwError s!"Failed to parse {code}"
  Term.elabTerm stx expectedType

#eval evaluate% "(1 / 3 + 5 - 7 / 9 : ℚ)" -- mkRat 41 9

/-- A mapping from `Fin 4` to the four basic arithmetic operations. -/
def opMap : Fin 4 → String
  | 0 => "+"
  | 1 => "-"
  | 2 => "*"
  | 3 => "/"

def evalWhiteboard (ops : Fin 4 → Fin 4) : ℚ :=
  withMainContext do
    let w := s!"(1 {opMap (ops 0)} 3 {opMap (ops 1)} 5 {opMap (ops 2)} 7 {opMap (ops 3)} 9 : ℚ)"
    match runParserCategory (← getEnv) `term w with
    | .error e => (0 : ℚ)
    | .ok stx => Term.elabTerm stx _

How can I get it to work?

[Jeremy Tan]

So basically I want to turn evaluate% into a standard definition, returning 0 for unparseable inputs or inputs not evaluating to a rational

[Kenny Lau]

well, you want to run meta-code in main-land, that's i don't think allowed

[Jeremy Tan]

I think I've got it @Kenny Lau (based on #Is there code for X? > get Parser from Lean @ 💬)

import Mathlib

section

open Lean Parser

/-- The four basic arithmetic operations. -/
inductive Op where
  | add | sub | mul | div
deriving DecidableEq, Repr, Inhabited

/-- A type of arithmetic expressions on natural numbers, but evaluating in the rationals. -/
inductive Arith where
  | val : ℚ → Arith
  | app : Op → Arith → Arith → Arith
deriving DecidableEq, Repr, Inhabited

unsafe def parseArith : Parser := arithParser 0 where
  arithParserFnCore : ParserFn :=
    prattParser `arith parsingTables .default (mkAntiquot "arith" `arith (isPseudoKind := true)).fn
  arithParser (prec : ℕ) : Parser :=
    { fn := adaptCacheableContextFn ({ · with prec }) (withCacheFn `arith arithParserFnCore) }
  num : Parser := Term.num
  add : TrailingParser := trailing_parser:30:30 " + " >> arithParser 31
  sub : TrailingParser := trailing_parser:30:30 " - " >> arithParser 31
  mul : TrailingParser := trailing_parser:35:35 " * " >> arithParser 36
  div : TrailingParser := trailing_parser:35:35 " / " >> arithParser 36
  parsingTables : PrattParsingTables := {
    trailingParsers := []
    trailingTable := [(`«+», add, 30), (`«-», sub, 30), (`«*», mul, 35), (`«/», div, 35)].foldl
      (fun map (a, b) ↦ map.insert a b) {}
    leadingParsers := []
    leadingTable := [(`«$», num, maxPrec), (`num, num, maxPrec)].foldl
      (fun map (a, b) ↦ map.insert a b) {}
  }

partial def evalArith : TSyntax `arith → ℚ
  | `(parseArith| $a:arith + $b:arith) => evalArith a + evalArith b
  | `(parseArith| $a:arith - $b:arith) => evalArith a - evalArith b
  | `(parseArith| $a:arith * $b:arith) => evalArith a * evalArith b
  | `(parseArith| $a:arith / $b:arith) => evalArith a / evalArith b
  | `(parseArith| $n:num) => n.getNat
  | _ => 0

instance : Insert Token TokenTable := ⟨fun a b ↦ b.insert a a⟩
instance : Singleton Token TokenTable := ⟨fun a ↦ insert a ∅⟩

def evalString (input : String) : ℚ := unsafe
  let env : Environment := unsafeCast ()
  let tokens : TokenTable := {"+", "-", "*", "/"}
  let state := parseArith.fn.run (mkInputContext input "<input>")
    (ParserModuleContext.mk env {} .anonymous []) tokens (mkParserState input)
  if state.hasError then 0 else evalArith ⟨state.stxStack.back⟩

end

#eval evalString "1 + 3 + 5 + 7 / 9"

Are there any further optimisations I can make?

[Kenny Lau]

actually i was trying another approach myself

[Jeremy Tan]

can you share it?

[Kenny Lau]

i haven't finished it

[Kenny Lau]

it doesn't work, which confirms my suspicion that you can't run metacode in main-land

[Kenny Lau]

import Mathlib

open Lean Parser Elab Tactic Meta Qq

unsafe def evalRat (code : String) : TermElabM ℚ := do
  let .ok stx := Parser.runParserCategory (← getEnv) `term code | return 67
  let qS ← Term.elabTermAndSynthesize stx (mkConst ``Rat)
  let q ← unsafe evalExpr ℚ (mkConst ``Rat) qS
  return q

/-- Turn a string into an expression, similar to Python's `eval`. -/
elab "evaluate%" code:str : term <= _expectedType => do
  let q ← unsafe evalRat code.getString
  return toExpr q

#check evaluate% "(1 / 3 + 5 - 7 / 9 : ℚ)" -- mkRat 41 9

elab "evaluate_arbitrary%" i:term : term <= _expectedType => do
  let sS ← Term.elabTermAndSynthesize i (mkConst ``Rat)
  let str ← unsafe evalExpr String (mkConst ``String) sS
  let q ← unsafe evalRat str
  return toExpr q

/-- A mapping from `Fin 4` to the four basic arithmetic operations. -/
def opMap : Fin 4 → String
  | 0 => "+"
  | 1 => "-"
  | 2 => "*"
  | 3 => "/"

def w (ops : Fin 4 → Fin 4) : String :=
  s!"(1 {opMap (ops 0)} 3 {opMap (ops 1)} 5 {opMap (ops 2)} 7 {opMap (ops 3)} 9 : ℚ)"

#check evaluate_arbitrary% (w ![3,0,1,3])

def evalWhiteboard (ops : Fin 4 → Fin 4) : ℚ :=
  evaluate_arbitrary% (w ops)

[Kenny Lau]

(kernel) declaration has free variables '_tmp✝'

[Kenny Lau]

or maybe that's not the reason and i missed something

[Kenny Lau]

@Jeremy Tan i think if i start again i would just write a parser myself like a programming exercise, like really working with the string here and not using any meta code at all

[Kenny Lau]

I think that's the only sensible way

[Kenny Lau]

see String.toNat?

[Kenny Lau]

is this agreeable to you?

[Jeremy Tan]

I'm just trying to understand how the working code I posted actually works

[Kenny Lau]

@Jeremy Tan well, run "magically" does the conversion to you in non-metaland from String to Syntax

[Kenny Lau]

then evalArith just parses the syntax manually

[Kenny Lau]

part of the code is also to define the custom syntax category "Arith"

[Kenny Lau]

it restricts the input to natural numbers with +-*/ rather than any possible way to make a rational number

[Kenny Lau]

so in particular mkRat 41 9 will not be valid input

[Kenny Lau]

but it was valid input in the first code you posted, which just uses the biggest syntax category possible, which is term

[Kenny Lau]

I tried to get rid of that big codeblock and just use the usual way to declare syntax, but it gets stuck in a loop for some reason:

import Mathlib

open Lean Parser Elab Tactic Meta Qq

declare_syntax_cat arith
syntax num : arith
syntax arith "+" arith : arith
syntax arith "-" arith : arith
syntax arith "*" arith : arith
syntax arith "/" arith : arith

partial def evalArith : TSyntax `arith → ℚ
  | `(arith| $a:arith + $b:arith) => evalArith a + evalArith b
  | `(arith| $a:arith - $b:arith) => evalArith a - evalArith b
  | `(arith| $a:arith * $b:arith) => evalArith a * evalArith b
  | `(arith| $a:arith / $b:arith) => evalArith a / evalArith b
  | `(arith| $n:num) => n.getNat
  | _ => 0

unsafe def evalRat (s : String) : ℚ :=
  match runParserCategory (unsafeCast ()) `arith s with
  | .error _ => 67
  | .ok stx => evalArith (.mk stx)

-- stuck in a loop, i don't know why
-- #eval evalRat "1 + 2 / 3"

[Robin Arnez]

Well, where does it get the information to run a parser category from? The environment of course... and you didn't provide an environment

[Kenny Lau]

@Robin Arnez but in the solution above, it got away with let env : Environment := unsafeCast (), what's the difference here?

[Robin Arnez]

In the solution above, the parser was run directly with a parser that contained all parsers you needed. However, when you run a parser category, there's no way for it to know the parsers associated to it unless you have an environment

[Kenny Lau]

is there a way to get the parser at that point of the file?

[Robin Arnez]

Well, the parsers that exists already have a problem, which is that they use the category parser for arith, which again needs the environment

[Kenny Lau]

yes, but I want to call the environment at this point of the file, and get a parser out of it, and then use that parser for the rest of the file

[Robin Arnez]

So either you find a way to get an environment with the stuff you need or you need to modify something from above (potentially automatically)

[Jeremy Tan]

Robin Arnez said:

In the solution above, the parser was run directly with a parser that contained all parsers you needed. However, when you run a parser category, there's no way for it to know the parsers associated to it unless you have an environment

Which solution are you referring to with "solution above"?

[Kenny Lau]

the one you posted