TermGenerator.ml 2.48 KB
Newer Older
POTTIER Francois's avatar
POTTIER Francois committed
1 2 3 4
(* TEMPORARY only 26 possible strings in [random_name]; fix that  *)
(* TEMPORARY alter the balance of lambda versus app in [generate] *)
(* TEMPORARY possibly implement shrinking *)

5 6
open Term

POTTIER Francois's avatar
POTTIER Francois committed
7 8 9
module StringSet =
  OST.Make(String)

10 11 12
module AtomSet =
  OST.Make(AlphaLib.Atom)

POTTIER Francois's avatar
POTTIER Francois committed
13 14
(* Randomly split an integer [n] into [n1 + n2]. *)

15 16 17 18 19 20 21 22
let split n =
  assert (n >= 0);
  let n1 = Random.int (n + 1) in
  let n2 = n - n1 in
  assert (0 <= n1 && n1 <= n);
  assert (0 <= n2 && n2 <= n);
  n1, n2

POTTIER Francois's avatar
POTTIER Francois committed
23 24 25
(* Randomly generate a name between "a" and "z". *)

let random_name () =
26 27 28 29
  let i = Random.int 26 in
  let c = Char.chr (Char.code 'a' + i) in
  String.make 1 c

30 31 32 33
(* Randomly generate a raw term whose free names are in the set [env]
   and whose size is exactly [n]. *)

let rec generate_raw env n =
34
  assert (n >= 0);
POTTIER Francois's avatar
POTTIER Francois committed
35
  assert (StringSet.cardinal env > 0);
36
  if n = 0 then
POTTIER Francois's avatar
POTTIER Francois committed
37
    TVar (StringSet.pick env)
38 39 40 41
  else
    match Random.int 2 with
    | 0 ->
        let n1, n2 = split (n - 1) in
42
        TApp (generate_raw env n1, generate_raw env n2)
43
    | 1 ->
44
        generate_raw_lambda env n
45 46 47
    | _ ->
        assert false

48 49
and generate_raw_lambda env n =
  assert (n > 0);
50
  let n = n - 1 in
POTTIER Francois's avatar
POTTIER Francois committed
51
  let x = random_name () in
52
  let env = StringSet.add x env in
53
  TLambda (x, generate_raw env n)
54

55 56 57
(* Randomly generate a closed raw term of size [n]. *)

let generate_raw n =
58 59
  assert (n > 0);
  (* Begin with [TLambda], so we have a nonempty [env]. *)
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
  generate_raw_lambda StringSet.empty n

(* Randomly generate a nominal term whose bound and free names are in the set [env]
   and whose size is [n]. *)

let rec generate_nominal env n =
  assert (n >= 0);
  assert (AtomSet.cardinal env > 0);
  if n = 0 then
    TVar (AtomSet.pick env)
  else
    match Random.int 2 with
    | 0 ->
        let n1, n2 = split (n - 1) in
        TApp (generate_nominal env n1, generate_nominal env n2)
    | 1 ->
        generate_nominal_lambda env n
    | _ ->
        assert false

and generate_nominal_lambda env n =
  assert (n > 0);
  let n = n - 1 in
  let x = AtomSet.pick env in
  TLambda (x, generate_nominal env n)

(* Generate a set of [k] fresh atoms. *)

let rec atoms accu k =
  if k = 0 then
    accu
  else
92
    let a = AlphaLib.Atom.fresh "a" in
93 94 95 96 97 98 99 100 101 102 103
    atoms (AtomSet.add a accu) (k - 1)

let atoms =
  atoms AtomSet.empty

(* Randomly generate a nominal term whose bound and free names are taken from a set
   of [k] fresh atoms and whose size is [n]. Note that this term does not satisfy
   the GUH. *)

let generate_nominal k n =
  generate_nominal (atoms k) n