src/HOL/Tools/numeral_syntax.ML
author wenzelm
Fri Jan 02 19:29:18 2009 +0100 (2009-01-02)
changeset 29316 0a7fcdd77f4b
parent 26086 3c243098b64a
child 35115 446c5063e4fd
permissions -rw-r--r--
removed dead code;
proper "_numeral" token markup;
proper printing of arguments (higher-order numerals);
     1 (*  Title:      HOL/Tools/numeral_syntax.ML
     2     Authors:    Markus Wenzel, TU Muenchen
     3 
     4 Concrete syntax for generic numerals -- preserves leading zeros/ones.
     5 *)
     6 
     7 signature NUMERAL_SYNTAX =
     8 sig
     9   val setup: theory -> theory
    10 end;
    11 
    12 structure NumeralSyntax: NUMERAL_SYNTAX =
    13 struct
    14 
    15 (* parse translation *)
    16 
    17 local
    18 
    19 fun mk_bin num =
    20   let
    21     fun bit b bs = HOLogic.mk_bit b $ bs;
    22     fun mk 0 = Syntax.const @{const_name Int.Pls}
    23       | mk ~1 = Syntax.const @{const_name Int.Min}
    24       | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
    25   in mk (#value (Syntax.read_xnum num)) end;
    26 
    27 in
    28 
    29 fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
    30       Syntax.const @{const_name Int.number_of} $ mk_bin num
    31   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    32 
    33 end;
    34 
    35 
    36 (* print translation *)
    37 
    38 local
    39 
    40 fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
    41   | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
    42   | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
    43   | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
    44   | dest_bin _ = raise Match;
    45 
    46 fun leading _ [] = 0
    47   | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
    48 
    49 fun int_of [] = 0
    50   | int_of (b :: bs) = b + 2 * int_of bs;
    51 
    52 fun dest_bin_str tm =
    53   let
    54     val rev_digs = dest_bin tm;
    55     val (sign, z) =
    56       (case rev rev_digs of
    57         ~1 :: bs => ("-", leading 1 bs)
    58       | bs => ("", leading 0 bs));
    59     val i = int_of rev_digs;
    60     val num = string_of_int (abs i);
    61   in
    62     if (i = 0 orelse i = 1) andalso z = 0 then raise Match
    63     else sign ^ implode (replicate z "0") ^ num
    64   end;
    65 
    66 fun syntax_numeral t =
    67   Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t));
    68 
    69 in
    70 
    71 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    72       let val t' =
    73         if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
    74         else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
    75       in list_comb (t', ts) end
    76   | numeral_tr' _ (*"number_of"*) T (t :: ts) =
    77       if T = dummyT then list_comb (syntax_numeral t, ts)
    78       else raise Match
    79   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    80 
    81 end;
    82 
    83 
    84 (* theory setup *)
    85 
    86 val setup =
    87   Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    88   Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
    89 
    90 end;