diff --git a/CHANGES.md b/CHANGES.md index b054dda822a4658eef9e4db182518cff57837104..07a5d71d60106da42b8cc11c0c84c1d26dd9f584 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,11 +1,14 @@ # Change List ## 2023-12-06 +Re-added discovery of formulas which could not be substituted for error reporting to `Substitution.ApplyRules` + Upgrade to Scala 3.3.1 - the `Proof` class has been temporarily unsealed, till [lampepfl/dotty#19031](https://github.com/lampepfl/dotty/issues/19031) / [epfl-lara/lisa#190](https://github.com/epfl-lara/lisa/issues/190) is fixed - minor fixes to address compilation errors, mostly involving explicitly specifying types or implicits in some places. + ## 2023-12-02 Creation of the present Change Liste, going back to October 2023 diff --git a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala index c5fd1620389878222dead2a862083d6c1cfb9290..fc7a0e2f52cd6b96401f4c6ea18eb74bcc7a000b 100644 --- a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala +++ b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala @@ -36,8 +36,6 @@ object Substitution { def apply(using lib: lisa.prooflib.Library, proof: lib.Proof)(substitutions: (proof.Fact | F.Formula | lib.JUSTIFICATION)*)( premise: proof.Fact )(bot: F.Sequent): proof.ProofTacticJudgement = { - // lazy val substitutionsK = substitutions.map() - // figure out instantiations for rules // takes a premise val premiseSequent: F.Sequent = proof.getSequent(premise) @@ -156,8 +154,30 @@ object Substitution { takenFormulaVars ) - lazy val violatingFormulaLeft: Option[Formula] = Some(top) // TODO - lazy val violatingFormulaRight: Option[Formula] = Some(top) // TODO + lazy val rightPairs = premiseSequent.right zip premiseSequent.right.map(x => bot.right.find(y => UnificationUtils.getContextFormula( + x, + y, + freeEqualities, + freeIffs, + confinedEqualities, + takenTermVars, + confinedIffs, + takenFormulaVars + ).isDefined)) + + lazy val leftPairs = filteredPrem zip filteredPrem.map(x => filteredBot.find(y => UnificationUtils.getContextFormula( + x, + y, + freeEqualities, + freeIffs, + confinedEqualities, + takenTermVars, + confinedIffs, + takenFormulaVars + ).isDefined)) + + lazy val violatingFormulaLeft = leftPairs.find(_._2.isEmpty) + lazy val violatingFormulaRight = rightPairs.find(_._2.isEmpty) if (leftContextsOpt.isEmpty) proof.InvalidProofTactic(s"Could not rewrite LHS of premise into conclusion with given substitutions.\nViolating Formula: ${violatingFormulaLeft.get}")