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

    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
      ) where

    import           SimpleSMT (SExpr)
    import qualified SimpleSMT as SMT
    import           Data.Map ( Map )
    import qualified Data.Map as Map
    import qualified Data.Set as Set
    import           Data.Maybe(catMaybes)
    import           Data.List(partition)
    import           Control.Exception
    import           Control.Monad(msum,zipWithM,void)
    import           Data.Char(isSpace)
    import           Text.Read(readMaybe)
    import qualified System.IO.Strict as StrictIO
    import           System.FilePath((</>))
    import           System.Directory(doesFileExist)

    import Cryptol.Prelude(cryptolTcContents)
    import Cryptol.TypeCheck.Type
    import Cryptol.TypeCheck.InferTypes
    import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
    import Cryptol.TypeCheck.TypePat hiding ((~>),(~~>))
    import Cryptol.TypeCheck.Subst(Subst)
    import Cryptol.Utils.Panic
    import Cryptol.Utils.PP ( Doc, pp )

    -- | 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 Logger
    logger <- if (SolverConfig -> Int
    solverVerbose SolverConfig
    sCfg) 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 a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Logger
    quietLogger
          let smtDbg :: Maybe Logger
    smtDbg = if (SolverConfig -> Int
    solverVerbose SolverConfig
    sCfg) 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 <- String
    -> [String]
    -> Maybe Logger
    -> Maybe (ExitCode -> IO ())
    -> IO Solver
    SMT.newSolverNotify
                        (SolverConfig -> String
    solverPath SolverConfig
    sCfg) (SolverConfig -> [String]
    solverArgs SolverConfig
    sCfg) Maybe Logger
    smtDbg ((ExitCode -> IO ()) -> Maybe (ExitCode -> IO ())
    forall a. a -> Maybe a
    Just (IO () -> ExitCode -> IO ()
    forall a b. a -> b -> a
    const IO ()
    onExit))
          let sol :: Solver
    sol = Solver -> Logger -> Solver
    Solver Solver
    solver Logger
    logger
          Solver -> SolverConfig -> IO ()
    setupSolver Solver
    sol SolverConfig
    sCfg
          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
    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 :: 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 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, 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 ]

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