src/HOL/Tools/numeral_syntax.ML
changeset 21780 ec264b9daf94
parent 21763 12a2773e3608
child 21789 c4f6bb392030
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Dec 12 00:25:03 2006 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Dec 12 00:25:05 2006 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Authors:    Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Concrete syntax for generic numerals.
     1.8 +Concrete syntax for generic numerals -- preserves leading zeros/ones.
     1.9  *)
    1.10  
    1.11  signature NUMERAL_SYNTAX =
    1.12 @@ -14,32 +14,64 @@
    1.13  struct
    1.14  
    1.15  
    1.16 -(* bit strings *)   (*we try to handle superfluous leading digits nicely*)
    1.17 +(* parse translation *)
    1.18 +
    1.19 +local
    1.20 +
    1.21 +fun mk_bin num =
    1.22 +  let
    1.23 +    val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
    1.24 +    fun bit b bs = Syntax.const "\\<^const>Numeral.Bit" $ bs $ HOLogic.mk_bit b;
    1.25 +    fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const "\\<^const>Numeral.Pls")
    1.26 +      | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const "\\<^const>Numeral.Min")
    1.27 +      | mk i = let val (q, r) = IntInf.divMod (i, 2) in bit r (mk q) end;
    1.28 +  in mk value end;
    1.29 +
    1.30 +in
    1.31 +
    1.32 +fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
    1.33 +      Syntax.const "Numeral.number_of" $ mk_bin num
    1.34 +  | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.35 +
    1.36 +end;
    1.37  
    1.38 -fun prefix_len _ [] = 0
    1.39 -  | prefix_len pred (x :: xs) =
    1.40 -      if pred x then 1 + prefix_len pred xs else 0;
    1.41 +
    1.42 +(* print translation *)
    1.43 +
    1.44 +local
    1.45 +
    1.46 +fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
    1.47 +  | dest_bit (Const ("Numeral.bit.B1", _)) = 1
    1.48 +  | dest_bit (Const ("bit.B0", _)) = 0
    1.49 +  | dest_bit (Const ("bit.B1", _)) = 1
    1.50 +  | dest_bit _ = raise Match;
    1.51 +
    1.52 +fun dest_bin (Const ("\\<^const>Numeral.Pls", _)) = []
    1.53 +  | dest_bin (Const ("\\<^const>Numeral.Min", _)) = [~1]
    1.54 +  | dest_bin (Const ("\\<^const>Numeral.Bit", _) $ bs $ b) = dest_bit b :: dest_bin bs
    1.55 +  | dest_bin _ = raise Match;
    1.56 +
    1.57 +fun leading _ [] = 0
    1.58 +  | leading (i: int) (j :: js) = if i = j then 1 + leading i js else 0;
    1.59 +
    1.60 +fun int_of [] = 0
    1.61 +  | int_of (b :: bs) = IntInf.fromInt b + 2 * int_of bs;
    1.62  
    1.63  fun dest_bin_str tm =
    1.64    let
    1.65 -    val rev_digs = HOLogic.bin_of tm handle TERM _ => raise Match
    1.66 -    val (sign, zs) =
    1.67 +    val rev_digs = dest_bin tm;
    1.68 +    val (sign, z) =
    1.69        (case rev rev_digs of
    1.70 -        ~1 :: bs => ("-", prefix_len (equal 1) bs)
    1.71 -      | bs => ("", prefix_len (equal 0) bs));
    1.72 -    val i = HOLogic.int_of rev_digs;
    1.73 +        ~1 :: bs => ("-", leading 1 bs)
    1.74 +      | bs => ("", leading 0 bs));
    1.75 +    val i = int_of rev_digs;
    1.76      val num = IntInf.toString (IntInf.abs i);
    1.77    in
    1.78 -    if i = IntInf.fromInt 0 orelse i = IntInf.fromInt 1 then raise Match
    1.79 -    else sign ^ implode (replicate zs "0") ^ num
    1.80 +    if (i = 0 orelse i = 1) andalso z = 0 then raise Match
    1.81 +    else sign ^ implode (replicate z "0") ^ num
    1.82    end;
    1.83  
    1.84 -
    1.85 -(* translation of integer numeral tokens to and from bitstrings *)
    1.86 -
    1.87 -fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
    1.88 -      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_binum (Syntax.read_xnum str)))
    1.89 -  | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.90 +in
    1.91  
    1.92  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    1.93        let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
    1.94 @@ -51,6 +83,8 @@
    1.95        else raise Match
    1.96    | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
    1.97  
    1.98 +end;
    1.99 +
   1.100  
   1.101  (* theory setup *)
   1.102