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