1(* ========================================================================= *)
2(* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6structure Subst :> Subst =
7struct
8
9open Useful;
10
11(* ------------------------------------------------------------------------- *)
12(* A type of first order logic substitutions.                                *)
13(* ------------------------------------------------------------------------- *)
14
15datatype subst = Subst of Term.term NameMap.map;
16
17(* ------------------------------------------------------------------------- *)
18(* Basic operations.                                                         *)
19(* ------------------------------------------------------------------------- *)
20
21val empty = Subst (NameMap.new ());
22
23fun null (Subst m) = NameMap.null m;
24
25fun size (Subst m) = NameMap.size m;
26
27fun peek (Subst m) v = NameMap.peek m v;
28
29fun insert (Subst m) v_tm = Subst (NameMap.insert m v_tm);
30
31fun singleton v_tm = insert empty v_tm;
32
33fun toList (Subst m) = NameMap.toList m;
34
35fun fromList l = Subst (NameMap.fromList l);
36
37fun foldl f b (Subst m) = NameMap.foldl f b m;
38
39fun foldr f b (Subst m) = NameMap.foldr f b m;
40
41fun pp sub =
42    Print.ppBracket "<[" "]>"
43      (Print.ppOpList "," (Print.ppOp2 " |->" Name.pp Term.pp))
44      (toList sub);
45
46val toString = Print.toString pp;
47
48(* ------------------------------------------------------------------------- *)
49(* Normalizing removes identity substitutions.                               *)
50(* ------------------------------------------------------------------------- *)
51
52local
53  fun isNotId (v,tm) = not (Term.equalVar v tm);
54in
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;
61end;
62
63(* ------------------------------------------------------------------------- *)
64(* Applying a substitution to a first order logic term.                      *)
65(* ------------------------------------------------------------------------- *)
66
67fun 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
88fun 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
97fun 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
112fun 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
123local
124  fun compatible ((_,tm1),(_,tm2)) =
125      if Term.equal tm1 tm2 then SOME tm1
126      else raise Error "Subst.union: incompatible";
127in
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);
132end;
133
134(* ------------------------------------------------------------------------- *)
135(* Substitutions can be inverted iff they are renaming substitutions.        *)
136(* ------------------------------------------------------------------------- *)
137
138local
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";
143in
144  fun invert (Subst m) = Subst (NameMap.foldl inv (NameMap.new ()) m);
145end;
146
147val isRenaming = can invert;
148
149(* ------------------------------------------------------------------------- *)
150(* Creating a substitution to freshen variables.                             *)
151(* ------------------------------------------------------------------------- *)
152
153val 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
164val redexes =
165    let
166      fun add (v,_,s) = NameSet.add s v
167    in
168      foldl add NameSet.empty
169    end;
170
171val residueFreeVars =
172    let
173      fun add (_,t,s) = NameSet.union s (Term.freeVars t)
174    in
175      foldl add NameSet.empty
176    end;
177
178val 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
189val 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
200local
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";
218in
219  fun match sub tm1 tm2 = matchList sub [(tm1,tm2)];
220end;
221
222(* ------------------------------------------------------------------------- *)
223(* Unification for first order logic terms.                                  *)
224(* ------------------------------------------------------------------------- *)
225
226local
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";
245in
246  fun unify sub tm1 tm2 = solve sub [(tm1,tm2)];
247end;
248
249end
250