1structure patriciaSyntax :> patriciaSyntax = 2struct 3 4open Abbrev HolKernel patriciaTheory; 5 6val ERR = Feedback.mk_HOL_ERR "patriciaSyntax" 7 8(* ------------------------------------------------------------------------- *) 9 10fun mk_ptree_type pty = 11 Type.mk_thy_type{Tyop="ptree", Thy="patricia", Args = [pty]}; 12 13fun dest_ptree_type ty = 14 case total dest_thy_type ty 15 of SOME {Tyop="ptree",Thy="patricia",Args=[pty]} => pty 16 | _ => raise ERR "dest_ptree_type" "not an instance of 'a ptree"; 17 18val is_ptree_type = Lib.can dest_ptree_type; 19 20fun mk_pat_const s = prim_mk_const{Name = s, Thy = "patricia"}; 21 22val empty_tm = mk_pat_const "Empty"; 23val leaf_tm = mk_pat_const "Leaf"; 24val branch_tm = mk_pat_const "Branch"; 25val peek_tm = mk_pat_const "PEEK"; 26val find_tm = mk_pat_const "FIND"; 27val add_tm = mk_pat_const "ADD"; 28val add_list_tm = mk_pat_const "ADD_LIST"; 29val remove_tm = mk_pat_const "REMOVE"; 30val traverse_tm = mk_pat_const "TRAVERSE"; 31val keys_tm = mk_pat_const "KEYS"; 32val transform_tm = mk_pat_const "TRANSFORM"; 33val every_leaf_tm = mk_pat_const "EVERY_LEAF"; 34val exists_leaf_tm = mk_pat_const "EXISTS_LEAF"; 35val size_tm = mk_pat_const "SIZE"; 36val depth_tm = mk_pat_const "DEPTH"; 37val is_ptree_tm = mk_pat_const "IS_PTREE"; 38val in_ptree_tm = mk_pat_const "IN_PTREE"; 39val insert_ptree_tm = mk_pat_const "INSERT_PTREE"; 40val branching_bit_tm = mk_pat_const "BRANCHING_BIT"; 41val ptree_of_numset_tm = mk_pat_const "PTREE_OF_NUMSET"; 42val numset_of_ptree_tm = mk_pat_const "NUMSET_OF_PTREE"; 43 44fun mk_empty ty = 45 inst[alpha |-> ty] empty_tm 46 handle HOL_ERR _ => raise ERR "mk_empty" ""; 47 48fun mk_leaf(k,d) = 49 list_mk_comb(inst[alpha |-> type_of d] leaf_tm,[k,d]) 50 handle HOL_ERR _ => raise ERR "mk_leaf" ""; 51 52fun mk_branch(p,m,l,r) = 53 list_mk_comb(inst[alpha |-> dest_ptree_type (type_of l)] branch_tm,[p,m,l,r]) 54 handle HOL_ERR _ => raise ERR "mk_branch" ""; 55 56fun mk_peek(t,k) = 57 list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] peek_tm,[t,k]) 58 handle HOL_ERR _ => raise ERR "mk_peek" ""; 59 60fun mk_find(t,k) = 61 list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] find_tm,[t,k]) 62 handle HOL_ERR _ => raise ERR "mk_find" ""; 63 64fun mk_add(t,x) = 65 list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] add_tm, [t,x]) 66 handle HOL_ERR _ => raise ERR "mk_add" ""; 67 68fun mk_add_list(t,l) = 69 list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] add_list_tm,[t,l]) 70 handle HOL_ERR _ => raise ERR "mk_add_list" ""; 71 72fun mk_remove(t,k) = 73 list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] remove_tm,[t,k]) 74 handle HOL_ERR _ => raise ERR "mk_remove" ""; 75 76fun mk_traverse t = 77 mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] traverse_tm,t) 78 handle HOL_ERR _ => raise ERR "mk_traverse" ""; 79 80fun mk_keys t = 81 mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] keys_tm,t) 82 handle HOL_ERR _ => raise ERR "mk_keys" ""; 83 84fun mk_transform(f,t) = 85 let val (typb, typa) = dom_rng (type_of f) in 86 list_mk_comb(inst[alpha |-> typa, beta |-> typb] transform_tm,[f,t]) 87 end handle HOL_ERR _ => raise ERR "mk_transform" ""; 88 89fun mk_every_leaf(p,t) = 90 list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] every_leaf_tm,[p,t]) 91 handle HOL_ERR _ => raise ERR "mk_every_leaf" ""; 92 93fun mk_exists_leaf(p,t) = 94 list_mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] exists_leaf_tm,[p,t]) 95 handle HOL_ERR _ => raise ERR "mk_exists_leaf" ""; 96 97fun mk_size t = 98 mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] size_tm,t) 99 handle HOL_ERR _ => raise ERR "mk_size" ""; 100 101fun mk_depth t = 102 mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] depth_tm,t) 103 handle HOL_ERR _ => raise ERR "mk_depth" ""; 104 105fun mk_is_ptree t = 106 mk_comb(inst[alpha |-> dest_ptree_type (type_of t)] is_ptree_tm,t) 107 handle HOL_ERR _ => raise ERR "mk_is_ptree" ""; 108 109fun mk_in_ptree(k,t) = 110 list_mk_comb(in_ptree_tm,[k,t]) 111 handle HOL_ERR _ => raise ERR "mk_in_ptree" ""; 112 113fun mk_insert_ptree(k,t) = 114 list_mk_comb (insert_ptree_tm,[k,t]) 115 handle HOL_ERR _ => raise ERR "mk_insert_ptree" ""; 116 117fun mk_branching_bit(m,n) = 118 list_mk_comb (branching_bit_tm,[m,n]) 119 handle HOL_ERR _ => raise ERR "mk_branching_bit" ""; 120 121fun mk_ptree_of_numset(t,s) = 122 list_mk_comb 123 (inst[alpha |-> dest_ptree_type (type_of t)] ptree_of_numset_tm,[t,s]) 124 handle HOL_ERR _ => raise ERR "mk_ptree_of_numset" ""; 125 126fun mk_numset_of_ptree s = 127 mk_comb(numset_of_ptree_tm,s) 128 handle HOL_ERR _ => raise ERR "mk_numset_of_ptree" ""; 129 130fun dest_quadop c e tm = 131 case with_exn strip_comb tm e of 132 (t,[t1,t2,t3,t4]) => if same_const t c then (t1,t2,t3,t4) else raise e 133 | _ => raise e; 134 135val dest_leaf = dest_binop leaf_tm (ERR "dest_leaf" ""); 136val dest_branch = dest_quadop branch_tm (ERR "dest_branch" ""); 137val dest_peek = dest_binop peek_tm (ERR "dest_peek" ""); 138val dest_find = dest_binop find_tm (ERR "dest_find" ""); 139val dest_add = dest_binop add_tm (ERR "dest_add" ""); 140val dest_add_list = dest_binop add_list_tm (ERR "dest_add_list" ""); 141val dest_remove = dest_binop remove_tm (ERR "dest_remove" ""); 142val dest_traverse = dest_monop traverse_tm (ERR "dest_traverse" ""); 143val dest_keys = dest_monop keys_tm (ERR "dest_keys" ""); 144val dest_transform = dest_binop transform_tm (ERR "dest_transform" ""); 145val dest_every_leaf = dest_binop every_leaf_tm (ERR "dest_every_leaf" ""); 146val dest_exists_leaf = dest_binop exists_leaf_tm (ERR "dest_exists_leaf" ""); 147val dest_size = dest_monop size_tm (ERR "dest_size" ""); 148val dest_depth = dest_monop depth_tm (ERR "dest_depth" ""); 149val dest_is_ptree = dest_monop is_ptree_tm (ERR "dest_is_ptree" ""); 150val dest_in_ptree = dest_binop in_ptree_tm (ERR "dest_in_ptree" ""); 151val dest_insert_ptree = dest_binop insert_ptree_tm (ERR "dest_insert_ptree" ""); 152 153val dest_branching_bit = 154 dest_binop branching_bit_tm (ERR "dest_branching_bit" ""); 155 156val dest_ptree_of_numset = 157 dest_binop ptree_of_numset_tm (ERR "dest_ptree_of_numset" ""); 158 159val dest_numset_of_ptree = 160 dest_monop numset_of_ptree_tm (ERR "dest_numset_of_ptree" ""); 161 162val is_empty = same_const empty_tm 163val is_leaf = can dest_leaf; 164val is_branch = can dest_branch; 165val is_peek = can dest_peek; 166val is_find = can dest_find; 167val is_add = can dest_add; 168val is_add_list = can dest_add_list; 169val is_remove = can dest_remove; 170val is_traverse = can dest_traverse; 171val is_keys = can dest_keys; 172val is_transform = can dest_transform; 173val is_every_leaf = can dest_every_leaf; 174val is_exists_leaf = can dest_exists_leaf; 175val is_size = can dest_size; 176val is_depth = can dest_depth; 177val is_is_ptree = can dest_is_ptree; 178val is_in_ptree = can dest_in_ptree; 179val is_insert_ptree = can dest_insert_ptree; 180val is_branching_bit = can dest_branching_bit; 181val is_ptree_of_numset = can dest_ptree_of_numset; 182val is_numset_of_ptree = can dest_numset_of_ptree; 183 184end 185