1(* ===================================================================== *)
2(* FILE          : Net.sml                                               *)
3(* DESCRIPTION   : Implementation of term nets, from the group at ICL.   *)
4(*                 Thanks! A term net is a database, keyed by terms.     *)
5(*                 Term nets were initially implemented by Larry Paulson *)
6(*                 for Cambridge LCF.                                    *)
7(*                                                                       *)
8(* AUTHOR        : Somebody in the ICL group.                            *)
9(* DATE          : August 26, 1991                                       *)
10(* MODIFIED      : Sept 5, 1992, to use deBruijn representation          *)
11(* Modified      : September 23, 1997, Ken Larsen                        *)
12(* Reimplemented : July 17, 1999, Konrad Slind                           *)
13(* ===================================================================== *)
14
15structure Net :> Net =
16struct
17
18open Lib Feedback
19
20type term = Term.term
21
22val ERR = mk_HOL_ERR "Net";
23
24(*---------------------------------------------------------------------------*
25 *   Tags corresponding to the underlying term constructors.                 *
26 *---------------------------------------------------------------------------*)
27
28datatype label
29    = V
30    | Cmb
31    | Lam
32    | Cnst of string * string ;  (* name * segment *)
33
34(*---------------------------------------------------------------------------*
35 *    Term nets.                                                             *
36 *---------------------------------------------------------------------------*)
37
38datatype 'a net
39    = LEAF of (term * 'a) list
40    | NODE of (label * 'a net) list;
41
42
43val empty = NODE [];
44
45fun is_empty (NODE[]) = true
46  | is_empty    _     = false;
47
48(*---------------------------------------------------------------------------*
49 * Determining the top constructor of a term.                                *
50 *---------------------------------------------------------------------------*)
51
52local open Term
53in
54fun label_of tm =
55   if is_abs tm then Lam else
56   if is_var tm then V else
57   if is_comb tm then Cmb
58   else let val {Name,Thy,...} = dest_thy_const tm
59        in Cnst (Name,Thy)
60        end
61end
62
63fun net_assoc label =
64 let fun get (LEAF _) = raise ERR "net_assoc" "LEAF: no children"
65       | get (NODE subnets) =
66            case assoc1 label subnets
67             of NONE => empty
68              | SOME (_,net) => net
69 in get
70 end;
71
72
73local
74  fun mtch tm (NODE []) = []
75    | mtch tm net =
76       let val label = label_of tm
77           val Vnet = net_assoc V net
78           val nets =
79            case label
80             of V => []
81              | Cnst _ => [net_assoc label net]
82              | Lam    => mtch (Term.body tm) (net_assoc Lam net)
83              | Cmb    => let val (Rator,Rand) = Term.dest_comb tm
84                          in itlist(append o mtch Rand)
85                                   (mtch Rator (net_assoc Cmb net)) []
86                           end
87       in itlist (fn NODE [] => I | net => cons net) nets [Vnet]
88       end
89in
90fun match tm net =
91  if is_empty net then []
92  else
93    itlist (fn LEAF L => append (map #2 L) | _ => fn y => y)
94           (mtch tm net) []
95end;
96
97(*---------------------------------------------------------------------------
98        Finding the elements mapped by a term in a term net.
99 ---------------------------------------------------------------------------*)
100
101fun index x net = let
102  fun appl  _   _  (LEAF L) = SOME L
103    | appl defd tm (NODE L) =
104      let val label = label_of tm
105      in case assoc1 label L
106          of NONE => NONE
107           | SOME (_,net) =>
108              case label
109               of Lam => appl defd (Term.body tm) net
110                | Cmb => let val (Rator,Rand) = Term.dest_comb tm
111                         in appl (Rand::defd) Rator net end
112                |  _  => let fun exec_defd [] (NODE _) = raise ERR "appl"
113                                  "NODE: should be at a LEAF instead"
114                               | exec_defd [] (LEAF L) = SOME L
115                               | exec_defd (h::rst) net =  appl rst h net
116                         in
117                           exec_defd defd net
118                         end
119      end
120in
121  case appl [] x net
122   of SOME L => map #2 L
123    | NONE   => []
124end;
125
126(*---------------------------------------------------------------------------*
127 *        Adding to a term net.                                              *
128 *---------------------------------------------------------------------------*)
129
130fun overwrite (p as (a,_)) =
131  let fun over [] = [p]
132        | over ((q as (x,_))::rst) =
133            if (a=x) then p::rst else q::over rst
134  in over
135  end;
136
137fun insert (p as (tm,_)) N =
138let fun enter _ _  (LEAF _) = raise ERR "insert" "LEAF: cannot insert"
139   | enter defd tm (NODE subnets) =
140      let val label = label_of tm
141          val child =
142             case assoc1 label subnets of NONE => empty | SOME (_,net) => net
143          val new_child =
144            case label
145             of Cmb => let val (Rator,Rand) = Term.dest_comb tm
146                       in enter (Rand::defd) Rator child end
147              | Lam => enter defd (Term.body tm) child
148              | _   => let fun exec [] (LEAF L)  = LEAF(p::L)
149                             | exec [] (NODE _)  = LEAF[p]
150                             | exec (h::rst) net = enter rst h net
151                       in
152                          exec defd child
153                       end
154      in
155         NODE (overwrite (label,new_child) subnets)
156      end
157in enter [] tm N
158end;
159
160
161(*---------------------------------------------------------------------------
162     Removing an element from a term net. It is not an error if the
163     element is not there.
164 ---------------------------------------------------------------------------*)
165
166fun split_assoc P =
167 let fun split front [] = raise ERR "split_assoc" "not found"
168       | split front (h::t) =
169          if P h then (rev front,h,t) else split (h::front) t
170 in
171    split []
172 end;
173
174
175fun delete (tm,P) N =
176let fun del [] = []
177      | del ((p as (x,q))::rst) =
178          if Term.aconv x tm andalso P q then del rst else p::del rst
179 fun remv  _   _ (LEAF L) = LEAF(del L)
180   | remv defd tm (NODE L) =
181     let val label = label_of tm
182         fun pred (x,_) = (x=label)
183         val (left,(_,childnet),right) = split_assoc pred L
184         val childnet' =
185           case label
186            of Lam => remv defd (Term.body tm) childnet
187             | Cmb => let val (Rator,Rand) = Term.dest_comb tm
188                      in remv (Rand::defd) Rator childnet end
189             |  _  => let fun exec_defd [] (NODE _) = raise ERR "remv"
190                                "NODE: should be at a LEAF instead"
191                            | exec_defd [] (LEAF L) = LEAF(del L)
192                            | exec_defd (h::rst) net =  remv rst h net
193                      in
194                        exec_defd defd childnet
195                      end
196         val childnetl =
197           case childnet' of NODE [] => [] | LEAF [] => [] | y => [(label,y)]
198     in
199       NODE (List.concat [left,childnetl,right])
200     end
201in
202  remv [] tm N handle Feedback.HOL_ERR _ => N
203end;
204
205fun filter P =
206 let fun filt (LEAF L) = LEAF(List.filter (fn (x,y) => P y) L)
207       | filt (NODE L) =
208          NODE (itlist  (fn (l,n) => fn list =>
209                 case filt n
210                  of LEAF [] => list
211                   | NODE [] => list
212                   |   n'    => (l,n')::list) L [])
213 in
214    filt
215 end;
216
217fun listItems0 (LEAF L) = L
218  | listItems0 (NODE L) = rev_itlist (append o listItems0 o #2) L [];
219
220fun union net1 net2 = rev_itlist insert (listItems0 net1) net2;
221
222fun listItems net = map #2 (listItems0 net);
223
224fun map f (LEAF L) = LEAF (List.map (fn (x,y) => (x, f y)) L)
225  | map f (NODE L) = NODE (List.map (fn (l,net) => (l,map f net)) L);
226
227fun itnet f (LEAF L) b = itlist f (List.map #2 L) b
228  | itnet f (NODE L) b = itlist (itnet f) (List.map #2 L) b;
229
230fun size net = itnet (fn x => fn y => y+1) net 0;
231
232
233(*---------------------------------------------------------------------------
234                Compatibility mode.
235 ---------------------------------------------------------------------------*)
236
237fun get_tip_list (LEAF L) = L
238  | get_tip_list (NODE _) = [];
239
240fun get_edge label =
241   let fun get (NODE edges) =
242              (case Lib.assoc1 label edges
243                 of SOME (_,net) => net
244                  | NONE => empty)
245         | get (LEAF _) = raise ERR "get_edge" "tips have no edges"
246   in get
247   end;
248
249fun net_update elem =
250let fun update _ _ (LEAF _) = raise ERR "net_update" "cannot update a tip"
251      | update defd tm (net as (NODE edges)) =
252           let fun exec_defd [] net = LEAF (elem::get_tip_list net)
253                 | exec_defd (h::rst) net = update rst h net
254               val label = label_of tm
255               val child = get_edge label net
256               val new_child =
257                 case label
258                   of Cmb => let val (Rator,Rand) = Term.dest_comb tm
259                             in update (Rator::defd) Rand child
260                             end
261                    | Lam => update defd (Term.body tm) child
262                    | _   => exec_defd defd child
263           in NODE (overwrite (label,new_child) edges)
264           end
265in  update
266end;
267
268fun enter (tm,elem) net = net_update (tm,elem) [] tm net;
269
270fun follow tm net =
271 let val nets =
272       case (label_of tm)
273       of (label as Cnst _) => [get_edge label net]
274        | V   => []
275        | Lam => follow (Term.body tm) (get_edge Lam net)
276        | Cmb => let val (Rator,Rand) = Term.dest_comb tm
277                 in Lib.itlist(fn i => fn A => (follow Rator i @ A))
278                              (follow Rand (get_edge Cmb net)) []
279                 end
280 in List.filter (not o is_empty) (get_edge V net::nets)
281 end;
282
283fun lookup tm net =
284 if is_empty net then []
285 else
286   itlist (fn (LEAF L) => (fn A => (List.map #2 L @ A)) | (NODE _) => I)
287          (follow tm net)  [];
288
289end (* Net *)
290