71 val mk_Suc: term -> term |
71 val mk_Suc: term -> term |
72 val dest_Suc: term -> term |
72 val dest_Suc: term -> term |
73 val Suc_zero: term |
73 val Suc_zero: term |
74 val mk_nat: IntInf.int -> term |
74 val mk_nat: IntInf.int -> term |
75 val dest_nat: term -> IntInf.int |
75 val dest_nat: term -> IntInf.int |
76 val intT: typ |
|
77 val mk_int: IntInf.int -> term |
|
78 val realT: typ |
|
79 val bitT: typ |
76 val bitT: typ |
80 val B0_const: term |
77 val B0_const: term |
81 val B1_const: term |
78 val B1_const: term |
|
79 val mk_bit: int -> term |
|
80 val dest_bit: term -> int |
|
81 val intT: typ |
82 val pls_const: term |
82 val pls_const: term |
83 val min_const: term |
83 val min_const: term |
84 val bit_const: term |
84 val bit_const: term |
85 val number_of_const: typ -> term |
85 val number_of_const: typ -> term |
86 val int_of: int list -> IntInf.int |
86 val mk_binum: IntInf.int -> term |
87 val dest_binum: term -> IntInf.int |
87 val dest_binum: term -> IntInf.int |
88 val mk_binum: IntInf.int -> term |
88 val mk_int: IntInf.int -> term |
89 val bin_of : term -> int list |
89 val realT: typ |
90 val listT : typ -> typ |
|
91 val nibbleT: typ |
90 val nibbleT: typ |
92 val mk_nibble: int -> term |
91 val mk_nibble: int -> term |
93 val dest_nibble: term -> int |
92 val dest_nibble: term -> int |
94 val charT: typ |
93 val charT: typ |
95 val mk_char: int -> term |
94 val mk_char: int -> term |
96 val dest_char: term -> int |
95 val dest_char: term -> int |
97 val stringT: typ |
96 val listT : typ -> typ |
98 val mk_list: typ -> term list -> term |
97 val mk_list: typ -> term list -> term |
99 val dest_list: term -> term list |
98 val dest_list: term -> term list |
|
99 val stringT: typ |
100 val mk_string : string -> term |
100 val mk_string : string -> term |
101 val dest_string : term -> string |
101 val dest_string : term -> string |
102 end; |
102 end; |
103 |
103 |
104 structure HOLogic: HOLOGIC = |
104 structure HOLogic: HOLOGIC = |
297 fun dest_nat (Const ("HOL.zero", _)) = 0 |
297 fun dest_nat (Const ("HOL.zero", _)) = 0 |
298 | dest_nat (Const ("Suc", _) $ t) = IntInf.+ (dest_nat t, 1) |
298 | dest_nat (Const ("Suc", _) $ t) = IntInf.+ (dest_nat t, 1) |
299 | dest_nat t = raise TERM ("dest_nat", [t]); |
299 | dest_nat t = raise TERM ("dest_nat", [t]); |
300 |
300 |
301 |
301 |
302 (* binary numerals and int *) |
302 (* bit *) |
303 |
303 |
304 val intT = Type ("IntDef.int", []); |
|
305 val bitT = Type ("Numeral.bit", []); |
304 val bitT = Type ("Numeral.bit", []); |
306 |
305 |
307 val B0_const = Const ("Numeral.bit.B0", bitT); |
306 val B0_const = Const ("Numeral.bit.B0", bitT); |
308 val B1_const = Const ("Numeral.bit.B1", bitT); |
307 val B1_const = Const ("Numeral.bit.B1", bitT); |
|
308 |
|
309 fun mk_bit 0 = B0_const |
|
310 | mk_bit 1 = B1_const |
|
311 | mk_bit _ = raise TERM ("mk_bit", []); |
|
312 |
|
313 fun dest_bit (Const ("Numeral.bit.B0", _)) = 0 |
|
314 | dest_bit (Const ("Numeral.bit.B1", _)) = 1 |
|
315 | dest_bit t = raise TERM ("dest_bit", [t]); |
|
316 |
|
317 |
|
318 (* binary numerals and int -- non-unique representation due to leading zeros/ones! *) |
|
319 |
|
320 val intT = Type ("IntDef.int", []); |
309 |
321 |
310 val pls_const = Const ("Numeral.Pls", intT) |
322 val pls_const = Const ("Numeral.Pls", intT) |
311 and min_const = Const ("Numeral.Min", intT) |
323 and min_const = Const ("Numeral.Min", intT) |
312 and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT); |
324 and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT); |
313 |
325 |
|
326 fun mk_binum 0 = pls_const |
|
327 | mk_binum ~1 = min_const |
|
328 | mk_binum i = |
|
329 let val (q, r) = IntInf.divMod (i, 2) |
|
330 in bit_const $ mk_binum q $ mk_bit r end; |
|
331 |
|
332 fun dest_binum (Const ("Numeral.Pls", _)) = 0 |
|
333 | dest_binum (Const ("Numeral.Min", _)) = ~1 |
|
334 | dest_binum (Const ("Numeral.Bit", _) $ bs $ b) = |
|
335 2 * dest_binum bs + IntInf.fromInt (dest_bit b) |
|
336 | dest_binum t = raise TERM ("dest_binum", [t]); |
|
337 |
314 fun number_of_const T = Const ("Numeral.number_of", intT --> T); |
338 fun number_of_const T = Const ("Numeral.number_of", intT --> T); |
315 |
|
316 fun int_of [] = 0 |
|
317 | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs); |
|
318 |
|
319 (*When called from a print translation, the Numeral qualifier will probably have |
|
320 been removed from Bit, bit.B0, etc.*) (* FIXME !? *) |
|
321 fun dest_bit (Const ("Numeral.bit.B0", _)) = 0 |
|
322 | dest_bit (Const ("Numeral.bit.B1", _)) = 1 |
|
323 | dest_bit (Const ("bit.B0", _)) = 0 |
|
324 | dest_bit (Const ("bit.B1", _)) = 1 |
|
325 | dest_bit t = raise TERM("dest_bit", [t]); |
|
326 |
|
327 fun bin_of (Const ("Numeral.Pls", _)) = [] |
|
328 | bin_of (Const ("Numeral.Min", _)) = [~1] |
|
329 | bin_of (Const ("Numeral.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
330 | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs |
|
331 | bin_of t = raise TERM("bin_of", [t]); |
|
332 |
|
333 val dest_binum = int_of o bin_of; |
|
334 |
|
335 fun mk_binum n = |
|
336 let |
|
337 fun mk_bit n = if n = 0 then B0_const else B1_const; |
|
338 fun bin_of n = |
|
339 if n = 0 then pls_const |
|
340 else if n = ~1 then min_const |
|
341 else |
|
342 let val (q, r) = IntInf.divMod (n, 2); |
|
343 in bit_const $ bin_of q $ mk_bit r end; |
|
344 in bin_of n end; |
|
345 |
339 |
346 fun mk_int 0 = Const ("HOL.zero", intT) |
340 fun mk_int 0 = Const ("HOL.zero", intT) |
347 | mk_int 1 = Const ("HOL.one", intT) |
341 | mk_int 1 = Const ("HOL.one", intT) |
348 | mk_int i = number_of_const intT $ mk_binum i; |
342 | mk_int i = number_of_const intT $ mk_binum i; |
349 |
343 |