Language.Fixpoint.Interface

Containing Constraints

data FInfo a

Constructors

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

Instances

Inputable (FInfo ())

Invoke Solver on Set of Constraints

solve :: Config -> FilePath -> [FilePath] -> FInfo a -> IO (FixResult (SubC a), HashMap Symbol Pred)

Solve a system of horn-clause constraints ----------------------------

solveFile :: Config -> IO ExitCode

Function to determine outcome

resultExit :: FixResult t -> ExitCode

Validity Query

checkValid :: Hashable a => a -> [(Symbol, Sort)] -> Pred -> IO (FixResult a)

One Shot validity query ----------------------------------------------