-- |
-- Module      :  Cryptol.TypeCheck.Solver.SMT
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE FlexibleContexts #-}
{-# Language FlexibleInstances #-}
{-# LANGUAGE PatternGuards #-}

module Cryptol.TypeCheck.Solver.SMT
  ( -- * Setup
    Solver
  , SolverConfig
  , withSolver
  , startSolver
  , stopSolver
  , isNumeric
  , resetSolver

    -- * Debugging
  , debugBlock
  , debugLog

    -- * Proving stuff
  , proveImp
  , checkUnsolvable
  , tryGetModel
  , shrinkModel

    -- * Lower level interactions
  , inNewFrame, TVars, declareVars, assume, unsolvable
  , push, pop
  ) 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,isJust)
import           Data.List(partition)
import           Control.Exception
import           Control.Monad(msum,zipWithM,void)
import           Data.Char(isSpace)
import           Text.Read(readMaybe)
import           System.IO(IOMode(..), hClose, openFile)
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 )




-- | An SMT solver packed with a logger for debugging.
data Solver = Solver
  { Solver -> Solver
solver    :: SMT.Solver
    -- ^ The actual solver

  , Solver -> Logger
logger    :: SMT.Logger
    -- ^ For debugging
  }

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)

-- | Start a fresh solver instance
startSolver :: IO () -> SolverConfig -> IO Solver
startSolver :: IO () -> SolverConfig -> IO Solver
startSolver IO ()
onExit SolverConfig
sCfg =
   do let smtFileEnabled :: Bool
smtFileEnabled = Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (SolverConfig -> Maybe String
solverSmtFile SolverConfig
sCfg)
      (Logger
logger, Maybe (IO ())
mbLoggerCloseHdl) <-
        -- There are two scenarios under which we want to explicitly log SMT
        -- solver interactions:
        --
        -- 1. The user wants to debug-print interactions with the `tcDebug`
        --    option
        -- 2. The user wants to write interactions to the `tcSmtFile` option
        --
        -- We enable logging if either one is true.
        if (SolverConfig -> Int
solverVerbose SolverConfig
sCfg) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
|| Bool
smtFileEnabled
        then case SolverConfig -> Maybe String
solverSmtFile SolverConfig
sCfg of
               Maybe String
Nothing ->
                 do Logger
logger <- Int -> IO Logger
SMT.newLogger Int
0
                    (Logger, Maybe (IO ())) -> IO (Logger, Maybe (IO ()))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Logger
logger, Maybe (IO ())
forall a. Maybe a
Nothing)
               Just String
file ->
                 do Handle
loggerHdl <- String -> IOMode -> IO Handle
openFile String
file IOMode
WriteMode
                    Logger
logger <- Handle -> Int -> IO Logger
SMT.newLoggerWithHandle Handle
loggerHdl Int
0
                    (Logger, Maybe (IO ())) -> IO (Logger, Maybe (IO ()))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Logger
logger, IO () -> Maybe (IO ())
forall a. a -> Maybe a
Just (Handle -> IO ()
hClose Handle
loggerHdl))
        else (Logger, Maybe (IO ())) -> IO (Logger, Maybe (IO ()))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Logger
quietLogger, Maybe (IO ())
forall a. Maybe a
Nothing)
      let smtDbg :: Maybe Logger
smtDbg = if (SolverConfig -> Int
solverVerbose SolverConfig
sCfg) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 Bool -> Bool -> Bool
|| Bool
smtFileEnabled
                   then Logger -> Maybe Logger
forall a. a -> Maybe a
Just Logger
logger
                   else Maybe Logger
forall a. Maybe a
Nothing
      Solver
solver <- Config -> IO Solver
SMT.newSolverWithConfig
                  (String -> [String] -> Config
SMT.defaultConfig (SolverConfig -> String
solverPath SolverConfig
sCfg) (SolverConfig -> [String]
solverArgs SolverConfig
sCfg))
                    { SMT.solverOnExit =
                        Just $ \ExitCode
_exitCode ->
                        do IO ()
onExit
                           Maybe (IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ Maybe (IO ())
mbLoggerCloseHdl
                    , SMT.solverLogger =
                        maybe SMT.noSolverLogger SMT.smtSolverLogger smtDbg
                    }
      let sol :: Solver
sol = Solver -> Logger -> Solver
Solver Solver
solver Logger
logger
      Solver -> SolverConfig -> IO ()
setupSolver Solver
sol SolverConfig
sCfg
      Solver -> IO Solver
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
sol

  where
  quietLogger :: Logger
quietLogger = SMT.Logger { logMessage :: String -> IO ()
SMT.logMessage = \String
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                           , logLevel :: IO Int
SMT.logLevel   = Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
                           , logSetLevel :: Int -> IO ()
SMT.logSetLevel= \Int
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                           , logTab :: IO ()
SMT.logTab     = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                           , logUntab :: IO ()
SMT.logUntab   = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                           }

-- | Shut down a solver instance
stopSolver :: Solver -> IO ()
stopSolver :: Solver -> IO ()
stopSolver 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)

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

-- | Execute a computation with a fresh solver instance.
withSolver :: IO () -> SolverConfig -> (Solver -> IO a) -> IO a
withSolver :: forall a. IO () -> SolverConfig -> (Solver -> IO a) -> IO a
withSolver IO ()
onExit SolverConfig
cfg = IO Solver -> (Solver -> IO ()) -> (Solver -> IO a) -> IO a
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

-- | Load the definitions used for type checking.
loadTcPrelude :: Solver -> [FilePath] {- ^ Search in this paths -} -> 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 (String -> IO ()) -> IO String -> IO ()
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
    | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
txt = () -> IO ()
forall a. a -> IO a
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 IO SExpr -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> IO ()
go String
rest
        Maybe (SExpr, String)
Nothing       -> String -> [String] -> IO ()
forall a. HasCallStack => String -> [String] -> a
panic String
"loadFile" [ String
"Failed to parse SMT file."
                                          , String
txt
                                          ]

  dropComments :: String -> String
dropComments = [String] -> String
unlines ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
dropComment ([String] -> [String])
-> (String -> [String]) -> String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
  dropComment :: String -> String
dropComment String
xs = case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
';') String
xs of
                     (String
as,Char
_:String
_) -> String
as
                     (String, String)
_ -> String
xs




--------------------------------------------------------------------------------
-- Debugging


debugBlock :: Solver -> String -> IO a -> IO a
debugBlock :: forall a. Solver -> String -> IO a -> IO a
debugBlock s :: Solver
s@Solver { Logger
Solver
solver :: Solver -> Solver
logger :: Solver -> Logger
solver :: Solver
logger :: Logger
.. } String
name IO a
m =
  do Solver -> String -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (String
";;; " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name)
     Logger -> IO ()
SMT.logTab Logger
logger
     a
a <- IO a
m
     Logger -> IO ()
SMT.logUntab Logger
logger
     a -> IO a
forall a. 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 Solver
s [t]
ts = case [t]
ts of
                        [] -> Solver -> String -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s String
"(none)"
                        [t]
_  -> (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 Solver
s Char
x     = Logger -> String -> IO ()
SMT.logMessage (Solver -> Logger
logger Solver
s) (Char -> String
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 = Solver -> [a] -> IO ()
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 -> Solver -> String -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s String
"(nothing)"
                   Just 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 Solver
s Doc
x = Solver -> String -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Doc -> String
forall a. Show a => a -> String
show Doc
x)

instance DebugLog Type where
  debugLog :: Solver -> Type -> IO ()
debugLog Solver
s 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 Solver
s 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 Solver
s 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)
--------------------------------------------------------------------------------


-- | Returns goals that were not proved
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
proveImp :: Solver -> [Type] -> [Goal] -> IO [Goal]
proveImp Solver
sol [Type]
ps [Goal]
gs0 =
  Solver -> String -> IO [Goal] -> IO [Goal]
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"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
         ([Goal]
gs,[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 -> String -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"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) [ Int
0 .. ] [TVar]
vs
     Solver -> String -> IO () -> IO ()
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> IO a
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)

-- | Check if the given goals are known to be unsolvable.
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable Solver
sol [Goal]
gs0 =
  Solver -> String -> IO Bool -> IO Bool
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"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 -> String -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"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) [ 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
     Bool -> IO Bool
forall a. a -> IO a
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 =
  Solver
-> String -> IO (Maybe [(TVar, Nat')]) -> IO (Maybe [(TVar, Nat')])
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"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) [ Int
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
             Result
SMT.Sat ->
               case [TVar]
as of
                 [] -> Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TVar, Nat')] -> Maybe [(TVar, Nat')]
forall a. a -> Maybe a
Just [])
                 [TVar]
_ -> 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 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 a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x, Nat'
t)
                         Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall a. a -> IO a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TVar -> Maybe (TVar, Nat')
parse [TVar]
as)
             Result
_ -> Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall a. a -> IO a
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 a. a -> IO a
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               <- String -> Maybe Integer
forall a. Read a => String -> Maybe a
readMaybe String
v
    = Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (if String
fin String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"false" then Nat'
Inf else Integer -> Nat'
Nat Integer
n)

  parseNum Value
_ = 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 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) (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 [(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) (TVar, Nat') -> [(TVar, Nat')] -> [(TVar, Nat')]
forall a. a -> [a] -> [a]
: [(TVar, Nat')]
done) [Type]
ps [(TVar, Nat')]
more
  go [(TVar, Nat')]
done [Type]
_ [] = [(TVar, Nat')] -> IO [(TVar, Nat')]
forall a. a -> IO a
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 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> IO Integer
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
0
    | Bool
otherwise =
      do let k1 :: Integer
k1 = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
k Integer
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
           Maybe [(TVar, Nat')]
Nothing     -> Integer -> IO Integer
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
k
           Just [(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 Integer
k2) -> [Type] -> TVar -> Integer -> IO Integer
shrink1 [Type]
ps TVar
x Integer
k2
               Maybe Nat'
_ -> String -> [String] -> IO Integer
forall a. HasCallStack => String -> [String] -> a
panic String
"shrink" [String
"model is missing variable", TVar -> String
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
     a -> IO a
forall a. a -> IO a
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") String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
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 ])
     (TVar, SExpr) -> IO (TVar, SExpr)
forall a. a -> IO a
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 =
  [(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) [ Int
0 .. ]
                                             [ TVar
v | TVar
v <- [TVar]
vs, TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
v Kind -> Kind -> Bool
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 =
  Solver -> String -> IO (Maybe Goal) -> IO (Maybe Goal)
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"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 (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 -> Maybe Goal -> IO (Maybe Goal)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Goal
forall a. Maybe a
Nothing
       Result
_         -> Maybe Goal -> IO (Maybe Goal)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Maybe Goal
forall a. a -> Maybe a
Just Goal
g)


-- | Check if some numeric goals are known to be unsolvable.
unsolvable :: Solver -> TVars -> [Prop] -> IO Bool
unsolvable :: Solver -> Map TVar SExpr -> [Type] -> IO Bool
unsolvable Solver
sol Map TVar SExpr
tvs [Type]
ps =
  Solver -> String -> IO Bool -> IO Bool
forall a. Solver -> String -> IO a -> IO a
debugBlock Solver
sol String
"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
       Result
SMT.Unsat -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       Result
_         -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False



--------------------------------------------------------------------------------

-- | Split up the 'And' in a goal
flatGoal :: Goal -> [Goal]
flatGoal :: Goal -> [Goal]
flatGoal Goal
g = [ Goal
g { goal = p } | Type
p <- Type -> [Type]
pSplitAnd (Goal -> Type
goal Goal
g) ]


-- | Assumes no 'And'
isNumeric :: Prop -> Bool
isNumeric :: Type -> Bool
isNumeric 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, (Type -> Match Type) -> Match Bool
forall {m :: * -> *} {a}. Monad m => (Type -> m a) -> m Bool
is Type -> Match Type
aPrime ]
  where
  is :: (Type -> m a) -> m Bool
is Type -> m a
f = Type -> m a
f Type
ty m a -> m Bool -> m Bool
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall a. a -> m a
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 = SExpr -> Match SExpr -> SExpr
forall a. a -> Match a -> a
matchDefault (String -> [String] -> SExpr
forall a. HasCallStack => String -> [String] -> a
panic String
"toSMT" [ String
"Unexpected type", Type -> String
forall a. Show a => a -> String
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 (\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 () -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryInf"
  , Pat Type Integer
aNat            Pat Type Integer -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryNat"

  , Type -> Match Type
aFin            (Type -> Match Type)
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryFin"
  , Type -> Match Type
aPrime          (Type -> Match Type)
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryPrime"
  , Type -> Match (Type, Type)
(|=|)           (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryEq"
  , Type -> Match (Type, Type)
(|/=|)          (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryNeq"
  , Type -> Match (Type, Type)
(|>=|)          (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryGeq"
  , Type -> Match (Type, Type)
aAnd            (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryAnd"
  , Pat Type ()
aTrue           Pat Type () -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryTrue"

  , Type -> Match (Type, Type)
anAdd           (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryAdd"
  , Type -> Match (Type, Type)
(|-|)           (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"crySub"
  , Type -> Match (Type, Type)
aMul            (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryMul"
  , Type -> Match (Type, Type)
(|^|)           (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryExp"
  , Type -> Match (Type, Type)
(|/|)           (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryDiv"
  , Type -> Match (Type, Type)
(|%|)           (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryMod"
  , Type -> Match (Type, Type)
aMin            (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryMin"
  , Type -> Match (Type, Type)
aMax            (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryMax"
  , Type -> Match Type
aWidth          (Type -> Match Type)
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryWidth"
  , Type -> Match (Type, Type)
aCeilDiv        (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryCeilDiv"
  , Type -> Match (Type, Type)
aCeilMod        (Type -> Match (Type, Type))
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryCeilMod"
  , Pat Type (Type, Type, Type)
aLenFromThenTo  Pat Type (Type, Type, Type)
-> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryLenFromThenTo"

  , Kind -> Pat Type ()
anError Kind
KNum    Pat Type () -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryErr"
  , Kind -> Pat Type ()
anError Kind
KProp   Pat Type () -> String -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> String -> Map TVar SExpr -> Type -> Match SExpr
~> String
"cryErrProp"

  , Pat Type TVar
aTVar           Pat Type TVar -> String -> Map TVar SExpr -> Type -> Match SExpr
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 Match a -> (a -> Match SExpr) -> Match SExpr
forall a b. Match a -> (a -> Match b) -> Match b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
a -> SExpr -> Match SExpr
forall a. a -> Match a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map TVar SExpr -> String -> a -> SExpr
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 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 -> 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 ]

--------------------------------------------------------------------------------