src/ZF/Tools/numeral_syntax.ML
author wenzelm
Sat Feb 13 23:24:57 2010 +0100 (2010-02-13)
changeset 35123 e286d5df187a
parent 35112 ff6f60e6ab85
child 40314 b5ec88d9ac03
permissions -rw-r--r--
modernized structures;
paulson@9570
     1
(*  Title:      ZF/Tools/numeral_syntax.ML
paulson@9570
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@9570
     3
paulson@9570
     4
Concrete syntax for generic numerals.  Assumes consts and syntax of
wenzelm@23146
     5
theory Bin.
paulson@9570
     6
*)
paulson@9570
     7
paulson@9570
     8
signature NUMERAL_SYNTAX =
paulson@9570
     9
sig
wenzelm@35112
    10
  val make_binary: int -> int list
wenzelm@35112
    11
  val dest_binary: int list -> int
wenzelm@35112
    12
  val int_tr: term list -> term
wenzelm@35112
    13
  val int_tr': bool -> typ -> term list -> term
wenzelm@35112
    14
  val setup: theory -> theory
paulson@9570
    15
end;
paulson@9570
    16
wenzelm@35123
    17
structure Numeral_Syntax: NUMERAL_SYNTAX =
paulson@9570
    18
struct
paulson@9570
    19
wenzelm@35112
    20
(* bits *)
paulson@9570
    21
wenzelm@35112
    22
fun mk_bit 0 = Syntax.const @{const_syntax "0"}
wenzelm@35112
    23
  | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
paulson@9570
    24
  | mk_bit _ = sys_error "mk_bit";
paulson@9570
    25
wenzelm@35112
    26
fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
wenzelm@35112
    27
  | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
paulson@9570
    28
  | dest_bit _ = raise Match;
paulson@9570
    29
paulson@9570
    30
wenzelm@35112
    31
(* bit strings *)
wenzelm@35112
    32
wenzelm@35112
    33
fun make_binary 0 = []
wenzelm@35112
    34
  | make_binary ~1 = [~1]
wenzelm@35112
    35
  | make_binary n = (n mod 2) :: make_binary (n div 2);
paulson@9570
    36
wenzelm@35112
    37
fun dest_binary [] = 0
wenzelm@35112
    38
  | dest_binary (b :: bs) = b + 2 * dest_binary bs;
wenzelm@35112
    39
wenzelm@35112
    40
wenzelm@35112
    41
(*try to handle superfluous leading digits nicely*)
paulson@9570
    42
fun prefix_len _ [] = 0
paulson@9570
    43
  | prefix_len pred (x :: xs) =
paulson@9570
    44
      if pred x then 1 + prefix_len pred xs else 0;
paulson@9570
    45
wenzelm@24630
    46
fun mk_bin i =
wenzelm@35112
    47
  let
wenzelm@35112
    48
    fun term_of [] = Syntax.const @{const_syntax Pls}
wenzelm@35112
    49
      | term_of [~1] = Syntax.const @{const_syntax Min}
wenzelm@35112
    50
      | term_of (b :: bs) = Syntax.const @{const_syntax Bit} $ term_of bs $ mk_bit b;
wenzelm@35112
    51
  in term_of (make_binary i) end;
paulson@9570
    52
wenzelm@35112
    53
fun bin_of (Const (@{const_syntax Pls}, _)) = []
wenzelm@35112
    54
  | bin_of (Const (@{const_syntax Min}, _)) = [~1]
wenzelm@35112
    55
  | bin_of (Const (@{const_syntax Bit}, _) $ bs $ b) = dest_bit b :: bin_of bs
paulson@9570
    56
  | bin_of _ = raise Match;
paulson@9570
    57
wenzelm@35112
    58
(*Leading 0s and (for negative numbers) -1s cause complications, though they 
paulson@15965
    59
  should never arise in normal use. The formalization used in HOL prevents 
paulson@15965
    60
  them altogether.*)
paulson@9570
    61
fun show_int t =
paulson@9570
    62
  let
paulson@9570
    63
    val rev_digs = bin_of t;
paulson@9570
    64
    val (sign, zs) =
wenzelm@35112
    65
      (case rev rev_digs of
wenzelm@35112
    66
         ~1 :: bs => ("-", prefix_len (equal 1) bs)
wenzelm@35112
    67
      | bs => ("",  prefix_len (equal 0) bs));
wenzelm@35112
    68
    val num = string_of_int (abs (dest_binary rev_digs));
paulson@9570
    69
  in
paulson@9570
    70
    "#" ^ sign ^ implode (replicate zs "0") ^ num
paulson@9570
    71
  end;
paulson@9570
    72
paulson@9570
    73
paulson@9570
    74
(* translation of integer constant tokens to and from binary *)
paulson@9570
    75
paulson@9570
    76
fun int_tr (*"_Int"*) [t as Free (str, _)] =
wenzelm@35112
    77
      Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
paulson@9570
    78
  | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
paulson@9570
    79
wenzelm@35112
    80
fun int_tr' _ _ (*"integ_of"*) [t] =
wenzelm@35112
    81
      Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
wenzelm@35112
    82
  | int_tr' (_: bool) (_: typ) _ = raise Match;
paulson@9570
    83
paulson@9570
    84
paulson@9570
    85
val setup =
wenzelm@35112
    86
 (Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #>
wenzelm@35112
    87
  Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]);
paulson@9570
    88
paulson@9570
    89
end;