summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/lean/Base/Primitives.lean2
-rw-r--r--backends/lean/Base/Primitives/Alloc.lean37
-rw-r--r--backends/lean/Base/Primitives/Base.lean4
-rw-r--r--backends/lean/Base/Primitives/CoreOpsDeref.lean18
4 files changed, 59 insertions, 2 deletions
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 6b7b0792..22378af7 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -2,3 +2,5 @@ import Base.Primitives.Base
import Base.Primitives.Scalar
import Base.Primitives.Array
import Base.Primitives.Vec
+import Base.Primitives.Alloc
+import Base.Primitives.CoreOpsDeref
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
new file mode 100644
index 00000000..0580421f
--- /dev/null
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -0,0 +1,37 @@
+import Lean
+import Base.Primitives.Base
+import Base.Primitives.CoreOpsDeref
+
+open Primitives
+open Result
+
+namespace alloc
+
+namespace boxed -- alloc.boxed
+
+namespace Box -- alloc.boxed.Box
+
+def deref (T : Type) (x : T) : Result T := ret x
+def deref_mut (T : Type) (x : T) : Result T := ret x
+def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x
+
+/-- Trait instance -/
+def coreOpsDerefInst (Self : Type) :
+ core.ops.deref.Deref Self := {
+ Target := Self
+ deref := deref Self
+}
+
+/-- Trait instance -/
+def coreOpsDerefMutInst (Self : Type) :
+ core.ops.deref.DerefMut Self := {
+ derefInst := coreOpsDerefInst Self
+ deref_mut := deref_mut Self
+ deref_mut_back := deref_mut_back Self
+}
+
+end Box -- alloc.boxed.Box
+
+end boxed -- alloc.boxed
+
+end alloc
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 7c0fa3bb..2bd081c0 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -120,8 +120,8 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
-- MISC --
----------
-@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x
-@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y
+@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : Result a := ret x
+@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : Result a := ret y
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
Use with `simp [ aeneas ]` -/
diff --git a/backends/lean/Base/Primitives/CoreOpsDeref.lean b/backends/lean/Base/Primitives/CoreOpsDeref.lean
new file mode 100644
index 00000000..2b540012
--- /dev/null
+++ b/backends/lean/Base/Primitives/CoreOpsDeref.lean
@@ -0,0 +1,18 @@
+import Lean
+import Base.Primitives.Base
+
+open Primitives
+open Result
+
+namespace core.ops.deref
+
+structure Deref (Self : Type) where
+ Target : Type
+ deref : Self → Result Target
+
+structure DerefMut (Self : Type) where
+ derefInst : Deref Self
+ deref_mut : Self → Result derefInst.Target
+ deref_mut_back : Self → derefInst.Target → Result Self
+
+end core.ops.deref