liquid-fixpoint-0.8.10.1: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Utils.Files

Contents

Description

This module contains Haskell variables representing globally visible names for files, paths, extensions.

Rather than have strings floating around the system, all constant names should be defined here, and the (exported) variables should be used and manipulated elsewhere.

Synopsis

Hardwired file extension names

data Ext Source #

Constructors

Cgi

Constraint Generation Information

Fq

Input to constraint solving (fixpoint)

Out

Output from constraint solving (fixpoint)

Html

HTML file with inferred type annotations

Annot

Text file with inferred types

Vim

Vim annotation file

Hs

Haskell source

HsBoot

Haskell source

LHs

Literate Haskell source

Js

JavaScript source

Ts

Typescript source

Spec

Spec file (e.g. include/Prelude.spec)

BinSpec

Lifted-Spec file, containing automatically generated specifications

Hquals

Qualifiers file (e.g. include/Prelude.hquals)

Result

Final result: SAFE/UNSAFE

Cst

HTML file with templates?

Mkdn

Markdown file (temporarily generated from .Lhs + annots)

Json

JSON file containing result (annots + errors)

Saved

Previous source (for incremental checking)

Cache

Previous output (for incremental checking)

Dot

Constraint Graph

Part Int

Partition

Auto Int

SMTLIB2 queries for automatically created proofs

Pred 
PAss 
Dat 
BinFq

Binary representation of .fq / FInfo

Smt2

SMTLIB2 query file

Min

filter constraints with delta debug

MinQuals

filter qualifiers with delta debug

MinKVars

filter kvars with delta debug

Instances
Eq Ext Source # 
Instance details

Defined in Language.Fixpoint.Utils.Files

Methods

(==) :: Ext -> Ext -> Bool #

(/=) :: Ext -> Ext -> Bool #

Ord Ext Source # 
Instance details

Defined in Language.Fixpoint.Utils.Files

Methods

compare :: Ext -> Ext -> Ordering #

(<) :: Ext -> Ext -> Bool #

(<=) :: Ext -> Ext -> Bool #

(>) :: Ext -> Ext -> Bool #

(>=) :: Ext -> Ext -> Bool #

max :: Ext -> Ext -> Ext #

min :: Ext -> Ext -> Ext #

Show Ext Source # 
Instance details

Defined in Language.Fixpoint.Utils.Files

Methods

showsPrec :: Int -> Ext -> ShowS #

show :: Ext -> String #

showList :: [Ext] -> ShowS #

Hardwired paths

getFixpointPath :: IO FilePath Source #

Hardwired Paths and Files -----------------------------

Various generic utility functions for finding and removing files