--
-- Copyright 2014, General Dynamics C4 Systems
--
-- This software may be distributed and modified according to the terms of
-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
-- See "LICENSE_GPLv2.txt" for details.
--
-- @TAG(GD_GPL)
--

name:                   SEL4
version:                1.4-pre
cabal-version:          >= 1.18
build-type:             Custom
license:                GPL
author:                 Philip Derrin et. al., NICTA
synopsis:               Executable specification for the seL4 Kernel
tested-with:            GHC == 7.8.3

Flag FFI
    description:        Include the C language bindings
    default:            True

Flag ArchArm
    description:        Include ARM modules and platforms
    default:            False

Flag ArchArmHyp
    description:        Include ARM (with Hypervisor Extensions) modules and platforms
    default:            False

Library
    exposed-modules:        SEL4
                            SEL4.Machine.Target
    -- Newer mtl's cause old APIs to be deprecated, which fails -Werror.
    -- base-4.8 (ghc 7.10) exports conflicting name Prelude.Word.
    build-depends:          mtl==2.1.3.1, base==4.7.*, array, containers, transformers

    if flag(FFI)
    -- FFIBindings currently relies on POSIX signal handlers.  This could
    -- be fixed.
        build-depends:      unix
        exposed-modules:    Simulation.FFIBindings
        include-dirs:       include
        install-includes:   sel4model.h gic.h
                            dist/build/Simulation/FFIBindings_stub.h
    else
        build-depends:      unix
        include-dirs:       include

    other-modules:          SEL4.API
                            SEL4.API.Syscall
                            SEL4.API.Faults
                            SEL4.API.Failures
                            SEL4.API.Types
                            SEL4.API.Types.Universal
                            SEL4.API.Invocation
                            SEL4.API.InvocationLabels
                            SEL4.Kernel
                            SEL4.Kernel.BootInfo
                            SEL4.Kernel.VSpace
                            SEL4.Kernel.CSpace
                            SEL4.Kernel.Init
                            SEL4.Kernel.Thread
                            SEL4.Kernel.FaultHandler
                            SEL4.Kernel.Hypervisor
                            SEL4.Object
                            SEL4.Object.ObjectType
                            SEL4.Object.CNode
                            SEL4.Object.Endpoint
                            SEL4.Object.TCB
                            SEL4.Object.Instances
                            SEL4.Object.Structures
                            SEL4.Object.Interrupt
                            SEL4.Object.Notification
                            SEL4.Object.Untyped
                            SEL4.Model
                            SEL4.Model.StateData
                            SEL4.Model.PSpace
                            SEL4.Model.Failures
                            SEL4.Model.Preemption
                            SEL4.Model.Syscall
                            SEL4.Machine
                            SEL4.Machine.RegisterSet
                            SEL4.Machine.Hardware
                            SEL4.Config
                            Data.BinaryTree
                            Data.Helpers

                            SEL4.Machine.Hardware.GICInterface
                            SEL4.Machine.Hardware.MCTInterface
                            SEL4.Machine.Hardware.MPTimerInterface
    if flag(ArchArm)
        other-modules:
                            SEL4.Machine.Hardware.ARM.KZM
                            SEL4.Machine.Hardware.ARM.Exynos4210
                            SEL4.Machine.Hardware.ARM.Sabre
                            SEL4.Machine.Hardware.ARM.Callbacks

                            SEL4.API.Types.ARM
                            SEL4.API.InvocationLabels.ARM
                            SEL4.API.Invocation.ARM
                            SEL4.API.Faults.ARM
                            SEL4.API.Failures.ARM
                            SEL4.Kernel.VSpace.ARM
                            SEL4.Kernel.Thread.ARM
                            SEL4.Kernel.Hypervisor.ARM
                            SEL4.Object.ObjectType.ARM
                            SEL4.Object.Structures.ARM
                            SEL4.Object.Interrupt.ARM
                            SEL4.Object.Instances.ARM
                            SEL4.Object.TCB.ARM
                            SEL4.Model.StateData.ARM
                            SEL4.Machine.RegisterSet.ARM
                            SEL4.Machine.Hardware.ARM

    -- FIXME ideally ARMHYP will share code with the main ARM development,
    -- but when doing an architecture port we want to make sure we are doing a
    -- full pass over the Haskell kernel, touching all files
    -- TODO consolidate later
    if flag(ArchArmHyp)
        other-modules:
                            SEL4.Machine.Hardware.ARM_HYP.TK1
                            SEL4.Machine.Hardware.ARM_HYP.Callbacks

                            SEL4.API.Types.ARM_HYP
                            SEL4.API.InvocationLabels.ARM_HYP
                            SEL4.API.Invocation.ARM_HYP
                            SEL4.API.Faults.ARM_HYP
                            SEL4.API.Failures.ARM_HYP
                            SEL4.Kernel.VSpace.ARM_HYP
                            SEL4.Kernel.Thread.ARM_HYP
                            SEL4.Kernel.Hypervisor.ARM_HYP
                            SEL4.Object.ObjectType.ARM_HYP
                            SEL4.Object.Structures.ARM_HYP
                            SEL4.Object.Interrupt.ARM_HYP
                            SEL4.Object.Instances.ARM_HYP
                            SEL4.Object.VCPU.ARM_HYP
                            SEL4.Object.TCB.ARM_HYP
                            SEL4.Model.StateData.ARM_HYP
                            SEL4.Machine.RegisterSet.ARM_HYP
                            SEL4.Machine.Hardware.ARM_HYP

    else
        -- FIXME: should be a flag also, or some other way to conditionally compile
        -- Setup.hs hooks can handle this, but do we want to do that?
        other-modules:

                            SEL4.API.Types.X64
                            SEL4.API.InvocationLabels.X64
                            SEL4.API.Invocation.X64
                            SEL4.Kernel.VSpace.X64
                            SEL4.Kernel.Thread.X64
                            SEL4.Object.ObjectType.X64
                            SEL4.Object.Structures.X64
                            SEL4.Object.Interrupt.X64
                            SEL4.Object.Instances.X64
                            SEL4.Object.IOPort.X64
                            SEL4.Object.TCB.X64
                            SEL4.Model.StateData.X64
                            SEL4.Machine.RegisterSet.X64
                            SEL4.Machine.Hardware.X64

                            SEL4.Machine.Hardware.X64.PC99

    hs-source-dirs:         src
    ghc-prof-options:       -auto-all -prof -fprof-auto
    ghc-options:            -Wall -Werror -O2 -fno-warn-unused-do-bind
                            -fno-warn-missing-signatures -fno-warn-orphans
                            -fno-spec-constr -fno-warn-name-shadowing
                            -fno-warn-unrecognised-pragmas
                            -fno-warn-unused-binds

    cpp-options:
                            -- set via Setup.hs hook

    Default-Language: Haskell98