1 (* ========================================================================= *) |
|
2 (* FIRST ORDER LOGIC SUBSTITUTIONS *) |
|
3 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) |
|
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 local |
|
34 fun compatible (tm1,tm2) = |
|
35 if tm1 = tm2 then SOME tm1 else raise Error "Subst.union: incompatible"; |
|
36 in |
|
37 fun union (s1 as Subst m1) (s2 as Subst m2) = |
|
38 if NameMap.null m1 then s2 |
|
39 else if NameMap.null m2 then s1 |
|
40 else Subst (NameMap.union compatible m1 m2); |
|
41 end; |
|
42 |
|
43 fun toList (Subst m) = NameMap.toList m; |
|
44 |
|
45 fun fromList l = Subst (NameMap.fromList l); |
|
46 |
|
47 fun foldl f b (Subst m) = NameMap.foldl f b m; |
|
48 |
|
49 fun foldr f b (Subst m) = NameMap.foldr f b m; |
|
50 |
|
51 fun pp ppstrm sub = |
|
52 Parser.ppBracket "<[" "]>" |
|
53 (Parser.ppSequence "," (Parser.ppBinop " |->" Parser.ppString Term.pp)) |
|
54 ppstrm (toList sub); |
|
55 |
|
56 val toString = Parser.toString pp; |
|
57 |
|
58 (* ------------------------------------------------------------------------- *) |
|
59 (* Normalizing removes identity substitutions. *) |
|
60 (* ------------------------------------------------------------------------- *) |
|
61 |
|
62 local |
|
63 fun isNotId (v,tm) = not (Term.equalVar v tm); |
|
64 in |
|
65 fun normalize (sub as Subst m) = |
|
66 let |
|
67 val m' = NameMap.filter isNotId m |
|
68 in |
|
69 if NameMap.size m = NameMap.size m' then sub else Subst m' |
|
70 end; |
|
71 end; |
|
72 |
|
73 (* ------------------------------------------------------------------------- *) |
|
74 (* Applying a substitution to a first order logic term. *) |
|
75 (* ------------------------------------------------------------------------- *) |
|
76 |
|
77 fun subst sub = |
|
78 let |
|
79 fun tmSub (tm as Term.Var v) = |
|
80 (case peek sub v of |
|
81 SOME tm' => if Sharing.pointerEqual (tm,tm') then tm else tm' |
|
82 | NONE => tm) |
|
83 | tmSub (tm as Term.Fn (f,args)) = |
|
84 let |
|
85 val args' = Sharing.map tmSub args |
|
86 in |
|
87 if Sharing.pointerEqual (args,args') then tm |
|
88 else Term.Fn (f,args') |
|
89 end |
|
90 in |
|
91 fn tm => if null sub then tm else tmSub tm |
|
92 end; |
|
93 |
|
94 (* ------------------------------------------------------------------------- *) |
|
95 (* Restricting a substitution to a given set of variables. *) |
|
96 (* ------------------------------------------------------------------------- *) |
|
97 |
|
98 fun restrict (sub as Subst m) varSet = |
|
99 let |
|
100 fun isRestrictedVar (v,_) = NameSet.member v varSet |
|
101 |
|
102 val m' = NameMap.filter isRestrictedVar m |
|
103 in |
|
104 if NameMap.size m = NameMap.size m' then sub else Subst m' |
|
105 end; |
|
106 |
|
107 fun remove (sub as Subst m) varSet = |
|
108 let |
|
109 fun isRestrictedVar (v,_) = not (NameSet.member v varSet) |
|
110 |
|
111 val m' = NameMap.filter isRestrictedVar m |
|
112 in |
|
113 if NameMap.size m = NameMap.size m' then sub else Subst m' |
|
114 end; |
|
115 |
|
116 (* ------------------------------------------------------------------------- *) |
|
117 (* Composing two substitutions so that the following identity holds: *) |
|
118 (* *) |
|
119 (* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *) |
|
120 (* ------------------------------------------------------------------------- *) |
|
121 |
|
122 fun compose (sub1 as Subst m1) sub2 = |
|
123 let |
|
124 fun f (v,tm,s) = insert s (v, subst sub2 tm) |
|
125 in |
|
126 if null sub2 then sub1 else NameMap.foldl f sub2 m1 |
|
127 end; |
|
128 |
|
129 (* ------------------------------------------------------------------------- *) |
|
130 (* Substitutions can be inverted iff they are renaming substitutions. *) |
|
131 (* ------------------------------------------------------------------------- *) |
|
132 |
|
133 local |
|
134 fun inv (v, Term.Var w, s) = |
|
135 if NameMap.inDomain w s then raise Error "Subst.invert: non-injective" |
|
136 else NameMap.insert s (w, Term.Var v) |
|
137 | inv (_, Term.Fn _, _) = raise Error "Subst.invert: non-variable"; |
|
138 in |
|
139 fun invert (Subst m) = Subst (NameMap.foldl inv (NameMap.new ()) m); |
|
140 end; |
|
141 |
|
142 val isRenaming = can invert; |
|
143 |
|
144 (* ------------------------------------------------------------------------- *) |
|
145 (* Creating a substitution to freshen variables. *) |
|
146 (* ------------------------------------------------------------------------- *) |
|
147 |
|
148 val freshVars = |
|
149 let |
|
150 fun add (v,m) = insert m (v, Term.newVar ()) |
|
151 in |
|
152 NameSet.foldl add empty |
|
153 end; |
|
154 |
|
155 (* ------------------------------------------------------------------------- *) |
|
156 (* Matching for first order logic terms. *) |
|
157 (* ------------------------------------------------------------------------- *) |
|
158 |
|
159 local |
|
160 fun matchList sub [] = sub |
|
161 | matchList sub ((Term.Var v, tm) :: rest) = |
|
162 let |
|
163 val sub = |
|
164 case peek sub v of |
|
165 NONE => insert sub (v,tm) |
|
166 | SOME tm' => |
|
167 if tm = tm' then sub |
|
168 else raise Error "Subst.match: incompatible matches" |
|
169 in |
|
170 matchList sub rest |
|
171 end |
|
172 | matchList sub ((Term.Fn (f1,args1), Term.Fn (f2,args2)) :: rest) = |
|
173 if f1 = f2 andalso length args1 = length args2 then |
|
174 matchList sub (zip args1 args2 @ rest) |
|
175 else raise Error "Subst.match: different structure" |
|
176 | matchList _ _ = raise Error "Subst.match: functions can't match vars"; |
|
177 in |
|
178 fun match sub tm1 tm2 = matchList sub [(tm1,tm2)]; |
|
179 end; |
|
180 |
|
181 (* ------------------------------------------------------------------------- *) |
|
182 (* Unification for first order logic terms. *) |
|
183 (* ------------------------------------------------------------------------- *) |
|
184 |
|
185 local |
|
186 fun solve sub [] = sub |
|
187 | solve sub ((tm1_tm2 as (tm1,tm2)) :: rest) = |
|
188 if Portable.pointerEqual tm1_tm2 then solve sub rest |
|
189 else solve' sub (subst sub tm1) (subst sub tm2) rest |
|
190 |
|
191 and solve' sub (Term.Var v) tm rest = |
|
192 if Term.equalVar v tm then solve sub rest |
|
193 else if Term.freeIn v tm then raise Error "Subst.unify: occurs check" |
|
194 else |
|
195 (case peek sub v of |
|
196 NONE => solve (compose sub (singleton (v,tm))) rest |
|
197 | SOME tm' => solve' sub tm' tm rest) |
|
198 | solve' sub tm1 (tm2 as Term.Var _) rest = solve' sub tm2 tm1 rest |
|
199 | solve' sub (Term.Fn (f1,args1)) (Term.Fn (f2,args2)) rest = |
|
200 if f1 = f2 andalso length args1 = length args2 then |
|
201 solve sub (zip args1 args2 @ rest) |
|
202 else |
|
203 raise Error "Subst.unify: different structure"; |
|
204 in |
|
205 fun unify sub tm1 tm2 = solve sub [(tm1,tm2)]; |
|
206 end; |
|
207 |
|
208 end |
|