1open HolKernel boolLib
2
3open numSyntax
4
5val gen = Random.newgen ()
6
7val vars = map (fn s => mk_var(s, num)) ["u", "v", "x", "y", "z"]
8
9fun gen_term() = let
10  val r = Random.random gen
11in
12  if r < 0.2 then mk_plus(gen_term(), gen_term())
13  else if r < 0.4 then mk_suc(gen_term())
14  else if r < 0.6 then zero_tm
15  else List.nth(vars, floor ((r - 0.6) / 0.08))
16end
17
18fun gen_atomic_formula () = let
19  val r = Random.random gen
20in
21  if r < 0.2 then mk_eq(gen_term(), gen_term())
22  else if r < 0.4 then mk_less(gen_term(), gen_term())
23  else if r < 0.6 then mk_greater(gen_term(), gen_term())
24  else if r < 0.8 then mk_geq(gen_term(), gen_term())
25  else mk_leq(gen_term(), gen_term())
26end
27
28fun gen_formula () = let
29  val r = Random.random gen
30in
31  if r < 0.75 then gen_atomic_formula()
32  else if r < 0.85 then mk_neg (gen_formula())
33  else if r < 0.90 then mk_conj (gen_formula(), gen_formula())
34  else if r < 0.95 then mk_disj (gen_formula(), gen_formula())
35  else mk_imp (gen_formula(), gen_formula())
36end
37
38val _ = Globals.show_types := true;
39fun gen n = if n <= 0 then ()
40            else (Parse.print_term (gen_formula());
41                  print "\n\n";
42                  gen (n - 1))
43
44fun die s = (TextIO.output(TextIO.stdErr, s);
45               TextIO.flushOut TextIO.stdErr;
46               Process.exit Process.failure);
47
48val numtoprint =
49  case CommandLine.arguments () of
50    [] => 10
51  | [x] => (let
52      val n = valOf (Int.fromString x)
53      val _ = n > 0 orelse raise Fail ""
54    in
55      n
56    end handle _ => die "Argument must be one positive integer\n")
57  | _ => die "Argument must be one positive integer\n"
58
59val _ = gen numtoprint
60