improve-0.2.3: An imperative, verifiable programming language for high assurance applications.

Language.ImProve.Core

Synopsis

Documentation

data E a whereSource

A logical, arithmetic, comparative, or conditional expression.

Constructors

Ref :: AllE a => V a -> E a 
Const :: AllE a => a -> E a 
Add :: NumE a => E a -> E a -> E a 
Sub :: NumE a => E a -> E a -> E a 
Mul :: NumE a => E a -> a -> E a 
Div :: NumE a => E a -> a -> E a 
Mod :: E Int -> Int -> E Int 
Not :: E Bool -> E Bool 
And :: E Bool -> E Bool -> E Bool 
Or :: E Bool -> E Bool -> E Bool 
Eq :: AllE a => E a -> E a -> E Bool 
Lt :: NumE a => E a -> E a -> E Bool 
Gt :: NumE a => E a -> E a -> E Bool 
Le :: NumE a => E a -> E a -> E Bool 
Ge :: NumE a => E a -> E a -> E Bool 
Mux :: AllE a => E Bool -> E a -> E a -> E a 

Instances

Eq (E a) 
Fractional (E Float) 
(Num a, AllE a, NumE a) => Num (E a) 
Show (E a) 

data V a Source

A mutable variable.

Constructors

V Bool [Name] a 

Instances

Eq a => Eq (V a) 
Ord a => Ord (V a) 
AllE a => VarInfo' (V a) 
PathName (V a) 

data UV Source

An untyped variable.

Constructors

UVBool (V Bool) 
UVInt (V Int) 
UVFloat (V Float) 

Instances

Eq UV 
Ord UV 
VarInfo' UV 

type Path = [Name]Source

type UID = IntSource

class PathName a whereSource

Methods

pathName :: a -> StringSource

class Eq a => AllE a whereSource

Methods

zero :: (Name -> a -> m (V a)) -> aSource

const' :: a -> ConstSource

untype :: V a -> UVSource

Instances

class AllE a => NumE a Source

Instances

data Const Source

Constructors

Bool Bool 
Int Int 
Float Float 

Instances

data Statement whereSource

Constructors

Assign :: AllE a => V a -> E a -> Statement 
Branch :: E Bool -> Statement -> Statement -> Statement 
Sequence :: Statement -> Statement -> Statement 
Theorem :: Int -> Int -> [Int] -> E Bool -> Statement 
Assume :: E Bool -> Statement 
Label :: Name -> Statement -> Statement 
Null :: Statement 

Instances

varInfo :: VarInfo' a => a -> VarInfoSource

stmtVars :: Statement -> [UV]Source

Variables in a program.

exprVars :: E a -> [UV]Source

Variables in an expression.

theorems :: Statement -> [(Int, Int, [Int], E Bool)]Source

Theorems in a program.