{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Propellor.EnsureProperty
        ( ensureProperty
        , property'
        , OuterMetaTypesWitness
        , EnsurePropertyAllowed
        ) where

import Propellor.Types
import Propellor.Types.Core
import Propellor.Types.MetaTypes
import Propellor.Exception

import GHC.TypeLits
import GHC.Exts (Constraint)
import Data.Type.Bool
import Data.Monoid
import Prelude

-- | For when code running in the Propellor monad needs to ensure a
-- Property.
--
-- Use `property'` to get the `OuterMetaTypesWithness`. For example:
--
-- > foo = Property Debian
-- > foo = property' "my property" $ \w -> do
-- > 	ensureProperty w (aptInstall "foo")
--
-- The type checker will prevent using ensureProperty with a property
-- that does not support the target OSes needed by the OuterMetaTypesWitness.
-- In the example above, aptInstall must support Debian, since foo
-- is supposed to support Debian.
--
-- The type checker will also prevent using ensureProperty with a property
-- with HasInfo in its MetaTypes. Doing so would cause the `Info` associated
-- with the property to be lost.
ensureProperty
        ::
                -- -Wredundant-constraints is turned off because
                -- this constraint appears redundant, but is actually
                -- crucial.
                ( EnsurePropertyAllowed inner outer)
        => OuterMetaTypesWitness outer
        -> Property (MetaTypes inner)
        -> Propellor Result
ensureProperty _ = maybe (return NoChange) catchPropellor . getSatisfy

type family EnsurePropertyAllowed inner outer :: Constraint where
        EnsurePropertyAllowed inner outer = 'True ~
                ((EnsurePropertyNoInfo inner)
                        &&
                (EnsurePropertyTargetOSMatches inner outer))

type family EnsurePropertyNoInfo (l :: [a]) :: Bool where
        EnsurePropertyNoInfo '[] = 'True
        EnsurePropertyNoInfo (t ': ts) = If (Not (t `EqT` 'WithInfo))
                (EnsurePropertyNoInfo ts)
                (TypeError ('Text "Cannot use ensureProperty with a Property that HasInfo."))

type family EnsurePropertyTargetOSMatches inner outer where
        EnsurePropertyTargetOSMatches inner outer =
                If (Targets outer `IsSubset` Targets inner)
                        'True
                        (IfStuck (Targets outer)
                                (DelayError
                                        ('Text "ensureProperty outer Property type is not able to be inferred here."
                                         ':$$: 'Text "Consider adding a type annotation."
                                        )
                                )
                                (DelayErrorFcf
                                        ('Text "ensureProperty inner Property is missing support for: "
                                         ':$$: PrettyPrintMetaTypes (Difference (Targets outer) (Targets inner))
                                        )
                                )
                        )

-- | Constructs a property, like `property`, but provides its
-- `OuterMetaTypesWitness`.
property'
        :: SingI metatypes
        => Desc
        -> (OuterMetaTypesWitness metatypes -> Propellor Result)
        -> Property (MetaTypes metatypes)
property' d a =
        let p = Property sing d (Just (a (outerMetaTypesWitness p))) mempty mempty
        in p

-- | Used to provide the metatypes of a Property to calls to 
-- 'ensureProperty` within it.
newtype OuterMetaTypesWitness metatypes = OuterMetaTypesWitness (MetaTypes metatypes)

outerMetaTypesWitness :: Property (MetaTypes l) -> OuterMetaTypesWitness l
outerMetaTypesWitness (Property metatypes _ _ _ _) = OuterMetaTypesWitness metatypes