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

Defined in Language.While.Syntax

Methods

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

EvalOpAt SBV WhileOpKind

Defined in Language.While.Syntax

Methods

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

PrettyOp WhileOpKind

Defined in Language.While.Syntax

Methods

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

Num (WhileExpr l AlgReal)

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)

Defined in Language.While.Syntax

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)

Defined in Language.While.Syntax

Associated Types

type VarKey (WhileVar String) :: Type

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

type VarEnv (WhileVar String) :: Type

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 :: Type -> Type)

Defined in Language.While.Syntax

Methods

pretty1 :: WhileVar l a -> String

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

Num (WhileExpr l AlgReal)

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)

Defined in Language.While.Syntax

Methods

fromString :: String -> WhileExpr s AlgReal

type VarKey (WhileVar String)

Defined in Language.While.Syntax

type VarKey (WhileVar String) = String

type VarSym (WhileVar String)

Defined in Language.While.Syntax

type VarSym (WhileVar String) = SBV

type VarEnv (WhileVar String)

Defined in Language.While.Syntax

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)

Defined in Language.While.Syntax

Methods

pretty :: Command l a -> String

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

data StepResult a

Constructors

Terminated

Failed

Progress a

Instances

Functor StepResult

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

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