Merge branch 'master' of https://github.com/LS-Lab/KeYmaeraX

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/bellerophon/BellerophonSyntax.scala

@@ -278,6 +278,20 @@ abstract case class BuiltInRightTactic(name: String) extends PositionalTactic {
   override def prettyString = name
 }
 
+
+abstract case class DependentTwoPositionTactic(name: String) extends BelleExpr {
+  override def prettyString: String = s"UnappliedTwoPositionTactic of name ${name}" //@todo
+
+  def computeExpr(p1: Position, p2: Position): DependentTactic
+
+  def apply(p1: Position, p2: Position) = AppliedDependentTwoPositionTactic(this, p1, p2)
+}
+
+case class AppliedDependentTwoPositionTactic(t: DependentTwoPositionTactic, p1: Position, p2: Position) extends BelleExpr {
+  /** pretty-printed form of this Bellerophon tactic expression */
+  override def prettyString: String = t.prettyString + "(" + p1 + "," + p2 + ")"
+}
+
 /**
   * Stores the position tactic and position at which the tactic was applied.
   * Useful for storing execution traces.
@@ -345,18 +359,18 @@ abstract case class BuiltInTwoPositionTactic(name: String) extends BelleExpr {
   def computeResult(provable : Provable, posOne: Position, posTwo: Position) : Provable
 
   /** Returns an explicit representation of the application of this tactic to the provided positions. */
-  final def apply(posOne: Position, posTwo: Position): AppliedTwoPositionTactic = AppliedTwoPositionTactic(this, posOne, posTwo)
+  final def apply(posOne: Position, posTwo: Position): AppliedBuiltinTwoPositionTactic = AppliedBuiltinTwoPositionTactic(this, posOne, posTwo)
   /** Returns an explicit representation of the application of this tactic to the provided positions.
     *
     * @note Convenience wrapper
     */
-  final def apply(posOne: Int, posTwo: Int): AppliedTwoPositionTactic = apply(Position(posOne), Position(posTwo))
+  final def apply(posOne: Int, posTwo: Int): AppliedBuiltinTwoPositionTactic = apply(Position(posOne), Position(posTwo))
 
   override def prettyString = name
 }
 
 /** Motivation is similar to [[AppliedPositionTactic]], but for [[BuiltInTwoPositionTactic]] */
-case class AppliedTwoPositionTactic(positionTactic: BuiltInTwoPositionTactic, posOne: Position, posTwo: Position) extends BelleExpr {
+case class AppliedBuiltinTwoPositionTactic(positionTactic: BuiltInTwoPositionTactic, posOne: Position, posTwo: Position) extends BelleExpr {
   final def computeResult(provable: Provable) : Provable = try {
     positionTactic.computeResult(provable, posOne, posTwo)
   } catch {

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/bellerophon/PositionLocator.scala

@@ -5,7 +5,7 @@
 
 package edu.cmu.cs.ls.keymaerax.bellerophon
 
-import edu.cmu.cs.ls.keymaerax.core.Formula
+import edu.cmu.cs.ls.keymaerax.core.{Formula, Provable}
 
 ////////////////////////////////////////////////////////////////////////////////////////////////////
 // Locate Positions
@@ -16,6 +16,8 @@ import edu.cmu.cs.ls.keymaerax.core.Formula
  */
 sealed trait PositionLocator {
   def prettyString: String
+
+  def toPosition(p: Provable): Position = ??? //@todo Surely this already exists?!
 }
 
 /** Locates the formula at the specified fixed position. Can optionally specify the expected formula or expected shape of formula at that position as contract. */

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/bellerophon/ReflectiveExpressionBuilder.scala

@@ -34,15 +34,17 @@ object ReflectiveExpressionBuilder {
       // someone is going to plug in the arguments later
       case (expr:BelleExpr, Nil, _) => expr
       case (expr:BelleExpr with PositionalTactic , arg::Nil, 1) => AppliedPositionTactic(expr, arg)
+      case (expr:DependentTwoPositionTactic, Fixed(arg1: Position, _, _) :: Fixed(arg2: Position, _, _) :: Nil, 2) =>
+        AppliedDependentTwoPositionTactic(expr, arg1, arg2)
       case (expr:DependentPositionTactic, arg::Nil, 1) => new AppliedDependentPositionTactic(expr, arg)
       case (expr:BuiltInTwoPositionTactic, Fixed(arg1: Position, _, _)::Fixed(arg2: Position, _, _)::Nil, 2) =>
-        AppliedTwoPositionTactic(expr, arg1, arg2)
+        AppliedBuiltinTwoPositionTactic(expr, arg1, arg2)
       case (expr: (Position => DependentPositionTactic), Fixed(arg1: Position, _, _)::arg2::Nil, 2) =>
         new AppliedDependentPositionTactic(expr(arg1), arg2)
       case (expr: ((Position, Position) => BelleExpr), Fixed(arg1: Position, _, _)::Fixed(arg2: Position, _, _)::Nil, 2) => expr(arg1, arg2)
       case (expr, pArgs, num) =>
         if (pArgs.length > num) {
-          throw new ReflectiveExpressionBuilderExn("Expected either " + num + " or 0 position arguments, got " + pArgs.length)
+          throw new ReflectiveExpressionBuilderExn("Expected either " + num + s" or 0 position arguments for ${expr.getClass} (${expr}), got " + pArgs.length)
         } else {
           throw new ReflectiveExpressionBuilderExn("Tactics with " + num + " arguments cannot have type " + expr.getClass.getSimpleName)
         }

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/bellerophon/RenUSubst.scala

@@ -77,6 +77,9 @@ object RenUSubst {
   * @see [[edu.cmu.cs.ls.keymaerax.core.USubst]]
   */
 sealed abstract class RenUSubst(private[bellerophon] val subsDefsInput: immutable.Seq[(Expression,Expression)]) extends (Expression => Expression) {
+  /** Returns true if there is no specified substitution. */
+  def isEmpty = subsDefsInput.isEmpty
+
   /** automatically filter out identity substitution no-ops */
   protected final val rens: immutable.Seq[(Variable,Variable)] = RenUSubst.renamingPartOnly(subsDefsInput)
   protected final val subsDefs: immutable.Seq[SubstitutionPair] = try {subsDefsInput.filterNot(sp => sp._1.isInstanceOf[Variable]).
@@ -157,7 +160,6 @@ sealed abstract class RenUSubst(private[bellerophon] val subsDefsInput: immutabl
         throw new SubstitutionClashException(toString, "undef", "undef", s.toString, "undef", ex.getMessage).initCause(ex)
     }
   }
-
 }
 
 /**

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/bellerophon/SequentialInterpreter.scala

@@ -76,7 +76,7 @@ case class SequentialInterpreter(listeners : Seq[IOListener] = Seq()) extends In
             case e: BelleError => throw e.inContext(positionTactic + " at " + pos, pr.prettyString)
           }
         }
-        case positionTactic@AppliedTwoPositionTactic(_, posOne, posTwo) => v match {
+        case positionTactic@AppliedBuiltinTwoPositionTactic(_, posOne, posTwo) => v match {
           case BelleProvable(pr, _) => try {
             BelleProvable(positionTactic.computeResult(pr))
           } catch {
@@ -270,6 +270,14 @@ case class SequentialInterpreter(listeners : Seq[IOListener] = Seq()) extends In
 
           apply(unification._2(unification._1.asInstanceOf[RenUSubst]), v)
         }
+
+        case AppliedDependentTwoPositionTactic(t, p1, p2) => {
+          val provable = v match {
+            case BelleProvable(p,_) => p
+            case _ => throw new BelleError("two position tactics can only be run on provable values.")
+          }
+          apply(t.computeExpr(p1, p2).computeExpr(provable), v)
+        }
       }
       listeners.foreach(l => l.end(v, expr, Left(result)))
       result

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/bellerophon/UIIndex.scala

@@ -11,6 +11,8 @@ import edu.cmu.cs.ls.keymaerax.btactics.ExpressionTraversal.{ExpressionTraversal
 import edu.cmu.cs.ls.keymaerax.btactics.{DerivationInfo, ExpressionTraversal}
 import edu.cmu.cs.ls.keymaerax.core._
 
+import scala.annotation.tailrec
+
 /**
   * User-Interface Axiom/Tactic Index: Indexing data structure for all canonically applicable (derived) axioms/rules/tactics in User-Interface.
   * @author aplatzer
@@ -206,13 +208,22 @@ object UIIndex {
       case (p1: AntePosition, p2: SuccPosition, Some(e1), Some(e2)) if p1.isTopLevel &&  p2.isTopLevel && e1 == e2 => "closeId" :: Nil
       case (p1: AntePosition, p2: SuccPosition, Some(e1), Some(e2)) if p1.isTopLevel && !p2.isTopLevel && e1 == e2 => /*@todo "knownR" ::*/ Nil
       case (_, _, Some(Equal(_, _)), _) => "L2R" :: Nil
+      case (_: AntePosition, _, Some(fa: Forall), Some(_:Formula)) if(bodyIsEquiv(fa)) => "equivRewriting" :: Nil
+      case (_: AntePosition, _, Some(_: Equiv), Some(_: Formula)) => "instantiatedEquivRewriting" :: Nil //@note for applying function definitions.
       case (_, _: AntePosition, Some(_: Term), Some(_: Forall)) => /*@todo "all instantiate pos" ::*/ Nil
       case (_, _: SuccPosition, Some(_: Term), Some(_: Exists)) => /*@todo "exists instantiate pos" ::*/ Nil
       case _ => Nil
       //@todo more drag-and-drop support
     }
   }
 
+  @tailrec
+  private def bodyIsEquiv(x: Forall): Boolean = x.child match {
+    case Forall(_, child:Forall) => bodyIsEquiv(child)
+    case Equiv(_,_) => true
+    case _ => false
+  }
+
   def comfortOf(stepName: String): Option[String] = stepName match {
     case "diffCut" => Some("diffInvariant")
     case "DIRule" => Some("autoDIRule")

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/AxiomInfo.scala

@@ -541,7 +541,9 @@ object DerivationInfo {
 
     // Proof rule two-position tactics
     new TwoPositionTacticInfo("coHide2", "W", {case () => SequentCalculus.cohide2}),
-//    new TwoPositionTacticInfo("exchangeL", "X", {case () => ProofRuleTactics.exchangeL}),
+    new TwoPositionTacticInfo("equivRewriting", RuleDisplayInfo("equivRewriting", (List("&Gamma;", "∀X p(X) <-> q(X)"), List("p(Z)", "&Delta;")), List((List("&Gamma;", "∀X p(X) <-> q(X)"), List("q(Z)", "&Delta;")))), {case () => PropositionalTactics.equivRewriting}),
+    new TwoPositionTacticInfo("instantiatedEquivRewriting", "instantiatedEquivRewriting", {case () => PropositionalTactics.instantiatedEquivRewriting}),
+    //    new TwoPositionTacticInfo("exchangeL", "X", {case () => ProofRuleTactics.exchangeL}),
 //    new TwoPositionTacticInfo("exchangeR", "X", {case () => ProofRuleTactics.exchangeR}),
     new TwoPositionTacticInfo("closeId",
       RuleDisplayInfo("closeId", (List("&Gamma;", "P"), List("P", "&Delta;")), Nil),

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/DifferentialHelper.scala

@@ -10,6 +10,7 @@ import edu.cmu.cs.ls.keymaerax.core.StaticSemantics._
 import edu.cmu.cs.ls.keymaerax.core.{Number, ODESystem, Term, _}
 
 /**
+  * @todo move to formula tools? Or make this ProgramTools?
   * Created by nfulton on 7/14/16.
   */
 object DifferentialHelper {

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/MiscTactics.scala

@@ -194,6 +194,12 @@ object TacticFactory {
     /** Creates a named tactic */
     def by(t: BelleExpr): BelleExpr = new NamedTactic(name, t)
 
+    def byTactic(t: ((Provable, Position, Position) => BelleExpr)) = new DependentTwoPositionTactic(name) {
+      override def computeExpr(p1: Position, p2: Position): DependentTactic = new DependentTactic("") {
+        override def computeExpr(p: Provable) = t(p, p1, p2)
+      }
+    }
+
     /** Creates a dependent position tactic without inspecting the formula at that position */
     def by(t: (Position => BelleExpr)): DependentPositionTactic = new DependentPositionTactic(name) {
       override def factory(pos: Position): DependentTactic = new DependentTactic(name) {

keymaerax-core/src/main/scala/edu/cmu/cs/ls/keymaerax/btactics/ProofRuleTactics.scala

@@ -23,7 +23,7 @@ object ProofRuleTactics {
    * Throw exception if there is more than one open subgoal on the provable.
    */
   private[btactics] def requireOneSubgoal(provable: Provable) =
-    if(provable.subgoals.length != 1) throw new BelleError("Expected exactly one sequent in Provable")
+    if(provable.subgoals.length != 1) throw new BelleError(s"Expected exactly one sequent in Provable but found ${provable.subgoals.length}")
 
   def applyRule(rule: Rule): BuiltInTactic = new BuiltInTactic("Apply Rule") {
     override def result(provable: Provable): Provable = {