{-# LANGUAGE CPP, DeriveDataTypeable #-}
module Language.Java.Paragon.Syntax where

#ifdef __GLASGOW_HASKELL__
#ifdef BASE4
import Data.Data
#else
import Data.Generics (Data(..),Typeable(..))
#endif
#endif

-----------------------------------------------------------------------
-- Packages


-- | A compilation unit is the top level syntactic goal symbol of a Java program.
data CompilationUnit = CompilationUnit (Maybe PackageDecl) [ImportDecl] [TypeDecl]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-- | A package declaration appears within a compilation unit to indicate the package to which the compilation unit belongs.
data PackageDecl = PackageDecl Name
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | An import declaration allows a static member or a named type to be referred to by a single unqualified identifier. 
--   The first argument signals whether the declaration only imports static members.
--   The last argument signals whether the declaration brings all names in the named type or package, or only brings
--   a single name into scope.
data ImportDecl
    = ImportDecl Bool {- static? -} Name Bool {- .*? -}
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-----------------------------------------------------------------------
-- Declarations

-- | A type declaration declares a class type or an interface type.
data TypeDecl
    = ClassTypeDecl ClassDecl
    | InterfaceTypeDecl InterfaceDecl
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A class declaration specifies a new named reference type.
data ClassDecl
    = ClassDecl [Modifier] Ident [TypeParam] (Maybe RefType) [RefType] ClassBody
    | EnumDecl  [Modifier] Ident                             [RefType] EnumBody
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A class body may contain declarations of members of the class, that is, 
--   fields, classes, interfaces and methods. 
--   A class body may also contain instance initializers, static 
--   initializers, and declarations of constructors for the class.
data ClassBody = ClassBody [Decl]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | The body of an enum type may contain enum constants.
data EnumBody = EnumBody [EnumConstant] [Decl]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | An enum constant defines an instance of the enum type.
data EnumConstant = EnumConstant Ident [Argument] (Maybe ClassBody)
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | An interface declaration introduces a new reference type whose members 
--   are classes, interfaces, constants and abstract methods. This type has 
--   no implementation, but otherwise unrelated classes can implement it by 
--   providing implementations for its abstract methods.
data InterfaceDecl
    = InterfaceDecl [Modifier] Ident [TypeParam] [RefType] InterfaceBody
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | The body of an interface may declare members of the interface.
data InterfaceBody
    = InterfaceBody [MemberDecl]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A declaration is either a member declaration, or a declaration of an
--   initializer, which may be static.
data Decl
    = MemberDecl MemberDecl
    | InitDecl Bool Block
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-- | A class or interface member can be an inner class or interface, a field or
--   constant, or a method or constructor. An interface may only have as members
--   constants (not fields), abstract methods, and no constructors.
data MemberDecl
    -- | The variables of a class type are introduced by field declarations.
    = FieldDecl [Modifier] Type [VarDecl]
    -- | A method declares executable code that can be invoked, passing a fixed number of values as arguments.
    | MethodDecl      [Modifier] [TypeParam] (Maybe Type) Ident [FormalParam] [ExceptionSpec] MethodBody
    -- | A constructor is used in the creation of an object that is an instance of a class.
    | ConstructorDecl [Modifier] [TypeParam]              Ident [FormalParam] [ExceptionSpec] ConstructorBody
    -- | A member class is a class whose declaration is directly enclosed in another class or interface declaration.
    | MemberClassDecl ClassDecl
    -- | A member interface is an interface whose declaration is directly enclosed in another class or interface declaration.
    | MemberInterfaceDecl InterfaceDecl

-- Paragon
    -- | A lock declaration is a special kind of field declaration.
    | LockDecl [Modifier]  Ident [Maybe Ident] (Maybe LockProperties)
    -- | A policy declaration - should be a field decl really.
    | PolicyDecl [Modifier] Ident Policy
{-    -- | An actor declaration is a special kind of field declaration.
    | ActorDecl [Modifier] Ident (Maybe VarInit) -}
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- int x; => VarDecl (VarId "x") Nothing
-- int x = 1; => VarDecl (VarId "x") (Just ...)
-- | A declaration of a variable, which may be explicitly initialized.
data VarDecl
    = VarDecl VarDeclId (Maybe VarInit)
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | The name of a variable in a declaration, which may be an array.
data VarDeclId
    = VarId Ident
    | VarDeclArray VarDeclId        
    -- ^ Multi-dimensional arrays are represented by nested applications of 'VarDeclArray' (Deprecated)
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | Explicit initializer for a variable declaration.
data VarInit
    = InitExp Exp
    | InitArray ArrayInit
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A formal parameter in method declaration. The last parameter
--   for a given declaration may be marked as variable arity,
--   indicated by the boolean argument.
data FormalParam = FormalParam [Modifier] Type Bool VarDeclId
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A method body is either a block of code that implements the method or simply a 
--   semicolon, indicating the lack of an implementation (modelled by 'Nothing').
data MethodBody = MethodBody (Maybe Block)
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | The first statement of a constructor body may be an explicit invocation of
--   another constructor of the same class or of the direct superclass.
data ConstructorBody = ConstructorBody (Maybe ExplConstrInv) [BlockStmt]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | An explicit constructor invocation invokes another constructor of the 
--   same class, or a constructor of the direct superclass, which may
--   be qualified to explicitly specify the newly created object's immediately 
--   enclosing instance. 
data ExplConstrInv
    = ThisInvoke             [NonWildTypeArgument] [Argument]
    | SuperInvoke            [NonWildTypeArgument] [Argument]
    | PrimarySuperInvoke Exp [NonWildTypeArgument] [Argument]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-- | A modifier specifying properties of a given declaration. In general only
--   a few of these modifiers are allowed for each declaration type, for instance
--   a member type declaration may only specify one of public, private or protected.
data Modifier
    = Public
    | Private
    | Protected
    | Abstract
    | Final
    | Static
    | StrictFP
    | Transient
    | Volatile
    | Native

    | Typemethod
    | Reflexive
    | Transitive
    | Commutative

    | Reads  Policy
    | Writes Policy
    | Opens   [Lock]
    | Closes  [Lock]
    | Expects [Lock]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

{- 
data LockExp 
    = LockExp [Lock]
    | LockVar Ident
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif
-}             

-----------------------------------------------------------------------
-- Statements

-- | A block is a sequence of statements, local class declarations 
--   and local variable declaration statements within braces.
data Block = Block [BlockStmt]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif



-- | A block statement is either a normal statement, a local 
--   class declaration or a local variable declaration.
data BlockStmt
    = BlockStmt Stmt
    | LocalClass ClassDecl
    | LocalVars [Modifier] Type [VarDecl]

-- Paragon
    | LocalLock [Modifier]  Ident [Maybe Ident] (Maybe LockProperties)
    | LocalPolicy [Modifier] Ident Policy
{-    | LocalActor [Modifier] Ident (Maybe VarInit) -}
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-- | A Java statement.
data Stmt
    -- | A statement can be a nested block.
    = StmtBlock Block
    -- | The @if-then@ statement allows conditional execution of a statement.
    | IfThen Exp Stmt
    -- | The @if-then-else@ statement allows conditional choice of two statements, executing one or the other but not both.
    | IfThenElse Exp Stmt Stmt
    -- | The @while@ statement executes an expression and a statement repeatedly until the value of the expression is false.
    | While Exp Stmt
    -- | The basic @for@ statement executes some initialization code, then executes an expression, a statement, and some 
    --   update code repeatedly until the value of the expression is false.
    | BasicFor (Maybe ForInit) (Maybe Exp) (Maybe [Exp]) Stmt
    -- | The enhanced @for@ statement iterates over an array or a value of a class that implements the @iterator@ interface.
    | EnhancedFor [Modifier] Type Ident Exp Stmt
    -- | An empty statement does nothing.
    | Empty
    -- | Certain kinds of expressions may be used as statements by following them with semicolons:
    --   assignments, pre- or post-inc- or decrementation, method invocation or class instance
    --   creation expressions.
    | ExpStmt Exp
    -- | An assertion is a statement containing a boolean expression, where an error is reported if the expression 
    --   evaluates to false.
    | Assert Exp (Maybe Exp)
    -- | The switch statement transfers control to one of several statements depending on the value of an expression.
    | Switch Exp [SwitchBlock]
    -- | The @do@ statement executes a statement and an expression repeatedly until the value of the expression is false.
    | Do Stmt Exp
    -- | A @break@ statement transfers control out of an enclosing statement.
    | Break (Maybe Ident)
    -- | A @continue@ statement may occur only in a while, do, or for statement. Control passes to the loop-continuation 
    --   point of that statement.
    | Continue (Maybe Ident)
    -- A @return@ statement returns control to the invoker of a method or constructor.
    | Return (Maybe Exp)
    -- | A @synchronized@ statement acquires a mutual-exclusion lock on behalf of the executing thread, executes a block, 
    --   then releases the lock. While the executing thread owns the lock, no other thread may acquire the lock.
    | Synchronized Exp Block
    -- | A @throw@ statement causes an exception to be thrown. 
    | Throw Exp
    -- | A try statement executes a block. If a value is thrown and the try statement has one or more catch clauses that 
    --   can catch it, then control will be transferred to the first such catch clause. If the try statement has a finally 
    --   clause, then another block of code is executed, no matter whether the try block completes normally or abruptly, 
    --   and no matter whether a catch clause is first given control.
    | Try Block [Catch] (Maybe {- finally -} Block)
    -- | Statements may have label prefixes.
    | Labeled Ident Stmt
    
-- Paragon    
    -- | Locks can be opened or closed.
    | Open  Lock
    | Close Lock
    | OpenBlock Lock Block
    | CloseBlock Lock Block
{-    -- A @when@ statement is a variant of @if@ that only tests whether locks are open.
    | WhenThen     Lock Stmt
    | WhenThenElse Lock Stmt Stmt    -}
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | If a value is thrown and the try statement has one or more catch clauses that can catch it, then control will be 
--   transferred to the first such catch clause.
data Catch = Catch FormalParam Block
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A block of code labelled with a @case@ or @default@ within a @switch@ statement.
data SwitchBlock
    = SwitchBlock SwitchLabel [BlockStmt]    
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A label within a @switch@ statement. 
data SwitchLabel
    -- | The expression contained in the @case@ must be a 'Lit' or an @enum@ constant.
    = SwitchCase Exp
    | Default
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | Initialization code for a basic @for@ statement.
data ForInit
    = ForLocalVars [Modifier] Type [VarDecl]
    | ForInitExps [Exp]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | An exception type has to be a class type or a type variable.
type ExceptionType = RefType -- restricted to ClassType or TypeVariable

data ExceptionSpec = ExceptionSpec [Modifier] ExceptionType
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-----------------------------------------------------------------------
-- Expressions

-- | Arguments to methods and constructors are expressions.
type Argument = Exp

-- | A Java expression.
data Exp
    -- | A literal denotes a fixed, unchanging value.
    = Lit Literal
    -- | A class literal, which is an expression consisting of the name of a class, interface, array, 
    --   or primitive type, or the pseudo-type void (modelled by 'Nothing'), followed by a `.' and the token class.
    | ClassLit (Maybe Type)
    -- | The keyword @this@ denotes a value that is a reference to the object for which the instance method
    --   was invoked, or to the object being constructed.
    | This
    -- | Any lexically enclosing instance can be referred to by explicitly qualifying the keyword this.
    | ThisClass Name
    -- | A parenthesized expression is a primary expression whose type is the type of the contained expression 
    --   and whose value at run time is the value of the contained expression. If the contained expression 
    --   denotes a variable then the parenthesized expression also denotes that variable.
    | Paren Exp
    -- | A class instance creation expression is used to create new objects that are instances of classes.
    -- | The first argument is a list of non-wildcard type arguments to a generic constructor.
    --   What follows is the type to be instantiated, the list of arguments passed to the constructor, and
    --   optionally a class body that makes the constructor result in an object of an /anonymous/ class.
    | InstanceCreation [TypeArgument] ClassType [Argument] (Maybe ClassBody)
    -- | A qualified class instance creation expression enables the creation of instances of inner member classes 
    --   and their anonymous subclasses.
    | QualInstanceCreation Exp [TypeArgument] Ident [Argument] (Maybe ClassBody)
    -- | An array instance creation expression is used to create new arrays. The last argument denotes the number
    --   of dimensions that have no explicit length given. These dimensions must be given last.
    | ArrayCreate Type [Exp] Int
    -- | An array instance creation expression may come with an explicit initializer. Such expressions may not
    --   be given explicit lengths for any of its dimensions.
    | ArrayCreateInit Type Int ArrayInit
    -- | A field access expression.
    | FieldAccess FieldAccess
    -- | A method invocation expression.
    | MethodInv MethodInvocation
    -- | An array access expression refers to a variable that is a component of an array.
    | ArrayAccess ArrayIndex
    -- | An expression name, e.g. a variable.
    | ExpName Name
    -- | Post-incrementation expression, i.e. an expression followed by @++@.
    | PostIncrement Exp
    -- | Post-decrementation expression, i.e. an expression followed by @--@.
    | PostDecrement Exp
    -- | Pre-incrementation expression, i.e. an expression preceded by @++@.
    | PreIncrement  Exp
    -- | Pre-decrementation expression, i.e. an expression preceded by @--@.
    | PreDecrement  Exp
    -- | Unary plus, the promotion of the value of the expression to a primitive numeric type.
    | PrePlus  Exp
    -- | Unary minus, the promotion of the negation of the value of the expression to a primitive numeric type.
    | PreMinus Exp
    -- | Unary bitwise complementation: note that, in all cases, @~x@ equals @(-x)-1@.
    | PreBitCompl Exp
    -- | Logical complementation of boolean values.
    | PreNot  Exp
    -- | A cast expression converts, at run time, a value of one numeric type to a similar value of another 
    --   numeric type; or confirms, at compile time, that the type of an expression is boolean; or checks, 
    --   at run time, that a reference value refers to an object whose class is compatible with a specified 
    --   reference type.
    | Cast  Type Exp
    -- | The application of a binary operator to two operand expressions.
    | BinOp Exp Op Exp
    -- | Testing whether the result of an expression is an instance of some reference type.
    | InstanceOf Exp RefType
    -- | The conditional operator @? :@ uses the boolean value of one expression to decide which of two other 
    --   expressions should be evaluated.
    | Cond Exp Exp Exp
    -- | Assignment of the result of an expression to a variable.
    | Assign Lhs AssignOp Exp

-- Paragon
    | PolicyExp PolicyExp --PolicyLit
--    | PolicyOf Ident
    | LockExp Lock
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A literal denotes a fixed, unchanging value.
data Literal
    = Int Integer
    | Word Integer
    | Float Double
    | Double Double
    | Boolean Bool
    | Char Char
    | String String
    | Null
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A binary infix operator.
data Op = Mult | Div | Rem | Add | Sub | LShift | RShift | RRShift
        | LThan | GThan | LThanE | GThanE | Equal | NotEq
        | And | Or | Xor | CAnd | COr
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | An assignment operator.
data AssignOp = EqualA | MultA | DivA | RemA | AddA | SubA
              | LShiftA | RShiftA | RRShiftA | AndA | XorA | OrA
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | The left-hand side of an assignment expression. This operand may be a named variable, such as a local 
--   variable or a field of the current object or class, or it may be a computed variable, as can result from 
--   a field access or an array access.
data Lhs
    = NameLhs Name          -- ^ Assign to a variable
    | FieldLhs FieldAccess  -- ^ Assign through a field access
    | ArrayLhs ArrayIndex   -- ^ Assign to an array
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | Array access
data ArrayIndex = ArrayIndex Exp Exp    -- ^ Index into an array
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A field access expression may access a field of an object or array, a reference to which is the value 
--   of either an expression or the special keyword super.
data FieldAccess
    = PrimaryFieldAccess Exp Ident      -- ^ Accessing a field of an object or array computed from an expression.
    | SuperFieldAccess Ident            -- ^ Accessing a field of the superclass.
    | ClassFieldAccess Name Ident       -- ^ Accessing a (static) field of a named class.
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-- | A method invocation expression is used to invoke a class or instance method.
data MethodInvocation
    -- | Invoking a specific named method. 
    = MethodCall Name [Argument]
    -- | Invoking a method of a class computed from a primary expression, giving arguments for any generic type parameters.
    | PrimaryMethodCall Exp [NonWildTypeArgument] Ident [Argument]
    -- | Invoking a method of the super class, giving arguments for any generic type parameters.
    | SuperMethodCall [NonWildTypeArgument] Ident [Argument]
    -- | Invoking a method of the superclass of a named class, giving arguments for any generic type parameters.
    | ClassMethodCall Name [NonWildTypeArgument] Ident [Argument]
    -- | Invoking a method of a named type, giving arguments for any generic type parameters.
    | TypeMethodCall  Name [NonWildTypeArgument] Ident [Argument]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | An array initializer may be specified in a declaration, or as part of an array creation expression, creating an 
--   array and providing some initial values
data ArrayInit
    = ArrayInit [VarInit]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-----------------------------------------------------------------------
-- Types


-- | There are two kinds of types in the Java programming language: primitive types and reference types.
data Type
    = PrimType PrimType
    | RefType RefType
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | There are three kinds of reference types: class types, interface types, and array types. 
--   Reference types may be parameterized with type arguments.
--   Type variables are introduced by generic type parameters.
data RefType
    = ClassRefType ClassType
    | TypeVariable Ident
    | ArrayType Type (Maybe Policy)
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A class or interface type consists of a type declaration specifier, 
--   optionally followed by type arguments (in which case it is a parameterized type).
data ClassType
    = ClassType [(Ident, [TypeArgument])]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | Type arguments may be either reference types or wildcards.
data TypeArgument
    = Wildcard (Maybe WildcardBound)
    | ActualArg NonWildTypeArgument
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

data NonWildTypeArgument
    = ActualType RefType -- also covers policies and actors, which must be names.
    | ActualPolicy Policy
    | ActualActor  Name
    | ActualLockState [Lock]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-- | Wildcards may be given explicit bounds, either upper (@extends@) or lower (@super@) bounds.
data WildcardBound
    = ExtendsBound RefType
    | SuperBound RefType
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A primitive type is predefined by the Java programming language and named by its reserved keyword.
data PrimType
    = BooleanT
    | ByteT
    | ShortT
    | IntT
    | LongT
    | CharT
    | FloatT
    | DoubleT
-- Paragon
    | ActorT 
    | PolicyT
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-- | A class is generic if it declares one or more type variables. These type variables are known 
--   as the type parameters of the class.
--   Paragon adds three new forms - actor, policy and lockstate parameters.
data TypeParam = TypeParam Ident [RefType]
-- Paragon
               | ActorParam Ident
               | PolicyParam Ident
               | LockStateParam Ident
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-----------------------------------------------------------------------
-- Paragon

type Policy = Exp

-- | A policy is a conjunction (set) of clauses, represented as a list.
--data PolicyLit = PolicyLit [Clause Actor]
data PolicyExp = PolicyLit [Clause Actor]
               | PolicyOf Ident
               | PolicyTypeVar Ident
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A lock property is a potentially recursive policy with an atom head.
data LockProperties = LockProperties [Clause Atom]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A clause of the form Sigma => a, where a is an actor and Sigma a set of
--   locks/atomic predicates that must be open/true.
data Clause a = Clause
    { cHead  :: a
    , cBody  :: [Atom]
    }
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | An actor variable, either forall-quantified within the current clause, or
--   free and thus concrete w.r.t. the policy under scrutiny.
data Actor = Actor ActorName    -- ^ Free actor variables
           | Var Ident          -- ^ Quantified actor variables
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

data ActorName = ActorName Name     -- ^ A free actor variable
               | ActorTypeVar Ident -- ^ A free actor type parameter
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A lock is an atomic n-ary predicate.
data Atom = Atom Name [Actor]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

data Lock = Lock Name [ActorName] | LockVar Ident
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif


-----------------------------------------------------------------------
-- Names and identifiers

-- | A single identifier.
data Ident = Ident String
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif

-- | A name, i.e. a period-separated list of identifiers.
data Name = Name [Ident]
#ifdef __GLASGOW_HASKELL__
  deriving (Eq,Ord,Show,Typeable,Data)
#else
  deriving (Eq,Ord,Show)
#endif