1open HolKernel Parse boolTheory boolLib pairTheory 2open constrFamiliesLib patternMatchesLib computeLib 3open quantHeuristicsLib simpLib boolSimps listTheory 4open BasicProvers 5open testutils 6 7 8val hard_fail = true; 9val _ = really_die := true; 10val quiet = false; 11val _ = Parse.current_backend := PPBackEnd.vt100_terminal; 12 13(* For manual 14 15set_trace "use pmatch_pp" 0 16val hard_fail = false; 17val _ = really_die := false; 18val quiet = false; 19val _ = Parse.current_backend := PPBackEnd.emacs_terminal; 20 21*) 22val _ = patternMatchesLib.ENABLE_PMATCH_CASES (); 23val list_ss = numLib.arith_ss ++ listSimps.LIST_ss 24 25fun test_gen print_inp print_res print_out check_res s f (inp, out_opt) = 26let 27 open PPBackEnd Parse 28 val _ = print (if quiet then "" else "Testing "^s^" "); 29 val _ = print_inp inp; 30 val _ = print ("\n "); 31 val ct = Timer.startCPUTimer(); 32 val res_opt = SOME (f inp) handle Interrupt => raise Interrupt 33 | _ => NONE; 34 35 val ok = if not (isSome out_opt) then not (isSome res_opt) else 36 isSome res_opt andalso 37 ( 38 check_res (inp, (valOf out_opt), (valOf res_opt)) 39 ) handle HOL_ERR _ => false 40 val quiet = quiet andalso ok 41 val _ = if ok then 42 print_with_style [FG Green] "OK " 43 else 44 (print_with_style [FG OrangeRed] "FAILED ") 45 46 val d_time = #usr (Timer.checkCPUTimer ct); 47 val _ = print ((Time.toString d_time)^ " s"); 48 val _ = if quiet then () else print ("\n "); 49 50 val _ = if quiet then () else 51 let 52 val _ = print "---> "; 53 val _ = if isSome res_opt then (print_res (valOf res_opt);print "\n") 54 else print "-\n" 55 val _ = if (not ok) then 56 (print " EXPECTED "; 57 if isSome out_opt then (print_out (valOf out_opt);print "\n") 58 else print "-\n") 59 else () 60 in () end 61 val _ = print "\n"; 62 val _ = if (not ok andalso hard_fail) then Process.exit Process.failure else (); 63in 64 () 65end; 66 67fun print_term' t = (print UnicodeChars.ldquo; 68 print (ppstring pp_term t); 69 print UnicodeChars.rdquo); 70fun print_thm' t = print (ppstring pp_thm t); 71 72val test_term_thm_gen = test_gen print_term' print_thm' print_term' 73 74val test_conv = test_term_thm_gen (fn (inp, out, res) => let 75 val (l, r) = dest_eq (concl res) 76in 77 (aconv l inp andalso aconv r out) 78end) 79 80 81(* ---------------------------------------------------------------------- 82 Parser 83 ---------------------------------------------------------------------- *) 84 85fun pel2string [] = "" 86 | pel2string (pLeft::rest) = "L" ^ pel2string rest 87 | pel2string (pRight::rest) = "R" ^ pel2string rest 88 | pel2string (pAbs::rest) = "A" ^ pel2string rest 89fun d2string (p,t1,t2) = 90 " " ^ 91 trace ("types", 1) term_to_string t1 ^ " - " ^ 92 trace ("types", 1) term_to_string t2 ^ 93 " (" ^ pel2string p ^ ")\n" 94 95fun test(inp, expected) = 96 let 97 val _ = tprint ("Parsing "^inp) 98 val tm = Parse.Term [QUOTE inp] 99 in 100 if aconv tm expected then OK() 101 else 102 let 103 val diffs = term_diff expected tm 104 in 105 die ("FAILED!\n" ^ String.concat (map d2string diffs)) 106 end 107 end 108 109val _ = app test [ 110 ("case b of T => F | F => T", 111 ``PMATCH (b:bool) [PMATCH_ROW (\u:one. T) (\u:one. T) (\u:one. F); 112 PMATCH_ROW (\u:one. F) (\u:one. T) (\u:one. T)]``), 113 114 ("case x of 0 => 3 | SUC n => n + 1", 115 ``PMATCH x [PMATCH_ROW (\u:one. 0) (\u:one. T) (\u:one. 3); 116 PMATCH_ROW (\n. SUC n) (\n:num. T) (\n. n + 1)]``), 117 118 ("case x of 0 => 3 | SUC _ => 4", 119 ``PMATCH x [PMATCH_ROW (\u:one. 0) (\u:one. T) (\u:one. 3); 120 PMATCH_ROW (\n:num. SUC n) (\n:num. T) (\n:num. 4)]``), 121 122 ("case (x : bool list) of [] => F | (x,xs) .| x::xs => x", 123 ``PMATCH x [PMATCH_ROW (\u:one. []:bool list) (\u:one. T) (\u:one. F); 124 PMATCH_ROW (\ (x:bool,xs:bool list). x::xs) 125 (\ (x:bool,xs:bool list). T) 126 (\ (x:bool,xs:bool list). x)]``), 127 128 ("(n:num) + case m of 0 => 3 | () .| SUC n => 10 | z => z", 129 ``(n:num) + 130 PMATCH m [PMATCH_ROW (\u:one. 0n) (\u:one. T) (\u:one. 3n); 131 PMATCH_ROW (\u:one. SUC n) (\u:one. T) (\u:one. 10); 132 PMATCH_ROW (\z:num. z) (\z:num. T) (\z:num. z)]``), 133 134 ("case x of 0 => 3 | () .| n => 4 | _ => 100", 135 ``PMATCH (x:num) [PMATCH_ROW (\u:one. 0n) (\u:one. T) (\u:one. 3n); 136 PMATCH_ROW (\u:one. n:num) (\u:one. T) (\u:one. 4n); 137 PMATCH_ROW (\x:num. x) (\x:num. T) (\x:num. 100n)]``), 138 139 ("n + case b of T => 1 | n => 2", 140 ``n + PMATCH (b:bool) 141 [PMATCH_ROW (\u:one. T) (\u:one. T) (\u:one. 1n); 142 PMATCH_ROW (\n:bool. n) (\n:bool. T) (\n:bool. 2n)]``), 143 144 ("n + case x of 0 => 1 | m .| m + n => m * 2", 145 ``n + PMATCH (x:num) 146 [PMATCH_ROW (\u:one. 0) (\u:one. T) (\u:one. 1); 147 PMATCH_ROW (\m:num. m + n) (\m:num. T) (\m:num. m * 2)]``), 148 149 ("case x of 0 => 3 | () .| n => 4 | x => 100", 150 ``PMATCH (x:num) [PMATCH_ROW (\u:one. 0n) (\u:one. T) (\u:one. 3n); 151 PMATCH_ROW (\u:one. n:num) (\u:one. T) (\u:one. 4n); 152 PMATCH_ROW (\x:num. x) (\x:num. T) (\x:num. 100n)]``), 153 154 ("case (y,x) of\ 155 \ | (NONE,[]) => 0\ 156 \ | (NONE,[T]) => 1\ 157 \ | (SOME T,[]) => 2\ 158 \ | (SOME _, _) => 3\ 159 \ | z .| (SOME _, z) => 4\ 160 \ | (z1, z2:'a) .| (SOME _, z1) => 5\ 161 \ | z .| (SOME T, z) when LENGTH x > 5 => 6\ 162 \ | (z1, z2, z3:'b list) .| (SOME z1, z2) when LENGTH z3 > 5 => 7", 163 ``PMATCH ((y :bool option),(x :bool list)) 164 [PMATCH_ROW (\_uv :unit. (NONE :bool option,[] :bool list)) 165 (\_uv :unit. T) 166 (\_uv :unit. 0n); 167 PMATCH_ROW (\_uv :unit. (NONE :bool option,[T])) 168 (\_uv:unit. T) 169 (\_uv:unit. 1n); 170 PMATCH_ROW (\_uv:unit. (SOME T, [] :bool list)) (\_uv:unit. T) 171 (\_uv :unit. 2n); 172 PMATCH_ROW (\ ((xx :bool),(yy :bool list)). (SOME xx,yy)) 173 (\ ((xx :bool),(yy :bool list)). T) 174 (\ ((xx :bool),(yy :bool list)). 3n); 175 PMATCH_ROW (\ ((z :bool list),(u2 :bool)). (SOME u2,z)) 176 (\ ((z :bool list),(u2 :bool)). T) 177 (\ ((z :bool list),(u2 :bool)). 4n); 178 PMATCH_ROW (\ (z1 :bool list, (z2 :'a, u3 :bool)). (SOME u3,z1)) 179 (\ (z1 :bool list, (z2 :'a, u3 :bool)). T) 180 (\ (z1 :bool list, (z2 :'a, u3 :bool)). 5n); 181 PMATCH_ROW (\ (z :bool list). (SOME T,z)) 182 (\ (z :bool list). LENGTH x > 5n) 183 (\ (z :bool list). 6n); 184 PMATCH_ROW 185 (\ ((z1 :bool),(z2 :bool list),(z3 :'b list)). (SOME z1,z2)) 186 (\ ((z1 :bool),(z2 :bool list),(z3 :'b list)). LENGTH z3 > 5n) 187 (\ ((z1 :bool),(z2 :bool list),(z3 :'b list)). 7n)]``), 188 189 ("case x of NONE => y | SOME (z:'foo) => (f z : 'bar)", 190 ``PMATCH (x:'foo option) [ 191 PMATCH_ROW (\_uv:unit. NONE) (\_uv:unit. T) (\_uv:unit. y:'bar); 192 PMATCH_ROW (\z:'foo. SOME z) (\z:'foo. T) (\z:'foo. f z : 'bar) 193 ]``), 194 195 ("case x of NONE => y | z:'foo .| SOME z => (f z : 'bar)", 196 ``PMATCH (x:'foo option) [ 197 PMATCH_ROW (\_uv:unit. NONE) (\_uv:unit. T) (\_uv:unit. y:'bar); 198 PMATCH_ROW (\z:'foo. SOME z) (\z:'foo. T) (\z:'foo. f z : 'bar) 199 ]``), 200 201 ("dtcase x of NONE => 3 | SOME y => y + 1", 202 ``option_CASE (x : num option) 3n (\z:num. z + 1)``) 203 204] 205 206fun shouldfail s = let 207 val _ = tprint ("Should NOT parse: " ^ s) 208in 209 case Lib.total (trace ("show_typecheck_errors", 0) Parse.Term) [QUOTE s] of 210 NONE => OK() 211 | SOME t => die ("FAILED!\n Parsed to: " ^ term_to_string t) 212end 213 214 215val _ = app shouldfail [ 216 "case x of NONE => F | y .| SOME(x,y) => x < y" 217] 218 219(* ---------------------------------------------------------------------- 220 Pretty-printer 221 ---------------------------------------------------------------------- *) 222 223val _ = app (raw_backend tpp) [ 224 "case x of 0 => 3 | SUC n => n", 225 "dtcase x of 0 => 3 | SUC n => n", 226 "(case x of 0 => 3 | SUC n => n) > 5", 227 "(dtcase x of 0 => 3 | SUC n => n) = 3", 228 "case SUC 5 of 0 => 3 | SUC n => n", 229 "dtcase SUC (SUC 5) of 0 => 3 | SUC n => n", 230 "case x of 0 => 4 | SUC _ => 10", 231 "case (x,y) of (NONE,_) => 10 | (SOME n,0) when n < 10 => 11", 232 "case x of 0 => 3 | () .| n => 4 | x => 100", 233 "case x of NONE => 3 | () .| SOME n => n | SOME x => x + 1", 234 "dtcase (x,y) of (NONE,z) => SUC z | (SOME n,z) => n", 235 "SUC (case x of 0 => 3 | SUC n => n)", 236 "SUC (dtcase x of 0 => 3 | SUC n => n)", 237 "case x of z .| 0 => z | SUC _ => 10", 238 "case x of (z,y) .| 0 => z | SUC _ => 10" 239] 240 241 242(******************************************************************************) 243(* Converting from existing decision trees *) 244(******************************************************************************) 245 246val tc = test_conv "PMATCH_INTRO_CONV" PMATCH_INTRO_CONV 247 248val t = ``dtcase x of (NONE, []) => 0``; 249val r_thm = SOME ``PMATCH (x :'a option # 'b list) 250 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),([] :'b list))) 251 (\(_uv :unit). T) (\(_uv :unit). (0 :num))]`` 252val _ = tc (t, r_thm); 253 254val t = ``dtcase x of 255 (NONE, []) => 0 256 | (SOME 2, []) => 2 257 | (SOME 3, (x :: xs)) => 3 + x 258 | (SOME _, (x :: xs)) => x`` 259val r_thm = SOME ``PMATCH x 260 [PMATCH_ROW (\(_uv :unit). ((NONE :num option),([] :num list))) 261 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 262 PMATCH_ROW (\(_uv :unit). (SOME (2 :num),([] :num list))) 263 (\(_uv :unit). T) (\(_uv :unit). (2 :num)); 264 PMATCH_ROW (\((x :num),(_0 :num list)). (SOME (3 :num),x::_0)) 265 (\((x :num),(_0 :num list)). T) 266 (\((x :num),(_0 :num list)). (3 :num) + x); 267 PMATCH_ROW (\((_0 :num),(x :num),(_1 :num list)). (SOME _0,x::_1)) 268 (\((_0 :num),(x :num),(_1 :num list)). T) 269 (\((_0 :num),(x :num),(_1 :num list)). x)]`` 270val _ = tc (t, r_thm); 271 272 273 274 275val tcn = test_conv "PMATCH_INTRO_CONV_NO_OPTIMISE" PMATCH_INTRO_CONV_NO_OPTIMISE 276 277val t = ``dtcase x of (NONE, []) => 0`` 278val r_thm = SOME ``PMATCH x 279 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),([] :'b list))) 280 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 281 PMATCH_ROW (\((v4 :'b),(v5 :'b list)). ((NONE :'a option),v4::v5)) 282 (\((v4 :'b),(v5 :'b list)). T) 283 (\((v4 :'b),(v5 :'b list)). (ARB :num)); 284 PMATCH_ROW (\((v2 :'a),(v1 :'b list)). (SOME v2,v1)) 285 (\((v2 :'a),(v1 :'b list)). T) 286 (\((v2 :'a),(v1 :'b list)). (ARB :num))]`` 287val _ = tcn (t, r_thm); 288 289val t = ``dtcase x of 290 (NONE, []) => 0 291 | (SOME 2, []) => 2 292 | (SOME 3, (x :: xs)) => 3 + x 293 | (SOME _, (x :: xs)) => x`` 294val r_thm = SOME `` 295 PMATCH x 296 [PMATCH_ROW (\(_uv :unit). ((NONE :num option),([] :num list))) 297 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 298 PMATCH_ROW (\(_uv :unit). (SOME (2 :num),([] :num list))) 299 (\(_uv :unit). T) (\(_uv :unit). (2 :num)); 300 PMATCH_ROW (\(v5 :num). (SOME v5,([] :num list))) (\(v5 :num). T) 301 (\(v5 :num). (ARB :num)); 302 PMATCH_ROW 303 (\((x :num),(xs :num list)). ((NONE :num option),x::xs)) 304 (\((x :num),(xs :num list)). T) 305 (\((x :num),(xs :num list)). (ARB :num)); 306 PMATCH_ROW (\((x :num),(xs :num list)). (SOME (3 :num),x::xs)) 307 (\((x :num),(xs :num list)). T) 308 (\((x :num),(xs :num list)). (3 :num) + x); 309 PMATCH_ROW 310 (\((v12 :num),(x :num),(xs :num list)). (SOME v12,x::xs)) 311 (\((v12 :num),(x :num),(xs :num list)). T) 312 (\((v12 :num),(x :num),(xs :num list)). x)]`` 313val _ = tcn (t, r_thm); 314 315 316val t = ``dtcase x of 0 => 0 | SUC x => if (x+1 = 2) then 1 else 2``; 317val r_thm = SOME ``case x of 0 => 0 | SUC x => (if x + 1 = 2 then 1 else 2)`` 318val _ = tc (t, r_thm); 319 320 321(******************************************************************************) 322(* Simplification *) 323(******************************************************************************) 324 325val test = test_conv "PMATCH_CLEANUP_PVARS_CONV" PMATCH_CLEANUP_PVARS_CONV (``PMATCH (x:('b # 'c) option) [ 326 PMATCH_ROW (\x:'a. NONE) (\x. T) (\x. 5); 327 PMATCH_ROW (\ (x,y). SOME (x,z)) (\ (x,y). T) (\ (x,y). 8); 328 PMATCH_ROW (\ (x,z). SOME (x,z)) (\_. T) (\ (a,y). 8)]``, 329SOME ``PMATCH (x:('b # 'c) option) 330 [PMATCH_ROW (\_uv:unit. NONE) (\_uv. T) (\_uv. 5); 331 PMATCH_ROW (\x. SOME (x,z)) (\x. T) (\x. 8); 332 PMATCH_ROW (\(x,z). SOME (x,z)) (\(x,z). T) (\(x,z). 8)]``) 333 334val test = test_conv "PMATCH_EXPAND_COLS_CONV" PMATCH_EXPAND_COLS_CONV (``PMATCH (x,y,z) 335 [PMATCH_ROW (\y. (0,y,T)) (\y. T) (\y. y); 336 PMATCH_ROW (\xyz. xyz) (\xyz. ~SND (SND xyz)) (\xyz. 2); 337 PMATCH_ROW (\(x,yz). (x,yz)) (\(x,yz). T) (\(x,yz). x)]``, 338SOME ``PMATCH (x,y,z) 339 [PMATCH_ROW (\y. (0,y,T)) (\y. T) (\y. y); 340 PMATCH_ROW (\(xyz_0,xyz_1,xyz_2). (xyz_0,xyz_1,xyz_2)) 341 (\(xyz_0,xyz_1,xyz_2). ~SND (SND (xyz_0,xyz_1,xyz_2))) 342 (\(xyz_0,xyz_1,xyz_2). 2); 343 PMATCH_ROW (\(x,yz_0,yz_1). (x,yz_0,yz_1)) (\(x,yz_0,yz_1). T) 344 (\(x,yz_0,yz_1). x)]``) 345 346val test = test_conv "PMATCH_EXPAND_COLS_CONV" PMATCH_EXPAND_COLS_CONV (``case xy of 347 | (SOME x, SOME y) => SOME (x + y) 348 | _ => NONE``, SOME (``case xy of 349 (SOME x,SOME y) => SOME (x + y) | (_,_) => NONE``)) 350 351val test = test_conv "PMATCH_EXPAND_COLS_CONV" PMATCH_EXPAND_COLS_CONV (``case (x,y) of 352 | (SOME x, SOME y) => SOME (x + y) 353 | _ => NONE``, SOME (`` 354 case (x,y) of 355 (SOME x,SOME y) => SOME (x + y) | (_,_) => NONE``)) 356 357val test = test_conv "PMATCH_INTRO_WILDCARDS_CONV" PMATCH_INTRO_WILDCARDS_CONV (``PMATCH (x,y,z) 358 [PMATCH_ROW (\(_x,y,z). (_x,y,z)) (\(_x,y,z). T) (\(_x,y,z). _x + y); 359 PMATCH_ROW (\(x,y,z). (x,y,z)) (\(x,y,z). z) (\(x,y,z). x)]``, SOME ``PMATCH (x,y,z) 360 [PMATCH_ROW (\(x,y,_0). (x,y,_0)) (\(x,y,_0). T) 361 (\(x,y,_0). x + y); 362 PMATCH_ROW (\(x,_0,z). (x,_0,z)) (\(x,_0,z). z) (\(x,_0,z). x)]``) 363 364 365val test = test_conv "PMATCH_CLEANUP_CONV" PMATCH_CLEANUP_CONV (``case (SUC x) of 366 x => x + 5``, SOME ``SUC x + 5``) 367 368val test = test_conv "PMATCH_CLEANUP_CONV" PMATCH_CLEANUP_CONV (``case (SOME (x:'a),y) of 369 (NONE, y) => 0 370 | (x, 0) => 1 371 | (SOME x, y) => 2 372 | (x, y) => 3``, SOME `` PMATCH (SOME (x:'a),y) 373 [PMATCH_ROW (\x. (x,0)) (\x. T) (\x. 1); 374 PMATCH_ROW (\(x,y). (SOME x,y)) (\(x,y). T) (\(x,y). 2)]``) 375 376val test = test_conv "PMATCH_CLEANUP_CONV" PMATCH_CLEANUP_CONV (``case (SOME (x:'a),y) of 377 (NONE, y) => 0 378 | (SOME x, y) => 2 379 | (x, y) => 3``, SOME ``2``) 380 381val test = test_conv "PMATCH_SIMP_COLS_CONV" PMATCH_SIMP_COLS_CONV (``case (SOME x,y) of 382 | (SOME x, 1) => x+y 383 | (x, y) => 3``, SOME ``PMATCH y 384 [PMATCH_ROW (\(_uv:unit). 1) (\_uv. T) (\_uv. x + y); 385 PMATCH_ROW (\y. y) (\y. T) (\y. 3)]``) 386 387val test = test_conv "PMATCH_SIMP_COLS_CONV" PMATCH_SIMP_COLS_CONV (``case (SOME x,y) of 388 | (SOME x, 1) => x+y 389 | (SOME 2, 2) => y 390 | (x, y) => 3``, SOME ``PMATCH (x,y) 391 [PMATCH_ROW (\x. (x,1)) (\x. T) (\x. x + y); 392 PMATCH_ROW (\(_uv:unit). (2,2)) (\_uv. T) (\_uv. y); 393 PMATCH_ROW (\(x_0,y). (x_0,y)) (\(x_0,y). T) (\(x_0,y). 3)]``) 394 395 396val test = test_conv "PMATCH_REMOVE_FAST_REDUNDANT_CONV" PMATCH_REMOVE_FAST_REDUNDANT_CONV (``case xy of 397 | (SOME x, y) => 1 398 | (SOME 2, 3) => 2 399 | (NONE, y) => 3 400 | (NONE, y) => 4 401 | (x, 5) => 5``, SOME `` 402 case xy of 403 | (SOME (x:num), y) => 1 404 | (NONE, y) => 3 405 | (x, 5) => 5``) 406 407val test = test_conv "PMATCH_REMOVE_REDUNDANT_CONV" PMATCH_REMOVE_REDUNDANT_CONV (``case xy of 408 | (SOME x, y) => 1 409 | (SOME 2, 3) => 2 410 | (NONE, y) => 3 411 | (NONE, y) => 4 412 | (x, 5) => 5``, SOME `` 413 case xy of 414 | (SOME (x:num), (y:num)) => 1 415 | (NONE, y) => 3``) 416 417 418val test = test_conv "PMATCH_REMOVE_FAST_SUBSUMED_CONV true" (PMATCH_REMOVE_FAST_SUBSUMED_CONV true) (``case xy of 419 | (SOME 2, _) => 2 420 | (NONE, 3) => 1 421 | (SOME x, _) => x 422 | (NONE, y) => y 423 | (x, 5) => ARB``, SOME 424``case xy of 425 | (NONE, 3) => 1 426 | (SOME x, _) => x 427 | (NONE, y) => y``) 428 429val test = test_conv "PMATCH_REMOVE_FAST_SUBSUMED_CONV false" (PMATCH_REMOVE_FAST_SUBSUMED_CONV false) (``case xy of 430 | (SOME 2, _) => 2 431 | (NONE, 3) => 1 432 | (SOME x, _) => x 433 | (NONE, y) => y 434 | (x, 5) => ARB``, SOME 435``case xy of 436 | (NONE, 3) => 1 437 | (SOME x, _) => x 438 | (NONE, y) => y 439 | (x, 5) => ARB``) 440 441val test = test_conv "PMATCH_SIMP_CONV" PMATCH_SIMP_CONV 442val test_fast = test_conv "PMATCH_FAST_SIMP_CONV" PMATCH_FAST_SIMP_CONV 443 444val t = 445 ``PMATCH ((a :num option),(x :num),(xs :num list)) 446 [PMATCH_ROW (\(_0 :num). ((NONE :num option),_0,([] :num list))) 447 (\(_0 :num). T) (\(_0 :num). (0 :num)); 448 PMATCH_ROW (\(x :num). ((NONE :num option),x,([] :num list))) 449 (\(x :num). x < (10 :num)) (\(x :num). x); 450 PMATCH_ROW (\(x :num). ((NONE :num option),x,[(2 :num)])) 451 (\(x :num). T) (\(x :num). x); 452 PMATCH_ROW (\((x :num),(v18 :num)). ((NONE :num option),x,[v18])) 453 (\((x :num),(v18 :num)). T) (\((x :num),(v18 :num)). (3 :num)); 454 PMATCH_ROW 455 (\((_3 :num),(_2 :num),(_1 :num)). 456 ((NONE :num option),_1,[_2; _3])) 457 (\((_3 :num),(_2 :num),(_1 :num)). T) 458 (\((_3 :num),(_2 :num),(_1 :num)). x); 459 PMATCH_ROW 460 (\((x :num),(v12 :num),(v16 :num),(v17 :num list)). 461 ((NONE :num option),x,v12::v16::v17)) 462 (\((x :num),(v12 :num),(v16 :num),(v17 :num list)). T) 463 (\((x :num),(v12 :num),(v16 :num),(v17 :num list)). (3 :num)); 464 PMATCH_ROW (\((y :num),(x :num),(z :num),(zs :'a)). (SOME y,x,[z])) 465 (\((y :num),(x :num),(z :num),(zs :'a)). T) 466 (\((y :num),(x :num),(z :num),(zs :'a)). x + (5 :num) + z); 467 PMATCH_ROW 468 (\((y :num),(v23 :num),(v24 :num list)). 469 (SOME y,(0 :num),v23::v24)) 470 (\((y :num),(v23 :num),(v24 :num list)). T) 471 (\((y :num),(v23 :num),(v24 :num list)). v23 + y); 472 PMATCH_ROW (\((y :num),(z :num),(v23 :num)). (SOME y,SUC z,[v23])) 473 (\((y :num),(z :num),(v23 :num)). y > (5 :num)) 474 (\((y :num),(z :num),(v23 :num)). (3 :num)); 475 PMATCH_ROW 476 (\((y :num),(z :num)). (SOME y,SUC z,[(1 :num); (2 :num)])) 477 (\((y :num),(z :num)). T) (\((y :num),(z :num)). y + z)]``; 478 479val t' = ``PMATCH (a,x,xs) 480 [PMATCH_ROW (\(_0 :num). ((NONE :num option),_0,([] :num list))) 481 (\(_0 :num). T) (\(_0 :num). (0 :num)); 482 PMATCH_ROW (\(x :num). ((NONE :num option),x,[(2 :num)])) 483 (\(x :num). T) (\(x :num). x); 484 PMATCH_ROW (\((_0 :num),(_1 :num)). ((NONE :num option),_0,[_1])) 485 (\((_0 :num),(_1 :num)). T) (\((_0 :num),(_1 :num)). (3 :num)); 486 PMATCH_ROW 487 (\((_3 :num),(_2 :num),(_1 :num)). 488 ((NONE :num option),_1,[_2; _3])) 489 (\((_3 :num),(_2 :num),(_1 :num)). T) 490 (\((_3 :num),(_2 :num),(_1 :num)). x); 491 PMATCH_ROW 492 (\((_0 :num),(_1 :num),(_2 :num),(_3 :num list)). 493 ((NONE :num option),_0,_1::_2::_3)) 494 (\((_0 :num),(_1 :num),(_2 :num),(_3 :num list)). T) 495 (\((_0 :num),(_1 :num),(_2 :num),(_3 :num list)). (3 :num)); 496 PMATCH_ROW (\((_0 :num),(x :num),(z :num)). (SOME _0,x,[z])) 497 (\((_0 :num),(x :num),(z :num)). T) 498 (\((_0 :num),(x :num),(z :num)). x + (5 :num) + z); 499 PMATCH_ROW 500 (\((y :num),(v23 :num),(_0 :num list)). 501 (SOME y,(0 :num),v23::_0)) 502 (\((y :num),(v23 :num),(_0 :num list)). T) 503 (\((y :num),(v23 :num),(_0 :num list)). v23 + y); 504 PMATCH_ROW 505 (\((y :num),(z :num)). (SOME y,SUC z,[(1 :num); (2 :num)])) 506 (\((y :num),(z :num)). T) (\((y :num),(z :num)). y + z)]``; 507 508val _ = test (t, (SOME t')) 509val _ = test_fast (t, NONE) 510 511 512val t = ``PMATCH (x,y,z) 513 [PMATCH_ROW (��(y,z). (1,y,z)) (��(y,z). T) (��(y,z). y + z); 514 PMATCH_ROW (��x. (x,2,4)) (��x. T) (��x. x + 4); 515 PMATCH_ROW (��(x,z). (x,2,z)) (��(x,z). T) (��(x,z). x + z); 516 PMATCH_ROW (��(x,y). (x,y,3)) (��(x,y). T) (��(x,y). x + y)]``; 517 518val t' = `` 519 PMATCH (x,y,z) 520 [PMATCH_ROW (��(y,z). (1,y,z)) (��(y,z). T) (��(y,z). y + z); 521 PMATCH_ROW (��(x,z). (x,2,z)) (��(x,z). T) (��(x,z). x + z); 522 PMATCH_ROW (��(x,y). (x,y,3)) (��(x,y). T) (��(x,y). x + y)]``; 523 524val _ = test (t, (SOME t')) 525val _ = test_fast (t, NONE) 526 527 528val t = 529 ``PMATCH ((NONE :'a option),(x :num),(xs :num list)) 530 [PMATCH_ROW (\(x :num). ((NONE :'a option),x,([] :num list))) 531 (\(x :num). T) (\(x :num). x); 532 PMATCH_ROW (\(x :num). ((NONE :'a option),x,[(2 :num)])) 533 (\(x :num). T) (\(x :num). x); 534 PMATCH_ROW (\((x :num),(v18 :num)). ((NONE :'a option),x,[v18])) 535 (\((x :num),(v18 :num)). T) (\((x :num),(v18 :num)). (3 :num)); 536 PMATCH_ROW 537 (\((x :num),(v12 :num),(v16 :num),(v17 :num list)). 538 ((NONE :'a option),x,v12::v16::v17)) 539 (\((x :num),(v12 :num),(v16 :num),(v17 :num list)). T) 540 (\((x :num),(v12 :num),(v16 :num),(v17 :num list)). (3 :num)); 541 PMATCH_ROW 542 (\((y :'a option),(x :num)). 543 (y,x,[(2 :num); (4 :num); (3 :num)])) 544 (\((y :'a option),(x :num)). x > (5 :num)) 545 (\((y :'a option),(x :num)). (3 :num) + x)]``; 546 547val t' = `` 548 PMATCH xs 549 [PMATCH_ROW (\(_0 :unit). ([] :num list)) (\(_0 :unit). T) 550 (\(_0 :unit). x); 551 PMATCH_ROW (\(_0 :unit). [(2 :num)]) (\(_0 :unit). T) 552 (\(_0 :unit). x); 553 PMATCH_ROW (\(_0 :num). [_0]) (\(_0 :num). T) 554 (\(_0 :num). (3 :num)); 555 PMATCH_ROW (\((_0 :num),(_1 :num),(_2 :num list)). _0::_1::_2) 556 (\((_0 :num),(_1 :num),(_2 :num list)). T) 557 (\((_0 :num),(_1 :num),(_2 :num list)). (3 :num))]``; 558 559val t'' = ``PMATCH xs 560 [PMATCH_ROW (\(_uv:unit). []) (\_uv. T) (\_uv. x); 561 PMATCH_ROW (\(_uv:unit). [2]) (\_uv. T) (\_uv. x); 562 PMATCH_ROW (\v18. [v18]) (\v18. T) (\v18. 3); 563 PMATCH_ROW (\(v12,v16,v17). v12::v16::v17) (\(v12,v16,v17). T) 564 (\(v12,v16,v17). 3); 565 PMATCH_ROW (\(_uv:unit). [2; 4; 3]) (\_uv. x > 5) (\_uv. 3 + x)]`` 566 567val _ = test (t, (SOME t')) 568val _ = test_fast (t, (SOME t'')) 569 570 571 572(*************************************) 573(* Removing DOUBLE-binds and guard *) 574(*************************************) 575 576val t0 = 577 ``PMATCH (l :num list) 578 [PMATCH_ROW (\(_uv :unit). ([] :num list)) (\(_uv :unit). T) 579 (\(_uv :unit). (0 :num)); 580 PMATCH_ROW (\((x :num),(y :num),(_0 :num list)). x::y::x::y::_0) 581 (\((x :num),(y :num),(_0 :num list)). T) 582 (\((x :num),(y :num),(_0 :num list)). x + y); 583 PMATCH_ROW (\((x :num),(y :num),(_1 :num list)). x::x::x::y::_1) 584 (\((x :num),(y :num),(_1 :num list)). T) 585 (\((x :num),(y :num),(_1 :num list)). x + x + x); 586 PMATCH_ROW (\((x :num),(_2 :num list)). x::_2) 587 (\((x :num),(_2 :num list)). T) 588 (\((x :num),(_2 :num list)). (1 :num))]``; 589 590val t1 = ``PMATCH l 591 [PMATCH_ROW (\(_uv :unit). ([] :num list)) (\(_uv :unit). T) 592 (\(_uv :unit). (0 :num)); 593 PMATCH_ROW 594 (\((x :num),(y :num),(_0 :num list),(y' :num),(x' :num)). 595 x::y::x'::y'::_0) 596 (\((x :num),(y :num),(_0 :num list),(y' :num),(x' :num)). 597 (y' = y) /\ (x' = x)) 598 (\((x :num),(y :num),(_0 :num list),(y' :num),(x' :num)). 599 x + y); 600 PMATCH_ROW 601 (\((x :num),(y :num),(_1 :num list),(x'' :num),(x' :num)). 602 x::x'::x''::y::_1) 603 (\((x :num),(y :num),(_1 :num list),(x'' :num),(x' :num)). 604 (x'' = x) /\ (x' = x)) 605 (\((x :num),(y :num),(_1 :num list),(x'' :num),(x' :num)). 606 x + x + x); 607 PMATCH_ROW (\((x :num),(_2 :num list)). x::_2) 608 (\((x :num),(_2 :num list)). T) 609 (\((x :num),(_2 :num list)). (1 :num))]``; 610 611val t2 = `` 612 PMATCH l 613 [PMATCH_ROW (\(_0 :unit). ([] :num list)) (\(_0 :unit). T) 614 (\(_0 :unit). (0 :num)); 615 PMATCH_ROW 616 (\((x :num),(y :num),(_0 :num list),(y' :num),(x' :num)). 617 x::y::x'::y'::_0) 618 (\((x :num),(y :num),(_0 :num list),(y' :num),(x' :num)). T) 619 (\((x :num),(y :num),(_0 :num list),(y' :num),(x' :num)). 620 if (y' = y) /\ (x' = x) then x + y 621 else 622 PMATCH (x::y::x'::y'::_0) 623 [PMATCH_ROW 624 (\((x :num),(_0 :num),(_1 :num list),(x'' :num), 625 (x' :num)). 626 x::x'::x''::_0::_1) 627 (\((x :num),(_0 :num),(_1 :num list),(x'' :num), 628 (x' :num)). 629 (x'' = x) /\ (x' = x)) 630 (\((x :num),(_0 :num),(_1 :num list),(x'' :num), 631 (x' :num)). 632 x + x + x); 633 PMATCH_ROW (\((_0 :num),(_2 :num list)). _0::_2) 634 (\((_0 :num),(_2 :num list)). T) 635 (\((_0 :num),(_2 :num list)). (1 :num))]); 636 PMATCH_ROW (\((_0 :num),(_2 :num list)). _0::_2) 637 (\((_0 :num),(_2 :num list)). T) 638 (\((_0 :num),(_2 :num list)). (1 :num))]`` 639 640val _ = test_conv "PMATCH_REMOVE_DOUBLE_BIND_CONV" PMATCH_REMOVE_DOUBLE_BIND_CONV (t0, SOME t1); 641 642val _ = test_conv "PMATCH_REMOVE_DOUBLE_BIND_CONV" PMATCH_REMOVE_DOUBLE_BIND_CONV (``case xy of 643 | (x, x) when x > 0 => x + x 644 | x.| (x, y) => x 645 | (x, _) => SUC x``, SOME `` 646case xy of 647 (x,x') when (x' = x) /\ x > 0 => x + x 648 | (x,y') when (y' = y) => x 649 | (x,_) => SUC x``) 650 651 652val _ = test_conv "PMATCH_REMOVE_DOUBLE_BIND_CONV" PMATCH_REMOVE_DOUBLE_BIND_CONV (``case (xx:('a # 'a)) of (x, x) => T | _ => F``, SOME ``case (xx:('a # 'a)) of (x, x') when (x' = x) => T | _ => F``) ; 653 654val _ = test_conv "PMATCH_REMOVE_GUARDS_CONV" PMATCH_REMOVE_GUARDS_CONV (t1, SOME t2); 655 656val t = ``PMATCH ((y :num option),(x :num option),(l :num list)) 657 [PMATCH_ROW (\(x :num option). (SOME (0 :num),x,([] :num list))) 658 (\(x :num option). T) (\(x :num option). x); 659 PMATCH_ROW (\(z :num option). (SOME (1 :num),z,[(2 :num)])) 660 (\(z :num option). F) (\(z :num option). z); 661 PMATCH_ROW (\(x :num option). (SOME (3 :num),x,[(2 :num)])) 662 (\(x :num option). IS_SOME x) (\(x :num option). x); 663 PMATCH_ROW (\((z :num option),(y :num option)). (y,z,[(2 :num)])) 664 (\((z :num option),(y :num option)). IS_SOME y) 665 (\((z :num option),(y :num option)). y); 666 PMATCH_ROW (\(z :num option). (SOME (1 :num),z,[(2 :num)])) 667 (\(z :num option). F) (\(z :num option). z); 668 PMATCH_ROW (\(x :num option). (SOME (3 :num),x,[(2 :num)])) 669 (\(x :num option). IS_SOME x) (\(x :num option). x)]``; 670 671val t' = `` PMATCH (y,l) 672 [PMATCH_ROW (\(_0 :unit). (SOME (0 :num),([] :num list))) 673 (\(_0 :unit). T) (\(_0 :unit). x); 674 PMATCH_ROW (\(_0 :unit). (SOME (3 :num),[(2 :num)])) 675 (\(_0 :unit). T) 676 (\(_0 :unit). if IS_SOME x then x else SOME (3 :num)); 677 PMATCH_ROW (\(y :num option). (y,[(2 :num)])) 678 (\(y :num option). T) 679 (\(y :num option). 680 if IS_SOME y then y else (PMATCH_INCOMPLETE :num option))]``; 681 682val _ = test_conv "PMATCH_REMOVE_GUARDS_CONV" PMATCH_REMOVE_GUARDS_CONV (t, SOME t'); 683 684 685val _ = test_conv "PMATCH_REMOVE_GUARDS_CONV" PMATCH_REMOVE_GUARDS_CONV (``case (x, y) of 686 | (x, 2) when EVEN x => x + x 687 | (SUC x, y) when ODD x => y + x + SUC x 688 | (SUC x, 1) => x 689 | (x, _) => x+3``, SOME ``case (x,y) of 690 (x,2) => 691 if EVEN x then x + x 692 else (case x of SUC x when ODD x => 2 + x + SUC x | x => x + 3) 693 | (SUC x,y) => 694 if ODD x then y + x + SUC x 695 else (case y of 1 => x | _ => SUC x + 3) 696 | (x,_) => x + 3``); 697 698 699 700val _ = test_conv "PMATCH_REMOVE_GUARDS_CONV" PMATCH_REMOVE_GUARDS_CONV (``case (x, y) of 701 | (x, 0) when EVEN x => (SOME x, T) 702 | (x, 0) => (SOME x, F) 703 | (0, _) => (NONE, T) 704 | (_, _) => (NONE, F)``, SOME ``case (x,y) of 705 (x,0) => if EVEN x then (SOME x,T) else (SOME x,F) 706 | (0,_) => (NONE,T) 707 | (_,_) => (NONE,F)``); 708 709 710val _ = test_conv "SIMP_CONV (numLib.std_ss ++ PMATCH_REMOVE_GUARDS_ss) []" (SIMP_CONV (numLib.std_ss ++ PMATCH_REMOVE_GUARDS_ss) []) ( 711 ``case x of 712 | _ when x < 5 => 0 713 | _ when x < 10 => 1 714 | _ when x < 15 => 2 715 | _ => 3``, SOME ``if x < 5 then 0 else if x < 10 then 1 else if x < 15 then 2 else 3``); 716 717 718(*************************************) 719(* LIFTING BOOLEAN *) 720(*************************************) 721 722 723val _ = test_conv "DEPTH_CONV (PMATCH_LIFT_BOOL_CONV false)" (DEPTH_CONV (PMATCH_LIFT_BOOL_CONV false)) (``P1 /\ (P (case (l1:'a list, l2) of 724 | ([], _) => [] 725 | (_, []) => [] 726 | (x::xs, y::ys) => [(x, y)])):bool``, 727 SOME ``P1 /\ (((l1 = ([]:'a list)) ==> P []) /\ ((l2 = []) ==> P []) /\ 728 (!x xs y ys. (l1 = x::xs) /\ (l2 = y::ys) ==> P [(x,y)]) /\ 729 (~PMATCH_IS_EXHAUSTIVE (l1,l2) 730 [PMATCH_ROW (\_0. ([],_0)) (\_0. T) (\_0. []); 731 PMATCH_ROW (\_0. (_0,[])) (\_0. T) (\_0. []); 732 PMATCH_ROW (\(x,xs,y,ys). (x::xs,y::ys)) (\(x,xs,y,ys). T) 733 (\(x,xs,y,ys). [(x,y)])] ==> 734 P ARB))``) 735 736 737val _ = test_conv "DEPTH_CONV (PMATCH_LIFT_BOOL_CONV true)" (DEPTH_CONV (PMATCH_LIFT_BOOL_CONV true)) (``P1 /\ (P (case (l1:'a list, l2) of 738 | ([], _) => [] 739 | (_, []) => [] 740 | (x::xs, y::ys) => [(x, y)])):bool``, 741 SOME ``P1 /\ (((l1 = ([]:'a list)) ==> P []) /\ ((l2 = []) ==> P []) /\ 742 (!x xs y ys. (l1 = x::xs) /\ (l2 = y::ys) ==> P [(x,y)]))``) 743 744 745val _ = test_conv "DEPTH_CONV (PMATCH_LIFT_BOOL_CONV false)" (DEPTH_CONV (PMATCH_LIFT_BOOL_CONV false)) (``P1 /\ (P (case (l1:'a list, l2:'c list) of 746 | ([], _) => ([]:'b list) 747 | (_, []) => [])):bool``, 748 SOME ``P1 /\ ((l1 = ([] :'a list)) ==> P ([] :'b list)) /\ 749 ((l2 = ([] :'c list)) ==> P ([] :'b list)) /\ 750 (~PMATCH_IS_EXHAUSTIVE (l1,l2) 751 [PMATCH_ROW (\(_0 :'c list). (([] :'a list),_0)) 752 (\(_0 :'c list). T) (\(_0 :'c list). ([] :'b list)); 753 PMATCH_ROW (\(_0 :'a list). (_0,([] :'c list))) 754 (\(_0 :'a list). T) (\(_0 :'a list). ([] :'b list))] ==> 755 P (ARB :'b list))``) 756 757val _ = test_conv "DEPTH_CONV (PMATCH_LIFT_BOOL_CONV true)" (DEPTH_CONV (PMATCH_LIFT_BOOL_CONV true)) (``P1 /\ (P (case (l1:'a list, l2:'c list) of 758 | ([], _) => ([]:'b list) 759 | (_, []) => [])):bool``, 760 SOME ``P1 /\ (((l1:'a list) = []) ==> P ([]:'b list)) /\ (((l2:'c list) = []) ==> P []) /\ 761 (PMATCH_ROW_COND_EX (l1,l2) (\(v2,v3,v6,v7). (v2::v3,v6::v7)) 762 (\(v2,v3,v6,v7). T) ==> 763 P ARB)``) 764 765 766val _ = Datatype.Datatype ` 767 tree = Empty 768 | Red tree 'a tree 769 | Black tree 'a tree`; 770 771 772val balance_black_def = TotalDefn.Define `balance_black a n b = 773 case (a,b) of 774 | (Red (Red a x b) y c,d) => 775 (Red (Black a x b) y (Black c n d)) 776 | (Red a x (Red b y c),d) => 777 (Red (Black a x b) y (Black c n d)) 778 | (a,Red (Red b y c) z d) => 779 (Red (Black a n b) y (Black c z d)) 780 | (a,Red b y (Red c z d)) => 781 (Red (Black a n b) y (Black c z d)) 782 | other => (Black a n b)` 783 784val tm = #2 (strip_forall (concl (balance_black_def))) 785 786val _ = test_conv "PMATCH_LIFT_BOOL_CONV true" (PMATCH_LIFT_BOOL_CONV true) (tm, SOME `` 787 (!a' x b' y c. 788 (a = Red (Red a' x b') y c) ==> 789 (balance_black a n b = Red (Black a' x b') y (Black c n b))) /\ 790 (!a' x b' y c. 791 (a = Red a' x (Red b' y c)) ==> 792 (!p_1 p_1' p_1''. 793 (Red p_1 p_1' p_1'' = a') ==> 794 ((p_1 = a') /\ (p_1' = x) /\ (p_1'' = b')) /\ (x = y) /\ 795 (Red b' y c = c)) ==> 796 (balance_black a n b = Red (Black a' x b') y (Black c n b))) /\ 797 (!b' y c z d. 798 (b = Red (Red b' y c) z d) ==> 799 (!p_1 p_1' p_1'' p_1''' p_1''''. 800 (Red p_1 p_1' (Red p_1'' p_1''' p_1'''') = a) ==> 801 ((p_1 = a) /\ (p_1' = n) /\ (p_1'' = b')) /\ (p_1''' = y) /\ 802 (p_1'''' = c) /\ (n = z) /\ (Red (Red b' y c) z d = d)) /\ 803 (!p_1 p_1' p_1'' p_1''' p_1''''. 804 (Red (Red p_1 p_1' p_1'') p_1''' p_1'''' = a) ==> 805 ((p_1 = a) /\ (p_1' = n) /\ (p_1'' = b')) /\ (p_1''' = y) /\ 806 (p_1'''' = c) /\ (n = z) /\ (Red (Red b' y c) z d = d)) ==> 807 (balance_black a n b = Red (Black a n b') y (Black c z d))) /\ 808 (!b' y c z d. 809 (b = Red b' y (Red c z d)) ==> 810 (!p_1' p_1'' p_1'''. 811 (Red p_1' p_1'' p_1''' = b') ==> 812 (p_1' = b') /\ (p_1'' = y) /\ (p_1''' = c) /\ (y = z) /\ 813 (Red c z d = d)) /\ 814 (!p_1 p_1' p_1'' p_1''' p_1''''. 815 (Red p_1 p_1' (Red p_1'' p_1''' p_1'''') = a) ==> 816 ((p_1 = a) /\ (p_1' = n) /\ (p_1'' = b')) /\ (p_1''' = y) /\ 817 (p_1'''' = c) /\ (n = z) /\ (Red b' y (Red c z d) = d)) /\ 818 (!p_1 p_1' p_1'' p_1''' p_1''''. 819 (Red (Red p_1 p_1' p_1'') p_1''' p_1'''' = a) ==> 820 ((p_1 = a) /\ (p_1' = n) /\ (p_1'' = b')) /\ (p_1''' = y) /\ 821 (p_1'''' = c) /\ (n = z) /\ (Red b' y (Red c z d) = d)) ==> 822 (balance_black a n b = Red (Black a n b') y (Black c z d))) /\ 823 ((!p_1' p_1'' p_1''' p_1'''' p_2. 824 Red p_1' p_1'' (Red p_1''' p_1'''' p_2) <> b) /\ 825 (!p_1' p_1'' p_1''' p_1'''' p_2. 826 Red (Red p_1' p_1'' p_1''') p_1'''' p_2 <> b) /\ 827 (!p_1 p_1' p_1'' p_1''' p_1''''. 828 Red p_1 p_1' (Red p_1'' p_1''' p_1'''') <> a) /\ 829 (!p_1 p_1' p_1'' p_1''' p_1''''. 830 Red (Red p_1 p_1' p_1'') p_1''' p_1'''' <> a) ==> 831 (balance_black a n b = Black a n b))``) 832 833 834(*********************************) 835(* Pattern Compilation *) 836(*********************************) 837 838val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 839 ``case l of NONE => 0 | SOME x => x``, SOME ``option_CASE l 0 (\x'. x')``) 840 841val t = ``case xyz of 842 | (_, F, T) => 1 843 | (F, T, _) => 2 844 | (_, _, F) => 3 845 | (_, _, T) => 4`` 846 847val test = test_conv "PMATCH_CASE_SPLIT_CONV_HEU colHeu_first_col" (PMATCH_CASE_SPLIT_CONV_HEU colHeu_first_col) (t, SOME 848 ``pair_CASE xyz 849 (\v v'. 850 pair_CASE v' 851 (\v'' v'''. 852 if v then 853 if v'' then if v''' then 4 else 3 854 else if v''' then 1 855 else 3 856 else if v'' then 2 857 else if v''' then 1 858 else 3))``) 859 860val test = test_conv "PMATCH_CASE_SPLIT_CONV_HEU colHeu_last_col" (PMATCH_CASE_SPLIT_CONV_HEU colHeu_last_col) (t, SOME 861 ``pair_CASE xyz 862 (\v v'. 863 pair_CASE v' 864 (\v'' v'''. 865 if v''' then if v'' then if v then 4 else 2 else 1 866 else if v'' then if v then 3 else 2 867 else 3))``) 868 869val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV (t, SOME 870 ``pair_CASE xyz 871 (\v v'. 872 pair_CASE v' 873 (\v'' v'''. 874 if v'' then if v then if v''' then 4 else 3 else 2 875 else if v''' then 1 876 else 3))``) 877 878val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV (t, SOME 879 ``pair_CASE xyz 880 (\v v'. 881 pair_CASE v' 882 (\v'' v'''. 883 if v'' then if v then if v''' then 4 else 3 else 2 884 else if v''' then 1 885 else 3))``) 886 887val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 888 ``case l of (SOME x, SOME y) => SOME (x+y) | _ => NONE``, SOME ``pair_CASE l 889 (\v v'. 890 option_CASE v NONE 891 (\x'. option_CASE v' NONE (\x''. SOME (x' + x''))))`` 892) 893 894val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 895 ``case x of 3 => 1 | _ => 0``, SOME ``literal_case (\v. if v = 3 then 1 else 0) x``) 896 897val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 898 ``case x of 0 => 1 | 1 => 1 | 2 => 2``, SOME `` literal_case 899 (\x. 900 if x = 0 then 1 901 else if x = 1 then 1 902 else if x = 2 then 2 903 else ARB) x``) 904 905val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 906 ``case x of 1 => 1 | 0 => 1 | 2 => 2``, SOME `` literal_case 907 (\x. 908 if x = 1 then 1 909 else if x = 0 then 1 910 else if x = 2 then 2 911 else ARB) x``) 912 913val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 914 ``case x of 1 => 1 | ().| c => 1``, SOME `` literal_case 915 (\x. 916 if x = 1 then 1 917 else if x = c then 1 918 else ARB) x``) 919 920val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 921 ``case x of 1 => 1 | ().| c => 2 | ().| d => 3``, SOME `` literal_case 922 (\x. 923 if x = 1 then 1 924 else if x = c then 2 925 else if x = d then 3 926 else ARB) x``) 927 928val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 929 ``case x of 0 => 1 | SUC 0 => 1 | SUC (SUC 0) => 2``, SOME `` 930 num_CASE x 1 931 (\n. num_CASE n 1 (\n'. num_CASE n' 2 (\n''. ARB)))``) 932 933 934val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 935 ``case l of [] => 1 | [_;_] => 2 | [3] => 3 | [_] => 4 | _ => 5``, SOME `` 936 list_CASE l 1 937 (\h t. 938 list_CASE t (literal_case (\x. if x = 3 then 3 else 4) h) 939 (\h' t'. list_CASE t' 2 (\h'' t''. 5)))``) 940 941val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 942 ``case xy of (0,0) => 1 | (1,1) => 1 | (1,2) => 2``, SOME ``pair_CASE xy 943 (\v v'. 944 literal_case 945 (\x. 946 if x = 0 then num_CASE v' 1 (\n. ARB) 947 else if x = 1 then 948 literal_case 949 (\x'. if x' = 1 then 1 else if x' = 2 then 2 else ARB) 950 v' 951 else ARB) v)``) 952 953 954val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 955 ``case xy of (0,0) => 1 | (1,1) => 1 | ().| (c,3) => 3 | (1,2) => 2 | ().| (c, 4) => 2``, SOME ``pair_CASE xy 956 (\v v'. 957 literal_case 958 (\x. 959 if x = 0 then num_CASE v 1 (\n. ARB) 960 else if x = 1 then 961 literal_case (\x'. if x' = 1 then 1 else ARB) v 962 else if x = 3 then 963 literal_case (\x''. if x'' = c then 3 else ARB) v 964 else if x = 2 then 965 literal_case (\x'''. if x''' = 1 then 2 else ARB) v 966 else if x = 4 then 967 literal_case (\x''''. if x'''' = c then 2 else ARB) v 968 else ARB) v')``) 969 970 971val list_REVCASE_def = TotalDefn.Define ` 972 list_REVCASE l c_nil c_snoc = 973 (if l = [] then c_nil else ( 974 c_snoc (LAST l) (BUTLAST l)))` 975 976val list_REVCASE_THM = prove (`` 977 ((list_REVCASE [] c_nil c_snoc) = c_nil) /\ 978 ((list_REVCASE (SNOC x xs) c_nil c_snoc) = c_snoc x xs)``, 979SIMP_TAC numLib.std_ss [list_REVCASE_def, rich_listTheory.NOT_SNOC_NIL, LAST_SNOC, FRONT_SNOC]) 980 981val cl = make_constructorList true [ 982 (``[]:'a list``, []), 983 (``SNOC: 'a -> 'a list -> 'a list``, ["x", "xs"]) 984] 985 986(* set_constructorFamily (cl, ``list_REVCASE``) *) 987val cf = mk_constructorFamily (cl, ``list_REVCASE``, 988 SIMP_TAC list_ss [rich_listTheory.NOT_SNOC_NIL] THEN 989 REPEAT STRIP_TAC THENL [ 990 ASSUME_TAC (Q.SPEC `x` listTheory.SNOC_CASES) THEN 991 FULL_SIMP_TAC numLib.std_ss [list_REVCASE_THM], 992 993 ASSUME_TAC (Q.SPEC `x` listTheory.SNOC_CASES) THEN 994 FULL_SIMP_TAC numLib.std_ss [list_REVCASE_THM], 995 PROVE_TAC [listTheory.SNOC_CASES] 996 ] 997) 998 999(* add this family *) 1000val _ = pmatch_compile_db_register_constrFam cf 1001 1002val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 1003 ``case l of 1004 | [] => 0 1005 | SNOC x _ => x``, SOME ``list_REVCASE l 0 (\x' xs. x')``) 1006 1007val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 1008 ``case lx of 1009 | (_, NONE) => 0 1010 | (SNOC x _, SOME y) => x + y``, SOME ``pair_CASE lx 1011 (\v v'. 1012 option_CASE v' 0 (\x'. list_REVCASE v ARB (\x'' xs. x'' + x')))``) 1013 1014val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 1015 ``case lx of 1016 | [] => 0 1017 | x::_ => x + y 1018 ``, SOME ``list_CASE lx 0 (\h t. h + y)``) 1019 1020val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 1021 ``case lx of 1022 | [] => 0 1023 | SNOC x _ => x 1024 | x::_ => x + y 1025 ``, NONE) 1026 1027 1028val tree_case_def = DB.fetch "-" "tree_case_def"; 1029 1030val tree_red_CASE_def = TotalDefn.Define ` 1031 tree_red_CASE tr f_red f_else = 1032 tree_CASE tr (f_else Empty) f_red 1033 (\t1 n t2. f_else (Black t1 n t2))` 1034 1035val tree_red_CASE_THM = prove (`` 1036 (tree_red_CASE Empty f_red f_else = f_else Empty) /\ 1037 (tree_red_CASE (Red t1 n t2) f_red f_else = f_red t1 n t2) /\ 1038 (tree_red_CASE (Black t1 n t2) f_red f_else = f_else (Black t1 n t2))``, 1039SIMP_TAC list_ss [tree_red_CASE_def, tree_case_def]) 1040 1041val cl = make_constructorList false [ 1042 (``Red : 'a tree -> 'a -> 'a tree -> 'a tree``, ["t1", "n", "t2"]) 1043] 1044 1045(* set_constructorFamily (cl, ``tree_red_CASE``) *) 1046val cf = mk_constructorFamily (cl, ``tree_red_CASE``, 1047 SIMP_TAC (srw_ss()) [tree_red_CASE_def] THEN 1048 CONJ_TAC THEN ( 1049 Cases_on `x` THEN 1050 SIMP_TAC (srw_ss()) [tree_red_CASE_def] 1051 )); 1052 1053val _ = pmatch_compile_db_register_constrFam cf; 1054 1055val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 1056 ``case (t:'a tree) of 1057 | Red _ _ _ => T 1058 | _ => F 1059 ``, SOME (``tree_red_CASE (t:'a tree) (\t a t0. T) (\x. F)``)) 1060 1061val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 1062 ``case (t:'a tree) of 1063 | Black _ _ _ => T 1064 | _ => F 1065 ``, SOME (``tree_CASE (t:'a tree) F (\t a t0. F) (\t' a' t0'. T)``)) 1066 1067 1068(*********************************) 1069(* Compilation to nchotomies *) 1070(*********************************) 1071 1072val test_nchot = test_gen (fn l => ( 1073 print "["; 1074 OldPP.pr_list print_term' (fn () => print ", ") (fn () => ()) l; 1075 print "]")) 1076 print_thm' print_term' (fn (inp, out, res) => aconv out (concl res)) 1077 "nchotomy_of_pats" nchotomy_of_pats 1078 1079 1080val _ = test_nchot ([``\x:unit. (NONE : num option)``, 1081 ``\x:num. SOME x``] , SOME ``!x. (x = NONE) \/ ?v1:num. x = SOME v1``) 1082 1083val _ = test_nchot ([``\x:num. x``, ``\x:num. x``], 1084 SOME ``!x. ?v0:num. x = v0``) 1085 1086val _ = test_nchot ([ 1087 ``\v:bool. (v, F, T)``, 1088 ``\v:bool. (F, T, v)``, 1089 ``\(v1:bool, v2:bool). (v1, v2, F)``, 1090 ``\(v1:bool, v2:bool). (v1, v2, F)``], 1091 SOME ``!x. 1092 (x = (T,T,T)) \/ (x = (T,T,F)) \/ (x = (F,T,T)) \/ (x = (F,T,F)) \/ 1093 (?v0. x = (v0,F,T)) \/ ?v0. x = (v0,F,F)``) 1094 1095val _ = test_nchot ([ 1096 ``\(x:num, y:num). (SOME x, SOME y)``, 1097 ``\(x : num option, y : num option). (x, y)``], 1098 SOME ``!x. 1099 (?v1. x = (NONE,v1)) \/ (?v2. x = (SOME v2,NONE)) \/ 1100 ?(v2:num) (v3:num). x = (SOME v2,SOME v3)``) 1101 1102val _ = test_nchot ([``\_:unit. 3``, ``\x:num. x``], SOME ( 1103 ``!x. (x = 3) \/ ?v1. v1 <> 3 /\ (x = v1)``)) 1104 1105val _ = test_nchot ([``\_:unit. 0``, ``\_:unit. SUC 0``, ``\_:unit. SUC (SUC 0)``], SOME ( 1106 ``!x. (x = 0) \/ (x = SUC 0) \/ (x = SUC (SUC 0)) \/ 1107 ?v3. x = SUC (SUC (SUC v3))``)) 1108 1109 1110(*********************************) 1111(* Fancy redundancy removal *) 1112(*********************************) 1113 1114val t = 1115 ``PMATCH ((x :'a option),(z :'b option)) 1116 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1117 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1118 PMATCH_ROW (\((_1 :'b option),(_0 :'a)). (SOME _0,_1)) 1119 (\((_1 :'b option),(_0 :'a)). T) 1120 (\((_1 :'b option),(_0 :'a)). (1 :num)); 1121 PMATCH_ROW (\(_2 :'a option). (_2,(NONE :'b option))) 1122 (\(_2 :'a option). T) (\(_2 :'a option). (2 :num))]``; 1123 1124val t' = `` 1125 PMATCH (x,z) 1126 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1127 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1128 PMATCH_ROW (\((_1 :'b option),(_0 :'a)). (SOME _0,_1)) 1129 (\((_1 :'b option),(_0 :'a)). T) 1130 (\((_1 :'b option),(_0 :'a)). (1 :num))]``; 1131 1132val _ = test_conv "PMATCH_REMOVE_REDUNDANT_CONV" PMATCH_REMOVE_REDUNDANT_CONV (t, SOME t'); 1133 1134 1135(*********************************) 1136(* Exhaustiveness *) 1137(*********************************) 1138 1139val test_precond = test_term_thm_gen (fn (inp, out, res) => let 1140 val (r, _) = dest_imp_only (concl res) 1141in 1142 (aconv r out) 1143end) 1144 1145val test_rhs = test_term_thm_gen (fn (inp, out, res) => let 1146 val (_, r) = dest_eq (concl res) 1147in 1148 (aconv r out) 1149end) 1150 1151val t = 1152 ``PMATCH ((x :'a option),(z :'b option)) 1153 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1154 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1155 PMATCH_ROW (\((_1 :'b option),(_0 :'a)). (SOME _0,_1)) 1156 (\((_1 :'b option),(_0 :'a)). T) 1157 (\((_1 :'b option),(_0 :'a)). (1 :num)); 1158 PMATCH_ROW (\((_3 :'b),(_2 :'a option)). (_2,SOME _3)) 1159 (\((_3 :'b),(_2 :'a option)). T) 1160 (\((_3 :'b),(_2 :'a option)). (2 :num))]``; 1161 1162val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, SOME ``~F``) 1163 1164val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME ``~F``) 1165 1166val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME T) 1167 1168val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, NONE) 1169 1170val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, SOME T) 1171 1172 1173val t = 1174 ``PMATCH ((x :'a option),(z :'b option)) 1175 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1176 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1177 PMATCH_ROW (\((_1 :'b option),(_0 :'a)). (SOME _0,_1)) 1178 (\((_1 :'b option),(_0 :'a)). T) 1179 (\((_1 :'b option),(_0 :'a)). (1 :num)); 1180 PMATCH_ROW (\((_3 :'b option),(_2 :'a option)). (_2,_3)) 1181 (\((_3 :'b option),(_2 :'a option)). T) 1182 (\((_3 :'b option),(_2 :'a option)). (2 :num))]``; 1183 1184val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, SOME ``~F``) 1185 1186val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME ``~F``) 1187 1188val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME T) 1189 1190val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, SOME T) 1191 1192val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, SOME T) 1193 1194 1195val t = 1196 ``PMATCH (xy : ('a option # 'b option)) 1197 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1198 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1199 PMATCH_ROW (\((_1 :'b option),(_0 :'a)). (SOME _0,_1)) 1200 (\((_1 :'b option),(_0 :'a)). T) 1201 (\((_1 :'b option),(_0 :'a)). (1 :num)); 1202 PMATCH_ROW (\ (_3 : ('a option # 'b option)). _3) 1203 (\_. T) 1204 (\_. (2 :num))]``; 1205 1206val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, SOME ``~F``) 1207 1208val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME ``~F``) 1209 1210val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME T) 1211 1212val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, SOME T) 1213 1214val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, SOME T) 1215 1216val t = 1217 ``PMATCH (xy : ('a option # 'b option)) 1218 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1219 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1220 PMATCH_ROW (\((_1 :'b option),(_0 :'a)). (SOME _0,_1)) 1221 (\((_1 :'b option),(_0 :'a)). T) 1222 (\((_1 :'b option),(_0 :'a)). (1 :num)); 1223 PMATCH_ROW (\((_3 :'b option),(_2 :'a option)). (_2,_3)) 1224 (\((_3 :'b option),(_2 :'a option)). T) 1225 (\((_3 :'b option),(_2 :'a option)). (2 :num))]``; 1226 1227val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, SOME ``~F``) 1228 1229val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME ``~F``) 1230 1231val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME T) 1232 1233val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, SOME T) 1234 1235val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, SOME T) 1236 1237 1238val t =``PMATCH xy []``; 1239 1240val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, NONE) 1241 1242val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME ``F``) 1243 1244val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME F) 1245 1246val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, SOME F) 1247 1248val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, NONE) 1249 1250 1251val t = 1252 ``PMATCH ((x :'a option),(z :'b option)) 1253 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1254 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1255 PMATCH_ROW (\((_3 :'b),(_2 :'a option)). (_2,SOME _3)) 1256 (\((_3 :'b),(_2 :'a option)). T) 1257 (\((_3 :'b),(_2 :'a option)). (2 :num))]``; 1258 1259val t' = ``PMATCH (x,z) 1260 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1261 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1262 PMATCH_ROW (\((_3 :'b),(_2 :'a option)). (_2,SOME _3)) 1263 (\((_3 :'b),(_2 :'a option)). T) 1264 (\((_3 :'b),(_2 :'a option)). (2 :num)); 1265 PMATCH_ROW (\(v3 :'a). (SOME v3,(NONE :'b option))) (\(v3 :'a). T) 1266 (\(v3 :'a). (ARB :num))]`` 1267 1268val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, SOME ``~PMATCH_ROW_COND_EX (x,z) (\v3. (SOME v3,NONE)) (\v3. T)``) 1269 1270val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME ``~PMATCH_ROW_COND_EX (x,z) (\v3. (SOME v3,NONE)) (\v3. T)``) 1271 1272val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME ``~PMATCH_ROW_COND_EX (x,z) (\v3. (SOME v3,NONE)) (\v3. T)``) 1273 1274val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, NONE) 1275 1276val _ = test_conv "PMATCH_COMPLETE_CONV true" (PMATCH_COMPLETE_CONV true) (t, SOME t') 1277 1278val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, SOME ``~PMATCH_ROW_COND_EX (x,z) (\v3. (SOME v3,NONE)) (\v3. T)``) 1279 1280val t = 1281 ``PMATCH (SOME x, NONE) 1282 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1283 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1284 PMATCH_ROW (\((_3 :'b),(_2 :'a option)). (_2,SOME _3)) 1285 (\((_3 :'b),(_2 :'a option)). T) 1286 (\((_3 :'b),(_2 :'a option)). (2 :num))]``; 1287 1288val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, SOME ``~PMATCH_ROW_COND_EX (SOME x,NONE) (\v3. (SOME v3,NONE)) (\v3. T)``) 1289 1290val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME ``F``) 1291 1292val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME F) 1293 1294val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, SOME F) 1295 1296val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, SOME 1297``~PMATCH_ROW_COND_EX (SOME x,NONE) (\v3. (SOME v3,NONE)) (\v3. T)``) 1298 1299 1300val t = 1301 ``PMATCH (NONE, SOME b) 1302 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1303 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1304 PMATCH_ROW (\((_3 :'b),(_2 :'a option)). (_2,SOME _3)) 1305 (\((_3 :'b),(_2 :'a option)). T) 1306 (\((_3 :'b),(_2 :'a option)). (2 :num))]``; 1307 1308val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, SOME ``~PMATCH_ROW_COND_EX (NONE,SOME b) (\v3. (SOME v3,NONE)) (\v3. T)``) 1309 1310val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME ``~F``) 1311 1312val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME T) 1313 1314val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, SOME T) 1315 1316val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, SOME T) 1317 1318 1319val t = ``PMATCH ((x :'a option),(z :'b option)) 1320 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1321 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1322 PMATCH_ROW (\((_1 :'b option),(_0 :'a)). (SOME _0,_1)) 1323 (\((_1 :'b option),(_0 :'a)). T) 1324 (\((_1 :'b option),(_0 :'a)). (1 :num)); 1325 PMATCH_ROW (\(_2 :'a option). (_2,(NONE :'b option))) 1326 (\(_2 :'a option). T) (\(_2 :'a option). (2 :num))]``; 1327 1328val p = ``~PMATCH_ROW_COND_EX ((x :'a option),(z :'b option)) 1329 (\(v3 :'b). ((NONE :'a option),SOME v3)) (\(v3 :'b). T)`` 1330 1331val t' = ``PMATCH (x,z) 1332 [PMATCH_ROW (\(_uv :unit). ((NONE :'a option),(NONE :'b option))) 1333 (\(_uv :unit). T) (\(_uv :unit). (0 :num)); 1334 PMATCH_ROW (\((_1 :'b option),(_0 :'a)). (SOME _0,_1)) 1335 (\((_1 :'b option),(_0 :'a)). T) 1336 (\((_1 :'b option),(_0 :'a)). (1 :num)); 1337 PMATCH_ROW (\(_2 :'a option). (_2,(NONE :'b option))) 1338 (\(_2 :'a option). T) (\(_2 :'a option). (2 :num)); 1339 PMATCH_ROW (\(v3 :'b). ((NONE :'a option),SOME v3)) (\(v3 :'b). T) 1340 (\(v3 :'b). (ARB :num))]``; 1341 1342val _ = test_precond "PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CONSEQ_CHECK (t, SOME `` ~PMATCH_ROW_COND_EX (x,z) (\v3. (NONE,SOME v3)) (\v3. T)``) 1343 1344val _ = test_precond "PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK" PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK (t, SOME `` ~PMATCH_ROW_COND_EX (x,z) (\v3. (NONE,SOME v3)) (\v3. T)``) 1345 1346val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_CHECK" PMATCH_IS_EXHAUSTIVE_CHECK (t, SOME p) 1347 1348val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_FAST_CHECK" PMATCH_IS_EXHAUSTIVE_FAST_CHECK (t, NONE) 1349 1350val _ = test_conv "PMATCH_COMPLETE_CONV true" (PMATCH_COMPLETE_CONV true) (t, SOME t') 1351 1352val _ = test_rhs "PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK" PMATCH_IS_EXHAUSTIVE_COMPILE_CHECK (t, SOME p) 1353 1354 1355(*********************************) 1356(* LIFTING *) 1357(*********************************) 1358 1359val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1360 (``case t of [] => 0 | x::_ => x``, NONE) 1361 1362val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1363 (``SUC (case t of [] => 0 | x::_ => x)``, SOME 1364 ``case t of [] => SUC 0 | x::_ => SUC x``) 1365 1366val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1367 (``SUC ((\c. (case t of [] => 0 | x::_ => x) + c) 5)``, SOME 1368 ``case t of [] => SUC ((\c. 0 + c) 5) | x::_ => SUC ((\c. x + c) 5)``) 1369 1370val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1371 (``(\c. (case t of [] => 0 | x::_ => x) + c)``, SOME 1372 ``case t of [] => (\c. 0 + c) | x::_ => (\c. x + c)``) 1373 1374val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1375 (``SUC ((\c. (case t of [] => c | x::_ => x) + c) 5)``, NONE) 1376 1377val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1378 (``(\c. (case t of [] => c | x::_ => x) + c)``, NONE) 1379 1380val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1381 (``SUC (case t of [] => 0)``, SOME 1382 ``case t of [] => SUC 0 | v1::v2 => SUC ARB``) 1383 1384val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1385 (``SUC ((\c. (case t of [] => 0) + c) 5)``, SOME 1386 ``case t of [] => SUC ((\c. 0 + c) 5) | _::_ => SUC ((\c. ARB + c) 5)``) 1387 1388val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1389 (``(\c. (case t of [] => 0) + c)``, SOME 1390 ``case t of [] => (\c. 0 + c) | _::_ => (\c. ARB + c)``) 1391 1392 1393val _ = test_conv "PMATCH_LIFT_CONV" PMATCH_LIFT_CONV 1394 (``(\c. (case t of [] => 0) + c + 2 * (case t of [] => 0))``, SOME 1395 ``case t of [] => (\c. 0 + c + 2 * 0) | _::_ => (\c. ARB + c + 2 * ARB)``) 1396 1397 1398(*********************************) 1399(* EXTENDING INPUT *) 1400(*********************************) 1401 1402val _ = test_conv "PMATCH_EXTEND_INPUT_CONV" (PMATCH_EXTEND_INPUT_CONV ``(n:num, l:num list)``) 1403 (``case (l, n) of ([], _) => c | (x::_, SUC m) => x + m``, SOME 1404 ``PMATCH ((n :num),(l :num list)) 1405 [PMATCH_ROW (\(_0 :num). (_0,([] :num list))) (\(_0 :num). T) 1406 (\(_0 :num). c); 1407 PMATCH_ROW (\((x :num),(_0 :num list),(m :num)). (SUC m,x::_0)) 1408 (\((x :num),(_0 :num list),(m :num)). T) 1409 (\((x :num),(_0 :num list),(m :num)). x + m)]``) 1410 1411 1412val _ = test_conv "PMATCH_EXTEND_INPUT_CONV" (PMATCH_EXTEND_INPUT_CONV ``(x1: 'a, n:num, x2:'b, l:num list, x3:'c)``) 1413 (``case (l, n) of ([], _) => c | (x::_, SUC m) => x + m``, SOME 1414 ``PMATCH ((x1 :'a),n,(x2 :'b),l,(x3 :num)) 1415 [PMATCH_ROW 1416 (\((_0 :num),(_1 :'a),(_2 :'b),(_3 :num)). 1417 (_1,_0,_2,([] :num list),_3)) 1418 (\((_0 :num),(_1 :'a),(_2 :'b),(_3 :num)). T) 1419 (\((_0 :num),(_1 :'a),(_2 :'b),(_3 :num)). c); 1420 PMATCH_ROW 1421 (\((x :num),(_0 :num list),(m :num),(_1 :'a),(_2 :'b), 1422 (_3 :num)). 1423 (_1,SUC m,_2,x::_0,_3)) 1424 (\((x :num),(_0 :num list),(m :num),(_1 :'a),(_2 :'b), 1425 (_3 :num)). 1426 T) 1427 (\((x :num),(_0 :num list),(m :num),(_1 :'a),(_2 :'b), 1428 (_3 :num)). 1429 x + m)]``) 1430 1431 1432val _ = test_conv "PMATCH_EXTEND_INPUT_CONV" (PMATCH_EXTEND_INPUT_CONV ``(x1: 'a, n:num, n, x2:'b, l:num list, x3:'c)``) 1433 (``case (l, n) of ([], _) => c | (x::_, SUC m) => x + m``, SOME 1434 ``PMATCH ((x1 :'a),n,n,(x2 :'b),l,(x3 :num)) 1435 [PMATCH_ROW 1436 (\((_0 :num),(_1 :'a),(_2 :num),(_3 :'b),(_4 :num)). 1437 (_1,_0,_2,_3,([] :num list),_4)) 1438 (\((_0 :num),(_1 :'a),(_2 :num),(_3 :'b),(_4 :num)). T) 1439 (\((_0 :num),(_1 :'a),(_2 :num),(_3 :'b),(_4 :num)). c); 1440 PMATCH_ROW 1441 (\((x :num),(_0 :num list),(m :num),(_1 :'a),(_2 :num),(_3 :'b), 1442 (_4 :num)). 1443 (_1,SUC m,_2,_3,x::_0,_4)) 1444 (\((x :num),(_0 :num list),(m :num),(_1 :'a),(_2 :num),(_3 :'b), 1445 (_4 :num)). 1446 T) 1447 (\((x :num),(_0 :num list),(m :num),(_1 :'a),(_2 :num),(_3 :'b), 1448 (_4 :num)). 1449 x + m)]``) 1450 1451 1452val _ = test_conv "PMATCH_EXTEND_INPUT_CONV" (PMATCH_EXTEND_INPUT_CONV ``(c:num, n:num, l:num list)``) 1453 (``case (l, n) of ([], _) => c | (x::_, SUC m) => x + m + n``, SOME 1454 ``PMATCH (c,n,l) 1455 [PMATCH_ROW (\(_0,c). (c,_0,[])) (\(_0,c). T) (\(_0,c). c); 1456 PMATCH_ROW (\(x,_0,m,_1). (_1,SUC m,x::_0)) (\(x,_0,m,_1). T) 1457 (\(x,_0,m,_1). x + m + SUC m)]``) 1458 1459 1460(*********************************) 1461(* FLATTENING *) 1462(*********************************) 1463 1464val _ = test_conv "PMATCH_FLATTEN_CONV false" (PMATCH_FLATTEN_CONV false) 1465 (``case (x, y) of ([], x::xs) => ( 1466 case xs of [] => 1 + x | (x::xs) => 5 + x + LENGTH xs) | (_, []) => 1``, 1467 SOME ``PMATCH (x,y) 1468 [PMATCH_ROW (\x. ([],[x])) (\x. T) (\x. 1 + x); 1469 PMATCH_ROW (\(x,xs,_0). ([],_0::x::xs)) (\(x,xs,_0). T) 1470 (\(x,xs,_0). 5 + x + LENGTH xs); 1471 PMATCH_ROW (\_0. (_0,[])) (\_0. T) (\_0. 1)]``) 1472 1473val _ = test_conv "PMATCH_FLATTEN_CONV true" (PMATCH_FLATTEN_CONV true) 1474 (``case (x, y) of ([], x::xs) => ( 1475 case xs of [] => 1 + x | (x::xs) => 5 + x + LENGTH xs) | (_, []) => 1``, 1476 SOME ``PMATCH (x,y) 1477 [PMATCH_ROW (\x. ([],[x])) (\x. T) (\x. 1 + x); 1478 PMATCH_ROW (\(x,xs,_0). ([],_0::x::xs)) (\(x,xs,_0). T) 1479 (\(x,xs,_0). 5 + x + LENGTH xs); 1480 PMATCH_ROW (\_0. (_0,[])) (\_0. T) (\_0. 1)]``) 1481 1482val _ = test_conv "PMATCH_FLATTEN_CONV false" (PMATCH_FLATTEN_CONV false) 1483 (``case (x, y) of ([], x::xs) => SUC ( 1484 case xs of [] => 1 + x | (x::xs) => 5 + x + LENGTH xs) | (_, []) => 1``, 1485 NONE) 1486 1487 1488val _ = test_conv "PMATCH_FLATTEN_CONV true" (PMATCH_FLATTEN_CONV true) 1489 (``case (x, y) of ([], x::xs) => SUC ( 1490 case xs of [] => 1 + x | (x::xs) => 5 + x + LENGTH xs) | (_, []) => 1``, 1491 SOME ``PMATCH (x,y) 1492 [PMATCH_ROW (\x. ([],[x])) (\x. T) (\x. SUC (1 + x)); 1493 PMATCH_ROW (\(x,xs,_0). ([],_0::x::xs)) (\(x,xs,_0). T) 1494 (\(x,xs,_0). SUC (5 + x + LENGTH xs)); 1495 PMATCH_ROW (\_0. (_0,[])) (\_0. T) (\_0. 1)]``) 1496 1497 1498val _ = test_conv "PMATCH_FLATTEN_CONV true" (PMATCH_FLATTEN_CONV true) 1499 (``case (x, y) of ([], x::xs) => SUC ( 1500 case xs of [] => 1 + x | (x::xs) => 5 + x + LENGTH xs) | (y::ys, []) => (case y of 0 => 1 | _ => 2)``, 1501 SOME ``PMATCH (x,y) 1502 [PMATCH_ROW (\x. ([],[x])) (\x. T) (\x. SUC (1 + x)); 1503 PMATCH_ROW (\(x,xs,_0). ([],_0::x::xs)) (\(x,xs,_0). T) 1504 (\(x,xs,_0). SUC (5 + x + LENGTH xs)); 1505 PMATCH_ROW (\_1. (0::_1,[])) (\_1. T) (\_1. 1); 1506 PMATCH_ROW (\(_0,_1). (_0::_1,[])) (\(_0,_1). T) (\(_0,_1). 2)]``) 1507 1508 1509val _ = test_conv "PMATCH_FLATTEN_CONV true" (PMATCH_FLATTEN_CONV true) 1510 (``case (x, y) of ([], x::xs) => SUC ( 1511 case xs of [] => 1 + x | (x::xs) => 5 + x + LENGTH xs) | (y::ys, []) => (case z of 0 => 1 | _ => 2)``, 1512 SOME ``PMATCH (x,y) 1513 [PMATCH_ROW (\x. ([],[x])) (\x. T) (\x. SUC (1 + x)); 1514 PMATCH_ROW (\(x,xs,_0). ([],_0::x::xs)) (\(x,xs,_0). T) 1515 (\(x,xs,_0). SUC (5 + x + LENGTH xs)); 1516 PMATCH_ROW (\(_0,_1). (_0::_1,[])) (\(_0,_1). T) 1517 (\(_0,_1). 1518 PMATCH z 1519 [PMATCH_ROW (\_:unit. 0) (\_. T) (\_. 1); 1520 PMATCH_ROW (\_0. _0) (\_0. T) (\_0. 2)])]``) 1521 1522 1523(*********************************) 1524(* EVAL *) 1525(*********************************) 1526 1527fun mk_t t = ``PMATCH (^t :num list) 1528 [PMATCH_ROW (\((y :num),(_0 :num)). [_0; y]) 1529 (\((y :num),(_0 :num)). T) (\((y :num),(_0 :num)). y); 1530 PMATCH_ROW (\((x :num),(_2 :num),(_1 :num)). [x; _1; _2]) 1531 (\((x :num),(_2 :num),(_1 :num)). T) 1532 (\((x :num),(_2 :num),(_1 :num)). x); 1533 PMATCH_ROW (\((x :num),(y :num),(_3 :num list)). x::y::_3) 1534 (\((x :num),(y :num),(_3 :num list)). T) 1535 (\((x :num),(y :num),(_3 :num list)). x + y); 1536 PMATCH_ROW (\(_uv :unit). ([] :num list)) (\(_uv :unit). T) 1537 (\(_uv :unit). (0 :num)); 1538 PMATCH_ROW (\(_4 :num list). _4) (\(_4 :num list). T) 1539 (\(_4 :num list). (1 :num))]``; 1540 1541fun run_test (t, r) = 1542 test_conv "EVAL_CONV" EVAL_CONV (mk_t t, SOME r); 1543 1544val _ = run_test (``[] : num list``, ``0``); 1545val _ = run_test (``[2;3] : num list``, ``3``); 1546val _ = run_test (``[2;30] : num list``, ``30``); 1547val _ = run_test (``[2;3;4] : num list``, ``2``); 1548val _ = run_test (``[4;3;4] : num list``, ``4``); 1549val _ = run_test (``[4;3;4;3] : num list``, ``7``); 1550val _ = run_test (``(4::3::l) : num list``, ``PMATCH ((4 :num)::(3 :num)::l) 1551 [PMATCH_ROW (\((y :num),(_0 :num)). [_0; y]) 1552 (\((y :num),(_0 :num)). T) (\((y :num),(_0 :num)). y); 1553 PMATCH_ROW (\((x :num),(_2 :num),(_1 :num)). [x; _1; _2]) 1554 (\((x :num),(_2 :num),(_1 :num)). T) 1555 (\((x :num),(_2 :num),(_1 :num)). x); 1556 PMATCH_ROW (\((x :num),(y :num),(_3 :num list)). x::y::_3) 1557 (\((x :num),(y :num),(_3 :num list)). T) 1558 (\((x :num),(y :num),(_3 :num list)). x + y)]``); 1559 1560val _ = test_conv "EVAL_CONV" EVAL_CONV (``case [] of x::xs => SUC x``, SOME ``ARB:num``); 1561 1562val _ = test_conv "EVAL_CONV" EVAL_CONV (``case [] of SNOC x xs => SUC x``, SOME ``ARB:num``); 1563 1564val _ = test_conv "EVAL_CONV" EVAL_CONV (``case [] of [] => 0 | SNOC x xs => SUC x``, SOME ``0``); 1565 1566val _ = test_conv "EVAL_CONV" EVAL_CONV (``case SNOC x xs of [] => 0 | SNOC x xs => SUC x``, SOME ``SUC x``); 1567 1568val test = test_conv "PMATCH_CASE_SPLIT_CONV" PMATCH_CASE_SPLIT_CONV ( 1569 ``case lx of 1570 | [] => 0 1571 | SNOC x _ => x 1572 | x::_ => x + y 1573 ``, NONE) 1574