Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data GenericsFn fn args res
- type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a, CountCases a ~ 1)
- fst_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn (a, b) → Term fn a
- snd_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn (a, b) → Term fn b
- pair_ ∷ ∀ fn a b. (HasSpec fn a, HasSpec fn b) ⇒ Term fn a → Term fn b → Term fn (a, b)
- left_ ∷ (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) ⇒ Term fn a → Term fn (Either a b)
- right_ ∷ (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) ⇒ Term fn b → Term fn (Either a b)
- cJust_ ∷ (HasSpec fn a, IsNormalType a) ⇒ Term fn a → Term fn (Maybe a)
- cNothing_ ∷ (HasSpec fn a, IsNormalType a) ⇒ Term fn (Maybe a)
- caseOn ∷ ∀ fn a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term fn a → FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
- branch ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ FunTy (MapList (Term fn) (Args a)) p → Weighted (Binder fn) a
- branchW ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ Int → FunTy (MapList (Term fn) (Args a)) p → Weighted (Binder fn) a
- forAll' ∷ ∀ fn t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) ⇒ Term fn t → FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Pred fn
- constrained' ∷ ∀ a fn p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) ⇒ FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Specification fn a
- reify' ∷ ∀ fn a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec fn b ~ TypeSpec fn (SimpleRep b), HasSpec fn (SimpleRep b), HasSimpleRep b, All (HasSpec fn) (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → FunTy (MapList (Term fn) (Args (SimpleRep b))) p → Pred fn
- con ∷ ∀ c a r fn. (SimpleRep a ~ SOP (TheSop a), TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a, r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a), ResultType r ~ Term fn a, SOPTerm c fn (TheSop a), ConstrTerm fn (ConstrOf c (TheSop a))) ⇒ r
- onCon ∷ ∀ c a fn p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All (HasSpec fn) (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p → Pred fn
- isCon ∷ ∀ c a fn. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → Pred fn
- sel ∷ ∀ n fn a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as, HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) ⇒ Term fn a → Term fn (At n as)
- match ∷ ∀ fn p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) ⇒ Term fn a → FunTy (MapList (Term fn) (ProductAsList a)) p → Pred fn
- onJust ∷ ∀ fn a p. (BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) ⇒ Term fn (Maybe a) → (Term fn a → p) → Pred fn
- isJust ∷ ∀ fn a. (BaseUniverse fn, HasSpec fn a, IsNormalType a) ⇒ Term fn (Maybe a) → Pred fn
- ifElse ∷ (BaseUniverse fn, IsPred p fn, IsPred q fn) ⇒ Term fn Bool → p → q → Pred fn
- chooseSpec ∷ HasSpec fn a ⇒ (Int, Specification fn a) → (Int, Specification fn a) → Specification fn a
Documentation
data GenericsFn fn args res Source #
Instances
FunctionLike (GenericsFn fn) Source # | |
Defined in Constrained.Spec.Generics | |
BaseUniverse fn ⇒ Functions (GenericsFn fn) fn Source # | |
Defined in Constrained.Spec.Generics propagateSpecFun ∷ ∀ (as ∷ [Type]) a b. (TypeList as, Typeable as, HasSpec fn a, HasSpec fn b, All (HasSpec fn) as) ⇒ GenericsFn fn as b → ListCtx Value as (HOLE a) → Specification fn b → Specification fn a Source # rewriteRules ∷ ∀ (as ∷ [Type]) b. (TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) ⇒ GenericsFn fn as b → List (Term fn) as → Maybe (Term fn b) Source # mapTypeSpec ∷ (HasSpec fn a, HasSpec fn b) ⇒ GenericsFn fn '[a] b → TypeSpec fn a → Specification fn b Source # | |
Show (GenericsFn fn as b) Source # | |
Defined in Constrained.Base | |
Eq (GenericsFn fn args res) Source # | |
Defined in Constrained.Base (==) ∷ GenericsFn fn args res → GenericsFn fn args res → Bool Source # (/=) ∷ GenericsFn fn args res → GenericsFn fn args res → Bool Source # |
type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a, CountCases a ~ 1) Source #
left_ ∷ (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) ⇒ Term fn a → Term fn (Either a b) Source #
right_ ∷ (HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) ⇒ Term fn b → Term fn (Either a b) Source #
caseOn ∷ ∀ fn a. (HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a, TypeSpec fn a ~ TypeSpec fn (SimpleRep a), SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) ⇒ Term fn a → FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn) Source #
branch ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ FunTy (MapList (Term fn) (Args a)) p → Weighted (Binder fn) a Source #
branchW ∷ ∀ fn p a. (HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) ⇒ Int → FunTy (MapList (Term fn) (Args a)) p → Weighted (Binder fn) a Source #
forAll' ∷ ∀ fn t a p. (Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t, HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn, IsProd (SimpleRep a), HasSpec fn a) ⇒ Term fn t → FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Pred fn Source #
Like forAll
but pattern matches on the `Term fn a`
constrained' ∷ ∀ a fn p. (Cases (SimpleRep a) ~ '[SimpleRep a], TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn (SimpleRep a), HasSimpleRep a, All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a), HasSpec fn a, IsPred p fn) ⇒ FunTy (MapList (Term fn) (Args (SimpleRep a))) p → Specification fn a Source #
Like constrained
but pattern matches on the bound `Term fn a`
reify' ∷ ∀ fn a b p. (Cases (SimpleRep b) ~ '[SimpleRep b], TypeSpec fn b ~ TypeSpec fn (SimpleRep b), HasSpec fn (SimpleRep b), HasSimpleRep b, All (HasSpec fn) (Args (SimpleRep b)), IsProd (SimpleRep b), HasSpec fn a, HasSpec fn b, IsPred p fn) ⇒ Term fn a → (a → b) → FunTy (MapList (Term fn) (Args (SimpleRep b))) p → Pred fn Source #
Like reify
but pattern matches on the bound `Term fn b`
con ∷ ∀ c a r fn. (SimpleRep a ~ SOP (TheSop a), TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)), TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a, r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a), ResultType r ~ Term fn a, SOPTerm c fn (TheSop a), ConstrTerm fn (ConstrOf c (TheSop a))) ⇒ r Source #
onCon ∷ ∀ c a fn p. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn, Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a), All (HasSpec fn) (ConstrOf c (TheSop a)), IsProd (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p → Pred fn Source #
isCon ∷ ∀ c a fn. (IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a), TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a, HasSpec fn a, HasSpec fn (SimpleRep a), SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a, All (HasSpec fn) (Cases (SOP (TheSop a))), HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) ⇒ Term fn a → Pred fn Source #
sel ∷ ∀ n fn a c as. (SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as], TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as, HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) ⇒ Term fn a → Term fn (At n as) Source #
match ∷ ∀ fn p a. (HasSpec fn a, IsProductType fn a, IsPred p fn) ⇒ Term fn a → FunTy (MapList (Term fn) (ProductAsList a)) p → Pred fn Source #
onJust ∷ ∀ fn a p. (BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) ⇒ Term fn (Maybe a) → (Term fn a → p) → Pred fn Source #
isJust ∷ ∀ fn a. (BaseUniverse fn, HasSpec fn a, IsNormalType a) ⇒ Term fn (Maybe a) → Pred fn Source #
chooseSpec ∷ HasSpec fn a ⇒ (Int, Specification fn a) → (Int, Specification fn a) → Specification fn a Source #