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