src/HOL/Tools/numeral_syntax.ML
author wenzelm
Wed Mar 03 00:32:14 2010 +0100 (2010-03-03)
changeset 35430 df2862dc23a8
parent 35363 09489d8ffece
child 39134 917b4b6ba3d2
permissions -rw-r--r--
adapted to authentic syntax -- actual types are verbatim;
     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 Numeral_Syntax: 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_syntax 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 @{syntax_const "_Numeral"} $
    68     (Syntax.const @{syntax_const "_numeral"} $ Syntax.free (dest_bin_str t));
    69 
    70 in
    71 
    72 fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
    73       let val t' =
    74         if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
    75         else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
    76       in list_comb (t', ts) end
    77   | numeral_tr' _ (*"number_of"*) T (t :: ts) =
    78       if T = dummyT then list_comb (syntax_numeral t, ts)
    79       else raise Match
    80   | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    81 
    82 end;
    83 
    84 
    85 (* theory setup *)
    86 
    87 val setup =
    88   Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
    89   Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
    90 
    91 end;