target-0.2.0.1: Generate test-suites from refinement types.

Safe HaskellNone
LanguageHaskell2010

Test.Target.Util

Documentation

type Depth = Int Source

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

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

reft :: SpecType -> Reft Source

data HList a where Source

Constructors

Nil :: HList [] 
(:::) :: a -> HList bs -> HList (a : bs) 

Instances

AllHave * Show as => Show (HList as) 

type family Map f xs :: [b] Source

Equations

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

type family Constraints cs :: Constraint Source

Instances

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

type AllHave c xs = Constraints (Map c xs) Source

type family Args a Source

Equations

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

type family Res a Source

Equations

Res (a -> b) = Res b 
Res a = a 

smt2Sort :: Sort -> Text Source

makeDecl :: Symbol -> Sort -> Text Source

safeFromJust :: String -> Maybe a -> a Source

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

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

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

stripQuals :: SpecType -> SpecType Source

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

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

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

loadModule :: FilePath -> Ghc ModSummary Source