(* Title: HOL/Tools/numeral_syntax.ML Authors: Markus Wenzel, TU Muenchen Concrete syntax for generic numerals -- preserves leading zeros/ones. *) signature NUMERAL_SYNTAX = sig val setup: theory -> theory end; structure NumeralSyntax: NUMERAL_SYNTAX = struct (* parse translation *) local fun mk_bin num = let fun bit b bs = HOLogic.mk_bit b $ bs; fun mk 0 = Syntax.const @{const_name Int.Pls} | mk ~1 = Syntax.const @{const_name Int.Min} | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end; in mk (#value (Syntax.read_xnum num)) end; in fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] = Syntax.const @{const_name Int.number_of} $ mk_bin num | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts); end; (* print translation *) local fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = [] | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1] | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs | dest_bin _ = raise Match; fun leading _ [] = 0 | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0; fun int_of [] = 0 | int_of (b :: bs) = b + 2 * int_of bs; fun dest_bin_str tm = let val rev_digs = dest_bin tm; val (sign, z) = (case rev rev_digs of ~1 :: bs => ("-", leading 1 bs) | bs => ("", leading 0 bs)); val i = int_of rev_digs; val num = string_of_int (abs i); in if (i = 0 orelse i = 1) andalso z = 0 then raise Match else sign ^ implode (replicate z "0") ^ num end; fun syntax_numeral t = Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t)); in fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) = let val t' = if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T in list_comb (t', ts) end | numeral_tr' _ (*"number_of"*) T (t :: ts) = if T = dummyT then list_comb (syntax_numeral t, ts) else raise Match | numeral_tr' _ (*"number_of"*) _ _ = raise Match; end; (* theory setup *) val setup = Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #> Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')]; end;