From 49030290e9bce67a9464ee028eaee11220d9480c Mon Sep 17 00:00:00 2001
From: "Adam C. Foltzer" <acfoltzer@galois.com>
Date: Wed, 18 Feb 2015 10:25:46 -0800
Subject: [PATCH] fix #93

Revised how we do output for `:sat` and `:prove` without arguments,
making it more clear what properties are being checked in each case.

Also reworded the output of `:check` slightly in the case where the
property has no inputs. It would be nice to make `:check` output more
consistent with the others.
---
 cryptol/REPL/Command.hs           | 12 ++++++++----
 tests/issues/issue066.icry.stdout |  2 +-
 tests/issues/issue093.cry         |  1 +
 tests/issues/issue093.icry.fails  |  1 -
 tests/issues/issue093.icry.stdout | 30 +++++++++++++++++++++---------
 tests/issues/issue160.icry.stdout | 18 ++++++++++++------
 6 files changed, 43 insertions(+), 21 deletions(-)
 delete mode 100644 tests/issues/issue093.icry.fails

diff --git a/cryptol/REPL/Command.hs b/cryptol/REPL/Command.hs
index 05880d3a..23e3217e 100644
--- a/cryptol/REPL/Command.hs
+++ b/cryptol/REPL/Command.hs
@@ -333,8 +333,10 @@ qcCmd qcMode str =
              do opts <- getPPValOpts
                 do delProgress
                    delTesting
-                   prtLn "FAILED for the following inputs:"
-                   io $ mapM_ (print . pp . E.WithBase opts) vs
+                   case vs of
+                     [] -> prtLn "FAILED"
+                     _  -> do prtLn "FAILED for the following inputs:"
+                              io $ mapM_ (print . pp . E.WithBase opts) vs
                    return False
 
 satCmd, proveCmd :: String -> REPL ()
@@ -350,7 +352,9 @@ cmdProveSat isSat "" =
      if null xs
         then io $ putStrLn "There are no properties in scope."
         else forM_ xs $ \x ->
-               do io $ putStr $ "property " ++ x ++ " "
+               do if isSat
+                     then io $ putStr $ ":sat "   ++ x ++ "\n\t"
+                     else io $ putStr $ ":prove " ++ x ++ "\n\t"
                   cmdProveSat isSat x
 cmdProveSat isSat str = do
   EnvString proverName <- getUser "prover"
@@ -385,7 +389,7 @@ onlineProveSat isSat str proverName mfile = do
       panic "REPL.Command" [ "got EmptyResult for online prover query" ]
     Symbolic.ProverError msg     -> io $ putStrLn msg
     Symbolic.ThmResult ts        -> do
-      io $ putStrLn (if isSat then "Unsatisfiable." else "Q.E.D.")
+      io $ putStrLn (if isSat then "Unsatisfiable" else "Q.E.D.")
       let (t, e) = mkSolverResult cexStr (not isSat) (Left ts)
       bindItVariable t e
     Symbolic.AllSatResult tevss -> do
diff --git a/tests/issues/issue066.icry.stdout b/tests/issues/issue066.icry.stdout
index 2dfa2b18..cce815de 100644
--- a/tests/issues/issue066.icry.stdout
+++ b/tests/issues/issue066.icry.stdout
@@ -12,7 +12,7 @@ f 0x3 = True
 it : {result : Bit, arg1 : [4]}
 {result = True, arg1 = 0x3}
 True
-Unsatisfiable.
+Unsatisfiable
 it : {result : Bit, arg1 : [4]}
 
 Run-time error: no satisfying assignment available
diff --git a/tests/issues/issue093.cry b/tests/issues/issue093.cry
index 27eaa493..4167d460 100644
--- a/tests/issues/issue093.cry
+++ b/tests/issues/issue093.cry
@@ -2,3 +2,4 @@ property t0 = True
 property t1 x = x == (x : [32])
 property t2 x y = if (x : [32]) < (y : [32]) then y != zero else True
 not_a_prop = True
+property f0 = False
diff --git a/tests/issues/issue093.icry.fails b/tests/issues/issue093.icry.fails
deleted file mode 100644
index 5502bd29..00000000
--- a/tests/issues/issue093.icry.fails
+++ /dev/null
@@ -1 +0,0 @@
-Known issue, see ticket #117.
diff --git a/tests/issues/issue093.icry.stdout b/tests/issues/issue093.icry.stdout
index 9d68113e..64e8d590 100644
--- a/tests/issues/issue093.icry.stdout
+++ b/tests/issues/issue093.icry.stdout
@@ -1,18 +1,30 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
+property f0 Using exhaustive testing.
+FAILED
 property t0 Using exhaustive testing.
-  0%passed 1 tests.
+passed 1 tests.
 Q.E.D.
 property t1 Using random testing.
-testing...  0%  1%  2%  3%  4%  5%  6%  7%  8%  9% 10% 11% 12% 13% 14% 15% 16% 17% 18% 19% 20% 21% 22% 23% 24% 25% 26% 27% 28% 29% 30% 31% 32% 33% 34% 35% 36% 37% 38% 39% 40% 41% 42% 43% 44% 45% 46% 47% 48% 49% 50% 51% 52% 53% 54% 55% 56% 57% 58% 59% 60% 61% 62% 63% 64% 65% 66% 67% 68% 69% 70% 71% 72% 73% 74% 75% 76% 77% 78% 79% 80% 81% 82% 83% 84% 85% 86% 87% 88% 89% 90% 91% 92% 93% 94% 95% 96% 97% 98% 99%passed 100 tests.
+testing...passed 100 tests.
 Coverage: 0.00% (100 of 2^^32 values)
 property t2 Using random testing.
-testing...  0%  1%  2%  3%  4%  5%  6%  7%  8%  9% 10% 11% 12% 13% 14% 15% 16% 17% 18% 19% 20% 21% 22% 23% 24% 25% 26% 27% 28% 29% 30% 31% 32% 33% 34% 35% 36% 37% 38% 39% 40% 41% 42% 43% 44% 45% 46% 47% 48% 49% 50% 51% 52% 53% 54% 55% 56% 57% 58% 59% 60% 61% 62% 63% 64% 65% 66% 67% 68% 69% 70% 71% 72% 73% 74% 75% 76% 77% 78% 79% 80% 81% 82% 83% 84% 85% 86% 87% 88% 89% 90% 91% 92% 93% 94% 95% 96% 97% 98% 99%passed 100 tests.
+testing...passed 100 tests.
 Coverage: 0.00% (100 of 2^^64 values)
-property t0 Q.E.D.
-property t1 Q.E.D.
-property t2 Q.E.D.
-property t0 = True
-property t1 0x00000000 = True
-property t2 0x00000000 0x00000000 = True
+:prove f0
+	f0 = False
+:prove t0
+	Q.E.D.
+:prove t1
+	Q.E.D.
+:prove t2
+	Q.E.D.
+:sat f0
+	Unsatisfiable
+:sat t0
+	t0 = True
+:sat t1
+	t1 0x00000000 = True
+:sat t2
+	t2 0x00000000 0x00000000 = True
diff --git a/tests/issues/issue160.icry.stdout b/tests/issues/issue160.icry.stdout
index 35529daf..030a592f 100644
--- a/tests/issues/issue160.icry.stdout
+++ b/tests/issues/issue160.icry.stdout
@@ -1,9 +1,15 @@
 Loading module Cryptol
 Loading module Cryptol
 Loading module Main
-property thm1 Q.E.D.
-property thm2 Q.E.D.
-property thm3 Q.E.D.
-property thm4 Q.E.D.
-property thm5 Q.E.D.
-property thm6 Q.E.D.
+:prove thm1
+	Q.E.D.
+:prove thm2
+	Q.E.D.
+:prove thm3
+	Q.E.D.
+:prove thm4
+	Q.E.D.
+:prove thm5
+	Q.E.D.
+:prove thm6
+	Q.E.D.