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