src/HOL/Tools/numeral_syntax.ML
 author wenzelm Tue Sep 18 16:08:00 2007 +0200 (2007-09-18) changeset 24630 351a308ab58d parent 22997 d4f3b015b50b child 24712 64ed05609568 permissions -rw-r--r--
simplified type int (eliminated IntInf.int, integer);
```     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_name Numeral.Bit} \$ bs \$ HOLogic.mk_bit b;
```
```    24     fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Numeral.Pls})
```
```    25       | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Numeral.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 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 (@{const_syntax Numeral.bit.B0}, _)) = 0
```
```    43   | dest_bit (Const (@{const_syntax 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_syntax "Numeral.Pls"}, _)) = []
```
```    49   | dest_bin (Const (@{const_syntax "Numeral.Min"}, _)) = [~1]
```
```    50   | dest_bin (Const (@{const_syntax "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) = 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 = string_of_int (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_syntax Numeral.number_of}, numeral_tr')];
```
```    93
```
```    94 end;
```