From b8d90d77dbd178ac19e4f81565eeb272e7b7ecb4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Sep 2020 20:03:43 -0700 Subject: [PATCH] feat: macro scope as the single mechanism for creating fresh names cc @Kha --- src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/Binders.lean | 8 +++---- src/Lean/Elab/Match.lean | 8 +++---- src/Lean/Elab/Term.lean | 29 ++++++++++-------------- tests/lean/PPRoundtrip.lean.expected.out | 4 ++-- 5 files changed, 23 insertions(+), 28 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index c45e2af19b..639fffc917 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -62,7 +62,7 @@ match arg with ensureArgType f val expectedType private def mkArrow (d b : Expr) : TermElabM Expr := do -n ← mkFreshAnonymousName; +n ← mkFreshUserName; pure $ Lean.mkForall n BinderInfo.default d b /- diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index dbed857e20..84a8e6fd89 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -26,7 +26,7 @@ else /-- Given syntax of the form `ident <|> hole`, return `ident`. If `hole`, then we create a new anonymous name. -/ private def expandBinderIdent (stx : Syntax) : TermElabM Syntax := match_syntax stx with -| `(_) => mkFreshAnonymousIdent stx +| `(_) => mkFreshIdent stx | _ => pure stx /-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name. -/ @@ -205,7 +205,7 @@ private partial def getFunBinderIdsAux? : Bool → Syntax → Array Syntax → T else do (some acc) ← getFunBinderIdsAux? false f acc | pure none; getFunBinderIdsAux? true a acc - | `(_) => do { ident ← mkFreshAnonymousIdent stx; pure (some (acc.push ident)) } + | `(_) => do { ident ← mkFreshIdent stx; pure (some (acc.push ident)) } | `($id:ident) => pure (some (acc.push id)) | _ => pure none @@ -225,7 +225,7 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na let binder := binders.get ⟨i, h⟩; let processAsPattern : Unit → TermElabM (Array Syntax × Syntax × Bool) := fun _ => do { let pattern := binder; - major ← mkFreshAnonymousIdent binder; + major ← mkFreshIdent binder; (binders, newBody, _) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder major (mkHole binder)); newBody ← `(match $major:ident with | $pattern => $newBody); pure (binders, newBody, true) @@ -235,7 +235,7 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na | Syntax.node `Lean.Parser.Term.instBinder _ => expandFunBindersAux body (i+1) (newBinders.push binder) | Syntax.node `Lean.Parser.Term.explicitBinder _ => expandFunBindersAux body (i+1) (newBinders.push binder) | Syntax.node `Lean.Parser.Term.hole _ => do - ident ← mkFreshAnonymousIdent binder; + ident ← mkFreshIdent binder; let type := binder; expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident type) | Syntax.node `Lean.Parser.Term.paren args => diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index f85b3235cc..6dba38e485 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -70,7 +70,7 @@ elabDiscrsWitMatchTypeAux discrStxs expectedType 0 matchType #[] private def mkUserNameFor (e : Expr) : TermElabM Name := match e with | Expr.fvar fvarId _ => do localDecl ← getLocalDecl fvarId; pure localDecl.userName -| _ => withFreshMacroScope do x ← `(x); pure x.getId +| _ => mkFreshUserName private def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptType : Syntax) (expectedType : Expr) : TermElabM (Array Expr × Expr) := let numDiscrs := discrStxs.size; @@ -495,7 +495,8 @@ private partial def withPatternVarsAux {α} (pVars : Array PatternVar) (k : Arra match pVars.get ⟨i, h⟩ with | PatternVar.anonymousVar mvarId => do type ← mkFreshTypeMVar; - withLocalDecl ((`_x).appendIndexAfter i) BinderInfo.default type fun x => + userName ← mkFreshUserName; + withLocalDecl userName BinderInfo.default type fun x => withPatternVarsAux (i+1) (decls.push (PatternVarDecl.anonymousVar mvarId x.fvarId!)) | PatternVar.localVar userName => do type ← mkFreshTypeMVar; @@ -585,8 +586,7 @@ match val? with /- HACK: `fvarId` is not in the scope of `mvarId` If this generates problems in the future, we should update the metavariable declarations. -/ assignExprMVar mvarId (mkFVar fvarId); - -- TODO: use macro scopes for creating userName - let userName := (`_x).appendIndexAfter (s.localDecls.size+1); + userName ← liftM $ mkFreshUserName; let newDecl := LocalDecl.cdecl (arbitrary _) fvarId userName type BinderInfo.default; modify $ fun s => { s with diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 2f86a05329..5708cce7d0 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -135,8 +135,6 @@ structure State := (syntheticMVars : List SyntheticMVarDecl := []) (mvarErrorContexts : List MVarErrorContext := []) (messages : MessageLog := {}) -(instImplicitIdx : Nat := 1) -(anonymousIdx : Nat := 1) (nextMacroScope : Nat := firstFrontendMacroScope + 1) (letRecsToLift : List LetRecToLift := []) @@ -435,28 +433,25 @@ pure e /-- Auxiliary method for creating fresh binder names. Do not confuse with the method for creating fresh free/meta variable ids. -/ -def mkFreshAnonymousName : TermElabM Name := do -s ← get; -let anonymousIdx := s.anonymousIdx; -modify $ fun s => { s with anonymousIdx := s.anonymousIdx + 1 }; -pure $ (`_a).appendIndexAfter anonymousIdx +def mkFreshUserName : TermElabM Name := +withFreshMacroScope do + x ← `(x); + pure x.getId /-- Auxiliary method for creating a `Syntax.ident` containing a fresh name. This method is intended for creating fresh binder names. - It is just a thin layer on top of `mkFreshAnonymousName`. -/ -def mkFreshAnonymousIdent (ref : Syntax) : TermElabM Syntax := do -n ← mkFreshAnonymousName; + It is just a thin layer on top of `mkFreshUserName`. -/ +def mkFreshIdent (ref : Syntax) : TermElabM Syntax := do +n ← mkFreshUserName; pure $ mkIdentFrom ref n /-- - Auxiliary method for creating binder names for local instances. - Users expect them to be named as `_inst_`. -/ -def mkFreshInstanceName : TermElabM Name := do -s ← get; -let instIdx := s.instImplicitIdx; -modify $ fun s => { s with instImplicitIdx := s.instImplicitIdx + 1 }; -pure $ (`_inst).appendIndexAfter instIdx + Auxiliary method for creating binder names for local instances. -/ +def mkFreshInstanceName : TermElabM Name := +withFreshMacroScope do + inst ← `(inst); + pure inst.getId private partial def hasCDot : Syntax → Bool | Syntax.node k args => diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index 0209677c40..d1991c3d03 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/tests/lean/PPRoundtrip.lean.expected.out @@ -18,14 +18,14 @@ fun (a b : Nat) => a fun (a : Nat)(b : Bool) => a fun {a b : Nat} => a typeAs ({α : Type} → α → α) fun {α : Type}(a : α) => a -fun {α : Type}[_inst_1 : HasToString α](a : α) => @HasToString.toString α _inst_1 a +fun {α : Type}[inst : HasToString α](a : α) => @HasToString.toString α inst a (α : Type) → α (α β : Type) → α Type → Type → Type (α : Type) → α → α (α : Type) → (a : α) → Eq a a {α : Type} → α -{α : Type} → [_inst_1 : HasToString α] → α +{α : Type} → [inst : HasToString α] → α 0 1 42