The q( ) and Q( ) macros

This file provides the main feature of Qq; the q( ) and Q( ) macros, which are available with open scoped Qq.

inductive Qq.Impl.ExprBackSubstResult : Type

• quoted (e : Lean.Expr) : Qq.Impl.ExprBackSubstResult
• unquoted (e : Lean.Expr) : Qq.Impl.ExprBackSubstResult

inductive Qq.Impl.MVarSynth : Type

• term (quotedType : Lean.Expr) (unquotedMVar : Lean.MVarId) : Qq.Impl.MVarSynth
• type (unquotedMVar : Lean.MVarId) : Qq.Impl.MVarSynth
• level (unquotedMVar : Lean.LMVarId) : Qq.Impl.MVarSynth

structure Qq.Impl.UnquoteState : Type

• mvars : List (Lean.Expr × Qq.Impl.MVarSynth)

  Quoted mvars in the outside lctx (of type Level, Quoted _, or Type). The outside mvars can also be of the form ?m x y z.

• levelSubst : Std.HashMap Lean.Expr Lean.Level

  Maps quoted expressions (of type Level) in the old context to level parameter names in the new context

• exprSubst : Std.HashMap Lean.Expr Lean.Expr

  Maps quoted expressions (of type Expr) in the old context to expressions in the new context

• unquoted : Lean.LocalContext

  New unquoted local context

• exprBackSubst : Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult

  Maps free variables in the new context to expressions in the old context (of type Expr)

• levelBackSubst : Std.HashMap Lean.Level Lean.Expr

  Maps free variables in the new context to levels in the old context (of type Level)

• abstractedFVars : Array Lean.FVarId

  New free variables in the new context that were newly introduced for irreducible expressions.

• levelNames : List Lean.Name
• mayPostpone : Bool

@[reducible, inline]

abbrev Qq.Impl.UnquoteM (α : Type) : Type

Equations

• Qq.Impl.UnquoteM = StateT Qq.Impl.UnquoteState Lean.MetaM

@[reducible, inline]

abbrev Qq.Impl.QuoteM (α : Type) : Type

Equations

• Qq.Impl.QuoteM = ReaderT Qq.Impl.UnquoteState Lean.MetaM

instance Qq.Impl.instMonadLiftQuoteMUnquoteM : MonadLift Qq.Impl.QuoteM Qq.Impl.UnquoteM

Equations

• Qq.Impl.instMonadLiftQuoteMUnquoteM = { monadLift := fun {α : Type} (k : Qq.Impl.QuoteM α) => do let __do_lift ← get liftM (k __do_lift) }

def Qq.Impl.determineLocalInstances (lctx : Lean.LocalContext) : Lean.MetaM Lean.LocalInstances

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.withUnquotedLCtx {m : Type → Type u_1} {α : Type} [MonadControlT Lean.MetaM m] [Monad m] [MonadLiftT Qq.Impl.QuoteM m] (k : m α) : m α

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.addDollar : Lean.Name → Lean.Name

Equations

• Qq.Impl.addDollar Lean.Name.anonymous = `«$»
• Qq.Impl.addDollar (Lean.Name.anonymous.str s) = Lean.Name.anonymous.str ("$" ++ s)
• Qq.Impl.addDollar (n.str s) = (Qq.Impl.addDollar n).str s
• Qq.Impl.addDollar (n.num i) = (Qq.Impl.addDollar n).num i

def Qq.Impl.removeDollar : Lean.Name → Option Lean.Name

Equations

• Qq.Impl.removeDollar Lean.Name.anonymous = none
• Qq.Impl.removeDollar `«$» = some Lean.Name.anonymous
• Qq.Impl.removeDollar (Lean.Name.anonymous.str s) = if s.startsWith "$" = true then some (Lean.Name.anonymous.str (s.drop 1)) else none
• Qq.Impl.removeDollar (n.str s) = Option.map (fun (x : Lean.Name) => x.str s) (Qq.Impl.removeDollar n)
• Qq.Impl.removeDollar (n.num i) = Option.map (fun (x : Lean.Name) => x.num i) (Qq.Impl.removeDollar n)

def Qq.Impl.stripDollars : Lean.Name → Lean.Name

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.stripDollars Lean.Name.anonymous = Lean.Name.anonymous
• Qq.Impl.stripDollars (n.str "$") = Qq.Impl.stripDollars n
• Qq.Impl.stripDollars (n.str s) = (Qq.Impl.stripDollars n).str s
• Qq.Impl.stripDollars (n.num i) = (Qq.Impl.stripDollars n).num i

def Qq.Impl.addSyntaxDollar : Lean.Syntax → Lean.Syntax

Equations

• Qq.Impl.addSyntaxDollar (Lean.Syntax.ident info rawVal val preresolved) = Lean.Syntax.ident info rawVal (Qq.Impl.addDollar val) preresolved
• Qq.Impl.addSyntaxDollar x✝ = panicWithPosWithDecl "Qq.Macro" "Qq.Impl.addSyntaxDollar" 104 11 (toString "addSyntaxDollar " ++ toString x✝ ++ toString "")

def Qq.Impl.mkAbstractedLevelName (e : Lean.Expr) : Lean.MetaM Lean.Name

Equations

• Qq.Impl.mkAbstractedLevelName e = do let __do_lift ← Lean.mkFreshId pure (e.getAppFn.constName?.getD `udummy ++ __do_lift)

def Qq.Impl.isAssignablePattern (e : Lean.Expr) : Lean.MetaM Bool

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.isBad (e : Lean.Expr) : Bool

Equations

• One or more equations did not get rendered due to their size.

partial def Qq.Impl.whnf (e : Lean.Expr) (e0 : Lean.Expr := e) : Lean.MetaM Lean.Expr

def Qq.Impl.whnfR (e : Lean.Expr) : Lean.MetaM Lean.Expr

Equations

• Qq.Impl.whnfR e = Lean.Meta.withReducible (Qq.Impl.whnf e)

partial def Qq.Impl.unquoteLevel (e : Lean.Expr) : Qq.Impl.UnquoteM Lean.Level

def Qq.Impl.unquoteLevelMVar (mvar : Lean.Expr) : Qq.Impl.UnquoteM Lean.Level

Equations

• One or more equations did not get rendered due to their size.

partial def Qq.Impl.unquoteLevelList (e : Lean.Expr) : Qq.Impl.UnquoteM (List Lean.Level)

def Qq.Impl.mkAbstractedName (e : Lean.Expr) : Qq.Impl.UnquoteM Lean.Name

Equations

• One or more equations did not get rendered due to their size.

@[inline]

opaque Qq.Impl.betaRev' (e : Lean.Expr) (revArgs : List Lean.Expr) : Lean.Expr

def Qq.Impl.makeZetaReduce (a : Lean.FVarId) (b : Lean.Expr) : Lean.MetaM (Option Lean.LocalContext)

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.makeDefEq (a b : Lean.Expr) : Lean.MetaM (Option Lean.LocalContext)

Equations

• One or more equations did not get rendered due to their size.

partial def Qq.Impl.unquoteExprList (e : Lean.Expr) : Qq.Impl.UnquoteM (List Lean.Expr)

partial def Qq.Impl.unquoteExprMVar (mvar : Lean.Expr) : Qq.Impl.UnquoteM Lean.Expr

partial def Qq.Impl.unquoteExpr (e : Lean.Expr) : Qq.Impl.UnquoteM Lean.Expr

def Qq.Impl.substLevel (a : Lean.Name) (b : Lean.Level) : Qq.Impl.UnquoteM Unit

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.unquoteLevelLCtx (addDefEqs : Bool := true) : Qq.Impl.UnquoteM Unit

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.unquoteLCtx : Qq.Impl.UnquoteM Unit

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.isLevelFVar (n : Lean.Name) : Lean.MetaM (Option Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.quoteLevel : Lean.Level → Qq.Impl.QuoteM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.quoteLevel Lean.Level.zero = pure (Lean.Expr.const `Lean.Level.zero [])
• Qq.Impl.quoteLevel u.succ = do let __do_lift ← Qq.Impl.quoteLevel u pure (Lean.mkApp (Lean.Expr.const `Lean.Level.succ []) __do_lift)
• Qq.Impl.quoteLevel (a.max b) = do let __do_lift ← Qq.Impl.quoteLevel a let __do_lift_1 ← Qq.Impl.quoteLevel b pure (Lean.mkApp2 (Lean.Expr.const `Lean.Level.max []) __do_lift __do_lift_1)
• Qq.Impl.quoteLevel (a.imax b) = do let __do_lift ← Qq.Impl.quoteLevel a let __do_lift_1 ← Qq.Impl.quoteLevel b pure (Lean.mkApp2 (Lean.Expr.const `Lean.Level.imax []) __do_lift __do_lift_1)

def Qq.Impl.quoteLevelList : List Lean.Level → Qq.Impl.QuoteM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Qq.Impl.quoteLevelList [] = pure (Lean.mkApp (Lean.Expr.const `List.nil [Lean.Level.zero]) (Lean.Expr.const `Lean.Level []))

partial def Qq.Impl.quoteExpr : Lean.Expr → Qq.Impl.QuoteM Lean.Expr

def Qq.Impl.unquoteMVarCore (mvar : Lean.Expr) : Qq.Impl.UnquoteM Unit

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.unquoteMVar (mvar : Lean.Expr) : Qq.Impl.UnquoteM Unit

Equations

• Qq.Impl.unquoteMVar mvar = do Qq.Impl.unquoteLCtx Qq.Impl.unquoteMVarCore mvar

def Qq.Impl.MVarSynth.isAssigned : Qq.Impl.MVarSynth → Lean.MetaM Bool

Equations

• (Qq.Impl.MVarSynth.term quotedType newMVar).isAssigned = newMVar.isAssigned
• (Qq.Impl.MVarSynth.type newMVar).isAssigned = newMVar.isAssigned
• (Qq.Impl.MVarSynth.level newMVar).isAssigned = Lean.isLevelMVarAssigned newMVar

def Qq.Impl.MVarSynth.synth : Qq.Impl.MVarSynth → Qq.Impl.QuoteM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• (Qq.Impl.MVarSynth.level newMVar).synth = do let __do_lift ← Lean.instantiateLevelMVars (Lean.Level.mvar newMVar) Qq.Impl.quoteLevel __do_lift

def Qq.Impl.lctxHasMVar : Lean.MetaM Bool

Equations

• Qq.Impl.lctxHasMVar = do let __do_lift ← Lean.getLCtx __do_lift.anyM fun (decl : Lean.LocalDecl) => do let __do_lift ← Lean.instantiateLocalDeclMVars decl pure __do_lift.hasExprMVar

@[specialize #[]]

def Qq.withProcessPostponed {m : Type → Type u_1} {α : Type} [Monad m] [MonadFinally m] [MonadLiftT Lean.MetaM m] (k : m α) : m α

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.UnquoteState.withLevelNames {α : Type} (s : Qq.Impl.UnquoteState) (k : Lean.Elab.TermElabM (α × Array Lean.Name)) : Lean.Elab.TermElabM α

Equations

• One or more equations did not get rendered due to their size.

def Qq.«termQl(_)» : Lean.ParserDescr

ql(u) quotes the universe level u.

Equations

• One or more equations did not get rendered due to their size.

def Qq.«term_=QL_» : Lean.ParserDescr

a =QL b says that the levels a and b are definitionally equal.

Equations

• One or more equations did not get rendered due to their size.

def Qq.Impl.macro (t : Lean.Syntax) (expectedType : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def Qq.«termQ(__)» : Lean.ParserDescr

q(t) quotes the Lean expression t into a Q(α) (if t : α)

Equations

• One or more equations did not get rendered due to their size.

def Qq.«termQ(__)_1» : Lean.ParserDescr

Q(α) is the type of Lean expressions having type α.

Equations

• One or more equations did not get rendered due to their size.

def Qq.«term_=Q_» : Lean.TrailingParserDescr

a =Q b says that a and b are definitionally equal.

Equations

• Qq.«term_=Q_» = Lean.ParserDescr.trailingNode `Qq.«term_=Q_» 1022 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =Q ") (Lean.ParserDescr.cat `term 51))

partial def Qq.Impl.floatLevelAntiquot' {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (stx : Lean.Syntax) : StateT (Array (Lean.Syntax × Lean.Syntax × Lean.Syntax)) m Lean.Syntax

partial def Qq.Impl.floatExprAntiquot' {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (depth : Nat) : Lean.Syntax → StateT (Array (Lean.Syntax × Lean.Syntax × Lean.Syntax)) m Lean.Syntax

def Qq.Impl.floatExprAntiquot {m : Type → Type} [Monad m] [Lean.MonadQuotation m] (depth : Nat) : Lean.Term → StateT (Array (Lean.Ident × Lean.Term × Lean.Term)) m Lean.Term

Equations

• One or more equations did not get rendered due to their size.