author | wenzelm |
Wed, 04 Oct 2017 12:00:53 +0200 | |
changeset 66787 | 64b47495676d |
parent 62597 | b3f2b8c906a6 |
child 68028 | 1f9f973eed2a |
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_cnumber: ctyp -> int -> cterm |
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58399
diff
changeset
|
10 |
val mk_number_syntax: int -> term |
62597 | 11 |
val mk_cnumeral: int -> cterm |
12 |
val mk_num_syntax: int -> term |
|
13 |
val dest_num_syntax: term -> int |
|
14 |
val dest_num: Code_Thingol.iterm -> int option |
|
58399 | 15 |
val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
16 |
end; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
17 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
18 |
structure Numeral: NUMERAL = |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
19 |
struct |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
20 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
21 |
(* numeral *) |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
22 |
|
62597 | 23 |
fun dest_num_syntax (Const (@{const_syntax Num.Bit0}, _) $ t) = 2 * dest_num_syntax t |
24 |
| dest_num_syntax (Const (@{const_syntax Num.Bit1}, _) $ t) = 2 * dest_num_syntax t + 1 |
|
25 |
| dest_num_syntax (Const (@{const_syntax Num.One}, _)) = 1; |
|
26 |
||
27 |
fun mk_num_syntax n = |
|
28 |
if n > 0 then |
|
29 |
(case IntInf.quotRem (n, 2) of |
|
30 |
(0, 1) => Syntax.const @{const_syntax One} |
|
31 |
| (n, 0) => Syntax.const @{const_syntax Bit0} $ mk_num_syntax n |
|
32 |
| (n, 1) => Syntax.const @{const_syntax Bit1} $ mk_num_syntax n) |
|
33 |
else raise Match |
|
34 |
||
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
35 |
fun mk_cbit 0 = @{cterm "Num.Bit0"} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
36 |
| mk_cbit 1 = @{cterm "Num.Bit1"} |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
37 |
| mk_cbit _ = raise CTERM ("mk_cbit", []); |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
38 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
39 |
fun mk_cnumeral i = |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
40 |
let |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
41 |
fun mk 1 = @{cterm "Num.One"} |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
42 |
| mk i = |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
23575
diff
changeset
|
43 |
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
|
44 |
Thm.apply (mk_cbit r) (mk q) |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
45 |
end |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
46 |
in |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
47 |
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
|
48 |
end |
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
49 |
|
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 |
(* number *) |
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 |
local |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
54 |
|
61150 | 55 |
val cterm_of = Thm.cterm_of @{context}; |
56 |
fun tvar S = (("'a", 0), S); |
|
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
57 |
|
61150 | 58 |
val zero_tvar = tvar @{sort zero}; |
59 |
val zero = cterm_of (Const (@{const_name zero_class.zero}, TVar zero_tvar)); |
|
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
60 |
|
61150 | 61 |
val one_tvar = tvar @{sort one}; |
62 |
val one = cterm_of (Const (@{const_name one_class.one}, TVar one_tvar)); |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
63 |
|
61150 | 64 |
val numeral_tvar = tvar @{sort numeral}; |
65 |
val numeral = cterm_of (Const (@{const_name numeral}, @{typ num} --> TVar numeral_tvar)); |
|
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
66 |
|
61150 | 67 |
val uminus_tvar = tvar @{sort uminus}; |
68 |
val uminus = cterm_of (Const (@{const_name uminus}, TVar uminus_tvar --> TVar uminus_tvar)); |
|
69 |
||
70 |
fun instT T v = Thm.instantiate_cterm ([(v, T)], []); |
|
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
71 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
72 |
in |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
73 |
|
61150 | 74 |
fun mk_cnumber T 0 = instT T zero_tvar zero |
75 |
| mk_cnumber T 1 = instT T one_tvar one |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46497
diff
changeset
|
76 |
| mk_cnumber T i = |
61150 | 77 |
if i > 0 then |
78 |
Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral i) |
|
79 |
else |
|
80 |
Thm.apply (instT T uminus_tvar uminus) |
|
81 |
(Thm.apply (instT T numeral_tvar numeral) (mk_cnumeral (~ i))); |
|
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
82 |
|
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
83 |
end; |
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
84 |
|
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58399
diff
changeset
|
85 |
fun mk_number_syntax n = |
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58399
diff
changeset
|
86 |
if n = 0 then Syntax.const @{const_syntax Groups.zero} |
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58399
diff
changeset
|
87 |
else if n = 1 then Syntax.const @{const_syntax Groups.one} |
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58399
diff
changeset
|
88 |
else Syntax.const @{const_syntax numeral} $ mk_num_syntax n; |
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
58399
diff
changeset
|
89 |
|
25932 | 90 |
|
91 |
(* code generator *) |
|
92 |
||
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
93 |
local open Basic_Code_Thingol in |
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
94 |
|
62597 | 95 |
fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1 |
96 |
| dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) = |
|
97 |
(case dest_num t of |
|
98 |
SOME n => SOME (2 * n) |
|
99 |
| _ => NONE) |
|
100 |
| dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) = |
|
101 |
(case dest_num t of |
|
102 |
SOME n => SOME (2 * n + 1) |
|
103 |
| _ => NONE) |
|
104 |
| dest_num _ = NONE; |
|
105 |
||
58399 | 106 |
fun add_code number_of preproc print target thy = |
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
107 |
let |
58399 | 108 |
fun pretty literals _ thm _ _ [(t, _)] = |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28308
diff
changeset
|
109 |
let |
62597 | 110 |
val n = case dest_num t of |
111 |
SOME n => n |
|
112 |
| NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term" |
|
113 |
in (Code_Printer.str o print literals o preproc) n end; |
|
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
114 |
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
|
115 |
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
|
116 |
[(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) |
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
117 |
end; |
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
118 |
|
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
119 |
end; (*local*) |
25932 | 120 |
|
23575
543803006b3f
Logical operations on numerals (see also HOL/hologic.ML).
wenzelm
parents:
diff
changeset
|
121 |
end; |