1structure MakeBigTerm =
2struct
3
4open HolKernel Random boolSyntax
5
6fun gen_ty gen = let
7  val n = Random.random gen
8in
9  if n < 0.1 then gen_ty gen --> gen_ty gen
10  else if n < 0.5 then bool
11  else if n < 0.9 then alpha
12  else beta
13end
14
15fun gen_var gen bvars tyr = let
16  val bvs = case tyr of NONE => bvars
17                      | SOME ty => List.filter (fn t => type_of t = ty) bvars
18in
19  if Random.random gen < 0.5 andalso not (null bvs) then
20    List.nth (bvs, Random.range(0, length bvs) gen)
21  else let
22      val ty = case tyr of NONE => gen_ty gen | SOME ty => ty
23    in
24      mk_var((if can dom_rng ty then "f" else "x")  ^
25             Int.toString (Random.range(0,25) gen), ty)
26    end
27end
28
29fun gen_term0 gen bvars sz tyrequired = let
30  val gt = gen_term0 gen bvars
31  fun rmk_comb sz tyr = let
32    val szs as (sz1, sz2) = (sz div 2, sz - sz div 2)
33    val (fsz, xsz) = if sz1 = sz2 then szs else
34                     if Random.random gen < 0.5 then (sz1, sz2) else (sz2, sz1)
35    val dom_ty = gen_ty gen
36    val rng_ty = case tyr of NONE => gen_ty gen  | SOME ty => ty
37  in
38    mk_comb(gt fsz (SOME (dom_ty --> rng_ty)), gt xsz (SOME dom_ty))
39  end
40in
41  case tyrequired of
42    NONE => let
43      val n = Random.random gen
44    in
45      if sz <= 1 then
46        if n < 0.1 then boolSyntax.F
47        else if n < 0.2 then boolSyntax.T
48        else if n < 0.3 then mk_arb (gen_ty gen)
49        else gen_var gen bvars NONE
50      else if sz = 2 then
51        if n < 0.7 then rmk_comb 2 NONE
52        else let
53            val bv = gen_var gen [] NONE
54          in
55            mk_abs(bv, gen_term0 gen (bv::bvars) 1 NONE)
56          end
57      else if n < 0.4 then let
58          val fsz = (sz - 1) div 2
59          val xsz = (sz - 1) - fsz
60          val opn = if n < 0.3 then mk_conj else mk_disj
61        in
62          opn(gt fsz (SOME bool), gt xsz (SOME bool))
63        end
64      else if n < 0.75 then rmk_comb sz NONE
65      else let
66          val bv = gen_var gen [] NONE
67        in
68          mk_abs(bv, gen_term0 gen (bv::bvars) (sz - 1) NONE)
69        end
70    end
71  | SOME ty => let
72      val n = Random.random gen
73    in
74      if sz = 1 then
75        if ty = bool then
76          if n < 0.15 then T
77          else if n < 0.30 then F
78          else gen_var gen bvars tyrequired
79        else if n < 0.3 then mk_arb ty
80        else gen_var gen bvars tyrequired
81      else
82        case Lib.total dom_rng ty of
83          NONE =>
84          if ty = bool andalso sz > 2 andalso n < 0.4 then let
85              val opn = if n < 0.3 then mk_conj else mk_disj
86              val arg1sz = (sz - 1) div 2
87              val arg2sz = (sz - 1) - arg1sz
88            in
89              opn (gt arg1sz (SOME bool), gt arg2sz (SOME bool))
90            end
91          else rmk_comb sz tyrequired
92        | SOME (d, r) =>
93          if n < 0.25 then let
94              val bv = gen_var gen [] (SOME d)
95            in
96              mk_abs(bv, gen_term0 gen (bv::bvars) (sz - 1) (SOME r))
97            end
98          else rmk_comb sz tyrequired
99    end
100end
101
102fun gen_term i sz = gen_term0 (Random.newgenseed i) [] sz NONE
103
104end
105