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