module Language.Why3.AST where
import Data.Data (Data, Typeable)
import Data.Text (Text)
import GHC.Generics (Generic)
import Control.DeepSeq(NFData(..))
type Name = Text
data Theory = Theory Name [Decl]
deriving (Eq,Ord,Read,Show,Generic,Typeable,Data)
data Decl = 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
deriving (Eq,Ord,Read,Show,Generic,Typeable,Data)
data TypeDef = TyRecord [ (Name, Type) ]
| Ty Type
| TyCase [TyCaseAlt]
deriving (Eq,Ord,Read,Show,Generic,Typeable,Data)
data TyCaseAlt = TyCaseAlt Name [Text] [(Maybe Name, Type)]
deriving (Eq,Ord,Read,Show,Generic,Typeable,Data)
data ImpExp = Import | Export
deriving (Eq,Ord,Read,Show,Generic,Typeable,Data)
data Literal = Integer Integer
| Real Text
| Bool Bool
deriving (Eq,Ord,Read,Show,Generic,Typeable,Data)
data Expr = 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
deriving (Eq,Ord,Show,Read,Generic,Typeable,Data)
data Quant = Forall | Exists
deriving (Eq,Ord,Show,Read,Generic,Typeable,Data)
data Conn = And | AsymAnd | Or | AsymOr | Implies | Iff
deriving (Eq,Ord,Show,Read,Generic,Typeable,Data)
data Pattern = PWild
| PVar Name
| PCon Name [Pattern]
deriving (Eq,Ord,Show,Read,Generic,Typeable,Data)
data Type = TyCon Name [Type]
| TyVar Name
| Tuple [Type]
deriving (Eq,Ord,Show,Read,Generic,Typeable,Data)
instance NFData Type where
rnf ty =
case ty of
TyCon x xs -> rnf x `seq` rnf xs
TyVar x -> rnf x
Tuple ts -> rnf ts