From 53276e99dceb35814d4783149631eadacc66ff91 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 13 Dec 2019 14:46:00 +0100 Subject: [PATCH] feat: implement proper macro scope handling for TermElabM --- src/Init/Lean/Elab/Quotation.lean | 36 -------------------------- src/Init/Lean/Elab/Term.lean | 14 ++++++++++- src/Init/Lean/Hygiene.lean | 42 +++++++++++++++++++++++++++++++ 3 files changed, 55 insertions(+), 37 deletions(-) create mode 100644 src/Init/Lean/Hygiene.lean diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean index d0805f526b..5c48c70083 100644 --- a/src/Init/Lean/Elab/Quotation.lean +++ b/src/Init/Lean/Elab/Quotation.lean @@ -11,36 +11,6 @@ import Init.Lean.Parser -- TODO: remove after removing old elaborator namespace Lean -abbrev MacroScope := Nat - -/-- A monad that supports syntax quotations. -/ -class MonadQuotation (m : Type → Type) := --- Get the fresh scope of the current macro invocation -(getCurrMacroScope {} : m MacroScope) --- Execute action in a new macro invocation context -(withFreshMacroScope {α : Type} : m α → m α) -export MonadQuotation - -def addMacroScope (n : Name) (scp : MacroScope) : Name := --- TODO: try harder to avoid clashes with other autogenerated names -mkNameNum n scp - -/-- Simplistic MonadQuotation that does not guarantee globally fresh names. It is only safe - if the syntax quotations do not introduce bindings around antiquotations, and - if references to globals are prefixed with `_root_.`. -/ -abbrev Unhygienic := ReaderT (List Nat) $ StateM Nat -namespace Unhygienic -instance MonadQuotation : MonadQuotation Unhygienic := { - getCurrMacroScope := do - stack ← read; - pure $ stack.head!, - withFreshMacroScope := fun α x => do - fresh ← modifyGet (fun n => (n, n + 1)); - adaptReader (fun stack => fresh::stack) x -} -protected def run {α : Type} (x : Unhygienic α) : α := run x [0] 1 -end Unhygienic - /-- Reflect a runtime datum back to surface syntax (best-effort). -/ class HasQuote (α : Type) := (quote : α → Syntax) @@ -76,12 +46,6 @@ instance Array.HasQuote {α : Type} [HasQuote α] : HasQuote (Array α) := namespace Elab namespace Term -instance TermElabM.MonadQuotation : MonadQuotation TermElabM := { --- FIXME: actually allocate macro scopes when we actually make use of them - getCurrMacroScope := pure 0, - withFreshMacroScope := fun α => id -} - private partial def quoteSyntax {m : Type → Type} [Monad m] [MonadQuotation m] (env : Environment) : Nat → Syntax → m Syntax | _, Syntax.ident info rawVal val preresolved => do -- TODO: pass scope information diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 6d693acd54..364f45dd96 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -7,6 +7,7 @@ prelude import Init.Lean.Util.Sorry import Init.Lean.Structure import Init.Lean.Meta +import Init.Lean.Hygiene import Init.Lean.Elab.Log import Init.Lean.Elab.Alias import Init.Lean.Elab.ResolveName @@ -23,6 +24,7 @@ structure Context extends Meta.Context := (univNames : List Name := []) (openDecls : List OpenDecl := []) (macroStack : List Syntax := []) +(macroScopeStack : List MacroScope := [0]) (mayPostpone : Bool := true) inductive SyntheticMVarKind @@ -39,6 +41,7 @@ structure State extends Meta.State := (messages : MessageLog := {}) (instImplicitIdx : Nat := 1) (anonymousIdx : Nat := 1) +(nextMacroScope : Nat := 1) instance State.inhabited : Inhabited State := ⟨{ env := arbitrary _ }⟩ @@ -52,6 +55,15 @@ instance TermElabM.inhabited {α} : Inhabited (TermElabM α) := instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩ +instance TermElabM.MonadQuotation : MonadQuotation TermElabM := { + getCurrMacroScope := do + ctx ← read; + pure ctx.macroScopeStack.head!, + withFreshMacroScope := fun α x => do + fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 })); + adaptReader (fun (ctx : Context) => { ctx with macroScopeStack := fresh::ctx.macroScopeStack }) x +} + inductive LVal | fieldIdx (i : Nat) | fieldName (name : String) @@ -272,7 +284,7 @@ partial def expandCDotAux : Bool → Syntax → StateT (Array Syntax) TermElabM | _, n => pure n def elabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := -withNode stx $ fun node => do +withFreshMacroScope $ withNode stx $ fun node => do trace! `Elab.step (toString stx); s ← get; let tables := termElabAttribute.ext.getState s.env; diff --git a/src/Init/Lean/Hygiene.lean b/src/Init/Lean/Hygiene.lean new file mode 100644 index 0000000000..00b0f4e2ac --- /dev/null +++ b/src/Init/Lean/Hygiene.lean @@ -0,0 +1,42 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ +prelude +import Init.Control +import Init.Lean.Syntax + +namespace Lean + +abbrev MacroScope := Nat + +/-- A monad that supports syntax quotations. -/ +class MonadQuotation (m : Type → Type) := +-- Get the fresh scope of the current macro invocation +(getCurrMacroScope {} : m MacroScope) +-- Execute action in a new macro invocation context +(withFreshMacroScope {α : Type} : m α → m α) +export MonadQuotation + +def addMacroScope (n : Name) (scp : MacroScope) : Name := +-- TODO: try harder to avoid clashes with other autogenerated names +mkNameNum n scp + +/-- Simplistic MonadQuotation that does not guarantee globally fresh names. It is only safe + if the syntax quotations do not introduce bindings around antiquotations, and + if references to globals are prefixed with `_root_.`. -/ +abbrev Unhygienic := ReaderT (List Nat) $ StateM Nat +namespace Unhygienic +instance MonadQuotation : MonadQuotation Unhygienic := { + getCurrMacroScope := do + stack ← read; + pure stack.head!, + withFreshMacroScope := fun α x => do + fresh ← modifyGet (fun n => (n, n + 1)); + adaptReader (fun stack => fresh::stack) x +} +protected def run {α : Type} (x : Unhygienic α) : α := run x [0] 1 +end Unhygienic + +end Lean