From d640105dcc939458fda120b472fa8e08487118ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Oct 2020 11:02:01 -0700 Subject: [PATCH] chore: cleanup --- src/Lean/Elab/Term.lean | 1245 +++++++++++++++++++-------------------- 1 file changed, 618 insertions(+), 627 deletions(-) diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 56b06ffded..a6bcd10c89 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -65,78 +65,78 @@ namespace Lean.Elab.Term first-order unification. -/ def setElabConfig (cfg : Meta.Config) : Meta.Config := -{ cfg with foApprox := true, ctxApprox := true, constApprox := false, quasiPatternApprox := false } + { cfg with foApprox := true, ctxApprox := true, constApprox := false, quasiPatternApprox := false } structure Context := -(fileName : String) -(fileMap : FileMap) -(currNamespace : Name) -(declName? : Option Name := none) -(levelNames : List Name := []) -(openDecls : List OpenDecl := []) -(macroStack : MacroStack := []) -(currMacroScope : MacroScope := firstFrontendMacroScope) -/- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`. - The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in - the list of pending synthetic metavariables, and returns `?m`. -/ -(mayPostpone : Bool := true) -/- When `errToSorry` is set to true, the method `elabTerm` catches - exceptions and converts them into synthetic `sorry`s. - The implementation of choice nodes and overloaded symbols rely on the fact - that when `errToSorry` is set to false for an elaboration function `F`, then - `errToSorry` remains `false` for all elaboration functions invoked by `F`. - That is, it is safe to transition `errToSorry` from `true` to `false`, but - we must not set `errToSorry` to `true` when it is currently set to `false`. -/ -(errToSorry : Bool := true) + (fileName : String) + (fileMap : FileMap) + (currNamespace : Name) + (declName? : Option Name := none) + (levelNames : List Name := []) + (openDecls : List OpenDecl := []) + (macroStack : MacroStack := []) + (currMacroScope : MacroScope := firstFrontendMacroScope) + /- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`. + The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in + the list of pending synthetic metavariables, and returns `?m`. -/ + (mayPostpone : Bool := true) + /- When `errToSorry` is set to true, the method `elabTerm` catches + exceptions and converts them into synthetic `sorry`s. + The implementation of choice nodes and overloaded symbols rely on the fact + that when `errToSorry` is set to false for an elaboration function `F`, then + `errToSorry` remains `false` for all elaboration functions invoked by `F`. + That is, it is safe to transition `errToSorry` from `true` to `false`, but + we must not set `errToSorry` to `true` when it is currently set to `false`. -/ + (errToSorry : Bool := true) /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/ inductive SyntheticMVarKind --- typeclass instance search -| typeClass -/- Similar to typeClass, but error messages are different. - if `f?` is `some f`, we produce an application type mismatch error message. - Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` - Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/ -| coe (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) --- tactic block execution -| tactic (declName? : Option Name) (tacticCode : Syntax) --- `elabTerm` call that threw `Exception.postpone` (input is stored at `SyntheticMVarDecl.ref`) -| postponed (macroStack : MacroStack) (declName? : Option Name) --- type defaulting (currently: defaulting numeric literals to `Nat`) -| withDefault (defaultVal : Expr) + -- typeclass instance search + | typeClass + /- Similar to typeClass, but error messages are different. + if `f?` is `some f`, we produce an application type mismatch error message. + Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` + Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/ + | coe (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) + -- tactic block execution + | tactic (declName? : Option Name) (tacticCode : Syntax) + -- `elabTerm` call that threw `Exception.postpone` (input is stored at `SyntheticMVarDecl.ref`) + | postponed (macroStack : MacroStack) (declName? : Option Name) + -- type defaulting (currently: defaulting numeric literals to `Nat`) + | withDefault (defaultVal : Expr) structure SyntheticMVarDecl := -(mvarId : MVarId) (stx : Syntax) (kind : SyntheticMVarKind) + (mvarId : MVarId) (stx : Syntax) (kind : SyntheticMVarKind) inductive MVarErrorKind -| implicitArg (ctx : Expr) -| hole -| custom (msgData : MessageData) + | implicitArg (ctx : Expr) + | hole + | custom (msgData : MessageData) structure MVarErrorInfo := -(mvarId : MVarId) -(ref : Syntax) -(kind : MVarErrorKind) + (mvarId : MVarId) + (ref : Syntax) + (kind : MVarErrorKind) structure LetRecToLift := -(ref : Syntax) -(fvarId : FVarId) -(attrs : Array Attribute) -(shortDeclName : Name) -(declName : Name) -(lctx : LocalContext) -(localInstances : LocalInstances) -(type : Expr) -(val : Expr) -(mvarId : MVarId) + (ref : Syntax) + (fvarId : FVarId) + (attrs : Array Attribute) + (shortDeclName : Name) + (declName : Name) + (lctx : LocalContext) + (localInstances : LocalInstances) + (type : Expr) + (val : Expr) + (mvarId : MVarId) structure State := -(syntheticMVars : List SyntheticMVarDecl := []) -(mvarErrorInfos : List MVarErrorInfo := []) -(messages : MessageLog := {}) -(letRecsToLift : List LetRecToLift := []) + (syntheticMVars : List SyntheticMVarDecl := []) + (mvarErrorInfos : List MVarErrorInfo := []) + (messages : MessageLog := {}) + (letRecsToLift : List LetRecToLift := []) -instance State.inhabited : Inhabited State := ⟨{}⟩ +instance : Inhabited State := ⟨{}⟩ abbrev TermElabM := ReaderT Context $ StateRefT State $ MetaM abbrev TermElab := Syntax → Option Expr → TermElabM Expr @@ -144,78 +144,80 @@ abbrev TermElab := Syntax → Option Expr → TermElabM Expr open Meta instance TermElabM.inhabited {α} : Inhabited (TermElabM α) := -⟨throw $ arbitrary _⟩ + ⟨throw $ arbitrary _⟩ structure SavedState := -(core : Core.State) -(meta : Meta.State) -(«elab» : State) + (core : Core.State) + (meta : Meta.State) + («elab» : State) -instance SavedState.inhabited : Inhabited SavedState := ⟨⟨arbitrary _, arbitrary _, arbitrary _⟩⟩ +instance : Inhabited SavedState := ⟨⟨arbitrary _, arbitrary _, arbitrary _⟩⟩ def saveAllState : TermElabM SavedState := do -pure { core := (← getThe Core.State), meta := (← getThe Meta.State), «elab» := (← get) } + pure { core := (← getThe Core.State), meta := (← getThe Meta.State), «elab» := (← get) } def SavedState.restore (s : SavedState) : TermElabM Unit := do -let traceState ← getTraceState -- We never backtrack trace message -set s.core -set s.meta -set s.elab -setTraceState traceState + let traceState ← getTraceState -- We never backtrack trace message + set s.core + set s.meta + set s.elab + setTraceState traceState abbrev TermElabResult := EStateM.Result Exception SavedState Expr -instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩ +instance : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩ def setMessageLog (messages : MessageLog) : TermElabM Unit := -modify fun s => { s with messages := messages } + modify fun s => { s with messages := messages } def resetMessageLog : TermElabM Unit := do -setMessageLog {} + setMessageLog {} def getMessageLog : TermElabM MessageLog := do -pure (← get).messages + pure (← get).messages /-- Execute `x`, save resulting expression and new state. If `x` fails, then it also stores exception and new state. Remark: we do not capture `Exception.postpone`. -/ @[inline] def observing (x : TermElabM Expr) : TermElabM TermElabResult := do -let s ← saveAllState -try - let e ← x - let sNew ← saveAllState - s.restore - pure (EStateM.Result.ok e sNew) -catch - | ex@(Exception.error _ _) => + let s ← saveAllState + try + let e ← x let sNew ← saveAllState s.restore - pure (EStateM.Result.error ex sNew) - | ex@(Exception.internal id) => - if id == postponeExceptionId then s.restore - throw ex + pure (EStateM.Result.ok e sNew) + catch + | ex@(Exception.error _ _) => + let sNew ← saveAllState + s.restore + pure (EStateM.Result.error ex sNew) + | ex@(Exception.internal id) => + if id == postponeExceptionId then s.restore + throw ex /-- Apply the result/exception and state captured with `observing`. We use this method to implement overloaded notation and symbols. -/ def applyResult (result : TermElabResult) : TermElabM Expr := -match result with -| EStateM.Result.ok e r => do r.restore; pure e -| EStateM.Result.error ex r => do r.restore; throw ex + match result with + | EStateM.Result.ok e r => do r.restore; pure e + | EStateM.Result.error ex r => do r.restore; throw ex instance : MonadIO TermElabM := { liftIO := fun x => liftMetaM $ liftIO x } @[inline] protected def liftMetaM {α} (x : MetaM α) : TermElabM α := do -liftM x + liftM x @[inline] def liftCoreM {α} (x : CoreM α) : TermElabM α := -Term.liftMetaM $ liftM x + Term.liftMetaM $ liftM x instance : MonadLiftT MetaM TermElabM := -⟨Term.liftMetaM⟩ + ⟨Term.liftMetaM⟩ + +def getLevelNames : TermElabM (List Name) := do + pure (← read).levelNames -def getLevelNames : TermElabM (List Name) := do pure (← read).levelNames def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do match (← getLCtx).find? fvar.fvarId! with | some d => pure d @@ -226,16 +228,17 @@ def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do -- { getRef := getRef, -- withRef := withRef } -instance : AddErrorMessageContext TermElabM := -{ add := fun ref msg => do - let ctx ← read - let ref := getBetterRef ref ctx.macroStack - let msg ← addMessageContext msg - let msg ← addMacroStack msg ctx.macroStack - pure (ref, msg) } +instance : AddErrorMessageContext TermElabM := { + add := fun ref msg => do + let ctx ← read + let ref := getBetterRef ref ctx.macroStack + let msg ← addMessageContext msg + let msg ← addMacroStack msg ctx.macroStack + pure (ref, msg) +} -instance monadLog : MonadLog TermElabM := -{ getRef := getRef, +instance monadLog : MonadLog TermElabM := { + getRef := getRef, getFileMap := do pure (← read).fileMap, getFileName := do pure (← read).fileName, logMessage := fun msg => do @@ -248,8 +251,8 @@ protected def getCurrMacroScope : TermElabM MacroScope := do pure (← read).cur protected def getMainModule : TermElabM Name := do pure (← getEnv).mainModule @[inline] protected def withFreshMacroScope {α} (x : TermElabM α) : TermElabM α := do -let fresh ← modifyGetThe Core.State (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 })) -withReader (fun ctx => { ctx with currMacroScope := fresh }) x + let fresh ← modifyGetThe Core.State (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 })) + withReader (fun ctx => { ctx with currMacroScope := fresh }) x instance monadQuotation : MonadQuotation TermElabM := { getCurrMacroScope := Term.getCurrMacroScope, @@ -258,7 +261,7 @@ instance monadQuotation : MonadQuotation TermElabM := { } unsafe def mkTermElabAttributeUnsafe : IO (KeyedDeclsAttribute TermElab) := -mkElabAttribute TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" + mkElabAttribute TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" @[implementedBy mkTermElabAttributeUnsafe] constant mkTermElabAttribute : IO (KeyedDeclsAttribute TermElab) @@ -272,16 +275,17 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl `[LVal.fieldName "foo", LVal.getOp i, LVal.fieldIdx 1]`. Recall that the notation `a[i]` is not just for accessing arrays in Lean. -/ inductive LVal -| fieldIdx (i : Nat) -| fieldName (name : String) -| getOp (idx : Syntax) + | fieldIdx (i : Nat) + | fieldName (name : String) + | getOp (idx : Syntax) instance LVal.hasToString : HasToString LVal := -⟨fun p => match p with | LVal.fieldIdx i => toString i | LVal.fieldName n => n | LVal.getOp idx => "[" ++ toString idx ++ "]"⟩ + ⟨fun p => match p with | LVal.fieldIdx i => toString i | LVal.fieldName n => n | LVal.getOp idx => "[" ++ toString idx ++ "]"⟩ -instance : MonadResolveName TermElabM := -{ getCurrNamespace := do pure (← read).currNamespace, - getOpenDecls := do pure (← read).openDecls } +instance : MonadResolveName TermElabM := { + getCurrNamespace := do pure (← read).currNamespace, + getOpenDecls := do pure (← read).openDecls +} def getDeclName? : TermElabM (Option Name) := do pure (← read).declName? def getLetRecsToLift : TermElabM (List LetRecToLift) := do pure (← get).letRecsToLift @@ -290,18 +294,18 @@ def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := do return (← getM def assignLevelMVar (mvarId : MVarId) (val : Level) : TermElabM Unit := modifyThe Meta.State fun s => { s with mctx := s.mctx.assignLevel mvarId val } def withDeclName {α} (name : Name) (x : TermElabM α) : TermElabM α := -withReader (fun ctx => { ctx with declName? := name }) x + withReader (fun ctx => { ctx with declName? := name }) x def withLevelNames {α} (levelNames : List Name) (x : TermElabM α) : TermElabM α := -withReader (fun ctx => { ctx with levelNames := levelNames }) x + withReader (fun ctx => { ctx with levelNames := levelNames }) x def withoutErrToSorry {α} (x : TermElabM α) : TermElabM α := -withReader (fun ctx => { ctx with errToSorry := false }) x + withReader (fun ctx => { ctx with errToSorry := false }) x /-- For testing `TermElabM` methods. The #eval command will sign the error. -/ def throwErrorIfErrors : TermElabM Unit := do -if (← get).messages.hasErrors then - throwError "Error(s)" + if (← get).messages.hasErrors then + throwError "Error(s)" @[inline] def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TermElabM Unit := withRef Syntax.missing $ trace cls msg @@ -309,71 +313,71 @@ withRef Syntax.missing $ trace cls msg def ppGoal (mvarId : MVarId) : TermElabM Format := liftMetaM $ Meta.ppGoal mvarId @[inline] def savingMCtx {α} (x : TermElabM α) : TermElabM α := do -let mctx ← getMCtx -try x finally setMCtx mctx + let mctx ← getMCtx + try x finally setMCtx mctx open Level (LevelElabM) def liftLevelM {α} (x : LevelElabM α) : TermElabM α := do -let ctx ← read -let ref ← getRef -let mctx ← getMCtx -let ngen ← getNGen -let lvlCtx : Level.Context := { ref := ref, levelNames := ctx.levelNames } -match (x lvlCtx).run { ngen := ngen, mctx := mctx } with -| EStateM.Result.ok a newS => do setMCtx newS.mctx; setNGen newS.ngen; pure a -| EStateM.Result.error ex _ => throw ex + let ctx ← read + let ref ← getRef + let mctx ← getMCtx + let ngen ← getNGen + let lvlCtx : Level.Context := { ref := ref, levelNames := ctx.levelNames } + match (x lvlCtx).run { ngen := ngen, mctx := mctx } with + | EStateM.Result.ok a newS => do setMCtx newS.mctx; setNGen newS.ngen; pure a + | EStateM.Result.error ex _ => throw ex def elabLevel (stx : Syntax) : TermElabM Level := -liftLevelM $ Level.elabLevel stx + liftLevelM $ Level.elabLevel stx /- Elaborate `x` with `stx` on the macro stack -/ @[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α := -withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x + withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x /- Add the given metavariable to the list of pending synthetic metavariables. The method `synthesizeSyntheticMVars` is used to process the metavariables on this list. -/ def registerSyntheticMVar (stx : Syntax) (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do -modify fun s => { s with syntheticMVars := { mvarId := mvarId, stx := stx, kind := kind } :: s.syntheticMVars } + modify fun s => { s with syntheticMVars := { mvarId := mvarId, stx := stx, kind := kind } :: s.syntheticMVars } def registerSyntheticMVarWithCurrRef (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do -registerSyntheticMVar (← getRef) mvarId kind + registerSyntheticMVar (← getRef) mvarId kind def registerMVarErrorHoleInfo (mvarId : MVarId) (ref : Syntax) : TermElabM Unit := do -modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.hole } :: s.mvarErrorInfos } + modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.hole } :: s.mvarErrorInfos } def registerMVarErrorImplicitArgInfo (mvarId : MVarId) (ref : Syntax) (app : Expr) : TermElabM Unit := do -modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.implicitArg app } :: s.mvarErrorInfos } + modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.implicitArg app } :: s.mvarErrorInfos } def registerMVarErrorCustomInfo (mvarId : MVarId) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := do -modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.custom msgData } :: s.mvarErrorInfos } + modify fun s => { s with mvarErrorInfos := { mvarId := mvarId, ref := ref, kind := MVarErrorKind.custom msgData } :: s.mvarErrorInfos } def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := -match e.getAppFn with -| Expr.mvar mvarId _ => registerMVarErrorCustomInfo mvarId ref msgData -| _ => pure () + match e.getAppFn with + | Expr.mvar mvarId _ => registerMVarErrorCustomInfo mvarId ref msgData + | _ => pure () def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit := do -match mvarErrorInfo.kind with -| MVarErrorKind.implicitArg app => do - let app ← instantiateMVars app - let f := app.getAppFn - let args := app.getAppArgs - let msg := args.foldl (init := "@" ++ MessageData.ofExpr f) fun (msg : MessageData) (arg : Expr) => - if arg.getAppFn.isMVar then - msg ++ " " ++ arg.getAppFn - else - msg ++ " …" - let msg : MessageData := "don't know how to synthesize implicit argument" ++ indentD msg - let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId - logErrorAt mvarErrorInfo.ref msg -| MVarErrorKind.hole => do - let msg : MessageData := "don't know how to synthesize placeholder" - let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId - logErrorAt mvarErrorInfo.ref msg -| MVarErrorKind.custom msgData => - logErrorAt mvarErrorInfo.ref msgData + match mvarErrorInfo.kind with + | MVarErrorKind.implicitArg app => do + let app ← instantiateMVars app + let f := app.getAppFn + let args := app.getAppArgs + let msg := args.foldl (init := "@" ++ MessageData.ofExpr f) fun (msg : MessageData) (arg : Expr) => + if arg.getAppFn.isMVar then + msg ++ " " ++ arg.getAppFn + else + msg ++ " …" + let msg : MessageData := "don't know how to synthesize implicit argument" ++ indentD msg + let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId + logErrorAt mvarErrorInfo.ref msg + | MVarErrorKind.hole => do + let msg : MessageData := "don't know how to synthesize placeholder" + let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId + logErrorAt mvarErrorInfo.ref msg + | MVarErrorKind.custom msgData => + logErrorAt mvarErrorInfo.ref msgData /-- Try to log errors for the unassigned metavariables `pendingMVarIds`. @@ -381,40 +385,40 @@ match mvarErrorInfo.kind with Remark: This method only succeeds if we have information for at least one given metavariable at `mvarErrorInfos`. -/ def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) : TermElabM Bool := do -let s ← get -let errorInfos := s.mvarErrorInfos -let (foundErrors, _) ← errorInfos.foldlM (init := (false, {})) fun (foundErrors, (alreadyVisited : NameSet)) mvarErrorInfo => do - let mvarId := mvarErrorInfo.mvarId; - if alreadyVisited.contains mvarId then - pure (foundErrors, alreadyVisited) - else do - let alreadyVisited := alreadyVisited.insert mvarId - /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or - delayed assigned to another metavariable that is unassigned. -/ - let mvarDeps ← getMVars (mkMVar mvarId) - if mvarDeps.any pendingMVarIds.contains then do - mvarErrorInfo.logError; - pure (true, alreadyVisited) - else + let s ← get + let errorInfos := s.mvarErrorInfos + let (foundErrors, _) ← errorInfos.foldlM (init := (false, {})) fun (foundErrors, (alreadyVisited : NameSet)) mvarErrorInfo => do + let mvarId := mvarErrorInfo.mvarId; + if alreadyVisited.contains mvarId then pure (foundErrors, alreadyVisited) -pure foundErrors + else do + let alreadyVisited := alreadyVisited.insert mvarId + /- The metavariable `mvarErrorInfo.mvarId` may have been assigned or + delayed assigned to another metavariable that is unassigned. -/ + let mvarDeps ← getMVars (mkMVar mvarId) + if mvarDeps.any pendingMVarIds.contains then do + mvarErrorInfo.logError; + pure (true, alreadyVisited) + else + pure (foundErrors, alreadyVisited) + pure foundErrors /-- Ensure metavariables registered using `registerMVarErrorInfos` (and used in the given declaration) have been assigned. -/ def ensureNoUnassignedMVars (decl : Declaration) : TermElabM Unit := do -let pendingMVarIds ← getMVarsAtDecl decl -let foundError ← logUnassignedUsingErrorInfos pendingMVarIds -if foundError then - throwAbort + let pendingMVarIds ← getMVarsAtDecl decl + let foundError ← logUnassignedUsingErrorInfos pendingMVarIds + if foundError then + throwAbort /- Execute `x` without allowing it to postpone elaboration tasks. That is, `tryPostpone` is a noop. -/ @[inline] def withoutPostponing {α} (x : TermElabM α) : TermElabM α := -withReader (fun ctx => { ctx with mayPostpone := false }) x + withReader (fun ctx => { ctx with mayPostpone := false }) x /-- Creates syntax for `(` `:` `)` -/ def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax := -mkNode `Lean.Parser.Term.explicitBinder #[mkAtom "(", mkNullNode #[ident], mkNullNode #[mkAtom ":", type], mkNullNode, mkAtom ")"] + mkNode `Lean.Parser.Term.explicitBinder #[mkAtom "(", mkNullNode #[ident], mkNullNode #[mkAtom ":", type], mkNullNode, mkAtom ")"] /-- Convert unassigned universe level metavariables into parameters. @@ -423,70 +427,70 @@ mkNode `Lean.Parser.Term.explicitBinder #[mkAtom "(", mkNullNode #[ident], mkNul Remark: we make sure the generated parameter names do not clash with the universes at `ctx.levelNames`. -/ def levelMVarToParam (e : Expr) (nextParamIdx : Nat := 1) : TermElabM (Expr × Nat) := do -let ctx ← read -let mctx ← getMCtx -let r := mctx.levelMVarToParam (fun n => ctx.levelNames.elem n) e `u nextParamIdx -setMCtx r.mctx -pure (r.expr, r.nextParamIdx) + let ctx ← read + let mctx ← getMCtx + let r := mctx.levelMVarToParam (fun n => ctx.levelNames.elem n) e `u nextParamIdx + setMCtx r.mctx + pure (r.expr, r.nextParamIdx) /-- Variant of `levelMVarToParam` where `nextParamIdx` is stored in a state monad. -/ def levelMVarToParam' (e : Expr) : StateRefT Nat TermElabM Expr := do -let nextParamIdx ← get -let (e, nextParamIdx) ← levelMVarToParam e nextParamIdx -set nextParamIdx -pure e + let nextParamIdx ← get + let (e, nextParamIdx) ← levelMVarToParam e nextParamIdx + set nextParamIdx + pure e /-- Auxiliary method for creating fresh binder names. Do not confuse with the method for creating fresh free/meta variable ids. -/ def mkFreshBinderName : TermElabM Name := -withFreshMacroScope $ MonadQuotation.addMacroScope `x + withFreshMacroScope $ MonadQuotation.addMacroScope `x /-- Auxiliary method for creating a `Syntax.ident` containing a fresh name. This method is intended for creating fresh binder names. It is just a thin layer on top of `mkFreshUserName`. -/ def mkFreshIdent (ref : Syntax) : TermElabM Syntax := do -let n ← mkFreshBinderName -pure $ mkIdentFrom ref n + let n ← mkFreshBinderName + pure $ mkIdentFrom ref n /-- Auxiliary method for creating binder names for local instances. -/ def mkFreshInstanceName : TermElabM Name := -withFreshMacroScope $ MonadQuotation.addMacroScope `inst + withFreshMacroScope $ MonadQuotation.addMacroScope `inst private def liftAttrM {α} (x : AttrM α) : TermElabM α := do -let ctx ← read -liftCoreM $ x.run { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } + let ctx ← read + liftCoreM $ x.run { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } private def applyAttributesCore (declName : Name) (attrs : Array Attribute) (applicationTime? : Option AttributeApplicationTime) (persistent : Bool) : TermElabM Unit := do -for attr in attrs do - let env ← getEnv - match getAttributeImpl env attr.name with - | Except.error errMsg => throwError errMsg - | Except.ok attrImpl => - match applicationTime? with - | none => liftAttrM $ attrImpl.add declName attr.args persistent - | some applicationTime => - if applicationTime == attrImpl.applicationTime then - liftAttrM $ attrImpl.add declName attr.args persistent + for attr in attrs do + let env ← getEnv + match getAttributeImpl env attr.name with + | Except.error errMsg => throwError errMsg + | Except.ok attrImpl => + match applicationTime? with + | none => liftAttrM $ attrImpl.add declName attr.args persistent + | some applicationTime => + if applicationTime == attrImpl.applicationTime then + liftAttrM $ attrImpl.add declName attr.args persistent /-- Apply given attributes **at** a given application time -/ def applyAttributesAt (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) (persistent : Bool := true) : TermElabM Unit := -applyAttributesCore declName attrs applicationTime persistent + applyAttributesCore declName attrs applicationTime persistent def applyAttributes (declName : Name) (attrs : Array Attribute) (persistent : Bool) : TermElabM Unit := -applyAttributesCore declName attrs none persistent + applyAttributesCore declName attrs none persistent /- Elaboration functions -/ private partial def hasCDot : Syntax → Bool -| Syntax.node k args => - if k == `Lean.Parser.Term.paren then false - else if k == `Lean.Parser.Term.cdot then true - else args.any hasCDot -| _ => false + | Syntax.node k args => + if k == `Lean.Parser.Term.paren then false + else if k == `Lean.Parser.Term.cdot then true + else args.any hasCDot + | _ => false /-- Auxiliary function for expandind the `·` notation. @@ -494,16 +498,16 @@ private partial def hasCDot : Syntax → Bool If `stx` is a `·`, we create a fresh identifier, store in the extra state, and return it. Otherwise, we just return `stx`. -/ private partial def expandCDot : Syntax → StateT (Array Syntax) MacroM Syntax -| stx@(Syntax.node k args) => - if k == `Lean.Parser.Term.paren then pure stx - else if k == `Lean.Parser.Term.cdot then withFreshMacroScope do - let id ← `(a) - modify fun s => s.push id; - pure id - else do - let args ← args.mapM expandCDot - pure $ Syntax.node k args -| stx => pure stx + | stx@(Syntax.node k args) => + if k == `Lean.Parser.Term.paren then pure stx + else if k == `Lean.Parser.Term.cdot then withFreshMacroScope do + let id ← `(a) + modify fun s => s.push id; + pure id + else do + let args ← args.mapM expandCDot + pure $ Syntax.node k args + | stx => pure stx /-- Return `some` if succeeded expanding `·` notation occurring in @@ -512,41 +516,41 @@ private partial def expandCDot : Syntax → StateT (Array Syntax) MacroM Syntax - `· + 1` => `fun _a_1 => _a_1 + 1` - `f · · b` => `fun _a_1 _a_2 => f _a_1 _a_2 b` -/ def expandCDot? (stx : Syntax) : MacroM (Option Syntax) := do -if hasCDot stx then - let (newStx, binders) ← (expandCDot stx).run #[]; - `(fun $binders* => $newStx) -else - pure none + if hasCDot stx then + let (newStx, binders) ← (expandCDot stx).run #[]; + `(fun $binders* => $newStx) + else + pure none def mkTypeMismatchError (header? : Option String) (e : Expr) (eType : Expr) (expectedType : Expr) : MessageData := -let header : MessageData := match header? with - | some header => msg!"{header} has type" - | none => msg!"type mismatch{indentExpr e}\nhas type" -msg!"{header}{indentExpr eType}\nbut is expected to have type{indentExpr expectedType}" + let header : MessageData := match header? with + | some header => msg!"{header} has type" + | none => msg!"type mismatch{indentExpr e}\nhas type" + msg!"{header}{indentExpr eType}\nbut is expected to have type{indentExpr expectedType}" def throwTypeMismatchError {α} (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α := -/- - We ignore `extraMsg?` for now. In all our tests, it contained no useful information. It was - always of the form: - ``` - failed to synthesize instance - CoeT - ``` - We should revisit this decision in the future and decide whether it may contain useful information - or not. -/ -let extraMsg := Format.nil -/- -let extraMsg : MessageData := match extraMsg? with - | none => Format.nil - | some extraMsg => Format.line ++ extraMsg; --/ -match f? with -| none => throwError $ mkTypeMismatchError header? e eType expectedType ++ extraMsg -| some f => Meta.throwAppTypeMismatch f e extraMsg + /- + We ignore `extraMsg?` for now. In all our tests, it contained no useful information. It was + always of the form: + ``` + failed to synthesize instance + CoeT + ``` + We should revisit this decision in the future and decide whether it may contain useful information + or not. -/ + let extraMsg := Format.nil + /- + let extraMsg : MessageData := match extraMsg? with + | none => Format.nil + | some extraMsg => Format.line ++ extraMsg; + -/ + match f? with + | none => throwError $ mkTypeMismatchError header? e eType expectedType ++ extraMsg + | some f => Meta.throwAppTypeMismatch f e extraMsg @[inline] def withoutMacroStackAtErr {α} (x : TermElabM α) : TermElabM α := -withTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := setMacroStackOption ctx.options false }) x + withTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := setMacroStackOption ctx.options false }) x /- Try to synthesize metavariable using type class resolution. This method assumes the local context and local instances of `instMVar` coincide @@ -555,34 +559,34 @@ withTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := se the instance contains unassigned metavariables that are blocking the type class resolution procedure. Throw an exception if resolution or assignment irrevocably fails. -/ def synthesizeInstMVarCore (instMVar : MVarId) : TermElabM Bool := do -let instMVarDecl ← getMVarDecl instMVar -let type := instMVarDecl.type -let type ← instantiateMVars type -let result ← trySynthInstance type -match result with -| LOption.some val => - if (← isExprMVarAssigned instMVar) then - let oldVal ← instantiateMVars (mkMVar instMVar) - unless (← isDefEq oldVal val) do - throwError! "synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized{indentExpr val}\ninferred{indentExpr oldVal}" - else - assignExprMVar instMVar val - pure true -| LOption.undef => pure false -- we will try later -| LOption.none => throwError! "failed to synthesize instance{indentExpr type}" + let instMVarDecl ← getMVarDecl instMVar + let type := instMVarDecl.type + let type ← instantiateMVars type + let result ← trySynthInstance type + match result with + | LOption.some val => + if (← isExprMVarAssigned instMVar) then + let oldVal ← instantiateMVars (mkMVar instMVar) + unless (← isDefEq oldVal val) do + throwError! "synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized{indentExpr val}\ninferred{indentExpr oldVal}" + else + assignExprMVar instMVar val + pure true + | LOption.undef => pure false -- we will try later + | LOption.none => throwError! "failed to synthesize instance{indentExpr type}" /- The coercion from `α` to `Thunk α` cannot be implemented using an instance because it would eagerly evaluate `e` -/ def tryCoeThunk? (expectedType : Expr) (eType : Expr) (e : Expr) : TermElabM (Option Expr) := do -match expectedType with -| Expr.app (Expr.const `Thunk u _) arg _ => - if (← isDefEq eType arg) then - pure (some (mkApp2 (mkConst `Thunk.mk u) arg (mkSimpleThunk e))) - else + match expectedType with + | Expr.app (Expr.const `Thunk u _) arg _ => + if (← isDefEq eType arg) then + pure (some (mkApp2 (mkConst `Thunk.mk u) arg (mkSimpleThunk e))) + else + pure none + | _ => pure none -| _ => - pure none /-- Try to apply coercion to make sure `e` has type `expectedType`. @@ -592,56 +596,56 @@ match expectedType with abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β ``` -/ private def tryCoe (errorMsgHeader? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Expr := do -if (← isDefEq expectedType eType) then - pure e -else match (← tryCoeThunk? expectedType eType e) with - | some r => pure r - | none => - let u ← getLevel eType - let v ← getLevel expectedType - let coeTInstType := mkAppN (mkConst `CoeT [u, v]) #[eType, e, expectedType] - let mvar ← mkFreshExprMVar coeTInstType MetavarKind.synthetic - let eNew := mkAppN (mkConst `coe [u, v]) #[eType, expectedType, e, mvar] - let mvarId := mvar.mvarId! - try - withoutMacroStackAtErr do - unless (← synthesizeInstMVarCore mvarId) do - registerSyntheticMVarWithCurrRef mvarId (SyntheticMVarKind.coe errorMsgHeader? expectedType eType e f?) - pure eNew - catch - | Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg - | _ => throwTypeMismatchError errorMsgHeader? expectedType eType e f? + if (← isDefEq expectedType eType) then + pure e + else match (← tryCoeThunk? expectedType eType e) with + | some r => pure r + | none => + let u ← getLevel eType + let v ← getLevel expectedType + let coeTInstType := mkAppN (mkConst `CoeT [u, v]) #[eType, e, expectedType] + let mvar ← mkFreshExprMVar coeTInstType MetavarKind.synthetic + let eNew := mkAppN (mkConst `coe [u, v]) #[eType, expectedType, e, mvar] + let mvarId := mvar.mvarId! + try + withoutMacroStackAtErr do + unless (← synthesizeInstMVarCore mvarId) do + registerSyntheticMVarWithCurrRef mvarId (SyntheticMVarKind.coe errorMsgHeader? expectedType eType e f?) + pure eNew + catch + | Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg + | _ => throwTypeMismatchError errorMsgHeader? expectedType eType e f? private def isTypeApp? (type : Expr) : TermElabM (Option (Expr × Expr)) := do -let type ← withReducible $ whnf type -match type with -| Expr.app m α _ => pure (some (m, α)) -| _ => pure none + let type ← withReducible $ whnf type + match type with + | Expr.app m α _ => pure (some (m, α)) + | _ => pure none structure IsMonadResult := -(m : Expr) -(α : Expr) -(inst : Expr) + (m : Expr) + (α : Expr) + (inst : Expr) private def isMonad? (type : Expr) : TermElabM (Option IsMonadResult) := do -let type ← withReducible $ whnf type -match type with -| Expr.app m α _ => - try - let monadType ← mkAppM `Monad #[m] - let result ← trySynthInstance monadType - match result with - | LOption.some inst => pure (some { m := m, α := α, inst := inst }) - | _ => pure none - catch _ => pure none -| _ => pure none + let type ← withReducible $ whnf type + match type with + | Expr.app m α _ => + try + let monadType ← mkAppM `Monad #[m] + let result ← trySynthInstance monadType + match result with + | LOption.some inst => pure (some { m := m, α := α, inst := inst }) + | _ => pure none + catch _ => pure none + | _ => pure none def synthesizeInst (type : Expr) : TermElabM Expr := do -let type ← instantiateMVars type -match (← trySynthInstance type) with -| LOption.some val => pure val -| LOption.undef => throwError! "failed to synthesize instance{indentExpr type}" -| LOption.none => throwError! "failed to synthesize instance{indentExpr type}" + let type ← instantiateMVars type + match (← trySynthInstance type) with + | LOption.some val => pure val + | LOption.undef => throwError! "failed to synthesize instance{indentExpr type}" + | LOption.none => throwError! "failed to synthesize instance{indentExpr type}" /-- Try to coerce `a : α` into `m β` by first coercing `a : α` into ‵β`, and then using `pure`. @@ -665,22 +669,22 @@ match (← trySynthInstance type) with ``` -/ private def tryPureCoe? (errorMsgHeader? : Option String) (m β α a : Expr) : TermElabM (Option Expr) := do -let doIt (_ : Unit) : TermElabM (Option Expr) := do - try - let aNew ← tryCoe errorMsgHeader? β α a none - let aNew ← mkPure m aNew - pure (some aNew) - catch _ => - pure none -let αHead := α.getAppFn -if !β.getAppFn.isMVar && !αHead.isMVar then - doIt () -- case 1 -else - let αIsMonad? ← isMonad? α - if !αHead.isMVar && αIsMonad?.isNone then - doIt () -- case 2 + let doIt : TermElabM (Option Expr) := do + try + let aNew ← tryCoe errorMsgHeader? β α a none + let aNew ← mkPure m aNew + pure (some aNew) + catch _ => + pure none + let αHead := α.getAppFn + if !β.getAppFn.isMVar && !αHead.isMVar then + doIt -- case 1 else - pure none + let αIsMonad? ← isMonad? α + if !αHead.isMVar && αIsMonad?.isNone then + doIt -- case 2 + else + pure none /- Try coercions and monad lifts to make sure `e` has type `expectedType`. @@ -738,45 +742,45 @@ since this goal does not contain any metavariables. And then, we convert `g x` into `liftM $ g x`. -/ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Expr := do -let expectedType ← instantiateMVars expectedType -let eType ← instantiateMVars eType -let some ⟨n, β, monadInst⟩ ← isMonad? expectedType | tryCoe errorMsgHeader? expectedType eType e f? -let β ← instantiateMVars β -let eNew? ← tryPureCoe? errorMsgHeader? n β eType e -match eNew? with -| some eNew => pure eNew -| none => - let some (m, α) ← isTypeApp? eType | tryCoe errorMsgHeader? expectedType eType e f? - if (← isDefEq m n) then - try - mkAppOptM `coeM #[m, α, β, none, monadInst, e] - catch _ => - throwTypeMismatchError errorMsgHeader? expectedType eType e f? - else - try - -- Construct lift from `m` to `n` - let monadLiftType ← mkAppM `MonadLiftT #[m, n] - let monadLiftVal ← synthesizeInst monadLiftType - let u_1 ← getDecLevel α - let u_2 ← getDecLevel eType - let u_3 ← getDecLevel expectedType - let eNew := mkAppN (Lean.mkConst `liftM [u_1, u_2, u_3]) #[m, n, monadLiftVal, α, e] - let eNewType ← inferType eNew - if (← isDefEq expectedType eNewType) then - pure eNew -- approach 2 worked - else - let u ← getLevel α - let v ← getLevel β - let coeTInstType := Lean.mkForall `a BinderInfo.default α $ mkAppN (mkConst `CoeT [u, v]) #[α, mkBVar 0, β] - let coeTInstVal ← synthesizeInst coeTInstType - let eNew := mkAppN (Lean.mkConst `liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e] + let expectedType ← instantiateMVars expectedType + let eType ← instantiateMVars eType + let some ⟨n, β, monadInst⟩ ← isMonad? expectedType | tryCoe errorMsgHeader? expectedType eType e f? + let β ← instantiateMVars β + let eNew? ← tryPureCoe? errorMsgHeader? n β eType e + match eNew? with + | some eNew => pure eNew + | none => + let some (m, α) ← isTypeApp? eType | tryCoe errorMsgHeader? expectedType eType e f? + if (← isDefEq m n) then + try + mkAppOptM `coeM #[m, α, β, none, monadInst, e] + catch _ => + throwTypeMismatchError errorMsgHeader? expectedType eType e f? + else + try + -- Construct lift from `m` to `n` + let monadLiftType ← mkAppM `MonadLiftT #[m, n] + let monadLiftVal ← synthesizeInst monadLiftType + let u_1 ← getDecLevel α + let u_2 ← getDecLevel eType + let u_3 ← getDecLevel expectedType + let eNew := mkAppN (Lean.mkConst `liftM [u_1, u_2, u_3]) #[m, n, monadLiftVal, α, e] let eNewType ← inferType eNew if (← isDefEq expectedType eNewType) then - pure eNew -- approach 3 worked + pure eNew -- approach 2 worked else - throwTypeMismatchError errorMsgHeader? expectedType eType e f? - catch _ => - throwTypeMismatchError errorMsgHeader? expectedType eType e f? + let u ← getLevel α + let v ← getLevel β + let coeTInstType := Lean.mkForall `a BinderInfo.default α $ mkAppN (mkConst `CoeT [u, v]) #[α, mkBVar 0, β] + let coeTInstVal ← synthesizeInst coeTInstType + let eNew := mkAppN (Lean.mkConst `liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e] + let eNewType ← inferType eNew + if (← isDefEq expectedType eNewType) then + pure eNew -- approach 3 worked + else + throwTypeMismatchError errorMsgHeader? expectedType eType e f? + catch _ => + throwTypeMismatchError errorMsgHeader? expectedType eType e f? /-- If `expectedType?` is `some t`, then ensure `t` and `eType` are definitionally equal. @@ -785,188 +789,188 @@ match eNew? with Argument `f?` is used only for generating error messages. -/ def ensureHasTypeAux (expectedType? : Option Expr) (eType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do -match expectedType? with -| none => pure e -| some expectedType => - if (← isDefEq eType expectedType) then - pure e - else - tryLiftAndCoe errorMsgHeader? expectedType eType e f? + match expectedType? with + | none => pure e + | some expectedType => + if (← isDefEq eType expectedType) then + pure e + else + tryLiftAndCoe errorMsgHeader? expectedType eType e f? /-- If `expectedType?` is `some t`, then ensure `t` and type of `e` are definitionally equal. If they are not, then try coercions. -/ def ensureHasType (expectedType? : Option Expr) (e : Expr) (errorMsgHeader? : Option String := none) : TermElabM Expr := -match expectedType? with -| none => pure e -| _ => do - let eType ← inferType e - ensureHasTypeAux expectedType? eType e none errorMsgHeader? + match expectedType? with + | none => pure e + | _ => do + let eType ← inferType e + ensureHasTypeAux expectedType? eType e none errorMsgHeader? private def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do -let expectedType ← match expectedType? with - | none => mkFreshTypeMVar - | some expectedType => pure expectedType -let u ← getLevel expectedType --- TODO: should be `(sorryAx.{$u} $expectedType true) when we support antiquotations at that place -let syntheticSorry := mkApp2 (mkConst `sorryAx [u]) expectedType (mkConst `Bool.true); -unless ex.hasSyntheticSorry do - logException ex -pure syntheticSorry + let expectedType ← match expectedType? with + | none => mkFreshTypeMVar + | some expectedType => pure expectedType + let u ← getLevel expectedType + -- TODO: should be `(sorryAx.{$u} $expectedType true) when we support antiquotations at that place + let syntheticSorry := mkApp2 (mkConst `sorryAx [u]) expectedType (mkConst `Bool.true); + unless ex.hasSyntheticSorry do + logException ex + pure syntheticSorry /-- If `mayPostpone == true`, throw `Expection.postpone`. -/ def tryPostpone : TermElabM Unit := do -let ctx ← read -if ctx.mayPostpone then - throwPostpone + let ctx ← read + if ctx.mayPostpone then + throwPostpone /-- If `mayPostpone == true` and `e`'s head is a metavariable, throw `Exception.postpone`. -/ def tryPostponeIfMVar (e : Expr) : TermElabM Unit := do -if e.getAppFn.isMVar then - let e ← instantiateMVars e if e.getAppFn.isMVar then - tryPostpone + let e ← instantiateMVars e + if e.getAppFn.isMVar then + tryPostpone def tryPostponeIfNoneOrMVar (e? : Option Expr) : TermElabM Unit := -match e? with -| some e => tryPostponeIfMVar e -| none => tryPostpone + match e? with + | some e => tryPostponeIfMVar e + | none => tryPostpone private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do -trace[Elab.postpone]! "{stx} : {expectedType?}" -let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque -let ctx ← read -registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack ctx.declName?) -pure mvar + trace[Elab.postpone]! "{stx} : {expectedType?}" + let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque + let ctx ← read + registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed ctx.macroStack ctx.declName?) + pure mvar /- Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or an error is found. -/ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) : List TermElab → TermElabM Expr -| [] => do throwError! "unexpected syntax{MessageData.nestD (Format.line ++ stx)}" -| (elabFn::elabFns) => do - try - elabFn stx expectedType? - catch ex => match ex with - | Exception.error _ _ => - let ctx ← read - if ctx.errToSorry then - exceptionToSorry ex expectedType? - else - throw ex - | Exception.internal id => - if id == unsupportedSyntaxExceptionId then - s.restore - elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns - else if catchExPostpone && id == postponeExceptionId then - /- If `elab` threw `Exception.postpone`, we reset any state modifications. - For example, we want to make sure pending synthetic metavariables created by `elab` before - it threw `Exception.postpone` are discarded. - Note that we are also discarding the messages created by `elab`. - - For example, consider the expression. - `((f.x a1).x a2).x a3` - Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`. - Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone` - because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and - finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would - keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is - wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch - and new metavariables are created for the nested functions. -/ - s.restore - postponeElabTerm stx expectedType? + | [] => do throwError! "unexpected syntax{MessageData.nestD (Format.line ++ stx)}" + | (elabFn::elabFns) => do + try + elabFn stx expectedType? + catch ex => match ex with + | Exception.error _ _ => + let ctx ← read + if ctx.errToSorry then + exceptionToSorry ex expectedType? else throw ex + | Exception.internal id => + if id == unsupportedSyntaxExceptionId then + s.restore + elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns + else if catchExPostpone && id == postponeExceptionId then + /- If `elab` threw `Exception.postpone`, we reset any state modifications. + For example, we want to make sure pending synthetic metavariables created by `elab` before + it threw `Exception.postpone` are discarded. + Note that we are also discarding the messages created by `elab`. + + For example, consider the expression. + `((f.x a1).x a2).x a3` + Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`. + Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone` + because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and + finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would + keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is + wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch + and new metavariables are created for the nested functions. -/ + s.restore + postponeElabTerm stx expectedType? + else + throw ex private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) : TermElabM Expr := do -let s ← saveAllState -let env ← getEnv -let table := termElabAttribute.ext.getState env $.table -let k := stx.getKind -match table.find? k with -| some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns -| none => throwError! "elaboration function for '{k}' has not been implemented" + let s ← saveAllState + let env ← getEnv + let table := termElabAttribute.ext.getState env $.table + let k := stx.getKind + match table.find? k with + | some elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns + | none => throwError! "elaboration function for '{k}' has not been implemented" -instance : MonadMacroAdapter TermElabM := -{ getCurrMacroScope := getCurrMacroScope, +instance : MonadMacroAdapter TermElabM := { + getCurrMacroScope := getCurrMacroScope, getNextMacroScope := do pure (← getThe Core.State).nextMacroScope, - setNextMacroScope := fun next => modifyThe Core.State fun s => { s with nextMacroScope := next } } + setNextMacroScope := fun next => modifyThe Core.State fun s => { s with nextMacroScope := next } +} private def isExplicit (stx : Syntax) : Bool := -match_syntax stx with -| `(@$f) => true -| _ => false + match_syntax stx with + | `(@$f) => true + | _ => false private def isExplicitApp (stx : Syntax) : Bool := -stx.getKind == `Lean.Parser.Term.app && isExplicit (stx.getArg 0) + stx.getKind == `Lean.Parser.Term.app && isExplicit (stx.getArg 0) /-- Return true if `stx` if a lambda abstraction containing a `{}` or `[]` binder annotation. Example: `fun {α} (a : α) => a` -/ private def isLambdaWithImplicit (stx : Syntax) : Bool := -match_syntax stx with -| `(fun $binders* => $body) => binders.any fun b => b.isOfKind `Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder -| _ => false + match_syntax stx with + | `(fun $binders* => $body) => binders.any fun b => b.isOfKind `Lean.Parser.Term.implicitBinder || b.isOfKind `Lean.Parser.Term.instBinder + | _ => false private partial def dropTermParens : Syntax → Syntax | stx => -match_syntax stx with -| `(($stx)) => dropTermParens stx -| _ => stx + match_syntax stx with + | `(($stx)) => dropTermParens stx + | _ => stx /-- Block usage of implicit lambdas if `stx` is `@f` or `@f arg1 ...` or `fun` with an implicit binder annotation. -/ def blockImplicitLambda (stx : Syntax) : Bool := -let stx := dropTermParens stx -isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx + let stx := dropTermParens stx + isExplicit stx || isExplicitApp stx || isLambdaWithImplicit stx /-- Return normalized expected type if it is of the form `{a : α} → β` or `[a : α] → β` and `blockImplicitLambda stx` is not true, else return `none`. -/ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : TermElabM (Option Expr) := -if blockImplicitLambda stx then pure none -else match expectedType? with - | some expectedType => do - let expectedType ← whnfForall expectedType - match expectedType with - | Expr.forallE _ _ _ c => if c.binderInfo.isExplicit then pure none else pure $ some expectedType - | _ => pure none - | _ => pure none + if blockImplicitLambda stx then pure none + else match expectedType? with + | some expectedType => do + let expectedType ← whnfForall expectedType + match expectedType with + | Expr.forallE _ _ _ c => if c.binderInfo.isExplicit then pure none else pure $ some expectedType + | _ => pure none + | _ => pure none private def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (fvars : Array Expr) : TermElabM Expr := do -let body ← elabUsingElabFns stx expectedType catchExPostpone --- body ← ensureHasType stx expectedType body; -let r ← mkLambdaFVars fvars body -trace[Elab.implicitForall]! r -pure r + let body ← elabUsingElabFns stx expectedType catchExPostpone + let r ← mkLambdaFVars fvars body + trace[Elab.implicitForall]! r + pure r private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) : Expr → Array Expr → TermElabM Expr -| type@(Expr.forallE n d b c), fvars => - if c.binderInfo.isExplicit then + | type@(Expr.forallE n d b c), fvars => + if c.binderInfo.isExplicit then + elabImplicitLambdaAux stx catchExPostpone type fvars + else withFreshMacroScope do + let n ← MonadQuotation.addMacroScope n + withLocalDecl n c.binderInfo d fun fvar => do + let type ← whnfForall (b.instantiate1 fvar) + elabImplicitLambda stx catchExPostpone type (fvars.push fvar) + | type, fvars => elabImplicitLambdaAux stx catchExPostpone type fvars - else withFreshMacroScope do - let n ← MonadQuotation.addMacroScope n - withLocalDecl n c.binderInfo d fun fvar => do - let type ← whnfForall (b.instantiate1 fvar) - elabImplicitLambda stx catchExPostpone type (fvars.push fvar) -| type, fvars => - elabImplicitLambdaAux stx catchExPostpone type fvars /- Main loop for `elabTerm` -/ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : Bool) (implicitLambda : Bool) : Syntax → TermElabM Expr -| stx => withFreshMacroScope $ withIncRecDepth do - trace[Elab.step]! "expected type: {expectedType?}, term\n{stx}" - withNestedTraces do - let env ← getEnv - let stxNew? ← catchInternalId unsupportedSyntaxExceptionId - (do let newStx ← adaptMacro (getMacros env) stx; pure (some newStx)) - (fun _ => pure none) - match stxNew? with - | some stxNew => withMacroExpansion stx stxNew $ elabTermAux expectedType? catchExPostpone implicitLambda stxNew - | _ => - let implicit? ← if implicitLambda then useImplicitLambda? stx expectedType? else pure none - match implicit? with - | some expectedType => elabImplicitLambda stx catchExPostpone expectedType #[] - | none => elabUsingElabFns stx expectedType? catchExPostpone + | stx => withFreshMacroScope $ withIncRecDepth do + trace[Elab.step]! "expected type: {expectedType?}, term\n{stx}" + withNestedTraces do + let env ← getEnv + let stxNew? ← catchInternalId unsupportedSyntaxExceptionId + (do let newStx ← adaptMacro (getMacros env) stx; pure (some newStx)) + (fun _ => pure none) + match stxNew? with + | some stxNew => withMacroExpansion stx stxNew $ elabTermAux expectedType? catchExPostpone implicitLambda stxNew + | _ => + let implicit? ← if implicitLambda then useImplicitLambda? stx expectedType? else pure none + match implicit? with + | some expectedType => elabImplicitLambda stx catchExPostpone expectedType #[] + | none => elabUsingElabFns stx expectedType? catchExPostpone /-- Main function for elaborating terms. @@ -982,27 +986,26 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : The option `catchExPostpone == false` is used to implement `resumeElabTerm` to prevent the creation of another synthetic metavariable when resuming the elaboration. -/ def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr := -withRef stx $ elabTermAux expectedType? catchExPostpone true stx + withRef stx $ elabTermAux expectedType? catchExPostpone true stx def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do -let e ← elabTerm stx expectedType? catchExPostpone -withRef stx $ ensureHasType expectedType? e errorMsgHeader? + let e ← elabTerm stx expectedType? catchExPostpone + withRef stx $ ensureHasType expectedType? e errorMsgHeader? def elabTermWithoutImplicitLambdas (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) : TermElabM Expr := do -elabTermAux expectedType? catchExPostpone false stx + elabTermAux expectedType? catchExPostpone false stx /-- Adapt a syntax transformation to a regular, term-producing elaborator. -/ -def adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab := -fun stx expectedType? => do +def adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab := fun stx expectedType? => do let stx' ← exp stx withMacroExpansion stx stx' $ elabTerm stx' expectedType? def mkInstMVar (type : Expr) : TermElabM Expr := do -let mvar ← mkFreshExprMVar type MetavarKind.synthetic -let mvarId := mvar.mvarId! -unless (← synthesizeInstMVarCore mvarId) do - registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass -pure mvar + let mvar ← mkFreshExprMVar type MetavarKind.synthetic + let mvarId := mvar.mvarId! + unless (← synthesizeInstMVarCore mvarId) do + registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass + pure mvar /- Relevant definitions: @@ -1011,79 +1014,75 @@ pure mvar abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β ``` -/ private def tryCoeSort (α : Expr) (a : Expr) : TermElabM Expr := do -let β ← mkFreshTypeMVar -let u ← getLevel α -let v ← getLevel β -let coeSortInstType := mkAppN (Lean.mkConst `CoeSort [u, v]) #[α, β] -let mvar ← mkFreshExprMVar coeSortInstType MetavarKind.synthetic -let mvarId := mvar.mvarId! -try - withoutMacroStackAtErr do - if (← synthesizeInstMVarCore mvarId) then - pure $ mkAppN (Lean.mkConst `coeSort [u, v]) #[α, β, a, mvar] - else - throwError "type expected" -catch - | Exception.error _ msg => throwError! "type expected\n{msg}" - | _ => throwError! "type expected" + let β ← mkFreshTypeMVar + let u ← getLevel α + let v ← getLevel β + let coeSortInstType := mkAppN (Lean.mkConst `CoeSort [u, v]) #[α, β] + let mvar ← mkFreshExprMVar coeSortInstType MetavarKind.synthetic + let mvarId := mvar.mvarId! + try + withoutMacroStackAtErr do + if (← synthesizeInstMVarCore mvarId) then + pure $ mkAppN (Lean.mkConst `coeSort [u, v]) #[α, β, a, mvar] + else + throwError "type expected" + catch + | Exception.error _ msg => throwError! "type expected\n{msg}" + | _ => throwError! "type expected" /-- Make sure `e` is a type by inferring its type and making sure it is a `Expr.sort` or is unifiable with `Expr.sort`, or can be coerced into one. -/ def ensureType (e : Expr) : TermElabM Expr := do -if (← isType e) then - pure e -else - let eType ← inferType e - let u ← mkFreshLevelMVar - if (← isDefEq eType (mkSort u)) then + if (← isType e) then pure e else - tryCoeSort eType e + let eType ← inferType e + let u ← mkFreshLevelMVar + if (← isDefEq eType (mkSort u)) then + pure e + else + tryCoeSort eType e /-- Elaborate `stx` and ensure result is a type. -/ def elabType (stx : Syntax) : TermElabM Expr := do -let u ← mkFreshLevelMVar -let type ← elabTerm stx (mkSort u) -withRef stx $ ensureType type + let u ← mkFreshLevelMVar + let type ← elabTerm stx (mkSort u) + withRef stx $ ensureType type def mkAuxName (suffix : Name) : TermElabM Name := do -let ctx ← read -match ctx.declName? with -| none => throwError "auxiliary declaration cannot be created when declaration name is not available" -| some declName => Lean.mkAuxName (declName ++ suffix) 1 + let ctx ← read + match ctx.declName? with + | none => throwError "auxiliary declaration cannot be created when declaration name is not available" + | some declName => Lean.mkAuxName (declName ++ suffix) 1 /- ======================================= Builtin elaboration functions ======================================= -/ -@[builtinTermElab «prop»] def elabProp : TermElab := -fun _ _ => pure $ mkSort levelZero +@[builtinTermElab «prop»] def elabProp : TermElab := fun _ _ => + pure $ mkSort levelZero private def elabOptLevel (stx : Syntax) : TermElabM Level := -if stx.isNone then - pure levelZero -else - elabLevel $ stx.getArg 0 + if stx.isNone then + pure levelZero + else + elabLevel $ stx.getArg 0 -@[builtinTermElab «sort»] def elabSort : TermElab := -fun stx _ => do +@[builtinTermElab «sort»] def elabSort : TermElab := fun stx _ => do let u ← elabOptLevel stx[1] pure $ mkSort u -@[builtinTermElab «type»] def elabTypeStx : TermElab := -fun stx _ => do +@[builtinTermElab «type»] def elabTypeStx : TermElab := fun stx _ => do let u ← elabOptLevel stx[1] pure $ mkSort (mkLevelSucc u) -@[builtinTermElab «hole»] def elabHole : TermElab := -fun stx expectedType? => do +@[builtinTermElab «hole»] def elabHole : TermElab := fun stx expectedType? => do let mvar ← mkFreshExprMVar expectedType? registerMVarErrorHoleInfo mvar.mvarId! stx pure mvar -@[builtinTermElab «syntheticHole»] def elabSyntheticHole : TermElab := -fun stx expectedType? => do +@[builtinTermElab «syntheticHole»] def elabSyntheticHole : TermElab := fun stx expectedType? => do let arg := stx[1] let userName := if arg.isIdent then arg.getId else Name.anonymous let mkNewHole : Unit → TermElabM Expr := fun _ => do @@ -1122,21 +1121,19 @@ fun stx expectedType? => do throwError "synthetic hole has already been defined with an incompatible local context" private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do -let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque -let mvarId := mvar.mvarId! -let ref ← getRef -let declName? ← getDeclName? -registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic declName? tacticCode -pure mvar + let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque + let mvarId := mvar.mvarId! + let ref ← getRef + let declName? ← getDeclName? + registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic declName? tacticCode + pure mvar -@[builtinTermElab byTactic] def elabByTactic : TermElab := -fun stx expectedType? => +@[builtinTermElab byTactic] def elabByTactic : TermElab := fun stx expectedType? => match expectedType? with | some expectedType => mkTacticMVar expectedType stx | none => throwError ("invalid 'by' tactic, expected type has not been provided") -@[builtinMacro Lean.Parser.Term.listLit] def expandListLit : Macro := -fun stx => +@[builtinMacro Lean.Parser.Term.listLit] def expandListLit : Macro := fun stx => let openBkt := stx[0] let args := stx[1] let closeBkt := stx[2] @@ -1144,89 +1141,86 @@ fun stx => let nilId := mkIdentFrom closeBkt `List.nil pure $ args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId -@[builtinMacro Lean.Parser.Term.arrayLit] def expandArrayLit : Macro := -fun stx => +@[builtinMacro Lean.Parser.Term.arrayLit] def expandArrayLit : Macro := fun stx => match_syntax stx with | `(#[$args*]) => `(List.toArray [$args*]) | _ => throw $ Macro.Exception.error stx "unexpected array literal syntax" def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do -let lctx ← getLCtx -let view := extractMacroScopes n -let rec loop (n : Name) (projs : List String) := - match lctx.findFromUserName? { view with name := n }.review with - | some decl => some (decl.toExpr, projs) - | none => match n with - | Name.str pre s _ => loop pre (s::projs) - | _ => none -pure $ loop view.name [] + let lctx ← getLCtx + let view := extractMacroScopes n + let rec loop (n : Name) (projs : List String) := + match lctx.findFromUserName? { view with name := n }.review with + | some decl => some (decl.toExpr, projs) + | none => match n with + | Name.str pre s _ => loop pre (s::projs) + | _ => none + pure $ loop view.name [] /- Return true iff `stx` is a `Syntax.ident`, and it is a local variable. -/ def isLocalIdent? (stx : Syntax) : TermElabM (Option Expr) := -match stx with -| Syntax.ident _ _ val _ => do - let r? ← resolveLocalName val - match r? with - | some (fvar, []) => pure (some fvar) - | _ => pure none -| _ => pure none + match stx with + | Syntax.ident _ _ val _ => do + let r? ← resolveLocalName val + match r? with + | some (fvar, []) => pure (some fvar) + | _ => pure none + | _ => pure none private def mkFreshLevelMVars (num : Nat) : TermElabM (List Level) := -num.foldM (init := []) fun _ us => do - let u ← mkFreshLevelMVar - pure $ u::us + num.foldM (init := []) fun _ us => do + let u ← mkFreshLevelMVar + pure $ u::us /-- Create an `Expr.const` using the given name and explicit levels. Remark: fresh universe metavariables are created if the constant has more universe parameters than `explicitLevels`. -/ def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do -let cinfo ← getConstInfo constName -if explicitLevels.length > cinfo.lparams.length then - throwError "too many explicit universe levels" -else - let numMissingLevels := cinfo.lparams.length - explicitLevels.length - let us ← mkFreshLevelMVars numMissingLevels - pure $ Lean.mkConst constName (explicitLevels ++ us) + let cinfo ← getConstInfo constName + if explicitLevels.length > cinfo.lparams.length then + throwError "too many explicit universe levels" + else + let numMissingLevels := cinfo.lparams.length - explicitLevels.length + let us ← mkFreshLevelMVars numMissingLevels + pure $ Lean.mkConst constName (explicitLevels ++ us) private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do -let env ← getEnv -candidates.foldlM (init := []) fun result (constName, projs) => do - -- TODO: better suppor for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail. - let const ← mkConst constName explicitLevels - pure $ (const, projs) :: result + let env ← getEnv + candidates.foldlM (init := []) fun result (constName, projs) => do + -- TODO: better suppor for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail. + let const ← mkConst constName explicitLevels + pure $ (const, projs) :: result def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do -let result? ← resolveLocalName n -match result? with -| some (e, projs) => - unless explicitLevels.isEmpty do - throwError! "invalid use of explicit universe parameters, '{e}' is a local" - pure [(e, projs)] -| none => - let process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do - if candidates.isEmpty then - let mainModule ← getMainModule - let view := extractMacroScopes n - throwError! "unknown identifier '{view.format mainModule}'" - mkConsts candidates explicitLevels - if preresolved.isEmpty then - let r ← resolveGlobalName n - process r - else - process preresolved + let result? ← resolveLocalName n + match result? with + | some (e, projs) => + unless explicitLevels.isEmpty do + throwError! "invalid use of explicit universe parameters, '{e}' is a local" + pure [(e, projs)] + | none => + let process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do + if candidates.isEmpty then + let mainModule ← getMainModule + let view := extractMacroScopes n + throwError! "unknown identifier '{view.format mainModule}'" + mkConsts candidates explicitLevels + if preresolved.isEmpty then + let r ← resolveGlobalName n + process r + else + process preresolved -@[builtinTermElab cdot] def elabBadCDot : TermElab := -fun stx _ => throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)" +@[builtinTermElab cdot] def elabBadCDot : TermElab := fun stx _ => + throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)" -@[builtinTermElab strLit] def elabStrLit : TermElab := -fun stx _ => do +@[builtinTermElab strLit] def elabStrLit : TermElab := fun stx _ => do match stx.isStrLit? with | some val => pure $ mkStrLit val | none => throwIllFormedSyntax -@[builtinTermElab numLit] def elabNumLit : TermElab := -fun stx expectedType? => do +@[builtinTermElab numLit] def elabNumLit : TermElab := fun stx expectedType? => do let val ← match stx.isNatLit? with | some val => pure (mkNatLit val) | none => throwIllFormedSyntax @@ -1240,8 +1234,7 @@ fun stx expectedType? => do let mvar ← mkInstMVar (mkApp (Lean.mkConst `HasOfNat [u]) typeMVar) pure $ mkApp3 (Lean.mkConst `HasOfNat.ofNat [u]) typeMVar mvar val -@[builtinTermElab charLit] def elabCharLit : TermElab := -fun stx _ => do +@[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do match stx.isCharLit? with | some val => pure $ mkApp (Lean.mkConst `Char.ofNat) (mkNatLit val.toNat) | none => throwIllFormedSyntax @@ -1252,13 +1245,11 @@ fun stx _ => | some val => pure $ toExpr val | none => throwIllFormedSyntax -@[builtinTermElab typeOf] def elabTypeOf : TermElab := -fun stx _ => do +@[builtinTermElab typeOf] def elabTypeOf : TermElab := fun stx _ => do let e ← elabTerm stx[1] none; inferType e -@[builtinTermElab ensureTypeOf] def elabEnsureTypeOf : TermElab := -fun stx expectedType? => +@[builtinTermElab ensureTypeOf] def elabEnsureTypeOf : TermElab := fun stx expectedType? => match stx[2].isStrLit? with | none => throwIllFormedSyntax | some msg => do @@ -1266,37 +1257,37 @@ fun stx expectedType? => let refTermType ← inferType refTerm elabTermEnsuringType stx[3] refTermType true msg -@[builtinTermElab ensureExpectedType] def elabEnsureExpectedType : TermElab := -fun stx expectedType? => +@[builtinTermElab ensureExpectedType] def elabEnsureExpectedType : TermElab := fun stx expectedType? => match stx[1].isStrLit? with | none => throwIllFormedSyntax | some msg => elabTermEnsuringType stx[2] expectedType? true msg -private def mkSomeContext : Context := -{ fileName := "", +private def mkSomeContext : Context := { + fileName := "", fileMap := arbitrary _, - currNamespace := Name.anonymous } + currNamespace := Name.anonymous +} @[inline] def TermElabM.run {α} (x : TermElabM α) (ctx : Context := mkSomeContext) (s : State := {}) : MetaM (α × State) := -withConfig setElabConfig (x ctx $.run s) + withConfig setElabConfig (x ctx $.run s) @[inline] def TermElabM.run' {α} (x : TermElabM α) (ctx : Context := mkSomeContext) (s : State := {}) : MetaM α := -(·.1) <$> x.run ctx s + (·.1) <$> x.run ctx s @[inline] def TermElabM.toIO {α} (x : TermElabM α) (ctxCore : Core.Context) (sCore : Core.State) (ctxMeta : Meta.Context) (sMeta : Meta.State) (ctx : Context) (s : State) : IO (α × Core.State × Meta.State × State) := do -let ((a, s), sCore, sMeta) ← (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta -pure (a, sCore, sMeta, s) + let ((a, s), sCore, sMeta) ← (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta + pure (a, sCore, sMeta, s) instance {α} [MetaHasEval α] : MetaHasEval (TermElabM α) := -⟨fun env opts x _ => - let x : TermElabM α := do - try x finally - let s ← get - liftIO $ s.messages.forM fun msg => msg.toString >>= IO.println - MetaHasEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩ + ⟨fun env opts x _ => + let x : TermElabM α := do + try x finally + let s ← get + liftIO $ s.messages.forM fun msg => msg.toString >>= IO.println + MetaHasEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩ end Term