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 KernelTypes
19
20val ERR = mk_HOL_ERR "Net";
21
22val break_abs = Term.break_abs;
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. The following is a bit         *
50 * convoluted, since doing a dest_abs requires a full traversal to replace   *
51 * the bound variable with a free one. Therefore we make a separate check    *
52 * for abstractions.                                                         *
53 *---------------------------------------------------------------------------*)
54
55local open Term
56in
57fun label_of tm =
58   if is_abs tm then Lam else
59   if is_bvar tm orelse is_var tm then V else
60   if is_comb tm then Cmb
61   else let val {Name,Thy,...} = dest_thy_const tm
62        in Cnst (Name,Thy)
63        end
64end
65
66fun net_assoc label =
67 let fun get (LEAF _) = raise ERR "net_assoc" "LEAF: no children"
68       | get (NODE subnets) =
69            case assoc1 label subnets
70             of NONE => empty
71              | SOME (_,net) => net
72 in get
73 end;
74
75
76local
77  fun mtch tm (NODE []) = []
78    | mtch tm net =
79       let val label = label_of tm
80           val Vnet = net_assoc V net
81           val nets =
82            case label
83             of V => []
84              | Cnst _ => [net_assoc label net]
85              | Lam    => mtch (break_abs tm) (net_assoc Lam net)
86              | Cmb    => let val (Rator,Rand) = Term.dest_comb tm
87                          in itlist(append o mtch Rand)
88                                   (mtch Rator (net_assoc Cmb net)) []
89                           end
90       in itlist (fn NODE [] => I | net => cons net) nets [Vnet]
91       end
92in
93fun match tm net =
94  if is_empty net then []
95  else
96    itlist (fn LEAF L => append (map #2 L) | _ => fn y => y)
97           (mtch tm net) []
98end;
99
100(*---------------------------------------------------------------------------
101        Finding the elements mapped by a term in a term net.
102 ---------------------------------------------------------------------------*)
103
104fun index x net = let
105  fun appl  _   _  (LEAF L) = SOME L
106    | appl defd tm (NODE L) =
107      let val label = label_of tm
108      in case assoc1 label L
109          of NONE => NONE
110           | SOME (_,net) =>
111              case label
112               of Lam => appl defd (break_abs tm) net
113                | Cmb => let val (Rator,Rand) = Term.dest_comb tm
114                         in appl (Rand::defd) Rator net end
115                |  _  => let fun exec_defd [] (NODE _) = raise ERR "appl"
116                                  "NODE: should be at a LEAF instead"
117                               | exec_defd [] (LEAF L) = SOME L
118                               | exec_defd (h::rst) net =  appl rst h net
119                         in
120                           exec_defd defd net
121                         end
122      end
123in
124  case appl [] x net
125   of SOME L => map #2 L
126    | NONE   => []
127end;
128
129(*---------------------------------------------------------------------------*
130 *        Adding to a term net.                                              *
131 *---------------------------------------------------------------------------*)
132
133fun overwrite (p as (a,_)) =
134  let fun over [] = [p]
135        | over ((q as (x,_))::rst) =
136            if (a=x) then p::rst else q::over rst
137  in over
138  end;
139
140fun insert (p as (tm,_)) N =
141let fun enter _ _  (LEAF _) = raise ERR "insert" "LEAF: cannot insert"
142   | enter defd tm (NODE subnets) =
143      let val label = label_of tm
144          val child =
145             case assoc1 label subnets of NONE => empty | SOME (_,net) => net
146          val new_child =
147            case label
148             of Cmb => let val (Rator,Rand) = Term.dest_comb tm
149                       in enter (Rand::defd) Rator child end
150              | Lam => enter defd (break_abs tm) child
151              | _   => let fun exec [] (LEAF L)  = LEAF(p::L)
152                             | exec [] (NODE _)  = LEAF[p]
153                             | exec (h::rst) net = enter rst h net
154                       in
155                          exec defd child
156                       end
157      in
158         NODE (overwrite (label,new_child) subnets)
159      end
160in enter [] tm N
161end;
162
163
164(*---------------------------------------------------------------------------
165     Removing an element from a term net. It is not an error if the
166     element is not there.
167 ---------------------------------------------------------------------------*)
168
169fun split_assoc P =
170 let fun split front [] = raise ERR "split_assoc" "not found"
171       | split front (h::t) =
172          if P h then (rev front,h,t) else split (h::front) t
173 in
174    split []
175 end;
176
177
178fun delete (tm,P) N =
179let fun del [] = []
180      | del ((p as (x,q))::rst) =
181          if Term.aconv x tm andalso P q then del rst else p::del rst
182 fun remv  _   _ (LEAF L) = LEAF(del L)
183   | remv defd tm (NODE L) =
184     let val label = label_of tm
185         fun pred (x,_) = (x=label)
186         val (left,(_,childnet),right) = split_assoc pred L
187         val childnet' =
188           case label
189            of Lam => remv defd (break_abs tm) childnet
190             | Cmb => let val (Rator,Rand) = Term.dest_comb tm
191                      in remv (Rand::defd) Rator childnet end
192             |  _  => let fun exec_defd [] (NODE _) = raise ERR "remv"
193                                "NODE: should be at a LEAF instead"
194                            | exec_defd [] (LEAF L) = LEAF(del L)
195                            | exec_defd (h::rst) net =  remv rst h net
196                      in
197                        exec_defd defd childnet
198                      end
199         val childnetl =
200           case childnet' of NODE [] => [] | LEAF [] => [] | y => [(label,y)]
201     in
202       NODE (List.concat [left,childnetl,right])
203     end
204in
205  remv [] tm N handle Feedback.HOL_ERR _ => N
206end;
207
208fun filter P =
209 let fun filt (LEAF L) = LEAF(List.filter (fn (x,y) => P y) L)
210       | filt (NODE L) =
211          NODE (itlist  (fn (l,n) => fn list =>
212                 case filt n
213                  of LEAF [] => list
214                   | NODE [] => list
215                   |   n'    => (l,n')::list) L [])
216 in
217    filt
218 end;
219
220fun listItems0 (LEAF L) = L
221  | listItems0 (NODE L) = rev_itlist (append o listItems0 o #2) L [];
222
223fun union net1 net2 = rev_itlist insert (listItems0 net1) net2;
224
225fun listItems net = map #2 (listItems0 net);
226
227fun map f (LEAF L) = LEAF (List.map (fn (x,y) => (x, f y)) L)
228  | map f (NODE L) = NODE (List.map (fn (l,net) => (l,map f net)) L);
229
230fun itnet f (LEAF L) b = itlist f (List.map #2 L) b
231  | itnet f (NODE L) b = itlist (itnet f) (List.map #2 L) b;
232
233fun size net = itnet (fn x => fn y => y+1) net 0;
234
235
236(*---------------------------------------------------------------------------
237                Compatibility mode.
238 ---------------------------------------------------------------------------*)
239
240fun get_tip_list (LEAF L) = L
241  | get_tip_list (NODE _) = [];
242
243fun get_edge label =
244   let fun get (NODE edges) =
245              (case Lib.assoc1 label edges
246                 of SOME (_,net) => net
247                  | NONE => empty)
248         | get (LEAF _) = raise ERR "get_edge" "tips have no edges"
249   in get
250   end;
251
252fun net_update elem =
253let fun update _ _ (LEAF _) = raise ERR "net_update" "cannot update a tip"
254      | update defd tm (net as (NODE edges)) =
255           let fun exec_defd [] net = LEAF (elem::get_tip_list net)
256                 | exec_defd (h::rst) net = update rst h net
257               val label = label_of tm
258               val child = get_edge label net
259               val new_child =
260                 case label
261                   of Cmb => let val (Rator,Rand) = Term.dest_comb tm
262                             in update (Rator::defd) Rand child
263                             end
264                    | Lam => update defd (break_abs tm) child
265                    | _   => exec_defd defd child
266           in NODE (overwrite (label,new_child) edges)
267           end
268in  update
269end;
270
271fun enter (tm,elem) net = net_update (tm,elem) [] tm net;
272
273fun follow tm net =
274 let val nets =
275       case (label_of tm)
276       of (label as Cnst _) => [get_edge label net]
277        | V   => []
278        | Lam => follow (break_abs tm) (get_edge Lam net)
279        | Cmb => let val (Rator,Rand) = Term.dest_comb tm
280                 in Lib.itlist(fn i => fn A => (follow Rator i @ A))
281                              (follow Rand (get_edge Cmb net)) []
282                 end
283 in List.filter (not o is_empty) (get_edge V net::nets)
284 end;
285
286fun lookup tm net =
287 if is_empty net then []
288 else
289   itlist (fn (LEAF L) => (fn A => (List.map #2 L @ A)) | (NODE _) => I)
290          (follow tm net)  [];
291
292end (* Net *)
293