Safe Haskell | None |
---|---|
Language | Haskell98 |
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.
Containing Constraints
Invoke Solver on an FInfo
solve :: Config -> FInfo a -> IO (Result a) Source
Solve FInfo system of horn-clause constraints ------------------------
Invoke Solver on a .fq file
solveFQ :: Config -> IO ExitCode Source
Solve .fq File -------------------------------------------------------
Function to determine outcome
resultExit :: FixResult a -> ExitCode Source
Parse Qualifiers from File
parseFInfo :: [FilePath] -> IO (FInfo a) Source
Parse External Qualifiers --------------------------------------------