parsing a DSL

Stream: metaprogramming / tactics

[Paige Thomas]

I'm trying to see if I can use meta programming to parse a first order logic formula, starting here

open Lean Elab

inductive Formula : Type
  | pred_ : String → List String → Formula

syntax (name := pred) str "(" (str ("," str)*)? ")" : term

@[macro pred]
def predMacro : Macro := fun stx =>
match stx with
| `( $p ($vs) ) => `(Formula.pred_ $p $vs)
| _ => Macro.throwUnsupported

#check "P" ()

However, this gives "elaboration function for 'pred' has not been implemented", which seems straightforward, but I'm confused as to why this doesn't work as is.

[Paige Thomas]

(and I'm not sure how to implement one to fix it)

[Mario Carneiro]

your pattern match is not sufficient, you only matched functions with exactly one argument

[Mario Carneiro]

as a result, the macro is going to the throwUnsupported branch, meaning that it is left unelaborated and you get that message

[Paige Thomas]

Thank you.

[Paige Thomas]

Is there a way to code this so that quotations around the strings are not needed?

inductive Formula : Type
  | pred_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  deriving Inhabited, DecidableEq


def Formula.toString : Formula → String
  | pred_ X xs =>
    if xs.isEmpty
    then s! "{X}"
    else s! "({X} {xs})"
  | eq_ x y => s! "({x} = {y})"
  | true_ => "T"
  | false_ => "F"
  | not_ phi => s! "¬ {phi.toString}"
  | imp_ phi psi => s! "({phi.toString} → {psi.toString})"
  | forall_ x phi => s! "(∀ {x}. {phi.toString})"
  | exists_ x phi => s! "(∃ {x}. {phi.toString})"

instance : ToString Formula :=
  { toString := fun (F : Formula) => F.toString }

instance : Repr Formula :=
  { reprPrec := fun (F : Formula) _ => F.toString.toFormat }


declare_syntax_cat formula

syntax str "(" str,* ")" : formula
syntax "(" str "=" str ")" : formula
syntax "T" : formula
syntax "F" : formula
syntax "~" formula : formula
syntax "(" formula "->" formula ")" : formula
syntax "(" "A." str formula ")" : formula
syntax "(" "E." str formula ")" : formula

syntax "[Formula|" formula "]" : term

macro_rules
  | `([Formula| $X:str ( $xs,* )]) => `(Formula.pred_ $X [$xs,*])
  | `([Formula| ( $x:str = $y:str )]) => `(Formula.eq_ $x $y)
  | `([Formula| T]) => `(Formula.true_)
  | `([Formula| F]) => `(Formula.false_)
  | `([Formula| ~ $phi:formula]) => `(Formula.not_ [Formula| $phi])
  | `([Formula| ($phi:formula -> $psi:formula)]) => `(Formula.imp_ [Formula| $phi] [Formula| $psi])
  | `([Formula| ( A. $x $phi)]) => `(Formula.forall_ $x [Formula| $phi])
  | `([Formula| ( E. $x $phi)]) => `(Formula.exists_ $x [Formula| $phi])

#check [Formula| "P" ()]
#check [Formula| "P" ("x")]
#check [Formula| "P" ("x", "y")]
#check [Formula| ( "P" ("x", "y") -> "P" () )]
#check [Formula| ( ~ "P" ("x", "y") -> ("x" = "y") )]
#check [Formula| (A. "x" "P" ("x"))]
#check [Formula| (E. "x" "P" ("x"))]

For example, to have #check [Formula| ( P (x, y) -> P () )] work?

[Damiano Testa]

Can you assume that what is in str is an ident? (This means that it could be a theorem name: roughly, it starts with a letter, consists only of letters, digits, underscore and the odd unicode charater).

[Paige Thomas]

Yes, I think that would work.

[Paige Thomas]

Do you mean something like
| `([Formula| $X:ident ( $xs,* )]) => `(Formula.pred_ $X [$xs,*])
I'm not sure how to convert the $X from an ident to a string.

[Damiano Testa]

If that is allowed, and id is an identifier, then getId gives you a Name and Name.toString converts it into a string.

[Damiano Testa]

So, you could use id.getId.toString.

[Paige Thomas]

If I do

syntax ident "(" str,* ")" : formula
...
  | `([Formula| $X:ident ( $xs,* )]) => `(Formula.pred_ ($X).getId.toString [$xs,*])
...
#check [Formula| P ()]

I get

Formula.pred_ (sorryAx String true) [] : Formula

mathlib-demo.lean:56:17

unknown identifier 'P'

[Damiano Testa]

Let me try to play with it.

[Damiano Testa]

I have not tried all of them, but this seems to work on the first #check:

macro_rules
  | `([Formula| $X:ident ( $xs,* )]) => let Xstr := Lean.Syntax.mkStrLit X.getId.toString; `(Formula.pred_ $Xstr [$xs,*])

[Damiano Testa]

I replaced all strs in your syntax declarations with idents. After that, you convert the ident to an str via Lean.Syntax.mkStrLit X.getId.toString and you pass it back to your Formula.

[Damiano Testa]

I imagine that you could probably set things up to directly use idents and not need to convert into strings, with a little advance planning.

[Paige Thomas]

Beautiful! Thank you!!

[Paige Thomas]

How did you handle the $xs,*?

[Paige Thomas]

Is there a way to map that translation over it?

[Damiano Testa]

Ah, I got lazy and did not undo those: let me have a look!

[Damiano Testa]

Sorry, I have to run now and I have not really had a chance to fix it. The solution is something along these lines, but as is, it does not work:

let xstrs : Lean.Syntax.TSepArray `ident "," := ⟨xs.getElems.map (Lean.Syntax.mkStrLit ·.getId.toString)⟩
let xstrs : List (Lean.TSyntax `term):= (xs.getElems.map (Lean.Syntax.mkStrLit ·.getId.toString)).toList

[Paige Thomas]

Ok, thank you!

[Paige Thomas]

I was wondering if someone might be able to tell me what I am doing wrong here:

import Lean

open Lean Elab Meta


inductive Formula : Type
  | pred_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  deriving Inhabited, DecidableEq


def Formula.toString : Formula → String
  | pred_ X xs =>
    if xs.isEmpty
    then s! "{X}"
    else s! "({X} {xs})"
  | eq_ x y => s! "({x} = {y})"
  | true_ => "T"
  | false_ => "F"
  | not_ phi => s! "¬ {phi.toString}"
  | imp_ phi psi => s! "({phi.toString} → {psi.toString})"
  | forall_ x phi => s! "(∀ {x}. {phi.toString})"
  | exists_ x phi => s! "(∃ {x}. {phi.toString})"

instance : ToString Formula :=
  { toString := fun (F : Formula) => F.toString }

instance : Repr Formula :=
  { reprPrec := fun (F : Formula) _ => F.toString.toFormat }


declare_syntax_cat formula

syntax ident "(" ident,* ")" : formula
syntax "(" ident "=" ident ")" : formula
syntax "T" : formula
syntax "F" : formula
syntax "~" formula : formula
syntax "(" formula "->" formula ")" : formula
syntax "(" "A." ident formula ")" : formula
syntax "(" "E." ident formula ")" : formula


partial def elabFormula : Syntax → MetaM Expr
  | `(formula| $X:ident ($xs,*)) =>
    let X' : Expr := Lean.mkStrLit X.getId.toString;
    let xs' : Array Expr := xs.getElems.map (Lean.mkStrLit ·.getId.toString);
    mkAppM ``Formula.pred_ ((#[X']) ++ xs')

  | `(formula| ($x:ident = $y:ident)) =>
    let x' : Expr := Lean.mkStrLit x.getId.toString;
    let y' : Expr := Lean.mkStrLit y.getId.toString;
    mkAppM ``Formula.eq_ #[x', y']

  | `(formula| T) => mkAppM ``Formula.true_ #[]

  | `(formula| F) => mkAppM ``Formula.false_ #[]

  | `(formula| ~ $phi) => do
    let phi' : Expr ← elabFormula phi;
    mkAppM ``Formula.not_ #[phi']

  | `(formula| ($phi:formula -> $psi:formula)) => do
    let phi' : Expr ← elabFormula phi;
    let psi' : Expr ← elabFormula psi;
    mkAppM ``Formula.imp_ #[phi', psi']

  | `(formula| (A. $x:ident $phi)) => do
    let x' : Expr := Lean.mkStrLit x.getId.toString;
    let phi' : Expr ← elabFormula phi;
    mkAppM ``Formula.forall_ #[x', phi']

  | `(formula| (E. $x:ident $phi)) => do
    let x' : Expr := Lean.mkStrLit x.getId.toString;
    let phi' : Expr ← elabFormula phi;
    mkAppM ``Formula.exists_ #[x', phi']

  | _ => throwUnsupportedSyntax


elab ">>" p:formula "<<" : term => elabFormula p

#check >> P () << works, but #check >> P (x) << gives

application type mismatch
  Formula.pred_ "P" "x"
argument
  "x"
has type
  String : Type
but is expected to have type
  List String : Type

and #check >> ( A. x P () ) << gives

application type mismatch
  Formula.forall_ "x" (Formula.pred_ "P")
argument
  Formula.pred_ "P"
has type
  List String → Formula : Type
but is expected to have type
  Formula : Type

[Jannis Limperg]

In the pred_ case of elabFormula, you construct the application Formula.pred_ X' x1 ... xn where the xi are elements of xs. Instead, you want to turn the list of syntax objects xs into a list literal. Complete code:

import Lean

open Lean Elab Meta

inductive Formula : Type
  | pred_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  deriving Inhabited, DecidableEq, Repr

def Formula.toString : Formula → String
  | pred_ X xs =>
    if xs.isEmpty
    then s! "{X}"
    else s! "({X} {xs})"
  | eq_ x y => s! "({x} = {y})"
  | true_ => "T"
  | false_ => "F"
  | not_ phi => s! "¬ {phi.toString}"
  | imp_ phi psi => s! "({phi.toString} → {psi.toString})"
  | forall_ x phi => s! "(∀ {x}. {phi.toString})"
  | exists_ x phi => s! "(∃ {x}. {phi.toString})"

instance : ToString Formula :=
  { toString := fun (F : Formula) => F.toString }

declare_syntax_cat formula

syntax ident "(" ident,* ")" : formula
syntax "(" ident "=" ident ")" : formula
syntax "T" : formula
syntax "F" : formula
syntax "~" formula : formula
syntax "(" formula "->" formula ")" : formula
syntax "(" "A." ident formula ")" : formula
syntax "(" "E." ident formula ")" : formula


partial def elabFormula : Syntax → MetaM Expr
  | `(formula| $X:ident ($xs,*)) => do
    let X' : Expr := Lean.mkStrLit X.getId.toString;
    let xs' : Array Expr := xs.getElems.map (Lean.mkStrLit ·.getId.toString);
    let xsList ← mkListLit (.const ``String []) xs'.toList
    mkAppM ``Formula.pred_ #[X', xsList]

  | `(formula| ($x:ident = $y:ident)) =>
    let x' : Expr := Lean.mkStrLit x.getId.toString;
    let y' : Expr := Lean.mkStrLit y.getId.toString;
    mkAppM ``Formula.eq_ #[x', y']

  | `(formula| T) => mkAppM ``Formula.true_ #[]

  | `(formula| F) => mkAppM ``Formula.false_ #[]

  | `(formula| ~ $phi) => do
    let phi' : Expr ← elabFormula phi;
    mkAppM ``Formula.not_ #[phi']

  | `(formula| ($phi:formula -> $psi:formula)) => do
    let phi' : Expr ← elabFormula phi;
    let psi' : Expr ← elabFormula psi;
    mkAppM ``Formula.imp_ #[phi', psi']

  | `(formula| (A. $x:ident $phi)) => do
    let x' : Expr := Lean.mkStrLit x.getId.toString;
    let phi' : Expr ← elabFormula phi;
    mkAppM ``Formula.forall_ #[x', phi']

  | `(formula| (E. $x:ident $phi)) => do
    let x' : Expr := Lean.mkStrLit x.getId.toString;
    let phi' : Expr ← elabFormula phi;
    mkAppM ``Formula.exists_ #[x', phi']

  | _ => throwUnsupportedSyntax


elab ">>" p:formula "<<" : term => elabFormula p

#check >> P () <<
#check >> P (x) <<
#check >> ( A. x P () ) <<

Some other suggestions:

• Derive Repr. Repr is supposed to give a string that can be parsed back by Lean, so it's best to derive it. (ToString, on the other hand, is free-form.)
• Use delimiters for your formulas that give an unambiguous parse, e.g. (formula| ...), instead of >> ... <<. The latter can be parsed as a regular Lean term involving the operators >> and <<. It seems to work for the examples, but I wouldn't risk complications later.
• Semicolons in do blocks are unnecessary.

[Paige Thomas]

@Jannis Limperg Thank you!

[Paige Thomas]

I was wondering if someone might know how to make an Expr for Option.none : Option Nat. The #check here gives "incorrect number of universe levels none", which I'm not sure how to interpret.

import Lean

open Lean Elab Meta

inductive Term_ : Type
| Hole : Option Nat → Term_
deriving Inhabited, DecidableEq, Repr

declare_syntax_cat term_

syntax "?" : term_

partial def elabTerm : Syntax → MetaM Expr
  | `(term_| ?) => do
    mkAppM ``Term_.Hole #[mkConst ``Option.none []]

  | _ => throwUnsupportedSyntax


elab "(Term_|" e:term_ ")" : term => elabTerm e

#check (Term_| ?)

[Chris Bailey]

import Lean

open Lean Elab Meta

inductive Term_ : Type
| Hole : Option Nat → Term_
deriving Inhabited, DecidableEq, Repr

declare_syntax_cat term_

syntax "?" : term_

partial def elabTerm : Syntax → MetaM Expr
  | `(term_| ?) => do
    let op ← mkAppOptM ``Option.none #[some (.const ``Nat [])]
    mkAppM ``Term_.Hole #[op]

  | _ => throwUnsupportedSyntax

elab "(Term_|" e:term_ ")" : term => elabTerm e

#check (Term_| ?)

[Chris Bailey]

Option.none needs more of a hint since it's polymorphic and has a universe parameter (it has one implicit type argument), but mkAppM doesn't try to synthesize the implicit for you (per the docstring).

[Paige Thomas]

Is that what the #[some (.const ``Nat [])] is doing?

[Chris Bailey]

Yeah, the dosctring for mkAppOptM explains the general idea in more depth, but it lets you provide the implicits in the array (consider it like @Option.none <arg>)

[Paige Thomas]

Oh, I see.

[Chris Bailey]

Well I guess in this case @Option.none Nat

[Paige Thomas]

Thank you!

[Paige Thomas]

(deleted)

[Paige Thomas]

(deleted)

[Paige Thomas]

I'm a bit confused about this error that shows up on the last line in the example:

import Lean
import Batteries.Tactic.Lint.Frontend
import Mathlib.Util.CompileInductive


set_option autoImplicit false


/--
  The type of formulas.
-/
inductive Formula_ (α : Type) : Type
  | false_ : Formula_ α
  | true_ : Formula_ α
  | atom_ : α → Formula_ α
  | not_ : Formula_ α → Formula_ α
  | and_ : Formula_ α → Formula_ α → Formula_ α
  | or_ : Formula_ α → Formula_ α → Formula_ α
  | imp_ : Formula_ α → Formula_ α → Formula_ α
  | iff_ : Formula_ α → Formula_ α → Formula_ α
  | forall_ : String → Formula_ α → Formula_ α
  | exists_ : String → Formula_ α → Formula_ α
  deriving Inhabited, DecidableEq, Repr

compile_inductive% Formula_


open Lean Elab Meta

declare_syntax_cat formula


syntax "F" : formula
syntax "T" : formula
syntax ident : formula
syntax "~" formula : formula
syntax "(" formula "->" formula ")" : formula
syntax "(" formula "/\\" formula ")" : formula
syntax "(" formula "\\/" formula ")" : formula
syntax "(" formula "<->" formula ")" : formula
syntax "(" "A." ident formula ")" : formula
syntax "(" "E." ident formula ")" : formula


partial def elabFormula : Syntax → MetaM Expr
  | `(formula| F) => mkAppOptM ``Formula_.false_ #[some (.const ``String [])]

  | `(formula| T) => mkAppOptM ``Formula_.true_ #[some (.const ``String [])]

  | `(formula| $a:ident) => do
    let x' : Expr := Lean.mkStrLit a.getId.toString
    mkAppOptM ``Formula_.atom_ #[some (.const ``String []), x']

  | `(formula| ~ $phi) => do
    let phi' : Expr ← elabFormula phi
    mkAppOptM ``Formula_.not_ #[some (.const ``String []), phi']

  | `(formula| ($phi:formula /\ $psi:formula)) => do
    let phi' : Expr ← elabFormula phi
    let psi' : Expr ← elabFormula psi
    mkAppOptM ``Formula_.and_ #[some (.const ``String []), phi', psi']

  | `(formula| ($phi:formula \/ $psi:formula)) => do
    let phi' : Expr ← elabFormula phi
    let psi' : Expr ← elabFormula psi
    mkAppOptM ``Formula_.or_ #[some (.const ``String []), phi', psi']

  | `(formula| ($phi:formula -> $psi:formula)) => do
    let phi' : Expr ← elabFormula phi
    let psi' : Expr ← elabFormula psi
    mkAppOptM ``Formula_.imp_ #[some (.const ``String []), phi', psi']

  | `(formula| ($phi:formula <-> $psi:formula)) => do
    let phi' : Expr ← elabFormula phi
    let psi' : Expr ← elabFormula psi
    mkAppOptM ``Formula_.iff_ #[some (.const ``String []), phi', psi']

  | `(formula| (A. $x:ident $phi)) => do
    let x' : Expr := Lean.mkStrLit x.getId.toString
    let phi' : Expr ← elabFormula phi
    mkAppOptM ``Formula_.forall_ #[some (.const ``String []), x', phi']

  | `(formula| (E. $x:ident $phi)) => do
    let x' : Expr := Lean.mkStrLit x.getId.toString
    let phi' : Expr ← elabFormula phi
    mkAppOptM ``Formula_.exists_ #[some (.const ``String []), x', phi']

  | _ => throwUnsupportedSyntax


elab "(Formula_|" p:formula ")" : term => elabFormula p

#check (Formula_| P )
#check (Formula_| ( A. x P ) )
#check (Formula_| ( A. x (A. y (P <-> Q ) ) ) )


example
  (α : Type)
  (F : Formula_ α) : True := sorry

unexpected token 'F'; expected '_' or identifier

It appears for some reason or another it is viewing the F as the token that would get parsed to Formula_.false_?