sbv-14.1: Data/SBV/Client.hs
-----------------------------------------------------------------------------
-- |
-- 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 -Wno-orphans #-}
module Data.SBV.Client
( sbvCheckSolverInstallation
, defaultSolverConfig
, getAvailableSolvers
, mkSymbolic
, getConstructors
) where
import Data.SBV.Core.TH (getConstructors, bad, report)
import Data.Generics
import Control.Monad (filterM, mapAndUnzipM, zipWithM)
import Test.QuickCheck (Arbitrary(..), elements)
import qualified Control.Exception as C
import Data.Char
import Data.Word
import Data.Int
import Data.Ratio
import qualified "template-haskell" Language.Haskell.TH as TH
import qualified "template-haskell" Language.Haskell.TH.Syntax as TH
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 cfg = check `C.catch` (\(_ :: C.SomeException) -> pure False)
where check = do ThmResult r <- proveWith cfg $ \x -> sNot (sNot x) .== (x :: SBool)
case r of
Unsatisfiable{} -> pure True
_ -> pure 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 ()
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 t'" ++ cs ++ "'."
add False (cnm, cs) = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc cnm) $ "Symbolic version of the constructor v'" ++ cs ++ "'."
-- | Add document to a generated function
addDoc :: String -> TH.Name -> TH.Q ()
addDoc what tnm = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc tnm) what
-- | 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
-- 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 (n, fs) = do
as <- mapM (const (TH.newName "a")) fs
inp <- TH.newName "inp"
c <- TH.newName "c"
let app a b = [| $a (literal $b) |]
TH.clause [TH.asP inp (TH.conP n (map TH.varP as))]
(TH.normalB
(TH.caseE [| sequenceA $(TH.listE [ [| unlitCV (literal $(TH.varE a)) |] | a <- as ]) |]
[ TH.match [p|Just $(TH.varP c)|]
(TH.normalB [| let k = kindOf $(TH.varE inp)
in SBV $ SVal k (Left (CV k (CADT (TH.nameBase n, $(TH.varE c)))))
|])
[]
, TH.match [p|Nothing|]
(TH.normalB (foldl app (TH.varE (TH.mkName ('s' : TH.nameBase n))) (map TH.varE as)))
[]
]))
[]
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 -> TH.FunD 'literal <$> mapM mkLitClause cstrs
ADTFull -> 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 |]
-- make the initializer to get the subtypes registered
st <- TH.newName "_st" -- Get an underscored name here, since st might go unused if there're no subtypes
register <- do let concretize b@TH.ConT{} = b
concretize TH.VarT{} = TH.ConT ''Integer
concretize (TH.AppT l arg) = TH.AppT (concretize l) (concretize arg)
concretize r = r
end <- TH.noBindS [| pure () |]
pure $ TH.DoE Nothing $ [TH.NoBindS (TH.AppE (TH.AppE (TH.VarE 'registerKind) (TH.VarE st))
(TH.AppE (TH.VarE 'kindOf)
(TH.AppTypeE (TH.ConE 'Proxy) (concretize t))))
| (_, fts) <- cstrs, (_, t, KApp n _) <- fts, n /= TH.nameBase typeName
] ++ [end]
let regFun = TH.FunD 'mkSymValInit [TH.Clause [TH.VarP st, TH.WildP] (TH.NormalB register) []]
let symVal = TH.InstanceD
Nothing
symCtx
(TH.AppT (TH.ConT ''SymVal) typeCon)
[ litFun
, regFun
, 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) []]]
hasArbitrary <- TH.isInstance ''Arbitrary [typeCon]
arbDecl <- case () of
() | hasArbitrary -> pure []
| isEnum -> let universe = TH.listE [TH.conE con | (con, _) <- cstrs]
in [d|instance Arbitrary $(pure typeCon) where
arbitrary = elements $universe
|]
| True -> [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.Q ((TH.Name, String), [TH.Dec])
declConstructor (n, ntks) = do
let ats = map (mkSBV . (\(_, t, _) -> t)) ntks
ty = inSymValContext $ foldr (TH.AppT . TH.AppT TH.ArrowT) sType ats
bnm = TH.nameBase n
nm = TH.mkName $ 's' : bnm
as <- mapM (const (TH.newName "a")) ntks
c <- TH.newName "c"
cls <- TH.clause (map TH.varP as)
(TH.normalB
(TH.caseE [| sequenceA $(TH.listE [ [| unlitCV $(TH.varE a) |] | a <- as ]) |]
[ TH.match [p|Just $(TH.varP c)|]
(TH.normalB [| let k = kindOf (undefined `asTypeOf` res)
res = SBV $ SVal k (Left (CV k (CADT (bnm, $(TH.varE c)))))
in res
|])
[]
, TH.match [p|Nothing|]
(TH.normalB (foldl (\a b -> [| $a $b |]) [| mkADTConstructor bnm |] (map TH.varE as)))
[]
]))
[]
pure ((nm, bnm), [TH.SigD nm ty, TH.FunD nm [cls]])
(constrNames, cdecls) <- mapAndUnzipM 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 -- NB. field count starts at 1!
declAccessor :: TH.Name -> (Maybe TH.Name, TH.Type, Kind) -> Int -> TH.Q [((TH.Name, String), [TH.Dec])]
declAccessor c (mbUN, ft, _) i = do
let bnm = TH.nameBase c
anm = "get" ++ bnm ++ "_" ++ show i
nm = TH.mkName anm
ty = inSymValContext $ TH.AppT (TH.AppT TH.ArrowT sType) (mkSBV ft)
cls <- do inp <- TH.newName "inp"
TH.clause [TH.varP inp]
(TH.normalB
(TH.caseE [| unlitCV $(TH.varE inp) |]
[ TH.match [p|Just (_, CADT (got, kv))|]
(TH.guardedB [do g <- TH.normalG [| got == bnm |]
e <- [| let (k, v) = (kv !! (i-1))
in SBV $ SVal k (Left (CV k v))
|]
pure (g, e)
])
[]
, TH.match [p|_|]
(TH.normalB [| mkADTAccessor anm $(TH.varE inp) |])
[]
]))
[]
-- If there's a custom accessor given, declare that here too
extras <- case mbUN of
Nothing -> pure []
Just un -> do let sun = TH.mkName $ 's' : TH.nameBase un
pure [((sun, bnm), [TH.SigD sun ty, TH.FunD sun [cls]])]
pure $ ((nm, bnm), [TH.SigD nm ty, TH.FunD nm [cls]]) : extras
allDefs <- sequence [zipWithM (declAccessor c) fs [(1::Int) ..] | (c, fs) <- cstrs]
let (accessorNames, accessorDecls) = unzip $ concat (concat allDefs)
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 (fs ++ [se])) (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 (fTypes ++ [sType])))
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.Q ((TH.Name, String), [TH.Dec])
declTester (c, _) = do
let ty = inSymValContext $ TH.AppT (TH.AppT TH.ArrowT sType) (TH.ConT ''SBool)
bnm = TH.nameBase c
nm = TH.mkName $ "is" ++ bnm
inp <- TH.newName "inp"
cls <- TH.clause [TH.varP inp]
(TH.normalB
(TH.caseE [| unlitCV $(TH.varE inp) |]
[ TH.match [p|Just (_, CADT (got, _))|]
(TH.normalB [| literal (got == bnm) |])
[]
, TH.match [p|Nothing|]
(TH.normalB [| mkADTTester ("is-" ++ bnm) $(TH.varE inp) |])
[]
]))
[]
pure ((nm, bnm), [TH.SigD nm ty, TH.FunD nm [cls]])
(testerNames, testerDecls) <- mapAndUnzipM 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)
-- | Find the SBV kind for this type
toSBV :: TH.Name -> TH.Name -> TH.Type -> TH.Q Kind
toSBV typeName constructorName = go
where hasArrows (TH.AppT TH.ArrowT _) = True
hasArrows (TH.AppT lhs rhs) = hasArrows lhs || hasArrows rhs
hasArrows _ = False
-- 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
-- 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)
-- Rational
go (TH.AppT (TH.ConT nm) (TH.ConT i))
| nm == ''Ratio && i == ''Integer
= pure KRational
-- 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 : " ++ TH.pprint 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 : " ++ TH.pprint t
, ""
, if hasArrows t
then "Higher order fields (i.e., function values) are not supported."
else 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 == ''Char = Just $ Right KChar
| t == ''String = Just $ Right KString
| t == ''AlgReal = Just $ Right KReal
| t == ''Rational = Just $ Right KRational
| 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."
])
-- 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 = TH.lamE . map (\a -> TH.conP 'Forall [TH.varP a])
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 ++ extraNames)
(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
lcnm = map toLower cnm
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 = do en <- mapM (const (TH.newName (lcnm ++ "_extraN"))) [0 .. extraArgCnt-1]
TH.appE (TH.varE 'quantifiedBool)
(mkLam en (foldl TH.appE (TH.varE pf) (map TH.varE (n : en))))
cases <- mapM mkIndCase cstrs
post <- do a <- TH.newName "recVal"
TH.appE (TH.varE 'quantifiedBool)
(mkLam (a : extraNames) $ 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]]