max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: handle prec DSL at infixl macro

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-14 15:35:37 -08:00
parent 68f943a753
commit fcaf38d566
3 changed files with 34 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Meta.lean
View file

@ -648,6 +648,10 @@ partial def evalPrec : Syntax → MacroM Nat
macro "evalPrec! " p:prec:max : term => return quote (← evalPrec p)
def evalOptPrec : Option Syntax → MacroM Nat
| some prec => evalPrec prec
| none => return 0
end Lean
namespace Array

6
src/Lean/Elab/Syntax.lean
View file

@ -382,14 +382,12 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
-- TODO: cleanup after we have support for optional syntax at `match_syntax`
@[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
withAttrKindGlobal stx fun stx =>
withAttrKindGlobal stx fun stx => do
match stx with
| `(infix $[: $prec]? $[[$prio]]? $op => $f) => `(infixl $[: $prec]? $[[$prio]]? $op => $f)
| `(infixr $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs $[: $prec]? => $f lhs rhs)
| `(infixl $[: $prec]? $[[$prio]]? $op => $f) =>
let prec1 : Syntax := match (prec : Option Syntax) with
| some prec => quote (prec.toNat+1)
| none => quote 0
let prec1 := quote <| (← evalOptPrec prec) + 1
`(notation $[: $prec]? $[[$prio]]? lhs $op:strLit rhs:$prec1 => $f lhs rhs)
| `(prefix $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? $op:strLit arg $[: $prec]? => $f arg)
| `(postfix $[: $prec]? $[[$prio]]? $op => $f) => `(notation $[: $prec]? $[[$prio]]? arg $op:strLit => $f arg)

28
tests/lean/run/precDSL.lean Normal file
View file

@ -0,0 +1,28 @@
syntax:max "fn " ident "=>" term : term
syntax:(lead+1) "function " ident "=>" term : term
macro_rules
| `(fn $x:ident => $b) => `(fun $x:ident => $b)
| `(function $x:ident => $b) => `(fun $x:ident => $b)
#check id fn x => x + 1
#check id function x => x + 1
macro "addPrec" : prec => `(65)
macro "mulPrec" : prec => `(70)
infix:addPrec " +' " => Nat.add
infix:mulPrec " *' " => Nat.mul
#eval 10 +' 2 *' 3
theorem ex1 : 10 +' 2 *' 3 = 16 :=
rfl
theorem ex2 : 10 + 2 * 3 = 16 :=
rfl
infix:(addPrec-1) " *'' " => Nat.mul
theorem ex3 : 10 +' 2 *'' 3 = 36 :=
rfl