aboutsummaryrefslogtreecommitdiffstats
path: root/lib/mininix/run.ml
blob: f33bace12ed4954ed408111b44e71c8e94147a53 (about) (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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