Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Synthesize.Generate

Synopsis

genTerms :: SpecType -> SM [CoreExpr]
data SearchMode
- = ArgsMode
- | ResultMode
genTerms' :: SearchMode -> SpecType -> SM [CoreExpr]
genArgs :: SpecType -> SM [CoreExpr]
withDepthFillArgs :: SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
argsFill :: ExprMemory -> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
withDepthFill :: SearchMode -> SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr]
fill :: SearchMode -> Int -> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr]
type Depth = Int
feasible :: Depth -> (CoreExpr, Int) -> Bool
feasibles :: Depth -> Int -> [(CoreExpr, Int)] -> [Int]
isFeasible :: Depth -> [[(CoreExpr, Int)]] -> [[Int]]
findFeasibles :: Depth -> [[(CoreExpr, Int)]] -> ([[Int]], [Int])
toExpr :: [Int] -> [(CoreExpr, Int)] -> ([(CoreExpr, Int)], [(CoreExpr, Int)])
fixCands :: Int -> [Int] -> [[(CoreExpr, Int)]] -> ([[(CoreExpr, Int)]], [[(CoreExpr, Int)]])
replace :: Int -> a -> [a] -> [a]
repeatFix :: [Int] -> [[Int]] -> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> [CoreExpr] -> SM [CoreExpr]
prune :: Depth -> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
fillOne :: (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr]
applyTerm :: [CoreExpr] -> [(CoreExpr, Int)] -> Type -> SM [CoreExpr]
applyArg :: [CoreExpr] -> (CoreExpr, Int) -> Type -> SM [CoreExpr]
applyTerms :: [CoreExpr] -> [[(CoreExpr, Int)]] -> [Type] -> SM [CoreExpr]
prodScrutinees :: [(Type, CoreExpr, Int)] -> [[[(CoreExpr, Int)]]] -> SM [CoreExpr]
synthesizeScrutinee :: [Var] -> SM [CoreExpr]

Documentation

genTerms :: SpecType -> SM [CoreExpr] #

data SearchMode #

Constructors

ArgsMode	searching for arguments of functions that can eventually produce the top level hole fill
ResultMode	searching for the hole fill

Instances

Instances details

Eq SearchMode #
Instance details Defined in Language.Haskell.Liquid.Synthesize.Generate Methods (==) :: SearchMode -> SearchMode -> Bool # (/=) :: SearchMode -> SearchMode -> Bool #
Show SearchMode #
Instance details Defined in Language.Haskell.Liquid.Synthesize.Generate Methods showsPrec :: Int -> SearchMode -> ShowS # show :: SearchMode -> String # showList :: [SearchMode] -> ShowS #

genTerms' :: SearchMode -> SpecType -> SM [CoreExpr] #

genArgs :: SpecType -> SM [CoreExpr] #

withDepthFillArgs :: SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr] #

argsFill :: ExprMemory -> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr] #

withDepthFill :: SearchMode -> SpecType -> Int -> [(Type, CoreExpr, Int)] -> SM [CoreExpr] #

fill :: SearchMode -> Int -> [(Type, CoreExpr, Int)] -> [CoreExpr] -> SM [CoreExpr] #

type Depth = Int #

Pruning terms for function application | --

feasible :: Depth -> (CoreExpr, Int) -> Bool #

feasibles :: Depth -> Int -> [(CoreExpr, Int)] -> [Int] #

isFeasible :: Depth -> [[(CoreExpr, Int)]] -> [[Int]] #

findFeasibles :: Depth -> [[(CoreExpr, Int)]] -> ([[Int]], [Int]) #

toExpr :: [Int] -> [(CoreExpr, Int)] -> ([(CoreExpr, Int)], [(CoreExpr, Int)]) #

fixCands :: Int -> [Int] -> [[(CoreExpr, Int)]] -> ([[(CoreExpr, Int)]], [[(CoreExpr, Int)]]) #

replace :: Int -> a -> [a] -> [a] #

The first argument should be an 1-based index.

repeatFix :: [Int] -> [[Int]] -> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> [CoreExpr] -> SM [CoreExpr] #

prune :: Depth -> (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr] #

fillOne :: (Type, CoreExpr, Int) -> [[(CoreExpr, Int)]] -> SM [CoreExpr] #

applyTerm :: [CoreExpr] -> [(CoreExpr, Int)] -> Type -> SM [CoreExpr] #

applyArg :: [CoreExpr] -> (CoreExpr, Int) -> Type -> SM [CoreExpr] #

applyTerms :: [CoreExpr] -> [[(CoreExpr, Int)]] -> [Type] -> SM [CoreExpr] #

prodScrutinees :: [(Type, CoreExpr, Int)] -> [[[(CoreExpr, Int)]]] -> SM [CoreExpr] #

synthesizeScrutinee :: [Var] -> SM [CoreExpr] #