From 8871e087e8da07de9f604077135aaf426f11fdcd Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Thu, 3 Oct 2024 16:17:19 +1000
Subject: [PATCH] Test for ways in which competing rewrites get applied

Desired behaviours taken by observation from de7fb61814, chosen
arbitrarily as a point that I happened to have checked out and before
changes in cfa24e268b.
---
 src/simp/src/selftest.sml | 30 ++++++++++++++++++++++++++----
 1 file changed, 26 insertions(+), 4 deletions(-)

diff --git a/src/simp/src/selftest.sml b/src/simp/src/selftest.sml
index 5fe7703134..dd296b31dc 100644
--- a/src/simp/src/selftest.sml
+++ b/src/simp/src/selftest.sml
@@ -1,6 +1,9 @@
 open HolKernel Parse boolLib simpLib
 open testutils boolSimps BackchainingLib
 
+val failcount = ref 0
+val _ = diemode := Remember failcount
+
 val _ = Portable.catch_SIGINT()
 
 (* earlier versions of the simplifier would go into an infinite loop on
@@ -426,12 +429,14 @@ val _ = let
         | _ => false
   fun test (msg, tac, ing, outgs) =
       (tprint msg;
-       require_msg (testresult outgs) printgoals (VALID tac) ing)
+       require_msg (testresult outgs) printgoals tac ing)
   val T_t = “?x:'a. p”
   fun gs c = global_simp_tac c
   val fs = full_simp_tac
   val gsc = {droptrues=true,elimvars=false,strip=true,oldestfirst=true}
   val gsc' = {droptrues=true,elimvars=false,strip=true,oldestfirst=false}
+  val bss1 = bool_ss ++ rewrites [ASSUME “x = T”]
+  val bss2 = bss1 ++ rewrites [ASSUME “x = F”]
 in
   List.app (ignore o test) [
     ("Abbrev var not rewritten",
@@ -460,9 +465,26 @@ in
      ([“x = F”, “y = T”], “p /\ x /\ y”), [([“x = F”, “y = T”], “p /\ x”)]),
     ("IgnAsm (sub-match)",
      asm_simp_tac bool_ss [markerLib.IgnAsm ‘F (* sa *)’],
-     ([“x = F”, “y = T”], “p /\ x /\ y”), [([“x = F”, “y = T”], “p /\ x”)])
-
+     ([“x = F”, “y = T”], “p /\ x /\ y”), [([“x = F”, “y = T”], “p /\ x”)]),
+    ("Rewrite competition: ASM vs arg",
+     asm_simp_tac bool_ss [ASSUME “x = T”],
+     ([“x = F”], “P (x:bool):bool”), [([“x = F”], “P F:bool”)]),
+    ("Rewrite competition: ARG1 vs arg2",
+     asm_simp_tac bool_ss [ASSUME “x = T”, ASSUME “x = F”],
+     ([], “P (x:bool):bool”), [([], “P T:bool”)]),
+    ("Rewrite competition: ASM1 vs asm2",
+     asm_simp_tac bool_ss [],
+     ([“x=T”, “x=F”], “P (x:bool):bool”), [([“x=T”,“x=F”], “P T:bool”)]),
+    ("Rewrite competition: ss1 vs SS2",
+     asm_simp_tac bss2 [],
+     ([], “P(x:bool):bool”), [([], “P F:bool”)]),
+    ("Rewrite competition: ARG vs ss",
+     asm_simp_tac bss1 [ASSUME “x = F”],
+     ([], “P(x:bool):bool”), [([], “P F:bool”)]),
+    ("Rewrite competition: ASM vs ss",
+     asm_simp_tac bss1 [],
+    ([“x = F”], “P(x:bool):bool”), [([“x = F”], “P F:bool”)])
   ]
 end
 
-val _ = Process.exit Process.success
+val _ = exit_count0 failcount