# HG changeset patch # User krauss # Date 1172655370 -3600 # Node ID 44679bbcf43be123c7e930537f6ebe00e9120802 # Parent a7263f3304943d199032e87473b0d0e1ba3bfbad cleanup, fixing sml/nj related problems diff -r a7263f330494 -r 44679bbcf43b src/HOL/Library/size_change_termination.ML --- a/src/HOL/Library/size_change_termination.ML Wed Feb 28 00:22:26 2007 +0100 +++ b/src/HOL/Library/size_change_termination.ML Wed Feb 28 10:36:10 2007 +0100 @@ -182,8 +182,8 @@ -val mk_number = HOLogic.mk_nat -val dest_number = HOLogic.dest_nat +val mk_number = HOLogic.mk_nat o IntInf.fromInt +val dest_number = IntInf.toInt o HOLogic.dest_nat fun nums_to i = map mk_number (0 upto (i - 1)) @@ -343,10 +343,6 @@ |> simple_result -fun pr_tac (st : thm) = Seq.single (Output.warning (PolyML.makestring st); st) -fun pr_thm (st : thm) = (Output.warning (PolyML.makestring st); st) - - fun build_approximating_graph thy Dtab Mtab Mss mlens mint nint = let val D1 = Dtab mint and D2 = Dtab nint @@ -480,398 +476,6 @@ end - - - - - - - - - - -(* Faster implementation of transitive closures *) - -(* sedge: Only relevant edges. Qtrees have separate value for 0 *) -datatype sedge = LESS | LEQ | BOTH - - - -datatype key = KHere | K0 of key | K1 of key - -datatype 'a stree = - sLeaf of 'a - | sBranch of ('a * 'a stree * 'a stree) - -(* -fun lookup (sLeaf x) KHere = x - | lookup (sBranch x s t) KHere = x - | lookup (sBranch x s t) (K0 k) = lookup s k - | lookup (sBranch x s t) (K1 k) = lookup t k - | lookup _ _ = raise Match -*) - -datatype 'a qtree = - QEmpty - | QNode of 'a - | QQuad of ('a qtree * 'a qtree * 'a qtree * 'a qtree) - -fun qlookup z QEmpty k l = z - | qlookup z (QNode S) k l = S - | qlookup z (QQuad (a, b, c, d)) (K0 k) (K0 l) = qlookup z a k l - | qlookup z (QQuad (a, b, c, d)) (K0 k) (K1 l) = qlookup z b k l - | qlookup z (QQuad (a, b, c, d)) (K1 k) (K0 l) = qlookup z c k l - | qlookup z (QQuad (a, b, c, d)) (K1 k) (K1 l) = qlookup z d k l - | qlookup _ _ _ _ = raise Match - - - -(* Size-change graphs *) - -type - scg = sedge qtree - - -(* addition of single edges *) -fun add_sedge BOTH _ = BOTH - | add_sedge LESS LESS = LESS - | add_sedge LESS _ = BOTH - | add_sedge LEQ LEQ = LEQ - | add_sedge LEQ _ = BOTH - -fun mult_sedge LESS _ = LESS - | mult_sedge _ LESS = LESS - | mult_sedge LEQ x = x - | mult_sedge BOTH _ = BOTH - -fun subsumes_edge LESS LESS = true - | subsumes_edge LEQ _ = true - | subsumes_edge _ _ = false - - - - -(* subsumes_SCG G H := G contains strictly less estimations than H *) -fun subsumes_SCG (QEmpty : scg) (H : scg) = true - | subsumes_SCG (QQuad (a, b, c, d)) (QQuad (e,f,g,h)) = - (subsumes_SCG a e) andalso (subsumes_SCG b f) - andalso (subsumes_SCG c g) andalso (subsumes_SCG d h) - | subsumes_SCG (QNode e) (QNode e') = subsumes_edge e e' - | subsumes_SCG _ QEmpty = false - | subsumes_SCG _ _ = raise Match - - -(* managing lists of SCGs. *) - -(* - Graphs are partially ordered. A list of graphs has the invariant that no G,H with G <= H. - To maintain this when adding a new graph G, check - (1) G <= H for some H in l => Do nothing - (2) has to be added. Then, all H <= G can be removed. - - We can check (2) first, removing all smaller graphs. - If we could remove at least one, just add G in the end (Invariant!). - Otherwise, check again, if G needs to be added at all. - - OTOH, doing (1) first is probably better, because it does not produce garbage unless needed. - - The definition is tail-recursive. Order is not preserved (unneccessary). -*) - - - -fun add_scg' G Hs = (* returns a flag indicating if the graph was really added *) - if exists (fn H => subsumes_SCG H G) Hs then (false, Hs) (* redundant addition *) - else (true, G :: remove (uncurry subsumes_SCG) G Hs) (* remove all new redundancy and add G *) - (* NB: This does the second checks twice :-( *) - -(* Simpler version *) -fun add_scg' G Hs = (not (member (op =) Hs G), insert (op =) G Hs) - - -val add_scg = snd oo add_scg' (* without flag *) - - - - - -(* quadtrees *) - -fun keylen 0 = 0 - | keylen n = (keylen (n div 2)) + 1 - -fun mk_key 0 _ = KHere - | mk_key l m = if m mod 2 = 0 - then K0 (mk_key (l - 1) (m div 2)) - else K1 (mk_key (l - 1) (m div 2)) - - -fun qupdate f KHere KHere n = f n - | qupdate f (K0 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (qupdate f k k' a, b, c, d) - | qupdate f (K0 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, qupdate f k k' b, c, d) - | qupdate f (K1 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (a, b, qupdate f k k' c, d) - | qupdate f (K1 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, b, c, qupdate f k k' d) - - - - - - - - -(* quadtree composition *) - -fun qadd A QEmpty q = q - | qadd A q QEmpty = q - | qadd A (QNode s) (QNode t) = QNode (A s t) - | qadd A (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) = - QQuad (qadd A a e, qadd A b f, qadd A c g, qadd A d h) - | qadd _ _ _ = raise Match - - -fun qmult A m QEmpty H = QEmpty - | qmult A m G QEmpty = QEmpty - | qmult A m (QNode x) (QNode y) = QNode (m x y) - | qmult A m (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) = - QQuad ((qadd A (qmult A m a e) (qmult A m b g)), - (qadd A (qmult A m a f) (qmult A m b h)), - (qadd A (qmult A m c e) (qmult A m d g)), - (qadd A (qmult A m c f) (qmult A m d h))) - | qmult _ _ _ _ = raise Match - - -val (mult_scg : scg -> scg -> scg) = qmult add_sedge mult_sedge - -(* Misc notes: - -- When building the tcl: Check on addition and raise FAIL if the property is not true... (pract) - -- Can we reduce subsumption checking by some integer fingerprints? - - Number of edges: LESS(G) LEQ(G) - G <= H ==> E(G) <= E(H) - - - -How to check: - -For each pair of adjacent edges: n -> m -> q - compute all product SCGS and check if they are subsumed by something in the tcl. - - all midnode m: all fromnode n: all tonode q: alledges (n,m) e: alledges (m,q) e': subsumes (e*e') (edgs m,q) - - This is still quite a lot of checking... But: no garbage, just inspection. Can probably be done in logic. - -*) - - - -(* Operations on lists: These preserve the invariants *) -fun SCGs_mult Gs Hs = fold (fn (G,H) => add_scg (mult_scg G H)) (product Gs Hs) [] -val SCGs_plus = fold add_scg - - -fun add_scgs Gs Hs = fold_rev (fn G => fn (Xs,As) => - let val (b, Xs') = add_scg' G Xs - in (Xs', if b then G::As else As) end) - Gs (Hs,[]) - -(* Transitive Closure for lists of SCGs *) -fun SCGs_tcl Gs = - let - fun aux S [] = S - | aux S (H::HS) = - let val (S', Ns) = add_scgs (map (mult_scg H) Gs) S - in aux S' (SCGs_plus Ns HS) end - in - aux Gs Gs - end - - - -(* Kleene algorithm: DP version, with imperative array... *) - - - - -(* Terrible imperative stuff: *) -type matrix = scg list array array - -fun mupdate i j f M = - let - val row = Array.sub (M, i) - val x = Array.sub (row, j) - in - Array.update (row, j, f x) - end - -fun mget i j M = Array.sub(Array.sub(M,i),j) - -fun print_scg (x : scg) = Output.warning (PolyML.makestring x); - - -fun kleene add mult tcl M = - let - val n = Array.length M - - fun update Mkk i j k = - let - val Mik = mget i k M - val Mkj = mget k j M - in - mupdate i j (fn X => X |> add (mult Mik (mult Mkk Mkj)) - |> add (mult Mik Mkj)) - M - end - - fun step k () = - let - val _ = mupdate k k tcl M - val Mkk = mget k k M - - val no_k = filter_out (fn i => i = k) (0 upto (n - 1)) - val _ = fold (fn i => fold (fn j => K (update Mkk i j k)) no_k) no_k () - - val _ = fold (fn i => K (update Mkk i k k)) no_k () - - val _ = fold (fn j => K (update Mkk k j k)) no_k () - in - () - end - in - fold step (0 upto (n - 1)) () - end - -val (SCGs_kleene : matrix -> unit) = kleene SCGs_plus SCGs_mult SCGs_tcl - - -fun andop x y = x andalso y -fun orop x y = x orelse y - -fun array2 n x = Array.tabulate (n, (fn i => Array.array (n, x))) - -(*val bool_kleene = kleene orop andop I - - -fun test_bool () = - let - val M = array2 2 false - val _ = mupdate 0 1 (K true) M - val _ = mupdate 1 0 (K true) M - val _ = bool_kleene M - in - M - end -*) - -(* Standard 2-2-Size-change graphs *) - -val swap = QQuad(QEmpty, QNode LEQ, - QNode LEQ, QEmpty) - -val swapRTop = QQuad(QNode LESS, QNode LEQ, - QNode LEQ, QEmpty) - -val BTopRBot = QQuad(QNode LEQ, QEmpty, - QEmpty, QNode LESS) - -val RTopBBot = QQuad(QNode LESS, QEmpty, - QEmpty, QNode LEQ) - -val R2Straight = QQuad(QNode LESS, QEmpty, - QEmpty, QNode LESS) - -val R3StraightUp = QQuad(QNode LESS, QEmpty, - QNode LESS, QNode LESS) - -val R3StraightDn = QQuad(QNode LESS, QNode LESS, - QEmpty, QNode LESS) - - - - -val diag = QQuad(QEmpty, QNode LEQ, - QEmpty, QEmpty) - -val straight = QQuad(QNode LEQ, QEmpty, - QEmpty, QEmpty) - - - -val R467913 = ([R2Straight, R3StraightDn, R3StraightDn] @ replicate 11 R2Straight @ [R3StraightUp, R3StraightUp]) - |> map single - -val swapPos = [(0,8),(0,9),(0,10),(3,4),(3,5),(11,12)] - -val BRPos = (map (pair 5) (0 :: (3 upto 7))) - @ (map (pair 8) [8,9,11,12,13]) - @ (map (pair 12) [8,9,11,12,13]) - -val RBPos = map (pair 10) (3 upto 10) - -fun afold f arr x = Array.foldl (uncurry f) x arr - -fun msize M = afold (afold (curry op + o length)) M 0 - -fun TestM () = - let - val M = array2 16 ([] : scg list) - val _ = Array.update (M, 4, Array.fromList R467913) - val _ = Array.update (M, 6, Array.fromList R467913) - val _ = Array.update (M, 7, Array.fromList R467913) - val _ = Array.update (M, 9, Array.fromList R467913) - val _ = Array.update (M, 13, Array.fromList R467913) - - val _ = map (fn (i,j) => mupdate i j (K [swap]) M) swapPos - val _ = map (fn (i,j) => mupdate i j (K [BTopRBot]) M) BRPos - val _ = map (fn (i,j) => mupdate i j (K [RTopBBot]) M) RBPos - - val _ = mupdate 1 14 (K [swapRTop]) M - val _ = mupdate 2 15 (K [swapRTop]) M - - val G = [QQuad (QNode LEQ, QNode LESS, QEmpty, QNode LESS)] - val _ = mupdate 5 1 (K G) M - val _ = mupdate 8 2 (K G) M - val _ = mupdate 12 2 (K G) M - - val G = [QQuad (QNode LESS, QEmpty, QNode LESS, QNode LEQ)] - val _ = mupdate 10 14 (K G) M - - val G = [QQuad (QEmpty, QNode LEQ, QNode LESS, QNode LESS)] - val _ = mupdate 14 1 (K G) M - val _ = mupdate 14 2 (K G) M - val _ = mupdate 15 1 (K G) M - val _ = mupdate 15 2 (K G) M - in - M - end - - - - - -fun add_edge x QEmpty = QNode x - | add_edge x (QNode y) = QNode (add_sedge x y) - - -fun sedge2ML (Const ("SCT_Definition.sedge.LESS", _)) = LESS - | sedge2ML (Const ("SCT_Definition.sedge.LEQ", _)) = LEQ - - - - - - - - - - - - - - - - end