1structure testutils :> testutils = 2struct 3 4open Lib Feedback 5 6datatype testresult = datatype Exn.result 7datatype die_mode = ProcessExit | FailException | Remember of int ref 8 9val linewidth = ref 80 10val output_linewidth = Holmake_tools.getWidth() 11 12fun is_result (Exn.Res _) = true 13 | is_result _ = false 14fun crush extra w s = 15 let 16 val exsize = UTF8.size extra 17 val desired_size = UTF8.size s + exsize 18 in 19 if desired_size <= w then 20 UTF8.padRight #" " w (s ^ extra) 21 else 22 UTF8.substring(s,0,w-exsize) ^ extra 23 end 24val rmNLs = String.translate (fn #"\n" => " " | c => str c) 25 26fun tprint s = print (crush " ... " (output_linewidth - 3) (rmNLs s)) 27 28fun printsize s = 29 let 30 fun normal c s = 31 case UTF8.getChar s of 32 NONE => c 33 | SOME ((_, 27), rest) => escape c rest 34 | SOME (_, rest) => normal (c + 1) rest 35 and escape c s = 36 case UTF8.getChar s of 37 NONE => c + 1 38 | SOME (("[", _), rest) => ANSIp c rest 39 | SOME (_, rest) => normal (c - 1) rest 40 (* bare escape consumes next 2, it seems *) 41 and ANSIp c s = (* ANSI parameters *) 42 case UTF8.getChar s of 43 NONE => c 44 | SOME ((_, i), rest) => 45 if 0x30 <= i andalso i <= 0x3F then ANSIp c rest 46 else ANSIib c s 47 and ANSIib c s = (* ANSI intermediate bytes *) 48 case UTF8.getChar s of 49 NONE => c 50 | SOME ((_, i), rest) => 51 if 0x20 <= i andalso i <= 0x2F then ANSIib c rest 52 else ANSIfinal c s 53 and ANSIfinal c s = (* ANSI final bytes *) 54 case UTF8.getChar s of 55 NONE => c 56 | SOME(_, rest) => normal c rest 57 in 58 normal 0 s 59 end 60 61fun tadd s = 62 let 63 val (pfx,sfx) = Substring.position "\n" (Substring.full s) 64 in 65 for_se 1 (printsize (Substring.string pfx)) (fn _ => print "\008"); 66 print s 67 end 68 69fun checkterm pfx s = 70 case OS.Process.getEnv "TERM" of 71 NONE => s 72 | SOME term => 73 if String.isPrefix "xterm" term then 74 pfx ^ s ^ "\027[0m" 75 else 76 s 77 78val bold = checkterm "\027[1m" 79val boldred = checkterm "\027[31m\027[1m" 80val boldgreen = checkterm "\027[32m\027[1m" 81val red = checkterm "\027[31m" 82val dim = checkterm "\027[2m" 83val clear = checkterm "\027[0m" 84 85val FAILEDstr = "\027[2CFAILED!" 86val diemode = ref ProcessExit 87val S = HOLPP.add_string 88fun pretty_die p = 89 (tadd (boldred FAILEDstr ^ "\n"); 90 HOLPP.prettyPrint (print, output_linewidth) p; 91 print "\n"; 92 case (!diemode) of 93 ProcessExit => OS.Process.exit OS.Process.failure 94 | FailException => raise (Fail ("DIE:" ^ HOLPP.pp_to_string 75 (K p) ())) 95 | Remember iref => (iref := !iref + 1)) 96fun die s = pretty_die (S s) 97fun OK () = print (boldgreen "OK" ^ "\n") 98fun exit_count0 iref = 99 OS.Process.exit 100 (if !iref = 0 then OS.Process.success 101 else 102 (print ("Failure count = " ^ Int.toString (!iref) ^ "\n"); 103 OS.Process.failure)) 104 105fun unicode_off f = Feedback.trace ("Unicode", 0) f 106fun raw_backend f = 107 Lib.with_flag (Parse.current_backend, PPBackEnd.raw_terminal) f 108 109fun quietly f = Feedback.quiet_messages (Feedback.quiet_warnings f) 110 111local 112 val pfxsize = size "Testing printing of ..." + 3 113 (* 3 for quotations marks and an extra space *) 114in 115fun standard_tpp_message s = let 116 open UTF8 117 fun trunc s = 118 if size s + pfxsize > output_linewidth - 18 then 119 let 120 val s' = substring(s,0,output_linewidth - 22 - pfxsize) 121 in 122 s' ^ " ..." 123 end 124 else s 125 fun pretty s = s |> String.translate (fn #"\n" => "\\n" | c => str c) 126 |> trunc 127in 128 "Testing printing of "^UnicodeChars.lsquo ^ pretty s ^ UnicodeChars.rsquo 129end 130end (* local *) 131 132exception InternalDie of HOLPP.pretty 133fun tppw width {input=s,output,testf} = let 134 val _ = tprint (testf s) 135 val t = Parse.Term [QUOTE s] 136 handle HOL_ERR _ => raise InternalDie (S "Parse failed!") 137 val res = HOLPP.pp_to_string width Parse.pp_term t 138 fun f s = String.translate 139 (fn #" " => UTF8.chr 0x2423 | #"\n" => "\n " | c => str c) s 140in 141 if res = output then OK() else 142 die (" Saw:\n >|" ^ clear (f res) ^ 143 "|<\n rather than \n >|" ^ clear (f output) ^ "|<\n") 144end handle InternalDie p => pretty_die p 145fun tpp s = tppw (!linewidth) {input=s,output=s,testf=standard_tpp_message} 146 147fun tpp_expected r = tppw (!linewidth) r 148 149fun timed f check x = 150 let 151 val cputimer = Timer.startCPUTimer() 152 val res = Res (f x) handle e => Exn e 153 val {nongc = {usr,...}, gc = {usr = gc,...}} = Timer.checkCPUTimes cputimer 154 val usr_s = "(" ^ Time.toString usr ^"s) " 155 val gc_s = if Time.toReal usr > 0.000001 andalso 156 Time.toReal gc / Time.toReal usr > 0.20 157 then 158 boldred ("[GC = " ^ Time.toString gc ^ "] ") 159 else "" 160 val _ = tadd (gc_s ^ usr_s) 161 in 162 check res 163 end 164 165fun exncheck f (Res a) = f a 166 | exncheck f (Exn e) = die (" Unexpected EXN:\n "^General.exnMessage e) 167 168fun convtest (nm,conv,tm,expected) = 169 let 170 open Term 171 val _ = tprint nm 172 fun c th = 173 let 174 val (l,r) = 175 let 176 val (eql, r) = dest_comb (Thm.concl th) 177 val (eq, l) = dest_comb eql 178 val _ = assert (same_const equality) eq 179 in 180 (l,r) 181 end handle e => 182 raise InternalDie 183 (S ("Didn't get equality; rather exn "^ 184 General.exnMessage e)) 185 open HOLPP 186 in 187 if aconv l tm then 188 if aconv r expected then OK() 189 else raise InternalDie (block CONSISTENT 2 [ 190 S "Got:", add_break(1,0), 191 Parse.pp_term r 192 ]) 193 else 194 raise InternalDie (block CONSISTENT 2 [ 195 S "Conv result LHS =", add_break(1,0), 196 Parse.pp_term l]) 197 end 198 in 199 timed conv (exncheck c) tm 200 end handle InternalDie p => pretty_die p 201 202fun check_HOL_ERRexn P e = 203 case e of 204 HOL_ERR{origin_structure,origin_function,message} => 205 P (origin_structure, origin_function, message) 206 | _ => false 207 208fun check_HOL_ERR P (Res _) = false 209 | check_HOL_ERR P (Exn e) = check_HOL_ERRexn P e 210 211fun is_struct_HOL_ERR st1 = check_HOL_ERRexn (fn (st2,_,_) => st1 = st2) 212fun check_result P (Res r) = P r 213 | check_result P _ = false 214 215 216 217fun require_msgk P pr f k x = 218 let 219 open HOLPP 220 fun idie s = raise InternalDie s 221 fun check res = 222 if P res then (OK(); res) 223 else 224 case res of 225 Exn e => idie ( 226 block CONSISTENT 0 [ 227 S " ", add_break(1,0), 228 block CONSISTENT 2[ 229 S "Unexpected exception:", add_break(1,0), 230 S (General.exnMessage e) 231 ] 232 ] 233 ) 234 | Res y => idie ( 235 block CONSISTENT 0 [ 236 S " ", add_break(1,0), 237 block CONSISTENT 2[ 238 S "Unexpected result:", add_break(1,0), 239 pr y 240 ] 241 ] 242 ) 243 val result = timed f check x 244 in 245 k result 246 end handle InternalDie p => pretty_die p 247fun require_pretty_msg P pr f x = require_msgk P pr f (fn _ => ()) x 248fun require_msg P pr = require_pretty_msg P (S o pr) 249fun require P f x = require_msg P (fn _ => "") f x 250 251fun shouldfail {printarg,testfn,printresult,checkexn} arg = 252 let 253 val _ = tprint (printarg arg) 254 fun check (Res r) = false 255 | check (Exn e) = checkexn e 256 in 257 require_msg check printresult testfn arg 258 end 259 260end (* struct *) 261