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