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

module Cryptol.TypeCheck.Solver.SMT
  ( -- * Setup
    Solver
  , withSolver
  , isNumeric

    -- * Debugging
  , debugBlock
  , debugLog

    -- * Proving stuff
  , 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 -- ( Doc )




-- | 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
  }

-- | Execute a computation with a fresh solver instance.
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
withSolver SolverConfig{ Int
FilePath
[FilePath]
solverPreludePath :: SolverConfig -> [FilePath]
solverVerbose :: SolverConfig -> Int
solverArgs :: SolverConfig -> [FilePath]
solverPath :: SolverConfig -> FilePath
solverPreludePath :: [FilePath]
solverVerbose :: Int
solverArgs :: [FilePath]
solverPath :: FilePath
.. } =
     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
> Int
0 then Int -> IO Logger
SMT.newLogger Int
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
> Int
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 FilePath
":global-decls" FilePath
"false"
           -- SMT.setLogic solver "QF_LIA"
           let sol :: Solver
sol = Solver :: Solver -> Logger -> Solver
Solver { Solver
Logger
solver :: Solver
logger :: Logger
logger :: 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)
       (\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 = \FilePath
_ -> () -> 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 Int
0
                           , logSetLevel :: Int -> IO ()
SMT.logSetLevel= \Int
_ -> () -> 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 ()
                           }


-- | Load the definitions used for type checking.
loadTcPrelude :: Solver -> [FilePath] {- ^ Search in this paths -} -> IO ()
loadTcPrelude :: Solver -> [FilePath] -> IO ()
loadTcPrelude Solver
s [] = Solver -> FilePath -> IO ()
loadString Solver
s FilePath
cryptolTcContents
loadTcPrelude Solver
s (FilePath
p : [FilePath]
ps) =
  do let file :: FilePath
file = FilePath
p FilePath -> 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 Solver
s 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 Solver
s FilePath
str = FilePath -> IO ()
go (FilePath -> FilePath
dropComments FilePath
str)
  where
  go :: FilePath -> IO ()
go 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 (SExpr
e,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
        Maybe (SExpr, FilePath)
Nothing       -> FilePath -> [FilePath] -> IO ()
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"loadFile" [ FilePath
"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 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
== Char
';') FilePath
xs of
                     (FilePath
as,Char
_:FilePath
_) -> FilePath
as
                     (FilePath, FilePath)
_ -> FilePath
xs




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


debugBlock :: Solver -> String -> IO a -> IO a
debugBlock :: Solver -> FilePath -> IO a -> IO a
debugBlock s :: Solver
s@Solver { Solver
Logger
logger :: Logger
solver :: Solver
logger :: Solver -> Logger
solver :: Solver -> Solver
.. } FilePath
name 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 Solver
s [t]
ts = case [t]
ts of
                        [] -> Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s FilePath
"(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 -> 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 Solver
s 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 Solver
s Maybe a
x = case Maybe a
x of
                   Maybe a
Nothing -> Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s FilePath
"(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 -> 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 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 -> FilePath -> IO [Goal] -> IO [Goal]
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol FilePath
"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 -> FilePath -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol FilePath
"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 -> FilePath -> IO () -> IO ()
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol FilePath
"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)

-- | 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 -> FilePath -> IO Bool -> IO Bool
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol FilePath
"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 FilePath
"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 (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
-> FilePath
-> IO (Maybe [(TVar, Nat')])
-> IO (Maybe [(TVar, Nat')])
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol FilePath
"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 (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 (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)
             Result
_ -> 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 Value
a
    | SMT.Other SExpr
s <- Value
a
    , SMT.List [SExpr
con,SExpr
val,SExpr
isFin,SExpr
isErr] <- SExpr
s
    , SMT.Atom FilePath
"mk-infnat" <- SExpr
con
    , SMT.Atom FilePath
"false"     <- SExpr
isErr
    , SMT.Atom FilePath
fin         <- SExpr
isFin
    , SMT.Atom FilePath
v           <- SExpr
val
    , Just 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
== FilePath
"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 (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 (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 (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'
_ -> FilePath -> [FilePath] -> IO Integer
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"shrink" [FilePath
"model is missing variable", TVar -> FilePath
forall a. Show a => a -> FilePath
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)


declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
s Int
x TVar
v =
  do let name :: FilePath
name = (if TVar -> Bool
isFreeTV TVar
v then FilePath
"fv" else FilePath
"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 FilePath
"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 Solver
s Map TVar SExpr
tvs Type
p = Solver -> SExpr -> IO ()
SMT.assert (Solver -> Solver
solver Solver
s) (FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
"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 -> FilePath -> IO (Maybe Goal) -> IO (Maybe Goal)
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol FilePath
"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 FilePath
"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 (m :: * -> *) a. Monad m => a -> m a
return Maybe Goal
forall a. Maybe a
Nothing
       Result
_         -> 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)


-- | 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 -> FilePath -> IO Bool -> IO Bool
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol FilePath
"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 (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       Result
_         -> Bool -> IO Bool
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 :: Type
goal = Type
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 ]
  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 (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 FilePath
"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 (FilePath -> [FilePath] -> SExpr
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic FilePath
"toSMT" [ FilePath
"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 (\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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"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
~> FilePath
"cryLenFromThenTo"

  , Kind -> Pat Type ()
anError Kind
KNum    Pat Type () -> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> FilePath
"cryErr"
  , Kind -> Pat Type ()
anError Kind
KProp   Pat Type () -> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> FilePath
"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
~> FilePath
"(unused)"
  ]

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

(~>) :: Mk a => (Type -> Match a) -> String -> TVars -> Type -> Match SExpr
(Type -> Match a
m ~> :: (Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> FilePath
f) Map TVar SExpr
tvs 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 -> 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 Map TVar SExpr
_ FilePath
f ()
_ = FilePath -> SExpr
SMT.const FilePath
f

instance Mk Integer where
  mk :: Map TVar SExpr -> FilePath -> Integer -> SExpr
mk Map TVar SExpr
_ FilePath
f 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 Map TVar SExpr
tvs FilePath
_ 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 Map TVar SExpr
tvs FilePath
f Type
x = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x]

instance Mk (Type,Type) where
  mk :: Map TVar SExpr -> FilePath -> (Type, Type) -> SExpr
mk Map TVar SExpr
tvs FilePath
f (Type
x,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 Map TVar SExpr
tvs FilePath
f (Type
x,Type
y,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 ]

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