src/ZF/Tools/numeral_syntax.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 15965 f422f8283491
child 21781 8314ebb5364d
permissions -rw-r--r--
setup: theory -> theory;
paulson@9570
     1
(*  Title:      ZF/Tools/numeral_syntax.ML
paulson@9570
     2
    ID:         $Id$
paulson@9570
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@9570
     4
paulson@9570
     5
Concrete syntax for generic numerals.  Assumes consts and syntax of
paulson@9570
     6
theory ZF/Integ/Bin.
paulson@9570
     7
*)
paulson@9570
     8
paulson@9570
     9
signature NUMERAL_SYNTAX =
paulson@9570
    10
sig
paulson@15965
    11
  val dest_bin : term -> IntInf.int
paulson@15965
    12
  val mk_bin   : IntInf.int -> term
paulson@9570
    13
  val int_tr   : term list -> term
paulson@9570
    14
  val int_tr'  : bool -> typ -> term list -> term
wenzelm@18708
    15
  val setup    : theory -> theory
paulson@9570
    16
end;
paulson@9570
    17
paulson@9570
    18
structure NumeralSyntax: NUMERAL_SYNTAX =
paulson@9570
    19
struct
paulson@9570
    20
paulson@9570
    21
(* Bits *)
paulson@9570
    22
paulson@9570
    23
val zero = Const("0", iT);
paulson@9570
    24
val succ = Const("succ", iT --> iT);
paulson@9570
    25
paulson@15965
    26
fun mk_bit (0: IntInf.int) = zero
paulson@9570
    27
  | mk_bit 1 = succ$zero
paulson@9570
    28
  | mk_bit _ = sys_error "mk_bit";
paulson@9570
    29
paulson@9570
    30
fun dest_bit (Const ("0", _)) = 0
paulson@9570
    31
  | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
paulson@9570
    32
  | dest_bit _ = raise Match;
paulson@9570
    33
paulson@9570
    34
paulson@9570
    35
(* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
paulson@9570
    36
paulson@9570
    37
fun prefix_len _ [] = 0
paulson@9570
    38
  | prefix_len pred (x :: xs) =
paulson@9570
    39
      if pred x then 1 + prefix_len pred xs else 0;
paulson@9570
    40
paulson@9570
    41
val pls_const = Const ("Bin.bin.Pls", iT)
paulson@9570
    42
and min_const = Const ("Bin.bin.Min", iT)
paulson@9570
    43
and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
paulson@9570
    44
paulson@15965
    45
fun mk_bin (i: IntInf.int) =
paulson@15965
    46
  let fun bin_of_int 0  = []
paulson@15965
    47
  	    | bin_of_int ~1 = [~1]
paulson@15965
    48
    	| bin_of_int n  = (n mod 2) :: bin_of_int (n div 2);
paulson@9570
    49
paulson@9570
    50
      fun term_of []   = pls_const
paulson@15965
    51
	    | term_of [~1] = min_const
paulson@15965
    52
	    | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
paulson@9570
    53
  in
paulson@15965
    54
    term_of (bin_of_int i)
paulson@9570
    55
  end;
paulson@9570
    56
paulson@9570
    57
(*we consider all "spellings", since they could vary depending on the caller*)
paulson@9570
    58
fun bin_of (Const ("Pls", _)) = []
paulson@9570
    59
  | bin_of (Const ("bin.Pls", _)) = []
paulson@9570
    60
  | bin_of (Const ("Bin.bin.Pls", _)) = []
paulson@9570
    61
  | bin_of (Const ("Min", _)) = [~1]
paulson@9570
    62
  | bin_of (Const ("bin.Min", _)) = [~1]
paulson@9570
    63
  | bin_of (Const ("Bin.bin.Min", _)) = [~1]
paulson@9570
    64
  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
paulson@9570
    65
  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
paulson@9570
    66
  | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
paulson@9570
    67
  | bin_of _ = raise Match;
paulson@9570
    68
paulson@15965
    69
(*Convert a list of bits to an integer*)
paulson@15965
    70
fun integ_of [] = 0 : IntInf.int
paulson@15965
    71
  | integ_of (b :: bs) = (IntInf.fromInt b) + 2 * integ_of bs;
paulson@9570
    72
paulson@9570
    73
val dest_bin = integ_of o bin_of;
paulson@9570
    74
paulson@15965
    75
(*leading 0s and (for negative numbers) -1s cause complications, though they 
paulson@15965
    76
  should never arise in normal use. The formalization used in HOL prevents 
paulson@15965
    77
  them altogether.*)
paulson@9570
    78
fun show_int t =
paulson@9570
    79
  let
paulson@9570
    80
    val rev_digs = bin_of t;
paulson@9570
    81
    val (sign, zs) =
paulson@9570
    82
	(case rev rev_digs of
paulson@9570
    83
	     ~1 :: bs => ("-", prefix_len (equal 1) bs)
paulson@9570
    84
	   | bs =>       ("",  prefix_len (equal 0) bs));
paulson@15965
    85
    val num = IntInf.toString (abs (integ_of rev_digs));
paulson@9570
    86
  in
paulson@9570
    87
    "#" ^ sign ^ implode (replicate zs "0") ^ num
paulson@9570
    88
  end;
paulson@9570
    89
paulson@9570
    90
paulson@9570
    91
paulson@9570
    92
(* translation of integer constant tokens to and from binary *)
paulson@9570
    93
paulson@9570
    94
fun int_tr (*"_Int"*) [t as Free (str, _)] =
wenzelm@10917
    95
      Syntax.const "integ_of" $ mk_bin (Syntax.read_xnum str)
paulson@9570
    96
  | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
paulson@9570
    97
wenzelm@10917
    98
fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t)
paulson@9570
    99
  | int_tr' (_:bool) (_:typ)     _ = raise Match;
paulson@9570
   100
paulson@9570
   101
paulson@9570
   102
val setup =
wenzelm@18708
   103
 (Theory.add_trfuns ([], [("_Int", int_tr)], [], []) #>
wenzelm@18708
   104
  Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
paulson@9570
   105
paulson@9570
   106
end;