Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Constrained.Spec.Map
Contents
Synopsis
- data MapSpec k v = MapSpec {
- mapSpecHint ∷ Maybe Integer
- mapSpecMustKeys ∷ Set k
- mapSpecMustValues ∷ [v]
- mapSpecSize ∷ Specification Integer
- mapSpecElem ∷ Specification (k, v)
- mapSpecFold ∷ FoldSpec v
- defaultMapSpec ∷ Ord k ⇒ MapSpec k v
- fstSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification k
- sndSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification v
- data MapW (dom ∷ [Type]) (rng ∷ Type) where
- DomW ∷ (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) ⇒ MapW '[Map k v] (Set k)
- RngW ∷ (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) ⇒ MapW '[Map k v] [v]
- LookupW ∷ (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) ⇒ MapW '[k, Map k v] (Maybe v)
- mapSem ∷ MapW d r → FunTy d r
- dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k)
- rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v]
- lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v)
Documentation
Constructors
MapSpec | |
Fields
|
Instances
defaultMapSpec ∷ Ord k ⇒ MapSpec k v Source #
emptySpec without all the constraints
fstSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification k Source #
sndSpec ∷ ∀ k v. (HasSpec k, HasSpec v) ⇒ Specification (k, v) → Specification v Source #
data MapW (dom ∷ [Type]) (rng ∷ Type) where Source #
Constructors
DomW ∷ (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) ⇒ MapW '[Map k v] (Set k) | |
RngW ∷ (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) ⇒ MapW '[Map k v] [v] | |
LookupW ∷ (HasSpec k, HasSpec v, IsNormalType k, IsNormalType v, Ord k) ⇒ MapW '[k, Map k v] (Maybe v) |
Instances
Syntax MapW Source # | |
Logic MapW Source # | |
Defined in Constrained.Spec.Map Methods propagateTypeSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires MapW as b, HasSpec a) ⇒ MapW as b → ListCtx Value as (HOLE a) → TypeSpec b → [b] → Specification a Source # propagateMemberSpec ∷ ∀ (as ∷ [Type]) b a. (AppRequires MapW as b, HasSpec a) ⇒ MapW as b → ListCtx Value as (HOLE a) → NonEmpty b → Specification a Source # propagate ∷ ∀ (as ∷ [Type]) b a. (AppRequires MapW as b, HasSpec a) ⇒ MapW as b → ListCtx Value as (HOLE a) → Specification b → Specification a Source # rewriteRules ∷ ∀ (dom ∷ [Type]) rng. (TypeList dom, Typeable dom, HasSpec rng, All HasSpec dom) ⇒ MapW dom rng → List Term dom → Evidence (AppRequires MapW dom rng) → Maybe (Term rng) Source # mapTypeSpec ∷ (HasSpec a, HasSpec b) ⇒ MapW '[a] b → TypeSpec a → Specification b Source # saturate ∷ ∀ (dom ∷ [Type]). MapW dom Bool → List Term dom → [Pred] Source # | |
Semantics MapW Source # | |
Show (MapW d r) Source # | |
Eq (MapW dom rng) Source # | |
dom_ ∷ (HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term (Set k) Source #
rng_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term (Map k v) → Term [v] Source #
lookup_ ∷ (HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) ⇒ Term k → Term (Map k v) → Term (Maybe v) Source #