# HG changeset patch # User wenzelm # Date 1186151299 -7200 # Node ID 0683a2fc40418118064285eccd1ebc8d8ed42e49 # Parent eac44d0fe228cb703cd9fb312c55a7289bcf61ac moved Admin/proper_int.ML to Pure/ML-Systems/proper_int.ML; diff -r eac44d0fe228 -r 0683a2fc4041 Admin/proper_int.ML --- 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; diff -r eac44d0fe228 -r 0683a2fc4041 src/Pure/IsaMakefile --- 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 diff -r eac44d0fe228 -r 0683a2fc4041 src/Pure/ML-Systems/proper_int.ML --- /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;