Safe Haskell	None
Language	Haskell2010

Language.While.Syntax

Documentation

data WhileOpKind (as :: [Type]) r where Source #

Constructors

OpLit :: AlgReal -> WhileOpKind ('[] :: [Type]) AlgReal
OpAdd :: WhileOpKind '[AlgReal, AlgReal] AlgReal
OpSub :: WhileOpKind '[AlgReal, AlgReal] AlgReal
OpMul :: WhileOpKind '[AlgReal, AlgReal] AlgReal
OpEq :: WhileOpKind '[AlgReal, AlgReal] Bool
OpLT :: WhileOpKind '[AlgReal, AlgReal] Bool
OpLE :: WhileOpKind '[AlgReal, AlgReal] Bool
OpGT :: WhileOpKind '[AlgReal, AlgReal] Bool
OpGE :: WhileOpKind '[AlgReal, AlgReal] Bool
OpAnd :: WhileOpKind '[Bool, Bool] Bool
OpOr :: WhileOpKind '[Bool, Bool] Bool
OpNot :: WhileOpKind '[Bool] Bool

Instances

Instances details

EvalOpAt Identity WhileOpKind Source #
Instance details Defined in Language.While.Syntax Methods evalMany :: forall (as :: [Type]) r. WhileOpKind as r -> Rec Identity as -> Identity r Source #
EvalOpAt SBV WhileOpKind Source #
Instance details Defined in Language.While.Syntax Methods evalMany :: forall (as :: [Type]) r. WhileOpKind as r -> Rec SBV as -> SBV r Source #
PrettyOp WhileOpKind Source #
Instance details Defined in Language.While.Syntax Methods prettysPrecOp :: forall (t :: Type -> Type) (as :: [Type]) a. Pretty1 t => Int -> WhileOpKind as a -> Rec t as -> ShowS Source #
IsString s => IsString (WhileExpr s AlgReal) Source #
Instance details Defined in Language.While.Syntax Methods fromString :: String -> WhileExpr s AlgReal #
Num (WhileExpr l AlgReal) Source #
Instance details Defined in Language.While.Syntax Methods (+) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal # (-) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal # (*) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal # negate :: WhileExpr l AlgReal -> WhileExpr l AlgReal # abs :: WhileExpr l AlgReal -> WhileExpr l AlgReal # signum :: WhileExpr l AlgReal -> WhileExpr l AlgReal # fromInteger :: Integer -> WhileExpr l AlgReal #

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

type WhileOp = GeneralOp WhileOpKind Source #

data WhileVar l a where Source #

Constructors

WhileVar :: forall l. l -> WhileVar l AlgReal

Instances

Instances details

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

Instance details

Defined in Language.While.Syntax

Methods

pretty1 :: WhileVar l a -> String Source #

prettys1Prec :: Int -> WhileVar l a -> ShowS Source #

VerifiableVar (WhileVar String) Source #

Instance details

Defined in Language.While.Syntax

Associated Types

type VarKey (WhileVar String)
Instance details Defined in Language.While.Syntax type VarKey (WhileVar String) = String
type VarSym (WhileVar String)
Instance details Defined in Language.While.Syntax type VarSym (WhileVar String) = SBV
type VarEnv (WhileVar String)
Instance details Defined in Language.While.Syntax type VarEnv (WhileVar String) = ()

Methods

symForVar :: WhileVar String a -> VarEnv (WhileVar String) -> Symbolic (VarSym (WhileVar String) a) Source #

varKey :: WhileVar String a -> VarKey (WhileVar String) Source #

eqVarTypes :: WhileVar String a -> WhileVar String b -> Maybe (a :~: b) Source #

castVarSym :: WhileVar String a -> VarSym (WhileVar String) b -> Maybe (VarSym (WhileVar String) a) Source #

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

Instance details

Defined in Language.While.Syntax

Methods

fromString :: String -> WhileExpr s AlgReal #

Num (WhileExpr l AlgReal) Source #

Instance details

Defined in Language.While.Syntax

Methods

(+) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal #

(-) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal #

(*) :: WhileExpr l AlgReal -> WhileExpr l AlgReal -> WhileExpr l AlgReal #

negate :: WhileExpr l AlgReal -> WhileExpr l AlgReal #

abs :: WhileExpr l AlgReal -> WhileExpr l AlgReal #

signum :: WhileExpr l AlgReal -> WhileExpr l AlgReal #

fromInteger :: Integer -> WhileExpr l AlgReal #

type VarEnv (WhileVar String) Source #

Instance details

Defined in Language.While.Syntax

type VarEnv (WhileVar String) = ()

type VarKey (WhileVar String) Source #

Instance details

Defined in Language.While.Syntax

type VarKey (WhileVar String) = String

type VarSym (WhileVar String) Source #

Instance details

Defined in Language.While.Syntax

type VarSym (WhileVar String) = SBV

type WhileExpr l = HFree WhileOp (WhileVar l) Source #

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

Instances details

(Pretty l, Pretty a) => Pretty (Command l a) Source #
Instance details Defined in Language.While.Syntax Methods pretty :: Command l a -> String Source # prettysPrec :: Int -> Command l a -> ShowS Source #

data StepResult a Source #

Constructors

Terminated
Failed
Progress a

Instances

Instances details

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 #

oneStep :: Ord l => Command l a -> State (Map l AlgReal) (StepResult (Command l a)) Source #

runCommand :: Ord l => Command l a -> State (Map l AlgReal) Bool Source #

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