Initialize repository

1 files changed, 17 insertions, 0 deletions

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