diff options
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Primitives.lean | 29 |
1 files changed, 22 insertions, 7 deletions
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index d3de1d10..85e088fc 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -4,6 +4,8 @@ import Init.Data.List.Basic import Mathlib.Tactic.RunCmd import Mathlib.Tactic.Linarith +namespace Primitives + -------------------- -- ASSERT COMMAND --Std. -------------------- @@ -46,6 +48,7 @@ open Error inductive Result (α : Type u) where | ret (v: α): Result α | fail (e: Error): Result α + | div deriving Repr, BEq open Result @@ -53,20 +56,28 @@ open Result instance Result_Inhabited (α : Type u) : Inhabited (Result α) := Inhabited.mk (fail panic) +instance Result_Nonempty (α : Type u) : Nonempty (Result α) := + Nonempty.intro div + /- HELPERS -/ def ret? {α: Type} (r: Result α): Bool := match r with - | Result.ret _ => true - | Result.fail _ => false + | ret _ => true + | fail _ | div => false + +def div? {α: Type} (r: Result α): Bool := + match r with + | div => true + | ret _ | fail _ => false def massert (b:Bool) : Result Unit := - if b then .ret () else fail assertionFailure + if b then ret () else fail assertionFailure def eval_global {α: Type} (x: Result α) (_: ret? x): α := match x with - | Result.fail _ => by contradiction - | Result.ret x => x + | fail _ | div => by contradiction + | ret x => x /- DO-DSL SUPPORT -/ @@ -74,6 +85,7 @@ def bind (x: Result α) (f: α -> Result β) : Result β := match x with | ret v => f v | fail v => fail v + | div => div -- Allows using Result in do-blocks instance : Bind Result where @@ -92,8 +104,9 @@ instance : Pure Result where def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } := match o with - | .ret x => .ret ⟨x, rfl⟩ - | .fail e => .fail e + | ret x => ret ⟨x, rfl⟩ + | fail e => fail e + | div => div macro "let" e:term " ⟵ " f:term : doElem => `(doElem| let ⟨$e, h⟩ ← Result.attach $f) @@ -648,3 +661,5 @@ def vec_index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec /-- Aeneas-translated function -- useful to reduce non-recursive definitions. Use with `simp [ aeneas ]` -/ register_simp_attr aeneas + +end Primitives |