new version of Metis 2.3 (29 Dec. 2010)
1.1 --- a/src/Tools/Metis/Makefile Thu Mar 24 17:49:27 2011 +0100
1.2 +++ b/src/Tools/Metis/Makefile Thu Mar 24 17:49:27 2011 +0100
1.3 @@ -179,6 +179,12 @@
1.4
1.5 POLYML_OPTS =
1.6
1.7 +ifeq ($(shell uname), Darwin)
1.8 + POLYML_LINK_OPTS = -lpolymain -lpolyml -segprot POLY rwx rwx
1.9 +else
1.10 + POLYML_LINK_OPTS = -lpolymain -lpolyml
1.11 +endif
1.12 +
1.13 POLYML_SRC = \
1.14 src/Random.sig src/Random.sml \
1.15 src/Portable.sig src/PortablePolyml.sml \
1.16 @@ -205,7 +211,7 @@
1.17 @echo '*****************************'
1.18 @echo
1.19 @echo $@
1.20 - cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) -lpolymain -lpolyml
1.21 + cd bin/polyml && $(CC) -o $(notdir $@) $(notdir $<) $(POLYML_LINK_OPTS)
1.22 @echo
1.23
1.24 .PHONY: polyml-info
2.1 --- a/src/Tools/Metis/metis.ML Thu Mar 24 17:49:27 2011 +0100
2.2 +++ b/src/Tools/Metis/metis.ML Thu Mar 24 17:49:27 2011 +0100
2.3 @@ -555,7 +555,20 @@
2.4 (* Tracing. *)
2.5 (* ------------------------------------------------------------------------- *)
2.6
2.7 -val tracePrint = Unsynchronized.ref TextIO.print;
2.8 +local
2.9 + val traceOut = TextIO.stdOut;
2.10 +
2.11 + fun tracePrintFn mesg =
2.12 + let
2.13 + val () = TextIO.output (traceOut,mesg)
2.14 +
2.15 + val () = TextIO.flushOut traceOut
2.16 + in
2.17 + ()
2.18 + end;
2.19 +in
2.20 + val tracePrint = Unsynchronized.ref tracePrintFn;
2.21 +end;
2.22
2.23 fun trace mesg = !tracePrint mesg;
2.24
2.25 @@ -759,7 +772,7 @@
2.26 case l of
2.27 [] =>
2.28 let
2.29 - val acc = if null row then acc else rev row :: acc
2.30 + val acc = if List.null row then acc else rev row :: acc
2.31 in
2.32 rev acc
2.33 end
2.34 @@ -788,9 +801,9 @@
2.35 local
2.36 fun fstEq ((x,_),(y,_)) = x = y;
2.37
2.38 - fun collapse l = (fst (hd l), map snd l);
2.39 -in
2.40 - fun groupsByFst l = map collapse (groupsBy fstEq l);
2.41 + fun collapse l = (fst (hd l), List.map snd l);
2.42 +in
2.43 + fun groupsByFst l = List.map collapse (groupsBy fstEq l);
2.44 end;
2.45
2.46 fun groupsOf n =
2.47 @@ -935,10 +948,10 @@
2.48 | sortMap f cmp xs =
2.49 let
2.50 fun ncmp ((m,_),(n,_)) = cmp (m,n)
2.51 - val nxs = map (fn x => (f x, x)) xs
2.52 + val nxs = List.map (fn x => (f x, x)) xs
2.53 val nys = sort ncmp nxs
2.54 in
2.55 - map snd nys
2.56 + List.map snd nys
2.57 end;
2.58
2.59 (* ------------------------------------------------------------------------- *)
2.60 @@ -1146,7 +1159,7 @@
2.61
2.62 fun alignColumn {leftAlign,padChar} column =
2.63 let
2.64 - val (n,_) = maximum Int.compare (map size column)
2.65 + val (n,_) = maximum Int.compare (List.map size column)
2.66
2.67 fun pad entry row =
2.68 let
2.69 @@ -1162,13 +1175,18 @@
2.70 local
2.71 fun alignTab aligns rows =
2.72 case aligns of
2.73 - [] => map (K "") rows
2.74 - | [{leftAlign = true, padChar = #" "}] => map hd rows
2.75 + [] => List.map (K "") rows
2.76 + | [{leftAlign = true, padChar = #" "}] => List.map hd rows
2.77 | align :: aligns =>
2.78 - alignColumn align (map hd rows) (alignTab aligns (map tl rows));
2.79 + let
2.80 + val col = List.map hd rows
2.81 + and cols = alignTab aligns (List.map tl rows)
2.82 + in
2.83 + alignColumn align col cols
2.84 + end;
2.85 in
2.86 fun alignTable aligns rows =
2.87 - if null rows then [] else alignTab aligns rows;
2.88 + if List.null rows then [] else alignTab aligns rows;
2.89 end;
2.90
2.91 (* ------------------------------------------------------------------------- *)
2.92 @@ -6599,6 +6617,8 @@
2.93
2.94 val ppPpstream : ppstream pp
2.95
2.96 +val ppException : exn pp
2.97 +
2.98 (* ------------------------------------------------------------------------- *)
2.99 (* Pretty-printing infix operators. *)
2.100 (* ------------------------------------------------------------------------- *)
2.101 @@ -6689,7 +6709,7 @@
2.102
2.103 fun escapeString {escape} =
2.104 let
2.105 - val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
2.106 + val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
2.107
2.108 fun escapeChar c =
2.109 case c of
2.110 @@ -6858,7 +6878,7 @@
2.111 let
2.112 val Block {indent = _, style = _, size, chunks} = block
2.113
2.114 - val empty = null chunks
2.115 + val empty = List.null chunks
2.116
2.117 (*BasicDebug
2.118 val _ = not empty orelse size = 0 orelse
2.119 @@ -7430,7 +7450,7 @@
2.120 lines
2.121 end
2.122 in
2.123 - if null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
2.124 + if List.null lines then Metis_Stream.Nil else Metis_Stream.singleton lines
2.125 end;
2.126 in
2.127 fun execute {lineLength} =
2.128 @@ -7503,7 +7523,7 @@
2.129 fun ppOpA a = sequence (ppOp' s) (ppA a)
2.130 in
2.131 fn [] => skip
2.132 - | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
2.133 + | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
2.134 end;
2.135
2.136 fun ppOpStream' s ppA =
2.137 @@ -7655,6 +7675,8 @@
2.138
2.139 val ppPpstream = ppStream ppStep;
2.140
2.141 +fun ppException e = ppString (exnMessage e);
2.142 +
2.143 (* ------------------------------------------------------------------------- *)
2.144 (* Pretty-printing infix operators. *)
2.145 (* ------------------------------------------------------------------------- *)
2.146 @@ -8258,9 +8280,9 @@
2.147
2.148 val newNames : int -> name list
2.149
2.150 -val variantPrime : (name -> bool) -> name -> name
2.151 -
2.152 -val variantNum : (name -> bool) -> name -> name
2.153 +val variantPrime : {avoid : name -> bool} -> name -> name
2.154 +
2.155 +val variantNum : {avoid : name -> bool} -> name -> name
2.156
2.157 (* ------------------------------------------------------------------------- *)
2.158 (* Parsing and pretty printing. *)
2.159 @@ -8311,22 +8333,21 @@
2.160 in
2.161 fun newName () = numName (newInt ());
2.162
2.163 - fun newNames n = map numName (newInts n);
2.164 -end;
2.165 -
2.166 -fun variantPrime acceptable =
2.167 - let
2.168 - fun variant n = if acceptable n then n else variant (n ^ "'")
2.169 + fun newNames n = List.map numName (newInts n);
2.170 +end;
2.171 +
2.172 +fun variantPrime {avoid} =
2.173 + let
2.174 + fun variant n = if avoid n then variant (n ^ "'") else n
2.175 in
2.176 variant
2.177 end;
2.178
2.179 local
2.180 - fun isDigitOrPrime #"'" = true
2.181 - | isDigitOrPrime c = Char.isDigit c;
2.182 -in
2.183 - fun variantNum acceptable n =
2.184 - if acceptable n then n
2.185 + fun isDigitOrPrime c = c = #"'" orelse Char.isDigit c;
2.186 +in
2.187 + fun variantNum {avoid} n =
2.188 + if not (avoid n) then n
2.189 else
2.190 let
2.191 val n = stripSuffix isDigitOrPrime n
2.192 @@ -8335,7 +8356,7 @@
2.193 let
2.194 val n_i = n ^ Int.toString i
2.195 in
2.196 - if acceptable n_i then n_i else variant (i + 1)
2.197 + if avoid n_i then variant (i + 1) else n_i
2.198 end
2.199 in
2.200 variant 0
2.201 @@ -8878,7 +8899,7 @@
2.202 in
2.203 case tm of
2.204 Var _ => subtms rest acc
2.205 - | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
2.206 + | Fn (_,args) => subtms (List.map f (enumerate args) @ rest) acc
2.207 end;
2.208 in
2.209 fun subterms tm = subtms [([],tm)] [];
2.210 @@ -8909,7 +8930,7 @@
2.211 Var _ => search rest
2.212 | Fn (_,a) =>
2.213 let
2.214 - val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
2.215 + val subtms = List.map (fn (i,t) => (i :: path, t)) (enumerate a)
2.216 in
2.217 search (subtms @ rest)
2.218 end
2.219 @@ -8949,14 +8970,14 @@
2.220
2.221 fun newVar () = Var (Metis_Name.newName ());
2.222
2.223 -fun newVars n = map Var (Metis_Name.newNames n);
2.224 -
2.225 -local
2.226 - fun avoidAcceptable avoid n = not (Metis_NameSet.member n avoid);
2.227 -in
2.228 - fun variantPrime avoid = Metis_Name.variantPrime (avoidAcceptable avoid);
2.229 -
2.230 - fun variantNum avoid = Metis_Name.variantNum (avoidAcceptable avoid);
2.231 +fun newVars n = List.map Var (Metis_Name.newNames n);
2.232 +
2.233 +local
2.234 + fun avoid av n = Metis_NameSet.member n av;
2.235 +in
2.236 + fun variantPrime av = Metis_Name.variantPrime {avoid = avoid av};
2.237 +
2.238 + fun variantNum av = Metis_Name.variantNum {avoid = avoid av};
2.239 end;
2.240
2.241 (* ------------------------------------------------------------------------- *)
2.242 @@ -9028,7 +9049,7 @@
2.243
2.244 val acc = (rev path, tm) :: acc
2.245
2.246 - val rest = map f (enumerate args) @ rest
2.247 + val rest = List.map f (enumerate args) @ rest
2.248 in
2.249 subtms rest acc
2.250 end;
2.251 @@ -9237,7 +9258,7 @@
2.252 and basic bv (Var v) = varName bv v
2.253 | basic bv (Fn (f,args)) =
2.254 Metis_Print.blockProgram Metis_Print.Inconsistent 2
2.255 - (functionName bv f :: map (functionArgument bv) args)
2.256 + (functionName bv f :: List.map (functionArgument bv) args)
2.257
2.258 and customBracket bv tm =
2.259 case destBrack tm of
2.260 @@ -9249,13 +9270,13 @@
2.261 NONE => term bv tm
2.262 | SOME (q,v,vs,tm) =>
2.263 let
2.264 - val bv = Metis_StringSet.addList bv (map Metis_Name.toString (v :: vs))
2.265 + val bv = Metis_StringSet.addList bv (List.map Metis_Name.toString (v :: vs))
2.266 in
2.267 Metis_Print.program
2.268 [Metis_Print.ppString q,
2.269 varName bv v,
2.270 Metis_Print.program
2.271 - (map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
2.272 + (List.map (Metis_Print.sequence (Metis_Print.addBreak 1) o varName bv) vs),
2.273 Metis_Print.ppString ".",
2.274 Metis_Print.addBreak 1,
2.275 innerQuant bv tm]
2.276 @@ -9342,9 +9363,9 @@
2.277 and neg = !negation
2.278 and bracks = ("(",")") :: !brackets
2.279
2.280 - val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
2.281 -
2.282 - val bTokens = map #2 bracks @ map #3 bracks
2.283 + val bracks = List.map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
2.284 +
2.285 + val bTokens = List.map #2 bracks @ List.map #3 bracks
2.286
2.287 fun possibleVarName "" = false
2.288 | possibleVarName s = isAlphaNum (String.sub (s,0))
2.289 @@ -9399,8 +9420,8 @@
2.290 in
2.291 var ||
2.292 const ||
2.293 - first (map bracket bracks) ||
2.294 - first (map quantifier quants)
2.295 + first (List.map bracket bracks) ||
2.296 + first (List.map quantifier quants)
2.297 end tokens
2.298
2.299 and molecule bv tokens =
2.300 @@ -10057,7 +10078,7 @@
2.301
2.302 fun subterms ((_,tms) : atom) =
2.303 let
2.304 - fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Metis_Term.subterms tm) @ l
2.305 + fun f ((n,tm),l) = List.map (fn (p,s) => (n :: p, s)) (Metis_Term.subterms tm) @ l
2.306 in
2.307 List.foldl f [] (enumerate tms)
2.308 end;
2.309 @@ -10941,9 +10962,9 @@
2.310
2.311 fun promote (Metis_Term.Var v) = Metis_Atom (v,[])
2.312 | promote (Metis_Term.Fn (f,tms)) =
2.313 - if Metis_Name.equal f truthName andalso null tms then
2.314 + if Metis_Name.equal f truthName andalso List.null tms then
2.315 True
2.316 - else if Metis_Name.equal f falsityName andalso null tms then
2.317 + else if Metis_Name.equal f falsityName andalso List.null tms then
2.318 False
2.319 else if Metis_Name.toString f = !Metis_Term.negation andalso length tms = 1 then
2.320 Not (promote (hd tms))
2.321 @@ -10973,7 +10994,7 @@
2.322
2.323 local
2.324 fun add_asms asms goal =
2.325 - if null asms then goal else Imp (listMkConj (rev asms), goal);
2.326 + if List.null asms then goal else Imp (listMkConj (rev asms), goal);
2.327
2.328 fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
2.329
2.330 @@ -10987,7 +11008,7 @@
2.331 | (true, Imp (f1,f2)) => split (f1 :: asms) true f2
2.332 | (true, Iff (f1,f2)) =>
2.333 split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
2.334 - | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
2.335 + | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f)
2.336 (* Negative splittables *)
2.337 | (false,False) => []
2.338 | (false, Not f) => split asms true f
2.339 @@ -10997,7 +11018,7 @@
2.340 | (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
2.341 | (false, Iff (f1,f2)) =>
2.342 split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
2.343 - | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
2.344 + | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
2.345 (* Unsplittables *)
2.346 | _ => [add_asms asms (if pol then fm else Not fm)];
2.347 in
2.348 @@ -11750,7 +11771,7 @@
2.349 local
2.350 fun toFormula th =
2.351 Metis_Formula.listMkDisj
2.352 - (map Metis_Literal.toFormula (Metis_LiteralSet.toList (clause th)));
2.353 + (List.map Metis_Literal.toFormula (Metis_LiteralSet.toList (clause th)));
2.354 in
2.355 fun pp th =
2.356 Metis_Print.blockProgram Metis_Print.Inconsistent 3
2.357 @@ -12057,7 +12078,7 @@
2.358 Metis_Print.blockProgram Metis_Print.Consistent 0
2.359 [Metis_Print.ppString "START OF PROOF",
2.360 Metis_Print.addNewline,
2.361 - Metis_Print.program (map ppStep prf),
2.362 + Metis_Print.program (List.map ppStep prf),
2.363 Metis_Print.ppString "END OF PROOF"]
2.364 end
2.365 (*MetisDebug
2.366 @@ -12737,6 +12758,7 @@
2.367 else
2.368 let
2.369 val sub = Metis_Subst.fromList [(xVarName,x),(yVarName,y)]
2.370 +
2.371 val symTh = Metis_Thm.subst sub symmetry
2.372 in
2.373 Metis_Thm.resolve lit th symTh
2.374 @@ -12750,9 +12772,9 @@
2.375
2.376 type equation = (Metis_Term.term * Metis_Term.term) * Metis_Thm.thm;
2.377
2.378 -fun ppEquation (_,th) = Metis_Thm.pp th;
2.379 -
2.380 -fun equationToString x = Metis_Print.toString ppEquation x;
2.381 +fun ppEquation ((_,th) : equation) = Metis_Thm.pp th;
2.382 +
2.383 +val equationToString = Metis_Print.toString ppEquation;
2.384
2.385 fun equationLiteral (t_u,th) =
2.386 let
2.387 @@ -12866,7 +12888,7 @@
2.388
2.389 fun rewrConv (eqn as ((x,y), eqTh)) path tm =
2.390 if Metis_Term.equal x y then allConv tm
2.391 - else if null path then (y,eqTh)
2.392 + else if List.null path then (y,eqTh)
2.393 else
2.394 let
2.395 val reflTh = Metis_Thm.refl tm
2.396 @@ -12905,7 +12927,7 @@
2.397
2.398 fun subtermsConv _ (tm as Metis_Term.Var _) = allConv tm
2.399 | subtermsConv conv (tm as Metis_Term.Fn (_,a)) =
2.400 - everyConv (map (subtermConv conv) (interval 0 (length a))) tm;
2.401 + everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;
2.402
2.403 (* ------------------------------------------------------------------------- *)
2.404 (* Applying a conversion to every subterm, with some traversal strategy. *)
2.405 @@ -13019,7 +13041,7 @@
2.406
2.407 fun allArgumentsLiterule conv lit =
2.408 everyLiterule
2.409 - (map (argumentLiterule conv) (interval 0 (Metis_Literal.arity lit))) lit;
2.410 + (List.map (argumentLiterule conv) (interval 0 (Metis_Literal.arity lit))) lit;
2.411
2.412 (* ------------------------------------------------------------------------- *)
2.413 (* A rule takes one theorem and either deduces another or raises an Error *)
2.414 @@ -13435,7 +13457,7 @@
2.415 let
2.416 fun fact sub = removeSym (Metis_Thm.subst sub th)
2.417 in
2.418 - map fact (factor' (Metis_Thm.clause th))
2.419 + List.map fact (factor' (Metis_Thm.clause th))
2.420 end;
2.421
2.422 end
2.423 @@ -14453,11 +14475,11 @@
2.424
2.425 val deps = List.filter (isUnproved proved) pars
2.426 in
2.427 - if null deps then
2.428 + if List.null deps then
2.429 let
2.430 val (fm,inf) = destThm th
2.431
2.432 - val fms = map (lookupProved proved) pars
2.433 + val fms = List.map (lookupProved proved) pars
2.434
2.435 val acc = (fm,inf,fms) :: acc
2.436
2.437 @@ -14884,7 +14906,7 @@
2.438 let
2.439 val cls = proveCnf [mkAxiom fm]
2.440 in
2.441 - map fst cls
2.442 + List.map fst cls
2.443 end;
2.444
2.445 end
2.446 @@ -15441,7 +15463,7 @@
2.447 local
2.448 fun mkEntry tag (na,n) = (tag,na,n);
2.449
2.450 - fun mkList tag m = map (mkEntry tag) (Metis_NameArityMap.toList m);
2.451 + fun mkList tag m = List.map (mkEntry tag) (Metis_NameArityMap.toList m);
2.452
2.453 fun ppEntry (tag,source_arity,target) =
2.454 Metis_Print.blockProgram Metis_Print.Inconsistent 2
2.455 @@ -15461,7 +15483,7 @@
2.456 | entry :: entries =>
2.457 Metis_Print.blockProgram Metis_Print.Consistent 0
2.458 (ppEntry entry ::
2.459 - map (Metis_Print.sequence Metis_Print.addNewline o ppEntry) entries)
2.460 + List.map (Metis_Print.sequence Metis_Print.addNewline o ppEntry) entries)
2.461 end;
2.462 end;
2.463
2.464 @@ -15507,7 +15529,7 @@
2.465 end;
2.466
2.467 val projectionFixed =
2.468 - unionListFixed (map arityProjectionFixed projectionList);
2.469 + unionListFixed (List.map arityProjectionFixed projectionList);
2.470
2.471 (* Arithmetic *)
2.472
2.473 @@ -15610,7 +15632,7 @@
2.474 let
2.475 val fns =
2.476 Metis_NameArityMap.fromList
2.477 - (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
2.478 + (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
2.479 numeralList @
2.480 [((addName,2), fixed2 addFn),
2.481 ((divName,2), fixed2 divFn),
2.482 @@ -15710,7 +15732,7 @@
2.483 let
2.484 val fns =
2.485 Metis_NameArityMap.fromList
2.486 - (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
2.487 + (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
2.488 numeralList @
2.489 [((addName,2), fixed2 addFn),
2.490 ((divName,2), fixed2 divFn),
2.491 @@ -16202,13 +16224,13 @@
2.492 fun interpret tm =
2.493 case destTerm tm of
2.494 Metis_Term.Var v => getValuation V v
2.495 - | Metis_Term.Fn (f,tms) => interpretFunction M (f, map interpret tms)
2.496 + | Metis_Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
2.497 in
2.498 interpret
2.499 end;
2.500
2.501 fun interpretAtom M V (r,tms) =
2.502 - interpretRelation M (r, map (interpretTerm M V) tms);
2.503 + interpretRelation M (r, List.map (interpretTerm M V) tms);
2.504
2.505 fun interpretFormula M =
2.506 let
2.507 @@ -16325,7 +16347,7 @@
2.508 Metis_Term.Var v => (ModelVar, getValuation V v)
2.509 | Metis_Term.Fn (f,tms) =>
2.510 let
2.511 - val (tms,xs) = unzip (map modelTm tms)
2.512 + val (tms,xs) = unzip (List.map modelTm tms)
2.513 in
2.514 (ModelFn (f,tms,xs), interpretFunction M (f,xs))
2.515 end
2.516 @@ -16408,7 +16430,7 @@
2.517 let
2.518 fun onTarget ys = interpretRelation M (rel,ys) = target
2.519
2.520 - val (tms,xs) = unzip (map (modelTerm M V) tms)
2.521 + val (tms,xs) = unzip (List.map (modelTerm M V) tms)
2.522
2.523 val rel_xs = (rel,xs)
2.524
2.525 @@ -16424,7 +16446,7 @@
2.526 fun pertClause M V cl acc = Metis_LiteralSet.foldl (pertLiteral M V) acc cl;
2.527
2.528 fun pickPerturb M perts =
2.529 - if null perts then ()
2.530 + if List.null perts then ()
2.531 else perturb M (List.nth (perts, Metis_Portable.randomInt (length perts)));
2.532 in
2.533 fun perturbTerm M V (tm,target) =
2.534 @@ -16564,16 +16586,16 @@
2.535 Metis_Formula.listMkDisj (Metis_LiteralSet.transform Metis_Literal.toFormula cl);
2.536 in
2.537 fun toFormula prob =
2.538 - Metis_Formula.listMkConj (map clauseToFormula (toClauses prob));
2.539 + Metis_Formula.listMkConj (List.map clauseToFormula (toClauses prob));
2.540
2.541 fun toGoal {axioms,conjecture} =
2.542 let
2.543 val clToFm = Metis_Formula.generalize o clauseToFormula
2.544 - val clsToFm = Metis_Formula.listMkConj o map clToFm
2.545 + val clsToFm = Metis_Formula.listMkConj o List.map clToFm
2.546
2.547 val fm = Metis_Formula.False
2.548 val fm =
2.549 - if null conjecture then fm
2.550 + if List.null conjecture then fm
2.551 else Metis_Formula.Imp (clsToFm conjecture, fm)
2.552 val fm = Metis_Formula.Imp (clsToFm axioms, fm)
2.553 in
2.554 @@ -16641,7 +16663,7 @@
2.555 val horn =
2.556 if List.exists Metis_LiteralSet.null cls then Trivial
2.557 else if List.all (fn cl => Metis_LiteralSet.size cl = 1) cls then Unit
2.558 - else
2.559 + else
2.560 let
2.561 fun pos cl = Metis_LiteralSet.count Metis_Literal.positive cl <= 1
2.562 fun neg cl = Metis_LiteralSet.count Metis_Literal.negative cl <= 1
2.563 @@ -16786,7 +16808,7 @@
2.564 fun equalFnQterm f1 f2 = compareFnQterm (f1,f2) = EQUAL;
2.565
2.566 fun termToQterm (Metis_Term.Var _) = Var
2.567 - | termToQterm (Metis_Term.Fn (f,l)) = Fn ((f, length l), map termToQterm l);
2.568 + | termToQterm (Metis_Term.Fn (f,l)) = Fn ((f, length l), List.map termToQterm l);
2.569
2.570 local
2.571 fun qm [] = true
2.572 @@ -16852,7 +16874,7 @@
2.573
2.574 local
2.575 fun qtermToTerm Var = anonymousVar
2.576 - | qtermToTerm (Fn ((f,_),l)) = Metis_Term.Fn (f, map qtermToTerm l);
2.577 + | qtermToTerm (Fn ((f,_),l)) = Metis_Term.Fn (f, List.map qtermToTerm l);
2.578 in
2.579 val ppQterm = Metis_Print.ppMap qtermToTerm Metis_Term.pp;
2.580 end;
2.581 @@ -17075,7 +17097,7 @@
2.582
2.583 fun fifoize ({fifo, ...} : parameters) l = if fifo then sort idwise l else l;
2.584 in
2.585 - fun finally parm l = map snd (fifoize parm l);
2.586 + fun finally parm l = List.map snd (fifoize parm l);
2.587 end;
2.588
2.589 local
2.590 @@ -17966,7 +17988,7 @@
2.591 fun ppWeight (Weight (m,c)) =
2.592 let
2.593 val l = Metis_NameMap.toList m
2.594 - val l = map (fn (v,n) => (SOME v, n)) l
2.595 + val l = List.map (fn (v,n) => (SOME v, n)) l
2.596 val l = if c = 0 then l else l @ [(NONE,c)]
2.597 in
2.598 ppWeightList l
2.599 @@ -18243,7 +18265,7 @@
2.600
2.601 fun ppField f ppA a =
2.602 Metis_Print.blockProgram Metis_Print.Inconsistent 2
2.603 - [Metis_Print.addString (f ^ " ="),
2.604 + [Metis_Print.ppString (f ^ " ="),
2.605 Metis_Print.addBreak 1,
2.606 ppA a];
2.607
2.608 @@ -18269,24 +18291,24 @@
2.609 in
2.610 fun pp (Metis_Rewrite {known,redexes,subterms,waiting,...}) =
2.611 Metis_Print.blockProgram Metis_Print.Inconsistent 2
2.612 - [Metis_Print.addString "Metis_Rewrite",
2.613 + [Metis_Print.ppString "Metis_Rewrite",
2.614 Metis_Print.addBreak 1,
2.615 Metis_Print.blockProgram Metis_Print.Inconsistent 1
2.616 - [Metis_Print.addString "{",
2.617 + [Metis_Print.ppString "{",
2.618 ppKnown known,
2.619 (*MetisTrace5
2.620 - Metis_Print.addString ",",
2.621 + Metis_Print.ppString ",",
2.622 Metis_Print.addBreak 1,
2.623 ppRedexes redexes,
2.624 - Metis_Print.addString ",",
2.625 + Metis_Print.ppString ",",
2.626 Metis_Print.addBreak 1,
2.627 ppSubterms subterms,
2.628 - Metis_Print.addString ",",
2.629 + Metis_Print.ppString ",",
2.630 Metis_Print.addBreak 1,
2.631 ppWaiting waiting,
2.632 *)
2.633 Metis_Print.skip],
2.634 - Metis_Print.addString "}"]
2.635 + Metis_Print.ppString "}"]
2.636 end;
2.637 *)
2.638
2.639 @@ -18349,10 +18371,15 @@
2.640 else
2.641 let
2.642 val Metis_Rewrite {order,redexes,subterms,waiting, ...} = rw
2.643 +
2.644 val ort = orderToOrient (order (fst eqn))
2.645 +
2.646 val known = Metis_IntMap.insert known (id,(eqn,ort))
2.647 +
2.648 val redexes = addRedexes id (eqn,ort) redexes
2.649 +
2.650 val waiting = Metis_IntSet.add waiting id
2.651 +
2.652 val rw =
2.653 Metis_Rewrite
2.654 {order = order, known = known, redexes = redexes,
2.655 @@ -18364,7 +18391,11 @@
2.656 rw
2.657 end;
2.658
2.659 -fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
2.660 +local
2.661 + fun uncurriedAdd (eqn,rw) = add rw eqn;
2.662 +in
2.663 + fun addList rw = List.foldl uncurriedAdd rw;
2.664 +end;
2.665
2.666 (* ------------------------------------------------------------------------- *)
2.667 (* Rewriting (the order must be a refinement of the rewrite order). *)
2.668 @@ -18797,7 +18828,7 @@
2.669 val ppResult = Metis_Print.ppPair pp (Metis_Print.ppList Metis_Print.ppInt)
2.670 val () = Metis_Print.trace ppResult "Metis_Rewrite.reduce': result" result
2.671 *)
2.672 - val ths = map (fn (id,((_,th),_)) => (id,th)) (Metis_IntMap.toList known')
2.673 + val ths = List.map (fn (id,((_,th),_)) => (id,th)) (Metis_IntMap.toList known')
2.674 val _ =
2.675 not (List.exists (uncurry (thmReducible order known')) ths) orelse
2.676 raise Bug "Metis_Rewrite.reduce': not fully reduced"
2.677 @@ -18824,7 +18855,11 @@
2.678 end;
2.679 end;
2.680
2.681 -fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
2.682 +local
2.683 + val order : reductionOrder = K (SOME GREATER);
2.684 +in
2.685 + val rewrite = orderedRewrite order;
2.686 +end;
2.687
2.688 end
2.689
2.690 @@ -19172,7 +19207,7 @@
2.691
2.692 val default : parameters =
2.693 {ordering = Metis_KnuthBendixOrder.default,
2.694 - orderLiterals = UnsignedLiteralOrder,
2.695 + orderLiterals = PositiveLiteralOrder,
2.696 orderTerms = true};
2.697
2.698 fun mk info = Metis_Clause info
2.699 @@ -19364,7 +19399,7 @@
2.700
2.701 fun apply sub = new parameters (Metis_Thm.subst sub thm)
2.702 in
2.703 - map apply (Metis_Rule.factor' lits)
2.704 + List.map apply (Metis_Rule.factor' lits)
2.705 end;
2.706
2.707 (*MetisTrace5
2.708 @@ -20409,8 +20444,8 @@
2.709 Metis_Clause.mk {parameters = clause, id = Metis_Clause.newId (), thm = th}
2.710
2.711 val active = empty parameters
2.712 - val (active,axioms) = factor active (map mk_clause axioms)
2.713 - val (active,conjecture) = factor active (map mk_clause conjecture)
2.714 + val (active,axioms) = factor active (List.map mk_clause axioms)
2.715 + val (active,conjecture) = factor active (List.map mk_clause conjecture)
2.716 in
2.717 (active, {axioms = axioms, conjecture = conjecture})
2.718 end;
2.719 @@ -20591,7 +20626,7 @@
2.720 val pp =
2.721 Metis_Print.ppMap
2.722 (fn Metis_Waiting {clauses,...} =>
2.723 - map (fn (w,(_,cl)) => (w, Metis_Clause.id cl, cl)) (Metis_Heap.toList clauses))
2.724 + List.map (fn (w,(_,cl)) => (w, Metis_Clause.id cl, cl)) (Metis_Heap.toList clauses))
2.725 (Metis_Print.ppList (Metis_Print.ppTriple Metis_Print.ppReal Metis_Print.ppInt Metis_Clause.pp));
2.726 *)
2.727
2.728 @@ -20609,10 +20644,10 @@
2.729 (fvs,lits)
2.730 end;
2.731
2.732 -val mkModelClauses = map mkModelClause;
2.733 +val mkModelClauses = List.map mkModelClause;
2.734
2.735 fun perturbModel M cls =
2.736 - if null cls then K ()
2.737 + if List.null cls then K ()
2.738 else
2.739 let
2.740 val N = {size = Metis_Model.size M}
2.741 @@ -20723,6 +20758,14 @@
2.742 val Metis_Waiting {parameters,clauses,models} = waiting
2.743 val {models = modelParameters, ...} = parameters
2.744
2.745 +(*MetisDebug
2.746 + val _ = not (List.null cls) orelse
2.747 + raise Bug "Metis_Waiting.add': null"
2.748 +
2.749 + val _ = length mcls = length cls orelse
2.750 + raise Bug "Metis_Waiting.add': different lengths"
2.751 +*)
2.752 +
2.753 val dist = dist + Math.ln (Real.fromInt (length cls))
2.754
2.755 fun addCl ((mcl,cl),acc) =
2.756 @@ -20739,22 +20782,23 @@
2.757 Metis_Waiting {parameters = parameters, clauses = clauses, models = models}
2.758 end;
2.759
2.760 -fun add waiting (_,[]) = waiting
2.761 - | add waiting (dist,cls) =
2.762 - let
2.763 +fun add waiting (dist,cls) =
2.764 + if List.null cls then waiting
2.765 + else
2.766 + let
2.767 (*MetisTrace3
2.768 - val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
2.769 - val () = Metis_Print.trace (Metis_Print.ppList Metis_Clause.pp) "Metis_Waiting.add: cls" cls
2.770 -*)
2.771 -
2.772 - val waiting = add' waiting dist (mkModelClauses cls) cls
2.773 + val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
2.774 + val () = Metis_Print.trace (Metis_Print.ppList Metis_Clause.pp) "Metis_Waiting.add: cls" cls
2.775 +*)
2.776 +
2.777 + val waiting = add' waiting dist (mkModelClauses cls) cls
2.778
2.779 (*MetisTrace3
2.780 - val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
2.781 -*)
2.782 - in
2.783 - waiting
2.784 - end;
2.785 + val () = Metis_Print.trace pp "Metis_Waiting.add: waiting" waiting
2.786 +*)
2.787 + in
2.788 + waiting
2.789 + end;
2.790
2.791 local
2.792 fun cmp ((w1,_),(w2,_)) = Real.compare (w1,w2);
2.793 @@ -20763,7 +20807,7 @@
2.794 let
2.795 val {models = modelParameters, ...} = parameters
2.796 val clauses = Metis_Heap.new cmp
2.797 - and models = map (initialModel axioms conjecture) modelParameters
2.798 + and models = List.map (initialModel axioms conjecture) modelParameters
2.799 in
2.800 Metis_Waiting {parameters = parameters, clauses = clauses, models = models}
2.801 end;
2.802 @@ -20775,8 +20819,17 @@
2.803
2.804 val waiting = empty parameters mAxioms mConjecture
2.805 in
2.806 - add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
2.807 - end;
2.808 + if List.null axioms andalso List.null conjecture then waiting
2.809 + else add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
2.810 + end
2.811 +(*MetisDebug
2.812 + handle e =>
2.813 + let
2.814 + val () = Metis_Print.trace Metis_Print.ppException "Metis_Waiting.new: exception" e
2.815 + in
2.816 + raise e
2.817 + end;
2.818 +*)
2.819 end;
2.820
2.821 (* ------------------------------------------------------------------------- *)
2.822 @@ -20788,9 +20841,12 @@
2.823 else
2.824 let
2.825 val ((_,dcl),clauses) = Metis_Heap.remove clauses
2.826 +
2.827 val waiting =
2.828 Metis_Waiting
2.829 - {parameters = parameters, clauses = clauses, models = models}
2.830 + {parameters = parameters,
2.831 + clauses = clauses,
2.832 + models = models}
2.833 in
2.834 SOME (dcl,waiting)
2.835 end;
2.836 @@ -20888,11 +20944,21 @@
2.837 fun new parameters ths =
2.838 let
2.839 val {active = activeParm, waiting = waitingParm} = parameters
2.840 +
2.841 val (active,cls) = Metis_Active.new activeParm ths (* cls = factored ths *)
2.842 +
2.843 val waiting = Metis_Waiting.new waitingParm cls
2.844 in
2.845 Metis_Resolution {parameters = parameters, active = active, waiting = waiting}
2.846 - end;
2.847 + end
2.848 +(*MetisDebug
2.849 + handle e =>
2.850 + let
2.851 + val () = Metis_Print.trace Metis_Print.ppException "Metis_Resolution.new: exception" e
2.852 + in
2.853 + raise e
2.854 + end;
2.855 +*)
2.856
2.857 fun active (Metis_Resolution {active = a, ...}) = a;
2.858
2.859 @@ -20917,9 +20983,10 @@
2.860 Decided of decision
2.861 | Undecided of resolution;
2.862
2.863 -fun iterate resolution =
2.864 - let
2.865 - val Metis_Resolution {parameters,active,waiting} = resolution
2.866 +fun iterate res =
2.867 + let
2.868 + val Metis_Resolution {parameters,active,waiting} = res
2.869 +
2.870 (*MetisTrace2
2.871 val () = Metis_Print.trace Metis_Active.pp "Metis_Resolution.iterate: active" active
2.872 val () = Metis_Print.trace Metis_Waiting.pp "Metis_Resolution.iterate: waiting" waiting
2.873 @@ -20927,7 +20994,11 @@
2.874 in
2.875 case Metis_Waiting.remove waiting of
2.876 NONE =>
2.877 - Decided (Satisfiable (map Metis_Clause.thm (Metis_Active.saturation active)))
2.878 + let
2.879 + val sat = Satisfiable (List.map Metis_Clause.thm (Metis_Active.saturation active))
2.880 + in
2.881 + Decided sat
2.882 + end
2.883 | SOME ((d,cl),waiting) =>
2.884 if Metis_Clause.isContradiction cl then
2.885 Decided (Contradiction (Metis_Clause.thm cl))
2.886 @@ -20937,18 +21008,23 @@
2.887 val () = Metis_Print.trace Metis_Clause.pp "Metis_Resolution.iterate: cl" cl
2.888 *)
2.889 val (active,cls) = Metis_Active.add active cl
2.890 +
2.891 val waiting = Metis_Waiting.add waiting (d,cls)
2.892 - in
2.893 - Undecided
2.894 - (Metis_Resolution
2.895 - {parameters = parameters, active = active, waiting = waiting})
2.896 - end
2.897 - end;
2.898 -
2.899 -fun loop resolution =
2.900 - case iterate resolution of
2.901 - Decided decision => decision
2.902 - | Undecided resolution => loop resolution;
2.903 +
2.904 + val res =
2.905 + Metis_Resolution
2.906 + {parameters = parameters,
2.907 + active = active,
2.908 + waiting = waiting}
2.909 + in
2.910 + Undecided res
2.911 + end
2.912 + end;
2.913 +
2.914 +fun loop res =
2.915 + case iterate res of
2.916 + Decided dec => dec
2.917 + | Undecided res => loop res;
2.918
2.919 end
2.920 ;
3.1 --- a/src/Tools/Metis/src/Active.sml Thu Mar 24 17:49:27 2011 +0100
3.2 +++ b/src/Tools/Metis/src/Active.sml Thu Mar 24 17:49:27 2011 +0100
3.3 @@ -876,8 +876,8 @@
3.4 Clause.mk {parameters = clause, id = Clause.newId (), thm = th}
3.5
3.6 val active = empty parameters
3.7 - val (active,axioms) = factor active (map mk_clause axioms)
3.8 - val (active,conjecture) = factor active (map mk_clause conjecture)
3.9 + val (active,axioms) = factor active (List.map mk_clause axioms)
3.10 + val (active,conjecture) = factor active (List.map mk_clause conjecture)
3.11 in
3.12 (active, {axioms = axioms, conjecture = conjecture})
3.13 end;
4.1 --- a/src/Tools/Metis/src/Atom.sml Thu Mar 24 17:49:27 2011 +0100
4.2 +++ b/src/Tools/Metis/src/Atom.sml Thu Mar 24 17:49:27 2011 +0100
4.3 @@ -84,7 +84,7 @@
4.4
4.5 fun subterms ((_,tms) : atom) =
4.6 let
4.7 - fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
4.8 + fun f ((n,tm),l) = List.map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
4.9 in
4.10 List.foldl f [] (enumerate tms)
4.11 end;
5.1 --- a/src/Tools/Metis/src/Clause.sml Thu Mar 24 17:49:27 2011 +0100
5.2 +++ b/src/Tools/Metis/src/Clause.sml Thu Mar 24 17:49:27 2011 +0100
5.3 @@ -69,7 +69,7 @@
5.4
5.5 val default : parameters =
5.6 {ordering = KnuthBendixOrder.default,
5.7 - orderLiterals = UnsignedLiteralOrder,
5.8 + orderLiterals = PositiveLiteralOrder,
5.9 orderTerms = true};
5.10
5.11 fun mk info = Clause info
5.12 @@ -261,7 +261,7 @@
5.13
5.14 fun apply sub = new parameters (Thm.subst sub thm)
5.15 in
5.16 - map apply (Rule.factor' lits)
5.17 + List.map apply (Rule.factor' lits)
5.18 end;
5.19
5.20 (*MetisTrace5
6.1 --- a/src/Tools/Metis/src/Formula.sml Thu Mar 24 17:49:27 2011 +0100
6.2 +++ b/src/Tools/Metis/src/Formula.sml Thu Mar 24 17:49:27 2011 +0100
6.3 @@ -517,9 +517,9 @@
6.4
6.5 fun promote (Term.Var v) = Atom (v,[])
6.6 | promote (Term.Fn (f,tms)) =
6.7 - if Name.equal f truthName andalso null tms then
6.8 + if Name.equal f truthName andalso List.null tms then
6.9 True
6.10 - else if Name.equal f falsityName andalso null tms then
6.11 + else if Name.equal f falsityName andalso List.null tms then
6.12 False
6.13 else if Name.toString f = !Term.negation andalso length tms = 1 then
6.14 Not (promote (hd tms))
6.15 @@ -549,7 +549,7 @@
6.16
6.17 local
6.18 fun add_asms asms goal =
6.19 - if null asms then goal else Imp (listMkConj (rev asms), goal);
6.20 + if List.null asms then goal else Imp (listMkConj (rev asms), goal);
6.21
6.22 fun add_var_asms asms v goal = add_asms asms (Forall (v,goal));
6.23
6.24 @@ -563,7 +563,7 @@
6.25 | (true, Imp (f1,f2)) => split (f1 :: asms) true f2
6.26 | (true, Iff (f1,f2)) =>
6.27 split (f1 :: asms) true f2 @ split (f2 :: asms) true f1
6.28 - | (true, Forall (v,f)) => map (add_var_asms asms v) (split [] true f)
6.29 + | (true, Forall (v,f)) => List.map (add_var_asms asms v) (split [] true f)
6.30 (* Negative splittables *)
6.31 | (false,False) => []
6.32 | (false, Not f) => split asms true f
6.33 @@ -573,7 +573,7 @@
6.34 | (false, Imp (f1,f2)) => split asms true f1 @ split (f1 :: asms) false f2
6.35 | (false, Iff (f1,f2)) =>
6.36 split (f1 :: asms) false f2 @ split (f2 :: asms) false f1
6.37 - | (false, Exists (v,f)) => map (add_var_asms asms v) (split [] false f)
6.38 + | (false, Exists (v,f)) => List.map (add_var_asms asms v) (split [] false f)
6.39 (* Unsplittables *)
6.40 | _ => [add_asms asms (if pol then fm else Not fm)];
6.41 in
7.1 --- a/src/Tools/Metis/src/KnuthBendixOrder.sml Thu Mar 24 17:49:27 2011 +0100
7.2 +++ b/src/Tools/Metis/src/KnuthBendixOrder.sml Thu Mar 24 17:49:27 2011 +0100
7.3 @@ -113,7 +113,7 @@
7.4 fun ppWeight (Weight (m,c)) =
7.5 let
7.6 val l = NameMap.toList m
7.7 - val l = map (fn (v,n) => (SOME v, n)) l
7.8 + val l = List.map (fn (v,n) => (SOME v, n)) l
7.9 val l = if c = 0 then l else l @ [(NONE,c)]
7.10 in
7.11 ppWeightList l
8.1 --- a/src/Tools/Metis/src/Model.sml Thu Mar 24 17:49:27 2011 +0100
8.2 +++ b/src/Tools/Metis/src/Model.sml Thu Mar 24 17:49:27 2011 +0100
8.3 @@ -268,7 +268,7 @@
8.4 local
8.5 fun mkEntry tag (na,n) = (tag,na,n);
8.6
8.7 - fun mkList tag m = map (mkEntry tag) (NameArityMap.toList m);
8.8 + fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m);
8.9
8.10 fun ppEntry (tag,source_arity,target) =
8.11 Print.blockProgram Print.Inconsistent 2
8.12 @@ -288,7 +288,7 @@
8.13 | entry :: entries =>
8.14 Print.blockProgram Print.Consistent 0
8.15 (ppEntry entry ::
8.16 - map (Print.sequence Print.addNewline o ppEntry) entries)
8.17 + List.map (Print.sequence Print.addNewline o ppEntry) entries)
8.18 end;
8.19 end;
8.20
8.21 @@ -334,7 +334,7 @@
8.22 end;
8.23
8.24 val projectionFixed =
8.25 - unionListFixed (map arityProjectionFixed projectionList);
8.26 + unionListFixed (List.map arityProjectionFixed projectionList);
8.27
8.28 (* Arithmetic *)
8.29
8.30 @@ -437,7 +437,7 @@
8.31 let
8.32 val fns =
8.33 NameArityMap.fromList
8.34 - (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
8.35 + (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
8.36 numeralList @
8.37 [((addName,2), fixed2 addFn),
8.38 ((divName,2), fixed2 divFn),
8.39 @@ -537,7 +537,7 @@
8.40 let
8.41 val fns =
8.42 NameArityMap.fromList
8.43 - (map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
8.44 + (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
8.45 numeralList @
8.46 [((addName,2), fixed2 addFn),
8.47 ((divName,2), fixed2 divFn),
8.48 @@ -1029,13 +1029,13 @@
8.49 fun interpret tm =
8.50 case destTerm tm of
8.51 Term.Var v => getValuation V v
8.52 - | Term.Fn (f,tms) => interpretFunction M (f, map interpret tms)
8.53 + | Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
8.54 in
8.55 interpret
8.56 end;
8.57
8.58 fun interpretAtom M V (r,tms) =
8.59 - interpretRelation M (r, map (interpretTerm M V) tms);
8.60 + interpretRelation M (r, List.map (interpretTerm M V) tms);
8.61
8.62 fun interpretFormula M =
8.63 let
8.64 @@ -1152,7 +1152,7 @@
8.65 Term.Var v => (ModelVar, getValuation V v)
8.66 | Term.Fn (f,tms) =>
8.67 let
8.68 - val (tms,xs) = unzip (map modelTm tms)
8.69 + val (tms,xs) = unzip (List.map modelTm tms)
8.70 in
8.71 (ModelFn (f,tms,xs), interpretFunction M (f,xs))
8.72 end
8.73 @@ -1235,7 +1235,7 @@
8.74 let
8.75 fun onTarget ys = interpretRelation M (rel,ys) = target
8.76
8.77 - val (tms,xs) = unzip (map (modelTerm M V) tms)
8.78 + val (tms,xs) = unzip (List.map (modelTerm M V) tms)
8.79
8.80 val rel_xs = (rel,xs)
8.81
8.82 @@ -1251,7 +1251,7 @@
8.83 fun pertClause M V cl acc = LiteralSet.foldl (pertLiteral M V) acc cl;
8.84
8.85 fun pickPerturb M perts =
8.86 - if null perts then ()
8.87 + if List.null perts then ()
8.88 else perturb M (List.nth (perts, Portable.randomInt (length perts)));
8.89 in
8.90 fun perturbTerm M V (tm,target) =
9.1 --- a/src/Tools/Metis/src/Name.sig Thu Mar 24 17:49:27 2011 +0100
9.2 +++ b/src/Tools/Metis/src/Name.sig Thu Mar 24 17:49:27 2011 +0100
9.3 @@ -28,9 +28,9 @@
9.4
9.5 val newNames : int -> name list
9.6
9.7 -val variantPrime : (name -> bool) -> name -> name
9.8 +val variantPrime : {avoid : name -> bool} -> name -> name
9.9
9.10 -val variantNum : (name -> bool) -> name -> name
9.11 +val variantNum : {avoid : name -> bool} -> name -> name
9.12
9.13 (* ------------------------------------------------------------------------- *)
9.14 (* Parsing and pretty printing. *)
10.1 --- a/src/Tools/Metis/src/Name.sml Thu Mar 24 17:49:27 2011 +0100
10.2 +++ b/src/Tools/Metis/src/Name.sml Thu Mar 24 17:49:27 2011 +0100
10.3 @@ -33,22 +33,21 @@
10.4 in
10.5 fun newName () = numName (newInt ());
10.6
10.7 - fun newNames n = map numName (newInts n);
10.8 + fun newNames n = List.map numName (newInts n);
10.9 end;
10.10
10.11 -fun variantPrime acceptable =
10.12 +fun variantPrime {avoid} =
10.13 let
10.14 - fun variant n = if acceptable n then n else variant (n ^ "'")
10.15 + fun variant n = if avoid n then variant (n ^ "'") else n
10.16 in
10.17 variant
10.18 end;
10.19
10.20 local
10.21 - fun isDigitOrPrime #"'" = true
10.22 - | isDigitOrPrime c = Char.isDigit c;
10.23 + fun isDigitOrPrime c = c = #"'" orelse Char.isDigit c;
10.24 in
10.25 - fun variantNum acceptable n =
10.26 - if acceptable n then n
10.27 + fun variantNum {avoid} n =
10.28 + if not (avoid n) then n
10.29 else
10.30 let
10.31 val n = stripSuffix isDigitOrPrime n
10.32 @@ -57,7 +56,7 @@
10.33 let
10.34 val n_i = n ^ Int.toString i
10.35 in
10.36 - if acceptable n_i then n_i else variant (i + 1)
10.37 + if avoid n_i then variant (i + 1) else n_i
10.38 end
10.39 in
10.40 variant 0
11.1 --- a/src/Tools/Metis/src/Normalize.sml Thu Mar 24 17:49:27 2011 +0100
11.2 +++ b/src/Tools/Metis/src/Normalize.sml Thu Mar 24 17:49:27 2011 +0100
11.3 @@ -951,11 +951,11 @@
11.4
11.5 val deps = List.filter (isUnproved proved) pars
11.6 in
11.7 - if null deps then
11.8 + if List.null deps then
11.9 let
11.10 val (fm,inf) = destThm th
11.11
11.12 - val fms = map (lookupProved proved) pars
11.13 + val fms = List.map (lookupProved proved) pars
11.14
11.15 val acc = (fm,inf,fms) :: acc
11.16
11.17 @@ -1382,7 +1382,7 @@
11.18 let
11.19 val cls = proveCnf [mkAxiom fm]
11.20 in
11.21 - map fst cls
11.22 + List.map fst cls
11.23 end;
11.24
11.25 end
12.1 --- a/src/Tools/Metis/src/Options.sml Thu Mar 24 17:49:27 2011 +0100
12.2 +++ b/src/Tools/Metis/src/Options.sml Thu Mar 24 17:49:27 2011 +0100
12.3 @@ -155,7 +155,7 @@
12.4 [{leftAlign = true, padChar = #"."},
12.5 {leftAlign = true, padChar = #" "}]
12.6
12.7 - val table = alignTable alignment (map listOpts options)
12.8 + val table = alignTable alignment (List.map listOpts options)
12.9 in
12.10 header ^ join "\n" table ^ "\n" ^ footer
12.11 end;
13.1 --- a/src/Tools/Metis/src/PortableMosml.sml Thu Mar 24 17:49:27 2011 +0100
13.2 +++ b/src/Tools/Metis/src/PortableMosml.sml Thu Mar 24 17:49:27 2011 +0100
13.3 @@ -67,7 +67,7 @@
13.4 val _ = catch_interrupt true;
13.5
13.6 (* ------------------------------------------------------------------------- *)
13.7 -(* Forcing fully qualified names of some key functions. *)
13.8 +(* Forcing fully qualified names of functions with generic names. *)
13.9 (* ------------------------------------------------------------------------- *)
13.10
13.11 (*BasicDebug
13.12 @@ -75,6 +75,8 @@
13.13 and foldl = ()
13.14 and foldr = ()
13.15 and implode = ()
13.16 +and map = ()
13.17 +and null = ()
13.18 and print = ();
13.19 *)
13.20
13.21 @@ -112,10 +114,18 @@
13.22
13.23 fun OS_Process_isSuccess s = s = OS.Process.success;
13.24
13.25 -fun String_concatWith s l =
13.26 - case l of
13.27 - [] => ""
13.28 - | h :: t => List.foldl (fn (x,y) => y ^ s ^ x) h t;
13.29 +fun String_concatWith s =
13.30 + let
13.31 + fun add (x,l) = s :: x :: l
13.32 + in
13.33 + fn [] => ""
13.34 + | x :: xs =>
13.35 + let
13.36 + val xs = List.foldl add [] (rev xs)
13.37 + in
13.38 + String.concat (x :: xs)
13.39 + end
13.40 + end;
13.41
13.42 fun String_isSubstring p s =
13.43 let
14.1 --- a/src/Tools/Metis/src/Print.sig Thu Mar 24 17:49:27 2011 +0100
14.2 +++ b/src/Tools/Metis/src/Print.sig Thu Mar 24 17:49:27 2011 +0100
14.3 @@ -131,6 +131,8 @@
14.4
14.5 val ppPpstream : ppstream pp
14.6
14.7 +val ppException : exn pp
14.8 +
14.9 (* ------------------------------------------------------------------------- *)
14.10 (* Pretty-printing infix operators. *)
14.11 (* ------------------------------------------------------------------------- *)
15.1 --- a/src/Tools/Metis/src/Print.sml Thu Mar 24 17:49:27 2011 +0100
15.2 +++ b/src/Tools/Metis/src/Print.sml Thu Mar 24 17:49:27 2011 +0100
15.3 @@ -46,7 +46,7 @@
15.4
15.5 fun escapeString {escape} =
15.6 let
15.7 - val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
15.8 + val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape
15.9
15.10 fun escapeChar c =
15.11 case c of
15.12 @@ -215,7 +215,7 @@
15.13 let
15.14 val Block {indent = _, style = _, size, chunks} = block
15.15
15.16 - val empty = null chunks
15.17 + val empty = List.null chunks
15.18
15.19 (*BasicDebug
15.20 val _ = not empty orelse size = 0 orelse
15.21 @@ -787,7 +787,7 @@
15.22 lines
15.23 end
15.24 in
15.25 - if null lines then Stream.Nil else Stream.singleton lines
15.26 + if List.null lines then Stream.Nil else Stream.singleton lines
15.27 end;
15.28 in
15.29 fun execute {lineLength} =
15.30 @@ -860,7 +860,7 @@
15.31 fun ppOpA a = sequence (ppOp' s) (ppA a)
15.32 in
15.33 fn [] => skip
15.34 - | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
15.35 + | h :: t => blockProgram Inconsistent 0 (ppA h :: List.map ppOpA t)
15.36 end;
15.37
15.38 fun ppOpStream' s ppA =
15.39 @@ -1012,6 +1012,8 @@
15.40
15.41 val ppPpstream = ppStream ppStep;
15.42
15.43 +fun ppException e = ppString (exnMessage e);
15.44 +
15.45 (* ------------------------------------------------------------------------- *)
15.46 (* Pretty-printing infix operators. *)
15.47 (* ------------------------------------------------------------------------- *)
16.1 --- a/src/Tools/Metis/src/Problem.sml Thu Mar 24 17:49:27 2011 +0100
16.2 +++ b/src/Tools/Metis/src/Problem.sml Thu Mar 24 17:49:27 2011 +0100
16.3 @@ -44,16 +44,16 @@
16.4 Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
16.5 in
16.6 fun toFormula prob =
16.7 - Formula.listMkConj (map clauseToFormula (toClauses prob));
16.8 + Formula.listMkConj (List.map clauseToFormula (toClauses prob));
16.9
16.10 fun toGoal {axioms,conjecture} =
16.11 let
16.12 val clToFm = Formula.generalize o clauseToFormula
16.13 - val clsToFm = Formula.listMkConj o map clToFm
16.14 + val clsToFm = Formula.listMkConj o List.map clToFm
16.15
16.16 val fm = Formula.False
16.17 val fm =
16.18 - if null conjecture then fm
16.19 + if List.null conjecture then fm
16.20 else Formula.Imp (clsToFm conjecture, fm)
16.21 val fm = Formula.Imp (clsToFm axioms, fm)
16.22 in
16.23 @@ -121,7 +121,7 @@
16.24 val horn =
16.25 if List.exists LiteralSet.null cls then Trivial
16.26 else if List.all (fn cl => LiteralSet.size cl = 1) cls then Unit
16.27 - else
16.28 + else
16.29 let
16.30 fun pos cl = LiteralSet.count Literal.positive cl <= 1
16.31 fun neg cl = LiteralSet.count Literal.negative cl <= 1
17.1 --- a/src/Tools/Metis/src/Proof.sml Thu Mar 24 17:49:27 2011 +0100
17.2 +++ b/src/Tools/Metis/src/Proof.sml Thu Mar 24 17:49:27 2011 +0100
17.3 @@ -133,7 +133,7 @@
17.4 Print.blockProgram Print.Consistent 0
17.5 [Print.ppString "START OF PROOF",
17.6 Print.addNewline,
17.7 - Print.program (map ppStep prf),
17.8 + Print.program (List.map ppStep prf),
17.9 Print.ppString "END OF PROOF"]
17.10 end
17.11 (*MetisDebug
18.1 --- a/src/Tools/Metis/src/Resolution.sml Thu Mar 24 17:49:27 2011 +0100
18.2 +++ b/src/Tools/Metis/src/Resolution.sml Thu Mar 24 17:49:27 2011 +0100
18.3 @@ -33,11 +33,21 @@
18.4 fun new parameters ths =
18.5 let
18.6 val {active = activeParm, waiting = waitingParm} = parameters
18.7 +
18.8 val (active,cls) = Active.new activeParm ths (* cls = factored ths *)
18.9 +
18.10 val waiting = Waiting.new waitingParm cls
18.11 in
18.12 Resolution {parameters = parameters, active = active, waiting = waiting}
18.13 - end;
18.14 + end
18.15 +(*MetisDebug
18.16 + handle e =>
18.17 + let
18.18 + val () = Print.trace Print.ppException "Resolution.new: exception" e
18.19 + in
18.20 + raise e
18.21 + end;
18.22 +*)
18.23
18.24 fun active (Resolution {active = a, ...}) = a;
18.25
18.26 @@ -62,9 +72,10 @@
18.27 Decided of decision
18.28 | Undecided of resolution;
18.29
18.30 -fun iterate resolution =
18.31 +fun iterate res =
18.32 let
18.33 - val Resolution {parameters,active,waiting} = resolution
18.34 + val Resolution {parameters,active,waiting} = res
18.35 +
18.36 (*MetisTrace2
18.37 val () = Print.trace Active.pp "Resolution.iterate: active" active
18.38 val () = Print.trace Waiting.pp "Resolution.iterate: waiting" waiting
18.39 @@ -72,7 +83,11 @@
18.40 in
18.41 case Waiting.remove waiting of
18.42 NONE =>
18.43 - Decided (Satisfiable (map Clause.thm (Active.saturation active)))
18.44 + let
18.45 + val sat = Satisfiable (List.map Clause.thm (Active.saturation active))
18.46 + in
18.47 + Decided sat
18.48 + end
18.49 | SOME ((d,cl),waiting) =>
18.50 if Clause.isContradiction cl then
18.51 Decided (Contradiction (Clause.thm cl))
18.52 @@ -82,17 +97,22 @@
18.53 val () = Print.trace Clause.pp "Resolution.iterate: cl" cl
18.54 *)
18.55 val (active,cls) = Active.add active cl
18.56 +
18.57 val waiting = Waiting.add waiting (d,cls)
18.58 +
18.59 + val res =
18.60 + Resolution
18.61 + {parameters = parameters,
18.62 + active = active,
18.63 + waiting = waiting}
18.64 in
18.65 - Undecided
18.66 - (Resolution
18.67 - {parameters = parameters, active = active, waiting = waiting})
18.68 + Undecided res
18.69 end
18.70 end;
18.71
18.72 -fun loop resolution =
18.73 - case iterate resolution of
18.74 - Decided decision => decision
18.75 - | Undecided resolution => loop resolution;
18.76 +fun loop res =
18.77 + case iterate res of
18.78 + Decided dec => dec
18.79 + | Undecided res => loop res;
18.80
18.81 end
19.1 --- a/src/Tools/Metis/src/Rewrite.sml Thu Mar 24 17:49:27 2011 +0100
19.2 +++ b/src/Tools/Metis/src/Rewrite.sml Thu Mar 24 17:49:27 2011 +0100
19.3 @@ -86,7 +86,7 @@
19.4
19.5 fun ppField f ppA a =
19.6 Print.blockProgram Print.Inconsistent 2
19.7 - [Print.addString (f ^ " ="),
19.8 + [Print.ppString (f ^ " ="),
19.9 Print.addBreak 1,
19.10 ppA a];
19.11
19.12 @@ -112,24 +112,24 @@
19.13 in
19.14 fun pp (Rewrite {known,redexes,subterms,waiting,...}) =
19.15 Print.blockProgram Print.Inconsistent 2
19.16 - [Print.addString "Rewrite",
19.17 + [Print.ppString "Rewrite",
19.18 Print.addBreak 1,
19.19 Print.blockProgram Print.Inconsistent 1
19.20 - [Print.addString "{",
19.21 + [Print.ppString "{",
19.22 ppKnown known,
19.23 (*MetisTrace5
19.24 - Print.addString ",",
19.25 + Print.ppString ",",
19.26 Print.addBreak 1,
19.27 ppRedexes redexes,
19.28 - Print.addString ",",
19.29 + Print.ppString ",",
19.30 Print.addBreak 1,
19.31 ppSubterms subterms,
19.32 - Print.addString ",",
19.33 + Print.ppString ",",
19.34 Print.addBreak 1,
19.35 ppWaiting waiting,
19.36 *)
19.37 Print.skip],
19.38 - Print.addString "}"]
19.39 + Print.ppString "}"]
19.40 end;
19.41 *)
19.42
19.43 @@ -192,10 +192,15 @@
19.44 else
19.45 let
19.46 val Rewrite {order,redexes,subterms,waiting, ...} = rw
19.47 +
19.48 val ort = orderToOrient (order (fst eqn))
19.49 +
19.50 val known = IntMap.insert known (id,(eqn,ort))
19.51 +
19.52 val redexes = addRedexes id (eqn,ort) redexes
19.53 +
19.54 val waiting = IntSet.add waiting id
19.55 +
19.56 val rw =
19.57 Rewrite
19.58 {order = order, known = known, redexes = redexes,
19.59 @@ -207,7 +212,11 @@
19.60 rw
19.61 end;
19.62
19.63 -fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
19.64 +local
19.65 + fun uncurriedAdd (eqn,rw) = add rw eqn;
19.66 +in
19.67 + fun addList rw = List.foldl uncurriedAdd rw;
19.68 +end;
19.69
19.70 (* ------------------------------------------------------------------------- *)
19.71 (* Rewriting (the order must be a refinement of the rewrite order). *)
19.72 @@ -640,7 +649,7 @@
19.73 val ppResult = Print.ppPair pp (Print.ppList Print.ppInt)
19.74 val () = Print.trace ppResult "Rewrite.reduce': result" result
19.75 *)
19.76 - val ths = map (fn (id,((_,th),_)) => (id,th)) (IntMap.toList known')
19.77 + val ths = List.map (fn (id,((_,th),_)) => (id,th)) (IntMap.toList known')
19.78 val _ =
19.79 not (List.exists (uncurry (thmReducible order known')) ths) orelse
19.80 raise Bug "Rewrite.reduce': not fully reduced"
19.81 @@ -667,6 +676,10 @@
19.82 end;
19.83 end;
19.84
19.85 -fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
19.86 +local
19.87 + val order : reductionOrder = K (SOME GREATER);
19.88 +in
19.89 + val rewrite = orderedRewrite order;
19.90 +end;
19.91
19.92 end
20.1 --- a/src/Tools/Metis/src/Rule.sml Thu Mar 24 17:49:27 2011 +0100
20.2 +++ b/src/Tools/Metis/src/Rule.sml Thu Mar 24 17:49:27 2011 +0100
20.3 @@ -81,6 +81,7 @@
20.4 else
20.5 let
20.6 val sub = Subst.fromList [(xVarName,x),(yVarName,y)]
20.7 +
20.8 val symTh = Thm.subst sub symmetry
20.9 in
20.10 Thm.resolve lit th symTh
20.11 @@ -94,9 +95,9 @@
20.12
20.13 type equation = (Term.term * Term.term) * Thm.thm;
20.14
20.15 -fun ppEquation (_,th) = Thm.pp th;
20.16 +fun ppEquation ((_,th) : equation) = Thm.pp th;
20.17
20.18 -fun equationToString x = Print.toString ppEquation x;
20.19 +val equationToString = Print.toString ppEquation;
20.20
20.21 fun equationLiteral (t_u,th) =
20.22 let
20.23 @@ -210,7 +211,7 @@
20.24
20.25 fun rewrConv (eqn as ((x,y), eqTh)) path tm =
20.26 if Term.equal x y then allConv tm
20.27 - else if null path then (y,eqTh)
20.28 + else if List.null path then (y,eqTh)
20.29 else
20.30 let
20.31 val reflTh = Thm.refl tm
20.32 @@ -249,7 +250,7 @@
20.33
20.34 fun subtermsConv _ (tm as Term.Var _) = allConv tm
20.35 | subtermsConv conv (tm as Term.Fn (_,a)) =
20.36 - everyConv (map (subtermConv conv) (interval 0 (length a))) tm;
20.37 + everyConv (List.map (subtermConv conv) (interval 0 (length a))) tm;
20.38
20.39 (* ------------------------------------------------------------------------- *)
20.40 (* Applying a conversion to every subterm, with some traversal strategy. *)
20.41 @@ -363,7 +364,7 @@
20.42
20.43 fun allArgumentsLiterule conv lit =
20.44 everyLiterule
20.45 - (map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit;
20.46 + (List.map (argumentLiterule conv) (interval 0 (Literal.arity lit))) lit;
20.47
20.48 (* ------------------------------------------------------------------------- *)
20.49 (* A rule takes one theorem and either deduces another or raises an Error *)
20.50 @@ -779,7 +780,7 @@
20.51 let
20.52 fun fact sub = removeSym (Thm.subst sub th)
20.53 in
20.54 - map fact (factor' (Thm.clause th))
20.55 + List.map fact (factor' (Thm.clause th))
20.56 end;
20.57
20.58 end
21.1 --- a/src/Tools/Metis/src/Term.sml Thu Mar 24 17:49:27 2011 +0100
21.2 +++ b/src/Tools/Metis/src/Term.sml Thu Mar 24 17:49:27 2011 +0100
21.3 @@ -164,7 +164,7 @@
21.4 in
21.5 case tm of
21.6 Var _ => subtms rest acc
21.7 - | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
21.8 + | Fn (_,args) => subtms (List.map f (enumerate args) @ rest) acc
21.9 end;
21.10 in
21.11 fun subterms tm = subtms [([],tm)] [];
21.12 @@ -195,7 +195,7 @@
21.13 Var _ => search rest
21.14 | Fn (_,a) =>
21.15 let
21.16 - val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
21.17 + val subtms = List.map (fn (i,t) => (i :: path, t)) (enumerate a)
21.18 in
21.19 search (subtms @ rest)
21.20 end
21.21 @@ -235,14 +235,14 @@
21.22
21.23 fun newVar () = Var (Name.newName ());
21.24
21.25 -fun newVars n = map Var (Name.newNames n);
21.26 +fun newVars n = List.map Var (Name.newNames n);
21.27
21.28 local
21.29 - fun avoidAcceptable avoid n = not (NameSet.member n avoid);
21.30 + fun avoid av n = NameSet.member n av;
21.31 in
21.32 - fun variantPrime avoid = Name.variantPrime (avoidAcceptable avoid);
21.33 + fun variantPrime av = Name.variantPrime {avoid = avoid av};
21.34
21.35 - fun variantNum avoid = Name.variantNum (avoidAcceptable avoid);
21.36 + fun variantNum av = Name.variantNum {avoid = avoid av};
21.37 end;
21.38
21.39 (* ------------------------------------------------------------------------- *)
21.40 @@ -314,7 +314,7 @@
21.41
21.42 val acc = (rev path, tm) :: acc
21.43
21.44 - val rest = map f (enumerate args) @ rest
21.45 + val rest = List.map f (enumerate args) @ rest
21.46 in
21.47 subtms rest acc
21.48 end;
21.49 @@ -523,7 +523,7 @@
21.50 and basic bv (Var v) = varName bv v
21.51 | basic bv (Fn (f,args)) =
21.52 Print.blockProgram Print.Inconsistent 2
21.53 - (functionName bv f :: map (functionArgument bv) args)
21.54 + (functionName bv f :: List.map (functionArgument bv) args)
21.55
21.56 and customBracket bv tm =
21.57 case destBrack tm of
21.58 @@ -535,13 +535,13 @@
21.59 NONE => term bv tm
21.60 | SOME (q,v,vs,tm) =>
21.61 let
21.62 - val bv = StringSet.addList bv (map Name.toString (v :: vs))
21.63 + val bv = StringSet.addList bv (List.map Name.toString (v :: vs))
21.64 in
21.65 Print.program
21.66 [Print.ppString q,
21.67 varName bv v,
21.68 Print.program
21.69 - (map (Print.sequence (Print.addBreak 1) o varName bv) vs),
21.70 + (List.map (Print.sequence (Print.addBreak 1) o varName bv) vs),
21.71 Print.ppString ".",
21.72 Print.addBreak 1,
21.73 innerQuant bv tm]
21.74 @@ -628,9 +628,9 @@
21.75 and neg = !negation
21.76 and bracks = ("(",")") :: !brackets
21.77
21.78 - val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
21.79 + val bracks = List.map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
21.80
21.81 - val bTokens = map #2 bracks @ map #3 bracks
21.82 + val bTokens = List.map #2 bracks @ List.map #3 bracks
21.83
21.84 fun possibleVarName "" = false
21.85 | possibleVarName s = isAlphaNum (String.sub (s,0))
21.86 @@ -685,8 +685,8 @@
21.87 in
21.88 var ||
21.89 const ||
21.90 - first (map bracket bracks) ||
21.91 - first (map quantifier quants)
21.92 + first (List.map bracket bracks) ||
21.93 + first (List.map quantifier quants)
21.94 end tokens
21.95
21.96 and molecule bv tokens =
22.1 --- a/src/Tools/Metis/src/TermNet.sml Thu Mar 24 17:49:27 2011 +0100
22.2 +++ b/src/Tools/Metis/src/TermNet.sml Thu Mar 24 17:49:27 2011 +0100
22.3 @@ -50,7 +50,7 @@
22.4 fun equalFnQterm f1 f2 = compareFnQterm (f1,f2) = EQUAL;
22.5
22.6 fun termToQterm (Term.Var _) = Var
22.7 - | termToQterm (Term.Fn (f,l)) = Fn ((f, length l), map termToQterm l);
22.8 + | termToQterm (Term.Fn (f,l)) = Fn ((f, length l), List.map termToQterm l);
22.9
22.10 local
22.11 fun qm [] = true
22.12 @@ -116,7 +116,7 @@
22.13
22.14 local
22.15 fun qtermToTerm Var = anonymousVar
22.16 - | qtermToTerm (Fn ((f,_),l)) = Term.Fn (f, map qtermToTerm l);
22.17 + | qtermToTerm (Fn ((f,_),l)) = Term.Fn (f, List.map qtermToTerm l);
22.18 in
22.19 val ppQterm = Print.ppMap qtermToTerm Term.pp;
22.20 end;
22.21 @@ -339,7 +339,7 @@
22.22
22.23 fun fifoize ({fifo, ...} : parameters) l = if fifo then sort idwise l else l;
22.24 in
22.25 - fun finally parm l = map snd (fifoize parm l);
22.26 + fun finally parm l = List.map snd (fifoize parm l);
22.27 end;
22.28
22.29 local
23.1 --- a/src/Tools/Metis/src/Thm.sml Thu Mar 24 17:49:27 2011 +0100
23.2 +++ b/src/Tools/Metis/src/Thm.sml Thu Mar 24 17:49:27 2011 +0100
23.3 @@ -107,7 +107,7 @@
23.4 local
23.5 fun toFormula th =
23.6 Formula.listMkDisj
23.7 - (map Literal.toFormula (LiteralSet.toList (clause th)));
23.8 + (List.map Literal.toFormula (LiteralSet.toList (clause th)));
23.9 in
23.10 fun pp th =
23.11 Print.blockProgram Print.Inconsistent 3
24.1 --- a/src/Tools/Metis/src/Tptp.sml Thu Mar 24 17:49:27 2011 +0100
24.2 +++ b/src/Tools/Metis/src/Tptp.sml Thu Mar 24 17:49:27 2011 +0100
24.3 @@ -430,8 +430,8 @@
24.4 fun lift {name,arity,tptp} =
24.5 {name = Name.fromString name, arity = arity, tptp = tptp}
24.6
24.7 - val functionMapping = map lift defaultFunctionMapping
24.8 - and relationMapping = map lift defaultRelationMapping
24.9 + val functionMapping = List.map lift defaultFunctionMapping
24.10 + and relationMapping = List.map lift defaultRelationMapping
24.11
24.12 val mapping =
24.13 {functionMapping = functionMapping,
24.14 @@ -448,7 +448,7 @@
24.15 let
24.16 fun mkEntry {name,arity,model} = ((Name.fromString name, arity), model)
24.17
24.18 - fun mkMap l = NameArityMap.fromList (map mkEntry l)
24.19 + fun mkMap l = NameArityMap.fromList (List.map mkEntry l)
24.20 in
24.21 {functionMap = mkMap funcModel,
24.22 relationMap = mkMap relModel}
24.23 @@ -766,8 +766,12 @@
24.24 val lexToken = alphaNumToken || punctToken || quoteToken;
24.25
24.26 val space = many (some Char.isSpace) >> K ();
24.27 +
24.28 + val space1 = atLeastOne (some Char.isSpace) >> K ();
24.29 in
24.30 - val lexer = (space ++ lexToken ++ space) >> (fn ((),(tok,())) => tok);
24.31 + val lexer =
24.32 + (space ++ lexToken) >> (fn ((),tok) => [tok]) ||
24.33 + space1 >> K [];
24.34 end;
24.35
24.36 (* ------------------------------------------------------------------------- *)
24.37 @@ -800,11 +804,11 @@
24.38 List.foldl fvs NameSet.empty
24.39 end;
24.40
24.41 -fun clauseSubst sub lits = map (literalSubst sub) lits;
24.42 -
24.43 -fun clauseToFormula lits = Formula.listMkDisj (map literalToFormula lits);
24.44 -
24.45 -fun clauseFromFormula fm = map literalFromFormula (Formula.stripDisj fm);
24.46 +fun clauseSubst sub lits = List.map (literalSubst sub) lits;
24.47 +
24.48 +fun clauseToFormula lits = Formula.listMkDisj (List.map literalToFormula lits);
24.49 +
24.50 +fun clauseFromFormula fm = List.map literalFromFormula (Formula.stripDisj fm);
24.51
24.52 fun clauseFromLiteralSet cl =
24.53 clauseFromFormula
24.54 @@ -1105,7 +1109,7 @@
24.55 end
24.56 | ProofFormulaSource {inference,parents} =>
24.57 let
24.58 - val isTaut = null parents
24.59 + val isTaut = List.null parents
24.60
24.61 val gen = if isTaut then GEN_INTRODUCED else GEN_INFERENCE
24.62
24.63 @@ -1118,7 +1122,7 @@
24.64 Proof.Subst (s,_) => s
24.65 | _ => Subst.empty
24.66 in
24.67 - map (fn parent => (parent,sub)) parents
24.68 + List.map (fn parent => (parent,sub)) parents
24.69 end
24.70 in
24.71 Print.blockProgram Print.Inconsistent (size gen + 1)
24.72 @@ -1300,7 +1304,7 @@
24.73 | f [x] = x
24.74 | f (h :: t) = (h ++ f t) >> K ();
24.75 in
24.76 - fun symbolParser s = f (map punctParser (String.explode s));
24.77 + fun symbolParser s = f (List.map punctParser (String.explode s));
24.78 end;
24.79
24.80 val definedParser =
24.81 @@ -1568,7 +1572,7 @@
24.82
24.83 and quantifiedFormulaParser mapping input =
24.84 let
24.85 - fun mk (q,(vs,((),f))) = q (map (mkVarName mapping) vs, f)
24.86 + fun mk (q,(vs,((),f))) = q (List.map (mkVarName mapping) vs, f)
24.87 in
24.88 (quantifierParser ++ varListParser ++ punctParser #":" ++
24.89 unitaryFormulaParser mapping) >> mk
24.90 @@ -1699,7 +1703,7 @@
24.91
24.92 fun parseChars parser chars =
24.93 let
24.94 - val tokens = Parse.everything (lexer >> singleton) chars
24.95 + val tokens = Parse.everything lexer chars
24.96 in
24.97 Parse.everything (parser >> singleton) tokens
24.98 end;
24.99 @@ -1904,7 +1908,7 @@
24.100 val {problem,sources} : normalization = acc
24.101 val {axioms,conjecture} = problem
24.102
24.103 - val cls = map fst clauses
24.104 + val cls = List.map fst clauses
24.105 val (axioms,conjecture) =
24.106 if isCnfConjectureRole role then (axioms, cls @ conjecture)
24.107 else (cls @ axioms, conjecture)
24.108 @@ -1939,7 +1943,7 @@
24.109 fun sourcify (cl,inf) = (cl, FofClauseSource inf)
24.110
24.111 val (clauses,cnf) = Normalize.addCnf th cnf
24.112 - val clauses = map sourcify clauses
24.113 + val clauses = List.map sourcify clauses
24.114 val norm = addClauses role clauses norm
24.115 in
24.116 (norm,cnf)
24.117 @@ -1978,26 +1982,26 @@
24.118 let
24.119 val subgoals = Formula.splitGoal goal
24.120 val subgoals =
24.121 - if null subgoals then [Formula.True] else subgoals
24.122 + if List.null subgoals then [Formula.True] else subgoals
24.123
24.124 val parents = [name]
24.125 in
24.126 - map (mk parents) subgoals
24.127 + List.map (mk parents) subgoals
24.128 end
24.129 in
24.130 - fn goals => List.concat (map split goals)
24.131 + fn goals => List.concat (List.map split goals)
24.132 end;
24.133
24.134 fun clausesToGoal cls =
24.135 let
24.136 - val cls = map (Formula.generalize o clauseToFormula o snd) cls
24.137 + val cls = List.map (Formula.generalize o clauseToFormula o snd) cls
24.138 in
24.139 Formula.listMkConj cls
24.140 end;
24.141
24.142 fun formulasToGoal fms =
24.143 let
24.144 - val fms = map (Formula.generalize o snd) fms
24.145 + val fms = List.map (Formula.generalize o snd) fms
24.146 in
24.147 Formula.listMkConj fms
24.148 end;
24.149 @@ -2013,11 +2017,11 @@
24.150 | FofGoal goals => formulasToGoal goals
24.151
24.152 val fm =
24.153 - if null fofAxioms then fm
24.154 + if List.null fofAxioms then fm
24.155 else Formula.Imp (formulasToGoal fofAxioms, fm)
24.156
24.157 val fm =
24.158 - if null cnfAxioms then fm
24.159 + if List.null cnfAxioms then fm
24.160 else Formula.Imp (clausesToGoal cnfAxioms, fm)
24.161 in
24.162 fm
24.163 @@ -2137,8 +2141,8 @@
24.164 let
24.165 val Problem {comments,includes,formulas} = problem
24.166
24.167 - val includesTop = null comments
24.168 - val formulasTop = includesTop andalso null includes
24.169 + val includesTop = List.null comments
24.170 + val formulasTop = includesTop andalso List.null includes
24.171 in
24.172 Stream.toTextFile
24.173 {filename = filename}
24.174 @@ -2153,8 +2157,8 @@
24.175 local
24.176 fun refute {axioms,conjecture} =
24.177 let
24.178 - val axioms = map Thm.axiom axioms
24.179 - and conjecture = map Thm.axiom conjecture
24.180 + val axioms = List.map Thm.axiom axioms
24.181 + and conjecture = List.map Thm.axiom conjecture
24.182 val problem = {axioms = axioms, conjecture = conjecture}
24.183 val resolution = Resolution.new Resolution.default problem
24.184 in
24.185 @@ -2166,7 +2170,7 @@
24.186 fun prove filename =
24.187 let
24.188 val problem = read filename
24.189 - val problems = map #problem (normalize problem)
24.190 + val problems = List.map #problem (normalize problem)
24.191 in
24.192 List.all refute problems
24.193 end;
24.194 @@ -2334,7 +2338,7 @@
24.195 val number = i - 1
24.196
24.197 val (subgoal,formulas) =
24.198 - if null pars then (NONE,formulas)
24.199 + if List.null pars then (NONE,formulas)
24.200 else
24.201 let
24.202 val role = PlainRole
24.203 @@ -2374,7 +2378,7 @@
24.204 | Normalize.Definition (_,fm) => fm :: fms
24.205 | _ => fms
24.206
24.207 - val parents = map (lookupFormulaName fmNames) fms
24.208 + val parents = List.map (lookupFormulaName fmNames) fms
24.209 in
24.210 NormalizeFormulaSource
24.211 {inference = inference,
24.212 @@ -2388,9 +2392,9 @@
24.213 Proof.Axiom cl => [lookupClauseSourceName sources fmNames cl]
24.214 | _ =>
24.215 let
24.216 - val cls = map Thm.clause (Proof.parents inference)
24.217 + val cls = List.map Thm.clause (Proof.parents inference)
24.218 in
24.219 - map (lookupClauseName clNames) cls
24.220 + List.map (lookupClauseName clNames) cls
24.221 end
24.222 in
24.223 ProofFormulaSource
25.1 --- a/src/Tools/Metis/src/Useful.sml Thu Mar 24 17:49:27 2011 +0100
25.2 +++ b/src/Tools/Metis/src/Useful.sml Thu Mar 24 17:49:27 2011 +0100
25.3 @@ -50,7 +50,20 @@
25.4 (* Tracing. *)
25.5 (* ------------------------------------------------------------------------- *)
25.6
25.7 -val tracePrint = ref TextIO.print;
25.8 +local
25.9 + val traceOut = TextIO.stdOut;
25.10 +
25.11 + fun tracePrintFn mesg =
25.12 + let
25.13 + val () = TextIO.output (traceOut,mesg)
25.14 +
25.15 + val () = TextIO.flushOut traceOut
25.16 + in
25.17 + ()
25.18 + end;
25.19 +in
25.20 + val tracePrint = ref tracePrintFn;
25.21 +end;
25.22
25.23 fun trace mesg = !tracePrint mesg;
25.24
25.25 @@ -254,7 +267,7 @@
25.26 case l of
25.27 [] =>
25.28 let
25.29 - val acc = if null row then acc else rev row :: acc
25.30 + val acc = if List.null row then acc else rev row :: acc
25.31 in
25.32 rev acc
25.33 end
25.34 @@ -283,9 +296,9 @@
25.35 local
25.36 fun fstEq ((x,_),(y,_)) = x = y;
25.37
25.38 - fun collapse l = (fst (hd l), map snd l);
25.39 + fun collapse l = (fst (hd l), List.map snd l);
25.40 in
25.41 - fun groupsByFst l = map collapse (groupsBy fstEq l);
25.42 + fun groupsByFst l = List.map collapse (groupsBy fstEq l);
25.43 end;
25.44
25.45 fun groupsOf n =
25.46 @@ -430,10 +443,10 @@
25.47 | sortMap f cmp xs =
25.48 let
25.49 fun ncmp ((m,_),(n,_)) = cmp (m,n)
25.50 - val nxs = map (fn x => (f x, x)) xs
25.51 + val nxs = List.map (fn x => (f x, x)) xs
25.52 val nys = sort ncmp nxs
25.53 in
25.54 - map snd nys
25.55 + List.map snd nys
25.56 end;
25.57
25.58 (* ------------------------------------------------------------------------- *)
25.59 @@ -641,7 +654,7 @@
25.60
25.61 fun alignColumn {leftAlign,padChar} column =
25.62 let
25.63 - val (n,_) = maximum Int.compare (map size column)
25.64 + val (n,_) = maximum Int.compare (List.map size column)
25.65
25.66 fun pad entry row =
25.67 let
25.68 @@ -657,13 +670,18 @@
25.69 local
25.70 fun alignTab aligns rows =
25.71 case aligns of
25.72 - [] => map (K "") rows
25.73 - | [{leftAlign = true, padChar = #" "}] => map hd rows
25.74 + [] => List.map (K "") rows
25.75 + | [{leftAlign = true, padChar = #" "}] => List.map hd rows
25.76 | align :: aligns =>
25.77 - alignColumn align (map hd rows) (alignTab aligns (map tl rows));
25.78 + let
25.79 + val col = List.map hd rows
25.80 + and cols = alignTab aligns (List.map tl rows)
25.81 + in
25.82 + alignColumn align col cols
25.83 + end;
25.84 in
25.85 fun alignTable aligns rows =
25.86 - if null rows then [] else alignTab aligns rows;
25.87 + if List.null rows then [] else alignTab aligns rows;
25.88 end;
25.89
25.90 (* ------------------------------------------------------------------------- *)
26.1 --- a/src/Tools/Metis/src/Waiting.sml Thu Mar 24 17:49:27 2011 +0100
26.2 +++ b/src/Tools/Metis/src/Waiting.sml Thu Mar 24 17:49:27 2011 +0100
26.3 @@ -63,7 +63,7 @@
26.4 val pp =
26.5 Print.ppMap
26.6 (fn Waiting {clauses,...} =>
26.7 - map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses))
26.8 + List.map (fn (w,(_,cl)) => (w, Clause.id cl, cl)) (Heap.toList clauses))
26.9 (Print.ppList (Print.ppTriple Print.ppReal Print.ppInt Clause.pp));
26.10 *)
26.11
26.12 @@ -81,10 +81,10 @@
26.13 (fvs,lits)
26.14 end;
26.15
26.16 -val mkModelClauses = map mkModelClause;
26.17 +val mkModelClauses = List.map mkModelClause;
26.18
26.19 fun perturbModel M cls =
26.20 - if null cls then K ()
26.21 + if List.null cls then K ()
26.22 else
26.23 let
26.24 val N = {size = Model.size M}
26.25 @@ -195,6 +195,14 @@
26.26 val Waiting {parameters,clauses,models} = waiting
26.27 val {models = modelParameters, ...} = parameters
26.28
26.29 +(*MetisDebug
26.30 + val _ = not (List.null cls) orelse
26.31 + raise Bug "Waiting.add': null"
26.32 +
26.33 + val _ = length mcls = length cls orelse
26.34 + raise Bug "Waiting.add': different lengths"
26.35 +*)
26.36 +
26.37 val dist = dist + Math.ln (Real.fromInt (length cls))
26.38
26.39 fun addCl ((mcl,cl),acc) =
26.40 @@ -211,22 +219,23 @@
26.41 Waiting {parameters = parameters, clauses = clauses, models = models}
26.42 end;
26.43
26.44 -fun add waiting (_,[]) = waiting
26.45 - | add waiting (dist,cls) =
26.46 - let
26.47 +fun add waiting (dist,cls) =
26.48 + if List.null cls then waiting
26.49 + else
26.50 + let
26.51 (*MetisTrace3
26.52 - val () = Print.trace pp "Waiting.add: waiting" waiting
26.53 - val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls
26.54 + val () = Print.trace pp "Waiting.add: waiting" waiting
26.55 + val () = Print.trace (Print.ppList Clause.pp) "Waiting.add: cls" cls
26.56 *)
26.57
26.58 - val waiting = add' waiting dist (mkModelClauses cls) cls
26.59 + val waiting = add' waiting dist (mkModelClauses cls) cls
26.60
26.61 (*MetisTrace3
26.62 - val () = Print.trace pp "Waiting.add: waiting" waiting
26.63 + val () = Print.trace pp "Waiting.add: waiting" waiting
26.64 *)
26.65 - in
26.66 - waiting
26.67 - end;
26.68 + in
26.69 + waiting
26.70 + end;
26.71
26.72 local
26.73 fun cmp ((w1,_),(w2,_)) = Real.compare (w1,w2);
26.74 @@ -235,7 +244,7 @@
26.75 let
26.76 val {models = modelParameters, ...} = parameters
26.77 val clauses = Heap.new cmp
26.78 - and models = map (initialModel axioms conjecture) modelParameters
26.79 + and models = List.map (initialModel axioms conjecture) modelParameters
26.80 in
26.81 Waiting {parameters = parameters, clauses = clauses, models = models}
26.82 end;
26.83 @@ -247,8 +256,17 @@
26.84
26.85 val waiting = empty parameters mAxioms mConjecture
26.86 in
26.87 - add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
26.88 - end;
26.89 + if List.null axioms andalso List.null conjecture then waiting
26.90 + else add' waiting 0.0 (mAxioms @ mConjecture) (axioms @ conjecture)
26.91 + end
26.92 +(*MetisDebug
26.93 + handle e =>
26.94 + let
26.95 + val () = Print.trace Print.ppException "Waiting.new: exception" e
26.96 + in
26.97 + raise e
26.98 + end;
26.99 +*)
26.100 end;
26.101
26.102 (* ------------------------------------------------------------------------- *)
26.103 @@ -260,9 +278,12 @@
26.104 else
26.105 let
26.106 val ((_,dcl),clauses) = Heap.remove clauses
26.107 +
26.108 val waiting =
26.109 Waiting
26.110 - {parameters = parameters, clauses = clauses, models = models}
26.111 + {parameters = parameters,
26.112 + clauses = clauses,
26.113 + models = models}
26.114 in
26.115 SOME (dcl,waiting)
26.116 end;
27.1 --- a/src/Tools/Metis/src/metis.sml Thu Mar 24 17:49:27 2011 +0100
27.2 +++ b/src/Tools/Metis/src/metis.sml Thu Mar 24 17:49:27 2011 +0100
27.3 @@ -13,23 +13,25 @@
27.4
27.5 val VERSION = "2.3";
27.6
27.7 -val versionString = PROGRAM^" "^VERSION^" (release 20100916)"^"\n";
27.8 +val versionString = PROGRAM^" "^VERSION^" (release 20101229)"^"\n";
27.9
27.10 (* ------------------------------------------------------------------------- *)
27.11 (* Program options. *)
27.12 (* ------------------------------------------------------------------------- *)
27.13
27.14 +val ITEMS = ["name","goal","clauses","size","category","proof","saturation"];
27.15 +
27.16 +val TIMEOUT : int option ref = ref NONE;
27.17 +
27.18 +val TPTP : string option ref = ref NONE;
27.19 +
27.20 val QUIET = ref false;
27.21
27.22 val TEST = ref false;
27.23
27.24 -val TPTP : string option ref = ref NONE;
27.25 -
27.26 -val ITEMS = ["name","goal","clauses","size","category","proof","saturation"];
27.27 -
27.28 val extended_items = "all" :: ITEMS;
27.29
27.30 -val show_items = map (fn s => (s, ref false)) ITEMS;
27.31 +val show_items = List.map (fn s => (s, ref false)) ITEMS;
27.32
27.33 fun show_ref s =
27.34 case List.find (equal s o fst) show_items of
27.35 @@ -68,6 +70,11 @@
27.36 description = "hide ITEM (see below for list)",
27.37 processor =
27.38 beginOpt (enumOpt extended_items endOpt) (fn _ => fn s => hide s)},
27.39 + {switches = ["--time-limit"], arguments = ["N"],
27.40 + description = "give up after N seconds",
27.41 + processor =
27.42 + beginOpt (optionOpt ("-", intOpt (SOME 0, NONE)) endOpt)
27.43 + (fn _ => fn n => TIMEOUT := n)},
27.44 {switches = ["--tptp"], arguments = ["DIR"],
27.45 description = "specify the TPTP installation directory",
27.46 processor =
27.47 @@ -113,6 +120,25 @@
27.48 (* The core application. *)
27.49 (* ------------------------------------------------------------------------- *)
27.50
27.51 +fun newLimit () =
27.52 + case !TIMEOUT of
27.53 + NONE => K true
27.54 + | SOME lim =>
27.55 + let
27.56 + val timer = Timer.startRealTimer ()
27.57 +
27.58 + val lim = Time.fromReal (Real.fromInt lim)
27.59 +
27.60 + fun check () =
27.61 + let
27.62 + val time = Timer.checkRealTimer timer
27.63 + in
27.64 + Time.<= (time,lim)
27.65 + end
27.66 + in
27.67 + check
27.68 + end;
27.69 +
27.70 (*MetisDebug
27.71 val next_cnf =
27.72 let
27.73 @@ -237,7 +263,7 @@
27.74 names = Tptp.noClauseNames,
27.75 roles = Tptp.noClauseRoles,
27.76 problem = {axioms = [],
27.77 - conjecture = map Thm.clause ths}}
27.78 + conjecture = List.map Thm.clause ths}}
27.79
27.80 val mapping =
27.81 Tptp.addVarSetMapping Tptp.defaultMapping
27.82 @@ -294,21 +320,25 @@
27.83 end
27.84 *)
27.85 val () = display_clauses cls
27.86 +
27.87 val () = display_size cls
27.88 +
27.89 val () = display_category cls
27.90 in
27.91 ()
27.92 end;
27.93
27.94 fun mkTptpFilename filename =
27.95 - case !TPTP of
27.96 - NONE => filename
27.97 - | SOME tptp =>
27.98 - let
27.99 - val tptp = stripSuffix (equal #"/") tptp
27.100 - in
27.101 - tptp ^ "/" ^ filename
27.102 - end;
27.103 + if isPrefix "/" filename then filename
27.104 + else
27.105 + case !TPTP of
27.106 + NONE => filename
27.107 + | SOME tptp =>
27.108 + let
27.109 + val tptp = stripSuffix (equal #"/") tptp
27.110 + in
27.111 + tptp ^ "/" ^ filename
27.112 + end;
27.113
27.114 fun readIncludes mapping seen formulas includes =
27.115 case includes of
27.116 @@ -338,7 +368,7 @@
27.117
27.118 val Tptp.Problem {comments,includes,formulas} = problem
27.119 in
27.120 - if null includes then problem
27.121 + if List.null includes then problem
27.122 else
27.123 let
27.124 val seen = StringSet.empty
27.125 @@ -356,8 +386,7 @@
27.126
27.127 val resolutionParameters =
27.128 let
27.129 - val {active,
27.130 - waiting} = Resolution.default
27.131 + val {active,waiting} = Resolution.default
27.132
27.133 val waiting =
27.134 let
27.135 @@ -394,17 +423,25 @@
27.136 waiting = waiting}
27.137 end;
27.138
27.139 - fun refute {axioms,conjecture} =
27.140 + fun resolutionLoop limit res =
27.141 + case Resolution.iterate res of
27.142 + Resolution.Decided dec => SOME dec
27.143 + | Resolution.Undecided res =>
27.144 + if limit () then resolutionLoop limit res else NONE;
27.145 +
27.146 + fun refute limit {axioms,conjecture} =
27.147 let
27.148 - val axioms = map Thm.axiom axioms
27.149 - and conjecture = map Thm.axiom conjecture
27.150 + val axioms = List.map Thm.axiom axioms
27.151 + and conjecture = List.map Thm.axiom conjecture
27.152 +
27.153 val problem = {axioms = axioms, conjecture = conjecture}
27.154 - val resolution = Resolution.new resolutionParameters problem
27.155 +
27.156 + val res = Resolution.new resolutionParameters problem
27.157 in
27.158 - Resolution.loop resolution
27.159 + resolutionLoop limit res
27.160 end;
27.161
27.162 - fun refuteAll filename tptp probs acc =
27.163 + fun refuteAll limit filename tptp probs acc =
27.164 case probs of
27.165 [] =>
27.166 let
27.167 @@ -427,10 +464,10 @@
27.168
27.169 val () = display_problem filename problem
27.170 in
27.171 - if !TEST then refuteAll filename tptp probs acc
27.172 + if !TEST then refuteAll limit filename tptp probs acc
27.173 else
27.174 - case refute problem of
27.175 - Resolution.Contradiction th =>
27.176 + case refute limit problem of
27.177 + SOME (Resolution.Contradiction th) =>
27.178 let
27.179 val subgoalProof =
27.180 {subgoal = subgoal,
27.181 @@ -439,9 +476,9 @@
27.182
27.183 val acc = subgoalProof :: acc
27.184 in
27.185 - refuteAll filename tptp probs acc
27.186 + refuteAll limit filename tptp probs acc
27.187 end
27.188 - | Resolution.Satisfiable ths =>
27.189 + | SOME (Resolution.Satisfiable ths) =>
27.190 let
27.191 val status =
27.192 if Tptp.hasFofConjecture tptp then
27.193 @@ -450,29 +487,42 @@
27.194 Tptp.SatisfiableStatus
27.195
27.196 val () = display_status filename status
27.197 +
27.198 val () = display_saturation filename ths
27.199 in
27.200 false
27.201 end
27.202 + | NONE =>
27.203 + let
27.204 + val status = Tptp.UnknownStatus
27.205 +
27.206 + val () = display_status filename status
27.207 + in
27.208 + false
27.209 + end
27.210 end;
27.211 in
27.212 - fun prove mapping filename =
27.213 + fun prove limit mapping filename =
27.214 let
27.215 val () = display_sep ()
27.216 +
27.217 val () = display_name filename
27.218 +
27.219 val tptp = read mapping filename
27.220 +
27.221 val () = display_goal tptp
27.222 +
27.223 val problems = Tptp.normalize tptp
27.224 in
27.225 - refuteAll filename tptp problems []
27.226 + refuteAll limit filename tptp problems []
27.227 end;
27.228 +end;
27.229
27.230 - fun proveAll mapping filenames =
27.231 - List.all
27.232 - (if !QUIET then prove mapping
27.233 - else fn filename => prove mapping filename orelse true)
27.234 - filenames;
27.235 -end;
27.236 +fun proveAll limit mapping filenames =
27.237 + List.all
27.238 + (if !QUIET then prove limit mapping
27.239 + else fn filename => prove limit mapping filename orelse true)
27.240 + filenames;
27.241
27.242 (* ------------------------------------------------------------------------- *)
27.243 (* Top level. *)
27.244 @@ -482,11 +532,13 @@
27.245 let
27.246 val work = processOptions ()
27.247
27.248 - val () = if null work then usage "no input problem files" else ()
27.249 + val () = if List.null work then usage "no input problem files" else ()
27.250 +
27.251 + val limit = newLimit ()
27.252
27.253 val mapping = Tptp.defaultMapping
27.254
27.255 - val success = proveAll mapping work
27.256 + val success = proveAll limit mapping work
27.257 in
27.258 exit {message = NONE, usage = false, success = success}
27.259 end
28.1 --- a/src/Tools/Metis/src/problems.sml Thu Mar 24 17:49:27 2011 +0100
28.2 +++ b/src/Tools/Metis/src/problems.sml Thu Mar 24 17:49:27 2011 +0100
28.3 @@ -22,7 +22,7 @@
28.4 fun mkProblem collection description (problem : problem) : problem =
28.5 let
28.6 val {name,comments,goal} = problem
28.7 - val comments = if null comments then [] else "" :: comments
28.8 + val comments = if List.null comments then [] else "" :: comments
28.9 val comments = "Description: " ^ description :: comments
28.10 val comments = mkCollection collection :: comments
28.11 in
28.12 @@ -33,7 +33,7 @@
28.13 Useful.mem (mkCollection collection) comments;
28.14
28.15 fun mkProblems collection description problems =
28.16 - map (mkProblem collection description) problems;
28.17 + List.map (mkProblem collection description) problems;
28.18 end;
28.19
28.20 (* ========================================================================= *)
29.1 --- a/src/Tools/Metis/src/problems2tptp.sml Thu Mar 24 17:49:27 2011 +0100
29.2 +++ b/src/Tools/Metis/src/problems2tptp.sml Thu Mar 24 17:49:27 2011 +0100
29.3 @@ -34,7 +34,7 @@
29.4 if x <> x' then dups xs
29.5 else raise Error ("duplicate problem name: " ^ x)
29.6
29.7 - val names = sort String.compare (map #name problems)
29.8 + val names = sort String.compare (List.map #name problems)
29.9 in
29.10 dups names
29.11 end;
29.12 @@ -56,8 +56,8 @@
29.13 val comments =
29.14 [comment_bar] @
29.15 ["Name: " ^ name] @
29.16 - (if null comments then [] else "" :: comments) @
29.17 - (if null comment_footer then [] else "" :: comment_footer) @
29.18 + (if List.null comments then [] else "" :: comments) @
29.19 + (if List.null comment_footer then [] else "" :: comment_footer) @
29.20 [comment_bar]
29.21
29.22 val includes = []
29.23 @@ -145,7 +145,7 @@
29.24 val (opts,work) =
29.25 Options.processOptions programOptions (CommandLine.arguments ());
29.26
29.27 -val () = if null work then () else usage "too many arguments";
29.28 +val () = if List.null work then () else usage "too many arguments";
29.29
29.30 (* ------------------------------------------------------------------------- *)
29.31 (* Top level. *)
30.1 --- a/src/Tools/Metis/src/selftest.sml Thu Mar 24 17:49:27 2011 +0100
30.2 +++ b/src/Tools/Metis/src/selftest.sml Thu Mar 24 17:49:27 2011 +0100
30.3 @@ -84,7 +84,7 @@
30.4 and L = Literal.parse
30.5 and F = Formula.parse
30.6 and S = Subst.fromList;
30.7 -val LS = LiteralSet.fromList o map L;
30.8 +val LS = LiteralSet.fromList o List.map L;
30.9 val AX = Thm.axiom o LS;
30.10 val CL = mkCl Clause.default o AX;
30.11 val Q = (fn th => (Thm.destUnitEq th, th)) o AX o singleton
30.12 @@ -116,7 +116,7 @@
30.13 val () = SAY "The parser and pretty-printer";
30.14 (* ------------------------------------------------------------------------- *)
30.15
30.16 -fun prep l = (chop_newline o String.concat o map unquote) l;
30.17 +fun prep l = (chop_newline o String.concat o List.map unquote) l;
30.18
30.19 fun mini_print n fm = withRef (Print.lineLength,n) Formula.toString fm;
30.20
30.21 @@ -509,7 +509,7 @@
30.22 fun clauseToFormula cl =
30.23 Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl);
30.24 in
30.25 - fun clausesToFormula cls = Formula.listMkConj (map clauseToFormula cls);
30.26 + fun clausesToFormula cls = Formula.listMkConj (List.map clauseToFormula cls);
30.27 end;
30.28
30.29 val cnf' = pvFm o clausesToFormula o Normalize.cnf o F;
30.30 @@ -565,7 +565,7 @@
30.31 in
30.32 fun checkModel M cls =
30.33 let
30.34 - val table = map (checkModelClause M) cls
30.35 + val table = List.map (checkModelClause M) cls
30.36
30.37 val rows = alignTable format table
30.38
30.39 @@ -587,7 +587,7 @@
30.40 else Model.perturbClause M V cl
30.41 end
30.42
30.43 - val cls = map (fn cl => (LiteralSet.freeVars cl, cl)) cls
30.44 + val cls = List.map (fn cl => (LiteralSet.freeVars cl, cl)) cls
30.45
30.46 fun perturbClauses () = app perturbClause cls
30.47
30.48 @@ -1085,7 +1085,7 @@
30.49
30.50 val quot_clauses =
30.51 Formula.listMkConj o sort Formula.compare o
30.52 - map (quot o snd o Formula.stripForall) o Formula.stripConj;
30.53 + List.map (quot o snd o Formula.stripForall) o Formula.stripConj;
30.54
30.55 fun quotient (Formula.Imp (a, Formula.Imp (b, Formula.False))) =
30.56 Formula.Imp (quot_clauses a, Formula.Imp (quot_clauses b, Formula.False))
30.57 @@ -1142,6 +1142,8 @@
30.58 end;
30.59
30.60 val _ = tptp "PUZ001-1";
30.61 +val _ = tptp "NO_FORMULAS";
30.62 +val _ = tptp "SEPARATED_COMMENTS";
30.63 val _ = tptp "NUMBERED_FORMULAS";
30.64 val _ = tptp "DEFINED_TERMS";
30.65 val _ = tptp "SYSTEM_TERMS";