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