{-# OPTIONS -fglasgow-exts #-}

module LISS.Syntax where

import Data.Generics

data Liss = 
  Liss ProgramName Body 
    deriving (Eq, Show, Typeable, Data)

data Body = 
  Body Declarations Statement 
    deriving (Eq, Show, Typeable, Data)

data Declaration = 
    VarDec Arg
  | SubprogDec [Spec] ProgramName Args Type Body ReturnStat deriving (Eq, Show, Typeable, Data)

data Type = 
    Integer 
  | Boolean 
  | Sequence 
  | Set
  | Array Int 
    deriving (Eq, Show, Typeable, Data)

data Arg = 
  Arg Var Type 
    deriving (Eq, Show, Typeable, Data)

data Statement =
    IntAssign IntVar IntExp
  | SetAssign SetVar SetExp
  | SeqAssign SeqVar SeqExp
  | BoolAssign BoolVar BoolExp
  | ArrayPosAssign ArrayVar IntExp IntExp
  | SequenceS Statement Statement
  | IfThenElse BoolExp Statement Statement
  | While LoopAnnot BoolExp Statement
  | For IntVar IntExp IntExp Step BoolExp Statement
  | ForEach IntVar SeqExp BoolExp Statement
  | Read IntVar
  | Write IntExp
  | WriteString String
  | Skip 
    deriving (Eq, Show, Typeable, Data)

data ReturnStat = 
    ReturnInt IntExp
  | ReturnBool BoolExp
  | ReturnSet SetExp
  | ReturnSeq SeqExp
  | ReturnArray ArrayExp
    deriving (Eq, Show, Typeable, Data)

data IntExp =
    IntConst Int
  | IntVarExp IntVar
  | ArrayAccess ArrayVar IntExp
  | Negative IntExp
  | Sum IntExp IntExp
  | Sub IntExp IntExp
  | Mult IntExp IntExp
  | Div IntExp IntExp
  | Rem IntExp IntExp
  | Head SeqExp
  | IntFunction FName Vars
    deriving (Eq, Show, Typeable, Data)

data BoolExp =
    BoolConst Bool
  | BoolVarExp BoolVar
  | Equal IntExp IntExp
  | Diff IntExp IntExp
  | Lesser IntExp IntExp
  | LessEq IntExp IntExp
  | Greater IntExp IntExp
  | GreatEq IntExp IntExp
  | Negation BoolExp
  | Conj BoolExp BoolExp
  | Disj BoolExp BoolExp
  | Imp BoolExp BoolExp
  | Equiv BoolExp BoolExp
  | EmptySeq SeqExp
  | ElemSet IntExp SetExp
  | BoolFunction FName Vars
    deriving (Eq, Show, Typeable, Data)

data SeqExp =
    SeqVarExp SeqVar
  | SeqConst [IntExp] 
  | SeqNull
  | Tail SeqExp
  | Cons IntExp SeqExp
  | SeqFunction FName Vars
    deriving (Eq, Show, Typeable, Data)

data SetExp =
    SetVarExp SetVar
  | SetConst IntVar BoolExp
  | SetNull
  | Union SetExp SetExp
  | Intersect SetExp SetExp
  | SetFunction FName Vars
    deriving (Eq, Show, Typeable, Data)

data ArrayExp =
    ArrayVarExp ArrayVar
  | ArrayFunction FName Vars
    deriving (Eq, Show, Typeable, Data)

type Var = String
type Args = [Arg]
type Vars = [Var]
type ProgramName = String
type Declarations = [Declaration]
type FName = String
type IntVar = Var
type BoolVar = Var
type SetVar = Var
type SeqVar = Var
type ArrayVar = Var
type Step = Int


-- Annotations
type Identifier = String
type LoopAnnot = (Assertion, Maybe WfArg)
type WfArg = Term -- coupled with a Maybe Identifier?
type Assertion = Predicate -- coupled with a Maybe Identifier?

data Spec = Pre Predicate | Post Predicate
    deriving (Eq, Show, Typeable, Data)

data Term =
    TIntConst Int
  | TIntVar IntVar
  | TArrayAccess String Term
  | TNegative Term
  | TSum Term Term
  | TSub Term Term
  | TMult Term Term
  | TDiv Term Term
  | TRem Term Term
  | THead SeqExp
  | TIntFun FName Vars
  | TOld Var
--  | TOldPos Var Term -- ??
  | Result
    deriving (Eq, Show, Typeable, Data)

data Predicate = 
    PBoolConst Bool
  | PBoolVar BoolVar
  | PEqual Term Term
  | PDiff Term Term
  | PLesser Term Term
  | PLessEq Term Term
  | PGreater Term Term
  | PGreatEq Term Term
  | PNegation Predicate
  | PConj Predicate Predicate
  | PDisj Predicate Predicate
  | PImp Predicate Predicate
  | PEquiv Predicate Predicate
  | PEmptySeq SeqExp
  | PElemSet IntExp SetExp
  | PBoolFunction FName Vars
  | PIfThenElse Term Predicate Predicate
  | Forall Args Predicate
  | Exists Args Predicate
  | ValidIndex ArrayVar IntExp
    deriving (Eq, Show, Typeable, Data)
