src/HOL/Tools/numeral_syntax.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 29316 0a7fcdd77f4b
child 35115 446c5063e4fd
permissions -rw-r--r--
use long names for old-style fold combinators;
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
20067
26bac504ef90 hex and binary numerals (contributed by Rafal Kolanski)
kleing
parents: 19481
diff changeset
     2
    Authors:    Markus Wenzel, TU Muenchen
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     3
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
     4
Concrete syntax for generic numerals -- preserves leading zeros/ones.
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     5
*)
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
signature NUMERAL_SYNTAX =
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
     8
sig
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 16365
diff changeset
     9
  val setup: theory -> theory
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    10
end;
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    11
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    12
structure NumeralSyntax: NUMERAL_SYNTAX =
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    13
struct
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    14
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    15
(* parse translation *)
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    16
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    17
local
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
fun mk_bin num =
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    20
  let
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
    21
    fun bit b bs = HOLogic.mk_bit b $ bs;
29316
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    22
    fun mk 0 = Syntax.const @{const_name Int.Pls}
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    23
      | mk ~1 = Syntax.const @{const_name Int.Min}
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 22997
diff changeset
    24
      | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
29316
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    25
  in mk (#value (Syntax.read_xnum num)) end;
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    26
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    27
in
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    28
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    29
fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 24712
diff changeset
    30
      Syntax.const @{const_name Int.number_of} $ mk_bin num
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    31
  | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    32
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    33
end;
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    34
21780
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
(* print translation *)
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    37
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    38
local
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    39
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 24712
diff changeset
    40
fun dest_bin (Const (@{const_syntax "Int.Pls"}, _)) = []
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 24712
diff changeset
    41
  | dest_bin (Const (@{const_syntax "Int.Min"}, _)) = [~1]
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
    42
  | dest_bin (Const (@{const_syntax "Int.Bit0"}, _) $ bs) = 0 :: dest_bin bs
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
    43
  | dest_bin (Const (@{const_syntax "Int.Bit1"}, _) $ bs) = 1 :: dest_bin bs
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    44
  | dest_bin _ = raise Match;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    45
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    46
fun leading _ [] = 0
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    47
  | 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
    48
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    49
fun int_of [] = 0
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 22997
diff changeset
    50
  | int_of (b :: bs) = b + 2 * int_of bs;
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    51
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    52
fun dest_bin_str tm =
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    53
  let
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    54
    val rev_digs = dest_bin tm;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    55
    val (sign, z) =
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    56
      (case rev rev_digs of
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    57
        ~1 :: bs => ("-", leading 1 bs)
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    58
      | bs => ("", leading 0 bs));
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    59
    val i = int_of rev_digs;
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 22997
diff changeset
    60
    val num = string_of_int (abs i);
11701
3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents: 11488
diff changeset
    61
  in
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    62
    if (i = 0 orelse i = 1) andalso z = 0 then raise Match
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    63
    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
    64
  end;
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    65
29316
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    66
fun syntax_numeral t =
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    67
  Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t));
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    68
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    69
in
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    70
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    71
fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
29316
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    72
      let val t' =
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    73
        if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    74
        else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    75
      in list_comb (t', ts) end
13110
ca8cd110f769 be liberal about missing types;
wenzelm
parents: 11701
diff changeset
    76
  | numeral_tr' _ (*"number_of"*) T (t :: ts) =
29316
0a7fcdd77f4b removed dead code;
wenzelm
parents: 26086
diff changeset
    77
      if T = dummyT then list_comb (syntax_numeral t, ts)
13110
ca8cd110f769 be liberal about missing types;
wenzelm
parents: 11701
diff changeset
    78
      else raise Match
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    79
  | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    80
21780
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    81
end;
ec264b9daf94 authentic syntax for Pls/Min/Bit;
wenzelm
parents: 21763
diff changeset
    82
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    83
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    84
(* theory setup *)
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    85
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    86
val setup =
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24630
diff changeset
    87
  Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 24712
diff changeset
    88
  Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
6905
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    89
9bc05ec3497b added Numeral.thy, Tools/numeral_syntax.ML;
wenzelm
parents:
diff changeset
    90
end;