Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: allow EStateM to be used universe-polymorphically #3010

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

feat: allow EStateM to be used universe-polymorphically #3010

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5839989
feat: allow `EStateM` to be used polymorphically
eric-wieser Dec 1, 2023
8ac6853
update test output; this looks like some accidental elaboration reord…
eric-wieser Dec 1, 2023
9852b05
Merge remote-tracking branch 'upstream/master' into EStateM-universes
eric-wieser Sep 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/Init/Control/EState.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ universe u v

namespace EStateM

variable {ε σ α : Type u}
variable {ε : Type uε} {σ : Type uσ} {α : Type uα}

instance [ToString ε] [ToString α] : ToString (Result ε σ α) where
toString
Expand All @@ -27,7 +27,7 @@ end EStateM

namespace EStateM

variable {ε σ α β : Type u}
variable {ε : Type uε} {σ : Type uσ} {α : Type uα} {β : Type uβ}

/-- Alternative orElse operator that allows to select which exception should be used.
The default is to use the first exception since the standard `orElse` uses the second. -/
Expand All @@ -54,7 +54,7 @@ instance : MonadFinally (EStateM ε σ) := {
| Result.error e₂ s => Result.error e₂ s
}

@[always_inline, inline] def fromStateM {ε σ α : Type} (x : StateM σ α) : EStateM ε σ α := fun s =>
@[always_inline, inline] def fromStateM {ε σ α : Type _} (x : StateM σ α) : EStateM ε σ α := fun s =>
match x.run s with
| (a, s') => EStateM.Result.ok a s'

Expand Down
8 changes: 4 additions & 4 deletions src/Init/Prelude.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3266,13 +3266,13 @@ namespace EStateM
`Result ε σ α` is equivalent to `Except ε α × σ`, but using a single
combined inductive yields a more efficient data representation.
-/
inductive Result (ε σ α : Type u) where
inductive Result (ε : Type uε) (σ : Type uσ) (α : Type uα) where
/-- A success value of type `α`, and a new state `σ`. -/
| ok : α → σ → Result ε σ α
/-- A failure value of type `ε`, and a new state `σ`. -/
| error : ε → σ → Result ε σ α

variable {ε σ α : Type u}
variable {ε σ α : Type _}

instance [Inhabited ε] [Inhabited σ] : Inhabited (Result ε σ α) where
default := Result.error default default
Expand All @@ -3284,11 +3284,11 @@ open EStateM (Result) in
`EStateM ε σ` is a combined error and state monad, equivalent to
`ExceptT ε (StateM σ)` but more efficient.
-/
def EStateM (ε σ α : Type u) := σ → Result ε σ α
def EStateM (ε : Type uε) (σ : Type uσ) (α : Type uα) := σ → Result ε σ α

namespace EStateM

variable {ε σ α β : Type u}
variable {ε : Type uε} {σ : Type uσ} {α : Type uα} {β : Type uβ}

instance [Inhabited ε] : Inhabited (EStateM ε σ α) where
default := fun s => Result.error default s
Expand Down
22 changes: 12 additions & 10 deletions tests/lean/new-compiler/CompilerElimDeadBranches.lean.expected.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,21 +47,23 @@
let _x.5 := some _ _x.4;
return _x.5
[Compiler.result] size: 1 def addSomeVal x : Option Nat := let _x.1 := addSomeVal._redArg; return _x.1
[Compiler.elimDeadBranches] Eliminating monadic with #[("_x.207",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("_x.211",
[Compiler.elimDeadBranches] Eliminating monadic with #[("_x.212",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.205",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.91",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.ok #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("x", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.207",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("val.64", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("val.200", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.212",
("a.206", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.205",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Except.error #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("a.208", Lean.Compiler.LCNF.UnreachableBranches.Value.top),
("_x.211",
Lean.Compiler.LCNF.UnreachableBranches.Value.ctor `Option.some #[Lean.Compiler.LCNF.UnreachableBranches.Value.top]),
("_x.88", Lean.Compiler.LCNF.UnreachableBranches.Value.top), ("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
("y", Lean.Compiler.LCNF.UnreachableBranches.Value.top)]
[Compiler.elimDeadBranches] Threw away cases _x.211 branch Option.none
[Compiler.elimDeadBranches] Threw away cases _x.212 branch Option.none
[Compiler.elimDeadBranches] Threw away cases _x.205 branch Except.ok
Expand Down
Loading