| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Solver
Description
This module implements the top-level API for interfacing with Fixpoint In particular it exports the functions that solve constraints supplied either as .fq files or as FInfo.
Synopsis
- solve :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
- type Solver a = Config -> FInfo a -> IO (Result (Integer, a))
- solveFQ :: Config -> IO ExitCode
- resultExit :: FixResult a -> ExitCode
- resultExitCode :: Result SubcId -> IO ExitCode
- parseFInfo :: [FilePath] -> IO (FInfo a)
- simplifyFInfo :: (NFData a, Fixpoint a, Show a, Loc a) => Config -> FInfo a -> IO (SInfo a)
Invoke Solver on an FInfo
solve :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a Source #
Solve FInfo system of horn-clause constraints -----------------------------
type Solver a = Config -> FInfo a -> IO (Result (Integer, a)) Source #
Top level Solvers ----------------------------------------------------
Invoke Solver on a .fq file
solveFQ :: Config -> IO ExitCode Source #
Solve an .fq file ----------------------------------------------------
Function to determine outcome
resultExit :: FixResult a -> ExitCode Source #
Parse Qualifiers from File
parseFInfo :: [FilePath] -> IO (FInfo a) Source #
Parse External Qualifiers -------------------------------------------------