From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Mon, 7 Jul 2025 21:52:08 +0200
Subject: Initialize repository

---
 lib/mininix/run.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 lib/mininix/run.ml

(limited to 'lib/mininix/run.ml')

diff --git a/lib/mininix/run.ml b/lib/mininix/run.ml
new file mode 100644
index 0000000..f33bace
--- /dev/null
+++ b/lib/mininix/run.ml
@@ -0,0 +1,17 @@
+open Core
+
+(* The [n]th Church numeral *)
+let rec church n f x = if n <= 0 then x else church (n - 1) f (f x)
+
+let limited =
+  church 2048
+    (fun x -> Extraction.Internal.Datatypes.S x)
+    Extraction.Internal.Datatypes.O
+
+let rec infinity = Extraction.Internal.Datatypes.S infinity
+
+let interp ~fuel ~mode ~env e =
+  let mode : Extraction.mode =
+    match mode with `Shallow -> SHALLOW | `Deep -> DEEP
+  and fuel = match fuel with `Unlimited -> infinity | `Limited -> limited in
+  Extraction.interp' fuel mode env e
-- 
cgit v1.2.3