copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
--- a/src/Tools/Metis/Makefile Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/Makefile Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
###############################################################################
# METIS MAKEFILE
-# Copyright (c) 2001 Joe Hurd, distributed under the GNU GPL version 2
+# Copyright (c) 2001 Joe Hurd, distributed under the MIT license
###############################################################################
.SUFFIXES:
--- a/src/Tools/Metis/scripts/mlpp Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/scripts/mlpp Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
#!/usr/bin/perl
-# Copyright (c) 2006 Joe Hurd, All Rights Reserved
+# Copyright (c) 2006 Joe Hurd, distributed under the MIT license
use strict;
use warnings;
@@ -78,6 +78,8 @@
$text =~ s/Array\.modifyi/Array_modifyi/g;
$text =~ s/OS\.Process\.isSuccess/OS_Process_isSuccess/g;
$text =~ s/PP\.ppstream/ppstream/g;
+ $text =~ s/String\.concatWith/String_concatWith/g;
+ $text =~ s/String\.isSubstring/String_isSubstring/g;
$text =~ s/String\.isSuffix/String_isSuffix/g;
$text =~ s/Substring\.full/Substring_full/g;
$text =~ s/TextIO\.inputLine/TextIO_inputLine/g;
--- a/src/Tools/Metis/src/Active.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Active.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Active =
--- a/src/Tools/Metis/src/Active.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Active.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE ACTIVE SET OF CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Active :> Active =
@@ -25,7 +25,7 @@
| NONE => rw
end
in
- foldl add (Rewrite.new (KnuthBendixOrder.compare ordering))
+ List.foldl add (Rewrite.new (KnuthBendixOrder.compare ordering))
end;
fun allFactors red =
@@ -293,8 +293,8 @@
end
val cls = clauses active
- val (cls,_) = foldl remove ([], Subsume.new ()) cls
- val (cls,subs) = foldl remove ([], Subsume.new ()) cls
+ val (cls,_) = List.foldl remove ([], Subsume.new ()) cls
+ val (cls,subs) = List.foldl remove ([], Subsume.new ()) cls
(*MetisDebug
val Active {parameters,...} = active
@@ -321,7 +321,7 @@
local
fun ppField f ppA a =
Print.blockProgram Print.Inconsistent 2
- [Print.addString (f ^ " ="),
+ [Print.ppString (f ^ " ="),
Print.addBreak 1,
ppA a];
@@ -342,21 +342,21 @@
in
fun pp (Active {clauses,rewrite,subterms,...}) =
Print.blockProgram Print.Inconsistent 2
- [Print.addString "Active",
+ [Print.ppString "Active",
Print.addBreak 1,
Print.blockProgram Print.Inconsistent 1
- [Print.addString "{",
+ [Print.ppString "{",
ppClauses clauses,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppRewrite rewrite,
(*MetisTrace5
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppSubterms subterms,
*)
Print.skip],
- Print.addString "}"];
+ Print.ppString "}"];
end;
*)
@@ -474,7 +474,7 @@
fun add ((lit,ort,tm),equations) =
TermNet.insert equations (tm,(cl,lit,ort,tm))
in
- foldl add equations (Clause.largestEquations cl)
+ List.foldl add equations (Clause.largestEquations cl)
end;
fun addSubterms subterms cl =
@@ -482,7 +482,7 @@
fun add ((lit,path,tm),subterms) =
TermNet.insert subterms (tm,(cl,lit,path,tm))
in
- foldl add subterms (Clause.largestSubterms cl)
+ List.foldl add subterms (Clause.largestSubterms cl)
end;
fun addAllSubterms allSubterms cl =
@@ -490,7 +490,7 @@
fun add ((_,_,tm),allSubterms) =
TermNet.insert allSubterms (tm,(cl,tm))
in
- foldl add allSubterms (Clause.allSubterms cl)
+ List.foldl add allSubterms (Clause.allSubterms cl)
end;
fun addClause active cl =
@@ -541,7 +541,8 @@
*)
in
if Atom.isEq atm then acc
- else foldl resolve acc (LiteralNet.unify literals (Literal.negate lit))
+ else
+ List.foldl resolve acc (LiteralNet.unify literals (Literal.negate lit))
end;
fun deduceParamodulationWith subterms cl ((lit,ort,tm),acc) =
@@ -551,7 +552,7 @@
SOME cl' => cl' :: acc
| NONE => acc
in
- foldl para acc (TermNet.unify subterms tm)
+ List.foldl para acc (TermNet.unify subterms tm)
end;
fun deduceParamodulationInto equations cl ((lit,path,tm),acc) =
@@ -561,7 +562,7 @@
SOME cl' => cl' :: acc
| NONE => acc
in
- foldl para acc (TermNet.unify equations tm)
+ List.foldl para acc (TermNet.unify equations tm)
end;
fun deduce active cl =
@@ -587,8 +588,8 @@
val acc = []
val acc = LiteralSet.foldl (deduceResolution literals cl) acc lits
- val acc = foldl (deduceParamodulationWith subterms cl) acc eqns
- val acc = foldl (deduceParamodulationInto equations cl) acc subtms
+ val acc = List.foldl (deduceParamodulationWith subterms cl) acc eqns
+ val acc = List.foldl (deduceParamodulationInto equations cl) acc subtms
val acc = rev acc
(*MetisTrace5
@@ -834,7 +835,7 @@
let
val cls = sort_utilitywise (cl :: Clause.factor cl)
in
- foldl factor_add active_subsume_acc cls
+ List.foldl factor_add active_subsume_acc cls
end;
fun factor' active acc [] = (active, rev acc)
@@ -842,7 +843,7 @@
let
val cls = sort_utilitywise cls
val subsume = getSubsume active
- val (active,_,acc) = foldl factor1 (active,subsume,acc) cls
+ val (active,_,acc) = List.foldl factor1 (active,subsume,acc) cls
val (active,cls) = extract_rewritables active
in
factor' active acc cls
--- a/src/Tools/Metis/src/Atom.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Atom.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Atom =
--- a/src/Tools/Metis/src/Atom.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Atom.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Atom :> Atom =
@@ -34,14 +34,14 @@
let
fun f (tm,acc) = NameAritySet.union (Term.functions tm) acc
in
- fn atm => foldl f NameAritySet.empty (arguments atm)
+ fn atm => List.foldl f NameAritySet.empty (arguments atm)
end;
val functionNames =
let
fun f (tm,acc) = NameSet.union (Term.functionNames tm) acc
in
- fn atm => foldl f NameSet.empty (arguments atm)
+ fn atm => List.foldl f NameSet.empty (arguments atm)
end;
(* Binary relations *)
@@ -58,7 +58,8 @@
(* The size of an atom in symbols. *)
(* ------------------------------------------------------------------------- *)
-fun symbols atm = foldl (fn (tm,z) => Term.symbols tm + z) 1 (arguments atm);
+fun symbols atm =
+ List.foldl (fn (tm,z) => Term.symbols tm + z) 1 (arguments atm);
(* ------------------------------------------------------------------------- *)
(* A total comparison function for atoms. *)
@@ -85,7 +86,7 @@
let
fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
in
- foldl f [] (enumerate tms)
+ List.foldl f [] (enumerate tms)
end;
fun replace _ ([],_) = raise Bug "Atom.replace: empty path"
@@ -120,7 +121,7 @@
let
fun f (tm,acc) = NameSet.union (Term.freeVars tm) acc
in
- fn atm => foldl f NameSet.empty (arguments atm)
+ fn atm => List.foldl f NameSet.empty (arguments atm)
end;
(* ------------------------------------------------------------------------- *)
@@ -146,7 +147,7 @@
val _ = (Name.equal p1 p2 andalso length tms1 = length tms2) orelse
raise Error "Atom.match"
in
- foldl matchArg sub (zip tms1 tms2)
+ List.foldl matchArg sub (zip tms1 tms2)
end;
end;
@@ -162,7 +163,7 @@
val _ = (Name.equal p1 p2 andalso length tms1 = length tms2) orelse
raise Error "Atom.unify"
in
- foldl unifyArg sub (zip tms1 tms2)
+ List.foldl unifyArg sub (zip tms1 tms2)
end;
end;
@@ -211,7 +212,7 @@
(* ------------------------------------------------------------------------- *)
fun typedSymbols ((_,tms) : atom) =
- foldl (fn (tm,z) => Term.typedSymbols tm + z) 1 tms;
+ List.foldl (fn (tm,z) => Term.typedSymbols tm + z) 1 tms;
fun nonVarTypedSubterms (_,tms) =
let
@@ -219,10 +220,10 @@
let
fun addTm ((path,tm),acc) = (n :: path, tm) :: acc
in
- foldl addTm acc (Term.nonVarTypedSubterms arg)
+ List.foldl addTm acc (Term.nonVarTypedSubterms arg)
end
in
- foldl addArg [] (enumerate tms)
+ List.foldl addArg [] (enumerate tms)
end;
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/AtomNet.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/AtomNet.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature AtomNet =
--- a/src/Tools/Metis/src/AtomNet.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/AtomNet.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure AtomNet :> AtomNet =
@@ -35,7 +35,7 @@
fun insert net (atm,a) = TermNet.insert net (atomToTerm atm, a);
-fun fromList parm l = foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
+fun fromList parm l = List.foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;
val filter = TermNet.filter;
--- a/src/Tools/Metis/src/Clause.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Clause =
--- a/src/Tools/Metis/src/Clause.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CLAUSE = ID + THEOREM *)
-(* Copyright (c) 2002-2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Clause :> Clause =
@@ -15,10 +15,17 @@
val newId =
let
val r = ref 0
+
+ fun new () =
+ let
+ val ref n = r
+
+ val () = r := n + 1
+ in
+ n
+ end
in
- (* MODIFIED by Jasmin Blanchette *)
- fn () => CRITICAL (fn () =>
- case r of ref n => let val () = r := n + 1 in n end)
+ fn () => Portable.critical new ()
end;
(* ------------------------------------------------------------------------- *)
@@ -62,7 +69,7 @@
val default : parameters =
{ordering = KnuthBendixOrder.default,
- orderLiterals = UnsignedLiteralOrder (* PositiveLiteralOrder *) (* MODIFIED by Jasmin Blanchette *),
+ orderLiterals = UnsignedLiteralOrder,
orderTerms = true};
fun mk info = Clause info
@@ -181,7 +188,7 @@
let
fun addTm ((path,tm),acc) = (lit,path,tm) :: acc
in
- foldl addTm acc (Literal.nonVarTypedSubterms lit)
+ List.foldl addTm acc (Literal.nonVarTypedSubterms lit)
end;
in
fun largestSubterms cl = LiteralSet.foldl addLit [] (largestLiterals cl);
--- a/src/Tools/Metis/src/ElementSet.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/ElementSet.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature ElementSet =
--- a/src/Tools/Metis/src/ElementSet.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/ElementSet.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
functor ElementSet (KM : KeyMap) :> ElementSet
--- a/src/Tools/Metis/src/Formula.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Formula.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Formula =
--- a/src/Tools/Metis/src/Formula.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Formula.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC FORMULAS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Formula :> Formula =
@@ -145,7 +145,7 @@
(* Conjunctions *)
fun listMkConj fms =
- case rev fms of [] => True | fm :: fms => foldl And fm fms;
+ case rev fms of [] => True | fm :: fms => List.foldl And fm fms;
local
fun strip cs (And (p,q)) = strip (p :: cs) q
@@ -168,7 +168,7 @@
(* Disjunctions *)
fun listMkDisj fms =
- case rev fms of [] => False | fm :: fms => foldl Or fm fms;
+ case rev fms of [] => False | fm :: fms => List.foldl Or fm fms;
local
fun strip cs (Or (p,q)) = strip (p :: cs) q
@@ -191,7 +191,7 @@
(* Equivalences *)
fun listMkEquiv fms =
- case rev fms of [] => True | fm :: fms => foldl Iff fm fms;
+ case rev fms of [] => True | fm :: fms => List.foldl Iff fm fms;
local
fun strip cs (Iff (p,q)) = strip (p :: cs) q
--- a/src/Tools/Metis/src/Heap.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Heap.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Heap =
--- a/src/Tools/Metis/src/Heap.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Heap.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Heap :> Heap =
--- a/src/Tools/Metis/src/KeyMap.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/KeyMap.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature KeyMap =
--- a/src/Tools/Metis/src/KeyMap.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/KeyMap.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
@@ -887,38 +887,40 @@
(* ------------------------------------------------------------------------- *)
datatype 'value iterator =
- LR of (key * 'value) * 'value tree * 'value node list
- | RL of (key * 'value) * 'value tree * 'value node list;
+ LeftToRightIterator of
+ (key * 'value) * 'value tree * 'value node list
+ | RightToLeftIterator of
+ (key * 'value) * 'value tree * 'value node list;
-fun fromSpineLR nodes =
+fun fromSpineLeftToRightIterator nodes =
case nodes of
[] => NONE
| Node {key,value,right,...} :: nodes =>
- SOME (LR ((key,value),right,nodes));
+ SOME (LeftToRightIterator ((key,value),right,nodes));
-fun fromSpineRL nodes =
+fun fromSpineRightToLeftIterator nodes =
case nodes of
[] => NONE
| Node {key,value,left,...} :: nodes =>
- SOME (RL ((key,value),left,nodes));
+ SOME (RightToLeftIterator ((key,value),left,nodes));
-fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
+fun addLeftToRightIterator nodes tree = fromSpineLeftToRightIterator (treeLeftSpine nodes tree);
-fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
+fun addRightToLeftIterator nodes tree = fromSpineRightToLeftIterator (treeRightSpine nodes tree);
-fun treeMkIterator tree = addLR [] tree;
+fun treeMkIterator tree = addLeftToRightIterator [] tree;
-fun treeMkRevIterator tree = addRL [] tree;
+fun treeMkRevIterator tree = addRightToLeftIterator [] tree;
fun readIterator iter =
case iter of
- LR (key_value,_,_) => key_value
- | RL (key_value,_,_) => key_value;
+ LeftToRightIterator (key_value,_,_) => key_value
+ | RightToLeftIterator (key_value,_,_) => key_value;
fun advanceIterator iter =
case iter of
- LR (_,tree,nodes) => addLR nodes tree
- | RL (_,tree,nodes) => addRL nodes tree;
+ LeftToRightIterator (_,tree,nodes) => addLeftToRightIterator nodes tree
+ | RightToLeftIterator (_,tree,nodes) => addRightToLeftIterator nodes tree;
fun foldIterator f acc io =
case io of
--- a/src/Tools/Metis/src/KnuthBendixOrder.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE KNUTH-BENDIX TERM ORDERING *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature KnuthBendixOrder =
--- a/src/Tools/Metis/src/KnuthBendixOrder.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* KNUTH-BENDIX TERM ORDERING CONSTRAINTS *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure KnuthBendixOrder :> KnuthBendixOrder =
@@ -99,7 +99,7 @@
val ppWeightList =
let
fun ppCoeff n =
- if n < 0 then Print.sequence (Print.addString "~") (ppCoeff (~n))
+ if n < 0 then Print.sequence (Print.ppString "~") (ppCoeff (~n))
else if n = 1 then Print.skip
else Print.ppInt n
--- a/src/Tools/Metis/src/Lazy.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Lazy.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Lazy =
--- a/src/Tools/Metis/src/Lazy.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Lazy.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Lazy :> Lazy =
--- a/src/Tools/Metis/src/Literal.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Literal.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Literal =
--- a/src/Tools/Metis/src/Literal.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Literal.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Literal :> Literal =
--- a/src/Tools/Metis/src/LiteralNet.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/LiteralNet.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature LiteralNet =
--- a/src/Tools/Metis/src/LiteralNet.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/LiteralNet.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure LiteralNet :> LiteralNet =
@@ -39,7 +39,7 @@
| insert {positive,negative} ((false,atm),a) =
{positive = positive, negative = AtomNet.insert negative (atm,a)};
-fun fromList parm l = foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
+fun fromList parm l = List.foldl (fn (lit_a,n) => insert n lit_a) (new parm) l;
fun filter pred {positive,negative} =
{positive = AtomNet.filter pred positive,
--- a/src/Tools/Metis/src/Map.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Map.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Map =
--- a/src/Tools/Metis/src/Map.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Map.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Map :> Map =
@@ -879,38 +879,40 @@
(* ------------------------------------------------------------------------- *)
datatype ('key,'value) iterator =
- LR of ('key * 'value) * ('key,'value) tree * ('key,'value) node list
- | RL of ('key * 'value) * ('key,'value) tree * ('key,'value) node list;
+ LeftToRightIterator of
+ ('key * 'value) * ('key,'value) tree * ('key,'value) node list
+ | RightToLeftIterator of
+ ('key * 'value) * ('key,'value) tree * ('key,'value) node list;
-fun fromSpineLR nodes =
+fun fromSpineLeftToRightIterator nodes =
case nodes of
[] => NONE
| Node {key,value,right,...} :: nodes =>
- SOME (LR ((key,value),right,nodes));
+ SOME (LeftToRightIterator ((key,value),right,nodes));
-fun fromSpineRL nodes =
+fun fromSpineRightToLeftIterator nodes =
case nodes of
[] => NONE
| Node {key,value,left,...} :: nodes =>
- SOME (RL ((key,value),left,nodes));
+ SOME (RightToLeftIterator ((key,value),left,nodes));
-fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
+fun addLeftToRightIterator nodes tree = fromSpineLeftToRightIterator (treeLeftSpine nodes tree);
-fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
+fun addRightToLeftIterator nodes tree = fromSpineRightToLeftIterator (treeRightSpine nodes tree);
-fun treeMkIterator tree = addLR [] tree;
+fun treeMkIterator tree = addLeftToRightIterator [] tree;
-fun treeMkRevIterator tree = addRL [] tree;
+fun treeMkRevIterator tree = addRightToLeftIterator [] tree;
fun readIterator iter =
case iter of
- LR (key_value,_,_) => key_value
- | RL (key_value,_,_) => key_value;
+ LeftToRightIterator (key_value,_,_) => key_value
+ | RightToLeftIterator (key_value,_,_) => key_value;
fun advanceIterator iter =
case iter of
- LR (_,tree,nodes) => addLR nodes tree
- | RL (_,tree,nodes) => addRL nodes tree;
+ LeftToRightIterator (_,tree,nodes) => addLeftToRightIterator nodes tree
+ | RightToLeftIterator (_,tree,nodes) => addRightToLeftIterator nodes tree;
fun foldIterator f acc io =
case io of
--- a/src/Tools/Metis/src/Model.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Model.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Model =
--- a/src/Tools/Metis/src/Model.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Model.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* RANDOM FINITE MODELS *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Model :> Model =
@@ -272,10 +272,10 @@
fun ppEntry (tag,source_arity,target) =
Print.blockProgram Print.Inconsistent 2
- [Print.addString tag,
+ [Print.ppString tag,
Print.addBreak 1,
NameArity.pp source_arity,
- Print.addString " ->",
+ Print.ppString " ->",
Print.addBreak 1,
Name.pp target];
in
@@ -1190,7 +1190,7 @@
let
fun add (y,acc) = FunctionPerturbation (func_xs,y) :: acc
in
- foldl add acc target
+ List.foldl add acc target
end
in
pertTerms M onTarget tms xs acc
@@ -1271,8 +1271,8 @@
fun pp M =
Print.program
- [Print.addString "Model{",
+ [Print.ppString "Model{",
Print.ppInt (size M),
- Print.addString "}"];
+ Print.ppString "}"];
end
--- a/src/Tools/Metis/src/Name.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Name.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Name =
--- a/src/Tools/Metis/src/Name.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Name.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAMES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Name :> Name =
@@ -84,15 +84,15 @@
structure NameSet =
struct
- local
- structure S = ElementSet (NameMap);
- in
- open S;
- end;
+local
+ structure S = ElementSet (NameMap);
+in
+ open S;
+end;
- val pp =
- Print.ppMap
- toList
- (Print.ppBracket "{" "}" (Print.ppOpList "," Name.pp));
+val pp =
+ Print.ppMap
+ toList
+ (Print.ppBracket "{" "}" (Print.ppOpList "," Name.pp));
end
--- a/src/Tools/Metis/src/NameArity.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/NameArity.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature NameArity =
--- a/src/Tools/Metis/src/NameArity.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/NameArity.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NAME/ARITY PAIRS *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure NameArity :> NameArity =
@@ -46,7 +46,7 @@
fun pp (n,i) =
Print.blockProgram Print.Inconsistent 0
[Name.pp n,
- Print.addString "/",
+ Print.ppString "/",
Print.ppInt i];
end
@@ -57,35 +57,36 @@
structure NameArityMap =
struct
- local
- structure S = KeyMap (NameArityOrdered);
- in
- open S;
- end;
+local
+ structure S = KeyMap (NameArityOrdered);
+in
+ open S;
+end;
- fun compose m1 m2 =
- let
- fun pk ((_,a),n) = peek m2 (n,a)
- in
- mapPartial pk m1
- end;
+fun compose m1 m2 =
+ let
+ fun pk ((_,a),n) = peek m2 (n,a)
+ in
+ mapPartial pk m1
+ end;
end
structure NameAritySet =
struct
- local
- structure S = ElementSet (NameArityMap);
- in
- open S;
- end;
+local
+ structure S = ElementSet (NameArityMap);
+in
+ open S;
+end;
- val allNullary = all NameArity.nullary;
+val allNullary = all NameArity.nullary;
- val pp =
- Print.ppMap
- toList
- (Print.ppBracket "{" "}" (Print.ppOpList "," NameArity.pp));
+val pp =
+ Print.ppMap
+ toList
+ (Print.ppBracket "{" "}" (Print.ppOpList "," NameArity.pp));
+
end
--- a/src/Tools/Metis/src/Normalize.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001-2009 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Normalize =
--- a/src/Tools/Metis/src/Normalize.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Normalize :> Normalize =
@@ -688,19 +688,20 @@
val newSkolemFunction =
let
val counter : int StringMap.map ref = ref (StringMap.new ())
+
+ fun new n () =
+ let
+ val ref m = counter
+ val s = Name.toString n
+ val i = Option.getOpt (StringMap.peek m s, 0)
+ val () = counter := StringMap.insert m (s, i + 1)
+ val i = if i = 0 then "" else "_" ^ Int.toString i
+ val s = skolemPrefix ^ "_" ^ s ^ i
+ in
+ Name.fromString s
+ end
in
- (* MODIFIED by Jasmin Blanchette *)
- fn n => CRITICAL (fn () =>
- let
- val ref m = counter
- val s = Name.toString n
- val i = Option.getOpt (StringMap.peek m s, 0)
- val () = counter := StringMap.insert m (s, i + 1)
- val i = if i = 0 then "" else "_" ^ Int.toString i
- val s = skolemPrefix ^ "_" ^ s ^ i
- in
- Name.fromString s
- end)
+ fn n => Portable.critical (new n) ()
end;
fun skolemize fv bv fm =
@@ -815,8 +816,8 @@
(c2', s2', (c1,s1,fm,c2,s2) :: l)
end
- val (c1,_,fms) = foldl fwd (count0,empty,[]) fms
- val (c2,_,fms) = foldl bwd (count0,empty,[]) fms
+ val (c1,_,fms) = List.foldl fwd (count0,empty,[]) fms
+ val (c2,_,fms) = List.foldl bwd (count0,empty,[]) fms
(*MetisDebug
val _ = countEquivish c1 c2 orelse
@@ -861,10 +862,10 @@
let
val fms = sortMap (measure o count) countCompare fms
in
- foldl breakSet1 best (cumulatives fms)
+ List.foldl breakSet1 best (cumulatives fms)
end
- val best = foldl breakSing best (cumulatives fms)
+ val best = List.foldl breakSing best (cumulatives fms)
val best = breakSet I best
val best = breakSet countNegate best
val best = breakSet countClauses best
@@ -1244,14 +1245,13 @@
let
val counter : int ref = ref 0
in
- (* MODIFIED by Jasmin Blanchette *)
- fn () => CRITICAL (fn () =>
+ fn () =>
let
val ref i = counter
val () = counter := i + 1
in
definitionPrefix ^ "_" ^ Int.toString i
- end)
+ end
end;
fun newDefinition def =
--- a/src/Tools/Metis/src/Options.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Options.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROCESSING COMMAND LINE OPTIONS *)
-(* Copyright (c) 2003-2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Options =
--- a/src/Tools/Metis/src/Options.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Options.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROCESSING COMMAND LINE OPTIONS *)
-(* Copyright (c) 2003-2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Options :> Options =
@@ -146,7 +146,7 @@
fun indent (s, "" :: l) = indent (s ^ " ", l) | indent x = x
val (res,n) = indent (" ",n)
val res = res ^ join ", " n
- val res = foldl (fn (x,y) => y ^ " " ^ x) res r
+ val res = List.foldl (fn (x,y) => y ^ " " ^ x) res r
in
[res ^ " ...", " " ^ s]
end
@@ -185,7 +185,7 @@
exit allopts {message = SOME mesg, usage = true, success = false};
fun version allopts =
- (print (versionInformation allopts);
+ (TextIO.print (versionInformation allopts);
exit allopts {message = NONE, usage = false, success = true});
(* ------------------------------------------------------------------------- *)
@@ -220,7 +220,8 @@
| process ("-v" :: _) = version allopts
| process ("--version" :: _) = version allopts
| process (x :: xs) =
- if x = "" orelse x = "-" orelse hd (explode x) <> #"-" then ([], x :: xs)
+ if x = "" orelse x = "-" orelse hd (String.explode x) <> #"-" then
+ ([], x :: xs)
else
let
val (r,f) = findOption x
@@ -233,7 +234,8 @@
fn l =>
let
val (a,b) = process l
- val a = foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (rev a)
+
+ val a = List.foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (rev a)
in
(a,b)
end
--- a/src/Tools/Metis/src/Ordered.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Ordered.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Ordered =
--- a/src/Tools/Metis/src/Ordered.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Ordered.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure IntOrdered =
--- a/src/Tools/Metis/src/Parse.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Parse.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Parse =
@@ -99,8 +99,9 @@
(* ------------------------------------------------------------------------- *)
val parseInfixes :
- Print.infixes -> (string * 'a * 'a -> 'a) -> (string,'a) parser ->
- (string,'a) parser
+ Print.infixes ->
+ (Print.token * 'a * 'a -> 'a) -> ('b,Print.token) parser ->
+ ('b,'a) parser -> ('b,'a) parser
(* ------------------------------------------------------------------------- *)
(* Quotations. *)
--- a/src/Tools/Metis/src/Parse.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Parse.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PARSING *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Parse :> Parse =
@@ -134,7 +134,7 @@
val ref (n,_,l2,l3) = lastLine
val () = lastLine := (n + 1, l2, l3, line)
in
- explode line
+ String.explode line
end
in
Stream.memoize (Stream.map saveLast lines)
@@ -160,7 +160,7 @@
[] => nothing
| c :: cs => (exactChar c ++ exactCharList cs) >> snd;
-fun exactString s = exactCharList (explode s);
+fun exactString s = exactCharList (String.explode s);
fun escapeString {escape} =
let
@@ -183,7 +183,7 @@
((exactChar #"\\" ++ escapeParser) >> snd) ||
some isNormal
in
- many charParser >> implode
+ many charParser >> String.implode
end;
local
@@ -196,46 +196,51 @@
val atLeastOneSpace = atLeastOne space >> K ();
end;
-fun fromString parser s = fromList parser (explode s);
+fun fromString parser s = fromList parser (String.explode s);
(* ------------------------------------------------------------------------- *)
(* Infix operators. *)
(* ------------------------------------------------------------------------- *)
-fun parseGenInfix update sof toks parse inp =
+fun parseLayeredInfixes {tokens,assoc} mk tokParser subParser =
let
- val (e,rest) = parse inp
-
- val continue =
- case rest of
- Stream.Nil => NONE
- | Stream.Cons (h_t as (h,_)) =>
- if StringSet.member h toks then SOME h_t else NONE
- in
- case continue of
- NONE => (sof e, rest)
- | SOME (h,t) => parseGenInfix update (update sof h e) toks parse (t ())
- end;
+ fun layerTokParser inp =
+ let
+ val tok_rest as (tok,_) = tokParser inp
+ in
+ if StringSet.member tok tokens then tok_rest
+ else raise NoParse
+ end
-local
- fun add ({leftSpaces = _, token = t, rightSpaces = _}, s) = StringSet.add s t;
+ fun layerMk (x,txs) =
+ case assoc of
+ Print.LeftAssoc =>
+ let
+ fun inc ((t,y),z) = mk (t,z,y)
+ in
+ List.foldl inc x txs
+ end
+ | Print.NonAssoc =>
+ (case txs of
+ [] => x
+ | [(t,y)] => mk (t,x,y)
+ | _ => raise NoParse)
+ | Print.RightAssoc =>
+ (case rev txs of
+ [] => x
+ | tx :: txs =>
+ let
+ fun inc ((t,y),(u,z)) = (t, mk (u,y,z))
- fun parse leftAssoc toks con =
- let
- val update =
- if leftAssoc then (fn f => fn t => fn a => fn b => con (t, f a, b))
- else (fn f => fn t => fn a => fn b => f (con (t, a, b)))
- in
- parseGenInfix update I toks
- end;
-in
- fun parseLayeredInfixes {tokens,leftAssoc} =
- let
- val toks = List.foldl add StringSet.empty tokens
- in
- parse leftAssoc toks
- end;
-end;
+ val (t,y) = List.foldl inc tx txs
+ in
+ mk (t,x,y)
+ end)
+
+ val layerParser = subParser ++ many (layerTokParser ++ subParser)
+ in
+ layerParser >> layerMk
+ end;
fun parseInfixes ops =
let
@@ -243,7 +248,8 @@
val iparsers = List.map parseLayeredInfixes layeredOps
in
- fn con => fn subparser => foldl (fn (p,sp) => p con sp) subparser iparsers
+ fn mk => fn tokParser => fn subParser =>
+ List.foldr (fn (p,sp) => p mk tokParser sp) subParser iparsers
end;
(* ------------------------------------------------------------------------- *)
@@ -257,7 +263,7 @@
fun expand (QUOTE q, s) = s ^ q
| expand (ANTIQUOTE a, s) = s ^ printer a
- val string = foldl expand "" quote
+ val string = List.foldl expand "" quote
in
parser string
end;
--- a/src/Tools/Metis/src/Portable.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Portable.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
-(* ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* ML COMPILER SPECIFIC FUNCTIONS *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Portable =
@@ -19,17 +19,10 @@
val pointerEqual : 'a * 'a -> bool
(* ------------------------------------------------------------------------- *)
-(* Timing function applications. *)
+(* Marking critical sections of code. *)
(* ------------------------------------------------------------------------- *)
-val time : ('a -> 'b) -> 'a -> 'b
-
-(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-(* MODIFIED by Jasmin Blanchette *)
-val CRITICAL: (unit -> 'a) -> 'a
+val critical : (unit -> 'a) -> unit -> 'a
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
@@ -43,4 +36,10 @@
val randomWord : unit -> Word.word
+(* ------------------------------------------------------------------------- *)
+(* Timing function applications. *)
+(* ------------------------------------------------------------------------- *)
+
+val time : ('a -> 'b) -> 'a -> 'b
+
end
--- a/src/Tools/Metis/src/PortableMlton.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/PortableMlton.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MLTON SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Portable :> Portable =
@@ -19,6 +19,33 @@
val pointerEqual = MLton.eq;
(* ------------------------------------------------------------------------- *)
+(* Marking critical sections of code. *)
+(* ------------------------------------------------------------------------- *)
+
+fun critical f () = f ();
+
+(* ------------------------------------------------------------------------- *)
+(* Generating random values. *)
+(* ------------------------------------------------------------------------- *)
+
+fun randomWord () = MLton.Random.rand ();
+
+fun randomBool () = Word.andb (randomWord (),0w1) = 0w0;
+
+fun randomInt 1 = 0
+ | randomInt 2 = Word.toInt (Word.andb (randomWord (), 0w1))
+ | randomInt 4 = Word.toInt (Word.andb (randomWord (), 0w3))
+ | randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
+
+local
+ fun wordToReal w = Real.fromInt (Word.toInt (Word.>> (w,0w1)))
+
+ val normalizer = 1.0 / wordToReal (Word.notb 0w0);
+in
+ fun randomReal () = normalizer * wordToReal (randomWord ());
+end;
+
+(* ------------------------------------------------------------------------- *)
(* Timing function applications. *)
(* ------------------------------------------------------------------------- *)
@@ -56,34 +83,6 @@
y
end;
-(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-(* MODIFIED by Jasmin Blanchette *)
-fun CRITICAL e = e (); (*dummy*)
-
-(* ------------------------------------------------------------------------- *)
-(* Generating random values. *)
-(* ------------------------------------------------------------------------- *)
-
-fun randomWord () = MLton.Random.rand ();
-
-fun randomBool () = Word.andb (randomWord (),0w1) = 0w0;
-
-fun randomInt 1 = 0
- | randomInt 2 = Word.toInt (Word.andb (randomWord (), 0w1))
- | randomInt 4 = Word.toInt (Word.andb (randomWord (), 0w3))
- | randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
-
-local
- fun wordToReal w = Real.fromInt (Word.toInt (Word.>> (w,0w1)))
-
- val normalizer = 1.0 / wordToReal (Word.notb 0w0);
-in
- fun randomReal () = normalizer * wordToReal (randomWord ());
-end;
-
end
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/PortableMosml.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/PortableMosml.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MOSCOW ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Portable :> Portable =
@@ -23,17 +23,10 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Timing function applications. *)
+(* Marking critical sections of code. *)
(* ------------------------------------------------------------------------- *)
-val time = Mosml.time;
-
-(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-(* MODIFIED by Jasmin Blanchette *)
-fun CRITICAL e = e (); (*dummy*)
+fun critical f () = f ();
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
@@ -57,6 +50,12 @@
Word.orb (Word.<< (h,0w16), l)
end;
+(* ------------------------------------------------------------------------- *)
+(* Timing function applications. *)
+(* ------------------------------------------------------------------------- *)
+
+val time = Mosml.time;
+
end
(* ------------------------------------------------------------------------- *)
@@ -68,6 +67,18 @@
val _ = catch_interrupt true;
(* ------------------------------------------------------------------------- *)
+(* Forcing fully qualified names of some key functions. *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+val explode = ()
+and foldl = ()
+and foldr = ()
+and implode = ()
+and print = ();
+*)
+
+(* ------------------------------------------------------------------------- *)
(* Ad-hoc upgrading of the Moscow ML basis library. *)
(* ------------------------------------------------------------------------- *)
@@ -101,6 +112,28 @@
fun OS_Process_isSuccess s = s = OS.Process.success;
+fun String_concatWith s l =
+ case l of
+ [] => ""
+ | h :: t => List.foldl (fn (x,y) => y ^ s ^ x) h t;
+
+fun String_isSubstring p s =
+ let
+ val sizeP = size p
+ and sizeS = size s
+ in
+ if sizeP > sizeS then false
+ else if sizeP = sizeS then p = s
+ else
+ let
+ fun check i = String.substring (s,i,sizeP) = p
+
+ fun checkn i = check i orelse (i > 0 andalso checkn (i - 1))
+ in
+ checkn (sizeS - sizeP)
+ end
+ end;
+
fun String_isSuffix p s =
let
val sizeP = size p
--- a/src/Tools/Metis/src/PortablePolyml.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/PortablePolyml.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* POLY/ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Portable :> Portable =
@@ -19,6 +19,24 @@
fun pointerEqual (x : 'a, y : 'a) = PolyML.pointerEq(x,y);
(* ------------------------------------------------------------------------- *)
+(* Marking critical sections of code. *)
+(* ------------------------------------------------------------------------- *)
+
+fun critical f () = f ();
+
+(* ------------------------------------------------------------------------- *)
+(* Generating random values. *)
+(* ------------------------------------------------------------------------- *)
+
+val randomWord = Random.nextWord;
+
+val randomBool = Random.nextBool;
+
+val randomInt = Random.nextInt;
+
+val randomReal = Random.nextReal;
+
+(* ------------------------------------------------------------------------- *)
(* Timing function applications. *)
(* ------------------------------------------------------------------------- *)
@@ -44,7 +62,7 @@
val {usr,sys} = Timer.checkCPUTimer c
val real = Timer.checkRealTimer r
in
- TextIO.print (* MODIFIED by Jasmin Blanchette *)
+ print
("User: " ^ p usr ^ " System: " ^ p sys ^
" Real: " ^ p real ^ "\n")
end
@@ -56,26 +74,6 @@
y
end;
-(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-(* MODIFIED by Jasmin Blanchette *)
-fun CRITICAL e = NAMED_CRITICAL "metis" e;
-
-
-(* ------------------------------------------------------------------------- *)
-(* Generating random values. *)
-(* ------------------------------------------------------------------------- *)
-
-val randomWord = Random.nextWord;
-
-val randomBool = Random.nextBool;
-
-val randomInt = Random.nextInt;
-
-val randomReal = Random.nextReal;
-
end
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Print.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Print.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,27 +1,39 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Print =
sig
(* ------------------------------------------------------------------------- *)
+(* Escaping strings. *)
+(* ------------------------------------------------------------------------- *)
+
+val escapeString : {escape : char list} -> string -> string
+
+(* ------------------------------------------------------------------------- *)
+(* A type of strings annotated with their size. *)
+(* ------------------------------------------------------------------------- *)
+
+type stringSize = string * int
+
+val mkStringSize : string -> stringSize
+
+(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
(* ------------------------------------------------------------------------- *)
datatype breakStyle = Consistent | Inconsistent
-datatype ppStep =
+datatype step =
BeginBlock of breakStyle * int
| EndBlock
- | AddString of string
+ | AddString of stringSize
| AddBreak of int
| AddNewline
-type ppstream = ppStep Stream.stream
-
-type 'a pp = 'a -> ppstream
+type ppstream = step Stream.stream
(* ------------------------------------------------------------------------- *)
(* Pretty-printer primitives. *)
@@ -31,7 +43,7 @@
val endBlock : ppstream
-val addString : string -> ppstream
+val addString : stringSize -> ppstream
val addBreak : int -> ppstream
@@ -51,18 +63,24 @@
val blockProgram : breakStyle -> int -> ppstream list -> ppstream
-val bracket : string -> string -> ppstream -> ppstream
+(* ------------------------------------------------------------------------- *)
+(* Executing pretty-printers to generate lines. *)
+(* ------------------------------------------------------------------------- *)
-val field : string -> ppstream -> ppstream
-
-val record : (string * ppstream) list -> ppstream
+val execute :
+ {lineLength : int} -> ppstream ->
+ {indent : int, line : string} Stream.stream
(* ------------------------------------------------------------------------- *)
(* Pretty-printer combinators. *)
(* ------------------------------------------------------------------------- *)
+type 'a pp = 'a -> ppstream
+
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
+val ppString : string pp
+
val ppBracket : string -> string -> 'a pp -> 'a pp
val ppOp : string -> ppstream
@@ -81,8 +99,6 @@
val ppChar : char pp
-val ppString : string pp
-
val ppEscapeString : {escape : char list} -> string pp
val ppUnit : unit pp
@@ -111,7 +127,7 @@
val ppBreakStyle : breakStyle pp
-val ppPpStep : ppStep pp
+val ppStep : step pp
val ppPpstream : ppstream pp
@@ -119,28 +135,27 @@
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
+type token = string
+
+datatype assoc =
+ LeftAssoc
+ | NonAssoc
+ | RightAssoc
+
datatype infixes =
Infixes of
- {token : string,
+ {token : token,
precedence : int,
- leftAssoc : bool} list
+ assoc : assoc} list
val tokensInfixes : infixes -> StringSet.set
-val layerInfixes :
- infixes ->
- {tokens : {leftSpaces : int, token : string, rightSpaces : int} list,
- leftAssoc : bool} list
+val layerInfixes : infixes -> {tokens : StringSet.set, assoc : assoc} list
val ppInfixes :
- infixes -> ('a -> (string * 'a * 'a) option) -> ('a * bool) pp ->
- ('a * bool) pp
-
-(* ------------------------------------------------------------------------- *)
-(* Executing pretty-printers to generate lines. *)
-(* ------------------------------------------------------------------------- *)
-
-val execute : {lineLength : int} -> ppstream -> string Stream.stream
+ infixes ->
+ ('a -> (token * 'a * 'a) option) -> ('a * token) pp ->
+ ('a * bool) pp -> ('a * bool) pp
(* ------------------------------------------------------------------------- *)
(* Executing pretty-printers with a global line length. *)
--- a/src/Tools/Metis/src/Print.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Print.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRETTY-PRINTING *)
-(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Print :> Print =
@@ -29,23 +29,47 @@
| Stream.Cons (h,t) => revAppend h (revConcat o t);
local
- fun join current prev = (prev ^ "\n", current);
+ fun calcSpaces n = nChars #" " n;
+
+ val cacheSize = 2 * initialLineLength;
+
+ val cachedSpaces = Vector.tabulate (cacheSize,calcSpaces);
in
- fun joinNewline strm =
- case strm of
- Stream.Nil => Stream.Nil
- | Stream.Cons (h,t) => Stream.maps join Stream.singleton h (t ());
+ fun nSpaces n =
+ if n < cacheSize then Vector.sub (cachedSpaces,n)
+ else calcSpaces n;
end;
-local
- fun calcSpaces n = nChars #" " n;
+(* ------------------------------------------------------------------------- *)
+(* Escaping strings. *)
+(* ------------------------------------------------------------------------- *)
+
+fun escapeString {escape} =
+ let
+ val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
- val cachedSpaces = Vector.tabulate (initialLineLength,calcSpaces);
-in
- fun nSpaces n =
- if n < initialLineLength then Vector.sub (cachedSpaces,n)
- else calcSpaces n;
-end;
+ fun escapeChar c =
+ case c of
+ #"\\" => "\\\\"
+ | #"\n" => "\\n"
+ | #"\t" => "\\t"
+ | _ =>
+ case List.find (equal c o fst) escapeMap of
+ SOME (_,s) => s
+ | NONE => str c
+ in
+ String.translate escapeChar
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of strings annotated with their size. *)
+(* ------------------------------------------------------------------------- *)
+
+type stringSize = string * int;
+
+fun mkStringSize s = (s, size s);
+
+val emptyStringSize = mkStringSize "";
(* ------------------------------------------------------------------------- *)
(* A type of pretty-printers. *)
@@ -53,23 +77,21 @@
datatype breakStyle = Consistent | Inconsistent;
-datatype ppStep =
+datatype step =
BeginBlock of breakStyle * int
| EndBlock
- | AddString of string
+ | AddString of stringSize
| AddBreak of int
| AddNewline;
-type ppstream = ppStep Stream.stream;
-
-type 'a pp = 'a -> ppstream;
+type ppstream = step Stream.stream;
fun breakStyleToString style =
case style of
Consistent => "Consistent"
| Inconsistent => "Inconsistent";
-fun ppStepToString step =
+fun stepToString step =
case step of
BeginBlock _ => "BeginBlock"
| EndBlock => "EndBlock"
@@ -109,330 +131,6 @@
fun blockProgram style indent pps = block style indent (program pps);
-fun bracket l r pp =
- blockProgram Inconsistent (size l)
- [addString l,
- pp,
- addString r];
-
-fun field f pp =
- blockProgram Inconsistent 2
- [addString (f ^ " ="),
- addBreak 1,
- pp];
-
-val record =
- let
- val sep = sequence (addString ",") (addBreak 1)
-
- fun recordField (f,pp) = field f pp
-
- fun sepField f = sequence sep (recordField f)
-
- fun fields [] = []
- | fields (f :: fs) = recordField f :: map sepField fs
- in
- bracket "{" "}" o blockProgram Consistent 0 o fields
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printer combinators. *)
-(* ------------------------------------------------------------------------- *)
-
-fun ppMap f ppB a : ppstream = ppB (f a);
-
-fun ppBracket l r ppA a = bracket l r (ppA a);
-
-fun ppOp s = sequence (if s = "" then skip else addString s) (addBreak 1);
-
-fun ppOp2 ab ppA ppB (a,b) =
- blockProgram Inconsistent 0
- [ppA a,
- ppOp ab,
- ppB b];
-
-fun ppOp3 ab bc ppA ppB ppC (a,b,c) =
- blockProgram Inconsistent 0
- [ppA a,
- ppOp ab,
- ppB b,
- ppOp bc,
- ppC c];
-
-fun ppOpList s ppA =
- let
- fun ppOpA a = sequence (ppOp s) (ppA a)
- in
- fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
- end;
-
-fun ppOpStream s ppA =
- let
- fun ppOpA a = sequence (ppOp s) (ppA a)
- in
- fn Stream.Nil => skip
- | Stream.Cons (h,t) =>
- blockProgram Inconsistent 0
- [ppA h,
- Stream.concat (Stream.map ppOpA (t ()))]
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printers for common types. *)
-(* ------------------------------------------------------------------------- *)
-
-fun ppChar c = addString (str c);
-
-val ppString = addString;
-
-fun ppEscapeString {escape} =
- let
- val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
-
- fun escapeChar c =
- case c of
- #"\\" => "\\\\"
- | #"\n" => "\\n"
- | #"\t" => "\\t"
- | _ =>
- case List.find (equal c o fst) escapeMap of
- SOME (_,s) => s
- | NONE => str c
- in
- fn s => addString (String.translate escapeChar s)
- end;
-
-val ppUnit : unit pp = K (addString "()");
-
-fun ppBool b = addString (if b then "true" else "false");
-
-fun ppInt i = addString (Int.toString i);
-
-local
- val ppNeg = addString "~"
- and ppSep = addString ","
- and ppZero = addString "0"
- and ppZeroZero = addString "00";
-
- fun ppIntBlock i =
- if i < 10 then sequence ppZeroZero (ppInt i)
- else if i < 100 then sequence ppZero (ppInt i)
- else ppInt i;
-
- fun ppIntBlocks i =
- if i < 1000 then ppInt i
- else sequence (ppIntBlocks (i div 1000))
- (sequence ppSep (ppIntBlock (i mod 1000)));
-in
- fun ppPrettyInt i =
- if i < 0 then sequence ppNeg (ppIntBlocks (~i))
- else ppIntBlocks i;
-end;
-
-fun ppReal r = addString (Real.toString r);
-
-fun ppPercent p = addString (percentToString p);
-
-fun ppOrder x =
- addString
- (case x of
- LESS => "Less"
- | EQUAL => "Equal"
- | GREATER => "Greater");
-
-fun ppList ppA = ppBracket "[" "]" (ppOpList "," ppA);
-
-fun ppStream ppA = ppBracket "[" "]" (ppOpStream "," ppA);
-
-fun ppOption ppA ao =
- case ao of
- SOME a => ppA a
- | NONE => addString "-";
-
-fun ppPair ppA ppB = ppBracket "(" ")" (ppOp2 "," ppA ppB);
-
-fun ppTriple ppA ppB ppC = ppBracket "(" ")" (ppOp3 "," "," ppA ppB ppC);
-
-fun ppBreakStyle style = addString (breakStyleToString style);
-
-fun ppPpStep step =
- let
- val cmd = ppStepToString step
- in
- blockProgram Inconsistent 2
- (addString cmd ::
- (case step of
- BeginBlock style_indent =>
- [addBreak 1,
- ppPair ppBreakStyle ppInt style_indent]
- | EndBlock => []
- | AddString s =>
- [addBreak 1,
- addString ("\"" ^ s ^ "\"")]
- | AddBreak n =>
- [addBreak 1,
- ppInt n]
- | AddNewline => []))
- end;
-
-val ppPpstream = ppStream ppPpStep;
-
-(* ------------------------------------------------------------------------- *)
-(* Pretty-printing infix operators. *)
-(* ------------------------------------------------------------------------- *)
-
-datatype infixes =
- Infixes of
- {token : string,
- precedence : int,
- leftAssoc : bool} list;
-
-local
- fun chop l =
- case l of
- #" " :: l => let val (n,l) = chop l in (n + 1, l) end
- | _ => (0,l);
-in
- fun opSpaces tok =
- let
- val tok = explode tok
- val (r,tok) = chop (rev tok)
- val (l,tok) = chop (rev tok)
- val tok = implode tok
- in
- {leftSpaces = l, token = tok, rightSpaces = r}
- end;
-end;
-
-fun ppOpSpaces {leftSpaces,token,rightSpaces} =
- let
- val leftSpacesToken =
- if leftSpaces = 0 then token else nSpaces leftSpaces ^ token
- in
- sequence
- (addString leftSpacesToken)
- (addBreak rightSpaces)
- end;
-
-local
- fun new t l acc = {tokens = [opSpaces t], leftAssoc = l} :: acc;
-
- fun add t l acc =
- case acc of
- [] => raise Bug "Print.layerInfixOps.layer"
- | {tokens = ts, leftAssoc = l'} :: acc =>
- if l = l' then {tokens = opSpaces t :: ts, leftAssoc = l} :: acc
- else raise Bug "Print.layerInfixOps: mixed assocs";
-
- fun layer ({token = t, precedence = p, leftAssoc = l}, (acc,p')) =
- let
- val acc = if p = p' then add t l acc else new t l acc
- in
- (acc,p)
- end;
-in
- fun layerInfixes (Infixes i) =
- case sortMap #precedence Int.compare i of
- [] => []
- | {token = t, precedence = p, leftAssoc = l} :: i =>
- let
- val acc = new t l []
-
- val (acc,_) = List.foldl layer (acc,p) i
- in
- acc
- end;
-end;
-
-val tokensLayeredInfixes =
- let
- fun addToken ({leftSpaces = _, token = t, rightSpaces = _}, s) =
- StringSet.add s t
-
- fun addTokens ({tokens = t, leftAssoc = _}, s) =
- List.foldl addToken s t
- in
- List.foldl addTokens StringSet.empty
- end;
-
-val tokensInfixes = tokensLayeredInfixes o layerInfixes;
-
-local
- val mkTokenMap =
- let
- fun add (token,m) =
- let
- val {leftSpaces = _, token = t, rightSpaces = _} = token
- in
- StringMap.insert m (t, ppOpSpaces token)
- end
- in
- List.foldl add (StringMap.new ())
- end;
-in
- fun ppGenInfix {tokens,leftAssoc} =
- let
- val tokenMap = mkTokenMap tokens
- in
- fn dest => fn ppSub =>
- let
- fun dest' tm =
- case dest tm of
- NONE => NONE
- | SOME (t,a,b) =>
- case StringMap.peek tokenMap t of
- NONE => NONE
- | SOME p => SOME (p,a,b)
-
- fun ppGo (tmr as (tm,r)) =
- case dest' tm of
- NONE => ppSub tmr
- | SOME (p,a,b) =>
- program
- [(if leftAssoc then ppGo else ppSub) (a,true),
- p,
- (if leftAssoc then ppSub else ppGo) (b,r)]
- in
- fn tmr as (tm,_) =>
- if Option.isSome (dest' tm) then
- block Inconsistent 0 (ppGo tmr)
- else
- ppSub tmr
- end
- end;
-end
-
-fun ppInfixes ops =
- let
- val layeredOps = layerInfixes ops
-
- val toks = tokensLayeredInfixes layeredOps
-
- val iprinters = List.map ppGenInfix layeredOps
- in
- fn dest => fn ppSub =>
- let
- fun printer sub = foldl (fn (ip,p) => ip dest p) sub iprinters
-
- fun isOp t =
- case dest t of
- SOME (x,_,_) => StringSet.member x toks
- | NONE => false
-
- fun subpr (tmr as (tm,_)) =
- if isOp tm then
- blockProgram Inconsistent 1
- [addString "(",
- printer subpr (tm,false),
- addString ")"]
- else
- ppSub tmr
- in
- fn tmr => block Inconsistent 0 (printer subpr tmr)
- end
- end;
-
(* ------------------------------------------------------------------------- *)
(* Executing pretty-printers to generate lines. *)
(* ------------------------------------------------------------------------- *)
@@ -496,18 +194,22 @@
val sizeChunks = List.foldl (fn (c,z) => sizeChunk c + z) 0;
local
- fun render acc [] = acc
- | render acc (chunk :: chunks) =
- case chunk of
- StringChunk {string = s, ...} => render (acc ^ s) chunks
- | BreakChunk n => render (acc ^ nSpaces n) chunks
- | BlockChunk (Block {chunks = l, ...}) =>
- render acc (List.revAppend (l,chunks));
+ fun flatten acc chunks =
+ case chunks of
+ [] => rev acc
+ | chunk :: chunks =>
+ case chunk of
+ StringChunk {string = s, ...} => flatten (s :: acc) chunks
+ | BreakChunk n => flatten (nSpaces n :: acc) chunks
+ | BlockChunk (Block {chunks = l, ...}) =>
+ flatten acc (List.revAppend (l,chunks));
in
- fun renderChunks indent chunks = render (nSpaces indent) (rev chunks);
+ fun renderChunks indent chunks =
+ {indent = indent,
+ line = String.concat (flatten [] (rev chunks))};
+end;
- fun renderChunk indent chunk = renderChunks indent [chunk];
-end;
+fun renderChunk indent chunk = renderChunks indent [chunk];
fun isEmptyBlock block =
let
@@ -523,6 +225,7 @@
empty
end;
+(*BasicDebug
fun checkBlock ind block =
let
val Block {indent, style = _, size, chunks} = block
@@ -558,6 +261,7 @@
in
check initialIndent o rev
end;
+*)
val initialBlock =
let
@@ -969,12 +673,10 @@
(lines,state)
end;
- fun executeAddString lineLength s lines state =
+ fun executeAddString lineLength (s,n) lines state =
let
val State {blocks,lineIndent,lineSize} = state
- val n = size s
-
val blocks =
case blocks of
[] => raise Bug "Print.executeAddString: no block"
@@ -1061,10 +763,13 @@
fun executeAddNewline lineLength lines state =
let
- val (lines,state) = executeAddString lineLength "" lines state
- val (lines,state) = executeBigBreak lineLength lines state
+ val (lines,state) =
+ executeAddString lineLength emptyStringSize lines state
+
+ val (lines,state) =
+ executeBigBreak lineLength lines state
in
- executeAddString lineLength "" lines state
+ executeAddString lineLength emptyStringSize lines state
end;
fun final lineLength lines state =
@@ -1108,7 +813,7 @@
(lines,state)
end
handle Bug bug =>
- raise Bug ("Print.advance: after " ^ ppStepToString step ^
+ raise Bug ("Print.advance: after " ^ stepToString step ^
" command:\n" ^ bug)
*)
in
@@ -1117,21 +822,372 @@
end;
(* ------------------------------------------------------------------------- *)
+(* Pretty-printer combinators. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a pp = 'a -> ppstream;
+
+fun ppMap f ppB a : ppstream = ppB (f a);
+
+fun ppBracket' l r ppA a =
+ let
+ val (_,n) = l
+ in
+ blockProgram Inconsistent n
+ [addString l,
+ ppA a,
+ addString r]
+ end;
+
+fun ppOp' s = sequence (addString s) (addBreak 1);
+
+fun ppOp2' ab ppA ppB (a,b) =
+ blockProgram Inconsistent 0
+ [ppA a,
+ ppOp' ab,
+ ppB b];
+
+fun ppOp3' ab bc ppA ppB ppC (a,b,c) =
+ blockProgram Inconsistent 0
+ [ppA a,
+ ppOp' ab,
+ ppB b,
+ ppOp' bc,
+ ppC c];
+
+fun ppOpList' s ppA =
+ let
+ fun ppOpA a = sequence (ppOp' s) (ppA a)
+ in
+ fn [] => skip
+ | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
+ end;
+
+fun ppOpStream' s ppA =
+ let
+ fun ppOpA a = sequence (ppOp' s) (ppA a)
+ in
+ fn Stream.Nil => skip
+ | Stream.Cons (h,t) =>
+ blockProgram Inconsistent 0
+ [ppA h,
+ Stream.concat (Stream.map ppOpA (t ()))]
+ end;
+
+fun ppBracket l r = ppBracket' (mkStringSize l) (mkStringSize r);
+
+fun ppOp s = ppOp' (mkStringSize s);
+
+fun ppOp2 ab = ppOp2' (mkStringSize ab);
+
+fun ppOp3 ab bc = ppOp3' (mkStringSize ab) (mkStringSize bc);
+
+fun ppOpList s = ppOpList' (mkStringSize s);
+
+fun ppOpStream s = ppOpStream' (mkStringSize s);
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printers for common types. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppChar c = addString (str c, 1);
+
+fun ppString s = addString (mkStringSize s);
+
+fun ppEscapeString escape = ppMap (escapeString escape) ppString;
+
+local
+ val pp = ppString "()";
+in
+ fun ppUnit () = pp;
+end;
+
+local
+ val ppTrue = ppString "true"
+ and ppFalse = ppString "false";
+in
+ fun ppBool b = if b then ppTrue else ppFalse;
+end;
+
+val ppInt = ppMap Int.toString ppString;
+
+local
+ val ppNeg = ppString "~"
+ and ppSep = ppString ","
+ and ppZero = ppString "0"
+ and ppZeroZero = ppString "00";
+
+ fun ppIntBlock i =
+ if i < 10 then sequence ppZeroZero (ppInt i)
+ else if i < 100 then sequence ppZero (ppInt i)
+ else ppInt i;
+
+ fun ppIntBlocks i =
+ if i < 1000 then ppInt i
+ else sequence (ppIntBlocks (i div 1000))
+ (sequence ppSep (ppIntBlock (i mod 1000)));
+in
+ fun ppPrettyInt i =
+ if i < 0 then sequence ppNeg (ppIntBlocks (~i))
+ else ppIntBlocks i;
+end;
+
+val ppReal = ppMap Real.toString ppString;
+
+val ppPercent = ppMap percentToString ppString;
+
+local
+ val ppLess = ppString "Less"
+ and ppEqual = ppString "Equal"
+ and ppGreater = ppString "Greater";
+in
+ fun ppOrder ord =
+ case ord of
+ LESS => ppLess
+ | EQUAL => ppEqual
+ | GREATER => ppGreater;
+end;
+
+local
+ val left = mkStringSize "["
+ and right = mkStringSize "]"
+ and sep = mkStringSize ",";
+in
+ fun ppList ppX xs = ppBracket' left right (ppOpList' sep ppX) xs;
+
+ fun ppStream ppX xs = ppBracket' left right (ppOpStream' sep ppX) xs;
+end;
+
+local
+ val ppNone = ppString "-";
+in
+ fun ppOption ppX xo =
+ case xo of
+ SOME x => ppX x
+ | NONE => ppNone;
+end;
+
+local
+ val left = mkStringSize "("
+ and right = mkStringSize ")"
+ and sep = mkStringSize ",";
+in
+ fun ppPair ppA ppB =
+ ppBracket' left right (ppOp2' sep ppA ppB);
+
+ fun ppTriple ppA ppB ppC =
+ ppBracket' left right (ppOp3' sep sep ppA ppB ppC);
+end;
+
+val ppBreakStyle = ppMap breakStyleToString ppString;
+
+val ppStep = ppMap stepToString ppString;
+
+val ppStringSize =
+ let
+ val left = mkStringSize "\""
+ and right = mkStringSize "\""
+ and escape = {escape = [#"\""]}
+
+ val pp = ppBracket' left right (ppEscapeString escape)
+ in
+ fn (s,n) => if size s = n then pp s else ppPair pp ppInt (s,n)
+ end;
+
+fun ppStep step =
+ blockProgram Inconsistent 2
+ (ppStep step ::
+ (case step of
+ BeginBlock style_indent =>
+ [addBreak 1,
+ ppPair ppBreakStyle ppInt style_indent]
+ | EndBlock => []
+ | AddString s =>
+ [addBreak 1,
+ ppStringSize s]
+ | AddBreak n =>
+ [addBreak 1,
+ ppInt n]
+ | AddNewline => []));
+
+val ppPpstream = ppStream ppStep;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing infix operators. *)
+(* ------------------------------------------------------------------------- *)
+
+type token = string;
+
+datatype assoc =
+ LeftAssoc
+ | NonAssoc
+ | RightAssoc;
+
+datatype infixes =
+ Infixes of
+ {token : token,
+ precedence : int,
+ assoc : assoc} list;
+
+local
+ fun comparePrecedence (io1,io2) =
+ let
+ val {token = _, precedence = p1, assoc = _} = io1
+ and {token = _, precedence = p2, assoc = _} = io2
+ in
+ Int.compare (p2,p1)
+ end;
+
+ fun equalAssoc a a' =
+ case a of
+ LeftAssoc => (case a' of LeftAssoc => true | _ => false)
+ | NonAssoc => (case a' of NonAssoc => true | _ => false)
+ | RightAssoc => (case a' of RightAssoc => true | _ => false);
+
+ fun new t a acc = {tokens = StringSet.singleton t, assoc = a} :: acc;
+
+ fun add t a' acc =
+ case acc of
+ [] => raise Bug "Print.layerInfixes: null"
+ | {tokens = ts, assoc = a} :: acc =>
+ if equalAssoc a a' then {tokens = StringSet.add ts t, assoc = a} :: acc
+ else raise Bug "Print.layerInfixes: mixed assocs";
+
+ fun layer ({token = t, precedence = p, assoc = a}, (acc,p')) =
+ let
+ val acc = if p = p' then add t a acc else new t a acc
+ in
+ (acc,p)
+ end;
+in
+ fun layerInfixes (Infixes ios) =
+ case sort comparePrecedence ios of
+ [] => []
+ | {token = t, precedence = p, assoc = a} :: ios =>
+ let
+ val acc = new t a []
+
+ val (acc,_) = List.foldl layer (acc,p) ios
+ in
+ acc
+ end;
+end;
+
+local
+ fun add ({tokens = ts, assoc = _}, tokens) = StringSet.union ts tokens;
+in
+ fun tokensLayeredInfixes l = List.foldl add StringSet.empty l;
+end;
+
+fun tokensInfixes ios = tokensLayeredInfixes (layerInfixes ios);
+
+fun destInfixOp dest tokens tm =
+ case dest tm of
+ NONE => NONE
+ | s as SOME (t,a,b) => if StringSet.member t tokens then s else NONE;
+
+fun ppLayeredInfixes dest ppTok {tokens,assoc} ppLower ppSub =
+ let
+ fun isLayer t = StringSet.member t tokens
+
+ fun ppTerm aligned (tm,r) =
+ case dest tm of
+ NONE => ppSub (tm,r)
+ | SOME (t,a,b) =>
+ if aligned andalso isLayer t then ppLayer (tm,t,a,b,r)
+ else ppLower (tm,t,a,b,r)
+
+ and ppLeft tm_r =
+ let
+ val aligned = case assoc of LeftAssoc => true | _ => false
+ in
+ ppTerm aligned tm_r
+ end
+
+ and ppLayer (tm,t,a,b,r) =
+ program
+ [ppLeft (a,true),
+ ppTok (tm,t),
+ ppRight (b,r)]
+
+ and ppRight tm_r =
+ let
+ val aligned = case assoc of RightAssoc => true | _ => false
+ in
+ ppTerm aligned tm_r
+ end
+ in
+ fn tm_t_a_b_r as (_,t,_,_,_) =>
+ if isLayer t then block Inconsistent 0 (ppLayer tm_t_a_b_r)
+ else ppLower tm_t_a_b_r
+ end;
+
+local
+ val leftBrack = mkStringSize "("
+ and rightBrack = mkStringSize ")";
+in
+ fun ppInfixes ops =
+ let
+ val layers = layerInfixes ops
+
+ val toks = tokensLayeredInfixes layers
+ in
+ fn dest => fn ppTok => fn ppSub =>
+ let
+ fun destOp tm = destInfixOp dest toks tm
+
+ fun ppInfix tm_t_a_b_r = ppLayers layers tm_t_a_b_r
+
+ and ppLayers ls (tm,t,a,b,r) =
+ case ls of
+ [] =>
+ ppBracket' leftBrack rightBrack ppInfix (tm,t,a,b,false)
+ | l :: ls =>
+ let
+ val ppLower = ppLayers ls
+ in
+ ppLayeredInfixes destOp ppTok l ppLower ppSub (tm,t,a,b,r)
+ end
+ in
+ fn (tm,r) =>
+ case destOp tm of
+ SOME (t,a,b) => ppInfix (tm,t,a,b,r)
+ | NONE => ppSub (tm,r)
+ end
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
(* Executing pretty-printers with a global line length. *)
(* ------------------------------------------------------------------------- *)
val lineLength = ref initialLineLength;
fun toStream ppA a =
- Stream.map (fn s => s ^ "\n")
+ Stream.map (fn {indent,line} => nSpaces indent ^ line ^ "\n")
(execute {lineLength = !lineLength} (ppA a));
-fun toString ppA a =
- case execute {lineLength = !lineLength} (ppA a) of
- Stream.Nil => ""
- | Stream.Cons (h,t) => Stream.foldl (fn (s,z) => z ^ "\n" ^ s) h (t ());
+local
+ fun inc {indent,line} acc = line :: nSpaces indent :: acc;
-fun trace ppX nameX x =
- Useful.trace (toString (ppOp2 " =" ppString ppX) (nameX,x) ^ "\n");
+ fun incn (indent_line,acc) = inc indent_line ("\n" :: acc);
+in
+ fun toString ppA a =
+ case execute {lineLength = !lineLength} (ppA a) of
+ Stream.Nil => ""
+ | Stream.Cons (h,t) =>
+ let
+ val lines = Stream.foldl incn (inc h []) (t ())
+ in
+ String.concat (rev lines)
+ end;
+end;
+
+local
+ val sep = mkStringSize " =";
+in
+ fun trace ppX nameX x =
+ Useful.trace (toString (ppOp2' sep ppString ppX) (nameX,x) ^ "\n");
+end;
end
--- a/src/Tools/Metis/src/Problem.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Problem.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Problem =
--- a/src/Tools/Metis/src/Problem.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Problem.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* CNF PROBLEMS *)
-(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Problem :> Problem =
@@ -29,9 +29,9 @@
val cls = toClauses prob
in
{clauses = length cls,
- literals = foldl lits 0 cls,
- symbols = foldl syms 0 cls,
- typedSymbols = foldl typedSyms 0 cls}
+ literals = List.foldl lits 0 cls,
+ symbols = List.foldl syms 0 cls,
+ typedSymbols = List.foldl typedSyms 0 cls}
end;
fun freeVars {axioms,conjecture} =
--- a/src/Tools/Metis/src/Proof.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Proof.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Proof =
--- a/src/Tools/Metis/src/Proof.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Proof.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Proof :> Proof =
@@ -39,40 +39,40 @@
fun ppSubst ppThm (sub,thm) =
Print.sequence (Print.addBreak 1)
(Print.blockProgram Print.Inconsistent 1
- [Print.addString "{",
+ [Print.ppString "{",
Print.ppOp2 " =" Print.ppString Subst.pp ("sub",sub),
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.ppOp2 " =" Print.ppString ppThm ("thm",thm),
- Print.addString "}"]);
+ Print.ppString "}"]);
fun ppResolve ppThm (res,pos,neg) =
Print.sequence (Print.addBreak 1)
(Print.blockProgram Print.Inconsistent 1
- [Print.addString "{",
+ [Print.ppString "{",
Print.ppOp2 " =" Print.ppString Atom.pp ("res",res),
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.ppOp2 " =" Print.ppString ppThm ("pos",pos),
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.ppOp2 " =" Print.ppString ppThm ("neg",neg),
- Print.addString "}"]);
+ Print.ppString "}"]);
fun ppRefl tm = Print.sequence (Print.addBreak 1) (Term.pp tm);
fun ppEquality (lit,path,res) =
Print.sequence (Print.addBreak 1)
(Print.blockProgram Print.Inconsistent 1
- [Print.addString "{",
+ [Print.ppString "{",
Print.ppOp2 " =" Print.ppString Literal.pp ("lit",lit),
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.ppOp2 " =" Print.ppString Term.ppPath ("path",path),
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.ppOp2 " =" Print.ppString Term.pp ("res",res),
- Print.addString "}"]);
+ Print.ppString "}"]);
fun ppInf ppAxiom ppThm inf =
let
@@ -80,7 +80,7 @@
in
Print.block Print.Inconsistent 2
(Print.sequence
- (Print.addString infString)
+ (Print.ppString infString)
(case inf of
Axiom cl => ppAxiom cl
| Assume x => ppAssume x
@@ -106,7 +106,7 @@
val prf = enumerate prf
fun ppThm th =
- Print.addString
+ Print.ppString
let
val cl = Thm.clause th
@@ -123,7 +123,7 @@
in
Print.sequence
(Print.blockProgram Print.Consistent (1 + size s)
- [Print.addString (s ^ " "),
+ [Print.ppString (s ^ " "),
Thm.pp th,
Print.addBreak 2,
Print.ppBracket "[" "]" (ppInf (K Print.skip) ppThm) inf])
@@ -131,10 +131,10 @@
end
in
Print.blockProgram Print.Consistent 0
- [Print.addString "START OF PROOF",
+ [Print.ppString "START OF PROOF",
Print.addNewline,
Print.program (map ppStep prf),
- Print.addString "END OF PROOF"]
+ Print.ppString "END OF PROOF"]
end
(*MetisDebug
handle Error err => raise Bug ("Proof.pp: shouldn't fail:\n" ^ err);
--- a/src/Tools/Metis/src/Random.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Random.sig Thu Sep 16 07:24:04 2010 +0200
@@ -8,6 +8,7 @@
signature Random =
sig
+
val nextWord : unit -> word
val nextBool : unit -> bool
--- a/src/Tools/Metis/src/Resolution.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Resolution.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Resolution =
--- a/src/Tools/Metis/src/Resolution.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Resolution.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE RESOLUTION PROOF PROCEDURE *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Resolution :> Resolution =
--- a/src/Tools/Metis/src/Rewrite.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Rewrite.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Rewrite =
--- a/src/Tools/Metis/src/Rewrite.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Rewrite.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ORDERED REWRITING FOR FIRST ORDER TERMS *)
-(* Copyright (c) 2003-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Rewrite :> Rewrite =
@@ -207,7 +207,7 @@
rw
end;
-val addList = foldl (fn (eqn,rw) => add rw eqn);
+val addList = List.foldl (fn (eqn,rw) => add rw eqn);
(* ------------------------------------------------------------------------- *)
(* Rewriting (the order must be a refinement of the rewrite order). *)
@@ -434,8 +434,9 @@
let
fun addSubterm b ((path,tm),net) = TermNet.insert net (tm,(id,b,path))
- val subterms = foldl (addSubterm true) subterms (Term.subterms l)
- val subterms = foldl (addSubterm false) subterms (Term.subterms r)
+ val subterms = List.foldl (addSubterm true) subterms (Term.subterms l)
+
+ val subterms = List.foldl (addSubterm false) subterms (Term.subterms r)
in
subterms
end;
@@ -660,7 +661,7 @@
in
fun orderedRewrite order ths =
let
- val rw = foldl addEqn (new order) (enumerate ths)
+ val rw = List.foldl addEqn (new order) (enumerate ths)
in
rewriteRule rw order
end;
--- a/src/Tools/Metis/src/Rule.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Rule =
--- a/src/Tools/Metis/src/Rule.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Rule :> Rule =
@@ -156,17 +156,19 @@
val noConv : conv = fn _ => raise Error "noConv";
+(*MetisDebug
fun traceConv s conv tm =
let
val res as (tm',th) = conv tm
- val () = print (s ^ ": " ^ Term.toString tm ^ " --> " ^
+ val () = trace (s ^ ": " ^ Term.toString tm ^ " --> " ^
Term.toString tm' ^ " " ^ Thm.toString th ^ "\n")
in
res
end
handle Error err =>
- (print (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n");
+ (trace (s ^ ": " ^ Term.toString tm ^ " --> Error: " ^ err ^ "\n");
raise Error (s ^ ": " ^ err));
+*)
fun thenConvTrans tm (tm',th1) (tm'',th2) =
let
@@ -455,7 +457,7 @@
val reflTh = Thm.refl (Term.Fn (f,xs))
val reflLit = Thm.destUnit reflTh
in
- fst (foldl cong (reflTh,reflLit) (enumerate ys))
+ fst (List.foldl cong (reflTh,reflLit) (enumerate ys))
end;
(* ------------------------------------------------------------------------- *)
@@ -482,7 +484,7 @@
val assumeLit = (false,(R,xs))
val assumeTh = Thm.assume assumeLit
in
- fst (foldl cong (assumeTh,assumeLit) (enumerate ys))
+ fst (List.foldl cong (assumeTh,assumeLit) (enumerate ys))
end;
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Set.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Set.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Set =
--- a/src/Tools/Metis/src/Set.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Set.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Set :> Set =
--- a/src/Tools/Metis/src/Sharing.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Sharing.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Sharing =
--- a/src/Tools/Metis/src/Sharing.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Sharing.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Sharing :> Sharing =
--- a/src/Tools/Metis/src/Stream.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Stream.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Stream =
--- a/src/Tools/Metis/src/Stream.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Stream.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,13 +1,11 @@
(* ========================================================================= *)
(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Stream :> Stream =
struct
-open Useful; (* MODIFIED by Jasmin Blanchette *)
-
val K = Useful.K;
val pair = Useful.pair;
@@ -201,9 +199,9 @@
fun listConcat s = concat (map fromList s);
-fun toString s = implode (toList s);
+fun toString s = String.implode (toList s);
-fun fromString s = fromList (explode s);
+fun fromString s = fromList (String.explode s);
fun toTextFile {filename = f} s =
let
--- a/src/Tools/Metis/src/Subst.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Subst.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Subst =
--- a/src/Tools/Metis/src/Subst.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Subst.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC SUBSTITUTIONS *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Subst :> Subst =
--- a/src/Tools/Metis/src/Subsume.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Subsume.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Subsume =
--- a/src/Tools/Metis/src/Subsume.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Subsume.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Subsume :> Subsume =
--- a/src/Tools/Metis/src/Term.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Term.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Term =
--- a/src/Tools/Metis/src/Term.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Term.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Term :> Term =
@@ -348,7 +348,7 @@
val isApp = can destApp;
-fun listMkApp (f,l) = foldl mkApp f l;
+fun listMkApp (f,l) = List.foldl mkApp f l;
local
fun strip tms tm =
@@ -368,38 +368,38 @@
val infixes =
(ref o Print.Infixes)
[(* ML symbols *)
- {token = " / ", precedence = 7, leftAssoc = true},
- {token = " div ", precedence = 7, leftAssoc = true},
- {token = " mod ", precedence = 7, leftAssoc = true},
- {token = " * ", precedence = 7, leftAssoc = true},
- {token = " + ", precedence = 6, leftAssoc = true},
- {token = " - ", precedence = 6, leftAssoc = true},
- {token = " ^ ", precedence = 6, leftAssoc = true},
- {token = " @ ", precedence = 5, leftAssoc = false},
- {token = " :: ", precedence = 5, leftAssoc = false},
- {token = " = ", precedence = 4, leftAssoc = true},
- {token = " <> ", precedence = 4, leftAssoc = true},
- {token = " <= ", precedence = 4, leftAssoc = true},
- {token = " < ", precedence = 4, leftAssoc = true},
- {token = " >= ", precedence = 4, leftAssoc = true},
- {token = " > ", precedence = 4, leftAssoc = true},
- {token = " o ", precedence = 3, leftAssoc = true},
- {token = " -> ", precedence = 2, leftAssoc = false}, (* inferred prec *)
- {token = " : ", precedence = 1, leftAssoc = false}, (* inferred prec *)
- {token = ", ", precedence = 0, leftAssoc = false}, (* inferred prec *)
+ {token = "/", precedence = 7, assoc = Print.LeftAssoc},
+ {token = "div", precedence = 7, assoc = Print.LeftAssoc},
+ {token = "mod", precedence = 7, assoc = Print.LeftAssoc},
+ {token = "*", precedence = 7, assoc = Print.LeftAssoc},
+ {token = "+", precedence = 6, assoc = Print.LeftAssoc},
+ {token = "-", precedence = 6, assoc = Print.LeftAssoc},
+ {token = "^", precedence = 6, assoc = Print.LeftAssoc},
+ {token = "@", precedence = 5, assoc = Print.RightAssoc},
+ {token = "::", precedence = 5, assoc = Print.RightAssoc},
+ {token = "=", precedence = 4, assoc = Print.NonAssoc},
+ {token = "<>", precedence = 4, assoc = Print.NonAssoc},
+ {token = "<=", precedence = 4, assoc = Print.NonAssoc},
+ {token = "<", precedence = 4, assoc = Print.NonAssoc},
+ {token = ">=", precedence = 4, assoc = Print.NonAssoc},
+ {token = ">", precedence = 4, assoc = Print.NonAssoc},
+ {token = "o", precedence = 3, assoc = Print.LeftAssoc},
+ {token = "->", precedence = 2, assoc = Print.RightAssoc},
+ {token = ":", precedence = 1, assoc = Print.NonAssoc},
+ {token = ",", precedence = 0, assoc = Print.RightAssoc},
(* Logical connectives *)
- {token = " /\\ ", precedence = ~1, leftAssoc = false},
- {token = " \\/ ", precedence = ~2, leftAssoc = false},
- {token = " ==> ", precedence = ~3, leftAssoc = false},
- {token = " <=> ", precedence = ~4, leftAssoc = false},
+ {token = "/\\", precedence = ~1, assoc = Print.RightAssoc},
+ {token = "\\/", precedence = ~2, assoc = Print.RightAssoc},
+ {token = "==>", precedence = ~3, assoc = Print.RightAssoc},
+ {token = "<=>", precedence = ~4, assoc = Print.RightAssoc},
(* Other symbols *)
- {token = " . ", precedence = 9, leftAssoc = true}, (* function app *)
- {token = " ** ", precedence = 8, leftAssoc = true},
- {token = " ++ ", precedence = 6, leftAssoc = true},
- {token = " -- ", precedence = 6, leftAssoc = true},
- {token = " == ", precedence = 4, leftAssoc = true}];
+ {token = ".", precedence = 9, assoc = Print.LeftAssoc},
+ {token = "**", precedence = 8, assoc = Print.LeftAssoc},
+ {token = "++", precedence = 6, assoc = Print.LeftAssoc},
+ {token = "--", precedence = 6, assoc = Print.LeftAssoc},
+ {token = "==", precedence = 4, assoc = Print.NonAssoc}];
(* The negation symbol *)
@@ -422,9 +422,14 @@
and neg = !negation
and bracks = !brackets
- val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
+ val bMap =
+ let
+ fun f (b1,b2) = (b1 ^ b2, b1, b2)
+ in
+ List.map f bracks
+ end
- val bTokens = map #2 bracks @ map #3 bracks
+ val bTokens = op@ (unzip bracks)
val iTokens = Print.tokensInfixes iOps
@@ -438,7 +443,15 @@
end
| _ => NONE
- val iPrinter = Print.ppInfixes iOps destI
+ fun isI tm = Option.isSome (destI tm)
+
+ fun iToken (_,tok) =
+ Print.program
+ [(if tok = "," then Print.skip else Print.ppString " "),
+ Print.ppString tok,
+ Print.addBreak 1];
+
+ val iPrinter = Print.ppInfixes iOps destI iToken
val specialTokens =
StringSet.addList iTokens (neg :: quants @ ["$","(",")"] @ bTokens)
@@ -466,8 +479,6 @@
fun functionName bv = Print.ppMap (checkFunctionName bv) Print.ppString
- fun isI tm = Option.isSome (destI tm)
-
fun stripNeg tm =
case tm of
Fn (f,[a]) =>
@@ -494,7 +505,7 @@
let
val s = Name.toString b
in
- case List.find (fn (n,_,_) => n = s) bracks of
+ case List.find (fn (n,_,_) => n = s) bMap of
NONE => NONE
| SOME (_,b1,b2) => SOME (b1,tm,b2)
end
@@ -527,11 +538,11 @@
val bv = StringSet.addList bv (map Name.toString (v :: vs))
in
Print.program
- [Print.addString q,
+ [Print.ppString q,
varName bv v,
Print.program
(map (Print.sequence (Print.addBreak 1) o varName bv) vs),
- Print.addString ".",
+ Print.ppString ".",
Print.addBreak 1,
innerQuant bv tm]
end
@@ -545,7 +556,7 @@
val (n,tm) = stripNeg tm
in
Print.blockProgram Print.Inconsistent n
- [Print.duplicate n (Print.addString neg),
+ [Print.duplicate n (Print.ppString neg),
if isI tm orelse (r andalso isQuant tm) then bracket bv tm
else quantifier bv tm]
end
@@ -571,31 +582,32 @@
val isAlphaNum =
let
- val alphaNumChars = explode "_'"
+ val alphaNumChars = String.explode "_'"
in
fn c => mem c alphaNumChars orelse Char.isAlphaNum c
end;
local
- val alphaNumToken = atLeastOne (some isAlphaNum) >> implode;
+ val alphaNumToken = atLeastOne (some isAlphaNum) >> String.implode;
val symbolToken =
let
fun isNeg c = str c = !negation
- val symbolChars = explode "<>=-*+/\\?@|!$%&#^:;~"
+ val symbolChars = String.explode "<>=-*+/\\?@|!$%&#^:;~"
fun isSymbol c = mem c symbolChars
fun isNonNegSymbol c = not (isNeg c) andalso isSymbol c
in
some isNeg >> str ||
- (some isNonNegSymbol ++ many (some isSymbol)) >> (implode o op::)
+ (some isNonNegSymbol ++ many (some isSymbol)) >>
+ (String.implode o op::)
end;
val punctToken =
let
- val punctChars = explode "()[]{}.,"
+ val punctChars = String.explode "()[]{}.,"
fun isPunct c = mem c punctChars
in
@@ -627,8 +639,9 @@
val iTokens = Print.tokensInfixes iOps
- val iParser =
- parseInfixes iOps (fn (f,a,b) => Fn (Name.fromString f, [a,b]))
+ fun iMk (f,a,b) = Fn (Name.fromString f, [a,b])
+
+ val iParser = parseInfixes iOps iMk any
val specialTokens =
StringSet.addList iTokens (neg :: quants @ ["$"] @ bTokens)
@@ -667,7 +680,7 @@
some (Useful.equal ".")) >>++
(fn (_,(vs,_)) =>
term (StringSet.addList bv vs) >>
- (fn body => foldr bind body vs))
+ (fn body => List.foldr bind body vs))
end
in
var ||
@@ -696,7 +709,7 @@
in
fun fromString input =
let
- val chars = Stream.fromList (explode input)
+ val chars = Stream.fromList (String.explode input)
val tokens = everything (lexer >> singleton) chars
@@ -709,7 +722,8 @@
end;
local
- val antiquotedTermToString = Print.toString (Print.ppBracket "(" ")" pp);
+ val antiquotedTermToString =
+ Print.toString (Print.ppBracket "(" ")" pp);
in
val parse = Parse.parseQuotation antiquotedTermToString fromString;
end;
--- a/src/Tools/Metis/src/TermNet.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/TermNet.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature TermNet =
--- a/src/Tools/Metis/src/TermNet.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/TermNet.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure TermNet :> TermNet =
@@ -158,7 +158,7 @@
fun null net = size net = 0;
-fun singles qtms a = foldr Single a qtms;
+fun singles qtms a = List.foldr Single a qtms;
local
fun pre NONE = (0,NONE)
@@ -188,7 +188,7 @@
handle Error _ => raise Bug "TermNet.insert: should never fail";
end;
-fun fromList parm l = foldl (fn (tm_a,n) => insert n tm_a) (new parm) l;
+fun fromList parm l = List.foldl (fn (tm_a,n) => insert n tm_a) (new parm) l;
fun filter pred =
let
@@ -441,7 +441,7 @@
local
fun inc (qtm, Result l, acc) =
- foldl (fn ((n,a),acc) => (n,(qtm,a)) :: acc) acc l
+ List.foldl (fn ((n,a),acc) => (n,(qtm,a)) :: acc) acc l
| inc _ = raise Bug "TermNet.pp.inc";
fun toList (Net (_,_,NONE)) = []
--- a/src/Tools/Metis/src/Thm.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Thm.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Thm =
--- a/src/Tools/Metis/src/Thm.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Thm.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Thm :> Thm =
@@ -111,7 +111,7 @@
in
fun pp th =
Print.blockProgram Print.Inconsistent 3
- [Print.addString "|- ",
+ [Print.ppString "|- ",
Formula.pp (toFormula th)];
end;
--- a/src/Tools/Metis/src/Tptp.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Tptp.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE TPTP PROBLEM FILE FORMAT *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Tptp =
--- a/src/Tools/Metis/src/Tptp.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Tptp.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE TPTP PROBLEM FILE FORMAT *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Tptp :> Tptp =
@@ -158,7 +158,7 @@
fun isTptpChar #"_" = true
| isTptpChar c = Char.isAlphaNum c;
- fun isTptpName l s = nonEmptyPred (existsPred l) (explode s);
+ fun isTptpName l s = nonEmptyPred (existsPred l) (String.explode s);
fun isRegular (c,cs) =
Char.isLower c andalso List.all isTptpChar cs;
@@ -175,14 +175,14 @@
fun mkTptpVarName s =
let
val s =
- case List.filter isTptpChar (explode s) of
+ case List.filter isTptpChar (String.explode s) of
[] => [#"X"]
| l as c :: cs =>
if Char.isUpper c then l
else if Char.isLower c then Char.toUpper c :: cs
else #"X" :: l
in
- implode s
+ String.implode s
end;
val isTptpConstName = isTptpName [isRegular,isNumber,isDefined,isSystem]
@@ -615,10 +615,10 @@
let
val s = varToTptp mapping v
in
- Print.addString s
+ Print.ppString s
end;
-fun ppFnName mapping fa = Print.addString (fnToTptp mapping fa);
+fun ppFnName mapping fa = Print.ppString (fnToTptp mapping fa);
fun ppConst mapping c = ppFnName mapping (c,0);
@@ -633,14 +633,14 @@
| a =>
Print.blockProgram Print.Inconsistent 2
[ppFnName mapping (f,a),
- Print.addString "(",
+ Print.ppString "(",
Print.ppOpList "," term tms,
- Print.addString ")"]
+ Print.ppString ")"]
in
Print.block Print.Inconsistent 0 o term
end;
-fun ppRelName mapping ra = Print.addString (relToTptp mapping ra);
+fun ppRelName mapping ra = Print.ppString (relToTptp mapping ra);
fun ppProp mapping p = ppRelName mapping (p,0);
@@ -650,12 +650,12 @@
| a =>
Print.blockProgram Print.Inconsistent 2
[ppRelName mapping (r,a),
- Print.addString "(",
+ Print.ppString "(",
Print.ppOpList "," (ppTerm mapping) tms,
- Print.addString ")"];
+ Print.ppString ")"];
local
- val neg = Print.sequence (Print.addString "~") (Print.addBreak 1);
+ val neg = Print.sequence (Print.ppString "~") (Print.addBreak 1);
fun fof mapping fm =
case fm of
@@ -672,8 +672,8 @@
and unitary mapping fm =
case fm of
- Formula.True => Print.addString "$true"
- | Formula.False => Print.addString "$false"
+ Formula.True => Print.ppString "$true"
+ | Formula.False => Print.ppString "$false"
| Formula.Forall _ => quantified mapping ("!", Formula.stripForall fm)
| Formula.Exists _ => quantified mapping ("?", Formula.stripExists fm)
| Formula.Not _ =>
@@ -693,21 +693,21 @@
| NONE => ppAtom mapping atm)
| _ =>
Print.blockProgram Print.Inconsistent 1
- [Print.addString "(",
+ [Print.ppString "(",
fof mapping fm,
- Print.addString ")"]
+ Print.ppString ")"]
and quantified mapping (q,(vs,fm)) =
let
val mapping = addVarListMapping mapping vs
in
Print.blockProgram Print.Inconsistent 2
- [Print.addString q,
- Print.addString " ",
+ [Print.ppString q,
+ Print.ppString " ",
Print.blockProgram Print.Inconsistent (String.size q)
- [Print.addString "[",
+ [Print.ppString "[",
Print.ppOpList "," (ppVar mapping) vs,
- Print.addString "] :"],
+ Print.ppString "] :"],
Print.addBreak 1,
unitary mapping fm]
end;
@@ -735,7 +735,8 @@
infixr 7 >>
infixr 6 ||
- val alphaNumToken = atLeastOne (some isAlphaNum) >> (AlphaNum o implode);
+ val alphaNumToken =
+ atLeastOne (some isAlphaNum) >> (AlphaNum o String.implode);
val punctToken =
let
@@ -759,7 +760,7 @@
some (not o stopOn) >> singleton
in
exactChar #"'" ++ many quotedParser ++ exactChar #"'" >>
- (fn (_,(l,_)) => Quote (implode (List.concat l)))
+ (fn (_,(l,_)) => Quote (String.implode (List.concat l)))
end;
val lexToken = alphaNumToken || punctToken || quoteToken;
@@ -779,7 +780,7 @@
let
fun funcs (lit,acc) = NameAritySet.union (functionsLiteral lit) acc
in
- foldl funcs NameAritySet.empty
+ List.foldl funcs NameAritySet.empty
end;
val clauseRelations =
@@ -789,14 +790,14 @@
NONE => acc
| SOME r => NameAritySet.add acc r
in
- foldl rels NameAritySet.empty
+ List.foldl rels NameAritySet.empty
end;
val clauseFreeVars =
let
fun fvs (lit,acc) = NameSet.union (freeVarsLiteral lit) acc
in
- foldl fvs NameSet.empty
+ List.foldl fvs NameSet.empty
end;
fun clauseSubst sub lits = map (literalSubst sub) lits;
@@ -1013,7 +1014,7 @@
fun ppLiteralInf mapping (pol,atm) =
Print.sequence
- (if pol then Print.skip else Print.addString "~ ")
+ (if pol then Print.skip else Print.ppString "~ ")
(ppAtomInf mapping atm);
in
fun ppProofTerm mapping =
@@ -1032,7 +1033,7 @@
fun ppProof mapping inf =
Print.blockProgram Print.Inconsistent 1
- [Print.addString "[",
+ [Print.ppString "[",
(case inf of
Proof.Axiom _ => Print.skip
| Proof.Assume atm => ppProofAtom mapping atm
@@ -1042,13 +1043,13 @@
| Proof.Equality (lit,path,tm) =>
Print.program
[ppProofLiteral mapping lit,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppProofPath path,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppProofTerm mapping tm]),
- Print.addString "]"];
+ Print.ppString "]"];
val ppParent = ppFormulaName;
@@ -1073,16 +1074,16 @@
val name = nameStrip inference
in
Print.blockProgram Print.Inconsistent (size gen + 1)
- [Print.addString gen,
- Print.addString "(",
- Print.addString name,
- Print.addString ",",
+ [Print.ppString gen,
+ Print.ppString "(",
+ Print.ppString name,
+ Print.ppString ",",
Print.addBreak 1,
Print.ppBracket "[" "]" (ppStrip mapping) inference,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.ppList ppParent parents,
- Print.addString ")"]
+ Print.ppString ")"]
end
| NormalizeFormulaSource {inference,parents} =>
let
@@ -1091,16 +1092,16 @@
val name = nameNormalize inference
in
Print.blockProgram Print.Inconsistent (size gen + 1)
- [Print.addString gen,
- Print.addString "(",
- Print.addString name,
- Print.addString ",",
+ [Print.ppString gen,
+ Print.ppString "(",
+ Print.ppString name,
+ Print.ppString ",",
Print.addBreak 1,
Print.ppBracket "[" "]" (ppNormalize mapping) inference,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.ppList ppParent parents,
- Print.addString ")"]
+ Print.ppString ")"]
end
| ProofFormulaSource {inference,parents} =>
let
@@ -1121,28 +1122,28 @@
end
in
Print.blockProgram Print.Inconsistent (size gen + 1)
- ([Print.addString gen,
- Print.addString "("] @
+ ([Print.ppString gen,
+ Print.ppString "("] @
(if isTaut then
- [Print.addString "tautology",
- Print.addString ",",
+ [Print.ppString "tautology",
+ Print.ppString ",",
Print.addBreak 1,
Print.blockProgram Print.Inconsistent 1
- [Print.addString "[",
- Print.addString name,
- Print.addString ",",
+ [Print.ppString "[",
+ Print.ppString name,
+ Print.ppString ",",
Print.addBreak 1,
ppProof mapping inference,
- Print.addString "]"]]
+ Print.ppString "]"]]
else
- [Print.addString name,
- Print.addString ",",
+ [Print.ppString name,
+ Print.ppString ",",
Print.addBreak 1,
ppProof mapping inference,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.ppList (ppProofParent mapping) parents]) @
- [Print.addString ")"])
+ [Print.ppString ")"])
end
end;
@@ -1208,14 +1209,14 @@
let
fun funcs (fm,acc) = NameAritySet.union (functionsFormula fm) acc
in
- foldl funcs NameAritySet.empty
+ List.foldl funcs NameAritySet.empty
end;
val formulasRelations =
let
fun rels (fm,acc) = NameAritySet.union (relationsFormula fm) acc
in
- foldl rels NameAritySet.empty
+ List.foldl rels NameAritySet.empty
end;
fun isCnfConjectureFormula fm =
@@ -1244,24 +1245,24 @@
| FofFormulaBody _ => "fof"
in
Print.blockProgram Print.Inconsistent (size gen + 1)
- ([Print.addString gen,
- Print.addString "(",
+ ([Print.ppString gen,
+ Print.ppString "(",
ppFormulaName name,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppRole role,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
Print.blockProgram Print.Consistent 1
- [Print.addString "(",
+ [Print.ppString "(",
ppFormulaBody mapping body,
- Print.addString ")"]] @
+ Print.ppString ")"]] @
(if isNoFormulaSource source then []
else
- [Print.addString ",",
+ [Print.ppString ",",
Print.addBreak 1,
ppFormulaSource mapping source]) @
- [Print.addString ")."])
+ [Print.ppString ")."])
end;
fun formulaToString mapping = Print.toString (ppFormula mapping);
@@ -1285,7 +1286,7 @@
val stringParser = lowerParser || upperParser;
- val numberParser = someAlphaNum (List.all Char.isDigit o explode);
+ val numberParser = someAlphaNum (List.all Char.isDigit o String.explode);
fun somePunct p =
maybe (fn Punct c => if p c then SOME c else NONE | _ => NONE);
@@ -1299,7 +1300,7 @@
| f [x] = x
| f (h :: t) = (h ++ f t) >> K ();
in
- fun symbolParser s = f (map punctParser (explode s));
+ fun symbolParser s = f (map punctParser (String.explode s));
end;
val definedParser =
@@ -1641,9 +1642,9 @@
fun ppInclude i =
Print.blockProgram Print.Inconsistent 2
- [Print.addString "include('",
- Print.addString i,
- Print.addString "')."];
+ [Print.ppString "include('",
+ Print.ppString i,
+ Print.ppString "')."];
val includeToString = Print.toString ppInclude;
@@ -1745,8 +1746,8 @@
fun destLineComment cs =
case cs of
[] => ""
- | #"%" :: #" " :: rest => implode rest
- | #"%" :: rest => implode rest
+ | #"%" :: #" " :: rest => String.implode rest
+ | #"%" :: rest => String.implode rest
| _ => raise Error "Tptp.destLineComment";
val isLineComment = can destLineComment;
--- a/src/Tools/Metis/src/Units.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Units.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Units =
--- a/src/Tools/Metis/src/Units.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Units.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* A STORE FOR UNIT THEOREMS *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Units :> Units =
@@ -47,7 +47,7 @@
end
end;
-val addList = foldl (fn (th,u) => add u th);
+val addList = List.foldl (fn (th,u) => add u th);
(* ------------------------------------------------------------------------- *)
(* Matching. *)
--- a/src/Tools/Metis/src/Useful.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Useful =
@@ -22,8 +22,6 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val print : string -> unit (* MODIFIED by Jasmin Blanchette *)
-
val tracePrint : (string -> unit) ref
val trace : string -> unit
@@ -109,10 +107,6 @@
(* Lists: note we count elements from 0. *)
(* ------------------------------------------------------------------------- *)
-val foldl : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b (* MODIFIED by Jasmin Blanchette *)
-
-val foldr : ('a * 'b -> 'b) -> 'b -> 'a list -> 'b (* MODIFIED by Jasmin Blanchette *)
-
val cons : 'a -> 'a list -> 'a list
val hdTl : 'a list -> 'a * 'a list
@@ -217,10 +211,6 @@
(* Strings. *)
(* ------------------------------------------------------------------------- *)
-val implode : char list -> string (* MODIFIED by Jasmin Blanchette *)
-
-val explode : string -> char list (* MODIFIED by Jasmin Blanchette *)
-
val rot : int -> char -> char
val charToInt : char -> int option
@@ -323,7 +313,9 @@
val try : ('a -> 'b) -> 'a -> 'b
-val chat : string -> unit
+val chat : string -> unit (* stdout *)
+
+val chide : string -> unit (* stderr *)
val warn : string -> unit
--- a/src/Tools/Metis/src/Useful.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Useful :> Useful =
@@ -50,9 +50,7 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val print = TextIO.print; (* MODIFIED by Jasmin Blanchette *)
-
-val tracePrint = ref print;
+val tracePrint = ref TextIO.print;
fun trace mesg = !tracePrint mesg;
@@ -172,10 +170,6 @@
(* Lists. *)
(* ------------------------------------------------------------------------- *)
-val foldl = List.foldl; (* MODIFIED by Jasmin Blanchette *)
-
-val foldr = List.foldr; (* MODIFIED by Jasmin Blanchette *)
-
fun cons x y = x :: y;
fun hdTl l = (hd l, tl l);
@@ -211,19 +205,22 @@
fun zip xs ys = zipWith pair xs ys;
-fun unzip ab =
- foldl (fn ((x, y), (xs, ys)) => (x :: xs, y :: ys)) ([], []) (rev ab);
+local
+ fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
+in
+ fun unzip ab = List.foldl inc ([],[]) (rev ab);
+end;
fun cartwith f =
- let
- fun aux _ res _ [] = res
- | aux xsCopy res [] (y :: yt) = aux xsCopy res xsCopy yt
- | aux xsCopy res (x :: xt) (ys as y :: _) =
- aux xsCopy (f x y :: res) xt ys
- in
- fn xs => fn ys =>
- let val xs' = rev xs in aux xs' [] xs' (rev ys) end
- end;
+ let
+ fun aux _ res _ [] = res
+ | aux xsCopy res [] (y :: yt) = aux xsCopy res xsCopy yt
+ | aux xsCopy res (x :: xt) (ys as y :: _) =
+ aux xsCopy (f x y :: res) xt ys
+ in
+ fn xs => fn ys =>
+ let val xs' = rev xs in aux xs' [] xs' (rev ys) end
+ end;
fun cart xs ys = cartwith pair xs ys;
@@ -342,15 +339,32 @@
fun delete x s = List.filter (not o equal x) s;
-fun setify s = rev (foldl (fn (v,x) => if mem v x then x else v :: x) [] s);
+local
+ fun inc (v,x) = if mem v x then x else v :: x;
+in
+ fun setify s = rev (List.foldl inc [] s);
+end;
-fun union s t = foldl (fn (v,x) => if mem v t then x else v :: x) t (rev s);
+fun union s t =
+ let
+ fun inc (v,x) = if mem v t then x else v :: x
+ in
+ List.foldl inc t (rev s)
+ end;
fun intersect s t =
- foldl (fn (v,x) => if mem v t then v :: x else x) [] (rev s);
+ let
+ fun inc (v,x) = if mem v t then v :: x else x
+ in
+ List.foldl inc [] (rev s)
+ end;
fun difference s t =
- foldl (fn (v,x) => if mem v t then x else v :: x) [] (rev s);
+ let
+ fun inc (v,x) = if mem v t then x else v :: x
+ in
+ List.foldl inc [] (rev s)
+ end;
fun subset s t = List.all (fn x => mem x t) s;
@@ -460,8 +474,7 @@
val primesList = ref [2];
in
- (* MODIFIED by Jasmin Blanchette *)
- fun primes n = CRITICAL (fn () =>
+ fun primes n =
let
val ref ps = primesList
@@ -476,11 +489,10 @@
in
ps
end
- end);
+ end;
end;
-(* MODIFIED by Jasmin Blanchette *)
-fun primesUpTo n = CRITICAL (fn () =>
+fun primesUpTo n =
let
fun f k =
let
@@ -492,22 +504,18 @@
end
in
f 8
- end);
+ end;
(* ------------------------------------------------------------------------- *)
(* Strings. *)
(* ------------------------------------------------------------------------- *)
-val implode = String.implode (* MODIFIED by Jasmin Blanchette *)
-
-val explode = String.explode (* MODIFIED by Jasmin Blanchette *)
-
local
fun len l = (length l, l)
- val upper = len (explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
+ val upper = len (String.explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
- val lower = len (explode "abcdefghijklmnopqrstuvwxyz");
+ val lower = len (String.explode "abcdefghijklmnopqrstuvwxyz");
fun rotate (n,l) c k =
List.nth (l, (k + Option.valOf (index (equal c) l)) mod n);
@@ -546,7 +554,7 @@
let
fun dup 0 l = l | dup n l = dup (n - 1) (x :: l)
in
- fn n => implode (dup n [])
+ fn n => String.implode (dup n [])
end;
fun chomp s =
@@ -558,14 +566,15 @@
end;
local
- fun chop [] = []
- | chop (l as (h :: t)) = if Char.isSpace h then chop t else l;
+ fun chop l =
+ case l of
+ [] => []
+ | h :: t => if Char.isSpace h then chop t else l;
in
- val trim = implode o chop o rev o chop o rev o explode;
+ val trim = String.implode o chop o rev o chop o rev o String.explode;
end;
-fun join _ [] = ""
- | join s (h :: t) = foldl (fn (x,y) => y ^ s ^ x) h t;
+val join = String.concatWith;
local
fun match [] l = SOME l
@@ -573,18 +582,19 @@
| match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
fun stringify acc [] = acc
- | stringify acc (h :: t) = stringify (implode h :: acc) t;
+ | stringify acc (h :: t) = stringify (String.implode h :: acc) t;
in
fun split sep =
let
val pat = String.explode sep
+
fun div1 prev recent [] = stringify [] (rev recent :: prev)
| div1 prev recent (l as h :: t) =
case match pat l of
NONE => div1 prev (h :: recent) t
| SOME rest => div1 (rev recent :: prev) [] rest
in
- fn s => div1 [] [] (explode s)
+ fn s => div1 [] [] (String.explode s)
end;
end;
@@ -714,24 +724,22 @@
local
val generator = ref 0
in
- (* MODIFIED by Jasmin Blanchette *)
- fun newInt () = CRITICAL (fn () =>
+ fun newInt () =
let
val n = !generator
val () = generator := n + 1
in
n
- end);
+ end;
fun newInts 0 = []
- (* MODIFIED by Jasmin Blanchette *)
- | newInts k = CRITICAL (fn () =>
+ | newInts k =
let
val n = !generator
val () = generator := n + k
in
interval n k
- end);
+ end;
end;
fun withRef (r,new) f x =
@@ -811,10 +819,12 @@
(* Profiling and error reporting. *)
(* ------------------------------------------------------------------------- *)
-fun chat s = TextIO.output (TextIO.stdErr, s ^ "\n");
+fun chat s = TextIO.output (TextIO.stdOut, s ^ "\n");
+
+fun chide s = TextIO.output (TextIO.stdErr, s ^ "\n");
local
- fun err x s = chat (x ^ ": " ^ s);
+ fun err x s = chide (x ^ ": " ^ s);
in
fun try f x = f x
handle e as Error _ => (err "try" (errorToString e); raise e)
--- a/src/Tools/Metis/src/Waiting.sig Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Waiting.sig Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
signature Waiting =
--- a/src/Tools/Metis/src/Waiting.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/Waiting.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE WAITING SET OF CLAUSES *)
-(* Copyright (c) 2002-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
structure Waiting :> Waiting =
@@ -40,17 +40,16 @@
(* ------------------------------------------------------------------------- *)
val defaultModels : modelParameters list =
- [(* MODIFIED by Jasmin Blanchette
- {model = Model.default,
+ [{model = Model.default,
initialPerturbations = 100,
maxChecks = SOME 20,
perturbations = 0,
- weight = 1.0} *)];
+ weight = 1.0}];
val default : parameters =
{symbolsWeight = 1.0,
- literalsWeight = (* 1.0 *) 0.0, (* MODIFIED by Jasmin Blanchette *)
- variablesWeight = (* 1.0 *) 0.0, (* MODIFIED by Jasmin Blanchette *)
+ literalsWeight = 1.0,
+ variablesWeight = 1.0,
models = defaultModels};
fun size (Waiting {clauses,...}) = Heap.size clauses;
@@ -163,7 +162,7 @@
val symbolsW = Math.pow (clauseSymbols lits, symbolsWeight)
val variablesW = Math.pow (clauseVariables lits, variablesWeight)
val literalsW = Math.pow (clauseLiterals lits, literalsWeight)
- val modelsW = (* checkModels models mods mcl *) 1.0 (* MODIFIED by Jasmin Blanchette *)
+ val modelsW = checkModels models mods mcl
(*MetisTrace4
val () = trace ("Waiting.clauseWeight: dist = " ^
Real.toString dist ^ "\n")
--- a/src/Tools/Metis/src/metis.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/metis.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,21 +1,6 @@
(* ========================================================================= *)
(* METIS FIRST ORDER PROVER *)
-(* *)
-(* Copyright (c) 2001 Joe Hurd *)
-(* *)
-(* Metis is free software; you can redistribute it and/or modify *)
-(* it under the terms of the GNU General Public License as published by *)
-(* the Free Software Foundation; either version 2 of the License, or *)
-(* (at your option) any later version. *)
-(* *)
-(* Metis is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU General Public License for more details. *)
-(* *)
-(* You should have received a copy of the GNU General Public License *)
-(* along with Metis; if not, write to the Free Software *)
-(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
open Useful;
@@ -26,9 +11,9 @@
val PROGRAM = "metis";
-val VERSION = "2.2";
+val VERSION = "2.3";
-val versionString = PROGRAM^" "^VERSION^" (release 20100825)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20100915)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)
@@ -146,11 +131,11 @@
local
fun display_sep () =
if notshowing_any () then ()
- else print (nChars #"-" (!Print.lineLength) ^ "\n");
+ else TextIO.print (nChars #"-" (!Print.lineLength) ^ "\n");
fun display_name filename =
if notshowing "name" then ()
- else print ("Problem: " ^ filename ^ "\n\n");
+ else TextIO.print ("Problem: " ^ filename ^ "\n\n");
fun display_goal tptp =
if notshowing "goal" then ()
@@ -158,12 +143,12 @@
let
val goal = Tptp.goal tptp
in
- print ("Goal:\n" ^ Formula.toString goal ^ "\n\n")
+ TextIO.print ("Goal:\n" ^ Formula.toString goal ^ "\n\n")
end;
fun display_clauses cls =
if notshowing "clauses" then ()
- else print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n");
+ else TextIO.print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n");
fun display_size cls =
if notshowing "size" then ()
@@ -174,7 +159,7 @@
val {clauses,literals,symbols,typedSymbols} = Problem.size cls
in
- print
+ TextIO.print
("Size: " ^
plural clauses "clause" ^ ", " ^
plural literals "literal" ^ ", " ^
@@ -188,12 +173,12 @@
let
val cat = Problem.categorize cls
in
- print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n")
+ TextIO.print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n")
end;
local
fun display_proof_start filename =
- print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n");
+ TextIO.print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n");
fun display_proof_body problem proofs =
let
@@ -224,7 +209,7 @@
end;
fun display_proof_end filename =
- print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n");
+ TextIO.print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n");
in
fun display_proof filename problem proofs =
if notshowing "proof" then ()
@@ -264,17 +249,24 @@
filename = "saturation.tptp"}
end
*)
- val () = print ("\nSZS output start Saturation for " ^ filename ^ "\n")
- val () = app (fn th => print (Thm.toString th ^ "\n")) ths
- val () = print ("SZS output end Saturation for " ^ filename ^ "\n\n")
+ val () =
+ TextIO.print
+ ("\nSZS output start Saturation for " ^ filename ^ "\n")
+
+ val () = app (fn th => TextIO.print (Thm.toString th ^ "\n")) ths
+
+ val () =
+ TextIO.print
+ ("SZS output end Saturation for " ^ filename ^ "\n\n")
in
()
end;
fun display_status filename status =
if notshowing "status" then ()
- else print ("SZS status " ^ Tptp.toStringStatus status ^
- " for " ^ filename ^ "\n");
+ else
+ TextIO.print ("SZS status " ^ Tptp.toStringStatus status ^
+ " for " ^ filename ^ "\n");
fun display_problem filename cls =
let
--- a/src/Tools/Metis/src/problems.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/problems.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
(* ========================================================================= *)
--- a/src/Tools/Metis/src/problems2tptp.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/problems2tptp.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
open Useful;
@@ -39,7 +39,7 @@
dups names
end;
-fun listProblem {name, comments = _, goal = _} = print (name ^ "\n");
+fun listProblem {name, comments = _, goal = _} = TextIO.print (name ^ "\n");
fun outputProblem outputDir {name,comments,goal} =
let
--- a/src/Tools/Metis/src/selftest.sml Wed Sep 15 22:24:35 2010 +0200
+++ b/src/Tools/Metis/src/selftest.sml Thu Sep 16 07:24:04 2010 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* METIS TESTS *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
@@ -52,11 +52,11 @@
| partialOrderToString NONE = "NONE";
fun SAY s =
- print
+ TextIO.print
("-------------------------------------" ^
"-------------------------------------\n" ^ s ^ "\n\n");
-fun printval p x = (print (Print.toString p x ^ "\n\n"); x);
+fun printval p x = (TextIO.print (Print.toString p x ^ "\n\n"); x);
fun mkCl p th = Clause.mk {parameters = p, id = Clause.newId (), thm = th};
@@ -92,12 +92,13 @@
fun test_fun eq p r a =
if eq r a then p a ^ "\n" else
- (print ("\n\n" ^
- "test: should have\n-->" ^ p r ^ "<--\n\n" ^
- "test: actually have\n-->" ^ p a ^ "<--\n\n");
+ (TextIO.print
+ ("\n\n" ^
+ "test: should have\n-->" ^ p r ^ "<--\n\n" ^
+ "test: actually have\n-->" ^ p a ^ "<--\n\n");
raise Fail "test: failed a test");
-fun test eq p r a = print (test_fun eq p r a ^ "\n");
+fun test eq p r a = TextIO.print (test_fun eq p r a ^ "\n");
val test_tm = test Term.equal Term.toString o Term.parse;
@@ -123,7 +124,7 @@
(fn s => test_fun equal I s ((mini_print n o Formula.fromString) s))
(prep q);
-fun test_pp q = print (testlen_pp 40 q ^ "\n");
+fun test_pp q = TextIO.print (testlen_pp 40 q ^ "\n");
val () = test_pp `3 = f x`;
@@ -568,7 +569,7 @@
val rows = alignTable format table
- val () = print (join "\n" rows ^ "\n\n")
+ val () = TextIO.print (join "\n" rows ^ "\n\n")
in
()
end;
@@ -626,8 +627,8 @@
val fm = LiteralSet.disjoin cl
in
Print.blockProgram Print.Consistent ind
- [Print.addString p,
- Print.addString (nChars #" " (ind - size p)),
+ [Print.ppString p,
+ Print.ppString (nChars #" " (ind - size p)),
Formula.pp fm]
end;
@@ -1108,13 +1109,19 @@
val _ =
test_fun equal I g (mini_print (!Print.lineLength) p)
- handle e => (print ("Error in problem " ^ name ^ "\n\n"); raise e)
+ handle e =>
+ (TextIO.print ("Error in problem " ^ name ^ "\n\n");
+ raise e)
in
(name,p) :: acc
end;
in
fun check_syntax (p : problem list) =
- (foldl check [] p; print "ok\n\n");
+ let
+ val _ = List.foldl check [] p
+ in
+ TextIO.print "ok\n\n"
+ end;
end;
val () = check_syntax problems;
@@ -1125,11 +1132,11 @@
fun tptp f =
let
- val () = print ("parsing " ^ f ^ "... ")
+ val () = TextIO.print ("parsing " ^ f ^ "... ")
val filename = "tptp/" ^ f ^ ".tptp"
val mapping = Tptp.defaultMapping
val goal = Tptp.goal (Tptp.read {filename = filename, mapping = mapping})
- val () = print "ok\n"
+ val () = TextIO.print "ok\n"
in
pvFm goal
end;