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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.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

LHs

Literate Haskell source

Js

JavaScript source

Ts

Typescript source

Spec

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

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)

Pred 
PAss 
Dat 
Smt2

SMTLIB2 query file

Instances

Hardwired paths

getFixpointPath :: IO FilePath Source

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

Various generic utility functions for finding and removing files