Test.Target.Util

Documentation

type Depth = Int

io :: MonadIO m => IO a -> m a

myTrace :: Show a => String -> a -> a

reft :: SpecType -> Reft

data HList a where

Constructors

Nil :: HList []

(:::) :: a -> HList bs -> HList (a : bs)

Instances

AllHave * Show as => Show (HList as)

type family Map f xs :: [b]

Equations

Map f [] = []

Map f (x : xs) = f x : Map f xs

type family Constraints cs :: Constraint

Instances

type Constraints ([] Constraint) = ()

type Constraints ((:) Constraint c cs) = (c, Constraints cs)

type AllHave c xs = Constraints (Map c xs)

type family Args a

Equations

Args (a -> b) = a : Args b

Args a = []

type family Res a

Equations

Res (a -> b) = Res b

Res a = a

smt2Sort :: Sort -> Text

makeDecl :: Symbol -> Sort -> Text

safeFromJust :: String -> Maybe a -> a

applyPreds :: SpecType -> SpecType -> [(Symbol, SpecType)]

propPsToProp :: [(PVar t3, Ref t (UReft t2) t1)] -> Ref t (UReft t2) t1 -> Ref t (UReft t2) t1

propPToProp :: (PVar t3, Ref t (UReft t2) t1) -> Ref t (UReft t2) t1 -> Ref t (UReft t2) t1

stripQuals :: SpecType -> SpecType

fourth4 :: (t, t1, t2, t3) -> t3

getSpec :: [String] -> FilePath -> IO GhcSpec

runGhc :: [String] -> Ghc a -> IO a

loadModule :: FilePath -> Ghc ModSummary