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

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 #
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 #
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 #
IsString s => IsString (WhileExpr s AlgReal) Source #
Instance details Defined in Language.While.Syntax 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

Instances details

VerifiableVar (WhileVar String) Source #
Instance details Defined in Language.While.Syntax Associated Types type VarKey (WhileVar String) Source # type VarSym (WhileVar String) :: Type -> Type 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 :: Type -> Type) Source #
Instance details Defined in Language.While.Syntax Methods pretty1 :: forall (a :: k). WhileVar l a -> String Source # prettys1Prec :: forall (a :: k). Int -> WhileVar l a -> ShowS Source #
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 #
IsString s => IsString (WhileExpr s AlgReal) Source #
Instance details Defined in Language.While.Syntax Methods fromString :: String -> WhileExpr s AlgReal #
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 VarEnv (WhileVar String) Source #
Instance details Defined in Language.While.Syntax 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

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 #