1open HolKernel boolLib
2
3open intSyntax
4
5val gen = Random.newgen ()
6
7val vars = map (fn s => mk_var(s, int_ty)) ["u", "v", "x", "y", "z"]
8
9fun gen_term v = let
10  val c = term_of_int (Arbint.fromInt (Random.range(~20, 21) gen))
11in
12  mk_mult(c, v)
13end
14
15fun gen_lhs() = list_mk_plus (map gen_term vars)
16
17fun gen_rhs() = term_of_int (Arbint.fromInt(Random.range(~100,101) gen))
18
19fun gen_atomic_formula () = let
20  val r = Random.random gen
21  val opn = if r < 0.33 then mk_eq else mk_less
22in
23  opn(gen_lhs(), gen_rhs())
24end
25
26fun gen_formula () = let
27  val r = Random.random gen
28in
29  if r < 0.65 then gen_atomic_formula()
30  else if r < 0.70 then mk_neg (gen_formula())
31  else if r < 0.80 then mk_conj (gen_formula(), gen_formula())
32  else if r < 0.90 then mk_disj (gen_formula(), gen_formula())
33  else mk_imp (gen_formula(), gen_formula())
34end
35
36val _ = Globals.show_types := true;
37fun gen n = if n <= 0 then ()
38            else (Parse.print_term (gen_formula());
39                  print "\n\n";
40                  gen (n - 1))
41
42fun die s = (TextIO.output(TextIO.stdErr, s);
43               TextIO.flushOut TextIO.stdErr;
44               Process.exit Process.failure);
45
46val numtoprint =
47  case CommandLine.arguments () of
48    [] => 10
49  | [x] => (let
50      val n = valOf (Int.fromString x)
51      val _ = n > 0 orelse raise Fail ""
52    in
53      n
54    end handle _ => die "Argument must be one positive integer\n")
55  | _ => die "Argument must be one positive integer\n"
56
57val _ = gen numtoprint
58