Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Haskell.Liquid.Measure

Contents

Specifications
Type Aliases
Constructors

Synopsis

data Spec ty bndr = Spec {
- measures :: ![Measure ty bndr]
- impSigs :: ![(Symbol, Sort)]
- expSigs :: ![(Symbol, Sort)]
- asmSigs :: ![(LocSymbol, ty)]
- sigs :: ![(LocSymbol, ty)]
- localSigs :: ![(LocSymbol, ty)]
- reflSigs :: ![(LocSymbol, ty)]
- invariants :: ![(Maybe LocSymbol, ty)]
- ialiases :: ![(ty, ty)]
- imports :: ![Symbol]
- dataDecls :: ![DataDecl]
- newtyDecls :: ![DataDecl]
- includes :: ![FilePath]
- aliases :: ![Located (RTAlias Symbol BareType)]
- ealiases :: ![Located (RTAlias Symbol Expr)]
- embeds :: !(TCEmb LocSymbol)
- qualifiers :: ![Qualifier]
- lvars :: !(HashSet LocSymbol)
- lazy :: !(HashSet LocSymbol)
- rewrites :: !(HashSet LocSymbol)
- rewriteWith :: !(HashMap LocSymbol [LocSymbol])
- fails :: !(HashSet LocSymbol)
- reflects :: !(HashSet LocSymbol)
- autois :: !(HashMap LocSymbol (Maybe Int))
- hmeas :: !(HashSet LocSymbol)
- hbounds :: !(HashSet LocSymbol)
- inlines :: !(HashSet LocSymbol)
- ignores :: !(HashSet LocSymbol)
- autosize :: !(HashSet LocSymbol)
- pragmas :: ![Located String]
- cmeasures :: ![Measure ty ()]
- imeasures :: ![Measure ty bndr]
- classes :: ![RClass ty]
- claws :: ![RClass ty]
- relational :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
- asmRel :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
- termexprs :: ![(LocSymbol, [Located Expr])]
- rinstance :: ![RInstance ty]
- ilaws :: ![RILaws ty]
- dvariance :: ![(LocSymbol, [Variance])]
- dsize :: ![([ty], LocSymbol)]
- bounds :: !(RRBEnv ty)
- defs :: !(HashMap LocSymbol Symbol)
- axeqs :: ![Equation]
}
data MSpec ty ctor = MSpec {
- ctorMap :: HashMap Symbol [Def ty ctor]
- measMap :: HashMap LocSymbol (Measure ty ctor)
- cmeasMap :: HashMap LocSymbol (Measure ty ())
- imeas :: ![Measure ty ctor]
}
type BareSpec = Spec LocBareType LocSymbol
type BareMeasure = Measure LocBareType LocSymbol
type SpecMeasure = Measure LocSpecType DataCon
mkM :: LocSymbol -> ty -> [Def ty bndr] -> MeasureKind -> UnSortedExprs -> Measure ty bndr
mkMSpec :: [Measure t LocSymbol] -> [Measure t ()] -> [Measure t LocSymbol] -> MSpec t LocSymbol
mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
dataConTypes :: Bool -> MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)])
defRefType :: Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft
bodyPred :: Expr -> Body -> Expr

Specifications

data Spec ty bndr Source #

A generic Spec type, polymorphic over the inner choice of type and binder.

Constructors

Spec

Fields

measures :: ![Measure ty bndr]
User-defined properties for ADTs
impSigs :: ![(Symbol, Sort)]
Imported variables types
expSigs :: ![(Symbol, Sort)]
Exported variables types
asmSigs :: ![(LocSymbol, ty)]
Assumed (unchecked) types; including reflected signatures
sigs :: ![(LocSymbol, ty)]
Imported functions and types
localSigs :: ![(LocSymbol, ty)]
Local type signatures
reflSigs :: ![(LocSymbol, ty)]
Reflected type signatures
invariants :: ![(Maybe LocSymbol, ty)]
Data type invariants; the Maybe is the generating measure
ialiases :: ![(ty, ty)]
Data type invariants to be checked
imports :: ![Symbol]
Loaded spec module names
dataDecls :: ![DataDecl]
Predicated data definitions
newtyDecls :: ![DataDecl]
Predicated new type definitions
includes :: ![FilePath]
Included qualifier files
aliases :: ![Located (RTAlias Symbol BareType)]
RefType aliases
ealiases :: ![Located (RTAlias Symbol Expr)]
Expression aliases
embeds :: !(TCEmb LocSymbol)
GHC-Tycon-to-fixpoint Tycon map
qualifiers :: ![Qualifier]
Qualifiers in source/spec files
lvars :: !(HashSet LocSymbol)
Variables that should be checked in the environment they are used
lazy :: !(HashSet LocSymbol)
Ignore Termination Check in these Functions
rewrites :: !(HashSet LocSymbol)
Theorems turned into rewrite rules
rewriteWith :: !(HashMap LocSymbol [LocSymbol])
Definitions using rewrite rules
fails :: !(HashSet LocSymbol)
These Functions should be unsafe
reflects :: !(HashSet LocSymbol)
Binders to reflect
autois :: !(HashMap LocSymbol (Maybe Int))
Automatically instantiate axioms in these Functions with maybe specified fuel
hmeas :: !(HashSet LocSymbol)
Binders to turn into measures using haskell definitions
hbounds :: !(HashSet LocSymbol)
Binders to turn into bounds using haskell definitions
inlines :: !(HashSet LocSymbol)
Binders to turn into logic inline using haskell definitions
ignores :: !(HashSet LocSymbol)
Binders to ignore during checking; that is DON't check the corebind.
autosize :: !(HashSet LocSymbol)
Type Constructors that get automatically sizing info
pragmas :: ![Located String]
Command-line configurations passed in through source
cmeasures :: ![Measure ty ()]
Measures attached to a type-class
imeasures :: ![Measure ty bndr]
Mappings from (measure,type) -> measure
classes :: ![RClass ty]
Refined Type-Classes
claws :: ![RClass ty]
Refined Type-Classe Laws
relational :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Relational types
asmRel :: ![(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Assumed relational types
termexprs :: ![(LocSymbol, [Located Expr])]
Terminating Conditions for functions
rinstance :: ![RInstance ty]
ilaws :: ![RILaws ty]
dvariance :: ![(LocSymbol, [Variance])]
TODO ? Where do these come from ?!
dsize :: ![([ty], LocSymbol)]
Size measure to enforce fancy termination
bounds :: !(RRBEnv ty)
defs :: !(HashMap LocSymbol Symbol)
Temporary (?) hack to deal with dictionaries in specifications see testsposNatClass.hs
axeqs :: ![Equation]
Equalities used for Proof-By-Evaluation

Instances

Instances details

Qualify ModSpecs Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> ModSpecs -> ModSpecs Source #
Qualify BareSpec Source #
Instance details Defined in Language.Haskell.Liquid.Bare.Resolve Methods qualify :: Env -> ModName -> SourcePos -> [Symbol] -> BareSpec -> BareSpec Source #
Monoid (Spec ty bndr) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods mempty :: Spec ty bndr # mappend :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr # mconcat :: [Spec ty bndr] -> Spec ty bndr #
Semigroup (Spec ty bndr) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods (<>) :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr # sconcat :: NonEmpty (Spec ty bndr) -> Spec ty bndr # stimes :: Integral b => b -> Spec ty bndr -> Spec ty bndr #
Generic (Spec ty bndr) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Associated Types type Rep (Spec ty bndr) :: Type -> Type # Methods from :: Spec ty bndr -> Rep (Spec ty bndr) x # to :: Rep (Spec ty bndr) x -> Spec ty bndr #
(PPrint ty, PPrint bndr, Show ty) => Show (Spec ty bndr) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods showsPrec :: Int -> Spec ty bndr -> ShowS # show :: Spec ty bndr -> String # showList :: [Spec ty bndr] -> ShowS #
Binary (Spec LocBareType LocSymbol) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods put :: Spec LocBareType LocSymbol -> Put # get :: Get (Spec LocBareType LocSymbol) # putList :: [Spec LocBareType LocSymbol] -> Put #
(Show ty, Show bndr, PPrint ty, PPrint bndr) => PPrint (Spec ty bndr) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods pprintTidy :: Tidy -> Spec ty bndr -> Doc # pprintPrec :: Int -> Tidy -> Spec ty bndr -> Doc #
type Rep (Spec ty bndr) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Specs type Rep (Spec ty bndr) = D1 ('MetaData "Spec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "Spec" 'PrefixI 'True) (((((S1 ('MetaSel ('Just "measures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty bndr]) :: S1 ('MetaSel ('Just "impSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)])) :: (S1 ('MetaSel ('Just "expSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :: (S1 ('MetaSel ('Just "asmSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :: S1 ('MetaSel ('Just "sigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)])))) :: ((S1 ('MetaSel ('Just "localSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :: (S1 ('MetaSel ('Just "reflSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :: S1 ('MetaSel ('Just "invariants") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Maybe LocSymbol, ty)]))) :: (S1 ('MetaSel ('Just "ialiases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(ty, ty)]) :: (S1 ('MetaSel ('Just "imports") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Symbol]) :: S1 ('MetaSel ('Just "dataDecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]))))) :: (((S1 ('MetaSel ('Just "newtyDecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]) :: S1 ('MetaSel ('Just "includes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [FilePath])) :: (S1 ('MetaSel ('Just "aliases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (RTAlias Symbol BareType)]) :: (S1 ('MetaSel ('Just "ealiases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (RTAlias Symbol Expr)]) :: S1 ('MetaSel ('Just "embeds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (TCEmb LocSymbol))))) :: ((S1 ('MetaSel ('Just "qualifiers") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Qualifier]) :: (S1 ('MetaSel ('Just "lvars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "lazy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)))) :: (S1 ('MetaSel ('Just "rewrites") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: (S1 ('MetaSel ('Just "rewriteWith") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol [LocSymbol])) :: S1 ('MetaSel ('Just "fails") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))))))) :: ((((S1 ('MetaSel ('Just "reflects") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "autois") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol (Maybe Int)))) :: (S1 ('MetaSel ('Just "hmeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: (S1 ('MetaSel ('Just "hbounds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "inlines") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))))) :: ((S1 ('MetaSel ('Just "ignores") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: (S1 ('MetaSel ('Just "autosize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :: S1 ('MetaSel ('Just "pragmas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located String]))) :: (S1 ('MetaSel ('Just "cmeasures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ()]) :: (S1 ('MetaSel ('Just "imeasures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty bndr]) :: S1 ('MetaSel ('Just "classes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RClass ty]))))) :: (((S1 ('MetaSel ('Just "claws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RClass ty]) :: S1 ('MetaSel ('Just "relational") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)])) :: (S1 ('MetaSel ('Just "asmRel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]) :: (S1 ('MetaSel ('Just "termexprs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Located Expr])]) :: S1 ('MetaSel ('Just "rinstance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RInstance ty])))) :: ((S1 ('MetaSel ('Just "ilaws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RILaws ty]) :: (S1 ('MetaSel ('Just "dvariance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Variance])]) :: S1 ('MetaSel ('Just "dsize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [([ty], LocSymbol)]))) :: (S1 ('MetaSel ('Just "bounds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (RRBEnv ty)) :: (S1 ('MetaSel ('Just "defs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol Symbol)) :*: S1 ('MetaSel ('Just "axeqs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation]))))))))

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

Instances details

Bifunctor MSpec Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods bimap :: (a -> b) -> (c -> d) -> MSpec a c -> MSpec b d # first :: (a -> b) -> MSpec a c -> MSpec b c # second :: (b -> c) -> MSpec a b -> MSpec a c #
Functor (MSpec ty) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods fmap :: (a -> b) -> MSpec ty a -> MSpec ty b # (<$) :: a -> MSpec ty b -> MSpec ty a #
(Data ty, Data ctor) => Data (MSpec ty ctor) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MSpec ty ctor -> c (MSpec ty ctor) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MSpec ty ctor) # toConstr :: MSpec ty ctor -> Constr # dataTypeOf :: MSpec ty ctor -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (MSpec ty ctor)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (MSpec ty ctor)) # gmapT :: (forall b. Data b => b -> b) -> MSpec ty ctor -> MSpec ty ctor # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r # gmapQ :: (forall d. Data d => d -> u) -> MSpec ty ctor -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MSpec ty ctor -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #
Eq ctor => Monoid (MSpec ty ctor) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods mempty :: MSpec ty ctor # mappend :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor # mconcat :: [MSpec ty ctor] -> MSpec ty ctor #
Eq ctor => Semigroup (MSpec ty ctor) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods (<>) :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor # sconcat :: NonEmpty (MSpec ty ctor) -> MSpec ty ctor # stimes :: Integral b => b -> MSpec ty ctor -> MSpec ty ctor #
Generic (MSpec ty ctor) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Associated Types type Rep (MSpec ty ctor) :: Type -> Type # Methods from :: MSpec ty ctor -> Rep (MSpec ty ctor) x # to :: Rep (MSpec ty ctor) x -> MSpec ty ctor #
(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods showsPrec :: Int -> MSpec ty ctor -> ShowS # show :: MSpec ty ctor -> String # showList :: [MSpec ty ctor] -> ShowS #
(PPrint t, PPrint a) => PPrint (MSpec t a) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types Methods pprintTidy :: Tidy -> MSpec t a -> Doc # pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #
type Rep (MSpec ty ctor) Source #
Instance details Defined in Language.Haskell.Liquid.Types.Types type Rep (MSpec ty ctor)

Type Aliases

type BareSpec = Spec LocBareType LocSymbol Source #

type BareMeasure = Measure LocBareType LocSymbol Source #

type SpecMeasure = Measure LocSpecType DataCon Source #

Constructors

mkM :: LocSymbol -> ty -> [Def ty bndr] -> MeasureKind -> UnSortedExprs -> Measure ty bndr Source #

mkMSpec :: [Measure t LocSymbol] -> [Measure t ()] -> [Measure t LocSymbol] -> MSpec t LocSymbol Source #

mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor Source #

dataConTypes :: Bool -> MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)]) Source #

defRefType :: Bool -> Type -> Def (RRType Reft) DataCon -> RRType Reft Source #

bodyPred :: Expr -> Body -> Expr Source #