Parsing integer literals

Stream: metaprogramming / tactics

[Josh Cohen]

Given a numeric literal n: TSyntax `num, is there a better way to construct the corresponding Int literal than converting to a Nat and back i.e. .app (.const ``Int.ofNat []) (mkNatLit n.getNat)? I couldn't find a mkIntLit or similar in the prelude.

[Aaron Liu]

probably the Lean.ToExpr instance for Int?

[Bhavik Mehta]

To get the expr for an int, you can use docs#Lean.mkIntLit

[Josh Cohen]

I am trying to solve the opposite problem - to generate an Int from a parsed numeric literal, rather than getting an Expr from an Int. In fact, I think the thing I am missing is not mkIntLit but rather some Int version of Lean.TSyntax.getNat : NumList -> Nat.

[Kenny Lau]

@Josh Cohen note that -37 is not a num so your question is not really well-formed

import Mathlib

namespace Lean.TSyntax

def getInt : Term → Int
  | `(-$n:num) => -n.getNat
  | `($n:num) => n.getNat
  | _ => 0

end Lean.TSyntax

#eval do
  let s : Lean.Term ← `(37)
  Lean.logInfo m!"{s.getInt}"
  let s : Lean.Term ← `(-67)
  Lean.logInfo m!"{s.getInt}"

Also your original problem did ask about getting an Expr... and you said mkIntLit which does exist and is Int -> Expr...?

I am a bit confused about what exactly you're asking for. It would help both of us greatly if you could include some code with a blank that we can fill in. (#mwe)

[Josh Cohen]

Sorry, I don't understand your comment. I didn't mention anything about -37, and every num should be parsable as an int, I would imagine. Here is a mwe:

inductive expr : Type where
  | const : Int -> expr
  | var : String -> expr

def elabExpr : Lean.Syntax → MetaM Expr
  | `(-$n:num) => do return mkAppN (.const ``expr.const []) #[- n.getNat]
  | `($n:num) => do return mkAppN (.const ``expr.const []) #[n.getNat]
  | _ => throwUnsupportedSyntax

I would like to be able to parse the num as Int here, and I am wondering if there is a better way than getNat, followed by mkNatLit, then Int.ofNat.

[Aaron Liu]

But -$n:num is not a num, it's a minus sign (which is a unary operator) followed by a $n:num

[Kenny Lau]

@Josh Cohen well, the better way is to not skip steps, and go from syntax to Int and then to Expr; then you wouldn't have to repeat code for the Int -> Expr part!

[Kenny Lau]

did you see the function I wrote above?