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