-
Notifications
You must be signed in to change notification settings - Fork 18
/
sequentProofToTptp.scala
52 lines (40 loc) · 1.57 KB
/
sequentProofToTptp.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
package gapt.formats.tptp
import gapt.expr._
import gapt.expr.formula.Formula
import gapt.expr.formula.fol.FOLConst
import gapt.expr.formula.hol.universalClosure
import gapt.proofs.{ Sequent, SequentProof }
import scala.collection.mutable
class sequentProofToTptp[Proof <: SequentProof[Formula, Proof]] {
def line( label: String, role: FormulaRole, inf: Proof, annotations: Seq[GeneralTerm] ): TptpInput =
AnnotatedFormula( "fof", label, role, universalClosure( inf.conclusion.toFormula ), annotations )
private def convertInference(
labelMap: collection.Map[Proof, String],
inf: Proof ): TptpInput = {
val label = labelMap( inf )
inf match {
case p =>
val inferenceName = p.longName.flatMap {
case c if c.isUpper => "_" + c.toLower
case c => c.toString
}.dropWhile( _ == '_' ).stripSuffix( "_rule" )
val parents = p.immediateSubProofs.map( labelMap )
line( label, "plain", inf,
Seq( TptpTerm( "inference", FOLConst( inferenceName ),
GeneralList(), GeneralList( parents.map( FOLConst( _ ) ) ) ) ) )
}
}
def apply( proof: Proof ): TptpFile = {
val inputs = Seq.newBuilder[TptpInput]
val labelMap = mutable.Map[Proof, String]()
for ( ( p, i ) <- proof.dagLike.postOrder.zipWithIndex ) {
labelMap( p ) = s"p$i"
inputs += convertInference( labelMap, p )
}
TptpFile( inputs.result() )
}
}
object sequentProofToTptp {
def apply[Proof <: SequentProof[Formula, Proof]]( p: Proof ): TptpFile =
new sequentProofToTptp().apply( p )
}