module Why.Syntax where

type LabIdentifier  = String -- what is this?
type Identifier	    = String
type Terms	    = [Term]
type Identifiers    = [Identifier]
type Triggers	    = [Trigger]
type Trigger	    = [Term] -- one or more Term
type Types	    = [Type]
type LogicBinder    = (Identifier, Type)
type TypeParameters = Identifiers
type Effects	    = (Maybe Identifiers, Maybe Identifiers, Maybe Identifiers)
type Pre	    = Assertion
type Post	    = (Assertion, ExnConditions)
type ExnConditions  = [ExnCondition]
type ExnCondition   = (Identifier, Assertion)
type Assertion	    = (Predicate, Maybe Identifier)
type Binders	    = [(Identifiers, ValueType)]
type RecFun	    = (Identifier, Binders, ValueType, WfArg, Prog)
type LoopAnnot	    = (Assertion, Maybe WfArg)
type WfArg	    = (Term, Maybe Identifier)
type Why	    = [Declaration]
type LogicBinders   = [LogicBinder]
type LogicArgTypes  = [LogicArgType]
type Assertions	    = [Assertion]
type Handlers	    = [Handler]

data Term = 
    Const Constant
  | Sum Term Term
  | Sub Term Term
  | Mult Term Term
  | Div Term Term
  | Rem Term Term
  | TNegation Term
  | TVar LabIdentifier
  | TFunction Identifier Terms -- one or more Term
--  | X LabIdentifier (Maybe Term) -- what is this?
  | TIfThenElse Term Term Term
    deriving (Show, Read, Eq)

data Constant =
    IntConst Int
  | RealConst Float
  | BoolConst Bool
  | Void
    deriving (Show, Read, Eq)

data Predicate = 
    PredTrue
  | PredFalse
  | PVar Identifier
  | PFunction Identifier Terms -- one or more Term
  | Equal Term Term
  | Diff Term Term
  | Lesser Term Term
  | LessEq Term Term
  | Greater Term Term
  | GreatEq Term Term
  | PNegation Predicate
  | Conj Predicate Predicate
  | Disj Predicate Predicate
  | Imp Predicate Predicate
  | Equiv Predicate Predicate
  | PIfThenElse Term Predicate Predicate
  | Forall Identifiers Type Triggers Predicate -- one or more Identifier, Trigger
  | Exists Identifiers Type Predicate
--  | X Identifier String Predicate -- what is this?
    deriving (Show, Read, Eq)

data Type = 
    TInt 
  | TBool 
  | TReal 
  | TUnit 
  | User Identifier
--  | X Identifier -- what is this?
--  | Y Type Identifier -- what is this?
--  | Z Types Identifier -- what is this?
    deriving (Show, Read, Eq)

data LDeclaration =
    DType Bool (Maybe TypeParameters) Identifier
  | DLogic Bool Identifiers Type
  | DFunction Identifier LogicBinders Type Term
  | DPredicate Identifier LogicBinders Predicate
  | DAxiom Identifier Predicate
  | DGoal Identifier Predicate
    deriving (Show, Read, Eq)

data LogicType =
    Prop LogicArgTypes
  | LTArrow LogicArgTypes Type
    deriving (Show, Read, Eq)

data LogicArgType = LATPrim Type | LATArray Type
    deriving (Show, Read, Eq)

data SimpleValueType = 
    SVTPrim Type
  | SVTRef Type
  | SVTArray Type
    deriving (Show, Read, Eq)

data ValueType = 
    Simple SimpleValueType
  | VTArrow SimpleValueType ComputationType
  | VTLArrow Identifier SimpleValueType ComputationType
    deriving (Show, Read, Eq)

data ComputationType =
    CT (Maybe Pre) (Maybe Identifier) ValueType Effects (Maybe Post)
  | CTVT ValueType
    deriving (Show, Read, Eq)

data Prog =
    PConst Constant
  | PIdent Identifier
  | RefAccess Identifier
  | Assign Identifier Prog
  | ArrayAccess Identifier Prog
  | ArrayAssign Identifier Prog Prog
  | Infix Prog InfixOp Prog
  | Symm Prog
  | Not Prog
  | LetIn Identifier Prog Prog
  | LetInRef Identifier Prog Prog
  | ProgIfThenElse Prog Prog (Maybe Prog)
  | While Prog LoopAnnot Prog
  | Seq Prog Prog
--  | X Identifier Prog -- what is this?
  | Assert Assertions Prog
  | PPre Pre Prog
  | PPost1 Prog Post
  | PPost2 Prog Post
  | Fun Binders Prog
  | LetBind Identifier Binders Prog Prog
  | LetRec RecFun (Maybe Prog)
  | App Prog Prog
  | Raise1 Identifier (Maybe ValueType)
  | Raise2 Identifier Prog (Maybe ValueType)
  | TryWith Prog Handlers
  | Absurd (Maybe ValueType)
  | Block Prog -- is it necessary?
    deriving (Show, Read, Eq)

data InfixOp = OpPlus | OpMinus | OpMult | OpDiv | OpRem | OpEq | OpNEq | OpL | OpLE | OpG | OpGE | OpOr | OpAnd
    deriving (Show, Read, Eq)

data Handler = 
    Hand1 Identifier Prog
  | Hand2 Identifier Identifier Prog
    deriving (Show, Read, Eq)

data Declaration = 
    Let Identifier (Maybe Binders) Prog
  | DLetRec RecFun
  | Parameter Bool Identifiers ValueType -- one or more Identifier
  | Exception Identifier (Maybe Type)
  | L LDeclaration
    deriving (Show, Read, Eq)
