1structure LVTermNet :> LVTermNet =
2struct
3
4open HolKernel
5
6datatype label = V of int
7               | C of {Name : string, Thy : string} * int
8               | Lam of int
9               | LV of string * int
10type key = term list * term
11
12val tlt_compare = pair_compare (list_compare Term.compare, Term.compare)
13
14fun labcmp (p as (l1, l2)) =
15    case p of
16      (V n1, V n2) => Int.compare(n1, n2)
17    | (V _, _) => LESS
18    | (_, V _) => GREATER
19    | (C ({Name=nm1,Thy=th1}, n1), C ({Name=nm2,Thy=th2}, n2)) =>
20         pair_compare (Int.compare,
21                       pair_compare (String.compare, String.compare))
22                      ((n1, (th1, nm1)), (n2, (th2, nm2)))
23    | (C _, _) => LESS
24    | (_, C _) => GREATER
25    | (Lam n1, Lam n2) => Int.compare (n1, n2)
26    | (Lam _, _) => LESS
27    | (_, Lam _) => GREATER
28    | (LV p1, LV p2) => pair_compare (String.compare, Int.compare) (p1, p2)
29
30datatype 'a N = LF of (key,'a list) Binarymap.dict
31              | ND of (label,'a N) Binarymap.dict
32              | EMPTY
33(* redundant EMPTY constructor is used to get around value polymorphism problem
34   when creating a single value for empty below *)
35
36type 'a lvtermnet = 'a N * int
37
38val empty = (EMPTY, 0)
39
40fun mkempty () = ND (Binarymap.mkDict labcmp)
41
42fun ndest_term (fvs, tm) = let
43  val (f, args) = strip_comb tm
44  val args' = map (fn t => (fvs, t)) args
45in
46  case dest_term f of
47    VAR(s, ty) => if mem f fvs then (LV (s, length args), args')
48                  else (V (length args), args')
49  | LAMB(bv, bod) => (Lam (length args), (subtract fvs [bv], bod) :: args')
50  | CONST{Name,Thy,Ty} => (C ({Name=Name,Thy=Thy}, length args), args')
51  | COMB _ => raise Fail "impossible"
52end
53
54fun cons_insert (bmap, k, i) =
55    case Binarymap.peek(bmap,k) of
56      NONE => Binarymap.insert(bmap,k,[i])
57    | SOME items => Binarymap.insert(bmap,k,i::items)
58
59fun insert ((net,sz), k, item) = let
60  fun newnode labs =
61      case labs of
62        [] => LF (Binarymap.mkDict tlt_compare)
63      | _ => mkempty()
64  fun trav (net, tms) =
65      case (net, tms) of
66        (LF d, []) => LF (cons_insert(d,k,item))
67      | (ND d, k::ks0) => let
68          val (lab, rest) = ndest_term k
69          val ks = rest @ ks0
70          val n' =
71              case Binarymap.peek(d,lab) of
72                NONE => trav(newnode ks, ks)
73              | SOME n => trav(n, ks)
74        in
75          ND (Binarymap.insert(d, lab, n'))
76        end
77      | (EMPTY, ks) => trav(mkempty(), ks)
78      | _ => raise Fail "LVTermNet.insert: catastrophic invariant failure"
79in
80  (trav(net,[k]), sz + 1)
81end
82
83fun listItems (net, sz) = let
84  fun cons'(k,vs,acc) = List.foldl (fn (v,acc) => (k,v)::acc) acc vs
85  fun trav (net, acc) =
86      case net of
87        LF d => Binarymap.foldl cons' acc d
88      | ND d => let
89          fun foldthis (k,v,acc) = trav(v,acc)
90        in
91          Binarymap.foldl foldthis acc d
92        end
93      | EMPTY => []
94in
95  trav(net, [])
96end
97
98fun numItems (net, sz) = sz
99
100fun peek ((net,sz), k) = let
101  fun trav (net, tms) =
102      case (net, tms) of
103        (LF d, []) => (valOf (Binarymap.peek(d, k)) handle Option => [])
104      | (ND d, k::ks) => let
105          val (lab, rest) = ndest_term k
106        in
107          case Binarymap.peek(d, lab) of
108            NONE => []
109          | SOME n => trav(n, rest @ ks)
110        end
111      | (EMPTY, _) => []
112      | _ => raise Fail "LVTermNet.peek: catastrophic invariant failure"
113in
114  trav(net, [k])
115end
116
117val find = peek
118
119fun lookup_label tm = let
120  val (f, args) = strip_comb tm
121in
122  case dest_term f of
123    CONST{Name, Thy, ...} => (C ({Name=Name,Thy=Thy}, length args), args)
124  | LAMB(Bvar, Body) => (Lam (length args), Body::args)
125  | VAR (s, _) => (LV (s, length args), args)
126  | _ => raise Fail "LVTermNet.lookup_label: catastrophic invariant failure"
127end
128
129fun conslistItems (d, acc) = let
130  fun listfold k (v,acc) = (k,v)::acc
131  fun mapfold (k,vs,acc) = List.foldl (listfold k) acc vs
132in
133  Binarymap.foldl mapfold acc d
134end
135
136fun match ((net,sz), tm) = let
137  fun trav acc (net, ks) =
138      case (net, ks) of
139        (EMPTY, _) => []
140      | (LF d, []) => conslistItems (d, acc)
141      | (ND d, k::ks0) => let
142          val varresult = case Binarymap.peek(d, V 0) of
143                            NONE => acc
144                          | SOME n => trav acc (n, ks0)
145          val (lab, rest) = lookup_label k
146          val restn = length rest
147          val varhead_results = let
148            fun recurse acc n =
149              if n = 0 then acc
150              else
151                case Binarymap.peek (d, V n) of
152                    NONE => recurse acc (n - 1)
153                  | SOME m => recurse
154                                (trav acc (m, List.drop(rest, restn - n) @ ks0))
155                                (n - 1)
156          in
157            recurse varresult (length (#2 (strip_comb k)))
158          end
159        in
160          case Binarymap.peek (d, lab) of
161            NONE => varhead_results
162          | SOME n => trav varhead_results (n, rest @ ks0)
163        end
164      | _ => raise Fail "LVTermNet.match: catastrophic invariant failure"
165in
166  trav [] (net, [tm])
167end
168
169fun delete ((net,sz), k) = let
170  fun trav (p as (net, ks)) =
171      case p of
172        (EMPTY, _) => raise Binarymap.NotFound
173      | (LF d, []) => let
174          val (d',removed) = Binarymap.remove(d, k)
175        in
176          if Binarymap.numItems d' = 0 then (NONE, removed)
177          else (SOME (LF d'), removed)
178        end
179      | (ND d, k::ks) => let
180          val (lab, rest) = ndest_term k
181        in
182          case Binarymap.peek(d, lab) of
183            NONE => raise Binarymap.NotFound
184          | SOME n => let
185            in
186              case trav (n, rest @ ks) of
187                (NONE, removed) => let
188                  val (d',_) = Binarymap.remove(d, lab)
189                in
190                  if Binarymap.numItems d' = 0 then (NONE, removed)
191                  else (SOME (ND d'), removed)
192                end
193              | (SOME n', removed) => (SOME (ND (Binarymap.insert(d,lab,n'))),
194                                       removed)
195            end
196        end
197      | _ => raise Fail "LVTermNet.delete: catastrophic invariant failure"
198in
199  case trav (net, [k]) of
200    (NONE, removed) => (empty, removed)
201  | (SOME n, removed) =>  ((n,sz-1), removed)
202end
203
204fun app f (net, sz) = let
205  fun trav n =
206      case n of
207        LF d => Binarymap.app f d
208      | ND d => Binarymap.app (fn (lab, n) => trav n) d
209      | EMPTY => ()
210in
211  trav net
212end
213
214fun consfoldl f acc d = let
215  fun listfold k (d, acc) = f (k, d, acc)
216  fun mapfold (k,vs,acc) = List.foldl (listfold k) acc vs
217in
218  Binarymap.foldl mapfold acc d
219end
220
221fun fold f acc (net, sz) = let
222  fun trav acc n =
223      case n of
224        LF d => consfoldl f acc d
225      | ND d => Binarymap.foldl (fn (lab,n',acc) => trav acc n') acc d
226      | EMPTY => acc
227in
228  trav acc net
229end
230
231fun consmap f d = let
232  fun foldthis (k,vs,acc) = let
233    val bs = map (fn v => f(k,v)) vs
234  in
235    Binarymap.insert(acc,k,bs)
236  end
237in
238  Binarymap.foldl foldthis (Binarymap.mkDict tlt_compare) d
239end
240
241fun map f (net, sz) = let
242  fun trav n =
243      case n of
244        LF d => LF (consmap f d)
245      | ND d => ND (Binarymap.transform trav d)
246      | EMPTY => EMPTY
247in
248  (trav net, sz)
249end
250
251fun transform f = map (fn (k,v) => f v)
252
253
254end (* struct *)
255