-- |
-- 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{ .. } =
     IO Solver -> (Solver -> IO ()) -> (Solver -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket
       (do Logger
logger <- if Int
solverVerbose Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 then Int -> IO Logger
SMT.newLogger 0
                                          else Logger -> IO Logger
forall (m :: * -> *) a. Monad m => a -> m a
return Logger
quietLogger
           let smtDbg :: Maybe Logger
smtDbg = if Int
solverVerbose Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then Logger -> Maybe Logger
forall a. a -> Maybe a
Just Logger
logger else Maybe Logger
forall a. Maybe a
Nothing
           Solver
solver <- FilePath -> [FilePath] -> Maybe Logger -> IO Solver
SMT.newSolver FilePath
solverPath [FilePath]
solverArgs Maybe Logger
smtDbg
           Bool
_ <- Solver -> FilePath -> FilePath -> IO Bool
SMT.setOptionMaybe Solver
solver ":global-decls" "false"
           -- SMT.setLogic solver "QF_LIA"
           let sol :: Solver
sol = Solver :: Solver -> Logger -> Solver
Solver { .. }
           Solver -> [FilePath] -> IO ()
loadTcPrelude Solver
sol [FilePath]
solverPreludePath
           Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return Solver
sol)
       (\s :: Solver
s -> IO ExitCode -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO ExitCode -> IO ()) -> IO ExitCode -> IO ()
forall a b. (a -> b) -> a -> b
$ Solver -> IO ExitCode
SMT.stop (Solver -> Solver
solver Solver
s))

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


-- | Load the definitions used for type checking.
loadTcPrelude :: Solver -> [FilePath] {- ^ Search in this paths -} -> IO ()
loadTcPrelude :: Solver -> [FilePath] -> IO ()
loadTcPrelude s :: Solver
s [] = Solver -> FilePath -> IO ()
loadString Solver
s FilePath
cryptolTcContents
loadTcPrelude s :: Solver
s (p :: FilePath
p : ps :: [FilePath]
ps) =
  do let file :: FilePath
file = FilePath
p FilePath -> FilePath -> FilePath
</> "CryptolTC.z3"
     Bool
yes <- FilePath -> IO Bool
doesFileExist FilePath
file
     if Bool
yes then Solver -> FilePath -> IO ()
loadFile Solver
s FilePath
file
            else Solver -> [FilePath] -> IO ()
loadTcPrelude Solver
s [FilePath]
ps


loadFile :: Solver -> FilePath -> IO ()
loadFile :: Solver -> FilePath -> IO ()
loadFile s :: Solver
s file :: FilePath
file = Solver -> FilePath -> IO ()
loadString Solver
s (FilePath -> IO ()) -> IO FilePath -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO FilePath
StrictIO.readFile FilePath
file

loadString :: Solver -> String -> IO ()
loadString :: Solver -> FilePath -> IO ()
loadString s :: Solver
s str :: FilePath
str = FilePath -> IO ()
go (FilePath -> FilePath
dropComments FilePath
str)
  where
  go :: FilePath -> IO ()
go txt :: FilePath
txt
    | (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace FilePath
txt = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    | Bool
otherwise =
      case FilePath -> Maybe (SExpr, FilePath)
SMT.readSExpr FilePath
txt of
        Just (e :: SExpr
e,rest :: FilePath
rest) -> Solver -> SExpr -> IO SExpr
SMT.command (Solver -> Solver
solver Solver
s) SExpr
e IO SExpr -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FilePath -> IO ()
go FilePath
rest
        Nothing       -> FilePath -> [FilePath] -> IO ()
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "loadFile" [ "Failed to parse SMT file."
                                          , FilePath
txt
                                          ]

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




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


debugBlock :: Solver -> String -> IO a -> IO a
debugBlock :: Solver -> FilePath -> IO a -> IO a
debugBlock s :: Solver
s@Solver { .. } name :: FilePath
name m :: IO a
m =
  do Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s FilePath
name
     Logger -> IO ()
SMT.logTab Logger
logger
     a
a <- IO a
m
     Logger -> IO ()
SMT.logUntab Logger
logger
     a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

class DebugLog t where
  debugLog :: Solver -> t -> IO ()

  debugLogList :: Solver -> [t] -> IO ()
  debugLogList s :: Solver
s ts :: [t]
ts = case [t]
ts of
                        [] -> Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s "(none)"
                        _  -> (t -> IO ()) -> [t] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> t -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s) [t]
ts

instance DebugLog Char where
  debugLog :: Solver -> Char -> IO ()
debugLog s :: Solver
s x :: Char
x     = Logger -> FilePath -> IO ()
SMT.logMessage (Solver -> Logger
logger Solver
s) (Char -> FilePath
forall a. Show a => a -> FilePath
show Char
x)
  debugLogList :: Solver -> FilePath -> IO ()
debugLogList s :: Solver
s x :: FilePath
x = Logger -> FilePath -> IO ()
SMT.logMessage (Solver -> Logger
logger Solver
s) FilePath
x

instance DebugLog a => DebugLog [a] where
  debugLog :: Solver -> [a] -> IO ()
debugLog = Solver -> [a] -> IO ()
forall a. DebugLog a => Solver -> [a] -> IO ()
debugLogList

instance DebugLog a => DebugLog (Maybe a) where
  debugLog :: Solver -> Maybe a -> IO ()
debugLog s :: Solver
s x :: Maybe a
x = case Maybe a
x of
                   Nothing -> Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s "(nothing)"
                   Just a :: a
a  -> Solver -> a -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s a
a

instance DebugLog Doc where
  debugLog :: Solver -> Doc -> IO ()
debugLog s :: Solver
s x :: Doc
x = Solver -> FilePath -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Doc -> FilePath
forall a. Show a => a -> FilePath
show Doc
x)

instance DebugLog Type where
  debugLog :: Solver -> Type -> IO ()
debugLog s :: Solver
s x :: Type
x = Solver -> Doc -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Type -> Doc
forall a. PP a => a -> Doc
pp Type
x)

instance DebugLog Goal where
  debugLog :: Solver -> Goal -> IO ()
debugLog s :: Solver
s x :: Goal
x = Solver -> Type -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Goal -> Type
goal Goal
x)

instance DebugLog Subst where
  debugLog :: Solver -> Subst -> IO ()
debugLog s :: Solver
s x :: Subst
x = Solver -> Doc -> IO ()
forall t. DebugLog t => Solver -> t -> IO ()
debugLog Solver
s (Subst -> Doc
forall a. PP a => a -> Doc
pp Subst
x)
--------------------------------------------------------------------------------





-- | Returns goals that were not proved
proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
proveImp :: Solver -> [Type] -> [Goal] -> IO [Goal]
proveImp sol :: Solver
sol ps :: [Type]
ps gs0 :: [Goal]
gs0 =
  Solver -> FilePath -> IO [Goal] -> IO [Goal]
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "PROVE IMP" (IO [Goal] -> IO [Goal]) -> IO [Goal] -> IO [Goal]
forall a b. (a -> b) -> a -> b
$
  do let gs1 :: [Goal]
gs1       = (Goal -> [Goal]) -> [Goal] -> [Goal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Goal -> [Goal]
flatGoal [Goal]
gs0
         (gs :: [Goal]
gs,rest :: [Goal]
rest) = (Goal -> Bool) -> [Goal] -> ([Goal], [Goal])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Type -> Bool
isNumeric (Type -> Bool) -> (Goal -> Type) -> Goal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Goal -> Type
goal) [Goal]
gs1
         numAsmp :: [Type]
numAsmp   = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
isNumeric ((Type -> [Type]) -> [Type] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd [Type]
ps)
         vs :: [TVar]
vs        = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList (([Type], [Type]) -> Set TVar
forall t. FVS t => t -> Set TVar
fvs ([Type]
numAsmp, (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal [Goal]
gs))
     Map TVar SExpr
tvs <- Solver -> FilePath -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "VARIABLES" (IO (Map TVar SExpr) -> IO (Map TVar SExpr))
-> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a b. (a -> b) -> a -> b
$
       do Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)
          [(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ 0 .. ] [TVar]
vs
     Solver -> FilePath -> IO () -> IO ()
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "ASSUMPTIONS" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
       (Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
numAsmp
     [Maybe Goal]
gs' <- (Goal -> IO (Maybe Goal)) -> [Goal] -> IO [Maybe Goal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Map TVar SExpr -> Goal -> IO (Maybe Goal)
prove Solver
sol Map TVar SExpr
tvs) [Goal]
gs
     Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)
     [Goal] -> IO [Goal]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Maybe Goal] -> [Goal]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Goal]
gs' [Goal] -> [Goal] -> [Goal]
forall a. [a] -> [a] -> [a]
++ [Goal]
rest)

-- | Check if the given goals are known to be unsolvable.
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable :: Solver -> [Goal] -> IO Bool
checkUnsolvable sol :: Solver
sol gs0 :: [Goal]
gs0 =
  Solver -> FilePath -> IO Bool -> IO Bool
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "CHECK UNSOLVABLE" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
  do let ps :: [Type]
ps = (Type -> Bool) -> [Type] -> [Type]
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
isNumeric
            ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Goal -> Type) -> [Goal] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Goal -> Type
goal
            ([Goal] -> [Type]) -> [Goal] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Goal -> [Goal]) -> [Goal] -> [Goal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Goal -> [Goal]
flatGoal [Goal]
gs0
         vs :: [TVar]
vs = Set TVar -> [TVar]
forall a. Set a -> [a]
Set.toList ([Type] -> Set TVar
forall t. FVS t => t -> Set TVar
fvs [Type]
ps)
     Map TVar SExpr
tvs <- Solver -> FilePath -> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "VARIABLES" (IO (Map TVar SExpr) -> IO (Map TVar SExpr))
-> IO (Map TVar SExpr) -> IO (Map TVar SExpr)
forall a b. (a -> b) -> a -> b
$
       do Solver -> IO ()
push Solver
sol
          [(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ 0 .. ] [TVar]
vs
     Bool
ans <- Solver -> Map TVar SExpr -> [Type] -> IO Bool
unsolvable Solver
sol Map TVar SExpr
tvs [Type]
ps
     Solver -> IO ()
pop Solver
sol
     Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ans

tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar,Nat')])
tryGetModel :: Solver -> [TVar] -> [Type] -> IO (Maybe [(TVar, Nat')])
tryGetModel sol :: Solver
sol as :: [TVar]
as ps :: [Type]
ps =
  Solver
-> FilePath
-> IO (Maybe [(TVar, Nat')])
-> IO (Maybe [(TVar, Nat')])
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "TRY GET MODEL" (IO (Maybe [(TVar, Nat')]) -> IO (Maybe [(TVar, Nat')]))
-> IO (Maybe [(TVar, Nat')]) -> IO (Maybe [(TVar, Nat')])
forall a b. (a -> b) -> a -> b
$
  do Solver -> IO ()
push Solver
sol
     Map TVar SExpr
tvs <- [(TVar, SExpr)] -> Map TVar SExpr
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(TVar, SExpr)] -> Map TVar SExpr)
-> IO [(TVar, SExpr)] -> IO (Map TVar SExpr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> TVar -> IO (TVar, SExpr))
-> [Int] -> [TVar] -> IO [(TVar, SExpr)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar Solver
sol) [ 0 .. ] [TVar]
as
     (Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
ps
     Result
sat <- Solver -> IO Result
SMT.check (Solver -> Solver
solver Solver
sol)
     Maybe [(TVar, Nat')]
su <- case Result
sat of
             SMT.Sat ->
               case [TVar]
as of
                 [] -> Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TVar, Nat')] -> Maybe [(TVar, Nat')]
forall a. a -> Maybe a
Just [])
                 _ -> do [(SExpr, Value)]
res <- Solver -> [SExpr] -> IO [(SExpr, Value)]
SMT.getExprs (Solver -> Solver
solver Solver
sol) (Map TVar SExpr -> [SExpr]
forall k a. Map k a -> [a]
Map.elems Map TVar SExpr
tvs)
                         let parse :: TVar -> Maybe (TVar, Nat')
parse x :: TVar
x = do SExpr
e <- TVar -> Map TVar SExpr -> Maybe SExpr
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TVar
x Map TVar SExpr
tvs
                                          Nat'
t <- Value -> Maybe Nat'
parseNum (Value -> Maybe Nat') -> Maybe Value -> Maybe Nat'
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SExpr -> [(SExpr, Value)] -> Maybe Value
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup SExpr
e [(SExpr, Value)]
res
                                          (TVar, Nat') -> Maybe (TVar, Nat')
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
x, Nat'
t)
                         Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return ((TVar -> Maybe (TVar, Nat')) -> [TVar] -> Maybe [(TVar, Nat')]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TVar -> Maybe (TVar, Nat')
parse [TVar]
as)
             _ -> Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TVar, Nat')]
forall a. Maybe a
Nothing
     Solver -> IO ()
pop Solver
sol
     Maybe [(TVar, Nat')] -> IO (Maybe [(TVar, Nat')])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [(TVar, Nat')]
su

  where
  parseNum :: Value -> Maybe Nat'
parseNum a :: Value
a
    | SMT.Other s :: SExpr
s <- Value
a
    , SMT.List [con :: SExpr
con,val :: SExpr
val,isFin :: SExpr
isFin,isErr :: SExpr
isErr] <- SExpr
s
    , SMT.Atom "mk-infnat" <- SExpr
con
    , SMT.Atom "false"     <- SExpr
isErr
    , SMT.Atom fin :: FilePath
fin         <- SExpr
isFin
    , SMT.Atom v :: FilePath
v           <- SExpr
val
    , Just n :: Integer
n               <- FilePath -> Maybe Integer
forall a. Read a => FilePath -> Maybe a
readMaybe FilePath
v
    = Nat' -> Maybe Nat'
forall a. a -> Maybe a
Just (if FilePath
fin FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== "false" then Nat'
Inf else Integer -> Nat'
Nat Integer
n)

  parseNum _ = Maybe Nat'
forall a. Maybe a
Nothing

shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar,Nat')] -> IO [(TVar,Nat')]
shrinkModel :: Solver -> [TVar] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
shrinkModel sol :: Solver
sol as :: [TVar]
as ps0 :: [Type]
ps0 mdl :: [(TVar, Nat')]
mdl = [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go [] [Type]
ps0 [(TVar, Nat')]
mdl
  where
  go :: [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go done :: [(TVar, Nat')]
done ps :: [Type]
ps ((x :: TVar
x,Nat k :: Integer
k) : more :: [(TVar, Nat')]
more) =
    do Integer
k1 <- [Type] -> TVar -> Integer -> IO Integer
shrink1 [Type]
ps TVar
x Integer
k
       [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go ((TVar
x,Integer -> Nat'
Nat Integer
k1) (TVar, Nat') -> [(TVar, Nat')] -> [(TVar, Nat')]
forall a. a -> [a] -> [a]
: [(TVar, Nat')]
done) ((Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k1 Type -> Type -> Type
>== TVar -> Type
TVar TVar
x) Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps) [(TVar, Nat')]
more

  go done :: [(TVar, Nat')]
done ps :: [Type]
ps ((x :: TVar
x,i :: Nat'
i) : more :: [(TVar, Nat')]
more) = [(TVar, Nat')] -> [Type] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
go ((TVar
x,Nat'
i) (TVar, Nat') -> [(TVar, Nat')] -> [(TVar, Nat')]
forall a. a -> [a] -> [a]
: [(TVar, Nat')]
done) [Type]
ps [(TVar, Nat')]
more
  go done :: [(TVar, Nat')]
done _ [] = [(TVar, Nat')] -> IO [(TVar, Nat')]
forall (m :: * -> *) a. Monad m => a -> m a
return [(TVar, Nat')]
done

  shrink1 :: [Type] -> TVar -> Integer -> IO Integer
shrink1 ps :: [Type]
ps x :: TVar
x k :: Integer
k
    | Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return 0
    | Bool
otherwise =
      do let k1 :: Integer
k1 = Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
k 2
             p1 :: Type
p1 = Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
k1 Type -> Type -> Type
>== TVar -> Type
TVar TVar
x
         Maybe [(TVar, Nat')]
mb <- Solver -> [TVar] -> [Type] -> IO (Maybe [(TVar, Nat')])
tryGetModel Solver
sol [TVar]
as (Type
p1 Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ps)
         case Maybe [(TVar, Nat')]
mb of
           Nothing     -> Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
k
           Just newMdl :: [(TVar, Nat')]
newMdl ->
             case TVar -> [(TVar, Nat')] -> Maybe Nat'
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TVar
x [(TVar, Nat')]
newMdl of
               Just (Nat k2 :: Integer
k2) -> [Type] -> TVar -> Integer -> IO Integer
shrink1 [Type]
ps TVar
x Integer
k2
               _ -> FilePath -> [FilePath] -> IO Integer
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "shrink" ["model is missing variable", TVar -> FilePath
forall a. Show a => a -> FilePath
show TVar
x]



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

push :: Solver -> IO ()
push :: Solver -> IO ()
push sol :: Solver
sol = Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)

pop :: Solver -> IO ()
pop :: Solver -> IO ()
pop sol :: Solver
sol = Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)


declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar :: Solver -> Int -> TVar -> IO (TVar, SExpr)
declareVar s :: Solver
s x :: Int
x v :: TVar
v =
  do let name :: FilePath
name = (if TVar -> Bool
isFreeTV TVar
v then "fv" else "kv") FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
x
     SExpr
e <- Solver -> FilePath -> SExpr -> IO SExpr
SMT.declare (Solver -> Solver
solver Solver
s) FilePath
name SExpr
cryInfNat
     Solver -> SExpr -> IO ()
SMT.assert (Solver -> Solver
solver Solver
s) (FilePath -> [SExpr] -> SExpr
SMT.fun "cryVar" [ SExpr
e ])
     (TVar, SExpr) -> IO (TVar, SExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return (TVar
v,SExpr
e)

assume :: Solver -> TVars -> Prop -> IO ()
assume :: Solver -> Map TVar SExpr -> Type -> IO ()
assume s :: Solver
s tvs :: Map TVar SExpr
tvs p :: Type
p = Solver -> SExpr -> IO ()
SMT.assert (Solver -> Solver
solver Solver
s) (FilePath -> [SExpr] -> SExpr
SMT.fun "cryAssume" [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
p ])

prove :: Solver -> TVars -> Goal -> IO (Maybe Goal)
prove :: Solver -> Map TVar SExpr -> Goal -> IO (Maybe Goal)
prove sol :: Solver
sol tvs :: Map TVar SExpr
tvs g :: Goal
g =
  Solver -> FilePath -> IO (Maybe Goal) -> IO (Maybe Goal)
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "PROVE" (IO (Maybe Goal) -> IO (Maybe Goal))
-> IO (Maybe Goal) -> IO (Maybe Goal)
forall a b. (a -> b) -> a -> b
$
  do let s :: Solver
s = Solver -> Solver
solver Solver
sol
     Solver -> IO ()
push Solver
sol
     Solver -> SExpr -> IO ()
SMT.assert Solver
s (FilePath -> [SExpr] -> SExpr
SMT.fun "cryProve" [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs (Goal -> Type
goal Goal
g) ])
     Result
res <- Solver -> IO Result
SMT.check Solver
s
     Solver -> IO ()
pop Solver
sol
     case Result
res of
       SMT.Unsat -> Maybe Goal -> IO (Maybe Goal)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Goal
forall a. Maybe a
Nothing
       _         -> Maybe Goal -> IO (Maybe Goal)
forall (m :: * -> *) a. Monad m => a -> m a
return (Goal -> Maybe Goal
forall a. a -> Maybe a
Just Goal
g)


-- | 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 sol :: Solver
sol tvs :: Map TVar SExpr
tvs ps :: [Type]
ps =
  Solver -> FilePath -> IO Bool -> IO Bool
forall a. Solver -> FilePath -> IO a -> IO a
debugBlock Solver
sol "UNSOLVABLE" (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$
  do Solver -> IO ()
SMT.push (Solver -> Solver
solver Solver
sol)
     (Type -> IO ()) -> [Type] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Solver -> Map TVar SExpr -> Type -> IO ()
assume Solver
sol Map TVar SExpr
tvs) [Type]
ps
     Result
res <- Solver -> IO Result
SMT.check (Solver -> Solver
solver Solver
sol)
     Solver -> IO ()
SMT.pop (Solver -> Solver
solver Solver
sol)
     case Result
res of
       SMT.Unsat -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
       _         -> Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False



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

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


-- | Assumes no 'And'
isNumeric :: Prop -> Bool
isNumeric :: Type -> Bool
isNumeric ty :: Type
ty = Bool -> Match Bool -> Bool
forall a. a -> Match a -> a
matchDefault Bool
False (Match Bool -> Bool) -> Match Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Match Bool] -> Match Bool
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|=|), (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|/=|), (Type -> Match (Type, Type)) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match (Type, Type)
(|>=|), (Type -> Match Type) -> Match Bool
forall (m :: * -> *) a. Monad m => (Type -> m a) -> m Bool
is Type -> Match Type
aFin ]
  where
  is :: (Type -> m a) -> m Bool
is f :: Type -> m a
f = Type -> m a
f Type
ty m a -> m Bool -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True


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

type TVars = Map TVar SExpr

cryInfNat :: SExpr
cryInfNat :: SExpr
cryInfNat = FilePath -> SExpr
SMT.const "InfNat"


toSMT :: TVars -> Type -> SExpr
toSMT :: Map TVar SExpr -> Type -> SExpr
toSMT tvs :: Map TVar SExpr
tvs ty :: Type
ty = SExpr -> Match SExpr -> SExpr
forall a. a -> Match a -> a
matchDefault (FilePath -> [FilePath] -> SExpr
forall a. HasCallStack => FilePath -> [FilePath] -> a
panic "toSMT" [ "Unexpected type", Type -> FilePath
forall a. Show a => a -> FilePath
show Type
ty ])
  (Match SExpr -> SExpr) -> Match SExpr -> SExpr
forall a b. (a -> b) -> a -> b
$ [Match SExpr] -> Match SExpr
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Match SExpr] -> Match SExpr) -> [Match SExpr] -> Match SExpr
forall a b. (a -> b) -> a -> b
$ ((Map TVar SExpr -> Type -> Match SExpr) -> Match SExpr)
-> [Map TVar SExpr -> Type -> Match SExpr] -> [Match SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (\f :: Map TVar SExpr -> Type -> Match SExpr
f -> Map TVar SExpr -> Type -> Match SExpr
f Map TVar SExpr
tvs Type
ty)
  [ Pat Type ()
aInf            Pat Type () -> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryInf"
  , Pat Type Integer
aNat            Pat Type Integer
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "cryNat"

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

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

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

  , Pat Type TVar
aTVar           Pat Type TVar -> FilePath -> Map TVar SExpr -> Type -> Match SExpr
forall a.
Mk a =>
(Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> "(unused)"
  ]

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

(~>) :: Mk a => (Type -> Match a) -> String -> TVars -> Type -> Match SExpr
(m :: Type -> Match a
m ~> :: (Type -> Match a)
-> FilePath -> Map TVar SExpr -> Type -> Match SExpr
~> f :: FilePath
f) tvs :: Map TVar SExpr
tvs t :: Type
t = Type -> Match a
m Type
t Match a -> (a -> Match SExpr) -> Match SExpr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: a
a -> SExpr -> Match SExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (Map TVar SExpr -> FilePath -> a -> SExpr
forall t. Mk t => Map TVar SExpr -> FilePath -> t -> SExpr
mk Map TVar SExpr
tvs FilePath
f a
a)

class Mk t where
  mk :: TVars -> String -> t -> SExpr

instance Mk () where
  mk :: Map TVar SExpr -> FilePath -> () -> SExpr
mk _ f :: FilePath
f _ = FilePath -> SExpr
SMT.const FilePath
f

instance Mk Integer where
  mk :: Map TVar SExpr -> FilePath -> Integer -> SExpr
mk _ f :: FilePath
f x :: Integer
x = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [ Integer -> SExpr
SMT.int Integer
x ]

instance Mk TVar where
  mk :: Map TVar SExpr -> FilePath -> TVar -> SExpr
mk tvs :: Map TVar SExpr
tvs _ x :: TVar
x = Map TVar SExpr
tvs Map TVar SExpr -> TVar -> SExpr
forall k a. Ord k => Map k a -> k -> a
Map.! TVar
x

instance Mk Type where
  mk :: Map TVar SExpr -> FilePath -> Type -> SExpr
mk tvs :: Map TVar SExpr
tvs f :: FilePath
f x :: Type
x = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x]

instance Mk TCErrorMessage where
  mk :: Map TVar SExpr -> FilePath -> TCErrorMessage -> SExpr
mk _ f :: FilePath
f _ = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f []

instance Mk (Type,Type) where
  mk :: Map TVar SExpr -> FilePath -> (Type, Type) -> SExpr
mk tvs :: Map TVar SExpr
tvs f :: FilePath
f (x :: Type
x,y :: Type
y) = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
y]

instance Mk (Type,Type,Type) where
  mk :: Map TVar SExpr -> FilePath -> (Type, Type, Type) -> SExpr
mk tvs :: Map TVar SExpr
tvs f :: FilePath
f (x :: Type
x,y :: Type
y,z :: Type
z) = FilePath -> [SExpr] -> SExpr
SMT.fun FilePath
f [ Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
x, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
y, Map TVar SExpr -> Type -> SExpr
toSMT Map TVar SExpr
tvs Type
z ]

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