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

fix: binop% info tree

Browse source
This commit is contained in:
Sebastian Ullrich 2022-12-01 10:52:09 +01:00 • committed by Leonardo de Moura
parent 4ec1c10dc0
commit d59f5c2ffa
4 changed files with 136 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

84
src/Lean/Elab/Extra.lean
View file

@ -138,16 +138,17 @@ private inductive Tree where
| term (ref : Syntax) (infoTrees : PersistentArray InfoTree) (val : Expr)
/--
`ref` is the original syntax that expanded into `binop%`.
`macroName` is the `macro_rule` that produce the expansion. We store this information
here to make sure "go to definition" behaves similarly to notation defined without using `binop%` helper elaborator.
-/
| binop (ref : Syntax) (macroName : Name) (lazy : Bool) (f : Expr) (lhs rhs : Tree)
| binop (ref : Syntax) (lazy : Bool) (f : Expr) (lhs rhs : Tree)
/--
`ref` is the original syntax that expanded into `unop%`.
`macroName` is the `macro_rule` that produce the expansion. We store this information
here to make sure "go to definition" behaves similarly to notation defined without using `unop%` helper elaborator.
-/
| unop (ref : Syntax) (macroName : Name) (f : Expr) (arg : Tree)
| unop (ref : Syntax) (f : Expr) (arg : Tree)
/--
Used for assembling the info tree. We store this information
to make sure "go to definition" behaves similarly to notation defined without using `binop%` helper elaborator.
-/
| macroExpansion (macroName : Name) (stx stx' : Syntax) (nested : Tree)
private partial def toTree (s : Syntax) : TermElabM Tree := do
@ -163,32 +164,30 @@ private partial def toTree (s : Syntax) : TermElabM Tree := do
where
go (s : Syntax) := do
match s with
| `(binop% $f $lhs $rhs) => processBinOp (lazy := false) s .anonymous f lhs rhs
| `(binop_lazy% $f $lhs $rhs) => processBinOp (lazy := true) s .anonymous f lhs rhs
| `(unop% $f $arg) => processUnOp s .anonymous f arg
| `(binop% $f $lhs $rhs) => processBinOp (lazy := false) s f lhs rhs
| `(binop_lazy% $f $lhs $rhs) => processBinOp (lazy := true) s f lhs rhs
| `(unop% $f $arg) => processUnOp s f arg
| `(($e)) =>
if hasCDot e then
processLeaf s
else
go e
| _ =>
match (← liftMacroM <| expandMacroImpl? (← getEnv) s) with
| some (macroName, s?) =>
let s' ← liftMacroM <| liftExcept s?
match s' with
| `(binop% $f $lhs $rhs) => processBinOp (lazy := false) s macroName f lhs rhs
| `(binop_lazy% $f $lhs $rhs) => processBinOp (lazy := true) s macroName f lhs rhs
| `(unop% $f $arg) => processUnOp s .anonymous f arg
| _ => processLeaf s
| none => processLeaf s
withRef s do
match (← liftMacroM <| expandMacroImpl? (← getEnv) s) with
| some (macroName, s?) =>
let s' ← liftMacroM <| liftExcept s?
withPushMacroExpansionStack s s' do
return .macroExpansion macroName s s' (← go s')
| none => processLeaf s
processBinOp (ref : Syntax) (declName : Name) (f lhs rhs : Syntax) (lazy : Bool) := do
processBinOp (ref : Syntax) (f lhs rhs : Syntax) (lazy : Bool) := do
let some f ← resolveId? f | throwUnknownConstant f.getId
return .binop (lazy := lazy) ref declName f (← go lhs) (← go rhs)
return .binop (lazy := lazy) ref f (← go lhs) (← go rhs)
processUnOp (ref : Syntax) (declName : Name) (f arg : Syntax) := do
processUnOp (ref : Syntax) (f arg : Syntax) := do
let some f ← resolveId? f | throwUnknownConstant f.getId
return .unop ref declName f (← go arg)
return .unop ref f (← go arg)
processLeaf (s : Syntax) := do
let e ← elabTerm s none
@ -229,8 +228,9 @@ where
go (t : Tree) : StateRefT AnalyzeResult TermElabM Unit := do
unless (← get).hasUncomparable do
match t with
| .binop _ _ _ _ lhs rhs => go lhs; go rhs
| .unop _ _ _ arg => go arg
| .macroExpansion _ _ _ nested => go nested
| .binop _ _ _ lhs rhs => go lhs; go rhs
| .unop _ _ arg => go arg
| .term _ _ val =>
let type ← instantiateMVars (← inferType val)
unless isUnknow type do
@ -256,15 +256,20 @@ private def toExprCore (t : Tree) : TermElabM Expr := do
match t with
| .term _ trees e =>
modifyInfoState (fun s => { s with trees := s.trees ++ trees }); return e
| .binop ref macroName true f lhs rhs =>
withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo macroName ref) do
mkBinOp f (← toExprCore lhs) (← mkFunUnit (← toExprCore rhs))
| .binop ref macroName false f lhs rhs =>
withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo macroName ref) do
mkBinOp f (← toExprCore lhs) (← toExprCore rhs)
| .unop ref macroName f arg =>
withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo macroName ref) do
| .binop ref lazy f lhs rhs =>
withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
let lhs ← toExprCore lhs
let mut rhs ← toExprCore rhs
if lazy then
rhs ← mkFunUnit rhs
mkBinOp f lhs rhs
| .unop ref f arg =>
withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo .anonymous ref) do
mkUnOp f (← toExprCore arg)
| .macroExpansion macroName stx stx' nested =>
withRef stx <| withInfoContext' stx (mkInfo := mkTermInfo macroName stx) do
withMacroExpansion stx stx' do
toExprCore nested
/--
Auxiliary function to decide whether we should coerce `f`'s argument to `maxType` or not.
@ -343,7 +348,7 @@ mutual
where
go (t : Tree) (f? : Option Expr) (lhs : Bool) (isPred : Bool) : TermElabM Tree := do
match t with
| .binop ref macroName lazy f lhs rhs =>
| .binop ref lazy f lhs rhs =>
/-
We only keep applying coercions to `maxType` if `f` is predicate or
`f` has a homogenous instance with `maxType`. See `hasHomogeneousInstance` for additional details.
@ -351,14 +356,14 @@ mutual
Remark: We assume `binrel%` elaborator is only used with homogenous predicates.
-/
if (← pure isPred <||> hasHomogeneousInstance f maxType) then
return .binop ref macroName lazy f (← go lhs f true false) (← go rhs f false false)
return .binop ref lazy f (← go lhs f true false) (← go rhs f false false)
else
let r ← withRef ref <| withInfoContext' ref (mkInfo := mkTermInfo macroName ref) do
let r ← withRef ref do
mkBinOp f (← toExpr lhs none) (← toExpr rhs none)
let infoTrees ← getResetInfoTrees
return .term ref infoTrees r
| .unop ref macroName f arg =>
return .unop ref macroName f (← go arg none false false)
| .unop ref f arg =>
return .unop ref f (← go arg none false false)
| .term ref trees e =>
let type ← instantiateMVars (← inferType e)
trace[Elab.binop] "visiting {e} : {type} =?= {maxType}"
@ -372,6 +377,9 @@ mutual
else
trace[Elab.binop] "added coercion: {e} : {type} => {maxType}"
withRef ref <| return .term ref trees (← mkCoe maxType e)
| .macroExpansion macroName stx stx' nested =>
withRef stx <| withPushMacroExpansionStack stx stx' do
return .macroExpansion macroName stx stx' (← go nested f? lhs isPred)
private partial def toExpr (tree : Tree) (expectedType? : Option Expr) : TermElabM Expr := do
let r ← analyze tree expectedType?
@ -441,7 +449,7 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
-/
let lhs ← withRef stx[2] <| toTree stx[2]
let rhs ← withRef stx[3] <| toTree stx[3]
let tree := .binop (lazy := false) stx .anonymous f lhs rhs
let tree := .binop (lazy := false) stx f lhs rhs
let r ← analyze tree none
trace[Elab.binrel] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"
if r.hasUncomparable || r.max?.isNone then

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

@ -457,9 +457,13 @@ def elabLevel (stx : Syntax) : TermElabM Level :=
liftLevelM <| Level.elabLevel stx
/-- Elaborate `x` with `stx` on the macro stack -/
def withPushMacroExpansionStack (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
/-- Elaborate `x` with `stx` on the macro stack and produce macro expansion info -/
def withMacroExpansion (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α :=
withMacroExpansionInfo beforeStx afterStx do
withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
withPushMacroExpansionStack beforeStx afterStx x
/--
Add the given metavariable to the list of pending synthetic metavariables.

7
tests/lean/binopInfoTree.lean Normal file
View file

@ -0,0 +1,7 @@
notation a " +' " b => a + b
set_option trace.Elab.info true
-- should contain all macro expansions
#check 1 + 2 + 3
-- should propagate through multiple macro expansions
#check fun (n m l : Nat) => (n + (m +' l) : Int)

78
tests/lean/binopInfoTree.lean.expected.out Normal file
View file

@ -0,0 +1,78 @@
[Elab.info] • command @ ⟨3, 0⟩-⟨3, 31⟩ @ Lean.Elab.Command.elabSetOption
• [.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨3, 0⟩-⟨3, 26⟩
• option trace.Elab.info @ ⟨3, 11⟩-⟨3, 26⟩
1 + 2 + 3 : Nat
[Elab.info] • command @ ⟨5, 0⟩-⟨5, 16⟩ @ Lean.Elab.Command.elabCheck
• 1 + 2 + 3 : Nat @ ⟨5, 7⟩-⟨5, 16⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
• Macro expansion
1 + 2 +
3
-- should propagate through multiple macro expansions
===>
binop% HAdd.hAdd✝
(1 + 2)3
-- should propagate through multiple macro expansions
• 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† @ Lean.Elab.Term.Op.elabBinOp
• 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩†
• 1 + 2 : Nat @ ⟨5, 7⟩-⟨5, 12⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
• Macro expansion
1 + 2
===>
binop% HAdd.hAdd✝ 1 2
• 1 + 2 : Nat @ ⟨5, 7⟩†-⟨5, 12⟩†
• [.] `HAdd.hAdd._@.binopInfoTree._hyg.176 : none @ ⟨5, 7⟩†-⟨5, 16⟩†
• [.] `HAdd.hAdd._@.binopInfoTree._hyg.178 : none @ ⟨5, 7⟩†-⟨5, 12⟩†
• 1 : Nat @ ⟨5, 7⟩-⟨5, 8⟩ @ Lean.Elab.Term.elabNumLit
• 2 : Nat @ ⟨5, 11⟩-⟨5, 12⟩ @ Lean.Elab.Term.elabNumLit
• 3 : Nat @ ⟨5, 15⟩-⟨5, 16⟩ @ Lean.Elab.Term.elabNumLit
fun n m l => Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Nat → Nat → Nat → Int
[Elab.info] • command @ ⟨7, 0⟩-⟨7, 48⟩ @ Lean.Elab.Command.elabCheck
• fun n m l =>
Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun
• Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
• [.] `Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
• Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
• n (isBinder := true) : Nat @ ⟨7, 12⟩-⟨7, 13⟩
• Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
• [.] `Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
• Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
• m (isBinder := true) : Nat @ ⟨7, 14⟩-⟨7, 15⟩
• Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent
• [.] `Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩
• Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩
• l (isBinder := true) : Nat @ ⟨7, 16⟩-⟨7, 17⟩
• Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription
• Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ @ Lean.Elab.Term.elabIdent
• [.] `Int : some Sort.{?_uniq} @ ⟨7, 44⟩-⟨7, 47⟩
• Int : Type @ ⟨7, 44⟩-⟨7, 47⟩
• Int.ofNat n +
(Int.ofNat m + Int.ofNat l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2»
• Macro expansion
n + (m +' l)
===>
binop% HAdd.hAdd✝ n(m +' l)
• Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp
• Int.ofNat n + (Int.ofNat m + Int.ofNat l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩†
• [.] `HAdd.hAdd._@.binopInfoTree._hyg.192 : none @ ⟨7, 29⟩†-⟨7, 41⟩†
• n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent
• [.] `n : none @ ⟨7, 29⟩-⟨7, 30⟩
• n : Nat @ ⟨7, 29⟩-⟨7, 30⟩
• Int.ofNat m + Int.ofNat l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1»
• Macro expansion
m +' l
===>
m + l
• Int.ofNat m +
Int.ofNat l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2»
• Macro expansion
m + l
===>
binop% HAdd.hAdd✝ m l
• Int.ofNat m + Int.ofNat l : Int @ ⟨7, 34⟩†-⟨7, 40⟩†
• [.] `HAdd.hAdd._@.binopInfoTree._hyg.196 : none @ ⟨7, 34⟩†-⟨7, 40⟩†
• m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ @ Lean.Elab.Term.elabIdent
• [.] `m : none @ ⟨7, 34⟩-⟨7, 35⟩
• m : Nat @ ⟨7, 34⟩-⟨7, 35⟩
• l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ @ Lean.Elab.Term.elabIdent
• [.] `l : none @ ⟨7, 39⟩-⟨7, 40⟩
• l : Nat @ ⟨7, 39⟩-⟨7, 40⟩