author | haftmann |
Mon, 01 Sep 2008 10:18:37 +0200 | |
changeset 28064 | d4a6460c53d1 |
parent 28054 | 2b84d34c5d02 |
child 28090 | 29af3c712d2b |
permissions | -rw-r--r-- |
haftmann@25919 | 1 |
(* Title: HOL/Tools/Int.ML |
wenzelm@23575 | 2 |
ID: $Id$ |
wenzelm@23575 | 3 |
Author: Makarius |
wenzelm@23575 | 4 |
|
wenzelm@23575 | 5 |
Logical operations on numerals (see also HOL/hologic.ML). |
wenzelm@23575 | 6 |
*) |
wenzelm@23575 | 7 |
|
wenzelm@23575 | 8 |
signature NUMERAL = |
wenzelm@23575 | 9 |
sig |
wenzelm@24630 | 10 |
val mk_cnumeral: int -> cterm |
wenzelm@24630 | 11 |
val mk_cnumber: ctyp -> int -> cterm |
haftmann@25932 | 12 |
val add_code: string -> bool -> bool -> string -> theory -> theory |
wenzelm@23575 | 13 |
end; |
wenzelm@23575 | 14 |
|
wenzelm@23575 | 15 |
structure Numeral: NUMERAL = |
wenzelm@23575 | 16 |
struct |
wenzelm@23575 | 17 |
|
wenzelm@23575 | 18 |
(* numeral *) |
wenzelm@23575 | 19 |
|
huffman@26086 | 20 |
fun mk_cbit 0 = @{cterm "Int.Bit0"} |
huffman@26086 | 21 |
| mk_cbit 1 = @{cterm "Int.Bit1"} |
wenzelm@23575 | 22 |
| mk_cbit _ = raise CTERM ("mk_cbit", []); |
wenzelm@23575 | 23 |
|
haftmann@25919 | 24 |
fun mk_cnumeral 0 = @{cterm "Int.Pls"} |
haftmann@25919 | 25 |
| mk_cnumeral ~1 = @{cterm "Int.Min"} |
wenzelm@23575 | 26 |
| mk_cnumeral i = |
wenzelm@24630 | 27 |
let val (q, r) = Integer.div_mod i 2 in |
huffman@26086 | 28 |
Thm.capply (mk_cbit r) (mk_cnumeral q) |
wenzelm@23575 | 29 |
end; |
wenzelm@23575 | 30 |
|
wenzelm@23575 | 31 |
|
wenzelm@23575 | 32 |
(* number *) |
wenzelm@23575 | 33 |
|
wenzelm@23575 | 34 |
local |
wenzelm@23575 | 35 |
|
wenzelm@23575 | 36 |
val zero = @{cpat "0"}; |
wenzelm@23575 | 37 |
val zeroT = Thm.ctyp_of_term zero; |
wenzelm@23575 | 38 |
|
wenzelm@23575 | 39 |
val one = @{cpat "1"}; |
wenzelm@23575 | 40 |
val oneT = Thm.ctyp_of_term one; |
wenzelm@23575 | 41 |
|
wenzelm@23575 | 42 |
val number_of = @{cpat "number_of"}; |
wenzelm@23575 | 43 |
val numberT = Thm.ctyp_of @{theory} (Term.range_type (Thm.typ_of (Thm.ctyp_of_term number_of))); |
wenzelm@23575 | 44 |
|
wenzelm@23575 | 45 |
fun instT T V = Thm.instantiate_cterm ([(V, T)], []); |
wenzelm@23575 | 46 |
|
wenzelm@23575 | 47 |
in |
wenzelm@23575 | 48 |
|
wenzelm@23575 | 49 |
fun mk_cnumber T 0 = instT T zeroT zero |
wenzelm@23575 | 50 |
| mk_cnumber T 1 = instT T oneT one |
wenzelm@23575 | 51 |
| mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i); |
wenzelm@23575 | 52 |
|
wenzelm@23575 | 53 |
end; |
wenzelm@23575 | 54 |
|
haftmann@25932 | 55 |
|
haftmann@25932 | 56 |
(* code generator *) |
haftmann@25932 | 57 |
|
haftmann@25932 | 58 |
fun add_code number_of negative unbounded target = |
haftmann@28064 | 59 |
Code_Target.add_literal_numeral target negative unbounded number_of |
haftmann@25932 | 60 |
@{const_name Int.Pls} @{const_name Int.Min} |
huffman@26086 | 61 |
@{const_name Int.Bit0} @{const_name Int.Bit1}; |
haftmann@25932 | 62 |
|
wenzelm@23575 | 63 |
end; |