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