macro parser for nested lists

Stream: general

[Frederick Pu]

Hi, I've defined nested lists and I'm trying to make a macro parser for it. Any help would be appreciated:

inductive NestedList (α : Type) : Type
| nil : NestedList α  -- []
| cons₁ : α → NestedList α → NestedList α  -- a l => [a, ...l]
| cons₂ : NestedList α → NestedList α → NestedList α -- l₁ l₂ → [l₁, ...l₂]

def aux {α : Type} [ToString α] : NestedList α → String
| NestedList.nil => ""
| NestedList.cons₁ a NestedList.nil => toString a
| NestedList.cons₁ a l => toString a ++ ", " ++ aux l
| NestedList.cons₂ a NestedList.nil => "[" ++ aux a ++ "]"
| NestedList.cons₂ a l => "[" ++ aux a  ++ "]" ++ ", " ++ aux l

instance  {α : Type} [ToString α] : ToString (NestedList α) :=
  ⟨fun x => "[" ++ aux x ++ "]"⟩

def exampleNestedList : NestedList Nat :=
  NestedList.cons₂ (NestedList.cons₁ 1 (NestedList.cons₁ 2 NestedList.nil)) NestedList.nil -- [[1, 2]]

[Kyle Miller]

Here's a solution:

inductive NestedList (α : Type) : Type
| nil : NestedList α  -- []
| cons₁ : α → NestedList α → NestedList α  -- a l => [a, ...l]
| cons₂ : NestedList α → NestedList α → NestedList α -- l₁ l₂ → [l₁, ...l₂]

def aux {α : Type} [ToString α] : NestedList α → String
| NestedList.nil => ""
| NestedList.cons₁ a NestedList.nil => toString a
| NestedList.cons₁ a l => toString a ++ ", " ++ aux l
| NestedList.cons₂ a NestedList.nil => "N[" ++ aux a ++ "]"
| NestedList.cons₂ a l => "N[" ++ aux a  ++ "]" ++ ", " ++ aux l

instance  {α : Type} [ToString α] : ToString (NestedList α) :=
  ⟨fun x => "N[" ++ aux x ++ "]"⟩

def exampleNestedList : NestedList Nat :=
  NestedList.cons₂ (NestedList.cons₁ 1 (NestedList.cons₁ 2 NestedList.nil)) NestedList.nil
#eval exampleNestedList
-- N[N[1, 2]]

syntax "N[" term,* "]" : term

macro_rules
  | `(N[]) => `(NestedList.nil)
  | `(N[N[$xs,*]]) => `(NestedList.cons₂ N[$xs,*] NestedList.nil)
  | `(N[N[$xs,*], $ys,*]) => `(NestedList.cons₂ N[$xs,*] N[$ys,*])
  | `(N[$x]) => `(NestedList.cons₁ $x NestedList.nil)
  | `(N[$x, $xs,*]) => `(NestedList.cons₁ $x N[$xs,*])

#eval N[N[1,2]]
-- N[N[1, 2]]
#eval N[1,N[2,3],4,N[N[5,6],7]]
-- N[1, N[2, 3], 4, N[N[5, 6], 7]]

[Kyle Miller]

The macros need more cases than you think since, for example, case 3 is looking for a , after the first element, but a one-element list doesn't have such a comma.

[Frederick Pu]

tysm