From bc644bd88e28cf39fcf665670f975e594c53ca4b Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Tue, 13 Dec 2022 09:39:56 +1100
Subject: [PATCH] Rework new Q tests to not depend on arithmetic

Q is tested before numbers exist.

Also report each test-case individually, making it easier to know
what's failed when and if things fail.
---
 src/q/selftest.sml | 89 ++++++++++++++++++++++++++--------------------
 1 file changed, 50 insertions(+), 39 deletions(-)

diff --git a/src/q/selftest.sml b/src/q/selftest.sml
index 46e78f13bd..6e2d879777 100644
--- a/src/q/selftest.sml
+++ b/src/q/selftest.sml
@@ -28,20 +28,32 @@ in
   else die "FAILED!"
 end handle InternalDie s => die s
 
-val _ = tprint "Testing Q.LIST_REFINE_EXISTS_TAC"
+(* fake arithmetic *)
+val _ = new_type ("num", 0)
+val _ = new_constant ("*", ``:num -> num -> num``)
+val _ = new_constant ("+", ``:num -> num -> num``)
+val _ = new_constant ("<", ``:num -> num -> bool``)
+val _ = new_constant ("SUC", ``:num -> num``)
+val _ = new_constant ("zero", ``:num``)
+val _ = new_constant ("three", ``:num``)
+val _ = new_constant ("five", ``:num``)
+val _ = set_fixity "+" (Infixl 500)
+val _ = set_fixity "*" (Infixl 600)
+val _ = set_fixity "<" (Infix(NONASSOC, 450))
+
 val _ = let
     val tests = [ (* triples of: (goal, quotations, expected (single) subgoal) *)
       (* Simple test *)
       (
-        ([], ``∃n m. n + m = 0``),
+        ([], ``∃n m. n + m = zero``),
         [`_`, `SUC l`] : term frag list list,
-        ``∃l n. n + SUC l = 0``
+        ``∃l n. n + SUC l = zero``
       ),
       (* Use variable in assumption *)
       (
-        ([``l = 0``], ``∃n m. n + m = 0``),
+        ([``l = zero``], ``∃n m. n + m = zero``),
         [`_`, `SUC l`],
-        ``∃n. n + SUC l = 0``
+        ``∃n. n + SUC l = zero``
       ),
       (* Witness var shadowing boundvar *)
       (
@@ -51,7 +63,7 @@ val _ = let
       ),
       (* Boundvar `c` shadowing freevar *)
       (
-        ([``c = 5``], ``∃n m c. n + m = c``),
+        ([``c = five``], ``∃n m c. n + m = c``),
         [`_`,`SUC c`],
         ``∃n c'. n + SUC c = c'``
       ),
@@ -63,13 +75,13 @@ val _ = let
       ),
       (* Re-use term across quotations *)
       (
-        ([], ``∃n m l. n + m + l = 0``),
+        ([], ``∃n m l. n + m + l = zero``),
         [`_`,`k`,`SUC k`],
-        ``∃k n. n + k + SUC k = 0``
+        ``∃k n. n + k + SUC k = zero``
       ),
       (* Slightly more involved tests *)
       (
-        ([``n = 2``,``c = 5``], ``∃a b c d. a + b = c + d``),
+        ([``n = three``,``c = five``], ``∃a b c d. a + b = c + d``),
         [`_`,`SUC c`, `_`, `n + m`],
         ``∃m a c'. a + SUC c = c' + (n + m)``
       ),
@@ -88,48 +100,47 @@ val _ = let
             P x'' (Q x x' x'³') x'⁴'``
       )
     ]
-    fun checkSubgoals (sgs, vld:validation) (expected_asms, expected_goal) =
+    fun checkSubgoals (expected_asms, expected_goal) (sgs, vld:validation)  =
       case sgs of
         [(asms,sg)] =>
-          if (ListPair.allEq (uncurry aconv) (asms, expected_asms)) andalso
-             aconv sg expected_goal
-          then vld (map mk_thm sgs)
-               handle _ => raise InternalDie "FAILED! Bad validation"
-          else raise InternalDie "FAILED! Does not match expected result"
-      | _ => raise InternalDie "FAILED! Too many subgoals produced"
-    fun test_single (input, qs, expected) = let
-        val result = Q.LIST_REFINE_EXISTS_TAC qs input
-                     handle _ => raise InternalDie "FAILED! Tactic failed"
-        in checkSubgoals result (fst input, expected) end
-    val _ = List.map test_single tests
-  in OK () end
-  handle InternalDie s => die s
+           ListPair.allEq (uncurry aconv) (asms, expected_asms) andalso
+           aconv sg expected_goal andalso
+           (can vld (map mk_thm sgs) orelse
+            (die "FAILED! Bad validation"; false))
+      | _ => (die "FAILED! Too many subgoals produced"; false)
+    fun test_single (input, qs, expected) =
+        let
+          val _ = tprint ("Q.LIST_REFINE_EXISTS_TAC: " ^
+                          term_to_string (#2 input))
+          open HOLPP
+        in
+          require_pretty_msg (check_result $ checkSubgoals (#1 input, expected))
+                             (block CONSISTENT 0 o
+                              pr_list goalStack.pp_goal
+                                      [add_string ",", add_break(1,0)] o
+                              fst)
+                             (Q.LIST_REFINE_EXISTS_TAC qs)
+                             input
+        end
+  in
+    List.app test_single tests
+  end
 
 (* combinator *)
 val _ = new_definition("I_DEF", ``I = \x:'a. x``);
 
-(* fake arithmetic *)
-val _ = new_type ("num", 0)
-val _ = new_constant ("*", ``:num -> num -> num``)
-val _ = new_constant ("+", ``:num -> num -> num``)
-val _ = new_constant ("<", ``:num -> num -> bool``)
-val _ = new_constant ("SUC", ``:num -> num``)
-val _ = new_constant ("zero", ``:num``)
-val _ = set_fixity "+" (Infixl 500)
-val _ = set_fixity "*" (Infixl 600)
-val _ = set_fixity "<" (Infix(NONASSOC, 450))
 
 fun aconvdie m t1 t2 =
     aconv t1 t2 orelse raise InternalDie ("FAILED! (" ^ m ^ " wrong)")
 
 val _ = tprint "Q.MATCH_RENAME_TAC 1"
-val gl0 = ([``x < y``], ``x = z:num``)
-val expected_a0 = ``a < y``
-val expected_c0 = ``a = b:num``
-val (sgs, _) = Q.MATCH_RENAME_TAC `a = b` gl0
+val glZ = ([``x < y``], ``x = z:num``)
+val expected_aZ = ``a < y``
+val expected_cZ = ``a = b:num``
+val (sgs, _) = Q.MATCH_RENAME_TAC `a = b` glZ
 val _ = (case sgs of
-            [([a], c)] => (aconvdie "assumption" a expected_a0;
-                           aconvdie "goal" c expected_c0;
+            [([a], c)] => (aconvdie "assumption" a expected_aZ;
+                           aconvdie "goal" c expected_cZ;
                            OK())
           | _ => die "FAILED!")
         handle InternalDie s => die s