aboutsummaryrefslogtreecommitdiffstats
path: root/lib/mininix/run.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/mininix/run.ml')
-rw-r--r--lib/mininix/run.ml17
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 @@
1open Core
2
3(* The [n]th Church numeral *)
4let rec church n f x = if n <= 0 then x else church (n - 1) f (f x)
5
6let limited =
7 church 2048
8 (fun x -> Extraction.Internal.Datatypes.S x)
9 Extraction.Internal.Datatypes.O
10
11let rec infinity = Extraction.Internal.Datatypes.S infinity
12
13let interp ~fuel ~mode ~env e =
14 let mode : Extraction.mode =
15 match mode with `Shallow -> SHALLOW | `Deep -> DEEP
16 and fuel = match fuel with `Unlimited -> infinity | `Limited -> limited in
17 Extraction.interp' fuel mode env e