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