1(* ========================================================================= *) 2(* SUBSTITUTIONS ON FIRST-ORDER TERMS AND FORMULAS *) 3(* Copyright (c) 2002-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6structure mlibSubst :> mlibSubst = 7struct 8 9open mlibUseful mlibTerm; 10 11infix @> ::> 12 13structure M = Binarymap; local open Binarymap in end; 14 15(* ------------------------------------------------------------------------- *) 16(* Helper functions. *) 17(* ------------------------------------------------------------------------- *) 18 19fun Mpurge (d, k) = fst (M.remove (d, k)) handle NotFound => d; 20 21(* ------------------------------------------------------------------------- *) 22(* The underlying representation. *) 23(* ------------------------------------------------------------------------- *) 24 25datatype subst = mlibSubst of (string, term) M.dict; 26 27(* ------------------------------------------------------------------------- *) 28(* Operations. *) 29(* ------------------------------------------------------------------------- *) 30 31val |<>| = mlibSubst (M.mkDict String.compare); 32 33fun (a |-> b) ::> (mlibSubst d) = mlibSubst (M.insert (d, a, b)); 34 35fun (mlibSubst sub1) @> (mlibSubst sub2) = 36 mlibSubst (M.foldl (fn (a, b, d) => M.insert (d, a, b)) sub2 sub1); 37 38fun null (mlibSubst s) = M.numItems s = 0; 39 40fun find_redex r (mlibSubst d) = M.peek (d, r); 41 42fun purge v (mlibSubst d) = mlibSubst (Mpurge (d, v)); 43 44local 45 exception Unchanged; 46 47 fun always f x = f x handle Unchanged => x; 48 49 fun pair_unchanged f (x, y) = 50 let 51 val (c, x) = (true, f x) handle Unchanged => (false, x) 52 val (c, y) = (true, f y) handle Unchanged => (c, y) 53 in 54 if c then (x, y) else raise Unchanged 55 end; 56 57 fun list_unchanged f = 58 let 59 fun g (x, (b, l)) = (true, f x :: l) handle Unchanged => (b, x :: l) 60 fun h (true, l) = rev l | h (false, _) = raise Unchanged 61 in 62 h o foldl g (false, []) 63 end; 64 65 fun find_unchanged v r = 66 case find_redex v r of SOME t => t | NONE => raise Unchanged; 67 68 fun tm_subst r = 69 let 70 fun f (Var v) = find_unchanged v r 71 | f (Fn (n, a)) = Fn (n, list_unchanged f a) 72 in 73 f 74 end; 75 76 fun fm_subst r = 77 let 78 fun f False = raise Unchanged 79 | f True = raise Unchanged 80 | f (Atom tm ) = Atom (tm_subst r tm) 81 | f (Not p ) = Not (f p) 82 | f (And pq ) = And (pair_unchanged f pq) 83 | f (Or pq ) = Or (pair_unchanged f pq) 84 | f (Imp pq ) = Imp (pair_unchanged f pq) 85 | f (Iff pq ) = Iff (pair_unchanged f pq) 86 | f (Forall vp) = fm_substq r Forall vp 87 | f (Exists vp) = fm_substq r Exists vp 88 in 89 if null r then I else always f 90 end 91 and fm_substq r Q (v, p) = 92 let val v' = variant v (FV (fm_subst (purge v r) p)) 93 in Q (v', fm_subst ((v |-> Var v') ::> r) p) 94 end; 95in 96 fun term_subst env tm = if null env then tm else always (tm_subst env) tm; 97 fun formula_subst env fm = fm_subst env fm; 98end; 99 100fun norm (sub as mlibSubst dict) = 101 let 102 fun check (a, b, (c, d)) = 103 if Var a = b then (true, fst (M.remove (d, a))) else (c, d) 104 val (removed, dict') = M.foldl check (false, dict) dict 105 in 106 if removed then mlibSubst dict' else sub 107 end; 108 109fun to_maplets (mlibSubst s) = map (op|->) (M.listItems s); 110 111fun from_maplets ms = foldl (op ::>) |<>| (rev ms); 112 113fun restrict vs = 114 from_maplets o List.filter (fn (a |-> _) => mem a vs) o to_maplets; 115 116(* Note: this just doesn't work with cyclic substitutions! *) 117fun refine (mlibSubst sub1) sub2 = 118 let 119 fun f ((a, b), s) = 120 let val b' = term_subst sub2 b 121 in if Var a = b' then s else (a |-> b') ::> s 122 end 123 in 124 foldl f sub2 (M.listItems sub1) 125 end; 126 127local 128 exception QF 129 fun rs (v, Var w, l) = if mem w l then raise QF else w :: l 130 | rs (_, Fn _, _) = raise QF 131in 132 fun is_renaming (mlibSubst sub) = (M.foldl rs [] sub; true) handle QF => false; 133end; 134 135fun foldl f b (mlibSubst sub) = M.foldl (fn (s, t, a) => f (s |-> t) a) b sub; 136 137fun foldr f b (mlibSubst sub) = M.foldr (fn (s, t, a) => f (s |-> t) a) b sub; 138 139val pp_subst = 140 pp_map 141 to_maplets 142 (fn [] => pp_string"|<>|" | l => pp_list (pp_maplet pp_string pp_term) l) 143 144end 145