diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index bb0245b94e..76222a0e00 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -53,10 +53,10 @@ inductive SyntheticMVarKind where instance : ToString SyntheticMVarKind where toString - | SyntheticMVarKind.typeClass => "typeclass" - | SyntheticMVarKind.coe .. => "coe" - | SyntheticMVarKind.tactic .. => "tactic" - | SyntheticMVarKind.postponed .. => "postponed" + | .typeClass => "typeclass" + | .coe .. => "coe" + | .tactic .. => "tactic" + | .postponed .. => "postponed" structure SyntheticMVarDecl where mvarId : MVarId @@ -78,9 +78,9 @@ inductive MVarErrorKind where instance : ToString MVarErrorKind where toString - | MVarErrorKind.implicitArg _ => "implicitArg" - | MVarErrorKind.hole => "hole" - | MVarErrorKind.custom _ => "custom" + | .implicitArg _ => "implicitArg" + | .hole => "hole" + | .custom _ => "custom" /-- We can optionally associate an error context with metavariables. @@ -252,7 +252,7 @@ def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElab set s.elab setTraceState traceState unless restoreInfo do - modify fun s => { s with infoState := infoState } + modify fun s => { s with infoState } instance : MonadBacktrack SavedState TermElabM where saveState := Term.saveState @@ -278,11 +278,11 @@ def observing (x : TermElabM α) : TermElabM (TermElabResult α) := do s.restore (restoreInfo := true) return EStateM.Result.ok e sNew catch - | ex@(Exception.error _ _) => + | ex@(.error ..) => let sNew ← saveState s.restore (restoreInfo := true) return EStateM.Result.error ex sNew - | ex@(Exception.internal id _) => + | ex@(.internal id _) => if id == postponeExceptionId then s.restore (restoreInfo := true) throw ex @@ -292,8 +292,8 @@ def observing (x : TermElabM α) : TermElabM (TermElabResult α) := do We use this method to implement overloaded notation and symbols. -/ def applyResult (result : TermElabResult α) : TermElabM α := do match result with - | EStateM.Result.ok a r => r.restore (restoreInfo := true); return a - | EStateM.Result.error ex r => r.restore (restoreInfo := true); throw ex + | .ok a r => r.restore (restoreInfo := true); return a + | .error ex r => r.restore (restoreInfo := true); throw ex /-- Execute `x`, but keep state modifications only if `x` did not postpone. @@ -385,17 +385,17 @@ inductive LVal where | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax) def LVal.getRef : LVal → Syntax - | LVal.fieldIdx ref _ => ref - | LVal.fieldName ref .. => ref + | .fieldIdx ref _ => ref + | .fieldName ref .. => ref def LVal.isFieldName : LVal → Bool - | LVal.fieldName .. => true + | .fieldName .. => true | _ => false instance : ToString LVal where toString - | LVal.fieldIdx _ i => toString i - | LVal.fieldName _ n .. => n + | .fieldIdx _ i => toString i + | .fieldName _ n .. => n /-- Return the name of the declaration being elaborated if available. -/ def getDeclName? : TermElabM (Option Name) := return (← read).declName? @@ -453,8 +453,8 @@ def liftLevelM (x : LevelElabM α) : TermElabM α := do let ngen ← getNGen let lvlCtx : Level.Context := { options := (← getOptions), ref := (← getRef), autoBoundImplicit := ctx.autoBoundImplicit } match (x lvlCtx).run { ngen := ngen, mctx := mctx, levelNames := (← getLevelNames) } with - | EStateM.Result.ok a newS => setMCtx newS.mctx; setNGen newS.ngen; setLevelNames newS.levelNames; pure a - | EStateM.Result.error ex _ => throw ex + | .ok a newS => setMCtx newS.mctx; setNGen newS.ngen; setLevelNames newS.levelNames; pure a + | .error ex _ => throw ex def elabLevel (stx : Syntax) : TermElabM Level := liftLevelM <| Level.elabLevel stx @@ -468,7 +468,7 @@ def withMacroExpansion (beforeStx afterStx : Syntax) (x : TermElabM α) : TermEl 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, stx, kind } :: s.syntheticMVars } def registerSyntheticMVarWithCurrRef (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do registerSyntheticMVar (← getRef) mvarId kind @@ -477,13 +477,13 @@ def registerMVarErrorInfo (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit := modify fun s => { s with mvarErrorInfos := s.mvarErrorInfos.insert mvarErrorInfo.mvarId mvarErrorInfo } def registerMVarErrorHoleInfo (mvarId : MVarId) (ref : Syntax) : TermElabM Unit := - registerMVarErrorInfo { mvarId := mvarId, ref := ref, kind := MVarErrorKind.hole } + registerMVarErrorInfo { mvarId, ref, kind := .hole } def registerMVarErrorImplicitArgInfo (mvarId : MVarId) (ref : Syntax) (app : Expr) : TermElabM Unit := do - registerMVarErrorInfo { mvarId := mvarId, ref := ref, kind := MVarErrorKind.implicitArg app } + registerMVarErrorInfo { mvarId, ref, kind := .implicitArg app } def registerMVarErrorCustomInfo (mvarId : MVarId) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := do - registerMVarErrorInfo { mvarId := mvarId, ref := ref, kind := MVarErrorKind.custom msgData } + registerMVarErrorInfo { mvarId, ref, kind := .custom msgData } def getMVarErrorInfo? (mvarId : MVarId) : TermElabM (Option MVarErrorInfo) := do return (← get).mvarErrorInfos.find? mvarId @@ -670,17 +670,17 @@ abbrev M := MonadCacheT Expr Unit (OptionT TermElabM) partial def visit (e : Expr) : M Unit := do checkCache e fun _ => do match e with - | Expr.forallE _ d b _ => visit d; visit b - | Expr.lam _ d b _ => visit d; visit b - | Expr.letE _ t v b _ => visit t; visit v; visit b - | Expr.app f a => visit f; visit a - | Expr.mdata _ b => visit b - | Expr.proj _ _ b => visit b - | Expr.fvar fvarId .. => + | .forallE _ d b _ => visit d; visit b + | .lam _ d b _ => visit d; visit b + | .letE _ t v b _ => visit t; visit v; visit b + | .app f a => visit f; visit a + | .mdata _ b => visit b + | .proj _ _ b => visit b + | .fvar fvarId .. => match (← getLocalDecl fvarId) with - | LocalDecl.cdecl .. => return () + | .cdecl .. => return () | LocalDecl.ldecl (value := v) .. => visit v - | Expr.mvar mvarId .. => + | .mvar mvarId .. => let e' ← instantiateMVars e if e' != e then visit e' @@ -745,8 +745,8 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n unless (← isDefEq (mkMVar instMVar) val) do throwError "failed to assign synthesized type class instance{indentExpr val}" return true - | LOption.undef => return false -- we will try later - | LOption.none => + | .undef => return false -- we will try later + | .none => if (← read).ignoreTCFailures then return false else @@ -771,7 +771,7 @@ def synthesizeCoeInstMVarCore (instMVar : MVarId) : TermElabM Bool := do -/ def tryCoeThunk? (expectedType : Expr) (eType : Expr) (e : Expr) : TermElabM (Option Expr) := do match expectedType with - | Expr.app (Expr.const ``Thunk u) arg => + | .app (.const ``Thunk u) arg => if (← isDefEq eType arg) then return some (mkApp2 (mkConst ``Thunk.mk u) arg (mkSimpleThunk e)) else @@ -797,8 +797,8 @@ def mkCoe (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr := n registerSyntheticMVarWithCurrRef mvarAux.mvarId! (SyntheticMVarKind.coe errorMsgHeader? eNew expectedType eType e f?) return mvarAux catch - | Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg - | _ => throwTypeMismatchError errorMsgHeader? expectedType eType e f? + | .error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg + | _ => throwTypeMismatchError errorMsgHeader? expectedType eType e f? /-- Try to apply coercion to make sure `e` has type `expectedType`. @@ -819,17 +819,17 @@ private def tryCoe (errorMsgHeader? : Option String) (expectedType : Expr) (eTyp def isTypeApp? (type : Expr) : TermElabM (Option (Expr × Expr)) := do let type ← withReducible <| whnf type match type with - | Expr.app m α => return some ((← instantiateMVars m), (← instantiateMVars α)) - | _ => return none + | .app m α => return some ((← instantiateMVars m), (← instantiateMVars α)) + | _ => return none /-- Helper method used to implement auto-lift and coercions -/ private def synthesizeInst (type : Expr) : TermElabM Expr := do let type ← instantiateMVars type match (← trySynthInstance type) with - | LOption.some val => return val + | .some val => return val -- Note that `ignoreTCFailures` is not checked here since it must return a result. - | LOption.undef => throwError "failed to synthesize instance{indentExpr type}" - | LOption.none => throwError "failed to synthesize instance{indentExpr type}" + | .undef => throwError "failed to synthesize instance{indentExpr type}" + | .none => throwError "failed to synthesize instance{indentExpr type}" /-- Return `true` if `type` is of the form `m α` where `m` is a `Monad`. @@ -1094,9 +1094,9 @@ def isTacticOrPostponedHole? (e : Expr) : TermElabM (Option MVarId) := do match e with | Expr.mvar mvarId => match (← getSyntheticMVarDecl? mvarId) with - | some { kind := SyntheticMVarKind.tactic .., .. } => return mvarId - | some { kind := SyntheticMVarKind.postponed .., .. } => return mvarId - | _ => return none + | some { kind := .tactic .., .. } => return mvarId + | some { kind := .postponed .., .. } => return mvarId + | _ => return none | _ => pure none def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (isBinder := false) : TermElabM (Sum Info MVarId) := do @@ -1136,12 +1136,12 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : (try elabFn.value stx expectedType? catch ex => match ex with - | Exception.error _ _ => + | .error .. => if (← read).errToSorry then exceptionToSorry ex expectedType? else throw ex - | Exception.internal id _ => + | .internal id _ => if (← read).errToSorry && id == abortTermExceptionId then exceptionToSorry ex expectedType? else if id == unsupportedSyntaxExceptionId then @@ -1166,7 +1166,7 @@ private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : else throw ex) catch ex => match ex with - | Exception.internal id _ => + | .internal id _ => if id == unsupportedSyntaxExceptionId then s.restore -- also removes the info tree created above elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns @@ -1261,7 +1261,7 @@ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : Te else let expectedType ← whnfForall expectedType match expectedType with - | Expr.forallE _ _ _ c => + | .forallE _ _ _ c => if c.isImplicit || c.isInstImplicit then return some expectedType else @@ -1271,7 +1271,7 @@ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : Te private def decorateErrorMessageWithLambdaImplicitVars (ex : Exception) (impFVars : Array Expr) : TermElabM Exception := do match ex with - | Exception.error ref msg => + | .error ref msg => if impFVars.isEmpty then return Exception.error ref msg else @@ -1298,7 +1298,7 @@ private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) ( loop type #[] where loop - | type@(Expr.forallE n d b c), fvars => + | type@(.forallE n d b c), fvars => if c.isExplicit then elabImplicitLambdaAux stx catchExPostpone type fvars else withFreshMacroScope do @@ -1311,7 +1311,7 @@ where /- Main loop for `elabTerm` -/ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : Bool) (implicitLambda : Bool) : Syntax → TermElabM Expr - | Syntax.missing => mkSyntheticSorryFor expectedType? + | .missing => mkSyntheticSorryFor expectedType? | stx => withFreshMacroScope <| withIncRecDepth do trace[Elab.step] "expected type: {expectedType?}, term\n{stx}" checkMaxHeartbeats "elaborator" @@ -1332,7 +1332,7 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone : /-- Store in the `InfoTree` that `e` is a "dot"-completion target. -/ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) (field? : Option Syntax := none) : TermElabM Unit := do - addCompletionInfo <| CompletionInfo.dot { expr := e, stx, lctx := (← getLCtx), elaborator := Name.anonymous, expectedType? } (field? := field?) (expectedType? := expectedType?) + addCompletionInfo <| CompletionInfo.dot { expr := e, stx, lctx := (← getLCtx), elaborator := .anonymous, expectedType? } (field? := field?) (expectedType? := expectedType?) /-- Main function for elaborating terms. @@ -1413,7 +1413,7 @@ private def tryCoeSort (α : Expr) (a : Expr) : TermElabM Expr := do let u ← getLevel α let v ← getLevel β let coeSortInstType := mkAppN (Lean.mkConst ``CoeSort [u, v]) #[α, β] - let mvar ← mkFreshExprMVar coeSortInstType MetavarKind.synthetic + let mvar ← mkFreshExprMVar coeSortInstType .synthetic let mvarId := mvar.mvarId! try withoutMacroStackAtErr do @@ -1425,8 +1425,8 @@ private def tryCoeSort (α : Expr) (a : Expr) : TermElabM Expr := do else throwError "type expected" catch - | Exception.error _ msg => throwError "type expected\n{msg}" - | _ => throwError "type expected" + | .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` @@ -1463,7 +1463,7 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do | some n => -- Restore state, declare `n`, and try again s.restore - withLocalDecl n BinderInfo.implicit (← mkFreshTypeMVar) fun x => + withLocalDecl n .implicit (← mkFreshTypeMVar) fun x => withReader (fun ctx => { ctx with autoBoundImplicits := ctx.autoBoundImplicits.push x } ) do loop (← saveState) | none => throw ex