add Egg.scala

lisa-sets2/src/main/scala/lisa/automation/atp/Egg.scala

@@ -0,0 +1,123 @@
+package lisa.automation.atp
+import lisa.utils.fol.FOL as F
+import lisa.utils.prooflib.Library
+import lisa.utils.prooflib.OutputManager
+import lisa.utils.prooflib.ProofTacticLib.*
+import lisa.utils.K
+import lisa.utils.tptp.*
+
+import java.io.*
+import scala.io.Source
+import scala.util.Failure
+import scala.util.Success
+import scala.util.Try
+
+import ProofParser.*
+import KernelParser.*
+import sys.process._
+
+/**
+  * Goéland is an automated theorem prover. This tactic calls the Goéland prover to solve the current sequent.
+  * Goéland is only available on Linux yet, but proofs generated by Goéland should be kept in the library for future use.
+  * To ensure that proofs are published and can be replayed in any system, proofs from an ATPcan only be generated in draft mode.
+  * When in non-draft mode, the proof file should be given as an argument to the tactic (the exact file is provided by Lisa upon run without draft mode).
+  */
+object Egg extends ProofTactic with ProofSequentTactic {
+  private var i : Int = 0
+
+  val goelandExec = "../bin/egg-sc-tptp"
+
+  class OsNotSupportedException(msg: String) extends Exception(msg)
+
+  val foldername = "egg/"
+
+  /**
+    * Fetch a proof of a sequent that was previously proven by Goéland.
+    * The file must be in SC-TPTP format.
+    */
+  def apply(using lib: Library, proof: lib.Proof)(file:String)(bot: F.Sequent): proof.ProofTacticJudgement = {
+    val outputname = proof.owningTheorem.fullName+"_sol"
+    try {
+      val scproof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+      proof.ValidProofTactic(bot, scproof.steps, Seq())
+    } catch {
+      case e: FileNotFoundException => 
+        throw FileNotFoundException("The file "+foldername+outputname+".p was not found. To produce a proof, use `by Egg`. ")
+      case e => throw e
+    }
+  }
+
+
+  /**
+    * Solve a sequent using the Goéland automated theorem prover.
+    * At the moment, this option is only available on Linux system.
+    * The proof is generated and saved in a file in the `Egg` folder.
+    */
+  def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
+    from(using lib, proof)()(bot)
+  }
+
+  def from(using lib: Library, proof: lib.Proof)(premises: proof.Fact*)(bot: F.Sequent) = {
+    val axioms = premises.map(proof.getSequent)
+    solve(axioms, bot, proof.owningTheorem.fullName, lib.isDraft) match {
+      case Success(value) => proof.ValidProofTactic(bot, value.steps, premises)
+      case Failure(e) => e match
+        case e: FileNotFoundException  => throw new Exception("For compatibility reasons, external provers can't be called in non-draft mode" +
+          " unless all proofs have already been generated and be available in static files. You can enable draft mode by adding `draft()` at the top of your working file.")
+        case e: OsNotSupportedException => throw e
+        case e => 
+          throw e
+    }
+  }
+
+  inline def solve(axioms: Seq[F.Sequent], sequent: F.Sequent, source: String, generateProofs : Boolean): Try[K.SCProof] = 
+    solveK(axioms.map(_.underlying), sequent.underlying, source, generateProofs)
+
+
+  /**
+    * Solve a sequent using the Goéland automated theorem prover, and return the kernel proof.
+    * At the moment, this option is only available on Linux systems.
+    */
+  def solveK(using line: sourcecode.Line, file: sourcecode.File)(axioms: Seq[K.Sequent], sequent: K.Sequent, source:String, generateProofs : Boolean): Try[K.SCProof] = {
+    val filename = source
+    val outputname = source+"_sol"
+    val directory = File(foldername)
+    if (directory != null) && !directory.exists() then directory.mkdirs()
+
+    val freevars = (sequent.left.flatMap(_.freeVariables) ++ sequent.right.flatMap(_.freeVariables) ).toSet.map(x => x -> K.Variable(K.Identifier("X"+x.id.name, x.id.no), x.sort) ).toMap
+
+    val backMap = freevars.map{
+      case (x: K.Variable, xx: K.Variable) => xx -> x
+    }
+    val r = problemToFile(foldername, filename, "question"+i, axioms, sequent, source)
+    i += 1
+
+    if generateProofs then
+      val OS = System.getProperty("os.name")
+      if OS.contains("nix") || OS.contains("nux") || OS.contains("aix") then
+        val ret = s"chmod u+x \"$goelandExec\"".!
+        val cmd = (s"$goelandExec $foldername$filename.p $foldername$outputname.p") // TODO
+        val res = try {
+          cmd.!!
+        } catch {
+          case e: Exception => 
+            throw e
+        }
+        val proof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+        Success(proof)
+      else if OS.contains("win") then
+        Failure(OsNotSupportedException("The Egg automated theorem prover is not yet supported on Windows."))
+      else 
+        Failure(OsNotSupportedException("The Egg automated theorem prover is only supported on Linux for now."))
+    else 
+      if File(foldername+outputname+".p").exists() then
+        val proof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+        println(OutputManager.WARNING(s"WARNING: in ${file.value}:$line, For compatibility reasons, replace `by Egg` with `by Egg(\"$foldername$outputname\")`."))
+        Success(proof)
+
+      else Failure(Exception("For compatibility reasons, external provers can't be called in non-draft mode. You can enable draft mode by adding `draft()` at the top of your working file."))
+
+
+  }
+
+}