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;
wenzelm@6905
     1
(*  Title:      HOL/Tools/numeral_syntax.ML
wenzelm@6905
     2
    ID:         $Id$
kleing@20067
     3
    Authors:    Markus Wenzel, TU Muenchen
wenzelm@6905
     4
wenzelm@21780
     5
Concrete syntax for generic numerals -- preserves leading zeros/ones.
wenzelm@6905
     6
*)
wenzelm@6905
     7
wenzelm@6905
     8
signature NUMERAL_SYNTAX =
wenzelm@6905
     9
sig
wenzelm@18708
    10
  val setup: theory -> theory
wenzelm@6905
    11
end;
wenzelm@6905
    12
wenzelm@6905
    13
structure NumeralSyntax: NUMERAL_SYNTAX =
wenzelm@6905
    14
struct
wenzelm@6905
    15
wenzelm@6905
    16
wenzelm@21780
    17
(* parse translation *)
wenzelm@21780
    18
wenzelm@21780
    19
local
wenzelm@21780
    20
wenzelm@21780
    21
fun mk_bin num =
wenzelm@21780
    22
  let
wenzelm@21780
    23
    val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
wenzelm@21780
    24
    fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
wenzelm@21780
    25
    fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
wenzelm@21780
    26
      | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
wenzelm@21789
    27
      | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
wenzelm@21780
    28
  in mk value end;
wenzelm@21780
    29
wenzelm@21780
    30
in
wenzelm@21780
    31
wenzelm@21780
    32
fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
wenzelm@21780
    33
      Syntax.const "Numeral.number_of" $ mk_bin num
wenzelm@21780
    34
  | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
wenzelm@21780
    35
wenzelm@21780
    36
end;
wenzelm@6905
    37
wenzelm@21780
    38
wenzelm@21780
    39
(* print translation *)
wenzelm@21780
    40
wenzelm@21780
    41
local
wenzelm@21780
    42
wenzelm@21780
    43
fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
wenzelm@21780
    44
  | dest_bit (Const ("Numeral.bit.B1", _)) = 1
wenzelm@21780
    45
  | dest_bit (Const ("bit.B0", _)) = 0
wenzelm@21780
    46
  | dest_bit (Const ("bit.B1", _)) = 1
wenzelm@21780
    47
  | dest_bit _ = raise Match;
wenzelm@21780
    48
wenzelm@21780
    49
fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = []
wenzelm@21780
    50
  | dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1]
wenzelm@21780
    51
  | dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs
wenzelm@21780
    52
  | dest_bin _ = raise Match;
wenzelm@21780
    53
wenzelm@21780
    54
fun leading _ [] = 0
wenzelm@21780
    55
  | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
wenzelm@21780
    56
wenzelm@21780
    57
fun int_of [] = 0
wenzelm@21780
    58
  | int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs;
wenzelm@6905
    59
wenzelm@6905
    60
fun dest_bin_str tm =
wenzelm@6905
    61
  let
wenzelm@21780
    62
    val rev_digs = dest_bin tm;
wenzelm@21780
    63
    val (sign, z) =
wenzelm@6905
    64
      (case rev rev_digs of
wenzelm@21780
    65
        ~1 :: bs => ("-", leading 1 bs)
wenzelm@21780
    66
      | bs => ("", leading 0 bs));
wenzelm@21780
    67
    val i = int_of rev_digs;
obua@15595
    68
    val num = IntInf.toString (IntInf.abs i);
wenzelm@11701
    69
  in
wenzelm@21780
    70
    if (i = 0 orelse i = 1) andalso z = 0 then raise Match
wenzelm@21780
    71
    else sign ^ implode (replicate z "0") ^ num
wenzelm@11701
    72
  end;
wenzelm@6905
    73
wenzelm@21780
    74
in
wenzelm@6905
    75
wenzelm@6905
    76
fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
wenzelm@11488
    77
      let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
wenzelm@7429
    78
        if not (! show_types) andalso can Term.dest_Type T then t'
wenzelm@6905
    79
        else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
wenzelm@6905
    80
      end
wenzelm@13110
    81
  | numeral_tr' _ (*"number_of"*) T (t :: ts) =
wenzelm@13110
    82
      if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t)
wenzelm@13110
    83
      else raise Match
wenzelm@6905
    84
  | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
wenzelm@6905
    85
wenzelm@21780
    86
end;
wenzelm@21780
    87
wenzelm@6905
    88
wenzelm@6905
    89
(* theory setup *)
wenzelm@6905
    90
wenzelm@6905
    91
val setup =
wenzelm@18708
    92
  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
wenzelm@18708
    93
  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
wenzelm@6905
    94
wenzelm@6905
    95
end;