1(* ========================================================================= *) 2(* MATCHING AND UNIFICATION FOR SETS OF LITERALS *) 3(* Copyright (c) 2002-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6(* 7app load ["mlibUseful", "Mosml", "mlibTerm"]; 8*) 9 10(* 11*) 12structure mlibLiteralnet :> mlibLiteralnet = 13struct 14 15open mlibUseful mlibTerm; 16 17structure S = mlibStream; local open mlibStream in end; 18structure T = mlibTermnet; local open mlibTermnet in end; 19 20type 'a stream = 'a S.stream; 21type subst = mlibSubst.subst; 22 23val |<>| = mlibSubst.|<>|; 24 25(* ------------------------------------------------------------------------- *) 26(* Literal nets. *) 27(* ------------------------------------------------------------------------- *) 28 29type parameters = {fifo : bool}; 30 31type 'a literalnet = 32 ('a T.termnet * 'a T.termnet) * ((int * 'a list) * (int * 'a list)); 33 34fun empty p = ((T.empty p, T.empty p), ((0,[]),(0,[]))); 35 36fun insert (Atom a |-> b) ((p,n),tf) = ((T.insert (a |-> b) p, n), tf) 37 | insert (Not (Atom a) |-> b) ((p,n),tf) = ((p, T.insert (a |-> b) n), tf) 38 | insert (True |-> b) (pn,((n,l),f)) = (pn, ((n + 1, b :: l), f)) 39 | insert (False |-> b) (pn,(t,(n,l))) = (pn, (t, (n + 1, b :: l))) 40 | insert (f |-> _) _ = raise Bug ("insert: not a lit: "^formula_to_string f); 41 42local 43 fun pos ((pos, _ ), _ ) = T.size pos; 44 fun neg ((_, neg), _ ) = T.size neg; 45 fun truth (_, ((n, _), _ )) = n; 46 fun falsity (_, (_, (n, _))) = n; 47in 48 fun size l = truth l + falsity l + pos l + neg l; 49 fun size_profile l = {t = truth l, f = falsity l, p = pos l, n = neg l}; 50end; 51 52fun match ((pos,_),_) (Atom a) = T.match pos a 53 | match ((_,neg),_) (Not (Atom a)) = T.match neg a 54 | match (_,((_,t),_)) True = t 55 | match (_,(_,(_,f))) False = f 56 | match _ _ = raise Bug "match: not a literal"; 57 58fun matched ((pos,_),_) (Atom a) = T.matched pos a 59 | matched ((_,neg),_) (Not (Atom a)) = T.matched neg a 60 | matched (_,((_,t),_)) True = t 61 | matched (_,(_,(_,f))) False = f 62 | matched _ _ = raise Bug "matched: not a literal"; 63 64fun unify ((pos,_),_) (Atom a) = T.unify pos a 65 | unify ((_,neg),_) (Not (Atom a)) = T.unify neg a 66 | unify (_,((_,t),_)) True = t 67 | unify (_,(_,(_,f))) False = f 68 | unify _ _ = raise Bug "unify: not a literal"; 69 70fun filter pred = 71 let 72 fun filt (_,l) = let val l = List.filter pred l in (length l, l) end 73 in 74 fn ((pos,neg),(t,f)) => 75 ((T.filter pred pos, T.filter pred neg), (filt t, filt f)) 76 end; 77 78fun from_maplets p l = foldl (uncurry insert) (empty p) l; 79 80fun to_maplets ((pos,neg),((_,t),(_,f))) = 81 map (fn x => True |-> x) t @ 82 map (fn x => False |-> x) f @ 83 map (fn t |-> x => Atom t |-> x) (T.to_maplets pos) @ 84 map (fn t |-> x => Not (Atom t) |-> x) (T.to_maplets neg); 85 86fun pp_literalnet pp_a = 87 pp_map to_maplets (pp_list (pp_maplet pp_formula pp_a)); 88 89end 90