From c65537aea515285a608e9cd31564f7a6579a692e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 May 2022 15:26:55 -0700 Subject: [PATCH] feat: `Option` is a `Monad` again TODO: remove `OptionM` after update stage0 see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084 --- src/Init/Control/Option.lean | 4 - src/Init/Data/Option/Basic.lean | 24 ++++ src/Init/Data/ToString/Basic.lean | 13 +-- src/Init/Meta.lean | 104 +++++++++--------- src/Lean/Class.lean | 2 +- src/Lean/Compiler/ConstFolding.lean | 69 ++++++------ src/Lean/Compiler/ExternAttr.lean | 2 +- src/Lean/Compiler/IR/Basic.lean | 2 +- src/Lean/Data/Lsp/Communication.lean | 2 +- src/Lean/Elab/PreDefinition/WF/Eqns.lean | 4 +- .../Elab/PreDefinition/WF/PackDomain.lean | 2 +- src/Lean/Elab/Quotation.lean | 2 +- src/Lean/Level.lean | 6 +- src/Lean/Server/InfoUtils.lean | 6 +- src/Lean/Syntax.lean | 33 +++--- src/Lean/Util/Recognizers.lean | 37 +++---- tests/lean/interactive/plainTermGoal.lean | 2 +- .../plainTermGoal.lean.expected.out | 4 +- tests/lean/run/305.lean | 2 +- tests/lean/run/498.lean | 2 +- tests/lean/run/500_lean3.lean | 2 +- tests/lean/run/deep1.lean | 4 +- tests/lean/run/irCompilerBug.lean | 4 +- 23 files changed, 170 insertions(+), 162 deletions(-) diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index def3545973..5a36ff7014 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -78,7 +78,3 @@ instance [Monad m] : MonadControl m (OptionT m) where stM := Option liftWith f := liftM <| f fun x => x.run restoreM x := x - -def liftOption [Alternative m] : Option α → m α - | some a => pure a - | none => failure diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index 3fe819c9b1..6d9c6bbbb3 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -86,3 +86,27 @@ deriving instance BEq for Option instance [LT α] : LT (Option α) where lt := Option.lt (· < ·) + +instance : Functor Option where + map := Option.map + +instance : Monad Option where + pure := Option.some + bind := Option.bind + +instance : Alternative Option where + failure := Option.none + orElse := Option.orElse + +def liftOption [Alternative m] : Option α → m α + | some a => pure a + | none => failure + +@[inline] protected def Option.tryCatch (x : Option α) (handle : Unit → Option α) : Option α := + match x with + | some _ => x + | none => handle () + +instance : MonadExceptOf Unit Option where + throw := fun _ => Option.none + tryCatch := Option.tryCatch diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean index 3cca43430f..6b632cbe77 100644 --- a/src/Init/Data/ToString/Basic.lean +++ b/src/Init/Data/ToString/Basic.lean @@ -123,13 +123,12 @@ instance {α : Type u} {β : α → Type v} [ToString α] [s : ∀ x, ToString ( instance {α : Type u} {p : α → Prop} [ToString α] : ToString (Subtype p) := ⟨fun s => toString (val s)⟩ -def String.toInt? (s : String) : Option Int := - OptionM.run do - if s.get 0 = '-' then do - let v ← (s.toSubstring.drop 1).toNat?; - pure <| - Int.ofNat v - else - Int.ofNat <$> s.toNat? +def String.toInt? (s : String) : Option Int := do + if s.get 0 = '-' then do + let v ← (s.toSubstring.drop 1).toNat?; + pure <| - Int.ofNat v + else + Int.ofNat <$> s.toNat? def String.isInt (s : String) : Bool := if s.get 0 = '-' then diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 82fc619a68..ae520a567d 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -621,42 +621,40 @@ def toNat (stx : Syntax) : Nat := | some val => val | none => 0 -def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := - OptionM.run do - let c := s.get i - let i := s.next i - if c == '\\' then pure ('\\', i) - else if c = '\"' then pure ('\"', i) - else if c = '\'' then pure ('\'', i) - else if c = 'r' then pure ('\r', i) - else if c = 'n' then pure ('\n', i) - else if c = 't' then pure ('\t', i) - else if c = 'x' then - let (d₁, i) ← decodeHexDigit s i - let (d₂, i) ← decodeHexDigit s i - pure (Char.ofNat (16*d₁ + d₂), i) - else if c = 'u' then do - let (d₁, i) ← decodeHexDigit s i - let (d₂, i) ← decodeHexDigit s i - let (d₃, i) ← decodeHexDigit s i - let (d₄, i) ← decodeHexDigit s i - pure (Char.ofNat (16*(16*(16*d₁ + d₂) + d₃) + d₄), i) - else - none +def decodeQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := do + let c := s.get i + let i := s.next i + if c == '\\' then pure ('\\', i) + else if c = '\"' then pure ('\"', i) + else if c = '\'' then pure ('\'', i) + else if c = 'r' then pure ('\r', i) + else if c = 'n' then pure ('\n', i) + else if c = 't' then pure ('\t', i) + else if c = 'x' then + let (d₁, i) ← decodeHexDigit s i + let (d₂, i) ← decodeHexDigit s i + pure (Char.ofNat (16*d₁ + d₂), i) + else if c = 'u' then do + let (d₁, i) ← decodeHexDigit s i + let (d₂, i) ← decodeHexDigit s i + let (d₃, i) ← decodeHexDigit s i + let (d₄, i) ← decodeHexDigit s i + pure (Char.ofNat (16*(16*(16*d₁ + d₂) + d₃) + d₄), i) + else + none -partial def decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Option String := - OptionM.run do - let c := s.get i - let i := s.next i - if c == '\"' then - pure acc - else if s.atEnd i then - none - else if c == '\\' then do - let (c, i) ← decodeQuotedChar s i - decodeStrLitAux s i (acc.push c) - else - decodeStrLitAux s i (acc.push c) +partial def decodeStrLitAux (s : String) (i : String.Pos) (acc : String) : Option String := do + let c := s.get i + let i := s.next i + if c == '\"' then + pure acc + else if s.atEnd i then + none + else if c == '\\' then do + let (c, i) ← decodeQuotedChar s i + decodeStrLitAux s i (acc.push c) + else + decodeStrLitAux s i (acc.push c) def decodeStrLit (s : String) : Option String := decodeStrLitAux s ⟨1⟩ "" @@ -666,14 +664,13 @@ def isStrLit? (stx : Syntax) : Option String := | some val => decodeStrLit val | _ => none -def decodeCharLit (s : String) : Option Char := - OptionM.run do - let c := s.get ⟨1⟩ - if c == '\\' then do - let (c, _) ← decodeQuotedChar s ⟨2⟩ - pure c - else - pure c +def decodeCharLit (s : String) : Option Char := do + let c := s.get ⟨1⟩ + if c == '\\' then do + let (c, _) ← decodeQuotedChar s ⟨2⟩ + pure c + else + pure c def isCharLit? (stx : Syntax) : Option Char := match isLit? charLitKind stx with @@ -785,7 +782,7 @@ instance : Quote Nat := ⟨fun n => Syntax.mkNumLit <| toString n⟩ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[quote s.toString]⟩ -- in contrast to `Name.toString`, we can, and want to be, precise here -private def getEscapedNameParts? (acc : List String) : Name → OptionM (List String) +private def getEscapedNameParts? (acc : List String) : Name → Option (List String) | Name.anonymous => return acc | Name.str n s _ => do let s ← Name.escapePart s @@ -934,18 +931,17 @@ abbrev autoParam.{u} (α : Sort u) (tactic : Lean.Syntax) : Sort u := α /- Helper functions for manipulating interpolated strings -/ namespace Lean.Syntax -private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := - OptionM.run do - match decodeQuotedChar s i with - | some r => some r - | none => - let c := s.get i - let i := s.next i - if c == '{' then pure ('{', i) - else none +private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := do + match decodeQuotedChar s i with + | some r => some r + | none => + let c := s.get i + let i := s.next i + if c == '{' then pure ('{', i) + else none private partial def decodeInterpStrLit (s : String) : Option String := - let rec loop (i : String.Pos) (acc : String) : OptionM String := + let rec loop (i : String.Pos) (acc : String) : Option String := let c := s.get i let i := s.next i if c == '\"' || c == '{' then diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index b9d00e3615..667e547cfa 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -93,7 +93,7 @@ private def consumeNLambdas : Nat → Expr → Option Expr partial def getClassName (env : Environment) : Expr → Option Name | Expr.forallE _ _ b _ => getClassName env b - | e => OptionM.run do + | e => do let Expr.const c _ _ ← pure e.getAppFn | none let info ← env.find? c match info.value? with diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean index 8a9571f755..eff716ced4 100644 --- a/src/Lean/Compiler/ConstFolding.lean +++ b/src/Lean/Compiler/ConstFolding.lean @@ -55,12 +55,11 @@ def mkUIntLit (info : NumScalarTypeInfo) (n : Nat) : Expr := def mkUInt32Lit (n : Nat) : Expr := mkUIntLit {nbits := 32} n -def foldBinUInt (fn : NumScalarTypeInfo → Bool → Nat → Nat → Nat) (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr := - OptionM.run do - let n₁ ← getNumLit a₁ - let n₂ ← getNumLit a₂ - let info ← getInfoFromVal a₁ - return mkUIntLit info (fn info beforeErasure n₁ n₂) +def foldBinUInt (fn : NumScalarTypeInfo → Bool → Nat → Nat → Nat) (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr := do + let n₁ ← getNumLit a₁ + let n₂ ← getNumLit a₂ + let info ← getInfoFromVal a₁ + return mkUIntLit info (fn info beforeErasure n₁ n₂) def foldUIntAdd := foldBinUInt fun _ _ => Add.add def foldUIntMul := foldBinUInt fun _ _ => Mul.mul @@ -75,11 +74,10 @@ def preUIntBinFoldFns : List (Name × BinFoldFn) := def uintBinFoldFns : List (Name × BinFoldFn) := numScalarTypes.foldl (fun r info => r ++ (preUIntBinFoldFns.map (fun ⟨suffix, fn⟩ => (info.id ++ suffix, fn)))) [] -def foldNatBinOp (fn : Nat → Nat → Nat) (a₁ a₂ : Expr) : Option Expr := - OptionM.run do - let n₁ ← getNumLit a₁ - let n₂ ← getNumLit a₂ - return mkRawNatLit (fn n₁ n₂) +def foldNatBinOp (fn : Nat → Nat → Nat) (a₁ a₂ : Expr) : Option Expr := do + let n₁ ← getNumLit a₁ + let n₂ ← getNumLit a₂ + return mkRawNatLit (fn n₁ n₂) def foldNatAdd (_ : Bool) := foldNatBinOp Add.add def foldNatMul (_ : Bool) := foldNatBinOp Mul.mul @@ -89,14 +87,13 @@ def foldNatMod (_ : Bool) := foldNatBinOp Mod.mod -- TODO: add option for controlling the limit def natPowThreshold := 256 -def foldNatPow (_ : Bool) (a₁ a₂ : Expr) : Option Expr := - OptionM.run do - let n₁ ← getNumLit a₁ - let n₂ ← getNumLit a₂ - if n₂ < natPowThreshold then - return mkRawNatLit (n₁ ^ n₂) - else - failure +def foldNatPow (_ : Bool) (a₁ a₂ : Expr) : Option Expr := do + let n₁ ← getNumLit a₁ + let n₂ ← getNumLit a₂ + if n₂ < natPowThreshold then + return mkRawNatLit (n₁ ^ n₂) + else + failure def mkNatEq (a b : Expr) : Expr := mkAppN (mkConst ``Eq [levelOne]) #[(mkConst `Nat), a, b] @@ -115,24 +112,22 @@ def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr := | true, false => mkDecIsFalse pred (mkLcProof pred) def foldNatBinPred (mkPred : Expr → Expr → Expr) (fn : Nat → Nat → Bool) - (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr := - OptionM.run do - let n₁ ← getNumLit a₁ - let n₂ ← getNumLit a₂ - return toDecidableExpr beforeErasure (mkPred a₁ a₂) (fn n₁ n₂) + (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr := do + let n₁ ← getNumLit a₁ + let n₂ ← getNumLit a₂ + return toDecidableExpr beforeErasure (mkPred a₁ a₂) (fn n₁ n₂) def foldNatDecEq := foldNatBinPred mkNatEq (fun a b => a = b) def foldNatDecLt := foldNatBinPred mkNatLt (fun a b => a < b) def foldNatDecLe := foldNatBinPred mkNatLe (fun a b => a ≤ b) -def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option Expr := - OptionM.run do - let n₁ ← getNumLit a₁ - let n₂ ← getNumLit a₂ - if fn n₁ n₂ then - return mkConst ``Bool.true - else - return mkConst ``Bool.false +def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option Expr := do + let n₁ ← getNumLit a₁ + let n₂ ← getNumLit a₂ + if fn n₁ n₂ then + return mkConst ``Bool.true + else + return mkConst ``Bool.false def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b) def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b) @@ -183,11 +178,11 @@ def boolFoldFns : List (Name × BinFoldFn) := def binFoldFns : List (Name × BinFoldFn) := boolFoldFns ++ uintBinFoldFns ++ natFoldFns -def foldNatSucc (_ : Bool) (a : Expr) : Option Expr := OptionM.run do +def foldNatSucc (_ : Bool) (a : Expr) : Option Expr := do let n ← getNumLit a return mkRawNatLit (n+1) -def foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr := OptionM.run do +def foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr := do guard (!beforeErasure) let n ← getNumLit a if isValidChar n.toUInt32 then @@ -195,7 +190,7 @@ def foldCharOfNat (beforeErasure : Bool) (a : Expr) : Option Expr := OptionM.run else return mkUInt32Lit 0 -def foldToNat (_ : Bool) (a : Expr) : Option Expr := OptionM.run do +def foldToNat (_ : Bool) (a : Expr) : Option Expr := do let n ← getNumLit a return mkRawNatLit n @@ -214,7 +209,7 @@ def findUnFoldFn (fn : Name) : Option UnFoldFn := unFoldFns.lookup fn @[export lean_fold_bin_op] -def foldBinOp (beforeErasure : Bool) (f : Expr) (a : Expr) (b : Expr) : Option Expr := OptionM.run do +def foldBinOp (beforeErasure : Bool) (f : Expr) (a : Expr) (b : Expr) : Option Expr := do match f with | Expr.const fn _ _ => let foldFn ← findBinFoldFn fn @@ -223,7 +218,7 @@ def foldBinOp (beforeErasure : Bool) (f : Expr) (a : Expr) (b : Expr) : Option E failure @[export lean_fold_un_op] -def foldUnOp (beforeErasure : Bool) (f : Expr) (a : Expr) : Option Expr := OptionM.run do +def foldUnOp (beforeErasure : Bool) (f : Expr) (a : Expr) : Option Expr := do match f with | Expr.const fn _ _ => let foldFn ← findUnFoldFn fn diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean index 4b0951f6a7..2fe873cf0d 100644 --- a/src/Lean/Compiler/ExternAttr.lean +++ b/src/Lean/Compiler/ExternAttr.lean @@ -130,7 +130,7 @@ def isExternC (env : Environment) (fn : Name) : Bool := | some { entries := [ ExternEntry.standard `all _ ], .. } => true | _ => false -def getExternNameFor (env : Environment) (backend : Name) (fn : Name) : Option String := OptionM.run do +def getExternNameFor (env : Environment) (backend : Name) (fn : Name) : Option String := do let data ← getExternAttrData env fn let entry ← getExternEntryFor data backend match entry with diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 30765a3d4b..ed4bf35027 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -566,7 +566,7 @@ def addParamRename (ρ : IndexRenaming) (p₁ p₂ : Param) : Option IndexRenami else none -def addParamsRename (ρ : IndexRenaming) (ps₁ ps₂ : Array Param) : Option IndexRenaming := OptionM.run do +def addParamsRename (ρ : IndexRenaming) (ps₁ ps₂ : Array Param) : Option IndexRenaming := do if ps₁.size != ps₂.size then failure else diff --git a/src/Lean/Data/Lsp/Communication.lean b/src/Lean/Data/Lsp/Communication.lean index cbb5252ee8..af3762586c 100644 --- a/src/Lean/Data/Lsp/Communication.lean +++ b/src/Lean/Data/Lsp/Communication.lean @@ -15,7 +15,7 @@ open Lean open Lean.JsonRpc section - private def parseHeaderField (s : String) : Option (String × String) := OptionM.run do + private def parseHeaderField (s : String) : Option (String × String) := do guard $ s ≠ "" ∧ s.takeRight 2 = "\r\n" let xs := (s.dropRight 2).splitOn ": " match xs with diff --git a/src/Lean/Elab/PreDefinition/WF/Eqns.lean b/src/Lean/Elab/PreDefinition/WF/Eqns.lean index 38c00903a1..5e0c3ea0da 100644 --- a/src/Lean/Elab/PreDefinition/WF/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/WF/Eqns.lean @@ -43,14 +43,14 @@ private def hasWellFoundedFix (e : Expr) : Bool := Helper function for decoding the packed argument for a `WellFounded.fix` application. Recall that we use `PSum` and `PSigma` for packing the arguments of mutually recursive nary functions. -/ -private partial def decodePackedArg? (info : EqnInfo) (e : Expr) : Option (Name × Array Expr) := OptionM.run do +private partial def decodePackedArg? (info : EqnInfo) (e : Expr) : Option (Name × Array Expr) := do if info.declNames.size == 1 then let args := decodePSigma e #[] return (info.declNames[0], args) else decodePSum? e 0 where - decodePSum? (e : Expr) (i : Nat) : Option (Name × Array Expr) := OptionM.run do + decodePSum? (e : Expr) (i : Nat) : Option (Name × Array Expr) := do if e.isAppOfArity ``PSum.inl 3 then decodePSum? e.appArg! i else if e.isAppOfArity ``PSum.inr 3 then diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean index e52e666ddd..2bbae325f8 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean @@ -113,7 +113,7 @@ partial def packDomain (fixedPrefix : Nat) (preDefs : Array PreDefinition) : Met return preDefsNew where /-- Return `some i` if `e` is a `preDefs[i]` application -/ - isAppOfPreDef? (e : Expr) : OptionM Nat := do + isAppOfPreDef? (e : Expr) : Option Nat := do let f := e.getAppFn guard f.isConst preDefs.findIdx? (·.declName == f.constName!) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 35ff8dbce7..9df3253259 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -343,7 +343,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := let contents := if contents.size == 1 then contents[0] else mkNullNode contents - `(match OptionM.run ($(discrs).sequenceMap fun + `(match ($(discrs).sequenceMap fun | `($contents) => some $tuple | _ => none) with | some $resId => $yes diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 744ca98773..306f8c7e8f 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -383,10 +383,10 @@ def dec : Level → Option Level | param _ _ => none | mvar _ _ => none | succ l _ => l - | max l₁ l₂ _ => OptionM.run do return mkLevelMax (← dec l₁) (← dec l₂) + | max l₁ l₂ _ => return mkLevelMax (← dec l₁) (← dec l₂) /- Remark: `mkLevelMax` in the following line is not a typo. If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/ - | imax l₁ l₂ _ => OptionM.run do return mkLevelMax (← dec l₁) (← dec l₂) + | imax l₁ l₂ _ => return mkLevelMax (← dec l₁) (← dec l₂) /- Level to Format/Syntax -/ @@ -590,7 +590,7 @@ def Level.collectMVars (u : Level) (s : MVarIdSet := {}) : MVarIdSet := | _ => s def Level.find? (u : Level) (p : Level → Bool) : Option Level := - let rec visit (u : Level) : OptionM Level := + let rec visit (u : Level) : Option Level := if p u then return u else match u with diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 70fa088aa0..c4aa78547d 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -102,7 +102,7 @@ def Info.range? (i : Info) : Option String.Range := def Info.contains (i : Info) (pos : String.Pos) : Bool := i.range?.any (·.contains pos) -def Info.size? (i : Info) : Option String.Pos := OptionM.run do +def Info.size? (i : Info) : Option String.Pos := do let pos ← i.pos? let tailPos ← i.tailPos? return tailPos - pos @@ -114,12 +114,12 @@ def Info.isSmaller (i₁ i₂ : Info) : Bool := | some _, none => true | _, _ => false -def Info.occursBefore? (i : Info) (hoverPos : String.Pos) : Option String.Pos := OptionM.run do +def Info.occursBefore? (i : Info) (hoverPos : String.Pos) : Option String.Pos := do let tailPos ← i.tailPos? guard (tailPos ≤ hoverPos) return hoverPos - tailPos -def Info.occursInside? (i : Info) (hoverPos : String.Pos) : Option String.Pos := OptionM.run do +def Info.occursInside? (i : Info) (hoverPos : String.Pos) : Option String.Pos := do let headPos ← i.pos? let tailPos ← i.tailPos? guard (headPos ≤ hoverPos && hoverPos < tailPos) diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index db76f16a51..9757530f80 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -250,23 +250,22 @@ partial instance : ForIn m TopDown Syntax where | ForInStep.yield b => return b | ForInStep.done b => return b -partial def reprint (stx : Syntax) : Option String := - OptionM.run do - let mut s := "" - for stx in stx.topDown (firstChoiceOnly := true) do - match stx with - | atom info val => s := s ++ reprintLeaf info val - | ident info rawVal _ _ => s := s ++ reprintLeaf info rawVal.toString - | node info kind args => - if kind == choiceKind then - -- this visit the first arg twice, but that should hardly be a problem - -- given that choice nodes are quite rare and small - let s0 ← reprint args[0] - for arg in args[1:] do - let s' ← reprint arg - guard (s0 == s') - | _ => pure () - return s +partial def reprint (stx : Syntax) : Option String := do + let mut s := "" + for stx in stx.topDown (firstChoiceOnly := true) do + match stx with + | atom info val => s := s ++ reprintLeaf info val + | ident info rawVal _ _ => s := s ++ reprintLeaf info rawVal.toString + | node info kind args => + if kind == choiceKind then + -- this visit the first arg twice, but that should hardly be a problem + -- given that choice nodes are quite rare and small + let s0 ← reprint args[0] + for arg in args[1:] do + let s' ← reprint arg + guard (s0 == s') + | _ => pure () + return s where reprintLeaf (info : SourceInfo) (val : String) : String := match info with diff --git a/src/Lean/Util/Recognizers.lean b/src/Lean/Util/Recognizers.lean index 1c4f3e0eb3..176f35423d 100644 --- a/src/Lean/Util/Recognizers.lean +++ b/src/Lean/Util/Recognizers.lean @@ -117,24 +117,23 @@ def isConstructorApp? (env : Environment) (e : Expr) : Option ConstructorVal := def isConstructorApp (env : Environment) (e : Expr) : Bool := e.isConstructorApp? env |>.isSome -def constructorApp? (env : Environment) (e : Expr) : Option (ConstructorVal × Array Expr) := - OptionM.run do - match e with - | Expr.lit (Literal.natVal n) _ => - if n == 0 then do - let v ← getConstructorVal? env `Nat.zero - pure (v, #[]) - else do - let v ← getConstructorVal? env `Nat.succ - pure (v, #[mkNatLit (n-1)]) - | _ => - match e.getAppFn with - | Expr.const n _ _ => do - let v ← getConstructorVal? env n - if v.numParams + v.numFields == e.getAppNumArgs then - pure (v, e.getAppArgs) - else - none - | _ => none +def constructorApp? (env : Environment) (e : Expr) : Option (ConstructorVal × Array Expr) := do + match e with + | Expr.lit (Literal.natVal n) _ => + if n == 0 then do + let v ← getConstructorVal? env `Nat.zero + pure (v, #[]) + else do + let v ← getConstructorVal? env `Nat.succ + pure (v, #[mkNatLit (n-1)]) + | _ => + match e.getAppFn with + | Expr.const n _ _ => do + let v ← getConstructorVal? env n + if v.numParams + v.numFields == e.getAppNumArgs then + pure (v, e.getAppArgs) + else + none + | _ => none end Lean.Expr diff --git a/tests/lean/interactive/plainTermGoal.lean b/tests/lean/interactive/plainTermGoal.lean index 0520208125..40934a1857 100644 --- a/tests/lean/interactive/plainTermGoal.lean +++ b/tests/lean/interactive/plainTermGoal.lean @@ -7,7 +7,7 @@ example : 0 < 2 := --^ $/lean/plainTermGoal --^ $/lean/plainTermGoal -example : OptionM Unit := do +example : Option Unit := do let y : Int ← none let x := Nat.zero --^ $/lean/plainTermGoal diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out index f3c1f64bb7..2850ddf973 100644 --- a/tests/lean/interactive/plainTermGoal.lean.expected.out +++ b/tests/lean/interactive/plainTermGoal.lean.expected.out @@ -26,8 +26,8 @@ {"textDocument": {"uri": "file://plainTermGoal.lean"}, "position": {"line": 11, "character": 10}} {"range": - {"start": {"line": 9, "character": 26}, "end": {"line": 13, "character": 11}}, - "goal": "⊢ OptionM Unit"} + {"start": {"line": 9, "character": 25}, "end": {"line": 13, "character": 11}}, + "goal": "⊢ Option Unit"} {"textDocument": {"uri": "file://plainTermGoal.lean"}, "position": {"line": 16, "character": 17}} {"range": diff --git a/tests/lean/run/305.lean b/tests/lean/run/305.lean index 970a6430a9..bdebaea140 100644 --- a/tests/lean/run/305.lean +++ b/tests/lean/run/305.lean @@ -19,7 +19,7 @@ namespace Cmd def flag? (c : Cmd) (longName : String) : Option Unit := c.flags.find? (·.longName = longName) def hasFlag (c : Cmd) (longName : String) : Bool := c.flag? longName |>.isSome - def subCmdByFullName? (c : Cmd) (fullName : Array String) : Option Cmd := OptionM.run do + def subCmdByFullName? (c : Cmd) (fullName : Array String) : Option Cmd := do let mut c := c guard <| c.name = fullName.get? 0 for subName in fullName[1:] do diff --git a/tests/lean/run/498.lean b/tests/lean/run/498.lean index 2d2f301465..4c4692b166 100644 --- a/tests/lean/run/498.lean +++ b/tests/lean/run/498.lean @@ -51,7 +51,7 @@ inductive Kind (flag : Flag) (inputFlag : InputFlag) (msg : String := - let complementaryName? : Option String := OptionM.run do + let complementaryName? : Option String := do if inputFlag.isShort then pure s!" (`--{flag.longName}`)" else diff --git a/tests/lean/run/500_lean3.lean b/tests/lean/run/500_lean3.lean index 893baa58d6..67a3de01d1 100644 --- a/tests/lean/run/500_lean3.lean +++ b/tests/lean/run/500_lean3.lean @@ -1,4 +1,4 @@ -example (foo bar : OptionM Nat) : False := by +example (foo bar : Option Nat) : False := by have : do { let x ← bar; foo } = bar >>= fun x => foo := rfl admit done diff --git a/tests/lean/run/deep1.lean b/tests/lean/run/deep1.lean index 426fdd0b38..26748d10d6 100644 --- a/tests/lean/run/deep1.lean +++ b/tests/lean/run/deep1.lean @@ -2,11 +2,11 @@ partial def recurseM [Monad μ] (curr: α) (action: α -> μ (List α)) : μ PUn let children ← action curr children.forM (recurseM · action) -def specificTraverseList : OptionM Unit := recurseM () (fun _ => some []) +def specificTraverseList : Option Unit := recurseM () (fun _ => some []) partial def recurseM2 [Monad μ] (curr: α) (action: α -> μ (Array α)) : μ PUnit := do let children ← action curr children.forM (recurseM2 · action) -def specificTraverseArray : OptionM Unit := +def specificTraverseArray : Option Unit := recurseM2 () (fun _ => some #[]) diff --git a/tests/lean/run/irCompilerBug.lean b/tests/lean/run/irCompilerBug.lean index 4e76ce9a1c..24385860e7 100644 --- a/tests/lean/run/irCompilerBug.lean +++ b/tests/lean/run/irCompilerBug.lean @@ -6,7 +6,7 @@ structure Payload := -@[noinline] def get? (p : Payload) (k : Nat) : OptionM Nat := +@[noinline] def get? (p : Payload) (k : Nat) : Option Nat := if p.key == k then pure p.val else failure inductive T @@ -15,7 +15,7 @@ inductive T | c (i : Nat) | d (i : Nat) -@[noinline] def foo (p : Payload) : OptionM T := +@[noinline] def foo (p : Payload) : Option T := (do let i ← get? p 1; pure (T.a i))