----------------------------------------------------------------------------- -- | -- 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 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 -- 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 [| return () |] 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 (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.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) 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 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]]