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

Safe HaskellNone
LanguageHaskell2010

Language.While.Syntax

Documentation

prettys1Binop :: Pretty1 t => Int -> String -> Int -> t a -> t b -> ShowS Source #

data WhileVar l a where Source #

Constructors

WhileVar :: l -> WhileVar l AlgReal 
Instances
VerifiableVar (WhileVar String) Source # 
Instance details

Defined in Language.While.Syntax

Associated Types

type VarKey (WhileVar String) :: Type Source #

type VarSym (WhileVar String) :: Type -> Type Source #

type VarEnv (WhileVar String) :: Type Source #

Pretty l => Pretty1 (WhileVar l :: Type -> Type) Source # 
Instance details

Defined in Language.While.Syntax

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

type VarKey (WhileVar String) Source # 
Instance details

Defined in Language.While.Syntax

type VarSym (WhileVar String) Source # 
Instance details

Defined in Language.While.Syntax

type VarEnv (WhileVar String) Source # 
Instance details

Defined in Language.While.Syntax

type VarEnv (WhileVar String) = ()

data Command l a Source #

Constructors

CAnn a (Command l a) 
CSeq (Command l a) (Command l a) 
CSkip 
CAssign l (WhileExpr l AlgReal) 
CIf (WhileExpr l Bool) (Command l a) (Command l a) 
CWhile (WhileExpr l Bool) (Command l a) 
Instances
(Pretty l, Pretty a) => Pretty (Command l a) Source # 
Instance details

Defined in Language.While.Syntax

data StepResult a Source #

Constructors

Terminated 
Failed 
Progress a 
Instances
Functor StepResult Source # 
Instance details

Defined in Language.While.Syntax

Methods

fmap :: (a -> b) -> StepResult a -> StepResult b #

(<$) :: a -> StepResult b -> StepResult a #

evalWhileExpr :: Applicative f => (forall x. WhileVar l x -> f x) -> WhileExpr l a -> f a Source #

lookupVar :: Ord l => Map l AlgReal -> WhileVar l a -> Maybe a Source #