{-# OPTIONS -fglasgow-exts #-}

module Why.SyntaxFlattened where

import Data.Generics

type LabIdentifier  = (String,Maybe String) -- what is this?
type Identifier	    = String
type Terms	    = [WhyF]
type Identifiers    = [Identifier]
type Triggers	    = [Trigger]
type Trigger	    = [WhyF] -- one or more WhyF
type Types	    = [WhyF]
type LogicBinder    = (Identifier, WhyF)
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	    = (WhyF, Maybe Identifier)
type Binders	    = [(Identifier, WhyF)]
type RecFun	    = (Identifier, Binders, WhyF, Maybe WfArg, WhyF)
type LoopAnnot	    = (Assertion, Maybe WfArg)
type WfArg	    = (WhyF, Maybe Identifier)
type Why	    = [WhyF]
type LogicBinders   = [LogicBinder]
type LogicArgTypes  = [WhyF]
type Assertions	    = [Assertion]
type Handlers	    = [WhyF]

data WhyF = 
  Const WhyF
  | Sum WhyF WhyF
  | Sub WhyF WhyF
  | Mult WhyF WhyF
  | Div WhyF WhyF
  | Rem WhyF WhyF
  | TNegation WhyF
  | TVar LabIdentifier
  | TFunction Identifier Terms -- one or more WhyF
  | TArrayAccess LabIdentifier WhyF
  | TOld Identifier
  | TIfThenElse WhyF WhyF WhyF
  | TResult

-- data WhyF =
  | IntConst Int
  | RealConst Float
  | BoolConst Bool
  | Void

-- data WhyF = 
  | PredTrue
  | PredFalse
  | PVar Identifier
  | PFunction Identifier Terms -- one or more WhyF
  | Equal WhyF WhyF
  | Diff WhyF WhyF
  | Lesser WhyF WhyF
  | LessEq WhyF WhyF
  | Greater WhyF WhyF
  | GreatEq WhyF WhyF
  | PNegation WhyF
  | Conj WhyF WhyF
  | Disj WhyF WhyF
  | Imp WhyF WhyF
  | Equiv WhyF WhyF
  | PIfThenElse WhyF WhyF WhyF
  | Forall Identifiers WhyF Triggers WhyF -- one or more Identifier, Trigger
  | Exists Identifiers WhyF WhyF
--  | X Identifier String WhyF -- what is this?

-- data WhyF = 
  | TInt 
  | TBool 
  | TReal 
  | TUnit 
  | User Identifier
--  | X Identifier -- what is this?
--  | Y WhyF Identifier -- what is this?
--  | Z Types Identifier -- what is this?

-- data WhyF =
  | DType Bool (Maybe TypeParameters) Identifier
  | DLogic Bool Identifiers WhyF
  | DFunction Identifier LogicBinders WhyF WhyF
  | DPredicate Identifier LogicBinders WhyF
  | DAxiom Identifier WhyF
  | DGoal Identifier WhyF

-- data WhyF =
  | Prop LogicArgTypes
  | LTArrow LogicArgTypes WhyF

-- data WhyF = 
  | LATPrim WhyF | LATArray WhyF

-- data WhyF = 
  | SVTPrim WhyF
  | SVTRef WhyF
  | SVTArray WhyF

-- data WhyF = 
  | Simple WhyF
  | VTArrow WhyF WhyF
  | VTLArrow Identifier WhyF WhyF

-- data WhyF =
  | CT (Maybe Pre) (Maybe Identifier) WhyF Effects (Maybe Post)
  | CTVT WhyF

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

-- data WhyF = 
  | OpPlus | OpMinus | OpMult | OpDiv | OpRem | OpEq | OpNEq | OpL | OpLE | OpG | OpGE | OpOr | OpAnd

-- data WhyF = 
  | Hand1 Identifier WhyF
  | Hand2 Identifier Identifier WhyF

-- data WhyF = 
  | Let Identifier (Maybe Binders) WhyF
  | DLetRec RecFun
  | Parameter Bool Identifiers WhyF -- one or more Identifier
  | Exception Identifier (Maybe WhyF)
  | L WhyF
    deriving (Typeable, Data, Show, Read, Eq)
