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