src/HOL/Tools/numeral_syntax.ML
author wenzelm
Tue Dec 12 12:03:46 2006 +0100 (2006-12-12)
changeset 21789 c4f6bb392030
parent 21780 ec264b9daf94
child 21821 7fa19d17f488
permissions -rw-r--r--
make SML/NJ happy;
     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 
    17 (* parse translation *)
    18 
    19 local
    20 
    21 fun mk_bin num =
    22   let
    23     val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
    24     fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
    25     fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
    26       | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
    27       | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
    28   in mk value end;
    29 
    30 in
    31 
    32 fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
    33       Syntax.const "Numeral.number_of" $ mk_bin num
    34   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    35 
    36 end;
    37 
    38 
    39 (* print translation *)
    40 
    41 local
    42 
    43 fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
    44   | dest_bit (Const ("Numeral.bit.B1", _)) = 1
    45   | dest_bit (Const ("bit.B0", _)) = 0
    46   | dest_bit (Const ("bit.B1", _)) = 1
    47   | dest_bit _ = raise Match;
    48 
    49 fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = []
    50   | dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1]
    51   | dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs
    52   | dest_bin _ = raise Match;
    53 
    54 fun leading _ [] = 0
    55   | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
    56 
    57 fun int_of [] = 0
    58   | int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs;
    59 
    60 fun dest_bin_str tm =
    61   let
    62     val rev_digs = dest_bin tm;
    63     val (sign, z) =
    64       (case rev rev_digs of
    65         ~1 :: bs => ("-", leading 1 bs)
    66       | bs => ("", leading 0 bs));
    67     val i = int_of rev_digs;
    68     val num = IntInf.toString (IntInf.abs i);
    69   in
    70     if (i = 0 orelse i = 1) andalso z = 0 then raise Match
    71     else sign ^ implode (replicate z "0") ^ num
    72   end;
    73 
    74 in
    75 
    76 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    77       let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
    78         if not (! show_types) andalso can Term.dest_Type T then t'
    79         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
    80       end
    81   | numeral_tr' _ (*"number_of"*) T (t :: ts) =
    82       if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t)
    83       else raise Match
    84   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    85 
    86 end;
    87 
    88 
    89 (* theory setup *)
    90 
    91 val setup =
    92   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    93   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
    94 
    95 end;