From a8cab84735bc4e7808db190ad4e89a5386e3560b Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 7 Jul 2022 20:36:21 +0200 Subject: [PATCH] refactor: use computed fields for Expr --- src/Lean/Attributes.lean | 2 +- src/Lean/Class.lean | 2 +- src/Lean/Compiler/ConstFolding.lean | 20 +- src/Lean/Compiler/InitAttr.lean | 8 +- src/Lean/Compiler/Util.lean | 8 +- src/Lean/Elab/App.lean | 22 +- src/Lean/Elab/DeclUtil.lean | 4 +- src/Lean/Elab/Deriving/Inhabited.lean | 2 +- src/Lean/Elab/Do.lean | 2 +- src/Lean/Elab/Extra.lean | 2 +- src/Lean/Elab/Inductive.lean | 12 +- src/Lean/Elab/Match.lean | 30 +- src/Lean/Elab/MutualDef.lean | 16 +- src/Lean/Elab/PatternVar.lean | 4 +- src/Lean/Elab/PreDefinition/Basic.lean | 4 +- src/Lean/Elab/PreDefinition/Eqns.lean | 10 +- src/Lean/Elab/PreDefinition/Main.lean | 2 +- .../Elab/PreDefinition/Structural/BRecOn.lean | 16 +- .../PreDefinition/Structural/IndPred.lean | 10 +- .../Structural/SmartUnfolding.lean | 4 +- src/Lean/Elab/PreDefinition/WF/Fix.lean | 8 +- .../Elab/PreDefinition/WF/PackDomain.lean | 6 +- src/Lean/Elab/RecAppSyntax.lean | 2 +- src/Lean/Elab/StructInst.lean | 18 +- src/Lean/Elab/Structure.lean | 12 +- src/Lean/Elab/Syntax.lean | 10 +- src/Lean/Elab/Tactic/ElabTerm.lean | 6 +- src/Lean/Elab/Tactic/Induction.lean | 2 +- src/Lean/Elab/Term.lean | 22 +- src/Lean/Environment.lean | 4 +- src/Lean/Expr.lean | 337 +++++++++--------- src/Lean/HeadIndex.lean | 40 +-- src/Lean/KeyedDeclsAttribute.lean | 2 +- src/Lean/Linter/Basic.lean | 4 +- src/Lean/Meta/AbstractMVars.lean | 18 +- src/Lean/Meta/AbstractNestedProofs.lean | 6 +- src/Lean/Meta/AppBuilder.lean | 14 +- src/Lean/Meta/Basic.lean | 36 +- src/Lean/Meta/CasesOn.lean | 2 +- src/Lean/Meta/Check.lean | 10 +- src/Lean/Meta/Closure.lean | 14 +- src/Lean/Meta/DiscrTree.lean | 18 +- src/Lean/Meta/ExprDefEq.lean | 64 ++-- src/Lean/Meta/ExprLens.lean | 32 +- src/Lean/Meta/ExprTraverse.lean | 8 +- src/Lean/Meta/ForEachExpr.lean | 12 +- src/Lean/Meta/FunInfo.lean | 6 +- src/Lean/Meta/GeneralizeTelescope.lean | 2 +- src/Lean/Meta/InferType.lean | 94 ++--- src/Lean/Meta/Instances.lean | 2 +- src/Lean/Meta/KAbstract.lean | 6 +- src/Lean/Meta/Match/Basic.lean | 8 +- src/Lean/Meta/Match/CaseValues.lean | 4 +- src/Lean/Meta/Match/MVarRenaming.lean | 2 +- src/Lean/Meta/Match/Match.lean | 34 +- src/Lean/Meta/Match/MatchEqs.lean | 2 +- src/Lean/Meta/Match/MatcherInfo.lean | 2 +- src/Lean/Meta/Offset.lean | 14 +- src/Lean/Meta/PPGoal.lean | 8 +- src/Lean/Meta/RecursorInfo.lean | 8 +- src/Lean/Meta/ReduceEval.lean | 4 +- src/Lean/Meta/SynthInstance.lean | 22 +- src/Lean/Meta/Tactic/AC/Main.lean | 4 +- src/Lean/Meta/Tactic/Cases.lean | 2 +- src/Lean/Meta/Tactic/ElimInfo.lean | 4 +- src/Lean/Meta/Tactic/FVarSubst.lean | 2 +- src/Lean/Meta/Tactic/Induction.lean | 6 +- src/Lean/Meta/Tactic/Intro.lean | 6 +- .../Meta/Tactic/LinearArith/Nat/Basic.lean | 12 +- src/Lean/Meta/Tactic/Replace.lean | 2 +- src/Lean/Meta/Tactic/Simp/Main.lean | 4 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 8 +- src/Lean/Meta/Tactic/Split.lean | 2 +- src/Lean/Meta/Tactic/Subst.lean | 2 +- src/Lean/Meta/Tactic/UnifyEq.lean | 2 +- src/Lean/Meta/Tactic/Util.lean | 2 +- src/Lean/Meta/Transform.lean | 14 +- src/Lean/Meta/WHNF.lean | 62 ++-- src/Lean/MetavarContext.lean | 82 ++--- src/Lean/MonadEnv.lean | 2 +- src/Lean/Parser/Extension.lean | 12 +- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 22 +- .../PrettyPrinter/Delaborator/Builtins.lean | 38 +- .../PrettyPrinter/Delaborator/SubExpr.lean | 4 +- src/Lean/Server/Completion.lean | 6 +- .../Server/FileWorker/WidgetRequests.lean | 2 +- src/Lean/SubExpr.lean | 2 +- src/Lean/Util/CollectFVars.lean | 8 +- src/Lean/Util/CollectLevelParams.lean | 10 +- src/Lean/Util/CollectMVars.lean | 8 +- src/Lean/Util/FindExpr.lean | 16 +- src/Lean/Util/FindLevelMVar.lean | 10 +- src/Lean/Util/FindMVar.lean | 8 +- src/Lean/Util/FoldConsts.lean | 8 +- src/Lean/Util/ForEachExpr.lean | 6 +- src/Lean/Util/HasConstCache.lean | 6 +- src/Lean/Util/OccursCheck.lean | 8 +- src/Lean/Util/Recognizers.lean | 10 +- src/Lean/Util/ReplaceExpr.lean | 12 +- src/Lean/Util/ReplaceLevel.lean | 20 +- src/Lean/Util/Sorry.lean | 4 +- tests/lean/run/KyleAlg.lean | 6 +- .../run/addDecorationsWithoutPartial.lean | 12 +- tests/lean/run/depElim1.lean | 6 +- tests/lean/run/elabCmd.lean | 2 +- tests/lean/run/monadCache.lean | 20 +- tests/lean/run/replace.lean | 4 +- tests/lean/updateExprIssue.lean | 2 +- tests/lean/updateExprIssue.lean.expected.out | 24 +- 109 files changed, 811 insertions(+), 808 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 4961781234..946f0e53c0 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -323,7 +323,7 @@ unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) | none => throw ("unknow constant '" ++ toString declName ++ "'") | some info => match info.type with - | Expr.const `Lean.AttributeImpl _ _ => env.evalConst AttributeImpl opts declName + | Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName | _ => throw ("unexpected attribute implementation type at '" ++ toString declName ++ "' (`AttributeImpl` expected") @[implementedBy mkAttributeImplOfConstantUnsafe] diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index 1841458bd9..e63eca0642 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -94,7 +94,7 @@ private def consumeNLambdas : Nat → Expr → Option Expr partial def getClassName (env : Environment) : Expr → Option Name | Expr.forallE _ _ b _ => getClassName env b | e => do - let Expr.const c _ _ ← pure e.getAppFn | none + let Expr.const c _ ← pure e.getAppFn | none let info ← env.find? c match info.value? with | some val => do diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean index eff716ced4..f249789bc1 100644 --- a/src/Lean/Compiler/ConstFolding.lean +++ b/src/Lean/Compiler/ConstFolding.lean @@ -40,14 +40,14 @@ def getInfoFromFn (fn : Name) : List NumScalarTypeInfo → Option NumScalarTypeI else getInfoFromFn fn infos def getInfoFromVal : Expr → Option NumScalarTypeInfo - | Expr.app (Expr.const fn _ _) _ _ => getInfoFromFn fn numScalarTypes - | _ => none + | Expr.app (Expr.const fn _) _ => getInfoFromFn fn numScalarTypes + | _ => none @[export lean_get_num_lit] def getNumLit : Expr → Option Nat - | Expr.lit (Literal.natVal n) _ => some n - | Expr.app (Expr.const fn _ _) a _ => if isOfNat fn then getNumLit a else none - | _ => none + | Expr.lit (Literal.natVal n) => some n + | Expr.app (Expr.const fn _) a => if isOfNat fn then getNumLit a else none + | _ => none def mkUIntLit (info : NumScalarTypeInfo) (n : Nat) : Expr := mkApp (mkConst info.ofNatFn) (mkRawNatLit (n%info.size)) @@ -148,9 +148,9 @@ def natFoldFns : List (Name × BinFoldFn) := ] def getBoolLit : Expr → Option Bool - | Expr.const ``Bool.true _ _ => some true - | Expr.const ``Bool.false _ _ => some false - | _ => none + | Expr.const ``Bool.true _ => some true + | Expr.const ``Bool.false _ => some false + | _ => none def foldStrictAnd (_ : Bool) (a₁ a₂ : Expr) : Option Expr := let v₁ := getBoolLit a₁ @@ -211,7 +211,7 @@ def findUnFoldFn (fn : Name) : Option UnFoldFn := @[export lean_fold_bin_op] def foldBinOp (beforeErasure : Bool) (f : Expr) (a : Expr) (b : Expr) : Option Expr := do match f with - | Expr.const fn _ _ => + | Expr.const fn _ => let foldFn ← findBinFoldFn fn foldFn beforeErasure a b | _ => @@ -220,7 +220,7 @@ def foldBinOp (beforeErasure : Bool) (f : Expr) (a : Expr) (b : Expr) : Option E @[export lean_fold_un_op] def foldUnOp (beforeErasure : Bool) (f : Expr) (a : Expr) : Option Expr := do match f with - | Expr.const fn _ _ => + | Expr.const fn _ => let foldFn ← findUnFoldFn fn foldFn beforeErasure a | _ => failure diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index 5ead5894f3..9d16aa8ef5 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -9,12 +9,12 @@ import Lean.Attributes namespace Lean private def getIOTypeArg : Expr → Option Expr - | Expr.app (Expr.const `IO _ _) arg _ => some arg - | _ => none + | Expr.app (Expr.const `IO _) arg => some arg + | _ => none private def isUnitType : Expr → Bool - | Expr.const `Unit _ _ => true - | _ => false + | Expr.const `Unit _ => true + | _ => false private def isIOUnit (type : Expr) : Bool := match getIOTypeArg type with diff --git a/src/Lean/Compiler/Util.lean b/src/Lean/Compiler/Util.lean index 7734bde973..9f825302d2 100644 --- a/src/Lean/Compiler/Util.lean +++ b/src/Lean/Compiler/Util.lean @@ -39,13 +39,13 @@ instance : AndThen Visitor where | {found := true, result := true} => {found := true, result := x != y} def visit (x : FVarId) : Expr → Visitor - | Expr.fvar y _ => visitFVar y x - | Expr.app f a _ => visit x a >> visit x f + | Expr.fvar y => visitFVar y x + | Expr.app f a => visit x a >> visit x f | Expr.lam _ d b _ => visit x d >> visit x b | Expr.forallE _ d b _ => visit x d >> visit x b | Expr.letE _ t v b _ => visit x t >> visit x v >> visit x b - | Expr.mdata _ e _ => visit x e - | Expr.proj _ _ e _ => visit x e + | Expr.mdata _ e => visit x e + | Expr.proj _ _ e => visit x e | _ => skip end atMostOnce diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index fa41e22eaf..c26931f12c 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -249,11 +249,11 @@ private def fTypeHasOptAutoParams : M Bool := do See `propagateExpectedType`. Remark: `(explicit : Bool) == true` when `@` modifier is used. -/ private partial def getForallBody (explicit : Bool) : Nat → List NamedArg → Expr → Option Expr - | i, namedArgs, type@(Expr.forallE n d b c) => + | i, namedArgs, type@(Expr.forallE n d b bi) => match namedArgs.find? fun (namedArg : NamedArg) => namedArg.name == n with | some _ => getForallBody explicit i (eraseNamedArgCore namedArgs n) b | none => - if !explicit && !c.binderInfo.isExplicit then + if !explicit && !bi.isExplicit then getForallBody explicit i namedArgs b else if i > 0 then getForallBody explicit (i-1) namedArgs b @@ -462,21 +462,21 @@ where isResultType (type : Expr) (i : Nat) : Bool := match type with | .forallE _ _ b _ => isResultType b (i + 1) - | .bvar idx _ => idx == i + | .bvar idx => idx == i | _ => false /- (quick filter) Return true if `type` constains a binder `[C ...]` where `C` is a class containing outparams. -/ hasLocalInstaceWithOutParams (type : Expr) : CoreM Bool := do - let .forallE _ d b c := type | return false - if c.binderInfo.isInstImplicit then + let .forallE _ d b bi := type | return false + if bi.isInstImplicit then if let .const declName .. := d.getAppFn then if hasOutParams (← getEnv) declName then return true hasLocalInstaceWithOutParams b isOutParamOfLocalInstance (x : Expr) (type : Expr) : MetaM Bool := do - let .forallE _ d b c := type | return false - if c.binderInfo.isInstImplicit then + let .forallE _ d b bi := type | return false + if bi.isInstImplicit then if let .const declName .. := d.getAppFn then if hasOutParams (← getEnv) declName then let cType ← inferType d.getAppFn @@ -538,7 +538,7 @@ mutual let argType ← getArgExpectedType match (← read).explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with | false, some defVal, _ => addNewArg argName defVal; main - | false, _, some (Expr.const tacticDecl _ _) => + | false, _, some (Expr.const tacticDecl _) => let env ← getEnv let opts ← getOptions match evalSyntaxConstant env opts tacticDecl with @@ -773,12 +773,12 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L private partial def consumeImplicits (stx : Syntax) (e eType : Expr) (hasArgs : Bool) : TermElabM (Expr × Expr) := do let eType ← whnfCore eType match eType with - | .forallE _ d b c => - if c.binderInfo.isImplicit || (hasArgs && c.binderInfo.isStrictImplicit) then + | .forallE _ d b bi => + if bi.isImplicit || (hasArgs && bi.isStrictImplicit) then let mvar ← mkFreshExprMVar d registerMVarErrorHoleInfo mvar.mvarId! stx consumeImplicits stx (mkApp e mvar) (b.instantiate1 mvar) hasArgs - else if c.binderInfo.isInstImplicit then + else if bi.isInstImplicit then let mvar ← mkInstMVar d let r := mkApp e mvar registerMVarErrorImplicitArgInfo mvar.mvarId! stx r diff --git a/src/Lean/Elab/DeclUtil.lean b/src/Lean/Elab/DeclUtil.lean index c16831433c..0347b80b28 100644 --- a/src/Lean/Elab/DeclUtil.lean +++ b/src/Lean/Elab/DeclUtil.lean @@ -19,9 +19,9 @@ def forallTelescopeCompatibleAux {α} (k : Array Expr → Expr → Expr → Meta throwError "parameter name mismatch '{n₁}', expected '{n₂}'" unless (← isDefEq d₁ d₂) do throwError "parameter '{n₁}' {← mkHasTypeButIsExpectedMsg d₁ d₂}" - unless c₁.binderInfo == c₂.binderInfo do + unless c₁ == c₂ do throwError "binder annotation mismatch at parameter '{n₁}'" - withLocalDecl n₁ c₁.binderInfo d₁ fun x => + withLocalDecl n₁ c₁ d₁ fun x => let type₁ := b₁.instantiate1 x let type₂ := b₂.instantiate1 x forallTelescopeCompatibleAux k i type₁ type₂ (xs.push x) diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index a77bca5fc6..b4677459df 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -49,7 +49,7 @@ where else let visit {ω} : StateRefT IndexSet (ST ω) Unit := e.forEach fun - | Expr.fvar fvarId _ => + | Expr.fvar fvarId => match localInst2Index.find? fvarId with | some idx => modify (·.insert idx) | none => pure () diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 784a5d3793..bbb25ade1d 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -100,7 +100,7 @@ private def mkUnknownMonadResult : MetaM ExtractMonadResult := do private partial def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do let some expectedType := expectedType? | mkUnknownMonadResult let extractStep? (type : Expr) : MetaM (Option ExtractMonadResult) := do - let .app m returnType _ := type | return none + let .app m returnType := type | return none try let bindInstType ← mkAppM ``Bind #[m] discard <| Meta.synthInstance bindInstType diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index 1d5f8dcf32..d092458f06 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -171,7 +171,7 @@ private def isUnknow : Expr → Bool | Expr.mvar .. => true | Expr.app f .. => isUnknow f | Expr.letE _ _ _ b _ => isUnknow b - | Expr.mdata _ b _ => isUnknow b + | Expr.mdata _ b => isUnknow b | _ => false private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM AnalyzeResult := do diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index 490e7d26c8..65bed617de 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -204,7 +204,7 @@ where go (type : Expr) (acc : Array Name) : Array Name := match type with | .forallE n _ b _ => go b (acc.push n) - | .mdata _ b _ => go b acc + | .mdata _ b => go b acc | _ => acc /-- @@ -217,11 +217,11 @@ where go (type : Expr) (i : Nat) : Expr := if i < newNames.size then match type with - | .forallE n d b data => + | .forallE n d b bi => if n.hasMacroScopes then - mkForall newNames[i]! data.binderInfo d (go b (i+1)) + mkForall newNames[i]! bi d (go b (i+1)) else - mkForall n data.binderInfo d (go b (i+1)) + mkForall n bi d (go b (i+1)) | _ => type else type @@ -386,8 +386,8 @@ private def getResultingUniverse : List InductiveType → TermElabM Level | indType :: _ => forallTelescopeReducing indType.type fun _ r => do let r ← whnfD r match r with - | Expr.sort u _ => return u - | _ => throwError "unexpected inductive type resulting type{indentExpr r}" + | Expr.sort u => return u + | _ => throwError "unexpected inductive type resulting type{indentExpr r}" /-- Return `some ?m` if `u` is of the form `?m + k`. diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 23a203958d..5228c0c44f 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -26,8 +26,8 @@ private def expandSimpleMatch (stx : Syntax) (discr : Term) (lhsVar : Ident) (rh private def mkUserNameFor (e : Expr) : TermElabM Name := do match e with /- Remark: we use `mkFreshUserName` to make sure we don't add a variable to the local context that can be resolved to `e`. -/ - | Expr.fvar fvarId _ => mkFreshUserName ((← getLocalDecl fvarId).userName) - | _ => mkFreshBinderName + | Expr.fvar fvarId => mkFreshUserName ((← getLocalDecl fvarId).userName) + | _ => mkFreshBinderName /-- @@ -59,7 +59,7 @@ def isAtomicDiscr? (discr : Syntax) : TermElabM (Option Expr) := do private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do let term := discr[1] match (← isAtomicDiscr? term) with - | some e@(Expr.fvar fvarId _) => + | some e@(Expr.fvar fvarId) => let localDecl ← getLocalDecl fvarId if !isAuxDiscrName localDecl.userName then addTermInfo discr e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?` @@ -536,7 +536,7 @@ where processInaccessible (e : Expr) : M Expr := do let e' ← erasePatternRefAnnotations e match e' with - | Expr.fvar _ _ => + | Expr.fvar _ => if (← isExplicitPatternVar e') then processVar e else @@ -582,8 +582,8 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do if let some e := Match.isNamedPattern? e then let p ← toPattern <| e.getArg! 2 match e.getArg! 1, e.getArg! 3 with - | Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h - | _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'" + | Expr.fvar x, Expr.fvar h => return Pattern.as x p h + | _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'" else if isMatchValue e then return Pattern.val e else if e.isFVar then @@ -615,13 +615,13 @@ private partial def topSort (patternVars : Array Expr) : TermElabM (Array Expr) where visit (e : Expr) : TopSortM Unit := do match e with - | Expr.proj _ _ e _ => visit e + | Expr.proj _ _ e => visit e | 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.mvar mvarId _ => + | Expr.app f a => visit f; visit a + | Expr.mdata _ b => visit b + | Expr.mvar mvarId => let v ← instantiateMVars e if !v.isMVar then visit v @@ -631,7 +631,7 @@ where let mvarDecl ← getMVarDecl mvarId visit mvarDecl.type modify fun s => { s with result := s.result.push e } - | Expr.fvar fvarId _ => + | Expr.fvar fvarId => if patternVars.contains e then unless (← get).visitedFVars.contains fvarId do modify fun s => { s with visitedFVars := s.visitedFVars.insert fvarId } @@ -652,9 +652,9 @@ where | .forallE n d b _ => withLocalDecl n b.binderInfo (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x)) | .lam n d b _ => withLocalDecl n b.binderInfo (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x)) | .letE n t v b .. => withLetDecl n (← go t) (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x)) - | .app f a _ => return mkApp (← go f) (← go a) - | .proj _ _ b _ => return p.updateProj! (← go b) - | .mdata k b _ => + | .app f a => return mkApp (← go f) (← go a) + | .proj _ _ b => return p.updateProj! (← go b) + | .mdata k b => if inaccessible? p |>.isSome then return mkMData k (← withReader (fun _ => false) (go b)) else if let some (stx, p) := patternWithRef? p then @@ -1229,7 +1229,7 @@ private def isPatternVar (stx : Syntax) : TermElabM Bool := do match (← resolveId? stx "pattern") with | none => return isAtomicIdent stx | some f => match f with - | Expr.const fName _ _ => + | Expr.const fName _ => match (← getEnv).find? fName with | some (ConstantInfo.ctorInfo _) => return false | some _ => return !hasMatchPatternAttribute (← getEnv) fName diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index d8f152faf3..ca704343cf 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -248,10 +248,10 @@ private def instantiateMVarsAtLetRecToLift (toLift : LetRecToLift) : TermElabM L private def typeHasRecFun (type : Expr) (funFVars : Array Expr) (letRecsToLift : List LetRecToLift) : Option FVarId := let occ? := type.find? fun e => match e with - | Expr.fvar fvarId _ => funFVars.contains e || letRecsToLift.any fun toLift => toLift.fvarId == fvarId + | Expr.fvar fvarId => funFVars.contains e || letRecsToLift.any fun toLift => toLift.fvarId == fvarId | _ => false match occ? with - | some (Expr.fvar fvarId _) => some fvarId + | some (Expr.fvar fvarId) => some fvarId | _ => none private def getFunName (fvarId : FVarId) (letRecsToLift : List LetRecToLift) : TermElabM Name := do @@ -565,7 +565,7 @@ def insertReplacementForLetRecs (r : Replacement) (letRecClosures : List LetRecC def Replacement.apply (r : Replacement) (e : Expr) : Expr := e.replace fun e => match e with - | Expr.fvar fvarId _ => match r.find? fvarId with + | Expr.fvar fvarId => match r.find? fvarId with | some c => some c | _ => none | _ => none @@ -751,13 +751,13 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs : let rec visit (e : Expr) : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit := do checkCache { val := e : ExprStructEq } fun _ => do match e with - | .forallE n d b c | .lam n d b c => visit d e; withLocalDecl n c.binderInfo d fun x => visit (b.instantiate1 x) e + | .forallE n d b c | .lam n d b c => visit d e; withLocalDecl n c d fun x => visit (b.instantiate1 x) e | .letE n t v b _ => visit t e; visit v e; withLetDecl n t v fun x => visit (b.instantiate1 x) e | .app .. => e.withApp fun f args => do visit f e; args.forM fun arg => visit arg e - | .mdata _ b _ => visit b e - | .proj _ _ b _ => visit b e - | .sort u _ => visitLevel u (← read) - | .const _ us _ => us.forM (visitLevel · (← read)) + | .mdata _ b => visit b e + | .proj _ _ b => visit b e + | .sort u => visitLevel u (← read) + | .const _ us => us.forM (visitLevel · (← read)) | _ => pure () visit preDef.value preDef.value |>.run {} for preDef in preDefs do diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 08e4ae53d3..78807b63a7 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -236,7 +236,7 @@ where match (← resolveId? stx "pattern") with | none => processVar stx | some f => match f with - | Expr.const fName _ _ => + | Expr.const fName _ => match (← getEnv).find? fName with | some (ConstantInfo.ctorInfo _) => processCtor stx | some _ => @@ -296,7 +296,7 @@ where | `($fId:ident) => pure (fId, false) | `(@$fId:ident) => pure (fId, true) | _ => throwError "identifier expected" - let some (Expr.const fName _ _) ← resolveId? fId "pattern" (withInfo := true) | throwCtorExpected + let some (Expr.const fName _) ← resolveId? fId "pattern" (withInfo := true) | throwCtorExpected let fInfo ← getConstInfo fName let paramDecls ← forallTelescopeReducing fInfo.type fun xs _ => xs.mapM fun x => do let d ← getFVarLocalDecl x diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 0a3a63dd45..cdc955f3a3 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -55,7 +55,7 @@ def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevel let us := levelParams.map mkLevelParam let fixExpr (e : Expr) : Expr := e.replace fun c => match c with - | Expr.const declName _ _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none + | Expr.const declName _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none | _ => none return preDefs.map fun preDef => { preDef with @@ -173,7 +173,7 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit := { preDef with declName := Compiler.mkUnsafeRecName preDef.declName value := preDef.value.replace fun e => match e with - | Expr.const declName us _ => + | Expr.const declName us => if preDefs.any fun preDef => preDef.declName == declName then some <| mkConst (Compiler.mkUnsafeRecName declName) us else diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index d394f37809..5df7dee2d7 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -20,7 +20,7 @@ structure EqnInfoCore where partial def expand : Expr → Expr | Expr.letE _ _ v b _ => expand (b.instantiate1 v) - | Expr.mdata _ b _ => expand b + | Expr.mdata _ b => expand b | e => e def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do @@ -115,7 +115,7 @@ def simpEqnType (eqnType : Expr) : MetaM Expr := do for y in ys.reverse do trace[Elab.definition] ">> simpEqnType: {← inferType y}, {type}" if proofVars.contains y.fvarId! then - let some (_, Expr.fvar fvarId _, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in altenative{indentExpr eqnType}" + let some (_, Expr.fvar fvarId, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in altenative{indentExpr eqnType}" eliminated := eliminated.insert fvarId type := type.replaceFVarId fvarId rhs else if eliminated.contains y.fvarId! then @@ -250,10 +250,10 @@ def removeUnusedEqnHypotheses (declType declValue : Expr) : CoreM (Expr × Expr) where go (type value : Expr) (xs : Array Expr) (lctx : LocalContext) : CoreM (Expr × Expr) := do match value with - | .lam n d b i => + | .lam n d b bi => let d := d.instantiateRev xs let fvarId ← mkFreshFVarId - go (type.bindingBody!) b (xs.push (mkFVar fvarId)) (lctx.mkLocalDecl fvarId n d i.binderInfo) + go (type.bindingBody!) b (xs.push (mkFVar fvarId)) (lctx.mkLocalDecl fvarId n d bi) | _ => let type := type.instantiateRev xs let value := value.instantiateRev xs @@ -286,7 +286,7 @@ private partial def whnfAux (e : Expr) : MetaM Expr := do let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))` let f := e.getAppFn match f with - | Expr.proj _ _ s _ => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs + | Expr.proj _ _ s => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs | _ => return e /-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/ diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 6a9617b434..744e108b54 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -33,7 +33,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa private def isNonRecursive (preDef : PreDefinition) : Bool := Option.isNone $ preDef.value.find? fun - | Expr.const declName _ _ => preDef.declName == declName + | Expr.const declName _ => preDef.declName == declName | _ => false private def partitionPreDefs (preDefs : Array PreDefinition) : Array (Array PreDefinition) := diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 8e6d282288..92659fa214 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -21,11 +21,11 @@ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : E let belowDict ← whnf belowDict trace[Elab.definition.structural] "belowDict: {belowDict}, arg: {arg}" match belowDict with - | Expr.app (Expr.app (Expr.const `PProd _ _) d1 _) d2 _ => + | .app (.app (.const `PProd _) d1) d2 => (do toBelowAux C d1 arg (← mkAppM `PProd.fst #[F])) <|> (do toBelowAux C d2 arg (← mkAppM `PProd.snd #[F])) - | Expr.app (Expr.app (Expr.const `And _ _) d1 _) d2 _ => + | .app (.app (.const `And _) d1) d2 => (do toBelowAux C d1 arg (← mkAppM `And.left #[F])) <|> (do toBelowAux C d2 arg (← mkAppM `And.right #[F])) @@ -37,7 +37,7 @@ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : E let argTailArgs := argArgs.extract (n - xs.size) n let belowDict := belowDict.replaceFVars xs argTailArgs match belowDict with - | Expr.app belowDictFun belowDictArg _ => + | .app belowDictFun belowDictArg => unless belowDictFun.getAppFn == C do throwToBelowFailed unless ← isDefEq belowDictArg arg do throwToBelowFailed pure (mkAppN F argTailArgs) @@ -105,21 +105,21 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) return e match e with | Expr.lam n d b c => - withLocalDecl n c.binderInfo (← loop below d) fun x => do + withLocalDecl n c (← loop below d) fun x => do mkLambdaFVars #[x] (← loop below (b.instantiate1 x)) | Expr.forallE n d b c => - withLocalDecl n c.binderInfo (← loop below d) fun x => do + withLocalDecl n c (← loop below d) fun x => do mkForallFVars #[x] (← loop below (b.instantiate1 x)) | Expr.letE n type val body _ => withLetDecl n (← loop below type) (← loop below val) fun x => do mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false) - | Expr.mdata d b _ => + | Expr.mdata d b => if let some _ := getRecAppSyntax? e then loop below b else return mkMData d (← loop below b) - | Expr.proj n i e _ => return mkProj n i (← loop below e) - | Expr.app _ _ _ => + | Expr.proj n i e => return mkProj n i (← loop below e) + | Expr.app _ _ => let processApp (e : Expr) : StateRefT (HasConstCache recFnName) M Expr := e.withApp fun f args => do if f.isConstOf recFnName then diff --git a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean index 2f70bee15c..5264fad15b 100644 --- a/src/Lean/Elab/PreDefinition/Structural/IndPred.lean +++ b/src/Lean/Elab/PreDefinition/Structural/IndPred.lean @@ -15,17 +15,17 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr let rec loop (e : Expr) : M Expr := do match e with | Expr.lam n d b c => - withLocalDecl n c.binderInfo (← loop d) fun x => do + withLocalDecl n c (← loop d) fun x => do mkLambdaFVars #[x] (← loop (b.instantiate1 x)) | Expr.forallE n d b c => - withLocalDecl n c.binderInfo (← loop d) fun x => do + withLocalDecl n c (← loop d) fun x => do mkForallFVars #[x] (← loop (b.instantiate1 x)) | Expr.letE n type val body _ => withLetDecl n (← loop type) (← loop val) fun x => do mkLetFVars #[x] (← loop (body.instantiate1 x)) - | Expr.mdata d e _ => return mkMData d (← loop e) - | Expr.proj n i e _ => return mkProj n i (← loop e) - | Expr.app _ _ _ => + | Expr.mdata d e => return mkMData d (← loop e) + | Expr.proj n i e => return mkProj n i (← loop e) + | Expr.app _ _ => let processApp (e : Expr) : M Expr := do e.withApp fun f args => do if f.isConstOf recFnName then diff --git a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean index aab5ba1195..aaf3b54563 100644 --- a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean +++ b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean @@ -32,8 +32,8 @@ where | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b) | Expr.letE n type val body _ => withLetDecl n type (← visit val) fun x => do mkLetFVars #[x] (← visit (body.instantiate1 x)) - | Expr.mdata d b _ => return mkMData d (← visit b) - | Expr.proj n i s _ => return mkProj n i (← visit s) + | Expr.mdata d b => return mkMData d (← visit b) + | Expr.proj n i s => return mkProj n i (← visit s) | Expr.app .. => let processApp (e : Expr) : MetaM Expr := e.withApp fun f args => diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index a686f977e5..f879f6c7c1 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean @@ -63,20 +63,20 @@ where return e match e with | Expr.lam n d b c => - withLocalDecl n c.binderInfo (← loop F d) fun x => do + withLocalDecl n c (← loop F d) fun x => do mkLambdaFVars #[x] (← loop F (b.instantiate1 x)) | Expr.forallE n d b c => - withLocalDecl n c.binderInfo (← loop F d) fun x => do + withLocalDecl n c (← loop F d) fun x => do mkForallFVars #[x] (← loop F (b.instantiate1 x)) | Expr.letE n type val body _ => withLetDecl n (← loop F type) (← loop F val) fun x => do mkLetFVars #[x] (← loop F (body.instantiate1 x)) (usedLetOnly := false) - | Expr.mdata d b _ => + | Expr.mdata d b => if let some stx := getRecAppSyntax? e then withRef stx <| loop F b else return mkMData d (← loop F b) - | Expr.proj n i e _ => return mkProj n i (← loop F e) + | Expr.proj n i e => return mkProj n i (← loop F e) | Expr.const .. => if e.isConstOf recFnName then processRec F e else return e | Expr.app .. => match (← matchMatcherApp? e) with diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean index 1e7e77fc5c..0a6d1dbe19 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean @@ -131,16 +131,16 @@ where checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do match e with | Expr.lam n d b c => - withLocalDecl n c.binderInfo (← visit d) fun x => do + withLocalDecl n c (← visit d) fun x => do mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) | Expr.forallE n d b c => - withLocalDecl n c.binderInfo (← visit d) fun x => do + withLocalDecl n c (← visit d) fun x => do mkForallFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) | Expr.letE n t v b _ => withLetDecl n (← visit t) (← visit v) fun x => do mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x)) | Expr.proj n i s .. => return mkProj n i (← visit s) - | Expr.mdata d b _ => return mkMData d (← visit b) + | Expr.mdata d b => return mkMData d (← visit b) | Expr.app .. => visitApp e | Expr.const .. => visitApp e | e => return e, diff --git a/src/Lean/Elab/RecAppSyntax.lean b/src/Lean/Elab/RecAppSyntax.lean index 1d377a5a60..f482029aad 100644 --- a/src/Lean/Elab/RecAppSyntax.lean +++ b/src/Lean/Elab/RecAppSyntax.lean @@ -21,7 +21,7 @@ def mkRecAppWithSyntax (e : Expr) (stx : Syntax) : Expr := -/ def getRecAppSyntax? (e : Expr) : Option Syntax := match e with - | Expr.mdata d _ _ => + | Expr.mdata d _ => match d.find recAppKey with | some (DataValue.ofSyntax stx) => some stx | _ => none diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index d2043e824a..1e3dabb88f 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -209,7 +209,7 @@ private def getStructName (expectedType? : Option Expr) (sourceView : Source) : | some expectedType => let expectedType ← whnf expectedType match expectedType.getAppFn with - | Expr.const constName _ _ => + | Expr.const constName _ => unless isStructure (← getEnv) constName do throwError "invalid \{...} notation, structure type expected{indentExpr expectedType}" return constName @@ -559,7 +559,7 @@ private def mkCtorHeaderAux : Nat → Expr → Expr → Array MVarId → Array ( | n+1, type, ctorFn, instMVars, params => do match (← whnfForall type) with | .forallE paramName d b c => - match c.binderInfo with + match c with | .instImplicit => let a ← mkFreshExprMVar d .synthetic mkCtorHeaderAux n (b.instantiate1 a) (mkApp ctorFn a) (instMVars.push a.mvarId!) (params.push (paramName, a)) @@ -705,8 +705,8 @@ partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : Struct) : m (O | _ => match field.expr? with | none => unreachable! | some expr => match defaultMissing? expr with - | some (.mvar mvarId _) => return if (← isExprMVarAssigned mvarId) then none else some field - | _ => return none + | some (.mvar mvarId) => return if (← isExprMVarAssigned mvarId) then none else some field + | _ => return none def getFieldName (field : Field Struct) : Name := match field.lhs with @@ -727,7 +727,7 @@ def getFieldValue? (struct : Struct) (fieldName : Name) : Option Expr := partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Expr) | .lam n d b c => withRef struct.ref do - if c.binderInfo.isExplicit then + if c.isExplicit then let fieldName := n match getFieldValue? struct fieldName with | none => return none @@ -764,7 +764,7 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do | .lam .. => lambdaLetTelescope e fun xs b => do mkLambdaFVars xs (← reduce structNames b) | .forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← reduce structNames b) | .letE .. => lambdaLetTelescope e fun xs b => do mkLetFVars xs (← reduce structNames b) - | .proj _ i b _ => + | .proj _ i b => match (← Meta.project? b i) with | some r => reduce structNames r | none => return e.updateProj! (← reduce structNames b) @@ -780,13 +780,13 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do else let args ← e.getAppArgs.mapM (reduce structNames) return mkAppN f' args - | .mdata _ b _ => + | .mdata _ b => let b ← reduce structNames b if (defaultMissing? e).isSome && !b.isMVar then return b else return e.updateMData! b - | .mvar mvarId _ => + | .mvar mvarId => match (← getExprMVarAssignment? mvarId) with | some val => if val.isMVar then pure val else reduce structNames val | none => return e @@ -828,7 +828,7 @@ partial def step (struct : Struct) : M Unit := | none => unreachable! | some expr => match defaultMissing? expr with - | some (.mvar mvarId _) => + | some (.mvar mvarId) => unless (← isExprMVarAssigned mvarId) do let ctx ← read if (← withRef field.ref <| tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) then diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 6d9cd8b34c..9a1976b960 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -373,7 +373,7 @@ where go? (e : Expr) : TermElabM (Option Expr) := do match e with | Expr.lam n d b c => - if c.binderInfo.isExplicit then + if c.isExplicit then match fieldMap.find? n with | none => failed | some val => @@ -446,7 +446,7 @@ where mkCompositeField (parentType : Expr) (fieldMap : FieldMap) : TermElabM Expr := do let env ← getEnv - let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable! + let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable! let parentCtor := getStructureCtor env parentStructName let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs for fieldName in getStructureFields env parentStructName do @@ -570,8 +570,8 @@ where private def getResultUniverse (type : Expr) : TermElabM Level := do let type ← whnf type match type with - | Expr.sort u _ => pure u - | _ => throwError "unexpected structure resulting type" + | Expr.sort u => pure u + | _ => throwError "unexpected structure resulting type" private def collectUsed (params : Array Expr) (fieldInfos : Array StructFieldInfo) : StateRefT CollectFVars.State MetaM Unit := do params.forM fun p => do @@ -746,13 +746,13 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : let structName := view.declName let sourceFieldNames := getStructureFieldsFlattened env structName let structType := mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params - let Expr.const parentStructName _ _ ← pure parentType.getAppFn | unreachable! + let Expr.const parentStructName _ ← pure parentType.getAppFn | unreachable! let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default withLocalDecl `self binfo structType fun source => do let declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType)) let declType := declType.inferImplicit params.size true let rec copyFields (parentType : Expr) : MetaM Expr := do - let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable! + let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable! let parentCtor := getStructureCtor env parentStructName let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs for fieldName in getStructureFields env parentStructName do diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 2de3204c81..65eaaaa4f5 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -80,11 +80,11 @@ def resolveParserName [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv | none => none | some info => match info.type with - | Expr.const ``Lean.Parser.TrailingParser _ _ => (c, false) - | Expr.const ``Lean.Parser.Parser _ _ => (c, false) - | Expr.const ``Lean.ParserDescr _ _ => (c, true) - | Expr.const ``Lean.TrailingParserDescr _ _ => (c, true) - | _ => none + | Expr.const ``Lean.Parser.TrailingParser _ => (c, false) + | Expr.const ``Lean.Parser.Parser _ => (c, false) + | Expr.const ``Lean.ParserDescr _ => (c, true) + | Expr.const ``Lean.TrailingParserDescr _ => (c, true) + | _ => none catch _ => return [] open TSyntax.Compat in diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 730792c876..3f5d6ae0ad 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -191,8 +191,8 @@ def getFVarId (id : Syntax) : TacticM FVarId := withRef id do let e ← withMainContext do elabTermForApply id (mayPostpone := false) match e with - | Expr.fvar fvarId _ => return fvarId - | _ => throwError "unexpected term '{e}'; expected single reference to variable" + | Expr.fvar fvarId => return fvarId + | _ => throwError "unexpected term '{e}'; expected single reference to variable" def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do withMainContext do ids.mapM getFVarId @@ -224,7 +224,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId withMainContext do let e ← elabTerm stx none match e with - | Expr.fvar fvarId _ => pure fvarId + | Expr.fvar fvarId => pure fvarId | _ => let type ← inferType e let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 723912572c..94e7c0f6ac 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -130,7 +130,7 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name) let target ← withAssignableSyntheticOpaque <| Term.ensureHasType expectedType target modify fun s => { s with targetPos := s.targetPos + 1 } addNewArg target - else match c.binderInfo with + else match c with | BinderInfo.implicit => let arg ← mkFreshExprMVar (← getArgExpectedType) addNewArg arg diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 0b64715ab8..bb0245b94e 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -490,7 +490,7 @@ def getMVarErrorInfo? (mvarId : MVarId) : TermElabM (Option MVarErrorInfo) := do def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := match e.getAppFn with - | Expr.mvar mvarId _ => registerMVarErrorCustomInfo mvarId ref msgData + | Expr.mvar mvarId => registerMVarErrorCustomInfo mvarId ref msgData | _ => pure () /- @@ -673,9 +673,9 @@ partial def visit (e : Expr) : M Unit := do | 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.app f a => visit f; visit a + | Expr.mdata _ b => visit b + | Expr.proj _ _ b => visit b | Expr.fvar fvarId .. => match (← getLocalDecl fvarId) with | LocalDecl.cdecl .. => return () @@ -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 _ => + | Expr.app (Expr.const ``Thunk u) arg => if (← isDefEq eType arg) then return some (mkApp2 (mkConst ``Thunk.mk u) arg (mkSimpleThunk e)) else @@ -819,8 +819,8 @@ 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 + | Expr.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 @@ -1092,7 +1092,7 @@ partial def removeSaveInfoAnnotation (e : Expr) : Expr := -/ def isTacticOrPostponedHole? (e : Expr) : TermElabM (Option MVarId) := do match e with - | Expr.mvar mvarId _ => + | Expr.mvar mvarId => match (← getSyntheticMVarDecl? mvarId) with | some { kind := SyntheticMVarKind.tactic .., .. } => return mvarId | some { kind := SyntheticMVarKind.postponed .., .. } => return mvarId @@ -1262,7 +1262,7 @@ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : Te let expectedType ← whnfForall expectedType match expectedType with | Expr.forallE _ _ _ c => - if c.binderInfo.isImplicit || c.binderInfo.isInstImplicit then + if c.isImplicit || c.isInstImplicit then return some expectedType else return none @@ -1299,11 +1299,11 @@ private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) ( where loop | type@(Expr.forallE n d b c), fvars => - if c.binderInfo.isExplicit then + if c.isExplicit then elabImplicitLambdaAux stx catchExPostpone type fvars else withFreshMacroScope do let n ← MonadQuotation.addMacroScope n - withLocalDecl n c.binderInfo d fun fvar => do + withLocalDecl n c d fun fvar => do let type ← whnfForall (b.instantiate1 fvar) loop type (fvars.push fvar) | type, fvars => diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 69fa98a89d..048fe30174 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -744,14 +744,14 @@ unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (typeName : | none => throw ("unknown constant '" ++ toString constName ++ "'") | some info => match info.type with - | Expr.const c _ _ => + | Expr.const c _ => if c != typeName then throwUnexpectedType typeName constName else env.evalConst α opts constName | _ => throwUnexpectedType typeName constName def hasUnsafe (env : Environment) (e : Expr) : Bool := let c? := e.find? fun e => match e with - | Expr.const c _ _ => + | Expr.const c _ => match env.find? c with | some cinfo => cinfo.isUnsafe | none => false diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index dbac714f30..7d00d292b3 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -236,37 +236,69 @@ instance : Inhabited (FVarIdMap α) where /- We use the `E` suffix (short for `Expr`) to avoid collision with keywords. We considered using «...», but it is too inconvenient to use. -/ inductive Expr where - | bvar : Nat → Data → Expr -- bound variables - | fvar : FVarId → Data → Expr -- free variables - | mvar : MVarId → Data → Expr -- meta variables - | sort : Level → Data → Expr -- Sort - | const : Name → List Level → Data → Expr -- constants - | app : Expr → Expr → Data → Expr -- application - | lam : Name → Expr → Expr → Data → Expr -- lambda abstraction - | forallE : Name → Expr → Expr → Data → Expr -- (dependent) arrow - | letE : Name → Expr → Expr → Expr → Data → Expr -- let expressions - | lit : Literal → Data → Expr -- literals - | mdata : MData → Expr → Data → Expr -- metadata - | proj : Name → Nat → Expr → Data → Expr -- projection - deriving Inhabited, Repr + | bvar : Nat → Expr -- bound variables + | fvar : FVarId → Expr -- free variables + | mvar : MVarId → Expr -- meta variables + | sort : Level → Expr -- Sort + | const : Name → List Level → Expr -- constants + | app : Expr → Expr → Expr -- application + | lam : Name → Expr → Expr → BinderInfo → Expr -- lambda abstraction + | forallE : Name → Expr → Expr → BinderInfo → Expr -- (dependent) arrow + | letE : Name → Expr → Expr → Expr → Bool → Expr -- let expressions + | lit : Literal → Expr -- literals + | mdata : MData → Expr → Expr -- metadata + | proj : Name → Nat → Expr → Expr -- projection +with + @[computedField, extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"] + data : @& Expr → Data + | .const n lvls => mkData (mixHash 5 <| mixHash (hash n) (hash lvls)) 0 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam) + | .bvar idx => mkData (mixHash 7 <| hash idx) (idx+1) + | .sort lvl => mkData (mixHash 11 <| hash lvl) 0 0 false false lvl.hasMVar lvl.hasParam + | .fvar fvarId => mkData (mixHash 13 <| hash fvarId) 0 0 true + | .mvar fvarId => mkData (mixHash 17 <| hash fvarId) 0 0 false true + | .mdata _m e => + let d := e.data.approxDepth.toUInt32+1 + mkData (mixHash d.toUInt64 <| e.data.hash) e.data.looseBVarRange.toNat d e.data.hasFVar e.data.hasExprMVar e.data.hasLevelMVar e.data.hasLevelParam + | .proj s i e => + let d := e.data.approxDepth.toUInt32+1 + mkData (mixHash d.toUInt64 <| mixHash (hash s) <| mixHash (hash i) e.data.hash) + e.data.looseBVarRange.toNat d e.data.hasFVar e.data.hasExprMVar e.data.hasLevelMVar e.data.hasLevelParam + | .app f a => mkAppData f.data a.data + | .lam _x t b bi => + let d := (max t.data.approxDepth.toUInt32 b.data.approxDepth.toUInt32) + 1 + mkDataForBinder (mixHash d.toUInt64 <| mixHash t.data.hash b.data.hash) + (max t.data.looseBVarRange.toNat (b.data.looseBVarRange.toNat - 1)) + d + (t.data.hasFVar || b.data.hasFVar) + (t.data.hasExprMVar || b.data.hasExprMVar) + (t.data.hasLevelMVar || b.data.hasLevelMVar) + (t.data.hasLevelParam || b.data.hasLevelParam) + bi + | .forallE _x t b bi => + let d := (max t.data.approxDepth.toUInt32 b.data.approxDepth.toUInt32) + 1 + mkDataForBinder (mixHash d.toUInt64 <| mixHash t.data.hash b.data.hash) + (max t.data.looseBVarRange.toNat (b.data.looseBVarRange.toNat - 1)) + d + (t.data.hasFVar || b.data.hasFVar) + (t.data.hasExprMVar || b.data.hasExprMVar) + (t.data.hasLevelMVar || b.data.hasLevelMVar) + (t.data.hasLevelParam || b.data.hasLevelParam) + bi + | .letE _x t v b nonDep => + let d := (max (max t.data.approxDepth.toUInt32 v.data.approxDepth.toUInt32) b.data.approxDepth.toUInt32) + 1 + mkDataForLet (mixHash d.toUInt64 <| mixHash t.data.hash <| mixHash v.data.hash b.data.hash) + (max (max t.data.looseBVarRange.toNat v.data.looseBVarRange.toNat) (b.data.looseBVarRange.toNat - 1)) + d + (t.data.hasFVar || v.data.hasFVar || b.data.hasFVar) + (t.data.hasExprMVar || v.data.hasExprMVar || b.data.hasExprMVar) + (t.data.hasLevelMVar || v.data.hasLevelMVar || b.data.hasLevelMVar) + (t.data.hasLevelParam || v.data.hasLevelParam || b.data.hasLevelParam) + nonDep + | .lit l => mkData (mixHash 3 (hash l)) +deriving Inhabited, Repr namespace Expr -@[extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"] -def data : (@& Expr) → Data - | bvar _ d => d - | fvar _ d => d - | mvar _ d => d - | sort _ d => d - | const _ _ d => d - | app _ _ d => d - | lam _ _ _ d => d - | forallE _ _ _ d => d - | letE _ _ _ _ d => d - | lit _ d => d - | mdata _ _ d => d - | proj _ _ _ d => d - def ctorName : Expr → String | bvar .. => "bvar" | fvar .. => "fvar" @@ -329,7 +361,7 @@ def binderInfo (e : Expr) : BinderInfo := end Expr def mkConst (n : Name) (lvls : List Level := []) : Expr := - Expr.const n lvls <| mkData (mixHash 5 <| mixHash (hash n) (hash lvls)) 0 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam) + Expr.const n lvls def Literal.type : Literal → Expr | Literal.natVal _ => mkConst `Nat @@ -339,52 +371,31 @@ def Literal.type : Literal → Expr def Literal.typeEx : Literal → Expr := Literal.type def mkBVar (idx : Nat) : Expr := - Expr.bvar idx <| mkData (mixHash 7 <| hash idx) (idx+1) + Expr.bvar idx def mkSort (lvl : Level) : Expr := - Expr.sort lvl <| mkData (mixHash 11 <| hash lvl) 0 0 false false lvl.hasMVar lvl.hasParam + Expr.sort lvl def mkFVar (fvarId : FVarId) : Expr := - Expr.fvar fvarId <| mkData (mixHash 13 <| hash fvarId) 0 0 true + Expr.fvar fvarId def mkMVar (fvarId : MVarId) : Expr := - Expr.mvar fvarId <| mkData (mixHash 17 <| hash fvarId) 0 0 false true + Expr.mvar fvarId def mkMData (m : MData) (e : Expr) : Expr := - let d := e.approxDepth+1 - Expr.mdata m e <| mkData (mixHash d.toUInt64 <| hash e) e.looseBVarRange d e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam + Expr.mdata m e def mkProj (s : Name) (i : Nat) (e : Expr) : Expr := - let d := e.approxDepth+1 - Expr.proj s i e <| mkData (mixHash d.toUInt64 <| mixHash (hash s) <| mixHash (hash i) (hash e)) - e.looseBVarRange d e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam + Expr.proj s i e def mkApp (f a : Expr) : Expr := - Expr.app f a (mkAppData f.data a.data) + Expr.app f a def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr := - let d := (max t.approxDepth b.approxDepth) + 1 - -- let x := x.eraseMacroScopes - Expr.lam x t b <| mkDataForBinder (mixHash d.toUInt64 <| mixHash (hash t) (hash b)) - (max t.looseBVarRange (b.looseBVarRange - 1)) - d - (t.hasFVar || b.hasFVar) - (t.hasExprMVar || b.hasExprMVar) - (t.hasLevelMVar || b.hasLevelMVar) - (t.hasLevelParam || b.hasLevelParam) - bi + Expr.lam x t b bi def mkForall (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr := - let d := (max t.approxDepth b.approxDepth) + 1 - -- let x := x.eraseMacroScopes - Expr.forallE x t b <| mkDataForBinder (mixHash d.toUInt64 <| mixHash (hash t) (hash b)) - (max t.looseBVarRange (b.looseBVarRange - 1)) - d - (t.hasFVar || b.hasFVar) - (t.hasExprMVar || b.hasExprMVar) - (t.hasLevelMVar || b.hasLevelMVar) - (t.hasLevelParam || b.hasLevelParam) - bi + Expr.forallE x t b bi /-- Return `Unit -> type`. Do not confuse with `Thunk type` -/ def mkSimpleThunkType (type : Expr) : Expr := @@ -395,16 +406,7 @@ def mkSimpleThunk (type : Expr) : Expr := mkLambda `_ BinderInfo.default (Lean.mkConst `Unit) type def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr := - let d := (max (max t.approxDepth v.approxDepth) b.approxDepth) + 1 - -- let x := x.eraseMacroScopes - Expr.letE x t v b <| mkDataForLet (mixHash d.toUInt64 <| mixHash (hash t) <| mixHash (hash v) (hash b)) - (max (max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1)) - d - (t.hasFVar || v.hasFVar || b.hasFVar) - (t.hasExprMVar || v.hasExprMVar || b.hasExprMVar) - (t.hasLevelMVar || v.hasLevelMVar || b.hasLevelMVar) - (t.hasLevelParam || v.hasLevelParam || b.hasLevelParam) - nonDep + Expr.letE x t v b nonDep def mkAppB (f a b : Expr) := mkApp (mkApp f a) b def mkApp2 (f a b : Expr) := mkAppB f a b @@ -418,7 +420,7 @@ def mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) := mkApp5 (mkApp4 f a b c def mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) := mkApp6 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆ def mkLit (l : Literal) : Expr := - Expr.lit l <| mkData (mixHash 3 (hash l)) + Expr.lit l def mkRawNatLit (n : Nat) : Expr := mkLit (Literal.natVal n) @@ -490,11 +492,11 @@ def isSort : Expr → Bool | _ => false def isType : Expr → Bool - | sort (Level.succ ..) _ => true + | sort (Level.succ ..) => true | _ => false def isProp : Expr → Bool - | sort (Level.zero ..) _ => true + | sort (Level.zero ..) => true | _ => false def isBVar : Expr → Bool @@ -558,20 +560,20 @@ def getForallBody : Expr → Expr function applications `f a₁ .. aₙ`, return `f`. Otherwise return the input expression. -/ def getAppFn : Expr → Expr - | app f _ _ => getAppFn f + | app f _ => getAppFn f | e => e def getAppNumArgsAux : Expr → Nat → Nat - | app f _ _, n => getAppNumArgsAux f (n+1) - | _, n => n + | app f _, n => getAppNumArgsAux f (n+1) + | _, n => n /-- Counts the number `n` of arguments for an expression `f a₁ .. aₙ`. -/ def getAppNumArgs (e : Expr) : Nat := getAppNumArgsAux e 0 private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr - | app f a _, as, i => getAppArgsAux f (as.set! i a) (i-1) - | _, as, _ => as + | app f a, as, i => getAppArgsAux f (as.set! i a) (i-1) + | _, as, _ => as /-- Given `f a₁ a₂ ... aₙ`, returns `#[a₁, ..., aₙ]` -/ @[inline] def getAppArgs (e : Expr) : Array Expr := @@ -580,16 +582,16 @@ private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr getAppArgsAux e (mkArray nargs dummy) (nargs-1) private def getAppRevArgsAux : Expr → Array Expr → Array Expr - | app f a _, as => getAppRevArgsAux f (as.push a) - | _, as => as + | app f a, as => getAppRevArgsAux f (as.push a) + | _, as => as /-- Same as `getAppArgs` but reverse the output array. -/ @[inline] def getAppRevArgs (e : Expr) : Array Expr := getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs) @[specialize] def withAppAux (k : Expr → Array Expr → α) : Expr → Array Expr → Nat → α - | app f a _, as, i => withAppAux k f (as.set! i a) (i-1) - | f, as, _ => k f as + | app f a, as, i => withAppAux k f (as.set! i a) (i-1) + | f, as, _ => k f as /-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]`. -/ @[inline] def withApp (e : Expr) (k : Expr → Array Expr → α) : α := @@ -604,22 +606,22 @@ def traverseApp {M} [Monad M] e.withApp fun fn args => mkAppN <$> f fn <*> args.mapM f @[specialize] private def withAppRevAux (k : Expr → Array Expr → α) : Expr → Array Expr → α - | app f a _, as => withAppRevAux k f (as.push a) - | f, as => k f as + | app f a, as => withAppRevAux k f (as.push a) + | f, as => k f as /-- Same as `withApp` but with arguments reversed. -/ @[inline] def withAppRev (e : Expr) (k : Expr → Array Expr → α) : α := withAppRevAux k e (Array.mkEmpty e.getAppNumArgs) def getRevArgD : Expr → Nat → Expr → Expr - | app _ a _, 0, _ => a - | app f _ _, i+1, v => getRevArgD f i v - | _, _, v => v + | app _ a, 0, _ => a + | app f _, i+1, v => getRevArgD f i v + | _, _, v => v def getRevArg! : Expr → Nat → Expr - | app _ a _, 0 => a - | app f _ _, i+1 => getRevArg! f i - | _, _ => panic! "invalid index" + | app _ a, 0 => a + | app f _, i+1 => getRevArg! f i + | _, _ => panic! "invalid index" /-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or panics if out of bounds. -/ @[inline] def getArg! (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr := @@ -632,87 +634,87 @@ def getRevArg! : Expr → Nat → Expr /-- Given `f a₀ a₁ ... aₙ`, returns true if `f` is a constant with name `n`. -/ def isAppOf (e : Expr) (n : Name) : Bool := match e.getAppFn with - | const c _ _ => c == n + | const c _ => c == n | _ => false /-- Given `f a₁ ... aᵢ`, returns true if `f` is a constant with name `n` and has the correct number of arguments. -/ def isAppOfArity : Expr → Name → Nat → Bool - | const c _ _, n, 0 => c == n - | app f _ _, n, a+1 => isAppOfArity f n a - | _, _, _ => false + | const c _, n, 0 => c == n + | app f _, n, a+1 => isAppOfArity f n a + | _, _, _ => false /-- Similar to `isAppOfArity` but skips `Expr.mdata`. -/ def isAppOfArity' : Expr → Name → Nat → Bool - | mdata _ b _ , n, a => isAppOfArity' b n a - | const c _ _, n, 0 => c == n - | app f _ _, n, a+1 => isAppOfArity' f n a - | _, _, _ => false + | mdata _ b , n, a => isAppOfArity' b n a + | const c _, n, 0 => c == n + | app f _, n, a+1 => isAppOfArity' f n a + | _, _, _ => false def appFn! : Expr → Expr - | app f _ _ => f - | _ => panic! "application expected" + | app f _ => f + | _ => panic! "application expected" def appArg! : Expr → Expr - | app _ a _ => a - | _ => panic! "application expected" + | app _ a => a + | _ => panic! "application expected" def appFn!' : Expr → Expr - | mdata _ b _ => appFn!' b - | app f _ _ => f - | _ => panic! "application expected" + | mdata _ b => appFn!' b + | app f _ => f + | _ => panic! "application expected" def appArg!' : Expr → Expr - | mdata _ b _ => appArg!' b - | app _ a _ => a - | _ => panic! "application expected" + | mdata _ b => appArg!' b + | app _ a => a + | _ => panic! "application expected" def sortLevel! : Expr → Level - | sort u .. => u - | _ => panic! "sort expected" + | sort u => u + | _ => panic! "sort expected" def litValue! : Expr → Literal - | lit v .. => v - | _ => panic! "literal expected" + | lit v => v + | _ => panic! "literal expected" def isNatLit : Expr → Bool - | lit (Literal.natVal _) _ => true - | _ => false + | lit (Literal.natVal _) => true + | _ => false def natLit? : Expr → Option Nat - | lit (Literal.natVal v) _ => v - | _ => none + | lit (Literal.natVal v) => v + | _ => none def isStringLit : Expr → Bool - | lit (Literal.strVal _) _ => true - | _ => false + | lit (Literal.strVal _) => true + | _ => false def isCharLit (e : Expr) : Bool := e.isAppOfArity ``Char.ofNat 1 && e.appArg!.isNatLit def constName! : Expr → Name - | const n _ _ => n - | _ => panic! "constant expected" + | const n _ => n + | _ => panic! "constant expected" def constName? : Expr → Option Name - | const n _ _ => some n - | _ => none + | const n _ => some n + | _ => none def constLevels! : Expr → List Level - | const _ ls _ => ls - | _ => panic! "constant expected" + | const _ ls => ls + | _ => panic! "constant expected" def bvarIdx! : Expr → Nat - | bvar idx _ => idx - | _ => panic! "bvar expected" + | bvar idx => idx + | _ => panic! "bvar expected" def fvarId! : Expr → FVarId - | fvar n _ => n - | _ => panic! "fvar expected" + | fvar n => n + | _ => panic! "fvar expected" def mvarId! : Expr → MVarId - | mvar n _ => n - | _ => panic! "mvar expected" + | mvar n => n + | _ => panic! "mvar expected" def bindingName! : Expr → Name | forallE n _ _ _ => n @@ -730,9 +732,9 @@ def bindingBody! : Expr → Expr | _ => panic! "binding expected" def bindingInfo! : Expr → BinderInfo - | forallE _ _ _ c => c.binderInfo - | lam _ _ _ c => c.binderInfo - | _ => panic! "binding expected" + | forallE _ _ _ bi => bi + | lam _ _ _ bi => bi + | _ => panic! "binding expected" def letName! : Expr → Name | letE n .. => n @@ -751,20 +753,20 @@ def letBody! : Expr → Expr | _ => panic! "let expression expected" def consumeMData : Expr → Expr - | mdata _ e _ => consumeMData e - | e => e + | mdata _ e => consumeMData e + | e => e def mdataExpr! : Expr → Expr - | mdata _ e _ => e - | _ => panic! "mdata expression expected" + | mdata _ e => e + | _ => panic! "mdata expression expected" def projExpr! : Expr → Expr - | proj _ _ e _ => e - | _ => panic! "proj expression expected" + | proj _ _ e => e + | _ => panic! "proj expression expected" def projIdx! : Expr → Nat - | proj _ i _ _ => i - | _ => panic! "proj expression expected" + | proj _ i _ => i + | _ => panic! "proj expression expected" def hasLooseBVars (e : Expr) : Bool := e.looseBVarRange > 0 @@ -780,8 +782,9 @@ opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool /-- Return true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter, or in the range if `tryRange == true`. -/ def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool - | Expr.forallE _ d b c, bvarIdx, tryRange => (c.binderInfo.isExplicit && hasLooseBVar d bvarIdx) || hasLooseBVarInExplicitDomain b (bvarIdx+1) tryRange - | e, bvarIdx, tryRange => tryRange && hasLooseBVar e bvarIdx + | Expr.forallE _ d b bi, bvarIdx, tryRange => + (bi.isExplicit && hasLooseBVar d bvarIdx) || hasLooseBVarInExplicitDomain b (bvarIdx+1) tryRange + | e, bvarIdx, tryRange => tryRange && hasLooseBVar e bvarIdx /-- Lower the loose bound variables `>= s` in `e` by `d`. @@ -806,9 +809,9 @@ opaque liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr When the `{}` annotation is used in these commands, we set `considerRange == false`. -/ def inferImplicit : Expr → Nat → Bool → Expr - | Expr.forallE n d b c, i+1, considerRange => + | Expr.forallE n d b bi, i+1, considerRange => let b := inferImplicit b i considerRange - let newInfo := if c.binderInfo.isExplicit && hasLooseBVarInExplicitDomain b 0 considerRange then BinderInfo.implicit else c.binderInfo + let newInfo := if bi.isExplicit && hasLooseBVarInExplicitDomain b 0 considerRange then BinderInfo.implicit else bi mkForall n newInfo d b | e, 0, _ => e | e, _, _ => e @@ -953,7 +956,7 @@ partial def betaRev (f : Expr) (revArgs : Array Expr) (useZeta := false) (preser else let n := sz - i mkAppRevRange (e.instantiateRange n sz revArgs) 0 n revArgs - | Expr.mdata k b _=> + | Expr.mdata k b => if preserveMData then let n := sz - i mkMData k (mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs) @@ -972,7 +975,7 @@ def beta (f : Expr) (args : Array Expr) : Expr := def isHeadBetaTargetFn (useZeta : Bool) : Expr → Bool | Expr.lam .. => true | Expr.letE _ _ _ b _ => useZeta && isHeadBetaTargetFn useZeta b - | Expr.mdata _ b _ => isHeadBetaTargetFn useZeta b + | Expr.mdata _ b => isHeadBetaTargetFn useZeta b | _ => false /-- `(fun x => e) a` ==> `e[x/a]`. -/ @@ -984,9 +987,9 @@ def isHeadBetaTarget (e : Expr) (useZeta := false) : Bool := e.getAppFn.isHeadBetaTargetFn useZeta private def etaExpandedBody : Expr → Nat → Nat → Option Expr - | app f (bvar j _) _, n+1, i => if j == i then etaExpandedBody f n (i+1) else none - | _, _+1, _ => none - | f, 0, _ => if f.hasLooseBVars then none else some f + | app f (bvar j), n+1, i => if j == i then etaExpandedBody f n (i+1) else none + | _, _+1, _ => none + | f, 0, _ => if f.hasLooseBVars then none else some f private def etaExpandedAux : Expr → Nat → Option Expr | lam _ _ b _, n => etaExpandedAux b (n+1) @@ -1048,11 +1051,11 @@ partial def consumeMDataAndTypeAnnotations (e : Expr) : Expr := match e with | Expr.forallE _ d b _ => visit d || visit b | Expr.lam _ d b _ => visit d || visit b - | Expr.mdata _ e _ => visit e + | Expr.mdata _ e => visit e | Expr.letE _ t v b _ => visit t || visit v || visit b - | Expr.app f a _ => visit f || visit a - | Expr.proj _ _ e _ => visit e - | Expr.fvar fvarId _ => p fvarId + | Expr.app f a => visit f || visit a + | Expr.proj _ _ e => visit e + | Expr.fvar fvarId => p fvarId | _ => false visit e @@ -1128,8 +1131,8 @@ def updateForall (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody @[inline] def updateForallE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr := match h : e with - | forallE _ _ _ c => updateForall e c.binderInfo newDomain newBody (h ▸ rfl) - | _ => panic! "forall expected" + | forallE _ _ _ c => updateForall e c newDomain newBody (h ▸ rfl) + | _ => panic! "forall expected" @[extern "lean_expr_update_lambda"] def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isLambda) : Expr := @@ -1142,7 +1145,7 @@ def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody @[inline] def updateLambdaE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr := match h : e with - | lam _ _ _ c => updateLambda e c.binderInfo newDomain newBody (h ▸ rfl) + | lam _ _ _ c => updateLambda e c newDomain newBody (h ▸ rfl) | _ => panic! "lambda expected" @[extern "lean_expr_update_let"] @@ -1155,15 +1158,15 @@ def updateLet (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (h : | _ => panic! "let expression expected" def updateFn : Expr → Expr → Expr - | e@(app f a _), g => e.updateApp! (updateFn f g) a - | _, g => g + | e@(app f a), g => e.updateApp! (updateFn f g) a + | _, g => g partial def eta (e : Expr) : Expr := match e with | Expr.lam _ d b _ => let b' := b.eta match b' with - | Expr.app f (Expr.bvar 0 _) _ => + | .app f (.bvar 0) => if !f.hasLooseBVar 0 then f.lowerLooseBVars 1 1 else @@ -1180,11 +1183,11 @@ partial def eta (e : Expr) : Expr := | lam _ d b _ => e.updateLambdaE! (visit d) (visit b) | forallE _ d b _ => e.updateForallE! (visit d) (visit b) | letE _ t v b _ => e.updateLet! (visit t) (visit v) (visit b) - | app f a _ => e.updateApp! (visit f) (visit a) - | proj _ _ s _ => e.updateProj! (visit s) - | mdata _ b _ => e.updateMData! (visit b) - | const _ us _ => e.updateConst! (us.map (fun u => u.instantiateParams s)) - | sort u _ => e.updateSort! (u.instantiateParams s) + | app f a => e.updateApp! (visit f) (visit a) + | proj _ _ s => e.updateProj! (visit s) + | mdata _ b => e.updateMData! (visit b) + | const _ us => e.updateConst! (us.map (fun u => u.instantiateParams s)) + | sort u => e.updateSort! (u.instantiateParams s) | e => e visit e @@ -1246,8 +1249,8 @@ def mkAnnotation (kind : Name) (e : Expr) : Expr := def annotation? (kind : Name) (e : Expr) : Option Expr := match e with - | Expr.mdata d b _ => if d.size == 1 && d.getBool kind false then some b else none - | _ => none + | .mdata d b => if d.size == 1 && d.getBool kind false then some b else none + | _ => none def mkLetFunAnnotation (e : Expr) : Expr := mkAnnotation `let_fun e @@ -1278,7 +1281,7 @@ private def patternRefAnnotationKey := `_patWithRef -/ def patternWithRef? (p : Expr) : Option (Syntax × Expr) := match p with - | Expr.mdata d _ _ => + | Expr.mdata d _ => match d.find patternRefAnnotationKey with | some (DataValue.ofSyntax stx) => some (stx, p.mdataExpr!) | _ => none diff --git a/src/Lean/HeadIndex.lean b/src/Lean/HeadIndex.lean index bbcabc7e88..57f1c51e7e 100644 --- a/src/Lean/HeadIndex.lean +++ b/src/Lean/HeadIndex.lean @@ -37,15 +37,15 @@ end HeadIndex namespace Expr def head : Expr → Expr - | app f _ _ => head f + | app f _ => head f | letE _ _ _ b _ => head b - | mdata _ e _ => head e + | mdata _ e => head e | e => e private def headNumArgsAux : Expr → Nat → Nat - | app f _ _, n => headNumArgsAux f (n + 1) + | app f _, n => headNumArgsAux f (n + 1) | letE _ _ _ b _, n => headNumArgsAux b n - | mdata _ e _, n => headNumArgsAux e n + | mdata _ e, n => headNumArgsAux e n | _, n => n def headNumArgs (e : Expr) : Nat := @@ -60,17 +60,17 @@ def headNumArgs (e : Expr) : Nat := ``` -/ private def toHeadIndexQuick? : Expr → Option HeadIndex - | mvar mvarId _ => HeadIndex.mvar mvarId - | fvar fvarId _ => HeadIndex.fvar fvarId - | const constName _ _ => HeadIndex.const constName - | proj structName idx _ _ => HeadIndex.proj structName idx - | sort _ _ => HeadIndex.sort + | mvar mvarId => HeadIndex.mvar mvarId + | fvar fvarId => HeadIndex.fvar fvarId + | const constName _ => HeadIndex.const constName + | proj structName idx _ => HeadIndex.proj structName idx + | sort _ => HeadIndex.sort | lam _ _ _ _ => HeadIndex.lam | forallE _ _ _ _ => HeadIndex.forallE - | lit v _ => HeadIndex.lit v - | app f _ _ => toHeadIndexQuick? f + | lit v => HeadIndex.lit v + | app f _ => toHeadIndexQuick? f | letE _ _ _ b _ => toHeadIndexQuick? b - | mdata _ e _ => toHeadIndexQuick? e + | mdata _ e => toHeadIndexQuick? e | _ => none /- @@ -80,17 +80,17 @@ private def toHeadIndexQuick? : Expr → Option HeadIndex since `toHeadIndexQuick?` succeeds most of the time. -/ private partial def toHeadIndexSlow : Expr → HeadIndex - | mvar mvarId _ => HeadIndex.mvar mvarId - | fvar fvarId _ => HeadIndex.fvar fvarId - | const constName _ _ => HeadIndex.const constName - | proj structName idx _ _ => HeadIndex.proj structName idx - | sort _ _ => HeadIndex.sort + | mvar mvarId => HeadIndex.mvar mvarId + | fvar fvarId => HeadIndex.fvar fvarId + | const constName _ => HeadIndex.const constName + | proj structName idx _ => HeadIndex.proj structName idx + | sort _ => HeadIndex.sort | lam _ _ _ _ => HeadIndex.lam | forallE _ _ _ _ => HeadIndex.forallE - | lit v _ => HeadIndex.lit v - | app f _ _ => toHeadIndexSlow f + | lit v => HeadIndex.lit v + | app f _ => toHeadIndexSlow f | letE _ _ v b _ => toHeadIndexSlow (b.instantiate1 v) - | mdata _ e _ => toHeadIndexSlow e + | mdata _ e => toHeadIndexSlow e | _ => panic! "unexpected expression kind" def toHeadIndex (e : Expr) : HeadIndex := diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 86ee113616..be9855988a 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -120,7 +120,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe let key ← df.evalKey true stx let decl ← getConstInfo declName match decl.type with - | Expr.const c _ _ => + | Expr.const c _ => if c != df.valueTypeName then throwError "unexpected type at '{declName}', '{df.valueTypeName}' expected" else /- builtin_initialize @addBuiltin $(mkConst valueTypeName) $(mkConst attrDeclName) $(key) $(declName) $(mkConst declName) -/ diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean index 210e3d6836..dc627c584d 100644 --- a/src/Lean/Linter/Basic.lean +++ b/src/Lean/Linter/Basic.lean @@ -70,8 +70,8 @@ def unusedVariables : Linter := fun stx => do let tacticFVarUses : HashSet FVarId ← tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do let (_, s) ← StateT.run (s := uses) <| expr.forEach fun - | .fvar id _ => modify (·.insert id) - | _ => pure () + | .fvar id => modify (·.insert id) + | _ => pure () return s -- determine unused variables diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean index d09ded902e..4af4a0f934 100644 --- a/src/Lean/Meta/AbstractMVars.lean +++ b/src/Lean/Meta/AbstractMVars.lean @@ -71,18 +71,18 @@ partial def abstractExprMVars (e : Expr) : M Expr := do return e else match e with - | e@(Expr.lit _ _) => return e - | e@(Expr.bvar _ _) => return e - | e@(Expr.fvar _ _) => return e - | e@(Expr.sort u _) => return e.updateSort! (← abstractLevelMVars u) - | e@(Expr.const _ us _) => return e.updateConst! (← us.mapM abstractLevelMVars) - | e@(Expr.proj _ _ s _) => return e.updateProj! (← abstractExprMVars s) - | e@(Expr.app f a _) => return e.updateApp! (← abstractExprMVars f) (← abstractExprMVars a) - | e@(Expr.mdata _ b _) => return e.updateMData! (← abstractExprMVars b) + | e@(Expr.lit _) => return e + | e@(Expr.bvar _) => return e + | e@(Expr.fvar _) => return e + | e@(Expr.sort u) => return e.updateSort! (← abstractLevelMVars u) + | e@(Expr.const _ us) => return e.updateConst! (← us.mapM abstractLevelMVars) + | e@(Expr.proj _ _ s) => return e.updateProj! (← abstractExprMVars s) + | e@(Expr.app f a) => return e.updateApp! (← abstractExprMVars f) (← abstractExprMVars a) + | e@(Expr.mdata _ b) => return e.updateMData! (← abstractExprMVars b) | e@(Expr.lam _ d b _) => return e.updateLambdaE! (← abstractExprMVars d) (← abstractExprMVars b) | e@(Expr.forallE _ d b _) => return e.updateForallE! (← abstractExprMVars d) (← abstractExprMVars b) | e@(Expr.letE _ t v b _) => return e.updateLet! (← abstractExprMVars t) (← abstractExprMVars v) (← abstractExprMVars b) - | e@(Expr.mvar mvarId _) => + | e@(Expr.mvar mvarId) => let decl := (← getMCtx).getDecl mvarId if decl.depth != (← getMCtx).depth then return e diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean index 00c5fd1e96..75c6bb378b 100644 --- a/src/Lean/Meta/AbstractNestedProofs.lean +++ b/src/Lean/Meta/AbstractNestedProofs.lean @@ -57,9 +57,9 @@ partial def visit (e : Expr) : M Expr := do | Expr.lam _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false) | Expr.letE _ _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false) | Expr.forallE _ _ _ _ => forallTelescope e fun xs b => visitBinders xs do mkForallFVars xs (← visit b) - | Expr.mdata _ b _ => return e.updateMData! (← visit b) - | Expr.proj _ _ b _ => return e.updateProj! (← visit b) - | Expr.app _ _ _ => e.withApp fun f args => return mkAppN f (← args.mapM visit) + | Expr.mdata _ b => return e.updateMData! (← visit b) + | Expr.proj _ _ b => return e.updateProj! (← visit b) + | Expr.app _ _ => e.withApp fun f args => return mkAppN f (← args.mapM visit) | _ => pure e end AbstractNestedProofs diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index b146a8691d..2a1f646027 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -205,9 +205,9 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met if i >= xs.size then mkAppMFinal `mkAppM f args instMVars else match type with - | Expr.forallE n d b c => + | Expr.forallE n d b bi => let d := d.instantiateRevRange j args.size args - match c.binderInfo with + match bi with | BinderInfo.implicit => let mvar ← mkFreshExprMVar d MetavarKind.natural n loop b i j (args.push mvar) instMVars @@ -265,12 +265,12 @@ def mkAppM' (f : Expr) (xs : Array Expr) : MetaM Expr := do return r private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat → Array Expr → Nat → Array MVarId → Expr → MetaM Expr - | i, args, j, instMVars, Expr.forallE n d b c => do + | i, args, j, instMVars, Expr.forallE n d b bi => do let d := d.instantiateRevRange j args.size args if h : i < xs.size then match xs.get ⟨i, h⟩ with | none => - match c.binderInfo with + match bi with | BinderInfo.instImplicit => do let mvar ← mkFreshExprMVar d MetavarKind.synthetic n mkAppOptMAux f xs (i+1) (args.push mvar) j (instMVars.push mvar.mvarId!) b @@ -332,7 +332,7 @@ def mkEqNDRec (motive h1 h2 : Expr) : MetaM Expr := do let u2 ← getLevel α let motiveType ← infer motive match motiveType with - | Expr.forallE _ _ (Expr.sort u1 _) _ => + | Expr.forallE _ _ (Expr.sort u1) _ => return mkAppN (mkConst ``Eq.ndrec [u1, u2]) #[α, a, motive, h1, b, h2] | _ => throwAppBuilderException ``Eq.ndrec ("invalid motive" ++ indentExpr motive) @@ -347,7 +347,7 @@ def mkEqRec (motive h1 h2 : Expr) : MetaM Expr := do let u2 ← getLevel α let motiveType ← infer motive match motiveType with - | Expr.forallE _ _ (Expr.forallE _ _ (Expr.sort u1 _) _) _ => + | Expr.forallE _ _ (Expr.forallE _ _ (Expr.sort u1) _) _ => return mkAppN (mkConst ``Eq.rec [u1, u2]) #[α, a, motive, h1, b, h2] | _ => throwAppBuilderException ``Eq.rec ("invalid motive" ++ indentExpr motive) @@ -379,7 +379,7 @@ partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do let type ← inferType s let type ← whnf type match type.getAppFn with - | Expr.const structName us _ => + | Expr.const structName us => let env ← getEnv unless isStructure env structName do throwAppBuilderException `mkProjection ("structure expected" ++ hasTypeMsg s type) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index c693e38a1e..65f1957605 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -690,13 +690,13 @@ private partial def isClassQuick? : Expr → MetaM (LOption Name) | Expr.letE .. => pure LOption.undef | Expr.proj .. => pure LOption.undef | Expr.forallE _ _ b _ => isClassQuick? b - | Expr.mdata _ e _ => isClassQuick? e - | Expr.const n _ _ => isClassQuickConst? n - | Expr.mvar mvarId _ => do + | Expr.mdata _ e => isClassQuick? e + | Expr.const n _ => isClassQuickConst? n + | Expr.mvar mvarId => do match (← getExprMVarAssignment? mvarId) with | some val => isClassQuick? val | none => pure LOption.none - | Expr.app f _ _ => + | Expr.app f _ => match f.getAppFn with | Expr.const n .. => isClassQuickConst? n | Expr.lam .. => pure LOption.undef @@ -798,11 +798,11 @@ mutual (k : Array Expr → Expr → MetaM α) : MetaM α := do let rec process (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (type : Expr) : MetaM α := do match type with - | Expr.forallE n d b c => + | Expr.forallE n d b bi => if fvarsSizeLtMaxFVars fvars maxFVars? then let d := d.instantiateRevRange j fvars.size fvars let fvarId ← mkFreshFVarId - let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo + let lctx := lctx.mkLocalDecl fvarId n d bi let fvar := mkFVar fvarId let fvars := fvars.push fvar process lctx fvars j b @@ -840,13 +840,13 @@ mutual forallTelescopeReducingAux type none fun _ type => do let env ← getEnv match type.getAppFn with - | Expr.const c _ _ => do + | Expr.const c _ => do if isClass env c then return some c else -- make sure abbreviations are unfolded match (← whnf type).getAppFn with - | Expr.const c _ _ => return if isClass env c then some c else none + | Expr.const c _ => return if isClass env c then some c else none | _ => return none | _ => return none @@ -910,10 +910,10 @@ private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (k : Array where process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (e : Expr) : MetaM α := do match consumeLet, e with - | _, Expr.lam n d b c => + | _, Expr.lam n d b bi => let d := d.instantiateRevRange j fvars.size fvars let fvarId ← mkFreshFVarId - let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo + let lctx := lctx.mkLocalDecl fvarId n d bi let fvar := mkFVar fvarId process consumeLet lctx (fvars.push fvar) j b | true, Expr.letE n t v b _ => do @@ -958,12 +958,12 @@ where return (mvars, bis, type) else match type with - | Expr.forallE n d b c => + | Expr.forallE n d b bi => let d := d.instantiateRevRange j mvars.size mvars - let k := if c.binderInfo.isInstImplicit then MetavarKind.synthetic else kind + let k := if bi.isInstImplicit then MetavarKind.synthetic else kind let mvar ← mkFreshExprMVar d k n let mvars := mvars.push mvar - let bis := bis.push c.binderInfo + let bis := bis.push bi process mvars bis j b | _ => let type := type.instantiateRevRange j mvars.size mvars; @@ -1008,11 +1008,11 @@ where finalize () else match type with - | Expr.lam _ d b c => + | Expr.lam _ d b bi => let d := d.instantiateRevRange j mvars.size mvars let mvar ← mkFreshExprMVar d let mvars := mvars.push mvar - let bis := bis.push c.binderInfo + let bis := bis.push bi process mvars bis j b | _ => finalize () @@ -1348,9 +1348,9 @@ def getResetPostponed : MetaM (PersistentArray PostponedEntry) := do /-- Annotate any constant and sort in `e` that satisfies `p` with `pp.universes true` -/ private def exposeRelevantUniverses (e : Expr) (p : Level → Bool) : Expr := e.replace fun - | Expr.const _ us _ => if us.any p then some (e.setPPUniverses true) else none - | Expr.sort u _ => if p u then some (e.setPPUniverses true) else none - | _ => none + | Expr.const _ us => if us.any p then some (e.setPPUniverses true) else none + | Expr.sort u => if p u then some (e.setPPUniverses true) else none + | _ => none private def mkLeveErrorMessageCore (header : String) (entry : PostponedEntry) : MetaM MessageData := do match entry.ctx? with diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index bc7cb40b4e..7646455f9e 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -24,7 +24,7 @@ structure CasesOnApp where /-- Return `some c` if `e` is a `casesOn` application. -/ def toCasesOnApp? (e : Expr) : MetaM (Option CasesOnApp) := do let f := e.getAppFn - let .const declName us _ := f | return none + let .const declName us := f | return none unless isCasesOnRecursor (← getEnv) declName do return none let indName := declName.getPrefix let .inductInfo info ← getConstInfo indName | return none diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean index ae46897d14..241e79d0a2 100644 --- a/src/Lean/Meta/Check.lean +++ b/src/Lean/Meta/Check.lean @@ -32,7 +32,7 @@ private def getFunctionDomain (f : Expr) : MetaM (Expr × BinderInfo) := do let fType ← inferType f let fType ← whnfD fType match fType with - | Expr.forallE _ d _ c => return (d, c.binderInfo) + | Expr.forallE _ d _ c => return (d, c) | _ => throwFunctionExpected f /- @@ -152,10 +152,10 @@ where | .forallE .. => checkForall e | .lam .. => checkLambdaLet e | .letE .. => checkLambdaLet e - | .const c lvls _ => checkConstant c lvls - | .app f a _ => check f; check a; checkApp f a - | .mdata _ e _ => check e - | .proj _ _ e _ => check e + | .const c lvls => checkConstant c lvls + | .app f a => check f; check a; checkApp f a + | .mdata _ e => check e + | .proj _ _ e => check e | _ => return () checkLambdaLet (e : Expr) : MonadCacheT ExprStructEq Unit MetaM Unit := diff --git a/src/Lean/Meta/Closure.lean b/src/Lean/Meta/Closure.lean index fb188a86f5..d8e52610c8 100644 --- a/src/Lean/Meta/Closure.lean +++ b/src/Lean/Meta/Closure.lean @@ -188,15 +188,15 @@ def pushToProcess (elem : ToProcessElement) : ClosureM Unit := partial def collectExprAux (e : Expr) : ClosureM Expr := do let collect (e : Expr) := visitExpr collectExprAux e match e with - | Expr.proj _ _ s _ => return e.updateProj! (← collect s) + | Expr.proj _ _ s => return e.updateProj! (← collect s) | Expr.forallE _ d b _ => return e.updateForallE! (← collect d) (← collect b) | Expr.lam _ d b _ => return e.updateLambdaE! (← collect d) (← collect b) | Expr.letE _ t v b _ => return e.updateLet! (← collect t) (← collect v) (← collect b) - | Expr.app f a _ => return e.updateApp! (← collect f) (← collect a) - | Expr.mdata _ b _ => return e.updateMData! (← collect b) - | Expr.sort u _ => return e.updateSort! (← collectLevel u) - | Expr.const _ us _ => return e.updateConst! (← us.mapM collectLevel) - | Expr.mvar mvarId _ => + | Expr.app f a => return e.updateApp! (← collect f) (← collect a) + | Expr.mdata _ b => return e.updateMData! (← collect b) + | Expr.sort u => return e.updateSort! (← collectLevel u) + | Expr.const _ us => return e.updateConst! (← us.mapM collectLevel) + | Expr.mvar mvarId => let mvarDecl ← getMVarDecl mvarId let type ← preprocess mvarDecl.type let type ← collect type @@ -207,7 +207,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do exprMVarArgs := s.exprMVarArgs.push e } return mkFVar newFVarId - | Expr.fvar fvarId _ => + | Expr.fvar fvarId => match (← read).zeta, (← getLocalDecl fvarId).value? with | true, some value => collect (← preprocess value) | _, _ => diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index b7c560a30e..379de67392 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -159,7 +159,7 @@ private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Boo isProof a private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr → MetaM (Array Expr) - | i, Expr.app f a _, todo => do + | i, Expr.app f a, todo => do if (← ignoreArg a i infos) then pushArgsAux infos (i-1) f (todo.push tmpStar) else @@ -280,8 +280,8 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key let todo ← pushArgsAux info.paramInfo (nargs-1) e todo return (k, todo) match fn with - | Expr.lit v _ => return (Key.lit v, todo) - | Expr.const c _ _ => + | Expr.lit v => return (Key.lit v, todo) + | Expr.const c _ => unless root do if (← shouldAddAsStar c e) then return (Key.star, todo) @@ -289,10 +289,10 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key push (Key.const c nargs) nargs | Expr.proj s i a .. => return (Key.proj s i, todo.push a) - | Expr.fvar fvarId _ => + | Expr.fvar fvarId => let nargs := e.getAppNumArgs push (Key.fvar fvarId nargs) nargs - | Expr.mvar mvarId _ => + | Expr.mvar mvarId => if mvarId == tmpMVarId then -- We use `tmp to mark implicit arguments and proofs return (Key.star, todo) @@ -368,8 +368,8 @@ def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Expr) := do let e ← whnfDT e root match e.getAppFn with - | Expr.lit v _ => return (Key.lit v, #[]) - | Expr.const c _ _ => + | Expr.lit v => return (Key.lit v, #[]) + | Expr.const c _ => if (← getConfig).isDefEqStuckEx && e.hasExprMVar then if (← isReducible c) then /- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not unfolded. @@ -400,10 +400,10 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex Meta.throwIsDefEqStuck let nargs := e.getAppNumArgs return (Key.const c nargs, e.getAppRevArgs) - | Expr.fvar fvarId _ => + | Expr.fvar fvarId => let nargs := e.getAppNumArgs return (Key.fvar fvarId nargs, e.getAppRevArgs) - | Expr.mvar mvarId _ => + | Expr.mvar mvarId => if isMatch then return (Key.other, #[]) else do diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 058ca88e58..eb4c2c7195 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -78,7 +78,7 @@ private def isDefEqEta (a b : Expr) : MetaM Bool := do let bType ← whnfD bType match bType with | Expr.forallE n d _ c => - let b' := mkLambda n c.binderInfo d (mkApp b (mkBVar 0)) + let b' := mkLambda n c d (mkApp b (mkBVar 0)) checkpointDefEq <| Meta.isExprDefEqAux a b' | _ => pure false else @@ -124,7 +124,7 @@ def isDefEqStringLit (s t : Expr) : MetaM LBool := do Remark: `n` may be 0. -/ def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do match e.etaExpanded? with - | some (Expr.mvar mvarId _) => + | some (Expr.mvar mvarId) => if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then pure false else if (← isExprMVarAssigned mvarId) then @@ -356,10 +356,10 @@ where | 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 _ => + | Expr.app f a => visit f; visit a + | Expr.mdata _ b => visit b + | Expr.proj _ _ b => visit b + | Expr.fvar fvarId => let localDecl ← getLocalDecl fvarId if localDecl.isLet && localDecl.index > (← read) then modify fun s => s.insert localDecl.fvarId @@ -752,8 +752,8 @@ mutual partial def check (e : Expr) : CheckAssignmentM Expr := do match e with - | Expr.mdata _ b _ => return e.updateMData! (← visit check b) - | Expr.proj _ _ s _ => return e.updateProj! (← visit check s) + | Expr.mdata _ b => return e.updateMData! (← visit check b) + | Expr.proj _ _ s => return e.updateProj! (← visit check s) | Expr.lam _ d b _ => return e.updateLambdaE! (← visit check d) (← visit check b) | Expr.forallE _ d b _ => return e.updateForallE! (← visit check d) (← visit check b) | Expr.letE _ t v b _ => return e.updateLet! (← visit check t) (← visit check v) (← visit check b) @@ -789,9 +789,9 @@ partial def check if !e.hasExprMVar && !e.hasFVar then true else match e with - | Expr.mdata _ b _ => visit b - | Expr.proj _ _ s _ => visit s - | Expr.app f a _ => visit f && visit a + | Expr.mdata _ b => visit b + | Expr.proj _ _ s => visit s + | Expr.app f a => visit f && visit a | Expr.lam _ d b _ => visit d && visit b | Expr.forallE _ d b _ => visit d && visit b | Expr.letE _ t v b _ => visit t && visit v && visit b @@ -806,7 +806,7 @@ partial def check | _ => if fvars.any fun x => x.fvarId! == fvarId then true else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it - | Expr.mvar mvarId' _ => + | Expr.mvar mvarId' => match mctx.getExprAssignmentCore? mvarId' with | some _ => false -- use CheckAssignment.check to instantiate | none => @@ -851,7 +851,7 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool := match v with - | Expr.app f a _ => + | Expr.app f a => if args.isEmpty then pure false else @@ -891,8 +891,8 @@ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr) loop v private partial def simpAssignmentArgAux : Expr → MetaM Expr - | Expr.mdata _ e _ => simpAssignmentArgAux e - | e@(Expr.fvar fvarId _) => do + | Expr.mdata _ e => simpAssignmentArgAux e + | e@(Expr.fvar fvarId) => do let decl ← getLocalDecl fvarId match decl.value? with | some value => simpAssignmentArgAux value @@ -992,7 +992,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool : let arg ← simpAssignmentArg arg let args := args.set ⟨i, h⟩ arg match arg with - | Expr.fvar fvarId _ => + | Expr.fvar fvarId => if args[0:i].any fun prevArg => prevArg == arg then useFOApprox args else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then @@ -1048,7 +1048,7 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do match t.getAppFn with - | Expr.const c _ _ => + | Expr.const c _ => match (← getConst? c) with | r@(some info) => if info.hasValue then return r else return none | _ => return none @@ -1133,8 +1133,8 @@ private abbrev unfold (e : Expr) (failK : MetaM α) (successK : Expr → MetaM /-- Auxiliary method for isDefEqDelta -/ private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do match t, s with - | Expr.const _ ls₁ _, Expr.const _ ls₂ _ => isListLevelDefEq ls₁ ls₂ - | Expr.app _ _ _, Expr.app _ _ _ => + | Expr.const _ ls₁, Expr.const _ ls₂ => isListLevelDefEq ls₁ ls₂ + | Expr.app _ _, Expr.app _ _ => if (← tryHeuristic t s) then pure LBool.true else @@ -1145,8 +1145,8 @@ private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do private def sameHeadSymbol (t s : Expr) : Bool := match t.getAppFn, s.getAppFn with - | Expr.const c₁ _ _, Expr.const c₂ _ _ => c₁ == c₂ - | _, _ => false + | Expr.const c₁ _, Expr.const c₂ _ => c₁ == c₂ + | _, _ => false /-- - If headSymbol (unfold t) == headSymbol s, then unfold t @@ -1262,8 +1262,8 @@ private def isDefEqDelta (t s : Expr) : MetaM LBool := do unfoldNonProjFnDefEq tInfo sInfo t s private def isAssigned : Expr → MetaM Bool - | Expr.mvar mvarId _ => isExprMVarAssigned mvarId - | _ => pure false + | Expr.mvar mvarId => isExprMVarAssigned mvarId + | _ => pure false private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do let tFn := t.getAppFn @@ -1295,7 +1295,7 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do return some (mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs) private def isSynthetic : Expr → MetaM Bool - | Expr.mvar mvarId _ => do + | Expr.mvar mvarId => do let mvarDecl ← getMVarDecl mvarId match mvarDecl.kind with | MetavarKind.synthetic => pure true @@ -1304,8 +1304,8 @@ private def isSynthetic : Expr → MetaM Bool | _ => pure false private def isAssignable : Expr → MetaM Bool - | Expr.mvar mvarId _ => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b) - | _ => pure false + | Expr.mvar mvarId => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b) + | _ => pure false private def etaEq (t s : Expr) : Bool := match t.etaExpanded? with @@ -1391,13 +1391,13 @@ private partial def isDefEqQuick (t s : Expr) : MetaM LBool := let t := consumeLet t let s := consumeLet s match t, s with - | Expr.lit l₁ _, Expr.lit l₂ _ => return (l₁ == l₂).toLBool - | Expr.sort u _, Expr.sort v _ => toLBoolM <| isLevelDefEqAux u v + | Expr.lit l₁, Expr.lit l₂ => return (l₁ == l₂).toLBool + | Expr.sort u, Expr.sort v => toLBoolM <| isLevelDefEqAux u v | Expr.lam .., Expr.lam .. => if t == s then pure LBool.true else toLBoolM <| isDefEqBinding t s | Expr.forallE .., Expr.forallE .. => if t == s then pure LBool.true else toLBoolM <| isDefEqBinding t s -- | Expr.mdata _ t _, s => isDefEqQuick t s -- | t, Expr.mdata _ s _ => isDefEqQuick t s - | Expr.fvar fvarId₁ _, Expr.fvar fvarId₂ _ => do + | Expr.fvar fvarId₁, Expr.fvar fvarId₂ => do if (← isLetFVar fvarId₁ <||> isLetFVar fvarId₂) then pure LBool.undef else if fvarId₁ == fvarId₂ then @@ -1572,9 +1572,9 @@ private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do tryUnificationHints t s <||> tryUnificationHints s t private def isDefEqProj : Expr → Expr → MetaM Bool - | Expr.proj _ i t _, Expr.proj _ j s _ => pure (i == j) <&&> Meta.isExprDefEqAux t s - | Expr.proj structName 0 s _, v => isDefEqSingleton structName s v - | v, Expr.proj structName 0 s _ => isDefEqSingleton structName s v + | Expr.proj _ i t, Expr.proj _ j s => pure (i == j) <&&> Meta.isExprDefEqAux t s + | Expr.proj structName 0 s, v => isDefEqSingleton structName s v + | v, Expr.proj structName 0 s => isDefEqSingleton structName s v | _, _ => pure false where /- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve contraint as `?m ... =?= ⟨v⟩` -/ diff --git a/src/Lean/Meta/ExprLens.lean b/src/Lean/Meta/ExprLens.lean index 04fcde4cc1..a794eaafde 100644 --- a/src/Lean/Meta/ExprLens.lean +++ b/src/Lean/Meta/ExprLens.lean @@ -28,17 +28,17 @@ Mdata is ignored. An index of 3 is interpreted as the type of the expression. An See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/ private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr - | 0, e@(Expr.app f a _) => return e.updateApp! (← g f) a - | 1, e@(Expr.app f a _) => return e.updateApp! f (← g a) + | 0, e@(Expr.app f a) => return e.updateApp! (← g f) a + | 1, e@(Expr.app f a) => return e.updateApp! f (← g a) | 0, e@(Expr.lam _ y b _) => return e.updateLambdaE! (← g y) b - | 1, (Expr.lam n y b c) => withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x] + | 1, (Expr.lam n y b c) => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b - | 1, (Expr.forallE n y b c) => withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x] + | 1, (Expr.forallE n y b c) => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x] | 0, e@(Expr.letE _ y a b _) => return e.updateLet! (← g y) a b | 1, e@(Expr.letE _ y a b _) => return e.updateLet! y (← g a) b | 2, (Expr.letE n y a b _) => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x] - | 0, e@(Expr.proj _ _ b _) => e.updateProj! <$> g b - | n, e@(Expr.mdata _ a _) => e.updateMData! <$> lensCoord g n a + | 0, e@(Expr.proj _ _ b) => e.updateProj! <$> g b + | n, e@(Expr.mdata _ a) => e.updateMData! <$> lensCoord g n a | 3, _ => throwError "Lensing on types is not supported" | c, e => throwError "Invalid coordinate {c} for {e}" @@ -57,17 +57,17 @@ The subexpression value passed to `k` is not instantiated with respect to the array of free variables. -/ private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) : Nat → Expr → M α | 3, _ => throwError "Internal: Types should be handled by viewAux" - | 0, (Expr.app f _ _) => k fvars f - | 1, (Expr.app _ a _) => k fvars a + | 0, (Expr.app f _) => k fvars f + | 1, (Expr.app _ a) => k fvars a | 0, (Expr.lam _ y _ _) => k fvars y - | 1, (Expr.lam n y b c) => withLocalDecl n c.binderInfo (y.instantiateRev fvars) fun x => k (fvars.push x) b + | 1, (Expr.lam n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b | 0, (Expr.forallE _ y _ _) => k fvars y - | 1, (Expr.forallE n y b c) => withLocalDecl n c.binderInfo (y.instantiateRev fvars) fun x => k (fvars.push x) b + | 1, (Expr.forallE n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b | 0, (Expr.letE _ y _ _ _) => k fvars y | 1, (Expr.letE _ _ a _ _) => k fvars a | 2, (Expr.letE n y a b _) => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b - | 0, (Expr.proj _ _ b _) => k fvars b - | n, (Expr.mdata _ a _) => viewCoordAux k fvars n a + | 0, (Expr.proj _ _ b) => k fvars b + | n, (Expr.mdata _ a) => viewCoordAux k fvars n a | c, e => throwError "Invalid coordinate {c} for {e}" private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : List Nat → Expr → M α @@ -123,8 +123,8 @@ variable {M} [Monad M] [MonadError M] /-- Get the raw subexpression without performing any instantiation. -/ private def viewCoordRaw: Expr → Nat → M Expr | e , 3 => throwError "Can't viewRaw the type of {e}" - | (Expr.app f _ _) , 0 => pure f - | (Expr.app _ a _) , 1 => pure a + | (Expr.app f _) , 0 => pure f + | (Expr.app _ a) , 1 => pure a | (Expr.lam _ y _ _) , 0 => pure y | (Expr.lam _ _ b _) , 1 => pure b | (Expr.forallE _ y _ _), 0 => pure y @@ -132,8 +132,8 @@ private def viewCoordRaw: Expr → Nat → M Expr | (Expr.letE _ y _ _ _) , 0 => pure y | (Expr.letE _ _ a _ _) , 1 => pure a | (Expr.letE _ _ _ b _) , 2 => pure b - | (Expr.proj _ _ b _) , 0 => pure b - | (Expr.mdata _ a _) , n => viewCoordRaw a n + | (Expr.proj _ _ b) , 0 => pure b + | (Expr.mdata _ a) , n => viewCoordRaw a n | e , c => throwError "Bad coordinate {c} for {e}" diff --git a/src/Lean/Meta/ExprTraverse.lean b/src/Lean/Meta/ExprTraverse.lean index 9e51f0c7b4..12aa047833 100644 --- a/src/Lean/Meta/ExprTraverse.lean +++ b/src/Lean/Meta/ExprTraverse.lean @@ -23,7 +23,7 @@ def traverseLambdaWithPos where visit (fvars : Array Expr) (p : Pos) : Expr → M Expr | (Expr.lam n d b c) => do let d ← f p.pushBindingDomain <| d.instantiateRev fvars - withLocalDecl n c.binderInfo d fun x => + withLocalDecl n c d fun x => visit (fvars.push x) p.pushBindingBody b | e => do let body ← f p <| e.instantiateRev fvars @@ -35,7 +35,7 @@ def traverseForallWithPos where visit fvars (p : Pos): Expr → M Expr | (Expr.forallE n d b c) => do let d ← f p.pushBindingDomain <| d.instantiateRev fvars - withLocalDecl n c.binderInfo d fun x => + withLocalDecl n c d fun x => visit (fvars.push x) p.pushBindingBody b | e => do let body ← f p <| e.instantiateRev fvars @@ -64,8 +64,8 @@ def traverseChildrenWithPos (visit : Pos → Expr → M Expr) (p : Pos) (e: Expr | Expr.lam .. => traverseLambdaWithPos visit p e | Expr.letE .. => traverseLetWithPos visit p e | Expr.app .. => Expr.traverseAppWithPos visit p e - | Expr.mdata _ b _ => e.updateMData! <$> visit p b - | Expr.proj _ _ b _ => e.updateProj! <$> visit p.pushProj b + | Expr.mdata _ b => e.updateMData! <$> visit p b + | Expr.proj _ _ b => e.updateProj! <$> visit p.pushProj b | _ => pure e /-- Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run diff --git a/src/Lean/Meta/ForEachExpr.lean b/src/Lean/Meta/ForEachExpr.lean index 78b6514abf..c3121483f2 100644 --- a/src/Lean/Meta/ForEachExpr.lean +++ b/src/Lean/Meta/ForEachExpr.lean @@ -18,12 +18,12 @@ private partial def visitBinder (fn : Expr → MetaM Bool) : Array Expr → Nat | fvars, j, Expr.lam n d b c => do let d := d.instantiateRevRange j fvars.size fvars visit fn d - withLocalDecl n c.binderInfo d fun x => + withLocalDecl n c d fun x => visitBinder fn (fvars.push x) j b | fvars, j, Expr.forallE n d b c => do let d := d.instantiateRevRange j fvars.size fvars visit fn d - withLocalDecl n c.binderInfo d fun x => + withLocalDecl n c d fun x => visitBinder fn (fvars.push x) j b | fvars, j, Expr.letE n t v b _ => do let t := t.instantiateRevRange j fvars.size fvars @@ -41,9 +41,9 @@ partial def visit (fn : Expr → MetaM Bool) (e : Expr) : M Unit := | .forallE .. => visitBinder fn #[] 0 e | .lam .. => visitBinder fn #[] 0 e | .letE .. => visitBinder fn #[] 0 e - | .app f a _ => visit fn f; visit fn a - | .mdata _ b _ => visit fn b - | .proj _ _ b _ => visit fn b + | .app f a => visit fn f; visit fn a + | .mdata _ b => visit fn b + | .proj _ _ b => visit fn b | _ => return () end @@ -63,7 +63,7 @@ def forEachExpr (e : Expr) (f : Expr → MetaM Unit) : MetaM Unit := /-- Return true iff `x` is a metavariable with an anonymous user facing name. -/ private def shouldInferBinderName (x : Expr) : MetaM Bool := do match x with - | .mvar mvarId _ => return (← Meta.getMVarDecl mvarId).userName.isAnonymous + | .mvar mvarId => return (← Meta.getMVarDecl mvarId).userName.isAnonymous | _ => return false /-- diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean index 87dad6d33c..e1a37d3b54 100644 --- a/src/Lean/Meta/FunInfo.lean +++ b/src/Lean/Meta/FunInfo.lean @@ -24,12 +24,12 @@ namespace Lean.Meta private def collectDeps (fvars : Array Expr) (e : Expr) : Array Nat := let rec visit (e : Expr) (deps : Array Nat) : Array Nat := match e with - | .app f a _ => whenHasVar e deps (visit a ∘ visit f) + | .app f a => whenHasVar e deps (visit a ∘ visit f) | .forallE _ d b _ => whenHasVar e deps (visit b ∘ visit d) | .lam _ d b _ => whenHasVar e deps (visit b ∘ visit d) | .letE _ t v b _ => whenHasVar e deps (visit b ∘ visit v ∘ visit t) - | .proj _ _ e _ => visit e deps - | .mdata _ e _ => visit e deps + | .proj _ _ e => visit e deps + | .mdata _ e => visit e deps | .fvar .. => match fvars.indexOf? e with | none => deps diff --git a/src/Lean/Meta/GeneralizeTelescope.lean b/src/Lean/Meta/GeneralizeTelescope.lean index 7a4da2ffdf..fbac805195 100644 --- a/src/Lean/Meta/GeneralizeTelescope.lean +++ b/src/Lean/Meta/GeneralizeTelescope.lean @@ -38,7 +38,7 @@ partial def generalizeTelescopeAux {α} (k : Array Expr → MetaM α) let entries ← updateTypes e x entries (i+1) generalizeTelescopeAux k entries (i+1) (fvars.push x) match entries.get ⟨i, h⟩ with - | ⟨e@(.fvar fvarId _), type, false⟩ => + | ⟨e@(.fvar fvarId), type, false⟩ => let localDecl ← getLocalDecl fvarId match localDecl with | .cdecl .. => generalizeTelescopeAux k entries (i+1) (fvars.push e) diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 3fd5a54115..69b8f7db2c 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -38,8 +38,8 @@ where | .forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1)) | .lam _ d b _ => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1)) | .letE _ t v b _ => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1)) - | .mdata _ b _ => return e.updateMData! (← visit b offset) - | .proj _ _ b _ => return e.updateProj! (← visit b offset) + | .mdata _ b => return e.updateMData! (← visit b offset) + | .proj _ _ b => return e.updateProj! (← visit b offset) | .app .. => e.withAppRev fun f revArgs => do let fNew ← visit f offset @@ -49,7 +49,7 @@ where return fNew.betaRev revArgs else return mkAppRev fNew revArgs - | Expr.bvar vidx _ => + | Expr.bvar vidx => -- Recall that looseBVarRange for `Expr.bvar` is `vidx+1`. -- So, we must have offset ≤ vidx, since we are in the "else" branch of `if offset >= e.looseBVarRange` let n := stop - start @@ -126,8 +126,8 @@ def getLevel (type : Expr) : MetaM Level := do let typeType ← inferType type let typeType ← whnfD typeType match typeType with - | Expr.sort lvl _ => return lvl - | Expr.mvar mvarId _ => + | Expr.sort lvl => return lvl + | Expr.mvar mvarId => if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then throwTypeExcepted type else @@ -183,16 +183,16 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do def inferTypeImp (e : Expr) : MetaM Expr := let rec infer (e : Expr) : MetaM Expr := do match e with - | .const c [] _ => inferConstType c [] - | .const c us _ => checkInferTypeCache e (inferConstType c us) - | .proj n i s _ => checkInferTypeCache e (inferProjType n i s) + | .const c [] => inferConstType c [] + | .const c us => checkInferTypeCache e (inferConstType c us) + | .proj n i s => checkInferTypeCache e (inferProjType n i s) | .app f .. => checkInferTypeCache e (inferAppType f.getAppFn e.getAppArgs) - | .mvar mvarId _ => inferMVarType mvarId - | .fvar fvarId _ => inferFVarType fvarId - | .bvar bidx _ => throwError "unexpected bound variable {mkBVar bidx}" - | .mdata _ e _ => infer e - | .lit v _ => return v.type - | .sort lvl _ => return mkSort (mkLevelSucc lvl) + | .mvar mvarId => inferMVarType mvarId + | .fvar fvarId => inferFVarType fvarId + | .bvar bidx => throwError "unexpected bound variable {mkBVar bidx}" + | .mdata _ e => infer e + | .lit v => return v.type + | .sort lvl => return mkSort (mkLevelSucc lvl) | .forallE .. => checkInferTypeCache e (inferForallType e) | .lam .. => checkInferTypeCache e (inferLambdaType e) | .letE .. => checkInferTypeCache e (inferLambdaType e) @@ -214,22 +214,22 @@ private def isAlwaysZero : Level → Bool if `type` is of the form `A_1 -> ... -> A_n -> Prop`. Remark: `type` can be a dependent arrow. -/ private partial def isArrowProp : Expr → Nat → MetaM LBool - | .sort u _, 0 => return isAlwaysZero (← instantiateLevelMVars u) |>.toLBool + | .sort u, 0 => return isAlwaysZero (← instantiateLevelMVars u) |>.toLBool | .forallE .., 0 => return LBool.false | .forallE _ _ b _, n+1 => isArrowProp b n | .letE _ _ _ b _, n => isArrowProp b n - | .mdata _ e _, n => isArrowProp e n + | .mdata _ e, n => isArrowProp e n | _, _ => return LBool.undef /-- `isPropQuickApp f n` is an "approximate" predicate which returns `LBool.true` if `f` applied to `n` arguments is a proposition. -/ private partial def isPropQuickApp : Expr → Nat → MetaM LBool - | .const c lvls _, arity => do let constType ← inferConstType c lvls; isArrowProp constType arity - | .fvar fvarId _, arity => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType arity - | .mvar mvarId _, arity => do let mvarType ← inferMVarType mvarId; isArrowProp mvarType arity + | .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowProp constType arity + | .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType arity + | .mvar mvarId, arity => do let mvarType ← inferMVarType mvarId; isArrowProp mvarType arity | .app f .., arity => isPropQuickApp f (arity+1) - | .mdata _ e _, arity => isPropQuickApp e arity + | .mdata _ e, arity => isPropQuickApp e arity | .letE _ _ _ b _, arity => isPropQuickApp b arity | .lam .., 0 => return LBool.false | .lam _ _ b _, arity+1 => isPropQuickApp b arity @@ -246,10 +246,10 @@ partial def isPropQuick : Expr → MetaM LBool | .letE _ _ _ b _ => isPropQuick b | .proj .. => return LBool.undef | .forallE _ _ b _ => isPropQuick b - | .mdata _ e _ => isPropQuick e - | .const c lvls _ => do let constType ← inferConstType c lvls; isArrowProp constType 0 - | .fvar fvarId _ => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType 0 - | .mvar mvarId _ => do let mvarType ← inferMVarType mvarId; isArrowProp mvarType 0 + | .mdata _ e => isPropQuick e + | .const c lvls => do let constType ← inferConstType c lvls; isArrowProp constType 0 + | .fvar fvarId => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType 0 + | .mvar mvarId => do let mvarType ← inferMVarType mvarId; isArrowProp mvarType 0 | .app f .. => isPropQuickApp f 1 /-- `isProp whnf e` return `true` if `e` is a proposition. @@ -266,8 +266,8 @@ def isProp (e : Expr) : MetaM Bool := do let type ← inferType e let type ← whnfD type match type with - | Expr.sort u _ => return isAlwaysZero (← instantiateLevelMVars u) - | _ => return false + | Expr.sort u => return isAlwaysZero (← instantiateLevelMVars u) + | _ => return false /-- `isArrowProposition type n` is an "approximate" predicate which returns `LBool.true` @@ -276,7 +276,7 @@ def isProp (e : Expr) : MetaM Bool := do private partial def isArrowProposition : Expr → Nat → MetaM LBool | .forallE _ _ b _, n+1 => isArrowProposition b n | .letE _ _ _ b _, n => isArrowProposition b n - | .mdata _ e _, n => isArrowProposition e n + | .mdata _ e, n => isArrowProposition e n | type, 0 => isPropQuick type | _, _ => return LBool.undef @@ -285,11 +285,11 @@ mutual `isProofQuickApp f n` is an "approximate" predicate which returns `LBool.true` if `f` applied to `n` arguments is a proof. -/ private partial def isProofQuickApp : Expr → Nat → MetaM LBool - | .const c lvls _, arity => do let constType ← inferConstType c lvls; isArrowProposition constType arity - | .fvar fvarId _, arity => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType arity - | .mvar mvarId _, arity => do let mvarType ← inferMVarType mvarId; isArrowProposition mvarType arity - | .app f _ _, arity => isProofQuickApp f (arity+1) - | .mdata _ e _, arity => isProofQuickApp e arity + | .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowProposition constType arity + | .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType arity + | .mvar mvarId, arity => do let mvarType ← inferMVarType mvarId; isArrowProposition mvarType arity + | .app f _, arity => isProofQuickApp f (arity+1) + | .mdata _ e, arity => isProofQuickApp e arity | .letE _ _ _ b _, arity => isProofQuickApp b arity | .lam _ _ b _, 0 => isProofQuick b | .lam _ _ b _, arity+1 => isProofQuickApp b arity @@ -306,10 +306,10 @@ partial def isProofQuick : Expr → MetaM LBool | .letE _ _ _ b _ => isProofQuick b | .proj .. => return LBool.undef | .forallE .. => return LBool.false - | .mdata _ e _ => isProofQuick e - | .const c lvls _ => do let constType ← inferConstType c lvls; isArrowProposition constType 0 - | .fvar fvarId _ => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType 0 - | .mvar mvarId _ => do let mvarType ← inferMVarType mvarId; isArrowProposition mvarType 0 + | .mdata _ e => isProofQuick e + | .const c lvls => do let constType ← inferConstType c lvls; isArrowProposition constType 0 + | .fvar fvarId => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType 0 + | .mvar mvarId => do let mvarType ← inferMVarType mvarId; isArrowProposition mvarType 0 | .app f .. => isProofQuickApp f 1 end @@ -329,18 +329,18 @@ private partial def isArrowType : Expr → Nat → MetaM LBool | .forallE .., 0 => return LBool.false | .forallE _ _ b _, n+1 => isArrowType b n | .letE _ _ _ b _, n => isArrowType b n - | .mdata _ e _, n => isArrowType e n + | .mdata _ e, n => isArrowType e n | _, _ => return LBool.undef /-- `isTypeQuickApp f n` is an "approximate" predicate which returns `LBool.true` if `f` applied to `n` arguments is a type. -/ private partial def isTypeQuickApp : Expr → Nat → MetaM LBool - | .const c lvls _, arity => do let constType ← inferConstType c lvls; isArrowType constType arity - | .fvar fvarId _, arity => do let fvarType ← inferFVarType fvarId; isArrowType fvarType arity - | .mvar mvarId _, arity => do let mvarType ← inferMVarType mvarId; isArrowType mvarType arity - | .app f _ _, arity => isTypeQuickApp f (arity+1) - | .mdata _ e _, arity => isTypeQuickApp e arity + | .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowType constType arity + | .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowType fvarType arity + | .mvar mvarId, arity => do let mvarType ← inferMVarType mvarId; isArrowType mvarType arity + | .app f _, arity => isTypeQuickApp f (arity+1) + | .mdata _ e, arity => isTypeQuickApp e arity | .letE _ _ _ b _, arity => isTypeQuickApp b arity | .lam .., 0 => return LBool.false | .lam _ _ b _, arity+1 => isTypeQuickApp b arity @@ -357,10 +357,10 @@ partial def isTypeQuick : Expr → MetaM LBool | .letE _ _ _ b _ => isTypeQuick b | .proj .. => return LBool.undef | .forallE .. => return LBool.true - | .mdata _ e _ => isTypeQuick e - | .const c lvls _ => do let constType ← inferConstType c lvls; isArrowType constType 0 - | .fvar fvarId _ => do let fvarType ← inferFVarType fvarId; isArrowType fvarType 0 - | .mvar mvarId _ => do let mvarType ← inferMVarType mvarId; isArrowType mvarType 0 + | .mdata _ e => isTypeQuick e + | .const c lvls => do let constType ← inferConstType c lvls; isArrowType constType 0 + | .fvar fvarId => do let fvarType ← inferFVarType fvarId; isArrowType fvarType 0 + | .mvar mvarId => do let mvarType ← inferMVarType mvarId; isArrowType mvarType 0 | .app f .. => isTypeQuickApp f 1 def isType (e : Expr) : MetaM Bool := do @@ -379,7 +379,7 @@ partial def isTypeFormerType (type : Expr) : MetaM Bool := do match type with | .sort .. => return true | .forallE n d b c => - withLocalDecl' n c.binderInfo d fun fvar => isTypeFormerType (b.instantiate1 fvar) + withLocalDecl' n c d fun fvar => isTypeFormerType (b.instantiate1 fvar) | _ => return false /-- diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 84b7582813..853895d3b7 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -114,7 +114,7 @@ def addDefaultInstance (declName : Name) (prio : Nat := 0) : MetaM Unit := do | some info => forallTelescopeReducing info.type fun _ type => do match type.getAppFn with - | Expr.const className _ _ => + | Expr.const className _ => unless isClass (← getEnv) className do throwError "invalid default instance '{declName}', it has type '({className} ...)', but {className}' is not a type class" setEnv <| defaultInstanceExtension.addEntry (← getEnv) { className := className, instanceName := declName, priority := prio } diff --git a/src/Lean/Meta/KAbstract.lean b/src/Lean/Meta/KAbstract.lean index 38f60e9a63..206183517f 100644 --- a/src/Lean/Meta/KAbstract.lean +++ b/src/Lean/Meta/KAbstract.lean @@ -19,9 +19,9 @@ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : Me let rec visit (e : Expr) (offset : Nat) : StateRefT Nat MetaM Expr := do let visitChildren : Unit → StateRefT Nat MetaM Expr := fun _ => do match e with - | Expr.app f a _ => return e.updateApp! (← visit f offset) (← visit a offset) - | Expr.mdata _ b _ => return e.updateMData! (← visit b offset) - | Expr.proj _ _ b _ => return e.updateProj! (← visit b offset) + | Expr.app f a => return e.updateApp! (← visit f offset) (← visit a offset) + | Expr.mdata _ b => return e.updateMData! (← visit b offset) + | Expr.proj _ _ b => return e.updateProj! (← visit b offset) | Expr.letE _ t v b _ => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1)) | Expr.lam _ d b _ => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1)) | Expr.forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1)) diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean index 2aa77e8c3b..ed9fad00d4 100644 --- a/src/Lean/Meta/Match/Basic.lean +++ b/src/Lean/Meta/Match/Basic.lean @@ -230,8 +230,8 @@ partial def replaceFVarId (fvarId : FVarId) (ex : Example) : Example → Example partial def applyFVarSubst (s : FVarSubst) : Example → Example | var fvarId => match s.get fvarId with - | Expr.fvar fvarId' _ => var fvarId' - | _ => underscore + | Expr.fvar fvarId' => var fvarId' + | _ => underscore | ctor n exs => ctor n $ exs.map (applyFVarSubst s) | arrayLit exs => arrayLit $ exs.map (applyFVarSubst s) | ex => ex @@ -306,8 +306,8 @@ partial def toPattern (e : Expr) : MetaM Pattern := do if let some e := isNamedPattern? e then let p ← toPattern <| e.getArg! 2 match e.getArg! 1, e.getArg! 3 with - | Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h - | _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'" + | Expr.fvar x, Expr.fvar h => return Pattern.as x p h + | _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'" else if isMatchValue e then return Pattern.val e else if e.isFVar then diff --git a/src/Lean/Meta/Match/CaseValues.lean b/src/Lean/Meta/Match/CaseValues.lean index dbd15a7de8..24e70524dc 100644 --- a/src/Lean/Meta/Match/CaseValues.lean +++ b/src/Lean/Meta/Match/CaseValues.lean @@ -87,8 +87,8 @@ def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNameP appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i) let thenMVarId ← hs.foldlM (fun thenMVarId h => match thenSubgoal.subst.get h with - | Expr.fvar fvarId _ => tryClear thenMVarId fvarId - | _ => pure thenMVarId) + | Expr.fvar fvarId => tryClear thenMVarId fvarId + | _ => pure thenMVarId) thenSubgoal.mvarId let subgoals ← if substNewEqs then let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH false thenSubgoal.subst true diff --git a/src/Lean/Meta/Match/MVarRenaming.lean b/src/Lean/Meta/Match/MVarRenaming.lean index 25795dc757..0dc7ee9ca7 100644 --- a/src/Lean/Meta/Match/MVarRenaming.lean +++ b/src/Lean/Meta/Match/MVarRenaming.lean @@ -27,7 +27,7 @@ def MVarRenaming.apply (s : MVarRenaming) (e : Expr) : Expr := if !e.hasMVar then e else if s.map.isEmpty then e else e.replace fun e => match e with - | Expr.mvar mvarId _ => match s.map.find? mvarId with + | Expr.mvar mvarId => match s.map.find? mvarId with | none => e | some newMVarId => mkMVar newMVarId | _ => none diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index c53996e8d8..b2ba02d2c8 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -89,8 +89,8 @@ private def isDone (p : Problem) : Bool := /-- Return true if the next element on the `p.vars` list is a variable. -/ private def isNextVar (p : Problem) : Bool := match p.vars with - | Expr.fvar _ _ :: _ => true - | _ => false + | Expr.fvar _ :: _ => true + | _ => false private def hasAsPattern (p : Problem) : Bool := p.alts.any fun alt => match alt.patterns with @@ -249,12 +249,12 @@ def isAltVar (fvarId : FVarId) : M Bool := do def expandIfVar (e : Expr) : M Expr := do match e with - | Expr.fvar _ _ => return (← get).fvarSubst.apply e - | _ => return e + | Expr.fvar _ => return (← get).fvarSubst.apply e + | _ => return e def occurs (fvarId : FVarId) (v : Expr) : Bool := Option.isSome <| v.find? fun e => match e with - | Expr.fvar fvarId' _ => fvarId == fvarId' + | Expr.fvar fvarId' => fvarId == fvarId' | _=> false def assign (fvarId : FVarId) (v : Expr) : M Bool := do @@ -330,10 +330,10 @@ partial def unify (a : Expr) (b : Expr) : M Bool := do if a != a' || b != b' then unify a' b' else match a, b with - | Expr.fvar aFvarId _, Expr.fvar bFVarId _ => assign aFvarId b <||> assign bFVarId a - | Expr.fvar aFvarId _, b => assign aFvarId b - | a, Expr.fvar bFVarId _ => assign bFVarId a - | Expr.app aFn aArg _, Expr.app bFn bArg _ => unify aFn bFn <&&> unify aArg bArg + | Expr.fvar aFvarId, Expr.fvar bFVarId => assign aFvarId b <||> assign bFVarId a + | Expr.fvar aFvarId, b => assign aFvarId b + | a, Expr.fvar bFVarId => assign bFVarId a + | Expr.app aFn aArg, Expr.app bFn bArg => unify aFn bFn <&&> unify aArg bArg | _, _ => return false end Unify @@ -372,15 +372,15 @@ private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) : let patterns := alt.patterns.map fun p => p.applyFVarSubst subst let rhs := subst.apply alt.rhs let ctorFieldPatterns := ctorFields.toList.map fun ctorField => match subst.get ctorField.fvarId! with - | e@(Expr.fvar fvarId _) => if inLocalDecls newAltDecls fvarId then Pattern.var fvarId else Pattern.inaccessible e - | e => Pattern.inaccessible e + | e@(Expr.fvar fvarId) => if inLocalDecls newAltDecls fvarId then Pattern.var fvarId else Pattern.inaccessible e + | e => Pattern.inaccessible e return some { alt with fvarDecls := newAltDecls, rhs := rhs, patterns := ctorFieldPatterns ++ patterns } private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do let xType ← inferType x let xType ← whnfD xType match xType.getAppFn with - | Expr.const constName _ _ => + | Expr.const constName _ => let cinfo ← getConstInfo constName match cinfo with | ConstantInfo.inductInfo val => return some val @@ -471,8 +471,8 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do let newVars := fields ++ xs let newVars := newVars.map fun x => x.applyFVarSubst subst let subex := Example.ctor subgoal.ctorName <| fields.map fun field => match field with - | Expr.fvar fvarId _ => Example.var fvarId - | _ => Example.underscore -- This case can happen due to dependent elimination + | Expr.fvar fvarId => Example.var fvarId + | _ => Example.underscore -- This case can happen due to dependent elimination let examples := p.examples.map <| Example.replaceFVarId x.fvarId! subex let examples := examples.map <| Example.applyFVarSubst subst let newAlts := p.alts.filter fun alt => match alt.patterns with @@ -625,9 +625,9 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do private def expandNatValuePattern (p : Problem) : Problem := let alts := p.alts.map fun alt => match alt.patterns with - | Pattern.val (Expr.lit (Literal.natVal 0) _) :: ps => { alt with patterns := Pattern.ctor `Nat.zero [] [] [] :: ps } - | Pattern.val (Expr.lit (Literal.natVal (n+1)) _) :: ps => { alt with patterns := Pattern.ctor `Nat.succ [] [] [Pattern.val (mkRawNatLit n)] :: ps } - | _ => alt + | Pattern.val (Expr.lit (Literal.natVal 0)) :: ps => { alt with patterns := Pattern.ctor `Nat.zero [] [] [] :: ps } + | Pattern.val (Expr.lit (Literal.natVal (n+1))) :: ps => { alt with patterns := Pattern.ctor `Nat.succ [] [] [Pattern.val (mkRawNatLit n)] :: ps } + | _ => alt { p with alts := alts } private def traceStep (msg : String) : StateRefT State MetaM Unit := do diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index fb4ed8dfde..698d52c8a4 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -25,7 +25,7 @@ partial def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := do where findFVar? (e : Expr) : MetaM (Option FVarId) := do match e.getAppFn with - | Expr.proj _ _ e _ => findFVar? e + | Expr.proj _ _ e => findFVar? e | f => if !f.isConst then return none diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index 40563bf3dc..7eb67ee06e 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -135,7 +135,7 @@ structure MatcherApp where def matchMatcherApp? [Monad m] [MonadEnv m] (e : Expr) : m (Option MatcherApp) := do match e.getAppFn with - | Expr.const declName declLevels _ => + | Expr.const declName declLevels => match (← getMatcherInfo? declName) with | none => return none | some info => diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean index a1aa8c2513..e3eb148cd2 100644 --- a/src/Lean/Meta/Offset.lean +++ b/src/Lean/Meta/Offset.lean @@ -25,8 +25,8 @@ def isNatProjInst (declName : Name) (numArgs : Nat) : Bool := Evaluate simple `Nat` expressions. Remark: this method assumes the given expression has type `Nat`. -/ partial def evalNat : Expr → OptionT MetaM Nat - | Expr.lit (Literal.natVal n) _ => return n - | Expr.mdata _ e _ => evalNat e + | Expr.lit (Literal.natVal n) => return n + | Expr.mdata _ e => evalNat e | Expr.const `Nat.zero .. => return 0 | e@(Expr.app ..) => visit e | e@(Expr.mvar ..) => visit e @@ -36,7 +36,7 @@ where let f := e.getAppFn match f with | Expr.mvar .. => withInstantiatedMVars e evalNat - | Expr.const c _ _ => + | Expr.const c _ => let nargs := e.getAppNumArgs if c == ``Nat.succ && nargs == 1 then let v ← evalNat (e.getArg! 0) @@ -61,11 +61,11 @@ where /- Quick function for converting `e` into `s + k` s.t. `e` is definitionally equal to `Nat.add s k`. -/ private partial def getOffsetAux : Expr → Bool → OptionT MetaM (Expr × Nat) - | e@(Expr.app _ a _), top => do + | e@(Expr.app _ a), top => do let f := e.getAppFn match f with | Expr.mvar .. => withInstantiatedMVars e (getOffsetAux · top) - | Expr.const c _ _ => + | Expr.const c _ => let nargs := e.getAppNumArgs if c == ``Nat.succ && nargs == 1 then let (s, k) ← getOffsetAux a false @@ -84,11 +84,11 @@ private def getOffset (e : Expr) : OptionT MetaM (Expr × Nat) := getOffsetAux e true private partial def isOffset : Expr → OptionT MetaM (Expr × Nat) - | e@(Expr.app _ _ _) => + | e@(Expr.app _ _) => let f := e.getAppFn match f with | Expr.mvar .. => withInstantiatedMVars e isOffset - | Expr.const c _ _ => + | Expr.const c _ => let nargs := e.getAppNumArgs if (c == ``Nat.succ && nargs == 1) || (c == ``Nat.add && nargs == 2) || (c == ``Add.add && nargs == 4) || (c == ``HAdd.hAdd && nargs == 6) then getOffset e diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean index 66d0a20005..8addf605b5 100644 --- a/src/Lean/Meta/PPGoal.lean +++ b/src/Lean/Meta/PPGoal.lean @@ -89,10 +89,10 @@ where | 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 _ => if (← isMarked fvarId) then unmark fvarId + | Expr.app f a => visit f; visit a + | Expr.mdata _ b => visit b + | Expr.proj _ _ b => visit b + | Expr.fvar fvarId => if (← isMarked fvarId) then unmark fvarId | _ => pure () def fixpointStep : M Unit := do diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 2e7c4163b7..bf790bf899 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -160,9 +160,9 @@ private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndic private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM Level := match motiveResultType with - | Expr.sort u@(Level.zero) _ => pure u - | Expr.sort u@(Level.param _) _ => pure u - | _ => + | Expr.sort u@(Level.zero) => pure u + | Expr.sort u@(Level.param _) => pure u + | _ => throwError "invalid user defined recursor '{declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter" private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : Level) (Ilevels : List Level) : MetaM (List RecursorUnivLevelPos) := do @@ -214,7 +214,7 @@ private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) : let majorType ← inferType major majorType.withApp fun I Iargs => match I with - | Expr.const Iname Ilevels _ => do + | Expr.const Iname Ilevels => do let paramsPos ← getParamsPos declName xs numParams Iargs let indicesPos ← getIndicesPos declName xs majorPos numIndices Iargs let motiveType ← inferType motive diff --git a/src/Lean/Meta/ReduceEval.lean b/src/Lean/Meta/ReduceEval.lean index 9747bc77e4..e6db75a10b 100644 --- a/src/Lean/Meta/ReduceEval.lean +++ b/src/Lean/Meta/ReduceEval.lean @@ -36,12 +36,12 @@ instance [ReduceEval α] : ReduceEval (Option α) where instance : ReduceEval String where reduceEval e := do - let Expr.lit (Literal.strVal s) _ ← whnf e | throwFailedToEval e + let Expr.lit (Literal.strVal s) ← whnf e | throwFailedToEval e pure s private partial def evalName (e : Expr) : MetaM Name := do let e ← whnf e - let Expr.const c _ _ ← pure e.getAppFn | throwFailedToEval e + let Expr.const c _ ← pure e.getAppFn | throwFailedToEval e let nargs := e.getAppNumArgs if c == ``Lean.Name.anonymous && nargs == 0 then pure Name.anonymous else if c == ``Lean.Name.str && nargs == 2 then do diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index b6a8dc9323..fb49e5c731 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -118,15 +118,15 @@ partial def normExpr (e : Expr) : M Expr := do if !e.hasMVar then pure e else match e with - | Expr.const _ us _ => return e.updateConst! (← us.mapM normLevel) - | Expr.sort u _ => return e.updateSort! (← normLevel u) - | Expr.app f a _ => return e.updateApp! (← normExpr f) (← normExpr a) + | Expr.const _ us => return e.updateConst! (← us.mapM normLevel) + | Expr.sort u => return e.updateSort! (← normLevel u) + | Expr.app f a => return e.updateApp! (← normExpr f) (← normExpr a) | Expr.letE _ t v b _ => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b) | Expr.forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b) | Expr.lam _ d b _ => return e.updateLambdaE! (← normExpr d) (← normExpr b) - | Expr.mdata _ b _ => return e.updateMData! (← normExpr b) - | Expr.proj _ _ b _ => return e.updateProj! (← normExpr b) - | Expr.mvar mvarId _ => + | Expr.mdata _ b => return e.updateMData! (← normExpr b) + | Expr.proj _ _ b => return e.updateProj! (← normExpr b) + | Expr.mvar mvarId => if !(← isExprMVarAssignable mvarId) then return e else @@ -201,7 +201,7 @@ def getInstances (type : Expr) : MetaM (Array Expr) := do let result := result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority let erasedInstances ← getErasedInstances let result ← result.filterMapM fun e => match e.val with - | Expr.const constName us _ => + | Expr.const constName us => if erasedInstances.contains constName then return none else @@ -272,13 +272,13 @@ structure SubgoalsResult where private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr) : Array Expr → Nat → List Expr → Expr → Expr → MetaM SubgoalsResult - | args, j, subgoals, instVal, Expr.forallE _ d b c => do + | args, j, subgoals, instVal, Expr.forallE _ d b bi => do let d := d.instantiateRevRange j args.size args let mvarType ← mkForallFVars xs d let mvar ← mkFreshExprMVarAt lctx localInsts mvarType let arg := mkAppN mvar xs let instVal := mkApp instVal arg - let subgoals := if c.binderInfo.isInstImplicit then mvar::subgoals else subgoals + let subgoals := if bi.isInstImplicit then mvar::subgoals else subgoals let args := args.push (mkAppN mvar xs) getSubgoalsAux lctx localInsts xs args j subgoals instVal b | args, j, subgoals, instVal, type => do @@ -308,7 +308,7 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array let instType ← inferType inst let result ← getSubgoalsAux lctx localInsts xs #[] 0 [] inst instType match inst.getAppFn with - | Expr.const constName _ _ => + | Expr.const constName _ => let env ← getEnv if hasInferTCGoalsRLAttribute env constName then return result @@ -644,7 +644,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) : private def preprocessOutParam (type : Expr) : MetaM Expr := forallTelescope type fun xs typeBody => do match typeBody.getAppFn with - | c@(Expr.const constName _ _) => + | c@(Expr.const constName _) => let env ← getEnv if !hasOutParams env constName then return type diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean index 623e3574c2..447a7ecab5 100644 --- a/src/Lean/Meta/Tactic/AC/Main.lean +++ b/src/Lean/Meta/Tactic/AC/Main.lean @@ -57,8 +57,8 @@ inductive PreExpr | op (lhs rhs : PreExpr) | var (e : Expr) -@[matchPattern] def bin {x₁ x₂} (op l r : Expr) := - Expr.app (Expr.app op l x₁) r x₂ +@[matchPattern] def bin (op l r : Expr) := + Expr.app (Expr.app op l) r def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do let (preExpr, vars) ← diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean index e9f55c113c..c4f3928078 100644 --- a/src/Lean/Meta/Tactic/Cases.lean +++ b/src/Lean/Meta/Tactic/Cases.lean @@ -181,7 +181,7 @@ private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array Cases s₂.mapM fun s => do indicesFVarIds.foldlM (init := s) fun s indexFVarId => match s.subst.get indexFVarId with - | Expr.fvar indexFVarId' _ => + | Expr.fvar indexFVarId' => (do let mvarId ← clear s.mvarId indexFVarId'; pure { s with mvarId := mvarId, subst := s.subst.erase indexFVarId }) <|> (pure s) diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean index e1ece88bfd..c3f7217321 100644 --- a/src/Lean/Meta/Tactic/ElimInfo.lean +++ b/src/Lean/Meta/Tactic/ElimInfo.lean @@ -67,9 +67,9 @@ partial def addImplicitTargets (elimInfo : ElimInfo) (targets : Array Expr) : Me where collect (type : Expr) (argIdx targetIdx : Nat) (targets' : Array Expr) : MetaM (Array Expr) := do match (← whnfD type) with - | Expr.forallE _ d b c => + | Expr.forallE _ d b bi => if elimInfo.targetsPos.contains argIdx then - if c.binderInfo.isExplicit then + if bi.isExplicit then unless targetIdx < targets.size do throwError "insufficient number of targets for '{elimInfo.name}'" let target := targets[targetIdx]! diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean index aea5310ead..9293126dd2 100644 --- a/src/Lean/Meta/Tactic/FVarSubst.lean +++ b/src/Lean/Meta/Tactic/FVarSubst.lean @@ -52,7 +52,7 @@ def apply (s : FVarSubst) (e : Expr) : Expr := if s.map.isEmpty then e else if !e.hasFVar then e else e.replace fun e => match e with - | Expr.fvar fvarId _ => match s.map.find? fvarId with + | Expr.fvar fvarId => match s.map.find? fvarId with | none => e | some v => v | _ => none diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean index 8afd3057c3..ff31f58cf7 100644 --- a/src/Lean/Meta/Tactic/Induction.lean +++ b/src/Lean/Meta/Tactic/Induction.lean @@ -14,7 +14,7 @@ import Lean.Meta.Tactic.FVarSubst namespace Lean.Meta private partial def getTargetArity : Expr → Nat - | Expr.mdata _ b _ => getTargetArity b + | Expr.mdata _ b => getTargetArity b | Expr.forallE _ _ b _ => getTargetArity b + 1 | e => if e.isHeadBetaTarget then getTargetArity e.headBeta else 0 @@ -79,7 +79,7 @@ private partial def finalize | Expr.forallE n d _ c => let d := d.headBeta -- Remark is givenNames is not empty, then user provided explicit alternatives for each minor premise - if c.binderInfo.isInstImplicit && givenNames.isEmpty then + if c.isInstImplicit && givenNames.isEmpty then match (← synthInstance? d) with | some inst => let recursor := mkApp recursor inst @@ -181,7 +181,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi let some majorType ← whnfUntil majorLocalDecl.type recursorInfo.typeName | throwUnexpectedMajorType mvarId majorLocalDecl.type majorType.withApp fun majorTypeFn majorTypeArgs => do match majorTypeFn with - | Expr.const _ majorTypeFnLevels _ => do + | Expr.const _ majorTypeFnLevels => do let majorTypeFnLevels := majorTypeFnLevels.toArray let (recursorLevels, foundTargetLevel) ← recursorInfo.univLevelPos.foldlM (init := (#[], false)) fun (recursorLevels, foundTargetLevel) (univPos : RecursorUnivLevelPos) => do diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean index 7085dcb617..1ebbee1c9f 100644 --- a/src/Lean/Meta/Tactic/Intro.lean +++ b/src/Lean/Meta/Tactic/Intro.lean @@ -38,8 +38,8 @@ namespace Lean.Meta let type := type.instantiateRevRange j fvars.size fvars let type := type.headBeta let fvarId ← mkFreshFVarId - let (n, s) ← mkName lctx n c.binderInfo.isExplicit s - let lctx := lctx.mkLocalDecl fvarId n type c.binderInfo + let (n, s) ← mkName lctx n c.isExplicit s + let lctx := lctx.mkLocalDecl fvarId n type c let fvar := mkFVar fvarId let fvars := fvars.push fvar loop i lctx fvars j s body @@ -123,7 +123,7 @@ abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) := private def getIntrosSize : Expr → Nat | Expr.forallE _ _ b _ => getIntrosSize b + 1 | Expr.letE _ _ _ b _ => getIntrosSize b + 1 - | Expr.mdata _ b _ => getIntrosSize b + | Expr.mdata _ b => getIntrosSize b | _ => 0 def intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean index 28ff61ff98..250e3aa771 100644 --- a/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean +++ b/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean @@ -73,12 +73,12 @@ def addAsVar (e : Expr) : M LinearExpr := do partial def toLinearExpr (e : Expr) : M LinearExpr := do match e with - | Expr.lit (Literal.natVal n) _ => return num n - | Expr.mdata _ e _ => toLinearExpr e - | Expr.const ``Nat.zero .. => return num 0 - | Expr.app .. => visit e - | Expr.mvar .. => visit e - | _ => addAsVar e + | Expr.lit (Literal.natVal n) => return num n + | Expr.mdata _ e => toLinearExpr e + | Expr.const ``Nat.zero .. => return num 0 + | Expr.app .. => visit e + | Expr.mvar .. => visit e + | _ => addAsVar e where visit (e : Expr) : M LinearExpr := do let f := e.getAppFn diff --git a/src/Lean/Meta/Tactic/Replace.lean b/src/Lean/Meta/Tactic/Replace.lean index 0b779b7938..fef76e7e60 100644 --- a/src/Lean/Meta/Tactic/Replace.lean +++ b/src/Lean/Meta/Tactic/Replace.lean @@ -111,7 +111,7 @@ def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkD let (_, mvarId) ← introNP mvarId numReverted pure mvarId match target with - | Expr.forallE n d b c => do check d; finalize (mkForall n c.binderInfo typeNew b) + | Expr.forallE n d b c => do check d; finalize (mkForall n c typeNew b) | Expr.letE n t v b _ => do check t; finalize (mkLet n typeNew v b) | _ => throwTacticEx `changeHypothesis mvarId "unexpected auxiliary target" diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index ba3c0a202a..ae1be6a3f7 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -199,7 +199,7 @@ partial def lambdaTelescopeDSimp (e : Expr) (k : Array Expr → Expr → M α) : where go (xs : Array Expr) (e : Expr) : M α := do match e with - | .lam n d b c => withLocalDecl n c.binderInfo (← dsimp d) fun x => go (xs.push x) (b.instantiate1 x) + | .lam n d b c => withLocalDecl n c (← dsimp d) fun x => go (xs.push x) (b.instantiate1 x) | e => k xs e inductive SimpLetCase where @@ -283,7 +283,7 @@ where simpStep (e : Expr) : M Result := do match e with - | Expr.mdata m e _ => let r ← simp e; return { r with expr := mkMData m r.expr } + | Expr.mdata m e => let r ← simp e; return { r with expr := mkMData m r.expr } | Expr.proj .. => simpProj e | Expr.app .. => simpApp e | Expr.lam .. => simpLambda e diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index c053cf80b3..a4922676a2 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -141,15 +141,15 @@ def SimpTheorems.erase [Monad m] [MonadError m] (d : SimpTheorems) (declName : N return d.eraseCore declName private partial def isPerm : Expr → Expr → MetaM Bool - | Expr.app f₁ a₁ _, Expr.app f₂ a₂ _ => isPerm f₁ f₂ <&&> isPerm a₁ a₂ - | Expr.mdata _ s _, t => isPerm s t - | s, Expr.mdata _ t _ => isPerm s t + | Expr.app f₁ a₁, Expr.app f₂ a₂ => isPerm f₁ f₂ <&&> isPerm a₁ a₂ + | Expr.mdata _ s, t => isPerm s t + | s, Expr.mdata _ t => isPerm s t | s@(Expr.mvar ..), t@(Expr.mvar ..) => isDefEq s t | Expr.forallE n₁ d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x) | Expr.lam n₁ d₁ b₁ _, Expr.lam _ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x) | Expr.letE n₁ t₁ v₁ b₁ _, Expr.letE _ t₂ v₂ b₂ _ => isPerm t₁ t₂ <&&> isPerm v₁ v₂ <&&> withLetDecl n₁ t₁ v₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x) - | Expr.proj _ i₁ b₁ _, Expr.proj _ i₂ b₂ _ => pure (i₁ == i₂) <&&> isPerm b₁ b₂ + | Expr.proj _ i₁ b₁, Expr.proj _ i₂ b₂ => pure (i₁ == i₂) <&&> isPerm b₁ b₂ | s, t => return s == t private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index d0249300ef..64b5b923e5 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -187,7 +187,7 @@ private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs : let mut mvarId := mvarId let mut fvarSubst := fvarSubst for fvarId in discrEqs do - if let .fvar fvarId _ := fvarSubst.apply (mkFVar fvarId) then + if let .fvar fvarId := fvarSubst.apply (mkFVar fvarId) then let (fvarId, mvarId') ← heqToEq mvarId fvarId match (← substCore? mvarId' fvarId (symm := false) fvarSubst) with | some (fvarSubst', mvarId') => mvarId := mvarId'; fvarSubst := fvarSubst' diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean index 8a593d18a9..11835b7b47 100644 --- a/src/Lean/Meta/Tactic/Subst.lean +++ b/src/Lean/Meta/Tactic/Subst.lean @@ -26,7 +26,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst : let a ← instantiateMVars <| if symm then rhs else lhs let b ← instantiateMVars <| if symm then lhs else rhs match a with - | Expr.fvar aFVarId _ => do + | Expr.fvar aFVarId => do let aFVarIdOriginal := aFVarId trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId.name}) with {b}" if (← exprDependsOn b aFVarId) then diff --git a/src/Lean/Meta/Tactic/UnifyEq.lean b/src/Lean/Meta/Tactic/UnifyEq.lean index a725c7abd6..7e6234b294 100644 --- a/src/Lean/Meta/Tactic/UnifyEq.lean +++ b/src/Lean/Meta/Tactic/UnifyEq.lean @@ -87,7 +87,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {}) let a ← instantiateMVars a let b ← instantiateMVars b match a, b with - | Expr.fvar aFVarId _, Expr.fvar bFVarId _ => + | Expr.fvar aFVarId, Expr.fvar bFVarId => /- x = y -/ let aDecl ← getLocalDecl aFVarId let bDecl ← getLocalDecl bFVarId diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean index b9cb8cd95b..b916c67978 100644 --- a/src/Lean/Meta/Tactic/Util.lean +++ b/src/Lean/Meta/Tactic/Util.lean @@ -86,7 +86,7 @@ where let e ← instantiateMVars e let visit : StateRefT FVarIdHashSet MetaM FVarIdHashSet := do e.forEach fun - | Expr.fvar fvarId _ => modify fun s => s.erase fvarId + | Expr.fvar fvarId => modify fun s => s.erase fvarId | _ => pure () get visit |>.run' candidates diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean index d5dc31eb70..dc9c7ca8c3 100644 --- a/src/Lean/Meta/Transform.lean +++ b/src/Lean/Meta/Transform.lean @@ -46,8 +46,8 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m] | Expr.lam _ d b _ => visitPost (e.updateLambdaE! (← visit d) (← visit b)) | Expr.letE _ t v b _ => visitPost (e.updateLet! (← visit t) (← visit v) (← visit b)) | Expr.app .. => e.withApp fun f args => do visitPost (mkAppN (← visit f) (← args.mapM visit)) - | Expr.mdata _ b _ => visitPost (e.updateMData! (← visit b)) - | Expr.proj _ _ b _ => visitPost (e.updateProj! (← visit b)) + | Expr.mdata _ b => visitPost (e.updateMData! (← visit b)) + | Expr.proj _ _ b => visitPost (e.updateProj! (← visit b)) | _ => visitPost e visit input |>.run @@ -78,13 +78,13 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] let rec visitLambda (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do match e with | Expr.lam n d b c => - withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x => + withLocalDecl n c (← visit (d.instantiateRev fvars)) fun x => visitLambda (fvars.push x) b | e => visitPost (← mkLambdaFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars))) let rec visitForall (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do match e with | Expr.forallE n d b c => - withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x => + withLocalDecl n c (← visit (d.instantiateRev fvars)) fun x => visitForall (fvars.push x) b | e => visitPost (← mkForallFVars (usedLetOnly := usedLetOnly) fvars (← visit (e.instantiateRev fvars))) let rec visitLet (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do @@ -103,15 +103,15 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] | Expr.lam .. => visitLambda #[] e | Expr.letE .. => visitLet #[] e | Expr.app .. => visitApp e - | Expr.mdata _ b _ => visitPost (e.updateMData! (← visit b)) - | Expr.proj _ _ b _ => visitPost (e.updateProj! (← visit b)) + | Expr.mdata _ b => visitPost (e.updateMData! (← visit b)) + | Expr.proj _ _ b => visitPost (e.updateProj! (← visit b)) | _ => visitPost e visit input |>.run def zetaReduce (e : Expr) : MetaM Expr := do let pre (e : Expr) : MetaM TransformStep := do match e with - | Expr.fvar fvarId _ => + | Expr.fvar fvarId => match (← getLCtx).find? fvarId with | none => return TransformStep.done e | some localDecl => diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 66c526c19e..cdeb894d3c 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -63,7 +63,7 @@ def isAuxDef (constName : Name) : MetaM Bool := do @[inline] private def matchConstAux {α} (e : Expr) (failK : Unit → MetaM α) (k : ConstantInfo → List Level → MetaM α) : MetaM α := match e with - | Expr.const name lvls _ => do + | Expr.const name lvls => do let (some cinfo) ← getConst? name | failK () k cinfo lvls | _ => failK () @@ -78,24 +78,24 @@ private def getFirstCtor (d : Name) : MetaM (Option Name) := do private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) := do match type.getAppFn with - | Expr.const d lvls _ => + | Expr.const d lvls => let (some ctor) ← getFirstCtor d | pure none return mkAppN (mkConst ctor lvls) (type.getAppArgs.shrink nparams) | _ => return none def toCtorIfLit : Expr → Expr - | Expr.lit (Literal.natVal v) _ => + | Expr.lit (Literal.natVal v) => if v == 0 then mkConst `Nat.zero else mkApp (mkConst `Nat.succ) (mkRawNatLit (v-1)) - | Expr.lit (Literal.strVal v) _ => + | Expr.lit (Literal.strVal v) => mkApp (mkConst `String.mk) (toExpr v.toList) | e => e private def getRecRuleFor (recVal : RecursorVal) (major : Expr) : Option RecursorRule := match major.getAppFn with - | Expr.const fn _ _ => recVal.rules.find? fun r => r.ctor == fn - | _ => none + | Expr.const fn _ => recVal.rules.find? fun r => r.ctor == fn + | _ => none private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do let majorType ← inferType major @@ -152,7 +152,7 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr if !majorTypeI.isConstOf inductName then return major match majorType.getAppFn with - | Expr.const d us _ => + | Expr.const d us => if (← whnfD (← inferType majorType)) == mkSort levelZero then return major -- We do not perform eta for propositions, see implementation in the kernel else @@ -206,7 +206,7 @@ private def reduceQuotRec (recVal : QuotVal) (recLvls : List Level) (recArgs : let major := recArgs.get ⟨majorPos, h⟩ let major ← whnf major match major with - | Expr.app (Expr.app (Expr.app (Expr.const majorFn _ _) _ _) _ _) majorArg _ => do + | Expr.app (Expr.app (Expr.app (Expr.const majorFn _) _) _) majorArg => do let some (ConstantInfo.quotInfo { kind := QuotKind.ctor, .. }) ← getConstNoEx? majorFn | failK () let f := recArgs[argPos]! let r := mkApp f majorArg @@ -254,24 +254,24 @@ mutual /-- Return `some (Expr.mvar mvarId)` if metavariable `mvarId` is blocking reduction. -/ partial def getStuckMVar? (e : Expr) : MetaM (Option MVarId) := do match e with - | Expr.mdata _ e _ => getStuckMVar? e - | Expr.proj _ _ e _ => getStuckMVar? (← whnf e) + | Expr.mdata _ e => getStuckMVar? e + | Expr.proj _ _ e => getStuckMVar? (← whnf e) | Expr.mvar .. => do let e ← instantiateMVars e match e with - | Expr.mvar mvarId _ => pure (some mvarId) + | Expr.mvar mvarId => pure (some mvarId) | _ => getStuckMVar? e | Expr.app f .. => let f := f.getAppFn match f with - | Expr.mvar mvarId _ => return some mvarId - | Expr.const fName _ _ => + | Expr.mvar mvarId => return some mvarId + | Expr.const fName _ => let cinfo? ← getConstNoEx? fName match cinfo? with | some $ ConstantInfo.recInfo recVal => isRecStuck? recVal e.getAppArgs | some $ ConstantInfo.quotInfo recVal => isQuotRecStuck? recVal e.getAppArgs | _ => return none - | Expr.proj _ _ e _ => getStuckMVar? (← whnf e) + | Expr.proj _ _ e => getStuckMVar? (← whnf e) | _ => return none | _ => return none end @@ -292,8 +292,8 @@ end | Expr.const .. => k e | Expr.app .. => k e | Expr.proj .. => k e - | Expr.mdata _ e _ => whnfEasyCases e k - | Expr.fvar fvarId _ => + | Expr.mdata _ e => whnfEasyCases e k + | Expr.fvar fvarId => let decl ← getLocalDecl fvarId match decl with | LocalDecl.cdecl .. => return e @@ -305,7 +305,7 @@ end if cfg.trackZeta then modify fun s => { s with zetaFVarIds := s.zetaFVarIds.insert fvarId } whnfEasyCases v k - | Expr.mvar mvarId _ => + | Expr.mvar mvarId => match (← getExprMVarAssignment? mvarId) with | some v => whnfEasyCases v k | none => return e @@ -400,7 +400,7 @@ private def whnfMatcher (e : Expr) : MetaM Expr := do def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do match e.getAppFn with - | Expr.const declName declLevels _ => + | Expr.const declName declLevels => let some info ← getMatcherInfo? declName | return ReduceMatcherResult.notMatcher let args := e.getAppArgs @@ -441,8 +441,8 @@ def project? (e : Expr) (i : Nat) : MetaM (Option Expr) := do /-- Reduce kernel projection `Expr.proj ..` expression. -/ def reduceProj? (e : Expr) : MetaM (Option Expr) := do match e with - | Expr.proj _ i c _ => project? c i - | _ => return none + | Expr.proj _ i c => project? c i + | _ => return none /-- Auxiliary method for reducing terms of the form `?m t_1 ... t_n` where `?m` is delayed assigned. @@ -511,7 +511,7 @@ where else return e | _ => return e - | Expr.proj _ i c _ => + | Expr.proj _ i c => let c ← if deltaAtProj then whnf c else whnfCore c match (← projectCore? c i) with | some e => go e @@ -556,8 +556,8 @@ where | Expr.letE n t v b _ => withLetDecl n t (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x)) | Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← go b) | Expr.app f a .. => return mkApp (← go f) (← go a) - | Expr.proj _ _ s _ => return e.updateProj! (← go s) - | Expr.mdata _ b _ => + | Expr.proj _ _ s => return e.updateProj! (← go s) + | Expr.mdata _ b => if let some m := smartUnfoldingMatch? e then goMatch m else @@ -613,7 +613,7 @@ mutual /-- Unfold definition using "smart unfolding" if possible. -/ partial def unfoldDefinition? (e : Expr) : MetaM (Option Expr) := match e with - | Expr.app f _ _ => + | Expr.app f _ => matchConstAux f.getAppFn (fun _ => unfoldProjInstWhenIntances? e) fun fInfo fLvls => do if fInfo.levelParams.length != fLvls.length then return none @@ -681,7 +681,7 @@ mutual unfoldDefault () else unfoldDefault () - | Expr.const declName lvls _ => do + | Expr.const declName lvls => do if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then return none else @@ -737,7 +737,7 @@ unsafe def reduceNatNativeUnsafe (constName : Name) : MetaM Nat := evalConstChec def reduceNative? (e : Expr) : MetaM (Option Expr) := match e with - | Expr.app (Expr.const fName _ _) (Expr.const argName _ _) _ => + | Expr.app (Expr.const fName _) (Expr.const argName _) => if fName == ``Lean.reduceBool then do return toExpr (← reduceBoolNative argName) else if fName == ``Lean.reduceNat then do @@ -750,9 +750,9 @@ def reduceNative? (e : Expr) : MetaM (Option Expr) := @[inline] def withNatValue {α} (a : Expr) (k : Nat → MetaM (Option α)) : MetaM (Option α) := do let a ← whnf a match a with - | Expr.const `Nat.zero _ _ => k 0 - | Expr.lit (Literal.natVal v) _ => k v - | _ => return none + | Expr.const `Nat.zero _ => k 0 + | Expr.lit (Literal.natVal v) => k v + | _ => return none def reduceUnaryNatOp (f : Nat → Nat) (a : Expr) : MetaM (Option Expr) := withNatValue a fun a => @@ -773,12 +773,12 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) := if e.hasFVar || e.hasMVar then return none else match e with - | Expr.app (Expr.const fn _ _) a _ => + | Expr.app (Expr.const fn _) a => if fn == ``Nat.succ then reduceUnaryNatOp Nat.succ a else return none - | Expr.app (Expr.app (Expr.const fn _ _) a1 _) a2 _ => + | Expr.app (Expr.app (Expr.const fn _) a1) a2 => if fn == ``Nat.add then reduceBinNatOp Nat.add a1 a2 else if fn == ``Nat.sub then reduceBinNatOp Nat.sub a1 a2 else if fn == ``Nat.mul then reduceBinNatOp Nat.mul a1 a2 diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 53b52d4c66..d32ea9e633 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -374,18 +374,18 @@ def hasAssignedLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool /-- Return `true` iff expression contains assigned (level/expr) metavariables or delayed assigned mvars -/ def hasAssignedMVar [Monad m] [MonadMCtx m] : Expr → m Bool - | Expr.const _ lvls _ => lvls.anyM hasAssignedLevelMVar - | Expr.sort lvl _ => hasAssignedLevelMVar lvl - | Expr.app f a _ => (pure f.hasMVar <&&> hasAssignedMVar f) <||> (pure a.hasMVar <&&> hasAssignedMVar a) + | Expr.const _ lvls => lvls.anyM hasAssignedLevelMVar + | Expr.sort lvl => hasAssignedLevelMVar lvl + | Expr.app f a => (pure f.hasMVar <&&> hasAssignedMVar f) <||> (pure a.hasMVar <&&> hasAssignedMVar a) | Expr.letE _ t v b _ => (pure t.hasMVar <&&> hasAssignedMVar t) <||> (pure v.hasMVar <&&> hasAssignedMVar v) <||> (pure b.hasMVar <&&> hasAssignedMVar b) | Expr.forallE _ d b _ => (pure d.hasMVar <&&> hasAssignedMVar d) <||> (pure b.hasMVar <&&> hasAssignedMVar b) | Expr.lam _ d b _ => (pure d.hasMVar <&&> hasAssignedMVar d) <||> (pure b.hasMVar <&&> hasAssignedMVar b) - | Expr.fvar _ _ => return false - | Expr.bvar _ _ => return false - | Expr.lit _ _ => return false - | Expr.mdata _ e _ => pure e.hasMVar <&&> hasAssignedMVar e - | Expr.proj _ _ e _ => pure e.hasMVar <&&> hasAssignedMVar e - | Expr.mvar mvarId _ => isExprMVarAssigned mvarId <||> isMVarDelayedAssigned mvarId + | Expr.fvar _ => return false + | Expr.bvar _ => return false + | Expr.lit _ => return false + | Expr.mdata _ e => pure e.hasMVar <&&> hasAssignedMVar e + | Expr.proj _ _ e => pure e.hasMVar <&&> hasAssignedMVar e + | Expr.mvar mvarId => isExprMVarAssigned mvarId <||> isMVarDelayedAssigned mvarId /-- Return true iff the given level contains a metavariable that can be assigned. -/ def hasAssignableLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool @@ -398,18 +398,18 @@ def hasAssignableLevelMVar [Monad m] [MonadMCtx m] : Level → m Bool /-- Return `true` iff expression contains a metavariable that can be assigned. -/ def hasAssignableMVar [Monad m] [MonadMCtx m] : Expr → m Bool - | Expr.const _ lvls _ => lvls.anyM hasAssignableLevelMVar - | Expr.sort lvl _ => hasAssignableLevelMVar lvl - | Expr.app f a _ => (pure f.hasMVar <&&> hasAssignableMVar f) <||> (pure a.hasMVar <&&> hasAssignableMVar a) + | Expr.const _ lvls => lvls.anyM hasAssignableLevelMVar + | Expr.sort lvl => hasAssignableLevelMVar lvl + | Expr.app f a => (pure f.hasMVar <&&> hasAssignableMVar f) <||> (pure a.hasMVar <&&> hasAssignableMVar a) | Expr.letE _ t v b _ => (pure t.hasMVar <&&> hasAssignableMVar t) <||> (pure v.hasMVar <&&> hasAssignableMVar v) <||> (pure b.hasMVar <&&> hasAssignableMVar b) | Expr.forallE _ d b _ => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b) | Expr.lam _ d b _ => (pure d.hasMVar <&&> hasAssignableMVar d) <||> (pure b.hasMVar <&&> hasAssignableMVar b) - | Expr.fvar _ _ => return false - | Expr.bvar _ _ => return false - | Expr.lit _ _ => return false - | Expr.mdata _ e _ => pure e.hasMVar <&&> hasAssignableMVar e - | Expr.proj _ _ e _ => pure e.hasMVar <&&> hasAssignableMVar e - | Expr.mvar mvarId _ => isExprMVarAssignable mvarId + | Expr.fvar _ => return false + | Expr.bvar _ => return false + | Expr.lit _ => return false + | Expr.mdata _ e => pure e.hasMVar <&&> hasAssignableMVar e + | Expr.proj _ _ e => pure e.hasMVar <&&> hasAssignableMVar e + | Expr.mvar mvarId => isExprMVarAssignable mvarId /-- Add `mvarId := u` to the universe metavariable assignment. @@ -464,13 +464,13 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi if !e.hasMVar then pure e else checkCache { val := e : ExprStructEq } fun _ => do match e with - | Expr.proj _ _ s _ => return e.updateProj! (← instantiateExprMVars s) + | Expr.proj _ _ s => return e.updateProj! (← instantiateExprMVars s) | Expr.forallE _ d b _ => return e.updateForallE! (← instantiateExprMVars d) (← instantiateExprMVars b) | Expr.lam _ d b _ => return e.updateLambdaE! (← instantiateExprMVars d) (← instantiateExprMVars b) | Expr.letE _ t v b _ => return e.updateLet! (← instantiateExprMVars t) (← instantiateExprMVars v) (← instantiateExprMVars b) - | Expr.const _ lvls _ => return e.updateConst! (← lvls.mapM instantiateLevelMVars) - | Expr.sort lvl _ => return e.updateSort! (← instantiateLevelMVars lvl) - | Expr.mdata _ b _ => return e.updateMData! (← instantiateExprMVars b) + | Expr.const _ lvls => return e.updateConst! (← lvls.mapM instantiateLevelMVars) + | Expr.sort lvl => return e.updateSort! (← instantiateLevelMVars lvl) + | Expr.mdata _ b => return e.updateMData! (← instantiateExprMVars b) | Expr.app .. => e.withApp fun f args => do let instArgs (f : Expr) : MonadCacheT ExprStructEq Expr m Expr := do let args ← args.mapM instantiateExprMVars @@ -484,7 +484,7 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi else instArgs f match f with - | Expr.mvar mvarId _ => + | Expr.mvar mvarId => match (← getDelayedMVarAssignment? mvarId) with | none => instApp | some { fvars, mvarIdPending } => @@ -521,7 +521,7 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi let result := mkAppRange result fvars.size args.size args pure result | _ => instApp - | e@(Expr.mvar mvarId _) => checkCache { val := e : ExprStructEq } fun _ => do + | e@(Expr.mvar mvarId) => checkCache { val := e : ExprStructEq } fun _ => do match (← getExprMVarAssignment? mvarId) with | some newE => do let newE' ← instantiateExprMVars newE @@ -603,11 +603,11 @@ private def shouldVisit (e : Expr) : M Bool := do | Expr.app f a .. => visitApp f <||> visit a | e => visit e, visitMain : Expr → M Bool - | Expr.proj _ _ s _ => visit s + | Expr.proj _ _ s => visit s | 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.mdata _ b _ => visit b + | Expr.mdata _ b => visit b | e@(Expr.app ..) => do let f := e.getAppFn if f.isMVar then @@ -620,7 +620,7 @@ private def shouldVisit (e : Expr) : M Bool := do visitApp e else visitApp e - | Expr.mvar mvarId _ => do + | Expr.mvar mvarId => do match (← getExprMVarAssignment? mvarId) with | some a => visit a | none => @@ -629,7 +629,7 @@ private def shouldVisit (e : Expr) : M Bool := do else let lctx := (← getMCtx).getDecl mvarId |>.lctx return lctx.any fun decl => pf decl.fvarId - | Expr.fvar fvarId _ => return pf fvarId + | Expr.fvar fvarId => return pf fvarId | _ => pure false visit e @@ -958,13 +958,13 @@ mutual private partial def elim (xs : Array Expr) (e : Expr) : M Expr := match e with - | Expr.proj _ _ s _ => return e.updateProj! (← visit xs s) + | Expr.proj _ _ s => return e.updateProj! (← visit xs s) | Expr.forallE _ d b _ => return e.updateForallE! (← visit xs d) (← visit xs b) | Expr.lam _ d b _ => return e.updateLambdaE! (← visit xs d) (← visit xs b) | Expr.letE _ t v b _ => return e.updateLet! (← visit xs t) (← visit xs v) (← visit xs b) - | Expr.mdata _ b _ => return e.updateMData! (← visit xs b) + | Expr.mdata _ b => return e.updateMData! (← visit xs b) | Expr.app .. => e.withApp fun f args => elimApp xs f args - | Expr.mvar _ _ => elimApp xs e #[] + | Expr.mvar _ => elimApp xs e #[] | e => return e private partial def mkAuxMVarType (lctx : LocalContext) (xs : Array Expr) (kind : MetavarKind) (e : Expr) : M Expr := do @@ -1053,7 +1053,7 @@ mutual private partial def elimApp (xs : Array Expr) (f : Expr) (args : Array Expr) : M Expr := do match f with - | Expr.mvar mvarId _ => + | Expr.mvar mvarId => match (← getExprMVarAssignment? mvarId) with | some newF => if newF.isLambda then @@ -1164,9 +1164,9 @@ def mkBinding (isLambda : Bool) (xs : Array Expr) (e : Expr) (usedOnly : Bool := - All locals in `e` are declared in `lctx` - All metavariables `?m` in `e` have a local context which is a subprefix of `lctx` or are assigned, and the assignment is well-formed. -/ partial def isWellFormed [Monad m] [MonadMCtx m] (lctx : LocalContext) : Expr → m Bool - | Expr.mdata _ e _ => isWellFormed lctx e - | Expr.proj _ _ e _ => isWellFormed lctx e - | e@(Expr.app f a _) => pure (!e.hasExprMVar && !e.hasFVar) <||> (isWellFormed lctx f <&&> isWellFormed lctx a) + | Expr.mdata _ e => isWellFormed lctx e + | Expr.proj _ _ e => isWellFormed lctx e + | e@(Expr.app f a) => pure (!e.hasExprMVar && !e.hasFVar) <||> (isWellFormed lctx f <&&> isWellFormed lctx a) | e@(Expr.lam _ d b _) => pure (!e.hasExprMVar && !e.hasFVar) <||> (isWellFormed lctx d <&&> isWellFormed lctx b) | e@(Expr.forallE _ d b _) => pure (!e.hasExprMVar && !e.hasFVar) <||> (isWellFormed lctx d <&&> isWellFormed lctx b) | e@(Expr.letE _ t v b _) => pure (!e.hasExprMVar && !e.hasFVar) <||> (isWellFormed lctx t <&&> isWellFormed lctx v <&&> isWellFormed lctx b) @@ -1174,14 +1174,14 @@ partial def isWellFormed [Monad m] [MonadMCtx m] (lctx : LocalContext) : Expr | Expr.bvar .. => return true | Expr.sort .. => return true | Expr.lit .. => return true - | Expr.mvar mvarId _ => do + | Expr.mvar mvarId => do let mvarDecl := (← getMCtx).getDecl mvarId; if mvarDecl.lctx.isSubPrefixOf lctx then return true else match (← getExprMVarAssignment? mvarId) with | none => return false | some v => isWellFormed lctx v - | Expr.fvar fvarId _ => return lctx.contains fvarId + | Expr.fvar fvarId => return lctx.contains fvarId namespace LevelMVarToParam @@ -1242,14 +1242,14 @@ partial def main (e : Expr) : M Expr := else checkCache { val := e : ExprStructEq } fun _ => do match e with - | Expr.proj _ _ s _ => return e.updateProj! (← main s) + | Expr.proj _ _ s => return e.updateProj! (← main s) | Expr.forallE _ d b _ => return e.updateForallE! (← main d) (← main b) | Expr.lam _ d b _ => return e.updateLambdaE! (← main d) (← main b) | Expr.letE _ t v b _ => return e.updateLet! (← main t) (← main v) (← main b) | Expr.app .. => e.withApp fun f args => visitApp f args - | Expr.mdata _ b _ => return e.updateMData! (← main b) - | Expr.const _ us _ => return e.updateConst! (← us.mapM visitLevel) - | Expr.sort u _ => return e.updateSort! (← visitLevel u) + | Expr.mdata _ b => return e.updateMData! (← main b) + | Expr.const _ us => return e.updateConst! (← us.mapM visitLevel) + | Expr.sort u => return e.updateSort! (← visitLevel u) | Expr.mvar .. => visitApp e #[] | e => return e where diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 05e77eea11..7837c6ec34 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -52,7 +52,7 @@ def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool := @[inline] def matchConst [Monad m] [MonadEnv m] (e : Expr) (failK : Unit → m α) (k : ConstantInfo → List Level → m α) : m α := do match e with - | Expr.const constName us _ => do + | Expr.const constName us => do match (← getEnv).find? constName with | some cinfo => k cinfo us | none => failK () diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 3d0e7e9d78..9daeccd190 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -250,17 +250,17 @@ unsafe def mkParserOfConstantUnsafe (constName : Name) (compileParserDescr : Par | none => throw ↑s!"unknown constant '{constName}'" | some info => match info.type with - | Expr.const `Lean.Parser.TrailingParser _ _ => + | Expr.const `Lean.Parser.TrailingParser _ => let p ← IO.ofExcept $ env.evalConst Parser opts constName pure ⟨false, p⟩ - | Expr.const `Lean.Parser.Parser _ _ => + | Expr.const `Lean.Parser.Parser _ => let p ← IO.ofExcept $ env.evalConst Parser opts constName pure ⟨true, p⟩ - | Expr.const `Lean.ParserDescr _ _ => + | Expr.const `Lean.ParserDescr _ => let d ← IO.ofExcept $ env.evalConst ParserDescr opts constName let p ← compileParserDescr d pure ⟨true, p⟩ - | Expr.const `Lean.TrailingParserDescr _ _ => + | Expr.const `Lean.TrailingParserDescr _ => let d ← IO.ofExcept $ env.evalConst TrailingParserDescr opts constName let p ← compileParserDescr d pure ⟨false, p⟩ @@ -485,9 +485,9 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name) unless kind == AttributeKind.global do throwError "invalid attribute '{attrName}', must be global" let decl ← getConstInfo declName match decl.type with - | Expr.const `Lean.Parser.TrailingParser _ _ => + | Expr.const `Lean.Parser.TrailingParser _ => declareTrailingBuiltinParser catName declName prio - | Expr.const `Lean.Parser.Parser _ _ => + | Expr.const `Lean.Parser.Parser _ => declareLeadingBuiltinParser catName declName prio | _ => throwError "unexpected parser type at '{declName}' (`Parser` or `TrailingParser` expected)" if let some doc ← findDocString? (← getEnv) declName then diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index d7cf8a3947..205c76a9b8 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -118,24 +118,24 @@ unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) := def getExprKind : DelabM Name := do let e ← getExpr pure $ match e with - | Expr.bvar _ _ => `bvar - | Expr.fvar _ _ => `fvar - | Expr.mvar _ _ => `mvar - | Expr.sort _ _ => `sort - | Expr.const c _ _ => + | Expr.bvar _ => `bvar + | Expr.fvar _ => `fvar + | Expr.mvar _ => `mvar + | Expr.sort _ => `sort + | Expr.const c _ => -- we identify constants as "nullary applications" to reduce special casing `app ++ c - | Expr.app fn _ _ => match fn.getAppFn with - | Expr.const c _ _ => `app ++ c + | Expr.app fn _ => match fn.getAppFn with + | Expr.const c _ => `app ++ c | _ => `app | Expr.lam _ _ _ _ => `lam | Expr.forallE _ _ _ _ => `forallE | Expr.letE _ _ _ _ _ => `letE - | Expr.lit _ _ => `lit - | Expr.mdata m _ _ => match m.entries with + | Expr.lit _ => `lit + | Expr.mdata m _ => match m.entries with | [(key, _)] => `mdata ++ key | _ => `mdata - | Expr.proj _ _ _ _ => `proj + | Expr.proj _ _ _ => `proj def getOptionsAtCurrPos : DelabM Options := do let ctx ← read @@ -187,7 +187,7 @@ def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do where bodyUsesSuggestion (lctx : LocalContext) (suggestion' : Name) : Bool := Option.isSome <| body.find? fun - | Expr.fvar fvarId _ => + | Expr.fvar fvarId => match lctx.find? fvarId with | none => false | some decl => decl.userName == suggestion' diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 0d6854684e..9c835ad229 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -19,12 +19,12 @@ def maybeAddBlockImplicit (ident : Syntax) : DelabM Syntax := do if ← getPPOption getPPAnalysisBlockImplicit then `(@$ident:ident) else pure ident def unfoldMDatas : Expr → Expr - | Expr.mdata _ e _ => unfoldMDatas e - | e => e + | Expr.mdata _ e => unfoldMDatas e + | e => e @[builtinDelab fvar] def delabFVar : Delab := do -let Expr.fvar id _ ← getExpr | unreachable! +let Expr.fvar id ← getExpr | unreachable! try let l ← getLocalDecl id maybeAddBlockImplicit (mkIdent l.userName) @@ -35,12 +35,12 @@ catch _ => -- loose bound variable, use pseudo syntax @[builtinDelab bvar] def delabBVar : Delab := do - let Expr.bvar idx _ ← getExpr | unreachable! + let Expr.bvar idx ← getExpr | unreachable! pure $ mkIdent $ Name.mkSimple $ "#" ++ toString idx @[builtinDelab mvar] def delabMVar : Delab := do - let Expr.mvar n _ ← getExpr | unreachable! + let Expr.mvar n ← getExpr | unreachable! let mvarDecl ← getMVarDecl n let n := match mvarDecl.userName with @@ -50,7 +50,7 @@ def delabMVar : Delab := do @[builtinDelab sort] def delabSort : Delab := do - let Expr.sort l _ ← getExpr | unreachable! + let Expr.sort l ← getExpr | unreachable! match l with | Level.zero => `(Prop) | Level.succ .zero => `(Type) @@ -87,7 +87,7 @@ where -- NOTE: not a registered delaborator, as `const` is never called (see [delab] description) def delabConst : Delab := do - let Expr.const c₀ ls _ ← getExpr | unreachable! + let Expr.const c₀ ls ← getExpr | unreachable! let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀ let mut c ← unresolveNameGlobal c₀ @@ -374,7 +374,7 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat -- incrementally fill `AppMatchState` from arguments let st ← withAppFnArgs (do - let (Expr.const c us _) ← getExpr | failure + let (Expr.const c us) ← getExpr | failure let (some info) ← getMatcherInfo? c | failure return { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState }) (fun st => do @@ -605,7 +605,7 @@ def delabLetE : Delab := do @[builtinDelab lit] def delabLit : Delab := do - let Expr.lit l _ ← getExpr | unreachable! + let Expr.lit l ← getExpr | unreachable! match l with | Literal.natVal n => pure $ quote n | Literal.strVal s => pure $ quote s @@ -613,7 +613,7 @@ def delabLit : Delab := do -- `@OfNat.ofNat _ n _` ~> `n` @[builtinDelab app.OfNat.ofNat] def delabOfNat : Delab := whenPPOption getPPCoercions do - let (Expr.app (Expr.app _ (Expr.lit (Literal.natVal n) _) _) _ _) ← getExpr | failure + let .app (.app _ (.lit (.natVal n))) _ ← getExpr | failure return quote n -- `@OfDecimal.ofDecimal _ _ m s e` ~> `m*10^(sign * e)` where `sign == 1` if `s = false` and `sign = -1` if `s = true` @@ -621,11 +621,11 @@ def delabOfNat : Delab := whenPPOption getPPCoercions do def delabOfScientific : Delab := whenPPOption getPPCoercions do let expr ← getExpr guard <| expr.getAppNumArgs == 5 - let Expr.lit (Literal.natVal m) _ ← pure (expr.getArg! 2) | failure - let Expr.lit (Literal.natVal e) _ ← pure (expr.getArg! 4) | failure + let .lit (.natVal m) ← pure (expr.getArg! 2) | failure + let .lit (.natVal e) ← pure (expr.getArg! 4) | failure let s ← match expr.getArg! 3 with - | Expr.const ``Bool.true _ _ => pure true - | Expr.const ``Bool.false _ _ => pure false + | Expr.const ``Bool.true _ => pure true + | Expr.const ``Bool.false _ => pure false | _ => failure let str := toString m if s && e == str.length then @@ -644,7 +644,7 @@ function. -/ @[builtinDelab proj] def delabProj : Delab := do - let Expr.proj _ idx _ _ ← getExpr | unreachable! + let Expr.proj _ idx _ ← getExpr | unreachable! let e ← withProj delab -- not perfectly authentic: elaborates to the `idx`-th named projection -- function (e.g. `e.1` is `Prod.fst e`), which unfolds to the actual @@ -655,8 +655,8 @@ def delabProj : Delab := do /-- Delaborate a call to a projection function such as `Prod.fst`. -/ @[builtinDelab app] def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do - let e@(Expr.app fn _ _) ← getExpr | failure - let .const c@(.str _ f) _ _ ← pure fn.getAppFn | failure + let e@(Expr.app fn _) ← getExpr | failure + let .const c@(.str _ f) _ ← pure fn.getAppFn | failure let env ← getEnv let some info ← pure $ env.getProjectionFnInfo? c | failure -- can't use with classes since the instance parameter is implicit @@ -769,8 +769,8 @@ def delabDo : Delab := whenPPOption getPPNotation do def reifyName : Expr → DelabM Name | .const ``Lean.Name.anonymous .. => return Name.anonymous - | .app (.app (.const ``Lean.Name.str ..) n _) (.lit (.strVal s) _) _ => return (← reifyName n).mkStr s - | .app (.app (.const ``Lean.Name.num ..) n _) (.lit (.natVal i) _) _ => return (← reifyName n).mkNum i + | .app (.app (.const ``Lean.Name.str ..) n) (.lit (.strVal s)) => return (← reifyName n).mkStr s + | .app (.app (.const ``Lean.Name.num ..) n) (.lit (.natVal i)) => return (← reifyName n).mkNum i | _ => failure @[builtinDelab app.Lean.Name.str] diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index 30bb845964..1688e672d1 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -56,11 +56,11 @@ def withBindingBody (n : Name) (x : m α) : m α := do descend (e.bindingBody!.instantiate1 fvar) 1 x def withProj (x : m α) : m α := do - let Expr.proj _ _ e _ ← getExpr | unreachable! + let Expr.proj _ _ e ← getExpr | unreachable! descend e 0 x def withMDataExpr (x : m α) : m α := do - let Expr.mdata _ e _ ← getExpr | unreachable! + let Expr.mdata _ e ← getExpr | unreachable! withTheReader SubExpr (fun ctx => { ctx with expr := e }) x def withLetVarType (x : m α) : m α := do diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index c4bfcd1a05..658ea76972 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -39,8 +39,8 @@ private partial def consumeImplicitPrefix (e : Expr) (k : Expr → MetaM α) : M match e with | Expr.forallE n d b c => -- We do not consume instance implicit arguments because the user probably wants be aware of this dependency - if c.binderInfo == BinderInfo.implicit then - withLocalDecl n c.binderInfo d fun arg => + if c == .implicit then + withLocalDecl n c d fun arg => consumeImplicitPrefix (b.instantiate1 arg) k else k e @@ -342,7 +342,7 @@ private partial def getDotCompletionTypeNames (type : Expr) : MetaM NameSet := return (← visit type |>.run {}).2 where visit (type : Expr) : StateRefT NameSet MetaM Unit := do - let .const typeName _ _ := type.getAppFn | return () + let .const typeName _ := type.getAppFn | return () modify fun s => s.insert typeName if isStructure (← getEnv) typeName then for parentName in getAllParentStructures (← getEnv) typeName do diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean index e708b4b2ae..e34696e885 100644 --- a/src/Lean/Server/FileWorker/WidgetRequests.lean +++ b/src/Lean/Server/FileWorker/WidgetRequests.lean @@ -131,7 +131,7 @@ builtin_initialize if !ls.isEmpty then return ls -- TODO(WN): unify handling of delab'd (infoview) and elab'd (editor) applications let .ofTermInfo ti := i.info | return #[] - let .app _ _ _ := ti.expr | return #[] + let .app _ _ := ti.expr | return #[] let some nm := ti.expr.getAppFn.constName? | return #[] i.ctx.runMetaM ti.lctx <| locationLinksFromDecl rc.srcSearchPath rc.doc.meta.uri nm none diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index bf21f612e2..8dd256327b 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -157,7 +157,7 @@ open SubExpr in `SubExpr.Pos` argument for tracking subexpression position. -/ def Expr.traverseAppWithPos {M} [Monad M] (visit : Pos → Expr → M Expr) (p : Pos) (e : Expr) : M Expr := match e with - | Expr.app f a _ => + | Expr.app f a => e.updateApp! <$> traverseAppWithPos visit p.pushAppFn f <*> visit p.pushAppArg a diff --git a/src/Lean/Util/CollectFVars.lean b/src/Lean/Util/CollectFVars.lean index aedd0d2f17..e064953948 100644 --- a/src/Lean/Util/CollectFVars.lean +++ b/src/Lean/Util/CollectFVars.lean @@ -25,13 +25,13 @@ mutual else main e { s with visitedExpr := s.visitedExpr.insert e } partial def main : Expr → Visitor - | Expr.proj _ _ e _ => visit e + | Expr.proj _ _ e => visit e | Expr.forallE _ d b _ => visit b ∘ visit d | Expr.lam _ d b _ => visit b ∘ visit d | Expr.letE _ t v b _ => visit b ∘ visit v ∘ visit t - | Expr.app f a _ => visit a ∘ visit f - | Expr.mdata _ b _ => visit b - | Expr.fvar fvarId _ => fun s => s.add fvarId + | Expr.app f a => visit a ∘ visit f + | Expr.mdata _ b => visit b + | Expr.fvar fvarId => fun s => s.add fvarId | _ => id end diff --git a/src/Lean/Util/CollectLevelParams.lean b/src/Lean/Util/CollectLevelParams.lean index 95416efbdd..eb2db9125e 100644 --- a/src/Lean/Util/CollectLevelParams.lean +++ b/src/Lean/Util/CollectLevelParams.lean @@ -38,14 +38,14 @@ mutual else main e { s with visitedExpr := s.visitedExpr.insert e } partial def main : Expr → Visitor - | Expr.proj _ _ s _ => visitExpr s + | Expr.proj _ _ s => visitExpr s | Expr.forallE _ d b _ => visitExpr b ∘ visitExpr d | Expr.lam _ d b _ => visitExpr b ∘ visitExpr d | Expr.letE _ t v b _ => visitExpr b ∘ visitExpr v ∘ visitExpr t - | Expr.app f a _ => visitExpr a ∘ visitExpr f - | Expr.mdata _ b _ => visitExpr b - | Expr.const _ us _ => fun s => us.foldl (fun s u => visitLevel u s) s - | Expr.sort u _ => visitLevel u + | Expr.app f a => visitExpr a ∘ visitExpr f + | Expr.mdata _ b => visitExpr b + | Expr.const _ us => fun s => us.foldl (fun s u => visitLevel u s) s + | Expr.sort u => visitLevel u | _ => id end diff --git a/src/Lean/Util/CollectMVars.lean b/src/Lean/Util/CollectMVars.lean index 58b1e10788..fd71d68baf 100644 --- a/src/Lean/Util/CollectMVars.lean +++ b/src/Lean/Util/CollectMVars.lean @@ -23,13 +23,13 @@ mutual else main e { s with visitedExpr := s.visitedExpr.insert e } partial def main : Expr → Visitor - | Expr.proj _ _ e _ => visit e + | Expr.proj _ _ e => visit e | Expr.forallE _ d b _ => visit b ∘ visit d | Expr.lam _ d b _ => visit b ∘ visit d | Expr.letE _ t v b _ => visit b ∘ visit v ∘ visit t - | Expr.app f a _ => visit a ∘ visit f - | Expr.mdata _ b _ => visit b - | Expr.mvar mvarId _ => fun s => { s with result := s.result.push mvarId } + | Expr.app f a => visit a ∘ visit f + | Expr.mdata _ b => visit b + | Expr.mvar mvarId => fun s => { s with result := s.result.push mvarId } | _ => id end diff --git a/src/Lean/Util/FindExpr.lean b/src/Lean/Util/FindExpr.lean index f1595b1f13..f43a29305c 100644 --- a/src/Lean/Util/FindExpr.lean +++ b/src/Lean/Util/FindExpr.lean @@ -37,10 +37,10 @@ unsafe def findM? (p : Expr → Bool) (size : USize) (e : Expr) : OptionT FindM else match e with | Expr.forallE _ d b _ => visit d <|> visit b | Expr.lam _ d b _ => visit d <|> visit b - | Expr.mdata _ b _ => visit b + | Expr.mdata _ b => visit b | Expr.letE _ t v b _ => visit t <|> visit v <|> visit b - | Expr.app f a _ => visit f <|> visit a - | Expr.proj _ _ b _ => visit b + | Expr.app f a => visit f <|> visit a + | Expr.proj _ _ b => visit b | _ => failure visit e @@ -61,10 +61,10 @@ def find? (p : Expr → Bool) (e : Expr) : Option Expr := else match e with | Expr.forallE _ d b _ => find? p d <|> find? p b | Expr.lam _ d b _ => find? p d <|> find? p b - | Expr.mdata _ b _ => find? p b + | Expr.mdata _ b => find? p b | Expr.letE _ t v b _ => find? p t <|> find? p v <|> find? p b - | Expr.app f a _ => find? p f <|> find? p a - | Expr.proj _ _ b _ => find? p b + | Expr.app f a => find? p f <|> find? p a + | Expr.proj _ _ b => find? p b | _ => none /-- Return true if `e` occurs in `t` -/ @@ -99,10 +99,10 @@ where match e with | Expr.forallE _ d b _ => visit d <|> visit b | Expr.lam _ d b _ => visit d <|> visit b - | Expr.mdata _ b _ => visit b + | Expr.mdata _ b => visit b | Expr.letE _ t v b _ => visit t <|> visit v <|> visit b | Expr.app .. => visitApp e - | Expr.proj _ _ b _ => visit b + | Expr.proj _ _ b => visit b | _ => failure unsafe def findUnsafe? (p : Expr → FindStep) (e : Expr) : Option Expr := diff --git a/src/Lean/Util/FindLevelMVar.lean b/src/Lean/Util/FindLevelMVar.lean index f1c07488de..44d5df4c66 100644 --- a/src/Lean/Util/FindLevelMVar.lean +++ b/src/Lean/Util/FindLevelMVar.lean @@ -16,14 +16,14 @@ mutual if s.isSome || !e.hasLevelMVar then s else main p e s partial def main (p : MVarId → Bool) : Expr → Visitor - | Expr.sort l _ => visitLevel p l - | Expr.const _ ls _ => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc + | Expr.sort l => visitLevel p l + | Expr.const _ ls => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc | Expr.forallE _ d b _ => visit p b ∘ visit p d | Expr.lam _ d b _ => visit p b ∘ visit p d | Expr.letE _ t v b _ => visit p b ∘ visit p v ∘ visit p t - | Expr.app f a _ => visit p a ∘ visit p f - | Expr.mdata _ b _ => visit p b - | Expr.proj _ _ e _ => visit p e + | Expr.app f a => visit p a ∘ visit p f + | Expr.mdata _ b => visit p b + | Expr.proj _ _ e => visit p e | _ => id partial def visitLevel (p : MVarId → Bool) (l : Level) : Visitor := fun s => diff --git a/src/Lean/Util/FindMVar.lean b/src/Lean/Util/FindMVar.lean index c135f28c93..eb49dc376f 100644 --- a/src/Lean/Util/FindMVar.lean +++ b/src/Lean/Util/FindMVar.lean @@ -16,13 +16,13 @@ mutual if s.isSome || !e.hasMVar then s else main p e s partial def main (p : MVarId → Bool) : Expr → Visitor - | Expr.proj _ _ e _ => visit p e + | Expr.proj _ _ e => visit p e | Expr.forallE _ d b _ => visit p b ∘ visit p d | Expr.lam _ d b _ => visit p b ∘ visit p d | Expr.letE _ t v b _ => visit p b ∘ visit p v ∘ visit p t - | Expr.app f a _ => visit p a ∘ visit p f - | Expr.mdata _ b _ => visit p b - | Expr.mvar mvarId _ => fun s => if s.isNone && p mvarId then some mvarId else s + | Expr.app f a => visit p a ∘ visit p f + | Expr.mdata _ b => visit p b + | Expr.mvar mvarId => fun s => if s.isNone && p mvarId then some mvarId else s | _ => id end diff --git a/src/Lean/Util/FoldConsts.lean b/src/Lean/Util/FoldConsts.lean index b0feef9fd7..4a00f0a3a1 100644 --- a/src/Lean/Util/FoldConsts.lean +++ b/src/Lean/Util/FoldConsts.lean @@ -36,11 +36,11 @@ unsafe def fold {α : Type} (f : Name → α → α) (size : USize) (e : Expr) ( match e with | Expr.forallE _ d b _ => visit b (← visit d acc) | Expr.lam _ d b _ => visit b (← visit d acc) - | Expr.mdata _ b _ => visit b acc + | Expr.mdata _ b => visit b acc | Expr.letE _ t v b _ => visit b (← visit v (← visit t acc)) - | Expr.app f a _ => visit a (← visit f acc) - | Expr.proj _ _ b _ => visit b acc - | Expr.const c _ _ => + | Expr.app f a => visit a (← visit f acc) + | Expr.proj _ _ b => visit b acc + | Expr.const c _ => let s ← get if s.visitedConsts.contains c then pure acc diff --git a/src/Lean/Util/ForEachExpr.lean b/src/Lean/Util/ForEachExpr.lean index b32cfb82fe..43ba068054 100644 --- a/src/Lean/Util/ForEachExpr.lean +++ b/src/Lean/Util/ForEachExpr.lean @@ -22,9 +22,9 @@ partial def visit (g : Expr → m Bool) (e : Expr) : MonadCacheT Expr Unit m Uni | Expr.forallE _ d b _ => do visit g d; visit g b | Expr.lam _ d b _ => do visit g d; visit g b | Expr.letE _ t v b _ => do visit g t; visit g v; visit g b - | Expr.app f a _ => do visit g f; visit g a - | Expr.mdata _ b _ => visit g b - | Expr.proj _ _ b _ => visit g b + | Expr.app f a => do visit g f; visit g a + | Expr.mdata _ b => visit g b + | Expr.proj _ _ b => visit g b | _ => pure () end ForEachExpr diff --git a/src/Lean/Util/HasConstCache.lean b/src/Lean/Util/HasConstCache.lean index 1db7571c05..a131d71728 100644 --- a/src/Lean/Util/HasConstCache.lean +++ b/src/Lean/Util/HasConstCache.lean @@ -16,12 +16,12 @@ unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declN else match e with | .const n .. => return n == declName - | .app f a _ => cache e (← containsUnsafe f <||> containsUnsafe a) + | .app f a => cache e (← containsUnsafe f <||> containsUnsafe a) | .lam _ d b _ => cache e (← containsUnsafe d <||> containsUnsafe b) | .forallE _ d b _ => cache e (← containsUnsafe d <||> containsUnsafe b) | .letE _ t v b _ => cache e (← containsUnsafe t <||> containsUnsafe v <||> containsUnsafe b) - | .mdata _ b _ => cache e (← containsUnsafe b) - | .proj _ _ b _ => cache e (← containsUnsafe b) + | .mdata _ b => cache e (← containsUnsafe b) + | .proj _ _ b => cache e (← containsUnsafe b) | _ => return false where cache (e : Expr) (r : Bool) : StateM (HasConstCache declName) Bool := do diff --git a/src/Lean/Util/OccursCheck.lean b/src/Lean/Util/OccursCheck.lean index 6094457e1f..d6b3326484 100644 --- a/src/Lean/Util/OccursCheck.lean +++ b/src/Lean/Util/OccursCheck.lean @@ -37,13 +37,13 @@ where else modify fun s => s.insert e match e with - | Expr.proj _ _ s _ => visit s + | Expr.proj _ _ s => visit s | 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.mdata _ b _ => visit b - | Expr.app f a _ => visit f; visit a - | Expr.mvar mvarId _ => visitMVar mvarId + | Expr.mdata _ b => visit b + | Expr.app f a => visit f; visit a + | Expr.mvar mvarId => visitMVar mvarId | _ => return () end Lean diff --git a/src/Lean/Util/Recognizers.lean b/src/Lean/Util/Recognizers.lean index 176f35423d..346d9c5204 100644 --- a/src/Lean/Util/Recognizers.lean +++ b/src/Lean/Util/Recognizers.lean @@ -10,7 +10,7 @@ namespace Expr @[inline] def const? (e : Expr) : Option (Name × List Level) := match e with - | Expr.const n us _ => some (n, us) + | Expr.const n us => some (n, us) | _ => none @[inline] def app1? (e : Expr) (fName : Name) : Option Expr := @@ -106,10 +106,10 @@ private def getConstructorVal? (env : Environment) (ctorName : Name) : Option Co def isConstructorApp? (env : Environment) (e : Expr) : Option ConstructorVal := match e with - | Expr.lit (Literal.natVal n) _ => if n == 0 then getConstructorVal? env `Nat.zero else getConstructorVal? env `Nat.succ + | Expr.lit (Literal.natVal n) => if n == 0 then getConstructorVal? env `Nat.zero else getConstructorVal? env `Nat.succ | _ => match e.getAppFn with - | Expr.const n _ _ => match getConstructorVal? env n with + | Expr.const n _ => match getConstructorVal? env n with | some v => if v.numParams + v.numFields == e.getAppNumArgs then some v else none | none => none | _ => none @@ -119,7 +119,7 @@ def isConstructorApp (env : Environment) (e : Expr) : Bool := def constructorApp? (env : Environment) (e : Expr) : Option (ConstructorVal × Array Expr) := do match e with - | Expr.lit (Literal.natVal n) _ => + | Expr.lit (Literal.natVal n) => if n == 0 then do let v ← getConstructorVal? env `Nat.zero pure (v, #[]) @@ -128,7 +128,7 @@ def constructorApp? (env : Environment) (e : Expr) : Option (ConstructorVal × A pure (v, #[mkNatLit (n-1)]) | _ => match e.getAppFn with - | Expr.const n _ _ => do + | Expr.const n _ => do let v ← getConstructorVal? env n if v.numParams + v.numFields == e.getAppNumArgs then pure (v, e.getAppArgs) diff --git a/src/Lean/Util/ReplaceExpr.lean b/src/Lean/Util/ReplaceExpr.lean index bae633c964..bf503aa2cb 100644 --- a/src/Lean/Util/ReplaceExpr.lean +++ b/src/Lean/Util/ReplaceExpr.lean @@ -34,10 +34,10 @@ unsafe def replaceUnsafeM (f? : Expr → Option Expr) (size : USize) (e : Expr) | none => match e with | Expr.forallE _ d b _ => cache i e <| e.updateForallE! (← visit d) (← visit b) | Expr.lam _ d b _ => cache i e <| e.updateLambdaE! (← visit d) (← visit b) - | Expr.mdata _ b _ => cache i e <| e.updateMData! (← visit b) + | Expr.mdata _ b => cache i e <| e.updateMData! (← visit b) | Expr.letE _ t v b _ => cache i e <| e.updateLet! (← visit t) (← visit v) (← visit b) - | Expr.app f a _ => cache i e <| e.updateApp! (← visit f) (← visit a) - | Expr.proj _ _ b _ => cache i e <| e.updateProj! (← visit b) + | Expr.app f a => cache i e <| e.updateApp! (← visit f) (← visit a) + | Expr.proj _ _ b => cache i e <| e.updateProj! (← visit b) | e => pure e visit e @@ -61,10 +61,10 @@ partial def replace (f? : Expr → Option Expr) (e : Expr) : Expr := | none => match e with | Expr.forallE _ d b _ => let d := replace f? d; let b := replace f? b; e.updateForallE! d b | Expr.lam _ d b _ => let d := replace f? d; let b := replace f? b; e.updateLambdaE! d b - | Expr.mdata _ b _ => let b := replace f? b; e.updateMData! b + | Expr.mdata _ b => let b := replace f? b; e.updateMData! b | Expr.letE _ t v b _ => let t := replace f? t; let v := replace f? v; let b := replace f? b; e.updateLet! t v b - | Expr.app f a _ => let f := replace f? f; let a := replace f? a; e.updateApp! f a - | Expr.proj _ _ b _ => let b := replace f? b; e.updateProj! b + | Expr.app f a => let f := replace f? f; let a := replace f? a; e.updateApp! f a + | Expr.proj _ _ b => let b := replace f? b; e.updateProj! b | e => e end Expr diff --git a/src/Lean/Util/ReplaceLevel.lean b/src/Lean/Util/ReplaceLevel.lean index 15226c75e0..119aedb690 100644 --- a/src/Lean/Util/ReplaceLevel.lean +++ b/src/Lean/Util/ReplaceLevel.lean @@ -45,12 +45,12 @@ unsafe def replaceUnsafeM (f? : Level → Option Level) (size : USize) (e : Expr else match e with | Expr.forallE _ d b _ => cache i e <| e.updateForallE! (← visit d) (← visit b) | Expr.lam _ d b _ => cache i e <| e.updateLambdaE! (← visit d) (← visit b) - | Expr.mdata _ b _ => cache i e <| e.updateMData! (← visit b) + | Expr.mdata _ b => cache i e <| e.updateMData! (← visit b) | Expr.letE _ t v b _ => cache i e <| e.updateLet! (← visit t) (← visit v) (← visit b) - | Expr.app f a _ => cache i e <| e.updateApp! (← visit f) (← visit a) - | Expr.proj _ _ b _ => cache i e <| e.updateProj! (← visit b) - | Expr.sort u _ => cache i e <| e.updateSort! (u.replace f?) - | Expr.const _ us _ => cache i e <| e.updateConst! (us.map (Level.replace f?)) + | Expr.app f a => cache i e <| e.updateApp! (← visit f) (← visit a) + | Expr.proj _ _ b => cache i e <| e.updateProj! (← visit b) + | Expr.sort u => cache i e <| e.updateSort! (u.replace f?) + | Expr.const _ us => cache i e <| e.updateConst! (us.map (Level.replace f?)) | e => pure e visit e @@ -67,12 +67,12 @@ end ReplaceLevelImpl partial def replaceLevel (f? : Level → Option Level) : Expr → Expr | e@(Expr.forallE _ d b _) => let d := replaceLevel f? d; let b := replaceLevel f? b; e.updateForallE! d b | e@(Expr.lam _ d b _) => let d := replaceLevel f? d; let b := replaceLevel f? b; e.updateLambdaE! d b - | e@(Expr.mdata _ b _) => let b := replaceLevel f? b; e.updateMData! b + | e@(Expr.mdata _ b) => let b := replaceLevel f? b; e.updateMData! b | e@(Expr.letE _ t v b _) => let t := replaceLevel f? t; let v := replaceLevel f? v; let b := replaceLevel f? b; e.updateLet! t v b - | e@(Expr.app f a _) => let f := replaceLevel f? f; let a := replaceLevel f? a; e.updateApp! f a - | e@(Expr.proj _ _ b _) => let b := replaceLevel f? b; e.updateProj! b - | e@(Expr.sort u _) => e.updateSort! (u.replace f?) - | e@(Expr.const _ us _) => e.updateConst! (us.map (Level.replace f?)) + | e@(Expr.app f a) => let f := replaceLevel f? f; let a := replaceLevel f? a; e.updateApp! f a + | e@(Expr.proj _ _ b) => let b := replaceLevel f? b; e.updateProj! b + | e@(Expr.sort u) => e.updateSort! (u.replace f?) + | e@(Expr.const _ us) => e.updateConst! (us.map (Level.replace f?)) | e => e end Expr diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean index 003b118a74..cb57adfed7 100644 --- a/src/Lean/Util/Sorry.lean +++ b/src/Lean/Util/Sorry.lean @@ -14,11 +14,11 @@ def Expr.isSorry : Expr → Bool | _ => false def Expr.isSyntheticSorry : Expr → Bool - | app (app (const ``sorryAx ..) ..) (const ``Bool.true ..) _ => true + | app (app (const ``sorryAx ..) ..) (const ``Bool.true ..) => true | _ => false def Expr.isNonSyntheticSorry : Expr → Bool - | app (app (const ``sorryAx ..) ..) (const ``Bool.false ..) _ => true + | app (app (const ``sorryAx ..) ..) (const ``Bool.false ..) => true | _ => false def Expr.hasSorry (e : Expr) : Bool := diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean index 30ad6aaecc..2163a80c55 100644 --- a/tests/lean/run/KyleAlg.lean +++ b/tests/lean/run/KyleAlg.lean @@ -237,12 +237,12 @@ where unless (← get).1.contains addr do modify fun (s, c) => (s.insert addr, c+1) match e with - | Expr.proj _ _ s _ => visit s + | Expr.proj _ _ s => visit s | 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.app f a => visit f; visit a + | Expr.mdata _ b => visit b | _ => return () @[implementedBy Expr.dagSizeUnsafe] diff --git a/tests/lean/run/addDecorationsWithoutPartial.lean b/tests/lean/run/addDecorationsWithoutPartial.lean index 33aa3c1608..73fa0aa512 100644 --- a/tests/lean/run/addDecorationsWithoutPartial.lean +++ b/tests/lean/run/addDecorationsWithoutPartial.lean @@ -29,10 +29,10 @@ unsafe def replaceUnsafeM (size : USize) (e : Expr) (f? : (e' : Expr) → sizeOf | none => match e with | Expr.forallE _ d b _ => cache i e <| e.updateForallE! (← visit d) (← visit b) | Expr.lam _ d b _ => cache i e <| e.updateLambdaE! (← visit d) (← visit b) - | Expr.mdata _ b _ => cache i e <| e.updateMData! (← visit b) + | Expr.mdata _ b => cache i e <| e.updateMData! (← visit b) | Expr.letE _ t v b _ => cache i e <| e.updateLet! (← visit t) (← visit v) (← visit b) - | Expr.app f a _ => cache i e <| e.updateApp! (← visit f) (← visit a) - | Expr.proj _ _ b _ => cache i e <| e.updateProj! (← visit b) + | Expr.app f a => cache i e <| e.updateApp! (← visit f) (← visit a) + | Expr.proj _ _ b => cache i e <| e.updateProj! (← visit b) | e => pure e visit e @@ -56,10 +56,10 @@ def replace' (e0 : Expr) (f? : (e : Expr) → sizeOf e ≤ sizeOf e0 → Option | none => match e with | Expr.forallE _ d b _ => let d := go d (dec h); let b := go b (dec h); e.updateForallE! d b | Expr.lam _ d b _ => let d := go d (dec h); let b := go b (dec h); e.updateLambdaE! d b - | Expr.mdata _ b _ => let b := go b (dec h); e.updateMData! b + | Expr.mdata _ b => let b := go b (dec h); e.updateMData! b | Expr.letE _ t v b _ => let t := go t (dec h); let v := go v (dec h); let b := go b (dec h); e.updateLet! t v b - | Expr.app f a _ => let f := go f (dec h); let a := go a (dec h); e.updateApp! f a - | Expr.proj _ _ b _ => let b := go b (dec h); e.updateProj! b + | Expr.app f a => let f := go f (dec h); let a := go a (dec h); e.updateApp! f a + | Expr.proj _ _ b => let b := go b (dec h); e.updateProj! b | e => e go e0 (Nat.le_refl ..) end Expr diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean index 0676706af4..f6a7ba6eb3 100644 --- a/tests/lean/run/depElim1.lean +++ b/tests/lean/run/depElim1.lean @@ -33,13 +33,13 @@ match env.find? ctorName with private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do let env ← getEnv match e with -| Expr.lit (Literal.natVal n) _ => +| Expr.lit (Literal.natVal n) => if n == 0 then getConstructorVal `Nat.zero (mkConst `Nat.zero) #[] else getConstructorVal `Nat.succ (mkConst `Nat.succ) #[mkNatLit (n-1)] | _ => let fn := e.getAppFn match fn with - | Expr.const n _ _ => getConstructorVal n fn e.getAppArgs - | _ => pure none + | Expr.const n _ => getConstructorVal n fn e.getAppArgs + | _ => pure none /- Convert expression using auxiliary hints `inaccessible` and `val` into a pattern -/ partial def mkPattern : Expr → MetaM Pattern diff --git a/tests/lean/run/elabCmd.lean b/tests/lean/run/elabCmd.lean index 9bc3baab71..fc362116c2 100644 --- a/tests/lean/run/elabCmd.lean +++ b/tests/lean/run/elabCmd.lean @@ -14,7 +14,7 @@ let env ← getEnv; def elabAnonCtor (args : Array (TSyntax `term)) (τ : Expr) : TermElabM Expr := match τ.getAppFn with - | Expr.const C _ _ => do + | Expr.const C _ => do let ctors ← getCtors C; (match ctors with | [c] => do diff --git a/tests/lean/run/monadCache.lean b/tests/lean/run/monadCache.lean index 056fa9adb9..545110aca4 100644 --- a/tests/lean/run/monadCache.lean +++ b/tests/lean/run/monadCache.lean @@ -10,9 +10,9 @@ partial def depth : Expr → MonadCacheT Expr Nat CoreM Nat | e => checkCache e fun _ => match e with - | Expr.const c [] _ => pure 1 - | Expr.app f a _ => do pure $ Nat.max (← depth f) (← depth a) + 1 - | _ => pure 0 + | Expr.const c [] => pure 1 + | Expr.app f a => do pure $ Nat.max (← depth f) (← depth a) + 1 + | _ => pure 0 #eval (depth (mkTower 100)).run @@ -20,9 +20,9 @@ partial def visit : Expr → MonadCacheT Expr Expr CoreM Expr | e => checkCache e fun _ => match e with - | Expr.const `a [] _ => pure $ mkConst `b - | Expr.app f a _ => e.updateApp! <$> visit f <*> visit a - | _ => pure e + | Expr.const `a [] => pure $ mkConst `b + | Expr.app f a => e.updateApp! <$> visit f <*> visit a + | _ => pure e #eval (visit (mkTower 4)).run @@ -34,16 +34,16 @@ let e ← (visit (mkTower 100)).run; (depth e).run partial def visitNoCache : Expr → CoreM Expr | e => match e with - | Expr.const `a [] _ => pure $ mkConst `b - | Expr.app f a _ => e.updateApp! <$> visitNoCache f <*> visitNoCache a - | _ => pure e + | Expr.const `a [] => pure $ mkConst `b + | Expr.app f a => e.updateApp! <$> visitNoCache f <*> visitNoCache a + | _ => pure e -- The following is super slow -- #eval do e ← visitNoCache (mkTower 30); (depth e).run def displayConsts (e : Expr) : CoreM Unit := e.forEach fun e => match e with - | Expr.const c _ _ => do IO.println c + | Expr.const c _ => do IO.println c | _ => pure () def tst2 : CoreM Unit := do diff --git a/tests/lean/run/replace.lean b/tests/lean/run/replace.lean index eedc78c1d6..ffa1bfd902 100644 --- a/tests/lean/run/replace.lean +++ b/tests/lean/run/replace.lean @@ -8,7 +8,7 @@ partial def mkBig : Nat → Expr def replaceTest (e : Expr) : Expr := e.replace $ fun e => match e with - | Expr.const c _ _ => if c == `f then mkConst `g else none + | Expr.const c _ => if c == `f then mkConst `g else none | _ => none #eval replaceTest $ mkBig 4 @@ -17,7 +17,7 @@ e.replace $ fun e => match e with def findTest (e : Expr) : Option Expr := e.find? $ fun e => match e with - | Expr.const c _ _ => c == `g + | Expr.const c _ => c == `g | _ => false #eval findTest $ mkBig 4 diff --git a/tests/lean/updateExprIssue.lean b/tests/lean/updateExprIssue.lean index 6c78cc4bbe..ea9cced25c 100644 --- a/tests/lean/updateExprIssue.lean +++ b/tests/lean/updateExprIssue.lean @@ -14,5 +14,5 @@ unsafe def tst1 : MetaM Unit := do set_option trace.compiler.ir.init true def sefFn (e : Expr) (f : Expr) : Expr := match e with - | .app _ a _ => e.updateApp! f a + | .app _ a => e.updateApp! f a | _ => e diff --git a/tests/lean/updateExprIssue.lean.expected.out b/tests/lean/updateExprIssue.lean.expected.out index 89c9412c22..c15dbe0275 100644 --- a/tests/lean/updateExprIssue.lean.expected.out +++ b/tests/lean/updateExprIssue.lean.expected.out @@ -2,29 +2,29 @@ [init] def sefFn (x_1 : obj) (x_2 : obj) : obj := case x_1 : obj of - Lean.Expr.bvar → + Lean.Expr.bvar._impl → ret x_1 - Lean.Expr.fvar → + Lean.Expr.fvar._impl → ret x_1 - Lean.Expr.mvar → + Lean.Expr.mvar._impl → ret x_1 - Lean.Expr.sort → + Lean.Expr.sort._impl → ret x_1 - Lean.Expr.const → + Lean.Expr.const._impl → ret x_1 - Lean.Expr.app → + Lean.Expr.app._impl → let x_3 : obj := proj[1] x_1; let x_4 : obj := Lean.Expr.updateApp x_1 x_2 x_3 ◾; ret x_4 - Lean.Expr.lam → + Lean.Expr.lam._impl → ret x_1 - Lean.Expr.forallE → + Lean.Expr.forallE._impl → ret x_1 - Lean.Expr.letE → + Lean.Expr.letE._impl → ret x_1 - Lean.Expr.lit → + Lean.Expr.lit._impl → ret x_1 - Lean.Expr.mdata → + Lean.Expr.mdata._impl → ret x_1 - Lean.Expr.proj → + Lean.Expr.proj._impl → ret x_1