1 (* ========================================================================= *) |
|
2 (* FIRST ORDER LOGIC ATOMS *) |
|
3 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) |
|
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 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 (* ------------------------------------------------------------------------- *) |
|
74 (* Subterms. *) |
|
75 (* ------------------------------------------------------------------------- *) |
|
76 |
|
77 fun subterm _ [] = raise Bug "Atom.subterm: empty path" |
|
78 | subterm ((_,tms) : atom) (h :: t) = |
|
79 if h >= length tms then raise Error "Atom.subterm: bad path" |
|
80 else Term.subterm (List.nth (tms,h)) t; |
|
81 |
|
82 fun subterms ((_,tms) : atom) = |
|
83 let |
|
84 fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l |
|
85 in |
|
86 foldl f [] (enumerate tms) |
|
87 end; |
|
88 |
|
89 fun replace _ ([],_) = raise Bug "Atom.replace: empty path" |
|
90 | replace (atm as (rel,tms)) (h :: t, res) : atom = |
|
91 if h >= length tms then raise Error "Atom.replace: bad path" |
|
92 else |
|
93 let |
|
94 val tm = List.nth (tms,h) |
|
95 val tm' = Term.replace tm (t,res) |
|
96 in |
|
97 if Sharing.pointerEqual (tm,tm') then atm |
|
98 else (rel, updateNth (h,tm') tms) |
|
99 end; |
|
100 |
|
101 fun find pred = |
|
102 let |
|
103 fun f (i,tm) = |
|
104 case Term.find pred tm of |
|
105 SOME path => SOME (i :: path) |
|
106 | NONE => NONE |
|
107 in |
|
108 fn (_,tms) : atom => first f (enumerate tms) |
|
109 end; |
|
110 |
|
111 (* ------------------------------------------------------------------------- *) |
|
112 (* Free variables. *) |
|
113 (* ------------------------------------------------------------------------- *) |
|
114 |
|
115 fun freeIn v atm = List.exists (Term.freeIn v) (arguments atm); |
|
116 |
|
117 val freeVars = |
|
118 let |
|
119 fun f (tm,acc) = NameSet.union (Term.freeVars tm) acc |
|
120 in |
|
121 fn atm => foldl f NameSet.empty (arguments atm) |
|
122 end; |
|
123 |
|
124 (* ------------------------------------------------------------------------- *) |
|
125 (* Substitutions. *) |
|
126 (* ------------------------------------------------------------------------- *) |
|
127 |
|
128 fun subst sub (atm as (p,tms)) : atom = |
|
129 let |
|
130 val tms' = Sharing.map (Subst.subst sub) tms |
|
131 in |
|
132 if Sharing.pointerEqual (tms',tms) then atm else (p,tms') |
|
133 end; |
|
134 |
|
135 (* ------------------------------------------------------------------------- *) |
|
136 (* Matching. *) |
|
137 (* ------------------------------------------------------------------------- *) |
|
138 |
|
139 local |
|
140 fun matchArg ((tm1,tm2),sub) = Subst.match sub tm1 tm2; |
|
141 in |
|
142 fun match sub (p1,tms1) (p2,tms2) = |
|
143 let |
|
144 val _ = (p1 = p2 andalso length tms1 = length tms2) orelse |
|
145 raise Error "Atom.match" |
|
146 in |
|
147 foldl matchArg sub (zip tms1 tms2) |
|
148 end; |
|
149 end; |
|
150 |
|
151 (* ------------------------------------------------------------------------- *) |
|
152 (* Unification. *) |
|
153 (* ------------------------------------------------------------------------- *) |
|
154 |
|
155 local |
|
156 fun unifyArg ((tm1,tm2),sub) = Subst.unify sub tm1 tm2; |
|
157 in |
|
158 fun unify sub (p1,tms1) (p2,tms2) = |
|
159 let |
|
160 val _ = (p1 = p2 andalso length tms1 = length tms2) orelse |
|
161 raise Error "Atom.unify" |
|
162 in |
|
163 foldl unifyArg sub (zip tms1 tms2) |
|
164 end; |
|
165 end; |
|
166 |
|
167 (* ------------------------------------------------------------------------- *) |
|
168 (* The equality relation. *) |
|
169 (* ------------------------------------------------------------------------- *) |
|
170 |
|
171 val eqName = "="; |
|
172 |
|
173 val eqArity = 2; |
|
174 |
|
175 val eqRelation = (eqName,eqArity); |
|
176 |
|
177 val mkEq = mkBinop eqName; |
|
178 |
|
179 fun destEq x = destBinop eqName x; |
|
180 |
|
181 fun isEq x = isBinop eqName x; |
|
182 |
|
183 fun mkRefl tm = mkEq (tm,tm); |
|
184 |
|
185 fun destRefl atm = |
|
186 let |
|
187 val (l,r) = destEq atm |
|
188 val _ = l = r orelse raise Error "Atom.destRefl" |
|
189 in |
|
190 l |
|
191 end; |
|
192 |
|
193 fun isRefl x = can destRefl x; |
|
194 |
|
195 fun sym atm = |
|
196 let |
|
197 val (l,r) = destEq atm |
|
198 val _ = l <> r orelse raise Error "Atom.sym: refl" |
|
199 in |
|
200 mkEq (r,l) |
|
201 end; |
|
202 |
|
203 fun lhs atm = fst (destEq atm); |
|
204 |
|
205 fun rhs atm = snd (destEq atm); |
|
206 |
|
207 (* ------------------------------------------------------------------------- *) |
|
208 (* Special support for terms with type annotations. *) |
|
209 (* ------------------------------------------------------------------------- *) |
|
210 |
|
211 fun typedSymbols ((_,tms) : atom) = |
|
212 foldl (fn (tm,z) => Term.typedSymbols tm + z) 1 tms; |
|
213 |
|
214 fun nonVarTypedSubterms (_,tms) = |
|
215 let |
|
216 fun addArg ((n,arg),acc) = |
|
217 let |
|
218 fun addTm ((path,tm),acc) = (n :: path, tm) :: acc |
|
219 in |
|
220 foldl addTm acc (Term.nonVarTypedSubterms arg) |
|
221 end |
|
222 in |
|
223 foldl addArg [] (enumerate tms) |
|
224 end; |
|
225 |
|
226 (* ------------------------------------------------------------------------- *) |
|
227 (* Parsing and pretty printing. *) |
|
228 (* ------------------------------------------------------------------------- *) |
|
229 |
|
230 val pp = Parser.ppMap Term.Fn Term.pp; |
|
231 |
|
232 val toString = Parser.toString pp; |
|
233 |
|
234 fun fromString s = Term.destFn (Term.fromString s); |
|
235 |
|
236 val parse = Parser.parseQuotation Term.toString fromString; |
|
237 |
|
238 end |
|
239 |
|
240 structure AtomOrdered = |
|
241 struct type t = Atom.atom val compare = Atom.compare end |
|
242 |
|
243 structure AtomSet = ElementSet (AtomOrdered); |
|
244 |
|
245 structure AtomMap = KeyMap (AtomOrdered); |
|