why3-0.8: Haskell support for the Why3 input format.

Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Why3.AST

Documentation

type Name = Text Source

data Theory Source

Constructors

Theory Name [Decl] 

Instances

data Decl Source

Constructors

Goal Name Expr 
Use (Maybe ImpExp) Name (Maybe Name) 
Axiom Name Expr 
Lemma Name Expr 
Type Name [Text] [(Name, [Text])] 
TypeDef Name [Text] [(Name, [Text])] TypeDef 
Predicate Name [Text] [Type] 
PredicateDef Name [Text] [(Maybe Name, Type)] Expr 
Function Name [Text] [Type] Type 
FunctionDef Name [Text] [(Maybe Name, Type)] Type Expr 

Instances

data TypeDef Source

Constructors

TyRecord [(Name, Type)] 
Ty Type 
TyCase [TyCaseAlt] 

Instances

data TyCaseAlt Source

Constructors

TyCaseAlt Name [Text] [(Maybe Name, Type)] 

Instances

data ImpExp Source

Constructors

Import 
Export 

Instances

data Literal Source

Constructors

Integer Integer 
Real Text 
Bool Bool 

Instances

data Expr Source

Constructors

Lit Literal 
App Name [Expr] 
Let Pattern Expr Expr 
If Expr Expr Expr 
Match [Expr] [(Pattern, Expr)] 
Conn Conn Expr Expr 
Not Expr 
Quant Quant [(Name, Type)] [[Expr]] Expr 
Field Name Expr 
Record [(Name, Expr)] 
RecordUpdate Expr [(Name, Expr)] 
Cast Expr Type 
Labeled Text Expr 

Instances

data Quant Source

Constructors

Forall 
Exists 

Instances

data Conn Source

Constructors

And 
AsymAnd 
Or 
AsymOr 
Implies 
Iff 

Instances

data Pattern Source

Constructors

PWild 
PVar Name 
PCon Name [Pattern] 

Instances

data Type Source

Constructors

TyCon Name [Type] 
TyVar Name 
Tuple [Type] 

Instances