fix integer overflow in numeral syntax for SML NJ.
authorobua
Tue Mar 08 16:02:52 2005 +0100 (2005-03-08)
changeset 15595dc8a41c7cefc
parent 15594 36f3e7ef3cb6
child 15596 8665d08085df
fix integer overflow in numeral syntax for SML NJ.
src/HOL/Tools/numeral_syntax.ML
src/HOL/hologic.ML
     1.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Mar 08 00:45:58 2005 +0100
     1.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Mar 08 16:02:52 2005 +0100
     1.3 @@ -42,18 +42,17 @@
     1.4        (case rev rev_digs of
     1.5          ~1 :: bs => ("-", prefix_len (equal 1) bs)
     1.6        | bs => ("", prefix_len (equal 0) bs));
     1.7 -    val i = HOLogic.int_of rev_digs;
     1.8 -    val num = string_of_int (abs i);
     1.9 +    val i = HOLogic.intinf_of rev_digs;
    1.10 +    val num = IntInf.toString (IntInf.abs i);
    1.11    in
    1.12 -    if i = 0 orelse i = 1 then raise Match
    1.13 +    if i = IntInf.fromInt 0 orelse i = IntInf.fromInt 1 then raise Match
    1.14      else sign ^ implode (replicate zs "0") ^ num
    1.15    end;
    1.16  
    1.17 -
    1.18  (* translation of integer numeral tokens to and from bitstrings *)
    1.19  
    1.20  fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
    1.21 -      (Syntax.const "Numeral.number_of" $ HOLogic.mk_bin (Syntax.read_xnum str))
    1.22 +      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin_from_intinf (valOf (IntInf.fromString str))))
    1.23    | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    1.24  
    1.25  fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
    1.26 @@ -74,5 +73,4 @@
    1.27    Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    1.28    Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    1.29  
    1.30 -
    1.31  end;
     2.1 --- a/src/HOL/hologic.ML	Tue Mar 08 00:45:58 2005 +0100
     2.2 +++ b/src/HOL/hologic.ML	Tue Mar 08 16:02:52 2005 +0100
     2.3 @@ -76,8 +76,10 @@
     2.4    val bit_const: term
     2.5    val number_of_const: typ -> term
     2.6    val int_of: int list -> int
     2.7 +  val intinf_of: int list -> IntInf.int
     2.8    val dest_binum: term -> int
     2.9    val mk_bin: int -> term
    2.10 +  val mk_bin_from_intinf: IntInf.int -> term
    2.11    val mk_list: ('a -> term) -> typ -> 'a list -> term
    2.12    val dest_list: term -> term list
    2.13  end;
    2.14 @@ -297,6 +299,9 @@
    2.15  fun int_of [] = 0
    2.16    | int_of (b :: bs) = b + 2 * int_of bs;
    2.17  
    2.18 +fun intinf_of [] = IntInf.fromInt 0
    2.19 +  | intinf_of (b :: bs) = IntInf.+ (IntInf.fromInt b, IntInf.*(IntInf.fromInt 2, intinf_of bs));
    2.20 +
    2.21  fun dest_bit (Const ("False", _)) = 0
    2.22    | dest_bit (Const ("True", _)) = 1
    2.23    | dest_bit t = raise TERM("dest_bit", [t]);
    2.24 @@ -323,6 +328,28 @@
    2.25        | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
    2.26      in term_of (bin_of n) end;
    2.27  
    2.28 +fun mk_bin_from_intinf  n =
    2.29 +    let
    2.30 +	val zero = IntInf.fromInt 0
    2.31 +	val minus_one = IntInf.fromInt ~1
    2.32 +	val two = IntInf.fromInt 2
    2.33 +
    2.34 +	fun mk_bit n = if n = zero then false_const else true_const
    2.35 +								 
    2.36 +	fun bin_of n = 
    2.37 +	    if n = zero then pls_const
    2.38 +	    else if n = minus_one then min_const
    2.39 +	    else 
    2.40 +		let 
    2.41 +		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!*)
    2.42 +	            val q = IntInf.div (n, two)
    2.43 +		    val r = IntInf.mod (n, two)
    2.44 +		in
    2.45 +		    bit_const $ bin_of q $ mk_bit r
    2.46 +		end
    2.47 +    in 
    2.48 +	bin_of n
    2.49 +    end
    2.50  
    2.51  (* int *)
    2.52