term representation of labeled binary tree

Stream: Is there code for X?

[Asei Inoue]

/-- Binary tree -/
inductive BinTree (α : Type) where
  | empty
  | node (val : α) (left right : BinTree α)
deriving DecidableEq, BEq

notation:max "∅" => BinTree.empty

variable {α : Type}

/-- Leaf of a binary tree -/
def BinTree.leaf (a : α) : BinTree α := .node a ∅ ∅

def BinTree.isEmpty (t : BinTree α) : Bool :=
  match t with
  | empty => true
  | node _ _ _ => false

def BinTree.isLeaf (t : BinTree α) : Bool :=
  match t with
  | empty => false
  | node _ left right =>
    left.isEmpty && right.isEmpty

@[inherit_doc]
notation:max "⟦" x "⟧" => BinTree.leaf x

/- ## Displaying a binary tree -/

protected def BinTree.toString [ToString α] (t : BinTree α) : String :=
  match t with
  | empty => "∅"
  | node val left right =>
    if t.isLeaf then
      toString val
    else
      toString val ++ " * " ++ "(" ++ BinTree.toString left ++ " + " ++ BinTree.toString right ++ ")"

instance [ToString α] : ToString (BinTree α) where
  toString := BinTree.toString

#guard toString ⟦1⟧ = "1"
#guard toString (BinTree.node 1 ⟦2⟧ .empty) = "1 * (2 + ∅)"
#guard toString (BinTree.node 1 ⟦2⟧ ⟦3⟧) = "1 * (2 + 3)"
#guard
  let tree := BinTree.node 1
    (left := BinTree.node 2 ⟦3⟧ ⟦4⟧)
    (right := BinTree.node 5 ⟦6⟧ ⟦7⟧)
  toString tree = "1 * (2 * (3 + 4) + 5 * (6 + 7))"

/- ## Syntax to represent a binary tree -/

/-- Syntax category for constructing a binary tree -/
declare_syntax_cat bintree
syntax "[tree| " bintree "]" : term

/-- Base case: Something like `[tree| 42]` corresponds to a leaf, so it is valid syntax -/
syntax num : bintree

/-- Base case: `[tree| ∅]` corresponds to an empty tree, so it is valid syntax -/
syntax "∅" : bintree

/-- Recursive step -/
syntax num " * " "(" bintree " + " bintree ")" : bintree

#check_failure [tree| 1 * (2 + 3)]
#check_failure [tree| 1 * (2 + ∅)]
#check_failure [tree| 1 * (2 * (3 + 4) + 5 * (6 + 7))]

macro_rules
  | `([tree| ∅]) => `(BinTree.empty)
  | `([tree| $num:num]) => `(BinTree.leaf $num)
  | `([tree| $v:num * ($l + $r)]) => `(BinTree.node $v [tree| $l] [tree| $r])

#guard
  let actual := [tree| 1 * (2 + 3)]
  let expected := BinTree.node 1 ⟦2⟧ ⟦3⟧
  actual = expected

#guard
  let actual := [tree| 12 * (2 + ∅)]
  let expected := BinTree.node 12 ⟦2⟧ ∅
  actual = expected

#guard
  let actual := [tree| 1 * (2 * (3 + 4) + 5 * (6 + 7))]
  let expected := BinTree.node 1
    (left := BinTree.node 2 ⟦3⟧ ⟦4⟧)
    (right := BinTree.node 5 ⟦6⟧ ⟦7⟧)
  actual = expected

/- ## Definition of Repr -/

def BinTree.reprPrec [ToString α] (tree : BinTree α) : String :=
  "[tree| " ++ toString tree ++ "]"

instance [ToString α] : Repr (BinTree α) where
  reprPrec := fun tree _ => BinTree.reprPrec tree

#eval [tree| 1 * (2 + 3)]
#eval [tree| 12 * (2 + ∅)]
#eval [tree| 1 * (2 * (3 + 4) + 5 * (6 + 7))]

[Asei Inoue]

I'm exploring better ways to represent terms of (binary) trees.
Writing tree terms with constructors quickly becomes deeply nested, which hurts readability and ergonomics.
SVGs are pleasant to view but awkward to author.
So I'd like to implement a “term syntax for labeled trees” in Lean.

[Asei Inoue]

The [tree| ... ] syntax defined in the code above works well, but it currently only supports numeric literals.
How can I write a more general macro that also works with other kinds of literals, such as string literals?

[Asei Inoue]

Thank you for advance!

[Aaron Liu]

Asei Inoue said:

The [tree| ... ] syntax defined in the code above works well, but it currently only supports numeric literals.
How can I write a more general macro that also works with other kinds of literals, such as string literals?

Just add in string literals?

[Asei Inoue]

This does not work...

declare_syntax_cat bintree
syntax "[tree| " bintree "]" : term

syntax num : bintree
syntax str : bintree
syntax "∅" : bintree

/-- Recursive step -/
syntax num " * " "(" bintree " + " bintree ")" : bintree
syntax str " * " "(" bintree " + " bintree ")" : bintree

#check_failure [tree| 1 * (2 + 3)]
#check_failure [tree| 1 * (2 + ∅)]
#check_failure [tree| 1 * (2 * (3 + 4) + 5 * (6 + 7))]
#check_failure [tree| 'x'] -- unexpected token error

[Asei Inoue]

@Aaron Liu How to fix this error?

[Henrik Böving]

Your syntax declarations only allow for

#check_failure [tree| "x"]

you'll need to add another syntax for the character literals

[Asei Inoue]

what is the suitable category for character literals?

self resolved

[Asei Inoue]

How to rewrite this macro_rules more simply?

/- ## Syntax to represent a binary tree -/

/-- Syntax category for constructing a binary tree -/
declare_syntax_cat bintree
syntax "[tree| " bintree "]" : term

declare_syntax_cat bintree_label
syntax bintree_label : bintree
syntax num : bintree_label
syntax str : bintree_label
syntax char : bintree_label

/-- Base case: `[tree| ∅]` corresponds to an empty tree, so it is valid syntax -/
syntax "∅" : bintree

/-- Recursive step -/
syntax bintree_label " * " "(" bintree " + " bintree ")" : bintree

#check_failure [tree| 1 * (2 + 3)]
#check_failure [tree| 1 * (2 + ∅)]
#check_failure [tree| 1 * (2 * (3 + 4) + 5 * (6 + 7))]
#check_failure [tree| "x"]
#check_failure [tree| 'x']

macro_rules
  | `([tree| ∅]) => `(BinTree.empty)
  | `([tree| $num:num]) => `(BinTree.leaf $num)
  | `([tree| $str:str]) => `(BinTree.leaf $str)
  | `([tree| $char:char]) => `(BinTree.leaf $char)
  | `([tree| $v:num * ($l + $r)]) => `(BinTree.node $v [tree| $l] [tree| $r])
  | `([tree| $v:str * ($l + $r)]) => `(BinTree.node $v [tree| $l] [tree| $r])
  | `([tree| $v:char * ($l + $r)]) => `(BinTree.node $v [tree| $l] [tree| $r])

[Henrik Böving]

This looks just right really

[Asei Inoue]

I cannot write simple concise rule for bintree_label?

[Asei Inoue]

This is my best attempt:

/- ## Syntax to represent a binary tree -/

/-- Syntax category for constructing a binary tree -/
declare_syntax_cat bintree
syntax "[tree| " bintree "]" : term

declare_syntax_cat bintree_label
syntax bintree_label : bintree
syntax num : bintree_label
syntax str : bintree_label
syntax char : bintree_label

/-- Base case: `[tree| ∅]` corresponds to an empty tree, so it is valid syntax -/
syntax "∅" : bintree

/-- Recursive step -/
syntax bintree_label " * " "(" bintree " + " bintree ")" : bintree

#check_failure [tree| 1 * (2 + 3)]
#check_failure [tree| 1 * (2 + ∅)]
#check_failure [tree| 1 * (2 * (3 + 4) + 5 * (6 + 7))]
#check_failure [tree| "x"]
#check_failure [tree| 'x']

open Lean Macro

def expandLabel (stx : TSyntax `bintree_label) : MacroM (TSyntax `term) := do
  match stx with
  | `(bintree_label| $num:num) => `(term| $num)
  | `(bintree_label| $str:str) => `(term| $str)
  | `(bintree_label| $char:char) => `(term| $char)
  | _ => throwUnsupported

macro_rules
  | `([tree| ∅]) => `(BinTree.empty)
  | `([tree| $label:bintree_label]) => do
    let label ← expandLabel label
    `(BinTree.leaf $label)
  | `([tree| $label:bintree_label * ($l + $r)]) => do
    let label ← expandLabel label
    `(BinTree.node $label [tree| $l] [tree| $r])

[Asei Inoue]

By the way, I want to write term representation syntax for general labeled-trees.

How to fix this error?

/-- Labeled tree -/
inductive Tree (α : Type) where
  /-- Empty tree -/
  | empty
  | node (v : α) (children : List (Tree α))

variable {α : Type}

/-- Leaf (a node with no children) -/
def Tree.leaf (v : α) : Tree α := Tree.node v []

@[inherit_doc]
local notation:max "⟦" v "⟧" => Tree.leaf v

section
-- ## Define syntax for constructing Tree terms

open Lean Macro

/-- Syntax category for labeled trees -/
declare_syntax_cat tree

/-- If `φ` is a `tree` syntax, then `[tree| φ]` represents a labeled tree -/
syntax "[tree| " tree "]" : term

/-- Labels of the tree. We allow numeric literals, string literals, and character literals as labels -/
syntax tree_label := num <|> str <|> char

/-- Base case: expressions like `[tree| 42]` are valid syntax -/
syntax tree_label : tree

/-- Recursive step -/
syntax tree_label " * " "(" sepBy(tree, " + ") ")" : tree

/-- Convert a `tree_label` syntax into a `term` -/
def expandLabel (stx : TSyntax `tree_label) : MacroM (TSyntax `term) :=
  match stx with
  | `(tree_label| $num:num) => `(term| $num)
  | `(tree_label| $str:str) => `(term| $str)
  | `(tree_label| $char:char) => `(term| $char)
  | _ => throwUnsupported

macro_rules
  | `(tree| $label:tree_label) => do
    let v ← expandLabel label
    `(term| Tree.leaf $v)
  | `(tree| $label:tree_label * ($children:tree+*)) => do
    let v ← expandLabel label
    let trees := children.getElems.map (fun x => `(term| [tree| $x]))
    `(term| Tree.node $v $trees)

end

[Asei Inoue]

I think let trees := children.getElems.map (fun x => (term| [tree| $x]))` is not good, but how to fix this?

[Asei Inoue]

Self resolved