{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE FlexibleContexts #-}
{-# Language FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE TypeSynonymInstances #-}
module Cryptol.TypeCheck.Solver.SMT
(
Solver
, withSolver
, isNumeric
, debugBlock
, debugLog
, proveImp
, checkUnsolvable
, tryGetModel
, shrinkModel
) where
import SimpleSMT (SExpr)
import qualified SimpleSMT as SMT
import Data.Map ( Map )
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe(catMaybes)
import Data.List(partition)
import Control.Exception
import Control.Monad(msum,zipWithM,void)
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.InferTypes
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.TypeCheck.TypePat hiding ((~>),(~~>))
import Cryptol.TypeCheck.Subst(Subst)
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
data Solver = Solver
{ Solver -> Solver
solver :: SMT.Solver
, Solver -> Logger
logger :: SMT.Logger
}
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
withSolver SolverConfig{ .. } =
IO Solver -> (Solver -> IO ()) -> (Solver -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket
(do Logger
logger <- if Int
solverVerbose Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then Int -> IO Logger
SMT.newLogger 0
else Logger -> IO Logger
forall (m :: * -> *) a. Monad m => a -> m a
return Logger
quietLogger
let smtDbg :: Maybe Logger
smtDbg = if Int
solverVerbose Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then Logger -> Maybe Logger
forall a. a -> Maybe a
Just Logger
logger else Maybe Logger
forall a. Maybe a
Nothing
Solver
solver <- FilePath -> [FilePath] -> Maybe Logger -> IO Solver
SMT.newSolver FilePath
solverPath [FilePath]
solverArgs Maybe Logger
smtDbg
Bool
_ <- Solver -> FilePath -> FilePath -> IO Bool
SMT.setOptionMaybe Solver
solver ":global-decls" "false"
let sol :: Solver
sol = Solver :: Solver -> Logger -> Solver
Solver { .. }
Solver -> [FilePath] -> IO ()
loadTcPrelude Solver
sol [FilePath]
solverPreludePath
Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
sol)
(\s :: Solver
s -> IO ExitCode -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO ExitCode -> IO ()) -> IO ExitCode -> IO ()
forall a b. (a -> b) -> a -> b
$ Solver -> IO ExitCode
SMT.stop (Solver -> Solver
solver Solver
s))
where
quietLogger :: Logger
quietLogger = Logger :: (FilePath -> IO ())
-> IO Int -> (Int -> IO ()) -> IO () -> IO () -> Logger
SMT.Logger { logMessage :: FilePath -> IO ()
SMT.logMessage = \_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, logLevel :: IO Int
SMT.logLevel = Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return 0
, logSetLevel :: Int -> IO ()
SMT.logSetLevel= \_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, logTab :: IO ()
SMT.logTab = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, logUntab :: IO ()
SMT.logUntab = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
loadTcPrelude :: Solver -> [FilePath] -> IO ()
loadTcPrelude :: Solver -> [FilePath] -> IO ()
loadTcPrelude s :: Solver
s [] = Solver -> FilePath -> IO ()
loadString Solver
s FilePath
cryptolTcContents
loadTcPrelude s :: Solver
s (p :: FilePath
p : ps :: [FilePath]
ps) =
do let file :: FilePath
file = FilePath
p FilePath -> FilePath -> FilePath
</> "CryptolTC.z3"
Bool
yes <- FilePath -> IO Bool
doesFileExist FilePath
file
if Bool
yes then Solver -> FilePath -> IO ()
loadFile Solver
s FilePath
file
else Solver -> [FilePath] -> IO ()
loadTcPrelude Solver
s [FilePath]
ps
loadFile :: Solver -> FilePath -> IO ()
loadFile :: Solver -> FilePath -> IO ()
loadFile s :: Solver
s file :: FilePath
file = Solver -> FilePath -> IO ()
loadString Solver
s (FilePath -> IO ()) -> IO FilePath -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO FilePath
StrictIO.readFile FilePath
file
loadString :: Solver -> String -> IO ()
loadString :: Solver -> FilePath -> IO ()
loadString s :: Solver
s str :: FilePath
str = FilePath -> IO ()
go (FilePath -> FilePath
dropComments FilePath
str)
where
go :: FilePath -> IO ()
go txt :: FilePath
txt
| (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace FilePath
txt = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise =
case FilePath -> Maybe (SExpr, FilePath)
SMT.readSExpr FilePath
txt of
Just (e :: SExpr
e,rest :: FilePath
rest) -> Solver -> SExpr -> IO SExpr
SMT.command (Solver -> Solver
solver Solver
s) SExpr
e IO SExpr -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FilePath -> IO ()
go FilePath
rest
Nothing -> FilePath -> [FilePath] -> IO ()
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "loadFile" [ "Failed to parse SMT file."
, FilePath
txt
]
dropComments :: FilePath -> FilePath
dropComments = [FilePath] -> FilePath
unlines ([FilePath] -> FilePath)
-> (FilePath -> [FilePath]) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> FilePath
dropComment ([FilePath] -> [FilePath])
-> (FilePath -> [FilePath]) -> FilePath -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines
dropComment :: FilePath -> FilePath
dropComment xs :: FilePath
xs = case (Char -> Bool) -> FilePath -> (FilePath, FilePath)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== ';') FilePath
xs of
(as :: FilePath
as,_:_) -> FilePath
as
_ -> FilePath
xs
debugBlock :: Solver -> String -> IO a -> IO a
debugBlock :: Solver -> FilePath -> IO a -> IO a
debugBlock s :: Solver
s@Solver { .. } name :: FilePath
name m :: IO a
m =
do Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s FilePath
name
Logger -> IO ()
SMT.logTab Logger
logger
a
a <- IO a
m
Logger -> IO ()
SMT.logUntab Logger
logger
a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
class DebugLog t where
debugLog :: Solver -> t -> IO ()
debugLogList :: Solver -> [t] -> IO ()
debugLogList s :: Solver
s ts :: [t]
ts = case [t]
ts of
[] -> Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s "(none)"
_ -> (t -> IO ()) -> [t] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> t -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s) [t]
ts
instance DebugLog Char where
debugLog :: Solver -> Char -> IO ()
debugLog s :: Solver
s x :: Char
x = Logger -> FilePath -> IO ()
SMT.logMessage (Solver -> Logger
logger Solver
s) (Char -> FilePath
forall a. Show a => a -> FilePath
show Char
x)
debugLogList :: Solver -> FilePath -> IO ()
debugLogList s :: Solver
s x :: FilePath
x = Logger -> FilePath -> IO ()
SMT.logMessage (Solver -> Logger
logger Solver
s) FilePath
x
instance DebugLog a => DebugLog [a] where
debugLog :: Solver -> [a] -> IO ()
debugLog = Solver -> [a] -> IO ()
forall a. DebugLog a => Solver -> [a] -> IO ()
debugLogList
instance DebugLog a => DebugLog (Maybe a) where
debugLog :: Solver -> Maybe a -> IO ()
debugLog s :: Solver
s x :: Maybe a
x = case Maybe a
x of
Nothing -> Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s "(nothing)"
Just a :: a
a -> Solver -> a -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s a
a
instance DebugLog Doc where
debugLog :: Solver -> Doc -> IO ()
debugLog s :: Solver
s x :: Doc
x = Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Doc -> FilePath
forall a. Show a => a -> FilePath
show Doc
x)
instance DebugLog Type where
debugLog :: Solver -> Type -> IO ()
debugLog s :: Solver
s x :: Type
x = Solver -> Doc -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Type -> Doc
forall a. PP a => a -> Doc
pp Type
x)
instance DebugLog Goal where
debugLog :: Solver -> Goal -> IO ()
debugLog s :: Solver
s x :: Goal
x = Solver -> Type -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Goal -> Type
goal Goal
x)
instance DebugLog Subst where
debugLog :: Solver -> Subst -> IO ()
debugLog s :: Solver
s x :: Subst
x = Solver -> Doc -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Subst -> Doc
forall a. PP a => a -> Doc
pp Subst
x)
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
proveImp :: Solver -> [Type] -> [Goal] -> IO [Goal]
proveImp sol :: Solver
sol ps :: [Type]
ps gs0 :: [Goal]
gs0 =
Solver -> FilePath -> IO [Goal] -> IO [Goal]
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "PROVE IMP" (IO [Goal] -> IO [Goal]) -> IO [Goal] -> IO [Goal]
forall a b. (a -> b) -> a -> b
$
do let gs1 :: [Goal]
gs1 = (Goal -> [Goal]) -> [Goal] -> [Goal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Goal -> [Goal]
flatGoal [Goal]
gs0
(gs :: [Goal]
gs,rest :: [Goal]
rest) = (Goal -> Bool) -> [Goal] -> ([Goal], [Goal])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Type -> Bool
isNumeric (Type -> Bool) -> (Goal -> Type) -> Goal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal) [Goal]
gs1
numAsmp :: [Type]
numAsmp = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
isNumeric ((Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd [Type]
ps)
vs :: [TVar]
vs = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (([Type], [Type]) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs ([Type]
numAsmp, (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal [Goal]
gs))
Map TVar SExpr
tvs <- Solver -> FilePath -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "VARIABLES" (IO (Map TVar SExpr) -> IO (Map TVar SExpr))
-> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a b. (a -> b) -> a -> b
$
do Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)
[(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ 0 .. ] [TVar]
vs
Solver -> FilePath -> IO () -> IO ()
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "ASSUMPTIONS" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
(Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
numAsmp
[Maybe Goal]
gs' <- (Goal -> IO (Maybe Goal)) -> [Goal] -> IO [Maybe Goal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Map TVar SExpr -> Goal -> IO (Maybe Goal)
prove Solver
sol Map TVar SExpr
tvs) [Goal]
gs
Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)
[Goal] -> IO [Goal]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe Goal] -> [Goal]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Goal]
gs' [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
rest)
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable sol :: Solver
sol gs0 :: [Goal]
gs0 =
Solver -> FilePath -> IO Bool -> IO Bool
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "CHECK UNSOLVABLE" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
do let ps :: [Type]
ps = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
isNumeric
([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal
([Goal] -> [Type]) -> [Goal] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Goal -> [Goal]) -> [Goal] -> [Goal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Goal -> [Goal]
flatGoal [Goal]
gs0
vs :: [TVar]
vs = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList ([Type] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Type]
ps)
Map TVar SExpr
tvs <- Solver -> FilePath -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "VARIABLES" (IO (Map TVar SExpr) -> IO (Map TVar SExpr))
-> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a b. (a -> b) -> a -> b
$
do Solver -> IO ()
push Solver
sol
[(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ 0 .. ] [TVar]
vs
Bool
ans <- Solver -> Map TVar SExpr -> [Type] -> IO Bool
unsolvable Solver
sol Map TVar SExpr
tvs [Type]
ps
Solver -> IO ()
pop Solver
sol
Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ans
tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar,Nat')])
tryGetModel :: Solver -> [TVar] -> [Type] -> IO (Maybe [(TVar, Nat')])
tryGetModel sol :: Solver
sol as :: [TVar]
as ps :: [Type]
ps =
Solver
-> FilePath
-> IO (Maybe [(TVar, Nat')])
-> IO (Maybe [(TVar, Nat')])
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "TRY GET MODEL" (IO (Maybe [(TVar, Nat')]) -> IO (Maybe [(TVar, Nat')]))
-> IO (Maybe [(TVar, Nat')]) -> IO (Maybe [(TVar, Nat')])
forall a b. (a -> b) -> a -> b
$
do Solver -> IO ()
push Solver
sol
Map TVar SExpr
tvs <- [(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ 0 .. ] [TVar]
as
(Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
ps
Result
sat <- Solver -> IO Result
SMT.check (Solver -> Solver
solver Solver
sol)
Maybe [(TVar, Nat')]
su <- case Result
sat of
SMT.Sat ->
case [TVar]
as of
[] -> Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TVar, Nat')] -> Maybe [(TVar, Nat')]
forall a. a -> Maybe a
Just [])
_ -> do [(SExpr, Value)]
res <- Solver -> [SExpr] -> IO [(SExpr, Value)]
SMT.getExprs (Solver -> Solver
solver Solver
sol) (Map TVar SExpr -> [SExpr]
forall k a. Map k a -> [a]
Map.elems Map TVar SExpr
tvs)
let parse :: TVar -> Maybe (TVar, Nat')
parse x :: TVar
x = do SExpr
e <- TVar -> Map TVar SExpr -> Maybe SExpr
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
x Map TVar SExpr
tvs
Nat'
t <- Value -> Maybe Nat'
parseNum (Value -> Maybe Nat') -> Maybe Value -> Maybe Nat'
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SExpr -> [(SExpr, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup SExpr
e [(SExpr, Value)]
res
(TVar, Nat') -> Maybe (TVar, Nat')
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x, Nat'
t)
Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return ((TVar -> Maybe (TVar, Nat')) -> [TVar] -> Maybe [(TVar, Nat')]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TVar -> Maybe (TVar, Nat')
parse [TVar]
as)
_ -> Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TVar, Nat')]
forall a. Maybe a
Nothing
Solver -> IO ()
pop Solver
sol
Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TVar, Nat')]
su
where
parseNum :: Value -> Maybe Nat'
parseNum a :: Value
a
| SMT.Other s :: SExpr
s <- Value
a
, SMT.List [con :: SExpr
con,val :: SExpr
val,isFin :: SExpr
isFin,isErr :: SExpr
isErr] <- SExpr
s
, SMT.Atom "mk-infnat" <- SExpr
con
, SMT.Atom "false" <- SExpr
isErr
, SMT.Atom fin :: FilePath
fin <- SExpr
isFin
, SMT.Atom v :: FilePath
v <- SExpr
val
, Just n :: Integer
n <- FilePath -> Maybe Integer
forall a. Read a => FilePath -> Maybe a
readMaybe FilePath
v
= Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (if FilePath
fin FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== "false" then Nat'
Inf else Integer -> Nat'
Nat Integer
n)
parseNum _ = Maybe Nat'
forall a. Maybe a
Nothing
shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar,Nat')] -> IO [(TVar,Nat')]
shrinkModel :: Solver -> [TVar] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
shrinkModel sol :: Solver
sol as :: [TVar]
as ps0 :: [Type]
ps0 mdl :: [(TVar, Nat')]
mdl = [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go [] [Type]
ps0 [(TVar, Nat')]
mdl
where
go :: [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go done :: [(TVar, Nat')]
done ps :: [Type]
ps ((x :: TVar
x,Nat k :: Integer
k) : more :: [(TVar, Nat')]
more) =
do Integer
k1 <- [Type] -> TVar -> Integer -> IO Integer
shrink1 [Type]
ps TVar
x Integer
k
[(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go ((TVar
x,Integer -> Nat'
Nat Integer
k1) (TVar, Nat') -> [(TVar, Nat')] -> [(TVar, Nat')]
forall a. a -> [a] -> [a]
: [(TVar, Nat')]
done) ((Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k1 Type -> Type -> Type
>== TVar -> Type
TVar TVar
x) Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps) [(TVar, Nat')]
more
go done :: [(TVar, Nat')]
done ps :: [Type]
ps ((x :: TVar
x,i :: Nat'
i) : more :: [(TVar, Nat')]
more) = [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go ((TVar
x,Nat'
i) (TVar, Nat') -> [(TVar, Nat')] -> [(TVar, Nat')]
forall a. a -> [a] -> [a]
: [(TVar, Nat')]
done) [Type]
ps [(TVar, Nat')]
more
go done :: [(TVar, Nat')]
done _ [] = [(TVar, Nat')] -> IO [(TVar, Nat')]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TVar, Nat')]
done
shrink1 :: [Type] -> TVar -> Integer -> IO Integer
shrink1 ps :: [Type]
ps x :: TVar
x k :: Integer
k
| Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return 0
| Bool
otherwise =
do let k1 :: Integer
k1 = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
k 2
p1 :: Type
p1 = Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k1 Type -> Type -> Type
>== TVar -> Type
TVar TVar
x
Maybe [(TVar, Nat')]
mb <- Solver -> [TVar] -> [Type] -> IO (Maybe [(TVar, Nat')])
tryGetModel Solver
sol [TVar]
as (Type
p1 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps)
case Maybe [(TVar, Nat')]
mb of
Nothing -> Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
k
Just newMdl :: [(TVar, Nat')]
newMdl ->
case TVar -> [(TVar, Nat')] -> Maybe Nat'
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TVar
x [(TVar, Nat')]
newMdl of
Just (Nat k2 :: Integer
k2) -> [Type] -> TVar -> Integer -> IO Integer
shrink1 [Type]
ps TVar
x Integer
k2
_ -> FilePath -> [FilePath] -> IO Integer
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "shrink" ["model is missing variable", TVar -> FilePath
forall a. Show a => a -> FilePath
show TVar
x]
push :: Solver -> IO ()
push :: Solver -> IO ()
push sol :: Solver
sol = Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)
pop :: Solver -> IO ()
pop :: Solver -> IO ()
pop sol :: Solver
sol = Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)
declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar s :: Solver
s x :: Int
x v :: TVar
v =
do let name :: FilePath
name = (if TVar -> Bool
isFreeTV TVar
v then "fv" else "kv") FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
x
SExpr
e <- Solver -> FilePath -> SExpr -> IO SExpr
SMT.declare (Solver -> Solver
solver Solver
s) FilePath
name SExpr
cryInfNat
Solver -> SExpr -> IO ()
SMT.assert (Solver -> Solver
solver Solver
s) (FilePath -> [SExpr] -> SExpr
SMT.fun "cryVar" [ SExpr
e ])
(TVar, SExpr) -> IO (TVar, SExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
v,SExpr
e)
assume :: Solver -> TVars -> Prop -> IO ()
assume :: Solver -> Map TVar SExpr -> Type -> IO ()
assume s :: Solver
s tvs :: Map TVar SExpr
tvs p :: Type
p = Solver -> SExpr -> IO ()
SMT.assert (Solver -> Solver
solver Solver
s) (FilePath -> [SExpr] -> SExpr
SMT.fun "cryAssume" [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
p ])
prove :: Solver -> TVars -> Goal -> IO (Maybe Goal)
prove :: Solver -> Map TVar SExpr -> Goal -> IO (Maybe Goal)
prove sol :: Solver
sol tvs :: Map TVar SExpr
tvs g :: Goal
g =
Solver -> FilePath -> IO (Maybe Goal) -> IO (Maybe Goal)
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "PROVE" (IO (Maybe Goal) -> IO (Maybe Goal))
-> IO (Maybe Goal) -> IO (Maybe Goal)
forall a b. (a -> b) -> a -> b
$
do let s :: Solver
s = Solver -> Solver
solver Solver
sol
Solver -> IO ()
push Solver
sol
Solver -> SExpr -> IO ()
SMT.assert Solver
s (FilePath -> [SExpr] -> SExpr
SMT.fun "cryProve" [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs (Goal -> Type
goal Goal
g) ])
Result
res <- Solver -> IO Result
SMT.check Solver
s
Solver -> IO ()
pop Solver
sol
case Result
res of
SMT.Unsat -> Maybe Goal -> IO (Maybe Goal)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Goal
forall a. Maybe a
Nothing
_ -> Maybe Goal -> IO (Maybe Goal)
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Maybe Goal
forall a. a -> Maybe a
Just Goal
g)
unsolvable :: Solver -> TVars -> [Prop] -> IO Bool
unsolvable :: Solver -> Map TVar SExpr -> [Type] -> IO Bool
unsolvable sol :: Solver
sol tvs :: Map TVar SExpr
tvs ps :: [Type]
ps =
Solver -> FilePath -> IO Bool -> IO Bool
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "UNSOLVABLE" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
do Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)
(Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
ps
Result
res <- Solver -> IO Result
SMT.check (Solver -> Solver
solver Solver
sol)
Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)
case Result
res of
SMT.Unsat -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
_ -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
flatGoal :: Goal -> [Goal]
flatGoal :: Goal -> [Goal]
flatGoal g :: Goal
g = [ Goal
g { goal :: Type
goal = Type
p } | Type
p <- Type -> [Type]
pSplitAnd (Goal -> Type
goal Goal
g) ]
isNumeric :: Prop -> Bool
isNumeric :: Type -> Bool
isNumeric ty :: Type
ty = Bool -> Match Bool -> Bool
forall a. a -> Match a -> a
matchDefault Bool
False (Match Bool -> Bool) -> Match Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Match Bool] -> Match Bool
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|=|), (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|/=|), (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|>=|), (Type -> Match Type) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match Type
aFin ]
where
is :: (Type -> m a) -> m Bool
is f :: Type -> m a
f = Type -> m a
f Type
ty m a -> m Bool -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
type TVars = Map TVar SExpr
cryInfNat :: SExpr
cryInfNat :: SExpr
cryInfNat = FilePath -> SExpr
SMT.const "InfNat"
toSMT :: TVars -> Type -> SExpr
toSMT :: Map TVar SExpr -> Type -> SExpr
toSMT tvs :: Map TVar SExpr
tvs ty :: Type
ty = SExpr -> Match SExpr -> SExpr
forall a. a -> Match a -> a
matchDefault (FilePath -> [FilePath] -> SExpr
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "toSMT" [ "Unexpected type", Type -> FilePath
forall a. Show a => a -> FilePath
show Type
ty ])
(Match SExpr -> SExpr) -> Match SExpr -> SExpr
forall a b. (a -> b) -> a -> b
$ [Match SExpr] -> Match SExpr
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Match SExpr] -> Match SExpr) -> [Match SExpr] -> Match SExpr
forall a b. (a -> b) -> a -> b
$ ((Map TVar SExpr -> Type -> Match SExpr) -> Match SExpr)
-> [Map TVar SExpr -> Type -> Match SExpr] -> [Match SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\f :: Map TVar SExpr -> Type -> Match SExpr
f -> Map TVar SExpr -> Type -> Match SExpr
f Map TVar SExpr
tvs Type
ty)
[ Pat Type ()
aInf Pat Type () -> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryInf"
, Pat Type Integer
aNat Pat Type Integer
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryNat"
, Type -> Match Type
aFin (Type -> Match Type)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryFin"
, Type -> Match (Type, Type)
(|=|) (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryEq"
, Type -> Match (Type, Type)
(|/=|) (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryNeq"
, Type -> Match (Type, Type)
(|>=|) (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryGeq"
, Type -> Match (Type, Type)
aAnd (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryAnd"
, Pat Type ()
aTrue Pat Type () -> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryTrue"
, Type -> Match (Type, Type)
anAdd (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryAdd"
, Type -> Match (Type, Type)
(|-|) (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "crySub"
, Type -> Match (Type, Type)
aMul (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryMul"
, Type -> Match (Type, Type)
(|^|) (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryExp"
, Type -> Match (Type, Type)
(|/|) (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryDiv"
, Type -> Match (Type, Type)
(|%|) (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryMod"
, Type -> Match (Type, Type)
aMin (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryMin"
, Type -> Match (Type, Type)
aMax (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryMax"
, Type -> Match Type
aWidth (Type -> Match Type)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryWidth"
, Type -> Match (Type, Type)
aCeilDiv (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryCeilDiv"
, Type -> Match (Type, Type)
aCeilMod (Type -> Match (Type, Type))
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryCeilMod"
, Pat Type (Type, Type, Type)
aLenFromThenTo Pat Type (Type, Type, Type)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryLenFromThenTo"
, Kind -> Pat Type TCErrorMessage
anError Kind
KNum Pat Type TCErrorMessage
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryErr"
, Kind -> Pat Type TCErrorMessage
anError Kind
KProp Pat Type TCErrorMessage
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryErrProp"
, Pat Type TVar
aTVar Pat Type TVar -> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "(unused)"
]
(~>) :: Mk a => (Type -> Match a) -> String -> TVars -> Type -> Match SExpr
(m :: Type -> Match a
m ~> :: (Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> f :: FilePath
f) tvs :: Map TVar SExpr
tvs t :: Type
t = Type -> Match a
m Type
t Match a -> (a -> Match SExpr) -> Match SExpr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: a
a -> SExpr -> Match SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (Map TVar SExpr -> FilePath -> a -> SExpr
forall t. Mk t => Map TVar SExpr -> FilePath -> t -> SExpr
mk Map TVar SExpr
tvs FilePath
f a
a)
class Mk t where
mk :: TVars -> String -> t -> SExpr
instance Mk () where
mk :: Map TVar SExpr -> FilePath -> () -> SExpr
mk _ f :: FilePath
f _ = FilePath -> SExpr
SMT.const FilePath
f
instance Mk Integer where
mk :: Map TVar SExpr -> FilePath -> Integer -> SExpr
mk _ f :: FilePath
f x :: Integer
x = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [ Integer -> SExpr
SMT.int Integer
x ]
instance Mk TVar where
mk :: Map TVar SExpr -> FilePath -> TVar -> SExpr
mk tvs :: Map TVar SExpr
tvs _ x :: TVar
x = Map TVar SExpr
tvs Map TVar SExpr -> TVar -> SExpr
forall k a. Ord k => Map k a -> k -> a
Map.! TVar
x
instance Mk Type where
mk :: Map TVar SExpr -> FilePath -> Type -> SExpr
mk tvs :: Map TVar SExpr
tvs f :: FilePath
f x :: Type
x = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x]
instance Mk TCErrorMessage where
mk :: Map TVar SExpr -> FilePath -> TCErrorMessage -> SExpr
mk _ f :: FilePath
f _ = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f []
instance Mk (Type,Type) where
mk :: Map TVar SExpr -> FilePath -> (Type, Type) -> SExpr
mk tvs :: Map TVar SExpr
tvs f :: FilePath
f (x :: Type
x,y :: Type
y) = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
y]
instance Mk (Type,Type,Type) where
mk :: Map TVar SExpr -> FilePath -> (Type, Type, Type) -> SExpr
mk tvs :: Map TVar SExpr
tvs f :: FilePath
f (x :: Type
x,y :: Type
y,z :: Type
z) = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
y, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
z ]