max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: Option is a Monad again

Browse source 
TODO: remove `OptionM` after update stage0

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
This commit is contained in:
Leonardo de Moura 2022-05-04 15:26:55 -07:00
parent 04d3c6feeb
commit c65537aea5
23 changed files with 170 additions and 162 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Control/Option.lean
View file

@ -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

24
src/Init/Data/Option/Basic.lean
View file

@ -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

13
src/Init/Data/ToString/Basic.lean
View file

@ -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

104
src/Init/Meta.lean
View file

@ -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

2
src/Lean/Class.lean
View file

@ -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

69
src/Lean/Compiler/ConstFolding.lean
View file

@ -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

2
src/Lean/Compiler/ExternAttr.lean
View file

@ -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

2
src/Lean/Compiler/IR/Basic.lean
View file

@ -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

2
src/Lean/Data/Lsp/Communication.lean
View file

@ -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

4
src/Lean/Elab/PreDefinition/WF/Eqns.lean
View file

@ -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

2
src/Lean/Elab/PreDefinition/WF/PackDomain.lean
View file

@ -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!)

2
src/Lean/Elab/Quotation.lean
View file

@ -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

6
src/Lean/Level.lean
View file

@ -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

6
src/Lean/Server/InfoUtils.lean
View file

@ -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)

33
src/Lean/Syntax.lean
View file

@ -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

37
src/Lean/Util/Recognizers.lean
View file

@ -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

2
tests/lean/interactive/plainTermGoal.lean
View file

@ -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

4
tests/lean/interactive/plainTermGoal.lean.expected.out
View file

@ -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":

2
tests/lean/run/305.lean
View file

@ -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

2
tests/lean/run/498.lean
View file

@ -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

2
tests/lean/run/500_lean3.lean
View file

@ -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

4
tests/lean/run/deep1.lean
View file

@ -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 #[])

4
tests/lean/run/irCompilerBug.lean
View file

@ -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))