Skip to content

Remove all ProofScript sequent features #3284

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
brianhuffman wants to merge 13 commits into
base: master
Choose a base branch
from
Draft

Remove all ProofScript sequent features #3284

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
31fa6aa
saw-script: Remove all sequent-specific `ProofScript` tactics.
brianhuffman May 26, 2026
e7e789f
saw-script: Remove `enable_sequent_goals`, `disable_sequent_goals`.
brianhuffman May 26, 2026
f865278
saw-central: Remove always-false field `rwSequentGoals`.
brianhuffman May 26, 2026
afd95b7
saw-central: Remove dead code from Proof.hs.
brianhuffman May 26, 2026
71d014f
saw-central: Remove unused constructors from `Evidence`.
brianhuffman May 26, 2026
967232e
saw-central: Remove unused local-hyps argument from `RewriteEvidence`.
brianhuffman May 27, 2026
f79b62b
saw-central: Remove `RawSequent`, `FocusedBranch` and `SequentState`.
brianhuffman May 27, 2026
0a802f6
saw-central: Remove type `Sequent` in favor of `Prop`.
brianhuffman May 27, 2026
9c9f4be
saw-script: Add `specialize_thm`, a pure variant of `specialize_theor…
brianhuffman May 26, 2026
d0f24ce
Add new SAWScript primitive `term_thm : Term -> Theorem`.
brianhuffman May 26, 2026
9bf3b69
Add new SAWScript primitive `apply_thm`.
brianhuffman May 28, 2026
0f1bf1b
Add new reimplementation of SAWScript primitive `goal_insert`.
brianhuffman May 29, 2026
2f1bf3d
Add command `subproof : ProofScript () -> ProofScript ()`.
brianhuffman Jun 3, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions saw-central/src/SAWCentral/Bisimulation.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ import SAWCentral.BisimulationTheorem
import SAWCentral.Builtins (unfold_term)
import SAWCentral.Options (Verbosity(..))
import SAWCentral.Panic (panic)
import SAWCentral.Proof
import SAWCentral.Proof hiding (applyTheorem)
import SAWCentral.Prover.Util (checkBooleanSchema)
import SAWCentral.Value

Expand Down Expand Up @@ -154,10 +154,10 @@ proveAll script ts = do
, goalName = "prove_bisim"
, goalLoc = show pos
, goalDesc = ""
, goalSequent = propToSequent prop
, goalProp = prop
, goalTags = mempty
}
res <- runProofScript script prop goal Nothing "prove_bisim" True False
res <- runProofScript script prop goal Nothing "prove_bisim" True
case res of
UnfinishedProof {} -> failProof res
ValidProof _ thm -> recordTheoremProof thm
Expand Down
Loading
Loading