improve-0.1.0: 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) 
PathName (V a) 

type Name = StringSource

type Path = [Name]Source

class PathName a whereSource

Methods

pathName :: a -> StringSource

Instances

class AllE a whereSource

Methods

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

const' :: a -> ConstSource

Instances

class AllE a => NumE a Source

Instances

data Const Source

Constructors

Bool Bool 
Int Int 
Float Float 

Instances

data Statement Source

Constructors

AssignBool (V Bool) (E Bool) 
AssignInt (V Int) (E Int) 
AssignFloat (V Float) (E Float) 
Branch (E Bool) Statement Statement 
Sequence Statement Statement 
Assert (E Bool) 
Assume (E Bool) 
Label Name Statement 
Null 

type VarInfo = (Bool, Path, Const)Source

varInfo :: AllE a => V a -> VarInfoSource

stmtVars :: Statement -> [VarInfo]Source

exprVars :: E a -> [VarInfo]Source