Language.While.Syntax

Documentation

data WhileOpKind as r where

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

Methods

evalMany :: op as r -> Rec Identity WhileOpKind as -> WhileOpKind r

EvalOpAt * SBV WhileOpKind

Methods

evalMany :: op as r -> Rec SBV WhileOpKind as -> WhileOpKind r

PrettyOp * * WhileOpKind

Methods

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

Num (WhileExpr l AlgReal)

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)

Methods

fromString :: String -> WhileExpr s AlgReal

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

type WhileOp = GeneralOp WhileOpKind

data WhileVar l a where

Constructors

WhileVar :: l -> WhileVar l AlgReal

Instances

VerifiableVar (WhileVar String)

Associated Types

type VarKey (WhileVar String :: * -> *) :: *

type VarSym (WhileVar String :: * -> *) :: * -> *

type VarEnv (WhileVar String :: * -> *) :: *

Methods

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

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

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

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

Pretty l => Pretty1 * (WhileVar l)

Methods

pretty1 :: t a -> String

prettys1Prec :: Int -> t a -> ShowS

Num (WhileExpr l AlgReal)

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)

Methods

fromString :: String -> WhileExpr s AlgReal

type VarKey (WhileVar String)

type VarKey (WhileVar String) = String

type VarSym (WhileVar String)

type VarSym (WhileVar String) = SBV

type VarEnv (WhileVar String)

type VarEnv (WhileVar String) = ()

type WhileExpr l = HFree WhileOp (WhileVar l)

data Command l a

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)

Methods

pretty :: Command l a -> String

prettysPrec :: Int -> Command l a -> ShowS

data StepResult a

Constructors

Terminated

Failed

Progress a

Instances

Functor StepResult

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

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

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

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