diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean index 28dc338d99..67b6f16fdb 100644 --- a/src/Lean/Elab/DeclUtil.lean +++ b/src/Lean/Elab/DeclUtil.lean @@ -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 diff --git a/src/Lean/Elab/Exception.lean b/src/Lean/Elab/Exception.lean index 1e0adddbed..5cb9d1fc24 100644 --- a/src/Lean/Elab/Exception.lean +++ b/src/Lean/Elab/Exception.lean @@ -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 diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index cac33748ab..7f8e320c4e 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -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 "" -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 "" + 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 diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean index d7f7d6f199..81a8b91260 100644 --- a/src/Lean/Elab/Import.lean +++ b/src/Lean/Elab/Import.lean @@ -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 "" -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 "" + 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 diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index c538c4e3a4..b3674534f6 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -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 diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 7bb5d5c3c5..568e492593 100644 --- a/src/Lean/Elab/Level.lean +++ b/src/Lean/Elab/Level.lean @@ -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 diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean index f9233b7a6b..ea611b48ac 100644 --- a/src/Lean/Elab/Log.lean +++ b/src/Lean/Elab/Log.lean @@ -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 diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index 1685a5f896..3d2528eb41 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -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 diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 6b9b43eefe..2188b43306 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -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 diff --git a/src/Lean/Elab/StrategyAttrs.lean b/src/Lean/Elab/StrategyAttrs.lean index c900509044..beefc14f42 100644 --- a/src/Lean/Elab/StrategyAttrs.lean +++ b/src/Lean/Elab/StrategyAttrs.lean @@ -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 diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index e9ace9d044..22c7de451c 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -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 ':' 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 ':' 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 [] ...`)" -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 [] ...`)" 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] diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index db2e564b97..7056b66659 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -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