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