<commit_before>package qrhl.tactic

import org.scalatest.funsuite.AnyFunSuite
import qrhl.toplevel.{TacticCommand, ToplevelTest}
import ToplevelTest.output
import qrhl.{DenotationalEqSubgoal, QRHLSubgoal}

class SwapTacTest extends AnyFunSuite {
  test("subprogram") {
    val tl = ToplevelTest.makeToplevelWithTheory()
    tl.run(
      """classical var b : bit.
        |classical var x : int.
        |classical var y : int.
        |quantum var Q : bit.
        |qrhl {undefined} b <- measure Q with computational_basis; b <- measure Q with computational_basis; x <- y+1; ~ skip; {undefined}.
        |""".stripMargin)
    val cmd = tl.state.parseCommand("swap left 2 1 subprograms second: { b <- measure Q with computational_basis; }")
    println(cmd)
    val TacticCommand(tactic : SwapTac) = cmd
    println(tactic)
    val subgoals = tactic.apply(tl.state, tl.state.goal.head)
    println(subgoals)
    assert(subgoals.length == 2)
    val List(deneq : DenotationalEqSubgoal, qrhl : QRHLSubgoal) = subgoals
    deneq.checkWelltyped(tl.state.isabelle)
    qrhl.checkWelltyped(tl.state.isabelle)
    assert(deneq.left.toString == "{ b <- measure Q in computational_basis; b <- measure Q in computational_basis; }")
    assert(deneq.right.toString == "{ b <- measure Q in computational_basis; b <- measure Q in computational_basis; }")
    assert(qrhl.left.toString == "{ b <- measure Q in computational_basis; x <- y + 1; b <- measure Q in computational_basis; }")
    assert(qrhl.right.toString == "{}")
  }
}<commit_msg>Fixed SwapTacTest. (Expected strings changed due to previous commit.)<commit_after>package qrhl.tactic

import org.scalatest.funsuite.AnyFunSuite
import qrhl.toplevel.{TacticCommand, ToplevelTest}
import ToplevelTest.output
import qrhl.{DenotationalEqSubgoal, QRHLSubgoal}

class SwapTacTest extends AnyFunSuite {
  test("subprogram") {
    val tl = ToplevelTest.makeToplevelWithTheory()
    tl.run(
      """classical var b : bit.
        |classical var x : int.
        |classical var y : int.
        |quantum var Q : bit.
        |qrhl {undefined} b <- measure Q with computational_basis; b <- measure Q with computational_basis; x <- y+1; ~ skip; {undefined}.
        |""".stripMargin)
    val cmd = tl.state.parseCommand("swap left 2 1 subprograms second: { b <- measure Q with computational_basis; }")
    println(cmd)
    val TacticCommand(tactic : SwapTac) = cmd
    println(tactic)
    val subgoals = tactic.apply(tl.state, tl.state.goal.head)
    println(subgoals)
    assert(subgoals.length == 2)
    val List(deneq : DenotationalEqSubgoal, qrhl : QRHLSubgoal) = subgoals
    deneq.checkWelltyped(tl.state.isabelle)
    qrhl.checkWelltyped(tl.state.isabelle)
    assert(deneq.left.toString == "{ b <- measure Q with computational_basis; b <- measure Q with computational_basis; }")
    assert(deneq.right.toString == "{ b <- measure Q with computational_basis; b <- measure Q with computational_basis; }")
    assert(qrhl.left.toString == "{ b <- measure Q with computational_basis; x <- y + 1; b <- measure Q with computational_basis; }")
    assert(qrhl.right.toString == "{}")
  }
}
{'fraction_non_alphanumeric': 0.11900191938579655, 'fraction_numerical': 0.003198976327575176, 'mean_word_length': 3.6325925925925926, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 3, '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': '1551819', 'n_tokens_mistral': 1118, 'n_tokens_neox': 1028, 'n_words': 258}