1structure TypeNet :> TypeNet = 2struct 3 4open HolKernel 5 6datatype label = TV 7 | TOP of {Thy : string, Tyop : string} * int 8 (* The integer records arity of operator - this is necessary when 9 types are redefined. If the old and new versions have the 10 same arity, all is well, but if they are different then the data 11 structure expects the wrong thing. 12 13 For example, if scratch$foo is of arity 1, then there will be a 14 ND node beneath it (where the argument gets treated). But if 15 the user dumps that foo, and replaces it with one of arity 0, an 16 attempt to follow the tree will find the node that was right before 17 when it should be a leaf. 18 19 If the user does a lot of this, the data structure will slowly fill 20 up with garbage. If a type gets replaced with a new one of the same 21 arity, the data for the old type will be returned as part of a 22 Binarymap.listItems when "match" is called, but the user will eliminate 23 the junk with the usual sort of call to match_type. With "peek", the 24 old data won't be called because the lookup at the leaf's Binarymap 25 will just find whatever's supposed to be associated with the new type. 26 *) 27 28fun reccmp ({Thy=th1,Tyop=op1}, {Thy=th2,Tyop=op2}) = 29 pair_compare(String.compare, String.compare) ((op1,th1),(op2,th2)) 30 31fun labcmp p = 32 case p of 33 (TV, TV) => EQUAL 34 | (TV, TOP _) => LESS 35 | (TOP opdata1, TOP opdata2) => 36 pair_compare(reccmp, Int.compare) (opdata1, opdata2) 37 | (TOP _, TV) => GREATER 38 39datatype 'a N = LF of (hol_type,'a) Binarymap.dict 40 | ND of (label,'a N) Binarymap.dict 41 | EMPTY 42(* redundant EMPTY constructor is used to get around value polymorphism problem 43 when creating a single value for empty below *) 44 45type 'a typenet = 'a N * int 46 47val empty = (EMPTY, 0) 48 49fun mkempty () = ND (Binarymap.mkDict labcmp) 50 51fun ndest_type ty = 52 if is_vartype ty then (TV, []) 53 else let 54 val {Thy,Tyop,Args} = dest_thy_type ty 55 in 56 (TOP({Thy=Thy,Tyop=Tyop},length Args), Args) 57 end 58 59fun insert ((net,sz), ty, item) = let 60 fun newnode labs = 61 case labs of 62 [] => LF (Binarymap.mkDict Type.compare) 63 | _ => mkempty() 64 fun trav (net, tys) = 65 case (net, tys) of 66 (LF d, []) => LF (Binarymap.insert(d,ty,item)) 67 | (ND d, ty::tys0) => let 68 val (lab, rest) = ndest_type ty 69 val tys = rest @ tys0 70 val n' = 71 case Binarymap.peek(d,lab) of 72 NONE => trav(newnode tys, tys) 73 | SOME n => trav(n, tys) 74 val d' = Binarymap.insert(d, lab, n') 75 in 76 ND d' 77 end 78 | (EMPTY, tys) => trav(mkempty(), tys) 79 | _ => raise Fail "TypeNet.insert: catastrophic invariant failure" 80in 81 (trav(net,[ty]), sz + 1) 82end 83 84fun listItems (net, sz) = let 85 fun cons'(k,v,acc) = (k,v)::acc 86 fun trav (net, acc) = 87 case net of 88 LF d => Binarymap.foldl cons' acc d 89 | ND d => let 90 fun foldthis (k,v,acc) = trav(v,acc) 91 in 92 Binarymap.foldl foldthis acc d 93 end 94 | EMPTY => [] 95in 96 trav(net, []) 97end 98 99fun numItems (net, sz) = sz 100 101fun peek ((net,sz), ty) = let 102 fun trav (net, tys) = 103 case (net, tys) of 104 (LF d, []) => Binarymap.peek(d, ty) 105 | (ND d, ty::tys) => let 106 val (lab, rest) = ndest_type ty 107 in 108 case Binarymap.peek(d, lab) of 109 NONE => NONE 110 | SOME n => trav(n, rest @ tys) 111 end 112 | (EMPTY, _) => NONE 113 | _ => raise Fail "TypeNet.peek: catastrophic invariant failure" 114in 115 trav(net, [ty]) 116end 117 118fun find (n, ty) = 119 valOf (peek (n, ty)) handle Option => raise Binarymap.NotFound 120 121fun match ((net,sz), ty) = let 122 fun trav acc (net, tyl) = 123 case (net, tyl) of 124 (EMPTY, _) => [] 125 | (LF d, []) => Binarymap.listItems d @ acc 126 | (ND d, ty::tys) => let 127 val varresult = case Binarymap.peek(d, TV) of 128 NONE => acc 129 | SOME n => trav acc (n, tys) 130 val (lab, rest) = ndest_type ty 131 in 132 case lab of 133 TV => varresult 134 | TOP _ => let 135 in 136 case Binarymap.peek (d, lab) of 137 NONE => varresult 138 | SOME n => trav varresult (n, rest @ tys) 139 end 140 end 141 | _ => raise Fail "TypeNet.match: catastrophic invariant failure" 142in 143 trav [] (net, [ty]) 144end 145 146fun delete ((net,sz), ty) = let 147 fun trav (p as (net, tyl)) = 148 case p of 149 (EMPTY, _) => raise Binarymap.NotFound 150 | (LF d, []) => let 151 val (d',removed) = Binarymap.remove(d, ty) 152 in 153 if Binarymap.numItems d' = 0 then (NONE, removed) 154 else (SOME (LF d'), removed) 155 end 156 | (ND d, ty::tys) => let 157 val (lab, rest) = ndest_type ty 158 in 159 case Binarymap.peek(d, lab) of 160 NONE => raise Binarymap.NotFound 161 | SOME n => let 162 in 163 case trav (n, rest @ tys) of 164 (NONE, removed) => let 165 val (d',_) = Binarymap.remove(d, lab) 166 in 167 if Binarymap.numItems d' = 0 then (NONE, removed) 168 else (SOME (ND d'), removed) 169 end 170 | (SOME n', removed) => (SOME (ND (Binarymap.insert(d,lab,n'))), 171 removed) 172 end 173 end 174 | _ => raise Fail "TypeNet.delete: catastrophic invariant failure" 175in 176 case trav (net, [ty]) of 177 (NONE, removed) => (empty, removed) 178 | (SOME n, removed) => ((n,sz-1), removed) 179end 180 181fun app f (net, sz) = let 182 fun trav n = 183 case n of 184 LF d => Binarymap.app f d 185 | ND d => Binarymap.app (fn (lab, n) => trav n) d 186 | EMPTY => () 187in 188 trav net 189end 190 191fun fold f acc (net, sz) = let 192 fun trav acc n = 193 case n of 194 LF d => Binarymap.foldl f acc d 195 | ND d => Binarymap.foldl (fn (lab,n',acc) => trav acc n') acc d 196 | EMPTY => acc 197in 198 trav acc net 199end 200 201fun map f (net, sz) = let 202 fun trav n = 203 case n of 204 LF d => LF (Binarymap.map f d) 205 | ND d => ND (Binarymap.transform trav d) 206 | EMPTY => EMPTY 207in 208 (trav net, sz) 209end 210 211fun transform f = map (fn (k,v) => f v) 212 213 214end (* struct *) 215