| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Solver
Contents
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.
Invoke Solver on an FInfo
solve :: (NFData a, Fixpoint 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
Extract ExitCode from Solver Result ----------------------------------
Parse Qualifiers from File
parseFInfo :: [FilePath] -> IO (FInfo a) Source
Parse External Qualifiers --------------------------------------------