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