-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathgen_random_terms.ml
76 lines (72 loc) · 2.55 KB
/
gen_random_terms.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
let _ =
let _ = Random.self_init () in
let size = int_of_string Sys.argv.(1) in
let env_len = int_of_string Sys.argv.(2) in
let num_terms = int_of_string Sys.argv.(3) in
let target_file = Sys.argv.(4) in
let term_count_file =
open_in_bin (try Sys.argv.(5) with _ -> "data/term_counts")
in
let table : Common.ApproxNum.t array array = input_value term_count_file in
close_in term_count_file;
let max_size = Array.length table in
let max_env_len = Array.length table.(0) in
if size <= 0 then
raise(Invalid_argument "gen_random_terms: non-positive size");
if env_len < 0 then
raise(Invalid_argument "gen_random_terms: negative number of free variables");
if size >= max_size then
raise(Invalid_argument "gen_random_terms: size too large");
if env_len >= max_env_len then
raise(Invalid_argument "gen_random_terms: free variable number too large");
let exception Fail in
let rec gen size env_len =
let open Common.ApproxNum in
let open Common.Syntax in
match size with
| 1 ->
Idx(Random.int env_len)
| _ ->
let count = table.(size).(env_len) in
let p = Random.float 1. in
let nth = p *> count in
let n_lam =
if env_len + 1 < max_env_len
then table.(size - 1).(env_len + 1)
else of_int 0
in
if compare nth n_lam <= 0
then
Lam(gen (size - 1) (env_len + 1))
else if size > 2 then
let rec loop acc i =
let n_func = table.(i ).(env_len) in
let n_arg = table.(size - 1 - i).(env_len) in
let acc' = acc <+> (n_func <*> n_arg) in
if compare nth acc' <= 0
then App( gen i env_len
, gen (size - 1 - i) env_len )
else loop acc' (i + 1)
in
loop n_lam 1
else
raise Fail
in
let out = open_out target_file in
let rec loop i =
if i >= num_terms
then ()
else
let i' =
match gen size env_len with
| tm ->
let buf = Common.Syntax.serialize tm in
Buffer.output_buffer out buf;
i + 1
| exception Fail ->
i
in
loop i'
in
loop 1;
close_out out