diff options
author | Zyad Hassan | 2024-04-12 10:48:03 -0700 |
---|---|---|
committer | Zyad Hassan | 2024-04-24 09:21:18 -0700 |
commit | 9b281e021b3b2dbfa6ff265cc843e0aac3b400ac (patch) | |
tree | e4231b5e3021e097f9b805a3372507d7bd7fc290 /backends/lean/Base/Primitives | |
parent | 1be37966ceea2510b911b119a96246b4657a62fd (diff) |
Add core::option::unwrap builtin
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r-- | backends/lean/Base/Primitives/Base.lean | 5 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Core.lean | 8 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 5 |
3 files changed, 13 insertions, 5 deletions
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 4c5b2795..ac4fd340 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -76,6 +76,11 @@ def eval_global {α: Type u} (x: Result α) (_: ok? x := by prove_eval_global) : | fail _ | div => by contradiction | ok x => x +def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a := + match x with + | some x => ok x + | none => fail e + /- DO-DSL SUPPORT -/ def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β := diff --git a/backends/lean/Base/Primitives/Core.lean b/backends/lean/Base/Primitives/Core.lean index 99f65985..b7dd6d2c 100644 --- a/backends/lean/Base/Primitives/Core.lean +++ b/backends/lean/Base/Primitives/Core.lean @@ -51,4 +51,12 @@ def clone.CloneBool : clone.Clone Bool := { clone := fun b => ok (clone.impls.CloneBool.clone b) } +namespace option + +/- [core::option::{core::option::Option<T>}::unwrap] -/ +def Option.unwrap (T : Type) (x : Option T) : Result T := + Result.ofOption x Error.panic + +end option -- core.option + end core diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 014decb1..2bee8a2f 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -364,11 +364,6 @@ def Scalar.tryMkOpt (ty : ScalarTy) (x : Int) : Option (Scalar ty) := some (Scalar.ofIntCore x (Scalar.check_bounds_imp_in_bounds h)) else none -def Result.ofOption {a : Type u} (x : Option a) (e : Error) : Result a := - match x with - | some x => ok x - | none => fail e - def Scalar.tryMk (ty : ScalarTy) (x : Int) : Result (Scalar ty) := Result.ofOption (tryMkOpt ty x) integerOverflow |