[isabelle-dev] NEWS: Isabelle support for Standard ML
Makarius
makarius at sketis.net
Tue Mar 25 21:28:45 CET 2014
* Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
Poly/ML, without the add-ons of Isabelle/ML. See also
~/src/Tools/SML/Examples.thy for some basic examples.
This refers to Isabelle/20cf88cd3188. It is one of the things that have
been in principle possible all the time, but required a bit longer to get
through the pipeline from the Ural.
The main changeset 600f432ab556 illustrates once again that ML inside
Isabelle is managed by Isabelle. We are not sitting on the bare metal
like the first generation after LCF did, so it is easy to determine
strictly which parts of the ML environment are accessible to newly
compiled sources.
Apart from the small examples above, which are also offered in the
Documentation panel of Isabelle/jEdit, I have made a quick test with
MetiTarski. The included changeset is the result of spending 5min with
the sources: it all works fine so far.
Hopefully nobody will ever use vi or Emacs for SML again ...
Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1395761675 -3600
# Tue Mar 25 16:34:35 2014 +0100
# Node ID 5d4869debe334911854a8d73a3ec54e07ee37243
# Parent 4afb77a153d01c28edddd6a4966b834943f23f99
basic setup for Isabelle/SML IDE (note that "RCF/SMT.sig" and "RCF/SMT.sml" were used twice);
diff -r 4afb77a153d0 -r 5d4869debe33 src/ALL.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ALL.thy Tue Mar 25 16:34:35 2014 +0100
@@ -0,0 +1,83 @@
+theory ALL
+imports Pure
+begin
+
+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/Calibrate.sig" SML_file "RCF/Calibrate.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"
+
+end
+
diff -r 4afb77a153d0 -r 5d4869debe33 src/Syntax/load.sml
--- a/src/Syntax/load.sml Fri Mar 21 15:44:34 2014 +0000
+++ b/src/Syntax/load.sml Tue Mar 25 16:34:35 2014 +0100
@@ -1,39 +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 4afb77a153d0 -r 5d4869debe33 src/Syntax/load0.sml
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Syntax/load0.sml Tue Mar 25 16:34:35 2014 +0100
@@ -0,0 +1,27 @@
+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