src/HOL/Tools/numeral_syntax.ML
author wenzelm
Mon Jan 16 21:50:15 2012 +0100 (2012-01-16)
changeset 46236 ae79f2978a67
parent 42290 b1f544c84040
permissions -rw-r--r--
position constraints for numerals enable PIDE markup;
wenzelm@6905
     1
(*  Title:      HOL/Tools/numeral_syntax.ML
kleing@20067
     2
    Authors:    Markus Wenzel, TU Muenchen
wenzelm@6905
     3
wenzelm@21780
     4
Concrete syntax for generic numerals -- preserves leading zeros/ones.
wenzelm@6905
     5
*)
wenzelm@6905
     6
wenzelm@6905
     7
signature NUMERAL_SYNTAX =
wenzelm@6905
     8
sig
wenzelm@18708
     9
  val setup: theory -> theory
wenzelm@6905
    10
end;
wenzelm@6905
    11
wenzelm@35123
    12
structure Numeral_Syntax: NUMERAL_SYNTAX =
wenzelm@6905
    13
struct
wenzelm@6905
    14
wenzelm@21780
    15
(* parse translation *)
wenzelm@21780
    16
wenzelm@21780
    17
local
wenzelm@21780
    18
wenzelm@21780
    19
fun mk_bin num =
wenzelm@21780
    20
  let
huffman@26086
    21
    fun bit b bs = HOLogic.mk_bit b $ bs;
wenzelm@29316
    22
    fun mk 0 = Syntax.const @{const_name Int.Pls}
wenzelm@29316
    23
      | mk ~1 = Syntax.const @{const_name Int.Min}
wenzelm@24630
    24
      | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
wenzelm@42290
    25
  in mk (#value (Lexicon.read_xnum num)) end;
wenzelm@21780
    26
wenzelm@21780
    27
in
wenzelm@21780
    28
wenzelm@46236
    29
fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ numeral_tr [t] $ u
wenzelm@46236
    30
  | numeral_tr [t as Const (num, _)] = Syntax.const @{const_syntax Int.number_of} $ mk_bin num
wenzelm@46236
    31
  | numeral_tr ts = raise TERM ("numeral_tr", ts);
wenzelm@21780
    32
wenzelm@21780
    33
end;
wenzelm@6905
    34
wenzelm@21780
    35
wenzelm@21780
    36
(* print translation *)
wenzelm@21780
    37
wenzelm@21780
    38
local
wenzelm@21780
    39
wenzelm@35115
    40
fun dest_bin (Const (@{const_syntax Int.Pls}, _)) = []
wenzelm@35115
    41
  | dest_bin (Const (@{const_syntax Int.Min}, _)) = [~1]
wenzelm@35115
    42
  | dest_bin (Const (@{const_syntax Int.Bit0}, _) $ bs) = 0 :: dest_bin bs
wenzelm@35115
    43
  | dest_bin (Const (@{const_syntax Int.Bit1}, _) $ bs) = 1 :: dest_bin bs
wenzelm@21780
    44
  | dest_bin _ = raise Match;
wenzelm@21780
    45
wenzelm@21780
    46
fun leading _ [] = 0
wenzelm@21780
    47
  | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
wenzelm@21780
    48
wenzelm@21780
    49
fun int_of [] = 0
wenzelm@24630
    50
  | int_of (b :: bs) = b + 2 * int_of bs;
wenzelm@6905
    51
wenzelm@6905
    52
fun dest_bin_str tm =
wenzelm@6905
    53
  let
wenzelm@21780
    54
    val rev_digs = dest_bin tm;
wenzelm@21780
    55
    val (sign, z) =
wenzelm@6905
    56
      (case rev rev_digs of
wenzelm@21780
    57
        ~1 :: bs => ("-", leading 1 bs)
wenzelm@21780
    58
      | bs => ("", leading 0 bs));
wenzelm@21780
    59
    val i = int_of rev_digs;
wenzelm@24630
    60
    val num = string_of_int (abs i);
wenzelm@11701
    61
  in
wenzelm@21780
    62
    if (i = 0 orelse i = 1) andalso z = 0 then raise Match
wenzelm@21780
    63
    else sign ^ implode (replicate z "0") ^ num
wenzelm@11701
    64
  end;
wenzelm@6905
    65
wenzelm@29316
    66
fun syntax_numeral t =
wenzelm@35115
    67
  Syntax.const @{syntax_const "_Numeral"} $
wenzelm@35115
    68
    (Syntax.const @{syntax_const "_numeral"} $ Syntax.free (dest_bin_str t));
wenzelm@29316
    69
wenzelm@21780
    70
in
wenzelm@6905
    71
wenzelm@42247
    72
fun numeral_tr' ctxt (Type (@{type_name fun}, [_, T])) (t :: ts) =
wenzelm@29316
    73
      let val t' =
wenzelm@39134
    74
        if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
wenzelm@42245
    75
        else
wenzelm@42248
    76
          Syntax.const @{syntax_const "_constrain"} $ syntax_numeral t $
wenzelm@42247
    77
            Syntax_Phases.term_of_typ ctxt T
wenzelm@29316
    78
      in list_comb (t', ts) end
wenzelm@42247
    79
  | numeral_tr' _ T (t :: ts) =
wenzelm@29316
    80
      if T = dummyT then list_comb (syntax_numeral t, ts)
wenzelm@13110
    81
      else raise Match
wenzelm@42247
    82
  | numeral_tr' _ _ _ = raise Match;
wenzelm@6905
    83
wenzelm@21780
    84
end;
wenzelm@21780
    85
wenzelm@6905
    86
wenzelm@6905
    87
(* theory setup *)
wenzelm@6905
    88
wenzelm@6905
    89
val setup =
wenzelm@35115
    90
  Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
wenzelm@39134
    91
  Sign.add_advanced_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
wenzelm@6905
    92
wenzelm@6905
    93
end;