1(*=========================================================================== 2 Testing term construction and destruction for big terms 3 4 When the terms get bigger, various things barf, like the 5 prettyprinter, and the naive way of doing list_mk_conj: 6 7 itlist (curry mk_conj) vlist tm 8 9 blows the stack, so things have to be made tail recursive. 10 ===========================================================================*) 11 12fun upto f b t = 13 let fun up i acc = if i < t then up (i+1) (f i::acc) else rev acc 14 in up b [] 15 end; 16 17val vars10 = upto (fn i => mk_var("v"^Int.toString i, bool)) 0 10; 18val vars100 = upto (fn i => mk_var("v"^Int.toString i, bool)) 0 100; 19val vars1K = upto (fn i => mk_var("v"^Int.toString i, bool)) 0 1000; 20val vars10K = upto (fn i => mk_var("v"^Int.toString i, bool)) 0 10000; 21val vars50K = upto (fn i => mk_var("v"^Int.toString i, bool)) 0 50000; 22val vars100K = upto (fn i => mk_var("v"^Int.toString i, bool)) 0 100000; 23val vars500K = upto (fn i => mk_var("v"^Int.toString i, bool)) 0 500000; 24val vars1M = upto (fn i => mk_var("v"^Int.toString i, bool)) 0 1000000; 25 26val body10 = time list_mk_conj vars10; 27val body100 = time list_mk_conj vars100; 28val body1K = time list_mk_conj vars1K; 29max_print_depth := 10; 30val body10K = time list_mk_conj vars10K; 31val body50K = time list_mk_conj vars50K; 32val body100K = time list_mk_conj vars100K; 33val body500K = time list_mk_conj vars500K; 34val body1M = time list_mk_conj vars1M; (* 9 secs *) 35 36val abs10 = (time HolKernel.list_mk_abs(vars10,body10); ()); 37val abs100 = (time HolKernel.list_mk_abs(vars100,body100); ()) 38val abs1K = (time HolKernel.list_mk_abs(vars1K,body1K); ()); 39val abs10K = (time HolKernel.list_mk_abs(vars10K,body10K); ()); 40val abs100K = (time HolKernel.list_mk_abs(vars100K,body100K); ()); 41val abs500K = (time HolKernel.list_mk_abs(vars500K,body500K); ()); 42val abs1M = (time HolKernel.list_mk_abs(vars1M,body1M); ()); 43 44val ALL10 = (time list_mk_forall(vars10,body10); ()); 45val ALL100 = (time list_mk_forall(vars100,body100); ()) 46val ALL1K = (time list_mk_forall(vars1K,body1K); ()); 47val ALL10K = (time list_mk_forall(vars10K,body10K); ()); 48val ALL100K = (time list_mk_forall(vars100K,body100K); ()); 49val ALL500K = (time list_mk_forall(vars500K,body500K); ()); 50val ALL1M = (time list_mk_forall(vars1M,body1M); ()); 51 52val dabs10 = let val abs10 = list_mk_abs(vars10,body10) 53 in time Term.strip_abs abs10 ; () end; 54val dabs100 = let val abs100 = list_mk_abs(vars100,body100) 55 in time Term.strip_abs abs100 ; () end; 56val dabs1K = let val abs1K = list_mk_abs(vars1K,body1K) 57 in time Term.strip_abs abs1K ; () end; 58val dabs10K = let val abs10K = list_mk_abs(vars10K,body10K) 59 in time Term.strip_abs abs10K ; () end; 60val dabs100K = let val abs100K = list_mk_abs(vars100K,body100K) 61 in time Term.strip_abs abs100K ; () end; 62val dabs100K' = let val abs100K' = list_mk_abs(vars10K,body100K) 63 in list_mk_abs(Term.strip_abs abs100K') = abs100K' end; 64val dabs500K = let val abs500K = list_mk_abs(vars500K,body500K) 65 in time Term.strip_abs abs500K ; () end; 66val dabs1M = let val abs1M = time list_mk_abs(vars1M,body1M) 67 in time Term.strip_abs abs1M ; () end; 68 69fun old_list_mk_abs(V,t) = itlist(curry mk_abs) V t; 70fun old_list_mk_forall(V,t) = itlist(curry mk_forall) V t; 71 72val old_abs10 = (time old_list_mk_abs(vars10,body10); ()); 73val old_abs100 = (time old_list_mk_abs(vars100,body100); ()); 74val old_abs1K = (time old_list_mk_abs(vars1K,body1K); ()); 75(* After this, it's too slow *) 76val abs10K = (time old_list_mk_abs(vars10K,body10K);()); 77val abs100K = (time old_list_mk_abs(vars100K,body100K); ()) 78val abs500K = (time old_list_mk_abs(vars500K,body500K); ()) 79val abs1M = time old_list_mk_abs(vars1M,body1M); 80 81(* --------------------------------------------------------------------------- 82 Some renaming checks 83 --------------------------------------------------------------------------- *) 84 85val x = mk_var("x",bool) 86val x' = mk_var("x'",bool) 87val x'' = mk_var("x''",bool) 88val x''' = mk_var("x'''",bool) 89val x'''' = mk_var("x''''",bool) 90val y = mk_var("y",bool); 91val z = mk_var("z",bool); 92 93strip_abs(beta_conv(Term `(\^x ^y. x) y`)); 94strip_abs(beta_conv(Term `(\^y ^x' ^x. y) x`)); 95strip_abs(beta_conv(Term `(\^y ^x ^x'. y) x`)); 96strip_abs(beta_conv(Term `(\^y ^x. y /\ x) x`)); 97strip_abs(beta_conv(Term `(\^y ^x ^x ^x. y /\ x) x`)); 98strip_abs(beta_conv(Term `(\^y ^x. y /\ x') x`)); 99strip_abs(beta_conv(Term `(\^y ^x. y /\ x' /\ x) x`)); 100strip_abs(beta_conv(Term `(\^y ^x. y /\ x' /\ x /\ x /\ x) x`)); 101strip_abs(beta_conv(Term `(\^y ^x. y /\ !x. y /\ x) x`)); 102strip_abs(beta_conv(Term `(\^y ^x'''' ^x''' ^x ^x'' ^x'. y) x`)); 103 104(* Note: 105 106 - strip_abs(beta_conv(Term `(\^y ^x'''' ^x''' ^x ^x'' ^x'. y) x`)); 107 > val it = ([`x''''`, `x'''`, `x'''''`, `x''`, `x'`], `x`) 108 109but 110 111 - beta_conv(Term `(\^y ^x'''' ^x''' ^x ^x'' ^x'. y) x`); 112 > val it = `\x'''' x''' x' x'' x'. x` 113 114The strip_abs only renames one bound variable to sort out the clash, 115while the step-by-step version is different: it ends up with an 116apparent shadow in the resulting scope. This isn't a bug, because the shadow 117doesn't bind anything, but still, doesn't seem quite right. 118 119In any case, the strip_abs result and the step-by-step result are different, 120which may cause some things to break, or some puzzlement. 121 122Another example: 123 124mk_abs(x,(beta_conv(Term `(\^y ^x. y /\ x) x`))); 125strip_abs it; 126 127mk_abs(x,beta_conv(mk_comb(mk_abs(z, 128mk_abs(x,(beta_conv(Term `(\^y ^x. y /\ x /\ z) x`)))),x))); 129strip_abs it; 130 131*) 132 133 134(*--------------------------------------------------------------------------- 135 dribble used to develop list_mk_binder 136 137fun enumerate [] _ acc = acc 138 | enumerate (h::t) i acc = enumerate t (i+1) ((h,i)::acc); 139 140fun mk_varmap vlist = 141 let open Polyhash 142 val vmap :(term,int) hash_table = mkPolyTable(length vlist, Fail "varmap") 143 val addin = insert vmap 144 in app addin (enumerate (rev vlist) 0 []) 145 ; vmap 146 end; 147 148fun max i [] = i 149 | max i (h::t) = max (if h>i then h else i) t; 150 151val varmap10 = mk_varmap vars10; 152val varmap100 = mk_varmap vars100; 153val varmap1K = mk_varmap vars1K; 154val varmap10K = mk_varmap vars10K; 155val varmap100K = mk_varmap vars100K; 156val varmap500K = mk_varmap vars500K; 157val varmap1M = mk_varmap vars1M; 158 159Polyhash.listItems varmap 10; 160 161max 0 (Polyhash.bucketSizes varmap10); (* 1 *) 162max 0 (Polyhash.bucketSizes varmap100); (* 2 *) 163max 0 (Polyhash.bucketSizes varmap1K); (* 3 *) 164max 0 (Polyhash.bucketSizes varmap10K); (* 4 *) 165max 0 (Polyhash.bucketSizes varmap100K); (* 4 *) 166max 0 (Polyhash.bucketSizes varmap1M); (* 5 *) (* tweaking? *) 167 168 ---------------------------------------------------------------------------*) 169