new version of Metis 2.3 (29 Dec. 2010)
--- a/src/Tools/Metis/Makefile Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/Makefile Thu Mar 24 17:49:27 2011 +0100
@@ -179,6 +179,12 @@
POLYML_OPTS =
+ifeq ($(shell uname), Darwin)
+ POLYML_LINK_OPTS = -lpolymain -lpolyml -segprot POLY rwx rwx
+else
+ POLYML_LINK_OPTS = -lpolymain -lpolyml
+endif
+
POLYML_SRC = \
src/Random.sig src/Random.sml \
src/Portable.sig src/PortablePolyml.sml \
@@ -205,7 +211,7 @@
@echo '*****************************'
@echo
@echo $@
- cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) -lpolymain -lpolyml
+ cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) $(POLYML_LINK_OPTS)
@echo
.PHONY: polyml-info
--- a/src/Tools/Metis/metis.ML Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/metis.ML Thu Mar 24 17:49:27 2011 +0100
@@ -555,7 +555,20 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val tracePrint = Unsynchronized.ref TextIO.print;
+local
+ val traceOut = TextIO.stdOut;
+
+ fun tracePrintFn mesg =
+ let
+ val () = TextIO.output (traceOut,mesg)
+
+ val () = TextIO.flushOut traceOut
+ in
+ ()
+ end;
+in
+ val tracePrint = Unsynchronized.ref tracePrintFn;
+end;
fun trace mesg = !tracePrint mesg;
@@ -759,7 +772,7 @@
case l of
[] =>
let
- val acc = if null row then acc else rev row :: acc
+ val acc = if List.null row then acc else rev row :: acc
in
rev acc
end
@@ -788,9 +801,9 @@
local
fun fstEq ((x,_),(y,_)) = x = y;
- fun collapse l = (fst (hd l), map snd l);
-in
- fun groupsByFst l = map collapse (groupsBy fstEq l);
+ fun collapse l = (fst (hd l), List.map snd l);
+in
+ fun groupsByFst l = List.map collapse (groupsBy fstEq l);
end;
fun groupsOf n =
@@ -935,10 +948,10 @@
| sortMap f cmp xs =
let
fun ncmp ((m,_),(n,_)) = cmp (m,n)
- val nxs = map (fn x => (f x, x)) xs
+ val nxs = List.map (fn x => (f x, x)) xs
val nys = sort ncmp nxs
in
- map snd nys
+ List.map snd nys
end;
(* ------------------------------------------------------------------------- *)
@@ -1146,7 +1159,7 @@
fun alignColumn {leftAlign,padChar} column =
let
- val (n,_) = maximum Int.compare (map size column)
+ val (n,_) = maximum Int.compare (List.map size column)
fun pad entry row =
let
@@ -1162,13 +1175,18 @@
local
fun alignTab aligns rows =
case aligns of
- [] => map (K "") rows
- | [{leftAlign = true, padChar = #" "}] => map hd rows
+ [] => List.map (K "") rows
+ | [{leftAlign = true, padChar = #" "}] => List.map hd rows
| align :: aligns =>
- alignColumn align (map hd rows) (alignTab aligns (map tl rows));
+ let
+ val col = List.map hd rows
+ and cols = alignTab aligns (List.map tl rows)
+ in
+ alignColumn align col cols
+ end;
in
fun alignTable aligns rows =
- if null rows then [] else alignTab aligns rows;
+ if List.null rows then [] else alignTab aligns rows;
end;
(* ------------------------------------------------------------------------- *)
@@ -6599,6 +6617,8 @@
val ppPpstream : ppstream pp
+val ppException : exn pp
+
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
@@ -6689,7 +6709,7 @@
fun escapeString {escape} =
let
- val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
+ val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
fun escapeChar c =
case c of
@@ -6858,7 +6878,7 @@
let
val Block {indent = _, style = _, size, chunks} = block
- val empty = null chunks
+ val empty = List.null chunks
(*BasicDebug
val _ = not empty orelse size = 0 orelse
@@ -7430,7 +7450,7 @@
lines
end
in
- if null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
+ if List.null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
end;
in
fun execute {lineLength} =
@@ -7503,7 +7523,7 @@
fun ppOpA a = sequence (ppOp' s) (ppA a)
in
fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
+ | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
end;
fun ppOpStream' s ppA =
@@ -7655,6 +7675,8 @@
val ppPpstream = ppStream ppStep;
+fun ppException e = ppString (exnMessage e);
+
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
@@ -8258,9 +8280,9 @@
val newNames : int -> name list
-val variantPrime : (name -> bool) -> name -> name
-
-val variantNum : (name -> bool) -> name -> name
+val variantPrime : {avoid : name -> bool} -> name -> name
+
+val variantNum : {avoid : name -> bool} -> name -> name
(* ------------------------------------------------------------------------- *)
(* Parsing and pretty printing. *)
@@ -8311,22 +8333,21 @@
in
fun newName () = numName (newInt ());
- fun newNames n = map numName (newInts n);
-end;
-
-fun variantPrime acceptable =
- let
- fun variant n = if acceptable n then n else variant (n ^ "'")
+ fun newNames n = List.map numName (newInts n);
+end;
+
+fun variantPrime {avoid} =
+ let
+ fun variant n = if avoid n then variant (n ^ "'") else n
in
variant
end;
local
- fun isDigitOrPrime #"'" = true
- | isDigitOrPrime c = Char.isDigit c;
-in
- fun variantNum acceptable n =
- if acceptable n then n
+ fun isDigitOrPrime c = c = #"'" orelse Char.isDigit c;
+in
+ fun variantNum {avoid} n =
+ if not (avoid n) then n
else
let
val n = stripSuffix isDigitOrPrime n
@@ -8335,7 +8356,7 @@
let
val n_i = n ^ Int.toString i
in
- if acceptable n_i then n_i else variant (i + 1)
+ if avoid n_i then variant (i + 1) else n_i
end
in
variant 0
@@ -8878,7 +8899,7 @@
in
case tm of
Var _ => subtms rest acc
- | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
+ | Fn (_,args) => subtms (List.map f (enumerate args) @ rest) acc
end;
in
fun subterms tm = subtms [([],tm)] [];
@@ -8909,7 +8930,7 @@
Var _ => search rest
| Fn (_,a) =>
let
- val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
+ val subtms = List.map (fn (i,t) => (i :: path, t)) (enumerate a)
in
search (subtms @ rest)
end
@@ -8949,14 +8970,14 @@
fun newVar () = Var (Metis_Name.newName ());
-fun newVars n = map Var (Metis_Name.newNames n);
-
-local
- fun avoidAcceptable avoid n = not (Metis_NameSet.member n avoid);
-in
- fun variantPrime avoid = Metis_Name.variantPrime (avoidAcceptable avoid);
-
- fun variantNum avoid = Metis_Name.variantNum (avoidAcceptable avoid);
+fun newVars n = List.map Var (Metis_Name.newNames n);
+
+local
+ fun avoid av n = Metis_NameSet.member n av;
+in
+ fun variantPrime av = Metis_Name.variantPrime {avoid = avoid av};
+
+ fun variantNum av = Metis_Name.variantNum {avoid = avoid av};
end;
(* ------------------------------------------------------------------------- *)
@@ -9028,7 +9049,7 @@
val acc = (rev path, tm) :: acc
- val rest = map f (enumerate args) @ rest
+ val rest = List.map f (enumerate args) @ rest
in
subtms rest acc
end;
@@ -9237,7 +9258,7 @@
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- (functionName bv f :: map (functionArgument bv) args)
+ (functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm =
case destBrack tm of
@@ -9249,13 +9270,13 @@
NONE => term bv tm
| SOME (q,v,vs,tm) =>
let
- val bv = Metis_StringSet.addList bv (map Metis_Name.toString (v :: vs))
+ val bv = Metis_StringSet.addList bv (List.map Metis_Name.toString (v :: vs))
in
Metis_Print.program
[Metis_Print.ppString q,
varName bv v,
Metis_Print.program
- (map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
+ (List.map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
Metis_Print.ppString ".",
Metis_Print.addBreak 1,
innerQuant bv tm]
@@ -9342,9 +9363,9 @@
and neg = !negation
and bracks = ("(",")") :: !brackets
- val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
-
- val bTokens = map #2 bracks @ map #3 bracks
+ val bracks = List.map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
+
+ val bTokens = List.map #2 bracks @ List.map #3 bracks
fun possibleVarName "" = false
| possibleVarName s = isAlphaNum (String.sub (s,0))
@@ -9399,8 +9420,8 @@
in
var ||
const ||
- first (map bracket bracks) ||
- first (map quantifier quants)
+ first (List.map bracket bracks) ||
+ first (List.map quantifier quants)
end tokens
and molecule bv tokens =
@@ -10057,7 +10078,7 @@
fun subterms ((_,tms) : atom) =
let
- fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Metis_Term.subterms tm) @ l
+ fun f ((n,tm),l) = List.map (fn (p,s) => (n :: p, s)) (Metis_Term.subterms tm) @ l
in
List.foldl f [] (enumerate tms)
end;
@@ -10941,9 +10962,9 @@
fun promote (Metis_Term.Var v) = Metis_Atom (v,[])
| promote (Metis_Term.Fn (f,tms)) =
- if Metis_Name.equal f truthName andalso null tms then
+ if Metis_Name.equal f truthName andalso List.null tms then
True
- else if Metis_Name.equal f falsityName andalso null tms then
+ else if Metis_Name.equal f falsityName andalso List.null tms then
False
else if Metis_Name.toString f = !Metis_Term.negation andalso length tms = 1 then
Not (promote (hd tms))
@@ -10973,7 +10994,7 @@
local
fun add_asms asms goal =
- if null asms then goal else Imp (listMkConj (rev asms), goal);
+ if List.null asms then goal else Imp (listMkConj (rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
@@ -10987,7 +11008,7 @@
| (true, Imp (f1,f2)) => split (f1 :: asms) true f2
| (true, Iff (f1,f2)) =>
split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
- | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
+ | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f)
(* Negative splittables *)
| (false,False) => []
| (false, Not f) => split asms true f
@@ -10997,7 +11018,7 @@
| (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
| (false, Iff (f1,f2)) =>
split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
- | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
+ | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
(* Unsplittables *)
| _ => [add_asms asms (if pol then fm else Not fm)];
in
@@ -11750,7 +11771,7 @@
local
fun toFormula th =
Metis_Formula.listMkDisj
- (map Metis_Literal.toFormula (Metis_LiteralSet.toList (clause th)));
+ (List.map Metis_Literal.toFormula (Metis_LiteralSet.toList (clause th)));
in
fun pp th =
Metis_Print.blockProgram Metis_Print.Inconsistent 3
@@ -12057,7 +12078,7 @@
Metis_Print.blockProgram Metis_Print.Consistent 0
[Metis_Print.ppString "START OF PROOF",
Metis_Print.addNewline,
- Metis_Print.program (map ppStep prf),
+ Metis_Print.program (List.map ppStep prf),
Metis_Print.ppString "END OF PROOF"]
end
(*MetisDebug
@@ -12737,6 +12758,7 @@
else
let
val sub = Metis_Subst.fromList [(xVarName,x),(yVarName,y)]
+
val symTh = Metis_Thm.subst sub symmetry
in
Metis_Thm.resolve lit th symTh
@@ -12750,9 +12772,9 @@
type equation = (Metis_Term.term * Metis_Term.term) * Metis_Thm.thm;
-fun ppEquation (_,th) = Metis_Thm.pp th;
-
-fun equationToString x = Metis_Print.toString ppEquation x;
+fun ppEquation ((_,th) : equation) = Metis_Thm.pp th;
+
+val equationToString = Metis_Print.toString ppEquation;
fun equationLiteral (t_u,th) =
let
@@ -12866,7 +12888,7 @@
fun rewrConv (eqn as ((x,y), eqTh)) path tm =
if Metis_Term.equal x y then allConv tm
- else if null path then (y,eqTh)
+ else if List.null path then (y,eqTh)
else
let
val reflTh = Metis_Thm.refl tm
@@ -12905,7 +12927,7 @@
fun subtermsConv _ (tm as Metis_Term.Var _) = allConv tm
| subtermsConv conv (tm as Metis_Term.Fn (_,a)) =
- everyConv (map (subtermConv conv) (interval 0 (length a))) tm;
+ everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;
(* ------------------------------------------------------------------------- *)
(* Applying a conversion to every subterm, with some traversal strategy. *)
@@ -13019,7 +13041,7 @@
fun allArgumentsLiterule conv lit =
everyLiterule
- (map (argumentLiterule conv) (interval 0 (Metis_Literal.arity lit))) lit;
+ (List.map (argumentLiterule conv) (interval 0 (Metis_Literal.arity lit))) lit;
(* ------------------------------------------------------------------------- *)
(* A rule takes one theorem and either deduces another or raises an Error *)
@@ -13435,7 +13457,7 @@
let
fun fact sub = removeSym (Metis_Thm.subst sub th)
in
- map fact (factor' (Metis_Thm.clause th))
+ List.map fact (factor' (Metis_Thm.clause th))
end;
end
@@ -14453,11 +14475,11 @@
val deps = List.filter (isUnproved proved) pars
in
- if null deps then
+ if List.null deps then
let
val (fm,inf) = destThm th
- val fms = map (lookupProved proved) pars
+ val fms = List.map (lookupProved proved) pars
val acc = (fm,inf,fms) :: acc
@@ -14884,7 +14906,7 @@
let
val cls = proveCnf [mkAxiom fm]
in
- map fst cls
+ List.map fst cls
end;
end
@@ -15441,7 +15463,7 @@
local
fun mkEntry tag (na,n) = (tag,na,n);
- fun mkList tag m = map (mkEntry tag) (Metis_NameArityMap.toList m);
+ fun mkList tag m = List.map (mkEntry tag) (Metis_NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
@@ -15461,7 +15483,7 @@
| entry :: entries =>
Metis_Print.blockProgram Metis_Print.Consistent 0
(ppEntry entry ::
- map (Metis_Print.sequence Metis_Print.addNewline o ppEntry) entries)
+ List.map (Metis_Print.sequence Metis_Print.addNewline o ppEntry) entries)
end;
end;
@@ -15507,7 +15529,7 @@
end;
val projectionFixed =
- unionListFixed (map arityProjectionFixed projectionList);
+ unionListFixed (List.map arityProjectionFixed projectionList);
(* Arithmetic *)
@@ -15610,7 +15632,7 @@
let
val fns =
Metis_NameArityMap.fromList
- (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
@@ -15710,7 +15732,7 @@
let
val fns =
Metis_NameArityMap.fromList
- (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
@@ -16202,13 +16224,13 @@
fun interpret tm =
case destTerm tm of
Metis_Term.Var v => getValuation V v
- | Metis_Term.Fn (f,tms) => interpretFunction M (f, map interpret tms)
+ | Metis_Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
in
interpret
end;
fun interpretAtom M V (r,tms) =
- interpretRelation M (r, map (interpretTerm M V) tms);
+ interpretRelation M (r, List.map (interpretTerm M V) tms);
fun interpretFormula M =
let
@@ -16325,7 +16347,7 @@
Metis_Term.Var v => (ModelVar, getValuation V v)
| Metis_Term.Fn (f,tms) =>
let
- val (tms,xs) = unzip (map modelTm tms)
+ val (tms,xs) = unzip (List.map modelTm tms)
in
(ModelFn (f,tms,xs), interpretFunction M (f,xs))
end
@@ -16408,7 +16430,7 @@
let
fun onTarget ys = interpretRelation M (rel,ys) = target
- val (tms,xs) = unzip (map (modelTerm M V) tms)
+ val (tms,xs) = unzip (List.map (modelTerm M V) tms)
val rel_xs = (rel,xs)
@@ -16424,7 +16446,7 @@
fun pertClause M V cl acc = Metis_LiteralSet.foldl (pertLiteral M V) acc cl;
fun pickPerturb M perts =
- if null perts then ()
+ if List.null perts then ()
else perturb M (List.nth (perts, Metis_Portable.randomInt (length perts)));
in
fun perturbTerm M V (tm,target) =
@@ -16564,16 +16586,16 @@
Metis_Formula.listMkDisj (Metis_LiteralSet.transform Metis_Literal.toFormula cl);
in
fun toFormula prob =
- Metis_Formula.listMkConj (map clauseToFormula (toClauses prob));
+ Metis_Formula.listMkConj (List.map clauseToFormula (toClauses prob));
fun toGoal {axioms,conjecture} =
let
val clToFm = Metis_Formula.generalize o clauseToFormula
- val clsToFm = Metis_Formula.listMkConj o map clToFm
+ val clsToFm = Metis_Formula.listMkConj o List.map clToFm
val fm = Metis_Formula.False
val fm =
- if null conjecture then fm
+ if List.null conjecture then fm
else Metis_Formula.Imp (clsToFm conjecture, fm)
val fm = Metis_Formula.Imp (clsToFm axioms, fm)
in
@@ -16641,7 +16663,7 @@
val horn =
if List.exists Metis_LiteralSet.null cls then Trivial
else if List.all (fn cl => Metis_LiteralSet.size cl = 1) cls then Unit
- else
+ else
let
fun pos cl = Metis_LiteralSet.count Metis_Literal.positive cl <= 1
fun neg cl = Metis_LiteralSet.count Metis_Literal.negative cl <= 1
@@ -16786,7 +16808,7 @@
fun equalFnQterm f1 f2 = compareFnQterm (f1,f2) = EQUAL;
fun termToQterm (Metis_Term.Var _) = Var
- | termToQterm (Metis_Term.Fn (f,l)) = Fn ((f, length l), map termToQterm l);
+ | termToQterm (Metis_Term.Fn (f,l)) = Fn ((f, length l), List.map termToQterm l);
local
fun qm [] = true
@@ -16852,7 +16874,7 @@
local
fun qtermToTerm Var = anonymousVar
- | qtermToTerm (Fn ((f,_),l)) = Metis_Term.Fn (f, map qtermToTerm l);
+ | qtermToTerm (Fn ((f,_),l)) = Metis_Term.Fn (f, List.map qtermToTerm l);
in
val ppQterm = Metis_Print.ppMap qtermToTerm Metis_Term.pp;
end;
@@ -17075,7 +17097,7 @@
fun fifoize ({fifo, ...} : parameters) l = if fifo then sort idwise l else l;
in
- fun finally parm l = map snd (fifoize parm l);
+ fun finally parm l = List.map snd (fifoize parm l);
end;
local
@@ -17966,7 +17988,7 @@
fun ppWeight (Weight (m,c)) =
let
val l = Metis_NameMap.toList m
- val l = map (fn (v,n) => (SOME v, n)) l
+ val l = List.map (fn (v,n) => (SOME v, n)) l
val l = if c = 0 then l else l @ [(NONE,c)]
in
ppWeightList l
@@ -18243,7 +18265,7 @@
fun ppField f ppA a =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- [Metis_Print.addString (f ^ " ="),
+ [Metis_Print.ppString (f ^ " ="),
Metis_Print.addBreak 1,
ppA a];
@@ -18269,24 +18291,24 @@
in
fun pp (Metis_Rewrite {known,redexes,subterms,waiting,...}) =
Metis_Print.blockProgram Metis_Print.Inconsistent 2
- [Metis_Print.addString "Metis_Rewrite",
+ [Metis_Print.ppString "Metis_Rewrite",
Metis_Print.addBreak 1,
Metis_Print.blockProgram Metis_Print.Inconsistent 1
- [Metis_Print.addString "{",
+ [Metis_Print.ppString "{",
ppKnown known,
(*MetisTrace5
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
ppRedexes redexes,
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
ppSubterms subterms,
- Metis_Print.addString ",",
+ Metis_Print.ppString ",",
Metis_Print.addBreak 1,
ppWaiting waiting,
*)
Metis_Print.skip],
- Metis_Print.addString "}"]
+ Metis_Print.ppString "}"]
end;
*)
@@ -18349,10 +18371,15 @@
else
let
val Metis_Rewrite {order,redexes,subterms,waiting, ...} = rw
+
val ort = orderToOrient (order (fst eqn))
+
val known = Metis_IntMap.insert known (id,(eqn,ort))
+
val redexes = addRedexes id (eqn,ort) redexes
+
val waiting = Metis_IntSet.add waiting id
+
val rw =
Metis_Rewrite
{order = order, known = known, redexes = redexes,
@@ -18364,7 +18391,11 @@
rw
end;
-fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
+local
+ fun uncurriedAdd (eqn,rw) = add rw eqn;
+in
+ fun addList rw = List.foldl uncurriedAdd rw;
+end;
(* ------------------------------------------------------------------------- *)
(* Rewriting (the order must be a refinement of the rewrite order). *)
@@ -18797,7 +18828,7 @@
val ppResult = Metis_Print.ppPair pp (Metis_Print.ppList Metis_Print.ppInt)
val () = Metis_Print.trace ppResult "Metis_Rewrite.reduce': result" result
*)
- val ths = map (fn (id,((_,th),_)) => (id,th)) (Metis_IntMap.toList known')
+ val ths = List.map (fn (id,((_,th),_)) => (id,th)) (Metis_IntMap.toList known')
val _ =
not (List.exists (uncurry (thmReducible order known')) ths) orelse
raise Bug "Metis_Rewrite.reduce': not fully reduced"
@@ -18824,7 +18855,11 @@
end;
end;
-fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
+local
+ val order : reductionOrder = K (SOME GREATER);
+in
+ val rewrite = orderedRewrite order;
+end;
end
@@ -19172,7 +19207,7 @@
val default : parameters =
{ordering = Metis_KnuthBendixOrder.default,
- orderLiterals = UnsignedLiteralOrder,
+ orderLiterals = PositiveLiteralOrder,
orderTerms = true};
fun mk info = Metis_Clause info
@@ -19364,7 +19399,7 @@
fun apply sub = new parameters (Metis_Thm.subst sub thm)
in
- map apply (Metis_Rule.factor' lits)
+ List.map apply (Metis_Rule.factor' lits)
end;
(*MetisTrace5
@@ -20409,8 +20444,8 @@
Metis_Clause.mk {parameters = clause, id = Metis_Clause.newId (), thm = th}
val active = empty parameters
- val (active,axioms) = factor active (map mk_clause axioms)
- val (active,conjecture) = factor active (map mk_clause conjecture)
+ val (active,axioms) = factor active (List.map mk_clause axioms)
+ val (active,conjecture) = factor active (List.map mk_clause conjecture)
in
(active, {axioms = axioms, conjecture = conjecture})
end;
@@ -20591,7 +20626,7 @@
val pp =
Metis_Print.ppMap
(fn Metis_Waiting {clauses,...} =>
- map (fn (w,(_,cl)) => (w, Metis_Clause.id cl, cl)) (Metis_Heap.toList clauses))
+ List.map (fn (w,(_,cl)) => (w, Metis_Clause.id cl, cl)) (Metis_Heap.toList clauses))
(Metis_Print.ppList (Metis_Print.ppTriple Metis_Print.ppReal Metis_Print.ppInt Metis_Clause.pp));
*)
@@ -20609,10 +20644,10 @@
(fvs,lits)
end;
-val mkModelClauses = map mkModelClause;
+val mkModelClauses = List.map mkModelClause;
fun perturbModel M cls =
- if null cls then K ()
+ if List.null cls then K ()
else
let
val N = {size = Metis_Model.size M}
@@ -20723,6 +20758,14 @@
val Metis_Waiting {parameters,clauses,models} = waiting
val {models = modelParameters, ...} = parameters
+(*MetisDebug
+ val _ = not (List.null cls) orelse
+ raise Bug "Metis_Waiting.add': null"
+
+ val _ = length mcls = length cls orelse
+ raise Bug "Metis_Waiting.add': different lengths"
+*)
+
val dist = dist + Math.ln (Real.fromInt (length cls))
fun addCl ((mcl,cl),acc) =
@@ -20739,22 +20782,23 @@
Metis_Waiting {parameters = parameters, clauses = clauses, models = models}
end;
-fun add waiting (_,[]) = waiting
- | add waiting (dist,cls) =
- let
+fun add waiting (dist,cls) =
+ if List.null cls then waiting
+ else
+ let
(*MetisTrace3
- val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
- val () = Metis_Print.trace (Metis_Print.ppList Metis_Clause.pp) "Metis_Waiting.add: cls" cls
-*)
-
- val waiting = add' waiting dist (mkModelClauses cls) cls
+ val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
+ val () = Metis_Print.trace (Metis_Print.ppList Metis_Clause.pp) "Metis_Waiting.add: cls" cls
+*)
+
+ val waiting = add' waiting dist (mkModelClauses cls) cls
(*MetisTrace3
- val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
-*)
- in
- waiting
- end;
+ val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
+*)
+ in
+ waiting
+ end;
local
fun cmp ((w1,_),(w2,_)) = Real.compare (w1,w2);
@@ -20763,7 +20807,7 @@
let
val {models = modelParameters, ...} = parameters
val clauses = Metis_Heap.new cmp
- and models = map (initialModel axioms conjecture) modelParameters
+ and models = List.map (initialModel axioms conjecture) modelParameters
in
Metis_Waiting {parameters = parameters, clauses = clauses, models = models}
end;
@@ -20775,8 +20819,17 @@
val waiting = empty parameters mAxioms mConjecture
in
- add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
- end;
+ if List.null axioms andalso List.null conjecture then waiting
+ else add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
+ end
+(*MetisDebug
+ handle e =>
+ let
+ val () = Metis_Print.trace Metis_Print.ppException "Metis_Waiting.new: exception" e
+ in
+ raise e
+ end;
+*)
end;
(* ------------------------------------------------------------------------- *)
@@ -20788,9 +20841,12 @@
else
let
val ((_,dcl),clauses) = Metis_Heap.remove clauses
+
val waiting =
Metis_Waiting
- {parameters = parameters, clauses = clauses, models = models}
+ {parameters = parameters,
+ clauses = clauses,
+ models = models}
in
SOME (dcl,waiting)
end;
@@ -20888,11 +20944,21 @@
fun new parameters ths =
let
val {active = activeParm, waiting = waitingParm} = parameters
+
val (active,cls) = Metis_Active.new activeParm ths (* cls = factored ths *)
+
val waiting = Metis_Waiting.new waitingParm cls
in
Metis_Resolution {parameters = parameters, active = active, waiting = waiting}
- end;
+ end
+(*MetisDebug
+ handle e =>
+ let
+ val () = Metis_Print.trace Metis_Print.ppException "Metis_Resolution.new: exception" e
+ in
+ raise e
+ end;
+*)
fun active (Metis_Resolution {active = a, ...}) = a;
@@ -20917,9 +20983,10 @@
Decided of decision
| Undecided of resolution;
-fun iterate resolution =
- let
- val Metis_Resolution {parameters,active,waiting} = resolution
+fun iterate res =
+ let
+ val Metis_Resolution {parameters,active,waiting} = res
+
(*MetisTrace2
val () = Metis_Print.trace Metis_Active.pp "Metis_Resolution.iterate: active" active
val () = Metis_Print.trace Metis_Waiting.pp "Metis_Resolution.iterate: waiting" waiting
@@ -20927,7 +20994,11 @@
in
case Metis_Waiting.remove waiting of
NONE =>
- Decided (Satisfiable (map Metis_Clause.thm (Metis_Active.saturation active)))
+ let
+ val sat = Satisfiable (List.map Metis_Clause.thm (Metis_Active.saturation active))
+ in
+ Decided sat
+ end
| SOME ((d,cl),waiting) =>
if Metis_Clause.isContradiction cl then
Decided (Contradiction (Metis_Clause.thm cl))
@@ -20937,18 +21008,23 @@
val () = Metis_Print.trace Metis_Clause.pp "Metis_Resolution.iterate: cl" cl
*)
val (active,cls) = Metis_Active.add active cl
+
val waiting = Metis_Waiting.add waiting (d,cls)
- in
- Undecided
- (Metis_Resolution
- {parameters = parameters, active = active, waiting = waiting})
- end
- end;
-
-fun loop resolution =
- case iterate resolution of
- Decided decision => decision
- | Undecided resolution => loop resolution;
+
+ val res =
+ Metis_Resolution
+ {parameters = parameters,
+ active = active,
+ waiting = waiting}
+ in
+ Undecided res
+ end
+ end;
+
+fun loop res =
+ case iterate res of
+ Decided dec => dec
+ | Undecided res => loop res;
end
;
--- a/src/Tools/Metis/src/Active.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Active.sml Thu Mar 24 17:49:27 2011 +0100
@@ -876,8 +876,8 @@
Clause.mk {parameters = clause, id = Clause.newId (), thm = th}
val active = empty parameters
- val (active,axioms) = factor active (map mk_clause axioms)
- val (active,conjecture) = factor active (map mk_clause conjecture)
+ val (active,axioms) = factor active (List.map mk_clause axioms)
+ val (active,conjecture) = factor active (List.map mk_clause conjecture)
in
(active, {axioms = axioms, conjecture = conjecture})
end;
--- a/src/Tools/Metis/src/Atom.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Atom.sml Thu Mar 24 17:49:27 2011 +0100
@@ -84,7 +84,7 @@
fun subterms ((_,tms) : atom) =
let
- fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
+ fun f ((n,tm),l) = List.map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
in
List.foldl f [] (enumerate tms)
end;
--- a/src/Tools/Metis/src/Clause.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Clause.sml Thu Mar 24 17:49:27 2011 +0100
@@ -69,7 +69,7 @@
val default : parameters =
{ordering = KnuthBendixOrder.default,
- orderLiterals = UnsignedLiteralOrder,
+ orderLiterals = PositiveLiteralOrder,
orderTerms = true};
fun mk info = Clause info
@@ -261,7 +261,7 @@
fun apply sub = new parameters (Thm.subst sub thm)
in
- map apply (Rule.factor' lits)
+ List.map apply (Rule.factor' lits)
end;
(*MetisTrace5
--- a/src/Tools/Metis/src/Formula.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Formula.sml Thu Mar 24 17:49:27 2011 +0100
@@ -517,9 +517,9 @@
fun promote (Term.Var v) = Atom (v,[])
| promote (Term.Fn (f,tms)) =
- if Name.equal f truthName andalso null tms then
+ if Name.equal f truthName andalso List.null tms then
True
- else if Name.equal f falsityName andalso null tms then
+ else if Name.equal f falsityName andalso List.null tms then
False
else if Name.toString f = !Term.negation andalso length tms = 1 then
Not (promote (hd tms))
@@ -549,7 +549,7 @@
local
fun add_asms asms goal =
- if null asms then goal else Imp (listMkConj (rev asms), goal);
+ if List.null asms then goal else Imp (listMkConj (rev asms), goal);
fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
@@ -563,7 +563,7 @@
| (true, Imp (f1,f2)) => split (f1 :: asms) true f2
| (true, Iff (f1,f2)) =>
split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
- | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
+ | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f)
(* Negative splittables *)
| (false,False) => []
| (false, Not f) => split asms true f
@@ -573,7 +573,7 @@
| (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
| (false, Iff (f1,f2)) =>
split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
- | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
+ | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
(* Unsplittables *)
| _ => [add_asms asms (if pol then fm else Not fm)];
in
--- a/src/Tools/Metis/src/KnuthBendixOrder.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Thu Mar 24 17:49:27 2011 +0100
@@ -113,7 +113,7 @@
fun ppWeight (Weight (m,c)) =
let
val l = NameMap.toList m
- val l = map (fn (v,n) => (SOME v, n)) l
+ val l = List.map (fn (v,n) => (SOME v, n)) l
val l = if c = 0 then l else l @ [(NONE,c)]
in
ppWeightList l
--- a/src/Tools/Metis/src/Model.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Model.sml Thu Mar 24 17:49:27 2011 +0100
@@ -268,7 +268,7 @@
local
fun mkEntry tag (na,n) = (tag,na,n);
- fun mkList tag m = map (mkEntry tag) (NameArityMap.toList m);
+ fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m);
fun ppEntry (tag,source_arity,target) =
Print.blockProgram Print.Inconsistent 2
@@ -288,7 +288,7 @@
| entry :: entries =>
Print.blockProgram Print.Consistent 0
(ppEntry entry ::
- map (Print.sequence Print.addNewline o ppEntry) entries)
+ List.map (Print.sequence Print.addNewline o ppEntry) entries)
end;
end;
@@ -334,7 +334,7 @@
end;
val projectionFixed =
- unionListFixed (map arityProjectionFixed projectionList);
+ unionListFixed (List.map arityProjectionFixed projectionList);
(* Arithmetic *)
@@ -437,7 +437,7 @@
let
val fns =
NameArityMap.fromList
- (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
@@ -537,7 +537,7 @@
let
val fns =
NameArityMap.fromList
- (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
+ (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
numeralList @
[((addName,2), fixed2 addFn),
((divName,2), fixed2 divFn),
@@ -1029,13 +1029,13 @@
fun interpret tm =
case destTerm tm of
Term.Var v => getValuation V v
- | Term.Fn (f,tms) => interpretFunction M (f, map interpret tms)
+ | Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
in
interpret
end;
fun interpretAtom M V (r,tms) =
- interpretRelation M (r, map (interpretTerm M V) tms);
+ interpretRelation M (r, List.map (interpretTerm M V) tms);
fun interpretFormula M =
let
@@ -1152,7 +1152,7 @@
Term.Var v => (ModelVar, getValuation V v)
| Term.Fn (f,tms) =>
let
- val (tms,xs) = unzip (map modelTm tms)
+ val (tms,xs) = unzip (List.map modelTm tms)
in
(ModelFn (f,tms,xs), interpretFunction M (f,xs))
end
@@ -1235,7 +1235,7 @@
let
fun onTarget ys = interpretRelation M (rel,ys) = target
- val (tms,xs) = unzip (map (modelTerm M V) tms)
+ val (tms,xs) = unzip (List.map (modelTerm M V) tms)
val rel_xs = (rel,xs)
@@ -1251,7 +1251,7 @@
fun pertClause M V cl acc = LiteralSet.foldl (pertLiteral M V) acc cl;
fun pickPerturb M perts =
- if null perts then ()
+ if List.null perts then ()
else perturb M (List.nth (perts, Portable.randomInt (length perts)));
in
fun perturbTerm M V (tm,target) =
--- a/src/Tools/Metis/src/Name.sig Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Name.sig Thu Mar 24 17:49:27 2011 +0100
@@ -28,9 +28,9 @@
val newNames : int -> name list
-val variantPrime : (name -> bool) -> name -> name
+val variantPrime : {avoid : name -> bool} -> name -> name
-val variantNum : (name -> bool) -> name -> name
+val variantNum : {avoid : name -> bool} -> name -> name
(* ------------------------------------------------------------------------- *)
(* Parsing and pretty printing. *)
--- a/src/Tools/Metis/src/Name.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Name.sml Thu Mar 24 17:49:27 2011 +0100
@@ -33,22 +33,21 @@
in
fun newName () = numName (newInt ());
- fun newNames n = map numName (newInts n);
+ fun newNames n = List.map numName (newInts n);
end;
-fun variantPrime acceptable =
+fun variantPrime {avoid} =
let
- fun variant n = if acceptable n then n else variant (n ^ "'")
+ fun variant n = if avoid n then variant (n ^ "'") else n
in
variant
end;
local
- fun isDigitOrPrime #"'" = true
- | isDigitOrPrime c = Char.isDigit c;
+ fun isDigitOrPrime c = c = #"'" orelse Char.isDigit c;
in
- fun variantNum acceptable n =
- if acceptable n then n
+ fun variantNum {avoid} n =
+ if not (avoid n) then n
else
let
val n = stripSuffix isDigitOrPrime n
@@ -57,7 +56,7 @@
let
val n_i = n ^ Int.toString i
in
- if acceptable n_i then n_i else variant (i + 1)
+ if avoid n_i then variant (i + 1) else n_i
end
in
variant 0
--- a/src/Tools/Metis/src/Normalize.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Normalize.sml Thu Mar 24 17:49:27 2011 +0100
@@ -951,11 +951,11 @@
val deps = List.filter (isUnproved proved) pars
in
- if null deps then
+ if List.null deps then
let
val (fm,inf) = destThm th
- val fms = map (lookupProved proved) pars
+ val fms = List.map (lookupProved proved) pars
val acc = (fm,inf,fms) :: acc
@@ -1382,7 +1382,7 @@
let
val cls = proveCnf [mkAxiom fm]
in
- map fst cls
+ List.map fst cls
end;
end
--- a/src/Tools/Metis/src/Options.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Options.sml Thu Mar 24 17:49:27 2011 +0100
@@ -155,7 +155,7 @@
[{leftAlign = true, padChar = #"."},
{leftAlign = true, padChar = #" "}]
- val table = alignTable alignment (map listOpts options)
+ val table = alignTable alignment (List.map listOpts options)
in
header ^ join "\n" table ^ "\n" ^ footer
end;
--- a/src/Tools/Metis/src/PortableMosml.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/PortableMosml.sml Thu Mar 24 17:49:27 2011 +0100
@@ -67,7 +67,7 @@
val _ = catch_interrupt true;
(* ------------------------------------------------------------------------- *)
-(* Forcing fully qualified names of some key functions. *)
+(* Forcing fully qualified names of functions with generic names. *)
(* ------------------------------------------------------------------------- *)
(*BasicDebug
@@ -75,6 +75,8 @@
and foldl = ()
and foldr = ()
and implode = ()
+and map = ()
+and null = ()
and print = ();
*)
@@ -112,10 +114,18 @@
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_concatWith s =
+ let
+ fun add (x,l) = s :: x :: l
+ in
+ fn [] => ""
+ | x :: xs =>
+ let
+ val xs = List.foldl add [] (rev xs)
+ in
+ String.concat (x :: xs)
+ end
+ end;
fun String_isSubstring p s =
let
--- a/src/Tools/Metis/src/Print.sig Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Print.sig Thu Mar 24 17:49:27 2011 +0100
@@ -131,6 +131,8 @@
val ppPpstream : ppstream pp
+val ppException : exn pp
+
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Print.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Print.sml Thu Mar 24 17:49:27 2011 +0100
@@ -46,7 +46,7 @@
fun escapeString {escape} =
let
- val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
+ val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
fun escapeChar c =
case c of
@@ -215,7 +215,7 @@
let
val Block {indent = _, style = _, size, chunks} = block
- val empty = null chunks
+ val empty = List.null chunks
(*BasicDebug
val _ = not empty orelse size = 0 orelse
@@ -787,7 +787,7 @@
lines
end
in
- if null lines then Stream.Nil else Stream.singleton lines
+ if List.null lines then Stream.Nil else Stream.singleton lines
end;
in
fun execute {lineLength} =
@@ -860,7 +860,7 @@
fun ppOpA a = sequence (ppOp' s) (ppA a)
in
fn [] => skip
- | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
+ | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
end;
fun ppOpStream' s ppA =
@@ -1012,6 +1012,8 @@
val ppPpstream = ppStream ppStep;
+fun ppException e = ppString (exnMessage e);
+
(* ------------------------------------------------------------------------- *)
(* Pretty-printing infix operators. *)
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Problem.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Problem.sml Thu Mar 24 17:49:27 2011 +0100
@@ -44,16 +44,16 @@
Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
in
fun toFormula prob =
- Formula.listMkConj (map clauseToFormula (toClauses prob));
+ Formula.listMkConj (List.map clauseToFormula (toClauses prob));
fun toGoal {axioms,conjecture} =
let
val clToFm = Formula.generalize o clauseToFormula
- val clsToFm = Formula.listMkConj o map clToFm
+ val clsToFm = Formula.listMkConj o List.map clToFm
val fm = Formula.False
val fm =
- if null conjecture then fm
+ if List.null conjecture then fm
else Formula.Imp (clsToFm conjecture, fm)
val fm = Formula.Imp (clsToFm axioms, fm)
in
@@ -121,7 +121,7 @@
val horn =
if List.exists LiteralSet.null cls then Trivial
else if List.all (fn cl => LiteralSet.size cl = 1) cls then Unit
- else
+ else
let
fun pos cl = LiteralSet.count Literal.positive cl <= 1
fun neg cl = LiteralSet.count Literal.negative cl <= 1
--- a/src/Tools/Metis/src/Proof.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Proof.sml Thu Mar 24 17:49:27 2011 +0100
@@ -133,7 +133,7 @@
Print.blockProgram Print.Consistent 0
[Print.ppString "START OF PROOF",
Print.addNewline,
- Print.program (map ppStep prf),
+ Print.program (List.map ppStep prf),
Print.ppString "END OF PROOF"]
end
(*MetisDebug
--- a/src/Tools/Metis/src/Resolution.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Resolution.sml Thu Mar 24 17:49:27 2011 +0100
@@ -33,11 +33,21 @@
fun new parameters ths =
let
val {active = activeParm, waiting = waitingParm} = parameters
+
val (active,cls) = Active.new activeParm ths (* cls = factored ths *)
+
val waiting = Waiting.new waitingParm cls
in
Resolution {parameters = parameters, active = active, waiting = waiting}
- end;
+ end
+(*MetisDebug
+ handle e =>
+ let
+ val () = Print.trace Print.ppException "Resolution.new: exception" e
+ in
+ raise e
+ end;
+*)
fun active (Resolution {active = a, ...}) = a;
@@ -62,9 +72,10 @@
Decided of decision
| Undecided of resolution;
-fun iterate resolution =
+fun iterate res =
let
- val Resolution {parameters,active,waiting} = resolution
+ val Resolution {parameters,active,waiting} = res
+
(*MetisTrace2
val () = Print.trace Active.pp "Resolution.iterate: active" active
val () = Print.trace Waiting.pp "Resolution.iterate: waiting" waiting
@@ -72,7 +83,11 @@
in
case Waiting.remove waiting of
NONE =>
- Decided (Satisfiable (map Clause.thm (Active.saturation active)))
+ let
+ val sat = Satisfiable (List.map Clause.thm (Active.saturation active))
+ in
+ Decided sat
+ end
| SOME ((d,cl),waiting) =>
if Clause.isContradiction cl then
Decided (Contradiction (Clause.thm cl))
@@ -82,17 +97,22 @@
val () = Print.trace Clause.pp "Resolution.iterate: cl" cl
*)
val (active,cls) = Active.add active cl
+
val waiting = Waiting.add waiting (d,cls)
+
+ val res =
+ Resolution
+ {parameters = parameters,
+ active = active,
+ waiting = waiting}
in
- Undecided
- (Resolution
- {parameters = parameters, active = active, waiting = waiting})
+ Undecided res
end
end;
-fun loop resolution =
- case iterate resolution of
- Decided decision => decision
- | Undecided resolution => loop resolution;
+fun loop res =
+ case iterate res of
+ Decided dec => dec
+ | Undecided res => loop res;
end
--- a/src/Tools/Metis/src/Rewrite.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Rewrite.sml Thu Mar 24 17:49:27 2011 +0100
@@ -86,7 +86,7 @@
fun ppField f ppA a =
Print.blockProgram Print.Inconsistent 2
- [Print.addString (f ^ " ="),
+ [Print.ppString (f ^ " ="),
Print.addBreak 1,
ppA a];
@@ -112,24 +112,24 @@
in
fun pp (Rewrite {known,redexes,subterms,waiting,...}) =
Print.blockProgram Print.Inconsistent 2
- [Print.addString "Rewrite",
+ [Print.ppString "Rewrite",
Print.addBreak 1,
Print.blockProgram Print.Inconsistent 1
- [Print.addString "{",
+ [Print.ppString "{",
ppKnown known,
(*MetisTrace5
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppRedexes redexes,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppSubterms subterms,
- Print.addString ",",
+ Print.ppString ",",
Print.addBreak 1,
ppWaiting waiting,
*)
Print.skip],
- Print.addString "}"]
+ Print.ppString "}"]
end;
*)
@@ -192,10 +192,15 @@
else
let
val Rewrite {order,redexes,subterms,waiting, ...} = rw
+
val ort = orderToOrient (order (fst eqn))
+
val known = IntMap.insert known (id,(eqn,ort))
+
val redexes = addRedexes id (eqn,ort) redexes
+
val waiting = IntSet.add waiting id
+
val rw =
Rewrite
{order = order, known = known, redexes = redexes,
@@ -207,7 +212,11 @@
rw
end;
-fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
+local
+ fun uncurriedAdd (eqn,rw) = add rw eqn;
+in
+ fun addList rw = List.foldl uncurriedAdd rw;
+end;
(* ------------------------------------------------------------------------- *)
(* Rewriting (the order must be a refinement of the rewrite order). *)
@@ -640,7 +649,7 @@
val ppResult = Print.ppPair pp (Print.ppList Print.ppInt)
val () = Print.trace ppResult "Rewrite.reduce': result" result
*)
- val ths = map (fn (id,((_,th),_)) => (id,th)) (IntMap.toList known')
+ val ths = List.map (fn (id,((_,th),_)) => (id,th)) (IntMap.toList known')
val _ =
not (List.exists (uncurry (thmReducible order known')) ths) orelse
raise Bug "Rewrite.reduce': not fully reduced"
@@ -667,6 +676,10 @@
end;
end;
-fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
+local
+ val order : reductionOrder = K (SOME GREATER);
+in
+ val rewrite = orderedRewrite order;
+end;
end
--- a/src/Tools/Metis/src/Rule.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Rule.sml Thu Mar 24 17:49:27 2011 +0100
@@ -81,6 +81,7 @@
else
let
val sub = Subst.fromList [(xVarName,x),(yVarName,y)]
+
val symTh = Thm.subst sub symmetry
in
Thm.resolve lit th symTh
@@ -94,9 +95,9 @@
type equation = (Term.term * Term.term) * Thm.thm;
-fun ppEquation (_,th) = Thm.pp th;
+fun ppEquation ((_,th) : equation) = Thm.pp th;
-fun equationToString x = Print.toString ppEquation x;
+val equationToString = Print.toString ppEquation;
fun equationLiteral (t_u,th) =
let
@@ -210,7 +211,7 @@
fun rewrConv (eqn as ((x,y), eqTh)) path tm =
if Term.equal x y then allConv tm
- else if null path then (y,eqTh)
+ else if List.null path then (y,eqTh)
else
let
val reflTh = Thm.refl tm
@@ -249,7 +250,7 @@
fun subtermsConv _ (tm as Term.Var _) = allConv tm
| subtermsConv conv (tm as Term.Fn (_,a)) =
- everyConv (map (subtermConv conv) (interval 0 (length a))) tm;
+ everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;
(* ------------------------------------------------------------------------- *)
(* Applying a conversion to every subterm, with some traversal strategy. *)
@@ -363,7 +364,7 @@
fun allArgumentsLiterule conv lit =
everyLiterule
- (map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit;
+ (List.map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit;
(* ------------------------------------------------------------------------- *)
(* A rule takes one theorem and either deduces another or raises an Error *)
@@ -779,7 +780,7 @@
let
fun fact sub = removeSym (Thm.subst sub th)
in
- map fact (factor' (Thm.clause th))
+ List.map fact (factor' (Thm.clause th))
end;
end
--- a/src/Tools/Metis/src/Term.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Term.sml Thu Mar 24 17:49:27 2011 +0100
@@ -164,7 +164,7 @@
in
case tm of
Var _ => subtms rest acc
- | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
+ | Fn (_,args) => subtms (List.map f (enumerate args) @ rest) acc
end;
in
fun subterms tm = subtms [([],tm)] [];
@@ -195,7 +195,7 @@
Var _ => search rest
| Fn (_,a) =>
let
- val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
+ val subtms = List.map (fn (i,t) => (i :: path, t)) (enumerate a)
in
search (subtms @ rest)
end
@@ -235,14 +235,14 @@
fun newVar () = Var (Name.newName ());
-fun newVars n = map Var (Name.newNames n);
+fun newVars n = List.map Var (Name.newNames n);
local
- fun avoidAcceptable avoid n = not (NameSet.member n avoid);
+ fun avoid av n = NameSet.member n av;
in
- fun variantPrime avoid = Name.variantPrime (avoidAcceptable avoid);
+ fun variantPrime av = Name.variantPrime {avoid = avoid av};
- fun variantNum avoid = Name.variantNum (avoidAcceptable avoid);
+ fun variantNum av = Name.variantNum {avoid = avoid av};
end;
(* ------------------------------------------------------------------------- *)
@@ -314,7 +314,7 @@
val acc = (rev path, tm) :: acc
- val rest = map f (enumerate args) @ rest
+ val rest = List.map f (enumerate args) @ rest
in
subtms rest acc
end;
@@ -523,7 +523,7 @@
and basic bv (Var v) = varName bv v
| basic bv (Fn (f,args)) =
Print.blockProgram Print.Inconsistent 2
- (functionName bv f :: map (functionArgument bv) args)
+ (functionName bv f :: List.map (functionArgument bv) args)
and customBracket bv tm =
case destBrack tm of
@@ -535,13 +535,13 @@
NONE => term bv tm
| SOME (q,v,vs,tm) =>
let
- val bv = StringSet.addList bv (map Name.toString (v :: vs))
+ val bv = StringSet.addList bv (List.map Name.toString (v :: vs))
in
Print.program
[Print.ppString q,
varName bv v,
Print.program
- (map (Print.sequence (Print.addBreak 1) o varName bv) vs),
+ (List.map (Print.sequence (Print.addBreak 1) o varName bv) vs),
Print.ppString ".",
Print.addBreak 1,
innerQuant bv tm]
@@ -628,9 +628,9 @@
and neg = !negation
and bracks = ("(",")") :: !brackets
- val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
+ val bracks = List.map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
- val bTokens = map #2 bracks @ map #3 bracks
+ val bTokens = List.map #2 bracks @ List.map #3 bracks
fun possibleVarName "" = false
| possibleVarName s = isAlphaNum (String.sub (s,0))
@@ -685,8 +685,8 @@
in
var ||
const ||
- first (map bracket bracks) ||
- first (map quantifier quants)
+ first (List.map bracket bracks) ||
+ first (List.map quantifier quants)
end tokens
and molecule bv tokens =
--- a/src/Tools/Metis/src/TermNet.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/TermNet.sml Thu Mar 24 17:49:27 2011 +0100
@@ -50,7 +50,7 @@
fun equalFnQterm f1 f2 = compareFnQterm (f1,f2) = EQUAL;
fun termToQterm (Term.Var _) = Var
- | termToQterm (Term.Fn (f,l)) = Fn ((f, length l), map termToQterm l);
+ | termToQterm (Term.Fn (f,l)) = Fn ((f, length l), List.map termToQterm l);
local
fun qm [] = true
@@ -116,7 +116,7 @@
local
fun qtermToTerm Var = anonymousVar
- | qtermToTerm (Fn ((f,_),l)) = Term.Fn (f, map qtermToTerm l);
+ | qtermToTerm (Fn ((f,_),l)) = Term.Fn (f, List.map qtermToTerm l);
in
val ppQterm = Print.ppMap qtermToTerm Term.pp;
end;
@@ -339,7 +339,7 @@
fun fifoize ({fifo, ...} : parameters) l = if fifo then sort idwise l else l;
in
- fun finally parm l = map snd (fifoize parm l);
+ fun finally parm l = List.map snd (fifoize parm l);
end;
local
--- a/src/Tools/Metis/src/Thm.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Thm.sml Thu Mar 24 17:49:27 2011 +0100
@@ -107,7 +107,7 @@
local
fun toFormula th =
Formula.listMkDisj
- (map Literal.toFormula (LiteralSet.toList (clause th)));
+ (List.map Literal.toFormula (LiteralSet.toList (clause th)));
in
fun pp th =
Print.blockProgram Print.Inconsistent 3
--- a/src/Tools/Metis/src/Tptp.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Tptp.sml Thu Mar 24 17:49:27 2011 +0100
@@ -430,8 +430,8 @@
fun lift {name,arity,tptp} =
{name = Name.fromString name, arity = arity, tptp = tptp}
- val functionMapping = map lift defaultFunctionMapping
- and relationMapping = map lift defaultRelationMapping
+ val functionMapping = List.map lift defaultFunctionMapping
+ and relationMapping = List.map lift defaultRelationMapping
val mapping =
{functionMapping = functionMapping,
@@ -448,7 +448,7 @@
let
fun mkEntry {name,arity,model} = ((Name.fromString name, arity), model)
- fun mkMap l = NameArityMap.fromList (map mkEntry l)
+ fun mkMap l = NameArityMap.fromList (List.map mkEntry l)
in
{functionMap = mkMap funcModel,
relationMap = mkMap relModel}
@@ -766,8 +766,12 @@
val lexToken = alphaNumToken || punctToken || quoteToken;
val space = many (some Char.isSpace) >> K ();
+
+ val space1 = atLeastOne (some Char.isSpace) >> K ();
in
- val lexer = (space ++ lexToken ++ space) >> (fn ((),(tok,())) => tok);
+ val lexer =
+ (space ++ lexToken) >> (fn ((),tok) => [tok]) ||
+ space1 >> K [];
end;
(* ------------------------------------------------------------------------- *)
@@ -800,11 +804,11 @@
List.foldl fvs NameSet.empty
end;
-fun clauseSubst sub lits = map (literalSubst sub) lits;
-
-fun clauseToFormula lits = Formula.listMkDisj (map literalToFormula lits);
-
-fun clauseFromFormula fm = map literalFromFormula (Formula.stripDisj fm);
+fun clauseSubst sub lits = List.map (literalSubst sub) lits;
+
+fun clauseToFormula lits = Formula.listMkDisj (List.map literalToFormula lits);
+
+fun clauseFromFormula fm = List.map literalFromFormula (Formula.stripDisj fm);
fun clauseFromLiteralSet cl =
clauseFromFormula
@@ -1105,7 +1109,7 @@
end
| ProofFormulaSource {inference,parents} =>
let
- val isTaut = null parents
+ val isTaut = List.null parents
val gen = if isTaut then GEN_INTRODUCED else GEN_INFERENCE
@@ -1118,7 +1122,7 @@
Proof.Subst (s,_) => s
| _ => Subst.empty
in
- map (fn parent => (parent,sub)) parents
+ List.map (fn parent => (parent,sub)) parents
end
in
Print.blockProgram Print.Inconsistent (size gen + 1)
@@ -1300,7 +1304,7 @@
| f [x] = x
| f (h :: t) = (h ++ f t) >> K ();
in
- fun symbolParser s = f (map punctParser (String.explode s));
+ fun symbolParser s = f (List.map punctParser (String.explode s));
end;
val definedParser =
@@ -1568,7 +1572,7 @@
and quantifiedFormulaParser mapping input =
let
- fun mk (q,(vs,((),f))) = q (map (mkVarName mapping) vs, f)
+ fun mk (q,(vs,((),f))) = q (List.map (mkVarName mapping) vs, f)
in
(quantifierParser ++ varListParser ++ punctParser #":" ++
unitaryFormulaParser mapping) >> mk
@@ -1699,7 +1703,7 @@
fun parseChars parser chars =
let
- val tokens = Parse.everything (lexer >> singleton) chars
+ val tokens = Parse.everything lexer chars
in
Parse.everything (parser >> singleton) tokens
end;
@@ -1904,7 +1908,7 @@
val {problem,sources} : normalization = acc
val {axioms,conjecture} = problem
- val cls = map fst clauses
+ val cls = List.map fst clauses
val (axioms,conjecture) =
if isCnfConjectureRole role then (axioms, cls @ conjecture)
else (cls @ axioms, conjecture)
@@ -1939,7 +1943,7 @@
fun sourcify (cl,inf) = (cl, FofClauseSource inf)
val (clauses,cnf) = Normalize.addCnf th cnf
- val clauses = map sourcify clauses
+ val clauses = List.map sourcify clauses
val norm = addClauses role clauses norm
in
(norm,cnf)
@@ -1978,26 +1982,26 @@
let
val subgoals = Formula.splitGoal goal
val subgoals =
- if null subgoals then [Formula.True] else subgoals
+ if List.null subgoals then [Formula.True] else subgoals
val parents = [name]
in
- map (mk parents) subgoals
+ List.map (mk parents) subgoals
end
in
- fn goals => List.concat (map split goals)
+ fn goals => List.concat (List.map split goals)
end;
fun clausesToGoal cls =
let
- val cls = map (Formula.generalize o clauseToFormula o snd) cls
+ val cls = List.map (Formula.generalize o clauseToFormula o snd) cls
in
Formula.listMkConj cls
end;
fun formulasToGoal fms =
let
- val fms = map (Formula.generalize o snd) fms
+ val fms = List.map (Formula.generalize o snd) fms
in
Formula.listMkConj fms
end;
@@ -2013,11 +2017,11 @@
| FofGoal goals => formulasToGoal goals
val fm =
- if null fofAxioms then fm
+ if List.null fofAxioms then fm
else Formula.Imp (formulasToGoal fofAxioms, fm)
val fm =
- if null cnfAxioms then fm
+ if List.null cnfAxioms then fm
else Formula.Imp (clausesToGoal cnfAxioms, fm)
in
fm
@@ -2137,8 +2141,8 @@
let
val Problem {comments,includes,formulas} = problem
- val includesTop = null comments
- val formulasTop = includesTop andalso null includes
+ val includesTop = List.null comments
+ val formulasTop = includesTop andalso List.null includes
in
Stream.toTextFile
{filename = filename}
@@ -2153,8 +2157,8 @@
local
fun refute {axioms,conjecture} =
let
- val axioms = map Thm.axiom axioms
- and conjecture = map Thm.axiom conjecture
+ val axioms = List.map Thm.axiom axioms
+ and conjecture = List.map Thm.axiom conjecture
val problem = {axioms = axioms, conjecture = conjecture}
val resolution = Resolution.new Resolution.default problem
in
@@ -2166,7 +2170,7 @@
fun prove filename =
let
val problem = read filename
- val problems = map #problem (normalize problem)
+ val problems = List.map #problem (normalize problem)
in
List.all refute problems
end;
@@ -2334,7 +2338,7 @@
val number = i - 1
val (subgoal,formulas) =
- if null pars then (NONE,formulas)
+ if List.null pars then (NONE,formulas)
else
let
val role = PlainRole
@@ -2374,7 +2378,7 @@
| Normalize.Definition (_,fm) => fm :: fms
| _ => fms
- val parents = map (lookupFormulaName fmNames) fms
+ val parents = List.map (lookupFormulaName fmNames) fms
in
NormalizeFormulaSource
{inference = inference,
@@ -2388,9 +2392,9 @@
Proof.Axiom cl => [lookupClauseSourceName sources fmNames cl]
| _ =>
let
- val cls = map Thm.clause (Proof.parents inference)
+ val cls = List.map Thm.clause (Proof.parents inference)
in
- map (lookupClauseName clNames) cls
+ List.map (lookupClauseName clNames) cls
end
in
ProofFormulaSource
--- a/src/Tools/Metis/src/Useful.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Useful.sml Thu Mar 24 17:49:27 2011 +0100
@@ -50,7 +50,20 @@
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
-val tracePrint = ref TextIO.print;
+local
+ val traceOut = TextIO.stdOut;
+
+ fun tracePrintFn mesg =
+ let
+ val () = TextIO.output (traceOut,mesg)
+
+ val () = TextIO.flushOut traceOut
+ in
+ ()
+ end;
+in
+ val tracePrint = ref tracePrintFn;
+end;
fun trace mesg = !tracePrint mesg;
@@ -254,7 +267,7 @@
case l of
[] =>
let
- val acc = if null row then acc else rev row :: acc
+ val acc = if List.null row then acc else rev row :: acc
in
rev acc
end
@@ -283,9 +296,9 @@
local
fun fstEq ((x,_),(y,_)) = x = y;
- fun collapse l = (fst (hd l), map snd l);
+ fun collapse l = (fst (hd l), List.map snd l);
in
- fun groupsByFst l = map collapse (groupsBy fstEq l);
+ fun groupsByFst l = List.map collapse (groupsBy fstEq l);
end;
fun groupsOf n =
@@ -430,10 +443,10 @@
| sortMap f cmp xs =
let
fun ncmp ((m,_),(n,_)) = cmp (m,n)
- val nxs = map (fn x => (f x, x)) xs
+ val nxs = List.map (fn x => (f x, x)) xs
val nys = sort ncmp nxs
in
- map snd nys
+ List.map snd nys
end;
(* ------------------------------------------------------------------------- *)
@@ -641,7 +654,7 @@
fun alignColumn {leftAlign,padChar} column =
let
- val (n,_) = maximum Int.compare (map size column)
+ val (n,_) = maximum Int.compare (List.map size column)
fun pad entry row =
let
@@ -657,13 +670,18 @@
local
fun alignTab aligns rows =
case aligns of
- [] => map (K "") rows
- | [{leftAlign = true, padChar = #" "}] => map hd rows
+ [] => List.map (K "") rows
+ | [{leftAlign = true, padChar = #" "}] => List.map hd rows
| align :: aligns =>
- alignColumn align (map hd rows) (alignTab aligns (map tl rows));
+ let
+ val col = List.map hd rows
+ and cols = alignTab aligns (List.map tl rows)
+ in
+ alignColumn align col cols
+ end;
in
fun alignTable aligns rows =
- if null rows then [] else alignTab aligns rows;
+ if List.null rows then [] else alignTab aligns rows;
end;
(* ------------------------------------------------------------------------- *)
--- a/src/Tools/Metis/src/Waiting.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/Waiting.sml Thu Mar 24 17:49:27 2011 +0100
@@ -63,7 +63,7 @@
val pp =
Print.ppMap
(fn Waiting {clauses,...} =>
- map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses))
+ List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses))
(Print.ppList (Print.ppTriple Print.ppReal Print.ppInt Clause.pp));
*)
@@ -81,10 +81,10 @@
(fvs,lits)
end;
-val mkModelClauses = map mkModelClause;
+val mkModelClauses = List.map mkModelClause;
fun perturbModel M cls =
- if null cls then K ()
+ if List.null cls then K ()
else
let
val N = {size = Model.size M}
@@ -195,6 +195,14 @@
val Waiting {parameters,clauses,models} = waiting
val {models = modelParameters, ...} = parameters
+(*MetisDebug
+ val _ = not (List.null cls) orelse
+ raise Bug "Waiting.add': null"
+
+ val _ = length mcls = length cls orelse
+ raise Bug "Waiting.add': different lengths"
+*)
+
val dist = dist + Math.ln (Real.fromInt (length cls))
fun addCl ((mcl,cl),acc) =
@@ -211,22 +219,23 @@
Waiting {parameters = parameters, clauses = clauses, models = models}
end;
-fun add waiting (_,[]) = waiting
- | add waiting (dist,cls) =
- let
+fun add waiting (dist,cls) =
+ if List.null cls then waiting
+ else
+ let
(*MetisTrace3
- val () = Print.trace pp "Waiting.add: waiting" waiting
- val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls
+ val () = Print.trace pp "Waiting.add: waiting" waiting
+ val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls
*)
- val waiting = add' waiting dist (mkModelClauses cls) cls
+ val waiting = add' waiting dist (mkModelClauses cls) cls
(*MetisTrace3
- val () = Print.trace pp "Waiting.add: waiting" waiting
+ val () = Print.trace pp "Waiting.add: waiting" waiting
*)
- in
- waiting
- end;
+ in
+ waiting
+ end;
local
fun cmp ((w1,_),(w2,_)) = Real.compare (w1,w2);
@@ -235,7 +244,7 @@
let
val {models = modelParameters, ...} = parameters
val clauses = Heap.new cmp
- and models = map (initialModel axioms conjecture) modelParameters
+ and models = List.map (initialModel axioms conjecture) modelParameters
in
Waiting {parameters = parameters, clauses = clauses, models = models}
end;
@@ -247,8 +256,17 @@
val waiting = empty parameters mAxioms mConjecture
in
- add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
- end;
+ if List.null axioms andalso List.null conjecture then waiting
+ else add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
+ end
+(*MetisDebug
+ handle e =>
+ let
+ val () = Print.trace Print.ppException "Waiting.new: exception" e
+ in
+ raise e
+ end;
+*)
end;
(* ------------------------------------------------------------------------- *)
@@ -260,9 +278,12 @@
else
let
val ((_,dcl),clauses) = Heap.remove clauses
+
val waiting =
Waiting
- {parameters = parameters, clauses = clauses, models = models}
+ {parameters = parameters,
+ clauses = clauses,
+ models = models}
in
SOME (dcl,waiting)
end;
--- a/src/Tools/Metis/src/metis.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/metis.sml Thu Mar 24 17:49:27 2011 +0100
@@ -13,23 +13,25 @@
val VERSION = "2.3";
-val versionString = PROGRAM^" "^VERSION^" (release 20100916)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20101229)"^"\n";
(* ------------------------------------------------------------------------- *)
(* Program options. *)
(* ------------------------------------------------------------------------- *)
+val ITEMS = ["name","goal","clauses","size","category","proof","saturation"];
+
+val TIMEOUT : int option ref = ref NONE;
+
+val TPTP : string option ref = ref NONE;
+
val QUIET = ref false;
val TEST = ref false;
-val TPTP : string option ref = ref NONE;
-
-val ITEMS = ["name","goal","clauses","size","category","proof","saturation"];
-
val extended_items = "all" :: ITEMS;
-val show_items = map (fn s => (s, ref false)) ITEMS;
+val show_items = List.map (fn s => (s, ref false)) ITEMS;
fun show_ref s =
case List.find (equal s o fst) show_items of
@@ -68,6 +70,11 @@
description = "hide ITEM (see below for list)",
processor =
beginOpt (enumOpt extended_items endOpt) (fn _ => fn s => hide s)},
+ {switches = ["--time-limit"], arguments = ["N"],
+ description = "give up after N seconds",
+ processor =
+ beginOpt (optionOpt ("-", intOpt (SOME 0, NONE)) endOpt)
+ (fn _ => fn n => TIMEOUT := n)},
{switches = ["--tptp"], arguments = ["DIR"],
description = "specify the TPTP installation directory",
processor =
@@ -113,6 +120,25 @@
(* The core application. *)
(* ------------------------------------------------------------------------- *)
+fun newLimit () =
+ case !TIMEOUT of
+ NONE => K true
+ | SOME lim =>
+ let
+ val timer = Timer.startRealTimer ()
+
+ val lim = Time.fromReal (Real.fromInt lim)
+
+ fun check () =
+ let
+ val time = Timer.checkRealTimer timer
+ in
+ Time.<= (time,lim)
+ end
+ in
+ check
+ end;
+
(*MetisDebug
val next_cnf =
let
@@ -237,7 +263,7 @@
names = Tptp.noClauseNames,
roles = Tptp.noClauseRoles,
problem = {axioms = [],
- conjecture = map Thm.clause ths}}
+ conjecture = List.map Thm.clause ths}}
val mapping =
Tptp.addVarSetMapping Tptp.defaultMapping
@@ -294,21 +320,25 @@
end
*)
val () = display_clauses cls
+
val () = display_size cls
+
val () = display_category cls
in
()
end;
fun mkTptpFilename filename =
- case !TPTP of
- NONE => filename
- | SOME tptp =>
- let
- val tptp = stripSuffix (equal #"/") tptp
- in
- tptp ^ "/" ^ filename
- end;
+ if isPrefix "/" filename then filename
+ else
+ case !TPTP of
+ NONE => filename
+ | SOME tptp =>
+ let
+ val tptp = stripSuffix (equal #"/") tptp
+ in
+ tptp ^ "/" ^ filename
+ end;
fun readIncludes mapping seen formulas includes =
case includes of
@@ -338,7 +368,7 @@
val Tptp.Problem {comments,includes,formulas} = problem
in
- if null includes then problem
+ if List.null includes then problem
else
let
val seen = StringSet.empty
@@ -356,8 +386,7 @@
val resolutionParameters =
let
- val {active,
- waiting} = Resolution.default
+ val {active,waiting} = Resolution.default
val waiting =
let
@@ -394,17 +423,25 @@
waiting = waiting}
end;
- fun refute {axioms,conjecture} =
+ fun resolutionLoop limit res =
+ case Resolution.iterate res of
+ Resolution.Decided dec => SOME dec
+ | Resolution.Undecided res =>
+ if limit () then resolutionLoop limit res else NONE;
+
+ fun refute limit {axioms,conjecture} =
let
- val axioms = map Thm.axiom axioms
- and conjecture = map Thm.axiom conjecture
+ val axioms = List.map Thm.axiom axioms
+ and conjecture = List.map Thm.axiom conjecture
+
val problem = {axioms = axioms, conjecture = conjecture}
- val resolution = Resolution.new resolutionParameters problem
+
+ val res = Resolution.new resolutionParameters problem
in
- Resolution.loop resolution
+ resolutionLoop limit res
end;
- fun refuteAll filename tptp probs acc =
+ fun refuteAll limit filename tptp probs acc =
case probs of
[] =>
let
@@ -427,10 +464,10 @@
val () = display_problem filename problem
in
- if !TEST then refuteAll filename tptp probs acc
+ if !TEST then refuteAll limit filename tptp probs acc
else
- case refute problem of
- Resolution.Contradiction th =>
+ case refute limit problem of
+ SOME (Resolution.Contradiction th) =>
let
val subgoalProof =
{subgoal = subgoal,
@@ -439,9 +476,9 @@
val acc = subgoalProof :: acc
in
- refuteAll filename tptp probs acc
+ refuteAll limit filename tptp probs acc
end
- | Resolution.Satisfiable ths =>
+ | SOME (Resolution.Satisfiable ths) =>
let
val status =
if Tptp.hasFofConjecture tptp then
@@ -450,29 +487,42 @@
Tptp.SatisfiableStatus
val () = display_status filename status
+
val () = display_saturation filename ths
in
false
end
+ | NONE =>
+ let
+ val status = Tptp.UnknownStatus
+
+ val () = display_status filename status
+ in
+ false
+ end
end;
in
- fun prove mapping filename =
+ fun prove limit mapping filename =
let
val () = display_sep ()
+
val () = display_name filename
+
val tptp = read mapping filename
+
val () = display_goal tptp
+
val problems = Tptp.normalize tptp
in
- refuteAll filename tptp problems []
+ refuteAll limit filename tptp problems []
end;
+end;
- fun proveAll mapping filenames =
- List.all
- (if !QUIET then prove mapping
- else fn filename => prove mapping filename orelse true)
- filenames;
-end;
+fun proveAll limit mapping filenames =
+ List.all
+ (if !QUIET then prove limit mapping
+ else fn filename => prove limit mapping filename orelse true)
+ filenames;
(* ------------------------------------------------------------------------- *)
(* Top level. *)
@@ -482,11 +532,13 @@
let
val work = processOptions ()
- val () = if null work then usage "no input problem files" else ()
+ val () = if List.null work then usage "no input problem files" else ()
+
+ val limit = newLimit ()
val mapping = Tptp.defaultMapping
- val success = proveAll mapping work
+ val success = proveAll limit mapping work
in
exit {message = NONE, usage = false, success = success}
end
--- a/src/Tools/Metis/src/problems.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/problems.sml Thu Mar 24 17:49:27 2011 +0100
@@ -22,7 +22,7 @@
fun mkProblem collection description (problem : problem) : problem =
let
val {name,comments,goal} = problem
- val comments = if null comments then [] else "" :: comments
+ val comments = if List.null comments then [] else "" :: comments
val comments = "Description: " ^ description :: comments
val comments = mkCollection collection :: comments
in
@@ -33,7 +33,7 @@
Useful.mem (mkCollection collection) comments;
fun mkProblems collection description problems =
- map (mkProblem collection description) problems;
+ List.map (mkProblem collection description) problems;
end;
(* ========================================================================= *)
--- a/src/Tools/Metis/src/problems2tptp.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/problems2tptp.sml Thu Mar 24 17:49:27 2011 +0100
@@ -34,7 +34,7 @@
if x <> x' then dups xs
else raise Error ("duplicate problem name: " ^ x)
- val names = sort String.compare (map #name problems)
+ val names = sort String.compare (List.map #name problems)
in
dups names
end;
@@ -56,8 +56,8 @@
val comments =
[comment_bar] @
["Name: " ^ name] @
- (if null comments then [] else "" :: comments) @
- (if null comment_footer then [] else "" :: comment_footer) @
+ (if List.null comments then [] else "" :: comments) @
+ (if List.null comment_footer then [] else "" :: comment_footer) @
[comment_bar]
val includes = []
@@ -145,7 +145,7 @@
val (opts,work) =
Options.processOptions programOptions (CommandLine.arguments ());
-val () = if null work then () else usage "too many arguments";
+val () = if List.null work then () else usage "too many arguments";
(* ------------------------------------------------------------------------- *)
(* Top level. *)
--- a/src/Tools/Metis/src/selftest.sml Thu Mar 24 17:49:27 2011 +0100
+++ b/src/Tools/Metis/src/selftest.sml Thu Mar 24 17:49:27 2011 +0100
@@ -84,7 +84,7 @@
and L = Literal.parse
and F = Formula.parse
and S = Subst.fromList;
-val LS = LiteralSet.fromList o map L;
+val LS = LiteralSet.fromList o List.map L;
val AX = Thm.axiom o LS;
val CL = mkCl Clause.default o AX;
val Q = (fn th => (Thm.destUnitEq th, th)) o AX o singleton
@@ -116,7 +116,7 @@
val () = SAY "The parser and pretty-printer";
(* ------------------------------------------------------------------------- *)
-fun prep l = (chop_newline o String.concat o map unquote) l;
+fun prep l = (chop_newline o String.concat o List.map unquote) l;
fun mini_print n fm = withRef (Print.lineLength,n) Formula.toString fm;
@@ -509,7 +509,7 @@
fun clauseToFormula cl =
Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
in
- fun clausesToFormula cls = Formula.listMkConj (map clauseToFormula cls);
+ fun clausesToFormula cls = Formula.listMkConj (List.map clauseToFormula cls);
end;
val cnf' = pvFm o clausesToFormula o Normalize.cnf o F;
@@ -565,7 +565,7 @@
in
fun checkModel M cls =
let
- val table = map (checkModelClause M) cls
+ val table = List.map (checkModelClause M) cls
val rows = alignTable format table
@@ -587,7 +587,7 @@
else Model.perturbClause M V cl
end
- val cls = map (fn cl => (LiteralSet.freeVars cl, cl)) cls
+ val cls = List.map (fn cl => (LiteralSet.freeVars cl, cl)) cls
fun perturbClauses () = app perturbClause cls
@@ -1085,7 +1085,7 @@
val quot_clauses =
Formula.listMkConj o sort Formula.compare o
- map (quot o snd o Formula.stripForall) o Formula.stripConj;
+ List.map (quot o snd o Formula.stripForall) o Formula.stripConj;
fun quotient (Formula.Imp (a, Formula.Imp (b, Formula.False))) =
Formula.Imp (quot_clauses a, Formula.Imp (quot_clauses b, Formula.False))
@@ -1142,6 +1142,8 @@
end;
val _ = tptp "PUZ001-1";
+val _ = tptp "NO_FORMULAS";
+val _ = tptp "SEPARATED_COMMENTS";
val _ = tptp "NUMBERED_FORMULAS";
val _ = tptp "DEFINED_TERMS";
val _ = tptp "SYSTEM_TERMS";