--- a/src/Tools/Metis/src/Tptp.sml Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/src/Tptp.sml Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
(* ========================================================================= *)
(* THE TPTP PROBLEM FILE FORMAT *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Tptp :> Tptp =
@@ -886,13 +886,26 @@
| FofFormulaBody fm => ppFof mapping (Formula.generalize fm);
(* ------------------------------------------------------------------------- *)
+(* Extra TPTP inferences. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype inference =
+ StripInference
+ | NegateInference;
+
+fun nameInference inf =
+ case inf of
+ StripInference => "strip"
+ | NegateInference => "negate";
+
+(* ------------------------------------------------------------------------- *)
(* TPTP formula sources. *)
(* ------------------------------------------------------------------------- *)
datatype formulaSource =
NoFormulaSource
| StripFormulaSource of
- {inference : string,
+ {inference : inference,
parents : formulaName list}
| NormalizeFormulaSource of
{inference : Normalize.inference,
@@ -983,8 +996,6 @@
val GEN_INFERENCE = "inference"
and GEN_INTRODUCED = "introduced";
- fun nameStrip inf = inf;
-
fun ppStrip mapping inf = Print.skip;
fun nameNormalize inf =
@@ -1075,7 +1086,7 @@
let
val gen = GEN_INFERENCE
- val name = nameStrip inference
+ val name = nameInference inference
in
Print.inconsistentBlock (size gen + 1)
[Print.ppString gen,
@@ -1315,7 +1326,7 @@
(fn ((),((),s)) => "$$" ^ s);
val nameParser =
- (stringParser || numberParser || quoteParser) >> FormulaName;
+ (lowerParser || numberParser || quoteParser) >> FormulaName;
val roleParser = lowerParser >> fromStringRole;
@@ -2043,46 +2054,79 @@
end;
local
- datatype blockComment =
- OutsideBlockComment
+ datatype comment =
+ NoComment
+ | EnteringLineComment
+ | InsideLineComment
| EnteringBlockComment
| InsideBlockComment
- | LeavingBlockComment;
-
- fun stripLineComments acc strm =
+ | LeavingBlockComment
+ | InsideSingleQuoteComment
+ | EscapedSingleQuoteComment;
+
+ fun stripInitialLineComments acc strm =
case strm of
Stream.Nil => (List.rev acc, Stream.Nil)
| Stream.Cons (line,rest) =>
case total destLineComment line of
- SOME s => stripLineComments (s :: acc) (rest ())
- | NONE => (List.rev acc, Stream.filter (not o isLineComment) strm);
-
- fun advanceBlockComment c state =
+ SOME s => stripInitialLineComments (s :: acc) (rest ())
+ | NONE => (List.rev acc, strm);
+
+ fun advanceComment c state =
case state of
- OutsideBlockComment =>
- if c = #"/" then (Stream.Nil, EnteringBlockComment)
- else (Stream.singleton c, OutsideBlockComment)
+ NoComment =>
+ (case c of
+ #"\n" => (Stream.Nil, EnteringLineComment)
+ | #"/" => (Stream.Nil, EnteringBlockComment)
+ | #"'" => (Stream.singleton #"'", InsideSingleQuoteComment)
+ | _ => (Stream.singleton c, NoComment))
+ | EnteringLineComment =>
+ (case c of
+ #"%" => (Stream.singleton #"\n", InsideLineComment)
+ | #"\n" => (Stream.singleton #"\n", EnteringLineComment)
+ | #"/" => (Stream.singleton #"\n", EnteringBlockComment)
+ | #"'" => (Stream.fromList [#"\n",#"'"], InsideSingleQuoteComment)
+ | _ => (Stream.fromList [#"\n",c], NoComment))
+ | InsideLineComment =>
+ (case c of
+ #"\n" => (Stream.Nil, EnteringLineComment)
+ | _ => (Stream.Nil, InsideLineComment))
| EnteringBlockComment =>
- if c = #"*" then (Stream.Nil, InsideBlockComment)
- else if c = #"/" then (Stream.singleton #"/", EnteringBlockComment)
- else (Stream.fromList [#"/",c], OutsideBlockComment)
+ (case c of
+ #"*" => (Stream.Nil, InsideBlockComment)
+ | #"\n" => (Stream.singleton #"/", EnteringLineComment)
+ | #"/" => (Stream.singleton #"/", EnteringBlockComment)
+ | #"'" => (Stream.fromList [#"/",#"'"], InsideSingleQuoteComment)
+ | _ => (Stream.fromList [#"/",c], NoComment))
| InsideBlockComment =>
- if c = #"*" then (Stream.Nil, LeavingBlockComment)
- else (Stream.Nil, InsideBlockComment)
+ (case c of
+ #"*" => (Stream.Nil, LeavingBlockComment)
+ | _ => (Stream.Nil, InsideBlockComment))
| LeavingBlockComment =>
- if c = #"/" then (Stream.Nil, OutsideBlockComment)
- else if c = #"*" then (Stream.Nil, LeavingBlockComment)
- else (Stream.Nil, InsideBlockComment);
-
- fun eofBlockComment state =
+ (case c of
+ #"/" => (Stream.Nil, NoComment)
+ | #"*" => (Stream.Nil, LeavingBlockComment)
+ | _ => (Stream.Nil, InsideBlockComment))
+ | InsideSingleQuoteComment =>
+ (case c of
+ #"'" => (Stream.singleton #"'", NoComment)
+ | #"\\" => (Stream.singleton #"\\", EscapedSingleQuoteComment)
+ | _ => (Stream.singleton c, InsideSingleQuoteComment))
+ | EscapedSingleQuoteComment =>
+ (Stream.singleton c, InsideSingleQuoteComment);
+
+ fun eofComment state =
case state of
- OutsideBlockComment => Stream.Nil
+ NoComment => Stream.Nil
+ | EnteringLineComment => Stream.singleton #"\n"
+ | InsideLineComment => Stream.Nil
| EnteringBlockComment => Stream.singleton #"/"
- | _ => raise Error "EOF inside a block comment";
-
- val stripBlockComments =
- Stream.mapsConcat advanceBlockComment eofBlockComment
- OutsideBlockComment;
+ | InsideBlockComment => raise Error "EOF inside a block comment"
+ | LeavingBlockComment => raise Error "EOF inside a block comment"
+ | InsideSingleQuoteComment => raise Error "EOF inside a single quote"
+ | EscapedSingleQuoteComment => raise Error "EOF inside a single quote";
+
+ val stripComments = Stream.mapsConcat advanceComment eofComment NoComment;
in
fun read {mapping,filename} =
let
@@ -2095,11 +2139,11 @@
(let
(* The character stream *)
- val (comments,chars) = stripLineComments [] chars
+ val (comments,chars) = stripInitialLineComments [] chars
val chars = Parse.everything Parse.any chars
- val chars = stripBlockComments chars
+ val chars = stripComments chars
(* The declaration stream *)
@@ -2347,7 +2391,7 @@
val source =
StripFormulaSource
- {inference = "strip",
+ {inference = StripInference,
parents = pars}
val formula =
@@ -2487,7 +2531,7 @@
let
val source =
StripFormulaSource
- {inference = "negate",
+ {inference = NegateInference,
parents = [name]}
val prefix = "negate_" ^ Int.toString number ^ "_"