39348
|
1 |
(* ========================================================================= *)
|
|
2 |
(* FIRST ORDER LOGIC ATOMS *)
|
|
3 |
(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
|
|
4 |
(* ========================================================================= *)
|
|
5 |
|
|
6 |
structure Atom :> Atom =
|
|
7 |
struct
|
|
8 |
|
|
9 |
open Useful;
|
|
10 |
|
|
11 |
(* ------------------------------------------------------------------------- *)
|
|
12 |
(* A type for storing first order logic atoms. *)
|
|
13 |
(* ------------------------------------------------------------------------- *)
|
|
14 |
|
|
15 |
type relationName = Name.name;
|
|
16 |
|
|
17 |
type relation = relationName * int;
|
|
18 |
|
|
19 |
type atom = relationName * Term.term list;
|
|
20 |
|
|
21 |
(* ------------------------------------------------------------------------- *)
|
|
22 |
(* Constructors and destructors. *)
|
|
23 |
(* ------------------------------------------------------------------------- *)
|
|
24 |
|
|
25 |
fun name ((rel,_) : atom) = rel;
|
|
26 |
|
|
27 |
fun arguments ((_,args) : atom) = args;
|
|
28 |
|
|
29 |
fun arity atm = length (arguments atm);
|
|
30 |
|
|
31 |
fun relation atm = (name atm, arity atm);
|
|
32 |
|
|
33 |
val functions =
|
|
34 |
let
|
|
35 |
fun f (tm,acc) = NameAritySet.union (Term.functions tm) acc
|
|
36 |
in
|
|
37 |
fn atm => foldl f NameAritySet.empty (arguments atm)
|
|
38 |
end;
|
|
39 |
|
|
40 |
val functionNames =
|
|
41 |
let
|
|
42 |
fun f (tm,acc) = NameSet.union (Term.functionNames tm) acc
|
|
43 |
in
|
|
44 |
fn atm => foldl f NameSet.empty (arguments atm)
|
|
45 |
end;
|
|
46 |
|
|
47 |
(* Binary relations *)
|
|
48 |
|
|
49 |
fun mkBinop p (a,b) : atom = (p,[a,b]);
|
|
50 |
|
|
51 |
fun destBinop p (x,[a,b]) =
|
|
52 |
if Name.equal x p then (a,b) else raise Error "Atom.destBinop: wrong binop"
|
|
53 |
| destBinop _ _ = raise Error "Atom.destBinop: not a binop";
|
|
54 |
|
|
55 |
fun isBinop p = can (destBinop p);
|
|
56 |
|
|
57 |
(* ------------------------------------------------------------------------- *)
|
|
58 |
(* The size of an atom in symbols. *)
|
|
59 |
(* ------------------------------------------------------------------------- *)
|
|
60 |
|
|
61 |
fun symbols atm = foldl (fn (tm,z) => Term.symbols tm + z) 1 (arguments atm);
|
|
62 |
|
|
63 |
(* ------------------------------------------------------------------------- *)
|
|
64 |
(* A total comparison function for atoms. *)
|
|
65 |
(* ------------------------------------------------------------------------- *)
|
|
66 |
|
|
67 |
fun compare ((p1,tms1),(p2,tms2)) =
|
|
68 |
case Name.compare (p1,p2) of
|
|
69 |
LESS => LESS
|
|
70 |
| EQUAL => lexCompare Term.compare (tms1,tms2)
|
|
71 |
| GREATER => GREATER;
|
|
72 |
|
|
73 |
fun equal atm1 atm2 = compare (atm1,atm2) = EQUAL;
|
|
74 |
|
|
75 |
(* ------------------------------------------------------------------------- *)
|
|
76 |
(* Subterms. *)
|
|
77 |
(* ------------------------------------------------------------------------- *)
|
|
78 |
|
|
79 |
fun subterm _ [] = raise Bug "Atom.subterm: empty path"
|
|
80 |
| subterm ((_,tms) : atom) (h :: t) =
|
|
81 |
if h >= length tms then raise Error "Atom.subterm: bad path"
|
|
82 |
else Term.subterm (List.nth (tms,h)) t;
|
|
83 |
|
|
84 |
fun subterms ((_,tms) : atom) =
|
|
85 |
let
|
|
86 |
fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
|
|
87 |
in
|
|
88 |
foldl f [] (enumerate tms)
|
|
89 |
end;
|
|
90 |
|
|
91 |
fun replace _ ([],_) = raise Bug "Atom.replace: empty path"
|
|
92 |
| replace (atm as (rel,tms)) (h :: t, res) : atom =
|
|
93 |
if h >= length tms then raise Error "Atom.replace: bad path"
|
|
94 |
else
|
|
95 |
let
|
|
96 |
val tm = List.nth (tms,h)
|
|
97 |
val tm' = Term.replace tm (t,res)
|
|
98 |
in
|
|
99 |
if Portable.pointerEqual (tm,tm') then atm
|
|
100 |
else (rel, updateNth (h,tm') tms)
|
|
101 |
end;
|
|
102 |
|
|
103 |
fun find pred =
|
|
104 |
let
|
|
105 |
fun f (i,tm) =
|
|
106 |
case Term.find pred tm of
|
|
107 |
SOME path => SOME (i :: path)
|
|
108 |
| NONE => NONE
|
|
109 |
in
|
|
110 |
fn (_,tms) : atom => first f (enumerate tms)
|
|
111 |
end;
|
|
112 |
|
|
113 |
(* ------------------------------------------------------------------------- *)
|
|
114 |
(* Free variables. *)
|
|
115 |
(* ------------------------------------------------------------------------- *)
|
|
116 |
|
|
117 |
fun freeIn v atm = List.exists (Term.freeIn v) (arguments atm);
|
|
118 |
|
|
119 |
val freeVars =
|
|
120 |
let
|
|
121 |
fun f (tm,acc) = NameSet.union (Term.freeVars tm) acc
|
|
122 |
in
|
|
123 |
fn atm => foldl f NameSet.empty (arguments atm)
|
|
124 |
end;
|
|
125 |
|
|
126 |
(* ------------------------------------------------------------------------- *)
|
|
127 |
(* Substitutions. *)
|
|
128 |
(* ------------------------------------------------------------------------- *)
|
|
129 |
|
|
130 |
fun subst sub (atm as (p,tms)) : atom =
|
|
131 |
let
|
|
132 |
val tms' = Sharing.map (Subst.subst sub) tms
|
|
133 |
in
|
|
134 |
if Portable.pointerEqual (tms',tms) then atm else (p,tms')
|
|
135 |
end;
|
|
136 |
|
|
137 |
(* ------------------------------------------------------------------------- *)
|
|
138 |
(* Matching. *)
|
|
139 |
(* ------------------------------------------------------------------------- *)
|
|
140 |
|
|
141 |
local
|
|
142 |
fun matchArg ((tm1,tm2),sub) = Subst.match sub tm1 tm2;
|
|
143 |
in
|
|
144 |
fun match sub (p1,tms1) (p2,tms2) =
|
|
145 |
let
|
|
146 |
val _ = (Name.equal p1 p2 andalso length tms1 = length tms2) orelse
|
|
147 |
raise Error "Atom.match"
|
|
148 |
in
|
|
149 |
foldl matchArg sub (zip tms1 tms2)
|
|
150 |
end;
|
|
151 |
end;
|
|
152 |
|
|
153 |
(* ------------------------------------------------------------------------- *)
|
|
154 |
(* Unification. *)
|
|
155 |
(* ------------------------------------------------------------------------- *)
|
|
156 |
|
|
157 |
local
|
|
158 |
fun unifyArg ((tm1,tm2),sub) = Subst.unify sub tm1 tm2;
|
|
159 |
in
|
|
160 |
fun unify sub (p1,tms1) (p2,tms2) =
|
|
161 |
let
|
|
162 |
val _ = (Name.equal p1 p2 andalso length tms1 = length tms2) orelse
|
|
163 |
raise Error "Atom.unify"
|
|
164 |
in
|
|
165 |
foldl unifyArg sub (zip tms1 tms2)
|
|
166 |
end;
|
|
167 |
end;
|
|
168 |
|
|
169 |
(* ------------------------------------------------------------------------- *)
|
|
170 |
(* The equality relation. *)
|
|
171 |
(* ------------------------------------------------------------------------- *)
|
|
172 |
|
|
173 |
val eqRelationName = Name.fromString "=";
|
|
174 |
|
|
175 |
val eqRelationArity = 2;
|
|
176 |
|
|
177 |
val eqRelation = (eqRelationName,eqRelationArity);
|
|
178 |
|
|
179 |
val mkEq = mkBinop eqRelationName;
|
|
180 |
|
|
181 |
fun destEq x = destBinop eqRelationName x;
|
|
182 |
|
|
183 |
fun isEq x = isBinop eqRelationName x;
|
|
184 |
|
|
185 |
fun mkRefl tm = mkEq (tm,tm);
|
|
186 |
|
|
187 |
fun destRefl atm =
|
|
188 |
let
|
|
189 |
val (l,r) = destEq atm
|
|
190 |
val _ = Term.equal l r orelse raise Error "Atom.destRefl"
|
|
191 |
in
|
|
192 |
l
|
|
193 |
end;
|
|
194 |
|
|
195 |
fun isRefl x = can destRefl x;
|
|
196 |
|
|
197 |
fun sym atm =
|
|
198 |
let
|
|
199 |
val (l,r) = destEq atm
|
|
200 |
val _ = not (Term.equal l r) orelse raise Error "Atom.sym: refl"
|
|
201 |
in
|
|
202 |
mkEq (r,l)
|
|
203 |
end;
|
|
204 |
|
|
205 |
fun lhs atm = fst (destEq atm);
|
|
206 |
|
|
207 |
fun rhs atm = snd (destEq atm);
|
|
208 |
|
|
209 |
(* ------------------------------------------------------------------------- *)
|
|
210 |
(* Special support for terms with type annotations. *)
|
|
211 |
(* ------------------------------------------------------------------------- *)
|
|
212 |
|
|
213 |
fun typedSymbols ((_,tms) : atom) =
|
|
214 |
foldl (fn (tm,z) => Term.typedSymbols tm + z) 1 tms;
|
|
215 |
|
|
216 |
fun nonVarTypedSubterms (_,tms) =
|
|
217 |
let
|
|
218 |
fun addArg ((n,arg),acc) =
|
|
219 |
let
|
|
220 |
fun addTm ((path,tm),acc) = (n :: path, tm) :: acc
|
|
221 |
in
|
|
222 |
foldl addTm acc (Term.nonVarTypedSubterms arg)
|
|
223 |
end
|
|
224 |
in
|
|
225 |
foldl addArg [] (enumerate tms)
|
|
226 |
end;
|
|
227 |
|
|
228 |
(* ------------------------------------------------------------------------- *)
|
|
229 |
(* Parsing and pretty printing. *)
|
|
230 |
(* ------------------------------------------------------------------------- *)
|
|
231 |
|
|
232 |
val pp = Print.ppMap Term.Fn Term.pp;
|
|
233 |
|
|
234 |
val toString = Print.toString pp;
|
|
235 |
|
|
236 |
fun fromString s = Term.destFn (Term.fromString s);
|
|
237 |
|
|
238 |
val parse = Parse.parseQuotation Term.toString fromString;
|
|
239 |
|
|
240 |
end
|
|
241 |
|
|
242 |
structure AtomOrdered =
|
|
243 |
struct type t = Atom.atom val compare = Atom.compare end
|
|
244 |
|
|
245 |
structure AtomMap = KeyMap (AtomOrdered);
|
|
246 |
|
|
247 |
structure AtomSet = ElementSet (AtomMap);
|