| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Fixpoint.Utils.Files
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
- data Ext
- extFileName :: Ext -> FilePath -> FilePath
- extFileNameR :: Ext -> FilePath -> FilePath
- tempDirectory :: FilePath -> FilePath
- extModuleName :: String -> Ext -> FilePath
- withExt :: FilePath -> Ext -> FilePath
- isExtFile :: Ext -> FilePath -> Bool
- isBinary :: FilePath -> Bool
- getFixpointPath :: IO FilePath
- getZ3LibPath :: IO FilePath
- getFileInDirs :: FilePath -> [FilePath] -> IO (Maybe FilePath)
- copyFiles :: [FilePath] -> FilePath -> IO ()
Hardwired file extension names
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 |
| HSmt2 | Horn query file |
| Min | filter constraints with delta debug |
| MinQuals | filter qualifiers with delta debug |
| MinKVars | filter kvars with delta debug |
tempDirectory :: FilePath -> FilePath Source #
Hardwired paths
getFixpointPath :: IO FilePath Source #
Hardwired Paths and Files -----------------------------