# HG changeset patch # User blanchet # Date 1284614644 -7200 # Node ID e330437cd22a55bbcf47b5998ac45a14d5b59fb1 # Parent 844a9ec448584fffaa684e4ad39c1e7f68d75289 copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/Makefile --- 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: diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/scripts/mlpp --- 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; diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Active.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Active.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Atom.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Atom.sml --- 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; (* ------------------------------------------------------------------------- *) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/AtomNet.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/AtomNet.sml --- 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; diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Clause.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Clause.sml --- 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); diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/ElementSet.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/ElementSet.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Formula.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Formula.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Heap.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Heap.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/KeyMap.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/KeyMap.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/KnuthBendixOrder.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/KnuthBendixOrder.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Lazy.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Lazy.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Literal.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Literal.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/LiteralNet.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/LiteralNet.sml --- 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, diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Map.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Map.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Model.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Model.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Name.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Name.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/NameArity.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/NameArity.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Normalize.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Normalize.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Options.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Options.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Ordered.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Ordered.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Parse.sig --- 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. *) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Parse.sml --- 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; diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Portable.sig --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/PortableMlton.sml --- 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 (* ------------------------------------------------------------------------- *) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/PortableMosml.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/PortablePolyml.sml --- 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 (* ------------------------------------------------------------------------- *) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Print.sig --- 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. *) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Print.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Problem.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Problem.sml --- 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} = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Proof.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Proof.sml --- 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); diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Random.sig --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Resolution.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Resolution.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Rewrite.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Rewrite.sml --- 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; diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Rule.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Rule.sml --- 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; (* ------------------------------------------------------------------------- *) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Set.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Set.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Sharing.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Sharing.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Stream.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Stream.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Subst.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Subst.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Subsume.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Subsume.sml --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Term.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Term.sml --- 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; diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/TermNet.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/TermNet.sml --- 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)) = [] diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Thm.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Thm.sml --- 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; diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Tptp.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Tptp.sml --- 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; diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Units.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Units.sml --- 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. *) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Useful.sig --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Useful.sml --- 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) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Waiting.sig --- 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 = diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/Waiting.sml --- 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") diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/metis.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/problems.sml --- 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 *) (* ========================================================================= *) (* ========================================================================= *) diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/problems2tptp.sml --- 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 diff -r 844a9ec44858 -r e330437cd22a src/Tools/Metis/src/selftest.sml --- 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;