verifiable-expressions-0.4.0: An intermediate language for Hoare logic style verification.

Safe HaskellNone
LanguageHaskell2010

Language.Expression.Choice

Synopsis

Documentation

data OpChoice ops (t :: * -> *) a where Source #

Form the union of a list of operators. This creates an operator which is a choice from one of its constituents.

For example, OpChoice '[NumOp, EqOp] is an operator that can either represent an arithmetic operation or an equality comparison.

Constructors

OpThis :: op t a -> OpChoice (op ': ops) t a 
OpThat :: OpChoice ops t a -> OpChoice (op ': ops) t a 

Instances

(HFoldableAt * k op, HFoldableAt * k (OpChoice ops)) => HFoldableAt * k (OpChoice ((:) ((* -> *) -> * -> *) op ops)) Source # 

Methods

hfoldMap :: (forall (b :: k). t b -> OpChoice ((((* -> *) -> * -> *) ': op) ops) b) -> h t a -> OpChoice ((((* -> *) -> * -> *) ': op) ops) a Source #

HFoldableAt * k (OpChoice ([] ((* -> *) -> * -> *))) Source # 

Methods

hfoldMap :: (forall (b :: k). t b -> OpChoice [(* -> *) -> * -> *] b) -> h t a -> OpChoice [(* -> *) -> * -> *] a Source #

(HTraversable * op, HTraversable * (OpChoice ops)) => HTraversable * (OpChoice ((:) ((* -> *) -> * -> *) op ops)) Source # 

Methods

htraverse :: Applicative f => (forall (b :: OpChoice ((((* -> *) -> * -> *) ': op) ops)). t b -> f (t' b)) -> h t a -> f (h t' a) Source #

hsequence :: Applicative f => h (Compose * (OpChoice ((((* -> *) -> * -> *) ': op) ops)) f t) a -> f (h t a) Source #

HTraversable * (OpChoice ([] ((* -> *) -> * -> *))) Source # 

Methods

htraverse :: Applicative f => (forall (b :: OpChoice [(* -> *) -> * -> *]). t b -> f (t' b)) -> h t a -> f (h t' a) Source #

hsequence :: Applicative f => h (Compose * (OpChoice [(* -> *) -> * -> *]) f t) a -> f (h t a) Source #

(HFunctor * op, HFunctor * (OpChoice ops)) => HFunctor * (OpChoice ((:) ((* -> *) -> * -> *) op ops)) Source # 

Methods

hmap :: (forall (b :: OpChoice ((((* -> *) -> * -> *) ': op) ops)). t b -> t' b) -> h t a -> h t' a Source #

HFunctor * (OpChoice ([] ((* -> *) -> * -> *))) Source # 

Methods

hmap :: (forall (b :: OpChoice [(* -> *) -> * -> *]). t b -> t' b) -> h t a -> h t' a Source #

(Pretty2 * * op, Pretty2 * * (OpChoice ops)) => Pretty2 * * (OpChoice ((:) ((* -> *) -> * -> *) op ops)) Source # 

Methods

pretty2 :: Pretty1 (OpChoice ((((* -> *) -> * -> *) ': op) ops)) t => op t a -> String Source #

prettys2Prec :: Pretty1 (OpChoice ((((* -> *) -> * -> *) ': op) ops)) t => Int -> op t a -> ShowS Source #

Pretty2 * * (OpChoice ([] ((* -> *) -> * -> *))) Source # 

Methods

pretty2 :: Pretty1 (OpChoice [(* -> *) -> * -> *]) t => op t a -> String Source #

prettys2Prec :: Pretty1 (OpChoice [(* -> *) -> * -> *]) t => Int -> op t a -> ShowS Source #

_OpThis :: Prism' (OpChoice (op ': ops) t a) (op t a) Source #

_OpThat :: Prism' (OpChoice (op ': ops) t a) (OpChoice ops t a) Source #

noOps :: OpChoice '[] t a -> x Source #

newtype AsOp (t :: * -> *) a op Source #

Constructors

AsOp (op t a) 

Instances

Wrapped (AsOp t a op) Source # 

Associated Types

type Unwrapped (AsOp t a op) :: * #

Methods

_Wrapped' :: Iso' (AsOp t a op) (Unwrapped (AsOp t a op)) #

(~) * (AsOp t1 a1 op1) t2 => Rewrapped (AsOp t3 a2 op2) t2 Source # 
type Unwrapped (AsOp t a op) Source # 
type Unwrapped (AsOp t a op) = op t a

choiceToUnion :: OpChoice ops t a -> Union (AsOp t a) ops Source #

unionToChoice :: Union (AsOp t a) ops -> OpChoice ops t a Source #

_OpChoice :: Iso (OpChoice ops t a) (OpChoice ops' t' a') (Union (AsOp t a) ops) (Union (AsOp t' a') ops') Source #

class ChooseOp op ops where Source #

This class provides a low-boilerplate way of lifting individual operators into a union, and extracting operators from a union.

Minimal complete definition

chooseOp

Methods

chooseOp :: Prism' (OpChoice ops t a) (op t a) Source #

Project a single operator from a union which contains it.

Instances

UElem ((* -> *) -> * -> *) op ops i => ChooseOp op ops Source # 

Methods

chooseOp :: (Choice p, Applicative f) => p (op t a) (f (op t a)) -> p (OpChoice ops t a) (f (OpChoice ops t a)) Source #

class SubsetOp ops1 ops2 where Source #

Minimal complete definition

subsetOp

Methods

subsetOp :: Prism' (OpChoice ops2 t a) (OpChoice ops1 t a) Source #

Instances

USubset ((* -> *) -> * -> *) ops1 ops2 is => SubsetOp ops1 ops2 Source # 

Methods

subsetOp :: (Choice p, Applicative f) => p (OpChoice ops1 t a) (f (OpChoice ops1 t a)) -> p (OpChoice ops2 t a) (f (OpChoice ops2 t a)) Source #

newtype HFree' ops v a Source #

HFree' ops v a is a higher-order free monad over the list of operators ops with variables in the type v and it represents a value of type a.

Intuitively, it represents an expression which may contain operations from any of the operators in the list ops.

Constructors

HFree' 

Fields

Instances

(HFoldableAt * k (OpChoice ops), HFunctor * (OpChoice ops)) => HFoldableAt * k (HFree' ops) Source # 

Methods

hfoldMap :: (forall (b :: k). t b -> HFree' ops b) -> h t a -> HFree' ops a Source #

Pretty2 * * (OpChoice ops) => Pretty2 * * (HFree' ops) Source # 

Methods

pretty2 :: Pretty1 (HFree' ops) t => op t a -> String Source #

prettys2Prec :: Pretty1 (HFree' ops) t => Int -> op t a -> ShowS Source #

HTraversable * (OpChoice ops) => HTraversable * (HFree' ops) Source # 

Methods

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

hsequence :: Applicative f => h (Compose * (HFree' ops) f t) a -> f (h t a) Source #

HFunctor * (OpChoice ops) => HMonad * (HFree' ops) Source # 
HFunctor * (OpChoice ops) => HBind * (HFree' ops) Source # 

Methods

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

HPointed * (HFree' ops) Source # 

Methods

hpure :: t a -> h t a Source #

HFunctor * (OpChoice ops) => HFunctor * (HFree' ops) Source # 

Methods

hmap :: (forall (b :: HFree' ops). t b -> t' b) -> h t a -> h t' a Source #

(Data (HFree * (OpChoice ops) v a), Typeable * (HFree' ops v a)) => Data (HFree' ops v a) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HFree' ops v a -> c (HFree' ops v a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (HFree' ops v a) #

toConstr :: HFree' ops v a -> Constr #

dataTypeOf :: HFree' ops v a -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (HFree' ops v a)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HFree' ops v a)) #

gmapT :: (forall b. Data b => b -> b) -> HFree' ops v a -> HFree' ops v a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HFree' ops v a -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HFree' ops v a -> r #

gmapQ :: (forall d. Data d => d -> u) -> HFree' ops v a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> HFree' ops v a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> HFree' ops v a -> m (HFree' ops v a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HFree' ops v a -> m (HFree' ops v a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HFree' ops v a -> m (HFree' ops v a) #

Wrapped (HFree' ops v a) Source # 

Associated Types

type Unwrapped (HFree' ops v a) :: * #

Methods

_Wrapped' :: Iso' (HFree' ops v a) (Unwrapped (HFree' ops v a)) #

(~) * (HFree' ops1 v1 a1) t => Rewrapped (HFree' ops2 v2 a2) t Source # 
type Unwrapped (HFree' ops v a) Source # 
type Unwrapped (HFree' ops v a) = HFree * (OpChoice ops) v a

squashExpression :: (HFunctor op1, HFunctor op2, HFunctor (OpChoice ops), ChooseOp op1 ops, ChooseOp op2 ops) => HFree op1 (HFree op2 v) a -> HFree' ops v a Source #

Squash a composition of expressions over different operators into a single-layered expression over a choice of the two operators.

hwrap' :: (HFunctor op, HFunctor (OpChoice ops), ChooseOp op ops) => op (HFree' ops v) a -> HFree' ops v a Source #