107 val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss') |
107 val (sign, istr) = case ss' of "-" :: istr => (~1, istr) | _ => (1, ss') |
108 in |
108 in |
109 case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE |
109 case Library.read_int istr of (i, []) => SOME (sign * i) | _ => NONE |
110 end; |
110 end; |
111 |
111 |
112 (** transform binary numeralsstrings **) |
112 (** transform binary numerals to "Free (string, T)" **) |
113 |
113 |
114 (*Makarius 100308, hacked by WN*) |
114 (* Makarius 100308 *) |
115 val numbers_to_string = |
115 val numbers_to_string = |
116 let |
116 let |
117 fun dest_num t = |
117 fun dest_num t = |
118 (case try HOLogic.dest_number t of |
118 (case try HOLogic.dest_number t of |
119 SOME (T, i) => |
119 SOME (T, i) => SOME (Free (signed_string_of_int i, T)) |
120 (*if T = @{typ int} orelse T = @{typ real} then WN*) |
|
121 SOME (Free (signed_string_of_int i, T)) |
|
122 (*else NONE WN*) |
|
123 | NONE => NONE); |
120 | NONE => NONE); |
124 fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) |
121 fun to_str (Abs (x, T, b)) = Abs (x, T, to_str b) |
125 | to_str (t as (u1 $ u2)) = |
122 | to_str (t as (u1 $ u2)) = |
126 (case dest_num t of |
123 (case dest_num t of SOME t' => t' | NONE => to_str u1 $ to_str u2) |
127 SOME t' => t' |
|
128 | NONE => to_str u1 $ to_str u2) |
|
129 | to_str t = perhaps dest_num t; |
124 | to_str t = perhaps dest_num t; |
130 in to_str end |
125 in to_str end |
131 val uminus_to_string = |
126 val uminus_to_string = |
132 let |
127 let |
133 fun dest_num t = |
128 fun dest_num t = |