Language.Haskell.Liquid.Bare

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.

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)

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).

Loading and Saving lifted specs from/to disk

loadLiftedSpec :: Config -> FilePath -> IO (Maybe BareSpec)

De/Serializing Spec files

saveLiftedSpec :: FilePath -> BareSpec -> IO ()