39348
|
1 |
(* ========================================================================= *)
|
|
2 |
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
|
39502
|
3 |
(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
|
39348
|
4 |
(* ========================================================================= *)
|
|
5 |
|
|
6 |
structure Subst :> Subst =
|
|
7 |
struct
|
|
8 |
|
|
9 |
open Useful;
|
|
10 |
|
|
11 |
(* ------------------------------------------------------------------------- *)
|
|
12 |
(* A type of first order logic substitutions. *)
|
|
13 |
(* ------------------------------------------------------------------------- *)
|
|
14 |
|
|
15 |
datatype subst = Subst of Term.term NameMap.map;
|
|
16 |
|
|
17 |
(* ------------------------------------------------------------------------- *)
|
|
18 |
(* Basic operations. *)
|
|
19 |
(* ------------------------------------------------------------------------- *)
|
|
20 |
|
|
21 |
val empty = Subst (NameMap.new ());
|
|
22 |
|
|
23 |
fun null (Subst m) = NameMap.null m;
|
|
24 |
|
|
25 |
fun size (Subst m) = NameMap.size m;
|
|
26 |
|
|
27 |
fun peek (Subst m) v = NameMap.peek m v;
|
|
28 |
|
|
29 |
fun insert (Subst m) v_tm = Subst (NameMap.insert m v_tm);
|
|
30 |
|
|
31 |
fun singleton v_tm = insert empty v_tm;
|
|
32 |
|
|
33 |
fun toList (Subst m) = NameMap.toList m;
|
|
34 |
|
|
35 |
fun fromList l = Subst (NameMap.fromList l);
|
|
36 |
|
|
37 |
fun foldl f b (Subst m) = NameMap.foldl f b m;
|
|
38 |
|
|
39 |
fun foldr f b (Subst m) = NameMap.foldr f b m;
|
|
40 |
|
|
41 |
fun pp sub =
|
|
42 |
Print.ppBracket "<[" "]>"
|
|
43 |
(Print.ppOpList "," (Print.ppOp2 " |->" Name.pp Term.pp))
|
|
44 |
(toList sub);
|
|
45 |
|
|
46 |
val toString = Print.toString pp;
|
|
47 |
|
|
48 |
(* ------------------------------------------------------------------------- *)
|
|
49 |
(* Normalizing removes identity substitutions. *)
|
|
50 |
(* ------------------------------------------------------------------------- *)
|
|
51 |
|
|
52 |
local
|
|
53 |
fun isNotId (v,tm) = not (Term.equalVar v tm);
|
|
54 |
in
|
|
55 |
fun normalize (sub as Subst m) =
|
|
56 |
let
|
|
57 |
val m' = NameMap.filter isNotId m
|
|
58 |
in
|
|
59 |
if NameMap.size m = NameMap.size m' then sub else Subst m'
|
|
60 |
end;
|
|
61 |
end;
|
|
62 |
|
|
63 |
(* ------------------------------------------------------------------------- *)
|
|
64 |
(* Applying a substitution to a first order logic term. *)
|
|
65 |
(* ------------------------------------------------------------------------- *)
|
|
66 |
|
|
67 |
fun subst sub =
|
|
68 |
let
|
|
69 |
fun tmSub (tm as Term.Var v) =
|
|
70 |
(case peek sub v of
|
|
71 |
SOME tm' => if Portable.pointerEqual (tm,tm') then tm else tm'
|
|
72 |
| NONE => tm)
|
|
73 |
| tmSub (tm as Term.Fn (f,args)) =
|
|
74 |
let
|
|
75 |
val args' = Sharing.map tmSub args
|
|
76 |
in
|
|
77 |
if Portable.pointerEqual (args,args') then tm
|
|
78 |
else Term.Fn (f,args')
|
|
79 |
end
|
|
80 |
in
|
|
81 |
fn tm => if null sub then tm else tmSub tm
|
|
82 |
end;
|
|
83 |
|
|
84 |
(* ------------------------------------------------------------------------- *)
|
|
85 |
(* Restricting a substitution to a given set of variables. *)
|
|
86 |
(* ------------------------------------------------------------------------- *)
|
|
87 |
|
|
88 |
fun restrict (sub as Subst m) varSet =
|
|
89 |
let
|
|
90 |
fun isRestrictedVar (v,_) = NameSet.member v varSet
|
|
91 |
|
|
92 |
val m' = NameMap.filter isRestrictedVar m
|
|
93 |
in
|
|
94 |
if NameMap.size m = NameMap.size m' then sub else Subst m'
|
|
95 |
end;
|
|
96 |
|
|
97 |
fun remove (sub as Subst m) varSet =
|
|
98 |
let
|
|
99 |
fun isRestrictedVar (v,_) = not (NameSet.member v varSet)
|
|
100 |
|
|
101 |
val m' = NameMap.filter isRestrictedVar m
|
|
102 |
in
|
|
103 |
if NameMap.size m = NameMap.size m' then sub else Subst m'
|
|
104 |
end;
|
|
105 |
|
|
106 |
(* ------------------------------------------------------------------------- *)
|
|
107 |
(* Composing two substitutions so that the following identity holds: *)
|
|
108 |
(* *)
|
|
109 |
(* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *)
|
|
110 |
(* ------------------------------------------------------------------------- *)
|
|
111 |
|
|
112 |
fun compose (sub1 as Subst m1) sub2 =
|
|
113 |
let
|
|
114 |
fun f (v,tm,s) = insert s (v, subst sub2 tm)
|
|
115 |
in
|
|
116 |
if null sub2 then sub1 else NameMap.foldl f sub2 m1
|
|
117 |
end;
|
|
118 |
|
|
119 |
(* ------------------------------------------------------------------------- *)
|
|
120 |
(* Creating the union of two compatible substitutions. *)
|
|
121 |
(* ------------------------------------------------------------------------- *)
|
|
122 |
|
|
123 |
local
|
|
124 |
fun compatible ((_,tm1),(_,tm2)) =
|
|
125 |
if Term.equal tm1 tm2 then SOME tm1
|
|
126 |
else raise Error "Subst.union: incompatible";
|
|
127 |
in
|
|
128 |
fun union (s1 as Subst m1) (s2 as Subst m2) =
|
|
129 |
if NameMap.null m1 then s2
|
|
130 |
else if NameMap.null m2 then s1
|
|
131 |
else Subst (NameMap.union compatible m1 m2);
|
|
132 |
end;
|
|
133 |
|
|
134 |
(* ------------------------------------------------------------------------- *)
|
|
135 |
(* Substitutions can be inverted iff they are renaming substitutions. *)
|
|
136 |
(* ------------------------------------------------------------------------- *)
|
|
137 |
|
|
138 |
local
|
|
139 |
fun inv (v, Term.Var w, s) =
|
|
140 |
if NameMap.inDomain w s then raise Error "Subst.invert: non-injective"
|
|
141 |
else NameMap.insert s (w, Term.Var v)
|
|
142 |
| inv (_, Term.Fn _, _) = raise Error "Subst.invert: non-variable";
|
|
143 |
in
|
|
144 |
fun invert (Subst m) = Subst (NameMap.foldl inv (NameMap.new ()) m);
|
|
145 |
end;
|
|
146 |
|
|
147 |
val isRenaming = can invert;
|
|
148 |
|
|
149 |
(* ------------------------------------------------------------------------- *)
|
|
150 |
(* Creating a substitution to freshen variables. *)
|
|
151 |
(* ------------------------------------------------------------------------- *)
|
|
152 |
|
|
153 |
val freshVars =
|
|
154 |
let
|
|
155 |
fun add (v,m) = insert m (v, Term.newVar ())
|
|
156 |
in
|
|
157 |
NameSet.foldl add empty
|
|
158 |
end;
|
|
159 |
|
|
160 |
(* ------------------------------------------------------------------------- *)
|
|
161 |
(* Free variables. *)
|
|
162 |
(* ------------------------------------------------------------------------- *)
|
|
163 |
|
|
164 |
val redexes =
|
|
165 |
let
|
|
166 |
fun add (v,_,s) = NameSet.add s v
|
|
167 |
in
|
|
168 |
foldl add NameSet.empty
|
|
169 |
end;
|
|
170 |
|
|
171 |
val residueFreeVars =
|
|
172 |
let
|
|
173 |
fun add (_,t,s) = NameSet.union s (Term.freeVars t)
|
|
174 |
in
|
|
175 |
foldl add NameSet.empty
|
|
176 |
end;
|
|
177 |
|
|
178 |
val freeVars =
|
|
179 |
let
|
|
180 |
fun add (v,t,s) = NameSet.union (NameSet.add s v) (Term.freeVars t)
|
|
181 |
in
|
|
182 |
foldl add NameSet.empty
|
|
183 |
end;
|
|
184 |
|
|
185 |
(* ------------------------------------------------------------------------- *)
|
|
186 |
(* Functions. *)
|
|
187 |
(* ------------------------------------------------------------------------- *)
|
|
188 |
|
|
189 |
val functions =
|
|
190 |
let
|
|
191 |
fun add (_,t,s) = NameAritySet.union s (Term.functions t)
|
|
192 |
in
|
|
193 |
foldl add NameAritySet.empty
|
|
194 |
end;
|
|
195 |
|
|
196 |
(* ------------------------------------------------------------------------- *)
|
|
197 |
(* Matching for first order logic terms. *)
|
|
198 |
(* ------------------------------------------------------------------------- *)
|
|
199 |
|
|
200 |
local
|
|
201 |
fun matchList sub [] = sub
|
|
202 |
| matchList sub ((Term.Var v, tm) :: rest) =
|
|
203 |
let
|
|
204 |
val sub =
|
|
205 |
case peek sub v of
|
|
206 |
NONE => insert sub (v,tm)
|
|
207 |
| SOME tm' =>
|
|
208 |
if Term.equal tm tm' then sub
|
|
209 |
else raise Error "Subst.match: incompatible matches"
|
|
210 |
in
|
|
211 |
matchList sub rest
|
|
212 |
end
|
|
213 |
| matchList sub ((Term.Fn (f1,args1), Term.Fn (f2,args2)) :: rest) =
|
|
214 |
if Name.equal f1 f2 andalso length args1 = length args2 then
|
|
215 |
matchList sub (zip args1 args2 @ rest)
|
|
216 |
else raise Error "Subst.match: different structure"
|
|
217 |
| matchList _ _ = raise Error "Subst.match: functions can't match vars";
|
|
218 |
in
|
|
219 |
fun match sub tm1 tm2 = matchList sub [(tm1,tm2)];
|
|
220 |
end;
|
|
221 |
|
|
222 |
(* ------------------------------------------------------------------------- *)
|
|
223 |
(* Unification for first order logic terms. *)
|
|
224 |
(* ------------------------------------------------------------------------- *)
|
|
225 |
|
|
226 |
local
|
|
227 |
fun solve sub [] = sub
|
|
228 |
| solve sub ((tm1_tm2 as (tm1,tm2)) :: rest) =
|
|
229 |
if Portable.pointerEqual tm1_tm2 then solve sub rest
|
|
230 |
else solve' sub (subst sub tm1) (subst sub tm2) rest
|
|
231 |
|
|
232 |
and solve' sub (Term.Var v) tm rest =
|
|
233 |
if Term.equalVar v tm then solve sub rest
|
|
234 |
else if Term.freeIn v tm then raise Error "Subst.unify: occurs check"
|
|
235 |
else
|
|
236 |
(case peek sub v of
|
|
237 |
NONE => solve (compose sub (singleton (v,tm))) rest
|
|
238 |
| SOME tm' => solve' sub tm' tm rest)
|
|
239 |
| solve' sub tm1 (tm2 as Term.Var _) rest = solve' sub tm2 tm1 rest
|
|
240 |
| solve' sub (Term.Fn (f1,args1)) (Term.Fn (f2,args2)) rest =
|
|
241 |
if Name.equal f1 f2 andalso length args1 = length args2 then
|
|
242 |
solve sub (zip args1 args2 @ rest)
|
|
243 |
else
|
|
244 |
raise Error "Subst.unify: different structure";
|
|
245 |
in
|
|
246 |
fun unify sub tm1 tm2 = solve sub [(tm1,tm2)];
|
|
247 |
end;
|
|
248 |
|
|
249 |
end
|