|
1 |
|
2 structure SCT = struct |
|
3 |
|
4 fun matrix [] ys = [] |
|
5 | matrix (x::xs) ys = map (pair x) ys :: matrix xs ys |
|
6 |
|
7 fun map_matrix f xss = map (map f) xss |
|
8 |
|
9 val scgT = Sign.read_typ (the_context (), K NONE) "scg" |
|
10 val acgT = Sign.read_typ (the_context (), K NONE) "acg" |
|
11 |
|
12 fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT)) |
|
13 fun graphT nT eT = Type ("Graphs.graph", [nT, eT]) |
|
14 |
|
15 fun graph_const nT eT = Const ("Graphs.graph.Graph", HOLogic.mk_setT (edgeT nT eT) --> graphT nT eT) |
|
16 |
|
17 |
|
18 val no_step_const = "SCT_Interpretation.no_step" |
|
19 val no_step_def = thm "SCT_Interpretation.no_step_def" |
|
20 val no_stepI = thm "SCT_Interpretation.no_stepI" |
|
21 |
|
22 fun mk_no_step RD1 RD2 = |
|
23 let val RDT = fastype_of RD1 |
|
24 in Const (no_step_const, RDT --> RDT --> HOLogic.boolT) $ RD1 $ RD2 end |
|
25 |
|
26 val decr_const = "SCT_Interpretation.decr" |
|
27 val decr_def = thm "SCT_Interpretation.decr_def" |
|
28 |
|
29 fun mk_decr RD1 RD2 M1 M2 = |
|
30 let val RDT = fastype_of RD1 |
|
31 val MT = fastype_of M1 |
|
32 in Const (decr_const, RDT --> RDT --> MT --> MT --> HOLogic.boolT) $ RD1 $ RD2 $ M1 $ M2 end |
|
33 |
|
34 val decreq_const = "SCT_Interpretation.decreq" |
|
35 val decreq_def = thm "SCT_Interpretation.decreq_def" |
|
36 |
|
37 fun mk_decreq RD1 RD2 M1 M2 = |
|
38 let val RDT = fastype_of RD1 |
|
39 val MT = fastype_of M1 |
|
40 in Const (decreq_const, RDT --> RDT --> MT --> MT --> HOLogic.boolT) $ RD1 $ RD2 $ M1 $ M2 end |
|
41 |
|
42 val stepP_const = "SCT_Interpretation.stepP" |
|
43 val stepP_def = thm "SCT_Interpretation.stepP.simps" |
|
44 |
|
45 fun mk_stepP RD1 RD2 M1 M2 Rel = |
|
46 let val RDT = fastype_of RD1 |
|
47 val MT = fastype_of M1 |
|
48 in |
|
49 Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT) |
|
50 $ RD1 $ RD2 $ M1 $ M2 $ Rel |
|
51 end |
|
52 |
|
53 val approx_const = "SCT_Interpretation.approx" |
|
54 val approx_empty = thm "SCT_Interpretation.approx_empty" |
|
55 val approx_less = thm "SCT_Interpretation.approx_less" |
|
56 val approx_leq = thm "SCT_Interpretation.approx_leq" |
|
57 |
|
58 fun mk_approx G RD1 RD2 Ms1 Ms2 = |
|
59 let val RDT = fastype_of RD1 |
|
60 val MsT = fastype_of Ms1 |
|
61 in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end |
|
62 |
|
63 val sound_int_const = "SCT_Interpretation.sound_int" |
|
64 val sound_int_def = thm "SCT_Interpretation.sound_int_def" |
|
65 fun mk_sound_int A RDs M = |
|
66 let val RDsT = fastype_of RDs |
|
67 val MT = fastype_of M |
|
68 in Const (sound_int_const, acgT --> RDsT --> MT --> HOLogic.boolT) $ A $ RDs $ M end |
|
69 |
|
70 |
|
71 val nth_const = "List.nth" |
|
72 fun mk_nth xs = |
|
73 let val lT as Type (_, [T]) = fastype_of xs |
|
74 in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end |
|
75 |
|
76 |
|
77 val less_nat_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
|
78 val lesseq_nat_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
|
79 |
|
80 |
|
81 (* |
|
82 val has_edge_const = "Graphs.has_edge" |
|
83 fun mk_has_edge G n e n' = |
|
84 let val nT = fastype_of n and eT = fastype_of e |
|
85 in Const (has_edge_const, graphT nT eT --> nT --> eT --> nT --> HOLogic.boolT) $ n $ e $ n' end |
|
86 *) |
|
87 |
|
88 |
|
89 val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"] |
|
90 |
|
91 val all_less_zero = thm "SCT_Interpretation.all_less_zero" |
|
92 val all_less_Suc = thm "SCT_Interpretation.all_less_Suc" |
|
93 |
|
94 |
|
95 |
|
96 (* Lists as finite multisets *) |
|
97 |
|
98 (* --> Library *) |
|
99 fun del_index n [] = [] |
|
100 | del_index n (x :: xs) = |
|
101 if n>0 then x :: del_index (n - 1) xs else xs |
|
102 |
|
103 |
|
104 fun remove1 eq x [] = [] |
|
105 | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys |
|
106 |
|
107 |
|
108 fun multi_union eq [] ys = ys |
|
109 | multi_union eq (x::xs) ys = x :: multi_union eq xs (remove1 eq x ys) |
|
110 |
|
111 |
|
112 fun dest_ex (Const ("Ex", _) $ Abs (a as (_,T,_))) = |
|
113 let |
|
114 val (n, body) = Term.dest_abs a |
|
115 in |
|
116 (Free (n, T), body) |
|
117 end |
|
118 | dest_ex _ = raise Match |
|
119 |
|
120 fun dest_all_ex (t as (Const ("Ex",_) $ _)) = |
|
121 let |
|
122 val (v,b) = dest_ex t |
|
123 val (vs, b') = dest_all_ex b |
|
124 in |
|
125 (v :: vs, b') |
|
126 end |
|
127 | dest_all_ex t = ([],t) |
|
128 |
|
129 |
|
130 fun dist_vars [] vs = (assert (null vs) "dist_vars"; []) |
|
131 | dist_vars (T::Ts) vs = |
|
132 case find_index (fn v => fastype_of v = T) vs of |
|
133 ~1 => Free ("", T) :: dist_vars Ts vs |
|
134 | i => (nth vs i) :: dist_vars Ts (del_index i vs) |
|
135 |
|
136 |
|
137 fun dest_case rebind t = |
|
138 let |
|
139 val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t |
|
140 val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs |
|
141 in |
|
142 foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match] |
|
143 end |
|
144 |
|
145 fun bind_many [] = I |
|
146 | bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs) |
|
147 |
|
148 (* Builds relation descriptions from a relation definition *) |
|
149 fun mk_reldescs (Abs a) = |
|
150 let |
|
151 val (_, Abs a') = Term.dest_abs a |
|
152 val (_, b) = Term.dest_abs a' |
|
153 val cases = HOLogic.dest_disj b |
|
154 val (vss, bs) = split_list (map dest_all_ex cases) |
|
155 val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) [] |
|
156 val rebind = map (bind_many o dist_vars unionTs) vss |
|
157 |
|
158 val RDs = map2 dest_case rebind bs |
|
159 in |
|
160 HOLogic.mk_list (fastype_of (hd RDs)) RDs |
|
161 end |
|
162 |
|
163 fun abs_rel_tac (st : thm) = |
|
164 let |
|
165 val thy = theory_of_thm st |
|
166 val (def, rd) = HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (prems_of st))) |
|
167 val RDs = cterm_of thy (mk_reldescs def) |
|
168 val rdvar = Var (the_single (Term.add_vars rd [])) |> cterm_of thy |
|
169 in |
|
170 Seq.single (cterm_instantiate [(rdvar, RDs)] st) |
|
171 end |
|
172 |
|
173 |
|
174 (* very primitive *) |
|
175 fun measures_of RD = |
|
176 let |
|
177 val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD))))) |
|
178 val measures = LexicographicOrder.mk_base_funs domT |
|
179 in |
|
180 measures |
|
181 end |
|
182 |
|
183 |
|
184 |
|
185 val mk_number = HOLogic.mk_nat |
|
186 val dest_number = HOLogic.dest_nat |
|
187 |
|
188 fun nums_to i = map mk_number (0 upto (i - 1)) |
|
189 |
|
190 |
|
191 fun unfold_then_auto thm = |
|
192 (SIMPSET (unfold_tac [thm])) |
|
193 THEN (CLASIMPSET auto_tac) |
|
194 |
|
195 val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"] |
|
196 val nth_ss = (HOL_basic_ss addsimps nth_simps) |
|
197 val simp_nth_tac = simp_tac nth_ss |
|
198 |
|
199 |
|
200 |
|
201 fun tabulate_tlist thy l = |
|
202 let |
|
203 val n = length (HOLogic.dest_list l) |
|
204 val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1)) |
|
205 in |
|
206 the o Inttab.lookup table |
|
207 end |
|
208 |
|
209 val get_elem = snd o Logic.dest_equals o prop_of |
|
210 |
|
211 |
|
212 (* Attempt a proof of a given goal *) |
|
213 |
|
214 datatype proof_result = |
|
215 Success of thm |
|
216 | Stuck of thm |
|
217 | Fail |
|
218 | False |
|
219 | Timeout (* not implemented *) |
|
220 |
|
221 fun try_to_prove tactic cgoal = |
|
222 case SINGLE tactic (Goal.init cgoal) of |
|
223 NONE => Fail |
|
224 | SOME st => if Thm.no_prems st |
|
225 then Success (Goal.finish st) |
|
226 else if prems_of st = [HOLogic.Trueprop $ HOLogic.false_const] then False |
|
227 else Stuck st |
|
228 |
|
229 fun simple_result (Success thm) = SOME thm |
|
230 | simple_result _ = NONE |
|
231 |
|
232 |
|
233 fun inst_nums thy i j (t:thm) = |
|
234 instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t |
|
235 |
|
236 datatype call_fact = |
|
237 NoStep of thm |
|
238 | Graph of (term * thm) |
|
239 |
|
240 fun rand (_ $ t) = t |
|
241 |
|
242 fun setup_probe_goal thy domT Dtab Mtab (i, j) = |
|
243 let |
|
244 val RD1 = get_elem (Dtab i) |
|
245 val RD2 = get_elem (Dtab j) |
|
246 val Ms1 = get_elem (Mtab i) |
|
247 val Ms2 = get_elem (Mtab j) |
|
248 |
|
249 val Mst1 = HOLogic.dest_list (rand Ms1) |
|
250 val Mst2 = HOLogic.dest_list (rand Ms2) |
|
251 |
|
252 val mvar1 = Free ("sctmfv1", domT --> HOLogic.natT) |
|
253 val mvar2 = Free ("sctmfv2", domT --> HOLogic.natT) |
|
254 val relvar = Free ("sctmfrel", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
|
255 val N = length Mst1 and M = length Mst2 |
|
256 val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar) |
|
257 |> cterm_of thy |
|
258 |> Goal.init |
|
259 |> CLASIMPSET auto_tac |> Seq.hd |
|
260 |
|
261 val no_step = saved_state |
|
262 |> forall_intr (cterm_of thy relvar) |
|
263 |> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const)))) |
|
264 |> CLASIMPSET auto_tac |> Seq.hd |
|
265 |
|
266 in |
|
267 if Thm.no_prems no_step |
|
268 then NoStep (Goal.finish no_step RS no_stepI) |
|
269 else |
|
270 let |
|
271 fun set_m1 i = |
|
272 let |
|
273 val M1 = nth Mst1 i |
|
274 val with_m1 = saved_state |
|
275 |> forall_intr (cterm_of thy mvar1) |
|
276 |> forall_elim (cterm_of thy M1) |
|
277 |> CLASIMPSET auto_tac |> Seq.hd |
|
278 |
|
279 fun set_m2 j = |
|
280 let |
|
281 val M2 = nth Mst2 j |
|
282 val with_m2 = with_m1 |
|
283 |> forall_intr (cterm_of thy mvar2) |
|
284 |> forall_elim (cterm_of thy M2) |
|
285 |> CLASIMPSET auto_tac |> Seq.hd |
|
286 |
|
287 val decr = forall_intr (cterm_of thy relvar) |
|
288 #> forall_elim (cterm_of thy less_nat_const) |
|
289 #> CLASIMPSET auto_tac #> Seq.hd |
|
290 |
|
291 val decreq = forall_intr (cterm_of thy relvar) |
|
292 #> forall_elim (cterm_of thy lesseq_nat_const) |
|
293 #> CLASIMPSET auto_tac #> Seq.hd |
|
294 |
|
295 val thm1 = decr with_m2 |
|
296 in |
|
297 if Thm.no_prems thm1 |
|
298 then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1)) |
|
299 else let val thm2 = decreq with_m2 in |
|
300 if Thm.no_prems thm2 |
|
301 then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1)) |
|
302 else all_tac end |
|
303 end |
|
304 in set_m2 end |
|
305 |
|
306 val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2) |
|
307 |
|
308 val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1))) |
|
309 THEN (rtac approx_empty 1) |
|
310 |
|
311 val approx_thm = goal |
|
312 |> cterm_of thy |
|
313 |> Goal.init |
|
314 |> tac |> Seq.hd |
|
315 |> Goal.finish |
|
316 |
|
317 val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm |
|
318 in |
|
319 Graph (G, approx_thm) |
|
320 end |
|
321 end |
|
322 |
|
323 |
|
324 |
|
325 |
|
326 |
|
327 fun probe_nostep thy Dtab i j = |
|
328 HOLogic.mk_Trueprop (mk_no_step (get_elem (Dtab i)) (get_elem (Dtab j))) |
|
329 |> cterm_of thy |
|
330 |> try_to_prove (unfold_then_auto no_step_def) |
|
331 |> simple_result |
|
332 |
|
333 fun probe_decr thy RD1 RD2 m1 m2 = |
|
334 HOLogic.mk_Trueprop (mk_decr RD1 RD2 m1 m2) |
|
335 |> cterm_of thy |
|
336 |> try_to_prove (unfold_then_auto decr_def) |
|
337 |> simple_result |
|
338 |
|
339 fun probe_decreq thy RD1 RD2 m1 m2 = |
|
340 HOLogic.mk_Trueprop (mk_decreq RD1 RD2 m1 m2) |
|
341 |> cterm_of thy |
|
342 |> try_to_prove (unfold_then_auto decreq_def) |
|
343 |> simple_result |
|
344 |
|
345 |
|
346 fun pr_tac (st : thm) = Seq.single (Output.warning (PolyML.makestring st); st) |
|
347 fun pr_thm (st : thm) = (Output.warning (PolyML.makestring st); st) |
|
348 |
|
349 |
|
350 fun build_approximating_graph thy Dtab Mtab Mss mlens mint nint = |
|
351 let |
|
352 val D1 = Dtab mint and D2 = Dtab nint |
|
353 val Mst1 = Mtab mint and Mst2 = Mtab nint |
|
354 |
|
355 val RD1 = get_elem D1 and RD2 = get_elem D2 |
|
356 val Ms1 = get_elem Mst1 and Ms2 = get_elem Mst2 |
|
357 |
|
358 val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2) |
|
359 |
|
360 val Ms1 = nth (nth Mss mint) and Ms2 = nth (nth Mss mint) |
|
361 |
|
362 fun add_edge (i,j) = |
|
363 case timeap_msg ("decr(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")") |
|
364 (probe_decr thy RD1 RD2 (Ms1 i)) (Ms2 j) of |
|
365 SOME thm => (Output.warning "Success"; (rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac thm 1)) |
|
366 | NONE => case timeap_msg ("decr(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")") |
|
367 (probe_decreq thy RD1 RD2 (Ms1 i)) (Ms2 j) of |
|
368 SOME thm => (Output.warning "Success"; (rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac thm 1)) |
|
369 | NONE => all_tac |
|
370 |
|
371 val approx_thm = |
|
372 goal |
|
373 |> cterm_of thy |
|
374 |> Goal.init |
|
375 |> SINGLE ((EVERY (map add_edge (product (0 upto (nth mlens mint) - 1) (0 upto (nth mlens nint) - 1)))) |
|
376 THEN (rtac approx_empty 1)) |
|
377 |> the |
|
378 |> Goal.finish |
|
379 |
|
380 val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm |
|
381 in |
|
382 (G, approx_thm) |
|
383 end |
|
384 |
|
385 |
|
386 |
|
387 fun prove_call_fact thy Dtab Mtab Mss mlens (m, n) = |
|
388 case probe_nostep thy Dtab m n of |
|
389 SOME thm => (Output.warning "NoStep"; NoStep thm) |
|
390 | NONE => Graph (build_approximating_graph thy Dtab Mtab Mss mlens m n) |
|
391 |
|
392 |
|
393 fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n)) |
|
394 |
|
395 |
|
396 fun mk_set T [] = Const ("{}", HOLogic.mk_setT T) |
|
397 | mk_set T (x :: xs) = Const ("insert", |
|
398 T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $ mk_set T xs |
|
399 |
|
400 fun dest_set (Const ("{}", _)) = [] |
|
401 | dest_set (Const ("insert", _) $ x $ xs) = x :: dest_set xs |
|
402 |
|
403 val pr_graph = Sign.string_of_term |
|
404 |
|
405 |
|
406 fun pr_matrix thy = map_matrix (fn Graph (G, _) => pr_graph thy G | _ => "X") |
|
407 |
|
408 val in_graph_tac = |
|
409 simp_tac (HOL_basic_ss addsimps has_edge_simps) 1 |
|
410 THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *) |
|
411 |
|
412 fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1 |
|
413 | approx_tac (Graph (G, thm)) = |
|
414 rtac disjI2 1 |
|
415 THEN rtac exI 1 |
|
416 THEN rtac conjI 1 |
|
417 THEN rtac thm 2 |
|
418 THEN in_graph_tac |
|
419 |
|
420 fun all_less_tac [] = rtac all_less_zero 1 |
|
421 | all_less_tac (t :: ts) = rtac all_less_Suc 1 |
|
422 THEN simp_nth_tac 1 |
|
423 THEN t |
|
424 THEN all_less_tac ts |
|
425 |
|
426 |
|
427 val length_const = "Nat.size" |
|
428 fun mk_length l = Const (length_const, fastype_of l --> HOLogic.natT) $ l |
|
429 val length_simps = thms "SCT_Interpretation.length_simps" |
|
430 |
|
431 |
|
432 |
|
433 fun mk_call_graph (st : thm) = |
|
434 let |
|
435 val thy = theory_of_thm st |
|
436 val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st)) |
|
437 |
|
438 val RDs = HOLogic.dest_list RDlist |
|
439 val n = length RDs |
|
440 |
|
441 val Mss = map measures_of RDs |
|
442 |
|
443 val domT = domain_type (fastype_of (hd (hd Mss))) |
|
444 |
|
445 val mfuns = map (fn Ms => mk_nth (HOLogic.mk_list (fastype_of (hd Ms)) Ms)) Mss |
|
446 |> (fn l => HOLogic.mk_list (fastype_of (hd l)) l) |
|
447 |
|
448 val Dtab = tabulate_tlist thy RDlist |
|
449 val Mtab = tabulate_tlist thy mfuns |
|
450 |
|
451 val len_simp = Simplifier.rewrite (HOL_basic_ss addsimps length_simps) (cterm_of thy (mk_length RDlist)) |
|
452 |
|
453 val mlens = map length Mss |
|
454 |
|
455 val indices = (n - 1 downto 0) |
|
456 val pairs = matrix indices indices |
|
457 val parts = map_matrix (fn (n,m) => |
|
458 (timeap_msg (string_of_int n ^ "," ^ string_of_int m) |
|
459 (setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs |
|
460 |
|
461 |
|
462 val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^ |
|
463 pr_graph thy G ^ ",\n") |
|
464 | _ => I) cs) parts "" |
|
465 val _ = Output.warning s |
|
466 |
|
467 |
|
468 val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs) |
|
469 |> mk_set (edgeT HOLogic.natT scgT) |
|
470 |> curry op $ (graph_const HOLogic.natT scgT) |
|
471 |
|
472 |
|
473 val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns) |
|
474 |
|
475 val tac = |
|
476 (SIMPSET (unfold_tac [sound_int_def, len_simp])) |
|
477 THEN all_less_tac (map (all_less_tac o map approx_tac) parts) |
|
478 in |
|
479 tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st) |
|
480 end |
|
481 |
|
482 |
|
483 |
|
484 |
|
485 |
|
486 |
|
487 |
|
488 |
|
489 |
|
490 |
|
491 |
|
492 |
|
493 (* Faster implementation of transitive closures *) |
|
494 |
|
495 (* sedge: Only relevant edges. Qtrees have separate value for 0 *) |
|
496 datatype sedge = LESS | LEQ | BOTH |
|
497 |
|
498 |
|
499 |
|
500 datatype key = KHere | K0 of key | K1 of key |
|
501 |
|
502 datatype 'a stree = |
|
503 sLeaf of 'a |
|
504 | sBranch of ('a * 'a stree * 'a stree) |
|
505 |
|
506 (* |
|
507 fun lookup (sLeaf x) KHere = x |
|
508 | lookup (sBranch x s t) KHere = x |
|
509 | lookup (sBranch x s t) (K0 k) = lookup s k |
|
510 | lookup (sBranch x s t) (K1 k) = lookup t k |
|
511 | lookup _ _ = raise Match |
|
512 *) |
|
513 |
|
514 datatype 'a qtree = |
|
515 QEmpty |
|
516 | QNode of 'a |
|
517 | QQuad of ('a qtree * 'a qtree * 'a qtree * 'a qtree) |
|
518 |
|
519 fun qlookup z QEmpty k l = z |
|
520 | qlookup z (QNode S) k l = S |
|
521 | qlookup z (QQuad (a, b, c, d)) (K0 k) (K0 l) = qlookup z a k l |
|
522 | qlookup z (QQuad (a, b, c, d)) (K0 k) (K1 l) = qlookup z b k l |
|
523 | qlookup z (QQuad (a, b, c, d)) (K1 k) (K0 l) = qlookup z c k l |
|
524 | qlookup z (QQuad (a, b, c, d)) (K1 k) (K1 l) = qlookup z d k l |
|
525 | qlookup _ _ _ _ = raise Match |
|
526 |
|
527 |
|
528 |
|
529 (* Size-change graphs *) |
|
530 |
|
531 type |
|
532 scg = sedge qtree |
|
533 |
|
534 |
|
535 (* addition of single edges *) |
|
536 fun add_sedge BOTH _ = BOTH |
|
537 | add_sedge LESS LESS = LESS |
|
538 | add_sedge LESS _ = BOTH |
|
539 | add_sedge LEQ LEQ = LEQ |
|
540 | add_sedge LEQ _ = BOTH |
|
541 |
|
542 fun mult_sedge LESS _ = LESS |
|
543 | mult_sedge _ LESS = LESS |
|
544 | mult_sedge LEQ x = x |
|
545 | mult_sedge BOTH _ = BOTH |
|
546 |
|
547 fun subsumes_edge LESS LESS = true |
|
548 | subsumes_edge LEQ _ = true |
|
549 | subsumes_edge _ _ = false |
|
550 |
|
551 |
|
552 |
|
553 |
|
554 (* subsumes_SCG G H := G contains strictly less estimations than H *) |
|
555 fun subsumes_SCG (QEmpty : scg) (H : scg) = true |
|
556 | subsumes_SCG (QQuad (a, b, c, d)) (QQuad (e,f,g,h)) = |
|
557 (subsumes_SCG a e) andalso (subsumes_SCG b f) |
|
558 andalso (subsumes_SCG c g) andalso (subsumes_SCG d h) |
|
559 | subsumes_SCG (QNode e) (QNode e') = subsumes_edge e e' |
|
560 | subsumes_SCG _ QEmpty = false |
|
561 | subsumes_SCG _ _ = raise Match |
|
562 |
|
563 |
|
564 (* managing lists of SCGs. *) |
|
565 |
|
566 (* |
|
567 Graphs are partially ordered. A list of graphs has the invariant that no G,H with G <= H. |
|
568 To maintain this when adding a new graph G, check |
|
569 (1) G <= H for some H in l => Do nothing |
|
570 (2) has to be added. Then, all H <= G can be removed. |
|
571 |
|
572 We can check (2) first, removing all smaller graphs. |
|
573 If we could remove at least one, just add G in the end (Invariant!). |
|
574 Otherwise, check again, if G needs to be added at all. |
|
575 |
|
576 OTOH, doing (1) first is probably better, because it does not produce garbage unless needed. |
|
577 |
|
578 The definition is tail-recursive. Order is not preserved (unneccessary). |
|
579 *) |
|
580 |
|
581 |
|
582 |
|
583 fun add_scg' G Hs = (* returns a flag indicating if the graph was really added *) |
|
584 if exists (fn H => subsumes_SCG H G) Hs then (false, Hs) (* redundant addition *) |
|
585 else (true, G :: remove (uncurry subsumes_SCG) G Hs) (* remove all new redundancy and add G *) |
|
586 (* NB: This does the second checks twice :-( *) |
|
587 |
|
588 (* Simpler version *) |
|
589 fun add_scg' G Hs = (not (member (op =) Hs G), insert (op =) G Hs) |
|
590 |
|
591 |
|
592 val add_scg = snd oo add_scg' (* without flag *) |
|
593 |
|
594 |
|
595 |
|
596 |
|
597 |
|
598 (* quadtrees *) |
|
599 |
|
600 fun keylen 0 = 0 |
|
601 | keylen n = (keylen (n div 2)) + 1 |
|
602 |
|
603 fun mk_key 0 _ = KHere |
|
604 | mk_key l m = if m mod 2 = 0 |
|
605 then K0 (mk_key (l - 1) (m div 2)) |
|
606 else K1 (mk_key (l - 1) (m div 2)) |
|
607 |
|
608 |
|
609 fun qupdate f KHere KHere n = f n |
|
610 | qupdate f (K0 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (qupdate f k k' a, b, c, d) |
|
611 | qupdate f (K0 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, qupdate f k k' b, c, d) |
|
612 | qupdate f (K1 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (a, b, qupdate f k k' c, d) |
|
613 | qupdate f (K1 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, b, c, qupdate f k k' d) |
|
614 |
|
615 |
|
616 |
|
617 |
|
618 |
|
619 |
|
620 |
|
621 |
|
622 (* quadtree composition *) |
|
623 |
|
624 fun qadd A QEmpty q = q |
|
625 | qadd A q QEmpty = q |
|
626 | qadd A (QNode s) (QNode t) = QNode (A s t) |
|
627 | qadd A (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) = |
|
628 QQuad (qadd A a e, qadd A b f, qadd A c g, qadd A d h) |
|
629 | qadd _ _ _ = raise Match |
|
630 |
|
631 |
|
632 fun qmult A m QEmpty H = QEmpty |
|
633 | qmult A m G QEmpty = QEmpty |
|
634 | qmult A m (QNode x) (QNode y) = QNode (m x y) |
|
635 | qmult A m (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) = |
|
636 QQuad ((qadd A (qmult A m a e) (qmult A m b g)), |
|
637 (qadd A (qmult A m a f) (qmult A m b h)), |
|
638 (qadd A (qmult A m c e) (qmult A m d g)), |
|
639 (qadd A (qmult A m c f) (qmult A m d h))) |
|
640 | qmult _ _ _ _ = raise Match |
|
641 |
|
642 |
|
643 val (mult_scg : scg -> scg -> scg) = qmult add_sedge mult_sedge |
|
644 |
|
645 (* Misc notes: |
|
646 |
|
647 - When building the tcl: Check on addition and raise FAIL if the property is not true... (pract) |
|
648 |
|
649 - Can we reduce subsumption checking by some integer fingerprints? |
|
650 |
|
651 Number of edges: LESS(G) LEQ(G) |
|
652 G <= H ==> E(G) <= E(H) |
|
653 |
|
654 |
|
655 |
|
656 How to check: |
|
657 |
|
658 For each pair of adjacent edges: n -> m -> q |
|
659 compute all product SCGS and check if they are subsumed by something in the tcl. |
|
660 |
|
661 all midnode m: all fromnode n: all tonode q: alledges (n,m) e: alledges (m,q) e': subsumes (e*e') (edgs m,q) |
|
662 |
|
663 This is still quite a lot of checking... But: no garbage, just inspection. Can probably be done in logic. |
|
664 |
|
665 *) |
|
666 |
|
667 |
|
668 |
|
669 (* Operations on lists: These preserve the invariants *) |
|
670 fun SCGs_mult Gs Hs = fold (fn (G,H) => add_scg (mult_scg G H)) (product Gs Hs) [] |
|
671 val SCGs_plus = fold add_scg |
|
672 |
|
673 |
|
674 fun add_scgs Gs Hs = fold_rev (fn G => fn (Xs,As) => |
|
675 let val (b, Xs') = add_scg' G Xs |
|
676 in (Xs', if b then G::As else As) end) |
|
677 Gs (Hs,[]) |
|
678 |
|
679 (* Transitive Closure for lists of SCGs *) |
|
680 fun SCGs_tcl Gs = |
|
681 let |
|
682 fun aux S [] = S |
|
683 | aux S (H::HS) = |
|
684 let val (S', Ns) = add_scgs (map (mult_scg H) Gs) S |
|
685 in aux S' (SCGs_plus Ns HS) end |
|
686 in |
|
687 aux Gs Gs |
|
688 end |
|
689 |
|
690 |
|
691 |
|
692 (* Kleene algorithm: DP version, with imperative array... *) |
|
693 |
|
694 |
|
695 |
|
696 |
|
697 (* Terrible imperative stuff: *) |
|
698 type matrix = scg list array array |
|
699 |
|
700 fun mupdate i j f M = |
|
701 let |
|
702 val row = Array.sub (M, i) |
|
703 val x = Array.sub (row, j) |
|
704 in |
|
705 Array.update (row, j, f x) |
|
706 end |
|
707 |
|
708 fun mget i j M = Array.sub(Array.sub(M,i),j) |
|
709 |
|
710 fun print_scg (x : scg) = Output.warning (PolyML.makestring x); |
|
711 |
|
712 |
|
713 fun kleene add mult tcl M = |
|
714 let |
|
715 val n = Array.length M |
|
716 |
|
717 fun update Mkk i j k = |
|
718 let |
|
719 val Mik = mget i k M |
|
720 val Mkj = mget k j M |
|
721 in |
|
722 mupdate i j (fn X => X |> add (mult Mik (mult Mkk Mkj)) |
|
723 |> add (mult Mik Mkj)) |
|
724 M |
|
725 end |
|
726 |
|
727 fun step k () = |
|
728 let |
|
729 val _ = mupdate k k tcl M |
|
730 val Mkk = mget k k M |
|
731 |
|
732 val no_k = filter_out (fn i => i = k) (0 upto (n - 1)) |
|
733 val _ = fold (fn i => fold (fn j => K (update Mkk i j k)) no_k) no_k () |
|
734 |
|
735 val _ = fold (fn i => K (update Mkk i k k)) no_k () |
|
736 |
|
737 val _ = fold (fn j => K (update Mkk k j k)) no_k () |
|
738 in |
|
739 () |
|
740 end |
|
741 in |
|
742 fold step (0 upto (n - 1)) () |
|
743 end |
|
744 |
|
745 val (SCGs_kleene : matrix -> unit) = kleene SCGs_plus SCGs_mult SCGs_tcl |
|
746 |
|
747 |
|
748 fun andop x y = x andalso y |
|
749 fun orop x y = x orelse y |
|
750 |
|
751 fun array2 n x = Array.tabulate (n, (fn i => Array.array (n, x))) |
|
752 |
|
753 (*val bool_kleene = kleene orop andop I |
|
754 |
|
755 |
|
756 fun test_bool () = |
|
757 let |
|
758 val M = array2 2 false |
|
759 val _ = mupdate 0 1 (K true) M |
|
760 val _ = mupdate 1 0 (K true) M |
|
761 val _ = bool_kleene M |
|
762 in |
|
763 M |
|
764 end |
|
765 *) |
|
766 |
|
767 (* Standard 2-2-Size-change graphs *) |
|
768 |
|
769 val swap = QQuad(QEmpty, QNode LEQ, |
|
770 QNode LEQ, QEmpty) |
|
771 |
|
772 val swapRTop = QQuad(QNode LESS, QNode LEQ, |
|
773 QNode LEQ, QEmpty) |
|
774 |
|
775 val BTopRBot = QQuad(QNode LEQ, QEmpty, |
|
776 QEmpty, QNode LESS) |
|
777 |
|
778 val RTopBBot = QQuad(QNode LESS, QEmpty, |
|
779 QEmpty, QNode LEQ) |
|
780 |
|
781 val R2Straight = QQuad(QNode LESS, QEmpty, |
|
782 QEmpty, QNode LESS) |
|
783 |
|
784 val R3StraightUp = QQuad(QNode LESS, QEmpty, |
|
785 QNode LESS, QNode LESS) |
|
786 |
|
787 val R3StraightDn = QQuad(QNode LESS, QNode LESS, |
|
788 QEmpty, QNode LESS) |
|
789 |
|
790 |
|
791 |
|
792 |
|
793 val diag = QQuad(QEmpty, QNode LEQ, |
|
794 QEmpty, QEmpty) |
|
795 |
|
796 val straight = QQuad(QNode LEQ, QEmpty, |
|
797 QEmpty, QEmpty) |
|
798 |
|
799 |
|
800 |
|
801 val R467913 = ([R2Straight, R3StraightDn, R3StraightDn] @ replicate 11 R2Straight @ [R3StraightUp, R3StraightUp]) |
|
802 |> map single |
|
803 |
|
804 val swapPos = [(0,8),(0,9),(0,10),(3,4),(3,5),(11,12)] |
|
805 |
|
806 val BRPos = (map (pair 5) (0 :: (3 upto 7))) |
|
807 @ (map (pair 8) [8,9,11,12,13]) |
|
808 @ (map (pair 12) [8,9,11,12,13]) |
|
809 |
|
810 val RBPos = map (pair 10) (3 upto 10) |
|
811 |
|
812 fun afold f arr x = Array.foldl (uncurry f) x arr |
|
813 |
|
814 fun msize M = afold (afold (curry op + o length)) M 0 |
|
815 |
|
816 fun TestM () = |
|
817 let |
|
818 val M = array2 16 ([] : scg list) |
|
819 val _ = Array.update (M, 4, Array.fromList R467913) |
|
820 val _ = Array.update (M, 6, Array.fromList R467913) |
|
821 val _ = Array.update (M, 7, Array.fromList R467913) |
|
822 val _ = Array.update (M, 9, Array.fromList R467913) |
|
823 val _ = Array.update (M, 13, Array.fromList R467913) |
|
824 |
|
825 val _ = map (fn (i,j) => mupdate i j (K [swap]) M) swapPos |
|
826 val _ = map (fn (i,j) => mupdate i j (K [BTopRBot]) M) BRPos |
|
827 val _ = map (fn (i,j) => mupdate i j (K [RTopBBot]) M) RBPos |
|
828 |
|
829 val _ = mupdate 1 14 (K [swapRTop]) M |
|
830 val _ = mupdate 2 15 (K [swapRTop]) M |
|
831 |
|
832 val G = [QQuad (QNode LEQ, QNode LESS, QEmpty, QNode LESS)] |
|
833 val _ = mupdate 5 1 (K G) M |
|
834 val _ = mupdate 8 2 (K G) M |
|
835 val _ = mupdate 12 2 (K G) M |
|
836 |
|
837 val G = [QQuad (QNode LESS, QEmpty, QNode LESS, QNode LEQ)] |
|
838 val _ = mupdate 10 14 (K G) M |
|
839 |
|
840 val G = [QQuad (QEmpty, QNode LEQ, QNode LESS, QNode LESS)] |
|
841 val _ = mupdate 14 1 (K G) M |
|
842 val _ = mupdate 14 2 (K G) M |
|
843 val _ = mupdate 15 1 (K G) M |
|
844 val _ = mupdate 15 2 (K G) M |
|
845 in |
|
846 M |
|
847 end |
|
848 |
|
849 |
|
850 |
|
851 |
|
852 |
|
853 fun add_edge x QEmpty = QNode x |
|
854 | add_edge x (QNode y) = QNode (add_sedge x y) |
|
855 |
|
856 |
|
857 fun sedge2ML (Const ("SCT_Definition.sedge.LESS", _)) = LESS |
|
858 | sedge2ML (Const ("SCT_Definition.sedge.LEQ", _)) = LEQ |
|
859 |
|
860 |
|
861 |
|
862 |
|
863 |
|
864 |
|
865 |
|
866 |
|
867 |
|
868 |
|
869 |
|
870 |
|
871 |
|
872 |
|
873 |
|
874 |
|
875 end |
|
876 |
|
877 |
|
878 |
|
879 |
|
880 |
|
881 |