dove-0.0.0: The Dove verification language.

Safe HaskellSafe-Inferred
LanguageHaskell2010

Language.Dove.Syntax

Documentation

data Expr Source

Constructors

Var String 
ForAll String Expr 
Let String Expr Expr 
Record [(String, Expr)] 
RecordOverlay Expr Expr 
RecordProject Expr String 
Array [Expr] 
ArrayAppend Expr Expr 
ArrayProject Expr Expr 
ArrayUpdate Expr Expr Expr 
UniOp UniOp Expr 
BinOp BinOp Expr Expr 
If Expr Expr Expr 
Unit 
Bool Bool 
Integer Integer 
Comment String Expr 

Instances

data UniOp Source

Constructors

Not 
Length 
Negate 
Abs 
Signum 
IsArray 
IsInt 

Instances

data BinOp Source

Constructors

And 
Or 
Implies 
Eq 
Lt 
Le 
Gt 
Ge 
Add 
Sub 
Mul 
Mod 

Instances

let' :: String -> Expr -> Expr -> Expr Source

forAll :: [String] -> Expr -> Expr Source

not' :: Expr -> Expr Source

(&&.) :: Expr -> Expr -> Expr Source

(||.) :: Expr -> Expr -> Expr Source

implies :: Expr -> Expr -> Expr Source

unit :: Expr Source

true :: Expr Source

false :: Expr Source

if' :: Expr -> Expr -> Expr -> Expr Source

length' :: Expr -> Expr Source

isArray :: Expr -> Expr Source

isInt :: Expr -> Expr Source

(==.) :: Expr -> Expr -> Expr Source

(<.) :: Expr -> Expr -> Expr Source

(<=.) :: Expr -> Expr -> Expr Source

(>.) :: Expr -> Expr -> Expr Source

(>=.) :: Expr -> Expr -> Expr Source

mod' :: Expr -> Expr -> Expr Source