{-# LANGUAGE BlockArguments, OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
module Data.Derivation.CanDerive (
-- * CAN DERIVE
canDerive,
-- * GIVENS
Givens, givens,
-- * WANTED
Wanted, wanted ) where
import Prelude hiding (unwords, log)
import Control.Arrow (second)
import Control.Monad ((<=<))
import Control.Monad.Try (Try, throw, tell, cons)
import Data.Map.Strict (empty)
import Data.Either (partitionEithers)
import Data.List (unfoldr, (\\), nub, partition, sort)
import Data.Bool (bool)
import Data.String (IsString)
import Data.Log (Log, (.+.), intersperse, unwords, log, Loggable(..))
import Data.Derivation.Constraint (
Constraint,
vars, has, isDerivFrom, positives, selfContained, eliminate )
import Data.Derivation.Expression.Internal (
Exp, ExpType(..), constraint, varBool )
---------------------------------------------------------------------------
-- * CAN DERIVE
-- * GIVENS
-- + NEWTYPE GIVENS AND CONSTRUCTOR
-- + GIVENS VARIABLES
-- + REMOVE VARIABLE
-- * WANTED
---------------------------------------------------------------------------
-- CAN DERIVE
---------------------------------------------------------------------------
canDerive :: (IsString s, Ord v) => Givens v -> Wanted v -> Try e (Log s v) Bool
canDerive g = (canDerive1 g `allM`) . unWanted
allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
p `allM` xs = and <$> p `mapM` xs
canDerive1 :: forall s v e .
(IsString s, Ord v) => Givens v -> Wanted1 v -> Try e (Log s v) Bool
canDerive1 g w = (s || d) <$ if s
then t $ ttl .+. lw .+. " is self-contained"
else t $ ttl .+. lw .+. " can" .+. nt .+. " be derived from"
where
s = selfContained w
d = any (w `isDerivFrom`) . unGivens . foldr rmVar g $ gVars g \\ vars w
t = tell @(Log s v)
ttl = "canDerive1: "; lw = log w; nt = bool "not" "" d
---------------------------------------------------------------------------
-- GIVENS
---------------------------------------------------------------------------
-- NEWTYPE GIVENS AND CONSTRUCTOR
newtype Givens v = Givens { unGivens :: [Constraint v] } deriving Show
instance IsString s => Loggable s v (Givens v) where
log (Givens cs) = "(Givens [" .+. intersperse ", " (log <$> cs) .+. "])"
givens :: forall s v . (IsString s, Ord v) =>
[Exp v 'Boolean] -> Try (Log s v) (Log s v) (Givens v)
givens gs = do
t $ "givens ([Exp v 'Boolean]): " .+. unwords (log <$> gs)
gs' <- Givens . nub . sort . ((++) <$> id <*> (positives <$>)) . concat
<$> (uncurry cons <=< constraint (varBool gs)) `mapM` gs
gs' <$ t ("givens (Givens v): " .+. log gs')
where t = tell @(Log s v)
-- GIVENS VARIABLES
gVars :: Ord v => Givens v -> [Maybe v]
gVars = nub . sort . concat . (vars <$>) . unGivens
-- REMOVE VARIABLE
rmVar :: Ord v => Maybe v -> Givens v -> Givens v
rmVar v (Givens gs) = Givens . sort . concat . uncurry (:)
. second (unfoldUntil null (rvStep v)) $ partition (not . (`has` v)) gs
rvStep :: Ord v => Maybe v -> [Constraint v] -> ([Constraint v], [Constraint v])
rvStep _ [] = ([], [])
rvStep v (c : cs) = partitionEithers $ rmVar1 v c <$> cs
rmVar1 :: Ord v => Maybe v -> Constraint v ->
Constraint v -> Either (Constraint v) (Constraint v)
rmVar1 v c0 c = maybe (Right c) Left $ eliminate v c0 c
unfoldUntil :: (s -> Bool) -> (s -> (r, s)) -> s -> [r]
unfoldUntil p f = unfoldr $ flip bool Nothing <$> Just . f <*> p
---------------------------------------------------------------------------
-- WANTED
---------------------------------------------------------------------------
newtype Wanted v = Wanted { unWanted :: [Wanted1 v] } deriving Show
type Wanted1 v = Constraint v
instance IsString s => Loggable s v (Wanted v) where
log (Wanted cs) = "(Wanted [" .+. intersperse ", " (log <$> cs) .+. "])"
wanted :: forall s v . (IsString s, Ord v) =>
Exp v 'Boolean -> Try (Log s v) (Log s v) (Wanted v)
wanted w = do
t $ "wanted (Exp v 'Boolean): " .+. log w
(e, s) <- constraint empty w
w' <- either throw (pure . Wanted . (: s)) e
w' <$ t ("wanted (Wanted v): " .+. log w')
where t = tell @(Log s v)