liquidhaskell-0.6.0.0: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Types

Contents

Description

This module should contain all the global type definitions and basic instances.

Synopsis

Options

data Config Source

Constructors

Config 

Fields

files :: [FilePath]

source files to check

idirs :: [FilePath]

path to directory for including specs

newcheck :: Bool

new liquid-fixpoint sort check

diffcheck :: Bool

check subset of binders modified (+ dependencies) since last check

linear :: Bool

uninterpreted integer multiplication and division

higherorder :: Bool

allow higher order binders into the logic

fullcheck :: Bool

check all binders (overrides diffcheck)

saveQuery :: Bool

save fixpoint query

binders :: [String]

set of binders to check

noCheckUnknown :: Bool

whether to complain about specifications for unexported and unused values

notermination :: Bool

disable termination check

autoproofs :: Bool

automatically construct proofs from axioms

nowarnings :: Bool

disable warnings output (only show errors)

trustinternals :: Bool

type all internal variables with true

nocaseexpand :: Bool

disable case expand

strata :: Bool

enable strata analysis

notruetypes :: Bool

disable truing top level types

totality :: Bool

check totality in definitions

noPrune :: Bool

disable prunning unsorted Refinements

cores :: Maybe Int

number of cores used to solve constraints

minPartSize :: Int

Minimum size of a partition

maxPartSize :: Int

Maximum size of a partition. Overrides minPartSize

maxParams :: Int

the maximum number of parameters to accept when mining qualifiers

smtsolver :: Maybe SMTSolver

name of smtsolver to use [default: try z3, cvc4, mathsat in order]

shortNames :: Bool

drop module qualifers from pretty-printed names.

shortErrors :: Bool

don't show subtyping errors and contexts.

cabalDir :: Bool

find and use .cabal file to include paths to sources for imported modules

ghcOptions :: [String]

command-line options to pass to GHC

cFiles :: [String]

.c files to compile and link against (for GHC)

eliminate :: Bool
 
port :: Int

port at which lhi should listen

exactDC :: Bool

Automatically generate singleton types for data constructors

scrapeImports :: Bool

scrape qualifiers from imported specifications

scrapeUsedImports :: Bool

scrape qualifiers from used, imported specifications

elimStats :: Bool

print eliminate stats

Instances

class HasConfig t where Source

Methods

getConfig :: t -> Config Source

Instances

hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool Source

Ghc Information

data GhcInfo Source

GHC Information : Code & Spec ------------------------------

Constructors

GI 

Fields

target :: !FilePath
 
env :: !HscEnv
 
cbs :: ![CoreBind]
 
derVars :: ![Var]
 
impVars :: ![Var]
 
defVars :: ![Var]
 
useVars :: ![Var]
 
hqFiles :: ![FilePath]
 
imports :: ![String]
 
includes :: ![FilePath]
 
spec :: !GhcSpec
 

Instances

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, Located SpecType)]

Asserted Reftypes eg. see include/Prelude.spec

asmSigs :: ![(Var, Located SpecType)]

Assumed Reftypes

inSigs :: ![(Var, Located SpecType)]

Auto generated Signatures

ctors :: ![(Var, Located SpecType)]

Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) }

meas :: ![(Symbol, Located SpecType)]

Measure Types eg. len :: [a] -> Int

invariants :: ![Located SpecType]

Data Type Invariants eg. forall a. {v: [a] | len(v) >= 0}

ialiases :: ![(Located SpecType, Located SpecType)]

Data Type Invariant Aliases

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 e.g. "embed Set as Set_set" from includeDataSet.spec

qualifiers :: ![Qualifier]

Qualifiers in Source/Spec files e.g testsposqualTest.hs

tgtVars :: ![Var]

Top-level Binders To Verify (empty means ALL binders)

decr :: ![(Var, [Int])]

Lexicographically ordered size witnesses for termination

texprs :: ![(Var, [Expr])]

Lexicographically ordered expressions for termination

lvars :: !(HashSet Var)

Variables that should be checked in the environment they are used

lazy :: !(HashSet Var)

Binders to IGNORE during termination checking

autosize :: !(HashSet TyCon)

Binders to IGNORE during termination checking

config :: !Config

Configuration Options

exports :: !NameSet

Names exported by the module being verified

measures :: [Measure SpecType DataCon]
 
tyconEnv :: HashMap TyCon RTyCon
 
dicts :: DEnv Var SpecType

Dictionary Environment

axioms :: [HAxiom]
 
logicMap :: LogicMap
 
proofType :: Maybe Type
 

Instances

data TargetVars Source

Which Top-Level Binders Should be Verified

Constructors

AllVars 
Only ![Var] 

Located Things

data Located a :: * -> *

Constructors

Loc 

Fields

loc :: !SourcePos

Start Position

locE :: !SourcePos

End Position

val :: a
 

Instances

Functor Located 
Foldable Located 
Traversable Located 
TyConable LocSymbol Source 
Resolvable LocSymbol Source 
Eq a => Eq (Located a) 
Data a => Data (Located a) 
Ord a => Ord (Located a) 
Show a => Show (Located a) 
IsString a => IsString (Located a) 
Generic (Located a) 
Binary a => Binary (Located a) 
NFData a => NFData (Located a) 
Hashable a => Hashable (Located a) 
Expression a => Expression (Located a) 
Subable a => Subable (Located a) 
Symbolic a => Symbolic (Located a) 
Loc (Located a) 
Fixpoint a => Fixpoint (Located a) 
PPrint a => PPrint (Located a) 
GhcLookup (Located Symbol) Source 
type Rep (Located a) = D1 D1Located (C1 C1_0Located ((:*:) (S1 S1_0_0Located (Rec0 SourcePos)) ((:*:) (S1 S1_0_1Located (Rec0 SourcePos)) (S1 S1_0_2Located (Rec0 a))))) 

dummyLoc :: a -> Located a

Symbols

type LocSymbol = Located Symbol

Located Symbols -----------------------------------------------------

type LocText = Located Text

Default unknown name

dummyName :: Symbol

isDummy :: Symbolic a => a -> Bool

Refined Type Constructors

data RTyCon Source

Constructors

RTyCon TyCon ![RPVar] !TyConInfo 

Instances

data TyConInfo Source

Co- and Contra-variance for TyCon --------------------------------

Indexes start from 0 and type or predicate arguments can be both covariant and contravaariant e.g., for the below Foo dataType

data Foo a b c d :: b - Prop, q :: Int -> Prop, r :: a -> Prop> = F (ar -> bp) | Q (c -> a) | G (Intq -> ar)

there will be:

varianceTyArgs = [Bivariant , Covariant, Contravatiant, Invariant] variancePsArgs = [Covariant, Contravatiant, Bivariant]

Constructors

TyConInfo 

Fields

varianceTyArgs :: !VarianceInfo

variance info for type variables

variancePsArgs :: !VarianceInfo

variance info for predicate variables

sizeFunction :: !(Maybe (Symbol -> Expr))

logical function that computes the size of the structure

Instances

defaultTyConInfo :: TyConInfo Source

rTyConPVs :: RTyCon -> [RPVar] Source

rTyConPropVs :: RTyCon -> [PVar RSort] Source

isClassRTyCon :: RTyCon -> Bool Source

Accessors for RTyCon

isClassType :: TyConable c => RType c t t1 -> Bool Source

isEqType :: TyConable c => RType c t t1 -> Bool Source

Refinement Types

data RType c tv r Source

Constructors

RVar 

Fields

rt_var :: !tv
 
rt_reft :: !r
 
RFun 

Fields

rt_bind :: !Symbol
 
rt_in :: !(RType c tv r)
 
rt_out :: !(RType c tv r)
 
rt_reft :: !r
 
RAllT 

Fields

rt_tvbind :: !tv
 
rt_ty :: !(RType c tv r)
 
RAllP 

Fields

rt_pvbind :: !(PVar (RType c tv ()))
 
rt_ty :: !(RType c tv r)
 
RAllS 

Fields

rt_sbind :: !Symbol
 
rt_ty :: !(RType c tv r)
 
RApp 

Fields

rt_tycon :: !c
 
rt_args :: ![RType c tv r]
 
rt_pargs :: ![RTProp c tv r]
 
rt_reft :: !r
 
RAllE 

Fields

rt_bind :: !Symbol
 
rt_allarg :: !(RType c tv r)
 
rt_ty :: !(RType c tv r)
 
REx 

Fields

rt_bind :: !Symbol
 
rt_exarg :: !(RType c tv r)
 
rt_ty :: !(RType c tv r)
 
RExprArg (Located Expr)

For expression arguments to type aliases see testsposvector2.hs

RAppTy 

Fields

rt_arg :: !(RType c tv r)
 
rt_res :: !(RType c tv r)
 
rt_reft :: !r
 
RRTy 

Fields

rt_env :: ![(Symbol, RType c tv r)]
 
rt_ref :: !r
 
rt_obl :: !Oblig
 
rt_ty :: !(RType c tv r)
 
RHole r

let LH match against the Haskell type and add k-vars, e.g. `x:_` see testsposHoles.hs

Instances

data Ref τ t Source

Ref describes `Prop τ` and HProp arguments applied to type constructors. For example, in [a]- v > h}>, we apply (via RApp) * the RProp denoted by `{h -> v > h}` to * the RTyCon denoted by `[]`. Thus, Ref is used for abstract-predicate (arguments) that are associated with _type constructors_ i.e. whose semantics are _dependent upon_ the data-type. In contrast, the Predicate argument in ur_pred in the UReft applies directly to any type and has semantics _independent of_ the data-type.

Constructors

RProp 

Fields

rf_args :: [(Symbol, τ)]
 
rf_body :: t

Abstract refinement associated with RTyCon

Instances

Functor (Ref τ) Source 
(Data τ, Data t) => Data (Ref τ t) Source 
Generic (Ref τ t) Source 
(NFData τ, NFData t) => NFData (Ref τ t) Source 
(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source 
(Reftable r, RefTypable c tv r) => Subable (RTProp c tv r) Source 
type Rep (Ref τ t) Source 

type RTProp c tv r = Ref (RType c tv ()) (RType c tv r) Source

RTProp is a convenient alias for Ref that will save a bunch of typing. In general, perhaps we need not expose Ref directly at all.

rPropP :: [(Symbol, τ)] -> r -> Ref τ (RType c tv r) Source

newtype RTyVar Source

Constructors

RTV TyVar 

Instances

data RTAlias tv ty Source

Refinement Type Aliases

Constructors

RTA 

Fields

rtName :: Symbol
 
rtTArgs :: [tv]
 
rtVArgs :: [tv]
 
rtBody :: ty
 
rtPos :: SourcePos
 
rtPosE :: SourcePos
 

Worlds

data HSeg t Source

Constructors

HBind 

Fields

hs_addr :: !Symbol
 
hs_val :: t
 
HVar UsedPVar 

Instances

Data t => Data (HSeg t) Source 
Generic (HSeg t) Source 
type Rep (HSeg t) Source 

newtype World t Source

A World is a Separation Logic predicate that is essentially a sequence of binders that satisfies two invariants (TODO:LIQUID): 1. Each `hs_addr :: Symbol` appears at most once, 2. There is at most one HVar in a list.

Constructors

World [HSeg t] 

Instances

Data t => Data (World t) Source 
Generic (World t) Source 
type Rep (World t) Source 

Classes describing operations on RTypes

class Eq c => TyConable c where Source

Minimal complete definition

isFun, isList, isTuple, ppTycon

Methods

isFun :: c -> Bool Source

isList :: c -> Bool Source

isTuple :: c -> Bool Source

ppTycon :: c -> Doc Source

isClass :: c -> Bool Source

isEqual :: c -> Bool Source

isNumCls :: c -> Bool Source

isFracCls :: c -> Bool Source

Instances

TyConable Symbol Source 
TyConable LocSymbol Source 
TyConable RTyCon Source

TyConable Instances -------------------------------------------------------

class (TyConable c, Eq c, Eq tv, Hashable tv, Reftable r, PPrint r) => RefTypable c tv r where Source

Methods

ppRType :: Prec -> RType c tv r -> Doc Source

class SubsTy tv ty a where Source

Methods

subt :: (tv, ty) -> a -> a Source

Predicate Variables

data PVar t Source

Abstract Predicate Variables ----------------------------------

Constructors

PV 

Fields

pname :: !Symbol
 
ptype :: !(PVKind t)
 
parg :: !Symbol
 
pargs :: ![(t, Symbol, Expr)]
 

Instances

isPropPV :: PVar t -> Bool Source

pvType :: PVar t -> t Source

data PVKind t Source

Constructors

PVProp t 
PVHProp 

Instances

newtype Predicate Source

Constructors

Pr [UsedPVar] 

Instances

Refinements

data UReft r Source

Constructors

MkUReft 

Fields

ur_reft :: !r
 
ur_pred :: !Predicate
 
ur_strata :: !Strata
 

Instances

Parse-time entities describing refined data types

data DataDecl Source

Values Related to Specifications ------------------------------------

Data type refinements

Constructors

D 

Fields

tycName :: LocSymbol

Type Constructor Name

tycTyVars :: [Symbol]

Tyvar Parameters

tycPVars :: [PVar BSort]

PVar Parameters

tycTyLabs :: [Symbol]

PLabel Parameters

tycDCons :: [(LocSymbol, [(Symbol, BareType)])]
DataCon, [(fieldName, fieldType)
]
tycSrcPos :: !SourcePos

Source Position

tycSFun :: Maybe (Symbol -> Expr)

Measure that should decrease in recursive calls

Instances

data DataConP Source

Constructors

DataConP 

Fields

dc_loc :: !SourcePos
 
freeTyVars :: ![RTyVar]
 
freePred :: ![PVar RSort]
 
freeLabels :: ![Symbol]
 
tyConsts :: ![SpecType]
 
tyArgs :: ![(Symbol, SpecType)]
 
tyRes :: !SpecType
 
dc_locE :: !SourcePos
 

Instances

data TyConP Source

Constructors

TyConP 

Fields

freeTyVarsTy :: ![RTyVar]
 
freePredTy :: ![PVar RSort]
 
freeLabelTy :: ![Symbol]
 
varianceTs :: !VarianceInfo
 
variancePs :: !VarianceInfo
 
sizeFun :: !(Maybe (Symbol -> Expr))
 

Instances

Pre-instantiated RType

type RRType = RType RTyCon RTyVar Source

type BRType = RType LocSymbol Symbol Source

type RRProp r = Ref RSort (RRType r) Source

type BSort = BRType () Source

type BPVar = PVar BSort Source

Instantiated RType

type BareType = BRType RReft Source

type PrType = RRType Predicate Source

type SpecType = RRType RReft Source

type SpecProp = RRProp RReft Source

type RSort = RRType () Source

type UsedPVar = PVar () Source

type RPVar = PVar RSort Source

type RReft = UReft Reft Source

data REnv Source

The type used during constraint generation, used also to define contexts for errors, hence in this file, and NOT in elsewhere. **DO NOT ATTEMPT TO MOVE** Am splitting into + global : many bindings, shared across all constraints + local : few bindings, relevant to particular constraints

Constructors

REnv 

Fields

reGlobal :: HashMap Symbol SpecType

the "global" names for module

reLocal :: HashMap Symbol SpecType

the "local" names for sub-exprs

Instances

Constructing & Destructing RTypes

data RTypeRep c tv r Source

Constructor and Destructors for RTypes ----------------------------

Constructors

RTypeRep 

Fields

ty_vars :: [tv]
 
ty_preds :: [PVar (RType c tv ())]
 
ty_labels :: [Symbol]
 
ty_binds :: [Symbol]
 
ty_refts :: [r]
 
ty_args :: [RType c tv r]
 
ty_res :: RType c tv r
 

fromRTypeRep :: RTypeRep c tv r -> RType c tv r Source

toRTypeRep :: RType c tv r -> RTypeRep c tv r Source

mkArrow :: (Foldable t, Foldable t1, Foldable t2, Foldable t3) => t tv -> t1 (PVar (RType c tv ())) -> t2 Symbol -> t3 (Symbol, RType c tv r, r) -> RType c tv r -> RType c tv r Source

bkArrowDeep :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a) Source

bkArrow :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a) Source

safeBkArrow :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a) Source

mkUnivs :: (Foldable t, Foldable t1, Foldable t2) => t tv -> t1 (PVar (RType c tv ())) -> t2 Symbol -> RType c tv r -> RType c tv r Source

bkUniv :: RType t1 a t2 -> ([a], [PVar (RType t1 a ())], [Symbol], RType t1 a t2) Source

bkClass :: TyConable c => RType c tv r -> ([(c, [RType c tv r])], RType c tv r) Source

rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r Source

rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r Source

rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r Source

Manipulating Predicates

pvars :: Predicate -> [UsedPVar] Source

pappSym :: Show a => a -> Symbol Source

pApp :: Symbol -> [Expr] -> Expr Source

Some tests on RTypes

isBase :: RType t t1 t2 -> Bool Source

isFunTy :: RType t t1 t2 -> Bool Source

isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool Source

Traversing RType

efoldReft :: (Reftable r, TyConable c) => (c -> [RType c tv r] -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b Source

foldReft :: (Reftable r, TyConable c) => (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source

foldReft' :: (Reftable r, TyConable c) => (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source

mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2 Source

mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2) Source

mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r Source

mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r Source

???

data Oblig Source

Different kinds of Check Obligations ------------------------------------

Constructors

OTerm

Obligation that proves termination

OInv

Obligation that proves invariants

OCons

Obligation that proves subtyping constraints

Instances

ignoreOblig :: RType t t1 t2 -> RType t t1 t2 Source

addInvCond :: SpecType -> RReft -> SpecType Source

Inferred Annotations

newtype AnnInfo a Source

Annotations -------------------------------------------------------

Constructors

AI (HashMap SrcSpan [(Maybe Text, a)]) 

Instances

data Annot t Source

Constructors

AnnUse t 
AnnDef t 
AnnRDf t 
AnnLoc SrcSpan 

Instances

Overall Output

data Output a Source

Output --------------------------------------------------------------------

Constructors

O 

Fields

o_vars :: Maybe [String]
 
o_errors :: ![UserError]
 
o_types :: !(AnnInfo a)
 
o_templs :: !(AnnInfo a)
 
o_bots :: ![SrcSpan]
 
o_result :: ErrorResult
 

Instances

Refinement Hole

hole :: Expr Source

isHole :: Expr -> Bool Source

hasHole :: Reftable r => r -> Bool Source

Converting To and From Sort

ofRSort :: Reftable r => RType c tv () -> RType c tv r Source

toRSort :: RType c tv r -> RType c tv () Source

rTypeValueVar :: Reftable r => RType c tv r -> Symbol Source

rTypeReft :: Reftable r => RType c tv r -> Reft Source

stripRTypeBase :: RType t t1 a -> Maybe a Source

Class for values that can be pretty printed

class PPrint a where

Implement either pprintTidy or pprintPrec

Minimal complete definition

Nothing

Methods

pprintTidy :: Tidy -> a -> Doc

pprintPrec :: Int -> Tidy -> a -> Doc

Instances

pprint :: PPrint a => a -> Doc

Top-level pretty printer

showpp :: PPrint a => a -> String

Printer Configuration

data PPEnv Source

Printer ----------------------------------------------------------------

Constructors

PP 

Fields

ppPs :: Bool
 
ppTyVar :: Bool
 
ppSs :: Bool
 
ppShort :: Bool
 

ppEnv :: PPEnv Source

ppEnvShort :: PPEnv -> PPEnv Source

Modules and Imports

data ModName Source

Constructors

ModName !ModType !ModuleName 

Instances

data ModType Source

Constructors

Target 
SrcImport 
SpecImport 

Instances

isSrcImport :: ModName -> Bool Source

isSpecImport :: ModName -> Bool Source

getModName :: ModName -> ModuleName Source

getModString :: ModName -> String Source

Refinement Type Aliases

data RTEnv Source

Constructors

RTE 

Fields

typeAliases :: HashMap Symbol (RTAlias RTyVar SpecType)
 
exprAliases :: HashMap Symbol (RTAlias Symbol Expr)
 

Instances

mapRT :: (HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias RTyVar SpecType)) -> RTEnv -> RTEnv Source

mapRE :: (HashMap Symbol (RTAlias Symbol Expr) -> HashMap Symbol (RTAlias Symbol Expr)) -> RTEnv -> RTEnv Source

Errors and Error Messages

module Language.Haskell.Liquid.Types.Errors

type Error = TError SpecType Source

type ErrorResult = FixResult UserError Source

Error Data Type ---------------------------------------------------

Source information (associated with constraints)

data Cinfo Source

Source Information Associated With Constraints --------------------

Constructors

Ci 

Fields

ci_loc :: !SrcSpan
 
ci_err :: !(Maybe Error)
 

Instances

Measures

data Measure ty ctor Source

Constructors

M 

Fields

name :: LocSymbol
 
sort :: ty
 
eqns :: [Def ty ctor]
 

Instances

Bifunctor Measure Source 
Functor (Measure ty) Source 
(Data ty, Data ctor) => Data (Measure ty ctor) Source 
PPrint (Measure t a) => Show (Measure t a) Source 
Generic (Measure ty ctor) Source 
Subable (Measure ty ctor) Source 
(PPrint t, PPrint a) => PPrint (Measure t a) Source 
Transformable (Measure t c) Source 
type Rep (Measure ty ctor) Source 

data CMeasure ty Source

Constructors

CM 

Fields

cName :: LocSymbol
 
cSort :: ty
 

Instances

data Def ty ctor Source

Constructors

Def 

Fields

measure :: LocSymbol
 
dparams :: [(Symbol, ty)]
 
ctor :: ctor
 
dsort :: Maybe ty
 
binds :: [(Symbol, Maybe ty)]
 
body :: Body
 

Instances

Bifunctor Def Source 
Functor (Def ty) Source 
(Eq ty, Eq ctor) => Eq (Def ty ctor) Source 
(Data ty, Data ctor) => Data (Def ty ctor) Source 
(Show ty, Show ctor) => Show (Def ty ctor) Source 
Generic (Def ty ctor) Source 
Subable (Def ty ctor) Source 
PPrint a => PPrint (Def t a) Source 
Transformable (Def t c) Source 
type Rep (Def ty ctor) Source 

data Body Source

Constructors

E Expr

Measure Refinement: {v | v = e }

P Expr

Measure Refinement: {v | (? v) = p }

R Symbol Expr

Measure Refinement: {v | p}

Instances

data MSpec ty ctor Source

Constructors

MSpec 

Fields

ctorMap :: HashMap Symbol [Def ty ctor]
 
measMap :: HashMap LocSymbol (Measure ty ctor)
 
cmeasMap :: HashMap LocSymbol (Measure ty ())
 
imeas :: ![Measure ty ctor]
 

Instances

Bifunctor MSpec Source 
Functor (MSpec ty) Source 
(Data ty, Data ctor) => Data (MSpec ty ctor) Source 
(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source 
Generic (MSpec ty ctor) Source 
Eq ctor => Monoid (MSpec ty ctor) Source 
(PPrint t, PPrint a) => PPrint (MSpec t a) Source 
type Rep (MSpec ty ctor) Source 

Type Classes

data RClass ty Source

Constructors

RClass 

Fields

rcName :: LocSymbol
 
rcSupers :: [ty]
 
rcTyVars :: [Symbol]
 
rcMethods :: [(LocSymbol, ty)]
 

Instances

KV Profiling

data KVKind Source

KVar Profile --------------------------------------------------------------

Constructors

RecBindE 
NonRecBindE 
TypeInstE 
PredInstE 
LamE 
CaseE 
LetE 

Instances

data KVProf Source

Instances

emptyKVProf :: KVProf Source

updKVProf :: KVKind -> Kuts -> KVProf -> KVProf Source

Misc

mapRTAVars :: (a -> tv) -> RTAlias a ty -> RTAlias tv ty Source

insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a Source

Strata

data Stratum Source

Constructors

SVar Symbol 
SDiv 
SWhnf 
SFin 

Instances

type Strata = [Stratum] Source

isSVar :: Stratum -> Bool Source

getStrata :: RType t t1 (UReft r) -> [Stratum] Source

makeDivType :: SpecType -> SpecType Source

makeFinType :: SpecType -> SpecType Source

CoreToLogic

data LogicMap Source

Constructors

LM 

Fields

logic_map :: HashMap Symbol LMap
 
axiom_map :: HashMap Var Symbol
 

Instances

toLogicMap :: [(Symbol, [Symbol], Expr)] -> LogicMap Source

eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr Source

data LMap Source

Constructors

LMap 

Fields

lvar :: Symbol
 
largs :: [Symbol]
 
lexpr :: Expr
 

Instances

Refined Instances

type RDEnv = DEnv Var SpecType Source

newtype DEnv x ty Source

Constructors

DEnv (HashMap x (HashMap Symbol ty)) 

Instances

(Eq x, Hashable x) => Monoid (DEnv x ty) Source 

data RInstance t Source

Refined Instances ---------------------------------------------------

Constructors

RI 

Fields

riclass :: LocSymbol
 
ritype :: t
 
risigs :: [(LocSymbol, t)]
 

Instances

Ureftable Instances

class Reftable r => UReftable r where Source

Minimal complete definition

Nothing

Methods

ofUReft :: UReft Reft -> r Source

Instances

String Literals

liquidBegin :: String Source

liquidEnd :: String Source

data Axiom b s e Source

Values Related to Specifications ------------------------------------

Constructors

Axiom 

Fields

aname :: (Var, Maybe DataCon)
 
abinds :: [b]
 
atypes :: [s]
 
alhs :: e
 
arhs :: e
 

Instances

type HAxiom = Axiom Var Type CoreExpr Source

type LAxiom = Axiom Symbol Sort Expr Source