author | wenzelm |
Sat, 01 Feb 2014 18:42:46 +0100 | |
changeset 55236 | 8d61b0aa7a0d |
parent 55148 | 7e1b7cb54114 |
child 58399 | c5430cf9aa87 |
permissions | -rw-r--r-- |
28308 | 1 |
(* Title: HOL/Tools/numeral.ML |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
3 |
|
51314
eac4bb5adbf9
just one HOLogic.Trueprop_conv, with regular exception CTERM;
wenzelm
parents:
48072
diff
changeset
|
4 |
Logical operations on numerals (see also HOL/Tools/hologic.ML). |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
5 |
*) |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
6 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
7 |
signature NUMERAL = |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
8 |
sig |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset
|
9 |
val mk_cnumeral: int -> cterm |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset
|
10 |
val mk_cnumber: ctyp -> int -> cterm |
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34898
diff
changeset
|
11 |
val add_code: string -> bool -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
12 |
end; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
13 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
14 |
structure Numeral: NUMERAL = |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
15 |
struct |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
16 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
17 |
(* numeral *) |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
18 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
19 |
fun mk_cbit 0 = @{cterm "Num.Bit0"} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
20 |
| mk_cbit 1 = @{cterm "Num.Bit1"} |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
21 |
| mk_cbit _ = raise CTERM ("mk_cbit", []); |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
22 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
23 |
fun mk_cnumeral i = |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
24 |
let |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
25 |
fun mk 1 = @{cterm "Num.One"} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
26 |
| mk i = |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset
|
27 |
let val (q, r) = Integer.div_mod i 2 in |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
28 |
Thm.apply (mk_cbit r) (mk q) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
29 |
end |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
30 |
in |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
31 |
if i > 0 then mk i else raise CTERM ("mk_cnumeral: negative input", []) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
32 |
end |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
33 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
34 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
35 |
(* number *) |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
36 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
37 |
local |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
38 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
39 |
val zero = @{cpat "0"}; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
40 |
val zeroT = Thm.ctyp_of_term zero; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
41 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
42 |
val one = @{cpat "1"}; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
43 |
val oneT = Thm.ctyp_of_term one; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
44 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
45 |
val numeral = @{cpat "numeral"}; |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
46 |
val numeralT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term numeral))); |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
47 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
52435
diff
changeset
|
48 |
val uminus = @{cpat "uminus"}; |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
52435
diff
changeset
|
49 |
val uminusT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term uminus))); |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
50 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
51 |
fun instT T V = Thm.instantiate_cterm ([(V, T)], []); |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
52 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
53 |
in |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
54 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
55 |
fun mk_cnumber T 0 = instT T zeroT zero |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
56 |
| mk_cnumber T 1 = instT T oneT one |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
57 |
| mk_cnumber T i = |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
58 |
if i > 0 then Thm.apply (instT T numeralT numeral) (mk_cnumeral i) |
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
52435
diff
changeset
|
59 |
else Thm.apply (instT T uminusT uminus) (Thm.apply (instT T numeralT numeral) (mk_cnumeral (~i))); |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
60 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
61 |
end; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
62 |
|
25932 | 63 |
|
64 |
(* code generator *) |
|
65 |
||
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
66 |
local open Basic_Code_Thingol in |
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
67 |
|
34944
970e1466028d
code literals: distinguish numeral classes by different entries
haftmann
parents:
34898
diff
changeset
|
68 |
fun add_code number_of negative print target thy = |
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
69 |
let |
55148
7e1b7cb54114
avoid (now superfluous) indirect passing of constant names
haftmann
parents:
55147
diff
changeset
|
70 |
fun dest_numeral thm t = |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset
|
71 |
let |
55148
7e1b7cb54114
avoid (now superfluous) indirect passing of constant names
haftmann
parents:
55147
diff
changeset
|
72 |
fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0 |
7e1b7cb54114
avoid (now superfluous) indirect passing of constant names
haftmann
parents:
55147
diff
changeset
|
73 |
| dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1 |
55236 | 74 |
| dest_bit _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal bit"; |
55148
7e1b7cb54114
avoid (now superfluous) indirect passing of constant names
haftmann
parents:
55147
diff
changeset
|
75 |
fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1 |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
76 |
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1 |
55236 | 77 |
| dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"; |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
78 |
in if negative then ~ (dest_num t) else dest_num t end; |
55148
7e1b7cb54114
avoid (now superfluous) indirect passing of constant names
haftmann
parents:
55147
diff
changeset
|
79 |
fun pretty literals _ thm _ _ [(t, _)] = |
7e1b7cb54114
avoid (now superfluous) indirect passing of constant names
haftmann
parents:
55147
diff
changeset
|
80 |
(Code_Printer.str o print literals o dest_numeral thm) t; |
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
81 |
in |
52435
6646bb548c6b
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
haftmann
parents:
51314
diff
changeset
|
82 |
thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of, |
55148
7e1b7cb54114
avoid (now superfluous) indirect passing of constant names
haftmann
parents:
55147
diff
changeset
|
83 |
[(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) |
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
84 |
end; |
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
85 |
|
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
86 |
end; (*local*) |
25932 | 87 |
|
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
88 |
end; |