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