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