-
Notifications
You must be signed in to change notification settings - Fork 18
/
TptpToString.scala
117 lines (105 loc) · 5.15 KB
/
TptpToString.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
package gapt.formats.tptp
import gapt.expr._
import gapt.expr.formula.All
import gapt.expr.formula.And
import gapt.expr.formula.Bottom
import gapt.expr.formula.Eq
import gapt.expr.formula.Ex
import gapt.expr.formula.Formula
import gapt.expr.formula.Iff
import gapt.expr.formula.Imp
import gapt.expr.formula.MonoidalBinaryPropConnectiveHelper
import gapt.expr.formula.Neg
import gapt.expr.formula.Or
import gapt.expr.formula.Top
import gapt.expr.subst.Substitution
import gapt.expr.ty.TBase
import gapt.expr.util.freeVariables
import gapt.expr.util.rename
object TptpToString {
def tptpInput( input: TptpInput ): String = input match {
case AnnotatedFormula( language, name, role, formula, annots ) =>
s"${atomic_word( language )}(${atomic_word( name )}, $role, ${expression( formula )}${annotations( annots )}).\n"
case IncludeDirective( fileName, None ) => s"include(${single_quoted( fileName )}).\n"
case IncludeDirective( fileName, Some( seq ) ) =>
//TODO: check what seq actually contains
val args = seq.map( single_quoted ).mkString( "[", ", ", "]" )
s"include(${single_quoted( fileName )}, ${args}).\n"
}
def annotations( annots: Seq[Expr] ): String = annots.map( expression ).map( ", " + _ ).mkString
def expression( expr: Expr ): String = expression( expr, prio.max )
private object prio {
val term = 0
val infix_formula = 2
val unitary_formula = 4
val binary_formula = 6
val max = binary_formula + 2
}
private def parenIf( enclosingPrio: Int, currentPrio: Int, inside: String ) =
if ( enclosingPrio <= currentPrio ) s"($inside)" else inside
private def binExpr( a: Expr, b: Expr, p: Int, newPrio: Int, op: String ) =
parenIf( p, newPrio, s"${expression( a, newPrio )} $op ${expression( b, newPrio )}" )
private def binAssocExpr( expr: Expr, p: Int, op: String, conn: MonoidalBinaryPropConnectiveHelper ) = {
def leftAssocJuncts( e: Expr ): Seq[Expr] = e match {
case conn( a, b ) => leftAssocJuncts( a ) :+ b
case _ => Seq( e )
}
parenIf( p, prio.binary_formula, leftAssocJuncts( expr ).map( expression( _, prio.binary_formula ) ).mkString( s" $op " ) )
}
private def quant( vs: Seq[Var], bd: Expr, p: Int, q: String ) = {
val ( vs_, bd_ ) = renameVars( vs, bd )
parenIf( p, prio.unitary_formula, s"$q[${vs_ map expression mkString ","}]: ${expression( bd_, prio.unitary_formula + 1 )}" )
}
private def expression( expr: Expr, p: Int ): String = expr match {
case GeneralList( elements @ _* ) =>
s"[${elements map expression mkString ", "}]"
case GeneralColon( a, b ) =>
s"${expression( a, prio.term )}:${expression( b, prio.term )}"
case Iff( a, b ) =>
binExpr( a, b, p, prio.binary_formula, "<=>" )
case Top() => "$true"
case Bottom() => "$false"
case Const( c, _, _ ) => atomic_word( c )
case Var( name, _ ) => variable( name )
case Neg( Eq( a, b ) ) => binExpr( a, b, p, prio.infix_formula, "!=" )
case Neg( f ) => parenIf( p, prio.unitary_formula, s"~ ${expression( f, prio.unitary_formula + 1 )}" )
case Eq( a, b ) => binExpr( a, b, p, prio.infix_formula, "=" )
case And( _, _ ) => binAssocExpr( expr, p, "&", And )
case Or( a, b ) => binAssocExpr( expr, p, "|", Or )
case Imp( a, b ) => binExpr( a, b, p, prio.binary_formula, "=>" )
case All.Block( vs, bd ) if vs.nonEmpty => quant( vs, bd, p, "!" )
case Ex.Block( vs, bd ) if vs.nonEmpty => quant( vs, bd, p, "?" )
case Apps( Const( hd, _, _ ), args ) if expr.ty.isInstanceOf[TBase] =>
s"${atomic_word( hd )}(${args map expression mkString ", "})"
case App( a, b ) => binExpr( a, b, p, prio.term, s"@" )
}
def renameVarName( name: String ) =
name.toUpperCase match {
case upper @ upperWordRegex() => upper
case _ =>
"X" + name.toUpperCase match {
case xupper @ upperWordRegex() => xupper
case _ => "X"
}
}
def renameVar( v: Var ) = Var( renameVarName( v.name ), v.ty )
def renameVars( vars: Seq[Var], body: Expr ): ( Seq[Var], Expr ) = {
val nameGen = rename.awayFrom( freeVariables( body ) -- vars )
val newVars = for ( fv <- vars ) yield nameGen.fresh( renameVar( fv ) )
( newVars, Substitution( vars zip newVars )( body ) )
}
def renameVars( f: Formula ): Formula =
renameVars( freeVariables( f ).toSeq, f )._2.asInstanceOf[Formula]
private val lowerWordRegex = "[a-z][A-Za-z0-9_]*".r
private val definedOrSystemWord = "[$][$]?[A-Za-z0-9_]*".r
private val singleQuoteAllowedRegex = """[\]-~ -&(-\[\\']+""".r
def atomic_word( name: String ): String = name match {
case lowerWordRegex() => name
case definedOrSystemWord() => name
case _ => single_quoted( name )
}
def single_quoted( name: String ): String =
"'" + name.replace( "\\", "\\\\" ).replace( "'", "\\'" ) + "'"
private val upperWordRegex = "[A-Z][A-Za-z0-9_]*".r
def variable( name: String ): String = name
}