From d59f5c2ffadd599a2c24fda535d4364a61350ca5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 1 Dec 2022 10:52:09 +0100 Subject: [PATCH] fix: `binop%` info tree --- src/Lean/Elab/Extra.lean | 84 ++++++++++++---------- src/Lean/Elab/Term.lean | 6 +- tests/lean/binopInfoTree.lean | 7 ++ tests/lean/binopInfoTree.lean.expected.out | 78 ++++++++++++++++++++ 4 files changed, 136 insertions(+), 39 deletions(-) create mode 100644 tests/lean/binopInfoTree.lean create mode 100644 tests/lean/binopInfoTree.lean.expected.out diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index 3d4851f536..6c2a7bd83a 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -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 diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index f03a9dd810..1d7aebf894 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -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. diff --git a/tests/lean/binopInfoTree.lean b/tests/lean/binopInfoTree.lean new file mode 100644 index 0000000000..bd5dbfcbca --- /dev/null +++ b/tests/lean/binopInfoTree.lean @@ -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) diff --git a/tests/lean/binopInfoTree.lean.expected.out b/tests/lean/binopInfoTree.lean.expected.out new file mode 100644 index 0000000000..0bce221527 --- /dev/null +++ b/tests/lean/binopInfoTree.lean.expected.out @@ -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⟩