-- |
--
module Distribution.SPDX.Extra (
  -- * Types
  -- | We don't export the constructors, as they change with Cabal version.
  License,
  LicenseExpression,
  SimpleLicenseExpression,
  LicenseId,
  LicenseExceptionId,

  -- * Logic
  satisfies,
  equivalent,
  ) where

import Control.Monad.SAT
import qualified Data.Map.Strict as Map
import Control.Monad.Trans.Class (lift)
import Data.Map.Strict (Map)
import Control.Monad.Trans.State
import Data.Maybe (isNothing)

import Distribution.SPDX
       (License (..), LicenseExceptionId, LicenseExpression (..), LicenseId,
       SimpleLicenseExpression (..))

-- $setup
-- >>> import Distribution.Parsec (simpleParsec)
-- >>> let unsafeParseExpr e = maybe (error $ "invalid: " ++ e) (id :: License -> License) (simpleParsec e)

-- |
--
-- @⟦ satisfies a b ⟧ ≡ a ≥ b ≡ a ∧ b = b @
--
-- >>> unsafeParseExpr "GPL-3.0-only" `satisfies` unsafeParseExpr "ISC AND MIT"
-- False
--
-- >>> unsafeParseExpr "Zlib" `satisfies` unsafeParseExpr "ISC AND MIT AND Zlib"
-- True
--
-- >>> unsafeParseExpr "(MIT OR GPL-2.0-only)" `satisfies` unsafeParseExpr "(ISC AND MIT)"
-- True
--
-- >>> unsafeParseExpr "(MIT AND GPL-2.0-only)" `satisfies` unsafeParseExpr "(MIT AND GPL-2.0-only)"
-- True
--
-- >>> unsafeParseExpr "(MIT AND GPL-2.0-only)" `satisfies` unsafeParseExpr "(ISC AND GPL-2.0-only)"
-- False
--
satisfies :: License -- ^ package license
          -> License -- ^ license policy
          -> Bool
satisfies :: License -> License -> Bool
satisfies License
a License
b = Maybe () -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ (forall s. SAT s ()) -> Maybe ()
forall a. (forall s. SAT s a) -> Maybe a
runSATMaybe ((forall s. SAT s ()) -> Maybe ())
-> (forall s. SAT s ()) -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (StateT (Map Lic (Lit s)) (SAT s) ()
 -> Map Lic (Lit s) -> SAT s ())
-> Map Lic (Lit s)
-> StateT (Map Lic (Lit s)) (SAT s) ()
-> SAT s ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Map Lic (Lit s)) (SAT s) () -> Map Lic (Lit s) -> SAT s ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Map Lic (Lit s)
forall k a. Map k a
Map.empty (StateT (Map Lic (Lit s)) (SAT s) () -> SAT s ())
-> StateT (Map Lic (Lit s)) (SAT s) () -> SAT s ()
forall a b. (a -> b) -> a -> b
$ do
    Lit s
a' <- License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s. License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
exprToProp License
a StateT (Map Lic (Lit s)) (SAT s) (Prop s)
-> (Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Lit s))
-> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall a b.
StateT (Map Lic (Lit s)) (SAT s) a
-> (a -> StateT (Map Lic (Lit s)) (SAT s) b)
-> StateT (Map Lic (Lit s)) (SAT s) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s))
-> (Prop s -> SAT s (Lit s))
-> Prop s
-> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop s -> SAT s (Lit s)
forall s. Prop s -> SAT s (Lit s)
addDefinition
    Lit s
b' <- License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s. License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
exprToProp License
b StateT (Map Lic (Lit s)) (SAT s) (Prop s)
-> (Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Lit s))
-> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall a b.
StateT (Map Lic (Lit s)) (SAT s) a
-> (a -> StateT (Map Lic (Lit s)) (SAT s) b)
-> StateT (Map Lic (Lit s)) (SAT s) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s))
-> (Prop s -> SAT s (Lit s))
-> Prop s
-> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop s -> SAT s (Lit s)
forall s. Prop s -> SAT s (Lit s)
addDefinition
    SAT s () -> StateT (Map Lic (Lit s)) (SAT s) ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (SAT s () -> StateT (Map Lic (Lit s)) (SAT s) ())
-> SAT s () -> StateT (Map Lic (Lit s)) (SAT s) ()
forall a b. (a -> b) -> a -> b
$ Prop s -> SAT s ()
forall s. Prop s -> SAT s ()
addProp (Prop s -> SAT s ()) -> Prop s -> SAT s ()
forall a b. (a -> b) -> a -> b
$ Prop s -> Prop s
forall a. Neg a => a -> a
neg (Prop s -> Prop s) -> Prop s -> Prop s
forall a b. (a -> b) -> a -> b
$ Lit s -> Prop s
forall s. Lit s -> Prop s
lit Lit s
b' Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
--> Lit s -> Prop s
forall s. Lit s -> Prop s
lit Lit s
a'
    SAT s () -> StateT (Map Lic (Lit s)) (SAT s) ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift SAT s ()
forall s. SAT s ()
solve_

    -- exprToLSLic b `LS.preorder` exprToLSLic a

-- | Check wheather two 'LicenseExpression' are equivalent.
--
-- >>> unsafeParseExpr "(MIT AND GPL-2.0-only)" `equivalent` unsafeParseExpr "(GPL-2.0-only AND MIT)"
-- True
--
-- >>> unsafeParseExpr "MIT" `equivalent` unsafeParseExpr "MIT OR BSD-3-Clause"
-- False
--
equivalent :: License -> License -> Bool
equivalent :: License -> License -> Bool
equivalent License
a License
b = Maybe () -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ (forall s. SAT s ()) -> Maybe ()
forall a. (forall s. SAT s a) -> Maybe a
runSATMaybe ((forall s. SAT s ()) -> Maybe ())
-> (forall s. SAT s ()) -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (StateT (Map Lic (Lit s)) (SAT s) ()
 -> Map Lic (Lit s) -> SAT s ())
-> Map Lic (Lit s)
-> StateT (Map Lic (Lit s)) (SAT s) ()
-> SAT s ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT (Map Lic (Lit s)) (SAT s) () -> Map Lic (Lit s) -> SAT s ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Map Lic (Lit s)
forall k a. Map k a
Map.empty (StateT (Map Lic (Lit s)) (SAT s) () -> SAT s ())
-> StateT (Map Lic (Lit s)) (SAT s) () -> SAT s ()
forall a b. (a -> b) -> a -> b
$ do
    Lit s
a' <- License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s. License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
exprToProp License
a StateT (Map Lic (Lit s)) (SAT s) (Prop s)
-> (Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Lit s))
-> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall a b.
StateT (Map Lic (Lit s)) (SAT s) a
-> (a -> StateT (Map Lic (Lit s)) (SAT s) b)
-> StateT (Map Lic (Lit s)) (SAT s) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s))
-> (Prop s -> SAT s (Lit s))
-> Prop s
-> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop s -> SAT s (Lit s)
forall s. Prop s -> SAT s (Lit s)
addDefinition
    Lit s
b' <- License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s. License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
exprToProp License
b StateT (Map Lic (Lit s)) (SAT s) (Prop s)
-> (Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Lit s))
-> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall a b.
StateT (Map Lic (Lit s)) (SAT s) a
-> (a -> StateT (Map Lic (Lit s)) (SAT s) b)
-> StateT (Map Lic (Lit s)) (SAT s) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s))
-> (Prop s -> SAT s (Lit s))
-> Prop s
-> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prop s -> SAT s (Lit s)
forall s. Prop s -> SAT s (Lit s)
addDefinition
    SAT s () -> StateT (Map Lic (Lit s)) (SAT s) ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (SAT s () -> StateT (Map Lic (Lit s)) (SAT s) ())
-> SAT s () -> StateT (Map Lic (Lit s)) (SAT s) ()
forall a b. (a -> b) -> a -> b
$ Prop s -> SAT s ()
forall s. Prop s -> SAT s ()
addProp (Prop s -> SAT s ()) -> Prop s -> SAT s ()
forall a b. (a -> b) -> a -> b
$ Prop s -> Prop s
forall a. Neg a => a -> a
neg (Prop s -> Prop s) -> Prop s -> Prop s
forall a b. (a -> b) -> a -> b
$ Lit s -> Prop s
forall s. Lit s -> Prop s
lit Lit s
a' Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
<-> Lit s -> Prop s
forall s. Lit s -> Prop s
lit Lit s
b'
    SAT s () -> StateT (Map Lic (Lit s)) (SAT s) ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift SAT s ()
forall s. SAT s ()
solve_

----------------------------------f---------------------------------------------
-- internal
-------------------------------------------------------------------------------

data Lic = Lic !SimpleLicenseExpression !(Maybe LicenseExceptionId)
  deriving (Lic -> Lic -> Bool
(Lic -> Lic -> Bool) -> (Lic -> Lic -> Bool) -> Eq Lic
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Lic -> Lic -> Bool
== :: Lic -> Lic -> Bool
$c/= :: Lic -> Lic -> Bool
/= :: Lic -> Lic -> Bool
Eq, Eq Lic
Eq Lic =>
(Lic -> Lic -> Ordering)
-> (Lic -> Lic -> Bool)
-> (Lic -> Lic -> Bool)
-> (Lic -> Lic -> Bool)
-> (Lic -> Lic -> Bool)
-> (Lic -> Lic -> Lic)
-> (Lic -> Lic -> Lic)
-> Ord Lic
Lic -> Lic -> Bool
Lic -> Lic -> Ordering
Lic -> Lic -> Lic
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Lic -> Lic -> Ordering
compare :: Lic -> Lic -> Ordering
$c< :: Lic -> Lic -> Bool
< :: Lic -> Lic -> Bool
$c<= :: Lic -> Lic -> Bool
<= :: Lic -> Lic -> Bool
$c> :: Lic -> Lic -> Bool
> :: Lic -> Lic -> Bool
$c>= :: Lic -> Lic -> Bool
>= :: Lic -> Lic -> Bool
$cmax :: Lic -> Lic -> Lic
max :: Lic -> Lic -> Lic
$cmin :: Lic -> Lic -> Lic
min :: Lic -> Lic -> Lic
Ord)

exprToProp :: License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
exprToProp :: forall s. License -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
exprToProp License
NONE          = Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall a. a -> StateT (Map Lic (Lit s)) (SAT s) a
forall (m :: * -> *) a. Monad m => a -> m a
return Prop s
forall s. Prop s
false
exprToProp (License LicenseExpression
lic) = LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s.
LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
licToProp LicenseExpression
lic

licToProp :: LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
licToProp :: forall s.
LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
licToProp (EAnd LicenseExpression
a LicenseExpression
b) = do
    Prop s
a' <- LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s.
LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
licToProp LicenseExpression
a
    Prop s
b' <- LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s.
LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
licToProp LicenseExpression
b
    Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall a. a -> StateT (Map Lic (Lit s)) (SAT s) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop s
a' Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
/\ Prop s
b')
licToProp (EOr LicenseExpression
a LicenseExpression
b) = do
    Prop s
a' <- LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s.
LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
licToProp LicenseExpression
a
    Prop s
b' <- LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall s.
LicenseExpression -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
licToProp LicenseExpression
b
    Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall a. a -> StateT (Map Lic (Lit s)) (SAT s) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Prop s
a' Prop s -> Prop s -> Prop s
forall s. Prop s -> Prop s -> Prop s
\/ Prop s
b')
licToProp (ELicense SimpleLicenseExpression
lic Maybe LicenseExceptionId
exc) = do
    let k :: Lic
k = SimpleLicenseExpression -> Maybe LicenseExceptionId -> Lic
Lic SimpleLicenseExpression
lic Maybe LicenseExceptionId
exc
    Map Lic (Lit s)
s <- StateT (Map Lic (Lit s)) (SAT s) (Map Lic (Lit s))
forall (m :: * -> *) s. Monad m => StateT s m s
get
    case Lic -> Map Lic (Lit s) -> Maybe (Lit s)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Lic
k Map Lic (Lit s)
s of
        Just Lit s
l -> Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall a. a -> StateT (Map Lic (Lit s)) (SAT s) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit s -> Prop s
forall s. Lit s -> Prop s
lit Lit s
l)
        Maybe (Lit s)
Nothing -> do
            Lit s
l <- SAT s (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) (Lit s)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (Map Lic (Lit s)) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift SAT s (Lit s)
forall s. SAT s (Lit s)
newLit
            Map Lic (Lit s) -> StateT (Map Lic (Lit s)) (SAT s) ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Lic -> Lit s -> Map Lic (Lit s) -> Map Lic (Lit s)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Lic
k Lit s
l Map Lic (Lit s)
s)
            Prop s -> StateT (Map Lic (Lit s)) (SAT s) (Prop s)
forall a. a -> StateT (Map Lic (Lit s)) (SAT s) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit s -> Prop s
forall s. Lit s -> Prop s
lit Lit s
l)