src/HOL/Tools/numeral_syntax.ML
author wenzelm
Tue, 12 Dec 2006 12:03:46 +0100
changeset 21789 c4f6bb392030
parent 21780 ec264b9daf94
child 21821 7fa19d17f488
permissions -rw-r--r--
make SML/NJ happy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/numeral_syntax.ML
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
20067
26bac504ef90 hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents: 19481
diff changeset
     3
    Authors:    Markus Wenzel, TU Muenchen
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     4
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
     5
Concrete syntax for generic numerals -- preserves leading zeros/ones.
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     6
*)
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     7
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     8
signature NUMERAL_SYNTAX =
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     9
sig
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 16365
diff changeset
    10
  val setup: theory -> theory
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    11
end;
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    12
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    13
structure NumeralSyntax: NUMERAL_SYNTAX =
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    14
struct
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    15
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    16
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    17
(* parse translation *)
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    18
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    19
local
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    20
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    21
fun mk_bin num =
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    22
  let
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    23
    val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    24
    fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    25
    fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    26
      | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
21789
c4f6bb392030 make SML/NJ happy;
wenzelm
parents: 21780
diff changeset
    27
      | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit (IntInf.toInt r) (mk q) end;
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    28
  in mk value end;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    29
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    30
in
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    31
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    32
fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    33
      Syntax.const "Numeral.number_of" $ mk_bin num
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    34
  | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    35
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    36
end;
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    37
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    38
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    39
(* print translation *)
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    40
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    41
local
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    42
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    43
fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    44
  | dest_bit (Const ("Numeral.bit.B1", _)) = 1
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    45
  | dest_bit (Const ("bit.B0", _)) = 0
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    46
  | dest_bit (Const ("bit.B1", _)) = 1
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    47
  | dest_bit _ = raise Match;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    48
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    49
fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = []
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    50
  | dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1]
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    51
  | dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    52
  | dest_bin _ = raise Match;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    53
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    54
fun leading _ [] = 0
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    55
  | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    56
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    57
fun int_of [] = 0
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    58
  | int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs;
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    59
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    60
fun dest_bin_str tm =
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    61
  let
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    62
    val rev_digs = dest_bin tm;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    63
    val (sign, z) =
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    64
      (case rev rev_digs of
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    65
        ~1 :: bs => ("-", leading 1 bs)
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    66
      | bs => ("", leading 0 bs));
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    67
    val i = int_of rev_digs;
15595
dc8a41c7cefc fix integer overflow in numeral syntax for SML NJ.
obua
parents: 15013
diff changeset
    68
    val num = IntInf.toString (IntInf.abs i);
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11488
diff changeset
    69
  in
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    70
    if (i = 0 orelse i = 1) andalso z = 0 then raise Match
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    71
    else sign ^ implode (replicate z "0") ^ num
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11488
diff changeset
    72
  end;
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    73
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    74
in
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    75
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    76
fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
11488
4ff900551340 constify numeral tokens in order to allow translations;
wenzelm
parents: 10891
diff changeset
    77
      let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
7429
8f284fbb8728 observe show_types;
wenzelm
parents: 7078
diff changeset
    78
        if not (! show_types) andalso can Term.dest_Type T then t'
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    79
        else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    80
      end
13110
ca8cd110f769 be liberal about missing types;
wenzelm
parents: 11701
diff changeset
    81
  | numeral_tr' _ (*"number_of"*) T (t :: ts) =
ca8cd110f769 be liberal about missing types;
wenzelm
parents: 11701
diff changeset
    82
      if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t)
ca8cd110f769 be liberal about missing types;
wenzelm
parents: 11701
diff changeset
    83
      else raise Match
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    84
  | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    85
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    86
end;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    87
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    88
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    89
(* theory setup *)
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    90
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    91
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 16365
diff changeset
    92
  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 16365
diff changeset
    93
  Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    94
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    95
end;