From 4a9b598ecde71e58e0b9ad44a2ad63ee22696a8c Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Sun, 16 Apr 2023 17:59:46 +0200 Subject: [PATCH 1/2] Keep track of which variables are shadowed, and make sure shadowed variables are not accessible in quotations --- Qq/Macro.lean | 26 +++++++++++++++++++++++--- examples/shadowing.lean | 13 +++++++++++++ 2 files changed, 36 insertions(+), 3 deletions(-) create mode 100644 examples/shadowing.lean diff --git a/Qq/Macro.lean b/Qq/Macro.lean index 2757b70..57e1b62 100644 --- a/Qq/Macro.lean +++ b/Qq/Macro.lean @@ -206,16 +206,36 @@ def makeDefEq (a b : Expr) : MetaM (Option LocalContext) := do return none def unquoteLCtx : UnquoteM Unit := do + let mut latestIdForName : PersistentHashMap Name FVarId := {} for ldecl in (← getLCtx) do let fv := ldecl.toExpr let ty := ldecl.type + let userName := addDollar ldecl.userName + + /- + Ensure that names which (in the original context) are shadowed by the currently considered + variable are also inaccessible in the quotation context, even if the variable is not added + to the new context + -/ + if let some id := latestIdForName.find? userName then + -- Shadowed names are made inaccessible by making them hygienic + let hygienicName ← MonadQuotation.addMacroScope userName + modify fun s => { s with + unquoted := s.unquoted.modifyLocalDecl id fun shadowed => + if shadowed.userName == userName then + shadowed.setUserName hygienicName + else + shadowed + } + latestIdForName := latestIdForName.insert userName ldecl.fvarId + let whnfTy ← withReducible <| whnf ty if whnfTy.isAppOfArity ``QQ 1 then let qTy := whnfTy.appArg! let newTy ← unquoteExpr qTy modify fun s => { s with unquoted := s.unquoted.addDecl $ - LocalDecl.cdecl ldecl.index ldecl.fvarId (addDollar ldecl.userName) newTy ldecl.binderInfo ldecl.kind + LocalDecl.cdecl ldecl.index ldecl.fvarId userName newTy ldecl.binderInfo ldecl.kind exprBackSubst := s.exprBackSubst.insert fv (.quoted fv) exprSubst := s.exprSubst.insert fv fv } @@ -227,7 +247,7 @@ def unquoteLCtx : UnquoteM Unit := do let eqTy := mkApp3 (.const ``Eq [tyLevel]) ty lhs rhs let unquoted := (← get).unquoted let unquoted := unquoted.addDecl <| - .cdecl ldecl.index ldecl.fvarId (addDollar ldecl.userName) eqTy ldecl.binderInfo ldecl.kind + .cdecl ldecl.index ldecl.fvarId userName eqTy ldecl.binderInfo ldecl.kind let unquoted := (← withUnquotedLCtx do makeDefEq lhs rhs).getD unquoted modify fun s => { s with unquoted @@ -243,7 +263,7 @@ def unquoteLCtx : UnquoteM Unit := do let .succ u ← getLevel ty | pure () let LOption.some inst ← trySynthInstance (mkApp (mkConst ``ToExpr [u]) ty) | pure () modify fun s => { s with - unquoted := s.unquoted.addDecl (ldecl.setUserName (addDollar ldecl.userName)) + unquoted := s.unquoted.addDecl (ldecl.setUserName userName) exprBackSubst := s.exprBackSubst.insert fv (.quoted (mkApp3 (mkConst ``toExpr [u]) ty inst fv)) exprSubst := s.exprSubst.insert fv fv } diff --git a/examples/shadowing.lean b/examples/shadowing.lean new file mode 100644 index 0000000..b3b3d60 --- /dev/null +++ b/examples/shadowing.lean @@ -0,0 +1,13 @@ +import Qq +open Qq + +/- + This fails, the second definition of `n`, which is not of type `Nat`, shadows the first, + `Nat`-typed, definition of `n`. + Even if the second definition is not available inside the quotation (`Nat → Nat` does not implement `ToExpr`) + we don't want `$n` to refer to the shadowed definition, that would be confusing +-/ +example : Q(Nat) := + let n : Nat := 1 + let n : Nat → Nat := fun _ => n + q($n) \ No newline at end of file From 6c2efd088743b196e10c539304d5902383a72ae3 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 13 Dec 2023 18:26:19 +0000 Subject: [PATCH 2/2] fix test --- examples/shadowing.lean | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/examples/shadowing.lean b/examples/shadowing.lean index b3b3d60..5aa6f8f 100644 --- a/examples/shadowing.lean +++ b/examples/shadowing.lean @@ -1,13 +1,31 @@ import Qq open Qq +-- TODO; use Std's `guard_msgs` instead +open Lean.Elab in +/-- `success_if_error% f with "msg"` expects `f` to emit the provided error -/ +elab "success_if_error% " f:term " with " msg:str : term <= expected_type => do + let initMsgs ← modifyGetThe Lean.Core.State fun st => (st.messages, { st with messages := {} }) + let fe ← Term.elabTerm f expected_type + let msgs := (← getThe Lean.Core.State).messages.msgs.filter (·.severity == .error) + modifyThe Lean.Core.State fun st => { st with messages := initMsgs } + match msgs.toList with + | m :: _ => + let ex_msg ← m.data.toString + if ex_msg ≠ msg.getString then + Lean.logErrorAt msg m!"got\n{ex_msg}\nexpected\n{msg}" + | [] => + Lean.logErrorAt f "Elaborated with no error" + return fe + /- - This fails, the second definition of `n`, which is not of type `Nat`, shadows the first, - `Nat`-typed, definition of `n`. + This fails, the second definition of `n`, which is not of type `Nat`, shadows the first, + `Nat`-typed, definition of `n`. Even if the second definition is not available inside the quotation (`Nat → Nat` does not implement `ToExpr`) we don't want `$n` to refer to the shadowed definition, that would be confusing -/ example : Q(Nat) := let n : Nat := 1 + let n : Nat := 2 let n : Nat → Nat := fun _ => n - q($n) \ No newline at end of file + success_if_error% q($n) with "unknown identifier '«$n»'"