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