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

Language.Expression.GeneralOp

Documentation

data GeneralOp op t a where Source #

Constructors

Op :: RMap as => op as r -> Rec t as -> GeneralOp op t r 

Instances

Instances details
EvalOpAt k2 op => HFoldableAt (k2 :: k1 -> Type) (GeneralOp op :: (k1 -> Type) -> k1 -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

hfoldMap :: forall t (a :: k). (forall (b :: k). t b -> k2 b) -> GeneralOp op t a -> k2 a Source #

PrettyOp op => Pretty2 (GeneralOp op :: (k1 -> Type) -> k2 -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

pretty2 :: forall (t :: k -> Type) (a :: k). Pretty1 t => GeneralOp op t a -> String Source #

prettys2Prec :: forall (t :: k -> Type) (a :: k). Pretty1 t => Int -> GeneralOp op t a -> ShowS Source #

HTraversable (GeneralOp op :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

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

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

HFunctor (GeneralOp op :: (u -> Type) -> u -> Type) Source # 
Instance details

Defined in Language.Expression.GeneralOp

Methods

hmap :: forall t t' (a :: u0). (forall (b :: u0). t b -> t' b) -> GeneralOp op t a -> GeneralOp op t' a Source #

Num (WhileExpr l AlgReal) Source # 
Instance details

Defined in Language.While.Syntax

IsString s => IsString (WhileExpr s AlgReal) Source # 
Instance details

Defined in Language.While.Syntax

class EvalOpAt k op where Source #

Methods

evalMany :: op as r -> Rec k as -> k r Source #

Instances

Instances details
EvalOpAt Identity WhileOpKind Source # 
Instance details

Defined in Language.While.Syntax

Methods

evalMany :: forall (as :: [k]) (r :: k). WhileOpKind as r -> Rec Identity as -> Identity r Source #

EvalOpAt SBV WhileOpKind Source # 
Instance details

Defined in Language.While.Syntax

Methods

evalMany :: forall (as :: [k]) (r :: k). WhileOpKind as r -> Rec SBV as -> SBV r Source #

class PrettyOp op where Source #

Methods

prettysPrecOp :: Pretty1 t => Int -> op as a -> Rec t as -> ShowS Source #

Instances

Instances details
PrettyOp WhileOpKind Source # 
Instance details

Defined in Language.While.Syntax

Methods

prettysPrecOp :: forall (t :: u -> Type) (as :: [u]) (a :: k). Pretty1 t => Int -> WhileOpKind as a -> Rec t as -> ShowS Source #