# HG changeset patch
# User obua
# Date 1110294172 -3600
# Node ID dc8a41c7cefc024204d3151ed8764bf1e528eb54
# Parent  36f3e7ef3cb69d6d7d8f8846ec09dfb5b8eeab1d
fix integer overflow in numeral syntax for SML NJ.

diff -r 36f3e7ef3cb6 -r dc8a41c7cefc src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Tue Mar 08 00:45:58 2005 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML	Tue Mar 08 16:02:52 2005 +0100
@@ -42,18 +42,17 @@
       (case rev rev_digs of
         ~1 :: bs => ("-", prefix_len (equal 1) bs)
       | bs => ("", prefix_len (equal 0) bs));
-    val i = HOLogic.int_of rev_digs;
-    val num = string_of_int (abs i);
+    val i = HOLogic.intinf_of rev_digs;
+    val num = IntInf.toString (IntInf.abs i);
   in
-    if i = 0 orelse i = 1 then raise Match
+    if i = IntInf.fromInt 0 orelse i = IntInf.fromInt 1 then raise Match
     else sign ^ implode (replicate zs "0") ^ num
   end;
 
-
 (* translation of integer numeral tokens to and from bitstrings *)
 
 fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
-      (Syntax.const "Numeral.number_of" $ HOLogic.mk_bin (Syntax.read_xnum str))
+      (Syntax.const "Numeral.number_of" $ (HOLogic.mk_bin_from_intinf (valOf (IntInf.fromString str))))
   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
 
 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
@@ -74,5 +73,4 @@
   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
 
-
 end;
diff -r 36f3e7ef3cb6 -r dc8a41c7cefc src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Tue Mar 08 00:45:58 2005 +0100
+++ b/src/HOL/hologic.ML	Tue Mar 08 16:02:52 2005 +0100
@@ -76,8 +76,10 @@
   val bit_const: term
   val number_of_const: typ -> term
   val int_of: int list -> int
+  val intinf_of: int list -> IntInf.int
   val dest_binum: term -> int
   val mk_bin: int -> term
+  val mk_bin_from_intinf: IntInf.int -> term
   val mk_list: ('a -> term) -> typ -> 'a list -> term
   val dest_list: term -> term list
 end;
@@ -297,6 +299,9 @@
 fun int_of [] = 0
   | int_of (b :: bs) = b + 2 * int_of bs;
 
+fun intinf_of [] = IntInf.fromInt 0
+  | intinf_of (b :: bs) = IntInf.+ (IntInf.fromInt b, IntInf.*(IntInf.fromInt 2, intinf_of bs));
+
 fun dest_bit (Const ("False", _)) = 0
   | dest_bit (Const ("True", _)) = 1
   | dest_bit t = raise TERM("dest_bit", [t]);
@@ -323,6 +328,28 @@
       | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
     in term_of (bin_of n) end;
 
+fun mk_bin_from_intinf  n =
+    let
+	val zero = IntInf.fromInt 0
+	val minus_one = IntInf.fromInt ~1
+	val two = IntInf.fromInt 2
+
+	fun mk_bit n = if n = zero then false_const else true_const
+								 
+	fun bin_of n = 
+	    if n = zero then pls_const
+	    else if n = minus_one then min_const
+	    else 
+		let 
+		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!*)
+	            val q = IntInf.div (n, two)
+		    val r = IntInf.mod (n, two)
+		in
+		    bit_const $ bin_of q $ mk_bit r
+		end
+    in 
+	bin_of n
+    end
 
 (* int *)