| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Bare
Description
This module contains the functions that convert from descriptions of
symbols, names and types (over freshly parsed bare Strings),
to representations connected to GHC Vars, Names, and Types.
The actual representations of bare and real (refinement) types are all
in RefType -- they are different instances of RType.
Synopsis
- makeTargetSpec :: Config -> LogicMap -> TargetSrc -> BareSpec -> TargetDependencies -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
- loadLiftedSpec :: Config -> FilePath -> IO (Maybe BareSpec)
- saveLiftedSpec :: FilePath -> BareSpec -> IO ()
Creating a TargetSpec
Liquid Haskell operates on TargetSpecs, so this module provides a single function called
makeTargetSpec to produce a TargetSpec, alongside the LiftedSpec. The former will be used by
functions like liquid or liquidOne to verify our program is correct, the latter will be serialised
to disk so that we can retrieve it later without having to re-check the relevant Haskell file.
makeTargetSpec :: Config -> LogicMap -> TargetSrc -> BareSpec -> TargetDependencies -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec) Source #
makeTargetSpec constructs the TargetSpec and then validates it. Upon success, the TargetSpec
and the LiftedSpec are returned. We perform error checking in "two phases": during the first phase,
we check for errors and warnings in the input BareSpec and the dependencies. During this phase we ideally
want to short-circuit in case the validation failure is found in one of the dependencies (to avoid
printing potentially endless failures).
The second phase involves creating the TargetSpec, and returning either the full list of diagnostics
(errors and warnings) in case things went wrong, or the final TargetSpec and LiftedSpec together
with a list of Warnings, which shouldn't abort the compilation (modulo explicit request from the user,
to treat warnings and errors).