--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/Tptp.sml Mon Sep 13 21:09:43 2010 +0200
@@ -0,0 +1,2559 @@
+(* ========================================================================= *)
+(* THE TPTP PROBLEM FILE FORMAT *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Tptp :> Tptp =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Default TPTP function and relation name mapping. *)
+(* ------------------------------------------------------------------------- *)
+
+val defaultFunctionMapping =
+ [(* Mapping TPTP functions to infix symbols *)
+ {name = "~", arity = 1, tptp = "negate"},
+ {name = "*", arity = 2, tptp = "multiply"},
+ {name = "/", arity = 2, tptp = "divide"},
+ {name = "+", arity = 2, tptp = "add"},
+ {name = "-", arity = 2, tptp = "subtract"},
+ {name = "::", arity = 2, tptp = "cons"},
+ {name = "@", arity = 2, tptp = "append"},
+ {name = ",", arity = 2, tptp = "pair"},
+ (* Expanding HOL symbols to TPTP alphanumerics *)
+ {name = ":", arity = 2, tptp = "has_type"},
+ {name = ".", arity = 2, tptp = "apply"}];
+
+val defaultRelationMapping =
+ [(* Mapping TPTP relations to infix symbols *)
+ {name = "=", arity = 2, tptp = "="}, (* this preserves the = symbol *)
+ {name = "==", arity = 2, tptp = "equalish"},
+ {name = "<=", arity = 2, tptp = "less_equal"},
+ {name = "<", arity = 2, tptp = "less_than"},
+ {name = ">=", arity = 2, tptp = "greater_equal"},
+ {name = ">", arity = 2, tptp = "greater_than"},
+ (* Expanding HOL symbols to TPTP alphanumerics *)
+ {name = "{}", arity = 1, tptp = "bool"}];
+
+(* ------------------------------------------------------------------------- *)
+(* Interpreting TPTP functions and relations in a finite model. *)
+(* ------------------------------------------------------------------------- *)
+
+val defaultFunctionModel =
+ [{name = "~", arity = 1, model = Model.negName},
+ {name = "*", arity = 2, model = Model.multName},
+ {name = "/", arity = 2, model = Model.divName},
+ {name = "+", arity = 2, model = Model.addName},
+ {name = "-", arity = 2, model = Model.subName},
+ {name = "::", arity = 2, model = Model.consName},
+ {name = "@", arity = 2, model = Model.appendName},
+ {name = ":", arity = 2, model = Term.hasTypeFunctionName},
+ {name = "additive_identity", arity = 0, model = Model.numeralName 0},
+ {name = "app", arity = 2, model = Model.appendName},
+ {name = "complement", arity = 1, model = Model.complementName},
+ {name = "difference", arity = 2, model = Model.differenceName},
+ {name = "divide", arity = 2, model = Model.divName},
+ {name = "empty_set", arity = 0, model = Model.emptyName},
+ {name = "identity", arity = 0, model = Model.numeralName 1},
+ {name = "identity_map", arity = 1, model = Model.projectionName 1},
+ {name = "intersection", arity = 2, model = Model.intersectName},
+ {name = "minus", arity = 1, model = Model.negName},
+ {name = "multiplicative_identity", arity = 0, model = Model.numeralName 1},
+ {name = "n0", arity = 0, model = Model.numeralName 0},
+ {name = "n1", arity = 0, model = Model.numeralName 1},
+ {name = "n2", arity = 0, model = Model.numeralName 2},
+ {name = "n3", arity = 0, model = Model.numeralName 3},
+ {name = "n4", arity = 0, model = Model.numeralName 4},
+ {name = "n5", arity = 0, model = Model.numeralName 5},
+ {name = "n6", arity = 0, model = Model.numeralName 6},
+ {name = "n7", arity = 0, model = Model.numeralName 7},
+ {name = "n8", arity = 0, model = Model.numeralName 8},
+ {name = "n9", arity = 0, model = Model.numeralName 9},
+ {name = "nil", arity = 0, model = Model.nilName},
+ {name = "null_class", arity = 0, model = Model.emptyName},
+ {name = "singleton", arity = 1, model = Model.singletonName},
+ {name = "successor", arity = 1, model = Model.sucName},
+ {name = "symmetric_difference", arity = 2,
+ model = Model.symmetricDifferenceName},
+ {name = "union", arity = 2, model = Model.unionName},
+ {name = "universal_class", arity = 0, model = Model.universeName}];
+
+val defaultRelationModel =
+ [{name = "=", arity = 2, model = Atom.eqRelationName},
+ {name = "==", arity = 2, model = Atom.eqRelationName},
+ {name = "<=", arity = 2, model = Model.leName},
+ {name = "<", arity = 2, model = Model.ltName},
+ {name = ">=", arity = 2, model = Model.geName},
+ {name = ">", arity = 2, model = Model.gtName},
+ {name = "divides", arity = 2, model = Model.dividesName},
+ {name = "element_of_set", arity = 2, model = Model.memberName},
+ {name = "equal", arity = 2, model = Atom.eqRelationName},
+ {name = "equal_elements", arity = 2, model = Atom.eqRelationName},
+ {name = "equal_sets", arity = 2, model = Atom.eqRelationName},
+ {name = "equivalent", arity = 2, model = Atom.eqRelationName},
+ {name = "less", arity = 2, model = Model.ltName},
+ {name = "less_or_equal", arity = 2, model = Model.leName},
+ {name = "member", arity = 2, model = Model.memberName},
+ {name = "subclass", arity = 2, model = Model.subsetName},
+ {name = "subset", arity = 2, model = Model.subsetName}];
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun isHdTlString hp tp s =
+ let
+ fun ct 0 = true
+ | ct i = tp (String.sub (s,i)) andalso ct (i - 1)
+
+ val n = size s
+ in
+ n > 0 andalso hp (String.sub (s,0)) andalso ct (n - 1)
+ end;
+
+fun stripSuffix pred s =
+ let
+ fun f 0 = ""
+ | f n =
+ let
+ val n' = n - 1
+ in
+ if pred (String.sub (s,n')) then f n'
+ else String.substring (s,0,n)
+ end
+ in
+ f (size s)
+ end;
+
+fun variant avoid s =
+ if not (StringSet.member s avoid) then s
+ else
+ let
+ val s = stripSuffix Char.isDigit s
+
+ fun var i =
+ let
+ val s_i = s ^ Int.toString i
+ in
+ if not (StringSet.member s_i avoid) then s_i else var (i + 1)
+ end
+ in
+ var 0
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping to legal TPTP names. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun nonEmptyPred p l =
+ case l of
+ [] => false
+ | c :: cs => p (c,cs);
+
+ fun existsPred l x = List.exists (fn p => p x) l;
+
+ fun isTptpChar #"_" = true
+ | isTptpChar c = Char.isAlphaNum c;
+
+ fun isTptpName l s = nonEmptyPred (existsPred l) (explode s);
+
+ fun isRegular (c,cs) =
+ Char.isLower c andalso List.all isTptpChar cs;
+
+ fun isNumber (c,cs) =
+ Char.isDigit c andalso List.all Char.isDigit cs;
+
+ fun isDefined (c,cs) =
+ c = #"$" andalso nonEmptyPred isRegular cs;
+
+ fun isSystem (c,cs) =
+ c = #"$" andalso nonEmptyPred isDefined cs;
+in
+ fun mkTptpVarName s =
+ let
+ val s =
+ case List.filter isTptpChar (explode s) of
+ [] => [#"X"]
+ | l as c :: cs =>
+ if Char.isUpper c then l
+ else if Char.isLower c then Char.toUpper c :: cs
+ else #"X" :: l
+ in
+ implode s
+ end;
+
+ val isTptpConstName = isTptpName [isRegular,isNumber,isDefined,isSystem]
+ and isTptpFnName = isTptpName [isRegular,isDefined,isSystem]
+ and isTptpPropName = isTptpName [isRegular,isDefined,isSystem]
+ and isTptpRelName = isTptpName [isRegular,isDefined,isSystem];
+
+ val isTptpFormulaName = isTptpName [isRegular,isNumber];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping to legal TPTP variable names. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype varToTptp = VarToTptp of StringSet.set * string NameMap.map;
+
+val emptyVarToTptp = VarToTptp (StringSet.empty, NameMap.new ());
+
+fun addVarToTptp vm v =
+ let
+ val VarToTptp (avoid,mapping) = vm
+ in
+ if NameMap.inDomain v mapping then vm
+ else
+ let
+ val s = variant avoid (mkTptpVarName (Name.toString v))
+
+ val avoid = StringSet.add avoid s
+ and mapping = NameMap.insert mapping (v,s)
+ in
+ VarToTptp (avoid,mapping)
+ end
+ end;
+
+local
+ fun add (v,vm) = addVarToTptp vm v;
+in
+ val addListVarToTptp = List.foldl add;
+
+ val addSetVarToTptp = NameSet.foldl add;
+end;
+
+val fromListVarToTptp = addListVarToTptp emptyVarToTptp;
+
+val fromSetVarToTptp = addSetVarToTptp emptyVarToTptp;
+
+fun getVarToTptp vm v =
+ let
+ val VarToTptp (_,mapping) = vm
+ in
+ case NameMap.peek mapping v of
+ SOME s => s
+ | NONE => raise Bug "Tptp.getVarToTptp: unknown var"
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping from TPTP variable names. *)
+(* ------------------------------------------------------------------------- *)
+
+fun getVarFromTptp s = Name.fromString s;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping to TPTP function and relation names. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype nameToTptp = NameToTptp of string NameArityMap.map;
+
+local
+ val emptyNames : string NameArityMap.map = NameArityMap.new ();
+
+ fun addNames ({name,arity,tptp},mapping) =
+ NameArityMap.insert mapping ((name,arity),tptp);
+
+ val fromListNames = List.foldl addNames emptyNames;
+in
+ fun mkNameToTptp mapping = NameToTptp (fromListNames mapping);
+end;
+
+local
+ fun escapeChar c =
+ case c of
+ #"\\" => "\\\\"
+ | #"'" => "\\'"
+ | #"\n" => "\\n"
+ | #"\t" => "\\t"
+ | _ => str c;
+
+ val escapeString = String.translate escapeChar;
+in
+ fun singleQuote s = "'" ^ escapeString s ^ "'";
+end;
+
+fun getNameToTptp isTptp s = if isTptp s then s else singleQuote s;
+
+fun getNameArityToTptp isZeroTptp isPlusTptp (NameToTptp mapping) na =
+ case NameArityMap.peek mapping na of
+ SOME s => s
+ | NONE =>
+ let
+ val (n,a) = na
+ val isTptp = if a = 0 then isZeroTptp else isPlusTptp
+ val s = Name.toString n
+ in
+ getNameToTptp isTptp s
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping from TPTP function and relation names. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype nameFromTptp = NameFromTptp of (string * int, Name.name) Map.map;
+
+local
+ val stringArityCompare = prodCompare String.compare Int.compare;
+
+ val emptyStringArityMap = Map.new stringArityCompare;
+
+ fun addStringArityMap ({name,arity,tptp},mapping) =
+ Map.insert mapping ((tptp,arity),name);
+
+ val fromListStringArityMap =
+ List.foldl addStringArityMap emptyStringArityMap;
+in
+ fun mkNameFromTptp mapping = NameFromTptp (fromListStringArityMap mapping);
+end;
+
+fun getNameFromTptp (NameFromTptp mapping) sa =
+ case Map.peek mapping sa of
+ SOME n => n
+ | NONE =>
+ let
+ val (s,_) = sa
+ in
+ Name.fromString s
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping to and from TPTP variable, function and relation names. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype mapping =
+ Mapping of
+ {varTo : varToTptp,
+ fnTo : nameToTptp,
+ relTo : nameToTptp,
+ fnFrom : nameFromTptp,
+ relFrom : nameFromTptp};
+
+fun mkMapping mapping =
+ let
+ val {functionMapping,relationMapping} = mapping
+
+ val varTo = emptyVarToTptp
+ val fnTo = mkNameToTptp functionMapping
+ val relTo = mkNameToTptp relationMapping
+
+ val fnFrom = mkNameFromTptp functionMapping
+ val relFrom = mkNameFromTptp relationMapping
+ in
+ Mapping
+ {varTo = varTo,
+ fnTo = fnTo,
+ relTo = relTo,
+ fnFrom = fnFrom,
+ relFrom = relFrom}
+ end;
+
+fun addVarListMapping mapping vs =
+ let
+ val Mapping
+ {varTo,
+ fnTo,
+ relTo,
+ fnFrom,
+ relFrom} = mapping
+
+ val varTo = addListVarToTptp varTo vs
+ in
+ Mapping
+ {varTo = varTo,
+ fnTo = fnTo,
+ relTo = relTo,
+ fnFrom = fnFrom,
+ relFrom = relFrom}
+ end;
+
+fun addVarSetMapping mapping vs =
+ let
+ val Mapping
+ {varTo,
+ fnTo,
+ relTo,
+ fnFrom,
+ relFrom} = mapping
+
+ val varTo = addSetVarToTptp varTo vs
+ in
+ Mapping
+ {varTo = varTo,
+ fnTo = fnTo,
+ relTo = relTo,
+ fnFrom = fnFrom,
+ relFrom = relFrom}
+ end;
+
+fun varToTptp mapping v =
+ let
+ val Mapping {varTo,...} = mapping
+ in
+ getVarToTptp varTo v
+ end;
+
+fun fnToTptp mapping fa =
+ let
+ val Mapping {fnTo,...} = mapping
+ in
+ getNameArityToTptp isTptpConstName isTptpFnName fnTo fa
+ end;
+
+fun relToTptp mapping ra =
+ let
+ val Mapping {relTo,...} = mapping
+ in
+ getNameArityToTptp isTptpPropName isTptpRelName relTo ra
+ end;
+
+fun varFromTptp (_ : mapping) v = getVarFromTptp v;
+
+fun fnFromTptp mapping fa =
+ let
+ val Mapping {fnFrom,...} = mapping
+ in
+ getNameFromTptp fnFrom fa
+ end;
+
+fun relFromTptp mapping ra =
+ let
+ val Mapping {relFrom,...} = mapping
+ in
+ getNameFromTptp relFrom ra
+ end;
+
+val defaultMapping =
+ let
+ fun lift {name,arity,tptp} =
+ {name = Name.fromString name, arity = arity, tptp = tptp}
+
+ val functionMapping = map lift defaultFunctionMapping
+ and relationMapping = map lift defaultRelationMapping
+
+ val mapping =
+ {functionMapping = functionMapping,
+ relationMapping = relationMapping}
+ in
+ mkMapping mapping
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Interpreting TPTP functions and relations in a finite model. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkFixedMap funcModel relModel =
+ let
+ fun mkEntry {name,arity,model} = ((Name.fromString name, arity), model)
+
+ fun mkMap l = NameArityMap.fromList (map mkEntry l)
+ in
+ {functionMap = mkMap funcModel,
+ relationMap = mkMap relModel}
+ end;
+
+val defaultFixedMap = mkFixedMap defaultFunctionModel defaultRelationModel;
+
+val defaultModel =
+ let
+ val {size = N, fixed = fix} = Model.default
+
+ val fix = Model.mapFixed defaultFixedMap fix
+ in
+ {size = N, fixed = fix}
+ end;
+
+local
+ fun toTptpMap toTptp =
+ let
+ fun add ((src,arity),dest,m) =
+ let
+ val src = Name.fromString (toTptp (src,arity))
+ in
+ NameArityMap.insert m ((src,arity),dest)
+ end
+ in
+ fn m => NameArityMap.foldl add (NameArityMap.new ()) m
+ end;
+
+ fun toTptpFixedMap mapping fixMap =
+ let
+ val {functionMap = fnMap, relationMap = relMap} = fixMap
+
+ val fnMap = toTptpMap (fnToTptp mapping) fnMap
+ and relMap = toTptpMap (relToTptp mapping) relMap
+ in
+ {functionMap = fnMap,
+ relationMap = relMap}
+ end;
+in
+ fun ppFixedMap mapping fixMap =
+ Model.ppFixedMap (toTptpFixedMap mapping fixMap);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP roles. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype role =
+ AxiomRole
+ | ConjectureRole
+ | DefinitionRole
+ | NegatedConjectureRole
+ | PlainRole
+ | TheoremRole
+ | OtherRole of string;
+
+fun isCnfConjectureRole role =
+ case role of
+ NegatedConjectureRole => true
+ | _ => false;
+
+fun isFofConjectureRole role =
+ case role of
+ ConjectureRole => true
+ | _ => false;
+
+fun toStringRole role =
+ case role of
+ AxiomRole => "axiom"
+ | ConjectureRole => "conjecture"
+ | DefinitionRole => "definition"
+ | NegatedConjectureRole => "negated_conjecture"
+ | PlainRole => "plain"
+ | TheoremRole => "theorem"
+ | OtherRole s => s;
+
+fun fromStringRole s =
+ case s of
+ "axiom" => AxiomRole
+ | "conjecture" => ConjectureRole
+ | "definition" => DefinitionRole
+ | "negated_conjecture" => NegatedConjectureRole
+ | "plain" => PlainRole
+ | "theorem" => TheoremRole
+ | _ => OtherRole s;
+
+val ppRole = Print.ppMap toStringRole Print.ppString;
+
+(* ------------------------------------------------------------------------- *)
+(* SZS statuses. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype status =
+ CounterSatisfiableStatus
+ | TheoremStatus
+ | SatisfiableStatus
+ | UnknownStatus
+ | UnsatisfiableStatus;
+
+fun toStringStatus status =
+ case status of
+ CounterSatisfiableStatus => "CounterSatisfiable"
+ | TheoremStatus => "Theorem"
+ | SatisfiableStatus => "Satisfiable"
+ | UnknownStatus => "Unknown"
+ | UnsatisfiableStatus => "Unsatisfiable";
+
+val ppStatus = Print.ppMap toStringStatus Print.ppString;
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP literals. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype literal =
+ Boolean of bool
+ | Literal of Literal.literal;
+
+fun destLiteral lit =
+ case lit of
+ Literal l => l
+ | _ => raise Error "Tptp.destLiteral";
+
+fun isBooleanLiteral lit =
+ case lit of
+ Boolean _ => true
+ | _ => false;
+
+fun equalBooleanLiteral b lit =
+ case lit of
+ Boolean b' => b = b'
+ | _ => false;
+
+fun negateLiteral (Boolean b) = (Boolean (not b))
+ | negateLiteral (Literal l) = (Literal (Literal.negate l));
+
+fun functionsLiteral (Boolean _) = NameAritySet.empty
+ | functionsLiteral (Literal lit) = Literal.functions lit;
+
+fun relationLiteral (Boolean _) = NONE
+ | relationLiteral (Literal lit) = SOME (Literal.relation lit);
+
+fun literalToFormula (Boolean true) = Formula.True
+ | literalToFormula (Boolean false) = Formula.False
+ | literalToFormula (Literal lit) = Literal.toFormula lit;
+
+fun literalFromFormula Formula.True = Boolean true
+ | literalFromFormula Formula.False = Boolean false
+ | literalFromFormula fm = Literal (Literal.fromFormula fm);
+
+fun freeVarsLiteral (Boolean _) = NameSet.empty
+ | freeVarsLiteral (Literal lit) = Literal.freeVars lit;
+
+fun literalSubst sub lit =
+ case lit of
+ Boolean _ => lit
+ | Literal l => Literal (Literal.subst sub l);
+
+(* ------------------------------------------------------------------------- *)
+(* Printing formulas using TPTP syntax. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppVar mapping v =
+ let
+ val s = varToTptp mapping v
+ in
+ Print.addString s
+ end;
+
+fun ppFnName mapping fa = Print.addString (fnToTptp mapping fa);
+
+fun ppConst mapping c = ppFnName mapping (c,0);
+
+fun ppTerm mapping =
+ let
+ fun term tm =
+ case tm of
+ Term.Var v => ppVar mapping v
+ | Term.Fn (f,tms) =>
+ case length tms of
+ 0 => ppConst mapping f
+ | a =>
+ Print.blockProgram Print.Inconsistent 2
+ [ppFnName mapping (f,a),
+ Print.addString "(",
+ Print.ppOpList "," term tms,
+ Print.addString ")"]
+ in
+ Print.block Print.Inconsistent 0 o term
+ end;
+
+fun ppRelName mapping ra = Print.addString (relToTptp mapping ra);
+
+fun ppProp mapping p = ppRelName mapping (p,0);
+
+fun ppAtom mapping (r,tms) =
+ case length tms of
+ 0 => ppProp mapping r
+ | a =>
+ Print.blockProgram Print.Inconsistent 2
+ [ppRelName mapping (r,a),
+ Print.addString "(",
+ Print.ppOpList "," (ppTerm mapping) tms,
+ Print.addString ")"];
+
+local
+ val neg = Print.sequence (Print.addString "~") (Print.addBreak 1);
+
+ fun fof mapping fm =
+ case fm of
+ Formula.And _ => assoc_binary mapping ("&", Formula.stripConj fm)
+ | Formula.Or _ => assoc_binary mapping ("|", Formula.stripDisj fm)
+ | Formula.Imp a_b => nonassoc_binary mapping ("=>",a_b)
+ | Formula.Iff a_b => nonassoc_binary mapping ("<=>",a_b)
+ | _ => unitary mapping fm
+
+ and nonassoc_binary mapping (s,a_b) =
+ Print.ppOp2 (" " ^ s) (unitary mapping) (unitary mapping) a_b
+
+ and assoc_binary mapping (s,l) = Print.ppOpList (" " ^ s) (unitary mapping) l
+
+ and unitary mapping fm =
+ case fm of
+ Formula.True => Print.addString "$true"
+ | Formula.False => Print.addString "$false"
+ | Formula.Forall _ => quantified mapping ("!", Formula.stripForall fm)
+ | Formula.Exists _ => quantified mapping ("?", Formula.stripExists fm)
+ | Formula.Not _ =>
+ (case total Formula.destNeq fm of
+ SOME a_b => Print.ppOp2 " !=" (ppTerm mapping) (ppTerm mapping) a_b
+ | NONE =>
+ let
+ val (n,fm) = Formula.stripNeg fm
+ in
+ Print.blockProgram Print.Inconsistent 2
+ [Print.duplicate n neg,
+ unitary mapping fm]
+ end)
+ | Formula.Atom atm =>
+ (case total Formula.destEq fm of
+ SOME a_b => Print.ppOp2 " =" (ppTerm mapping) (ppTerm mapping) a_b
+ | NONE => ppAtom mapping atm)
+ | _ =>
+ Print.blockProgram Print.Inconsistent 1
+ [Print.addString "(",
+ fof mapping fm,
+ Print.addString ")"]
+
+ and quantified mapping (q,(vs,fm)) =
+ let
+ val mapping = addVarListMapping mapping vs
+ in
+ Print.blockProgram Print.Inconsistent 2
+ [Print.addString q,
+ Print.addString " ",
+ Print.blockProgram Print.Inconsistent (String.size q)
+ [Print.addString "[",
+ Print.ppOpList "," (ppVar mapping) vs,
+ Print.addString "] :"],
+ Print.addBreak 1,
+ unitary mapping fm]
+ end;
+in
+ fun ppFof mapping fm = Print.block Print.Inconsistent 0 (fof mapping fm);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Lexing TPTP files. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype token =
+ AlphaNum of string
+ | Punct of char
+ | Quote of string;
+
+fun isAlphaNum #"_" = true
+ | isAlphaNum c = Char.isAlphaNum c;
+
+local
+ open Parse;
+
+ infixr 9 >>++
+ infixr 8 ++
+ infixr 7 >>
+ infixr 6 ||
+
+ val alphaNumToken = atLeastOne (some isAlphaNum) >> (AlphaNum o implode);
+
+ val punctToken =
+ let
+ val punctChars = "<>=-*+/\\?@|!$%&#^:;~()[]{}.,"
+ in
+ some (Char.contains punctChars) >> Punct
+ end;
+
+ val quoteToken =
+ let
+ val escapeParser =
+ some (equal #"'") >> singleton ||
+ some (equal #"\\") >> singleton
+
+ fun stopOn #"'" = true
+ | stopOn #"\n" = true
+ | stopOn _ = false
+
+ val quotedParser =
+ some (equal #"\\") ++ escapeParser >> op:: ||
+ some (not o stopOn) >> singleton
+ in
+ exactChar #"'" ++ many quotedParser ++ exactChar #"'" >>
+ (fn (_,(l,_)) => Quote (implode (List.concat l)))
+ end;
+
+ val lexToken = alphaNumToken || punctToken || quoteToken;
+
+ val space = many (some Char.isSpace) >> K ();
+in
+ val lexer = (space ++ lexToken ++ space) >> (fn ((),(tok,())) => tok);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP clauses. *)
+(* ------------------------------------------------------------------------- *)
+
+type clause = literal list;
+
+val clauseFunctions =
+ let
+ fun funcs (lit,acc) = NameAritySet.union (functionsLiteral lit) acc
+ in
+ foldl funcs NameAritySet.empty
+ end;
+
+val clauseRelations =
+ let
+ fun rels (lit,acc) =
+ case relationLiteral lit of
+ NONE => acc
+ | SOME r => NameAritySet.add acc r
+ in
+ foldl rels NameAritySet.empty
+ end;
+
+val clauseFreeVars =
+ let
+ fun fvs (lit,acc) = NameSet.union (freeVarsLiteral lit) acc
+ in
+ 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 clauseFromLiteralSet cl =
+ clauseFromFormula
+ (Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl));
+
+fun clauseFromThm th = clauseFromLiteralSet (Thm.clause th);
+
+fun ppClause mapping = Print.ppMap clauseToFormula (ppFof mapping);
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP formula names. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formulaName = FormulaName of string;
+
+datatype formulaNameSet = FormulaNameSet of formulaName Set.set;
+
+fun compareFormulaName (FormulaName s1, FormulaName s2) =
+ String.compare (s1,s2);
+
+fun toTptpFormulaName (FormulaName s) =
+ getNameToTptp isTptpFormulaName s;
+
+val ppFormulaName = Print.ppMap toTptpFormulaName Print.ppString;
+
+val emptyFormulaNameSet = FormulaNameSet (Set.empty compareFormulaName);
+
+fun memberFormulaNameSet n (FormulaNameSet s) = Set.member n s;
+
+fun addFormulaNameSet (FormulaNameSet s) n = FormulaNameSet (Set.add s n);
+
+fun addListFormulaNameSet (FormulaNameSet s) l =
+ FormulaNameSet (Set.addList s l);
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP formula bodies. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formulaBody =
+ CnfFormulaBody of literal list
+ | FofFormulaBody of Formula.formula;
+
+fun destCnfFormulaBody body =
+ case body of
+ CnfFormulaBody x => x
+ | _ => raise Error "destCnfFormulaBody";
+
+val isCnfFormulaBody = can destCnfFormulaBody;
+
+fun destFofFormulaBody body =
+ case body of
+ FofFormulaBody x => x
+ | _ => raise Error "destFofFormulaBody";
+
+val isFofFormulaBody = can destFofFormulaBody;
+
+fun formulaBodyFunctions body =
+ case body of
+ CnfFormulaBody cl => clauseFunctions cl
+ | FofFormulaBody fm => Formula.functions fm;
+
+fun formulaBodyRelations body =
+ case body of
+ CnfFormulaBody cl => clauseRelations cl
+ | FofFormulaBody fm => Formula.relations fm;
+
+fun formulaBodyFreeVars body =
+ case body of
+ CnfFormulaBody cl => clauseFreeVars cl
+ | FofFormulaBody fm => Formula.freeVars fm;
+
+fun ppFormulaBody mapping body =
+ case body of
+ CnfFormulaBody cl => ppClause mapping cl
+ | FofFormulaBody fm => ppFof mapping (Formula.generalize fm);
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP formula sources. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formulaSource =
+ NoFormulaSource
+ | StripFormulaSource of
+ {inference : string,
+ parents : formulaName list}
+ | NormalizeFormulaSource of
+ {inference : Normalize.inference,
+ parents : formulaName list}
+ | ProofFormulaSource of
+ {inference : Proof.inference,
+ parents : formulaName list};
+
+fun isNoFormulaSource source =
+ case source of
+ NoFormulaSource => true
+ | _ => false;
+
+fun functionsFormulaSource source =
+ case source of
+ NoFormulaSource => NameAritySet.empty
+ | StripFormulaSource _ => NameAritySet.empty
+ | NormalizeFormulaSource data =>
+ let
+ val {inference = inf, parents = _} = data
+ in
+ case inf of
+ Normalize.Axiom fm => Formula.functions fm
+ | Normalize.Definition (_,fm) => Formula.functions fm
+ | _ => NameAritySet.empty
+ end
+ | ProofFormulaSource data =>
+ let
+ val {inference = inf, parents = _} = data
+ in
+ case inf of
+ Proof.Axiom cl => LiteralSet.functions cl
+ | Proof.Assume atm => Atom.functions atm
+ | Proof.Subst (sub,_) => Subst.functions sub
+ | Proof.Resolve (atm,_,_) => Atom.functions atm
+ | Proof.Refl tm => Term.functions tm
+ | Proof.Equality (lit,_,tm) =>
+ NameAritySet.union (Literal.functions lit) (Term.functions tm)
+ end;
+
+fun relationsFormulaSource source =
+ case source of
+ NoFormulaSource => NameAritySet.empty
+ | StripFormulaSource _ => NameAritySet.empty
+ | NormalizeFormulaSource data =>
+ let
+ val {inference = inf, parents = _} = data
+ in
+ case inf of
+ Normalize.Axiom fm => Formula.relations fm
+ | Normalize.Definition (_,fm) => Formula.relations fm
+ | _ => NameAritySet.empty
+ end
+ | ProofFormulaSource data =>
+ let
+ val {inference = inf, parents = _} = data
+ in
+ case inf of
+ Proof.Axiom cl => LiteralSet.relations cl
+ | Proof.Assume atm => NameAritySet.singleton (Atom.relation atm)
+ | Proof.Subst _ => NameAritySet.empty
+ | Proof.Resolve (atm,_,_) => NameAritySet.singleton (Atom.relation atm)
+ | Proof.Refl tm => NameAritySet.empty
+ | Proof.Equality (lit,_,_) =>
+ NameAritySet.singleton (Literal.relation lit)
+ end;
+
+fun freeVarsFormulaSource source =
+ case source of
+ NoFormulaSource => NameSet.empty
+ | StripFormulaSource _ => NameSet.empty
+ | NormalizeFormulaSource data => NameSet.empty
+ | ProofFormulaSource data =>
+ let
+ val {inference = inf, parents = _} = data
+ in
+ case inf of
+ Proof.Axiom cl => LiteralSet.freeVars cl
+ | Proof.Assume atm => Atom.freeVars atm
+ | Proof.Subst (sub,_) => Subst.freeVars sub
+ | Proof.Resolve (atm,_,_) => Atom.freeVars atm
+ | Proof.Refl tm => Term.freeVars tm
+ | Proof.Equality (lit,_,tm) =>
+ NameSet.union (Literal.freeVars lit) (Term.freeVars tm)
+ end;
+
+local
+ val GEN_INFERENCE = "inference"
+ and GEN_INTRODUCED = "introduced";
+
+ fun nameStrip inf = inf;
+
+ fun ppStrip mapping inf = Print.skip;
+
+ fun nameNormalize inf =
+ case inf of
+ Normalize.Axiom _ => "canonicalize"
+ | Normalize.Definition _ => "canonicalize"
+ | Normalize.Simplify _ => "simplify"
+ | Normalize.Conjunct _ => "conjunct"
+ | Normalize.Specialize _ => "specialize"
+ | Normalize.Skolemize _ => "skolemize"
+ | Normalize.Clausify _ => "clausify";
+
+ fun ppNormalize mapping inf = Print.skip;
+
+ fun nameProof inf =
+ case inf of
+ Proof.Axiom _ => "canonicalize"
+ | Proof.Assume _ => "assume"
+ | Proof.Subst _ => "subst"
+ | Proof.Resolve _ => "resolve"
+ | Proof.Refl _ => "refl"
+ | Proof.Equality _ => "equality";
+
+ local
+ fun ppTermInf mapping = ppTerm mapping;
+
+ fun ppAtomInf mapping atm =
+ case total Atom.destEq atm of
+ SOME (a,b) => ppAtom mapping (Name.fromString "$equal", [a,b])
+ | NONE => ppAtom mapping atm;
+
+ fun ppLiteralInf mapping (pol,atm) =
+ Print.sequence
+ (if pol then Print.skip else Print.addString "~ ")
+ (ppAtomInf mapping atm);
+ in
+ fun ppProofTerm mapping =
+ Print.ppBracket "$fot(" ")" (ppTermInf mapping);
+
+ fun ppProofAtom mapping =
+ Print.ppBracket "$cnf(" ")" (ppAtomInf mapping);
+
+ fun ppProofLiteral mapping =
+ Print.ppBracket "$cnf(" ")" (ppLiteralInf mapping);
+ end;
+
+ val ppProofVar = ppVar;
+
+ val ppProofPath = Term.ppPath;
+
+ fun ppProof mapping inf =
+ Print.blockProgram Print.Inconsistent 1
+ [Print.addString "[",
+ (case inf of
+ Proof.Axiom _ => Print.skip
+ | Proof.Assume atm => ppProofAtom mapping atm
+ | Proof.Subst _ => Print.skip
+ | Proof.Resolve (atm,_,_) => ppProofAtom mapping atm
+ | Proof.Refl tm => ppProofTerm mapping tm
+ | Proof.Equality (lit,path,tm) =>
+ Print.program
+ [ppProofLiteral mapping lit,
+ Print.addString ",",
+ Print.addBreak 1,
+ ppProofPath path,
+ Print.addString ",",
+ Print.addBreak 1,
+ ppProofTerm mapping tm]),
+ Print.addString "]"];
+
+ val ppParent = ppFormulaName;
+
+ fun ppProofSubst mapping =
+ Print.ppMap Subst.toList
+ (Print.ppList
+ (Print.ppBracket "bind(" ")"
+ (Print.ppOp2 "," (ppProofVar mapping)
+ (ppProofTerm mapping))));
+
+ fun ppProofParent mapping (p,s) =
+ if Subst.null s then ppParent p
+ else Print.ppOp2 " :" ppParent (ppProofSubst mapping) (p,s);
+in
+ fun ppFormulaSource mapping source =
+ case source of
+ NoFormulaSource => Print.skip
+ | StripFormulaSource {inference,parents} =>
+ let
+ val gen = GEN_INFERENCE
+
+ val name = nameStrip inference
+ in
+ Print.blockProgram Print.Inconsistent (size gen + 1)
+ [Print.addString gen,
+ Print.addString "(",
+ Print.addString name,
+ Print.addString ",",
+ Print.addBreak 1,
+ Print.ppBracket "[" "]" (ppStrip mapping) inference,
+ Print.addString ",",
+ Print.addBreak 1,
+ Print.ppList ppParent parents,
+ Print.addString ")"]
+ end
+ | NormalizeFormulaSource {inference,parents} =>
+ let
+ val gen = GEN_INFERENCE
+
+ val name = nameNormalize inference
+ in
+ Print.blockProgram Print.Inconsistent (size gen + 1)
+ [Print.addString gen,
+ Print.addString "(",
+ Print.addString name,
+ Print.addString ",",
+ Print.addBreak 1,
+ Print.ppBracket "[" "]" (ppNormalize mapping) inference,
+ Print.addString ",",
+ Print.addBreak 1,
+ Print.ppList ppParent parents,
+ Print.addString ")"]
+ end
+ | ProofFormulaSource {inference,parents} =>
+ let
+ val isTaut = null parents
+
+ val gen = if isTaut then GEN_INTRODUCED else GEN_INFERENCE
+
+ val name = nameProof inference
+
+ val parents =
+ let
+ val sub =
+ case inference of
+ Proof.Subst (s,_) => s
+ | _ => Subst.empty
+ in
+ map (fn parent => (parent,sub)) parents
+ end
+ in
+ Print.blockProgram Print.Inconsistent (size gen + 1)
+ ([Print.addString gen,
+ Print.addString "("] @
+ (if isTaut then
+ [Print.addString "tautology",
+ Print.addString ",",
+ Print.addBreak 1,
+ Print.blockProgram Print.Inconsistent 1
+ [Print.addString "[",
+ Print.addString name,
+ Print.addString ",",
+ Print.addBreak 1,
+ ppProof mapping inference,
+ Print.addString "]"]]
+ else
+ [Print.addString name,
+ Print.addString ",",
+ Print.addBreak 1,
+ ppProof mapping inference,
+ Print.addString ",",
+ Print.addBreak 1,
+ Print.ppList (ppProofParent mapping) parents]) @
+ [Print.addString ")"])
+ end
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+ Formula of
+ {name : formulaName,
+ role : role,
+ body : formulaBody,
+ source : formulaSource};
+
+fun nameFormula (Formula {name,...}) = name;
+
+fun roleFormula (Formula {role,...}) = role;
+
+fun bodyFormula (Formula {body,...}) = body;
+
+fun sourceFormula (Formula {source,...}) = source;
+
+fun destCnfFormula fm = destCnfFormulaBody (bodyFormula fm);
+
+val isCnfFormula = can destCnfFormula;
+
+fun destFofFormula fm = destFofFormulaBody (bodyFormula fm);
+
+val isFofFormula = can destFofFormula;
+
+fun functionsFormula fm =
+ let
+ val bodyFns = formulaBodyFunctions (bodyFormula fm)
+ and sourceFns = functionsFormulaSource (sourceFormula fm)
+ in
+ NameAritySet.union bodyFns sourceFns
+ end;
+
+fun relationsFormula fm =
+ let
+ val bodyRels = formulaBodyRelations (bodyFormula fm)
+ and sourceRels = relationsFormulaSource (sourceFormula fm)
+ in
+ NameAritySet.union bodyRels sourceRels
+ end;
+
+fun freeVarsFormula fm =
+ let
+ val bodyFvs = formulaBodyFreeVars (bodyFormula fm)
+ and sourceFvs = freeVarsFormulaSource (sourceFormula fm)
+ in
+ NameSet.union bodyFvs sourceFvs
+ end;
+
+val freeVarsListFormula =
+ let
+ fun add (fm,vs) = NameSet.union vs (freeVarsFormula fm)
+ in
+ List.foldl add NameSet.empty
+ end;
+
+val formulasFunctions =
+ let
+ fun funcs (fm,acc) = NameAritySet.union (functionsFormula fm) acc
+ in
+ foldl funcs NameAritySet.empty
+ end;
+
+val formulasRelations =
+ let
+ fun rels (fm,acc) = NameAritySet.union (relationsFormula fm) acc
+ in
+ foldl rels NameAritySet.empty
+ end;
+
+fun isCnfConjectureFormula fm =
+ case fm of
+ Formula {role, body = CnfFormulaBody _, ...} => isCnfConjectureRole role
+ | _ => false;
+
+fun isFofConjectureFormula fm =
+ case fm of
+ Formula {role, body = FofFormulaBody _, ...} => isFofConjectureRole role
+ | _ => false;
+
+fun isConjectureFormula fm =
+ isCnfConjectureFormula fm orelse
+ isFofConjectureFormula fm;
+
+(* Parsing and pretty-printing *)
+
+fun ppFormula mapping fm =
+ let
+ val Formula {name,role,body,source} = fm
+
+ val gen =
+ case body of
+ CnfFormulaBody _ => "cnf"
+ | FofFormulaBody _ => "fof"
+ in
+ Print.blockProgram Print.Inconsistent (size gen + 1)
+ ([Print.addString gen,
+ Print.addString "(",
+ ppFormulaName name,
+ Print.addString ",",
+ Print.addBreak 1,
+ ppRole role,
+ Print.addString ",",
+ Print.addBreak 1,
+ Print.blockProgram Print.Consistent 1
+ [Print.addString "(",
+ ppFormulaBody mapping body,
+ Print.addString ")"]] @
+ (if isNoFormulaSource source then []
+ else
+ [Print.addString ",",
+ Print.addBreak 1,
+ ppFormulaSource mapping source]) @
+ [Print.addString ")."])
+ end;
+
+fun formulaToString mapping = Print.toString (ppFormula mapping);
+
+local
+ open Parse;
+
+ infixr 9 >>++
+ infixr 8 ++
+ infixr 7 >>
+ infixr 6 ||
+
+ fun someAlphaNum p =
+ maybe (fn AlphaNum s => if p s then SOME s else NONE | _ => NONE);
+
+ fun alphaNumParser s = someAlphaNum (equal s) >> K ();
+
+ val lowerParser = someAlphaNum (fn s => Char.isLower (String.sub (s,0)));
+
+ val upperParser = someAlphaNum (fn s => Char.isUpper (String.sub (s,0)));
+
+ val stringParser = lowerParser || upperParser;
+
+ val numberParser = someAlphaNum (List.all Char.isDigit o explode);
+
+ fun somePunct p =
+ maybe (fn Punct c => if p c then SOME c else NONE | _ => NONE);
+
+ fun punctParser c = somePunct (equal c) >> K ();
+
+ val quoteParser = maybe (fn Quote s => SOME s | _ => NONE);
+
+ local
+ fun f [] = raise Bug "symbolParser"
+ | f [x] = x
+ | f (h :: t) = (h ++ f t) >> K ();
+ in
+ fun symbolParser s = f (map punctParser (explode s));
+ end;
+
+ val definedParser =
+ punctParser #"$" ++ someAlphaNum (K true) >> (fn ((),s) => "$" ^ s);
+
+ val systemParser =
+ punctParser #"$" ++ punctParser #"$" ++ someAlphaNum (K true) >>
+ (fn ((),((),s)) => "$$" ^ s);
+
+ val nameParser =
+ (stringParser || numberParser || quoteParser) >> FormulaName;
+
+ val roleParser = lowerParser >> fromStringRole;
+
+ local
+ fun isProposition s = isHdTlString Char.isLower isAlphaNum s;
+ in
+ val propositionParser =
+ someAlphaNum isProposition ||
+ definedParser ||
+ systemParser ||
+ quoteParser;
+ end;
+
+ local
+ fun isFunction s = isHdTlString Char.isLower isAlphaNum s;
+ in
+ val functionParser =
+ someAlphaNum isFunction ||
+ definedParser ||
+ systemParser ||
+ quoteParser;
+ end;
+
+ local
+ fun isConstant s = isHdTlString Char.isLower isAlphaNum s;
+ in
+ val constantParser =
+ someAlphaNum isConstant ||
+ definedParser ||
+ numberParser ||
+ systemParser ||
+ quoteParser;
+ end;
+
+ val varParser = upperParser;
+
+ val varListParser =
+ (punctParser #"[" ++ varParser ++
+ many ((punctParser #"," ++ varParser) >> snd) ++
+ punctParser #"]") >>
+ (fn ((),(h,(t,()))) => h :: t);
+
+ fun mkVarName mapping v = varFromTptp mapping v;
+
+ fun mkVar mapping v =
+ let
+ val v = mkVarName mapping v
+ in
+ Term.Var v
+ end
+
+ fun mkFn mapping (f,tms) =
+ let
+ val f = fnFromTptp mapping (f, length tms)
+ in
+ Term.Fn (f,tms)
+ end;
+
+ fun mkConst mapping c = mkFn mapping (c,[]);
+
+ fun mkAtom mapping (r,tms) =
+ let
+ val r = relFromTptp mapping (r, length tms)
+ in
+ (r,tms)
+ end;
+
+ fun termParser mapping input =
+ let
+ val fnP = functionArgumentsParser mapping >> mkFn mapping
+ val nonFnP = nonFunctionArgumentsTermParser mapping
+ in
+ fnP || nonFnP
+ end input
+
+ and functionArgumentsParser mapping input =
+ let
+ val commaTmP = (punctParser #"," ++ termParser mapping) >> snd
+ in
+ (functionParser ++ punctParser #"(" ++ termParser mapping ++
+ many commaTmP ++ punctParser #")") >>
+ (fn (f,((),(t,(ts,())))) => (f, t :: ts))
+ end input
+
+ and nonFunctionArgumentsTermParser mapping input =
+ let
+ val varP = varParser >> mkVar mapping
+ val constP = constantParser >> mkConst mapping
+ in
+ varP || constP
+ end input;
+
+ fun binaryAtomParser mapping tm input =
+ let
+ val eqP =
+ (punctParser #"=" ++ termParser mapping) >>
+ (fn ((),r) => (true,("$equal",[tm,r])))
+
+ val neqP =
+ (symbolParser "!=" ++ termParser mapping) >>
+ (fn ((),r) => (false,("$equal",[tm,r])))
+ in
+ eqP || neqP
+ end input;
+
+ fun maybeBinaryAtomParser mapping (s,tms) input =
+ let
+ val tm = mkFn mapping (s,tms)
+ in
+ optional (binaryAtomParser mapping tm) >>
+ (fn SOME lit => lit
+ | NONE => (true,(s,tms)))
+ end input;
+
+ fun literalAtomParser mapping input =
+ let
+ val fnP =
+ functionArgumentsParser mapping >>++
+ maybeBinaryAtomParser mapping
+
+ val nonFnP =
+ nonFunctionArgumentsTermParser mapping >>++
+ binaryAtomParser mapping
+
+ val propP = propositionParser >> (fn s => (true,(s,[])))
+ in
+ fnP || nonFnP || propP
+ end input;
+
+ fun atomParser mapping input =
+ let
+ fun mk (pol,rel) =
+ case rel of
+ ("$true",[]) => Boolean pol
+ | ("$false",[]) => Boolean (not pol)
+ | ("$equal",[l,r]) => Literal (pol, Atom.mkEq (l,r))
+ | (r,tms) => Literal (pol, mkAtom mapping (r,tms))
+ in
+ literalAtomParser mapping >> mk
+ end input;
+
+ fun literalParser mapping input =
+ let
+ val negP =
+ (punctParser #"~" ++ atomParser mapping) >>
+ (negateLiteral o snd)
+
+ val posP = atomParser mapping
+ in
+ negP || posP
+ end input;
+
+ fun disjunctionParser mapping input =
+ let
+ val orLitP = (punctParser #"|" ++ literalParser mapping) >> snd
+ in
+ (literalParser mapping ++ many orLitP) >> (fn (h,t) => h :: t)
+ end input;
+
+ fun clauseParser mapping input =
+ let
+ val disjP = disjunctionParser mapping
+
+ val bracketDisjP =
+ (punctParser #"(" ++ disjP ++ punctParser #")") >>
+ (fn ((),(c,())) => c)
+ in
+ bracketDisjP || disjP
+ end input;
+
+ val binaryConnectiveParser =
+ (symbolParser "<=>" >> K Formula.Iff) ||
+ (symbolParser "=>" >> K Formula.Imp) ||
+ (symbolParser "<=" >> K (fn (f,g) => Formula.Imp (g,f))) ||
+ (symbolParser "<~>" >> K (Formula.Not o Formula.Iff)) ||
+ (symbolParser "~|" >> K (Formula.Not o Formula.Or)) ||
+ (symbolParser "~&" >> K (Formula.Not o Formula.And));
+
+ val quantifierParser =
+ (punctParser #"!" >> K Formula.listMkForall) ||
+ (punctParser #"?" >> K Formula.listMkExists);
+
+ fun fofFormulaParser mapping input =
+ let
+ fun mk (f,NONE) = f
+ | mk (f, SOME t) = t f
+ in
+ (unitaryFormulaParser mapping ++
+ optional (binaryFormulaParser mapping)) >> mk
+ end input
+
+ and binaryFormulaParser mapping input =
+ let
+ val nonAssocP = nonAssocBinaryFormulaParser mapping
+
+ val assocP = assocBinaryFormulaParser mapping
+ in
+ nonAssocP || assocP
+ end input
+
+ and nonAssocBinaryFormulaParser mapping input =
+ let
+ fun mk (c,g) f = c (f,g)
+ in
+ (binaryConnectiveParser ++ unitaryFormulaParser mapping) >> mk
+ end input
+
+ and assocBinaryFormulaParser mapping input =
+ let
+ val orP = orFormulaParser mapping
+
+ val andP = andFormulaParser mapping
+ in
+ orP || andP
+ end input
+
+ and orFormulaParser mapping input =
+ let
+ val orFmP = (punctParser #"|" ++ unitaryFormulaParser mapping) >> snd
+ in
+ atLeastOne orFmP >>
+ (fn fs => fn f => Formula.listMkDisj (f :: fs))
+ end input
+
+ and andFormulaParser mapping input =
+ let
+ val andFmP = (punctParser #"&" ++ unitaryFormulaParser mapping) >> snd
+ in
+ atLeastOne andFmP >>
+ (fn fs => fn f => Formula.listMkConj (f :: fs))
+ end input
+
+ and unitaryFormulaParser mapping input =
+ let
+ val quantP = quantifiedFormulaParser mapping
+
+ val unaryP = unaryFormulaParser mapping
+
+ val brackP =
+ (punctParser #"(" ++ fofFormulaParser mapping ++
+ punctParser #")") >>
+ (fn ((),(f,())) => f)
+
+ val atomP =
+ atomParser mapping >>
+ (fn Boolean b => Formula.mkBoolean b
+ | Literal l => Literal.toFormula l)
+ in
+ quantP ||
+ unaryP ||
+ brackP ||
+ atomP
+ end input
+
+ and quantifiedFormulaParser mapping input =
+ let
+ fun mk (q,(vs,((),f))) = q (map (mkVarName mapping) vs, f)
+ in
+ (quantifierParser ++ varListParser ++ punctParser #":" ++
+ unitaryFormulaParser mapping) >> mk
+ end input
+
+ and unaryFormulaParser mapping input =
+ let
+ fun mk (c,f) = c f
+ in
+ (unaryConnectiveParser ++ unitaryFormulaParser mapping) >> mk
+ end input
+
+ and unaryConnectiveParser input =
+ (punctParser #"~" >> K Formula.Not) input;
+
+ fun cnfParser mapping input =
+ let
+ fun mk ((),((),(name,((),(role,((),(cl,((),())))))))) =
+ let
+ val body = CnfFormulaBody cl
+ val source = NoFormulaSource
+ in
+ Formula
+ {name = name,
+ role = role,
+ body = body,
+ source = source}
+ end
+ in
+ (alphaNumParser "cnf" ++ punctParser #"(" ++
+ nameParser ++ punctParser #"," ++
+ roleParser ++ punctParser #"," ++
+ clauseParser mapping ++ punctParser #")" ++
+ punctParser #".") >> mk
+ end input;
+
+ fun fofParser mapping input =
+ let
+ fun mk ((),((),(name,((),(role,((),(fm,((),())))))))) =
+ let
+ val body = FofFormulaBody fm
+ val source = NoFormulaSource
+ in
+ Formula
+ {name = name,
+ role = role,
+ body = body,
+ source = source}
+ end
+ in
+ (alphaNumParser "fof" ++ punctParser #"(" ++
+ nameParser ++ punctParser #"," ++
+ roleParser ++ punctParser #"," ++
+ fofFormulaParser mapping ++ punctParser #")" ++
+ punctParser #".") >> mk
+ end input;
+in
+ fun formulaParser mapping input =
+ let
+ val cnfP = cnfParser mapping
+
+ val fofP = fofParser mapping
+ in
+ cnfP || fofP
+ end input;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Include declarations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppInclude i =
+ Print.blockProgram Print.Inconsistent 2
+ [Print.addString "include('",
+ Print.addString i,
+ Print.addString "')."];
+
+val includeToString = Print.toString ppInclude;
+
+local
+ open Parse;
+
+ infixr 9 >>++
+ infixr 8 ++
+ infixr 7 >>
+ infixr 6 ||
+
+ val filenameParser = maybe (fn Quote s => SOME s | _ => NONE);
+in
+ val includeParser =
+ (some (equal (AlphaNum "include")) ++
+ some (equal (Punct #"(")) ++
+ filenameParser ++
+ some (equal (Punct #")")) ++
+ some (equal (Punct #"."))) >>
+ (fn (_,(_,(f,(_,_)))) => f);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing TPTP files. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype declaration =
+ IncludeDeclaration of string
+ | FormulaDeclaration of formula;
+
+val partitionDeclarations =
+ let
+ fun part (d,(il,fl)) =
+ case d of
+ IncludeDeclaration i => (i :: il, fl)
+ | FormulaDeclaration f => (il, f :: fl)
+ in
+ fn l => List.foldl part ([],[]) (rev l)
+ end;
+
+local
+ open Parse;
+
+ infixr 9 >>++
+ infixr 8 ++
+ infixr 7 >>
+ infixr 6 ||
+
+ fun declarationParser mapping =
+ (includeParser >> IncludeDeclaration) ||
+ (formulaParser mapping >> FormulaDeclaration);
+
+ fun parseChars parser chars =
+ let
+ val tokens = Parse.everything (lexer >> singleton) chars
+ in
+ Parse.everything (parser >> singleton) tokens
+ end;
+in
+ fun parseDeclaration mapping = parseChars (declarationParser mapping);
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Clause information. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype clauseSource =
+ CnfClauseSource of formulaName * literal list
+ | FofClauseSource of Normalize.thm;
+
+type 'a clauseInfo = 'a LiteralSetMap.map;
+
+type clauseNames = formulaName clauseInfo;
+
+type clauseRoles = role clauseInfo;
+
+type clauseSources = clauseSource clauseInfo;
+
+val noClauseNames : clauseNames = LiteralSetMap.new ();
+
+val allClauseNames : clauseNames -> formulaNameSet =
+ let
+ fun add (_,n,s) = addFormulaNameSet s n
+ in
+ LiteralSetMap.foldl add emptyFormulaNameSet
+ end;
+
+val noClauseRoles : clauseRoles = LiteralSetMap.new ();
+
+val noClauseSources : clauseSources = LiteralSetMap.new ();
+
+(* ------------------------------------------------------------------------- *)
+(* Comments. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkLineComment "" = "%"
+ | mkLineComment line = "% " ^ line;
+
+fun destLineComment cs =
+ case cs of
+ [] => ""
+ | #"%" :: #" " :: rest => implode rest
+ | #"%" :: rest => implode rest
+ | _ => raise Error "Tptp.destLineComment";
+
+val isLineComment = can destLineComment;
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP problems. *)
+(* ------------------------------------------------------------------------- *)
+
+type comments = string list;
+
+type includes = string list;
+
+datatype problem =
+ Problem of
+ {comments : comments,
+ includes : includes,
+ formulas : formula list};
+
+fun hasCnfConjecture (Problem {formulas,...}) =
+ List.exists isCnfConjectureFormula formulas;
+
+fun hasFofConjecture (Problem {formulas,...}) =
+ List.exists isFofConjectureFormula formulas;
+
+fun hasConjecture (Problem {formulas,...}) =
+ List.exists isConjectureFormula formulas;
+
+fun freeVars (Problem {formulas,...}) = freeVarsListFormula formulas;
+
+local
+ fun bump n avoid =
+ let
+ val s = FormulaName (Int.toString n)
+ in
+ if memberFormulaNameSet s avoid then bump (n + 1) avoid
+ else (s, n, addFormulaNameSet avoid s)
+ end;
+
+ fun fromClause defaultRole names roles cl (n,avoid) =
+ let
+ val (name,n,avoid) =
+ case LiteralSetMap.peek names cl of
+ SOME name => (name,n,avoid)
+ | NONE => bump n avoid
+
+ val role = Option.getOpt (LiteralSetMap.peek roles cl, defaultRole)
+
+ val body = CnfFormulaBody (clauseFromLiteralSet cl)
+
+ val source = NoFormulaSource
+
+ val formula =
+ Formula
+ {name = name,
+ role = role,
+ body = body,
+ source = source}
+ in
+ (formula,(n,avoid))
+ end;
+in
+ fun mkProblem {comments,includes,names,roles,problem} =
+ let
+ fun fromCl defaultRole = fromClause defaultRole names roles
+
+ val {axioms,conjecture} = problem
+
+ val n_avoid = (0, allClauseNames names)
+
+ val (axiomFormulas,n_avoid) = maps (fromCl AxiomRole) axioms n_avoid
+
+ val (conjectureFormulas,_) =
+ maps (fromCl NegatedConjectureRole) conjecture n_avoid
+
+ val formulas = axiomFormulas @ conjectureFormulas
+ in
+ Problem
+ {comments = comments,
+ includes = includes,
+ formulas = formulas}
+ end;
+end;
+
+type normalization =
+ {problem : Problem.problem,
+ sources : clauseSources};
+
+val initialNormalization : normalization =
+ {problem = {axioms = [], conjecture = []},
+ sources = noClauseSources};
+
+datatype problemGoal =
+ NoGoal
+ | CnfGoal of (formulaName * clause) list
+ | FofGoal of (formulaName * Formula.formula) list;
+
+local
+ fun partitionFormula (formula,(cnfAxioms,fofAxioms,cnfGoals,fofGoals)) =
+ let
+ val Formula {name,role,body,...} = formula
+ in
+ case body of
+ CnfFormulaBody cl =>
+ if isCnfConjectureRole role then
+ let
+ val cnfGoals = (name,cl) :: cnfGoals
+ in
+ (cnfAxioms,fofAxioms,cnfGoals,fofGoals)
+ end
+ else
+ let
+ val cnfAxioms = (name,cl) :: cnfAxioms
+ in
+ (cnfAxioms,fofAxioms,cnfGoals,fofGoals)
+ end
+ | FofFormulaBody fm =>
+ if isFofConjectureRole role then
+ let
+ val fofGoals = (name,fm) :: fofGoals
+ in
+ (cnfAxioms,fofAxioms,cnfGoals,fofGoals)
+ end
+ else
+ let
+ val fofAxioms = (name,fm) :: fofAxioms
+ in
+ (cnfAxioms,fofAxioms,cnfGoals,fofGoals)
+ end
+ end;
+
+ fun partitionFormulas fms =
+ let
+ val (cnfAxioms,fofAxioms,cnfGoals,fofGoals) =
+ List.foldl partitionFormula ([],[],[],[]) fms
+
+ val goal =
+ case (rev cnfGoals, rev fofGoals) of
+ ([],[]) => NoGoal
+ | (cnfGoals,[]) => CnfGoal cnfGoals
+ | ([],fofGoals) => FofGoal fofGoals
+ | (_ :: _, _ :: _) =>
+ raise Error "TPTP problem has both cnf and fof conjecture formulas"
+ in
+ {cnfAxioms = rev cnfAxioms,
+ fofAxioms = rev fofAxioms,
+ goal = goal}
+ end;
+
+ fun addClauses role clauses acc : normalization =
+ let
+ fun addClause (cl_src,sources) =
+ LiteralSetMap.insert sources cl_src
+
+ val {problem,sources} : normalization = acc
+ val {axioms,conjecture} = problem
+
+ val cls = map fst clauses
+ val (axioms,conjecture) =
+ if isCnfConjectureRole role then (axioms, cls @ conjecture)
+ else (cls @ axioms, conjecture)
+
+ val problem = {axioms = axioms, conjecture = conjecture}
+ and sources = List.foldl addClause sources clauses
+ in
+ {problem = problem,
+ sources = sources}
+ end;
+
+ fun addCnf role ((name,clause),(norm,cnf)) =
+ if List.exists (equalBooleanLiteral true) clause then (norm,cnf)
+ else
+ let
+ val cl = List.mapPartial (total destLiteral) clause
+ val cl = LiteralSet.fromList cl
+
+ val src = CnfClauseSource (name,clause)
+
+ val norm = addClauses role [(cl,src)] norm
+ in
+ (norm,cnf)
+ end;
+
+ val addCnfAxiom = addCnf AxiomRole;
+
+ val addCnfGoal = addCnf NegatedConjectureRole;
+
+ fun addFof role (th,(norm,cnf)) =
+ let
+ fun sourcify (cl,inf) = (cl, FofClauseSource inf)
+
+ val (clauses,cnf) = Normalize.addCnf th cnf
+ val clauses = map sourcify clauses
+ val norm = addClauses role clauses norm
+ in
+ (norm,cnf)
+ end;
+
+ fun addFofAxiom ((_,fm),acc) =
+ addFof AxiomRole (Normalize.mkAxiom fm, acc);
+
+ fun normProblem subgoal (norm,_) =
+ let
+ val {problem,sources} = norm
+ val {axioms,conjecture} = problem
+ val problem = {axioms = rev axioms, conjecture = rev conjecture}
+ in
+ {subgoal = subgoal,
+ problem = problem,
+ sources = sources}
+ end;
+
+ val normProblemFalse = normProblem (Formula.False,[]);
+
+ fun splitProblem acc =
+ let
+ fun mk parents subgoal =
+ let
+ val subgoal = Formula.generalize subgoal
+
+ val th = Normalize.mkAxiom (Formula.Not subgoal)
+
+ val acc = addFof NegatedConjectureRole (th,acc)
+ in
+ normProblem (subgoal,parents) acc
+ end
+
+ fun split (name,goal) =
+ let
+ val subgoals = Formula.splitGoal goal
+ val subgoals =
+ if null subgoals then [Formula.True] else subgoals
+
+ val parents = [name]
+ in
+ map (mk parents) subgoals
+ end
+ in
+ fn goals => List.concat (map split goals)
+ end;
+
+ fun clausesToGoal cls =
+ let
+ val cls = 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
+ in
+ Formula.listMkConj fms
+ end;
+in
+ fun goal (Problem {formulas,...}) =
+ let
+ val {cnfAxioms,fofAxioms,goal} = partitionFormulas formulas
+
+ val fm =
+ case goal of
+ NoGoal => Formula.False
+ | CnfGoal cls => Formula.Imp (clausesToGoal cls, Formula.False)
+ | FofGoal goals => formulasToGoal goals
+
+ val fm =
+ if null fofAxioms then fm
+ else Formula.Imp (formulasToGoal fofAxioms, fm)
+
+ val fm =
+ if null cnfAxioms then fm
+ else Formula.Imp (clausesToGoal cnfAxioms, fm)
+ in
+ fm
+ end;
+
+ fun normalize (Problem {formulas,...}) =
+ let
+ val {cnfAxioms,fofAxioms,goal} = partitionFormulas formulas
+
+ val acc = (initialNormalization, Normalize.initialCnf)
+ val acc = List.foldl addCnfAxiom acc cnfAxioms
+ val acc = List.foldl addFofAxiom acc fofAxioms
+ in
+ case goal of
+ NoGoal => [normProblemFalse acc]
+ | CnfGoal cls => [normProblemFalse (List.foldl addCnfGoal acc cls)]
+ | FofGoal goals => splitProblem acc goals
+ end;
+end;
+
+local
+ datatype blockComment =
+ OutsideBlockComment
+ | EnteringBlockComment
+ | InsideBlockComment
+ | LeavingBlockComment;
+
+ fun stripLineComments acc strm =
+ case strm of
+ Stream.Nil => (rev acc, Stream.Nil)
+ | Stream.Cons (line,rest) =>
+ case total destLineComment line of
+ SOME s => stripLineComments (s :: acc) (rest ())
+ | NONE => (rev acc, Stream.filter (not o isLineComment) strm);
+
+ fun advanceBlockComment c state =
+ case state of
+ OutsideBlockComment =>
+ if c = #"/" then (Stream.Nil, EnteringBlockComment)
+ else (Stream.singleton c, OutsideBlockComment)
+ | EnteringBlockComment =>
+ if c = #"*" then (Stream.Nil, InsideBlockComment)
+ else if c = #"/" then (Stream.singleton #"/", EnteringBlockComment)
+ else (Stream.fromList [#"/",c], OutsideBlockComment)
+ | InsideBlockComment =>
+ if c = #"*" then (Stream.Nil, LeavingBlockComment)
+ else (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 state of
+ OutsideBlockComment => Stream.Nil
+ | EnteringBlockComment => Stream.singleton #"/"
+ | _ => raise Error "EOF inside a block comment";
+
+ val stripBlockComments =
+ Stream.mapsConcat advanceBlockComment eofBlockComment
+ OutsideBlockComment;
+in
+ fun read {mapping,filename} =
+ let
+ (* Estimating parse error line numbers *)
+
+ val lines = Stream.fromTextFile {filename = filename}
+
+ val {chars,parseErrorLocation} = Parse.initialize {lines = lines}
+ in
+ (let
+ (* The character stream *)
+
+ val (comments,chars) = stripLineComments [] chars
+
+ val chars = Parse.everything Parse.any chars
+
+ val chars = stripBlockComments chars
+
+ (* The declaration stream *)
+
+ val declarations = Stream.toList (parseDeclaration mapping chars)
+
+ val (includes,formulas) = partitionDeclarations declarations
+ in
+ Problem
+ {comments = comments,
+ includes = includes,
+ formulas = formulas}
+ end
+ handle Parse.NoParse => raise Error "parse error")
+ handle Error err =>
+ raise Error ("error in TPTP file \"" ^ filename ^ "\" " ^
+ parseErrorLocation () ^ "\n" ^ err)
+ end;
+end;
+
+local
+ val newline = Stream.singleton "\n";
+
+ fun spacer top = if top then Stream.Nil else newline;
+
+ fun mkComment comment = mkLineComment comment ^ "\n";
+
+ fun mkInclude inc = includeToString inc ^ "\n";
+
+ fun formulaStream _ _ [] = Stream.Nil
+ | formulaStream mapping top (h :: t) =
+ Stream.append
+ (Stream.concatList
+ [spacer top,
+ Stream.singleton (formulaToString mapping h),
+ newline])
+ (fn () => formulaStream mapping false t);
+in
+ fun write {problem,mapping,filename} =
+ let
+ val Problem {comments,includes,formulas} = problem
+
+ val includesTop = null comments
+ val formulasTop = includesTop andalso null includes
+ in
+ Stream.toTextFile
+ {filename = filename}
+ (Stream.concatList
+ [Stream.map mkComment (Stream.fromList comments),
+ spacer includesTop,
+ Stream.map mkInclude (Stream.fromList includes),
+ formulaStream mapping formulasTop formulas])
+ end;
+end;
+
+local
+ fun refute {axioms,conjecture} =
+ let
+ val axioms = map Thm.axiom axioms
+ and conjecture = map Thm.axiom conjecture
+ val problem = {axioms = axioms, conjecture = conjecture}
+ val resolution = Resolution.new Resolution.default problem
+ in
+ case Resolution.loop resolution of
+ Resolution.Contradiction _ => true
+ | Resolution.Satisfiable _ => false
+ end;
+in
+ fun prove filename =
+ let
+ val problem = read filename
+ val problems = map #problem (normalize problem)
+ in
+ List.all refute problems
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* TSTP proofs. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun newName avoid prefix =
+ let
+ fun bump i =
+ let
+ val name = FormulaName (prefix ^ Int.toString i)
+ val i = i + 1
+ in
+ if memberFormulaNameSet name avoid then bump i else (name,i)
+ end
+ in
+ bump
+ end;
+
+ fun lookupClauseSource sources cl =
+ case LiteralSetMap.peek sources cl of
+ SOME src => src
+ | NONE => raise Bug "Tptp.lookupClauseSource";
+
+ fun lookupFormulaName fmNames fm =
+ case FormulaMap.peek fmNames fm of
+ SOME name => name
+ | NONE => raise Bug "Tptp.lookupFormulaName";
+
+ fun lookupClauseName clNames cl =
+ case LiteralSetMap.peek clNames cl of
+ SOME name => name
+ | NONE => raise Bug "Tptp.lookupClauseName";
+
+ fun lookupClauseSourceName sources fmNames cl =
+ case lookupClauseSource sources cl of
+ CnfClauseSource (name,_) => name
+ | FofClauseSource th =>
+ let
+ val (fm,_) = Normalize.destThm th
+ in
+ lookupFormulaName fmNames fm
+ end;
+
+ fun collectProofDeps sources ((_,inf),names_ths) =
+ case inf of
+ Proof.Axiom cl =>
+ let
+ val (names,ths) = names_ths
+ in
+ case lookupClauseSource sources cl of
+ CnfClauseSource (name,_) =>
+ let
+ val names = addFormulaNameSet names name
+ in
+ (names,ths)
+ end
+ | FofClauseSource th =>
+ let
+ val ths = th :: ths
+ in
+ (names,ths)
+ end
+ end
+ | _ => names_ths;
+
+ fun collectNormalizeDeps ((_,inf,_),fofs_defs) =
+ case inf of
+ Normalize.Axiom fm =>
+ let
+ val (fofs,defs) = fofs_defs
+ val fofs = FormulaSet.add fofs fm
+ in
+ (fofs,defs)
+ end
+ | Normalize.Definition n_d =>
+ let
+ val (fofs,defs) = fofs_defs
+ val defs = StringMap.insert defs n_d
+ in
+ (fofs,defs)
+ end
+ | _ => fofs_defs;
+
+ fun collectSubgoalProofDeps subgoalProof (names,fofs,defs) =
+ let
+ val {subgoal,sources,refutation} = subgoalProof
+
+ val names = addListFormulaNameSet names (snd subgoal)
+
+ val proof = Proof.proof refutation
+
+ val (names,ths) =
+ List.foldl (collectProofDeps sources) (names,[]) proof
+
+ val normalization = Normalize.proveThms (rev ths)
+
+ val (fofs,defs) =
+ List.foldl collectNormalizeDeps (fofs,defs) normalization
+
+ val subgoalProof =
+ {subgoal = subgoal,
+ normalization = normalization,
+ sources = sources,
+ proof = proof}
+ in
+ (subgoalProof,(names,fofs,defs))
+ end;
+
+ fun addProblemFormula names fofs (formula,(avoid,formulas,fmNames)) =
+ let
+ val name = nameFormula formula
+
+ val avoid = addFormulaNameSet avoid name
+
+ val (formulas,fmNames) =
+ if memberFormulaNameSet name names then
+ (formula :: formulas, fmNames)
+ else
+ case bodyFormula formula of
+ CnfFormulaBody _ => (formulas,fmNames)
+ | FofFormulaBody fm =>
+ if not (FormulaSet.member fm fofs) then (formulas,fmNames)
+ else (formula :: formulas, FormulaMap.insert fmNames (fm,name))
+ in
+ (avoid,formulas,fmNames)
+ end;
+
+ fun addDefinitionFormula avoid (_,def,(formulas,i,fmNames)) =
+ let
+ val (name,i) = newName avoid "definition_" i
+
+ val role = DefinitionRole
+
+ val body = FofFormulaBody def
+
+ val source = NoFormulaSource
+
+ val formula =
+ Formula
+ {name = name,
+ role = role,
+ body = body,
+ source = source}
+
+ val formulas = formula :: formulas
+
+ val fmNames = FormulaMap.insert fmNames (def,name)
+ in
+ (formulas,i,fmNames)
+ end;
+
+ fun addSubgoalFormula avoid subgoalProof (formulas,i) =
+ let
+ val {subgoal,normalization,sources,proof} = subgoalProof
+
+ val (fm,pars) = subgoal
+
+ val (name,i) = newName avoid "subgoal_" i
+
+ val number = i - 1
+
+ val (subgoal,formulas) =
+ if null pars then (NONE,formulas)
+ else
+ let
+ val role = PlainRole
+
+ val body = FofFormulaBody fm
+
+ val source =
+ StripFormulaSource
+ {inference = "strip",
+ parents = pars}
+
+ val formula =
+ Formula
+ {name = name,
+ role = role,
+ body = body,
+ source = source}
+ in
+ (SOME (name,fm), formula :: formulas)
+ end
+
+ val subgoalProof =
+ {number = number,
+ subgoal = subgoal,
+ normalization = normalization,
+ sources = sources,
+ proof = proof}
+ in
+ (subgoalProof,(formulas,i))
+ end;
+
+ fun mkNormalizeFormulaSource fmNames inference fms =
+ let
+ val fms =
+ case inference of
+ Normalize.Axiom fm => fm :: fms
+ | Normalize.Definition (_,fm) => fm :: fms
+ | _ => fms
+
+ val parents = map (lookupFormulaName fmNames) fms
+ in
+ NormalizeFormulaSource
+ {inference = inference,
+ parents = parents}
+ end;
+
+ fun mkProofFormulaSource sources fmNames clNames inference =
+ let
+ val parents =
+ case inference of
+ Proof.Axiom cl => [lookupClauseSourceName sources fmNames cl]
+ | _ =>
+ let
+ val cls = map Thm.clause (Proof.parents inference)
+ in
+ map (lookupClauseName clNames) cls
+ end
+ in
+ ProofFormulaSource
+ {inference = inference,
+ parents = parents}
+ end;
+
+ fun addNormalizeFormula avoid prefix ((fm,inf,fms),acc) =
+ let
+ val (formulas,i,fmNames) = acc
+
+ val (name,i) = newName avoid prefix i
+
+ val role = PlainRole
+
+ val body = FofFormulaBody fm
+
+ val source = mkNormalizeFormulaSource fmNames inf fms
+
+ val formula =
+ Formula
+ {name = name,
+ role = role,
+ body = body,
+ source = source}
+
+ val formulas = formula :: formulas
+
+ val fmNames = FormulaMap.insert fmNames (fm,name)
+ in
+ (formulas,i,fmNames)
+ end;
+
+ fun isSameClause sources formulas inf =
+ case inf of
+ Proof.Axiom cl =>
+ (case lookupClauseSource sources cl of
+ CnfClauseSource (name,lits) =>
+ if List.exists isBooleanLiteral lits then NONE
+ else SOME name
+ | _ => NONE)
+ | _ => NONE;
+
+ fun addProofFormula avoid sources fmNames prefix ((th,inf),acc) =
+ let
+ val (formulas,i,clNames) = acc
+
+ val cl = Thm.clause th
+ in
+ case isSameClause sources formulas inf of
+ SOME name =>
+ let
+ val clNames = LiteralSetMap.insert clNames (cl,name)
+ in
+ (formulas,i,clNames)
+ end
+ | NONE =>
+ let
+ val (name,i) = newName avoid prefix i
+
+ val role = PlainRole
+
+ val body = CnfFormulaBody (clauseFromLiteralSet cl)
+
+ val source = mkProofFormulaSource sources fmNames clNames inf
+
+ val formula =
+ Formula
+ {name = name,
+ role = role,
+ body = body,
+ source = source}
+
+ val formulas = formula :: formulas
+
+ val clNames = LiteralSetMap.insert clNames (cl,name)
+ in
+ (formulas,i,clNames)
+ end
+ end;
+
+ fun addSubgoalProofFormulas avoid fmNames (subgoalProof,formulas) =
+ let
+ val {number,subgoal,normalization,sources,proof} = subgoalProof
+
+ val (formulas,fmNames) =
+ case subgoal of
+ NONE => (formulas,fmNames)
+ | SOME (name,fm) =>
+ let
+ val source =
+ StripFormulaSource
+ {inference = "negate",
+ parents = [name]}
+
+ val prefix = "negate_" ^ Int.toString number ^ "_"
+
+ val (name,_) = newName avoid prefix 0
+
+ val role = PlainRole
+
+ val fm = Formula.Not fm
+
+ val body = FofFormulaBody fm
+
+ val formula =
+ Formula
+ {name = name,
+ role = role,
+ body = body,
+ source = source}
+
+ val formulas = formula :: formulas
+
+ val fmNames = FormulaMap.insert fmNames (fm,name)
+ in
+ (formulas,fmNames)
+ end
+
+ val prefix = "normalize_" ^ Int.toString number ^ "_"
+ val (formulas,_,fmNames) =
+ List.foldl (addNormalizeFormula avoid prefix)
+ (formulas,0,fmNames) normalization
+
+ val prefix = "refute_" ^ Int.toString number ^ "_"
+ val clNames : formulaName LiteralSetMap.map = LiteralSetMap.new ()
+ val (formulas,_,_) =
+ List.foldl (addProofFormula avoid sources fmNames prefix)
+ (formulas,0,clNames) proof
+ in
+ formulas
+ end;
+in
+ fun fromProof {problem,proofs} =
+ let
+ val names = emptyFormulaNameSet
+ and fofs = FormulaSet.empty
+ and defs : Formula.formula StringMap.map = StringMap.new ()
+
+ val (proofs,(names,fofs,defs)) =
+ maps collectSubgoalProofDeps proofs (names,fofs,defs)
+
+ val Problem {formulas,...} = problem
+
+ val fmNames : formulaName FormulaMap.map = FormulaMap.new ()
+ val (avoid,formulas,fmNames) =
+ List.foldl (addProblemFormula names fofs)
+ (emptyFormulaNameSet,[],fmNames) formulas
+
+ val (formulas,_,fmNames) =
+ StringMap.foldl (addDefinitionFormula avoid)
+ (formulas,0,fmNames) defs
+
+ val (proofs,(formulas,_)) =
+ maps (addSubgoalFormula avoid) proofs (formulas,0)
+
+ val formulas =
+ List.foldl (addSubgoalProofFormulas avoid fmNames) formulas proofs
+ in
+ rev formulas
+ end
+(*MetisDebug
+ handle Error err => raise Bug ("Tptp.fromProof: shouldn't fail:\n" ^ err);
+*)
+end;
+
+end