dedb6c2e13
The stack of macro scopes is already implied by the stack of withFreshMacroScope calls, there is no need for an explicit stack. /cc @leodemoura
73 lines
3.5 KiB
Text
73 lines
3.5 KiB
Text
/-
|
||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Sebastian Ullrich
|
||
|
||
Runtime support for making quotation terms auto-hygienic, by mangling identifiers
|
||
introduced by them with a "macro scope" supplied by the context. Details to appear in a
|
||
paper soon.
|
||
-/
|
||
prelude
|
||
import Init.Control
|
||
import Init.Lean.Syntax
|
||
|
||
namespace Lean
|
||
|
||
abbrev MacroScope := Nat
|
||
|
||
/-- A monad that supports syntax quotations. Syntax quotations (in term
|
||
position) are monadic values that when executed retrieve the current "macro
|
||
scope" from the monad and apply it to every identifier they introduce
|
||
(independent of whether this identifier turns out to be a reference to an
|
||
existing declaration, or an actually fresh binding during further
|
||
elaboration). -/
|
||
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. This transformer should be
|
||
used at all places that morally qualify as the beginning of a "macro call",
|
||
e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it
|
||
can also be used internally inside a "macro" if identifiers introduced by
|
||
e.g. different recursive calls should be independent and not collide. While
|
||
returning an intermediate syntax tree that will recursively be expanded by
|
||
the elaborator can be used for the same effect, doing direct recursion inside
|
||
the macro guarded by this transformer is often easier because one is not
|
||
restricted to passing a single syntax tree. Modelling this helper as a
|
||
transformer and not just a monadic action ensures that the current macro
|
||
scope before the recursive call is restored after it, as expected. -/
|
||
(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, that
|
||
is, between different runs of this or other MonadQuotation implementations.
|
||
It is only safe if the syntax quotations do not introduce bindings around
|
||
antiquotations, and if references to globals are prefixed with `_root_.`
|
||
(which is not allowed to refer to a local variable).
|
||
|
||
`Unhygienic` can also be seen as a model implementation of `MonadQuotation`
|
||
(since it is completely hygienic as long as it is "run" only once and can
|
||
assume that there are no other implentations in use, as is the case for the
|
||
elaboration monads that carry their macro scope state through the entire
|
||
processing of a file). It uses the state monad to query and allocate the
|
||
next macro scope, and uses the reader monad to store the stack of scopes
|
||
corresponding to `withFreshMacroScope` calls. -/
|
||
abbrev Unhygienic := ReaderT MacroScope $ StateM MacroScope
|
||
namespace Unhygienic
|
||
instance MonadQuotation : MonadQuotation Unhygienic := {
|
||
getCurrMacroScope := read,
|
||
withFreshMacroScope := fun α x => do
|
||
fresh ← modifyGet (fun n => (n, n + 1));
|
||
adaptReader (fun _ => fresh) x
|
||
}
|
||
protected def run {α : Type} (x : Unhygienic α) : α := run x 0 1
|
||
end Unhygienic
|
||
|
||
instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=
|
||
{ getCurrMacroScope := liftM (getCurrMacroScope : m Nat),
|
||
withFreshMacroScope := fun α => monadMap (fun α => (withFreshMacroScope : m α → m α)) }
|
||
|
||
end Lean
|