[isabelle-dev] Integers in Poly/ML
Makarius
makarius at sketis.net
Wed Nov 2 16:29:38 CET 2016
On 02/11/16 15:58, Lawrence Paulson wrote:
> I have to say, I’m absolutely mystified by the response to my suggestion.
Why? I did not reject the idea, but only put it into the context of
Isabelle. MetiTarski is a small research experiment, but Isabelle a huge
and complex software product, with very high standards.
> We have spent a lot of time discussing problems caused by the cost of
> regression testing, and now we have the possibility of reducing that by 30%.
Where is the empirical measurement for Isabelle? Without that it is just
speculation.
A quick test with x86_64 and int = FixedInt might actually give some
ideas about the order of potential performance improvement. Do you want
to make one?
In the Jenkins project, there were also proposals to move to 64bit by
default, and thus lose a lot of performance. (The general waste of
resources of Jenkins is caused by high-level policies, though, and
theses were not openly discussed so far.)
> As to changes in behaviour that could be caused by overflows, I checked:
> exception Overflow is explicitly caught in only two places throughout
> the sources, both in HOL decision procedures (and therefore well outside
> the kernel) while the wildcard exception is caught in three places in
> Pure.
I routinely check these things before each release. Catch-all patterns
are more frequent than that, but they are OK.
I don't think that such a change would cause wrong results, but just
unexpected failure, and that is already bad enough in everyday use.
> No exception handlers had to be added when I converted MetiTarski
> to use fixed integers. An uncaught exception doesn’t prove anything, of
> course.
BTW, you have a lot of catch-all exception handlers in MetiTarski. The
Isabelle/ML IDE shows that -- my changeset from last summer is attached
again.
Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1464704221 -7200
# Tue May 31 16:17:01 2016 +0200
# Node ID e517f280847f40ff7b3a104c4c0f46bca815cc54
# Parent b11e8139b880bde17d291e1d35c3a3577185a82f
basic setup for Isabelle/SML IDE;
diff -r b11e8139b880 -r e517f280847f src/+ld.sml
--- a/src/+ld.sml Mon Mar 30 15:28:39 2015 +0100
+++ b/src/+ld.sml Tue May 31 16:17:01 2016 +0200
@@ -66,7 +66,12 @@
use"Tptp.sig"; use"Tptp.sml";
use"SMTLIB.sig"; use"SMTLIB.sml";
-use"Syntax/load.sml";
+use"Syntax/lib/base.sig";
+use"Syntax/lib/join.sml";
+use"Syntax/lib/lrtable.sml";
+use"Syntax/lib/stream.sml";
+use"Syntax/lib/parser2.sml";
+use"Syntax/load0.sml";
use"Options.sig"; use"Options.sml";
use"metis.sml";
diff -r b11e8139b880 -r e517f280847f src/ROOT.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ROOT.ML Tue May 31 16:17:01 2016 +0200
@@ -0,0 +1,75 @@
+SML_file "Portable.sig";
+SML_file "Random.sig"; SML_file "Random.sml";
+SML_file "PortablePolyml.sml";
+SML_file "Polyhash.sig"; SML_file "Polyhash.sml";
+SML_file "Useful.sig"; SML_file "Useful.sml";
+SML_file "rat.sml"; (*John Harrison's code*)
+SML_file "Lazy.sig"; SML_file "Lazy.sml";
+SML_file "Map.sig"; SML_file "Map.sml";
+SML_file "Set.sig"; SML_file "Set.sml";
+SML_file "Ordered.sig"; SML_file "Ordered.sml";
+SML_file "KeyMap.sig"; SML_file "KeyMap.sml";
+SML_file "ElementSet.sig"; SML_file "ElementSet.sml";
+SML_file "Sharing.sig"; SML_file "Sharing.sml";
+SML_file "Stream.sig"; SML_file "Stream.sml";
+SML_file "Heap.sig"; SML_file "Heap.sml";
+SML_file "Print.sig"; SML_file "Print.sml";
+SML_file "Parse.sig"; SML_file "Parse.sml";
+SML_file "Name.sig"; SML_file "Name.sml";
+SML_file "NameArity.sig"; SML_file "NameArity.sml";
+SML_file "Term.sig"; SML_file "Term.sml";
+SML_file "Subst.sig"; SML_file "Subst.sml";
+SML_file "Atom.sig"; SML_file "Atom.sml";
+SML_file "Formula.sig"; SML_file "Formula.sml";
+SML_file "Literal.sig"; SML_file "Literal.sml";
+SML_file "KnuthBendixOrder.sig"; SML_file "KnuthBendixOrder.sml";
+SML_file "Poly.sig"; SML_file "Poly.sml";
+SML_file "RCF/Common.sig"; SML_file "RCF/Common.sml";
+SML_file "RCF/Algebra.sig"; SML_file "RCF/Algebra.sml";
+SML_file "RCF/Groebner.sig"; SML_file "RCF/Groebner.sml";
+SML_file "RCF/SMT.sig"; SML_file "RCF/SMT.sml";
+SML_file "RCF/IntvlsFP.sig"; SML_file "RCF/IntvlsFP.sml";
+SML_file "RCF/Resultant.sig"; SML_file "RCF/Resultant.sml";
+SML_file "RCF/Sturm.sig"; SML_file "RCF/Sturm.sml";
+SML_file "RCF/RealAlg.sig"; SML_file "RCF/RealAlg.sml";
+SML_file "RCF/MTAlgebra.sig"; SML_file "RCF/MTAlgebra.sml";
+SML_file "RCF/CADProjO.sig"; SML_file "RCF/CADProjO.sml";
+SML_file "RCF/Mathematica.sig"; SML_file "RCF/Mathematica.sml";
+SML_file "RCF/Qepcad.sig"; SML_file "RCF/Qepcad.sml";
+SML_file "RCF/Nullsatz.sig"; SML_file "RCF/Nullsatz.sml";
+SML_file "RCF/CertRCFk.sig"; SML_file "RCF/CertRCFk.sml";
+SML_file "RCF/CertRCFp.sig"; SML_file "RCF/CertRCFp.sml";
+SML_file "RCF/RCF.sig"; SML_file "RCF/RCF.sml";
+SML_file "Thm.sig"; SML_file "Thm.sml";
+SML_file "Proof.sig"; SML_file "Proof.sml";
+SML_file "Rule.sig"; SML_file "Rule.sml";
+SML_file "Normalize.sig"; SML_file "Normalize.sml";
+SML_file "Model.sig"; SML_file "Model.sml";
+SML_file "Problem.sig"; SML_file "Problem.sml";
+SML_file "TermNet.sig"; SML_file "TermNet.sml";
+SML_file "AtomNet.sig"; SML_file "AtomNet.sml";
+SML_file "LiteralNet.sig"; SML_file "LiteralNet.sml";
+SML_file "Subsume.sig"; SML_file "Subsume.sml";
+SML_file "Rewrite.sig"; SML_file "Rewrite.sml";
+SML_file "Units.sig"; SML_file "Units.sml";
+SML_file "Clause.sig"; SML_file "Clause.sml";
+SML_file "Active.sig"; SML_file "Active.sml";
+SML_file "Waiting.sig"; SML_file "Waiting.sml";
+SML_file "SplitStack.sig"; SML_file "SplitStack.sml";
+SML_file "Resolution.sig"; SML_file "Resolution.sml";
+SML_file "Tptp.sig"; SML_file "Tptp.sml";
+SML_file "SMTLIB.sig"; SML_file "SMTLIB.sml";
+
+SML_file "Syntax/lib/base.sig";
+SML_file "Syntax/lib/join.sml";
+SML_file "Syntax/lib/lrtable.sml";
+SML_file "Syntax/lib/stream.sml";
+SML_file "Syntax/lib/parser2.sml";
+SML_file "Syntax/load0.sml";
+SML_file "Syntax/mt.grm.sig";
+SML_file "Syntax/mt.grm.sml";
+SML_file "Syntax/mt.lex.sml";
+SML_file "Syntax/load.sml";
+
+SML_file "Options.sig"; SML_file "Options.sml";
+SML_file "metis.sml";
diff -r b11e8139b880 -r e517f280847f src/Syntax/load.sml
--- a/src/Syntax/load.sml Mon Mar 30 15:28:39 2015 +0100
+++ b/src/Syntax/load.sml Tue May 31 16:17:01 2016 +0200
@@ -1,40 +1,3 @@
-use"Syntax/lib/base.sig";
-use"Syntax/lib/join.sml";
-use"Syntax/lib/lrtable.sml";
-use"Syntax/lib/stream.sml";
-use"Syntax/lib/parser2.sml";
-
-fun goodAtom (Term.Fn (s,_)) = size s > 0 andalso Char.isLower (String.sub (s,0))
- | goodAtom _ = false;
-
-fun fmOfAtom t =
- Formula.Atom (if goodAtom t then Term.destFn t else ("Bad_Formula",[t]));
-
-fun termOfDecimal s =
- let val mant::rest = String.tokens (fn c => c = #"e" orelse c = #"E") s (*remove exponent*)
- val e = Option.valOf (IntInf.fromString (hd rest)) handle Empty => 0
- val tenexp = Rat.exp (Rat.rat_of_intinf 10, Rat.rat_of_intinf e)
- val [uns] = String.tokens (fn c => c = #"+" orelse c = #"-") mant (*remove sign*)
- val a::ss = String.fields (fn c => c = #".") uns (*integer part*)
- val b = hd ss handle Empty => ""
- val n = String.size b
- val i = (if a="" then 0 else Option.valOf (IntInf.fromString a))
- val j = (if b="" then 0 else Option.valOf (IntInf.fromString b))
- val tenn = Useful.exp IntInf.* 10 n 1
- val r = Rat.mult (tenexp, Rat.rat_of_quotient (i*tenn+j, tenn))
- in Term.Rat (if String.isPrefix "-" s then Rat.neg r else r) end
- handle _ => (print ("Unable to translate numeric constant " ^ s ^ "\n");
- raise Parse.NoParse);
-
-fun litOfInterval (x, (il,lower,iu,upper)) =
- (true, ("interval",
- [Term.Rat (Rat.rat_of_int il), lower,
- Term.Rat (Rat.rat_of_int iu), upper, x]));
-
-use"Syntax/mt.grm.sig";
-use"Syntax/mt.grm.sml";
-use"Syntax/mt.lex.sml";
-
structure MTLrVals : MT_LRVALS =
MTLrValsFun(structure Token = LrParser.Token);
diff -r b11e8139b880 -r e517f280847f src/Syntax/load0.sml
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Syntax/load0.sml Tue May 31 16:17:01 2016 +0200
@@ -0,0 +1,26 @@
+fun goodAtom (Term.Fn (s,_)) = size s > 0 andalso Char.isLower (String.sub (s,0))
+ | goodAtom _ = false;
+
+fun fmOfAtom t =
+ Formula.Atom (if goodAtom t then Term.destFn t else ("Bad_Formula",[t]));
+
+fun termOfDecimal s =
+ let val mant::rest = String.tokens (fn c => c = #"e" orelse c = #"E") s (*remove exponent*)
+ val e = Option.valOf (IntInf.fromString (hd rest)) handle Empty => 0
+ val tenexp = Rat.exp (Rat.rat_of_intinf 10, Rat.rat_of_intinf e)
+ val [uns] = String.tokens (fn c => c = #"+" orelse c = #"-") mant (*remove sign*)
+ val a::ss = String.fields (fn c => c = #".") uns (*integer part*)
+ val b = hd ss handle Empty => ""
+ val n = String.size b
+ val i = (if a="" then 0 else Option.valOf (IntInf.fromString a))
+ val j = (if b="" then 0 else Option.valOf (IntInf.fromString b))
+ val tenn = Useful.exp IntInf.* 10 n 1
+ val r = Rat.mult (tenexp, Rat.rat_of_quotient (i*tenn+j, tenn))
+ in Term.Rat (if String.isPrefix "-" s then Rat.neg r else r) end
+ handle _ => (print ("Unable to translate numeric constant " ^ s ^ "\n");
+ raise Parse.NoParse);
+
+fun litOfInterval (x, (il,lower,iu,upper)) =
+ (true, ("interval",
+ [Term.Rat (Rat.rat_of_int il), lower,
+ Term.Rat (Rat.rat_of_int iu), upper, x]));
More information about the isabelle-dev
mailing list