verifiable-expressions-0.6.1: An intermediate language for Hoare logic style verification.
Safe HaskellNone
LanguageHaskell2010

Language.Expression.Scope

Synopsis

Documentation

class HBound k where Source #

Methods

(^>>>=) :: HMonad h => k h t a -> (forall b. t b -> h t' b) -> k h t' a Source #

Instances

Instances details
HBound (Scope g :: ((k -> Type) -> k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

(^>>>=) :: forall h t (a :: k0) (t' :: k1 -> Type). HMonad h => Scope g h t a -> (forall (b :: k1). t b -> h t' b) -> Scope g h t' a Source #

data BV g f a where Source #

Constructors

B :: g a -> BV g f a

Bound variable

F :: f a -> BV g f a

Free variable

Instances

Instances details
HBifoldableAt (k2 :: k1 -> Type) (BV :: (k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbifoldMap :: forall f g (a :: k). (forall (b :: k). f b -> k2 b) -> (forall (b :: k). g b -> k2 b) -> BV f g a -> k2 a Source #

Pretty1 t => Pretty2 (BV t :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Pretty

Methods

pretty2 :: forall (t0 :: k0 -> Type) (a :: k1). Pretty1 t0 => BV t t0 a -> String Source #

prettys2Prec :: forall (t0 :: k0 -> Type) (a :: k1). Pretty1 t0 => Int -> BV t t0 a -> ShowS Source #

HBitraversable (BV :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbitraverse :: forall f s s' t t' (a :: k0). Applicative f => (forall (b :: k0). s b -> f (s' b)) -> (forall (b :: k0). t b -> f (t' b)) -> BV s t a -> f (BV s' t' a) Source #

HBifunctor (BV :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbimap :: forall s s' t t' (a :: k0). (forall (b :: k0). s b -> s' b) -> (forall (b :: k0). t b -> t' b) -> BV s t a -> BV s' t' a Source #

hfirst :: forall s s' (t :: k0 -> Type) (a :: k0). (forall (b :: k0). s b -> s' b) -> BV s t a -> BV s' t a Source #

hsecond :: forall t t' (s :: k0 -> Type) (a :: k0). (forall (b :: k0). t b -> t' b) -> BV s t a -> BV s t' a Source #

HTraversable (BV g :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

htraverse :: forall f t t' (a :: u0). Applicative f => (forall (b :: u0). t b -> f (t' b)) -> BV g t a -> f (BV g t' a) Source #

hsequence :: forall f (t :: u0 -> Type) (a :: u0). Applicative f => BV g (Compose f t) a -> f (BV g t a) Source #

HMonad (BV g :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

HBind (BV g :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

(^>>=) :: forall t (a :: k0) (t' :: k0 -> Type). BV g t a -> (forall (b :: k0). t b -> BV g t' b) -> BV g t' a Source #

HPointed (BV g :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hpure :: forall t (a :: k0). t a -> BV g t a Source #

HFunctor (BV g :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hmap :: forall t t' (a :: u0). (forall (b :: u0). t b -> t' b) -> BV g t a -> BV g t' a Source #

foldBV :: (w a -> r) -> (v a -> r) -> BV w v a -> r Source #

hbitraverseBV :: Functor t => (g a -> t (g' b)) -> (f a -> t (f' b)) -> BV g f a -> t (BV g' f' b) Source #

hbimapBV :: (g a -> g' b) -> (f a -> f' b) -> BV g f a -> BV g' f' b Source #

newtype Scope g h f a Source #

Constructors

Scope 

Fields

Instances

Instances details
HDuofoldableAt (k2 :: k1 -> Type) (Scope k2 :: ((k1 -> Type) -> k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hduofoldMap :: forall s t (a :: k). HTraversable s => (forall (g :: k -> Type) (b :: k). (forall (c :: k). g c -> k2 c) -> s g b -> k2 b) -> (forall (b :: k). t b -> k2 b) -> Scope k2 s t a -> k2 a Source #

HBound (Scope g :: ((k -> Type) -> k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

(^>>>=) :: forall h t (a :: k0) (t' :: k1 -> Type). HMonad h => Scope g h t a -> (forall (b :: k1). t b -> h t' b) -> Scope g h t' a Source #

(Pretty2 h, Pretty1 t) => Pretty2 (Scope t h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Pretty

Methods

pretty2 :: forall (t0 :: k0 -> Type) (a :: k1). Pretty1 t0 => Scope t h t0 a -> String Source #

prettys2Prec :: forall (t0 :: k0 -> Type) (a :: k1). Pretty1 t0 => Int -> Scope t h t0 a -> ShowS Source #

HDuotraversable (Scope g :: ((u -> Type) -> u -> Type) -> (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hduotraverse :: forall f s s' t t' (a :: u0). Applicative f => (forall (g0 :: u0 -> Type) (g' :: u0 -> Type) (b :: u0). (forall (c :: u0). g0 c -> f (g' c)) -> s g0 b -> f (s' g' b)) -> (forall (b :: u0). t b -> f (t' b)) -> Scope g s t a -> f (Scope g s' t' a) Source #

HDuofunctor (Scope g :: ((u -> Type) -> u -> Type) -> (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hduomap :: forall s s' t t' (a :: u0). (forall (g0 :: u0 -> Type) (g' :: u0 -> Type) (b :: u0). (forall (c :: u0). g0 c -> g' c) -> s g0 b -> s' g' b) -> (forall (b :: u0). t b -> t' b) -> Scope g s t a -> Scope g s' t' a Source #

HTraversable h => HTraversable (Scope g h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

htraverse :: forall f t t' (a :: u0). Applicative f => (forall (b :: u0). t b -> f (t' b)) -> Scope g h t a -> f (Scope g h t' a) Source #

hsequence :: forall f (t :: u0 -> Type) (a :: u0). Applicative f => Scope g h (Compose f t) a -> f (Scope g h t a) Source #

HPointed h => HPointed (Scope g h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hpure :: forall t (a :: k0). t a -> Scope g h t a Source #

HFunctor h => HFunctor (Scope g h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hmap :: forall t t' (a :: u0). (forall (b :: u0). t b -> t' b) -> Scope g h t a -> Scope g h t' a Source #

_Scope :: Iso (Scope g h f a) (Scope g' h' f' a') (h (BV g (h f)) a) (h' (BV g' (h' f')) a') Source #

hbitraverseScope :: (Applicative t, HTraversable h) => (forall b. g b -> t (g' b)) -> (forall b. f b -> t (f' b)) -> Scope g h f a -> t (Scope g' h f' a) Source #

freeVar :: HPointed h => f a -> Scope g h f a Source #

boundVar :: HPointed h => g a -> Scope g h f a Source #

liftScope :: (HFunctor h, HPointed h) => h f a -> Scope g h f a Source #

abstractTraverse :: (HMonad h, HTraversable h, Applicative t) => (forall b. f b -> t (Maybe (g b))) -> h f a -> t (Scope g h f a) Source #

abstract :: HMonad h => (forall b. f b -> Maybe (g b)) -> h f a -> Scope g h f a Source #

newtype Scoped h f g a Source #

Sometimes it's convenient to move around the type arguments to Scope.

Constructors

Scoped 

Fields

Instances

Instances details
(HFunctor h, HFoldableAt k2 h) => HBifoldableAt (k2 :: k1 -> Type) (Scoped h :: (k1 -> Type) -> (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbifoldMap :: forall f g (a :: k). (forall (b :: k). f b -> k2 b) -> (forall (b :: k). g b -> k2 b) -> Scoped h f g a -> k2 a Source #

(Pretty2 h, Pretty1 t) => Pretty2 (Scoped h t :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Pretty

Methods

pretty2 :: forall (t0 :: k0 -> Type) (a :: k1). Pretty1 t0 => Scoped h t t0 a -> String Source #

prettys2Prec :: forall (t0 :: k0 -> Type) (a :: k1). Pretty1 t0 => Int -> Scoped h t t0 a -> ShowS Source #

HTraversable h => HBitraversable (Scoped h :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbitraverse :: forall f s s' t t' (a :: k0). Applicative f => (forall (b :: k0). s b -> f (s' b)) -> (forall (b :: k0). t b -> f (t' b)) -> Scoped h s t a -> f (Scoped h s' t' a) Source #

HFunctor h => HBifunctor (Scoped h :: (k -> Type) -> (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hbimap :: forall s s' t t' (a :: k0). (forall (b :: k0). s b -> s' b) -> (forall (b :: k0). t b -> t' b) -> Scoped h s t a -> Scoped h s' t' a Source #

hfirst :: forall s s' (t :: k0 -> Type) (a :: k0). (forall (b :: k0). s b -> s' b) -> Scoped h s t a -> Scoped h s' t a Source #

hsecond :: forall t t' (s :: k0 -> Type) (a :: k0). (forall (b :: k0). t b -> t' b) -> Scoped h s t a -> Scoped h s t' a Source #

HTraversable h => HTraversable (Scoped h f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

htraverse :: forall f0 t t' (a :: u0). Applicative f0 => (forall (b :: u0). t b -> f0 (t' b)) -> Scoped h f t a -> f0 (Scoped h f t' a) Source #

hsequence :: forall f0 (t :: u0 -> Type) (a :: u0). Applicative f0 => Scoped h f (Compose f0 t) a -> f0 (Scoped h f t a) Source #

HFunctor h => HFunctor (Scoped h f :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hmap :: forall t t' (a :: u0). (forall (b :: u0). t b -> t' b) -> Scoped h f t a -> Scoped h f t' a Source #

_Scoped :: Iso (Scoped h f g a) (Scoped h' f' g' a') (Scope g h f a) (Scope g' h' f' a') Source #

data SFree h f a Source #

Constructors

SPure (f a) 
SWrap (h (Scoped (SFree h) f) (SFree h f) a) 

Instances

Instances details
(HDuotraversable h, HDuofoldableAt k2 h) => HFoldableAt (k2 :: k1 -> Type) (SFree h :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> k2 b) -> SFree h t a -> k2 a Source #

Pretty3 h => Pretty2 (SFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Pretty

Methods

pretty2 :: forall (t :: k0 -> Type) (a :: k1). Pretty1 t => SFree h t a -> String Source #

prettys2Prec :: forall (t :: k0 -> Type) (a :: k1). Pretty1 t => Int -> SFree h t a -> ShowS Source #

HDuotraversable h => HTraversable (SFree h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

htraverse :: forall f t t' (a :: u0). Applicative f => (forall (b :: u0). t b -> f (t' b)) -> SFree h t a -> f (SFree h t' a) Source #

hsequence :: forall f (t :: u0 -> Type) (a :: u0). Applicative f => SFree h (Compose f t) a -> f (SFree h t a) Source #

HDuofunctor h => HMonad (SFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

HDuofunctor h => HBind (SFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

(^>>=) :: forall t (a :: k0) (t' :: k0 -> Type). SFree h t a -> (forall (b :: k0). t b -> SFree h t' b) -> SFree h t' a Source #

HPointed (SFree h :: (k -> Type) -> k -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hpure :: forall t (a :: k0). t a -> SFree h t a Source #

HDuofunctor h => HFunctor (SFree h :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.Scope

Methods

hmap :: forall t t' (a :: u0). (forall (b :: u0). t b -> t' b) -> SFree h t a -> SFree h t' a Source #