283 parse_translation {* |
283 parse_translation {* |
284 let |
284 let |
285 fun num_of_int n = |
285 fun num_of_int n = |
286 if n > 0 then |
286 if n > 0 then |
287 (case IntInf.quotRem (n, 2) of |
287 (case IntInf.quotRem (n, 2) of |
288 (0, 1) => Syntax.const @{const_name One} |
288 (0, 1) => Syntax.const @{const_syntax One} |
289 | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n |
289 | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n |
290 | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n) |
290 | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n) |
291 else raise Match |
291 else raise Match |
292 val numeral = Syntax.const @{const_name numeral} |
292 val numeral = Syntax.const @{const_syntax numeral} |
293 val uminus = Syntax.const @{const_name uminus} |
293 val uminus = Syntax.const @{const_syntax uminus} |
294 val one = Syntax.const @{const_name Groups.one} |
294 val one = Syntax.const @{const_syntax Groups.one} |
295 val zero = Syntax.const @{const_name Groups.zero} |
295 val zero = Syntax.const @{const_syntax Groups.zero} |
296 fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
296 fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = |
297 c $ numeral_tr [t] $ u |
297 c $ numeral_tr [t] $ u |
298 | numeral_tr [Const (num, _)] = |
298 | numeral_tr [Const (num, _)] = |
299 let |
299 let |
300 val {value, ...} = Lexicon.read_xnum num; |
300 val {value, ...} = Lexicon.read_xnum num; |
301 in |
301 in |
302 if value = 0 then zero else |
302 if value = 0 then zero else |
303 if value > 0 |
303 if value > 0 |
304 then numeral $ num_of_int value |
304 then numeral $ num_of_int value |
305 else if value = ~1 then uminus $ one |
305 else if value = ~1 then uminus $ one |
306 else uminus $ (numeral $ num_of_int (~value)) |
306 else uminus $ (numeral $ num_of_int (~ value)) |
307 end |
307 end |
308 | numeral_tr ts = raise TERM ("numeral_tr", ts); |
308 | numeral_tr ts = raise TERM ("numeral_tr", ts); |
309 in [("_Numeral", K numeral_tr)] end |
309 in [(@{syntax_const "_Numeral"}, K numeral_tr)] end |
310 *} |
310 *} |
311 |
311 |
312 typed_print_translation {* |
312 typed_print_translation {* |
313 let |
313 let |
314 fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n |
314 fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n |