--- a/NEWS Tue Sep 18 17:53:37 2007 +0200
+++ b/NEWS Tue Sep 18 18:05:34 2007 +0200
@@ -1142,7 +1142,7 @@
*** ML ***
-* Generic arithmetic modules: Tools/integer.ML, Tools/rat.ML, Tools/float.ML
+* Generic arithmetic modules: Tools/rat.ML, Tools/float.ML
* Context data interfaces (Theory/Proof/GenericDataFun): removed
name/print, uninitialized data defaults to ad-hoc copy of empty value,
--- a/src/HOL/HOL.thy Tue Sep 18 17:53:37 2007 +0200
+++ b/src/HOL/HOL.thy Tue Sep 18 18:05:34 2007 +0200
@@ -8,7 +8,6 @@
theory HOL
imports CPure
uses
- "~~/src/Tools/integer.ML"
("hologic.ML")
"~~/src/Tools/IsaPlanner/zipper.ML"
"~~/src/Tools/IsaPlanner/isand.ML"
--- a/src/HOL/IsaMakefile Tue Sep 18 17:53:37 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 18 18:05:34 2007 +0200
@@ -83,7 +83,7 @@
$(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML \
$(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
$(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
- $(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML $(SRC)/Tools/Metis/metis.ML\
+ $(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML\
$(SRC)/Tools/code/code_funcgr.ML \
$(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_package.ML \
$(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML \
--- a/src/Pure/General/ROOT.ML Tue Sep 18 17:53:37 2007 +0200
+++ b/src/Pure/General/ROOT.ML Tue Sep 18 18:05:34 2007 +0200
@@ -16,6 +16,7 @@
use "../ML/ml_parse.ML";
use "secure.ML";
+use "integer.ML";
use "stack.ML";
use "heap.ML";
use "ord_list.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/integer.ML Tue Sep 18 18:05:34 2007 +0200
@@ -0,0 +1,58 @@
+(* Title: Tools/integer.ML
+ ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+
+Unbounded integers.
+*)
+
+signature INTEGER =
+sig
+ val sign: int -> order
+ val sum: int list -> int
+ val div_mod: int -> int -> int * int
+ val square: int -> int
+ val pow: int -> int -> int (* exponent -> base -> result *)
+ val gcd: int -> int -> int
+ val gcds: int list -> int
+ val lcm: int -> int -> int
+ val lcms: int list -> int
+end;
+
+structure Integer : INTEGER =
+struct
+
+fun sign x = int_ord (x, 0);
+
+fun sum xs = fold (curry op +) xs 0;
+
+fun div_mod x y = IntInf.divMod (x, y);
+
+fun square x = x * x;
+
+fun pow k l =
+ let
+ fun pw 0 _ = 1
+ | pw 1 l = l
+ | pw k l =
+ let
+ val (k', r) = div_mod k 2;
+ val l' = pw k' (l * l);
+ in if r = 0 then l' else l' * l end;
+ in
+ if k < 0
+ then error "pow: negative exponent"
+ else pw k l
+ end;
+
+fun gcd x y =
+ let
+ fun gxd x y = if y = 0 then x else gxd y (x mod y)
+ in if x < y then gxd y x else gxd x y end;
+
+fun gcds xs = fold gcd xs 0;
+
+fun lcm x y = (x * y) div (gcd x y);
+fun lcms xs = fold lcm xs 1;
+
+end;
+
--- a/src/Pure/IsaMakefile Tue Sep 18 17:53:37 2007 +0200
+++ b/src/Pure/IsaMakefile Tue Sep 18 18:05:34 2007 +0200
@@ -26,7 +26,7 @@
$(OUT)/Pure$(ML_SUFFIX): \
CPure.thy General/ROOT.ML General/alist.ML General/balanced_tree.ML \
General/basics.ML General/buffer.ML General/file.ML General/graph.ML \
- General/heap.ML General/history.ML General/markup.ML \
+ General/heap.ML General/history.ML General/integer.ML General/markup.ML \
General/name_space.ML General/ord_list.ML General/output.ML \
General/path.ML General/position.ML General/pretty.ML \
General/print_mode.ML General/scan.ML General/secure.ML General/seq.ML \
@@ -51,10 +51,10 @@
ML-Systems/polyml-5.1.ML ML-Systems/polyml-interrupt-timeout.ML \
ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML \
ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/proper_int.ML \
- ML-Systems/smlnj.ML ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
- Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
- Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
- ProofGeneral/parsing.ML ProofGeneral/pgip.ML \
+ ML-Systems/smlnj.ML ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML \
+ ML/ml_syntax.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \
+ Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
+ ProofGeneral/ROOT.ML ProofGeneral/parsing.ML ProofGeneral/pgip.ML \
ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \
ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
--- a/src/Tools/integer.ML Tue Sep 18 17:53:37 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-(* Title: Tools/integer.ML
- ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-
-Unbounded integers.
-*)
-
-signature INTEGER =
-sig
- val sign: int -> order
- val sum: int list -> int
- val div_mod: int -> int -> int * int
- val square: int -> int
- val pow: int -> int -> int (* exponent -> base -> result *)
- val gcd: int -> int -> int
- val gcds: int list -> int
- val lcm: int -> int -> int
- val lcms: int list -> int
-end;
-
-structure Integer : INTEGER =
-struct
-
-fun sign x = int_ord (x, 0);
-
-fun sum xs = fold (curry op +) xs 0;
-
-fun div_mod x y = IntInf.divMod (x, y);
-
-fun square x = x * x;
-
-fun pow k l =
- let
- fun pw 0 _ = 1
- | pw 1 l = l
- | pw k l =
- let
- val (k', r) = div_mod k 2;
- val l' = pw k' (l * l);
- in if r = 0 then l' else l' * l end;
- in
- if k < 0
- then error "pow: negative exponent"
- else pw k l
- end;
-
-fun gcd x y =
- let
- fun gxd x y = if y = 0 then x else gxd y (x mod y)
- in if x < y then gxd y x else gxd x y end;
-
-fun gcds xs = fold gcd xs 0;
-
-fun lcm x y = (x * y) div (gcd x y);
-fun lcms xs = fold lcm xs 1;
-
-end;
-