Antiquot parser not working on some tokens.

Stream: lean4

[Paul Mure]

I'm writing a parser using the prattParser function. And some antiquots are giving me an unexpected token error.

import Lean
open Lean Parser

instance : Insert (Name × Parser × Nat) (TokenMap (Parser × Nat)) where
  insert | (n, p, prec), tm => tm.insert n (p, prec)
instance : Singleton (Name × Parser × Nat) (TokenMap (Parser × Nat)) where
  singleton | (n, p, prec) => TokenMap.insert {} n (p, prec)

inductive BinOp
  | pow | mul | div | mod | add | sub
  | land | lor

inductive Exp
  | nat (n : Nat)
  | bool (b : Bool)
  | binOp (op : BinOp) (x y : Exp)

unsafe def pExp : Parser :=
  p
where
  tt   := leading_parser:maxPrec "True"
  ff   := leading_parser:maxPrec "False"
  num  := Parser.numLit
  pow  := trailing_parser:100:101 " ** " >> p 100
  mul  := trailing_parser:90:90 " * " >> p 91
  div  := trailing_parser:90:90 " / " >> p 91
  mod  := trailing_parser:90:90 " % " >> p 91
  add  := trailing_parser:85:85 " + " >> p 86
  sub  := trailing_parser:85:85 " - " >> p 86
  land := trailing_parser:75:75 " and " >> p 76
  lor  := trailing_parser:70:70 " or " >> p 71

  parsingTables := {
    leadingTable := {
      (`True, tt, maxPrec),
      (`False, ff, maxPrec),
      (numLitKind, num, maxPrec)
    },
    trailingTable := {
      (`«**», pow, 100),
      (`«*», mul, 90),
      (`«/», div, 90),
      (`«%», mod, 90),
      (`«+», add, 85),
      (`«-», sub, 85),
      (`and, land, 75),
      (`or, lor, 70)
    },
  }
  pFn :=
    prattParser `exp parsingTables .default (mkAntiquot "exp" `exp false true).fn
  p (prec : Nat := 0) :=
    {fn := adaptCacheableContextFn ({ · with prec }) (withCacheFn `exp pFn)}

partial def eExp : TSyntax `exp → Except String Exp
  | `(pExp.tt| True) => .ok <| .bool true
  | `(pExp.ff| False) => .ok <| .bool false
  | `(pExp.num| $n:num) => .ok <| .nat n.getNat
  | `(pExp| $x:exp * $y:exp) => do .ok (.binOp .mul (← eExp x) (← eExp y))
  | `(pExp| $x:exp / $y:exp) => do .ok (.binOp .div (← eExp x) (← eExp y))
  | `(pExp| $x:exp % $y:exp) => do .ok (.binOp .mod (← eExp x) (← eExp y))
  | `(pExp| $x:exp + $y:exp) => do .ok (.binOp .add (← eExp x) (← eExp y))
  | `(pExp| $x:exp - $y:exp) => do .ok (.binOp .sub (← eExp x) (← eExp y))
  /- These don't work -/
  -- | `(pExp| $b:exp ** $e:exp) => do .ok (.binOp .pow (← eExp b) (← eExp e))
  -- | `(pExp| $x:exp and $y:exp) => do .ok (.binOp .land (← eExp x) (← eExp y))
  -- | `(pExp| $x:exp or $y:exp) => do .ok (.binOp .or (← eExp x) (← eExp y))
  | _ => throw "unsupported"

[Robin Arnez]

You need to add the token table:

private def mkContext (c : ParserContextCore) : ParserContext := by constructor; assumption

unsafe def pExp : Parser where
  fn c s :=
    let tokens := ["True", "False", "$", ":", "**", "*", "/", "%", "+", "-", "and", "or"]
    withResetCacheFn p.fn (mkContext { c with tokens := tokens.foldl (fun ts s => ts.insert s s) .empty }) s
where
...

should do the trick

[Robin Arnez]

Also you should add

(`«$», num, maxPrec)

to the leading table so you don't have to write pExp.num

[Paul Mure]

Oh neat! Thanks. Looks like doing this also work:

  tokens := ["True", "False", "$", ":", "**", "*", "/", "%", "+", "-", "and", "or"]
  p (prec : Nat := 0) := {
    fn := adaptCacheableContextFn ({ · with prec }) (withCacheFn `exp pFn),
    info := {
      collectTokens tokens' :=
        tokens.foldl (fun ts s => ts.insert s) tokens'
    }
  }

Do you know if one way is safer than the other?

[Robin Arnez]

The method you propose is probably safer (since modifying the context is not really intended) but it also has the problem that any other tokens that already exist in the context are preserved. This is probably not an issue though since you're probably going to call the parser directly through .run anyways (where you have control over the token table) and you probably only use it for antiquotations otherwise where additional keywords aren't a big deal.

[Paul Mure]

Thanks as always! Dropping down to this level of the parser is really tricky lol