Language.Fixpoint.Interface

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

data FInfo a

Constructors

FI (HashMap Integer (SubC a)) ![WfC a] !BindEnv !FEnv ![(Symbol, Sort)] Kuts ![Qualifier]

Instances

Show (FInfo a)

Monoid (FInfo a)

Inputable (FInfo ())

Invoke Solver on an FInfo

solve :: Config -> FInfo a -> IO (Result a)

Solve FInfo system of horn-clause constraints ------------------------

Invoke Solver on a .fq file

solveFQ :: Config -> IO ExitCode

Solve .fq File -------------------------------------------------------

Function to determine outcome

resultExit :: FixResult a -> ExitCode

Parse Qualifiers from File

parseFInfo :: [FilePath] -> IO (FInfo a)

Parse External Qualifiers --------------------------------------------