clean syntax for initializing associative lists?

Stream: lean4

[Dillon Huff]

I need to initialize some associative lists to test some lean4 code I've been running. I know that if the list is empty you can do:

def mylist : (Std.AssocList Int Int) := {}

But if I want a list with elements in it I don't see another syntax for this (besides actually calling Std.AssocList.cons which is very verbose. Is there something akin to the python map initialization syntax:

def myList : (Std.AssocList Int Int) := { 1 : 2, 3 : 4}

or could I create this via the macro system?

[Leonardo de Moura]

Here is a macro that uses List.toAssocList

import Std

syntax assocEntry := term ":" term
syntax "{" assocEntry,* "}" : term

macro_rules
  | `({ $[$k:term : $v:term],* }) => `([$[($k, $v)],*].toAssocList)

#check { 1 : 2, 3 : 4, 4 : 5 }

Here is one that expands the notation using AssocList.cons and AssocList.nil

import Std

syntax assocEntry := term ":" term
syntax "{" assocEntry,* "}" : term

macro_rules
  | `({ $es:assocEntry,* }) => do
    let r ← `(Std.AssocList.nil)
    es.getElems.foldrM (init := r) fun e r =>
      `(Std.AssocList.cons $(e[0]) $(e[2]) $r)

#check { 1 : 2, 3 : 4, 4 : 5 }

[Dillon Huff]

Thanks! That was just what I was looking for. One clarification: when I copy that code in and #check {} like so:

import Std

syntax assocEntry := term ":" term
syntax "{" assocEntry,* "}" : term

macro_rules
  | `({ $[$k:term : $v:term],* }) => `([$[($k, $v)],*].toAssocList)

#check { 1 : 2, 3 : 4, 4 : 5 }

macro_rules
  | `({ $es:assocEntry,* }) => do
    let r ← `(Std.AssocList.nil)
    es.getElems.foldrM (init := r) fun e r =>
      `(Std.AssocList.cons $(e[0]) $(e[2]) $r)

#check {}

I get an error message from vscode:

ambiguous, possible interpretations
  Std.AssocList.nil

  EmptyCollection.emptyCollectionLean 4 server

Can the macro syntax be tweaked to avoid this?

[Leonardo de Moura]

You can define the notation for non-empty lists only. We have to replace * with +

syntax "{" assocEntry,+ "}" : term

The following still works

#check ({} : Std.AssocList Nat Nat)

because we have the instance

instance : EmptyCollection (AssocList α β)

[Dillon Huff]

Makes sense. Thanks!