1(* ========================================================================= *) 2(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6open Useful; 7 8(* ------------------------------------------------------------------------- *) 9(* The program name. *) 10(* ------------------------------------------------------------------------- *) 11 12val PROGRAM = "problems2tptp"; 13 14(* ------------------------------------------------------------------------- *) 15(* Problem data. *) 16(* ------------------------------------------------------------------------- *) 17 18use "problems.sml"; 19 20(* ------------------------------------------------------------------------- *) 21(* Helper functions. *) 22(* ------------------------------------------------------------------------- *) 23 24fun addSlash "" = "" 25 | addSlash dir = 26 if String.sub (dir, size dir - 1) = #"/" then dir 27 else dir ^ "/"; 28 29fun checkProblems (problems : problem list) = 30 let 31 fun dups [] = () 32 | dups [_] = () 33 | dups (x :: (xs as x' :: _)) = 34 if x <> x' then dups xs 35 else raise Error ("duplicate problem name: " ^ x) 36 37 val names = sort String.compare (List.map #name problems) 38 in 39 dups names 40 end; 41 42fun listProblem {name, comments = _, goal = _} = TextIO.print (name ^ "\n"); 43 44fun outputProblem outputDir {name,comments,goal} = 45 let 46 val filename = name ^ ".tptp" 47 val filename = 48 case outputDir of 49 NONE => filename 50 | SOME dir => addSlash dir ^ filename 51 52 val comment_bar = nChars #"-" 77 53 val comment_footer = 54 ["TPTP file created by " ^ host () ^ " at " ^ 55 time () ^ " on " ^ date () ^ "."] 56 val comments = 57 [comment_bar] @ 58 ["Name: " ^ name] @ 59 (if List.null comments then [] else "" :: comments) @ 60 (if List.null comment_footer then [] else "" :: comment_footer) @ 61 [comment_bar] 62 63 val includes = [] 64 65 val formulas = 66 let 67 val name = Tptp.FormulaName "goal" 68 val role = Tptp.ConjectureRole 69 val body = Tptp.FofFormulaBody (Formula.parse goal) 70 val source = Tptp.NoFormulaSource 71 in 72 [Tptp.Formula 73 {name = name, 74 role = role, 75 body = body, 76 source = source}] 77 end 78 79 val problem = 80 Tptp.Problem 81 {comments = comments, 82 includes = includes, 83 formulas = formulas} 84 85 val mapping = Tptp.defaultMapping 86 87 val () = 88 Tptp.write 89 {problem = problem, 90 mapping = mapping, 91 filename = filename} 92 in 93 () 94 end; 95 96(* ------------------------------------------------------------------------- *) 97(* Program options. *) 98(* ------------------------------------------------------------------------- *) 99 100datatype mode = OutputMode | ListMode; 101 102val MODE : mode ref = ref OutputMode; 103 104val COLLECTION : string option ref = ref NONE; 105 106val OUTPUT_DIRECTORY : string option ref = ref NONE; 107 108local 109 open Useful Options; 110in 111 val specialOptions = 112 [{switches = ["--collection"], arguments = ["C"], 113 description = "restrict to the problems in collection C", 114 processor = 115 beginOpt 116 (stringOpt endOpt) 117 (fn _ => fn c => COLLECTION := SOME c)}, 118 {switches = ["--list"], arguments = [], 119 description = "just list the problems", 120 processor = beginOpt endOpt (fn _ => MODE := ListMode)}, 121 {switches = ["--output-dir"], arguments = ["DIR"], 122 description = "the output directory", 123 processor = 124 beginOpt 125 (stringOpt endOpt) 126 (fn _ => fn d => OUTPUT_DIRECTORY := SOME d)}]; 127end; 128 129val VERSION = "1.0"; 130 131val versionString = PROGRAM^" v"^VERSION^"\n"; 132 133val programOptions = 134 {name = PROGRAM, 135 version = versionString, 136 header = "usage: "^PROGRAM^" [option ...]\n" ^ 137 "Outputs the set of sample problems in TPTP format.\n", 138 footer = "", 139 options = specialOptions @ Options.basicOptions}; 140 141fun succeed () = Options.succeed programOptions; 142fun fail mesg = Options.fail programOptions mesg; 143fun usage mesg = Options.usage programOptions mesg; 144 145val (opts,work) = 146 Options.processOptions programOptions (CommandLine.arguments ()); 147 148val () = if List.null work then () else usage "too many arguments"; 149 150(* ------------------------------------------------------------------------- *) 151(* Top level. *) 152(* ------------------------------------------------------------------------- *) 153 154val () = 155let 156 val problems = 157 case !COLLECTION of 158 NONE => problems 159 | SOME c => List.filter (isCollection c) problems 160 161 val () = checkProblems problems 162 163 val () = 164 case !MODE of 165 ListMode => app listProblem problems 166 | OutputMode => app (outputProblem (!OUTPUT_DIRECTORY)) problems 167in 168 succeed () 169end 170handle Error s => die (PROGRAM^" failed:\n" ^ s) 171 | Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s); 172