{-# 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 :: forall (inner :: [MetaType]) (outer :: [MetaType]).
EnsurePropertyAllowed inner outer =>
OuterMetaTypesWitness outer
-> Property (MetaTypes inner) -> Propellor Result
ensureProperty OuterMetaTypesWitness outer
_ = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return Result
NoChange) forall (m :: * -> *).
(MonadIO m, MonadCatch m) =>
m Result -> m Result
catchPropellor forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p. IsProp p => p -> Maybe (Propellor Result)
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' :: forall {k} (metatypes :: k).
SingI metatypes =>
Desc
-> (OuterMetaTypesWitness metatypes -> Propellor Result)
-> Property (MetaTypes metatypes)
property' Desc
d OuterMetaTypesWitness metatypes -> Propellor Result
a =
	let p :: Property (Sing metatypes)
p = forall metatypes.
metatypes
-> Desc
-> Maybe (Propellor Result)
-> Info
-> [ChildProperty]
-> Property metatypes
Property forall {k} (t :: k). SingI t => Sing t
sing Desc
d (forall a. a -> Maybe a
Just (OuterMetaTypesWitness metatypes -> Propellor Result
a (forall {k} (l :: k).
Property (MetaTypes l) -> OuterMetaTypesWitness l
outerMetaTypesWitness Property (Sing metatypes)
p))) forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
	in Property (Sing metatypes)
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 :: forall {k} (l :: k).
Property (MetaTypes l) -> OuterMetaTypesWitness l
outerMetaTypesWitness (Property MetaTypes l
metatypes Desc
_ Maybe (Propellor Result)
_ Info
_ [ChildProperty]
_) = forall {k} (metatypes :: k).
MetaTypes metatypes -> OuterMetaTypesWitness metatypes
OuterMetaTypesWitness MetaTypes l
metatypes