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