eole_tester.ml

type term =
  | Var of string
  | Lam of string * term
  | App of term * term

module SMap = Map.Make(String)

type value =
  | Clos of string * term * env * (string * value) option ref
  | Freevar of string
  | StructApp of value * value
  | Lazy of term * env
  | Blackhole

and env = value ref SMap.t

let fresh = let r = ref 0 in fun prefix -> incr r; prefix ^ string_of_int !r

let evalcnt = ref 0

exception Timeout
let evalcnt_max = ref max_int

let makelazy t e =
  match t with
  | Var x -> SMap.find x e
  | _ -> ref (Lazy (t, e))

let rec eval t e deep_flag =
  incr evalcnt;
  if !evalcnt > !evalcnt_max then raise Timeout;
  match t with
  | App (t1, t2) ->
    begin match eval t1 e false with
      | Lazy _ | Blackhole -> assert false
      | Clos (x, t0, e0, _) ->
        eval t0 (SMap.add x (makelazy t2 e) e0) deep_flag
      | v -> StructApp (v, eval t2 e true)
    end
  | Lam (x, t) ->
    let z =
      if deep_flag then
        let z = fresh "_x" in
        Some (z, eval t (SMap.add x (ref (Freevar z)) e) true)
      else
        None
    in
    Clos (x, t, e, ref z)
  | Var x ->
    let u = SMap.find x e in
    if deep_flag then begin
      deepen u; !u
    end else begin
      force u
    end

and deepen v =
  match !v with
  | Blackhole -> assert false
  | Lazy (t, e) -> v := Blackhole; let r = eval t e true in v := r
  | Clos (x, t1, e1, n) when !n = None ->
    let z = fresh "_x" in
    n := Some (z, eval t1 (SMap.add x (ref (Freevar z)) e1) true)
  | _ -> ()

and force v =
  match !v with
  | Lazy (t, e) -> v := Blackhole; let r = eval t e false in v := r; r
  | _ -> !v

let run t =
  evalcnt := 0;
  let r = eval t SMap.empty true in
  r

let () = Random.init 42
let rec randterm n l =
  if n = 0 then
    if l = [] then Lam ("z", Var "z")
    else Var (List.nth l (Random.int (List.length l)))
  else if Random.int 1000 < 500 then
    let x = fresh "x" in Lam (x, randterm (n - 1) (x :: l))
  else
    let k = Random.int n in
    App (randterm k l, randterm (n - k - 1) l)

let rec print_eole_term ff t =
  match t with
  | Var x -> Format.fprintf ff "%sA" x
  | Lam (x, t) -> Format.fprintf ff "(%sA->%a)" x print_eole_term t
  | App (t1, t2) -> Format.fprintf ff "(%a %a)" print_eole_term t1 print_eole_term t2

let rec print_eole_result ff v =
  match v with
  | Lazy _ | Blackhole -> assert false
  | Freevar x -> Format.fprintf ff "%s" x
  | StructApp (v1, v2) ->
    Format.fprintf ff "(%a %a)" print_eole_result v1 print_eole_result v2
  | Clos (_, _, e, n) ->
    begin match !n with
      | None -> assert false
      | Some v ->
        Format.fprintf ff "(%s->%a)" (fst v) print_eole_result (snd v);
    end

let is_result_big r =
  let c = ref 0 in
  let rec aux v =
    if !c > 100000 then raise Exit;
    match v with
    | Freevar _ -> incr c
    | StructApp (v1, v2) -> incr c; aux v1; aux v2
    | Clos (_, _, _, n) -> (match !n with None -> assert false | Some v -> incr c; aux (snd v))
    | _ -> assert false
  in
  try aux r; false with Exit -> true

let eole_generate i t =
  let mxred = 100000 in
  let old = !evalcnt_max in
  evalcnt_max := mxred;
  begin match run t with
    | r ->
      if is_result_big r then
        Format.printf "Result too big to print@."
      else begin
        let f = open_out ("eole_test/test_" ^ string_of_int i ^ ".in") in
        Format.fprintf (Format.formatter_of_out_channel f) "%a.@." print_eole_term t;
        close_out f;
        let f = open_out ("eole_test/test_" ^ string_of_int i ^ ".out") in
        Format.fprintf (Format.formatter_of_out_channel f) "%a@." print_eole_result r;
        close_out f
      end
    | exception Timeout -> Format.printf "Timeout@."
  end;
  evalcnt_max := old

let () =
  for i = 1 to 10000 do
    eole_generate i (randterm 1000 []);
  done