-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Client
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Cross-cutting toplevel client functions
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                 #-}
{-# LANGUAGE DeriveLift          #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE PackageImports      #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TemplateHaskell     #-}
{-# LANGUAGE TupleSections       #-}

#if MIN_VERSION_template_haskell(2,22,1)
-- No need for newer versions of TH
#else
{-# LANGUAGE FlexibleInstances   #-}
#endif

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Client
  ( sbvCheckSolverInstallation
  , defaultSolverConfig
  , getAvailableSolvers
  , mkSymbolic
  , getConstructors
  ) where

import Data.Generics

import Control.Monad (filterM, mapAndUnzipM, zipWithM)
import Test.QuickCheck (Arbitrary(..), elements)

import qualified Control.Exception as C

import Data.Maybe (fromMaybe)

import Data.Char
import Data.Word
import Data.Int
import Data.Ratio

import qualified "template-haskell" Language.Haskell.TH        as TH
#if MIN_VERSION_template_haskell(2,18,0)
import qualified "template-haskell" Language.Haskell.TH.Syntax as TH
#endif

import Language.Haskell.TH.ExpandSyns as TH

import Data.SBV.Core.Concrete (cvRank)
import Data.SBV.Core.Data
import Data.SBV.Core.Model
import Data.SBV.Core.SizedFloats
import Data.SBV.Core.Symbolic (registerKind)

import Data.SBV.Provers.Prover
import qualified Data.SBV.List as SL

import Data.List (genericLength)

import Data.SBV.TP.Kernel

-- | Check whether the given solver is installed and is ready to go. This call does a
-- simple call to the solver to ensure all is well.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
sbvCheckSolverInstallation SMTConfig
cfg = IO Bool
check IO Bool -> (SomeException -> IO Bool) -> IO Bool
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
_ :: C.SomeException) -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
  where check :: IO Bool
check = do ThmResult SMTResult
r <- SMTConfig -> (SBool -> SBool) -> IO ThmResult
forall (m :: * -> *) a.
ProvableM m a =>
SMTConfig -> a -> m ThmResult
proveWith SMTConfig
cfg ((SBool -> SBool) -> IO ThmResult)
-> (SBool -> SBool) -> IO ThmResult
forall a b. (a -> b) -> a -> b
$ \SBool
x -> SBool -> SBool
sNot (SBool -> SBool
sNot SBool
x) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBool
x :: SBool)
                   case SMTResult
r of
                     Unsatisfiable{} -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                     SMTResult
_               -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | The default configs corresponding to supported SMT solvers
defaultSolverConfig :: Solver -> SMTConfig
defaultSolverConfig :: Solver -> SMTConfig
defaultSolverConfig Solver
ABC       = SMTConfig
abc
defaultSolverConfig Solver
Boolector = SMTConfig
boolector
defaultSolverConfig Solver
Bitwuzla  = SMTConfig
bitwuzla
defaultSolverConfig Solver
CVC4      = SMTConfig
cvc4
defaultSolverConfig Solver
CVC5      = SMTConfig
cvc5
defaultSolverConfig Solver
DReal     = SMTConfig
dReal
defaultSolverConfig Solver
MathSAT   = SMTConfig
mathSAT
defaultSolverConfig Solver
OpenSMT   = SMTConfig
openSMT
defaultSolverConfig Solver
Yices     = SMTConfig
yices
defaultSolverConfig Solver
Z3        = SMTConfig
z3

-- | Return the known available solver configs, installed on your machine.
getAvailableSolvers :: IO [SMTConfig]
getAvailableSolvers :: IO [SMTConfig]
getAvailableSolvers = (SMTConfig -> IO Bool) -> [SMTConfig] -> IO [SMTConfig]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM SMTConfig -> IO Bool
sbvCheckSolverInstallation ((Solver -> SMTConfig) -> [Solver] -> [SMTConfig]
forall a b. (a -> b) -> [a] -> [b]
map Solver -> SMTConfig
defaultSolverConfig [Solver
forall a. Bounded a => a
minBound .. Solver
forall a. Bounded a => a
maxBound])

#if MIN_VERSION_template_haskell(2,22,1)
-- Starting template haskell 2.22.1 the following instances are automatically provided
#else
deriving instance TH.Lift TH.OccName
deriving instance TH.Lift TH.NameSpace
deriving instance TH.Lift TH.PkgName
deriving instance TH.Lift TH.ModName
deriving instance TH.Lift TH.NameFlavour
deriving instance TH.Lift TH.Name
deriving instance TH.Lift TH.Type
deriving instance TH.Lift TH.Specificity
deriving instance TH.Lift (TH.TyVarBndr TH.Specificity)
deriving instance TH.Lift (TH.TyVarBndr ())
deriving instance TH.Lift TH.TyLit
#endif

-- A few other things we need to TH lift
deriving instance TH.Lift Kind

data ADTKind = ADTUninterpreted -- Completely uninterpreted
             | ADTEnum          -- Enumeration
             | ADTFull          -- A full datatype

-- | Create a mutually recursive group of ADTs.
mkSymbolic :: [TH.Name] -> TH.Q [TH.Dec]
mkSymbolic :: [Name] -> Q [Dec]
mkSymbolic [Name]
ts = [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> Q [Dec]) -> [Name] -> Q [[Dec]]
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 Name -> Q [Dec]
mkSymbolicADT [Name]
ts

-- | Create a symbolic ADT.
mkSymbolicADT :: TH.Name -> TH.Q [TH.Dec]
mkSymbolicADT :: Name -> Q [Dec]
mkSymbolicADT Name
typeName = do

     (ADTKind
tKind, [Name]
params, [(Name, [(Maybe Name, Type, Kind)])]
cstrs) <- Name -> Q (ADTKind, [Name], [(Name, [(Maybe Name, Type, Kind)])])
dissect Name
typeName
     [Dec]
ds <- ADTKind
-> Name
-> [Name]
-> [(Name, [(Maybe Name, Type, Kind)])]
-> Q [Dec]
mkADT ADTKind
tKind Name
typeName [Name]
params [(Name, [(Maybe Name, Type, Kind)])]
cstrs

     -- declare an "undefiner" so we don't have stray names
     Name
nm <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ String
"_undefiner_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
typeName
     String -> Name -> Q ()
addDoc String
"Autogenerated definition to avoid unused-variable warnings from GHC." Name
nm

     -- undefiner must be careful in putting ascriptions
     Name
aVar <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"a"
     let undefine :: Name -> Exp
undefine Name
n
           | String
base String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"sCase" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tbase = Int -> Exp
wrap Int
1   -- Needs an extra param
           | Bool
True                     = Int -> Exp
wrap Int
0
           where tbase :: String
tbase  = Name -> String
TH.nameBase Name
typeName
                 base :: String
base   = Name -> String
TH.nameBase Name
n
                 wrap :: Int -> Exp
wrap Int
c = (Exp -> Type -> Exp) -> Exp -> Cxt -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Type -> Exp
TH.AppTypeE (Name -> Exp
TH.VarE Name
n) (Int -> Type -> Cxt
forall a. Int -> a -> [a]
replicate (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
params) (Name -> Type
TH.ConT ''Integer))

         names :: [Exp]
names     = [Name -> Exp
undefine Name
n | TH.FunD Name
n [Clause]
_ <- [Dec]
ds]
         body :: Exp
body      = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'undefined)
                                   ([Exp]
names [Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
++ [Exp -> Type -> Exp
TH.SigE (Name -> Exp
TH.VarE 'undefined)
                                                      ((Type -> Type -> Type) -> Type -> Cxt -> Type
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
TH.AppT (Name -> Type
TH.ConT (String -> Name
TH.mkName (Char
'S' Char -> String -> String
forall a. a -> [a] -> [a]
: Name -> String
TH.nameBase Name
typeName)))
                                                                     ((Name -> Type) -> [Name] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Name -> Type
forall a b. a -> b -> a
const (Name -> Type
TH.ConT ''Integer)) [Name]
params))])

         undefSig :: Dec
undefSig  = Name -> Type -> Dec
TH.SigD Name
nm ([TyVarBndr Specificity] -> Cxt -> Type -> Type
TH.ForallT [] [] (Name -> Type
TH.VarT Name
aVar))
         undefBody :: Dec
undefBody = Name -> [Clause] -> Dec
TH.FunD Name
nm [[Pat] -> Body -> [Dec] -> Clause
TH.Clause [] (Exp -> Body
TH.NormalB Exp
body) []]

     [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [Dec]
ds [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec
undefSig, Dec
undefBody]

-- | Add document to a generated declaration for the declaration
addDeclDocs :: (TH.Name, String) -> [(TH.Name, String)] -> TH.Q ()
#if MIN_VERSION_template_haskell(2,18,0)
addDeclDocs :: (Name, String) -> [(Name, String)] -> Q ()
addDeclDocs (Name
tnm, String
ts) [(Name, String)]
cnms = do Bool -> (Name, String) -> Q ()
add Bool
True (Name
tnm, String
ts)
                                ((Name, String) -> Q ()) -> [(Name, String)] -> Q ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_  (Bool -> (Name, String) -> Q ()
add Bool
False) [(Name, String)]
cnms
   where add :: Bool -> (Name, String) -> Q ()
add Bool
True  (Name
cnm, String
cs) = Q () -> Q ()
TH.addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
TH.putDoc (Name -> DocLoc
TH.DeclDoc Name
cnm) (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ String
"Symbolic version of the type '"        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'."
         add Bool
False (Name
cnm, String
cs) = Q () -> Q ()
TH.addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
TH.putDoc (Name -> DocLoc
TH.DeclDoc Name
cnm) (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ String
"Symbolic version of the constructor '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'."
#else
addDeclDocs _ _ = pure ()
#endif

-- | Add document to a generated function
addDoc :: String -> TH.Name -> TH.Q ()
#if MIN_VERSION_template_haskell(2,18,0)
addDoc :: String -> Name -> Q ()
addDoc String
what Name
tnm = Q () -> Q ()
TH.addModFinalizer (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ DocLoc -> String -> Q ()
TH.putDoc (Name -> DocLoc
TH.DeclDoc Name
tnm) String
what
#else
addDoc _ _ = pure ()
#endif

-- | Symbolic version of a type
mkSBV :: TH.Type -> TH.Type
mkSBV :: Type -> Type
mkSBV Type
a = Name -> Type
TH.ConT ''SBV Type -> Type -> Type
`TH.AppT` Type
a

-- | Saturate the type with its parameters
saturate :: TH.Type -> [TH.Name] -> TH.Type
saturate :: Type -> [Name] -> Type
saturate Type
t [Name]
ps = (Name -> Type -> Type) -> Type -> [Name] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Name
p Type
b -> Type -> Type -> Type
TH.AppT Type
b (Name -> Type
TH.VarT Name
p)) Type
t ([Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
ps)

-- | Create a symbolic ADT
mkADT ::  ADTKind                                       -- What kind of ADT are we generating?
       -> TH.Name                                       -- type name
       -> [TH.Name]                                     -- parameters
       -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -- constructors
       -> TH.Q [TH.Dec]                                 -- declarations
mkADT :: ADTKind
-> Name
-> [Name]
-> [(Name, [(Maybe Name, Type, Kind)])]
-> Q [Dec]
mkADT ADTKind
adtKind Name
typeName [Name]
params [(Name, [(Maybe Name, Type, Kind)])]
cstrs = do

    let typeCon :: Type
typeCon = Type -> [Name] -> Type
saturate (Name -> Type
TH.ConT Name
typeName) [Name]
params
        sType :: Type
sType   = Type -> Type
mkSBV Type
typeCon

        inSymValContext :: Type -> Type
inSymValContext = [TyVarBndr Specificity] -> Cxt -> Type -> Type
TH.ForallT [] [Type -> Type -> Type
TH.AppT (Name -> Type
TH.ConT ''SymVal) (Name -> Type
TH.VarT Name
n) | Name
n <- [Name]
params]

        isEnum :: Bool
isEnum = case ADTKind
adtKind of
                  ADTKind
ADTUninterpreted -> Bool
False
                  ADTKind
ADTEnum          -> Bool
True
                  ADTKind
ADTFull          -> Bool
False

        -- Given Cstr f1 f2 f3, generate the clause:
        --     inp@(Cstr [f1, f2, f3]) = case sequenceA [unlitCV (literal f1), unlitCV (literal f2), unlitCV (literal f3)] of
        --                                 Just c  -> let k = kindOf inp
        --                                            in SBV $ SVal k (Left (CV k (CADT (Cstr, c))))
        --                                 Nothing -> sCstr (literal f1)
        --
        mkLitClause :: (Name, [a]) -> m Clause
mkLitClause (Name
n, [a]
fs) = do
           [Name]
as  <- (a -> m Name) -> [a] -> m [Name]
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 (m Name -> a -> m Name
forall a b. a -> b -> a
const (String -> m Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"a")) [a]
fs
           Name
inp <- String -> m Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"inp"
           Name
c   <- String -> m Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"c"

           let app :: m Exp -> m Exp -> m Exp
app m Exp
a m Exp
b = [| $m Exp
a (literal $m Exp
b) |]

           [m Pat] -> m Body -> [m Dec] -> m Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
TH.clause [Name -> m Pat -> m Pat
forall (m :: * -> *). Quote m => Name -> m Pat -> m Pat
TH.asP Name
inp (Name -> [m Pat] -> m Pat
forall (m :: * -> *). Quote m => Name -> [m Pat] -> m Pat
TH.conP Name
n ((Name -> m Pat) -> [Name] -> [m Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Pat
forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP [Name]
as))]
                     (m Exp -> m Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB
                           (m Exp -> [m Match] -> m Exp
forall (m :: * -> *). Quote m => m Exp -> [m Match] -> m Exp
TH.caseE [| sequenceA $([m Exp] -> m Exp
forall (m :: * -> *). Quote m => [m Exp] -> m Exp
TH.listE [ [| unlitCV (literal $(Name -> m Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
a)) |] | Name
a <- [Name]
as ]) |]
                                     [ m Pat -> m Body -> [m Dec] -> m Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
TH.match [p|Just $(Name -> m Pat
forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP Name
c)|]
                                                (m Exp -> m Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB [| let k = kindOf $(Name -> m Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
inp)
                                                               in SBV $ SVal k (Left (CV k (CADT (TH.nameBase n, $(Name -> m Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
c)))))
                                                            |])
                                                []
                                     , m Pat -> m Body -> [m Dec] -> m Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
TH.match [p|Nothing|]
                                                (m Exp -> m Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB ((m Exp -> m Exp -> m Exp) -> m Exp -> [m Exp] -> m Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl m Exp -> m Exp -> m Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
app (Name -> m Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE (String -> Name
TH.mkName (Char
's' Char -> String -> String
forall a. a -> [a] -> [a]
: Name -> String
TH.nameBase Name
n))) ((Name -> m Exp) -> [Name] -> [m Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> m Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE [Name]
as)))
                                                []
                                     ]))
                     []

    Dec
litFun <- case ADTKind
adtKind of
                ADTKind
ADTUninterpreted -> do Exp
noLit <- [| error $ unlines [ "Data.SBV: unexpected call to derived literal implementation"
                                                                   , "***"
                                                                   , "*** Type: " ++ show typeName
                                                                   , ""
                                                                   , "***Please report this as a bug!"
                                                                   ]
                                                |]
                                       Dec -> Q Dec
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ Name -> [Clause] -> Dec
TH.FunD 'literal [[Pat] -> Body -> [Dec] -> Clause
TH.Clause [Pat
TH.WildP] (Exp -> Body
TH.NormalB Exp
noLit) []]

                ADTKind
ADTEnum          -> Name -> [Clause] -> Dec
TH.FunD 'literal ([Clause] -> Dec) -> Q [Clause] -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Name, [(Maybe Name, Type, Kind)]) -> Q Clause)
-> [(Name, [(Maybe Name, Type, Kind)])] -> Q [Clause]
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 (Name, [(Maybe Name, Type, Kind)]) -> Q Clause
forall {m :: * -> *} {a}. Quote m => (Name, [a]) -> m Clause
mkLitClause [(Name, [(Maybe Name, Type, Kind)])]
cstrs
                ADTKind
ADTFull          -> Name -> [Clause] -> Dec
TH.FunD 'literal ([Clause] -> Dec) -> Q [Clause] -> Q Dec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Name, [(Maybe Name, Type, Kind)]) -> Q Clause)
-> [(Name, [(Maybe Name, Type, Kind)])] -> Q [Clause]
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 (Name, [(Maybe Name, Type, Kind)]) -> Q Clause
forall {m :: * -> *} {a}. Quote m => (Name, [a]) -> m Clause
mkLitClause [(Name, [(Maybe Name, Type, Kind)])]
cstrs

    Name
fromCVFunName <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (String
"cv2" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
typeName)
    String -> Name -> Q ()
addDoc (String
"Conversion from SMT values to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
typeName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" values.") Name
fromCVFunName

    let fromCVSig :: Dec
fromCVSig = Name -> Type -> Dec
TH.SigD Name
fromCVFunName
                            (Type -> Type
inSymValContext ((Type -> Type -> Type) -> Type -> Cxt -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Type -> Type
TH.AppT (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Type
TH.AppT Type
TH.ArrowT) Type
typeCon
                                                    [Name -> Type
TH.ConT ''String, Type -> Type -> Type
TH.AppT Type
TH.ListT (Name -> Type
TH.ConT ''CV)]))

        fromCVCls :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q TH.Clause
        fromCVCls :: (Name, [(Maybe Name, Type, Kind)]) -> Q Clause
fromCVCls (Name
nm, [(Maybe Name, Type, Kind)]
args) = do
            [Name]
ns <- ((Int, (Maybe Name, Type, Kind)) -> Q Name)
-> [(Int, (Maybe Name, Type, Kind))] -> Q [Name]
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 (\(Int
i, (Maybe Name, Type, Kind)
_) -> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (String
"a" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i)) ([Int]
-> [(Maybe Name, Type, Kind)] -> [(Int, (Maybe Name, Type, Kind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1::Int)..] [(Maybe Name, Type, Kind)]
args)
            let pat :: Pat
pat = (Name -> Pat -> Pat) -> Pat -> [Name] -> Pat
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((\Pat
p Pat
acc -> Name -> Cxt -> [Pat] -> Pat
TH.ConP '(:) [] [Pat
p, Pat
acc]) (Pat -> Pat -> Pat) -> (Name -> Pat) -> Name -> Pat -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Pat
TH.VarP) (Name -> Cxt -> [Pat] -> Pat
TH.ConP '[] [] []) [Name]
ns
            Clause -> Q Clause
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Clause -> Q Clause) -> Clause -> Q Clause
forall a b. (a -> b) -> a -> b
$ [Pat] -> Body -> [Dec] -> Clause
TH.Clause [Lit -> Pat
TH.LitP (String -> Lit
TH.StringL (Name -> String
TH.nameBase Name
nm)), Pat
pat]
                             (Exp -> Body
TH.NormalB ((Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.ConE Name
nm)
                                                        [Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'fromCV) (Name -> Exp
TH.VarE Name
n) | Name
n <- [Name]
ns]))
                             []

    Clause
catchAll <- do Name
s <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"s"
                   Name
l <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"l"
                   let errStr :: Exp
errStr   = Lit -> Exp
TH.LitE (String -> Lit
TH.StringL (String
"fromCV " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
typeName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Unexpected constructor/arity: "))
                       tup :: Exp
tup      = [Maybe Exp] -> Exp
TH.TupE [Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Name -> Exp
TH.VarE Name
s), Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'length) (Name -> Exp
TH.VarE Name
l))]
                       showCall :: Exp
showCall = Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'show) Exp
tup
                       errMsg :: Exp
errMsg   = Maybe Exp -> Exp -> Maybe Exp -> Exp
TH.InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
errStr) (Name -> Exp
TH.VarE '(++)) (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
showCall)
                   Clause -> Q Clause
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Clause -> Q Clause) -> Clause -> Q Clause
forall a b. (a -> b) -> a -> b
$ [Pat] -> Body -> [Dec] -> Clause
TH.Clause [Name -> Pat
TH.VarP Name
s, Name -> Pat
TH.VarP Name
l] (Exp -> Body
TH.NormalB (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'error) Exp
errMsg)) []

    Dec
fromCVFun <- do [Clause]
clss <- ((Name, [(Maybe Name, Type, Kind)]) -> Q Clause)
-> [(Name, [(Maybe Name, Type, Kind)])] -> Q [Clause]
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 (Name, [(Maybe Name, Type, Kind)]) -> Q Clause
fromCVCls [(Name, [(Maybe Name, Type, Kind)])]
cstrs
                    Dec -> Q Dec
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dec -> Q Dec) -> Dec -> Q Dec
forall a b. (a -> b) -> a -> b
$ Name -> [Clause] -> Dec
TH.FunD Name
fromCVFunName ([Clause]
clss [Clause] -> [Clause] -> [Clause]
forall a. [a] -> [a] -> [a]
++ [Clause
catchAll])

    Exp
getFromCV <- [| let unexpected w = error $ "fromCV: " ++ show typeName ++ ": " ++ w
                        kindName (KADT n _ _) = n
                        kindName (KApp n _)   = n
                        kindName k            = unexpected $ "An ADT kind was expected, but got: " ++ show k
                    in \case CV k (CADT (c, kvs)) | kindName k == unmod typeName
                                                 -> $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
fromCVFunName) c (map (uncurry CV) kvs)
                             CV k e -> unexpected $ "Was expecting a CADT value, but got kind: " ++ show k ++ " (rank: " ++ show (cvRank e) ++ ")"
                 |]

    Cxt
symCtx  <- [Q Type] -> Q Cxt
forall (m :: * -> *). Quote m => [m Type] -> m Cxt
TH.cxt [Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
TH.appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.conT ''SymVal) (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.varT Name
n) | Name
n <- [Name]
params]

    Exp
mmBound <- if Bool
isEnum
                  then let universe :: [Q Exp]
universe     = [Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.conE Name
con | (Name
con, [(Maybe Name, Type, Kind)]
_) <- [(Name, [(Maybe Name, Type, Kind)])]
cstrs]
                           (Q Exp
minb, Q Exp
maxb) = case ([Q Exp]
universe, [Q Exp] -> [Q Exp]
forall a. [a] -> [a]
reverse [Q Exp]
universe) of
                                             (Q Exp
x:[Q Exp]
_, Q Exp
y:[Q Exp]
_) -> (Q Exp
x, Q Exp
y)
                                             ([Q Exp], [Q Exp])
_          -> String -> (Q Exp, Q Exp)
forall a. HasCallStack => String -> a
error (String -> (Q Exp, Q Exp)) -> String -> (Q Exp, Q Exp)
forall a b. (a -> b) -> a -> b
$ String
"Impossible: Ran out of elements in determining bounds: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, [(Maybe Name, Type, Kind)])] -> String
forall a. Show a => a -> String
show [(Name, [(Maybe Name, Type, Kind)])]
cstrs
                       in [| Just ($Q Exp
minb, $Q Exp
maxb) |]
                  else [| Nothing |]

    -- make the initializer to get the subtypes registered
    Name
st <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"_st"  -- Get an underscored name here, since st might go unused if there're no subtypes
    Exp
register <- do let concretize :: Type -> Type
concretize b :: Type
b@TH.ConT{}     = Type
b
                       concretize TH.VarT{}       = Name -> Type
TH.ConT ''Integer
                       concretize (TH.AppT Type
l Type
arg) = Type -> Type -> Type
TH.AppT (Type -> Type
concretize Type
l) (Type -> Type
concretize Type
arg)
                       concretize Type
r               = Type
r

                   Stmt
end <- Q Exp -> Q Stmt
forall (m :: * -> *). Quote m => m Exp -> m Stmt
TH.noBindS [| return () |]
                   Exp -> Q Exp
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ Maybe ModName -> [Stmt] -> Exp
TH.DoE Maybe ModName
forall a. Maybe a
Nothing ([Stmt] -> Exp) -> [Stmt] -> Exp
forall a b. (a -> b) -> a -> b
$ [Exp -> Stmt
TH.NoBindS (Exp -> Exp -> Exp
TH.AppE (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'registerKind) (Name -> Exp
TH.VarE Name
st))
                                                                (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'kindOf)
                                                                         (Exp -> Type -> Exp
TH.AppTypeE (Name -> Exp
TH.ConE 'Proxy) (Type -> Type
concretize Type
t))))
                                           | (Name
_, [(Maybe Name, Type, Kind)]
fts) <- [(Name, [(Maybe Name, Type, Kind)])]
cstrs, (Maybe Name
_, Type
t, KApp String
n [Kind]
_) <- [(Maybe Name, Type, Kind)]
fts, String
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= Name -> String
TH.nameBase Name
typeName
                                           ] [Stmt] -> [Stmt] -> [Stmt]
forall a. [a] -> [a] -> [a]
++ [Stmt
end]

    let regFun :: Dec
regFun = Name -> [Clause] -> Dec
TH.FunD 'mkSymValInit [[Pat] -> Body -> [Dec] -> Clause
TH.Clause [Name -> Pat
TH.VarP Name
st, Pat
TH.WildP] (Exp -> Body
TH.NormalB Exp
register) []]

    let symVal :: Dec
symVal = Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
TH.InstanceD
                      Maybe Overlap
forall a. Maybe a
Nothing
                      Cxt
symCtx
                      (Type -> Type -> Type
TH.AppT (Name -> Type
TH.ConT ''SymVal) Type
typeCon)
                      [ Dec
litFun
                      , Dec
regFun
                      , Name -> [Clause] -> Dec
TH.FunD 'minMaxBound [[Pat] -> Body -> [Dec] -> Clause
TH.Clause [] (Exp -> Body
TH.NormalB Exp
mmBound)   []]
                      , Name -> [Clause] -> Dec
TH.FunD 'fromCV      [[Pat] -> Body -> [Dec] -> Clause
TH.Clause [] (Exp -> Body
TH.NormalB Exp
getFromCV) []]
                       ]

    Exp
defCstrs <- [| [(unmod n, map (\(_, _, t) -> t) ntks) | (n, ntks) <- cstrs] |]

    Cxt
kindCtx <- [Q Type] -> Q Cxt
forall (m :: * -> *). Quote m => [m Type] -> m Cxt
TH.cxt [Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
TH.appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.conT ''HasKind) (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.varT Name
p) | Name
p <- [Name]
params]

    let mkPair :: Exp -> Exp -> Exp
mkPair Exp
a Exp
b = [Maybe Exp] -> Exp
TH.TupE [Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
a, Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
b]
        kindDef :: Exp
kindDef = (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
TH.AppE [ Name -> Exp
TH.ConE 'KADT
                                 , Lit -> Exp
TH.LitE (String -> Lit
TH.StringL (Name -> String
unmod Name
typeName))
                                 , [Exp] -> Exp
TH.ListE [ Exp -> Exp -> Exp
mkPair (Lit -> Exp
TH.LitE (String -> Lit
TH.StringL (Name -> String
TH.nameBase Name
p)))
                                                     (Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'kindOf) (Exp -> Type -> Exp
TH.AppTypeE (Name -> Exp
TH.ConE 'Proxy) (Name -> Type
TH.VarT Name
p)))
                                            | Name
p <- [Name]
params
                                            ]
                                 , Exp
defCstrs
                                 ]

        kindDecl :: Dec
kindDecl = Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
TH.InstanceD
                        Maybe Overlap
forall a. Maybe a
Nothing
                        Cxt
kindCtx
                        (Type -> Type -> Type
TH.AppT (Name -> Type
TH.ConT ''HasKind) Type
typeCon)
                        [Name -> [Clause] -> Dec
TH.FunD 'kindOf [[Pat] -> Body -> [Dec] -> Clause
TH.Clause [Pat
TH.WildP] (Exp -> Body
TH.NormalB Exp
kindDef) []]]

    Bool
hasArbitrary <- Name -> Cxt -> Q Bool
TH.isInstance ''Arbitrary [Type
typeCon]
    [Dec]
arbDecl <- case () of
                () | Bool
hasArbitrary -> [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                   | Bool
isEnum       -> let universe :: Q Exp
universe  = [Q Exp] -> Q Exp
forall (m :: * -> *). Quote m => [m Exp] -> m Exp
TH.listE [Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.conE Name
con | (Name
con, [(Maybe Name, Type, Kind)]
_) <- [(Name, [(Maybe Name, Type, Kind)])]
cstrs]
                                     in [d|instance Arbitrary $(Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
typeCon) where
                                             arbitrary = elements $Q Exp
universe
                                        |]
                   | Bool
True         -> [d|instance {-# OVERLAPPABLE #-} Arbitrary $(Type -> Q Type
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
typeCon) where
                                          arbitrary = error $ unlines [ ""
                                                                      , "*** Data.SBV: Cannot quickcheck the given property."
                                                                      , "***"
                                                                      , "*** Default arbitrary instance for " ++ TH.nameBase typeName ++ " is too limited."
                                                                      , "***"
                                                                      , "*** You can overcome this by giving your own Arbitrary instance."
                                                                      , "*** Please get in touch if this workaround is not suitable for your case."
                                                                      ]
                                    |]

    -- Declare constructors
    let declConstructor :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q ((TH.Name, String), [TH.Dec])
        declConstructor :: (Name, [(Maybe Name, Type, Kind)]) -> Q ((Name, String), [Dec])
declConstructor (Name
n, [(Maybe Name, Type, Kind)]
ntks) = do
            let ats :: Cxt
ats = ((Maybe Name, Type, Kind) -> Type)
-> [(Maybe Name, Type, Kind)] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type
mkSBV (Type -> Type)
-> ((Maybe Name, Type, Kind) -> Type)
-> (Maybe Name, Type, Kind)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Maybe Name
_, Type
t, Kind
_) -> Type
t)) [(Maybe Name, Type, Kind)]
ntks
                ty :: Type
ty  = Type -> Type
inSymValContext (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Type) -> Type -> Cxt -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Type -> Type
TH.AppT (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Type
TH.AppT Type
TH.ArrowT) Type
sType Cxt
ats
                bnm :: String
bnm = Name -> String
TH.nameBase Name
n
                nm :: Name
nm  = String -> Name
TH.mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Char
's' Char -> String -> String
forall a. a -> [a] -> [a]
: String
bnm

            [Name]
as    <- ((Maybe Name, Type, Kind) -> Q Name)
-> [(Maybe Name, Type, Kind)] -> Q [Name]
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 (Q Name -> (Maybe Name, Type, Kind) -> Q Name
forall a b. a -> b -> a
const (String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"a")) [(Maybe Name, Type, Kind)]
ntks
            Name
c     <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"c"

            Clause
cls <- [Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
TH.clause ((Name -> Q Pat) -> [Name] -> [Q Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP [Name]
as)
                             (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB
                                   (Q Exp -> [Q Match] -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> [m Match] -> m Exp
TH.caseE [| sequenceA $([Q Exp] -> Q Exp
forall (m :: * -> *). Quote m => [m Exp] -> m Exp
TH.listE [ [| unlitCV $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
a) |] | Name
a <- [Name]
as ]) |]
                                             [ Q Pat -> Q Body -> [Q Dec] -> Q Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
TH.match [p|Just $(Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP Name
c)|]
                                                        (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB [| let k   = kindOf (undefined `asTypeOf` res)
                                                                           res = SBV $ SVal k (Left (CV k (CADT (bnm, $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
c)))))
                                                                       in res
                                                                    |])
                                                        []
                                             , Q Pat -> Q Body -> [Q Dec] -> Q Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
TH.match [p|Nothing|]
                                                        (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB ((Q Exp -> Q Exp -> Q Exp) -> Q Exp -> [Q Exp] -> Q Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Q Exp
a Q Exp
b -> [| $Q Exp
a $Q Exp
b |]) [| mkADTConstructor bnm |] ((Name -> Q Exp) -> [Name] -> [Q Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE [Name]
as)))
                                                        []
                                             ]))
                             []

            ((Name, String), [Dec]) -> Q ((Name, String), [Dec])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Name
nm, String
bnm), [Name -> Type -> Dec
TH.SigD Name
nm Type
ty, Name -> [Clause] -> Dec
TH.FunD Name
nm [Clause
cls]])

    ([(Name, String)]
constrNames, [[Dec]]
cdecls) <- ((Name, [(Maybe Name, Type, Kind)]) -> Q ((Name, String), [Dec]))
-> [(Name, [(Maybe Name, Type, Kind)])]
-> Q ([(Name, String)], [[Dec]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Name, [(Maybe Name, Type, Kind)]) -> Q ((Name, String), [Dec])
declConstructor [(Name, [(Maybe Name, Type, Kind)])]
cstrs

    let btname :: String
btname = Name -> String
TH.nameBase Name
typeName
        tname :: Name
tname  = String -> Name
TH.mkName (Char
'S' Char -> String -> String
forall a. a -> [a] -> [a]
: String
btname)
        tdecl :: Dec
tdecl  = Name -> [TyVarBndr BndrVis] -> Type -> Dec
TH.TySynD Name
tname [Name -> BndrVis -> TyVarBndr BndrVis
forall flag. Name -> flag -> TyVarBndr flag
TH.PlainTV Name
p BndrVis
TH.BndrReq | Name
p <- [Name]
params] Type
sType

    (Name, String) -> [(Name, String)] -> Q ()
addDeclDocs (Name
tname, String
btname) [(Name, String)]
constrNames

    -- Declare accessors
    let -- NB. field count starts at 1!
        declAccessor :: TH.Name -> (Maybe TH.Name, TH.Type, Kind) -> Int -> TH.Q [((TH.Name, String), [TH.Dec])]
        declAccessor :: Name
-> (Maybe Name, Type, Kind) -> Int -> Q [((Name, String), [Dec])]
declAccessor Name
c (Maybe Name
mbUN, Type
ft, Kind
_) Int
i = do
                let bnm :: String
bnm  = Name -> String
TH.nameBase Name
c
                    anm :: String
anm  = String
"get" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
                    nm :: Name
nm   = String -> Name
TH.mkName String
anm
                    ty :: Type
ty    = Type -> Type
inSymValContext (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TH.AppT (Type -> Type -> Type
TH.AppT Type
TH.ArrowT Type
sType) (Type -> Type
mkSBV Type
ft)

                Clause
cls <- do Name
inp <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"inp"
                          [Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
TH.clause [Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP Name
inp]
                                    (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB
                                          (Q Exp -> [Q Match] -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> [m Match] -> m Exp
TH.caseE [| unlitCV $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
inp) |]
                                                    [ Q Pat -> Q Body -> [Q Dec] -> Q Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
TH.match [p|Just (_, CADT (got, kv))|]
                                                               ([Q (Guard, Exp)] -> Q Body
forall (m :: * -> *). Quote m => [m (Guard, Exp)] -> m Body
TH.guardedB [do Guard
g <- Q Exp -> Q Guard
forall (m :: * -> *). Quote m => m Exp -> m Guard
TH.normalG [| got == bnm |]
                                                                                Exp
e <- [| let (k, v) = (kv !! (i-1))
                                                                                        in SBV $ SVal k (Left (CV k v))
                                                                                     |]
                                                                                (Guard, Exp) -> Q (Guard, Exp)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Guard
g, Exp
e)
                                                                            ])
                                                               []
                                                    , Q Pat -> Q Body -> [Q Dec] -> Q Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
TH.match [p|_|]
                                                               (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB [| mkADTAccessor anm $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
inp) |])
                                                               []
                                                    ]))
                                    []

                -- If there's a custom accessor given, declare that here too
                [((Name, String), [Dec])]
extras <- case Maybe Name
mbUN of
                            Maybe Name
Nothing -> [((Name, String), [Dec])] -> Q [((Name, String), [Dec])]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                            Just Name
un -> do let sun :: Name
sun = String -> Name
TH.mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ Char
's' Char -> String -> String
forall a. a -> [a] -> [a]
: Name -> String
TH.nameBase Name
un
                                          [((Name, String), [Dec])] -> Q [((Name, String), [Dec])]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((Name
sun, String
bnm), [Name -> Type -> Dec
TH.SigD Name
sun Type
ty, Name -> [Clause] -> Dec
TH.FunD Name
sun [Clause
cls]])]

                [((Name, String), [Dec])] -> Q [((Name, String), [Dec])]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([((Name, String), [Dec])] -> Q [((Name, String), [Dec])])
-> [((Name, String), [Dec])] -> Q [((Name, String), [Dec])]
forall a b. (a -> b) -> a -> b
$ ((Name
nm, String
bnm), [Name -> Type -> Dec
TH.SigD Name
nm Type
ty, Name -> [Clause] -> Dec
TH.FunD Name
nm [Clause
cls]]) ((Name, String), [Dec])
-> [((Name, String), [Dec])] -> [((Name, String), [Dec])]
forall a. a -> [a] -> [a]
: [((Name, String), [Dec])]
extras

    [[[((Name, String), [Dec])]]]
allDefs <- [Q [[((Name, String), [Dec])]]] -> Q [[[((Name, String), [Dec])]]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence [((Maybe Name, Type, Kind) -> Int -> Q [((Name, String), [Dec])])
-> [(Maybe Name, Type, Kind)]
-> [Int]
-> Q [[((Name, String), [Dec])]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Name
-> (Maybe Name, Type, Kind) -> Int -> Q [((Name, String), [Dec])]
declAccessor Name
c) [(Maybe Name, Type, Kind)]
fs [(Int
1::Int) ..] | (Name
c, [(Maybe Name, Type, Kind)]
fs) <- [(Name, [(Maybe Name, Type, Kind)])]
cstrs]
    let ([(Name, String)]
accessorNames, [[Dec]]
accessorDecls) = [((Name, String), [Dec])] -> ([(Name, String)], [[Dec]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((Name, String), [Dec])] -> ([(Name, String)], [[Dec]]))
-> [((Name, String), [Dec])] -> ([(Name, String)], [[Dec]])
forall a b. (a -> b) -> a -> b
$ [[((Name, String), [Dec])]] -> [((Name, String), [Dec])]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[[((Name, String), [Dec])]]] -> [[((Name, String), [Dec])]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[[((Name, String), [Dec])]]]
allDefs)

    ((Name, String) -> Q ()) -> [(Name, String)] -> Q ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> Name -> Q ()
addDoc String
"Field accessor function." (Name -> Q ())
-> ((Name, String) -> Name) -> (Name, String) -> Q ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, String) -> Name
forall a b. (a, b) -> a
fst) [(Name, String)]
accessorNames

    [Dec]
testerDecls <- Type
-> (Type -> Type)
-> [(Name, [(Maybe Name, Type, Kind)])]
-> Q [Dec]
mkTesters Type
sType Type -> Type
inSymValContext [(Name, [(Maybe Name, Type, Kind)])]
cstrs

    -- Get the case analyzer
    [Dec]
caseSigFuns <- ADTKind
-> Name
-> [Name]
-> [(Name, [(Maybe Name, Type, Kind)])]
-> Q [Dec]
mkCaseAnalyzer ADTKind
adtKind Name
typeName [Name]
params [(Name, [(Maybe Name, Type, Kind)])]
cstrs

    -- Get the induction schema, upto 5 extra args. Only for enums and adts
    [[Dec]]
indDecs <- do let schemas :: Q [[Dec]]
schemas = (Int -> Q [Dec]) -> [Int] -> Q [[Dec]]
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 (Name
-> [Name] -> [(Name, [(Maybe Name, Type, Kind)])] -> Int -> Q [Dec]
mkInductionSchema Name
typeName [Name]
params [(Name, [(Maybe Name, Type, Kind)])]
cstrs) [Int
0 .. Int
5]
                  case ADTKind
adtKind of
                    ADTKind
ADTUninterpreted -> [[Dec]] -> Q [[Dec]]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                    ADTKind
ADTEnum          -> Q [[Dec]]
schemas
                    ADTKind
ADTFull          -> Q [[Dec]]
schemas

    -- If this is an enumeration get EnumSymbolic and OrSymbolic instances
    [Dec]
symEnum <- case ADTKind
adtKind of
                ADTKind
ADTUninterpreted -> [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                ADTKind
ADTFull          -> [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
                ADTKind
ADTEnum          ->
                  let universe :: Q Exp
universe  = [Q Exp] -> Q Exp
forall (m :: * -> *). Quote m => [m Exp] -> m Exp
TH.listE [Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.conE                          Name
con   | (Name
con, [(Maybe Name, Type, Kind)]
_) <- [(Name, [(Maybe Name, Type, Kind)])]
cstrs]
                      universeS :: Q Exp
universeS = [Q Exp] -> Q Exp
forall (m :: * -> *). Quote m => [m Exp] -> m Exp
TH.listE [Lit -> Q Exp
forall (m :: * -> *). Quote m => Lit -> m Exp
TH.litE (String -> Lit
TH.stringL (Name -> String
TH.nameBase Name
con)) | (Name
con, [(Maybe Name, Type, Kind)]
_) <- [(Name, [(Maybe Name, Type, Kind)])]
cstrs]
                  in [d| instance SatModel $(Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.conT Name
typeName) where
                           parseCVs (CV _ (CADT (s, [])) : r)
                             | Just v <- s `lookup` zip $Q Exp
universeS $Q Exp
universe
                             = Just (v, r)
                           parseCVs _ = Nothing

                         instance SL.EnumSymbolic $(Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.conT Name
typeName) where
                           succ x = go (zip $Q Exp
universe (drop 1 $Q Exp
universe))
                             where go []              = some ("succ_" ++ show typeName ++ "_maximal") (const sTrue)
                                   go ((c, s) : rest) = ite (x .== literal c) (literal s) (go rest)

                           pred x = go (zip (drop 1 $Q Exp
universe) $Q Exp
universe)
                             where go []              = some ("pred_" ++ show typeName ++ "_minimal") (const sTrue)
                                   go ((c, s) : rest) = ite (x .== literal c) (literal s) (go rest)

                           toEnum x = go (zip $Q Exp
universe [0..])
                             where go []              = some ("toEnum_" ++ show typeName ++ "_out_of_range") (const sTrue)
                                   go ((c, i) : rest) = ite (x .== literal i) (literal c) (go rest)

                           fromEnum x = go 0 $Q Exp
universe
                             where go _ []     = error "fromEnum: Impossible happened, ran out of elements."
                                   go i [_]    = i
                                   go i (c:cs) = ite (x .== literal c) i (go (i+1) cs)

                           enumFrom n = SL.map SL.toEnum (SL.enumFromTo (SL.fromEnum n) (genericLength $Q Exp
universe - 1))

                           enumFromThen = smtFunction ("EnumSymbolic." ++ TH.nameBase typeName ++ ".enumFromThen") $ \n1 n2 ->
                                                      let i_n1, i_n2 :: SInteger
                                                          i_n1 = SL.fromEnum n1
                                                          i_n2 = SL.fromEnum n2
                                                      in SL.map SL.toEnum (ite (i_n2 .>= i_n1)
                                                                               (SL.enumFromThenTo i_n1 i_n2 (genericLength $Q Exp
universe - 1))
                                                                               (SL.enumFromThenTo i_n1 i_n2 0))

                           enumFromTo     n m   = SL.map SL.toEnum (SL.enumFromTo     (SL.fromEnum n) (SL.fromEnum m))

                           enumFromThenTo n m t = SL.map SL.toEnum (SL.enumFromThenTo (SL.fromEnum n) (SL.fromEnum m) (SL.fromEnum t))

                         instance OrdSymbolic (SBV $(Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.conT Name
typeName)) where
                           a .<  b = SL.fromEnum a .<  SL.fromEnum b
                           a .<= b = SL.fromEnum a .<= SL.fromEnum b
                           a .>  b = SL.fromEnum a .>  SL.fromEnum b
                           a .>= b = SL.fromEnum a .>= SL.fromEnum b
                     |]

    [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$  [Dec
tdecl, Dec
symVal, Dec
kindDecl]
         [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
arbDecl
         [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Dec]]
cdecls
         [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
testerDecls
         [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Dec]]
accessorDecls
         [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
symEnum
         [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec
fromCVSig, Dec
fromCVFun]
         [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
caseSigFuns
         [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Dec]]
indDecs

-- | Make a case analyzer for the type. Works for ADTs and enums. Returns sig and defn
mkCaseAnalyzer :: ADTKind -> TH.Name -> [TH.Name] -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -> TH.Q [TH.Dec]
mkCaseAnalyzer :: ADTKind
-> Name
-> [Name]
-> [(Name, [(Maybe Name, Type, Kind)])]
-> Q [Dec]
mkCaseAnalyzer ADTKind
kind Name
typeName [Name]
params [(Name, [(Maybe Name, Type, Kind)])]
cstrs = case ADTKind
kind of
                                              ADTKind
ADTUninterpreted -> [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [] -- no case analyzer for fully uninterpreted types
                                              ADTKind
ADTEnum          -> Q [Dec]
mk
                                              ADTKind
ADTFull          -> Q [Dec]
mk
  where mk :: Q [Dec]
mk = do let typeCon :: Type
typeCon = Type -> [Name] -> Type
saturate (Name -> Type
TH.ConT Name
typeName) [Name]
params
                    sType :: Type
sType   = Type -> Type
mkSBV Type
typeCon

                    bnm :: String
bnm = Name -> String
TH.nameBase Name
typeName
                    cnm :: Name
cnm = String -> Name
TH.mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"sCase" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bnm

                Name
se   <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (Char
's' Char -> String -> String
forall a. a -> [a] -> [a]
: String
bnm)
                [Name]
fs   <- ((Name, [(Maybe Name, Type, Kind)]) -> Q Name)
-> [(Name, [(Maybe Name, Type, Kind)])] -> Q [Name]
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 (\(Name
nm, [(Maybe Name, Type, Kind)]
_) -> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (Char
'f' Char -> String -> String
forall a. a -> [a] -> [a]
: Name -> String
TH.nameBase Name
nm)) [(Name, [(Maybe Name, Type, Kind)])]
cstrs
                Name
res  <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"result"

                let def :: Dec
def = Name -> [Clause] -> Dec
TH.FunD Name
cnm [[Pat] -> Body -> [Dec] -> Clause
TH.Clause ((Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
TH.VarP (Name
se Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
fs)) (Exp -> Body
TH.NormalB ([(Exp, Exp)] -> Exp
iteChain ((Name -> (Name, [(Maybe Name, Type, Kind)]) -> (Exp, Exp))
-> [Name] -> [(Name, [(Maybe Name, Type, Kind)])] -> [(Exp, Exp)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> Name -> (Name, [(Maybe Name, Type, Kind)]) -> (Exp, Exp)
mkCase Name
se) [Name]
fs [(Name, [(Maybe Name, Type, Kind)])]
cstrs))) []]

                    iteChain :: [(TH.Exp, TH.Exp)] -> TH.Exp
                    iteChain :: [(Exp, Exp)] -> Exp
iteChain []       = String -> Exp
forall a. HasCallStack => String -> a
error (String -> Exp) -> String -> Exp
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Data.SBV.mkADT: Impossible happened!"
                                                        , String
""
                                                        , String
"   Received an empty list for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
typeName
                                                        , String
""
                                                        , String
"While building the case-analyzer."
                                                        , String
"Please report this as a bug."
                                                        ]
                    iteChain [(Exp
_, Exp
l)]        = Exp
l
                    iteChain ((Exp
t, Exp
e) : [(Exp, Exp)]
rest) = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'ite) [Exp -> Exp -> Exp
TH.AppE Exp
t (Name -> Exp
TH.VarE Name
se), Exp
e, [(Exp, Exp)] -> Exp
iteChain [(Exp, Exp)]
rest]

                    mkCase :: TH.Name -> TH.Name -> (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> (TH.Exp, TH.Exp)
                    mkCase :: Name -> Name -> (Name, [(Maybe Name, Type, Kind)]) -> (Exp, Exp)
mkCase Name
cexpr Name
func (Name
c, [(Maybe Name, Type, Kind)]
fields) = (Name -> Exp
TH.VarE (String -> Name
TH.mkName (String
"is" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
c)), (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE Name
func) [Exp]
args)
                       where getters :: [Name]
getters = [String -> Name
TH.mkName (String
"get" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) | (Int
i, (Maybe Name, Type, Kind)
_) <- [Int]
-> [(Maybe Name, Type, Kind)] -> [(Int, (Maybe Name, Type, Kind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1 :: Int) ..] [(Maybe Name, Type, Kind)]
fields]
                             args :: [Exp]
args    = (Name -> Exp) -> [Name] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
g -> Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE Name
g) (Name -> Exp
TH.VarE Name
cexpr)) [Name]
getters

                    rvar :: Type
rvar   = Name -> Type
TH.VarT Name
res
                    mkFun :: Cxt -> Type
mkFun  = (Type -> Type -> Type) -> Type -> Cxt -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Type -> Type
TH.AppT (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Type
TH.AppT Type
TH.ArrowT) Type
rvar
                    fTypes :: Cxt
fTypes = [Cxt -> Type
mkFun (((Maybe Name, Type, Kind) -> Type)
-> [(Maybe Name, Type, Kind)] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Type
mkSBV (Type -> Type)
-> ((Maybe Name, Type, Kind) -> Type)
-> (Maybe Name, Type, Kind)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Maybe Name
_, Type
t, Kind
_) -> Type
t)) [(Maybe Name, Type, Kind)]
ftks) | (Name
_, [(Maybe Name, Type, Kind)]
ftks) <- [(Name, [(Maybe Name, Type, Kind)])]
cstrs]
                    sig :: Dec
sig    = Name -> Type -> Dec
TH.SigD Name
cnm ([TyVarBndr Specificity] -> Cxt -> Type -> Type
TH.ForallT []
                                                     (Type -> Type -> Type
TH.AppT (Name -> Type
TH.ConT ''Mergeable) (Name -> Type
TH.VarT Name
res)
                                                     Type -> Cxt -> Cxt
forall a. a -> [a] -> [a]
: [Type -> Type -> Type
TH.AppT (Name -> Type
TH.ConT ''SymVal) (Name -> Type
TH.VarT Name
p) | Name
p <- [Name]
params]
                                                     )
                                                     (Cxt -> Type
mkFun (Type
sType Type -> Cxt -> Cxt
forall a. a -> [a] -> [a]
: Cxt
fTypes)))

                String -> Name -> Q ()
addDoc (String
"Case analyzer for the type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".") Name
cnm
                [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Dec
sig, Dec
def]

-- | Declare testers
mkTesters :: TH.Type -> (TH.Type -> TH.Type) -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -> TH.Q [TH.Dec]
mkTesters :: Type
-> (Type -> Type)
-> [(Name, [(Maybe Name, Type, Kind)])]
-> Q [Dec]
mkTesters Type
sType Type -> Type
inSymValContext [(Name, [(Maybe Name, Type, Kind)])]
cstrs = do
    let declTester :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q ((TH.Name, String), [TH.Dec])
        declTester :: (Name, [(Maybe Name, Type, Kind)]) -> Q ((Name, String), [Dec])
declTester (Name
c, [(Maybe Name, Type, Kind)]
_) = do
             let ty :: Type
ty  = Type -> Type
inSymValContext (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
TH.AppT (Type -> Type -> Type
TH.AppT Type
TH.ArrowT Type
sType) (Name -> Type
TH.ConT ''SBool)
                 bnm :: String
bnm = Name -> String
TH.nameBase Name
c
                 nm :: Name
nm  = String -> Name
TH.mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"is" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
bnm

             Name
inp <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"inp"
             Clause
cls <- [Q Pat] -> Q Body -> [Q Dec] -> Q Clause
forall (m :: * -> *).
Quote m =>
[m Pat] -> m Body -> [m Dec] -> m Clause
TH.clause [Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP Name
inp]
                              (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB
                                    (Q Exp -> [Q Match] -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> [m Match] -> m Exp
TH.caseE [| unlitCV $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
inp) |]
                                              [ Q Pat -> Q Body -> [Q Dec] -> Q Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
TH.match [p|Just (_, CADT (got, _))|]
                                                         (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB [| literal (got == bnm) |])
                                                         []
                                              , Q Pat -> Q Body -> [Q Dec] -> Q Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
TH.match [p|Nothing|]
                                                         (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
TH.normalB [| mkADTTester ("is-" ++ bnm) $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
inp) |])
                                                         []
                                              ]))
                              []
             ((Name, String), [Dec]) -> Q ((Name, String), [Dec])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Name
nm, String
bnm), [Name -> Type -> Dec
TH.SigD Name
nm Type
ty, Name -> [Clause] -> Dec
TH.FunD Name
nm [Clause
cls]])

    ([(Name, String)]
testerNames, [[Dec]]
testerDecls) <- ((Name, [(Maybe Name, Type, Kind)]) -> Q ((Name, String), [Dec]))
-> [(Name, [(Maybe Name, Type, Kind)])]
-> Q ([(Name, String)], [[Dec]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (Name, [(Maybe Name, Type, Kind)]) -> Q ((Name, String), [Dec])
declTester [(Name, [(Maybe Name, Type, Kind)])]
cstrs

    ((Name, String) -> Q ()) -> [(Name, String)] -> Q ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> Name -> Q ()
addDoc String
"Field recognizer predicate." (Name -> Q ())
-> ((Name, String) -> Name) -> (Name, String) -> Q ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, String) -> Name
forall a b. (a, b) -> a
fst) [(Name, String)]
testerNames

    [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Dec] -> Q [Dec]) -> [Dec] -> Q [Dec]
forall a b. (a -> b) -> a -> b
$ [[Dec]] -> [Dec]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Dec]]
testerDecls

-- We'll just drop the modules to keep this simple
-- If you use multiple expressions named the same (coming from different modules), oh well.
unmod :: TH.Name -> String
unmod :: Name -> String
unmod = String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'.') (String -> String) -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
forall a. [a] -> [a]
reverse (String -> String) -> (Name -> String) -> Name -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Show a => a -> String
show

-- | Given a type name, determine what kind of a data-type it is.
dissect :: TH.Name -> TH.Q (ADTKind, [TH.Name], [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])])
dissect :: Name -> Q (ADTKind, [Name], [(Name, [(Maybe Name, Type, Kind)])])
dissect Name
typeName = do
        ([Name]
args, [(Name, [(Maybe Name, Type)])]
tcs) <- Name -> Q ([Name], [(Name, [(Maybe Name, Type)])])
getConstructors Name
typeName

        let mk :: Name -> (a, Type) -> Q (a, Type, Kind)
mk Name
n (a
mbfn, Type
t) = do Kind
k <- Type -> Q Type
expandSyns Type
t Q Type -> (Type -> Q Kind) -> Q Kind
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> Name -> Type -> Q Kind
toSBV Name
typeName Name
n
                                (a, Type, Kind) -> Q (a, Type, Kind)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
mbfn, Type
t, Kind
k)

        [(Name, [(Maybe Name, Type, Kind)])]
cs <- ((Name, [(Maybe Name, Type)])
 -> Q (Name, [(Maybe Name, Type, Kind)]))
-> [(Name, [(Maybe Name, Type)])]
-> Q [(Name, [(Maybe Name, Type, Kind)])]
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 (\(Name
n, [(Maybe Name, Type)]
ts) -> (Name
n,) ([(Maybe Name, Type, Kind)] -> (Name, [(Maybe Name, Type, Kind)]))
-> Q [(Maybe Name, Type, Kind)]
-> Q (Name, [(Maybe Name, Type, Kind)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Maybe Name, Type) -> Q (Maybe Name, Type, Kind))
-> [(Maybe Name, Type)] -> Q [(Maybe Name, Type, Kind)]
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 (Name -> (Maybe Name, Type) -> Q (Maybe Name, Type, Kind)
forall {a}. Name -> (a, Type) -> Q (a, Type, Kind)
mk Name
n) [(Maybe Name, Type)]
ts) [(Name, [(Maybe Name, Type)])]
tcs

        let k :: ADTKind
k | [(Name, [(Maybe Name, Type, Kind)])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, [(Maybe Name, Type, Kind)])]
cs             = ADTKind
ADTUninterpreted
              | ((Name, [(Maybe Name, Type, Kind)]) -> Bool)
-> [(Name, [(Maybe Name, Type, Kind)])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([(Maybe Name, Type, Kind)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Maybe Name, Type, Kind)] -> Bool)
-> ((Name, [(Maybe Name, Type, Kind)])
    -> [(Maybe Name, Type, Kind)])
-> (Name, [(Maybe Name, Type, Kind)])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, [(Maybe Name, Type, Kind)]) -> [(Maybe Name, Type, Kind)]
forall a b. (a, b) -> b
snd) [(Name, [(Maybe Name, Type, Kind)])]
cs = ADTKind
ADTEnum
              | Bool
True                = ADTKind
ADTFull

        (ADTKind, [Name], [(Name, [(Maybe Name, Type, Kind)])])
-> Q (ADTKind, [Name], [(Name, [(Maybe Name, Type, Kind)])])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ADTKind
k, [Name]
args, [(Name, [(Maybe Name, Type, Kind)])]
cs)

bad :: MonadFail m => String -> [String] -> m a
bad :: forall (m :: * -> *) a. MonadFail m => String -> [String] -> m a
bad String
what [String]
extras = String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String
"mkSymbolic: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
what) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"      " String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
extras

report :: String
report :: String
report = String
"Please report this as a feature request."

-- | Collect the constructors
getConstructors :: TH.Name -> TH.Q ([TH.Name], [(TH.Name, [(Maybe TH.Name, TH.Type)])])
getConstructors :: Name -> Q ([Name], [(Name, [(Maybe Name, Type)])])
getConstructors Name
typeName = do res :: ([Name], [(Name, [(Maybe Name, Type)])])
res@([Name]
_, [(Name, [(Maybe Name, Type)])]
cstrs) <- Type -> Q ([Name], [(Name, [(Maybe Name, Type)])])
getConstructorsFromType (Name -> Type
TH.ConT Name
typeName)

                              -- make sure accessors are unique
                              let noDup :: [Name] -> f ()
noDup [] = () -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                                  noDup (Name
n:[Name]
ns)
                                    | Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
ns = String -> [String] -> f ()
forall (m :: * -> *) a. MonadFail m => String -> [String] -> m a
bad String
"Unsupported field accessor definition."
                                                        [ String
"Multiply used: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
n
                                                        , String
""
                                                        , String
"SBV does not support cases where accessor fields are replicated."
                                                        , String
"Please use each accessor only once."
                                                        ]
                                    | Bool
True        = [Name] -> f ()
noDup [Name]
ns
                              [Name] -> Q ()
forall {f :: * -> *}. MonadFail f => [Name] -> f ()
noDup [Name
n | (Name
_, [(Maybe Name, Type)]
fs) <- [(Name, [(Maybe Name, Type)])]
cstrs, (Just Name
n, Type
_) <- [(Maybe Name, Type)]
fs]

                              ([Name], [(Name, [(Maybe Name, Type)])])
-> Q ([Name], [(Name, [(Maybe Name, Type)])])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Name], [(Name, [(Maybe Name, Type)])])
res

  where getConstructorsFromType :: TH.Type -> TH.Q ([TH.Name], [(TH.Name, [(Maybe TH.Name, TH.Type)])])
        getConstructorsFromType :: Type -> Q ([Name], [(Name, [(Maybe Name, Type)])])
getConstructorsFromType Type
ty = do Type
ty' <- Type -> Q Type
expandSyns Type
ty
                                        case Type -> Maybe (Name, Cxt)
headCon Type
ty' of
                                          Just (Name
n, Cxt
args) -> Name -> Cxt -> Q ([Name], [(Name, [(Maybe Name, Type)])])
reifyFromHead Name
n Cxt
args
                                          Maybe (Name, Cxt)
Nothing        -> String -> [String] -> Q ([Name], [(Name, [(Maybe Name, Type)])])
forall (m :: * -> *) a. MonadFail m => String -> [String] -> m a
bad String
"Not a type constructor"
                                                                [ String
"Name    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
typeName
                                                                , String
"Type    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty
                                                                , String
"Expanded: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
ty'
                                                                ]

        headCon :: TH.Type -> Maybe (TH.Name, [TH.Type])
        headCon :: Type -> Maybe (Name, Cxt)
headCon = Cxt -> Type -> Maybe (Name, Cxt)
go []
          where go :: Cxt -> Type -> Maybe (Name, Cxt)
go Cxt
args (TH.ConT Name
n)    = (Name, Cxt) -> Maybe (Name, Cxt)
forall a. a -> Maybe a
Just (Name
n, Cxt -> Cxt
forall a. [a] -> [a]
reverse Cxt
args)
                go Cxt
args (TH.AppT Type
t Type
a)  = Cxt -> Type -> Maybe (Name, Cxt)
go   (Type
aType -> Cxt -> Cxt
forall a. a -> [a] -> [a]
:Cxt
args) Type
t
                go Cxt
args (TH.SigT Type
t Type
_)  = Cxt -> Type -> Maybe (Name, Cxt)
go      Cxt
args Type
t
                go Cxt
args (TH.ParensT Type
t) = Cxt -> Type -> Maybe (Name, Cxt)
go      Cxt
args Type
t
                go Cxt
_    Type
_              = Maybe (Name, Cxt)
forall a. Maybe a
Nothing

        reifyFromHead :: TH.Name -> [TH.Type] -> TH.Q ([TH.Name], [(TH.Name, [(Maybe TH.Name, TH.Type)])])
        reifyFromHead :: Name -> Cxt -> Q ([Name], [(Name, [(Maybe Name, Type)])])
reifyFromHead Name
n Cxt
args = do Info
info <- Name -> Q Info
TH.reify Name
n
                                  case Info
info of
                                    TH.TyConI (TH.DataD    Cxt
_ Name
_ [TyVarBndr BndrVis]
tvs Maybe Type
_ [Con]
cons [DerivClause]
_) -> ((TyVarBndr BndrVis -> Name) -> [TyVarBndr BndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr BndrVis -> Name
tvName [TyVarBndr BndrVis]
tvs,) ([(Name, [(Maybe Name, Type)])]
 -> ([Name], [(Name, [(Maybe Name, Type)])]))
-> Q [(Name, [(Maybe Name, Type)])]
-> Q ([Name], [(Name, [(Maybe Name, Type)])])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Con -> Q (Name, [(Maybe Name, Type)]))
-> [Con] -> Q [(Name, [(Maybe Name, Type)])]
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 ([(Name, Type)] -> Con -> Q (Name, [(Maybe Name, Type)])
expandCon ([TyVarBndr BndrVis] -> Cxt -> [(Name, Type)]
mkSubst [TyVarBndr BndrVis]
tvs Cxt
args)) [Con]
cons
                                    TH.TyConI (TH.NewtypeD Cxt
_ Name
_ [TyVarBndr BndrVis]
tvs Maybe Type
_ Con
con  [DerivClause]
_) -> ((TyVarBndr BndrVis -> Name) -> [TyVarBndr BndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr BndrVis -> Name
tvName [TyVarBndr BndrVis]
tvs,) ([(Name, [(Maybe Name, Type)])]
 -> ([Name], [(Name, [(Maybe Name, Type)])]))
-> Q [(Name, [(Maybe Name, Type)])]
-> Q ([Name], [(Name, [(Maybe Name, Type)])])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Con -> Q (Name, [(Maybe Name, Type)]))
-> [Con] -> Q [(Name, [(Maybe Name, Type)])]
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 ([(Name, Type)] -> Con -> Q (Name, [(Maybe Name, Type)])
expandCon ([TyVarBndr BndrVis] -> Cxt -> [(Name, Type)]
mkSubst [TyVarBndr BndrVis]
tvs Cxt
args)) [Con
con]
                                    TH.TyConI (TH.TySynD Name
_ [TyVarBndr BndrVis]
tvs Type
rhs)          -> Type -> Q ([Name], [(Name, [(Maybe Name, Type)])])
getConstructorsFromType ([(Name, Type)] -> Type -> Type
applySubst ([TyVarBndr BndrVis] -> Cxt -> [(Name, Type)]
mkSubst [TyVarBndr BndrVis]
tvs Cxt
args) Type
rhs)
                                    Info
_ -> String -> [String] -> Q ([Name], [(Name, [(Maybe Name, Type)])])
forall (m :: * -> *) a. MonadFail m => String -> [String] -> m a
bad String
"Unsupported kind"
                                             [ String
"Type : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
typeName
                                             , String
"Name : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
                                             , String
"Kind : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Info -> String
forall a. Show a => a -> String
show Info
info
                                             ]

        onSnd :: (t -> f a) -> (t, t) -> f (t, a)
onSnd t -> f a
f (t
a, t
b) = (t
a,) (a -> (t, a)) -> f a -> f (t, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t -> f a
f t
b

        expandCon :: [(TH.Name, TH.Type)] -> TH.Con -> TH.Q (TH.Name, [(Maybe TH.Name, TH.Type)])
        expandCon :: [(Name, Type)] -> Con -> Q (Name, [(Maybe Name, Type)])
expandCon [(Name, Type)]
sub (TH.NormalC  Name
n [BangType]
fields)          = (Name
n,) ([(Maybe Name, Type)] -> (Name, [(Maybe Name, Type)]))
-> Q [(Maybe Name, Type)] -> Q (Name, [(Maybe Name, Type)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BangType -> Q (Maybe Name, Type))
-> [BangType] -> Q [(Maybe Name, Type)]
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 ((Type -> Q Type) -> (Maybe Name, Type) -> Q (Maybe Name, Type)
forall {f :: * -> *} {t} {a} {t}.
Functor f =>
(t -> f a) -> (t, t) -> f (t, a)
onSnd (Type -> Q Type
expandSyns (Type -> Q Type) -> (Type -> Type) -> Type -> Q Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, Type)] -> Type -> Type
applySubst [(Name, Type)]
sub) ((Maybe Name, Type) -> Q (Maybe Name, Type))
-> (BangType -> (Maybe Name, Type))
-> BangType
-> Q (Maybe Name, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(   Bang
_,Type
t) -> (Maybe Name
forall a. Maybe a
Nothing, Type
t))) [BangType]
fields
        expandCon [(Name, Type)]
sub (TH.RecC     Name
n [VarBangType]
fields)          = (Name
n,) ([(Maybe Name, Type)] -> (Name, [(Maybe Name, Type)]))
-> Q [(Maybe Name, Type)] -> Q (Name, [(Maybe Name, Type)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarBangType -> Q (Maybe Name, Type))
-> [VarBangType] -> Q [(Maybe Name, Type)]
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 ((Type -> Q Type) -> (Maybe Name, Type) -> Q (Maybe Name, Type)
forall {f :: * -> *} {t} {a} {t}.
Functor f =>
(t -> f a) -> (t, t) -> f (t, a)
onSnd (Type -> Q Type
expandSyns (Type -> Q Type) -> (Type -> Type) -> Type -> Q Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, Type)] -> Type -> Type
applySubst [(Name, Type)]
sub) ((Maybe Name, Type) -> Q (Maybe Name, Type))
-> (VarBangType -> (Maybe Name, Type))
-> VarBangType
-> Q (Maybe Name, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Name
fn,Bang
_,Type
t) -> (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
fn, Type
t))) [VarBangType]
fields
        expandCon [(Name, Type)]
sub (TH.InfixC   (Bang
_, Type
t1) Name
n (Bang
_, Type
t2)) = (Name
n,) ([(Maybe Name, Type)] -> (Name, [(Maybe Name, Type)]))
-> Q [(Maybe Name, Type)] -> Q (Name, [(Maybe Name, Type)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Maybe Name, Type) -> Q (Maybe Name, Type))
-> [(Maybe Name, Type)] -> Q [(Maybe Name, Type)]
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 ((Type -> Q Type) -> (Maybe Name, Type) -> Q (Maybe Name, Type)
forall {f :: * -> *} {t} {a} {t}.
Functor f =>
(t -> f a) -> (t, t) -> f (t, a)
onSnd (Type -> Q Type
expandSyns (Type -> Q Type) -> (Type -> Type) -> Type -> Q Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, Type)] -> Type -> Type
applySubst [(Name, Type)]
sub)) [(Maybe Name
forall a. Maybe a
Nothing, Type
t1), (Maybe Name
forall a. Maybe a
Nothing, Type
t2)]
        {- These don't have proper correspondences in SMTLib; so ignore.
        expandCon sub (TH.ForallC  _ _ c)             = expandCon sub c
        expandCon sub (TH.GadtC    [n] fields _)      = (n,) <$> mapM (onSnd (expandSyns . applySubst sub) . (\(   _,t) -> (Nothing, t))) fields
        expandCon sub (TH.RecGadtC [n] fields _)      = (n,) <$> mapM (onSnd (expandSyns . applySubst sub) . (\(fn,_,t) -> (Just fn, t))) fields
        -}
        expandCon [(Name, Type)]
_   Con
c                               = String -> [String] -> Q (Name, [(Maybe Name, Type)])
forall (m :: * -> *) a. MonadFail m => String -> [String] -> m a
bad String
"Unsupported constructor form: "
                                                            [ String
"Type       : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
typeName
                                                            , String
"Constructor: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Con -> String
forall a. Show a => a -> String
show Con
c
                                                            , String
""
                                                            , String
report
                                                            ]

        tvName :: TH.TyVarBndr TH.BndrVis -> TH.Name
        tvName :: TyVarBndr BndrVis -> Name
tvName (TH.PlainTV  Name
n BndrVis
_)   = Name
n
        tvName (TH.KindedTV Name
n BndrVis
_ Type
_) = Name
n

        -- | Make substitution from type variables to actual args
        mkSubst :: [TH.TyVarBndr TH.BndrVis] -> [TH.Type] -> [(TH.Name, TH.Type)]
        mkSubst :: [TyVarBndr BndrVis] -> Cxt -> [(Name, Type)]
mkSubst [TyVarBndr BndrVis]
tvs = [Name] -> Cxt -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((TyVarBndr BndrVis -> Name) -> [TyVarBndr BndrVis] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TyVarBndr BndrVis -> Name
tvName [TyVarBndr BndrVis]
tvs)

        -- | Apply substitution to a Type
        applySubst :: [(TH.Name, TH.Type)] -> TH.Type -> TH.Type
        applySubst :: [(Name, Type)] -> Type -> Type
applySubst [(Name, Type)]
sub = Type -> Type
go
          where go :: Type -> Type
go (TH.VarT    Name
n)        = Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe  (Name -> Type
TH.VarT Name
n) (Name
n Name -> [(Name, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Name, Type)]
sub)
                go (TH.AppT    Type
t1 Type
t2)    = Type -> Type -> Type
TH.AppT    (Type -> Type
go Type
t1) (Type -> Type
go Type
t2)
                go (TH.SigT    Type
t Type
k)      = Type -> Type -> Type
TH.SigT    (Type -> Type
go Type
t)  Type
k
                go (TH.ParensT Type
t)        = Type -> Type
TH.ParensT (Type -> Type
go Type
t)
                go (TH.InfixT  Type
t1 Name
n Type
t2)  = Type -> Name -> Type -> Type
TH.InfixT  (Type -> Type
go Type
t1) Name
n (Type -> Type
go Type
t2)
                go (TH.UInfixT Type
t1 Name
n Type
t2)  = Type -> Name -> Type -> Type
TH.UInfixT (Type -> Type
go Type
t1) Name
n (Type -> Type
go Type
t2)
                go (TH.ForallT [TyVarBndr Specificity]
bs Cxt
ctx Type
t) = [TyVarBndr Specificity] -> Cxt -> Type -> Type
TH.ForallT [TyVarBndr Specificity]
bs ((Type -> Type) -> Cxt -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
goPred Cxt
ctx) (Type -> Type
go Type
t)
                go Type
t                     = Type
t

                goPred :: Type -> Type
goPred (TH.AppT Type
t1 Type
t2) = Type -> Type -> Type
TH.AppT (Type -> Type
go Type
t1) (Type -> Type
go Type
t2)
                goPred Type
p               = Type
p

-- | Find the SBV kind for this type
toSBV :: TH.Name -> TH.Name -> TH.Type -> TH.Q Kind
toSBV :: Name -> Name -> Type -> Q Kind
toSBV Name
typeName Name
constructorName = Type -> Q Kind
forall {f :: * -> *}. MonadFail f => Type -> f Kind
go
  where hasArrows :: Type -> Bool
hasArrows (TH.AppT Type
TH.ArrowT Type
_)   = Bool
True
        hasArrows (TH.AppT Type
lhs       Type
rhs) = Type -> Bool
hasArrows Type
lhs Bool -> Bool -> Bool
|| Type -> Bool
hasArrows Type
rhs
        hasArrows Type
_                       = Bool
False

        -- Handle type variables (parameters)
        go :: Type -> f Kind
go (TH.VarT Name
v) = Kind -> f Kind
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind -> f Kind) -> Kind -> f Kind
forall a b. (a -> b) -> a -> b
$ String -> Kind
KVar (Name -> String
TH.nameBase Name
v)

        -- tuples
        go Type
t | Just Cxt
ps <- Type -> Maybe Cxt
getTuple Type
t = [Kind] -> Kind
KTuple ([Kind] -> Kind) -> f [Kind] -> f Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Kind) -> Cxt -> f [Kind]
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 Type -> f Kind
go Cxt
ps

        -- recognize strings, since we don't (yet) support chars
        go (TH.AppT Type
TH.ListT (TH.ConT Name
t)) | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Char = Kind -> f Kind
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
KString

        -- lists
        go (TH.AppT Type
TH.ListT Type
t) = Kind -> Kind
KList (Kind -> Kind) -> f Kind -> f Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> f Kind
go Type
t

        -- arbitrary words/ints
        go (TH.AppT (TH.ConT Name
nm) (TH.LitT (TH.NumTyLit Uniq
n)))
            | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''WordN = Kind -> f Kind
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind -> f Kind) -> Kind -> f Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False (Uniq -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Uniq
n)
            | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''IntN  = Kind -> f Kind
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind -> f Kind) -> Kind -> f Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
True  (Uniq -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Uniq
n)

        -- arbitrary floats
        go (TH.AppT (TH.AppT (TH.ConT Name
nm) (TH.LitT (TH.NumTyLit Uniq
eb))) (TH.LitT (TH.NumTyLit Uniq
sb)))
            | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''FloatingPoint = Kind -> f Kind
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Kind -> f Kind) -> Kind -> f Kind
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Kind
KFP (Uniq -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Uniq
eb) (Uniq -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Uniq
sb)

        -- Rational
        go (TH.AppT (TH.ConT Name
nm) (TH.ConT Name
i))
            | Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Ratio Bool -> Bool -> Bool
&& Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Integer
            = Kind -> f Kind
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
KRational

        -- deal with base types
        go t :: Type
t@(TH.ConT Name
constr)
            | Just Either (String, [String]) Kind
base <- Name -> Maybe (Either (String, [String]) Kind)
getBase Name
constr
            = case Either (String, [String]) Kind
base of
                Left (String
w, [String]
r) -> String -> [String] -> f Kind
forall (m :: * -> *) a. MonadFail m => String -> [String] -> m a
bad String
w ([String] -> f Kind) -> [String] -> f Kind
forall a b. (a -> b) -> a -> b
$ [ String
"Datatype   : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
typeName
                                       , String
"Constructor: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
constructorName
                                       , String
"Kind       : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Ppr a => a -> String
TH.pprint Type
t
                                       , String
""
                                       ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
r
                Right Kind
k     -> Kind -> f Kind
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
k

        -- deal with constructors
        go Type
t
           | Just (Name
c, Cxt
ps) <- Type -> Maybe (Name, Cxt)
getConApp Type
t
           = String -> [Kind] -> Kind
KApp (Name -> String
TH.nameBase Name
c) ([Kind] -> Kind) -> f [Kind] -> f Kind
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> f Kind) -> Cxt -> f [Kind]
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 Type -> f Kind
go Cxt
ps

        -- giving up
        go Type
t = String -> [String] -> f Kind
forall (m :: * -> *) a. MonadFail m => String -> [String] -> m a
bad String
"Unsupported constructor kind" [ String
"Datatype   : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
typeName
                                                  , String
"Constructor: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
TH.nameBase Name
constructorName
                                                  , String
"Kind       : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Ppr a => a -> String
TH.pprint Type
t
                                                  , String
""
                                                  , if Type -> Bool
hasArrows Type
t
                                                    then String
"Higher order fields (i.e., function values) are not supported."
                                                    else String
report
                                                  ]

        -- Extract application of a constructor to some type-variables
        getConApp :: Type -> Maybe (Name, Cxt)
getConApp Type
t = Type -> Cxt -> Maybe (Name, Cxt)
locate Type
t []
          where locate :: Type -> Cxt -> Maybe (Name, Cxt)
locate (TH.ConT Name
c)     Cxt
sofar = (Name, Cxt) -> Maybe (Name, Cxt)
forall a. a -> Maybe a
Just (Name
c, Cxt
sofar)
                locate (TH.AppT Type
l Type
arg) Cxt
sofar = Type -> Cxt -> Maybe (Name, Cxt)
locate Type
l (Type
arg Type -> Cxt -> Cxt
forall a. a -> [a] -> [a]
: Cxt
sofar)
                locate Type
_               Cxt
_     = Maybe (Name, Cxt)
forall a. Maybe a
Nothing

        -- Extract an N-tuple
        getTuple :: Type -> Maybe Cxt
getTuple = Cxt -> Type -> Maybe Cxt
tup []
          where tup :: Cxt -> Type -> Maybe Cxt
tup Cxt
sofar (TH.TupleT Int
_) = Cxt -> Maybe Cxt
forall a. a -> Maybe a
Just Cxt
sofar
                tup Cxt
sofar (TH.AppT Type
t Type
p) = Cxt -> Type -> Maybe Cxt
tup (Type
p Type -> Cxt -> Cxt
forall a. a -> [a] -> [a]
: Cxt
sofar) Type
t
                tup Cxt
_     Type
_             = Maybe Cxt
forall a. Maybe a
Nothing

        -- Given the name of a base type, what's the equivalent in the SBV domain (if we have it)
        getBase :: TH.Name -> Maybe (Either (String, [String]) Kind)
        getBase :: Name -> Maybe (Either (String, [String]) Kind)
getBase Name
t
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Bool     = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right Kind
KBool
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Integer  = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right Kind
KUnbounded
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Float    = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right Kind
KFloat
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Double   = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right Kind
KDouble
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Char     = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right Kind
KChar
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''String   = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right Kind
KString
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''AlgReal  = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right Kind
KReal
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Rational = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right Kind
KRational
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Word8    = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right (Kind -> Either (String, [String]) Kind)
-> Kind -> Either (String, [String]) Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False  Int
8
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Word16   = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right (Kind -> Either (String, [String]) Kind)
-> Kind -> Either (String, [String]) Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False Int
16
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Word32   = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right (Kind -> Either (String, [String]) Kind)
-> Kind -> Either (String, [String]) Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False Int
32
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Word64   = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right (Kind -> Either (String, [String]) Kind)
-> Kind -> Either (String, [String]) Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
False Int
64
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Int8     = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right (Kind -> Either (String, [String]) Kind)
-> Kind -> Either (String, [String]) Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
True   Int
8
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Int16    = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right (Kind -> Either (String, [String]) Kind)
-> Kind -> Either (String, [String]) Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
True  Int
16
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Int32    = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right (Kind -> Either (String, [String]) Kind)
-> Kind -> Either (String, [String]) Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
True  Int
32
          | Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Int64    = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ Kind -> Either (String, [String]) Kind
forall a b. b -> Either a b
Right (Kind -> Either (String, [String]) Kind)
-> Kind -> Either (String, [String]) Kind
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Kind
KBounded Bool
True  Int
64

          -- Platform specific, flag:
          |    Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Int
            Bool -> Bool -> Bool
|| Name
t Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Word  = Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a. a -> Maybe a
Just (Either (String, [String]) Kind
 -> Maybe (Either (String, [String]) Kind))
-> Either (String, [String]) Kind
-> Maybe (Either (String, [String]) Kind)
forall a b. (a -> b) -> a -> b
$ (String, [String]) -> Either (String, [String]) Kind
forall a b. a -> Either a b
Left ( String
"Platform specific type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
t
                                          , [ String
"Please pick a more specific type, such as"
                                            , String
"Integer, Word8, WordN 32, IntN 16 etc."
                                            ])

          -- Otherwise, can't translate
          | Bool
True            = Maybe (Either (String, [String]) Kind)
forall a. Maybe a
Nothing

-- | Make an induction schema for the type, with n extra arguments.
mkInductionSchema :: TH.Name -> [TH.Name] -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -> Int -> TH.Q [TH.Dec]
mkInductionSchema :: Name
-> [Name] -> [(Name, [(Maybe Name, Type, Kind)])] -> Int -> Q [Dec]
mkInductionSchema Name
typeName [Name]
params [(Name, [(Maybe Name, Type, Kind)])]
cstrs Int
extraArgCnt = do
   let btype :: String
btype = Name -> String
TH.nameBase Name
typeName
       nm :: String
nm    = String
"induct" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
btype String -> String -> String
forall a. [a] -> [a] -> [a]
++ if Int
extraArgCnt Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then String
"" else Int -> String
forall a. Show a => a -> String
show Int
extraArgCnt

   Name
pf <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"pf"

   [Name]
extraNames <- (Int -> Q Name) -> [Int] -> Q [Name]
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 (Q Name -> Int -> Q Name
forall a b. a -> b -> a
const (String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"extraN")) [Int
0 .. Int
extraArgCntInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
   [Name]
extraSyms  <- (Int -> Q Name) -> [Int] -> Q [Name]
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 (Q Name -> Int -> Q Name
forall a b. a -> b -> a
const (String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"extraS")) [Int
0 .. Int
extraArgCntInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
   [Name]
extraTypes <- (Int -> Q Name) -> [Int] -> Q [Name]
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 (Q Name -> Int -> Q Name
forall a b. a -> b -> a
const (String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"extraT")) [Int
0 .. Int
extraArgCntInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]

   let mkLam :: [Name] -> Q Exp -> Q Exp
mkLam = [Q Pat] -> Q Exp -> Q Exp
forall (m :: * -> *). Quote m => [m Pat] -> m Exp -> m Exp
TH.lamE ([Q Pat] -> Q Exp -> Q Exp)
-> ([Name] -> [Q Pat]) -> [Name] -> Q Exp -> Q Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name -> Q Pat) -> [Name] -> [Q Pat]
forall a b. (a -> b) -> [a] -> [b]
map (\Name
a -> Name -> [Q Pat] -> Q Pat
forall (m :: * -> *). Quote m => Name -> [m Pat] -> m Pat
TH.conP 'Forall [Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP Name
a])

   let mkIndCase :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q TH.Exp
       mkIndCase :: (Name, [(Maybe Name, Type, Kind)]) -> Q Exp
mkIndCase (Name
cstr, [(Maybe Name, Type, Kind)]
flds)
         | [(Maybe Name, Type, Kind)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Maybe Name, Type, Kind)]
flds Bool -> Bool -> Bool
&& [Name] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
extraNames
         = [| $(Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
pf) $(Q Exp
scstr) |]
         | Bool
True
         = do [Name]
as <- ((Maybe Name, Type, Kind) -> Q Name)
-> [(Maybe Name, Type, Kind)] -> Q [Name]
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 (Q Name -> (Maybe Name, Type, Kind) -> Q Name
forall a b. a -> b -> a
const (String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"a")) [(Maybe Name, Type, Kind)]
flds
              let -- When can we have the inductive hypothesis?
                  --  (1) same type
                  --  (2) applied at exactly the same types
                  isRecursive :: (a, b, Kind) -> Bool
isRecursive (a
_, b
_, Kind
k) = case Kind
k of
                                            KApp String
t [Kind]
ps -> String
t String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
btype Bool -> Bool -> Bool
&& [Kind]
ps [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== (Name -> Kind) -> [Name] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Kind
KVar (String -> Kind) -> (Name -> String) -> Name -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
TH.nameBase) [Name]
params
                                            Kind
_         -> Bool
False
                  recFields :: [Name]
recFields = [Name
a | (Name
a, (Maybe Name, Type, Kind)
f) <- [Name]
-> [(Maybe Name, Type, Kind)] -> [(Name, (Maybe Name, Type, Kind))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
as [(Maybe Name, Type, Kind)]
flds, (Maybe Name, Type, Kind) -> Bool
forall {a} {b}. (a, b, Kind) -> Bool
isRecursive (Maybe Name, Type, Kind)
f]

              Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE (Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE 'quantifiedBool)
                      ([Name] -> Q Exp -> Q Exp
mkLam ([Name]
as [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
extraNames)
                             ([Name] -> Q Exp -> Q Exp
mkImp [Name]
recFields ((Q Exp -> Q Exp -> Q Exp) -> Q Exp -> [Q Exp] -> Q Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE
                                                     (Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE (Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
pf) ((Q Exp -> Q Exp -> Q Exp) -> Q Exp -> [Q Exp] -> Q Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE Q Exp
scstr ((Name -> Q Exp) -> [Name] -> [Q Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE [Name]
as)))
                                                     ((Name -> Q Exp) -> [Name] -> [Q Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE [Name]
extraNames))))
         where cnm :: String
cnm   = Name -> String
TH.nameBase Name
cstr
               lcnm :: String
lcnm  = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
cnm
               scstr :: Q Exp
scstr = Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE (String -> Name
TH.mkName (Char
's' Char -> String -> String
forall a. a -> [a] -> [a]
: String
cnm))

               mkImp :: [Name] -> Q Exp -> Q Exp
mkImp []  Q Exp
e = Q Exp
e
               mkImp [Name
i] Q Exp
e = (Q Exp -> Q Exp -> Q Exp) -> [Q Exp] -> Q Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE [Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE '(.=>), Name -> Q Exp
assume Name
i, Q Exp
e]
               mkImp [Name]
is  Q Exp
e = (Q Exp -> Q Exp -> Q Exp) -> [Q Exp] -> Q Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE [Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE '(.=>), (Q Exp -> Q Exp -> Q Exp) -> [Q Exp] -> Q Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE [Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE 'sAnd, [Q Exp] -> Q Exp
forall (m :: * -> *). Quote m => [m Exp] -> m Exp
TH.listE ((Name -> Q Exp) -> [Name] -> [Q Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Exp
assume [Name]
is)], Q Exp
e]

               assume :: TH.Name -> TH.Q TH.Exp
               assume :: Name -> Q Exp
assume Name
n = do [Name]
en <- (Int -> Q Name) -> [Int] -> Q [Name]
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 (Q Name -> Int -> Q Name
forall a b. a -> b -> a
const (String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName (String
lcnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_extraN"))) [Int
0 .. Int
extraArgCntInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
                             Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE (Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE 'quantifiedBool)
                                     ([Name] -> Q Exp -> Q Exp
mkLam [Name]
en ((Q Exp -> Q Exp -> Q Exp) -> Q Exp -> [Q Exp] -> Q Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE (Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
pf) ((Name -> Q Exp) -> [Name] -> [Q Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
en))))

   [Exp]
cases <- ((Name, [(Maybe Name, Type, Kind)]) -> Q Exp)
-> [(Name, [(Maybe Name, Type, Kind)])] -> Q [Exp]
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 (Name, [(Maybe Name, Type, Kind)]) -> Q Exp
mkIndCase [(Name, [(Maybe Name, Type, Kind)])]
cstrs
   Exp
post  <- do Name
a <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"recVal"
               Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE (Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE 'quantifiedBool)
                       ([Name] -> Q Exp -> Q Exp
mkLam (Name
a Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
extraNames) (Q Exp -> Q Exp) -> Q Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ (Q Exp -> Q Exp -> Q Exp) -> Q Exp -> [Q Exp] -> Q Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Q Exp -> Q Exp -> Q Exp
forall {m :: * -> *}. Quote m => m Exp -> m Exp -> m Exp
TH.appE (Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
pf) ((Name -> Q Exp) -> [Name] -> [Q Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE (Name
a Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
extraNames)))

   Name
propName <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"prop"
   Name
argName  <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"a"
   Name
taName   <- String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
TH.newName String
"ta"

   let pre :: Exp
pre    = (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
TH.AppE [Name -> Exp
TH.VarE 'sAnd,  [Exp] -> Exp
TH.ListE [Exp]
cases]
       schema :: Exp
schema = (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
TH.AppE [Name -> Exp
TH.VarE '(.=>), Exp
pre, Exp
post]
       ihB :: Exp
ihB    = Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.VarE 'proofOf) ((Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
TH.AppE [Name -> Exp
TH.VarE 'internalAxiom, Lit -> Exp
TH.LitE (String -> Lit
TH.StringL String
nm), Exp
schema])

       instHead :: Type
instHead = Type -> Type -> Type
TH.AppT (Name -> Type
TH.ConT ''HasInductionSchema)
                          ((Type -> Type -> Type) -> Type -> Cxt -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> Type -> Type
TH.AppT (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Type -> Type
TH.AppT Type
TH.ArrowT)
                                 (Name -> Type
TH.ConT ''SBool)
                                 [  Type -> Type -> Type
TH.AppT (Name -> Type
TH.ConT ''Forall) (Name -> Type
TH.VarT Name
es) Type -> Type -> Type
`TH.AppT` Type
et
                                  | (Name
es, Type
et) <- [Name] -> Cxt -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Name
taName Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
extraSyms)
                                                    (Type -> [Name] -> Type
saturate (Name -> Type
TH.ConT Name
typeName) [Name]
params Type -> Cxt -> Cxt
forall a. a -> [a] -> [a]
: (Name -> Type) -> [Name] -> Cxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> Type
TH.VarT [Name]
extraTypes)
                                 ])

       pfFun :: Dec
pfFun = Name -> [Clause] -> Dec
TH.FunD Name
pf [[Pat] -> Body -> [Dec] -> Clause
TH.Clause ((Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
TH.VarP (Name
argName Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
extraNames))
                                     (Exp -> Body
TH.NormalB ((Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
TH.AppE
                                                        (Name -> Exp
TH.VarE Name
propName)
                                                        [Exp -> Exp -> Exp
TH.AppE (Name -> Exp
TH.ConE 'Forall) (Name -> Exp
TH.VarE Name
a) | Name
a <- Name
argName Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
extraNames]))
                                     []
                          ]

       method :: Dec
method = Name -> [Clause] -> Dec
TH.FunD 'inductionSchema
                        [[Pat] -> Body -> [Dec] -> Clause
TH.Clause [Name -> Pat
TH.VarP Name
propName]
                                   (Exp -> Body
TH.NormalB ([Dec] -> Exp -> Exp
TH.LetE [Dec
pfFun] Exp
ihB))
                                   []
                        ]

   Cxt
context <- [Q Type] -> Q Cxt
forall (m :: * -> *). Quote m => [m Type] -> m Cxt
TH.cxt [Q Type -> Q Type -> Q Type
forall (m :: * -> *). Quote m => m Type -> m Type -> m Type
TH.appT (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.conT ''SymVal) (Name -> Q Type
forall (m :: * -> *). Quote m => Name -> m Type
TH.varT Name
n) | Name
n <- [Name]
params [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
extraTypes]

   [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Maybe Overlap -> Cxt -> Type -> [Dec] -> Dec
TH.InstanceD Maybe Overlap
forall a. Maybe a
Nothing Cxt
context Type
instHead [Dec
method]]