aboutsummaryrefslogtreecommitdiffstats
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