18 structure NumeralSyntax: NUMERAL_SYNTAX = |
18 structure NumeralSyntax: NUMERAL_SYNTAX = |
19 struct |
19 struct |
20 |
20 |
21 (* Bits *) |
21 (* Bits *) |
22 |
22 |
23 val zero = Const("0", iT); |
23 fun mk_bit 0 = @{term "0"} |
24 val succ = Const("succ", iT --> iT); |
24 | mk_bit 1 = @{term "succ(0)"} |
25 |
|
26 fun mk_bit 0 = zero |
|
27 | mk_bit 1 = succ$zero |
|
28 | mk_bit _ = sys_error "mk_bit"; |
25 | mk_bit _ = sys_error "mk_bit"; |
29 |
26 |
30 fun dest_bit (Const ("0", _)) = 0 |
27 fun dest_bit (Const (@{const_name "0"}, _)) = 0 |
31 | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1 |
28 | dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1 |
32 | dest_bit _ = raise Match; |
29 | dest_bit _ = raise Match; |
33 |
30 |
34 |
31 |
35 (* Bit strings *) (*we try to handle superfluous leading digits nicely*) |
32 (* Bit strings *) (*we try to handle superfluous leading digits nicely*) |
36 |
33 |
37 fun prefix_len _ [] = 0 |
34 fun prefix_len _ [] = 0 |
38 | prefix_len pred (x :: xs) = |
35 | prefix_len pred (x :: xs) = |
39 if pred x then 1 + prefix_len pred xs else 0; |
36 if pred x then 1 + prefix_len pred xs else 0; |
40 |
37 |
41 val pls_const = Const ("Bin.bin.Pls", iT) |
|
42 and min_const = Const ("Bin.bin.Min", iT) |
|
43 and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT); |
|
44 |
|
45 fun mk_bin i = |
38 fun mk_bin i = |
46 let fun bin_of_int 0 = [] |
39 let fun bin_of_int 0 = [] |
47 | bin_of_int ~1 = [~1] |
40 | bin_of_int ~1 = [~1] |
48 | bin_of_int n = (n mod 2) :: bin_of_int (n div 2); |
41 | bin_of_int n = (n mod 2) :: bin_of_int (n div 2); |
49 |
42 |
50 fun term_of [] = pls_const |
43 fun term_of [] = @{const Pls} |
51 | term_of [~1] = min_const |
44 | term_of [~1] = @{const Min} |
52 | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b; |
45 | term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b; |
53 in |
46 in |
54 term_of (bin_of_int i) |
47 term_of (bin_of_int i) |
55 end; |
48 end; |
56 |
49 |
57 (*we consider all "spellings", since they could vary depending on the caller*) |
50 (*we consider all "spellings", since they could vary depending on the caller*) |