-
Notifications
You must be signed in to change notification settings - Fork 18
/
FileParser.scala
41 lines (32 loc) · 1.29 KB
/
FileParser.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
package gapt.prooftool
import gapt.formats.ivy.IvyParser
import gapt.formats.ivy.conversion.IvyToResolution
import gapt.expr._
import gapt.formats.llk.{ ExtendedProofDatabase, loadLLK }
import gapt.proofs.resolution.ResolutionProof
import ammonite.ops._
class FileParser( main: ProofToolViewer[_] ) {
def ivyFileReader( path: String ): Unit = {
val ivy = IvyToResolution( IvyParser( FilePath( path ) ) )
resProofs = ( "ivy_proof", ivy ) :: Nil
}
def llkFileReader( filename: String ): Unit = {
resProofs = Nil
proofdb = loadLLK( FilePath( filename ) )
}
def parseFile( path: String ): Unit = {
val dnLine = sys.props( "line.separator" ) + sys.props( "line.separator" )
try {
if ( path.endsWith( ".llk" ) ) llkFileReader( path )
else if ( path.endsWith( ".ivy" ) ) ivyFileReader( path )
else main.warningMessage( "Can not recognize file extension: " + path.substring( path.lastIndexOf( "." ) ) )
} catch {
case err: Throwable =>
main.errorMessage( "Could not load file: " + path + "!" + dnLine + main.getExceptionString( err ) )
}
}
def getProofs = proofdb.proofs
def getResolutionProofs = resProofs
private var proofdb = ExtendedProofDatabase( Map(), Map(), Map() )
private var resProofs: List[( String, ResolutionProof )] = Nil
}