Safe Haskell	Safe-Infered

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

Documentation

data GhcSpec Source

The following is the overall type for specifications obtained from parsing the target source and dependent libraries

Constructors

SP

Fields

tySigs :: ![(Var, SpecType)]: Asserted/Assumed Reftypes eg. see include/Prelude.spec
ctor :: ![(Var, SpecType)]: Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) }
meas :: ![(Symbol, RefType)]: Measure Types eg. len :: [a] -> Int
invariants :: ![SpecType]: Data Type Invariants eg. forall a. {v: [a] | len(v) >= 0}
dconsP :: ![(DataCon, DataConP)]: Predicated Data-Constructors e.g. see testsposMap.hs
tconsP :: ![(TyCon, TyConP)]: Predicated Type-Constructors eg. see testsposMap.hs
freeSyms :: ![(Symbol, Var)]: List of Symbol free in spec and corresponding GHC var eg. (Cons, Cons#7uz) from testsposex1.hs
tcEmbeds :: TCEmb TyCon: How to embed GHC Tycons into fixpoint sorts

Instances

Outputable GhcSpec

makeGhcSpec :: [Var] -> HscEnv -> Spec BareType Symbol -> IO GhcSpec Source