content: -----------------------------------------------------------------------------
  -- |
  -- 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 QuasiQuotes         #-}
  {-# 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)
  import Test.QuickCheck (Arbitrary(..), elements)
  
  import qualified Control.Exception as C
  
  import Data.Maybe (fromMaybe)
  
  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.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 cfg = check `C.catch` (\(_ :: C.SomeException) -> return False)
    where check = do ThmResult r <- proveWith cfg $ \x -> sNot (sNot x) .== (x :: SBool)
                     case r of
                       Unsatisfiable{} -> return True
                       _               -> return False
  
  -- | The default configs corresponding to supported SMT solvers
  defaultSolverConfig :: Solver -> SMTConfig
  defaultSolverConfig ABC       = abc
  defaultSolverConfig Boolector = boolector
  defaultSolverConfig Bitwuzla  = bitwuzla
  defaultSolverConfig CVC4      = cvc4
  defaultSolverConfig CVC5      = cvc5
  defaultSolverConfig DReal     = dReal
  defaultSolverConfig MathSAT   = mathSAT
  defaultSolverConfig OpenSMT   = openSMT
  defaultSolverConfig Yices     = yices
  defaultSolverConfig Z3        = z3
  
  -- | Return the known available solver configs, installed on your machine.
  getAvailableSolvers :: IO [SMTConfig]
  getAvailableSolvers = filterM sbvCheckSolverInstallation (map defaultSolverConfig [minBound .. 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 ts = concat <$> mapM mkSymbolicADT ts
  
  -- | Create a symbolic ADT.
  mkSymbolicADT :: TH.Name -> TH.Q [TH.Dec]
  mkSymbolicADT typeName = do
  
       (tKind, params, cstrs) <- dissect typeName
       ds <- mkADT tKind typeName params cstrs
  
       -- declare an "undefiner" so we don't have stray names
       nm <- TH.newName $ "_undefiner_" ++ TH.nameBase typeName
       addDoc "Autogenerated definition to avoid unused-variable warnings from GHC." nm
  
       -- undefiner must be careful in putting ascriptions
       aVar <- TH.newName "a"
       let undefine n
             | base == "sCase" ++ tbase = wrap 1   -- Needs an extra param
             | True                     = wrap 0
             where tbase  = TH.nameBase typeName
                   base   = TH.nameBase n
                   wrap c = foldl TH.AppTypeE (TH.VarE n) (replicate (c + length params) (TH.ConT ''Integer))
  
           names     = [undefine n | TH.FunD n _ <- ds]
           body      = foldl TH.AppE (TH.VarE 'undefined)
                                     (names ++ [TH.SigE (TH.VarE 'undefined)
                                                        (foldl TH.AppT (TH.ConT (TH.mkName ('S' : TH.nameBase typeName)))
                                                                       (map (const (TH.ConT ''Integer)) params))])
  
           undefSig  = TH.SigD nm (TH.ForallT [] [] (TH.VarT aVar))
           undefBody = TH.FunD nm [TH.Clause [] (TH.NormalB body) []]
  
       pure $ ds ++ [undefSig, 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 (tnm, ts) cnms = do add True (tnm, ts)
                                  mapM_  (add False) cnms
     where add True  (cnm, cs) = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc cnm) $ "Symbolic version of the type '"        ++ cs ++ "'."
           add False (cnm, cs) = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc cnm) $ "Symbolic version of the constructor '" ++ cs ++ "'."
  #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 what tnm = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc tnm) what
  #else
  addDoc _ _ = pure ()
  #endif
  
  -- | Symbolic version of a type
  mkSBV :: TH.Type -> TH.Type
  mkSBV a = TH.ConT ''SBV `TH.AppT` a
  
  -- | Saturate the type with its parameters
  saturate :: TH.Type -> [TH.Name] -> TH.Type
  saturate t ps = foldr (\p b -> TH.AppT b (TH.VarT p)) t (reverse 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 typeName params cstrs = do
  
      let typeCon = saturate (TH.ConT typeName) params
          sType   = mkSBV typeCon
  
          inSymValContext = TH.ForallT [] [TH.AppT (TH.ConT ''SymVal) (TH.VarT n) | n <- params]
  
          isEnum = case adtKind of
                    ADTUninterpreted -> False
                    ADTEnum          -> True
                    ADTFull          -> False
  
      litFun <- case adtKind of
                  ADTUninterpreted -> do noLit <- [| error $ unlines [ "Data.SBV: unexpected call to derived literal implementation"
                                                                     , "***"
                                                                     , "*** Type: " ++ show typeName
                                                                     , ""
                                                                     , "***Please report this as a bug!"
                                                                     ]
                                                  |]
                                         pure $ TH.FunD 'literal [TH.Clause [TH.WildP] (TH.NormalB noLit) []]
  
                  ADTEnum          -> let mkLitClause n = TH.clause [TH.conP n []]
                                                                    (TH.normalB [| let k = kindOf $(TH.conE n)
                                                                                   in SBV $ SVal k (Left (CV k (CADT (TH.nameBase n, []))))
                                                                                |])
                                                                    []
                                      in TH.FunD 'literal <$> mapM (mkLitClause . fst) cstrs
  
                  ADTFull          -> let mkLitClause (n, fs) = do as <- mapM (const (TH.newName "a")) fs
                                                                   let cn      = TH.mkName $ 's' : TH.nameBase n
                                                                       app a b = TH.AppE a (TH.AppE (TH.VarE 'literal) b)
                                                                   pure $ TH.Clause [TH.ConP n [] (map TH.VarP as)]
                                                                                    (TH.NormalB (foldl app (TH.VarE cn) (map TH.VarE as)))
                                                                                    []
                                      in TH.FunD 'literal <$> mapM mkLitClause cstrs
  
      fromCVFunName <- TH.newName ("cv2" ++ TH.nameBase typeName)
      addDoc ("Conversion from SMT values to " ++ TH.nameBase typeName ++ " values.") fromCVFunName
  
      let fromCVSig = TH.SigD fromCVFunName
                              (inSymValContext (foldr (TH.AppT . TH.AppT TH.ArrowT) typeCon
                                                      [TH.ConT ''String, TH.AppT TH.ListT (TH.ConT ''CV)]))
  
          fromCVCls :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q TH.Clause
          fromCVCls (nm, args) = do
              ns <- mapM (\(i, _) -> TH.newName ("a" ++ show i)) (zip [(1::Int)..] args)
              let pat = foldr ((\p acc -> TH.ConP '(:) [] [p, acc]) . TH.VarP) (TH.ConP '[] [] []) ns
              pure $ TH.Clause [TH.LitP (TH.StringL (TH.nameBase nm)), pat]
                               (TH.NormalB (foldl TH.AppE (TH.ConE nm)
                                                          [TH.AppE (TH.VarE 'fromCV) (TH.VarE n) | n <- ns]))
                               []
  
      catchAll <- do s <- TH.newName "s"
                     l <- TH.newName "l"
                     let errStr   = TH.LitE (TH.StringL ("fromCV " ++ TH.nameBase typeName ++ ": Unexpected constructor/arity: "))
                         tup      = TH.TupE [Just (TH.VarE s), Just (TH.AppE (TH.VarE 'length) (TH.VarE l))]
                         showCall = TH.AppE (TH.VarE 'show) tup
                         errMsg   = TH.InfixE (Just errStr) (TH.VarE '(++)) (Just showCall)
                     pure $ TH.Clause [TH.VarP s, TH.VarP l] (TH.NormalB (TH.AppE (TH.VarE 'error) errMsg)) []
  
      fromCVFun <- do clss <- mapM fromCVCls cstrs
                      pure $ TH.FunD fromCVFunName (clss ++ [catchAll])
  
      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
                                                   -> $(TH.varE fromCVFunName) c (map (uncurry CV) kvs)
                               CV k e -> unexpected $ "Was expecting a CADT value, but got kind: " ++ show k ++ " (rank: " ++ show (cvRank e) ++ ")"
                   |]
  
      symCtx  <- TH.cxt [TH.appT (TH.conT ''SymVal) (TH.varT n) | n <- params]
  
      mmBound <- if isEnum
                    then let universe     = [TH.conE con | (con, _) <- cstrs]
                             (minb, maxb) = case (universe, reverse universe) of
                                               (x:_, y:_) -> (x, y)
                                               _          -> error $ "Impossible: Ran out of elements in determining bounds: " ++ show cstrs
                         in [| Just ($minb, $maxb) |]
                    else [| Nothing |]
  
      let symVal = TH.InstanceD
                        Nothing
                        symCtx
                        (TH.AppT (TH.ConT ''SymVal) typeCon)
                        [ litFun
                        , TH.FunD 'minMaxBound [TH.Clause [] (TH.NormalB mmBound)   []]
                        , TH.FunD 'fromCV      [TH.Clause [] (TH.NormalB getFromCV) []]
                         ]
  
      defCstrs <- [| [(unmod n, map (\(_, _, t) -> t) ntks) | (n, ntks) <- cstrs] |]
  
      kindCtx <- TH.cxt [TH.appT (TH.conT ''HasKind) (TH.varT p) | p <- params]
  
      let mkPair a b = TH.TupE [Just a, Just b]
          kindDef = foldl1 TH.AppE [ TH.ConE 'KADT
                                   , TH.LitE (TH.StringL (unmod typeName))
                                   , TH.ListE [ mkPair (TH.LitE (TH.StringL (TH.nameBase p)))
                                                       (TH.AppE (TH.VarE 'kindOf) (TH.AppTypeE (TH.ConE 'Proxy) (TH.VarT p)))
                                              | p <- params
                                              ]
                                   , defCstrs
                                   ]
  
          kindDecl = TH.InstanceD
                          Nothing
                          kindCtx
                          (TH.AppT (TH.ConT ''HasKind) typeCon)
                          [TH.FunD 'kindOf [TH.Clause [TH.WildP] (TH.NormalB kindDef) []]]
  
      arbDecl <- if isEnum
                    then let universe  = TH.listE [TH.conE con | (con, _) <- cstrs]
                         in [d|instance Arbitrary $(pure typeCon) where
                                arbitrary = elements $universe
                            |]
                    else [d|instance {-# OVERLAPPABLE #-} Arbitrary $(pure 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.Name, String), [TH.Dec])
          declConstructor (c, ntks) = let ats = map (mkSBV . (\(_, t, _) -> t)) ntks
                                          ty  = inSymValContext $ foldr (TH.AppT . TH.AppT TH.ArrowT) sType ats
                                      in ((nm, bnm), [TH.SigD nm ty, def])
            where bnm  = TH.nameBase c
                  nm   = TH.mkName $ 's' : bnm
                  def  = TH.FunD nm [TH.Clause [] (TH.NormalB body) []]
                  body = TH.AppE (TH.VarE 'mkConstructor) (TH.LitE (TH.StringL bnm))
  
      let (constrNames, cdecls) = unzip $ map declConstructor cstrs
  
      let btname = TH.nameBase typeName
          tname  = TH.mkName ('S' : btname)
          tdecl  = TH.TySynD tname [TH.PlainTV p TH.BndrReq | p <- params] sType
  
      addDeclDocs (tname, btname) constrNames
  
      -- Declare accessors
      let declAccessor :: TH.Name -> (Maybe TH.Name, TH.Type, Kind) -> Int -> [((TH.Name, String), [TH.Dec])]
          declAccessor c (mbUN, ft, _) i = let ty    = inSymValContext $ TH.AppT (TH.AppT TH.ArrowT sType) (mkSBV ft)
                                               def n = TH.FunD n [TH.Clause [] (TH.NormalB body) []]
                                           in ((nm, bnm), [TH.SigD nm ty, def nm])
                                            : case mbUN of
                                               Nothing -> []
                                               Just un -> let sun = TH.mkName $ 's' : TH.nameBase un
                                                          in [((sun, bnm), [TH.SigD sun ty, def sun])]
            where bnm  = TH.nameBase c
                  anm  = "get" ++ bnm ++ "_" ++ show i
                  nm   = TH.mkName anm
                  body = TH.AppE (TH.VarE 'mkConstructor) (TH.LitE (TH.StringL anm))
  
      let (accessorNames, accessorDecls) = unzip $ concat (concat [zipWith (declAccessor c) fs [(1::Int) ..] | (c, fs) <- cstrs])
  
      mapM_ (addDoc "Field accessor function." . fst) accessorNames
  
      testerDecls <- mkTesters sType inSymValContext cstrs
  
      -- Get the case analyzer
      caseSigFuns <- mkCaseAnalyzer adtKind typeName params cstrs
  
      -- Get the induction schema, upto 5 extra args. Only for enums and adts
      indDecs <- do let schemas = mapM (mkInductionSchema typeName params cstrs) [0 .. 5]
                    case adtKind of
                      ADTUninterpreted -> pure []
                      ADTEnum          -> schemas
                      ADTFull          -> schemas
  
      -- If this is an enumeration get EnumSymbolic and OrSymbolic instances
      symEnum <- case adtKind of
                  ADTUninterpreted -> pure []
                  ADTFull          -> pure []
                  ADTEnum          ->
                    let universe  = TH.listE [TH.conE                          con   | (con, _) <- cstrs]
                        universeS = TH.listE [TH.litE (TH.stringL (TH.nameBase con)) | (con, _) <- cstrs]
                    in [d| instance SatModel $(TH.conT typeName) where
                             parseCVs (CV _ (CADT (s, [])) : r)
                               | Just v <- s `lookup` zip $universeS $universe
                               = Just (v, r)
                             parseCVs _ = Nothing
  
                           instance SL.EnumSymbolic $(TH.conT typeName) where
                             succ x = go (zip $universe (drop 1 $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 $universe) $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 $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 $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 $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 $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 $(TH.conT 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
                       |]
  
      pure $  [tdecl, symVal, kindDecl]
           ++ arbDecl
           ++ concat cdecls
           ++ testerDecls
           ++ concat accessorDecls
           ++ symEnum
           ++ [fromCVSig, fromCVFun]
           ++ caseSigFuns
           ++ concat 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 kind typeName params cstrs = case kind of
                                                ADTUninterpreted -> pure [] -- no case analyzer for fully uninterpreted types
                                                ADTEnum          -> mk
                                                ADTFull          -> mk
    where mk = do let typeCon = saturate (TH.ConT typeName) params
                      sType   = mkSBV typeCon
  
                      bnm = TH.nameBase typeName
                      cnm = TH.mkName $ "sCase" ++ bnm
  
                  se   <- TH.newName ('s' : bnm)
                  fs   <- mapM (\(nm, _) -> TH.newName ('f' : TH.nameBase nm)) cstrs
                  res  <- TH.newName "result"
  
                  let def = TH.FunD cnm [TH.Clause (map TH.VarP (se : fs)) (TH.NormalB (iteChain (zipWith (mkCase se) fs cstrs))) []]
  
                      iteChain :: [(TH.Exp, TH.Exp)] -> TH.Exp
                      iteChain []       = error $ unlines [ "Data.SBV.mkADT: Impossible happened!"
                                                          , ""
                                                          , "   Received an empty list for: " ++ show typeName
                                                          , ""
                                                          , "While building the case-analyzer."
                                                          , "Please report this as a bug."
                                                          ]
                      iteChain [(_, l)]        = l
                      iteChain ((t, e) : rest) = foldl TH.AppE (TH.VarE 'ite) [TH.AppE t (TH.VarE se), e, iteChain rest]
  
                      mkCase :: TH.Name -> TH.Name -> (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> (TH.Exp, TH.Exp)
                      mkCase cexpr func (c, fields) = (TH.VarE (TH.mkName ("is" ++ TH.nameBase c)), foldl TH.AppE (TH.VarE func) args)
                         where getters = [TH.mkName ("get" ++ TH.nameBase c ++ "_" ++ show i) | (i, _) <- zip [(1 :: Int) ..] fields]
                               args    = map (\g -> TH.AppE (TH.VarE g) (TH.VarE cexpr)) getters
  
                      rvar   = TH.VarT res
                      mkFun  = foldr (TH.AppT . TH.AppT TH.ArrowT) rvar
                      fTypes = [mkFun (map (mkSBV . (\(_, t, _) -> t)) ftks) | (_, ftks) <- cstrs]
                      sig    = TH.SigD cnm (TH.ForallT []
                                                       (TH.AppT (TH.ConT ''Mergeable) (TH.VarT res)
                                                       : [TH.AppT (TH.ConT ''SymVal) (TH.VarT p) | p <- params]
                                                       )
                                                       (mkFun (sType : fTypes)))
  
                  addDoc ("Case analyzer for the type " ++ bnm ++ ".") cnm
                  pure [sig, def]
  
  -- | Declare testers
  mkTesters :: TH.Type -> (TH.Type -> TH.Type) -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -> TH.Q [TH.Dec]
  mkTesters sType inSymValContext cstrs = do
      let declTester :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> ((TH.Name, String), [TH.Dec])
          declTester (c, _) = let ty = inSymValContext $ TH.AppT (TH.AppT TH.ArrowT sType) (TH.ConT ''SBool)
                              in ((nm, bnm), [TH.SigD nm ty, def])
            where bnm  = TH.nameBase c
                  nm   = TH.mkName $ "is" ++ bnm
                  def  = TH.FunD nm [TH.Clause [] (TH.NormalB body) []]
                  body = TH.AppE (TH.VarE 'mkConstructor) (TH.LitE (TH.StringL ("is-" ++ bnm)))
  
      let (testerNames, testerDecls) = unzip $ map declTester cstrs
  
      mapM_ (addDoc "Field recognizer predicate." . fst) testerNames
  
      pure $ concat 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 = reverse . takeWhile (/= '.') . reverse . 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 typeName = do
          (args, tcs) <- getConstructors typeName
  
          let mk n (mbfn, t) = do k <- expandSyns t >>= toSBV typeName n
                                  pure (mbfn, t, k)
  
          cs <- mapM (\(n, ts) -> (n,) <$> mapM (mk n) ts) tcs
  
          let k | null cs             = ADTUninterpreted
                | all (null . snd) cs = ADTEnum
                | True                = ADTFull
  
          pure (k, args, cs)
  
  bad :: MonadFail m => String -> [String] -> m a
  bad what extras = fail $ unlines $ ("mkSymbolic: " ++ what) : map ("      " ++) extras
  
  report :: String
  report = "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 typeName = do res@(_, cstrs) <- getConstructorsFromType (TH.ConT typeName)
  
                                -- make sure accessors are unique
                                let noDup [] = pure ()
                                    noDup (n:ns)
                                      | n `elem` ns = bad "Unsupported field accessor definition."
                                                          [ "Multiply used: " ++ TH.nameBase n
                                                          , ""
                                                          , "SBV does not support cases where accessor fields are replicated."
                                                          , "Please use each accessor only once."
                                                          ]
                                      | True        = noDup ns
                                noDup [n | (_, fs) <- cstrs, (Just n, _) <- fs]
  
                                pure res
  
    where getConstructorsFromType :: TH.Type -> TH.Q ([TH.Name], [(TH.Name, [(Maybe TH.Name, TH.Type)])])
          getConstructorsFromType ty = do ty' <- expandSyns ty
                                          case headCon ty' of
                                            Just (n, args) -> reifyFromHead n args
                                            Nothing        -> bad "Not a type constructor"
                                                                  [ "Name    : " ++ show typeName
                                                                  , "Type    : " ++ show ty
                                                                  , "Expanded: " ++ show ty'
                                                                  ]
  
          headCon :: TH.Type -> Maybe (TH.Name, [TH.Type])
          headCon = go []
            where go args (TH.ConT n)    = Just (n, reverse args)
                  go args (TH.AppT t a)  = go   (a:args) t
                  go args (TH.SigT t _)  = go      args t
                  go args (TH.ParensT t) = go      args t
                  go _    _              = Nothing
  
          reifyFromHead :: TH.Name -> [TH.Type] -> TH.Q ([TH.Name], [(TH.Name, [(Maybe TH.Name, TH.Type)])])
          reifyFromHead n args = do info <- TH.reify n
                                    case info of
                                      TH.TyConI (TH.DataD    _ _ tvs _ cons _) -> (map tvName tvs,) <$> mapM (expandCon (mkSubst tvs args)) cons
                                      TH.TyConI (TH.NewtypeD _ _ tvs _ con  _) -> (map tvName tvs,) <$> mapM (expandCon (mkSubst tvs args)) [con]
                                      TH.TyConI (TH.TySynD _ tvs rhs)          -> getConstructorsFromType (applySubst (mkSubst tvs args) rhs)
                                      _ -> bad "Unsupported kind"
                                               [ "Type : " ++ show typeName
                                               , "Name : " ++ show n
                                               , "Kind : " ++ show info
                                               ]
  
          onSnd f (a, b) = (a,) <$> f b
  
          expandCon :: [(TH.Name, TH.Type)] -> TH.Con -> TH.Q (TH.Name, [(Maybe TH.Name, TH.Type)])
          expandCon sub (TH.NormalC  n fields)          = (n,) <$> mapM (onSnd (expandSyns . applySubst sub) . (\(   _,t) -> (Nothing, t))) fields
          expandCon sub (TH.RecC     n fields)          = (n,) <$> mapM (onSnd (expandSyns . applySubst sub) . (\(fn,_,t) -> (Just fn, t))) fields
          expandCon sub (TH.InfixC   (_, t1) n (_, t2)) = (n,) <$> mapM (onSnd (expandSyns . applySubst sub)) [(Nothing, t1), (Nothing, 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 _   c                               = bad "Unsupported constructor form: "
                                                              [ "Type       : " ++ show typeName
                                                              , "Constructor: " ++ show c
                                                              , ""
                                                              , report
                                                              ]
  
          tvName :: TH.TyVarBndr TH.BndrVis -> TH.Name
          tvName (TH.PlainTV  n _)   = n
          tvName (TH.KindedTV n _ _) = n
  
          -- | Make substitution from type variables to actual args
          mkSubst :: [TH.TyVarBndr TH.BndrVis] -> [TH.Type] -> [(TH.Name, TH.Type)]
          mkSubst tvs = zip (map tvName tvs)
  
          -- | Apply substitution to a Type
          applySubst :: [(TH.Name, TH.Type)] -> TH.Type -> TH.Type
          applySubst sub = go
            where go (TH.VarT    n)        = fromMaybe  (TH.VarT n) (n `lookup` sub)
                  go (TH.AppT    t1 t2)    = TH.AppT    (go t1) (go t2)
                  go (TH.SigT    t k)      = TH.SigT    (go t)  k
                  go (TH.ParensT t)        = TH.ParensT (go t)
                  go (TH.InfixT  t1 n t2)  = TH.InfixT  (go t1) n (go t2)
                  go (TH.UInfixT t1 n t2)  = TH.UInfixT (go t1) n (go t2)
                  go (TH.ForallT bs ctx t) = TH.ForallT bs (map goPred ctx) (go t)
                  go t                     = t
  
                  goPred (TH.AppT t1 t2) = TH.AppT (go t1) (go t2)
                  goPred p               = p
  
  -- | Find the SBV kind for this type
  toSBV :: TH.Name -> TH.Name -> TH.Type -> TH.Q Kind
  toSBV typeName constructorName = go
    where -- Handle type variables (parameters)
          go (TH.VarT v) = pure $ KVar (TH.nameBase v)
  
          -- tuples
          go t | Just ps <- getTuple t = KTuple <$> mapM go ps
  
          -- recognize strings, since we don't (yet) support chars
          go (TH.AppT TH.ListT (TH.ConT t)) | t == ''Char = pure KString
  
          -- lists
          go (TH.AppT TH.ListT t) = KList <$> go t
  
          -- maybe
          go (TH.AppT (TH.ConT nm) t) | nm == ''Maybe = KMaybe <$> go t
  
          -- either
          go (TH.AppT (TH.AppT (TH.ConT nm) t1) t2) | nm == ''Either = KEither <$> go t1 <*> go t2
  
          -- arbitrary words/ints
          go (TH.AppT (TH.ConT nm) (TH.LitT (TH.NumTyLit n)))
              | nm == ''WordN = pure $ KBounded False (fromIntegral n)
              | nm == ''IntN  = pure $ KBounded True  (fromIntegral n)
  
          -- arbitrary floats
          go (TH.AppT (TH.AppT (TH.ConT nm) (TH.LitT (TH.NumTyLit eb))) (TH.LitT (TH.NumTyLit sb)))
              | nm == ''FloatingPoint = pure $ KFP (fromIntegral eb) (fromIntegral sb)
  
          -- Ratio requires extra attention, so ignore
          go (TH.AppT (TH.ConT nm) (TH.ConT i))
              | nm == ''Ratio && i == ''Integer
              = bad "Unsupported Rational type."
                    [ "While SBV supports SRational natively, this type is not yet supported"
                    , "as ADT fields as it needs extra constraints."
                    , ""
                    , "Please report this as a feature request."
                    ]
  
          -- deal with base types
          go t@(TH.ConT constr)
              | Just base <- getBase constr
              = case base of
                  Left (w, r) -> bad w $ [ "Datatype   : " ++ show typeName
                                         , "Constructor: " ++ show constructorName
                                         , "Kind       : " ++ show t
                                         , ""
                                         ] ++ r
                  Right k     -> pure k
  
          -- deal with constructors
          go t
             | Just (c, ps) <- getConApp t
             = KApp (TH.nameBase c) <$> mapM go ps
  
          -- giving up
          go t = bad "Unsupported constructor kind" [ "Datatype   : " ++ TH.nameBase typeName
                                                    , "Constructor: " ++ TH.nameBase constructorName
                                                    , "Kind       : " ++ show t
                                                    , ""
                                                    , report
                                                    ]
  
          -- Extract application of a constructor to some type-variables
          getConApp t = locate t []
            where locate (TH.ConT c)     sofar = Just (c, sofar)
                  locate (TH.AppT l arg) sofar = locate l (arg : sofar)
                  locate _               _     = Nothing
  
          -- Extract an N-tuple
          getTuple = tup []
            where tup sofar (TH.TupleT _) = Just sofar
                  tup sofar (TH.AppT t p) = tup (p : sofar) t
                  tup _     _             = 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 t
            | t == ''Bool     = Just $ Right KBool
            | t == ''Integer  = Just $ Right KUnbounded
            | t == ''Float    = Just $ Right KFloat
            | t == ''Double   = Just $ Right KDouble
            | t == ''String   = Just $ Right KString
            | t == ''AlgReal  = Just $ Right KReal
            | t == ''Word8    = Just $ Right $ KBounded False  8
            | t == ''Word16   = Just $ Right $ KBounded False 16
            | t == ''Word32   = Just $ Right $ KBounded False 32
            | t == ''Word64   = Just $ Right $ KBounded False 64
            | t == ''Int8     = Just $ Right $ KBounded True   8
            | t == ''Int16    = Just $ Right $ KBounded True  16
            | t == ''Int32    = Just $ Right $ KBounded True  32
            | t == ''Int64    = Just $ Right $ KBounded True  64
  
            -- Platform specific, flag:
            |    t == ''Int
              || t == ''Word  = Just $ Left ( "Platform specific type: " ++ show t
                                            , [ "Please pick a more specific type, such as"
                                              , "Integer, Word8, WordN 32, IntN 16 etc."
                                              ])
  
            -- Punt on char and rational. Because SMTLib's string translation requires us to put extra constraints.
            -- We'll do that when we get there.
            |    t == ''Char
              || t == ''Rational = Just $ Left ( "Unsupported base type for ADTs: " ++ show t
                                               , [ "While SBV supports SChar, and SRational natively,"
                                                 , "they are not yet supported as ADT fields as they need extra constraints."
                                                 , ""
                                                 , "Please report this as a feature request."
                                                 ])
  
            -- Otherwise, can't translate
            | True            = 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 typeName params cstrs extraArgCnt = do
     let btype = TH.nameBase typeName
         nm    = "induct" ++ btype ++ if extraArgCnt == 0 then "" else show extraArgCnt
  
     pf <- TH.newName "pf"
  
     extraNames <- mapM (const (TH.newName "extraN")) [0 .. extraArgCnt-1]
     extraSyms  <- mapM (const (TH.newName "extraS")) [0 .. extraArgCnt-1]
     extraTypes <- mapM (const (TH.newName "extraT")) [0 .. extraArgCnt-1]
  
     let mkLam as = TH.lamE (map (\a -> TH.conP 'Forall [TH.varP a]) (as ++ extraNames))
  
     let mkIndCase :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q TH.Exp
         mkIndCase (cstr, flds)
           | null flds && null extraNames
           = [| $(TH.varE pf) $(scstr) |]
           | True
           = do as <- mapM (const (TH.newName "a")) flds
                let -- When can we have the inductive hypothesis?
                    --  (1) same type
                    --  (2) applied at exactly the same types
                    isRecursive (_, _, k) = case k of
                                              KApp t ps -> t == btype && ps == map (KVar . TH.nameBase) params
                                              _         -> False
                    recFields = [a | (a, f) <- zip as flds, isRecursive f]
                TH.appE (TH.varE 'quantifiedBool)
                        (mkLam as (mkImp recFields (foldl TH.appE
                                                          (TH.appE (TH.varE pf) (foldl TH.appE scstr (map TH.varE as)))
                                                          (map TH.varE extraNames))))
           where cnm   = TH.nameBase cstr
                 scstr = TH.varE (TH.mkName ('s' : cnm))
  
                 mkImp []  e = e
                 mkImp [i] e = foldl1 TH.appE [TH.varE '(.=>), assume i, e]
                 mkImp is  e = foldl1 TH.appE [TH.varE '(.=>), foldl1 TH.appE [TH.varE 'sAnd, TH.listE (map assume is)], e]
  
                 assume :: TH.Name -> TH.Q TH.Exp
                 assume n = foldl TH.appE (TH.varE pf) (map TH.varE (n : extraNames))
  
     cases <- mapM mkIndCase cstrs
     post  <- do a <- TH.newName "recVal"
                 TH.appE (TH.varE 'quantifiedBool)
                         (mkLam [a] $ foldl TH.appE (TH.varE pf) (map TH.varE (a : extraNames)))
  
     propName <- TH.newName "prop"
     argName  <- TH.newName "a"
     taName   <- TH.newName "ta"
  
     let pre    = foldl1 TH.AppE [TH.VarE 'sAnd,  TH.ListE cases]
         schema = foldl1 TH.AppE [TH.VarE '(.=>), pre, post]
         ihB    = TH.AppE (TH.VarE 'proofOf) (foldl1 TH.AppE [TH.VarE 'internalAxiom, TH.LitE (TH.StringL nm), schema])
  
         instHead = TH.AppT (TH.ConT ''HasInductionSchema)
                            (foldr (TH.AppT . TH.AppT TH.ArrowT)
                                   (TH.ConT ''SBool)
                                   [  TH.AppT (TH.ConT ''Forall) (TH.VarT es) `TH.AppT` et
                                    | (es, et) <- zip (taName : extraSyms)
                                                      (saturate (TH.ConT typeName) params : map TH.VarT extraTypes)
                                   ])
  
         pfFun = TH.FunD pf [TH.Clause (map TH.VarP (argName : extraNames))
                                       (TH.NormalB (foldl TH.AppE
                                                          (TH.VarE propName)
                                                          [TH.AppE (TH.ConE 'Forall) (TH.VarE a) | a <- argName : extraNames]))
                                       []
                            ]
  
         method = TH.FunD 'inductionSchema
                          [TH.Clause [TH.VarP propName]
                                     (TH.NormalB (TH.LetE [pfFun] ihB))
                                     []
                          ]
  
     context <- TH.cxt [TH.appT (TH.conT ''SymVal) (TH.varT n) | n <- params ++ extraTypes]
  
     pure [TH.InstanceD Nothing context instHead [method]]
  