From 59214186b817329342d9d72e23adf12f7a3b1348 Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Sat, 29 Jun 2024 21:31:22 +0200
Subject: had some fun writing an IsabelleHOL backend

(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)
---
 backends/IsabelleHOL/Primitives.thy | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 backends/IsabelleHOL/Primitives.thy

(limited to 'backends/IsabelleHOL/Primitives.thy')

diff --git a/backends/IsabelleHOL/Primitives.thy b/backends/IsabelleHOL/Primitives.thy
new file mode 100644
index 00000000..a0cc40bd
--- /dev/null
+++ b/backends/IsabelleHOL/Primitives.thy
@@ -0,0 +1,19 @@
+theory Primitives imports
+ Main
+ "HOL-Library.Monad_Syntax"
+begin
+
+
+datatype u32 = u32 nat
+datatype 'a result = Ok 'a | Err
+fun u32_lt :: "u32 \<Rightarrow> u32 \<Rightarrow> bool" where
+  "u32_lt (u32 a) (u32 b) = (a < b)"
+
+definition bind :: "'a result \<Rightarrow> ('a \<Rightarrow> 'b result) \<Rightarrow> 'b result" where
+ "bind m f \<equiv> (case m of Err \<Rightarrow> Err | Ok a \<Rightarrow> f a)"
+
+adhoc_overloading Monad_Syntax.bind bind
+
+declare bind_def[simp]
+
+end
\ No newline at end of file
-- 
cgit v1.2.3