1structure patricia_castsSyntax :> patricia_castsSyntax =
2struct
3
4(* interactive use:
5  app load ["pred_setSyntax", "wordsSyntax", "patriciaSyntax",
6            "patricia_castsTheory"];
7*)
8
9open Abbrev HolKernel pred_setSyntax wordsSyntax patriciaSyntax
10     patricia_castsTheory;
11
12val ERR = mk_HOL_ERR "patricia_castsSyntax"
13
14(* ------------------------------------------------------------------------- *)
15
16fun mk_word_ptree_type (aty, bty) =
17  Type.mk_thy_type{Tyop="word_ptree", Thy="patricia_casts", Args = [aty, bty]};
18
19fun dest_word_ptree_type ty =
20  case total dest_thy_type ty of
21    SOME {Tyop="word_ptree",Thy="patricia_casts",Args=[aty, bty]} => (aty, bty)
22  | _ => raise ERR "dest_word_ptree_type"
23                   "not an instance of ('a,'b) word_ptree";
24
25val is_word_ptree_type = Lib.can dest_word_ptree_type;
26
27(* ......................................................................... *)
28
29fun mk_pat_const s = prim_mk_const{Name = s, Thy = "patricia_casts"};
30
31val the_ptree_tm        = mk_pat_const "THE_PTREE"
32val some_ptree_tm       = mk_pat_const "SOME_PTREE"
33val wordempty_tm        = mk_pat_const "WordEmpty";
34
35val peekw_tm            = mk_pat_const "PEEKw"
36val findw_tm            = mk_pat_const "FINDw"
37val addw_tm             = mk_pat_const "ADDw"
38val add_listw_tm        = mk_pat_const "ADD_LISTw"
39val removew_tm          = mk_pat_const "REMOVEw"
40val traversew_tm        = mk_pat_const "TRAVERSEw"
41val keysw_tm            = mk_pat_const "KEYSw"
42val transformw_tm       = mk_pat_const "TRANSFORMw"
43val every_leafw_tm      = mk_pat_const "EVERY_LEAFw"
44val exists_leafw_tm     = mk_pat_const "EXISTS_LEAFw"
45val sizew_tm            = mk_pat_const "SIZEw"
46val depthw_tm           = mk_pat_const "DEPTHw"
47val in_ptreew_tm        = mk_pat_const "IN_PTREEw"
48val insert_ptreew_tm    = mk_pat_const "INSERT_PTREEw"
49val ptree_of_wordset_tm = mk_pat_const "PTREE_OF_WORDSET"
50val wordset_of_ptree_tm = mk_pat_const "WORDSET_OF_PTREE";
51
52(* ......................................................................... *)
53
54val peeks_tm              = mk_pat_const "PEEKs"
55val finds_tm              = mk_pat_const "FINDs"
56val adds_tm               = mk_pat_const "ADDs"
57val add_lists_tm          = mk_pat_const "ADD_LISTs"
58val removes_tm            = mk_pat_const "REMOVEs"
59val traverses_tm          = mk_pat_const "TRAVERSEs"
60val keyss_tm              = mk_pat_const "KEYSs"
61val in_ptrees_tm          = mk_pat_const "IN_PTREEs"
62val insert_ptrees_tm      = mk_pat_const "INSERT_PTREEs"
63val ptree_of_stringset_tm = mk_pat_const "PTREE_OF_STRINGSET"
64val stringset_of_ptree_tm = mk_pat_const "STRINGSET_OF_PTREE";
65
66(* ......................................................................... *)
67
68fun mk_wordempty(aty, bty) =
69  inst[alpha |-> aty, beta |-> bty] wordempty_tm
70  handle HOL_ERR _ => raise ERR "mk_wordempty" "";
71
72fun mk_the_ptree t =
73let val (tya,tyb) = dest_word_ptree_type (type_of t) in
74  mk_comb(inst[alpha |-> tyb, beta |-> tya] the_ptree_tm,t)
75end handle HOL_ERR _ => raise ERR "mk_the_ptree" "";
76
77fun mk_some_ptree(ty,t) =
78  mk_comb(inst[alpha |-> ty,
79                beta |-> dest_ptree_type (type_of t)] some_ptree_tm,t)
80  handle HOL_ERR _ => raise ERR "mk_some_ptree" "";
81
82fun mk_peekw(t,k) =
83let val (tya,tyb) = dest_word_ptree_type (type_of t) in
84  list_mk_comb(inst[alpha |-> tya, beta |-> tyb] peekw_tm,[t,k])
85end handle HOL_ERR _ => raise ERR "mk_peekw" "";
86
87fun mk_findw(t,k) =
88let val (tya,tyb) = dest_word_ptree_type (type_of t) in
89  list_mk_comb(inst[alpha |-> tyb, beta |-> tya] findw_tm,[t,k])
90end handle HOL_ERR _ => raise ERR "mk_findw" "";
91
92fun mk_addw(t,x) =
93let val (tya,tyb) = dest_word_ptree_type (type_of t) in
94  list_mk_comb(inst[alpha |-> tya, beta |-> tyb] addw_tm,[t,x])
95end handle HOL_ERR _ => raise ERR "mk_addw" "";
96
97fun mk_add_listw(t,l) =
98let val (tya,tyb) = dest_word_ptree_type (type_of t) in
99  list_mk_comb(inst[alpha |-> tya, beta |-> tyb] add_listw_tm,[t,l])
100end handle HOL_ERR _ => raise ERR "mk_add_listw" "";
101
102fun mk_removew(t,k) =
103let val (tya,tyb) = dest_word_ptree_type (type_of t) in
104  list_mk_comb(inst[alpha |-> tya, beta |-> tyb] removew_tm,[t,k])
105end handle HOL_ERR _ => raise ERR "mk_removew" "";
106
107fun mk_traversew t =
108let val (tya,tyb) = dest_word_ptree_type (type_of t) in
109  mk_comb(inst[alpha |-> tya, beta |-> tyb] traversew_tm,t)
110end handle HOL_ERR _ => raise ERR "mk_traversew" "";
111
112fun mk_keysw t =
113let val (tya,tyb) = dest_word_ptree_type (type_of t) in
114  mk_comb(inst[alpha |-> tya, beta |-> tyb] keysw_tm,t)
115end handle HOL_ERR _ => raise ERR "mk_keysw" "";
116
117fun mk_transformw(f,t) =
118let val (typb, typa) = dom_rng (type_of f)
119    val tyc = fst (dest_word_ptree_type (type_of t))
120in
121  list_mk_comb(inst[alpha |-> typa, beta |-> typb,
122                    gamma |-> tyc] transformw_tm,[f,t])
123end handle HOL_ERR _ => raise ERR "mk_transformw" "";
124
125fun mk_every_leafw(p,t) =
126let val (tya,tyb) = dest_word_ptree_type (type_of t) in
127  list_mk_comb(inst[alpha |-> tya, beta |-> tyb] every_leafw_tm,[p,t])
128end handle HOL_ERR _ => raise ERR "mk_every_leafw" "";
129
130fun mk_exists_leafw(p,t) =
131let val (tya,tyb) = dest_word_ptree_type (type_of t) in
132  list_mk_comb(inst[alpha |-> tya, beta |-> tyb] exists_leafw_tm,[p,t])
133end handle HOL_ERR _ => raise ERR "mk_exists_leafw" "";
134
135fun mk_sizew t =
136let val (tya,tyb) = dest_word_ptree_type (type_of t) in
137  mk_comb(inst[alpha |-> tya, beta |-> tyb] sizew_tm,t)
138end handle HOL_ERR _ => raise ERR "mk_sizew" "";
139
140fun mk_depthw t =
141let val (tya,tyb) = dest_word_ptree_type (type_of t) in
142  mk_comb(inst[alpha |-> tya, beta |-> tyb] depthw_tm,t)
143end handle HOL_ERR _ => raise ERR "mk_depthw" "";
144
145fun mk_in_ptreew(k,t) =
146  list_mk_comb(inst[alpha |-> dest_word_type (type_of k)] in_ptreew_tm,[k,t])
147  handle HOL_ERR _ => raise ERR "mk_in_ptreew" "";
148
149fun mk_insert_ptreew(k,t) =
150  list_mk_comb
151    (inst[alpha |-> dest_word_type (type_of k)] insert_ptreew_tm,[k,t])
152  handle HOL_ERR _ => raise ERR "mk_insert_ptreew" "";
153
154fun mk_ptree_of_wordset s =
155let val typ = dest_word_type (dest_set_type (type_of s)) in
156  mk_comb(inst [alpha |-> typ] ptree_of_wordset_tm,s)
157end handle HOL_ERR _ => raise ERR "mk_ptree_of_wordset" "";
158
159fun mk_wordset_of_ptree t =
160let val typ = fst (dest_word_ptree_type (type_of t)) in
161  mk_comb(inst [alpha |-> typ] wordset_of_ptree_tm,t)
162end handle HOL_ERR _ => raise ERR "mk_wordset_of_ptree" "";
163
164(* ......................................................................... *)
165
166fun mk_peeks(t,k) =
167  list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] peeks_tm,[t,k])
168  handle HOL_ERR _ => raise ERR "mk_peeks" "";
169
170fun mk_finds(t,k) =
171  list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] finds_tm,[t,k])
172  handle HOL_ERR _ => raise ERR "mk_finds" "";
173
174fun mk_adds(t,x) =
175  list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] adds_tm, [t,x])
176  handle HOL_ERR _ => raise ERR "mk_adds" "";
177
178fun mk_add_lists(t,l) =
179  list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] add_lists_tm,[t,l])
180  handle HOL_ERR _ => raise ERR "mk_add_lists" "";
181
182fun mk_removes(t,k) =
183  list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] removes_tm,[t,k])
184  handle HOL_ERR _ => raise ERR "mk_removes" "";
185
186fun mk_traverses t =
187  mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] traverses_tm,t)
188  handle HOL_ERR _ => raise ERR "mk_traverses" "";
189
190fun mk_keyss t =
191  mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] keyss_tm,t)
192  handle HOL_ERR _ => raise ERR "mk_keyss" "";
193
194fun mk_in_ptrees(k,t) =
195  list_mk_comb(in_ptrees_tm,[k,t])
196  handle HOL_ERR _ => raise ERR "mk_in_ptrees" "";
197
198fun mk_insert_ptrees(k,t) =
199  list_mk_comb (insert_ptrees_tm,[k,t])
200  handle HOL_ERR _ => raise ERR "mk_insert_ptrees" "";
201
202fun mk_ptree_of_stringset s =
203  mk_comb(ptree_of_stringset_tm,s)
204  handle HOL_ERR _ => raise ERR "mk_ptree_of_stringset" "";
205
206fun mk_stringset_of_ptree s =
207  mk_comb(stringset_of_ptree_tm,s)
208  handle HOL_ERR _ => raise ERR "mk_stringset_of_ptree" "";
209
210(* ......................................................................... *)
211
212val dest_the_ptree     = dest_monop the_ptree_tm (ERR "dest_the_ptree" "")
213val dest_some_ptree    = dest_monop some_ptree_tm (ERR "dest_some_ptree" "")
214val dest_wordempty     = dest_monop wordempty_tm (ERR "dest_wordempty" "")
215val dest_peekw         = dest_binop peekw_tm (ERR "dest_peekw" "")
216val dest_findw         = dest_binop findw_tm (ERR "dest_findw" "")
217val dest_addw          = dest_binop addw_tm (ERR "dest_addw" "")
218val dest_add_listw     = dest_binop add_listw_tm (ERR "dest_add_listw" "")
219val dest_removew       = dest_binop removew_tm (ERR "dest_removew" "")
220val dest_traversew     = dest_monop traversew_tm (ERR "dest_traversew" "")
221val dest_keysw         = dest_monop keysw_tm (ERR "dest_keysw" "")
222val dest_transformw    = dest_binop transformw_tm (ERR "dest_transformw" "")
223val dest_every_leafw   = dest_binop every_leafw_tm (ERR "dest_every_leafw" "")
224val dest_exists_leafw  = dest_binop exists_leafw_tm (ERR "dest_exists_leafw" "")
225val dest_sizew         = dest_monop sizew_tm (ERR "dest_sizew" "")
226val dest_depthw        = dest_monop depthw_tm (ERR "dest_depthw" "")
227val dest_in_ptreew     = dest_binop in_ptreew_tm (ERR "dest_in_ptreew" "")
228val dest_insert_ptreew = dest_binop insert_ptreew_tm
229                           (ERR "dest_insert_ptreew" "");
230
231val dest_ptree_of_wordset =
232   dest_monop ptree_of_wordset_tm (ERR "dest_ptree_of_numset" "");
233
234val dest_wordset_of_ptree =
235   dest_monop wordset_of_ptree_tm (ERR "dest_numset_of_ptree" "");
236
237(* ......................................................................... *)
238
239val dest_peeks         = dest_binop peeks_tm (ERR "dest_peeks" "")
240val dest_finds         = dest_binop finds_tm (ERR "dest_finds" "")
241val dest_adds          = dest_binop adds_tm (ERR "dest_adds" "")
242val dest_add_lists     = dest_binop add_lists_tm (ERR "dest_add_lists" "")
243val dest_removes       = dest_binop removes_tm (ERR "dest_removes" "")
244val dest_traverses     = dest_monop traverses_tm (ERR "dest_traverses" "")
245val dest_keyss         = dest_monop keyss_tm (ERR "dest_keyss" "")
246val dest_in_ptrees     = dest_binop in_ptrees_tm (ERR "dest_in_ptrees" "")
247val dest_insert_ptrees = dest_binop insert_ptrees_tm
248                           (ERR "dest_insert_ptrees" "");
249
250val dest_ptree_of_stringset =
251   dest_monop ptree_of_stringset_tm (ERR "dest_ptree_of_numset" "");
252
253val dest_stringset_of_ptree =
254   dest_monop stringset_of_ptree_tm (ERR "dest_numset_of_ptree" "");
255
256(* ......................................................................... *)
257
258val is_the_ptree        = can dest_the_ptree
259val is_some_ptree       = can dest_some_ptree
260val is_wordempty        = can dest_wordempty
261val is_peekw            = can dest_peekw
262val is_findw            = can dest_findw
263val is_addw             = can dest_addw
264val is_add_listw        = can dest_add_listw
265val is_removew          = can dest_removew
266val is_traversew        = can dest_traversew
267val is_keysw            = can dest_keysw
268val is_transformw       = can dest_transformw
269val is_every_leafw      = can dest_every_leafw
270val is_exists_leafw     = can dest_exists_leafw
271val is_sizew            = can dest_sizew
272val is_depthw           = can dest_depthw
273val is_in_ptreew        = can dest_in_ptreew
274val is_insert_ptreew    = can dest_insert_ptreew
275val is_ptree_of_wordset = can dest_ptree_of_wordset
276val is_wordset_of_ptree = can dest_wordset_of_ptree;
277
278(* ......................................................................... *)
279
280val is_peeks            = can dest_peeks
281val is_finds            = can dest_finds
282val is_adds             = can dest_adds
283val is_add_lists        = can dest_add_lists
284val is_removes          = can dest_removes
285val is_traverses        = can dest_traverses
286val is_keyss            = can dest_keyss
287val is_in_ptrees        = can dest_in_ptrees
288val is_insert_ptrees    = can dest_insert_ptrees
289val is_ptree_of_stringset = can dest_ptree_of_stringset
290val is_stringset_of_ptree = can dest_stringset_of_ptree;
291
292end
293