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