bind it even when no counterexample/sat is available; add tests

Similar to what @weaversa requested in #66, we bind `it` to `False`
when we can't find a sat assignment, and `it` to `True` when we've
proved a theorem.

Also adds some simple tests for the sat/prove result binding, and let
binding at the repl.

cryptol/REPL/Command.hs

@@ -55,7 +55,6 @@ import qualified Cryptol.Symbolic
 
 import Control.Monad (guard,unless,forM_,when)
 import Data.Char (isSpace,isPunctuation,isSymbol)
-import Data.Foldable (for_)
 import Data.Function (on)
 import Data.List (intercalate,isPrefixOf)
 import Data.Maybe (fromMaybe,mapMaybe)
@@ -338,7 +337,10 @@ proveCmd str = do
   ppOpts <- getPPValOpts
   case result of
     Left msg        -> io $ putStrLn msg
-    Right Nothing   -> io $ putStrLn "Q.E.D."
+    Right Nothing   -> do
+      io $ putStrLn "Q.E.D."
+      -- set `it` variable to `True`
+      bindItVariable T.eTrue T.tBit
     Right (Just tevs) -> do
       let vs = map (\(_,_,v) -> v) tevs
           tes = map (\(t,e,_) -> (t,e)) tevs
@@ -369,7 +371,10 @@ satCmd str = do
   ppOpts <- getPPValOpts
   case result of
     Left msg        -> io $ putStrLn msg
-    Right Nothing   -> io $ putStrLn "Unsatisfiable."
+    Right Nothing   -> do
+      io $ putStrLn "Unsatisfiable."
+      -- set `it` variable to `False`
+      bindItVariable T.eFalse T.tBit
     Right (Just tevs) -> do
       let vs = map (\(_,_,v) -> v) tevs
           tes = map (\(t,e,_) -> (t,e)) tevs

src/Cryptol/TypeCheck/AST.hs

@@ -368,6 +368,12 @@ tInf      = TCon (TC TCInf) []
 tBit     :: Type
 tBit      = TCon (TC TCBit) []
 
+eTrue    :: Expr
+eTrue     = ECon ECTrue
+
+eFalse   :: Expr
+eFalse    = ECon ECFalse
+
 tWord    :: Type -> Type
 tWord a   = tSeq a tBit
 

tests/issues/issue006.cry

@@ -0,0 +1,5 @@
+f : [32] -> [32]
+f x = x + 2
+
+g : [32] -> [32]
+g x = f x + 1

tests/issues/issue006.icry

@@ -0,0 +1,7 @@
+:l issue006.cry
+g 5
+let f x = 0
+g 5
+(f : [32] -> [32]) 5
+let f x = if (x : [32]) == 0 then 1 else x * (f (x - 1))
+f 5

tests/issues/issue006.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+8
+8
+0
+120

tests/issues/issue066.icry

@@ -0,0 +1,22 @@
+let f x = (x : [4]) == x
+:prove f
+:t it
+it
+let f x = (x : [4]) == 3
+:prove f
+:t it
+it
+:sat f
+:t it
+it
+let f x = (x : [4]) == 3 && x == 2
+:sat f
+:t it
+it
+let g p = (p : { x : [32], y : [32]}).x == p.y
+:prove g
+:t it
+it
+:sat g
+:t it
+it

tests/issues/issue066.icry.stdout

@@ -0,0 +1,19 @@
+Loading module Cryptol
+Q.E.D.
+it : Bit
+True
+f 0 = False
+it : [4]
+0
+f 3 = True
+it : [4]
+3
+Unsatisfiable.
+it : Bit
+False
+g {x = 0, y = 1} = False
+it : {x : [32], y : [32]}
+{x = 0, y = 1}
+g {x = 0, y = 0} = True
+it : {x : [32], y : [32]}
+{x = 0, y = 0}