max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-26 07:54:11 -07:00
parent cffa3b0039
commit b4e8862716
12 changed files with 947 additions and 955 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

87
src/Lean/Elab/DeclUtil.lean
View file

@ -4,59 +4,61 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Meta.ExprDefEq
namespace Lean.Meta
def forallTelescopeCompatibleAux {α} (k : Array Expr → Expr → Expr → MetaM α) : Nat → Expr → Expr → Array Expr → MetaM α
| 0, type₁, type₂, xs => k xs type₁ type₂
| i+1, type₁, type₂, xs => do
let type₁ ← whnf type₁
let type₂ ← whnf type₂
match type₁, type₂ with
| Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ =>
unless n₁ == n₂ do
throwError! "parameter name mismatch '{n₁}', expected '{n₂}'"
unless (← isDefEq d₁ d₂) do
throwError! "type mismatch at parameter '{n₁}'{indentExpr d₁}\nexpected type{indentExpr d₂}"
unless c₁.binderInfo == c₂.binderInfo do
throwError! "binder annotation mismatch at parameter '{n₁}'"
withLocalDecl n₁ c₁.binderInfo d₁ fun x =>
let type₁ := b₁.instantiate1 x
let type₂ := b₂.instantiate1 x
forallTelescopeCompatibleAux k i type₁ type₂ (xs.push x)
| _, _ => throwError "unexpected number of parameters"
| 0, type₁, type₂, xs => k xs type₁ type₂
| i+1, type₁, type₂, xs => do
let type₁ ← whnf type₁
let type₂ ← whnf type₂
match type₁, type₂ with
| Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ =>
unless n₁ == n₂ do
throwError! "parameter name mismatch '{n₁}', expected '{n₂}'"
unless (← isDefEq d₁ d₂) do
throwError! "type mismatch at parameter '{n₁}'{indentExpr d₁}\nexpected type{indentExpr d₂}"
unless c₁.binderInfo == c₂.binderInfo do
throwError! "binder annotation mismatch at parameter '{n₁}'"
withLocalDecl n₁ c₁.binderInfo d₁ fun x =>
let type₁ := b₁.instantiate1 x
let type₂ := b₂.instantiate1 x
forallTelescopeCompatibleAux k i type₁ type₂ (xs.push x)
| _, _ => throwError "unexpected number of parameters"
/-- Given two forall-expressions `type₁` and `type₂`, ensure the first `numParams` parameters are compatible, and
then execute `k` with the parameters and remaining types. -/
@[inline] def forallTelescopeCompatible {α m} [Monad m] [MonadControlT MetaM m] (type₁ type₂ : Expr) (numParams : Nat) (k : Array Expr → Expr → Expr → m α) : m α :=
controlAt MetaM fun runInBase => forallTelescopeCompatibleAux (fun xs type₁ type₂ => runInBase $ k xs type₁ type₂) numParams type₁ type₂ #[]
controlAt MetaM fun runInBase =>
forallTelescopeCompatibleAux (fun xs type₁ type₂ => runInBase $ k xs type₁ type₂) numParams type₁ type₂ #[]
end Meta
namespace Elab
def expandOptDeclSig (stx : Syntax) : Syntax × Option Syntax :=
-- many Term.bracketedBinder >> Term.optType
let binders := stx[0]
let optType := stx[1] -- optional (parser! " : " >> termParser)
if optType.isNone then
(binders, none)
else
let typeSpec := optType[0]
(binders, some typeSpec[1])
-- many Term.bracketedBinder >> Term.optType
let binders := stx[0]
let optType := stx[1] -- optional (parser! " : " >> termParser)
if optType.isNone then
(binders, none)
else
let typeSpec := optType[0]
(binders, some typeSpec[1])
def expandDeclSig (stx : Syntax) : Syntax × Syntax :=
-- many Term.bracketedBinder >> Term.typeSpec
let binders := stx[0]
let typeSpec := stx[1]
(binders, typeSpec[1])
-- many Term.bracketedBinder >> Term.typeSpec
let binders := stx[0]
let typeSpec := stx[1]
(binders, typeSpec[1])
def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name :=
(env.mainModule ++ `_instance).appendIndexAfter nextIdx
(env.mainModule ++ `_instance).appendIndexAfter nextIdx
def isFreshInstanceName (name : Name) : Bool :=
match name with
| Name.str _ s _ => "_instance".isPrefixOf s
| _ => false
match name with
| Name.str _ s _ => "_instance".isPrefixOf s
| _ => false
/--
Sort the given list of `usedParams` using the following order:
@ -70,13 +72,12 @@ match name with
Remark: `explicitParams` are in reverse declaration order. That is, the head is the last declared parameter. -/
def sortDeclLevelParams (scopeParams : List Name) (allUserParams : List Name) (usedParams : Array Name) : Except String (List Name) :=
match allUserParams.find? $ fun u => !usedParams.contains u && !scopeParams.elem u with
| some u => throw s!"unused universe parameter '{u}'"
| none =>
let result := allUserParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) []
let remaining := usedParams.filter (fun levelParam => !allUserParams.elem levelParam)
let remaining := remaining.qsort Name.lt
pure $ result ++ remaining.toList
match allUserParams.find? $ fun u => !usedParams.contains u && !scopeParams.elem u with
| some u => throw s!"unused universe parameter '{u}'"
| none =>
let result := allUserParams.foldl (fun result levelName => if usedParams.elem levelName then levelName :: result else result) []
let remaining := usedParams.filter (fun levelParam => !allUserParams.elem levelParam)
let remaining := remaining.qsort Name.lt
pure $ result ++ remaining.toList
end Elab
end Lean
end Lean.Elab

15
src/Lean/Elab/Exception.lean
View file

@ -7,28 +7,29 @@ import Lean.InternalExceptionId
import Lean.Meta.Basic
namespace Lean.Elab
builtin_initialize postponeExceptionId : InternalExceptionId ← registerInternalExceptionId `postpone
builtin_initialize unsupportedSyntaxExceptionId : InternalExceptionId ← registerInternalExceptionId `unsupportedSyntax
builtin_initialize abortExceptionId : InternalExceptionId ← registerInternalExceptionId `abortElab
def throwPostpone {α m} [MonadExceptOf Exception m] : m α :=
throw $ Exception.internal postponeExceptionId
throw $ Exception.internal postponeExceptionId
def throwUnsupportedSyntax {α m} [MonadExceptOf Exception m] : m α :=
throw $ Exception.internal unsupportedSyntaxExceptionId
throw $ Exception.internal unsupportedSyntaxExceptionId
def throwIllFormedSyntax {α m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] : m α :=
throwError "ill-formed syntax"
throwError "ill-formed syntax"
def throwAlreadyDeclaredUniverseLevel {α m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (u : Name) : m α :=
throwError! "a universe level named '{u}' has already been declared"
throwError! "a universe level named '{u}' has already been declared"
-- Throw exception to abort elaboration without producing any error message
def throwAbort {α m} [MonadExcept Exception m] : m α :=
throw $ Exception.internal abortExceptionId
throw $ Exception.internal abortExceptionId
def mkMessageCore (fileName : String) (fileMap : FileMap) (msgData : MessageData) (severity : MessageSeverity) (pos : String.Pos) : Message :=
let pos := fileMap.toPosition pos
{ fileName := fileName, pos := pos, data := msgData, severity := severity }
let pos := fileMap.toPosition pos
{ fileName := fileName, pos := pos, data := msgData, severity := severity }
end Lean.Elab

95
src/Lean/Elab/Frontend.lean
View file

@ -8,34 +8,35 @@ import Lean.Elab.Command
import Lean.Util.Profile
namespace Lean.Elab.Frontend
structure State :=
(commandState : Command.State)
(parserState : Parser.ModuleParserState)
(cmdPos : String.Pos)
(commands : Array Syntax := #[])
(commandState : Command.State)
(parserState : Parser.ModuleParserState)
(cmdPos : String.Pos)
(commands : Array Syntax := #[])
structure Context :=
(inputCtx : Parser.InputContext)
(inputCtx : Parser.InputContext)
abbrev FrontendM := ReaderT Context $ StateRefT State IO
def setCommandState (commandState : Command.State) : FrontendM Unit :=
modify fun s => { s with commandState := commandState }
modify fun s => { s with commandState := commandState }
@[inline] def runCommandElabM (x : Command.CommandElabM Unit) : FrontendM Unit := do
let ctx ← read
let s ← get
let cmdCtx : Command.Context := { cmdPos := s.cmdPos, fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap }
let sNew? ← liftM $ EIO.toIO (fun _ => IO.Error.userError "unexpected error") (do (_, s) ← (x cmdCtx).run s.commandState; pure $ some s)
match sNew? with
| some sNew => setCommandState sNew
| none => pure ()
let ctx ← read
let s ← get
let cmdCtx : Command.Context := { cmdPos := s.cmdPos, fileName := ctx.inputCtx.fileName, fileMap := ctx.inputCtx.fileMap }
let sNew? ← liftM $ EIO.toIO (fun _ => IO.Error.userError "unexpected error") (do (_, s) ← (x cmdCtx).run s.commandState; pure $ some s)
match sNew? with
| some sNew => setCommandState sNew
| none => pure ()
def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit := do
runCommandElabM (Command.elabCommand stx)
runCommandElabM (Command.elabCommand stx)
def updateCmdPos : FrontendM Unit := do
modify fun s => { s with cmdPos := s.parserState.pos }
modify fun s => { s with cmdPos := s.parserState.pos }
def getParserState : FrontendM Parser.ModuleParserState := do pure (← get).parserState
def getCommandState : FrontendM Command.State := do pure (← get).commandState
@ -44,53 +45,53 @@ def setMessages (msgs : MessageLog) : FrontendM Unit := modify fun s => { s with
def getInputContext : FrontendM Parser.InputContext := do pure (← read).inputCtx
def processCommand : FrontendM Bool := do
updateCmdPos
let cmdState ← getCommandState
let ictx ← getInputContext
let pstate ← getParserState
let pos := ictx.fileMap.toPosition pstate.pos
match profileit "parsing" pos fun _ => Parser.parseCommand cmdState.env ictx pstate cmdState.messages with
| (cmd, ps, messages) =>
modify fun s => { s with commands := s.commands.push cmd }
setParserState ps
setMessages messages
if Parser.isEOI cmd || Parser.isExitCommand cmd then
pure true -- Done
else
profileitM IO.Error "elaboration" pos $ elabCommandAtFrontend cmd
pure false
updateCmdPos
let cmdState ← getCommandState
let ictx ← getInputContext
let pstate ← getParserState
let pos := ictx.fileMap.toPosition pstate.pos
match profileit "parsing" pos fun _ => Parser.parseCommand cmdState.env ictx pstate cmdState.messages with
| (cmd, ps, messages) =>
modify fun s => { s with commands := s.commands.push cmd }
setParserState ps
setMessages messages
if Parser.isEOI cmd || Parser.isExitCommand cmd then
pure true -- Done
else
profileitM IO.Error "elaboration" pos $ elabCommandAtFrontend cmd
pure false
partial def processCommands : FrontendM Unit := do
let done ← processCommand
unless done do
processCommands
let done ← processCommand
unless done do
processCommands
end Frontend
open Frontend
def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState) (commandState : Command.State) : IO State := do
let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
pure s
let (_, s) ← (Frontend.processCommands.run { inputCtx := inputCtx }).run { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
pure s
def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do
let fileName := fileName.getD "<input>"
let inputCtx := Parser.mkInputContext input fileName
let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
pure (s.commandState.env, s.commandState.messages)
let fileName := fileName.getD "<input>"
let inputCtx := Parser.mkInputContext input fileName
let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
pure (s.commandState.env, s.commandState.messages)
@[export lean_process_input]
def processExport (env : Environment) (input : String) (opts : Options) (fileName : String) : IO (Environment × List Message) := do
let (env, messages) ← process input env opts fileName
pure (env, messages.toList)
let (env, messages) ← process input env opts fileName
pure (env, messages.toList)
@[export lean_run_frontend]
def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) : IO (Environment × List Message × Module) := do
let inputCtx := Parser.mkInputContext input fileName
let (header, parserState, messages) ← Parser.parseHeader inputCtx
let (env, messages) ← processHeader header opts messages inputCtx
let env := env.setMainModule mainModuleName
let s ← IO.processCommands inputCtx parserState (Command.mkState env messages opts)
pure (s.commandState.env, s.commandState.messages.toList, { header := header, commands := s.commands })
let inputCtx := Parser.mkInputContext input fileName
let (header, parserState, messages) ← Parser.parseHeader inputCtx
let (env, messages) ← processHeader header opts messages inputCtx
let env := env.setMainModule mainModuleName
let s ← IO.processCommands inputCtx parserState (Command.mkState env messages opts)
pure (s.commandState.env, s.commandState.messages.toList, { header := header, commands := s.commands })
end Lean.Elab

46
src/Lean/Elab/Import.lean
View file

@ -7,39 +7,39 @@ import Lean.Parser.Module
namespace Lean.Elab
def headerToImports (header : Syntax) : List Import :=
let imports := if header[0].isNone then [{ module := `Init : Import }] else []
imports ++ header[1].getArgs.toList.map fun stx =>
-- `stx` is of the form `(Module.import "import" "runtime"? id)
let runtime := !stx[1].isNone
let id := stx[2].getId
{ module := id, runtimeOnly := runtime }
let imports := if header[0].isNone then [{ module := `Init : Import }] else []
imports ++ header[1].getArgs.toList.map fun stx =>
-- `stx` is of the form `(Module.import "import" "runtime"? id)
let runtime := !stx[1].isNone
let id := stx[2].getId
{ module := id, runtimeOnly := runtime }
def processHeader (header : Syntax) (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0)
: IO (Environment × MessageLog) := do
try
let env ← importModules (headerToImports header) opts trustLevel
pure (env, messages)
catch e =>
let env ← mkEmptyEnvironment
let spos := header.getPos.getD 0
let pos := inputCtx.fileMap.toPosition spos
pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
try
let env ← importModules (headerToImports header) opts trustLevel
pure (env, messages)
catch e =>
let env ← mkEmptyEnvironment
let spos := header.getPos.getD 0
let pos := inputCtx.fileMap.toPosition spos
pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do
let fileName := fileName.getD "<input>"
let inputCtx := Parser.mkInputContext input fileName
let (header, parserState, messages) ← Parser.parseHeader inputCtx
pure (headerToImports header, inputCtx.fileMap.toPosition parserState.pos, messages)
let fileName := fileName.getD "<input>"
let inputCtx := Parser.mkInputContext input fileName
let (header, parserState, messages) ← Parser.parseHeader inputCtx
pure (headerToImports header, inputCtx.fileMap.toPosition parserState.pos, messages)
@[export lean_parse_imports]
def parseImportsExport (input : String) (fileName : Option String) : IO (List Import × Position × List Message) := do
let (imports, pos, log) ← parseImports input fileName
pure (imports, pos, log.toList)
let (imports, pos, log) ← parseImports input fileName
pure (imports, pos, log.toList)
@[export lean_print_deps]
def printDeps (deps : List Import) : IO Unit := do
for dep in deps do
let fname ← findOLean dep.module;
IO.println fname
for dep in deps do
let fname ← findOLean dep.module;
IO.println fname
end Lean.Elab

168
src/Lean/Elab/LetRec.lean
View file

@ -7,106 +7,106 @@ import Lean.Elab.Attributes
import Lean.Elab.Binders
import Lean.Elab.DeclModifiers
import Lean.Elab.SyntheticMVars
namespace Lean.Elab.Term
open Meta
structure LetRecDeclView :=
(ref : Syntax)
(attrs : Array Attribute)
(shortDeclName : Name)
(declName : Name)
(numParams : Nat)
(type : Expr)
(mvar : Expr) -- auxiliary metavariable used to lift the 'let rec'
(valStx : Syntax)
(ref : Syntax)
(attrs : Array Attribute)
(shortDeclName : Name)
(declName : Name)
(numParams : Nat)
(type : Expr)
(mvar : Expr) -- auxiliary metavariable used to lift the 'let rec'
(valStx : Syntax)
structure LetRecView :=
(decls : Array LetRecDeclView)
(body : Syntax)
(decls : Array LetRecDeclView)
(body : Syntax)
/- group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser -/
private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
let decls ← letRec[1].getSepArgs.mapM fun (attrDeclStx : Syntax) => do
let attrOptStx := attrDeclStx[0]
let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
let decl := attrDeclStx[1][0]
if decl.isOfKind `Lean.Parser.Term.letPatDecl then
throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
let shortDeclName := decl[0].getId
let currDeclName? ← getDeclName?
let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
checkNotAlreadyDeclared declName
applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
let binders := decl[1].getArgs
let typeStx := expandOptType decl decl[2]
let (type, numParams) ← elabBinders binders fun xs => do
let type ← elabType typeStx
registerCustomErrorIfMVar type typeStx "failed to infer 'let rec' declaration type"
let type ← mkForallFVars xs type
pure (type, xs.size)
let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
let valStx ←
if decl.isOfKind `Lean.Parser.Term.letIdDecl then
pure decl[4]
else
liftMacroM $ expandMatchAltsIntoMatch decl decl[3]
pure {
ref := decl,
attrs := attrs,
shortDeclName := shortDeclName,
declName := declName,
numParams := numParams,
type := type,
mvar := mvar,
valStx := valStx
: LetRecDeclView }
else
throwUnsupportedSyntax
pure {
decls := decls,
body := letRec[3]
}
let decls ← letRec[1].getSepArgs.mapM fun (attrDeclStx : Syntax) => do
let attrOptStx := attrDeclStx[0]
let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
let decl := attrDeclStx[1][0]
if decl.isOfKind `Lean.Parser.Term.letPatDecl then
throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then
let shortDeclName := decl[0].getId
let currDeclName? ← getDeclName?
let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
checkNotAlreadyDeclared declName
applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration
let binders := decl[1].getArgs
let typeStx := expandOptType decl decl[2]
let (type, numParams) ← elabBinders binders fun xs => do
let type ← elabType typeStx
registerCustomErrorIfMVar type typeStx "failed to infer 'let rec' declaration type"
let type ← mkForallFVars xs type
pure (type, xs.size)
let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
let valStx ←
if decl.isOfKind `Lean.Parser.Term.letIdDecl then
pure decl[4]
else
liftMacroM $ expandMatchAltsIntoMatch decl decl[3]
pure {
ref := decl,
attrs := attrs,
shortDeclName := shortDeclName,
declName := declName,
numParams := numParams,
type := type,
mvar := mvar,
valStx := valStx
: LetRecDeclView }
else
throwUnsupportedSyntax
pure {
decls := decls,
body := letRec[3]
}
private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : Array Expr → TermElabM α) : TermElabM α :=
let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
if h : i < views.size then
let view := views.get ⟨i, h⟩
withLetDecl view.shortDeclName view.type view.mvar fun fvar => loop (i+1) (fvars.push fvar)
else
k fvars
loop 0 #[]
let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
if h : i < views.size then
let view := views.get ⟨i, h⟩
withLetDecl view.shortDeclName view.type view.mvar fun fvar => loop (i+1) (fvars.push fvar)
else
k fvars
loop 0 #[]
private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
view.decls.mapM fun view => do
forallBoundedTelescope view.type view.numParams fun xs type =>
withDeclName view.declName do
let value ← elabTermEnsuringType view.valStx type
mkLambdaFVars xs value
view.decls.mapM fun view => do
forallBoundedTelescope view.type view.numParams fun xs type =>
withDeclName view.declName do
let value ← elabTermEnsuringType view.valStx type
mkLambdaFVars xs value
private def abortIfContainsSyntheticSorry (e : Expr) : TermElabM Unit := do
let e ← instantiateMVars e
if e.hasSyntheticSorry then throwAbort
let e ← instantiateMVars e
if e.hasSyntheticSorry then throwAbort
private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
let lctx ← getLCtx
let localInsts ← getLocalInstances
let toLift := views.mapIdx fun i view => {
ref := view.ref,
fvarId := fvars[i].fvarId!,
attrs := view.attrs,
shortDeclName := view.shortDeclName,
declName := view.declName,
lctx := lctx,
localInstances := localInsts,
type := view.type,
val := values[i],
mvarId := view.mvar.mvarId!
: LetRecToLift }
modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift }
let lctx ← getLCtx
let localInsts ← getLocalInstances
let toLift := views.mapIdx fun i view => {
ref := view.ref,
fvarId := fvars[i].fvarId!,
attrs := view.attrs,
shortDeclName := view.shortDeclName,
declName := view.declName,
lctx := lctx,
localInstances := localInsts,
type := view.type,
val := values[i],
mvarId := view.mvar.mvarId!
: LetRecToLift }
modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift }
@[builtinTermElab «letrec»] def elabLetRec : TermElab :=
fun stx expectedType? => do
@[builtinTermElab «letrec»] def elabLetRec : TermElab := fun stx expectedType? => do
let view ← mkLetRecDeclView stx
withAuxLocalDecls view.decls fun fvars => do
let values ← elabLetRecDeclValues view
@ -114,6 +114,4 @@ fun stx expectedType? => do
registerLetRecsToLift view.decls fvars values
mkLetFVars fvars body
end Term
end Elab
end Lean
end Lean.Elab.Term

103
src/Lean/Elab/Level.lean
View file

@ -10,66 +10,69 @@ import Lean.Elab.Log
namespace Lean.Elab.Level
structure Context :=
(ref : Syntax)
(levelNames : List Name)
(ref : Syntax)
(levelNames : List Name)
structure State :=
(ngen : NameGenerator)
(mctx : MetavarContext)
(ngen : NameGenerator)
(mctx : MetavarContext)
abbrev LevelElabM := ReaderT Context (EStateM Exception State)
instance : Ref LevelElabM :=
{ getRef := do return (← read).ref,
withRef := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x }
instance : Ref LevelElabM := {
getRef := do return (← read).ref,
withRef := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
}
instance : AddMessageContext LevelElabM :=
{ addMessageContext := fun msg => pure msg }
instance : AddMessageContext LevelElabM := {
addMessageContext := fun msg => pure msg
}
instance : MonadNameGenerator LevelElabM :=
{ getNGen := do return (← get).ngen,
setNGen := fun ngen => modify fun s => { s with ngen := ngen } }
instance : MonadNameGenerator LevelElabM := {
getNGen := do return (← get).ngen,
setNGen := fun ngen => modify fun s => { s with ngen := ngen }
}
def mkFreshLevelMVar : LevelElabM Level := do
let mvarId ← mkFreshId
modify fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId }
return mkLevelMVar mvarId
let mvarId ← mkFreshId
modify fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId }
return mkLevelMVar mvarId
partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
let kind := stx.getKind
if kind == `Lean.Parser.Level.paren then
elabLevel (stx.getArg 1)
else if kind == `Lean.Parser.Level.max then
let args := stx.getArg 1 $.getArgs
let lvl ← elabLevel args.back
for arg in args[:args.size-1] do
let arg ← elabLevel arg
lvl := mkLevelMax lvl arg
return lvl
else if kind == `Lean.Parser.Level.imax then
let args := stx.getArg 1 $.getArgs
let lvl ← elabLevel args.back
for arg in args[:args.size-1] do
let arg ← elabLevel arg
lvl := mkLevelIMax lvl arg
return lvl
else if kind == `Lean.Parser.Level.hole then
mkFreshLevelMVar
else if kind == numLitKind then
match stx.isNatLit? with
| some val => return Level.ofNat val
| none => throwIllFormedSyntax
else if kind == identKind then
let paramName := stx.getId
unless (← read).levelNames.contains paramName do
throwError ("unknown universe level " ++ paramName)
return mkLevelParam paramName
else if kind == `Lean.Parser.Level.addLit then
let lvl ← elabLevel (stx.getArg 0)
match stx.getArg 2 $.isNatLit? with
| some val => return lvl.addOffset val
| none => throwIllFormedSyntax
else
throwError "unexpected universe level syntax kind"
let kind := stx.getKind
if kind == `Lean.Parser.Level.paren then
elabLevel (stx.getArg 1)
else if kind == `Lean.Parser.Level.max then
let args := stx.getArg 1 $.getArgs
let lvl ← elabLevel args.back
for arg in args[:args.size-1] do
let arg ← elabLevel arg
lvl := mkLevelMax lvl arg
return lvl
else if kind == `Lean.Parser.Level.imax then
let args := stx.getArg 1 $.getArgs
let lvl ← elabLevel args.back
for arg in args[:args.size-1] do
let arg ← elabLevel arg
lvl := mkLevelIMax lvl arg
return lvl
else if kind == `Lean.Parser.Level.hole then
mkFreshLevelMVar
else if kind == numLitKind then
match stx.isNatLit? with
| some val => return Level.ofNat val
| none => throwIllFormedSyntax
else if kind == identKind then
let paramName := stx.getId
unless (← read).levelNames.contains paramName do
throwError ("unknown universe level " ++ paramName)
return mkLevelParam paramName
else if kind == `Lean.Parser.Level.addLit then
let lvl ← elabLevel (stx.getArg 0)
match stx.getArg 2 $.isNatLit? with
| some val => return lvl.addOffset val
| none => throwIllFormedSyntax
else
throwError "unexpected universe level syntax kind"
end Lean.Elab.Level

69
src/Lean/Elab/Log.lean
View file

@ -9,74 +9,75 @@ import Lean.Elab.Exception
namespace Lean.Elab
class MonadLog (m : Type → Type) :=
(getRef : m Syntax)
(getFileMap : m FileMap)
(getFileName : m String)
(logMessage : Message → m Unit)
(getRef : m Syntax)
(getFileMap : m FileMap)
(getFileName : m String)
(logMessage : Message → m Unit)
instance (m n) [MonadLog m] [MonadLift m n] : MonadLog n :=
{ getRef := liftM (MonadLog.getRef : m _),
instance (m n) [MonadLog m] [MonadLift m n] : MonadLog n := {
getRef := liftM (MonadLog.getRef : m _),
getFileMap := liftM (MonadLog.getFileMap : m _),
getFileName := liftM (MonadLog.getFileName : m _),
logMessage := fun msg => liftM (MonadLog.logMessage msg : m _ ) }
logMessage := fun msg => liftM (MonadLog.logMessage msg : m _ )
}
export MonadLog (getFileMap getFileName logMessage)
variables {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m]
def getRefPos : m String.Pos := do
let ref ← MonadLog.getRef
return ref.getPos.getD 0
let ref ← MonadLog.getRef
return ref.getPos.getD 0
def getRefPosition : m Position := do
let fileMap ← getFileMap
return fileMap.toPosition (← getRefPos)
let fileMap ← getFileMap
return fileMap.toPosition (← getRefPos)
def logAt (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error): m Unit := do
let ref := replaceRef ref (← MonadLog.getRef)
let pos := ref.getPos.getD 0
let fileMap ← getFileMap
let msgData ← addMessageContext msgData
logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, data := msgData, severity := severity }
let ref := replaceRef ref (← MonadLog.getRef)
let pos := ref.getPos.getD 0
let fileMap ← getFileMap
let msgData ← addMessageContext msgData
logMessage { fileName := (← getFileName), pos := fileMap.toPosition pos, data := msgData, severity := severity }
def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
logAt ref msgData MessageSeverity.error
logAt ref msgData MessageSeverity.error
def logWarningAt (ref : Syntax) (msgData : MessageData) : m Unit :=
logAt ref msgData MessageSeverity.warning
logAt ref msgData MessageSeverity.warning
def logInfoAt (ref : Syntax) (msgData : MessageData) : m Unit :=
logAt ref msgData MessageSeverity.information
logAt ref msgData MessageSeverity.information
def log (msgData : MessageData) (severity : MessageSeverity := MessageSeverity.error): m Unit := do
let ref ← MonadLog.getRef
logAt ref msgData severity
let ref ← MonadLog.getRef
logAt ref msgData severity
def logError (msgData : MessageData) : m Unit :=
log msgData MessageSeverity.error
log msgData MessageSeverity.error
def logWarning (msgData : MessageData) : m Unit :=
log msgData MessageSeverity.warning
log msgData MessageSeverity.warning
def logInfo (msgData : MessageData) : m Unit :=
log msgData MessageSeverity.information
log msgData MessageSeverity.information
def logException [MonadIO m] (ex : Exception) : m Unit := do
match ex with
| Exception.error ref msg => logErrorAt ref msg
| Exception.internal id =>
unless id == abortExceptionId do
let name ← liftIO $ id.getName
logError ("internal exception: " ++ name)
match ex with
| Exception.error ref msg => logErrorAt ref msg
| Exception.internal id =>
unless id == abortExceptionId do
let name ← liftIO $ id.getName
logError ("internal exception: " ++ name)
def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
logInfo (MessageData.tagged cls msgData)
logInfo (MessageData.tagged cls msgData)
@[inline] def trace [MonadOptions m] (cls : Name) (msg : Unit → MessageData) : m Unit := do
if checkTraceOption (← getOptions) cls then
logTrace cls (msg ())
if checkTraceOption (← getOptions) cls then
logTrace cls (msg ())
def logDbgTrace [MonadOptions m] (msg : MessageData) : m Unit := do
trace `Elab.debug fun _ => msg
trace `Elab.debug fun _ => msg
end Lean.Elab

104
src/Lean/Elab/Print.lean
View file

@ -9,66 +9,64 @@ import Lean.Elab.Command
namespace Lean.Elab.Command
private def throwUnknownId (id : Name) : CommandElabM Unit :=
throwError! "unknown identifier '{id}'"
throwError! "unknown identifier '{id}'"
private def lparamsToMessageData (lparams : List Name) : MessageData :=
match lparams with
| [] => ""
| u::us => do
let m : MessageData := ".{" ++ u
for u in us do
m := m ++ ", " ++ u
return m ++ "}"
match lparams with
| [] => ""
| u::us => do
let m : MessageData := ".{" ++ u
for u in us do
m := m ++ ", " ++ u
return m ++ "}"
private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData := do
let m : MessageData := if isUnsafe then "unsafe " else ""
let m := if isProtected (← getEnv) id then m ++ "protected " else m
let (m, id) := match privateToUserName? id with
| some id => (m ++ "private ", id)
| none => (m, id)
let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type
pure m
let m : MessageData := if isUnsafe then "unsafe " else ""
let m := if isProtected (← getEnv) id then m ++ "protected " else m
let (m, id) := match privateToUserName? id with
| some id => (m ++ "private ", id)
| none => (m, id)
let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type
pure m
private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (isUnsafe := false) : CommandElabM Unit := do
let m ← mkHeader kind id lparams type isUnsafe
let m := m ++ " :=" ++ Format.line ++ value
logInfo m
let m ← mkHeader kind id lparams type isUnsafe
let m := m ++ " :=" ++ Format.line ++ value
logInfo m
private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
let m ← mkHeader kind id lparams type isUnsafe
logInfo m
logInfo (← mkHeader kind id lparams type isUnsafe)
private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
printAxiomLike "Quotient primitive" id lparams type
printAxiomLike "Quotient primitive" id lparams type
private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
(ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
let m ← mkHeader "inductive" id lparams type isUnsafe
let m := m ++ Format.line ++ "constructors:"
for ctor in ctors do
let cinfo ← getConstInfo ctor
m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
logInfo m
let m ← mkHeader "inductive" id lparams type isUnsafe
let m := m ++ Format.line ++ "constructors:"
for ctor in ctors do
let cinfo ← getConstInfo ctor
m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
logInfo m
private def printIdCore (id : Name) : CommandElabM Unit := do
match (← getEnv).find? id with
| ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
| ConstantInfo.defnInfo { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike "def" id us t v u
| ConstantInfo.thmInfo { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
| ConstantInfo.opaqueInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
| ConstantInfo.quotInfo { kind := kind, lparams := us, type := t, .. } => printQuot kind id us t
| ConstantInfo.ctorInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
| ConstantInfo.recInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
| ConstantInfo.inductInfo { lparams := us, nparams := nparams, nindices := nindices, type := t, ctors := ctors, isUnsafe := u, .. } =>
printInduct id us nparams nindices t ctors u
| none => throwUnknownId id
match (← getEnv).find? id with
| ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
| ConstantInfo.defnInfo { lparams := us, type := t, value := v, isUnsafe := u, .. } => printDefLike "def" id us t v u
| ConstantInfo.thmInfo { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
| ConstantInfo.opaqueInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
| ConstantInfo.quotInfo { kind := kind, lparams := us, type := t, .. } => printQuot kind id us t
| ConstantInfo.ctorInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
| ConstantInfo.recInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
| ConstantInfo.inductInfo { lparams := us, nparams := nparams, nindices := nindices, type := t, ctors := ctors, isUnsafe := u, .. } =>
printInduct id us nparams nindices t ctors u
| none => throwUnknownId id
private def printId (id : Name) : CommandElabM Unit := do
let cs ← resolveGlobalConst id
cs.forM printIdCore
let cs ← resolveGlobalConst id
cs.forM printIdCore
@[builtinCommandElab «print»] def elabPrint : CommandElab :=
fun stx =>
@[builtinCommandElab «print»] def elabPrint : CommandElab := fun stx =>
let numArgs := stx.getNumArgs
if numArgs == 2 then
let arg := stx[1]
@ -83,13 +81,12 @@ fun stx =>
namespace CollectAxioms
structure State :=
(visited : NameSet := {})
(axioms : Array Name := #[])
(visited : NameSet := {})
(axioms : Array Name := #[])
abbrev M := ReaderT Environment $ StateM State
partial def collect : Name → M Unit
| c => do
partial def collect (c : Name) : M Unit := do
let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect
let s ← get
unless s.visited.contains c do
@ -109,15 +106,14 @@ partial def collect : Name → M Unit
end CollectAxioms
private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
let env ← getEnv
let (_, s) := ((CollectAxioms.collect constName).run env).run {}
if s.axioms.isEmpty then
logInfo msg!"'{constName}' does not depend on any axioms"
else
logInfo msg!"'{constName}' depends on axioms: {s.axioms.toList}"
let env ← getEnv
let (_, s) := ((CollectAxioms.collect constName).run env).run {}
if s.axioms.isEmpty then
logInfo msg!"'{constName}' does not depend on any axioms"
else
logInfo msg!"'{constName}' depends on axioms: {s.axioms.toList}"
@[builtinCommandElab «printAxioms»] def elabPrintAxioms : CommandElab :=
fun stx => do
@[builtinCommandElab «printAxioms»] def elabPrintAxioms : CommandElab := fun stx => do
let id := stx[2].getId
let cs ← resolveGlobalConst id
cs.forM printAxiomsOf

425
src/Lean/Elab/Quotation.lean
View file

@ -27,105 +27,106 @@ open Meta
-- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros.
def isEscapedAntiquot (stx : Syntax) : Bool :=
!stx[1].getArgs.isEmpty
!stx[1].getArgs.isEmpty
def unescapeAntiquot (stx : Syntax) : Syntax :=
if isAntiquot stx then
stx.setArg 1 $ mkNullNode stx[1].getArgs.pop
else stx
if isAntiquot stx then
stx.setArg 1 $ mkNullNode stx[1].getArgs.pop
else
stx
def getAntiquotTerm (stx : Syntax) : Syntax :=
let e := stx[2]
if e.isIdent then e
else
-- `e` is from `"(" >> termParser >> ")"`
e[1]
let e := stx[2]
if e.isIdent then e
else
-- `e` is from `"(" >> termParser >> ")"`
e[1]
def antiquotKind? : Syntax → Option SyntaxNodeKind
| Syntax.node (Name.str k "antiquot" _) args =>
if args[3].isOfKind `antiquotName then some k
else
-- we treat all antiquotations where the kind was left implicit (`$e`) the same (see `elimAntiquotChoices`)
some Name.anonymous
| _ => none
| Syntax.node (Name.str k "antiquot" _) args =>
if args[3].isOfKind `antiquotName then some k
else
-- we treat all antiquotations where the kind was left implicit (`$e`) the same (see `elimAntiquotChoices`)
some Name.anonymous
| _ => none
-- `$e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes
def isAntiquotSplice (stx : Syntax) : Bool :=
isAntiquot stx && stx[4].getOptional?.isSome
isAntiquot stx && stx[4].getOptional?.isSome
-- If any item of a `many` node is an antiquotation splice, its result should
-- be substituted into the `many` node's children
def isAntiquotSplicePat (stx : Syntax) : Bool :=
stx.isOfKind nullKind && stx.getArgs.any fun arg => isAntiquotSplice arg && !isEscapedAntiquot arg
stx.isOfKind nullKind && stx.getArgs.any fun arg => isAntiquotSplice arg && !isEscapedAntiquot arg
/-- A term like `($e) is actually ambiguous: the antiquotation could be of kind `term`,
or `ident`, or ... . But it shouldn't really matter because antiquotations without
explicit kinds behave the same at runtime. So we replace `choice` nodes that contain
at least one implicit antiquotation with that antiquotation. -/
private partial def elimAntiquotChoices : Syntax → Syntax
| Syntax.node `choice args => match args.find? fun arg => antiquotKind? arg == Name.anonymous with
| some anti => anti
| none => Syntax.node `choice $ args.map elimAntiquotChoices
| Syntax.node k args => Syntax.node k $ args.map elimAntiquotChoices
| stx => stx
| Syntax.node `choice args => match args.find? fun arg => antiquotKind? arg == Name.anonymous with
| some anti => anti
| none => Syntax.node `choice $ args.map elimAntiquotChoices
| Syntax.node k args => Syntax.node k $ args.map elimAntiquotChoices
| stx => stx
-- Elaborate the content of a syntax quotation term
private partial def quoteSyntax : Syntax → TermElabM Syntax
| Syntax.ident info rawVal val preresolved => do
-- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
-- See the paper for details.
let r ← resolveGlobalName val
let preresolved := r ++ preresolved
let val := quote val
-- `scp` is bound in stxQuot.expand
`(Syntax.ident (SourceInfo.mk none none none) $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))
-- if antiquotation, insert contents as-is, else recurse
| stx@(Syntax.node k _) => do
if isAntiquot stx && !isEscapedAntiquot stx then
-- splices must occur in a `many` node
if isAntiquotSplice stx then throwErrorAt stx "unexpected antiquotation splice"
else pure $ getAntiquotTerm stx
else
let empty ← `(Array.empty);
-- if escaped antiquotation, decrement by one escape level
let stx := unescapeAntiquot stx
let args ← stx.getArgs.foldlM (fun args arg =>
if k == nullKind && isAntiquotSplice arg then
-- antiquotation splice pattern: inject args array
`(Array.append $args $(getAntiquotTerm arg))
else do
let arg ← quoteSyntax arg;
`(Array.push $args $arg)) empty
`(Syntax.node $(quote k) $args)
| Syntax.atom info val =>
`(Syntax.atom (SourceInfo.mk none none none) $(quote val))
| Syntax.missing => unreachable!
| Syntax.ident info rawVal val preresolved => do
-- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
-- See the paper for details.
let r ← resolveGlobalName val
let preresolved := r ++ preresolved
let val := quote val
-- `scp` is bound in stxQuot.expand
`(Syntax.ident (SourceInfo.mk none none none) $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))
-- if antiquotation, insert contents as-is, else recurse
| stx@(Syntax.node k _) => do
if isAntiquot stx && !isEscapedAntiquot stx then
-- splices must occur in a `many` node
if isAntiquotSplice stx then throwErrorAt stx "unexpected antiquotation splice"
else pure $ getAntiquotTerm stx
else
let empty ← `(Array.empty);
-- if escaped antiquotation, decrement by one escape level
let stx := unescapeAntiquot stx
let args ← stx.getArgs.foldlM (fun args arg =>
if k == nullKind && isAntiquotSplice arg then
-- antiquotation splice pattern: inject args array
`(Array.append $args $(getAntiquotTerm arg))
else do
let arg ← quoteSyntax arg;
`(Array.push $args $arg)) empty
`(Syntax.node $(quote k) $args)
| Syntax.atom info val =>
`(Syntax.atom (SourceInfo.mk none none none) $(quote val))
| Syntax.missing => unreachable!
def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do
let quoted := stx[1]
/- Syntax quotations are monadic values depending on the current macro scope. For efficiency, we bind
the macro scope once for each quotation, then build the syntax tree in a completely pure computation
depending on this binding. Note that regular function calls do not introduce a new macro scope (i.e.
we preserve referential transparency), so we can refer to this same `scp` inside `quoteSyntax` by
including it literally in a syntax quotation. -/
-- TODO: simplify to `(do scp ← getCurrMacroScope; pure $(quoteSyntax quoted))
stx ← quoteSyntax (elimAntiquotChoices quoted);
`(bind getCurrMacroScope (fun scp => bind getMainModule (fun mainModule => pure $stx)))
/- NOTE: It may seem like the newly introduced binding `scp` may accidentally
capture identifiers in an antiquotation introduced by `quoteSyntax`. However,
note that the syntax quotation above enjoys the same hygiene guarantees as
anywhere else in Lean; that is, we implement hygienic quotations by making
use of the hygienic quotation support of the bootstrapped Lean compiler!
let quoted := stx[1]
/- Syntax quotations are monadic values depending on the current macro scope. For efficiency, we bind
the macro scope once for each quotation, then build the syntax tree in a completely pure computation
depending on this binding. Note that regular function calls do not introduce a new macro scope (i.e.
we preserve referential transparency), so we can refer to this same `scp` inside `quoteSyntax` by
including it literally in a syntax quotation. -/
-- TODO: simplify to `(do scp ← getCurrMacroScope; pure $(quoteSyntax quoted))
stx ← quoteSyntax (elimAntiquotChoices quoted);
`(bind getCurrMacroScope (fun scp => bind getMainModule (fun mainModule => pure $stx)))
/- NOTE: It may seem like the newly introduced binding `scp` may accidentally
capture identifiers in an antiquotation introduced by `quoteSyntax`. However,
note that the syntax quotation above enjoys the same hygiene guarantees as
anywhere else in Lean; that is, we implement hygienic quotations by making
use of the hygienic quotation support of the bootstrapped Lean compiler!
Aside: While this might sound "dangerous", it is in fact less reliant on a
"chain of trust" than other bootstrapping parts of Lean: because this
implementation itself never uses `scp` (or any other identifier) both inside
and outside quotations, it can actually correctly be compiled by an
unhygienic (but otherwise correct) implementation of syntax quotations. As
long as it is then compiled again with the resulting executable (i.e. up to
stage 2), the result is a correct hygienic implementation. In this sense the
implementation is "self-stabilizing". It was in fact originally compiled
by an unhygienic prototype implementation. -/
Aside: While this might sound "dangerous", it is in fact less reliant on a
"chain of trust" than other bootstrapping parts of Lean: because this
implementation itself never uses `scp` (or any other identifier) both inside
and outside quotations, it can actually correctly be compiled by an
unhygienic (but otherwise correct) implementation of syntax quotations. As
long as it is then compiled again with the resulting executable (i.e. up to
stage 2), the result is a correct hygienic implementation. In this sense the
implementation is "self-stabilizing". It was in fact originally compiled
by an unhygienic prototype implementation. -/
@[builtinTermElab Parser.Level.quot] def elabLevelQuot : TermElab := adaptExpander stxQuot.expand
@[builtinTermElab Parser.Term.quot] def elabTermQuot : TermElab := adaptExpander stxQuot.expand
@ -143,173 +144,173 @@ private abbrev Alt := List Syntax × Syntax
/-- Information on a pattern's head that influences the compilation of a single
match step. -/
structure HeadInfo :=
-- Node kind to match, if any
(kind : Option SyntaxNodeKind := none)
-- Nested patterns for each argument, if any. In a single match step, we only
-- check that the arity matches. The arity is usually implied by the node kind,
-- but not in the case of `many` nodes.
(argPats : Option (Array Syntax) := none)
-- Function to apply to the right-hand side in case the match succeeds. Used to
-- bind pattern variables.
(rhsFn : Syntax → TermElabM Syntax := pure)
-- Node kind to match, if any
(kind : Option SyntaxNodeKind := none)
-- Nested patterns for each argument, if any. In a single match step, we only
-- check that the arity matches. The arity is usually implied by the node kind,
-- but not in the case of `many` nodes.
(argPats : Option (Array Syntax) := none)
-- Function to apply to the right-hand side in case the match succeeds. Used to
-- bind pattern variables.
(rhsFn : Syntax → TermElabM Syntax := pure)
instance : Inhabited HeadInfo := ⟨{}⟩
/-- `h1.generalizes h2` iff h1 is equal to or more general than h2, i.e. it matches all nodes
h2 matches. This induces a partial ordering. -/
def HeadInfo.generalizes : HeadInfo → HeadInfo → Bool
| { kind := none, .. }, _ => true
| { kind := some k1, argPats := none, .. },
{ kind := some k2, .. } => k1 == k2
| { kind := some k1, argPats := some ps1, .. },
{ kind := some k2, argPats := some ps2, .. } => k1 == k2 && ps1.size == ps2.size
| _, _ => false
| { kind := none, .. }, _ => true
| { kind := some k1, argPats := none, .. },
{ kind := some k2, .. } => k1 == k2
| { kind := some k1, argPats := some ps1, .. },
{ kind := some k2, argPats := some ps2, .. } => k1 == k2 && ps1.size == ps2.size
| _, _ => false
private def getHeadInfo (alt : Alt) : HeadInfo :=
let pat := alt.fst.head!;
let unconditional (rhsFn) := { rhsFn := rhsFn : HeadInfo };
-- variable pattern
if pat.isIdent then unconditional $ fun rhs => `(let $pat := discr; $rhs)
-- wildcard pattern
else if pat.isOfKind `Lean.Parser.Term.hole then unconditional pure
-- quotation pattern
else if isQuot pat then
let quoted := pat[1]
if quoted.isAtom then
-- We assume that atoms are uniquely determined by the node kind and never have to be checked
unconditional pure
else if isAntiquot quoted && !isEscapedAntiquot quoted then
-- quotation contains a single antiquotation
let k := antiquotKind? quoted;
-- Antiquotation kinds like `$id:ident` influence the parser, but also need to be considered by
-- match_syntax (but not by quotation terms). For example, `($id:ident) and `($e) are not
-- distinguishable without checking the kind of the node to be captured. Note that some
-- antiquotations like the latter one for terms do not correspond to any actual node kind
-- (signified by `k == Name.anonymous`), so we would only check for `ident` here.
--
-- if stx.isOfKind `ident then
-- let id := stx; ...
-- else
-- let e := stx; ...
let kind := if k == Name.anonymous then none else k
let anti := getAntiquotTerm quoted
-- Splices should only appear inside a nullKind node, see next case
if isAntiquotSplice quoted then unconditional $ fun _ => throwErrorAt quoted "unexpected antiquotation splice"
else if anti.isIdent then { kind := kind, rhsFn := fun rhs => `(let $anti := discr; $rhs) }
else unconditional fun _ => throwErrorAt anti ("match_syntax: antiquotation must be variable " ++ toString anti)
else if isAntiquotSplicePat quoted && quoted.getArgs.size == 1 then
-- quotation is a single antiquotation splice => bind args array
let anti := getAntiquotTerm quoted[0]
unconditional fun rhs => `(let $anti := Syntax.getArgs discr; $rhs)
-- TODO: support for more complex antiquotation splices
let pat := alt.fst.head!;
let unconditional (rhsFn) := { rhsFn := rhsFn : HeadInfo };
-- variable pattern
if pat.isIdent then unconditional $ fun rhs => `(let $pat := discr; $rhs)
-- wildcard pattern
else if pat.isOfKind `Lean.Parser.Term.hole then unconditional pure
-- quotation pattern
else if isQuot pat then
let quoted := pat[1]
if quoted.isAtom then
-- We assume that atoms are uniquely determined by the node kind and never have to be checked
unconditional pure
else if isAntiquot quoted && !isEscapedAntiquot quoted then
-- quotation contains a single antiquotation
let k := antiquotKind? quoted;
-- Antiquotation kinds like `$id:ident` influence the parser, but also need to be considered by
-- match_syntax (but not by quotation terms). For example, `($id:ident) and `($e) are not
-- distinguishable without checking the kind of the node to be captured. Note that some
-- antiquotations like the latter one for terms do not correspond to any actual node kind
-- (signified by `k == Name.anonymous`), so we would only check for `ident` here.
--
-- if stx.isOfKind `ident then
-- let id := stx; ...
-- else
-- let e := stx; ...
let kind := if k == Name.anonymous then none else k
let anti := getAntiquotTerm quoted
-- Splices should only appear inside a nullKind node, see next case
if isAntiquotSplice quoted then unconditional $ fun _ => throwErrorAt quoted "unexpected antiquotation splice"
else if anti.isIdent then { kind := kind, rhsFn := fun rhs => `(let $anti := discr; $rhs) }
else unconditional fun _ => throwErrorAt anti ("match_syntax: antiquotation must be variable " ++ toString anti)
else if isAntiquotSplicePat quoted && quoted.getArgs.size == 1 then
-- quotation is a single antiquotation splice => bind args array
let anti := getAntiquotTerm quoted[0]
unconditional fun rhs => `(let $anti := Syntax.getArgs discr; $rhs)
-- TODO: support for more complex antiquotation splices
else
-- not an antiquotation or escaped antiquotation: match head shape
let quoted := unescapeAntiquot quoted
let argPats := quoted.getArgs.map (pat.setArg 1);
{ kind := quoted.getKind, argPats := argPats }
else
-- not an antiquotation or escaped antiquotation: match head shape
let quoted := unescapeAntiquot quoted
let argPats := quoted.getArgs.map (pat.setArg 1);
{ kind := quoted.getKind, argPats := argPats }
else
unconditional $ fun _ => throwErrorAt pat ("match_syntax: unexpected pattern kind " ++ toString pat)
unconditional $ fun _ => throwErrorAt pat ("match_syntax: unexpected pattern kind " ++ toString pat)
-- Assuming that the first pattern of the alternative is taken, replace it with patterns (if any) for its
-- child nodes.
-- Ex: `($a + (- $b)) => `($a), `(+), `(- $b)
-- Note: The atom pattern `(+) will be discarded in a later step
private def explodeHeadPat (numArgs : Nat) : HeadInfo × Alt → TermElabM Alt
| (info, (pat::pats, rhs)) => do
let newPats := match info.argPats with
| some argPats => argPats.toList
| none => List.replicate numArgs $ Unhygienic.run `(_)
let rhs ← info.rhsFn rhs
pure (newPats ++ pats, rhs)
| _ => unreachable!
| (info, (pat::pats, rhs)) => do
let newPats := match info.argPats with
| some argPats => argPats.toList
| none => List.replicate numArgs $ Unhygienic.run `(_)
let rhs ← info.rhsFn rhs
pure (newPats ++ pats, rhs)
| _ => unreachable!
private partial def compileStxMatch : List Syntax → List Alt → TermElabM Syntax
| [], ([], rhs)::_ => pure rhs -- nothing left to match
| _, [] => throwError "non-exhaustive 'match_syntax'"
| discr::discrs, alts => do
let alts := (alts.map getHeadInfo).zip alts;
-- Choose a most specific pattern, ie. a minimal element according to `generalizes`.
-- If there are multiple minimal elements, the choice does not matter.
let (info, alt) := alts.tail!.foldl (fun (min : HeadInfo × Alt) (alt : HeadInfo × Alt) => if min.1.generalizes alt.1 then alt else min) alts.head!;
-- introduce pattern matches on the discriminant's children if there are any nested patterns
let newDiscrs ← match info.argPats with
| some pats => (List.range pats.size).mapM fun i => `(Syntax.getArg discr $(quote i))
| none => pure []
-- collect matching alternatives and explode them
let yesAlts := alts.filter fun (alt : HeadInfo × Alt) => alt.1.generalizes info
let yesAlts ← yesAlts.mapM $ explodeHeadPat newDiscrs.length
-- NOTE: use fresh macro scopes for recursive call so that different `discr`s introduced by the quotations below do not collide
let yes ← withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts
let some kind ← pure info.kind
-- unconditional match step
| `(let discr := $discr; $yes)
-- conditional match step
let noAlts := (alts.filter $ fun (alt : HeadInfo × Alt) => !info.generalizes alt.1).map (·.2)
let no ← withFreshMacroScope $ compileStxMatch (discr::discrs) noAlts
let cond ← match info.argPats with
| some pats => `(Syntax.isOfKind discr $(quote kind) && Array.size (Syntax.getArgs discr) == $(quote pats.size))
| none => `(Syntax.isOfKind discr $(quote kind))
`(let discr := $discr; if $cond = true then $yes else $no)
| _, _ => unreachable!
| [], ([], rhs)::_ => pure rhs -- nothing left to match
| _, [] => throwError "non-exhaustive 'match_syntax'"
| discr::discrs, alts => do
let alts := (alts.map getHeadInfo).zip alts;
-- Choose a most specific pattern, ie. a minimal element according to `generalizes`.
-- If there are multiple minimal elements, the choice does not matter.
let (info, alt) := alts.tail!.foldl (fun (min : HeadInfo × Alt) (alt : HeadInfo × Alt) => if min.1.generalizes alt.1 then alt else min) alts.head!;
-- introduce pattern matches on the discriminant's children if there are any nested patterns
let newDiscrs ← match info.argPats with
| some pats => (List.range pats.size).mapM fun i => `(Syntax.getArg discr $(quote i))
| none => pure []
-- collect matching alternatives and explode them
let yesAlts := alts.filter fun (alt : HeadInfo × Alt) => alt.1.generalizes info
let yesAlts ← yesAlts.mapM $ explodeHeadPat newDiscrs.length
-- NOTE: use fresh macro scopes for recursive call so that different `discr`s introduced by the quotations below do not collide
let yes ← withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts
let some kind ← pure info.kind
-- unconditional match step
| `(let discr := $discr; $yes)
-- conditional match step
let noAlts := (alts.filter $ fun (alt : HeadInfo × Alt) => !info.generalizes alt.1).map (·.2)
let no ← withFreshMacroScope $ compileStxMatch (discr::discrs) noAlts
let cond ← match info.argPats with
| some pats => `(Syntax.isOfKind discr $(quote kind) && Array.size (Syntax.getArgs discr) == $(quote pats.size))
| none => `(Syntax.isOfKind discr $(quote kind))
`(let discr := $discr; if $cond = true then $yes else $no)
| _, _ => unreachable!
private partial def getPatternVarsAux : Syntax → List Syntax
| stx@(Syntax.node k args) =>
if isAntiquot stx && !isEscapedAntiquot stx then
let anti := getAntiquotTerm stx
if anti.isIdent then [anti]
else []
else
List.join $ args.toList.map getPatternVarsAux
| _ => []
| stx@(Syntax.node k args) =>
if isAntiquot stx && !isEscapedAntiquot stx then
let anti := getAntiquotTerm stx
if anti.isIdent then [anti]
else []
else
List.join $ args.toList.map getPatternVarsAux
| _ => []
-- Get all pattern vars (as `Syntax.ident`s) in `stx`
partial def getPatternVars (stx : Syntax) : List Syntax :=
if isQuot stx then do
let quoted := stx.getArg 1;
getPatternVarsAux stx
else if stx.isIdent then
[stx]
else []
if isQuot stx then do
let quoted := stx.getArg 1;
getPatternVarsAux stx
else if stx.isIdent then
[stx]
else []
-- Transform alternatives by binding all right-hand sides to outside the match_syntax in order to prevent
-- code duplication during match_syntax compilation
private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → List Alt → TermElabM Syntax
| [], altsRev' => cont altsRev'.reverse
| (pats, rhs)::alts, altsRev' => do
let vars := List.join $ pats.map getPatternVars
match vars with
-- no antiquotations => introduce Unit parameter to preserve evaluation order
| [] =>
-- NOTE: references binding below
let rhs' ← `(rhs ())
-- NOTE: new macro scope so that introduced bindings do not collide
let stx ← withFreshMacroScope $ letBindRhss cont alts ((pats, rhs')::altsRev')
`(let rhs := fun _ => $rhs; $stx)
| _ =>
-- rhs ← `(fun $vars* => $rhs)
let rhs := Syntax.node `Lean.Parser.Term.fun #[mkAtom "fun", Syntax.node `null vars.toArray, mkAtom "=>", rhs]
let rhs' ← `(rhs)
let stx ← withFreshMacroScope $ letBindRhss cont alts ((pats, rhs')::altsRev')
`(let rhs := $rhs; $stx)
| [], altsRev' => cont altsRev'.reverse
| (pats, rhs)::alts, altsRev' => do
let vars := List.join $ pats.map getPatternVars
match vars with
-- no antiquotations => introduce Unit parameter to preserve evaluation order
| [] =>
-- NOTE: references binding below
let rhs' ← `(rhs ())
-- NOTE: new macro scope so that introduced bindings do not collide
let stx ← withFreshMacroScope $ letBindRhss cont alts ((pats, rhs')::altsRev')
`(let rhs := fun _ => $rhs; $stx)
| _ =>
-- rhs ← `(fun $vars* => $rhs)
let rhs := Syntax.node `Lean.Parser.Term.fun #[mkAtom "fun", Syntax.node `null vars.toArray, mkAtom "=>", rhs]
let rhs' ← `(rhs)
let stx ← withFreshMacroScope $ letBindRhss cont alts ((pats, rhs')::altsRev')
`(let rhs := $rhs; $stx)
def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
let discr := stx[1]
let alts := stx[3][1]
let alts ← alts.getSepArgs.mapM $ fun alt => do
let pats := alt.getArg 0;
let pat ←
if pats.getArgs.size == 1 then pure pats[0]
else throwError "match_syntax: expected exactly one pattern per alternative"
let pat := if isQuot pat then pat.setArg 1 $ elimAntiquotChoices $ pat[1] else pat
match pat.find? $ fun stx => stx.getKind == choiceKind with
| some choiceStx => throwErrorAt choiceStx "invalid pattern, nested syntax has multiple interpretations"
| none =>
let rhs := alt.getArg 2
pure ([pat], rhs)
-- letBindRhss (compileStxMatch stx [discr]) alts.toList []
compileStxMatch [discr] alts.toList
let discr := stx[1]
let alts := stx[3][1]
let alts ← alts.getSepArgs.mapM $ fun alt => do
let pats := alt.getArg 0;
let pat ←
if pats.getArgs.size == 1 then pure pats[0]
else throwError "match_syntax: expected exactly one pattern per alternative"
let pat := if isQuot pat then pat.setArg 1 $ elimAntiquotChoices $ pat[1] else pat
match pat.find? $ fun stx => stx.getKind == choiceKind with
| some choiceStx => throwErrorAt choiceStx "invalid pattern, nested syntax has multiple interpretations"
| none =>
let rhs := alt.getArg 2
pure ([pat], rhs)
-- letBindRhss (compileStxMatch stx [discr]) alts.toList []
compileStxMatch [discr] alts.toList
@[builtinTermElab «match_syntax»] def elabMatchSyntax : TermElab :=
adaptExpander match_syntax.expand
adaptExpander match_syntax.expand
end Lean.Elab.Term.Quotation

6
src/Lean/Elab/StrategyAttrs.lean
View file

@ -12,10 +12,10 @@ We want to support a more general approach, but we need to provide
the strategy selection attributes while we rely on the Lean3 elaborator.
-/
inductive ElaboratorStrategy
| simple | withExpectedType | asEliminator
| simple | withExpectedType | asEliminator
instance : Inhabited ElaboratorStrategy :=
⟨ElaboratorStrategy.withExpectedType⟩
⟨ElaboratorStrategy.withExpectedType⟩
builtin_initialize elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy ←
registerEnumAttributes `elaboratorStrategy
@ -25,6 +25,6 @@ builtin_initialize elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy
@[export lean_get_elaborator_strategy]
def getElaboratorStrategy (env : Environment) (n : Name) : Option ElaboratorStrategy :=
elaboratorStrategyAttrs.getValue env n
elaboratorStrategyAttrs.getValue env n
end Lean

432
src/Lean/Elab/Syntax.lean
View file

@ -13,58 +13,58 @@ Expand `optional «precedence»` where
precedenceLit : Parser := numLit <|> maxSymbol
maxSymbol := parser! nonReservedSymbol "max" -/
def expandOptPrecedence (stx : Syntax) : Option Nat :=
if stx.isNone then none
else match stx[0][1].isNatLit? with
| some v => some v
| _ => some Parser.maxPrec
if stx.isNone then
none
else match stx[0][1].isNatLit? with
| some v => some v
| _ => some Parser.maxPrec
private def mkParserSeq (ds : Array Syntax) : TermElabM Syntax := do
if ds.size == 0 then
throwUnsupportedSyntax
else if ds.size == 1 then
pure ds[0]
else
let r := ds[0]
for d in ds[1:ds.size] do
r ← `(ParserDescr.andthen $r $d)
return r
if ds.size == 0 then
throwUnsupportedSyntax
else if ds.size == 1 then
pure ds[0]
else
let r := ds[0]
for d in ds[1:ds.size] do
r ← `(ParserDescr.andthen $r $d)
return r
structure ToParserDescrContext :=
(catName : Name)
(first : Bool)
(leftRec : Bool) -- true iff left recursion is allowed
/- When `leadingIdentAsSymbol == true` we convert
`Lean.Parser.Syntax.atom` into `Lean.ParserDescr.nonReservedSymbol`
See comment at `Parser.ParserCategory`. -/
(leadingIdentAsSymbol : Bool)
(catName : Name)
(first : Bool)
(leftRec : Bool) -- true iff left recursion is allowed
/- When `leadingIdentAsSymbol == true` we convert
`Lean.Parser.Syntax.atom` into `Lean.ParserDescr.nonReservedSymbol`
See comment at `Parser.ParserCategory`. -/
(leadingIdentAsSymbol : Bool)
abbrev ToParserDescrM := ReaderT ToParserDescrContext (StateRefT Bool TermElabM)
private def markAsTrailingParser : ToParserDescrM Unit := set true
@[inline] private def withNotFirst {α} (x : ToParserDescrM α) : ToParserDescrM α :=
withReader (fun ctx => { ctx with first := false }) x
withReader (fun ctx => { ctx with first := false }) x
@[inline] private def withoutLeftRec {α} (x : ToParserDescrM α) : ToParserDescrM α :=
withReader (fun ctx => { ctx with leftRec := false }) x
withReader (fun ctx => { ctx with leftRec := false }) x
def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do
let ctx ← read
if ctx.first && stx.getKind == `Lean.Parser.Syntax.cat then
let cat := stx[0].getId.eraseMacroScopes
if cat == ctx.catName then
let prec? : Option Nat := expandOptPrecedence stx[1]
unless prec?.isNone do throwErrorAt stx[1] ("invalid occurrence of ':<num>' modifier in head")
unless ctx.leftRec do
throwErrorAt! stx[3] "invalid occurrence of '{cat}', parser algorithm does not allow this form of left recursion"
markAsTrailingParser -- mark as trailing par
pure true
let ctx ← read
if ctx.first && stx.getKind == `Lean.Parser.Syntax.cat then
let cat := stx[0].getId.eraseMacroScopes
if cat == ctx.catName then
let prec? : Option Nat := expandOptPrecedence stx[1]
unless prec?.isNone do throwErrorAt stx[1] ("invalid occurrence of ':<num>' modifier in head")
unless ctx.leftRec do
throwErrorAt! stx[3] "invalid occurrence of '{cat}', parser algorithm does not allow this form of left recursion"
markAsTrailingParser -- mark as trailing par
pure true
else
pure false
else
pure false
else
pure false
partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
| stx => do
partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := do
let kind := stx.getKind
if kind == nullKind then
let args := stx.getArgs
@ -172,31 +172,30 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
where `newStx` is of category `term`. After elaboration, `newStx` should have type
`TrailingParserDescr` if `trailingParser == true`, and `ParserDescr` otherwise. -/
def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (Syntax × Bool) := do
let env ← getEnv
let leadingIdentAsSymbol := Parser.leadingIdentAsSymbol env catName
(toParserDescrAux stx { catName := catName, first := true, leftRec := true, leadingIdentAsSymbol := leadingIdentAsSymbol }).run false
let env ← getEnv
let leadingIdentAsSymbol := Parser.leadingIdentAsSymbol env catName
(toParserDescrAux stx { catName := catName, first := true, leftRec := true, leadingIdentAsSymbol := leadingIdentAsSymbol }).run false
end Term
namespace Command
private def getCatSuffix (catName : Name) : String :=
match catName with
| Name.str _ s _ => s
| _ => unreachable!
match catName with
| Name.str _ s _ => s
| _ => unreachable!
private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
let quotSymbol := "`(" ++ getCatSuffix catName ++ "|"
let kind := catName ++ `quot
let cmd ← `(
@[termParser] def $(mkIdent kind) : Lean.ParserDescr :=
Lean.ParserDescr.node $(quote kind) $(quote Lean.Parser.maxPrec)
(Lean.ParserDescr.andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
(Lean.ParserDescr.andthen (Lean.ParserDescr.cat $(quote catName) 0) (Lean.ParserDescr.symbol ")"))))
elabCommand cmd
let quotSymbol := "`(" ++ getCatSuffix catName ++ "|"
let kind := catName ++ `quot
let cmd ← `(
@[termParser] def $(mkIdent kind) : Lean.ParserDescr :=
Lean.ParserDescr.node $(quote kind) $(quote Lean.Parser.maxPrec)
(Lean.ParserDescr.andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
(Lean.ParserDescr.andthen (Lean.ParserDescr.cat $(quote catName) 0) (Lean.ParserDescr.symbol ")"))))
elabCommand cmd
@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
fun stx => do
@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab := fun stx => do
let catName := stx[1].getId
let attrName := catName.appendAfter "Parser"
let env ← getEnv
@ -205,43 +204,43 @@ fun stx => do
declareSyntaxCatQuotParser catName
def mkKindName (catName : Name) : Name :=
`_kind ++ catName
`_kind ++ catName
def mkFreshKind (catName : Name) : CommandElabM Name := do
let scp ← getCurrMacroScope
let mainModule ← getMainModule
pure $ Lean.addMacroScope mainModule (mkKindName catName) scp
let scp ← getCurrMacroScope
let mainModule ← getMainModule
pure $ Lean.addMacroScope mainModule (mkKindName catName) scp
def Macro.mkFreshKind (catName : Name) : MacroM Name :=
Macro.addMacroScope (mkKindName catName)
Macro.addMacroScope (mkKindName catName)
def mkKind (stx : Syntax) : CommandElabM Name := do
let kind := stx.getId
if kind.hasMacroScopes then
pure kind
else
let currNamespace ← getCurrNamespace
pure (currNamespace ++ kind)
let kind := stx.getId
if kind.hasMacroScopes then
pure kind
else
let currNamespace ← getCurrNamespace
pure (currNamespace ++ kind)
private def elabKindPrio (stx : Syntax) (catName : Name) : CommandElabM (Name × Nat) := do
if stx.isNone then
let k ← mkFreshKind catName
pure (k, 0)
else
let arg := stx[1]
if arg.getKind == `Lean.Parser.Command.parserKind then
let k ← mkKind arg[0]
pure (k, 0)
else if arg.getKind == `Lean.Parser.Command.parserPrio then
if stx.isNone then
let k ← mkFreshKind catName
let prio := arg[0].isNatLit?.getD 0
pure (k, prio)
else if arg.getKind == `Lean.Parser.Command.parserKindPrio then
let k ← mkKind arg[0]
let prio := arg[2].isNatLit?.getD 0
pure (k, prio)
pure (k, 0)
else
throwError "unexpected syntax kind/priority"
let arg := stx[1]
if arg.getKind == `Lean.Parser.Command.parserKind then
let k ← mkKind arg[0]
pure (k, 0)
else if arg.getKind == `Lean.Parser.Command.parserPrio then
let k ← mkFreshKind catName
let prio := arg[0].isNatLit?.getD 0
pure (k, prio)
else if arg.getKind == `Lean.Parser.Command.parserKindPrio then
let k ← mkKind arg[0]
let prio := arg[2].isNatLit?.getD 0
pure (k, prio)
else
throwError "unexpected syntax kind/priority"
/- We assume a new syntax can be treated as an atom when it starts and ends with a token.
Here are examples of atom-like syntax.
@ -251,8 +250,7 @@ else
syntax "foo" : term
```
-/
private partial def isAtomLikeSyntax : Syntax → Bool
| stx =>
private partial def isAtomLikeSyntax (stx : Syntax) : Bool :=
let kind := stx.getKind
if kind == nullKind then
isAtomLikeSyntax stx[0] && isAtomLikeSyntax stx[stx.getNumArgs - 1]
@ -266,8 +264,7 @@ private partial def isAtomLikeSyntax : Syntax → Bool
/-
def «syntax» := parser! "syntax " >> optPrecedence >> optKindPrio >> many1 syntaxParser >> " : " >> ident
-/
@[builtinCommandElab «syntax»] def elabSyntax : CommandElab :=
fun stx => do
@[builtinCommandElab «syntax»] def elabSyntax : CommandElab := fun stx => do
let env ← getEnv
let cat := stx[5].getId.eraseMacroScopes
unless (Parser.isParserCategory env cat) do throwErrorAt stx[5] ("unknown category '" ++ cat ++ "'")
@ -291,179 +288,176 @@ fun stx => do
/-
def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
-/
@[builtinCommandElab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab :=
fun stx => do
@[builtinCommandElab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab := fun stx => do
let declName := stx[1]
let (val, _) ← runTermElabM none $ fun _ => Term.toParserDescr stx[3] Name.anonymous
let stx' ← `(def $declName : Lean.ParserDescr := $val)
withMacroExpansion stx stx' $ elabCommand stx'
def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
alts ← alts.mapSepElemsM fun alt => do
alts ← alts.mapSepElemsM fun alt => do
let lhs := alt[0]
let pat := lhs[0]
if !pat.isQuot then
throwUnsupportedSyntax
let quot := pat[1]
let k' := quot.getKind
if k' == k then
pure alt
else if k' == choiceKind then
match quot.getArgs.find? fun quotAlt => quotAlt.getKind == k with
| none => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
| some quot =>
let pat := pat.setArg 1 quot
let lhs := lhs.setArg 0 pat
pure $ alt.setArg 0 lhs
else
throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
let lhs := alt[0]
let pat := lhs[0]
if !pat.isQuot then
throwUnsupportedSyntax
let quot := pat[1]
let k' := quot.getKind
if k' == k then
pure alt
else if k' == choiceKind then
match quot.getArgs.find? fun quotAlt => quotAlt.getKind == k with
| none => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
| some quot =>
let pat := pat.setArg 1 quot
let lhs := lhs.setArg 0 pat
pure $ alt.setArg 0 lhs
else
throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
let lhs := alt[0]
let pat := lhs[0]
if !pat.isQuot then
throwUnsupportedSyntax
let quot := pat[1]
pure quot.getKind
pure quot.getKind
def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
let k ← inferMacroRulesAltKind (alts.get! 0)
if k == choiceKind then
throwErrorAt! alts[0]
"invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
else
let altsK ← alts.filterSepElemsM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
let altsNotK ← alts.filterSepElemsM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
let defCmd ← elabMacroRulesAux k altsK
if altsNotK.isEmpty then
pure defCmd
let k ← inferMacroRulesAltKind (alts.get! 0)
if k == choiceKind then
throwErrorAt! alts[0]
"invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
else
`($defCmd:command macro_rules $altsNotK:matchAlt*)
let altsK ← alts.filterSepElemsM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
let altsNotK ← alts.filterSepElemsM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
let defCmd ← elabMacroRulesAux k altsK
if altsNotK.isEmpty then
pure defCmd
else
`($defCmd:command macro_rules $altsNotK:matchAlt*)
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
adaptExpander $ fun stx => match_syntax stx with
| `(macro_rules $alts:matchAlt*) => elabNoKindMacroRulesAux alts
| `(macro_rules | $alts:matchAlt*) => elabNoKindMacroRulesAux alts
| `(macro_rules [$kind] $alts:matchAlt*) => do elabMacroRulesAux (← mkKind kind) alts
| `(macro_rules [$kind] | $alts:matchAlt*) => do elabMacroRulesAux (← mkKind kind) alts
| _ => throwUnsupportedSyntax
adaptExpander fun stx => match_syntax stx with
| `(macro_rules $alts:matchAlt*) => elabNoKindMacroRulesAux alts
| `(macro_rules | $alts:matchAlt*) => elabNoKindMacroRulesAux alts
| `(macro_rules [$kind] $alts:matchAlt*) => do elabMacroRulesAux (← mkKind kind) alts
| `(macro_rules [$kind] | $alts:matchAlt*) => do elabMacroRulesAux (← mkKind kind) alts
| _ => throwUnsupportedSyntax
@[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro :=
fun stx => match_syntax stx with
| `(infix:$prec $op => $f) => `(infixl:$prec $op => $f)
| `(infixr:$prec $op => $f) => `(notation:$prec lhs $op:strLit rhs:$prec => $f lhs rhs)
| `(infixl:$prec $op => $f) => let prec1 : Syntax := quote (prec.toNat+1); `(notation:$prec lhs $op:strLit rhs:$prec1 => $f lhs rhs)
| `(prefix:$prec $op => $f) => `(notation:$prec $op:strLit arg:$prec => $f arg)
| `(postfix:$prec $op => $f) => `(notation:$prec arg $op:strLit => $f arg)
| _ => Macro.throwUnsupported
fun stx => match_syntax stx with
| `(infix:$prec $op => $f) => `(infixl:$prec $op => $f)
| `(infixr:$prec $op => $f) => `(notation:$prec lhs $op:strLit rhs:$prec => $f lhs rhs)
| `(infixl:$prec $op => $f) => let prec1 : Syntax := quote (prec.toNat+1); `(notation:$prec lhs $op:strLit rhs:$prec1 => $f lhs rhs)
| `(prefix:$prec $op => $f) => `(notation:$prec $op:strLit arg:$prec => $f arg)
| `(postfix:$prec $op => $f) => `(notation:$prec arg $op:strLit => $f arg)
| _ => Macro.throwUnsupported
/- Wrap all occurrences of the given `ident` nodes in antiquotations -/
private partial def antiquote (vars : Array Syntax) : Syntax → Syntax
| stx => match_syntax stx with
| `($id:ident) =>
if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then
Syntax.node `antiquot #[mkAtom "$", mkNullNode, id, mkNullNode, mkNullNode]
else
stx
| _ => match stx with
| Syntax.node k args => Syntax.node k (args.map (antiquote vars))
| stx => stx
| stx => match_syntax stx with
| `($id:ident) =>
if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then
Syntax.node `antiquot #[mkAtom "$", mkNullNode, id, mkNullNode, mkNullNode]
else
stx
| _ => match stx with
| Syntax.node k args => Syntax.node k (args.map (antiquote vars))
| stx => stx
/- Convert `notation` command lhs item into a `syntax` command item -/
def expandNotationItemIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind
if k == `Lean.Parser.Command.identPrec then
pure $ Syntax.node `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term, stx[1]]
else if k == quotedSymbolKind then
match stx[1] with
| Syntax.atom info val => pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit val info]
| _ => Macro.throwUnsupported
else if k == strLitKind then
pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
else
Macro.throwUnsupported
let k := stx.getKind
if k == `Lean.Parser.Command.identPrec then
pure $ Syntax.node `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term, stx[1]]
else if k == quotedSymbolKind then
match stx[1] with
| Syntax.atom info val => pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit val info]
| _ => Macro.throwUnsupported
else if k == strLitKind then
pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
else
Macro.throwUnsupported
def strLitToPattern (stx: Syntax) : MacroM Syntax :=
match stx.isStrLit? with
| some str => pure $ mkAtomFrom stx str
| none => Macro.throwUnsupported
match stx.isStrLit? with
| some str => pure $ mkAtomFrom stx str
| none => Macro.throwUnsupported
/- Convert `notation` command lhs item a pattern element -/
def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind
if k == `Lean.Parser.Command.identPrec then
let item := stx[0]
pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
else if k == quotedSymbolKind then
pure stx[1]
else if k == strLitKind then
strLitToPattern stx
else
Macro.throwUnsupported
let k := stx.getKind
if k == `Lean.Parser.Command.identPrec then
let item := stx[0]
pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
else if k == quotedSymbolKind then
pure stx[1]
else if k == strLitKind then
strLitToPattern stx
else
Macro.throwUnsupported
private def expandNotationAux (ref : Syntax) (prec? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : MacroM Syntax := do
let kind ← Macro.mkFreshKind `term
-- build parser
let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
let cat := mkIdentFrom ref `term
-- build macro rules
let vars := items.filter fun item => item.getKind == `Lean.Parser.Command.identPrec
let vars := vars.map fun var => var[0]
let rhs := antiquote vars rhs
let patArgs ← items.mapM expandNotationItemIntoPattern
let pat := Syntax.node kind patArgs
match prec? with
| none => `(syntax [$(mkIdentFrom ref kind):ident] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
| some prec => `(syntax:$prec [$(mkIdentFrom ref kind):ident] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
let kind ← Macro.mkFreshKind `term
-- build parser
let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem
let cat := mkIdentFrom ref `term
-- build macro rules
let vars := items.filter fun item => item.getKind == `Lean.Parser.Command.identPrec
let vars := vars.map fun var => var[0]
let rhs := antiquote vars rhs
let patArgs ← items.mapM expandNotationItemIntoPattern
let pat := Syntax.node kind patArgs
match prec? with
| none => `(syntax [$(mkIdentFrom ref kind):ident] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
| some prec => `(syntax:$prec [$(mkIdentFrom ref kind):ident] $syntaxParts* : $cat macro_rules | `($pat) => `($rhs))
@[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro :=
fun stx =>
match_syntax stx with
| `(notation:$prec $items* => $rhs) => expandNotationAux stx prec items rhs
| `(notation $items:notationItem* => $rhs) => expandNotationAux stx none items rhs
| _ => Macro.throwUnsupported
@[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro := fun stx =>
match_syntax stx with
| `(notation:$prec $items* => $rhs) => expandNotationAux stx prec items rhs
| `(notation $items:notationItem* => $rhs) => expandNotationAux stx none items rhs
| _ => Macro.throwUnsupported
/- Convert `macro` argument into a `syntax` command item -/
def expandMacroArgIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind
if k == `Lean.Parser.Command.macroArgSimple then
pure stx[2]
else if k == strLitKind then
pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
else
Macro.throwUnsupported
let k := stx.getKind
if k == `Lean.Parser.Command.macroArgSimple then
pure stx[2]
else if k == strLitKind then
pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
else
Macro.throwUnsupported
/- Convert `macro` head into a `syntax` command item -/
def expandMacroHeadIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
if stx.isIdent then
let info := stx.getHeadInfo.getD {}
let id := stx.getId
pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info]
else
expandMacroArgIntoSyntaxItem stx
if stx.isIdent then
let info := stx.getHeadInfo.getD {}
let id := stx.getId
pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info]
else
expandMacroArgIntoSyntaxItem stx
/- Convert `macro` arg into a pattern element -/
def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind
if k == `Lean.Parser.Command.macroArgSimple then
let item := stx[0]
pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
else if k == strLitKind then
strLitToPattern stx
else
Macro.throwUnsupported
let k := stx.getKind
if k == `Lean.Parser.Command.macroArgSimple then
let item := stx[0]
pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
else if k == strLitKind then
strLitToPattern stx
else
Macro.throwUnsupported
/- Convert `macro` head into a pattern element -/
def expandMacroHeadIntoPattern (stx : Syntax) : MacroM Syntax :=
if stx.isIdent then
pure $ mkAtomFrom stx (toString stx.getId)
else
expandMacroArgIntoPattern stx
if stx.isIdent then
pure $ mkAtomFrom stx (toString stx.getId)
else
expandMacroArgIntoPattern stx
@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro :=
fun stx => do
@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro := fun stx => do
let prec := stx[1].getArgs
let head := stx[2]
let args := stx[3].getArgs
@ -488,22 +482,20 @@ fun stx => do
`(syntax $prec* [$(mkIdentFrom stx kind):ident] $stxParts* : $cat
macro_rules | `($pat) => `($rhsBody))
@[builtinInit] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.syntax
pure ()
builtin_initialize
registerTraceClass `Elab.syntax
@[inline] def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
Term.tryPostponeIfNoneOrMVar expectedType?
let some expectedType ← pure expectedType?
| throwError "expected type must be known"
x expectedType
Term.tryPostponeIfNoneOrMVar expectedType?
let some expectedType ← pure expectedType?
| throwError "expected type must be known"
x expectedType
/-
def elabTail := try (" : " >> ident) >> darrow >> termParser
parser! "elab " >> optPrecedence >> elabHead >> many elabArg >> elabTail
-/
@[builtinMacro Lean.Parser.Command.elab] def expandElab : Macro :=
fun stx => do
@[builtinMacro Lean.Parser.Command.elab] def expandElab : Macro := fun stx => do
let ref := stx
let prec := stx[1].getArgs
let head := stx[2]

352
src/Lean/Elab/SyntheticMVars.lean
View file

@ -6,183 +6,181 @@ Authors: Leonardo de Moura, Sebastian Ullrich
import Lean.Elab.Term
import Lean.Elab.Tactic.Basic
namespace Lean
namespace Elab
namespace Term
namespace Lean.Elab.Term
open Tactic (TacticM evalTactic getUnsolvedGoals)
open Meta
def liftTacticElabM {α} (mvarId : MVarId) (x : TacticM α) : TermElabM α :=
withMVarContext mvarId do
let s ← get
let savedSyntheticMVars := s.syntheticMVars
modify fun s => { s with syntheticMVars := [] }
try
x.run' { main := mvarId } { goals := [mvarId] }
finally
modify fun s => { s with syntheticMVars := savedSyntheticMVars }
withMVarContext mvarId do
let s ← get
let savedSyntheticMVars := s.syntheticMVars
modify fun s => { s with syntheticMVars := [] }
try
x.run' { main := mvarId } { goals := [mvarId] }
finally
modify fun s => { s with syntheticMVars := savedSyntheticMVars }
def ensureAssignmentHasNoMVars (mvarId : MVarId) : TermElabM Unit := do
let val ← instantiateMVars (mkMVar mvarId)
if val.hasExprMVar then throwError! "tactic failed, result still contain metavariables{indentExpr val}"
let val ← instantiateMVars (mkMVar mvarId)
if val.hasExprMVar then throwError! "tactic failed, result still contain metavariables{indentExpr val}"
def runTactic (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
/- Recall, `tacticCode` is the whole `by ...` expression.
We store the `by` because in the future we want to save the initial state information at the `by` position. -/
let code := tacticCode[1]
modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId }
let remainingGoals ← liftTacticElabM mvarId do evalTactic code; getUnsolvedGoals
unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals
ensureAssignmentHasNoMVars mvarId
/- Recall, `tacticCode` is the whole `by ...` expression.
We store the `by` because in the future we want to save the initial state information at the `by` position. -/
let code := tacticCode[1]
modifyThe Meta.State fun s => { s with mctx := s.mctx.instantiateMVarDeclMVars mvarId }
let remainingGoals ← liftTacticElabM mvarId do evalTactic code; getUnsolvedGoals
unless remainingGoals.isEmpty do reportUnsolvedGoals remainingGoals
ensureAssignmentHasNoMVars mvarId
/-- Auxiliary function used to implement `synthesizeSyntheticMVars`. -/
private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSorry := true) : TermElabM Expr :=
-- Remark: if `ctx.errToSorry` is already false, then we don't enable it. Recall tactics disable `errToSorry`
withReader (fun ctx => { ctx with errToSorry := ctx.errToSorry && errToSorry }) do
elabTerm stx expectedType? false
-- Remark: if `ctx.errToSorry` is already false, then we don't enable it. Recall tactics disable `errToSorry`
withReader (fun ctx => { ctx with errToSorry := ctx.errToSorry && errToSorry }) do
elabTerm stx expectedType? false
/--
Try to elaborate `stx` that was postponed by an elaboration method using `Expection.postpone`.
It returns `true` if it succeeded, and `false` otherwise.
It is used to implement `synthesizeSyntheticMVars`. -/
private def resumePostponed (macroStack : MacroStack) (declName? : Option Name) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool :=
withRef stx $ withMVarContext mvarId do
let s ← get
try
withReader (fun ctx => { ctx with macroStack := macroStack, declName? := declName? }) do
let mvarDecl ← getMVarDecl mvarId
let expectedType ← instantiateMVars mvarDecl.type
let result ← resumeElabTerm stx expectedType (!postponeOnError)
/- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
let result ← withRef stx $ ensureHasType expectedType result
assignExprMVar mvarId result
pure true
catch
| ex@(Exception.internal id) =>
if id == postponeExceptionId then
set s
pure false
else
throw ex
| ex@(Exception.error _ _) =>
if postponeOnError then
set s; pure false
else
logException ex
pure true
withRef stx $ withMVarContext mvarId do
let s ← get
try
withReader (fun ctx => { ctx with macroStack := macroStack, declName? := declName? }) do
let mvarDecl ← getMVarDecl mvarId
let expectedType ← instantiateMVars mvarDecl.type
let result ← resumeElabTerm stx expectedType (!postponeOnError)
/- We must ensure `result` has the expected type because it is the one expected by the method that postponed stx.
That is, the method does not have an opportunity to check whether `result` has the expected type or not. -/
let result ← withRef stx $ ensureHasType expectedType result
assignExprMVar mvarId result
pure true
catch
| ex@(Exception.internal id) =>
if id == postponeExceptionId then
set s
pure false
else
throw ex
| ex@(Exception.error _ _) =>
if postponeOnError then
set s; pure false
else
logException ex
pure true
/--
Similar to `synthesizeInstMVarCore`, but makes sure that `instMVar` local context and instances
are used. It also logs any error message produced. -/
private def synthesizePendingInstMVar (instMVar : MVarId) : TermElabM Bool :=
withMVarContext instMVar do
try
synthesizeInstMVarCore instMVar
catch
| ex@(Exception.error _ _) => logException ex; pure true
| _ => unreachable!
withMVarContext instMVar do
try
synthesizeInstMVarCore instMVar
catch
| ex@(Exception.error _ _) => logException ex; pure true
| _ => unreachable!
/--
Similar to `synthesizePendingInstMVar`, but generates type mismatch error message. -/
private def synthesizePendingCoeInstMVar
(instMVar : MVarId) (errorMsgHeader? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Bool :=
withMVarContext instMVar do
try
synthesizeInstMVarCore instMVar
catch
| Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg
| _ => unreachable!
withMVarContext instMVar do
try
synthesizeInstMVarCore instMVar
catch
| Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg
| _ => unreachable!
/--
Return `true` iff `mvarId` is assigned to a term whose the
head is not a metavariable. We use this method to process `SyntheticMVarKind.withDefault`. -/
private def checkWithDefault (mvarId : MVarId) : TermElabM Bool := do
let val ← instantiateMVars (mkMVar mvarId)
pure $ !val.getAppFn.isMVar
let val ← instantiateMVars (mkMVar mvarId)
pure $ !val.getAppFn.isMVar
/-- Try to synthesize the given pending synthetic metavariable. -/
private def synthesizeSyntheticMVar (mvarSyntheticDecl : SyntheticMVarDecl) (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool :=
withRef mvarSyntheticDecl.stx do
match mvarSyntheticDecl.kind with
| SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.mvarId
| SyntheticMVarKind.coe header? expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.mvarId header? expectedType eType e f?
-- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
| SyntheticMVarKind.withDefault _ => checkWithDefault mvarSyntheticDecl.mvarId
| SyntheticMVarKind.postponed macroStack declName? => resumePostponed macroStack declName? mvarSyntheticDecl.stx mvarSyntheticDecl.mvarId postponeOnError
| SyntheticMVarKind.tactic declName? tacticCode =>
withReader (fun ctx => { ctx with declName? := declName? }) do
if runTactics then
runTactic mvarSyntheticDecl.mvarId tacticCode
pure true
else
pure false
withRef mvarSyntheticDecl.stx do
match mvarSyntheticDecl.kind with
| SyntheticMVarKind.typeClass => synthesizePendingInstMVar mvarSyntheticDecl.mvarId
| SyntheticMVarKind.coe header? expectedType eType e f? => synthesizePendingCoeInstMVar mvarSyntheticDecl.mvarId header? expectedType eType e f?
-- NOTE: actual processing at `synthesizeSyntheticMVarsAux`
| SyntheticMVarKind.withDefault _ => checkWithDefault mvarSyntheticDecl.mvarId
| SyntheticMVarKind.postponed macroStack declName? => resumePostponed macroStack declName? mvarSyntheticDecl.stx mvarSyntheticDecl.mvarId postponeOnError
| SyntheticMVarKind.tactic declName? tacticCode =>
withReader (fun ctx => { ctx with declName? := declName? }) do
if runTactics then
runTactic mvarSyntheticDecl.mvarId tacticCode
pure true
else
pure false
/--
Try to synthesize the current list of pending synthetic metavariables.
Return `true` if at least one of them was synthesized. -/
private def synthesizeSyntheticMVarsStep (postponeOnError : Bool) (runTactics : Bool) : TermElabM Bool := do
let ctx ← read
traceAtCmdPos `Elab.resuming $ fun _ =>
fmt "resuming synthetic metavariables, mayPostpone: " ++ fmt ctx.mayPostpone ++ ", postponeOnError: " ++ toString postponeOnError
let s ← get
let syntheticMVars := s.syntheticMVars
let numSyntheticMVars := syntheticMVars.length
-- We reset `syntheticMVars` because new synthetic metavariables may be created by `synthesizeSyntheticMVar`.
modify fun s => { s with syntheticMVars := [] }
-- Recall that `syntheticMVars` is a list where head is the most recent pending synthetic metavariable.
-- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
-- It would not be incorrect to use `filterM`.
let remainingSyntheticMVars ← syntheticMVars.filterRevM fun mvarDecl => do
-- We use `traceM` because we want to make sure the metavar local context is used to trace the message
traceM `Elab.postpone (withMVarContext mvarDecl.mvarId do addMessageContext msg!"resuming {mkMVar mvarDecl.mvarId}")
let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics
trace[Elab.postpone]! if succeeded then fmt "succeeded" else fmt "not ready yet"
pure !succeeded
-- Merge new synthetic metavariables with `remainingSyntheticMVars`, i.e., metavariables that still couldn't be synthesized
modify fun s => { s with syntheticMVars := s.syntheticMVars ++ remainingSyntheticMVars }
pure $ numSyntheticMVars != remainingSyntheticMVars.length
let ctx ← read
traceAtCmdPos `Elab.resuming $ fun _ =>
fmt "resuming synthetic metavariables, mayPostpone: " ++ fmt ctx.mayPostpone ++ ", postponeOnError: " ++ toString postponeOnError
let s ← get
let syntheticMVars := s.syntheticMVars
let numSyntheticMVars := syntheticMVars.length
-- We reset `syntheticMVars` because new synthetic metavariables may be created by `synthesizeSyntheticMVar`.
modify fun s => { s with syntheticMVars := [] }
-- Recall that `syntheticMVars` is a list where head is the most recent pending synthetic metavariable.
-- We use `filterRevM` instead of `filterM` to make sure we process the synthetic metavariables using the order they were created.
-- It would not be incorrect to use `filterM`.
let remainingSyntheticMVars ← syntheticMVars.filterRevM fun mvarDecl => do
-- We use `traceM` because we want to make sure the metavar local context is used to trace the message
traceM `Elab.postpone (withMVarContext mvarDecl.mvarId do addMessageContext msg!"resuming {mkMVar mvarDecl.mvarId}")
let succeeded ← synthesizeSyntheticMVar mvarDecl postponeOnError runTactics
trace[Elab.postpone]! if succeeded then fmt "succeeded" else fmt "not ready yet"
pure !succeeded
-- Merge new synthetic metavariables with `remainingSyntheticMVars`, i.e., metavariables that still couldn't be synthesized
modify fun s => { s with syntheticMVars := s.syntheticMVars ++ remainingSyntheticMVars }
pure $ numSyntheticMVars != remainingSyntheticMVars.length
/--
Apply default value to any pending synthetic metavariable of kind `SyntheticMVarKind.withDefault`
Return true if something was synthesized. -/
def synthesizeUsingDefault : TermElabM Bool := do
let s ← get
let len := s.syntheticMVars.length
let newSyntheticMVars ← s.syntheticMVars.filterM fun mvarDecl =>
withRef mvarDecl.stx $
match mvarDecl.kind with
| SyntheticMVarKind.withDefault defaultVal => withMVarContext mvarDecl.mvarId do
let val ← instantiateMVars (mkMVar mvarDecl.mvarId)
if val.getAppFn.isMVar && !(← isDefEq val defaultVal) then
-- TODO: better error message
throwError! "failed to assign default value to metavariable{indentExpr val}\ndefault value{indentExpr defaultVal}"
pure false
| _ => pure true
modify fun s => { s with syntheticMVars := newSyntheticMVars }
pure $ newSyntheticMVars.length != len
let s ← get
let len := s.syntheticMVars.length
let newSyntheticMVars ← s.syntheticMVars.filterM fun mvarDecl =>
withRef mvarDecl.stx $
match mvarDecl.kind with
| SyntheticMVarKind.withDefault defaultVal => withMVarContext mvarDecl.mvarId do
let val ← instantiateMVars (mkMVar mvarDecl.mvarId)
if val.getAppFn.isMVar && !(← isDefEq val defaultVal) then
-- TODO: better error message
throwError! "failed to assign default value to metavariable{indentExpr val}\ndefault value{indentExpr defaultVal}"
pure false
| _ => pure true
modify fun s => { s with syntheticMVars := newSyntheticMVars }
pure $ newSyntheticMVars.length != len
/-- Report an error for each synthetic metavariable that could not be resolved. -/
private def reportStuckSyntheticMVars : TermElabM Unit := do
let s ← get
for mvarSyntheticDecl in s.syntheticMVars do
withRef mvarSyntheticDecl.stx do
match mvarSyntheticDecl.kind with
| SyntheticMVarKind.typeClass =>
withMVarContext mvarSyntheticDecl.mvarId do
let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId
logError $ "failed to create type class instance for " ++ indentExpr mvarDecl.type
| SyntheticMVarKind.coe header expectedType eType e f? =>
withMVarContext mvarSyntheticDecl.mvarId do
let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId
throwTypeMismatchError header expectedType eType e f? (some ("failed to create type class instance for " ++ indentExpr mvarDecl.type))
| _ => unreachable! -- TODO handle other cases.
let s ← get
for mvarSyntheticDecl in s.syntheticMVars do
withRef mvarSyntheticDecl.stx do
match mvarSyntheticDecl.kind with
| SyntheticMVarKind.typeClass =>
withMVarContext mvarSyntheticDecl.mvarId do
let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId
logError $ "failed to create type class instance for " ++ indentExpr mvarDecl.type
| SyntheticMVarKind.coe header expectedType eType e f? =>
withMVarContext mvarSyntheticDecl.mvarId do
let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId
throwTypeMismatchError header expectedType eType e f? (some ("failed to create type class instance for " ++ indentExpr mvarDecl.type))
| _ => unreachable! -- TODO handle other cases.
private def getSomeSynthethicMVarsRef : TermElabM Syntax := do
let s ← get
match s.syntheticMVars.find? $ fun (mvarDecl : SyntheticMVarDecl) => !mvarDecl.stx.getPos.isNone with
| some mvarDecl => pure mvarDecl.stx
| none => pure Syntax.missing
let s ← get
match s.syntheticMVars.find? $ fun (mvarDecl : SyntheticMVarDecl) => !mvarDecl.stx.getPos.isNone with
| some mvarDecl => pure mvarDecl.stx
| none => pure Syntax.missing
/--
Try to process pending synthetic metavariables. If `mayPostpone == false`,
@ -194,67 +192,67 @@ match s.syntheticMVars.find? $ fun (mvarDecl : SyntheticMVarDecl) => !mvarDecl.s
with `mayPostpone == false`. That is, we force them to produce error messages and/or commit to
a "best option". If, after that, we still haven't made progress, we report "stuck" errors. -/
partial def synthesizeSyntheticMVars (mayPostpone := true) : TermElabM Unit :=
let rec loop (u : Unit) : TermElabM Unit := do
let ref ← getSomeSynthethicMVarsRef
withRef ref $ withIncRecDepth do
let s ← get
unless s.syntheticMVars.isEmpty do
if ← synthesizeSyntheticMVarsStep false false then
loop ()
else if !mayPostpone then
/- Resume pending metavariables with "elaboration postponement" disabled.
We postpone elaboration errors in this step by setting `postponeOnError := true`.
Example:
```
#check let x := ⟨1, 2⟩; Prod.fst x
```
The term `⟨1, 2⟩` can't be elaborated because the expected type is not know.
The `x` at `Prod.fst x` is not elaborated because the type of `x` is not known.
When we execute the following step with "elaboration postponement" disabled,
the elaborator fails at `⟨1, 2⟩` and postpones it, and succeeds at `x` and learns
that its type must be of the form `Prod ?α ?β`.
let rec loop (u : Unit) : TermElabM Unit := do
let ref ← getSomeSynthethicMVarsRef
withRef ref $ withIncRecDepth do
let s ← get
unless s.syntheticMVars.isEmpty do
if ← synthesizeSyntheticMVarsStep false false then
loop ()
else if !mayPostpone then
/- Resume pending metavariables with "elaboration postponement" disabled.
We postpone elaboration errors in this step by setting `postponeOnError := true`.
Example:
```
#check let x := ⟨1, 2⟩; Prod.fst x
```
The term `⟨1, 2⟩` can't be elaborated because the expected type is not know.
The `x` at `Prod.fst x` is not elaborated because the type of `x` is not known.
When we execute the following step with "elaboration postponement" disabled,
the elaborator fails at `⟨1, 2⟩` and postpones it, and succeeds at `x` and learns
that its type must be of the form `Prod ?α ?β`.
Recall that we postponed `x` at `Prod.fst x` because its type it is not known.
We the type of `x` may learn later its type and it may contain implicit and/or auto arguments.
By disabling postponement, we are essentially giving up the opportunity of learning `x`s type
and assume it does not have implict and/or auto arguments. -/
if ← withoutPostponing (synthesizeSyntheticMVarsStep true false) then
loop ()
else if ← synthesizeUsingDefault then
loop ()
else if ← withoutPostponing (synthesizeSyntheticMVarsStep false false) then
loop ()
else if ← synthesizeSyntheticMVarsStep false true then
loop ()
else
reportStuckSyntheticMVars
loop ()
Recall that we postponed `x` at `Prod.fst x` because its type it is not known.
We the type of `x` may learn later its type and it may contain implicit and/or auto arguments.
By disabling postponement, we are essentially giving up the opportunity of learning `x`s type
and assume it does not have implict and/or auto arguments. -/
if ← withoutPostponing (synthesizeSyntheticMVarsStep true false) then
loop ()
else if ← synthesizeUsingDefault then
loop ()
else if ← withoutPostponing (synthesizeSyntheticMVarsStep false false) then
loop ()
else if ← synthesizeSyntheticMVarsStep false true then
loop ()
else
reportStuckSyntheticMVars
loop ()
def synthesizeSyntheticMVarsNoPostponing : TermElabM Unit :=
synthesizeSyntheticMVars (mayPostpone := false)
synthesizeSyntheticMVars (mayPostpone := false)
/--
Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
If `mayPostpone == false`, then all of them must be synthesized.
Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault` -/
def withSynthesize {α} (k : TermElabM α) (mayPostpone := false) : TermElabM α := do
let s ← get
let syntheticMVarsSaved := s.syntheticMVars
modify fun s => { s with syntheticMVars := [] }
try
let a ← k
synthesizeSyntheticMVars mayPostpone
if mayPostpone then
if (← synthesizeUsingDefault) then
synthesizeSyntheticMVars mayPostpone
pure a
finally
modify fun s => { s with syntheticMVars := s.syntheticMVars ++ syntheticMVarsSaved }
let s ← get
let syntheticMVarsSaved := s.syntheticMVars
modify fun s => { s with syntheticMVars := [] }
try
let a ← k
synthesizeSyntheticMVars mayPostpone
if mayPostpone then
if (← synthesizeUsingDefault) then
synthesizeSyntheticMVars mayPostpone
pure a
finally
modify fun s => { s with syntheticMVars := s.syntheticMVars ++ syntheticMVarsSaved }
/-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/
def elabTermAndSynthesize (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
withRef stx do
let v ← withSynthesize $ elabTerm stx expectedType?
instantiateMVars v
withRef stx do
let v ← withSynthesize $ elabTerm stx expectedType?
instantiateMVars v
end Lean.Elab.Term