Safe Haskell	None
Language	Haskell2010

Language.While.Syntax

Documentation

data WhileOpKind as r where Source #

Constructors

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

Instances

EvalOpAt * Identity WhileOpKind Source #
Methods evalMany :: op as r -> Rec Identity WhileOpKind as -> WhileOpKind r Source #
EvalOpAt * SBV WhileOpKind Source #
Methods evalMany :: op as r -> Rec SBV WhileOpKind as -> WhileOpKind r Source #
PrettyOp * * WhileOpKind Source #
Methods prettysPrecOp :: Pretty1 WhileOpKind t => Int -> op as a -> Rec WhileOpKind t as -> ShowS Source #
Num (WhileExpr l AlgReal) Source #
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 #
IsString s => IsString (WhileExpr s AlgReal) Source #
Methods fromString :: String -> WhileExpr s 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 :: l -> WhileVar l AlgReal

Instances

VerifiableVar (WhileVar String) Source #
Associated Types type VarKey (WhileVar String :: * -> ) :: Source # type VarSym (WhileVar String :: * -> ) :: -> * Source # type VarEnv (WhileVar String :: * -> ) :: Source # 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 #
Pretty l => Pretty1 * (WhileVar l) Source #
Methods pretty1 :: t a -> String Source # prettys1Prec :: Int -> t a -> ShowS Source #
Num (WhileExpr l AlgReal) Source #
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 #
IsString s => IsString (WhileExpr s AlgReal) Source #
Methods fromString :: String -> WhileExpr s AlgReal #
type VarKey (WhileVar String) Source #
type VarKey (WhileVar String) = String
type VarSym (WhileVar String) Source #
type VarSym (WhileVar String) = SBV
type VarEnv (WhileVar String) Source #
type VarEnv (WhileVar String) = ()

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

(Pretty l, Pretty a) => Pretty (Command l a) Source #
Methods pretty :: Command l a -> String Source # prettysPrec :: Int -> Command l a -> ShowS Source #

data StepResult a Source #

Constructors

Terminated
Failed
Progress a

Instances

Functor StepResult Source #
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 #