18 local |
18 local |
19 |
19 |
20 fun mk_bin num = |
20 fun mk_bin num = |
21 let |
21 let |
22 val {leading_zeros = z, value, ...} = Syntax.read_xnum num; |
22 val {leading_zeros = z, value, ...} = Syntax.read_xnum num; |
23 fun bit b bs = Syntax.const @{const_name Numeral.Bit} $ bs $ HOLogic.mk_bit b; |
23 fun bit b bs = Syntax.const @{const_name Int.Bit} $ bs $ HOLogic.mk_bit b; |
24 fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls}) |
24 fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Int.Pls}) |
25 | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.Min}) |
25 | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Int.Min}) |
26 | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end; |
26 | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end; |
27 in mk value end; |
27 in mk value end; |
28 |
28 |
29 in |
29 in |
30 |
30 |
31 fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] = |
31 fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] = |
32 Syntax.const @{const_name Numeral.number_of} $ mk_bin num |
32 Syntax.const @{const_name Int.number_of} $ mk_bin num |
33 | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); |
33 | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); |
34 |
34 |
35 end; |
35 end; |
36 |
36 |
37 |
37 |
38 (* print translation *) |
38 (* print translation *) |
39 |
39 |
40 local |
40 local |
41 |
41 |
42 fun dest_bit (Const (@{const_syntax Numeral.bit.B0}, _)) = 0 |
42 fun dest_bit (Const (@{const_syntax Int.bit.B0}, _)) = 0 |
43 | dest_bit (Const (@{const_syntax Numeral.bit.B1}, _)) = 1 |
43 | dest_bit (Const (@{const_syntax Int.bit.B1}, _)) = 1 |
44 | dest_bit (Const ("bit.B0", _)) = 0 |
44 | dest_bit (Const ("bit.B0", _)) = 0 |
45 | dest_bit (Const ("bit.B1", _)) = 1 |
45 | dest_bit (Const ("bit.B1", _)) = 1 |
46 | dest_bit _ = raise Match; |
46 | dest_bit _ = raise Match; |
47 |
47 |
48 fun dest_bin (Const (@{const_syntax "Numeral.Pls"}, _)) = [] |
48 fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = [] |
49 | dest_bin (Const (@{const_syntax "Numeral.Min"}, _)) = [~1] |
49 | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1] |
50 | dest_bin (Const (@{const_syntax "Numeral.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs |
50 | dest_bin (Const (@{const_syntax "Int.Bit"}, _) $ bs $ b) = dest_bit b :: dest_bin bs |
51 | dest_bin _ = raise Match; |
51 | dest_bin _ = raise Match; |
52 |
52 |
53 fun leading _ [] = 0 |
53 fun leading _ [] = 0 |
54 | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0; |
54 | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0; |
55 |
55 |