Merge branch 'master' into abstract-types

# Conflicts:
#	src/Cryptol/TypeCheck/Solver/SMT.hs

cryptol.cabal

@@ -76,6 +76,7 @@ library
                        mtl               >= 2.2.1,
                        time >= 1.6.0.1
 
+
   Build-tools:         alex, happy
   hs-source-dirs:      src
 
@@ -140,16 +141,8 @@ library
 
                        Cryptol.TypeCheck.Solver.Numeric,
                        Cryptol.TypeCheck.Solver.Improve,
-                       Cryptol.TypeCheck.Solver.CrySAT,
-                       Cryptol.TypeCheck.Solver.Numeric.AST,
-                       Cryptol.TypeCheck.Solver.Numeric.ImportExport,
-                       Cryptol.TypeCheck.Solver.Numeric.Defined,
                        Cryptol.TypeCheck.Solver.Numeric.Fin,
                        Cryptol.TypeCheck.Solver.Numeric.Interval,
-                       Cryptol.TypeCheck.Solver.Numeric.Simplify,
-                       Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr,
-                       Cryptol.TypeCheck.Solver.Numeric.NonLin,
-                       Cryptol.TypeCheck.Solver.Numeric.SMT,
 
                        Cryptol.Transform.MonoValues,
                        Cryptol.Transform.Specialize,

src/Cryptol/ModuleSystem/Env.hs

@@ -84,13 +84,7 @@ initialModuleEnv  = do
   let handle :: X.IOException -> IO String
       handle _e = return ""
   userDir <- X.catch (getAppUserDataDirectory "cryptol") handle
-  return ModuleEnv
+  let searchPath = [ curDir
-    { meLoadedModules = mempty
-    , meNameSeeds     = T.nameSeeds
-    , meEvalEnv       = mempty
-    , meFocusedModule = Nothing
-      -- we search these in order, taking the first match
-    , meSearchPath    = [ curDir
                    -- something like $HOME/.cryptol
                    , userDir
 #if defined(mingw32_HOST_OS) || defined(__MINGW32__)
@@ -109,12 +103,21 @@ initialModuleEnv  = do
                    , dataDir
 #endif
                    ]
+
+  return ModuleEnv
+    { meLoadedModules = mempty
+    , meNameSeeds     = T.nameSeeds
+    , meEvalEnv       = mempty
+    , meFocusedModule = Nothing
+      -- we search these in order, taking the first match
+    , meSearchPath    = searchPath
     , meDynEnv        = mempty
     , meMonoBinds     = True
     , meSolverConfig  = T.SolverConfig
                           { T.solverPath = "z3"
                           , T.solverArgs = [ "-smt2", "-in" ]
                           , T.solverVerbose = 0
+                          , T.solverPreludePath = searchPath
                           }
     , meCoreLint      = NoCoreLint
     , meSupply        = emptySupply

src/Cryptol/Prelude.hs

@@ -16,7 +16,7 @@
 module Cryptol.Prelude (
   writePreludeContents,
   writePreludeExtrasContents,
-  writeTcPreludeContents,
+  cryptolTcContents
   ) where
 
 
@@ -51,12 +51,4 @@ writePreludeExtrasContents = do
 cryptolTcContents :: String
 cryptolTcContents = [there|lib/CryptolTC.z3|]
 
--- | Write the contents of the Prelude to a temporary file so that
+
--- Cryptol can load the module.
-writeTcPreludeContents :: IO FilePath
-writeTcPreludeContents = do
-  tmpdir <- getTemporaryDirectory
-  (path, h) <- openTempFile tmpdir "CryptolTC.z3"
-  hPutStr h cryptolTcContents
-  hClose h
-  return path

src/Cryptol/REPL/Command.hs

@@ -70,7 +70,7 @@ import qualified Cryptol.TypeCheck.Parseable as T
 import qualified Cryptol.TypeCheck.Subst as T
 import qualified Cryptol.TypeCheck.InferTypes as T
 import           Cryptol.TypeCheck.Solve(defaultReplExpr)
-import qualified Cryptol.TypeCheck.Solver.CrySAT as CrySAT
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import Cryptol.TypeCheck.PP (dump,ppWithNames)
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic(panic)
@@ -964,7 +964,7 @@ replEvalExpr expr =
 
      me <- getModuleEnv
      let cfg = M.meSolverConfig me
-     mbDef <- io $ CrySAT.withSolver cfg (\s -> defaultReplExpr s def sig)
+     mbDef <- io $ SMT.withSolver cfg (\s -> defaultReplExpr s def sig)
 
      (def1,ty) <-
         case mbDef of

src/Cryptol/TypeCheck/Infer.hs

@@ -29,7 +29,7 @@ import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
                                         checkParameterConstraints)
 import           Cryptol.TypeCheck.Instantiate
 import           Cryptol.TypeCheck.Depends
-import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),emptySubst)
+import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@))
 import           Cryptol.TypeCheck.Solver.InfNat(genLog)
 import           Cryptol.Utils.Ident
 import           Cryptol.Utils.Panic(panic)
@@ -694,15 +694,7 @@ generalize bs0 gs0 =
      when (not (null ambig)) $ recordError $ AmbiguousType $ map dName bs
 
 
-     solver <- getSolver
+     let (as0,here1,defSu,ws) = improveByDefaultingWithPure maybeAmbig here0
-     (as0,here1,mb_defSu,ws) <- io $ improveByDefaultingWith solver maybeAmbig here0
-     defSu <- case mb_defSu of
-               Nothing -> do recordError $ UnsolvedGoals True here0
-                             return emptySubst
-               Just s  -> return s
-
-
-
      mapM_ recordWarning ws
      let here = map goal here1
 
@@ -712,7 +704,7 @@ generalize bs0 gs0 =
      totSu <- getSubst
      let
          su     = listSubst (zip as (map (TVar . tpVar) asPs)) @@ defSu @@ totSu
-         qs     = map (apSubst su) here
+         qs     = concatMap (pSplitAnd . apSubst su) here
 
          genE e = foldr ETAbs (foldr EProofAbs (apSubst su e) qs) asPs
          genB d = d { dDefinition = case dDefinition d of
@@ -806,17 +798,12 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
         when (not (null ambig)) $ recordError
                                 $ AmbiguousType [ thing (P.bName b) ]
 
-        solver <- getSolver
+        -- XXX: Uhm, why are we defaulting that 'later' things here?
-        (_,_,mb_defSu2,ws) <-
+        -- Surely this should be done later, when we solve them?
-            io $ improveByDefaultingWith solver maybeAmbig later
+        let (_,newGs,defSu2,ws) = improveByDefaultingWithPure maybeAmbig later
-        defSu2 <- case mb_defSu2 of
-                   Nothing -> do recordError $ UnsolvedGoals True later
-                                 return emptySubst
-                   Just s -> return s
         mapM_ recordWarning ws
         extendSubst defSu2
-
+        addGoals newGs
-     addGoals later
 
      su <- getSubst
      let su' = defSu1 @@ su

src/Cryptol/TypeCheck/InferTypes.hs

@@ -41,6 +41,8 @@ data SolverConfig = SolverConfig
   { solverPath    :: FilePath   -- ^ The SMT solver to invoke
   , solverArgs    :: [String]   -- ^ Additional arguments to pass to the solver
   , solverVerbose :: Int        -- ^ How verbose to be when type-checking
+  , solverPreludePath :: [FilePath]
+    -- ^ Look for the solver prelude in these locations.
   } deriving (Show, Generic, NFData)
 
 -- | The types of variables in the environment.

src/Cryptol/TypeCheck/Monad.hs

@@ -19,13 +19,12 @@ module Cryptol.TypeCheck.Monad
 import           Cryptol.ModuleSystem.Name (FreshM(..),Supply)
 import           Cryptol.Parser.Position
 import qualified Cryptol.Parser.AST as P
-import           Cryptol.Prelude (writeTcPreludeContents)
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Subst
 import           Cryptol.TypeCheck.Unify(mgu, Result(..), UnificationError(..))
 import           Cryptol.TypeCheck.InferTypes
 import qualified Cryptol.TypeCheck.SimpleSolver as Simple
-import qualified Cryptol.TypeCheck.Solver.CrySAT as CrySAT
+import qualified Cryptol.TypeCheck.Solver.SMT as SMT
 import           Cryptol.Utils.PP(pp, (<+>), Doc, text, quotes)
 import           Cryptol.Utils.Panic(panic)
 
@@ -42,8 +41,6 @@ import           MonadLib hiding (mapM)
 
 import           Data.IORef
 
-import           System.FilePath((</>))
-import           System.Directory(doesFileExist)
 
 
 import GHC.Generics (Generic)
@@ -103,9 +100,8 @@ bumpCounter = do RO { .. } <- IM ask
                  io $ modifyIORef' iSolveCounter (+1)
 
 runInferM :: TVars a => InferInput -> InferM a -> IO (InferOutput a)
-runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
+runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver ->
-  do loadCryTCPrel solver (inpSearchPath info)
+  do coutner <- newIORef 0
-     coutner <- newIORef 0
      rec ro <- return RO { iRange     = inpRange info
                      , iVars          = Map.map ExtVar (inpVars info)
                      , iTVars         = []
@@ -173,15 +169,6 @@ runInferM info (IM m) = CrySAT.withSolver (inpSolverConfig info) $ \solver ->
   -- The actual order does not matter
   cmpRange (Range x y z) (Range a b c) = compare (x,y,z) (a,b,c)
 
-  loadCryTCPrel s [] =
-    do file <- writeTcPreludeContents
-       CrySAT.loadFile s file
-
-  loadCryTCPrel s (p : ps) =
-    do let file = p </> "CryptolTC.z3"
-       yes <- doesFileExist file
-       if yes then CrySAT.loadFile s file
-              else loadCryTCPrel s ps
 
 
 
@@ -233,7 +220,7 @@ data RO = RO
     -- in where-blocks will never be generalized. Bindings with type
     -- signatures, and all bindings at top level are unaffected.
 
-  , iSolver :: CrySAT.Solver
+  , iSolver :: SMT.Solver
 
   , iPrimNames :: !PrimMap
 
@@ -324,7 +311,7 @@ recordWarning w =
   do r <- curRange
      IM $ sets_ $ \s -> s { iWarnings = (r,w) : iWarnings s }
 
-getSolver :: InferM CrySAT.Solver
+getSolver :: InferM SMT.Solver
 getSolver =
   do RO { .. } <- IM ask
      return iSolver

src/Cryptol/TypeCheck/Solve.hs

@@ -14,7 +14,7 @@ module Cryptol.TypeCheck.Solve
   , proveModuleTopLevel
   , wfType
   , wfTypeFunction
-  , improveByDefaultingWith
+  , improveByDefaultingWithPure
   , defaultReplExpr
   ) where
 
@@ -24,34 +24,28 @@ import           Cryptol.TypeCheck.Monad
 import           Cryptol.TypeCheck.Subst
                     (apSubst, singleSubst, isEmptySubst, substToList,
                           emptySubst,Subst,listSubst, (@@), Subst,
-                           apSubstMaybe, substBinds)
+                           substBinds)
 import qualified Cryptol.TypeCheck.SimpleSolver as Simplify
 import           Cryptol.TypeCheck.Solver.Types
 import           Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
 import           Cryptol.TypeCheck.SimpType(tMax)
 
 
-import           Cryptol.TypeCheck.Solver.SMT(proveImp,checkUnsolvable)
+import           Cryptol.TypeCheck.Solver.SMT(Solver,proveImp,tryGetModel)
 import           Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
 import           Cryptol.TypeCheck.Solver.Numeric.Interval
-import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
-import qualified Cryptol.TypeCheck.Solver.Numeric.ImportExport as Num
-import qualified Cryptol.TypeCheck.Solver.CrySAT as Num
-import           Cryptol.TypeCheck.Solver.CrySAT
 import           Cryptol.Utils.PP (text,vcat,(<+>))
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.Patterns(matchMaybe)
 
-import           Control.Monad (guard, mzero)
 import           Control.Applicative ((<|>))
-import           Data.Either(partitionEithers)
+import           Control.Monad(mzero,guard)
-import           Data.Maybe(catMaybes)
-import           Data.Map ( Map )
 import qualified Data.Map as Map
 import           Data.Set ( Set )
 import qualified Data.Set as Set
 
 
+
 {- | Add additional constraints that ensure validity of type function.
 Note that these constraints do not introduce additional malformed types,
 so the well-formedness constraints are guaranteed to be well-formed.
@@ -199,8 +193,8 @@ proveImplication lnam as ps gs =
      return su
 
 
-proveImplicationIO :: Num.Solver
+proveImplicationIO :: Solver
-                   -> Name     -- ^ Checking this function
+                   -> Maybe Name     -- ^ Checking this function
                    -> Set TVar -- ^ These appear in the env., and we should
                                -- not try to default the
                    -> [TParam] -- ^ Type parameters
@@ -273,49 +267,6 @@ cleanupError err =
 
 
 
-simpGoals' :: Num.Solver -> Ctxt -> [Goal] -> IO (Either [Goal] [Goal], Subst)
-simpGoals' s asmps gs0 = go emptySubst [] (wellFormed gs0 ++ gs0)
-  where
-  -- Assumes that the well-formed constraints are themselves well-formed.
-  wellFormed gs = [ g { goal = p } | g <- gs, p <- wfType (goal g) ]
-
-  go su old [] = return (Right old, su)
-  go su old gs =
-    do res  <- solveConstraints s asmps old gs
-       case res of
-         Left err -> return (Left err, su)
-         Right gs2 ->
-           do let gs3 = gs2 ++ old
-              mb <- computeImprovements s gs3
-              case mb of
-                Left err -> return (Left err, su)
-                Right impSu ->
-                  let (unchanged,changed) =
-                                    partitionEithers (map (applyImp impSu) gs3)
-                      new = wellFormed changed
-                  in go (impSu @@ su) unchanged (new ++ changed)
-
-  applyImp su g = case apSubstMaybe su (goal g) of
-                    Nothing -> Left g
-                    Just p  -> Right g { goal = p }
-
-
-{- Note:
-It is good to consider the other goals when evaluating terms.
-For example, consider the constraints:
-
-    P (x * inf), x >= 1
-
-We cannot simplify `x * inf` on its own, because we do not know if `x`
-might be 0.  However, in the contxt of `x >= 1`, we know that this is
-impossible, and we can simplify the constraints to:
-
-    P inf, x >= 1
-
-However, we should be careful to avoid circular reasoning, as we wouldn't
-want to use the fact that `x >= 1` to simplify `x >= 1` to true.
--}
-
 
 
 
@@ -328,110 +279,6 @@ assumptionIntervals as ps =
 
 
 
-solveConstraints :: Num.Solver ->
-                    Ctxt ->
-                    [Goal] {- We may use these, but don't try to solve,
-                              we already tried and failed. -} ->
-                    [Goal] {- Need to solve these -} ->
-                    IO (Either [Goal] [Goal])
-                    -- ^ Left: contradiciting goals,
-                    --   Right: goals that were not solved, or sub-goals
-                    --          for solved goals.  Does not include "old"
-solveConstraints s asmps otherGs gs0 =
-  debugBlock s "Solving constraints" $ go ctxt0 [] gs0
-
-  where
-  ctxt0 = assumptionIntervals asmps (map goal otherGs)
-
-
-  go _ unsolved [] =
-    do let (cs,nums) = partitionEithers (map Num.numericRight unsolved)
-       nums' <- solveNumerics s otherNumerics nums
-       return (Right (cs ++ nums'))
-
-  go ctxt unsolved (g : gs) =
-    case Simplify.simplifyStep ctxt (goal g) of
-      Unsolvable _x       -> return (Left [g])  -- maybe give error?
-      Unsolved            -> go ctxt (g : unsolved) gs
-      SolvedIf subs       ->
-        let cvt x = g { goal = x }
-        in  go ctxt unsolved (map cvt subs ++ gs)
-
-
-  otherNumerics = [ g | Right g <- map Num.numericRight otherGs ]
-
-
-
-
-solveNumerics :: Num.Solver ->
-                 [(Goal,Num.Prop)] {- ^ Consult these -} ->
-                 [(Goal,Num.Prop)] {- ^ Solve these -}   ->
-                 IO [Goal]
-solveNumerics _ _ [] = return []
-solveNumerics s consultGs solveGs =
-  Num.withScope s $
-    do _   <- Num.assumeProps s (map (goal . fst) consultGs)
-       Num.simplifyProps s (map Num.knownDefined solveGs)
-
-
-computeImprovements :: Num.Solver -> [Goal] -> IO (Either [Goal] Subst)
-computeImprovements s gs =
-  debugBlock s "Computing improvements" $
-  do let nums = [ g | Right g <- map Num.numericRight gs ]
-     res <- Num.withScope s $
-        do _  <- Num.assumeProps s (map (goal . fst) nums)
-           mb <- Num.check s
-           case mb of
-             Nothing       -> return Nothing
-             Just (suish,_ps1) ->
-               do let (su,_ps2) = importSplitImps suish
-                  -- Num.check has already checked that the intervals are sane,
-                  -- so we don't need to check for a broken interval here
-                  Right ints <- Num.getIntervals s
-                  return (Just (ints,su))
-     case res of
-       Just (_ints, su) -> return (Right su) -- ?
-{-
-         | isEmptySubst su
-         , (x,t) : _ <- mapMaybe (improveByDefn ints) gs ->
-           do let su' = singleSubst x t
-              debugLog s ("Improve by definition: " ++ show (pp su'))
-              return (Right su')
-         | otherwise -> return (Right su)
- -}
-       Nothing ->
-         do bad <- Num.minimizeContradictionSimpDef s
-                                                (map Num.knownDefined nums)
-            return (Left bad)
-
-
-
-
-
--- | Import an improving substitutin (i.e., a bunch of equations)
--- into a Cryptol substitution (which is idempotent).
--- The substitution will contain only unification variables.
--- "Improvements" on skolem variables become additional constraints.
-importSplitImps :: Map Num.Name Num.Expr -> (Subst, [Prop])
-importSplitImps = mk . partitionEithers . map imp . Map.toList
-  where
-  mk (uni,props) = (listSubst (catMaybes uni), props)
-
-  imp (x,e) = case (x, Num.importType e) of
-                (Num.UserName tv, Just ty) ->
-                  case tv of
-                    TVFree {}  -> Left (Just (tv,ty))
-                    TVBound {} -> Right (TVar tv =#= ty)
-
-                {- This may happen if we are working on an implication,
-                and we have an improvement about a variable in the
-                assumptions that is not in any og the goals.
-                XXX: Perhaps, we should mark these variable, so we don't waste
-                time to "improve" them. -}
-
-                _ -> Left Nothing
-
-
 
 
 
@@ -461,47 +308,6 @@ importSplitImps = mk . partitionEithers . map imp . Map.toList
       3. a substitution which indicates what got defaulted.
 -}
 
-improveByDefaultingWith ::
-  Num.Solver ->
-  [TVar] ->   -- candidates for defaulting
-  [Goal] ->   -- constraints
-    IO  ( [TVar]    -- non-defaulted
-        , [Goal]    -- new constraints
-        , Maybe Subst   -- Nothing: improve to False
-                        -- Just:    improvements from defaulting
-        , [Warning] -- warnings about defaulting
-        )
--- XXX: Remove this
--- improveByDefaultingWith s as gs = return (as,gs,emptySubst,[])
-improveByDefaultingWith s as gs =
-  do bad <- checkUnsolvable s gs
-     if bad
-       then return (as, gs, Nothing, [])
-       else tryImp
-
-  where
-  tryImp =
-    case improveByDefaultingWithPure as gs of
-      (xs,gs',su,ws) ->
-        do (res,su1) <- simpGoals' s Map.empty gs'
-           case res of
-             Left err ->
-               panic "improveByDefaultingWith"
-                    $ [ "Defaulting resulted in unsolvable constraints."
-                      , "Before:"
-                      ] ++ [ "  " ++ show (pp (goal g)) | g <- gs ] ++
-                      [ "After:"
-                      ] ++ [ "  " ++ show (pp (goal g)) | g <- gs' ] ++
-                      [ "Contradiction:" ] ++
-                      [ "  " ++ show (pp (goal g)) | g <- err ]
-             Right gs'' ->
-               do let su2 = su1 @@ su
-                      isDef x = x `Set.member` substBinds su2
-                  return ( filter (not . isDef) xs
-                         , gs''
-                         , Just su2
-                         , ws
-                         )
 
 
 improveByDefaultingWithPure :: [TVar] -> [Goal] ->
@@ -602,31 +408,19 @@ improveByDefaultingWithPure as ps =
 -- | Try to pick a reasonable instantiation for an expression, with
 -- the given type.  This is useful when we do evaluation at the REPL.
 -- The resulting types should satisfy the constraints of the schema.
-defaultReplExpr :: Num.Solver -> Expr -> Schema
+defaultReplExpr :: Solver -> Expr -> Schema
              -> IO (Maybe ([(TParam,Type)], Expr))
--- defaultReplExpr _ _ _ = return Nothing
+defaultReplExpr sol e s =
-defaultReplExpr so e s =
   if all (\v -> kindOf v == KNum) (sVars s)
      then do let params = map tpVar (sVars s)
-             mbSubst <- tryGetModel so params (sProps s)
+                 props  = sProps s
-             case mbSubst of
+             mbSubst <- tryGetModel sol params props
-               Just su ->
+             return $ do su <- mbSubst
-                 do (res,su1) <- simpGoals' so Map.empty (map (makeGoal su) (sProps s))
+                         guard (null (concatMap pSplitAnd (apSubst su props)))
-                    return $
+                         tys <- mapM (bindParam su) params
-                      case res of
-                        Right [] | isEmptySubst su1 ->
-                         do tys <- mapM (bindParam su) params
                          return (zip (sVars s) tys, appExpr tys)
-                        _ -> Nothing
-               _ -> return Nothing
-
      else return Nothing
   where
-  makeGoal su p = Goal { goalSource = error "goal source"
-                       , goalRange  = error "goal range"
-                       , goal       = apSubst su p
-                       }
-
   bindParam su tp =
     do let ty  = TVar tp
            ty' = apSubst su ty
@@ -637,15 +431,5 @@ defaultReplExpr so e s =
 
 
 
--- | Attempt to default the given constraints by asserting them in the SMT
--- solver, and asking it for a model.
-tryGetModel ::
-  Num.Solver ->
-  [TVar] ->   -- variables to try defaulting
-  [Prop] ->   -- constraints
-    IO (Maybe Subst)
-tryGetModel s xs ps =
-  -- We are only interested in finite instantiations
-  Num.getModel s (map (pFin . TVar) xs ++ ps)
 
 

src/Cryptol/TypeCheck/Solver/CrySAT.hs

@@ -1,696 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2013-2016 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
-
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-module Cryptol.TypeCheck.Solver.CrySAT
-  ( withScope, withSolver
-  , assumeProps, simplifyProps, getModel
-  , check
-  , Solver, logger, getIntervals
-  , DefinedProp(..)
-  , debugBlock
-  , DebugLog(..)
-  , knownDefined, numericRight
-  , minimizeContradictionSimpDef
-  , loadFile
-  , rawSolver
-  ) where
-
-import qualified Cryptol.TypeCheck.AST as Cry
-import           Cryptol.TypeCheck.InferTypes(Goal(..), SolverConfig(..))
-import qualified Cryptol.TypeCheck.Subst as Cry
-
-import           Cryptol.TypeCheck.Solver.Types
-import           Cryptol.TypeCheck.Solver.Numeric.AST
-import           Cryptol.TypeCheck.Solver.Numeric.Fin
-import           Cryptol.TypeCheck.Solver.Numeric.ImportExport
-import           Cryptol.TypeCheck.Solver.Numeric.Interval
-import           Cryptol.TypeCheck.Solver.Numeric.Defined
-import           Cryptol.TypeCheck.Solver.Numeric.Simplify
-import           Cryptol.TypeCheck.Solver.Numeric.NonLin
-import           Cryptol.TypeCheck.Solver.Numeric.SMT
-import           Cryptol.Utils.PP -- ( Doc )
-import           Cryptol.Utils.Panic ( panic )
-
-import           MonadLib
-import           Data.Maybe ( fromMaybe )
-import           Data.Map (Map)
-import qualified Data.Map as Map
-import           Data.Char(isSpace)
-import           Data.Foldable ( any, all )
-import qualified Data.Set as Set
-import           Data.IORef ( IORef, newIORef, readIORef, modifyIORef',
-                              atomicModifyIORef' )
-import           Prelude hiding (any,all)
-import qualified System.IO.Strict as StrictIO
-
-import qualified SimpleSMT as SMT
-
-
--- | We use this to remember what we simplified
-newtype SimpProp = SimpProp { unSimpProp :: Prop }
-
-simpProp :: Prop -> SimpProp
-simpProp p = SimpProp (crySimplify p)
-
-
-class    HasProp a        where getProp :: a -> Cry.Prop
-instance HasProp Cry.Prop where getProp  = id
-instance HasProp Goal     where getProp  = goal
-
-
--- | 'dpSimpProp' and 'dpSimpExprProp' should be logically equivalent,
--- to each other, and to whatever 'a' represents (usually 'a' is a 'Goal').
-data DefinedProp a = DefinedProp
-  { dpData         :: a
-    -- ^ Optional data to associate with prop.
-    -- Often, the original `Goal` from which the prop was extracted.
-
-  , dpSimpProp     :: SimpProp
-    {- ^ Fully simplified: may mention ORs, and named non-linear terms.
-    These are what we send to the prover, and we don't attempt to
-    convert them back into Cryptol types. -}
-
-  , dpSimpExprProp :: Prop
-    {- ^ A version of the proposition where just the expression terms
-    have been simplified.  These should not contain ORs or named non-linear
-    terms because we want to import them back into Crytpol types. -}
-  }
-
-knownDefined :: (a,Prop) -> DefinedProp a
-knownDefined (a,p) = DefinedProp
-  { dpData = a, dpSimpProp = simpProp p, dpSimpExprProp = p }
-
-
--- | Class goals go on the left, numeric goals go on the right.
-numericRight :: Goal -> Either Goal (Goal, Prop)
-numericRight g  = case exportProp (goal g) of
-                    Just p  -> Right (g, p)
-                    Nothing -> Left g
-
-
-
-
--- | Simplify a bunch of well-defined properties.
---  * Eliminates properties that are implied by the rest.
---  * Does not modify the set of assumptions.
-simplifyProps :: Solver -> [DefinedProp Goal] -> IO [Goal]
-simplifyProps s props =
-  debugBlock s "Simplifying properties" $
-  withScope s (go [] (eliminateSimpleGEQ props))
-  where
-  go survived [] = return survived
-
-  go survived (DefinedProp { dpSimpProp = SimpProp PTrue } : more) =
-                                                          go survived more
-
-  go survived (p : more) =
-    case dpSimpProp p of
-      SimpProp PTrue -> go survived more
-      SimpProp p' ->
-        do mbProved <- withScope s $
-             do mapM_ (assert s) more
-                e <- getIntervals s
-                case e of
-                  Left _     -> return Nothing
-                  Right ints -> do b <- prove s p'
-                                   return (Just (ints,b))
-           case mbProved of
-             Just (_,True)  -> go survived more
-
-             Just (ints,False) ->
-               debugLog s ("Using the fin solver:" ++ show (pp (goal (dpData p)))) >>
-               case cryIsFin ints (goal (dpData p)) of
-                 SolvedIf ps' ->
-                   do debugLog s "solved"
-                      let gg = dpData p
-                          gs' = [ gg { goal = pr } | pr <- ps' ]
-                      let more' = [ knownDefined g | Right g <- map numericRight gs' ]
-                      go survived (more' ++ more)
-                 Unsolved ->
-                   do debugLog s "unsolved"
-                      assert s p
-                      go (dpData p : survived) more
-
-                 x@(Unsolvable {}) ->
-                   do debugLog s (show (pp x))
-                      go (dpData p:survived) more
-
-             Nothing -> go (dpData p:survived) more
-
-
-{- | Simplify easy less-than-or-equal-to and equal-to goals.
-Those are common with long lists of literals, so we have special handling
-for them.  In particular:
-
-  * Reduce goals of the form @(a >= k1, a >= k2, a >= k3, ...)@ to
-   @a >= max (k1, k2, k3, ...)@, when all the k's are constant.
-
-  * Eliminate goals of the form @ki >= k2@, when @k2@ is leq than @k1@.
-
-  * Eliminate goals of the form @a >= 0@.
-
-NOTE:  This assumes that the goals are well-defined.
--}
-eliminateSimpleGEQ :: [DefinedProp a] -> [DefinedProp a]
-eliminateSimpleGEQ = go Map.empty []
-  where
-
-  go geqs other (g : rest) =
-    case dpSimpExprProp g of
-      K a :== K b
-        | a == b -> go geqs other rest
-
-      _ :>= K (Nat 0) ->
-          go geqs  other rest
-
-      K (Nat k1) :>= K (Nat k2)
-        | k1 >= k2 -> go geqs other rest
-
-      Var v :>= K (Nat k2) ->
-        go (addUpperBound v (k2,g) geqs) other rest
-
-      _ -> go geqs (g:other) rest
-
-  go geqs other [] = [ g | (_,g) <- Map.elems geqs ] ++ other
-
-  -- add in a possible upper bound for var
-  addUpperBound var g = Map.insertWith cmp var g
-    where
-    cmp a b | fst a > fst b = a
-            | otherwise     = b
-
-
-
-
-
--- | Add the given constraints as assumptions.
---  * We assume that the constraints are well-defined.
---  * Modifies the set of assumptions.
-assumeProps :: Solver -> [Cry.Prop] -> IO [SimpProp]
-assumeProps s props =
-  do let ps = [ (p,p') | p       <- props
-                       , Just p' <- [exportProp p] ]
-
-     let defPs = [ (p,cryDefinedProp p') | (p,p') <- ps ]
-
-     let simpProps = map knownDefined (defPs ++ ps)
-     mapM_ (assert s) simpProps
-     return (map dpSimpProp simpProps)
-  -- XXX: Instead of asserting one at a time, perhaps we should
-  -- assert a conjunction.  That way, we could simplify the whole thing
-  -- in one go, and would avoid having to assert 'true' many times.
-
-
-
-
--- | Given a list of propositions that together lead to a contradiction,
--- find a sub-set that still leads to a contradiction (but is smaller).
-minimizeContradictionSimpDef :: HasProp a => Solver -> [DefinedProp a] -> IO [a]
-minimizeContradictionSimpDef s ps = start [] ps
-  where
-  start bad todo =
-    do res <- SMT.check (solver s)
-       case res of
-         SMT.Unsat -> return (map dpData bad)
-         _         -> do solPush s
-                         go bad [] todo
-
-  go _ _ [] = panic "minimizeContradiction"
-               $ ("No contradiction" : map (show . ppProp . dpSimpExprProp) ps)
-  go bad prev (d : more) =
-    do assert s d
-       res <- SMT.check (solver s)
-       case res of
-         SMT.Unsat -> do solPop s
-                         assert s d
-                         start (d : bad) prev
-         _ -> go bad (d : prev) more
-
-
-
-{- | Attempt to find a substituion that, when applied, makes all of the
-given properties hold. -}
-getModel :: Solver -> [Cry.Prop] -> IO (Maybe Cry.Subst)
-getModel s props = withScope s $
-  do ps  <- assumeProps s props
-     res <- SMT.check (solver s)
-     let vars = Set.toList $ Set.unions $ map (cryPropFVS . unSimpProp) ps
-
-     case res of
-       SMT.Sat ->
-          do vs <- getVals (solver s) vars
-             -- This is guaranteed to be a model only for the *linear*
-             -- properties, so now we check if it works for the rest too.
-
-             let su1  = fmap K vs
-                 ps1  = [ fromMaybe p (apSubst su1 p) | SimpProp p <- ps ]
-                 ok p = case crySimplify p of
-                          PTrue -> True
-                          _     -> False
-
-                 su2 = Cry.listSubst
-                          [ (x, numTy v) | (UserName x, v) <- Map.toList vs ]
-
-             return (guard (all ok ps1) >> return su2)
-
-
-       _ -> return Nothing
-
-
-  where
-  numTy Inf     = Cry.tInf
-  numTy (Nat k) = Cry.tNum k
-
---------------------------------------------------------------------------------
-
-
--- | An SMT solver, and some info about declared variables.
-data Solver = Solver
-  { solver    :: SMT.Solver
-    -- ^ The actual solver
-
-  , declared  :: IORef VarInfo
-    -- ^ Information about declared variables, and assumptions in scope.
-
-  , logger    :: SMT.Logger
-    -- ^ For debugging
-  }
-
-loadFile :: Solver -> FilePath -> IO ()
-loadFile s file = go . dropComments =<< StrictIO.readFile file
-  where
-  go txt
-    | all isSpace txt = return ()
-    | otherwise = case SMT.readSExpr txt of
-                    Just (e,rest) -> SMT.command (solver s) e >> go rest
-                    Nothing       -> panic "loadFile" [ "Failed to parse SMT file."
-                                                      , txt
-                                                      ]
-
-  dropComments = unlines . map dropComment . lines
-  dropComment xs = case break (== ';') xs of
-                     (as,_:_) -> as
-                     _ -> xs
-
-rawSolver :: Solver -> SMT.Solver
-rawSolver = solver
-
-
-
--- | Keeps track of declared variables and non-linear terms.
-data VarInfo = VarInfo
-  { curScope    :: Scope
-  , otherScopes :: [Scope]
-  } deriving Show
-
-data Scope = Scope
-  { scopeNames    :: [Name]
-    -- ^ Variables declared in this scope (not counting the ones from
-    -- previous scopes).
-
-  , scopeNonLinS  :: NonLinS
-    {- ^ These are the non-linear terms mentioned in the assertions
-    that are currently asserted (including ones from previous scopes). -}
-
-  , scopeIntervals :: Either Cry.TVar (Map.Map Cry.TVar Interval)
-    -- ^ Either a type variable that makes the asserted properties unsatisfiable
-    -- (due to a broken interval), or the current set of intervals for type
-    -- variables. If a variable is not in the interval map, its value can be
-    -- anything.
-    --
-    -- This includes all intervals from previous scopes.
-
-  , scopeAsserted  :: [Cry.Prop]
-    -- ^ This is the set of currently-asserted cryptol properties only in this
-    -- scope.
-    --
-    -- This includes all asserted props from previous scopes.
-  } deriving Show
-
-scopeEmpty :: Scope
-scopeEmpty = Scope { scopeNames = [], scopeNonLinS = initialNonLinS
-                   , scopeIntervals = Right Map.empty, scopeAsserted = [] }
-
-scopeElem :: Name -> Scope -> Bool
-scopeElem x Scope { .. } = x `elem` scopeNames
-
-scopeInsert :: Name -> Scope -> Scope
-scopeInsert x Scope { .. } = Scope { scopeNames = x : scopeNames, .. }
-
-scopeAssertNew :: Cry.Prop -> Scope -> Scope
-scopeAssertNew prop Scope { .. } =
-  Scope { scopeIntervals = ints'
-        , scopeAsserted  = props
-        , .. }
-
-  where
-  props = prop : scopeAsserted
-  ints' = case scopeIntervals of
-            Left tv    -> Left tv
-            Right ints -> case computePropIntervals ints props of
-                            NoChange           -> scopeIntervals
-                            NewIntervals is    -> Right is
-                            InvalidInterval tv -> Left tv
-
-
--- | Given a *simplified* prop, separate linear and non-linear parts
--- and return the linear ones.
-scopeAssertSimpProp :: SimpProp -> Scope -> ([SimpProp],Scope)
-scopeAssertSimpProp (SimpProp p) Scope { .. } =
-  let (ps1,s1) = nonLinProp scopeNonLinS p
-  in (map SimpProp ps1, Scope { scopeNonLinS = s1, ..  })
-
-
-scopeAssert :: HasProp a => DefinedProp a -> Scope -> ([SimpProp],Scope)
-scopeAssert DefinedProp { .. } s =
-  let (ps1,s1) = scopeAssertSimpProp dpSimpProp s
-   in (ps1,scopeAssertNew (getProp dpData) s1)
-
-
--- | No scopes.
-viEmpty :: VarInfo
-viEmpty = VarInfo { curScope = scopeEmpty, otherScopes = [] }
-
--- | Check if a name is any of the scopes.
-viElem :: Name -> VarInfo -> Bool
-viElem x VarInfo { .. } = any (x `scopeElem`) (curScope : otherScopes)
-
--- | Add a name to a scope.
-viInsert :: Name -> VarInfo -> VarInfo
-viInsert x VarInfo { .. } = VarInfo { curScope = scopeInsert x curScope, .. }
-
--- | Add an assertion to the current scope. Returns the linear part.
-viAssertSimpProp :: SimpProp -> VarInfo -> (VarInfo, [SimpProp])
-viAssertSimpProp p VarInfo { .. } = ( VarInfo { curScope = s1, .. }, p1)
-  where (p1, s1) = scopeAssertSimpProp p curScope
-
-viAssert :: HasProp a => DefinedProp a -> VarInfo -> (VarInfo, [SimpProp])
-viAssert d VarInfo { .. } = (VarInfo { curScope = s1, .. },p1)
-  where (p1, s1) = scopeAssert d curScope
-
--- | Enter a scope.
-viPush :: VarInfo -> VarInfo
-viPush VarInfo { .. } =
-  VarInfo { curScope = scopeEmpty { scopeNonLinS   = scopeNonLinS curScope
-                                  , scopeAsserted  = scopeAsserted curScope
-                                  , scopeIntervals = scopeIntervals curScope }
-          , otherScopes = curScope : otherScopes
-          }
-
--- | Exit a scope.
-viPop :: VarInfo -> VarInfo
-viPop VarInfo { .. } = case otherScopes of
-                         c : cs -> VarInfo { curScope = c, otherScopes = cs }
-                         _ -> panic "viPop" ["no more scopes"]
-
-
--- | All declared names, that have not been "marked".
--- These are the variables whose values we are interested in.
-viUnmarkedNames :: VarInfo -> [ Name ]
-viUnmarkedNames VarInfo { .. } = concatMap scopeNames scopes
-  where scopes      = curScope : otherScopes
-
-
-getIntervals :: Solver -> IO (Either Cry.TVar (Map Cry.TVar Interval))
-getIntervals Solver { .. } =
-  do vi <- readIORef declared
-     return (scopeIntervals (curScope vi))
-
-
--- | All known non-linear terms.
-getNLSubst :: Solver -> IO Subst
-getNLSubst Solver { .. } =
-  do VarInfo { .. } <- readIORef declared
-     return $ nonLinSubst $ scopeNonLinS curScope
-
--- | Execute a computation with a fresh solver instance.
-withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
-withSolver SolverConfig { .. } k =
-  do logger <- if solverVerbose > 0 then SMT.newLogger 0 else return quietLogger
-
-
-     let smtDbg = if solverVerbose > 1 then Just logger else Nothing
-     solver <- SMT.newSolver solverPath solverArgs smtDbg
-     _ <- SMT.setOptionMaybe solver ":global-decls" "false"
-     -- SMT.setLogic solver "QF_LIA"
-     declared <- newIORef viEmpty
-     a <- k Solver { .. }
-     _ <- SMT.stop solver
-
-     return a
-
-  where
-  quietLogger = SMT.Logger { SMT.logMessage = \_ -> return ()
-                           , SMT.logLevel   = return 0
-                           , SMT.logSetLevel= \_ -> return ()
-                           , SMT.logTab     = return ()
-                           , SMT.logUntab   = return ()
-                           }
-
-solPush :: Solver -> IO ()
-solPush Solver { .. } =
-  do SMT.push solver
-     SMT.logTab logger
-     modifyIORef' declared viPush
-
-solPop :: Solver -> IO ()
-solPop Solver { .. } =
-  do modifyIORef' declared viPop
-     SMT.logUntab logger
-     SMT.pop solver
-
--- | Execute a computation in a new solver scope.
-withScope :: Solver -> IO a -> IO a
-withScope s k =
-  do solPush s
-     a <- k
-     solPop s
-     return a
-
--- | Declare a variable.
-declareVar :: Solver -> Name -> IO ()
-declareVar s@Solver { .. } a =
-  do done <- fmap (a `viElem`) (readIORef declared)
-     unless done $
-       do e  <- SMT.declare solver (smtName a)    SMT.tInt
-          let fin_a = smtFinName a
-          fin <- SMT.declare solver fin_a SMT.tBool
-          SMT.assert solver (SMT.geq e (SMT.int 0))
-
-          nlSu <- getNLSubst s
-          modifyIORef' declared (viInsert a)
-          case Map.lookup a nlSu of
-            Nothing -> return ()
-            Just e'  ->
-              do let finDef = crySimplify (Fin e')
-                 mapM_ (declareVar s) (Set.toList (cryPropFVS finDef))
-                 SMT.assert solver $
-                    SMT.eq fin (ifPropToSmtLib (desugarProp finDef))
-
-
-
--- | Add an assertion to the current context.
--- INVARIANT: Assertion is simplified.
-assert :: HasProp a => Solver -> DefinedProp a -> IO ()
-assert _               DefinedProp { dpSimpProp = SimpProp PTrue } = return ()
-assert s@Solver { .. } def@DefinedProp { dpSimpProp = p } =
-  do debugLog s ("Assuming: " ++ show (ppProp (unSimpProp p)))
-     a <- getIntervals s
-     debugLog s ("Intervals before:" ++ show (either pp ppIntervals a))
-     ps1' <- atomicModifyIORef' declared (viAssert def)
-     b <- getIntervals s
-     debugLog s ("Intervals after:" ++ show (either pp ppIntervals b))
-     let ps1 = map unSimpProp ps1'
-         vs  = Set.toList $ Set.unions $ map cryPropFVS ps1
-     mapM_ (declareVar s) vs
-     mapM_ (SMT.assert solver . ifPropToSmtLib . desugarProp) ps1
-
-
--- | Add an assertion to the current context.
--- INVARIANT: Assertion is simplified.
-assertSimpProp :: Solver -> SimpProp -> IO ()
-assertSimpProp _ (SimpProp PTrue) = return ()
-assertSimpProp s@Solver { .. } p@(SimpProp p0) =
-  do debugLog s ("Assuming: " ++ show (ppProp p0))
-     ps1' <- atomicModifyIORef' declared (viAssertSimpProp p)
-     let ps1 = map unSimpProp ps1'
-         vs  = Set.toList $ Set.unions $ map cryPropFVS ps1
-     mapM_ (declareVar s) vs
-     mapM_ (SMT.assert solver . ifPropToSmtLib . desugarProp) ps1
-
-
--- | Try to prove a property.  The result is 'True' when we are sure that
--- the property holds, and 'False' otherwise.  In other words, getting `False`
--- *does not* mean that the proposition does not hold.
-prove :: Solver -> Prop -> IO Bool
-prove _ PTrue  = return True
-prove s@Solver { .. } p =
-  debugBlock s ("Proving: " ++ show (ppProp p)) $
-  withScope s $
-  do assertSimpProp s (simpProp (Not p))
-     res <- SMT.check solver
-     case res of
-       SMT.Unsat   -> debugLog s "Proved" >> return True
-       SMT.Unknown -> debugLog s "Not proved" >> return False -- We are not sure
-       SMT.Sat     -> debugLog s "Not proved" >> return False
-        -- XXX: If the answer is Sat, it is possible that this is a
-        -- a fake example, as we need to evaluate the nonLinear constraints.
-        -- If they are all satisfied, then we have a genuine counter example.
-        -- Otherwise, we could look for another one...
-
-
-{- | Check if the current set of assumptions is satisfiable, and find
-some facts that must hold in any models of the current assumptions.
-
-Returns `Nothing` if the currently asserted constraints are known to
-be unsatisfiable.
-
-Returns `Just (su, sub-goals)` is the current set is satisfiable.
-  * The `su` is a substitution that may be applied to the current constraint
-    set without loosing generality.
-  * The `sub-goals` are additional constraints that must hold if the
-    constraint set is to be satisfiable.
--}
-check :: Solver -> IO (Maybe (Subst, [Prop]))
-check s@Solver { .. } =
-  do e <- getIntervals s
-     case e of
-
-       Left tv ->
-         do debugLog s ("Invalid interval: " ++ show (pp tv))
-            return Nothing
-
-       Right ints ->
-         do debugLog s ("Intervals:" ++ show (ppIntervals ints))
-            res <- SMT.check solver
-            case res of
-
-              SMT.Unsat   ->
-               do debugLog s "Not satisfiable"
-                  return Nothing
-
-              SMT.Unknown ->
-               do debugLog s "Unknown"
-                  return (Just (Map.empty, []))
-
-              SMT.Sat     ->
-               do debugLog s "Satisfiable"
-                  (impMap,sideConds) <- debugBlock s "Computing improvements"
-                                            (getImpSubst s)
-                  return (Just (impMap, sideConds))
-
-
-
-{- | Assuming that we are in a satisfiable state, try to compute an
-improving substitution.  We also return additional constraints that must
-hold for the currently asserted propositions to hold.
--}
-getImpSubst :: Solver -> IO (Subst,[Prop])
-getImpSubst s@Solver { .. } =
-  do names <- viUnmarkedNames `fmap` readIORef declared
-     m     <- getVals solver names
-     (impSu,sideConditions) <- cryImproveModel solver logger m
-
-     nlSu <- getNLSubst s
-
-     let isNonLinName (SysName {})  = True
-         isNonLinName (UserName {}) = False
-
-         (nlFacts, vFacts) = Map.partitionWithKey (\k _ -> isNonLinName k) impSu
-
-         (vV, vNL)  = Map.partition noNLVars vFacts
-
-         nlSu1  = fmap (doAppSubst vV) nlSu
-
-         (vNL_su,vNL_eqs) = Map.partitionWithKey goodDef
-                          $ fmap (doAppSubst nlSu1) vNL
-
-         nlSu2 = fmap (doAppSubst vNL_su) nlSu1
-         nlLkp x = case Map.lookup x nlSu2 of
-                     Just e  -> e
-                     Nothing -> panic "getImpSubst"
-                                [ "Missing NL variable:", show x ]
-
-         allSides =
-           [ Var a   :== e                  | (a,e) <- Map.toList vNL_eqs ] ++
-           [ nlLkp x :== doAppSubst nlSu2 e | (x,e) <- Map.toList nlFacts ] ++
-           [ doAppSubst nlSu2 si            | si    <- sideConditions ]
-
-         theImpSu = composeSubst vNL_su vV
-
-     debugBlock s "Improvments" $
-       do debugBlock s "substitution" $
-            mapM_ (debugLog s . dump) (Map.toList theImpSu)
-          debugBlock s "side-conditions" $ debugLog s allSides
-
-
-     return (theImpSu, allSides)
-
-
-  where
-  goodDef k e = not (k `Set.member` cryExprFVS e)
-
-  isNLVar (SysName _) = True
-  isNLVar _           = False
-
-  noNLVars e = all (not . isNLVar) (cryExprFVS e)
-
-  dump (x,e) = show (ppProp (Var x :== e))
-
---------------------------------------------------------------------------------
-
-debugBlock :: Solver -> String -> IO a -> IO a
-debugBlock s@Solver { .. } name m =
-  do debugLog s name
-     SMT.logTab logger
-     a <- m
-     SMT.logUntab logger
-     return a
-
-class DebugLog t where
-  debugLog :: Solver -> t -> IO ()
-
-  debugLogList :: Solver -> [t] -> IO ()
-  debugLogList s ts = case ts of
-                        [] -> debugLog s "(none)"
-                        _  -> mapM_ (debugLog s) ts
-
-instance DebugLog Char where
-  debugLog s x     = SMT.logMessage (logger s) (show x)
-  debugLogList s x = SMT.logMessage (logger s) x
-
-instance DebugLog a => DebugLog [a] where
-  debugLog = debugLogList
-
-instance DebugLog a => DebugLog (Maybe a) where
-  debugLog s x = case x of
-                   Nothing -> debugLog s "(nothing)"
-                   Just a  -> debugLog s a
-
-instance DebugLog Doc where
-  debugLog s x = debugLog s (show x)
-
-instance DebugLog Cry.Type where
-  debugLog s x = debugLog s (pp x)
-
-instance DebugLog Goal where
-  debugLog s x = debugLog s (goal x)
-
-instance DebugLog Cry.Subst where
-  debugLog s x = debugLog s (pp x)
-
-instance DebugLog Prop where
-  debugLog s x = debugLog s (ppProp x)
-
-
-

src/Cryptol/TypeCheck/Solver/Numeric/AST.hs

@@ -1,425 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2014-2016 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
---
--- The sytnax of numeric propositions.
-
-{-# LANGUAGE Safe #-}
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE DeriveGeneric #-}
-module Cryptol.TypeCheck.Solver.Numeric.AST
-  ( Name(..), ppName
-
-  , Prop(..), cryPropExprs, cryPropFVS
-  , ppProp, ppPropPrec
-
-  , Expr(..), zero, one, two, inf, cryAnds, cryOrs
-  , cryExprExprs, cryRebuildExpr
-  , cryExprFVS
-  , ppExpr, ppExprPrec
-
-  , Nat'(..)
-
-  , IfExpr, IfExpr'(..), ppIf, ppIfExpr
-
-  , Subst, HasVars(..), cryLet, composeSubst, doAppSubst
-  ) where
-
-import          Cryptol.TypeCheck.AST(TVar)
-import          Cryptol.TypeCheck.PP(pp)
-import          Cryptol.TypeCheck.Solver.InfNat ( Nat'(..) )
-import          Cryptol.Utils.PP ( Doc, text, (<+>), hang, ($$), char, (<>)
-                                 , parens, integer, sep )
-import          Cryptol.Utils.Panic ( panic )
-import          Cryptol.Utils.Misc ( anyJust )
-
--- import           Data.GenericTrie (TrieKey)
-import           GHC.Generics(Generic)
-import           Data.Maybe (fromMaybe)
-import           Data.Map ( Map )
-import qualified Data.Map as Map
-import           Data.Set ( Set )
-import qualified Data.Set as Set
-import qualified Control.Applicative as A
-import           Control.Monad ( liftM, ap )
-
-
-infixr 2 :||
-infixr 3 :&&
-infix  4 :==, :>, :>=, :==:, :>:
-infixl 6 :+, :-
-infixl 7 :*
-infixr 8 :^^
-
-
-
-data Name = UserName TVar | SysName Int
-            deriving (Show,Eq,Ord,Generic)
-
-
-
--- | Propopsitions, representing Cryptol's numeric constraints (and a bit more).
-data Prop =
-
-   -- Preidcates on natural numbers with infinity.
-   -- After simplification, the only one of these should be `fin x`,
-   -- where `x` is a variable.
-
-   Fin Expr | Expr :== Expr | Expr :>= Expr | Expr :> Expr
-
-
-  -- Predicate on strict natural numbers (i.e., no infinities)
-  -- Should be introduced by 'cryNatOp', to eliminte 'inf'.
-  | Expr :==: Expr | Expr :>: Expr
-
-  -- Standard logical strucutre>
-  | Prop :&& Prop | Prop :|| Prop
-  | Not Prop
-  | PFalse | PTrue
-    deriving (Eq,Show,Generic)
-
-
--- | Expressions, representing Cryptol's numeric types.
-data Expr = K Nat'
-          | Var Name
-          | Expr :+ Expr                  -- total
-          | Expr :- Expr                  -- partial: x >= y, fin y
-          | Expr :* Expr                  -- total
-          | Div Expr Expr                 -- partial: fin x, y >= 1
-          | Mod Expr Expr                 -- partial: fin x, y >= 1
-          | Expr :^^ Expr                 -- total
-          | Min Expr Expr                 -- total
-          | Max Expr Expr                 -- total
-          | Width Expr                    -- total
-          | LenFromThen   Expr Expr Expr  -- partial: x /= y, w >= width x
-          | LenFromThenTo Expr Expr Expr  -- partial: x /= y
-            deriving (Eq,Show,Generic,Ord)
-
-
--- | The constant @0@.
-zero :: Expr
-zero = K (Nat 0)
-
--- | The constant @1@.
-one :: Expr
-one = K (Nat 1)
-
--- | The constant @2@.
-two :: Expr
-two = K (Nat 2)
-
--- | The constant @infinity@.
-inf :: Expr
-inf = K Inf
-
-
--- | Make a conjucntion of the given properties.
-cryAnds :: [Prop] -> Prop
-cryAnds []  = PTrue
-cryAnds ps  = foldr1 (:&&) ps
-
--- | Make a disjunction of the given properties.
-cryOrs :: [Prop] -> Prop
-cryOrs []   = PFalse
-cryOrs ps   = foldr1 (:||) ps
-
-
-
-
--- | Compute all expressions in a property.
-cryPropExprs :: Prop -> [Expr]
-cryPropExprs = go []
-  where
-  go es prop =
-    case prop of
-      PTrue     -> es
-      PFalse    -> es
-      Not p     -> go es p
-      p :&& q   -> go (go es q) p
-      p :|| q   -> go (go es q) p
-
-      Fin x     -> x : es
-
-      x :== y   -> x : y : es
-      x :>  y   -> x : y : es
-      x :>= y   -> x : y : es
-
-      x :==: y  -> x : y : es
-      x :>:  y  -> x : y : es
-
-
--- | Compute the immediate sub-expressions of an expression.
-cryExprExprs :: Expr -> [Expr]
-cryExprExprs expr =
-  case expr of
-    K _                 -> []
-    Var _               -> []
-    x :+ y              -> [x,y]
-    x :- y              -> [x,y]
-    x :* y              -> [x,y]
-    Div x y             -> [x,y]
-    Mod x y             -> [x,y]
-    x :^^ y             -> [x,y]
-    Min x y             -> [x,y]
-    Max x y             -> [x,y]
-    Width x             -> [x]
-    LenFromThen   x y z -> [x,y,z]
-    LenFromThenTo x y z -> [x,y,z]
-
--- | Rebuild an expression, using the top-level strucutre of the first
--- expression, but the second list of expressions as sub-expressions.
-cryRebuildExpr :: Expr -> [Expr] -> Expr
-cryRebuildExpr expr args =
-  case (expr,args) of
-    (K _,   [])                     -> expr
-    (Var _, [])                     -> expr
-    (_ :+ _k, [x,y])                -> x :+ y
-    (_ :- _ , [x,y])                -> x :- y
-    (_ :* _ , [x,y])                -> x :* y
-    (Div _ _, [x,y])                -> Div x y
-    (Mod _ _, [x,y])                -> Mod x y
-    (_ :^^ _, [x,y])                -> x :^^ y
-    (Min _ _, [x,y])                -> Min x y
-    (Max _ _, [x,y])                -> Max x y
-    (Width _, [x])                  -> Width x
-    (LenFromThen   _ _ _ , [x,y,z]) -> LenFromThen x y z
-    (LenFromThenTo _ _ _ , [x,y,z]) -> LenFromThenTo x y z
-    _ -> panic "cryRebuildExpr" $ map show
-           $ text "expr:" <+> ppExpr expr
-           : [ text "arg:" <+> ppExpr a | a <- args ]
-
-
--- | Compute the free variables in an expression.
-cryExprFVS :: Expr -> Set Name
-cryExprFVS expr =
-  case expr of
-    Var x -> Set.singleton x
-    _     -> Set.unions (map cryExprFVS (cryExprExprs expr))
-
--- | Compute the free variables in a proposition.
-cryPropFVS :: Prop -> Set Name
-cryPropFVS = Set.unions . map cryExprFVS . cryPropExprs
-
-
-
-
-
-data IfExpr' p a = If p (IfExpr' p a) (IfExpr' p a) | Return a | Impossible
-                deriving Eq
-
-type IfExpr = IfExpr' Prop
-
-instance Monad (IfExpr' p) where
-  return  = Return
-  fail _  = Impossible
-  m >>= k = case m of
-              Impossible -> Impossible
-              Return a   -> k a
-              If p t e   -> If p (t >>= k) (e >>= k)
-
-instance Functor (IfExpr' p) where
-  fmap  = liftM
-
-instance A.Applicative (IfExpr' p) where
-  pure  = return
-  (<*>) = ap
-
-
---------------------------------------------------------------------------------
--- Substitution
---------------------------------------------------------------------------------
-
-type Subst = Map Name Expr
-
-composeSubst :: Subst -> Subst -> Subst
-composeSubst g f = Map.union f' g
-  where
-  f' = fmap (\e -> fromMaybe e (apSubst g e)) f
-
-cryLet :: HasVars e => Name -> Expr -> e -> Maybe e
-cryLet x e = apSubst (Map.singleton x e)
-
-doAppSubst :: HasVars a => Subst -> a -> a
-doAppSubst su a = fromMaybe a (apSubst su a)
-
--- | Replaces occurances of the name with the expression.
--- Returns 'Nothing' if there were no occurances of the name.
-class HasVars ast where
-  apSubst :: Subst -> ast -> Maybe ast
-
--- | This is used in the simplification to "apply" substitutions to Props.
-instance HasVars Bool where
-  apSubst _ _ = Nothing
-
-instance HasVars Expr where
-  apSubst su = go
-    where
-    go expr =
-      case expr of
-        K _                 -> Nothing
-        Var b               -> Map.lookup b su
-        x :+ y              -> bin (:+) x y
-        x :- y              -> bin (:-) x y
-        x :* y              -> bin (:*) x y
-        x :^^ y             -> bin (:^^) x y
-        Div x y             -> bin Div x y
-        Mod x y             -> bin Mod x y
-        Min x y             -> bin Min x y
-        Max x y             -> bin Max x y
-        Width x             -> Width `fmap` go x
-        LenFromThen x y w   -> three LenFromThen x y w
-        LenFromThenTo x y z -> three LenFromThen x y z
-
-    bin f x y = do [x',y'] <- anyJust go [x,y]
-                   return (f x' y')
-
-    three f x y z = do [x',y',z'] <- anyJust go [x,y,z]
-                       return (f x' y' z')
-
-instance HasVars Prop where
-  apSubst su = go
-    where
-    go prop =
-      case prop of
-        PFalse    -> Nothing
-        PTrue     -> Nothing
-        Not p     -> Not `fmap` go p
-        p :&& q   -> bin (:&&) p q
-        p :|| q   -> bin (:||) p q
-        Fin x     -> Fin `fmap` apSubst su x
-        x :== y   -> twoE (:==) x y
-        x :>= y   -> twoE (:>=) x y
-        x :> y    -> twoE (:>) x y
-        x :==: y  -> twoE (:==:) x y
-        x :>: y   -> twoE (:>) x y
-
-    bin f x y = do [x',y'] <- anyJust go [x,y]
-                   return (f x' y')
-
-    twoE f x y = do [x',y'] <- anyJust (apSubst su) [x,y]
-                    return (f x' y')
-
-
---------------------------------------------------------------------------------
--- Tries
---------------------------------------------------------------------------------
-
--- instance TrieKey Name
--- instance TrieKey Prop
--- instance TrieKey Expr
-
-
-
-
---------------------------------------------------------------------------------
--- Pretty Printing
---------------------------------------------------------------------------------
-
--- | Pretty print a name.
-ppName :: Name -> Doc
-ppName name =
-  case name of
-    UserName x -> pp x
-    SysName  x -> char '_' <> text (names !! x)
-
--- | An infinite list of names, for pretty prinitng.
-names :: [String]
-names  = concatMap gen [ 0 :: Integer .. ]
-  where
-  gen x  = [ a : suff x | a <- [ 'a' .. 'z' ] ]
-
-  suff 0 = ""
-  suff x = show x
-
-
-
--- | Pretty print a top-level property.
-ppProp :: Prop -> Doc
-ppProp = ppPropPrec 0
-
--- | Pretty print a proposition, in the given precedence context.
-ppPropPrec :: Int -> Prop -> Doc
-ppPropPrec prec prop =
-  case prop of
-    Fin x     -> fun "fin" ppExprPrec x
-    x :== y   -> bin "==" 4 1 1 ppExprPrec x y
-    x :>= y   -> bin ">=" 4 1 1 ppExprPrec x y
-    x :> y    -> bin ">"  4 1 1 ppExprPrec x y
-
-    x :==: y  -> bin "==#" 4 1 1 ppExprPrec x y
-    x :>: y   -> bin ">#"  4 1 1 ppExprPrec x y
-
-    p :&& q   -> bin "&&" 3 1 0 ppPropPrec p q
-    p :|| q   -> bin "||" 2 1 0 ppPropPrec p q
-    Not p     -> fun "not" ppPropPrec p
-    PTrue     -> text "True"
-    PFalse    -> text "False"
-
-  where
-  wrap p d = if prec > p then parens d else d
-
-  fun f how x = wrap 10 (text f <+> how 11 x)
-
-  bin op opP lMod rMod how x y =
-    wrap opP (sep [ how (opP + lMod) x, text op, how (opP + rMod) y ])
-
-
-
--- | Pretty print an expression at the top level.
-ppExpr :: Expr -> Doc
-ppExpr = ppExprPrec 0
-
--- | Pretty print an expression, in the given precedence context.
-ppExprPrec :: Int -> Expr -> Doc
-ppExprPrec prec expr =
-  case expr of
-    K Inf               -> text "inf"
-    K (Nat n)           -> integer n
-    Var a               -> ppName a
-    x :+ y              -> bin "+" 6 0 1 x y
-    x :- y              -> bin "-" 6 0 1 x y
-    x :* y              -> bin "*" 7 0 1 x y
-    Div x y             -> fun "div" [x,y]
-    Mod x y             -> fun "mod" [x,y]
-    x :^^ y             -> bin "^^" 8 1 0 x y
-    Min x y             -> fun "min" [x,y]
-    Max x y             -> fun "max" [x,y]
-    Width x             -> fun "width" [x]
-    LenFromThen x y w   -> fun "lenFromThen" [x,y,w]
-    LenFromThenTo x y z -> fun "lenFromThenTo" [x,y,z]
-
-  where
-  wrap p d = if prec > p then parens d else d
-
-  fun f xs = wrap 10 (text f <+> sep (map (ppExprPrec 11) xs))
-
-  bin op opP lMod rMod x y =
-    wrap opP
-      (ppExprPrec (opP + lMod) x <+> text op <+> ppExprPrec (opP + rMod) y)
-
-
-
--- | Pretty print an experssion with ifs.
-ppIfExpr :: IfExpr Expr -> Doc
-ppIfExpr = ppIf ppProp ppExpr
-
--- | Pretty print an experssion with ifs.
-ppIf :: (p -> Doc) -> (a -> Doc) -> IfExpr' p a -> Doc
-ppIf ppAtom ppVal = go
-  where
-  go expr =
-    case expr of
-      If p t e -> hang (text "if" <+> ppAtom p) 2
-                ( (text "then" <+> go t)  $$
-                  (text "else" <+> go e)
-                )
-      Return e    -> ppVal e
-      Impossible  -> text "<impossible>"
-
-
-

src/Cryptol/TypeCheck/Solver/Numeric/Defined.hs

@@ -1,55 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2014-2016 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
-
-{-# LANGUAGE Safe #-}
-module Cryptol.TypeCheck.Solver.Numeric.Defined where
-
-import Cryptol.TypeCheck.Solver.Numeric.AST
-import Cryptol.Utils.Panic ( panic )
-
--- | A condition ensure that the given *basic* proposition makes sense.
-cryDefinedProp :: Prop -> Prop
-cryDefinedProp prop =
-  case prop of
-    Fin x   -> cryDefined x
-    x :== y -> cryDefined x :&& cryDefined y
-    x :>= y -> cryDefined x :&& cryDefined y
-    Not p   -> cryDefinedProp p
-    _ -> panic "cryDefinedProp" [ "Not a simple property:"
-                                , show (ppProp prop)
-                                ]
-
-
--- | Generate a property ensuring that the expression is well-defined.
--- This might be a bit too strict.  For example, we reject things like
--- @max inf (0 - 1)@, which one might think would simplify to @inf@.
-cryDefined :: Expr -> Prop
-cryDefined expr =
-  case expr of
-    K _       -> PTrue
-    Var _     -> PTrue    -- Variables are always assumed to be OK.
-                      -- The idea is that we are going to check for
-                      -- defined-ness before instantiating variables.
-    x :+ y    -> cryDefined x :&& cryDefined y
-    x :- y    -> cryDefined x :&& cryDefined y :&&
-                 Fin y :&& x :>= y
-    x :* y    -> cryDefined x :&& cryDefined y
-    Div x y   -> cryDefined x :&& cryDefined y :&&
-                 Fin x :&& y :>= K (Nat 1)
-    Mod x y   -> cryDefined x :&& cryDefined y :&&
-                 Fin x :&& y :>= K (Nat 1)
-    x :^^ y   -> cryDefined x :&& cryDefined y
-    Min x y   -> cryDefined x :&& cryDefined y
-    Max x y   -> cryDefined x :&& cryDefined y
-    Width x   -> cryDefined x
-    LenFromThen x y w ->
-      cryDefined x :&& cryDefined y :&& cryDefined w :&&
-      Fin x :&& Fin y :&& Fin w :&& Not (x :== y) :&& w :>= Width x
-    LenFromThenTo x y z ->
-      cryDefined x :&& cryDefined y :&& cryDefined z :&&
-      Fin x :&& Fin y :&& Fin z :&& Not (x :== y)

src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs

@@ -1,171 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2014-2016 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
-
-{-# LANGUAGE Safe #-}
-module Cryptol.TypeCheck.Solver.Numeric.ImportExport
-  ( ExportM
-  , exportProp
-  , exportType
-  , runExportM
-  , exportPropM
-  , exportTypeM
-  , importProp
-  , importType
-  ) where
-
-import           Cryptol.TypeCheck.Solver.Numeric.AST
-import qualified Cryptol.TypeCheck.AST as Cry
-import qualified Cryptol.TypeCheck.SimpType as SCry
-import           MonadLib
-
-exportProp :: Cry.Prop -> Maybe Prop
-exportProp = runExportM . exportPropM
-
-exportType :: Cry.Prop -> Maybe Expr
-exportType = runExportM . exportTypeM
-
-runExportM :: ExportM a -> Maybe a
-runExportM = either (\_ -> Nothing) Just
-           . runId
-           . runExceptionT
-
-type ExportM = ExceptionT () Id
-
-exportPropM :: Cry.Prop -> ExportM Prop
-exportPropM ty =
-  case ty of
-    Cry.TUser _ _ t -> exportPropM t
-    Cry.TRec {}     -> raise ()
-    Cry.TVar {}     -> raise ()
-    Cry.TCon (Cry.PC pc) ts ->
-      mapM exportTypeM ts >>= \ets ->
-      case (pc, ets) of
-        (Cry.PFin,   [t])     -> return (Fin t)
-        (Cry.PEqual, [t1,t2]) -> return (t1 :== t2)
-        (Cry.PNeq,   [t1,t2]) -> return (Not (t1 :== t2))
-        (Cry.PGeq,   [t1,t2]) -> return (t1 :>= t2)
-        _                     -> raise ()
-    Cry.TCon _ _ -> raise ()
-
-exportTypeM :: Cry.Type -> ExportM Expr
-exportTypeM ty =
-  case ty of
-    Cry.TUser _ _ t -> exportTypeM t
-    Cry.TRec {}     -> raise ()
-    Cry.TVar x      -> return $ Var $ UserName x
-    Cry.TCon tc ts  ->
-      case tc of
-        Cry.TError {} -> raise ()
-
-        Cry.TC Cry.TCInf     -> return (K Inf)
-        Cry.TC (Cry.TCNum x) -> return (K (Nat x))
-        Cry.TC _             -> raise ()
-
-        Cry.TF f ->
-          mapM exportTypeM ts >>= \ets ->
-          case (f, ets) of
-            (Cry.TCAdd, [t1,t2]) -> return (t1 :+ t2)
-            (Cry.TCSub, [t1,t2]) -> return (t1 :- t2)
-            (Cry.TCMul, [t1,t2]) -> return (t1 :* t2)
-            (Cry.TCDiv, [t1,t2]) -> return (Div t1 t2)
-            (Cry.TCMod, [t1,t2]) -> return (Mod t1 t2)
-            (Cry.TCExp, [t1,t2]) -> return (t1 :^^ t2)
-            (Cry.TCMin, [t1,t2]) -> return (Min t1 t2)
-            (Cry.TCMax, [t1,t2]) -> return (Max t1 t2)
-            (Cry.TCWidth, [t1])  -> return (Width t1)
-            (Cry.TCLenFromThen,   [t1,t2,t3]) -> return (LenFromThen   t1 t2 t3)
-            (Cry.TCLenFromThenTo, [t1,t2,t3]) -> return (LenFromThenTo t1 t2 t3)
-
-            _ -> raise ()
-
-        Cry.PC _ -> raise ()
-
-importProp :: Prop -> Maybe [Cry.Prop]
-importProp prop =
-  case prop of
-    PFalse    -> Nothing
-    PTrue     -> Just []
-
-    Not p     -> importProp =<< pNot p
-    p1 :&& p2 -> do ps1 <- importProp p1
-                    ps2 <- importProp p2
-                    return (ps1 ++ ps2)
-    _  :|| _  -> Nothing
-
-    Fin expr -> do t <- importType expr
-                   return [ Cry.pFin t ]
-
-    e1 :==  e2 -> do t1 <- importType e1
-                     t2 <- importType e2
-                     return [t1 Cry.=#= t2]
-    e1 :>=  e2 -> do t1 <- importType e1
-                     t2 <- importType e2
-                     return [t1 Cry.>== t2]
-    _ :> _     -> Nothing
-    e1 :==: e2 -> do t1 <- importType e1
-                     t2 <- importType e2
-                     -- XXX: Do we need to add fin?
-                     return [t1 Cry.=#= t2]
-    _ :>: _    -> Nothing
-
-  where
-  pNot p =
-    case p of
-      PFalse  -> Just PTrue
-      PTrue   -> Nothing
-
-      Not a   -> Just a
-      _ :&& _ -> Nothing
-      a :|| b -> Just (Not a :&& Not b)
-
-      Fin a    -> Just (a :== K Inf)
-      _ :== _  -> Nothing
-      _ :>= _  -> Nothing
-      a :>  b  -> Just (b :>= a)
-      _ :==: _ -> Nothing
-      a :>: b  -> Just (b :>= a)
-      -- XXX: Do we need to add Fin on `a` and 'b'?
-
-
-importType :: Expr -> Maybe Cry.Type
-importType = go
-  where
-  go expr =
-    case expr of
-      Var x               -> case x of
-                               UserName v -> return (Cry.TVar v)
-                               _          -> Nothing
-      K n                 -> case n of
-                               Nat x -> Just (Cry.tNum x)
-                               Inf   -> Just (Cry.tInf)
-      x :+ y              -> op2 SCry.tAdd x y
-      x :- y              -> op2 SCry.tSub x y
-      x :* y              -> op2 SCry.tMul x y
-      Div x y             -> op2 SCry.tDiv x y
-      Mod x y             -> op2 SCry.tMod x y
-      x :^^ y             -> op2 SCry.tExp x y
-      Min x y             -> op2 SCry.tMin x y
-      Max x y             -> op2 SCry.tMax x y
-      Width x             -> op1 SCry.tWidth x
-      LenFromThen   x y z -> op3 SCry.tLenFromThen x y z
-      LenFromThenTo x y z -> op3 SCry.tLenFromThenTo x y z
-
-  op1 f x =
-    do t <- go x
-       return (f t)
-
-  op2 f x y =
-    do t1 <- go x
-       t2 <- go y
-       return (f t1 t2)
-
-  op3 f x y z =
-    do t1 <- go x
-       t2 <- go y
-       t3 <- go z
-       return (f t1 t2 t3)

src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs

@@ -1,281 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2014-2016 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
---
--- Separate Non-Linear Constraints
--- When we spot a non-linear expression, we name it and add it to a map.
---
--- If we see the same expression multiple times, then we give it the same name.
---
--- The body of the non-linear expression is not processed further,
--- so the resulting map should not contain any of the newly minted names.
-
-{-# LANGUAGE Safe, RecordWildCards #-}
-
-module Cryptol.TypeCheck.Solver.Numeric.NonLin
-  ( nonLinProp
-  , NonLinS, nonLinSubst
-  , initialNonLinS
-  , apSubstNL
-  , lookupNL
-  ) where
-
-import Cryptol.TypeCheck.Solver.Numeric.AST
-import Cryptol.TypeCheck.Solver.Numeric.Simplify
-import Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr
-import Cryptol.Utils.Panic(panic)
-
--- import           Data.GenericTrie (Trie)
--- import qualified Data.GenericTrie as Trie
-import           Data.Maybe ( fromMaybe )
-import           MonadLib
-import           Data.Map (Map)
-import qualified Data.Map as Map
-
-type Trie   = Map
-
-trie_empty :: Map k a
-trie_empty  = Map.empty
-
-trie_insert :: Expr -> a -> Map Expr a -> Map Expr a
-trie_insert = Map.insert
-
-trie_delete :: Expr -> Map Expr a -> Map Expr a
-trie_delete = Map.delete
-
-trie_lookup :: Expr -> Map Expr a -> Maybe a
-trie_lookup = Map.lookup
-
-
--- | Factor-out non-linear terms, by naming them.
-nonLinProp :: NonLinS -> Prop -> ([Prop], NonLinS)
-nonLinProp s0 prop = (p : ps, s)
-  where ((p,ps),s) = runNL s0 (nonLinPropM prop)
-
-{- | Apply a substituin to the non-linear expression database.
-Returns `Nothing` if nothing was affected.
-Otherwise returns `Just`, and a substitution for non-linear expressions
-that became linear.
-
-The definitions of NL terms do not contain other named NL terms,
-so it does not matter if the substitution contains bindings like @_a = e@.
-
-There should be no bindings that mention NL term names in the definitions
-of the substition (i.e, things like @x = _a@ are NOT ok).
--}
-apSubstNL :: Subst -> NonLinS -> Maybe (Subst, [Prop], NonLinS)
-apSubstNL su s0 = case runNL s0 (mApSubstNL su) of
-                    ((Nothing,_),_) -> Nothing
-                    ((Just su1,ps),r) -> Just (su1,ps,r)
-
-lookupNL :: Name -> NonLinS -> Maybe Expr
-lookupNL x NonLinS { .. } = Map.lookup x nonLinExprs
-
-
-runNL :: NonLinS -> NonLinM a -> ((a, [Prop]), NonLinS)
-runNL s m = runId
-          $ runStateT s
-          $ do a  <- m
-               ps <- finishTodos
-               return (a,ps)
-
--- | Get the known non-linear terms.
-nonLinSubst :: NonLinS -> Subst
-nonLinSubst = nonLinExprs
-
--- | The initial state for the linearization process.
-initialNonLinS :: NonLinS
-initialNonLinS = NonLinS
-  { nextName = 0
-  , nonLinExprs = Map.empty
-  , nlKnown = trie_empty
-  , nlTodo = []
-  }
-
-
-data SubstOneRes = NoChange
-                   -- ^ Substitution does not affect the expression.
-
-                 | Updated (Maybe (Name,Expr))
-                   -- ^ The expression was updated and, maybe, it became linear.
-
-
-{- | Apply the substituint to all non-linear bindings.
-Returns `Nothing` if nothing was affected.
-Otherwise returns `Just`, and a substituion mapping names that used
-to be non-linear but became linear.
-
-Note that we may return `Just empty`, indicating that some non-linear
-expressions were updated, but they remained non-linear. -}
-mApSubstNL :: Subst -> NonLinM (Maybe Subst)
-mApSubstNL su =
-  do s <- get
-     answers <- mapM (mApSubstOneNL su) (Map.toList (nonLinExprs s))
-     return (foldr upd Nothing answers)
-  where
-  upd NoChange ch     = ch
-  upd (Updated mb) ch = let lsu = fromMaybe Map.empty ch
-                        in Just (case mb of
-                                   Nothing    -> lsu
-                                   Just (x,e) -> Map.insert x e lsu)
-
-
-mApSubstOneNL :: Subst -> (Name,Expr) -> NonLinM SubstOneRes
-mApSubstOneNL su (x,e) =
-  case apSubst su e of
-    Nothing -> return NoChange
-    Just e1 ->
-      case crySimpExprMaybe e1 of
-
-        Nothing ->
-          sets $ \NonLinS { .. } ->
-            ( Updated Nothing
-            , NonLinS { nonLinExprs = Map.insert x e1 nonLinExprs
-                      , nlKnown = trie_insert e1 x (trie_delete e nlKnown)
-                      , .. }
-            )
-
-        Just e2
-          | isNonLinOp e2 ->
-          sets $ \NonLinS { .. } ->
-            (Updated Nothing
-            , NonLinS { nonLinExprs = Map.insert x e2 nonLinExprs
-                      , nlKnown = trie_insert e2 x (trie_delete e nlKnown)
-                      , .. }
-            )
-
-          | otherwise ->
-            do sets_ $ \NonLinS { .. } ->
-                 NonLinS { nonLinExprs = Map.delete x nonLinExprs
-                         , nlKnown = trie_delete e nlKnown
-                         , ..
-                         }
-               es <- mapM nonLinExprM (cryExprExprs e2)
-               let e3 = cryRebuildExpr e2 es
-               return (Updated (Just (x,e3)))
-
-
-
--- | Is the top-level operator a non-linear one.
-isNonLinOp :: Expr -> Bool
-isNonLinOp expr =
-  case expr of
-    K _   -> False
-    Var _ -> False
-
-    _ :+ _ -> False
-
-    _ :- _ -> False
-
-    x :* y ->
-      case (x,y) of
-        (K _, _)  -> False
-        (_, K _)  -> False
-        _         -> True
-
-    Div _ y ->
-      case y of
-        K (Nat n) -> n == 0
-        _         -> True
-
-    Mod _ y ->
-      case y of
-        K (Nat n) -> n == 0
-        _         -> True
-
-    _ :^^ _       -> True
-
-    Min _ _       -> False
-
-    Max _ _       -> False
-
-    Width _       -> True
-
-    LenFromThen _ _ _ -> True -- See also comment on `LenFromThenTo`
-
-    LenFromThenTo x y _ ->
-      case (x,y) of
-        (K _, K _) -> False
-        _          -> True    -- Actually, as long as the difference bettwen
-                              -- `x` and `y` is constant we'd be OK, but not
-                              -- sure how to do that...
-
-nlImplied :: Expr -> Name -> [Prop]
-nlImplied expr x =
-  map crySimplify $
-  case expr of
-    K (Nat n) :^^ e | n >= 2 -> [ Var x :>= one, Var x :>= e :+ one ]
-    Mod _ e                  -> [ e     :>= Var x :+ one ]
-
-    _                        -> []
-
-
-
-
-nonLinPropM :: Prop -> NonLinM Prop
-nonLinPropM prop =
-  case prop of
-    PFalse      -> return PFalse
-    PTrue       -> return PTrue
-    Not p       -> Not   `fmap` nonLinPropM p
-    p :&& q     -> (:&&) `fmap` nonLinPropM p `ap` nonLinPropM q
-    p :|| q     -> (:||) `fmap` nonLinPropM p `ap` nonLinPropM q
-    Fin (Var _) -> return prop
-    Fin _       -> unexpected
-    x :==: y    -> (:==:) `fmap` nonLinExprM x `ap` nonLinExprM y
-    x :>: y     -> (:>:)  `fmap` nonLinExprM x `ap` nonLinExprM y
-
-    _ :== _     -> unexpected
-    _ :>= _     -> unexpected
-    _ :> _      -> unexpected
-
-  where
-  unexpected = panic "nonLinPropM" [ show (ppProp prop) ]
-
-
-
-nonLinExprM :: Expr -> NonLinM Expr
-nonLinExprM expr
-  | isNonLinOp expr = nameExpr expr
-  | otherwise = cryRebuildExpr expr `fmap` mapM nonLinExprM (cryExprExprs expr)
-
-
-
-type NonLinM = StateT NonLinS Id
-
-data NonLinS = NonLinS
-  { nextName    :: !Int
-  , nonLinExprs :: Subst
-  , nlKnown     :: Trie Expr Name
-  , nlTodo      :: [Prop]
-  } deriving Show
-
-nameExpr :: Expr -> NonLinM Expr
-nameExpr e = sets $ \s ->
-  case trie_lookup e (nlKnown s) of
-    Just x -> (Var x, s)
-    Nothing ->
-      let x  = nextName s
-          n  = SysName x
-          s1 = NonLinS { nextName = 1 + x
-                       , nonLinExprs = Map.insert n e (nonLinExprs s)
-                       , nlKnown = trie_insert e n (nlKnown s)
-                       , nlTodo = nlImplied e n ++ nlTodo s
-                       }
-      in (Var n, s1)
-
-
-finishTodos :: NonLinM [Prop]
-finishTodos =
-  do s <- get
-     case nlTodo s of
-       [] -> return []
-       p : ps ->
-        do set s { nlTodo = ps }
-           p'  <- nonLinPropM p
-           ps' <- finishTodos
-           return (p' : ps')

src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs

@@ -1,517 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2014-2016 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
---
--- Desugar into SMTLIB Terminology
-
-{-# LANGUAGE Safe #-}
-
-module Cryptol.TypeCheck.Solver.Numeric.SMT
-  ( desugarProp
-  , smtName
-  , smtFinName
-  , ifPropToSmtLib
-  , cryImproveModel
-  , getVal
-  , getVals
-  ) where
-
-import           Cryptol.TypeCheck.AST (TVar(TVFree,TVBound))
-import           Cryptol.TypeCheck.Solver.InfNat
-import           Cryptol.TypeCheck.Solver.Numeric.AST
-import           Cryptol.TypeCheck.Solver.Numeric.Simplify(crySimplify)
-import           Cryptol.Utils.Misc ( anyJust )
-import           Cryptol.Utils.Panic ( panic )
-
-import           Data.List ( partition, unfoldr )
-import           Data.Map ( Map )
-import qualified Data.Map as Map
-import qualified Data.Set as Set
-import           SimpleSMT ( SExpr )
-import qualified SimpleSMT as SMT
-import           MonadLib
-
-
---------------------------------------------------------------------------------
--- Desugar to SMT
---------------------------------------------------------------------------------
-
--- XXX: Expanding the if-then-elses could make things large.
--- Perhaps keep them as first class things, in hope that the solver
--- can do something more clever with that?
-
-
--- | Assumes simplified, linear, finite, defined expressions.
-desugarExpr :: Expr -> IfExpr Expr
-desugarExpr expr =
-  do es <- mapM desugarExpr (cryExprExprs expr)
-     case (expr,es) of
-       (Min {}, [x,y]) -> If (x :>: y) (return y) (return x)
-       (Max {}, [x,y]) -> If (x :>: y) (return x) (return y)
-       (LenFromThenTo {}, [ x@(K (Nat a)), K (Nat b), z ])
-
-          -- going down
-          | a > b -> If (z :>: x) (return zero)
-                                  (return (Div (x :- z) step :+ one))
-
-          -- goind up
-          | b > a -> If (x :>: z) (return zero)
-                                  (return (Div (z :- x) step :+ one))
-
-          where step = K (Nat (abs (a - b)))
-
-       _ -> return (cryRebuildExpr expr es)
-
-
--- | Assumes simplified, linear, defined.
-desugarProp :: Prop -> IfExpr Prop
-desugarProp prop =
-  case prop of
-    PFalse      -> return PFalse
-    PTrue       -> return PTrue
-    Not p       -> Not   `fmap` desugarProp p
-    p :&& q     -> (:&&) `fmap` desugarProp p `ap` desugarProp q
-    p :|| q     -> (:||) `fmap` desugarProp p `ap` desugarProp q
-    Fin (Var _) -> return prop
-    x :==: y    -> (:==:) `fmap` desugarExpr x `ap` desugarExpr y
-    x :>: y     -> (:>:)  `fmap` desugarExpr x `ap` desugarExpr y
-
-    Fin _     -> unexpected
-    _ :== _   -> unexpected
-    _ :>= _   -> unexpected
-    _ :> _    -> unexpected
-
-  where
-  unexpected = panic "desugarProp" [ show (ppProp prop) ]
-
-
-ifPropToSmtLib :: IfExpr Prop -> SExpr
-ifPropToSmtLib ifProp =
-  case ifProp of
-    Impossible -> SMT.bool False -- Sholdn't really matter
-    Return p   -> propToSmtLib p
-    If p q r   -> SMT.ite (propToSmtLib p) (ifPropToSmtLib q) (ifPropToSmtLib r)
-
-propToSmtLib :: Prop -> SExpr
-propToSmtLib prop =
-  case prop of
-    PFalse       -> SMT.bool False
-    PTrue        -> SMT.bool True
-    Not p        -> case p of
-                      Fin _   -> SMT.not (propToSmtLib p)
-
-                      -- It is IMPORTANT that the fin constraints are outside
-                      -- the not.
-                      x :>: y -> addFin $ SMT.geq (exprToSmtLib y)
-                                                  (exprToSmtLib x)
-                      _ -> unexpected
-
-
-    p :&& q     -> SMT.and (propToSmtLib p) (propToSmtLib q)
-    p :|| q     -> SMT.or  (propToSmtLib p) (propToSmtLib q)
-    Fin (Var x) -> fin x
-
-    {- For the linear constraints, if the term is finite, then all of
-       its variables must have been finite.
-
-       XXX: Adding the `fin` decls at the leaves leads to some duplication:
-       We could add them just once for each conjunctoin of simple formulas,
-       but I am not sure how much this matters.
-    -}
-    x :==: y    -> addFin $ SMT.eq (exprToSmtLib x) (exprToSmtLib y)
-    x :>: y     -> addFin $ SMT.gt (exprToSmtLib x) (exprToSmtLib y)
-
-    Fin _       -> unexpected
-    _ :== _     -> unexpected
-    _ :>= _     -> unexpected
-    _ :> _      -> unexpected
-
-  where
-  unexpected = panic "propToSmtLib" [ show (ppProp prop) ]
-  fin x      = SMT.const (smtFinName x)
-
-  addFin e   = foldr (\x' e' -> SMT.and (fin x') e') e
-                     (Set.toList (cryPropFVS prop))
-
-exprToSmtLib :: Expr -> SExpr
-exprToSmtLib expr =
-
-  case expr of
-    K (Nat n)           -> SMT.int n
-    Var a               -> SMT.const (smtName a)
-    x :+ y              -> SMT.add (exprToSmtLib x) (exprToSmtLib y)
-    x :- y              -> SMT.sub (exprToSmtLib x) (exprToSmtLib y)
-    x :* y              -> SMT.mul (exprToSmtLib x) (exprToSmtLib y)
-    Div x y             -> SMT.div (exprToSmtLib x) (exprToSmtLib y)
-    Mod x y             -> SMT.mod (exprToSmtLib x) (exprToSmtLib y)
-
-    K Inf               -> unexpected
-    _ :^^ _             -> unexpected
-    Min {}              -> unexpected
-    Max {}              -> unexpected
-    Width {}            -> unexpected
-    LenFromThen {}      -> unexpected
-    LenFromThenTo {}    -> unexpected
-
-  where
-  unexpected = panic "exprToSmtLib" [ show (ppExpr expr) ]
-
-
--- | The name of a variable in the SMT translation.
-smtName :: Name -> String
-smtName a = case a of
-              SysName n -> name "s" n
-              UserName tv -> case tv of
-                               TVFree n _ _ _ -> name "u" n
-                               TVBound n _    -> name "k" n
-
-  where
-  name p n = case divMod n 26 of
-               (q,r) -> p ++ toEnum (fromEnum 'a' + r) :
-                              (if q == 0 then "" else show q)
-
-
--- | The name of a boolean variable, representing `fin x`.
-smtFinName :: Name -> String
-smtFinName x = "fin_" ++ smtName x
-
-
-
-
-
---------------------------------------------------------------------------------
--- Models
---------------------------------------------------------------------------------
-
-{- | Get the value for the given name.
-      * Assumes that we are in a SAT state (i.e., there is a model)
-      * Assumes that the name is in the model -}
-getVal :: SMT.Solver -> Name -> IO Nat'
-getVal s a =
-  do yes <- isInf a
-     if yes
-       then return Inf
-       else do v <- SMT.getConst s (smtName a)
-               case v of
-                 SMT.Int x | x >= 0 -> return (Nat x)
-                 _ -> panic "cryCheck.getVal" [ "Not a natural number", show v ]
-
-  where
-  isInf v = do yes <- SMT.getConst s (smtFinName v)
-               case yes of
-                 SMT.Bool ans -> return (not ans)
-                 _            -> panic "cryCheck.isInf"
-                                       [ "Not a boolean value", show yes ]
-
-
--- | Get the values for the given names.
-getVals :: SMT.Solver -> [Name] -> IO (Map Name Nat')
-getVals s xs =
-  do es <- mapM (getVal s) xs
-     return (Map.fromList (zip xs es))
-
-
--- | Convert a bunch of improving equations into an idempotent substitution.
--- Assumes that the equations don't have loops.
-toSubst :: Map Name Expr -> Subst
-toSubst m0 = last (m0 : unfoldr step m0)
-  where step m = do m1 <- anyJust (apSubst m) m
-                    return (m1,m1)
-
-
-{- | Given a model, compute an improving substitution, implied by the model.
-The entries in the substitution look like this:
-
-  * @x = A@         variable @x@ must equal constant @A@
-
-  * @x = y@         variable @x@ must equal variable @y@
-
-  * @x = A * y + B@ (coming soon)
-                    variable @x@ is a linear function of @y@,
-                    @A@ and @B@ are natural numbers.
--}
-
-
-
-{- | We are mostly interested in improving unification variables.
-However, it is also useful to improve skolem variables, as this could
-turn non-linear constraints into linear ones.  For example, if we
-have a constraint @x * y = z@, and we can figure out that @x@ must be 5,
-then we end up with a linear constraint @5 * y = z@.
--}
-cryImproveModel :: SMT.Solver -> SMT.Logger -> Map Name Nat'
-                -> IO (Map Name Expr, [Prop])
-cryImproveModel solver logger model =
-  do (imps,subGoals) <- go Map.empty [] initialTodo
-     return (toSubst imps, subGoals)
-
-  where
-  -- Process unification variables first.  That way, if we get `x = y`, we'd
-  -- prefer `x` to be a unification variable.
-  initialTodo    = uncurry (++) $ partition (isUniVar . fst) $ Map.toList model
-  isUniVar x     = case x of
-                     UserName (TVFree {}) -> True
-                     _                    -> False
-
-
-  -- done:  the set of known improvements
-  -- extra: the collection of inferred sub-goals
-  go done extra []             = return (done,extra)
-  go done extra ((x,e) : rest) =
-
-    -- x = K?
-    do mbCounter <- cryMustEqualK solver (Map.keys model) x e
-       case mbCounter of
-         Nothing -> go (Map.insert x (K e) done) extra rest
-         Just ce -> goV ce done extra [] x e rest
-
-
-  -- ce:    a counter example to `x = e`
-  -- done:  known improvements
-  -- extra: known sub-goals
-  -- todo:  more work to process once we are done with `x`.
-  goV _  done extra todo _ _ [] = go done extra (reverse todo)
-  goV ce done extra todo x e ((y,e') : more)
-    -- x = y?
-    | e == e' = do yesK <- cryMustEqualV solver x y
-                   if yesK then go (Map.insert x (Var y) done)
-                                   extra
-                                   (reverse todo ++ more)
-                           else tryLR
-
-    | otherwise = tryLR
-
-    where
-    next = goV ce done extra ((y,e'):todo) x e more
-
-    tryLR =
-      do mb <- tryLR_with x e y e'
-         case mb of
-           Just (r,subGoals) -> go (Map.insert x r done)
-                                   (subGoals ++ extra)
-                                   (reverse todo ++ more)
-           Nothing ->
-             do mb1 <- tryLR_with y e' x e
-                case mb1 of
-                  Nothing -> next
-                  Just (r, subGoals) -> go (Map.insert y r done)
-                                           (subGoals ++ extra)
-                                           (reverse todo ++ more)
-
-
-    tryLR_with v1 v1Expr v2 v2Expr =
-      case ( isUniVar v1
-           , v1Expr
-           , v2Expr
-           , Map.lookup v1 ce
-           , Map.lookup v2 ce
-           ) of
-        (True, x1, y1, Just x2, Just y2) ->
-          cryCheckLinRel solver logger v2 v1 (y1,x1) (y2,x2)
-        _ -> return Nothing
-
-
-
-
-
-
-
--- | Try to prove the given expression.
-checkUnsat :: SMT.Solver -> SExpr -> IO Bool
-checkUnsat s e =
-  do SMT.push s
-     SMT.assert s e
-     res <- SMT.check s
-     SMT.pop s
-     return (res == SMT.Unsat)
-
-
--- | Try to prove the given expression.
--- If we fail, we try to give a counter example.
--- If the answer is unknown, then we return an empty counter example.
-getCounterExample :: SMT.Solver -> [Name] -> SExpr -> IO (Maybe (Map Name Nat'))
-getCounterExample s xs e =
-  do SMT.push s
-     SMT.assert s e
-     res <- SMT.check s
-     ans <- case res of
-              SMT.Unsat   -> return Nothing
-              SMT.Unknown -> return (Just Map.empty)
-              SMT.Sat     -> Just `fmap` getVals s xs
-     SMT.pop s
-     return ans
-
-
-
-
-
--- | Is this the only possible value for the constant, under the current
--- assumptions.
--- Assumes that we are in a 'Sat' state.
--- Returns 'Nothing' if the variables must always match the given value.
--- Otherwise, we return a counter-example (which may be empty, if uniknown)
-cryMustEqualK :: SMT.Solver -> [Name] ->
-                 Name -> Nat' -> IO (Maybe (Map Name Nat'))
-cryMustEqualK solver xs x val =
-  case val of
-    Inf   -> getCounterExample solver xs (SMT.const (smtFinName x))
-    Nat n -> getCounterExample solver xs $
-             SMT.not $
-             SMT.and (SMT.const $ smtFinName x)
-                     (SMT.eq (SMT.const (smtName x)) (SMT.int n))
-
-
-
--- | Do these two variables need to always be the same, under the current
--- assumptions.
--- Assumes that we are in a 'Sat' state.
-cryMustEqualV :: SMT.Solver -> Name -> Name -> IO Bool
-cryMustEqualV solver x y =
-     checkUnsat solver $
-        SMT.not $
-        SMT.or (SMT.not (fin x) `SMT.and` SMT.not (fin y))
-               (fin x `SMT.and` fin y `SMT.and` SMT.eq (var x) (var y))
-
-  where fin a = SMT.const (smtFinName a)
-        var a = SMT.const (smtName a)
-
-
--- | Try to find a linear relation between the two variables, based
--- on two observed data points.
--- NOTE:  The variable being defined is the SECOND name.
-cryCheckLinRel :: SMT.Solver -> SMT.Logger ->
-         {- x -} Name {- ^ Definition in terms of this variable. -} ->
-         {- y -} Name {- ^ Define this variable. -} ->
-                 (Nat',Nat') {- ^ Values in one model (x,y) -} ->
-                 (Nat',Nat') {- ^ Values in another model (x,y) -} ->
-                 IO (Maybe (Expr,[Prop]))
-                 {- ^ Either nothing, or an improving expression, and any
-                      additional obligations -}
-cryCheckLinRel s logger x y p1 p2 =
-  -- First, try to find a linear relation that holds in all finite cases.
-  do SMT.push s
-     SMT.assert s (isFin x)
-     SMT.assert s (isFin y)
-     ans <- case (p1,p2) of
-              ((Nat x1, Nat y1), (Nat x2, Nat y2)) ->
-                  checkLR x1 y1 x2 y2
-
-              ((Inf,    Inf),    (Nat x2, Nat y2)) ->
-                 mbGoOn (getFinPt x2) $ \(x1,y1) -> checkLR x1 y1 x2 y2
-
-              ((Nat x1, Nat y1), (Inf,    Inf)) ->
-                 mbGoOn (getFinPt x1) $ \(x2,y2) -> checkLR x1 y1 x2 y2
-
-              _ -> return Nothing
-
-     SMT.pop s
-
-
-     -- Next, check the infinite cases: if @y = A * x + B@, then
-     -- either both @x@ and @y@ must be infinite or they both must be finite.
-     -- Note that we don't consider relations where A = 0: because they
-     -- would be handled when we checked that @y@ is a constant.
-     case ans of
-       Nothing -> return Nothing
-       Just e ->
-         do SMT.push s
-            SMT.assert s (SMT.not (SMT.eq (isFin x) (isFin y)))
-            c <- SMT.check s
-            SMT.pop s
-            case c of
-              SMT.Unsat -> return (Just e)
-              _         -> return Nothing
-
-  where
-  isFin a = SMT.const (smtFinName a)
-
-  -- XXX: Duplicates `cryDefined`
-  -- The constraints are always of the form: x >= K, or K >= x
-  wellDefined e =
-    case e of
-      (K (Nat a) :* t) :- K (Nat b) ->
-        let c = div (b + a - 1) a
-        in [ t :>= K (Nat c) ]
-
-      K (Nat b) :- (K (Nat a) :* t)
-        -> let c = div b a
-           in [ K (Nat c) :>= t ]
-
-      a  :- b -> [ a :>= b ]
-
-      _ -> []
-
-
-  checkLR x1 y1 x2 y2 =
-    do SMT.logMessage logger ("checkLR: " ++ show (x1,y1) ++ "   "
-                                          ++ show (x2,y2))
-       mbGoOn (return (linRel (x1,y1) (x2,y2))) (\(a,b) ->
-         do let sumTerm v
-                   | b == 0    = v
-                   | b < 0     = v :- K (Nat (negate b))
-                   | otherwise = v :+ K (Nat b)
-
-                expr
-                  | a == 1     = sumTerm (Var x)
-                  | a <  0     = K (Nat b) :- K (Nat (negate a)) :* Var x
-                  | otherwise  = sumTerm (K (Nat a) :* Var x)
-
-            SMT.logMessage logger ("candidate: " ++ show (ppProp (Var y :==: expr)))
-
-            proved <- checkUnsat s
-                    $ propToSmtLib $ crySimplify
-                    $ Not $ Var y :==: expr
-
-            if not proved
-               then SMT.logMessage logger "failed" >> return Nothing
-               else return (Just (expr,wellDefined expr)))
-
-  -- Try to get an example of another point, which is finite, and at
-  -- different @x@ coordinate.
-  getFinPt otherX =
-    do SMT.push s
-       SMT.assert s (SMT.not (SMT.eq (SMT.const (smtName x)) (SMT.int otherX)))
-       smtAns <- SMT.check s
-       ans <- case smtAns of
-                SMT.Sat ->
-                  do vX <- SMT.getConst s (smtName x)
-                     vY <- SMT.getConst s (smtName y)
-                     case (vX, vY) of
-                       (SMT.Int vx, SMT.Int vy)
-                          | vx >= 0 && vy >= 0 -> return (Just (vx,vy))
-                       _ -> return Nothing
-                _ -> return Nothing
-       SMT.pop s
-       return ans
-
-  mbGoOn m k = do ans <- m
-                  case ans of
-                    Nothing -> return Nothing
-                    Just a  -> k a
-
-{- | Compute a linear relation through two concrete points.
-Try to find a relation of the form @y = a * x + b@.
-Depending on the signs of @a@ and @b@, we need additional checks,
-to ensure tha @a * x + b@ is valid.
-
-y1 = A * x1 + B
-y2 = A * x2 + B
-(y2 - y1) = A * (x2 - x1)
-
-A = (y2 - y1) / (x2 - x1)
-B = y1 - A * x1
--}
-linRel :: (Integer,Integer)       {- ^ First point -} ->
-          (Integer,Integer)       {- ^ Second point -} ->
-          Maybe (Integer,Integer) {- ^ (A,B) -}
-linRel (x1,y1) (x2,y2) =
-  do guard (x1 /= x2)
-     let (a,r) = divMod (y2 - y1) (x2 - x1)
-     guard (r == 0 && a /= 0)    -- Not interested in A = 0
-     let b = y1 - a * x1
-     guard $ not $ a < 0 && b < 0   -- No way this will give a natural number.
-     return (a,b)

src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs

@@ -1,843 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2014-2016 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
---
--- TODO:
---  - Putting in a normal form to spot "prove by assumption"
---  - Additional simplification rules, namely various cancelation.
---  - Things like:  lg2 e(x) = x, where we know thate is increasing.
-
-{-# LANGUAGE Safe, PatternGuards, BangPatterns #-}
-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
-
-module Cryptol.TypeCheck.Solver.Numeric.Simplify
-  (
-  -- * Simplify a property
-  crySimplify, crySimplifyMaybe
-
-  -- * Simplify expressions in a prop
-  , crySimpPropExpr, crySimpPropExprMaybe
-  ) where
-
-import           Cryptol.TypeCheck.Solver.Numeric.AST
-import           Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr
-import           Cryptol.TypeCheck.Solver.InfNat(genLog,genRoot,rootExact)
-import           Cryptol.Utils.Misc ( anyJust )
-
-import           Control.Monad ( mplus )
-import           Data.List ( sortBy )
-import           Data.Maybe ( fromMaybe )
-import qualified Data.Set as Set
-
-
--- | Simplify a property, if possible.
-crySimplify :: Prop -> Prop
-crySimplify p = fromMaybe p (crySimplifyMaybe p)
-
--- | Simplify a property, if possible.
-crySimplifyMaybe :: Prop -> Maybe Prop
-crySimplifyMaybe p =
-  let mbSimpExprs = simpSubs p
-      exprsSimped = fromMaybe p mbSimpExprs
-      mbRearrange = tryRearrange exprsSimped
-      rearranged  = fromMaybe exprsSimped mbRearrange
-  in crySimplify `fmap` (crySimpStep rearranged `mplus` mbRearrange
-                                                `mplus` mbSimpExprs)
-
-  where
-  tryRearrange q = case q of
-                    _ :&& _ -> cryRearrangeAnd q
-                    _ :|| _ -> cryRearrangeOr  q
-                    _       -> Nothing
-
-  simpSubs q = case q of
-                Not a     -> Not `fmap` crySimplifyMaybe a
-                a :&& b   -> do [a',b'] <- anyJust crySimplifyMaybe [a,b]
-                                return (a' :&& b')
-                a :|| b   -> do [a',b'] <- anyJust crySimplifyMaybe [a,b]
-                                return (a' :|| b')
-                _         -> crySimpPropExprMaybe q
-
-
-
-
-
--- | A single simplification step.
-crySimpStep :: Prop -> Maybe Prop
-crySimpStep prop =
-  case prop of
-
-    Fin x     -> cryIsFin x   -- Fin only on variables.
-
-    x :== y   -> Just (cryIsEq x y)
-    x :>  y   -> Just (cryIsGt x y)
-
-    x :>= y   ->
-      case (x,y) of
-        -- XXX: DUPLICTION
-        (K (Nat 0), _)       -> Just (y :== zero)
-        (K (Nat a), Width b) -> Just (K (Nat (2 ^ a)) :>= b)
-
-        (_,       K (Nat 0)) -> Just PTrue
-        (Width e, K (Nat b)) -> Just (e :>= K (Nat (2^(b-1))))
-
-
-        (K Inf, _)     -> Just PTrue
-        (_, K Inf)     -> Just (x :== inf)
-        _              -> Just (x :== inf :|| one :+ x :> y)
-
-    x :==: y ->
-      case (x,y) of
-        (K a, K b)     -> Just (if a == b then PTrue else PFalse)
-        (K (Nat n), _) | Just p <- cryIsNat True n y -> Just p
-        (_, K (Nat n)) | Just p <- cryIsNat True n x -> Just p
-
-        _ | x == y    -> Just PTrue
-          | otherwise -> case (x,y) of
-                           (Var _, _) -> Nothing
-                           (_, Var _) -> Just (y :==: x)
-                           _          -> Nothing
-
-    x :>: y ->
-      case (x,y) of
-        (K (Nat n),_)  | Just p <- cryNatGt True n y -> Just p
-        (_, K (Nat n)) | Just p <- cryGtNat True n x -> Just p
-
-        _ | x == y      -> Just PFalse
-          | otherwise   -> Nothing
-
-
-    -- For :&& and :|| we assume that the props have been rearrnaged
-    p :&& q -> cryAnd p q
-    p :|| q -> cryOr p q
-
-    Not p   -> cryNot p
-    PFalse  -> Nothing
-    PTrue   -> Nothing
-
-
--- | Rebalance parens, and arrange conjucts so that we can transfer
--- information left-to-right.
-cryRearrangeAnd :: Prop -> Maybe Prop
-cryRearrangeAnd prop =
-  case rebalance prop of
-    Just p  -> Just p
-    Nothing -> cryAnds `fmap` cryRearrange cmpAnd (split prop)
-  where
-  rebalance (a :&& b) =
-    case a of
-      PFalse    -> Just PFalse
-      PTrue     -> Just b
-      a1 :&& a2 -> Just (a1 :&& (a2 :&& b))
-      _         -> fmap (a :&&) (rebalance b)
-  rebalance _ = Nothing
-
-  split (a :&& b) = a : split b
-  split a         = [a]
-
-
--- | Rebalance parens, and arrange disjuncts so that we can transfer
--- information left-to-right.
-cryRearrangeOr :: Prop -> Maybe Prop
-cryRearrangeOr prop =
-  case rebalance prop of
-    Just p  -> Just p
-    Nothing -> cryOrs `fmap` cryRearrange cmpOr (split prop)
-  where
-  rebalance (a :|| b) =
-    case a of
-      PFalse    -> Just b
-      PTrue     -> Just PTrue
-      a1 :|| a2 -> Just (a1 :|| (a2 :|| b))
-      _         -> fmap (a :||) (rebalance b)
-  rebalance _ = Nothing
-
-  split (a :|| b) = a : split b
-  split a         = [a]
-
-
-
-
--- | Identify propositions that are suiatable for inlining.
-cryIsDefn :: Prop -> Maybe (Name, Expr)
-cryIsDefn (Var x :==: e) = if (x `Set.member` cryExprFVS e)
-                              then Nothing
-                              else Just (x,e)
-cryIsDefn _              = Nothing
-
-
-
-
-
-type PropOrdering = (Int,Prop) -> (Int,Prop) -> Ordering
-
-{- | Rearrange proposition for conjuctions and disjunctions.
-
-information left-to-right, so we put proposition with information content
-on the left.
--}
-cryRearrange :: PropOrdering -> [Prop] -> Maybe [Prop]
-cryRearrange cmp ps = if ascending keys then Nothing else Just sortedProps
-  where
-  -- We tag each proposition with a number, so that later we can tell easily
-  -- if the propositions got rearranged.
-  (keys, sortedProps) = unzip (sortBy cmp (zip [ 0 :: Int .. ] ps))
-
-  ascending (x : y : zs) = x < y && ascending (y : zs)
-  ascending _            = True
-
-
-cmpAnd :: PropOrdering
-cmpAnd (k1,prop1) (k2,prop2) =
-  case (prop1, prop2) of
-
-    -- First comes PFalse, maybe we don't need to do anything
-    (PFalse, PFalse) -> compare k1 k2
-    (PFalse, _)      -> LT
-    (_,PFalse)       -> GT
-
-    -- Next comes PTrue
-    (PTrue, PTrue)   -> compare k1 k2
-    (PTrue, _)       -> LT
-    (_,PTrue)        -> GT
-
-    -- Next come `not (fin a)`  (i.e, a = inf)
-    (Not (Fin (Var x)), Not (Fin (Var y))) -> cmpVars x y
-    (Not (Fin (Var _)), _)                 -> LT
-    (_, Not (Fin (Var _)))                 -> GT
-
-    -- Next come definitions: `x = e` (with `x` not in `fvs e`)
-    -- XXX: Inefficient, because we keep recomputing free variables
-    -- (here, and then when actually applying the substitution)
-    _ | Just (x,_) <- mbL
-      , Just (y,_) <- mbR  -> cmpVars x y
-      | Just _     <- mbL  -> LT
-      | Just _     <- mbR  -> GT
-      where
-      mbL = cryIsDefn prop1
-      mbR = cryIsDefn prop2
-
-    -- Next come `fin a`
-    (Fin (Var x), Fin (Var y)) -> cmpVars x y
-    (Fin (Var _), _)           -> LT
-    (_, Fin (Var _))           -> GT
-
-    -- Everything else stays as is
-    _ -> compare k1 k2
-
-  where
-  cmpVars x y
-    | x < y     = LT
-    | x > y     = GT
-    | otherwise = compare k1 k2
-
-
-cmpOr :: PropOrdering
-cmpOr (k1,prop1) (k2,prop2) =
-  case (prop1, prop2) of
-
-    -- First comes PTrue, maybe we don't need to do anything
-    (PTrue, PTrue)   -> compare k1 k2
-    (PTrue, _)       -> LT
-    (_,PTrue)        -> GT
-
-    -- Next comes PFalse
-    (PFalse, PFalse) -> compare k1 k2
-    (PFalse, _)      -> LT
-    (_,PFalse)       -> GT
-
-    -- Next comes `fin a` (because we propagete `a = inf`)
-    (Fin (Var x), Fin (Var y)) -> cmpVars x y
-    (Fin (Var _), _)           -> LT
-    (_, Fin (Var _))           -> GT
-
-    -- Next come `not (fin a)`  (i.e, propagete (fin a))
-    (Not (Fin (Var x)), Not (Fin (Var y))) -> cmpVars x y
-    (Not (Fin (Var _)), _)                 -> LT
-    (_, Not (Fin (Var _)))                 -> GT
-
-    -- we don't propagete (x /= e) for now.
-
-    -- Everything else stays as is
-    _ -> compare k1 k2
-
-  where
-  cmpVars x y
-    | x < y     = LT
-    | x > y     = GT
-    | otherwise = compare k1 k2
-
-
-
-
-
--- | Simplification of ':&&'.
--- Assumes arranged conjucntions.
--- See 'cryRearrangeAnd'.
-cryAnd :: Prop -> Prop -> Maybe Prop
-cryAnd p q =
-  case p of
-    PTrue       -> Just q
-
-    PFalse      -> Just PFalse
-
-    Not (Fin (Var x))
-      | Just q' <- cryKnownFin x False q -> Just (p :&& q')
-
-    Fin (Var x)
-      | Just q' <- cryKnownFin x True q -> Just (p :&& q')
-
-    _ | Just (x,e) <- cryIsDefn p
-      , Just q'    <- cryLet x e q
-      -> Just (p :&& q')
-
-    _ -> Nothing
-
-
--- | Simplification of ':||'.
--- Assumes arranged disjunctions.
--- See 'cryRearrangeOr'
-cryOr :: Prop -> Prop -> Maybe Prop
-cryOr p q =
-  case p of
-    PTrue     -> Just PTrue
-
-    PFalse    -> Just q
-
-    Fin (Var x)
-      | Just q' <- cryKnownFin x False q -> Just (p :|| q')
-
-    Not (Fin (Var x))
-      | Just q' <- cryKnownFin x True q -> Just (p :|| q')
-
-    _ -> Nothing
-
-
-
--- | Propagate the fact that the variable is known to be finite ('True')
--- or not-finite ('False').
--- Note that this may introduce new expression redexes.
-cryKnownFin :: Name -> Bool -> Prop -> Maybe Prop
-cryKnownFin a isFin prop =
-  case prop of
-    Fin (Var a') | a == a' -> Just (if isFin then PTrue else PFalse)
-
-    p :&& q -> do [p',q'] <- anyJust (cryKnownFin a isFin) [p,q]
-                  return (p' :&& q')
-
-    p :|| q -> do [p',q'] <- anyJust (cryKnownFin a isFin) [p,q]
-                  return (p' :|| q')
-
-    Not p   -> Not `fmap` cryKnownFin a isFin p
-
-    x :==: y
-      | not isFin, Just [x',y'] <- anyJust (cryLet a inf) [x,y]
-      -> Just (cryNatOp (:==:) x' y')
-
-    x :>: y
-      | not isFin, Just [x',y'] <- anyJust (cryLet a inf) [x,y]
-      -> Just (cryNatOp (:>:) x' y')
-
-    -- All the other cases should be simplified, eventually.
-    _       -> Nothing
-
-
-
-
--- | Negation.
-cryNot :: Prop -> Maybe Prop
-cryNot prop =
-  case prop of
-    Fin _           -> Nothing
-
-    x :== y         -> Just (x :> y :|| y :> x)
-    x :>= y         -> Just (y :>  x)
-    x :>  y         -> Just (y :>= x)
-
-    x :==: y        -> Just (x :>: y :|| y :>: x)
-
-    _ :>: _         -> Nothing
-
-    p :&& q         -> Just (Not p :|| Not q)
-    p :|| q         -> Just (Not p :&& Not q)
-    Not p           -> Just p
-    PFalse          -> Just PTrue
-    PTrue           -> Just PFalse
-
-
-
--- | Simplificaiton for @:==@
-cryIsEq :: Expr -> Expr -> Prop
-cryIsEq l r =
-  case (l,r) of
-    (K m, K n)      -> if m == n then PTrue else PFalse
-
-    (K Inf, _)      -> Not (Fin r)
-    (_, K Inf)      -> Not (Fin l)
-
-    (Div x y, z)    -> x :>= z :* y :&& (one :+ z) :* y :> x
-
-    (K (Nat n),_) | Just p <- cryIsNat False n r -> p
-    (_,K (Nat n)) | Just p <- cryIsNat False n l -> p
-
-    _               -> Not (Fin l) :&& Not (Fin r)
-                   :|| Fin l :&& Fin r :&& cryNatOp (:==:) l r
-
-
-
-
--- | Simplificatoin for @:>@
-cryIsGt :: Expr -> Expr -> Prop
-cryIsGt (K m) (K n)   = if m > n then PTrue else PFalse
-cryIsGt (K (Nat n)) e | Just p <- cryNatGt False n e = p
-cryIsGt e (K (Nat n)) | Just p <- cryGtNat False n e = p
-
-cryIsGt x y           = Fin y :&& (x :== inf :||
-                                   Fin x :&& cryNatOp (:>:) x y)
-
-
-
--- | Attempt to simplify a @fin@ constraint.
--- Assumes a defined input.
-cryIsFin :: Expr -> Maybe Prop
-cryIsFin expr =
-  case expr of
-    K Inf                -> Just PFalse
-    K (Nat _)            -> Just PTrue
-    Var _                -> Nothing
-    t1 :+ t2             -> Just (Fin t1 :&& Fin t2)
-    t1 :- _              -> Just (Fin t1)
-
-    t1 :* t2             -> Just ( Fin t1 :&& Fin t2
-                               :|| t1 :== zero :&& t2 :== inf
-                               :|| t2 :== zero :&& t1 :== inf
-                                 )
-
-    Div t1 _             -> Just (Fin t1)
-    Mod _ _              -> Just PTrue
-
-    t1 :^^ t2            ->
-      Just ( Fin t1 :&& Fin t2
-         :|| t1 :== inf :&& t2 :== zero   -- inf ^^ 0
-         :|| t2 :== inf :&& (t1 :== zero :|| t1 :== one)
-                             -- 0 ^^ inf,    1 ^^ inf
-           )
-
-    Min t1 t2            -> Just (Fin t1 :|| Fin t2)
-    Max t1 t2            -> Just (Fin t1 :&& Fin t2)
-    Width t1             -> Just (Fin t1)
-    LenFromThen  _ _ _   -> Just PTrue
-    LenFromThenTo  _ _ _ -> Just PTrue
-
-
-cryIsNat :: Bool -> Integer -> Expr -> Maybe Prop
-cryIsNat useFinite n expr =
-  case expr of
-    K Inf     -> Just PFalse
-
-    K (Nat m) -> Just (if m == n then PTrue else PFalse)
-
-    Var _ | useFinite   -> Nothing
-          | otherwise   -> Just (Fin expr :&& expr :==: K (Nat n))
-
-    K (Nat m) :+ e2     -> Just $ if m > n then PFalse
-                                           else eq e2 $ K $ Nat $ n - m
-
-    x :+ y
-      | n == 0          -> Just (eq x zero :&& eq y zero)
-      | n == 1          -> Just (eq x zero :&& eq y one :||
-                                 eq x one  :&& eq y zero)
-      | otherwise       -> Nothing
-
-    e1 :- e2            -> Just $ eq (K (Nat n) :+ e2) e1
-
-    K (Nat m) :* e2     ->
-      Just $ if m == 0
-                then if n == 0 then PTrue else PFalse
-                else case divMod n m of
-                       (q,r) -> if r == 0 then eq e2 (K (Nat q))
-                                          else PFalse
-    e1 :* e2
-      | n == 0          -> Just (eq e1 zero :|| eq e2 zero)
-      | n == 1          -> Just (eq e1 one :&& eq e2 one)
-      | otherwise       -> Nothing
-
-    -- (x >= n * y) /\ ((n+1) * y > x)
-    Div x y             -> Just (gt (one :+ x) (K (Nat n) :* y) :&&
-                                 gt (K (Nat (n + 1)) :* y) x)
-
-    Mod _ _ | useFinite -> Nothing
-            | otherwise -> Just (cryNatOp (:==:) expr (K (Nat n)))
-
-
-    K (Nat m) :^^ y     -> Just $ case genLog n m of
-                                    Just (a, exact)
-                                      | exact -> eq y (K (Nat a))
-                                    _ -> PFalse
-    x :^^ K (Nat m)     -> Just $ case rootExact n m of
-                                    Just a  -> eq x (K (Nat a))
-                                    Nothing -> PFalse
-    x :^^ y
-      | n == 0          -> Just (eq x zero :&& gt y zero)
-      | n == 1          -> Just (eq x one  :|| eq y zero)
-      | otherwise       -> Nothing
-
-    Min x y
-      | n == 0          -> Just (eq x zero :|| eq y zero)
-      | otherwise       -> Just ( eq x (K (Nat n)) :&& gt y (K (Nat (n - 1)))
-                              :|| eq y (K (Nat n)) :&& gt x (K (Nat (n - 1)))
-                                )
-
-    Max x y             -> Just ( eq x (K (Nat n)) :&& gt (K (Nat (n + 1))) y
-                              :|| eq y (K (Nat n)) :&& gt (K (Nat (n + 1))) y
-                                )
-
-    Width x
-      | n == 0          -> Just (eq x zero)
-      | otherwise       -> Just (gt x (K (Nat (2^(n-1) - 1))) :&&
-                                 gt (K (Nat (2 ^ n))) x)
-
-    LenFromThen x y w
-      | n == 0          -> Just PFalse
-
-      -- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
-      | n == 1          -> Just (gt y x :&& gt (y :+ one) (two :^^ w))
-      | otherwise       -> Nothing -- XXX: maybe some more?
-
-
-    -- See `nLenFromThenTo` in 'Cryptol.TypeCheck.Solver.InfNat'
-    LenFromThenTo x y z
-      | n == 0          -> Just ( gt x y :&& gt z x
-                              :|| gt y x :&& gt x z
-                                )
-
-      -- See Note [Sequences of Length 1] in 'Cryptol.TypeCheck.Solver.InfNat'
-      | n == 1          -> Just (gt z y :&& gt (x :+ one) z     :||
-                                 gt y z :&& gt (z :+ one) x)
-      | otherwise       -> Nothing -- XXX: maybe some more?
-
-
-  where
-  eq x y = if useFinite then x :==: y else x :== y
-  gt x y = if useFinite then x :>: y  else x :>  y
-
--- | Constant > expression
-cryNatGt :: Bool -> Integer -> Expr -> Maybe Prop
-cryNatGt useFinite n expr
-  | n == 0    = Just PFalse
-  | n == 1    = Just (eq expr zero)
-  | otherwise =
-    case expr of
-      K x   -> Just $ if Nat n > x then PTrue else PFalse
-
-      Var _ -> Nothing
-
-      K (Nat m) :+ y -> Just $ if n >= m then gt (k (n - m)) y else PFalse
-      _ :+ _         -> Nothing
-
-      x :- y         -> Just $ gt (k n :+ y) x
-
-      K (Nat m) :* y
-        | m == 0    -> Just PTrue   -- because we know that n > 1
-        | otherwise -> Just $ case divMod n m of
-                                (q,0) -> gt (k q) y
-                                (0,_) -> eq y zero
-                                (q,_) -> gt (k (q + 1)) y
-      _ :* _          -> Nothing
-
-      Div x y         -> Just $ gt (k n :* y) x
-
-      Mod _ (K (Nat m))
-        | m <= n      -> Just PTrue
-
-      Mod (K (Nat m)) _
-        | m < n       -> Just PTrue
-      Mod _ _         -> Nothing
-
-
-      K (Nat m) :^^ y
-        | m == 0      -> Just PTrue   -- because n > 1
-        | m == 1      -> Just PTrue   -- ditto
-        | otherwise   -> do (a,exact) <- genLog n m
-                            return $ if exact
-                                        then gt (k a) y
-                                        else gt (k (a + 1)) y
-      x :^^ K (Nat m)
-        | m == 0      -> Just PTrue
-        | m == 1      -> Just (gt (k n) x)
-        | otherwise   -> do (a,exact) <- genRoot n m
-                            return $ if exact
-                                        then gt (k a) x
-                                        else gt (k (a + 1)) x
-      _ :^^ _         -> Nothing
-
-      Min x y         -> Just $ gt (k n) x :|| gt (k n) y
-      Max x y         -> Just $ gt (k n) x :&& gt (k n) y
-
-      Width x         -> Just $ gt (k (2 ^ n)) x
-
-      LenFromThen _ _ _   -> Nothing -- Are there some rules?
-
-      LenFromThenTo _ _ _ -> Nothing -- Are there some rulesj
-
-  where
-  k x    = K (Nat x)
-  eq x y = if useFinite then x :==: y else x :== y
-  gt x y = if useFinite then x :>: y  else x :>  y
-
-
-
--- | Expression > constant
-cryGtNat :: Bool -> Integer -> Expr -> Maybe Prop
-cryGtNat useFinite n expr =
-  case expr of
-    K x                 -> Just $ if x > Nat n then PTrue else PFalse
-    Var _               -> Nothing
-
-    K (Nat m) :+ y
-      | m > n           -> Just PTrue
-      | otherwise       -> Just (gt y (K (Nat (n - m))))
-
-    x :+ y
-      | n == 0          -> Just (gt x zero :|| gt y zero)
-      | otherwise       -> Nothing
-
-    x :- y              -> Just $ gt x (K (Nat n) :+ y)
-
-
-    K (Nat m) :* y
-      | m > 0           -> Just $ case divMod n m of
-                                    (a,_) -> gt y $ K $ Nat a
-
-    x :* y
-      | n == 0          -> Just (gt x zero :&& gt y zero)
-      | otherwise       -> Nothing
-
-    Div x y             -> Just $ gt (one :+ x) (K (Nat (n+1)) :* y)
-
-    Mod _ (K (Nat m))
-      | m <= n          -> Just PFalse
-    Mod (K (Nat m)) _
-      | m < n           -> Just PFalse
-    Mod _ _             -> Nothing
-
-    K (Nat m) :^^ y
-      | m == 0          -> Just $ if n == 0 then eq y zero else PFalse
-      | m == 1          -> Just $ if n == 0 then PTrue else PFalse
-      | otherwise       -> do (a,_exact) <- genLog n m
-                              Just (gt y (K (Nat a)))
-
-    x :^^ K (Nat m)
-      | m == 0          -> Just $ if n == 0 then PTrue else PFalse
-      | m == 1          -> Just $ gt x (K (Nat n))
-      | otherwise       -> do (a,exact) <- genRoot n m
-                              Just $ if exact
-                                        then gt x (K (Nat a))
-                                        else gt (one :+ x) (K (Nat (a+1)))
-
-    x :^^ y
-      | n == 0          -> Just (gt x zero :|| eq y zero)
-      | otherwise       -> Nothing
-
-    Min x y             -> Just $ gt x (K (Nat n)) :&& gt y (K (Nat n))
-    Max x y             -> Just $ gt x (K (Nat n)) :|| gt y (K (Nat n))
-
-    Width x             -> Just $ gt (one :+ x) (K (Nat (2 ^ n)))
-
-    LenFromThen _ _ _
-      | n == 0          -> Just PTrue
-      | otherwise       -> Nothing -- Are there some rules?
-
-    LenFromThenTo x y z
-      | n == 0          -> Just (gt x y :&& gt z x :|| gt y x :&& gt x z)
-      | otherwise       -> Nothing
-
-  where
-  eq x y = if useFinite then x :==: y else x :== y
-  gt x y = if useFinite then x :>: y  else x :>  y
-
-
-
--- | Simplify only the Expr parts of a Prop.
-crySimpPropExpr :: Prop -> Prop
-crySimpPropExpr p = fromMaybe p (crySimpPropExprMaybe p)
-
--- | Simplify only the Expr parts of a Prop.
--- Returns `Nothing` if there were no changes.
-crySimpPropExprMaybe  :: Prop -> Maybe Prop
-crySimpPropExprMaybe prop =
-  case prop of
-
-    Fin e                 -> Fin `fmap` crySimpExprMaybe e
-
-    a :==  b              -> binop crySimpExprMaybe (:== ) a b
-    a :>=  b              -> binop crySimpExprMaybe (:>= ) a b
-    a :>   b              -> binop crySimpExprMaybe (:>  ) a b
-    a :==: b              -> binop crySimpExprMaybe (:==:) a b
-    a :>:  b              -> binop crySimpExprMaybe (:>: ) a b
-
-    a :&& b               -> binop crySimpPropExprMaybe (:&&) a b
-    a :|| b               -> binop crySimpPropExprMaybe (:||) a b
-
-    Not p                 -> Not `fmap` crySimpPropExprMaybe p
-
-    PFalse                -> Nothing
-    PTrue                 -> Nothing
-
-  where
-
-  binop simp f l r =
-    case (simp l, simp r) of
-      (Nothing,Nothing) -> Nothing
-      (l',r')           -> Just (f (fromMaybe l l') (fromMaybe r r'))
-
-
-
-
-
-
--- | Our goal is to bubble @inf@ terms to the top of @Return@.
-cryNoInf :: Expr -> IfExpr Expr
-cryNoInf expr =
-  case expr of
-
-    -- These are the interesting cases where we have to branch
-
-    x :* y ->
-      do x' <- cryNoInf x
-         y' <- cryNoInf y
-         case (x', y') of
-           (K Inf, K Inf) -> return inf
-           (K Inf, _)     -> mkIf (y' :==: zero) (return zero) (return inf)
-           (_, K Inf)     -> mkIf (x' :==: zero) (return zero) (return inf)
-           _              -> return (x' :* y')
-
-    x :^^ y ->
-      do x' <- cryNoInf x
-         y' <- cryNoInf y
-         case (x', y') of
-           (K Inf, K Inf) -> return inf
-           (K Inf, _)     -> mkIf (y' :==: zero) (return one) (return inf)
-           (_, K Inf)     -> mkIf (x' :==: zero) (return zero)
-                           $ mkIf (x' :==: one)  (return one)
-                           $ return inf
-           _              -> return (x' :^^ y')
-
-
-
-    -- The rest just propagates
-
-    K _     -> return expr
-    Var _   -> return expr
-
-    x :+ y  ->
-      do x' <- cryNoInf x
-         y' <- cryNoInf y
-         case (x', y') of
-           (K Inf, _)  -> return inf
-           (_, K Inf)  -> return inf
-           _           -> return (x' :+ y')
-
-    x :- y  ->
-      do x' <- cryNoInf x
-         y' <- cryNoInf y
-         case (x', y') of
-           (_, K Inf)  -> Impossible
-           (K Inf, _)  -> return inf
-           _           -> mkIf (x' :==: y)
-                               (return zero)
-                               (mkIf (x' :>: y) (return (x' :- y'))
-                                                Impossible)
-
-    Div x y ->
-      do x' <- cryNoInf x
-         y' <- cryNoInf y
-         case (x', y') of
-           (K Inf, _) -> Impossible
-           (_, K Inf) -> return zero
-           _          -> mkIf (y' :>: zero) (return (Div x' y')) Impossible
-
-    Mod x y ->
-      do x' <- cryNoInf x
-         -- `Mod x y` is finite, even if `y` is `inf`, so first check
-         -- for finiteness.
-         mkIf (Fin y)
-              (do y' <- cryNoInf y
-                  case (x',y') of
-                    (K Inf, _) -> Impossible
-                    (_, K Inf) -> Impossible
-                    _ -> mkIf (y' :>: zero) (return (Mod x' y')) Impossible
-              )
-              (return x')
-
-    Min x y ->
-      do x' <- cryNoInf x
-         y' <- cryNoInf y
-         case (x',y') of
-           (K Inf, _) -> return y'
-           (_, K Inf) -> return x'
-           _          -> return (Min x' y')
-
-    Max x y ->
-      do x' <- cryNoInf x
-         y' <- cryNoInf y
-         case (x', y') of
-           (K Inf, _) -> return inf
-           (_, K Inf) -> return inf
-           _          -> return (Max x' y')
-
-    Width x ->
-      do x' <- cryNoInf x
-         case x' of
-           K Inf      -> return inf
-           _          -> return (Width x')
-
-    LenFromThen x y w   -> fun3 LenFromThen x y w
-    LenFromThenTo x y z -> fun3 LenFromThenTo x y z
-
-
-  where
-  fun3 f x y z =
-    do x' <- cryNoInf x
-       y' <- cryNoInf y
-       z' <- cryNoInf z
-       case (x',y',z') of
-         (K Inf, _, _) -> Impossible
-         (_, K Inf, _) -> Impossible
-         (_, _, K Inf) -> Impossible
-         _             -> mkIf (x' :==: y') Impossible
-                                            (return (f x' y' z'))
-
-  mkIf p t e = case crySimplify p of
-                 PTrue  -> t
-                 PFalse -> e
-                 p'     -> If p' t e
-
-
-
-
--- | Make an expression that should work ONLY on natural nubers.
--- Eliminates occurances of @inf@.
--- Assumes that the two input expressions are well-formed and finite.
--- The expression is constructed by the given function.
-cryNatOp :: (Expr -> Expr -> Prop) -> Expr -> Expr -> Prop
-cryNatOp op x y =
-  toProp $
-  do x' <- noInf x
-     y' <- noInf y
-     return (op x' y')
-  where
-  noInf a = do a' <- cryNoInf a
-               case a' of
-                 K Inf -> Impossible
-                 _     -> return a'
-
-  toProp ite =
-    case ite of
-      Impossible -> PFalse -- It doesn't matter, but @false@ might anihilate.
-      Return p   -> p
-      If p t e   -> p :&& toProp t :|| Not p :&& toProp e

src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs

@@ -1,213 +0,0 @@
--- |
--- Module      :  $Header$
--- Copyright   :  (c) 2015-2016 Galois, Inc.
--- License     :  BSD3
--- Maintainer  :  cryptol@galois.com
--- Stability   :  provisional
--- Portability :  portable
---
--- Simplification of expressions.
--- The result of simplifying an expression `e`, is a new expression `e'`,
--- which satisfies the property:
---
---    if e is well-defined then e and e' will evaluate to the same type.
---
-
-{-# LANGUAGE Safe, BangPatterns #-}
-module Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr where
-
-import           Cryptol.TypeCheck.Solver.Numeric.AST
-import qualified Cryptol.TypeCheck.Solver.InfNat as IN
-import           Cryptol.Utils.Misc ( anyJust )
-
-import           Control.Monad ( guard )
-import           Data.Maybe ( fromMaybe, maybeToList )
-import qualified Data.Map as Map
-
-
--- | Simplify an expression, if possible.
-crySimpExpr :: Expr -> Expr
-crySimpExpr expr = fromMaybe expr (crySimpExprMaybe expr)
-
--- | Perform simplification from the leaves up.
--- Returns `Nothing` if there were no changes.
-crySimpExprMaybe :: Expr -> Maybe Expr
-crySimpExprMaybe expr =
-  case crySimpExprStep (fromMaybe expr mbE1) of
-    Nothing -> mbE1
-    Just e2 -> Just (fromMaybe e2 (crySimpExprMaybe e2))
-  where
-  mbE1 = cryRebuildExpr expr `fmap` anyJust crySimpExprMaybe (cryExprExprs expr)
-
-
-
--- XXX: Add rules to group together occurances of variables
-
-
-data Sign = Pos | Neg deriving Show
-
-otherSign :: Sign -> Sign
-otherSign s = case s of
-                Pos -> Neg
-                Neg -> Pos
-
-signed :: Sign -> Integer -> Integer
-signed s = case s of
-             Pos -> id
-             Neg -> negate
-
-
-splitSum :: Expr -> [(Sign,Expr)]
-splitSum e0 = go Pos e0 []
-  where go s (e1 :+ e2) es = go s e1 (go s e2 es)
-        go s (e1 :- e2) es = go s e1 (go (otherSign s) e2 es)
-        go s e es          = (s,e) : es
-
-normSum :: Expr -> Expr
-normSum = posTerm . go 0 Map.empty Nothing . splitSum
-  where
-
-  -- constants, variables, other terms
-  go !_ !_  !_ ((Pos,K Inf) : _) = (Pos, K Inf)
-
-  go k xs t ((s, K (Nat n)) : es) = go (k + signed s n) xs t es
-
-  go k xs t ((s, Var x) : es) = go k (Map.insertWith (+) x (signed s 1) xs) t es
-
-  go k xs t ((s, K (Nat n) :* Var x) : es)
-    | n == 0     = go k xs t es
-    | otherwise  = go k (Map.insertWith (+) x (signed s n) xs) t es
-
-  go k xs Nothing (e : es) = go k xs (Just e) es
-
-  go k xs (Just e1) (e2 : es) = go k xs (Just (add e1 e2)) es
-
-  go k xs t [] =
-    let terms     = constTerm k
-                 ++ concatMap varTerm (Map.toList xs)
-                 ++ maybeToList t
-
-    in case terms of
-         [] -> (Pos, K (Nat 0))
-         ts -> foldr1 add ts
-
-  constTerm k
-    | k == 0    = []
-    | k >  0    = [ (Pos, K (Nat k)) ]
-    | otherwise = [ (Neg, K (Nat (negate k))) ]
-
-  varTerm (x,k)
-    | k == 0    = []
-    | k == 1    = [ (Pos, Var x) ]
-    | k > 0     = [ (Pos, K (Nat k) :* Var x) ]
-    | k == (-1) = [ (Neg, Var x) ]
-    | otherwise = [ (Neg, K (Nat (negate k)) :* Var x) ]
-
-  add (s1,t1) (s2,t2) =
-    case (s1,s2) of
-      (Pos,Pos) -> (Pos, t1 :+ t2)
-      (Pos,Neg) -> (Pos, t1 :- t2)
-      (Neg,Pos) -> (Pos, t2 :- t1)
-      (Neg,Neg) -> (Neg, t1 :+ t2)
-
-  posTerm (Pos,x) = x
-  posTerm (Neg,x) = K (Nat 0) :- x
-
-
-
-
-crySimpExprStep :: Expr -> Maybe Expr
-crySimpExprStep e =
-  case crySimpExprStep1 e of
-    Just e1 -> Just e1
-    Nothing -> do let e1 = normSum e
-                  guard (e /= e1)
-                  return e1
-
--- | Make a simplification step, assuming the expression is well-formed.
-crySimpExprStep1 :: Expr -> Maybe Expr
-crySimpExprStep1 expr =
-  case expr of
-    K _                   -> Nothing
-    Var _                 -> Nothing
-
-    _ :+ _                -> Nothing
-    _ :- _                -> Nothing
-
-    x :* y ->
-      case (x,y) of
-        (K (Nat 0), _)    -> Just zero
-        (K (Nat 1), _)    -> Just y
-        (K a, K b)        -> Just (K (IN.nMul a b))
-        (_,   K _)        -> Just (y :* x)
-
-        (K a, K b :* z)   -> Just (K (IN.nMul a b) :* z)
-
-        -- Normalize, somewhat
-        (a :* b, _)       -> Just (a :* (b :* y))
-        (Var a, Var b)
-          | b > a         -> Just (y :* x)
-
-        _                 -> Nothing
-
-    Div x y ->
-      case (x,y) of
-        (K (Nat 0), _)    -> Just zero
-        (_, K (Nat 1))    -> Just x
-        (_, K Inf)        -> Just zero
-        (K a, K b)        -> K `fmap` IN.nDiv a b
-        _ | x == y        -> Just one
-        _                 -> Nothing
-
-    Mod x y ->
-      case (x,y) of
-        (K (Nat 0), _)    -> Just zero
-        (_, K Inf)        -> Just x
-        (_, K (Nat 1))    -> Just zero
-        (K a, K b)        -> K `fmap` IN.nMod a b
-        _                 -> Nothing
-
-    x :^^ y ->
-      case (x,y) of
-        (_, K (Nat 0))    -> Just one
-        (_, K (Nat 1))    -> Just x
-        (K (Nat 1), _)    -> Just one
-        (K a, K b)        -> Just (K (IN.nExp a b))
-        _                 -> Nothing
-
-    Min x y ->
-      case (x,y) of
-        (K (Nat 0), _)    -> Just zero
-        (K Inf, _)        -> Just y
-        (_, K (Nat 0))    -> Just zero
-        (_, K Inf)        -> Just x
-        (K a, K b)        -> Just (K (IN.nMin a b))
-        _ | x == y        -> Just x
-        _                 -> Nothing
-
-    Max x y ->
-      case (x,y) of
-        (K (Nat 0), _)    -> Just y
-        (K Inf, _)        -> Just inf
-        (_, K (Nat 0))    -> Just x
-        (_, K Inf)        -> Just inf
-        (K a, K b)        -> Just (K (IN.nMax a b))
-        _ | x == y        -> Just x
-        _                 -> Nothing
-
-    Width x ->
-      case x of
-        K a                           -> Just (K (IN.nWidth a))
-        K (Nat 2) :^^ e               -> Just (one :+ e)
-        K (Nat 2) :^^ e :- K (Nat 1)  -> Just e
-        _                             -> Nothing
-
-    LenFromThen x y w ->
-      case (x,y,w) of
-        (K a, K b, K c)   -> K `fmap` IN.nLenFromThen a b c
-        _                 -> Nothing
-
-    LenFromThenTo x y z ->
-      case (x,y,z) of
-        (K a, K b, K c)   -> K `fmap` IN.nLenFromThenTo a b c
-        _                 -> Nothing

src/Cryptol/TypeCheck/Solver/SMT.hs

@@ -1,5 +1,31 @@
+-- |
+-- Module      :  $Header$
+-- Copyright   :  (c) 2013-2016 Galois, Inc.
+-- License     :  BSD3
+-- Maintainer  :  cryptol@galois.com
+-- Stability   :  provisional
+-- Portability :  portable
+{-# LANGUAGE Safe #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# Language FlexibleInstances #-}
-module Cryptol.TypeCheck.Solver.SMT (proveImp,checkUnsolvable) where
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Cryptol.TypeCheck.Solver.SMT
+  ( -- * Setup
+    Solver
+  , withSolver
+
+    -- * Debugging
+  , debugBlock
+  , debugLog
+
+    -- * Proving stuff
+  , proveImp
+  , checkUnsolvable
+  , tryGetModel
+  ) where
 
 import           SimpleSMT (SExpr)
 import qualified SimpleSMT as SMT
@@ -9,69 +35,229 @@ import qualified Data.Set as Set
 import           Data.Maybe(catMaybes)
 import           Data.List(partition)
 import           Control.Monad(msum,zipWithM)
+import           Data.Char(isSpace)
+import           Text.Read(readMaybe)
+import qualified System.IO.Strict as StrictIO
+import           System.FilePath((</>))
+import           System.Directory(doesFileExist)
 
+import Cryptol.Prelude(cryptolTcContents)
 import Cryptol.TypeCheck.Type
-import Cryptol.TypeCheck.Solver.CrySAT
 import Cryptol.TypeCheck.InferTypes
 import Cryptol.TypeCheck.TypePat hiding ((~>),(~~>))
+import Cryptol.TypeCheck.Subst(Subst, emptySubst, listSubst)
 import Cryptol.Utils.Panic
+import Cryptol.Utils.PP -- ( Doc )
+
+
+
+-- | An SMT solver packed with a logger for debugging.
+data Solver = Solver
+  { solver    :: SMT.Solver
+    -- ^ The actual solver
+
+  , logger    :: SMT.Logger
+    -- ^ For debugging
+  }
+
+-- | Execute a computation with a fresh solver instance.
+withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
+withSolver SolverConfig { .. } k =
+  do logger <- if solverVerbose > 0 then SMT.newLogger 0 else return quietLogger
+
+     let smtDbg = if solverVerbose > 1 then Just logger else Nothing
+     solver <- SMT.newSolver solverPath solverArgs smtDbg
+     _ <- SMT.setOptionMaybe solver ":global-decls" "false"
+     -- SMT.setLogic solver "QF_LIA"
+     let sol = Solver { .. }
+     loadTcPrelude sol solverPreludePath
+     a <- k sol
+     _ <- SMT.stop solver
+
+     return a
+
+  where
+  quietLogger = SMT.Logger { SMT.logMessage = \_ -> return ()
+                           , SMT.logLevel   = return 0
+                           , SMT.logSetLevel= \_ -> return ()
+                           , SMT.logTab     = return ()
+                           , SMT.logUntab   = return ()
+                           }
+
+
+-- | Load the definitions used for type checking.
+loadTcPrelude :: Solver -> [FilePath] {- ^ Search in this paths -} -> IO ()
+loadTcPrelude s [] = loadString s cryptolTcContents
+loadTcPrelude s (p : ps) =
+  do let file = p </> "CryptolTC.z3"
+     yes <- doesFileExist file
+     if yes then loadFile s file
+            else loadTcPrelude s ps
+
+
+loadFile :: Solver -> FilePath -> IO ()
+loadFile s file = loadString s =<< StrictIO.readFile file
+
+loadString :: Solver -> String -> IO ()
+loadString s str = go (dropComments str)
+  where
+  go txt
+    | all isSpace txt = return ()
+    | otherwise =
+      case SMT.readSExpr txt of
+        Just (e,rest) -> SMT.command (solver s) e >> go rest
+        Nothing       -> panic "loadFile" [ "Failed to parse SMT file."
+                                          , txt
+                                          ]
+
+  dropComments = unlines . map dropComment . lines
+  dropComment xs = case break (== ';') xs of
+                     (as,_:_) -> as
+                     _ -> xs
+
+
+
+
+--------------------------------------------------------------------------------
+-- Debugging
+
+
+debugBlock :: Solver -> String -> IO a -> IO a
+debugBlock s@Solver { .. } name m =
+  do debugLog s name
+     SMT.logTab logger
+     a <- m
+     SMT.logUntab logger
+     return a
+
+class DebugLog t where
+  debugLog :: Solver -> t -> IO ()
+
+  debugLogList :: Solver -> [t] -> IO ()
+  debugLogList s ts = case ts of
+                        [] -> debugLog s "(none)"
+                        _  -> mapM_ (debugLog s) ts
+
+instance DebugLog Char where
+  debugLog s x     = SMT.logMessage (logger s) (show x)
+  debugLogList s x = SMT.logMessage (logger s) x
+
+instance DebugLog a => DebugLog [a] where
+  debugLog = debugLogList
+
+instance DebugLog a => DebugLog (Maybe a) where
+  debugLog s x = case x of
+                   Nothing -> debugLog s "(nothing)"
+                   Just a  -> debugLog s a
+
+instance DebugLog Doc where
+  debugLog s x = debugLog s (show x)
+
+instance DebugLog Type where
+  debugLog s x = debugLog s (pp x)
+
+instance DebugLog Goal where
+  debugLog s x = debugLog s (goal x)
+
+instance DebugLog Subst where
+  debugLog s x = debugLog s (pp x)
+--------------------------------------------------------------------------------
+
+
+
 
 
 -- | Returns goals that were not proved
 proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
 proveImp sol ps gs0 =
   debugBlock sol "PROVE IMP" $
-  do let s = rawSolver sol
+  do let gs1       = concatMap flatGoal gs0
-     let gs1       = concatMap flatGoal gs0
          (gs,rest) = partition (isNumeric . goal) gs1
          numAsmp   = filter isNumeric (concatMap pSplitAnd ps)
-         vs        = Set.toList $ fvs (numAsmp, map goal gs)
+         vs        = Set.toList (fvs (numAsmp, map goal gs))
-
      tvs <- debugBlock sol "VARIABLES" $
-       do SMT.push s
+       do SMT.push (solver sol)
-          Map.fromList <$> zipWithM (declareVar s) [ 0 .. ] vs
+          Map.fromList <$> zipWithM (declareVar sol) [ 0 .. ] vs
      debugBlock sol "ASSUMPTIONS" $
-       mapM_ (assume s tvs) numAsmp
+       mapM_ (assume sol tvs) numAsmp
      gs' <- mapM (prove sol tvs) gs
-     SMT.pop s
+     SMT.pop (solver sol)
      return (catMaybes gs' ++ rest)
 
 -- | Check if the given goals are known to be unsolvable.
 checkUnsolvable :: Solver -> [Goal] -> IO Bool
 checkUnsolvable sol gs0 =
   debugBlock sol "CHECK UNSOLVABLE" $
-  do let s  = rawSolver sol
+  do let ps = filter isNumeric
-         ps = filter isNumeric
             $ map goal
             $ concatMap flatGoal gs0
-         vs = Set.toList $ fvs ps
+         vs = Set.toList (fvs ps)
      tvs <- debugBlock sol "VARIABLES" $
-       do SMT.push s
+       do push sol
-          mapM_ (debugLog sol) (map show vs)
+          Map.fromList <$> zipWithM (declareVar sol) [ 0 .. ] vs
-          Map.fromList <$> zipWithM (declareVar s) [ 0 .. ] vs
      ans <- unsolvable sol tvs ps
-     SMT.pop s
+     pop sol
      return ans
 
+tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe Subst)
+tryGetModel sol as ps =
+  do push sol
+     tvs <- Map.fromList <$> zipWithM (declareVar sol) [ 0 .. ] as
+     mapM_ (assume sol tvs) ps
+     sat <- SMT.check (solver sol)
+     su <- case sat of
+             SMT.Sat ->
+               case as of
+                 [] -> return (Just emptySubst)
+                 _ -> do res <- SMT.getExprs (solver sol) (Map.elems tvs)
+                         let parse x = do e <- Map.lookup x tvs
+                                          t <- parseNum =<< lookup e res
+                                          return (x, t)
+                         return (listSubst <$> mapM parse as)
+             _ -> return Nothing
+     pop sol
+     return su
+
+  where
+  parseNum a
+    | SMT.Other s <- a
+    , SMT.List [con,val,isFin,isErr] <- s
+    , SMT.Atom "mk-infnat" <- con
+    , SMT.Atom "false"     <- isErr
+    , SMT.Atom fin         <- isFin
+    , SMT.Atom v           <- val
+    , Just n               <- readMaybe v
+    = Just (if fin == "false" then tInf else tNum (n :: Integer))
+
+  parseNum _ = Nothing
+
 --------------------------------------------------------------------------------
 
-declareVar :: SMT.Solver -> Int -> TVar -> IO (TVar, SExpr)
+push :: Solver -> IO ()
-declareVar s x v = do let name = (if isFreeTV v then "fv" else "kv") ++ show x
+push sol = SMT.push (solver sol)
-                      e <- SMT.declare s name cryInfNat
+
-                      SMT.assert s (SMT.fun "cryVar" [ e ])
+pop :: Solver -> IO ()
+pop sol = SMT.pop (solver sol)
+
+
+declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
+declareVar s x v =
+  do let name = (if isFreeTV v then "fv" else "kv") ++ show x
+     e <- SMT.declare (solver s) name cryInfNat
+     SMT.assert (solver s) (SMT.fun "cryVar" [ e ])
      return (v,e)
 
-assume :: SMT.Solver -> TVars -> Prop -> IO ()
+assume :: Solver -> TVars -> Prop -> IO ()
-assume s tvs p = SMT.assert s (SMT.fun "cryAssume" [ toSMT tvs p ])
+assume s tvs p = SMT.assert (solver s) (SMT.fun "cryAssume" [ toSMT tvs p ])
 
 prove :: Solver -> TVars -> Goal -> IO (Maybe Goal)
 prove sol tvs g =
   debugBlock sol "PROVE" $
-  do let s = rawSolver sol
+  do let s = solver sol
-     SMT.push s
+     push sol
      SMT.assert s (SMT.fun "cryProve" [ toSMT tvs (goal g) ])
      res <- SMT.check s
-     SMT.pop s
+     pop sol
      case res of
        SMT.Unsat -> return Nothing
        _         -> return (Just g)
@@ -81,11 +267,10 @@ prove sol tvs g =
 unsolvable :: Solver -> TVars -> [Prop] -> IO Bool
 unsolvable sol tvs ps =
   debugBlock sol "UNSOLVABLE" $
-  do let s = rawSolver sol
+  do SMT.push (solver sol)
-     SMT.push s
+     mapM_ (assume sol tvs) ps
-     mapM_ (assume s tvs) ps
+     res <- SMT.check (solver sol)
-     res <- SMT.check s
+     SMT.pop (solver sol)
-     SMT.pop s
      case res of
        SMT.Unsat -> return True
        _         -> return False
@@ -161,9 +346,6 @@ instance Mk Integer where
 instance Mk TVar where
   mk tvs _ x = tvs Map.! x
 
-instance Mk TParam where
-  mk tvs f x = mk tvs f (tpVar x)
-
 instance Mk Type where
   mk tvs f x = SMT.fun f [toSMT tvs x]
 

tests/issues/issue002.icry.stdout

@@ -1,4 +1,4 @@
 Loading module Cryptol
-(5, True).0 : {a} (fin a, a >= 3) => [a]
+(5, True).0 : {a} (a >= 3, fin a) => [a]
-((5, True), False).0 : {a} (fin a, a >= 3) => ([a], Bit)
+((5, True), False).0 : {a} (a >= 3, fin a) => ([a], Bit)
-(((5, True), False).0).0 : {a} (fin a, a >= 3) => [a]
+(((5, True), False).0).0 : {a} (a >= 3, fin a) => [a]

tests/issues/padding.icry.stdout

@@ -1,6 +1,6 @@
 Loading module Cryptol
-Assuming a = 5
+Assuming a = inf
 Assuming b = 5
 [[0x01, 0x02, 0x03, 0x04, 0x05], [0x06, 0x07, 0x08, 0x09, 0x0a],
  [0x0b, 0x0c, 0x0d, 0x0e, 0x0f], [0x10, 0x11, 0x12, 0x13, 0x14],
- [0x15, 0x16, 0x17, 0x18, 0x00]]
+ [0x15, 0x16, 0x17, 0x18, 0x00], ...]

tests/mono-binds/test03.icry.stdout

@@ -9,8 +9,8 @@ test03::test = \{a} (fin a, a >= width a) ->
                test03::foo a <> <>
                where
                  /* Not recursive */
-                 test03::foo : {b} (fin b, b >= width a) => [b]
+                 test03::foo : {b} (b >= width a, fin b) => [b]
-                 test03::foo = \{b} (fin b, b >= width a) ->
+                 test03::foo = \{b} (b >= width a, fin b) ->
                                Cryptol::demote a b <> <> <>
                  
                

tests/mono-binds/test04.icry.stdout

@@ -4,8 +4,8 @@ Loading module test04
 module test04
 import Cryptol
 /* Not recursive */
-test04::test : {a, b} (fin b, b >= 4) => a -> ((a, ()), (a, [b]))
+test04::test : {a, b} (b >= 4, fin b) => a -> ((a, ()), (a, [b]))
-test04::test = \{a, b} (fin b, b >= 4) (a : a) ->
+test04::test = \{a, b} (b >= 4, fin b) (a : a) ->
                (test04::f () (), test04::f [b] (Cryptol::demote 10 b <> <> <>))
                where
                  /* Not recursive */

tests/mono-binds/test05.icry.stdout

@@ -14,8 +14,8 @@ test05::foo : [10]
 test05::foo = Cryptol::demote 10 10 <> <> <>
 
 /* Not recursive */
-test05::test : {a, b, c} (fin c, c >= 4) => [a]b -> [c]
+test05::test : {a, b, c} (c >= 4, fin c) => [a]b -> [c]
-test05::test = \{a, b, c} (fin c, c >= 4) (a : [a]b) ->
+test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
                Cryptol::demote 10 c <> <> <>
                where
                  /* Not recursive */
@@ -60,8 +60,8 @@ test05::foo : [10]
 test05::foo = Cryptol::demote 10 10 <> <> <>
 
 /* Not recursive */
-test05::test : {a, b, c} (fin c, c >= 4) => [a]b -> [c]
+test05::test : {a, b, c} (c >= 4, fin c) => [a]b -> [c]
-test05::test = \{a, b, c} (fin c, c >= 4) (a : [a]b) ->
+test05::test = \{a, b, c} (c >= 4, fin c) (a : [a]b) ->
                Cryptol::demote 10 c <> <> <>
                where
                  /* Not recursive */