precendence for do style dsls

Stream: general

[Frederick Pu]

I'm trying to make a dsl that piggy backs off of lean's do notation. I'm wondering how I can give it precendence just like do notation. Namely you can write Id.run do .... instead of Id.run (do ...). Here is the code I have so far:

import Lean

open Lean Elab Term
-- Declare syntax categories for cSeq and cItem

declare_syntax_cat cSeq

declare_syntax_cat cItem
-- Syntax for C-style integer declaration (creates a mutable variable)

syntax "int" ident "=" term ";" : cItem

syntax doSeq : cItem -- for debugging purposes only (shouldn't need this once dsl is fully defined)

syntax cItem : cSeq
syntax cItem cSeq : cSeq
syntax "c_do" cSeq : term

macro_rules
| `(c_do int $x:ident = $val; ) => `(do let mut $x := $val)
| `(c_do int $x:ident = $val; $seq:cSeq ) => `(do let mut $x := $val; c_do $seq)
| `(c_do $t:doSeq) => `(do $t)

def womp : Nat := Id.run (c_do int x = 0; return 0)

I want to be able to write Id.run c_do int x = 0; return 0

[Derek Rhodes]

If you're willing to use notation, then I think this may do what you want:

notation:10 "RUN " r:11 => Id.run $ r

def womp' : Nat := RUN c_do int x = 0; return 0

[Frederick Pu]

how does do do it?

[Derek Rhodes]

(the $ probably isn't necessary in the notation)

how does do do it?

Oh that's a good question, I have no idea! :)

[Frederick Pu]

mb we need a wiz like @Kyle Miller

[Frederick Pu]

actually ive switched more this approach

syntax "int" ident "=" term ";" : doElem
syntax "if" "(" term ")" "{" doSeq "}" : doElem
syntax ident "=" term ";" : doElem

macro_rules
  | `(doElem| int $x:ident = $y;) => `(doElem| let mut $x := $y)
  | `(doElem| if ($t:term) {$seq:doSeq}) => `(doElem| if $t then $seq)
  -- unexpected token '='; expected ')'
  | `(doElem| $x:ident = $y;) => `(doElem | $x := $y)

can some one pls explain why $x := $y doesnt work as a doElem?

[Mario Carneiro]

You should have precedences on the syntax declaration, just like in notation

[Mario Carneiro]

the invocation that will give you the same precedence as lean's do is

syntax:arg "c_do" cSeq : term

[Mario Carneiro]

Frederick Pu said:

can some one pls explain why $x := $y doesnt work as a doElem?

you need to give it a "type", $x:ident, because it's inferring $x:doElem which doesn't permit a := after it

[Frederick Pu]

but it's alrady $x:ident in match statement. What's the reason for this?

[Patrick Massot]

That’s the golden rule of antiquotations: if Lean is unhappy, add a type annotation even if it looks obvious.

[Patrick Massot]

They really don’t work like type annotations in ordinary Lean code.

[Mario Carneiro]

Frederick Pu said:

but it's alrady $x:ident in match statement. What's the reason for this?

The parser runs before typechecking, so it does not have the ability to propagate the type information while still parsing the syntax inside the quotation

[Frederick Pu]

but ident is a syntax category right?

[Mario Carneiro]

yes but the fact that x is a binding for an ident in that context is typing information

[Mario Carneiro]

specifically, you can see that x has type TSyntax ident in the context

[Mario Carneiro]

when you use the syntax $x, this is ambiguous to the parser regarding what syntax class it is supposed to be acting like

[Mario Carneiro]

and it would need to know the type of x to get the answer right in all situations

[Mario Carneiro]

so instead it just has a heuristic which is wrong a good chunk of the time

[Mario Carneiro]

in this case that heuristic guesses that $x is a doElem

[Mario Carneiro]

you override the heuristic by using the form $x:cat instead

[Mario Carneiro]

As Patrick says, it's not really a type annotation in the same sense as in regular lean code, because rather than using inference if you don't supply the type it uses a local heuristic (basically it looks at the first syntax category the current parser would consume at this point)

[Frederick Pu]

now im trying to make a macro for for loops. Any way to enforce that the first and second i is the same?

syntax "int" ident "=" term ";" : doElem
syntax "if" "(" term ")" "{" doSeq "}" : doElem
syntax ident "=" term ";" : doElem
syntax "for" "(" "int" ident "=" term ";" ident "<" term ";" ident "++" ")" "{" doSeq "}" : doElem

macro_rules
  | `(doElem| int $x:ident = $y;) => `(doElem| let mut $x := $y)
  | `(doElem| $x:ident = $y;) => `(doElem| $x:ident := $y)
  | `(doElem| if ($t:term) {$seq:doSeq}) => `(doElem| if $t then $seq)
  | `(doElem | for (int $i:ident = $t1:term; $i:ident < $t2:term; $i++){$seq}) => `(doElem| for $i in List.range' $t1 ($t2 - $t1) do $seq)

[Frederick Pu]

i ended up fixing it like this:

syntax "int" ident "=" term ";" : doElem
syntax "if" "(" term ")" "{" doSeq "}" : doElem
syntax ident "=" term ";" : doElem
syntax "for" "(" "int" ident "=" term ";" ident "<" term ";" ident "++" ")" "{" doSeq "}" : doElem

macro_rules
  | `(doElem| int $x:ident = $y;) => `(doElem| let mut $x := $y)
  | `(doElem| $x:ident = $y;) => `(doElem| $x:ident := $y)
  | `(doElem| if ($t:term) {$seq:doSeq}) => `(doElem| if $t then $seq)
  | `(doElem | for (int $i:ident = $t1:term; $i1:ident < $t2:term; $i2++){$seq}) => do
    if i.getId ≠ i1.getId ∨ i1.getId ≠ i2.getId then
      Macro.throwError "i's must match"
    `(doElem| for $i:ident in List.range' $t1 ($t2 - $t1) do $seq)
def womp : Nat := Id.run do
  int x = 10;
  x = x + 1;
  if (x = 30){
    for (int j = 0; j < x; j++){
      x = x + 1;
    }
    return 0;
  }
  return 10
#print womp

how do i make the linter error for unused variable apply all of the j's that occur in the for declaration?
image.png

[Mario Carneiro]

it's easier to do that in an elab rather than a macro. In a macro you can fake it by having some spurious syntax that contains a use of the variable but elaborates to nothing, like haveI := j; e stuck before some subexpression

[Frederick Pu]

can u give an example?

[Mario Carneiro]

something like

    `(doElem| for $i:ident in List.range' $t1 ($t2 - $t1) do let _ := ($i1, $i2); $seq)

[Frederick Pu]

macro_rules
  | `(doElem| int $x:ident = $y;) => `(doElem| let mut $x := $y)
  | `(doElem| $x:ident = $y;) => `(doElem| $x:ident := $y)
  | `(doElem| if ($t:term) {$seq:doSeq}) => `(doElem| if $t then $seq)
  | `(doElem | for (int $i:ident = $t1:term; $i1:ident < $t2:term; $i2++){$seq}) => do
    if i.getId ≠ i1.getId ∨ i1.getId ≠ i2.getId then
      Macro.throwError "i's must match"
    /-
      application type mismatch
        seq.raw
      argument
        seq
      has type
        TSyntax `Lean.Parser.Term.doSeq : Type
      but is expected to have type
        TSyntax `term : Type
      All Messages (4)
    -/
    `(doElem| for $i:ident in List.range' $t1 ($t2 - $t1) do let _ := ($i1, $i2) $seq)

[Mario Carneiro]

semicolon?

[Mario Carneiro]

possibly also nested do

[Mario Carneiro]

like ... do let := ($i1, $i2); do $seq

[Frederick Pu]

what does the second do do?

[Mario Carneiro]

it makes the doSeq into a doElem

[Frederick Pu]

now i get no linter errors at all

[Frederick Pu]

this works better:

macro_rules
  | `(doElem| int $x:ident = $y;) => `(doElem| let mut $x := $y)
  | `(doElem| $x:ident = $y;) => `(doElem| $x:ident := $y)
  | `(doElem| if ($t:term) {$seq:doSeq}) => `(doElem| if $t then $seq)
  | `(doElem | for (int $i:ident = $t1:term; $i1:ident < $t2:term; $i2++){$seq}) => do
    if i.getId ≠ i1.getId ∨ i1.getId ≠ i2.getId then
      Macro.throwError "i's must match"
    `(doElem| for $i:ident in List.range' $t1 ($t2 - $t1) do let $i1 := 0; let $i2 := 0; do $seq)

[Frederick Pu]

i think the issue before is since all three ident are identical so the ident is actually getting used

[Frederick Pu]

image.png

[Frederick Pu]

but that breaks the semantics tho

[Mario Carneiro]

oh, I thought you wanted to get no linter error because it is actually used twice

[Frederick Pu]

hmm i never thought about it like that

[Frederick Pu]

what about this

macro_rules
  | `(doElem| int $x:ident = $y;) => `(doElem| let mut $x := $y)
  | `(doElem| $x:ident = $y;) => `(doElem| $x:ident := $y)
  | `(doElem| if ($t:term) {$seq:doSeq}) => `(doElem| if $t then $seq)
  | `(doElem | for (int $i:ident = $t1:term; $i1:ident < $t2:term; $i2++){$seq}) => do
    if i.getId ≠ i1.getId ∨ i1.getId ≠ i2.getId then
      Macro.throwError "i's must match"
    `(doElem| for x in List.range' $t1 ($t2 - $t1) do let $i := x; let $i1 := x; let $i2 := x; do $seq)

[Frederick Pu]

is the x that i use guaranteed to be a new variable?

[Frederick Pu]

actually it doesnt work cause one of the idents gets shadowed

[Frederick Pu]

image.png

[Frederick Pu]

wait if the idents are considered different then why does your original fix get rid of the linter errors?

[Frederick Pu]

or does the additional let just trick the linter?

[Mario Carneiro]

no, it's not about the idents being different but about what they resolve to. The first i is used as the variable binder, so that's the definition site, and the other two are passed to a let that uses the variable, so those two act as uses of the variable (and e.g. you can ctrl-click on them and jump to the binder use)

[Mario Carneiro]

Frederick Pu said:

is the x that i use guaranteed to be a new variable?

Yes

[Mario Carneiro]

When you use i1 and i2 like that second example, they are not uses of the first variable but fresh binders, so ctrl-clicking on them will do nothing because they are all actually distinct binders, and uses inside the body will resolve to the last one since let $i2 will shadow the let $i and let $i1 binders

[Mario Carneiro]

I'm not sure why the last j is white in the photo though, which indicates that it isn't being used as either a variable binding or a use site

[Mario Carneiro]

There isn't that much magic going on in the first example. It's really just macro expanding to something like

for i in List.range a (b - a) do
  let __x := (i, i)
  ...

and if you were to write that directly, the linter would validly say that the first i is not unused, and the two later occurrences of i would resolve to the first one. The macro is doing exactly the same thing, it's just that the literal spans of the three i identifiers is slightly different in the text

[Frederick Pu]

i think the third one being white was cause i deleted one of the lets

[Frederick Pu]

image.png

[Frederick Pu]

also im not sure what u mean by binder

[Mario Carneiro]

a binder is something that creates a new local variable which has meaning within some scope

[Mario Carneiro]

In your for loop syntax, from the user's perspective, one would expect the first occurrence of j to be a binder and the other two to be a use

[Mario Carneiro]

another way to illustrate the difference between binders and uses is that a binder will not be an error if you put a completely new word that has not been seen in the text before like foobar1, while if you use a new word in a use site it will be an unknown variable error

[Frederick Pu]

so how come the two additional uses of the identifier in the un elaborated macro are associated with the two uses in elaborated result?

[Mario Carneiro]

that's what happens when you use i1 in the macro and embed it in the result. i1 is a Syntax object, and it contains data inside it about where in the source it came from, so that squiggles and hovers generated by the underlying expression eventually get back to the right span of text

[Mario Carneiro]

if you used ($i1, $i1) in the macro expansion instead of ($i1, $i2), then the source idenfifier corresponding to i1 in the text (the j in j < n) would get two type hovers which are the same, and the source identifier corresponding to i2 (the j in j++) would not be colored like a variable and have no type hovers

[Frederick Pu]

also this is kinda unrelated but what is Syntax. and how does the macro elaboration pipeline look like. Are all the syntax parsers parsed first and then whole thing is elaborated?

[Mario Carneiro]

A macro is basically a Syntax -> Syntax function

[Mario Carneiro]

an elab is a Syntax -> Expr function

[Mario Carneiro]

Syntax is the type that the parser produces from the source text, it has information in it about which grammatical constructs are used and where in the file each thing came from

[Frederick Pu]

so what order are all of the macros applied

[Mario Carneiro]

At the top level you have a command syntax object, corresponding to something like a definition or theorem or inductive type declaration. The parser parsed the text expecting a command, and this results in an AST object, that is, Syntax. The head node of that syntax is a grammar constructor produced from a parser such as Lean.Parser.Command.declaration (as a name), and this is the key which is used to look up in a list of elabs and macros. If there are any macros registered for the head symbol then that macro is run and it repeats with the result. If it's an elab then that function is run (in the case of commands it is just executed for effects).

An elab will be passed the input syntax, and will generally pattern match out parts of it and call elabTerm or other things on those AST subnodes in order to get e.g. the type and body of a declaration as Expr. This function in turn checks the head node, runs any macros, and otherwise runs an elab registered for that, which elaborates its subnodes and so on

[Mario Carneiro]

so the TLDR is that macros are run from the outside in

[Mario Carneiro]

and macros take precedence over elabs (but usually there is no overlap)

[Mario Carneiro]

this is also described in the other MIL book

[Frederick Pu]

so during the parser of the command syntax object does it call the parsers for other syntax categories. Or is the entire command syntax object parsed first?

[Mario Carneiro]

the entire command is parsed before any macros/elabs are run

[Mario Carneiro]

but parsing is indeed recursive, a parser for defs will call the parser for terms

[Mario Carneiro]

parser declarations tell you both the head node of the generated syntax tree as well as being functions you call to produce the syntax when some other parser decides it wants to call this one

[Mario Carneiro]

src#Lean.Parser.Command.declaration is a function which calls a bunch of other parsers in order to parse a node which is labeled `Lean.Parser.Command.declaration

[Frederick Pu]

will a parser for term call parser for doElem?

[Mario Carneiro]

term is an extensible grammar category. These work by having an attribute which allow you to register new things into that grammar category and all of them are tried (by some longest match rule) to parse a term. One of the term parsers is src#Lean.Parser.Term.do, which parses do followed by a doSeq, which calls doSeqIndent which calls doSeqItem which calls doElemParser which is the extensible parser for doElems.

[David Thrane Christiansen]

@Frederick Pu You might find it useful to read the manual section on extending Lean

[Frederick Pu]

thx ill take a look