212 | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; |
212 | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; |
213 |
213 |
214 |
214 |
215 (* explode atoms *) |
215 (* explode atoms *) |
216 |
216 |
217 fun explode_tr (*"_explode"*) [consC, nilC, bit0, bit1, Free (str, _)] = |
217 fun explode_tr (*"_explode"*) (ts as [consC, nilC, bit0, bit1, txt]) = |
218 let |
218 let |
219 fun mk_list [] = nilC |
219 fun mk_list [] = nilC |
220 | mk_list (t :: ts) = consC $ t $ mk_list ts; |
220 | mk_list (t :: ts) = consC $ t $ mk_list ts; |
221 |
221 |
222 fun encode_bit 0 = bit0 |
222 fun encode_bit 0 = bit0 |
223 | encode_bit 1 = bit1 |
223 | encode_bit 1 = bit1 |
224 | encode_bit _ = sys_error "encode_bit"; |
224 | encode_bit _ = sys_error "encode_bit"; |
225 |
225 |
226 fun encode_char c = (* FIXME leading 0s (?) *) |
226 fun encode_char c = (* FIXME leading 0s (?) *) |
227 mk_list (map encode_bit (radixpand (2, (ord c)))); |
227 mk_list (map encode_bit (radixpand (2, (ord c)))); |
|
228 |
|
229 val str = |
|
230 (case txt of |
|
231 Free (s, _) => s |
|
232 | Const (s, _) => s |
|
233 | _ => raise_term "explode_tr" ts); |
228 in |
234 in |
229 mk_list (map encode_char (explode str)) |
235 mk_list (map encode_char (explode str)) |
230 end |
236 end |
231 | explode_tr (*"_explode"*) ts = raise_term "explode_tr" ts; |
237 | explode_tr (*"_explode"*) ts = raise_term "explode_tr" ts; |
232 |
238 |
495 Delimfix ("'(_')", "idt => idt", ""), |
501 Delimfix ("'(_')", "idt => idt", ""), |
496 Delimfix ("_", "idt => idts", ""), |
502 Delimfix ("_", "idt => idts", ""), |
497 Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0), |
503 Mixfix ("_/ _", "[idt, idts] => idts", "_idts", [1, 0], 0), |
498 Delimfix ("_", "id => aprop", ""), |
504 Delimfix ("_", "id => aprop", ""), |
499 Delimfix ("_", "var => aprop", ""), |
505 Delimfix ("_", "var => aprop", ""), |
500 Mixfix ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], max_pri), (* FIXME lhs pri: 0 vs. max_pri *) |
506 Mixfix ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], max_pri), |
501 Delimfix ("PROP _", "aprop => prop", "_aprop"), |
507 Delimfix ("PROP _", "aprop => prop", "_aprop"), |
502 Delimfix ("_", "prop => asms", ""), |
508 Delimfix ("_", "prop => asms", ""), |
503 Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"), |
509 Delimfix ("_;/ _", "[prop, asms] => asms", "_asms"), |
504 Mixfix ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1), |
510 Mixfix ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1), |
505 Mixfix ("(_ ==/ _)", "['a::{}, 'a] => prop", "==", [3, 2], 2), |
511 Mixfix ("(_ ==/ _)", "['a::{}, 'a] => prop", "==", [3, 2], 2), |