Language.Haskell.Liquid.Prover.Solve

Documentation

type PrEnv = SEnv SortedReft

solve :: Query a -> IO (Proof a)

notGHCVar :: Show a => a -> Bool

iterativeSolve :: PrEnv -> Int -> Context -> [Ctor a] -> [Expr a] -> Expr -> [Axiom a] -> IO (Proof a)

type Arguments a = [(Sort, [Expr a])]

groupExpressions :: PrEnv -> [Expr a] -> Arguments a

placeExpr :: PrEnv -> Arguments a -> Expr a -> Arguments a

mergeExpressions :: Arguments a -> Arguments a -> Arguments a

placeArg :: [(Sort, [a])] -> (Sort, [a]) -> [(Sort, [a])]

findValid :: Context -> [Instance a] -> Expr -> IO (Maybe [Instance a])

minimize :: Context -> [Instance a] -> Expr -> IO [Instance a]

bruteSearch :: Context -> [Instance a] -> Expr -> IO (Maybe [Instance a])

filterEquivalentExpressions :: PrEnv -> Context -> [Instance a] -> Arguments a -> Arguments a -> IO (Arguments a)

makeEq :: PrEnv -> Expr a -> Expr a -> Maybe Expr

assertExpressions :: PrEnv -> Context -> (Sort, [Expr a]) -> IO ()

predCtor :: SEnv SortedReft -> Ctor a -> [Expr] -> Expr

makeExpressions :: PrEnv -> Context -> [Instance a] -> [Ctor a] -> Arguments a -> IO (Arguments a)

putExpr :: t -> Maybe Sort -> [(Sort, [t])] -> [(Sort, [t])]

makeArguments :: [Sort] -> Arguments a -> [[Expr a]]

makeCTorArgs :: Ctor a -> Arguments a -> [[Expr a]]

applyArguments :: [[a]] -> [[a]]

makeArgumnetsExpr :: Int -> [Expr a] -> [[Expr a]]

arity :: Ctor a -> Int

initExpressions :: [Var a] -> [Expr a]

instantiate :: PrEnv -> Arguments a -> Arguments a -> Axiom a -> [Instance a]

makeArgs' :: Int -> [Expr a] -> [[Expr a]]

duplicateArgs :: t -> t1 -> [t1]

makeArgs :: Int -> [Expr a] -> [[Expr a]]

axiomInstance :: PrEnv -> Axiom a -> [Expr a] -> Maybe (Instance a)

checkExpr :: PrEnv -> Expr a -> Bool

mkcheckExpr :: PrEnv -> Expr a -> Expr

makeSorts :: Query a -> [Sort]

unifiable :: Sort -> Sort -> Bool