<commit_before>package qrhl.tactic

import info.hupel.isabelle.pure.Term
import info.hupel.isabelle.{Operation, pure}
import qrhl._
import qrhl.isabelle.Isabelle
import qrhl.logic._

import scala.collection.mutable

object EqualTac {
  def apply(): EqualTac = EqualTac(Nil)
}

import Expression.typ_tight_codec
import Expression.term_tight_codec

case class EqualTac(exclude: List[String]) extends WpBothStyleTac() {
  override def getWP(state: State, left: Statement, right: Statement, post: Expression): (Expression, List[Subgoal]) = {
    val cvars = new mutable.LinkedHashSet[CVariable]()
    val qvars = new mutable.LinkedHashSet[QVariable]()
    val dummy = new mutable.LinkedHashSet[String]()

    val mismatches = new mutable.LinkedHashSet[(Statement,Statement)]()
    val env = state.environment

    // Adds the classical variables in e to cvars
    def collectExpr(e: Expression): Unit = e.caVariables(env,cvars,dummy)

    // For l=C[l1,...,ln], r=C[r1,...,rn] for programs li, ri, adds all (li,ri) to mismatches
    // Also adds all classical/quantum variables in l,r to cvars/qvars
    def collect(l: Statement, r: Statement) : Unit = (l,r) match {
      case (Assign(xl,el), Assign(xr,er)) if xl==xr && el==er =>
        cvars += xl; collectExpr(el)
      case (Sample(xl,el), Sample(xr,er)) if xl==xr && el==er =>
        cvars += xl; el.caVariables(env,cvars,dummy)
      case (Block(ssl @ _*), Block(ssr @ _*)) if ssl.length==ssr.length =>
        for ((sl,sr) <- ssl.zip(ssr))
          collect(sl,sr)
      case (Call(namel, argsl @ _*), Call(namer, argsr @ _*)) if namel==namer && !exclude.contains(namel) =>
        val p = env.programs(namel)
        val (cv,qv,_,_) = p.variablesRecursive
        cvars ++= cv; qvars ++= qv
        assert(argsl.length==argsr.length)
        for ((pl,pr) <- argsl.zip(argsr))
          collect(pl,pr)
      case (While(el,bodyl), While(er,bodyr)) if el==er =>
        collectExpr(el); collect(bodyl,bodyr)
      case (IfThenElse(el,p1l,p2l), IfThenElse(er,p1r,p2r)) if el==er =>
        collectExpr(el); collect(p1l,p1r); collect(p2l,p2r)
      case (QInit(vs1,e1),QInit(vs2,e2)) if vs1==vs2 && e1==e2 =>
        qvars ++= vs1; collectExpr(e1)
      case (Measurement(vl,vsl,el),Measurement(vr,vsr,er)) if vl==vr && vsl==vsr && el==er =>
        cvars += vl; collectExpr(el); qvars ++= vsl
      case (QApply(vsl,el), QApply(vsr,er)) if vsl==vsr && el==er =>
        qvars ++= vsl; collectExpr(el)
      case lr => mismatches.add(lr)
    }

    collect(left,right)
    // For left=C[l1,...,ln], right=C[r1,...,rn] for programs li, ri, mismatches contains all (li,ri) (in order but without duplicates)
    // And cvars/qvars contains all classical/quantum variables in left,right.

    val cvarsIdx1 = cvars.toList.map(_.index1)
    val cvarsIdx2 = cvars.toList.map(_.index2)
    val qvarsIdx1 = qvars.toList.map(_.index1)
    val qvarsIdx2 = qvars.toList.map(_.index2)

    // Computes wp and colocality, see QRHL.callWp in Isabelle/ML sources
    val (wp, colocality) = state.isabelle.isabelle.invoke(callWpOp,
      ((cvarsIdx1.map(_.valueTerm), cvarsIdx2.map(_.valueTerm),
        qvarsIdx1.map(_.variableTerm)), (qvarsIdx2.map(_.variableTerm),
        post.isabelleTerm, state.isabelle.contextId)))

    if (mismatches.nonEmpty) {
      println("*** WARNING: equal tactic with mismatches is not proven or carefully thought through yet! ***")
    }

    val mismatchGoals = mismatches.toList.map {
      case (l,r) => QRHLSubgoal(l.toBlock,r.toBlock,wp,wp,Nil)
    }
<commit_msg>Removed obsolete warning that equal-tactic is not proven<commit_after>package qrhl.tactic

import info.hupel.isabelle.pure.Term
import info.hupel.isabelle.{Operation, pure}
import qrhl._
import qrhl.isabelle.Isabelle
import qrhl.logic._

import scala.collection.mutable

object EqualTac {
  def apply(): EqualTac = EqualTac(Nil)
}

import Expression.typ_tight_codec
import Expression.term_tight_codec

case class EqualTac(exclude: List[String]) extends WpBothStyleTac() {
  override def getWP(state: State, left: Statement, right: Statement, post: Expression): (Expression, List[Subgoal]) = {
    val cvars = new mutable.LinkedHashSet[CVariable]()
    val qvars = new mutable.LinkedHashSet[QVariable]()
    val dummy = new mutable.LinkedHashSet[String]()

    val mismatches = new mutable.LinkedHashSet[(Statement,Statement)]()
    val env = state.environment

    // Adds the classical variables in e to cvars
    def collectExpr(e: Expression): Unit = e.caVariables(env,cvars,dummy)

    // For l=C[l1,...,ln], r=C[r1,...,rn] for programs li, ri, adds all (li,ri) to mismatches
    // Also adds all classical/quantum variables in l,r to cvars/qvars
    def collect(l: Statement, r: Statement) : Unit = (l,r) match {
      case (Assign(xl,el), Assign(xr,er)) if xl==xr && el==er =>
        cvars += xl; collectExpr(el)
      case (Sample(xl,el), Sample(xr,er)) if xl==xr && el==er =>
        cvars += xl; el.caVariables(env,cvars,dummy)
      case (Block(ssl @ _*), Block(ssr @ _*)) if ssl.length==ssr.length =>
        for ((sl,sr) <- ssl.zip(ssr))
          collect(sl,sr)
      case (Call(namel, argsl @ _*), Call(namer, argsr @ _*)) if namel==namer && !exclude.contains(namel) =>
        val p = env.programs(namel)
        val (cv,qv,_,_) = p.variablesRecursive
        cvars ++= cv; qvars ++= qv
        assert(argsl.length==argsr.length)
        for ((pl,pr) <- argsl.zip(argsr))
          collect(pl,pr)
      case (While(el,bodyl), While(er,bodyr)) if el==er =>
        collectExpr(el); collect(bodyl,bodyr)
      case (IfThenElse(el,p1l,p2l), IfThenElse(er,p1r,p2r)) if el==er =>
        collectExpr(el); collect(p1l,p1r); collect(p2l,p2r)
      case (QInit(vs1,e1),QInit(vs2,e2)) if vs1==vs2 && e1==e2 =>
        qvars ++= vs1; collectExpr(e1)
      case (Measurement(vl,vsl,el),Measurement(vr,vsr,er)) if vl==vr && vsl==vsr && el==er =>
        cvars += vl; collectExpr(el); qvars ++= vsl
      case (QApply(vsl,el), QApply(vsr,er)) if vsl==vsr && el==er =>
        qvars ++= vsl; collectExpr(el)
      case lr => mismatches.add(lr)
    }

    collect(left,right)
    // For left=C[l1,...,ln], right=C[r1,...,rn] for programs li, ri, mismatches contains all (li,ri) (in order but without duplicates)
    // And cvars/qvars contains all classical/quantum variables in left,right.

    val cvarsIdx1 = cvars.toList.map(_.index1)
    val cvarsIdx2 = cvars.toList.map(_.index2)
    val qvarsIdx1 = qvars.toList.map(_.index1)
    val qvarsIdx2 = qvars.toList.map(_.index2)

    // Computes wp and colocality, see QRHL.callWp in Isabelle/ML sources
    val (wp, colocality) = state.isabelle.isabelle.invoke(callWpOp,
      ((cvarsIdx1.map(_.valueTerm), cvarsIdx2.map(_.valueTerm),
        qvarsIdx1.map(_.variableTerm)), (qvarsIdx2.map(_.variableTerm),
        post.isabelleTerm, state.isabelle.contextId)))

    val mismatchGoals = mismatches.toList.map {
      case (l,r) => QRHLSubgoal(l.toBlock,r.toBlock,wp,wp,Nil)
    }

{'fraction_non_alphanumeric': 0.15289730349971314, 'fraction_numerical': 0.009753298909925417, 'mean_word_length': 3.557516339869281, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 25, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4880321', 'n_tokens_mistral': 2617, 'n_tokens_neox': 2536, 'n_words': 547}