From 3a09eb16f8fbb645e2eedb9bde65d8084034f8b5 Mon Sep 17 00:00:00 2001
From: Sankalp Gambhir <sankalp.gambhir47@gmail.com>
Date: Thu, 7 Dec 2023 10:10:01 +0100
Subject: [PATCH] Readd failed substitution reporting (#198)
* Readd failed substitution reporting
* File Changes
---
CHANGES.md | 3 ++
.../scala/lisa/automation/Substitution.scala | 28 ++++++++++++++++---
2 files changed, 27 insertions(+), 4 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index b054dda8..07a5d71d 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 c5fd1620..fc7a0e2f 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}")
--
GitLab