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

@@ -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

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

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

tests/issues/issue093.icry.fails

@@ -1 +0,0 @@
-Known issue, see ticket #117.

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

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.