Unexpander trouble

Stream: metaprogramming / tactics

[Shreyas Srinivas]

I have a problem with unexpanders when optional syntax is involved. I am writing STLC+integers+addition for a course (disclosure below): In order to simplify including integers, since they come up multiple times I declare the following syntax category:

declare_syntax_cat int
syntax ("-")? num : int
syntax "[Z| " int " ]" : term

When writing the unexpander for my language I include an unexpander for int literals contained in a constructor called IntLit

instance : Coe (TSyntax `int) (TSyntax `expr) where
  coe s := ⟨s.raw⟩
@[app_unexpander Expr.LitInt]
def unexpandLitInt : Unexpander
  | `($_Expr.LitInt [Z| $x:int]) => `([lam| $x])
  | _ => throw ()

Unfortunately this unexpander alone never kicks in. I can write expressions without any int literals and they unexpand very well.

#check [lam| x] -- [lam| "x" ] : _root_.Expr
#check [lam| λ y ↦ y + y + x] -- [lam| λ "y" ↦ "y" + "y" + "x" ] : _root_.Expr
#check [lam| -1] -- Expr.LitInt (-1) : _root_.Expr
-- The last line is not unexpanding into [lam | -1] as it should

I tried the exercise with num literals instead of int for integers (which of course means no negatives), and then the unexpander works perfectly well .

DISCLOSURE:

1. This is derived from the exercise of a Semantics course I am auditing
2. I am not taking this course for grades.
3. The assignments are in Coq. They absolutely don't test my ability to write lean (or Coq) metaprograms. All this stuff is given already. I am writing it in Lean for convenience and for learning. No solutions are included anywhere here.
4. The assignments are not graded. Grading is done through quizzes in the tutorials. The assignment is to help get comfortable with the proofs and Coq is just supposed to be an aide. It is not examined in any way.

[Shreyas Srinivas]

I'd be grateful for any help in this.

[Shreyas Srinivas]

If it helps to post all the code I can create a web editor link as well with the entire file.

[Shreyas Srinivas]

Here's my full code

[Shreyas Srinivas]

(deleted)

[Kyle Miller]

I think the problem isn't optional syntax, but rather that you're matching on [Z| ...] syntax. You can match on $x:num for positive numbers, but there's a subtlety with negative numbers. Here's a solution:

@[app_unexpander Expr.LitInt]
def unexpandLitInt : Unexpander
  | `($_ $x) =>
    match x with
    | `($x:num) => `([lam| $x])
    | `(-$x:num) => `([lam| -$x])
    | _ => throw ()
  | _ => throw ()

The problem with negatives is that ($_ -$x) matches subtraction, not negatives, and ($_ (-$x)) matches only when there are actually parentheses, but parentheses aren't inserted until later.

[Shreyas Srinivas]

Thanks. It works. But I am still puzzled that there should be any confusion over - since I don't have subtraction in my language. Only negation and specifically only for integer literals

[Shreyas Srinivas]

While I am at it, I don't understand why the $_ is needed or what it does. The example in the mpil book doesn't have any underscores there

[Kyle Miller]

$ is for antiquotations inside a quotation, and _ matches everything. Writing $_Expr.LitInt also matches everything, but it gives the matched term the name _Expr.LitInt. Preceding a name with _ makes the linter not complain about an unused variable.

[Kyle Miller]

In your code, you had a [Z| $x:int] pattern, but you don't have any unexpanders/delaborators to represent ints using this syntax, so the unexpander won't ever fire (this syntax never arises). Instead, without such an unexpander, you instead can match on how ints are delaborated.

[Kyle Miller]

Integers are represented as either natural numbers (the num class) or as Neg.neg of a natural number. When you have notation on, then the unexpander will see the unary operator - applied to the num.

set_option pp.notation false
#check (2 : Int) -- 2
#check (-2 : Int) -- Neg.neg 2

[Shreyas Srinivas]

Okay I am beginning to see some light. Another question because it popped up in the example which I have now modified. This is in particular about the val syntax category in which a value is either an integer literal or a lambda abstraction. I want to focus on the literal.

The syntax and macro definitions let me write something like [val| 1] and [val| 100] and automatically parses them to Val.LitIntV 1 and Val.LitIntV respectively. But how would I write a function like fun (n : ℤ) => [val| $n]. Specifically when applied to some integer, say 100, the function will output[val| 100]. My best guess is that I have to take n and construct a NumLit, say n_numlit and return [val| n_numlit]. However the only relevant function I found was mkNumLit which does not take integer values, only string values.

[Shreyas Srinivas]

Currently I am circumventing this trouble by writing the constructors and arguments explicitly, where necessary. This is fine of course, but it means that whenever variables show up and I have to build expressions from the values they get assigned, I am out of my neat little syntax world

[Kyle Miller]

Maybe this?

def mkValOfInt (n : ℤ) : Term := Unhygienic.run <|
  if 0 ≤ n then
    `([val| $(quote n.natAbs)])
  else
    `([val| -$(quote (-n).natAbs)])

[Shreyas Srinivas]

Kyle Miller said:

Maybe this?

def mkValOfInt (n : ℤ) : Term := Unhygienic.run <|
  if 0 ≤ n then
    `([val| $(quote n.natAbs)])
  else
    `([val| -$(quote (-n).natAbs)])

The function itself works. It only works with Lean.Unhygienice.run which I am learning about just now. Thanks :)