src/HOL/Tools/numeral_syntax.ML
author haftmann
Wed Dec 13 15:45:33 2006 +0100 (2006-12-13)
changeset 21821 7fa19d17f488
parent 21789 c4f6bb392030
child 22997 d4f3b015b50b
permissions -rw-r--r--
authentic syntax for number_of
     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 = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
    24     fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
    25       | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
    26       | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt 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 "Numeral.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_bit (Const ("Numeral.bit.B0", _)) = 0
    43   | dest_bit (Const ("Numeral.bit.B1", _)) = 1
    44   | dest_bit (Const ("bit.B0", _)) = 0
    45   | dest_bit (Const ("bit.B1", _)) = 1
    46   | dest_bit _ = raise Match;
    47 
    48 fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = []
    49   | dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1]
    50   | dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs
    51   | dest_bin _ = raise Match;
    52 
    53 fun leading _ [] = 0
    54   | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
    55 
    56 fun int_of [] = 0
    57   | int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs;
    58 
    59 fun dest_bin_str tm =
    60   let
    61     val rev_digs = dest_bin tm;
    62     val (sign, z) =
    63       (case rev rev_digs of
    64         ~1 :: bs => ("-", leading 1 bs)
    65       | bs => ("", leading 0 bs));
    66     val i = int_of rev_digs;
    67     val num = IntInf.toString (IntInf.abs i);
    68   in
    69     if (i = 0 orelse i = 1) andalso z = 0 then raise Match
    70     else sign ^ implode (replicate z "0") ^ num
    71   end;
    72 
    73 in
    74 
    75 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    76       let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
    77         if not (! show_types) andalso can Term.dest_Type T then t'
    78         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    79       end
    80   | numeral_tr' _ (*"number_of"*) T (t :: ts) =
    81       if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t)
    82       else raise Match
    83   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    84 
    85 end;
    86 
    87 
    88 (* theory setup *)
    89 
    90 val setup =
    91   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    92   Theory.add_trfunsT [("\\<^const>Numeral.number_of", numeral_tr')];
    93 
    94 end;