diff options
Diffstat (limited to 'lib/mininix/run.ml')
-rw-r--r-- | lib/mininix/run.ml | 17 |
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 @@ | |||
1 | open Core | ||
2 | |||
3 | (* The [n]th Church numeral *) | ||
4 | let rec church n f x = if n <= 0 then x else church (n - 1) f (f x) | ||
5 | |||
6 | let limited = | ||
7 | church 2048 | ||
8 | (fun x -> Extraction.Internal.Datatypes.S x) | ||
9 | Extraction.Internal.Datatypes.O | ||
10 | |||
11 | let rec infinity = Extraction.Internal.Datatypes.S infinity | ||
12 | |||
13 | let 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 | ||