--- a/Admin/proper_int.ML Fri Aug 03 16:28:18 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
-(* Title: Pure/ML-Systems/proper_int.ML
- ID: $Id$
- Author: Makarius
-
-SML basis with type int representing proper integers, not machine
-words.
-*)
-
-val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
-val dest_int = IntInf.toInt: IntInf.int -> Int.int;
-
-
-(* Int *)
-
-structure OrigInt = Int;
-structure OrigIntInf = IntInf;
-type int = IntInf.int;
-
-structure IntInf =
-struct
- open IntInf;
- fun fromInt (a: int) = a;
- fun toInt (a: int) = a;
- val log2 = mk_int o IntInf.log2;
- val sign = mk_int o IntInf.sign;
-end;
-
-structure Int = IntInf;
-
-
-(* List *)
-
-structure List =
-struct
- open List;
- fun length a = mk_int (List.length a);
- fun nth (a, b) = List.nth (a, dest_int b);
- fun take (a, b) = List.take (a, dest_int b);
- fun drop (a, b) = List.drop (a, dest_int b);
- fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
-end;
-
-val length = List.length;
-
-
-(* Array *)
-
-structure Array =
-struct
- open Array;
- val maxLen = mk_int Array.maxLen;
- fun array (a, b) = Array.array (dest_int a, b);
- fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
- fun length a = mk_int (Array.length a);
- fun sub (a, b) = Array.sub (a, dest_int b);
- fun update (a, b, c) = Array.update (a, dest_int b, c);
- fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
- fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
- fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
- fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
- fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun findi a b =
- (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
- NONE => NONE
- | SOME (c, d) => SOME (mk_int c, d));
-end;
-
-
-(* Vector *)
-
-structure Vector =
-struct
- open Vector;
- val maxLen = mk_int Vector.maxLen;
- fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
- fun length a = mk_int (Vector.length a);
- fun sub (a, b) = Vector.sub (a, dest_int b);
- fun update (a, b, c) = Vector.update (a, dest_int b, c);
- fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
- fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
- fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
- fun findi a b =
- (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
- NONE => NONE
- | SOME (c, d) => SOME (mk_int c, d));
-end;
-
-
-(* Char *)
-
-structure Char =
-struct
- open Char;
- val maxOrd = mk_int Char.maxOrd;
- val chr = Char.chr o dest_int;
- val ord = mk_int o Char.ord;
-end;
-
-val chr = Char.chr;
-val ord = Char.ord;
-
-
-(* String *)
-
-structure String =
-struct
- open String;
- val maxSize = mk_int String.maxSize;
- val size = mk_int o String.size;
- fun sub (a, b) = String.sub (a, dest_int b);
- fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
- fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
-end;
-
-val size = String.size;
-val substring = String.substring;
-
-
-(* Substring *)
-
-structure Substring =
-struct
- open Substring;
- fun sub (a, b) = Substring.sub (a, dest_int b);
- val size = mk_int o Substring.size;
- fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
- fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
- fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
- fun triml a b = Substring.triml (dest_int a) b;
- fun trimr a b = Substring.trimr (dest_int a) b;
- fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
- fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
-end;
-
-
-(* Word *)
-
-structure Word =
-struct
- open Word;
- val wordSize = mk_int Word.wordSize;
- val toInt = mk_int o Word.toInt;
- val toIntX = mk_int o Word.toIntX;
- val fromInt = Word.fromInt o dest_int;
-end;
-
-
-(* Real *)
-
-structure Real =
-struct
- open Real;
- val radix = mk_int Real.radix;
- val precision = mk_int Real.precision;
- fun sign a = mk_int (Real.sign a);
- fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
- fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
- val ceil = mk_int o Real.ceil;
- val floor = mk_int o Real.floor;
- val real = Real.fromInt o dest_int;
- val round = mk_int o Real.round;
- val trunc = mk_int o Real.trunc;
- fun toInt a b = mk_int (Real.toInt a b);
- fun fromInt a = Real.fromInt (dest_int a);
-end;
-
-val ceil = Real.ceil;
-val floor = Real.floor;
-val real = Real.real;
-val round = Real.round;
-val trunc = Real.trunc;
-
-
-(* TextIO *)
-
-structure TextIO =
-struct
- open TextIO;
- fun inputN (a, b) = TextIO.inputN (a, dest_int b);
- fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
-end;
-
-
-(* Time *)
-
-structure Time =
-struct
- open Time;
- fun fmt a b = Time.fmt (dest_int a) b;
-end;
--- a/src/Pure/IsaMakefile Fri Aug 03 16:28:18 2007 +0200
+++ b/src/Pure/IsaMakefile Fri Aug 03 16:28:19 2007 +0200
@@ -45,31 +45,31 @@
ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-5.0.ML 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/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \
- Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy \
- ROOT.ML ProofGeneral/parsing.ML ProofGeneral/pgip_input.ML \
- ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
- ProofGeneral/pgip.ML ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
- ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
- ProofGeneral/preferences.ML ProofGeneral/proof_general_pgip.ML \
- ProofGeneral/proof_general_emacs.ML ProofGeneral/ROOT.ML Syntax/ast.ML \
- Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \
- Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML \
- Thy/html.ML Thy/latex.ML Thy/ml_context.ML Thy/present.ML Thy/term_style.ML \
- Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_edit.ML Thy/thy_header.ML \
- Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML Tools/ROOT.ML \
- Tools/class_package.ML Tools/codegen_consts.ML Tools/codegen_data.ML \
- Tools/codegen_func.ML Tools/codegen_funcgr.ML Tools/codegen_names.ML \
- Tools/codegen_package.ML Tools/codegen_serializer.ML Tools/codegen_thingol.ML \
- Tools/invoke.ML Tools/named_thms.ML Tools/nbe.ML Tools/nbe_codegen.ML \
- Tools/nbe_eval.ML Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML \
- codegen.ML compress.ML config.ML conjunction.ML consts.ML context.ML \
- context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML \
- fact_index.ML goal.ML library.ML logic.ML meta_simplifier.ML \
- more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML \
- pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \
- tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \
- type_infer.ML unify.ML variable.ML
+ ML-Systems/proper_int.ML ML-Systems/smlnj.ML Proof/extraction.ML \
+ Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML Proof/proofchecker.ML \
+ Proof/reconstruct.ML Pure.thy ROOT.ML ProofGeneral/parsing.ML \
+ ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
+ ProofGeneral/pgip_markup.ML ProofGeneral/pgip.ML ProofGeneral/pgip_output.ML \
+ ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
+ ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \
+ ProofGeneral/proof_general_pgip.ML ProofGeneral/proof_general_emacs.ML \
+ ProofGeneral/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML \
+ Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
+ Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML Thy/latex.ML \
+ Thy/ml_context.ML Thy/present.ML Thy/term_style.ML Thy/thm_database.ML \
+ Thy/thm_deps.ML Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML \
+ Thy/thy_load.ML Thy/thy_output.ML Tools/ROOT.ML Tools/class_package.ML \
+ Tools/codegen_consts.ML Tools/codegen_data.ML Tools/codegen_func.ML \
+ Tools/codegen_funcgr.ML Tools/codegen_names.ML Tools/codegen_package.ML \
+ Tools/codegen_serializer.ML Tools/codegen_thingol.ML Tools/invoke.ML \
+ Tools/named_thms.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML \
+ Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML \
+ compress.ML config.ML conjunction.ML consts.ML context.ML context_position.ML \
+ conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML library.ML \
+ logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \
+ old_goals.ML pattern.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \
+ sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \
+ term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
@./mk
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/proper_int.ML Fri Aug 03 16:28:19 2007 +0200
@@ -0,0 +1,192 @@
+(* Title: Pure/ML-Systems/proper_int.ML
+ ID: $Id$
+ Author: Makarius
+
+SML basis with type int representing proper integers, not machine
+words.
+*)
+
+val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
+val dest_int = IntInf.toInt: IntInf.int -> Int.int;
+
+
+(* Int *)
+
+structure OrigInt = Int;
+structure OrigIntInf = IntInf;
+type int = IntInf.int;
+
+structure IntInf =
+struct
+ open IntInf;
+ fun fromInt (a: int) = a;
+ fun toInt (a: int) = a;
+ val log2 = mk_int o IntInf.log2;
+ val sign = mk_int o IntInf.sign;
+end;
+
+structure Int = IntInf;
+
+
+(* List *)
+
+structure List =
+struct
+ open List;
+ fun length a = mk_int (List.length a);
+ fun nth (a, b) = List.nth (a, dest_int b);
+ fun take (a, b) = List.take (a, dest_int b);
+ fun drop (a, b) = List.drop (a, dest_int b);
+ fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
+end;
+
+val length = List.length;
+
+
+(* Array *)
+
+structure Array =
+struct
+ open Array;
+ val maxLen = mk_int Array.maxLen;
+ fun array (a, b) = Array.array (dest_int a, b);
+ fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
+ fun length a = mk_int (Array.length a);
+ fun sub (a, b) = Array.sub (a, dest_int b);
+ fun update (a, b, c) = Array.update (a, dest_int b, c);
+ fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
+ fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
+ fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
+ fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
+ fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
+ fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
+ fun findi a b =
+ (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
+ NONE => NONE
+ | SOME (c, d) => SOME (mk_int c, d));
+end;
+
+
+(* Vector *)
+
+structure Vector =
+struct
+ open Vector;
+ val maxLen = mk_int Vector.maxLen;
+ fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
+ fun length a = mk_int (Vector.length a);
+ fun sub (a, b) = Vector.sub (a, dest_int b);
+ fun update (a, b, c) = Vector.update (a, dest_int b, c);
+ fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
+ fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
+ fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
+ fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
+ fun findi a b =
+ (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
+ NONE => NONE
+ | SOME (c, d) => SOME (mk_int c, d));
+end;
+
+
+(* Char *)
+
+structure Char =
+struct
+ open Char;
+ val maxOrd = mk_int Char.maxOrd;
+ val chr = Char.chr o dest_int;
+ val ord = mk_int o Char.ord;
+end;
+
+val chr = Char.chr;
+val ord = Char.ord;
+
+
+(* String *)
+
+structure String =
+struct
+ open String;
+ val maxSize = mk_int String.maxSize;
+ val size = mk_int o String.size;
+ fun sub (a, b) = String.sub (a, dest_int b);
+ fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
+ fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
+end;
+
+val size = String.size;
+val substring = String.substring;
+
+
+(* Substring *)
+
+structure Substring =
+struct
+ open Substring;
+ fun sub (a, b) = Substring.sub (a, dest_int b);
+ val size = mk_int o Substring.size;
+ fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
+ fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
+ fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
+ fun triml a b = Substring.triml (dest_int a) b;
+ fun trimr a b = Substring.trimr (dest_int a) b;
+ fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
+ fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
+end;
+
+
+(* Word *)
+
+structure Word =
+struct
+ open Word;
+ val wordSize = mk_int Word.wordSize;
+ val toInt = mk_int o Word.toInt;
+ val toIntX = mk_int o Word.toIntX;
+ val fromInt = Word.fromInt o dest_int;
+end;
+
+
+(* Real *)
+
+structure Real =
+struct
+ open Real;
+ val radix = mk_int Real.radix;
+ val precision = mk_int Real.precision;
+ fun sign a = mk_int (Real.sign a);
+ fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
+ fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
+ val ceil = mk_int o Real.ceil;
+ val floor = mk_int o Real.floor;
+ val real = Real.fromInt o dest_int;
+ val round = mk_int o Real.round;
+ val trunc = mk_int o Real.trunc;
+ fun toInt a b = mk_int (Real.toInt a b);
+ fun fromInt a = Real.fromInt (dest_int a);
+end;
+
+val ceil = Real.ceil;
+val floor = Real.floor;
+val real = Real.real;
+val round = Real.round;
+val trunc = Real.trunc;
+
+
+(* TextIO *)
+
+structure TextIO =
+struct
+ open TextIO;
+ fun inputN (a, b) = TextIO.inputN (a, dest_int b);
+ fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
+end;
+
+
+(* Time *)
+
+structure Time =
+struct
+ open Time;
+ fun fmt a b = Time.fmt (dest_int a) b;
+end;