Unverified symbolic calculations in Lean4 using PARI/GP

SymbolicAlgebra.lean

import Lean

open Lean Elab Term Meta Tactic

declare_syntax_cat arith
syntax str : arith
syntax ident : arith
syntax num : arith
syntax arith "+" arith : arith
syntax arith "-" arith : arith
syntax arith "*" arith : arith
syntax arith "/" arith : arith
syntax arith "^" arith : arith
syntax "(" arith ")" : arith

partial def arithToString : TSyntax `arith → String
  | `(arith| $x:str) => x.getString
  | `(arith| $a:ident) => toString a.getId
  | `(arith| $n:num) => toString n.getNat
  | `(arith| $a + $b) => s!"{arithToString a} + {arithToString b}"
  | `(arith| $a - $b) => s!"{arithToString a} - {arithToString b}"
  | `(arith| $a * $b) => s!"{arithToString a} * {arithToString b}"
  | `(arith| $a / $b) => s!"{arithToString a} / {arithToString b}"
  | `(arith| $a ^ $b) => s!"{arithToString a} ^ {arithToString b}"
  | `(arith| ($a)) => s!"({arithToString a})"      
  | _ => panic! "Invalid `arith` syntax"

open IO.Process in -- code by Max Nowak from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/external.20process/near/345090183
/-- Pipe input into stdin of the spawned process, then return output upon completion. -/
def cmd_with_stdin (args : SpawnArgs) (input : String) : IO Output := do
  let child <- spawn { args with stdin := .piped, stdout := .piped, stderr := .piped }
  let (stdin, child) <- child.takeStdin
  stdin.putStr input
  stdin.flush
  let stdout <- IO.asTask child.stdout.readToEnd Task.Priority.dedicated
  let stderr <- child.stderr.readToEnd
  let exitCode <- child.wait
  let stdout <- IO.ofExcept stdout.get
  return { exitCode, stdout, stderr }

def queryPari (a : TSyntax `arith) : IO String := do
  let out ← cmd_with_stdin 
              { cmd := "gp", args := #["-q"]} 
              <| arithToString a
  return out.stdout

elab "#symbolic" e:arith : command => do
  -- dbg_trace (arithToString e)
  let out ← queryPari e
  logInfoAt e out

#symbolic 2 + 2                    -- 4
#symbolic (x ^ 2 - 1) / (x + 1)    -- x - 1
#symbolic (x + 2) * (8 * x + 17)   -- 8*x^2 + 33*x + 34