{-# 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 :: Givens v -> Wanted v -> Try e (Log s v) Bool
canDerive Givens v
g = (Givens v -> Wanted1 v -> Try e (Log s v) Bool
forall s v e.
(IsString s, Ord v) =>
Givens v -> Wanted1 v -> Try e (Log s v) Bool
canDerive1 Givens v
g (Wanted1 v -> Try e (Log s v) Bool)
-> [Wanted1 v] -> Try e (Log s v) Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
`allM`) ([Wanted1 v] -> Try e (Log s v) Bool)
-> (Wanted v -> [Wanted1 v]) -> Wanted v -> Try e (Log s v) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Wanted v -> [Wanted1 v]
forall v. Wanted v -> [Wanted1 v]
unWanted

allM :: Monad m => (a -> m Bool) -> [a] -> m Bool
a -> m Bool
p allM :: (a -> m Bool) -> [a] -> m Bool
`allM` [a]
xs = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> m [Bool] -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m Bool
p (a -> m Bool) -> [a] -> m [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
`mapM` [a]
xs

canDerive1 :: forall s v e .
	(IsString s, Ord v) => Givens v -> Wanted1 v -> Try e (Log s v) Bool
canDerive1 :: Givens v -> Wanted1 v -> Try e (Log s v) Bool
canDerive1 Givens v
g Wanted1 v
w = (Bool
s Bool -> Bool -> Bool
|| Bool
d) Bool -> Try e (Log s v) () -> Try e (Log s v) Bool
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ if Bool
s
	then Log s v -> Try e (Log s v) ()
forall e. Log s v -> Try e (Log s v) ()
t (Log s v -> Try e (Log s v) ()) -> Log s v -> Try e (Log s v) ()
forall a b. (a -> b) -> a -> b
$ Log s v
ttl Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
lw Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
" is self-contained"
	else Log s v -> Try e (Log s v) ()
forall e. Log s v -> Try e (Log s v) ()
t (Log s v -> Try e (Log s v) ()) -> Log s v -> Try e (Log s v) ()
forall a b. (a -> b) -> a -> b
$ Log s v
ttl Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
lw Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
" can" Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
nt Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
" be derived from"
	where
	s :: Bool
s = Wanted1 v -> Bool
forall v. Constraint v -> Bool
selfContained Wanted1 v
w
	d :: Bool
d = (Wanted1 v -> Bool) -> [Wanted1 v] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Wanted1 v
w Wanted1 v -> Wanted1 v -> Bool
forall v. Ord v => Constraint v -> Constraint v -> Bool
`isDerivFrom`) ([Wanted1 v] -> Bool)
-> ([Maybe v] -> [Wanted1 v]) -> [Maybe v] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Givens v -> [Wanted1 v]
forall v. Givens v -> [Constraint v]
unGivens (Givens v -> [Wanted1 v])
-> ([Maybe v] -> Givens v) -> [Maybe v] -> [Wanted1 v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe v -> Givens v -> Givens v)
-> Givens v -> [Maybe v] -> Givens v
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Maybe v -> Givens v -> Givens v
forall v. Ord v => Maybe v -> Givens v -> Givens v
rmVar Givens v
g ([Maybe v] -> Bool) -> [Maybe v] -> Bool
forall a b. (a -> b) -> a -> b
$ Givens v -> [Maybe v]
forall v. Ord v => Givens v -> [Maybe v]
gVars Givens v
g [Maybe v] -> [Maybe v] -> [Maybe v]
forall a. Eq a => [a] -> [a] -> [a]
\\ Wanted1 v -> [Maybe v]
forall v. Ord v => Constraint v -> [Maybe v]
vars Wanted1 v
w
	t :: Log s v -> Try e (Log s v) ()
t = forall ws e. Set (Log s v) ws => Log s v -> Try e ws ()
forall w ws e. Set w ws => w -> Try e ws ()
tell @(Log s v)
	ttl :: Log s v
ttl = Log s v
"canDerive1: "; lw :: Log s v
lw = Wanted1 v -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Wanted1 v
w; nt :: Log s v
nt = Log s v -> Log s v -> Bool -> Log s v
forall a. a -> a -> Bool -> a
bool Log s v
"not" Log s v
"" Bool
d

---------------------------------------------------------------------------
-- GIVENS
---------------------------------------------------------------------------

-- NEWTYPE GIVENS AND CONSTRUCTOR

newtype Givens v = Givens { Givens v -> [Constraint v]
unGivens :: [Constraint v] } deriving Int -> Givens v -> ShowS
[Givens v] -> ShowS
Givens v -> String
(Int -> Givens v -> ShowS)
-> (Givens v -> String) -> ([Givens v] -> ShowS) -> Show (Givens v)
forall v. Show v => Int -> Givens v -> ShowS
forall v. Show v => [Givens v] -> ShowS
forall v. Show v => Givens v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Givens v] -> ShowS
$cshowList :: forall v. Show v => [Givens v] -> ShowS
show :: Givens v -> String
$cshow :: forall v. Show v => Givens v -> String
showsPrec :: Int -> Givens v -> ShowS
$cshowsPrec :: forall v. Show v => Int -> Givens v -> ShowS
Show

instance IsString s => Loggable s v (Givens v) where
	log :: Givens v -> Log s v
log (Givens [Constraint v]
cs) = Log s v
"(Givens [" Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v -> [Log s v] -> Log s v
forall s v. Log s v -> [Log s v] -> Log s v
intersperse Log s v
", " (Constraint v -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log (Constraint v -> Log s v) -> [Constraint v] -> [Log s v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Constraint v]
cs) Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
"])"

givens :: forall s v . (IsString s, Ord v) =>
	[Exp v 'Boolean] -> Try (Log s v) (Log s v) (Givens v)
givens :: [Exp v 'Boolean] -> Try (Log s v) (Log s v) (Givens v)
givens [Exp v 'Boolean]
gs = do
	Log s v -> Try (Log s v) (Log s v) ()
forall e. Log s v -> Try e (Log s v) ()
t (Log s v -> Try (Log s v) (Log s v) ())
-> Log s v -> Try (Log s v) (Log s v) ()
forall a b. (a -> b) -> a -> b
$ Log s v
"givens ([Exp v 'Boolean]): " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. [Log s v] -> Log s v
forall s v. IsString s => [Log s v] -> Log s v
unwords (Exp v 'Boolean -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log (Exp v 'Boolean -> Log s v) -> [Exp v 'Boolean] -> [Log s v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Exp v 'Boolean]
gs)
	Givens v
gs' <- [Constraint v] -> Givens v
forall v. [Constraint v] -> Givens v
Givens ([Constraint v] -> Givens v)
-> ([[Constraint v]] -> [Constraint v])
-> [[Constraint v]]
-> Givens v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint v] -> [Constraint v]
forall a. Eq a => [a] -> [a]
nub ([Constraint v] -> [Constraint v])
-> ([[Constraint v]] -> [Constraint v])
-> [[Constraint v]]
-> [Constraint v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint v] -> [Constraint v]
forall a. Ord a => [a] -> [a]
sort ([Constraint v] -> [Constraint v])
-> ([[Constraint v]] -> [Constraint v])
-> [[Constraint v]]
-> [Constraint v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Constraint v] -> [Constraint v] -> [Constraint v]
forall a. [a] -> [a] -> [a]
(++) ([Constraint v] -> [Constraint v] -> [Constraint v])
-> ([Constraint v] -> [Constraint v])
-> [Constraint v]
-> [Constraint v]
-> [Constraint v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Constraint v] -> [Constraint v]
forall a. a -> a
id ([Constraint v] -> [Constraint v] -> [Constraint v])
-> ([Constraint v] -> [Constraint v])
-> [Constraint v]
-> [Constraint v]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Constraint v -> Constraint v
forall v. Constraint v -> Constraint v
positives (Constraint v -> Constraint v) -> [Constraint v] -> [Constraint v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)) ([Constraint v] -> [Constraint v])
-> ([[Constraint v]] -> [Constraint v])
-> [[Constraint v]]
-> [Constraint v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Constraint v]] -> [Constraint v]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
		([[Constraint v]] -> Givens v)
-> Try (Log s v) (Log s v) [[Constraint v]]
-> Try (Log s v) (Log s v) (Givens v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Either (Log s v) (Constraint v)
 -> [Constraint v] -> Try (Log s v) (Log s v) [Constraint v])
-> (Either (Log s v) (Constraint v), [Constraint v])
-> Try (Log s v) (Log s v) [Constraint v]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Either (Log s v) (Constraint v)
-> [Constraint v] -> Try (Log s v) (Log s v) [Constraint v]
forall w a. (Monoid w, Set w w) => Either w a -> [a] -> Try w w [a]
cons ((Either (Log s v) (Constraint v), [Constraint v])
 -> Try (Log s v) (Log s v) [Constraint v])
-> (Exp v 'Boolean
    -> Try
         (Log s v)
         (Log s v)
         (Either (Log s v) (Constraint v), [Constraint v]))
-> Exp v 'Boolean
-> Try (Log s v) (Log s v) [Constraint v]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< VarBool v
-> Exp v 'Boolean
-> Try
     (Log s v)
     (Log s v)
     (Either (Log s v) (Constraint v), [Constraint v])
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Try
     (Log s v) w (Either (Log s v) (Constraint v), [Constraint v])
constraint ([Exp v 'Boolean] -> VarBool v
forall v. Ord v => [Exp v 'Boolean] -> VarBool v
varBool [Exp v 'Boolean]
gs)) (Exp v 'Boolean -> Try (Log s v) (Log s v) [Constraint v])
-> [Exp v 'Boolean] -> Try (Log s v) (Log s v) [[Constraint v]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
`mapM` [Exp v 'Boolean]
gs
	Givens v
gs' Givens v
-> Try (Log s v) (Log s v) () -> Try (Log s v) (Log s v) (Givens v)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Log s v -> Try (Log s v) (Log s v) ()
forall e. Log s v -> Try e (Log s v) ()
t (Log s v
"givens (Givens v): " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Givens v -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Givens v
gs')
	where t :: Log s v -> Try e (Log s v) ()
t = forall ws e. Set (Log s v) ws => Log s v -> Try e ws ()
forall w ws e. Set w ws => w -> Try e ws ()
tell @(Log s v)

-- GIVENS VARIABLES

gVars :: Ord v => Givens v -> [Maybe v]
gVars :: Givens v -> [Maybe v]
gVars = [Maybe v] -> [Maybe v]
forall a. Eq a => [a] -> [a]
nub ([Maybe v] -> [Maybe v])
-> (Givens v -> [Maybe v]) -> Givens v -> [Maybe v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe v] -> [Maybe v]
forall a. Ord a => [a] -> [a]
sort ([Maybe v] -> [Maybe v])
-> (Givens v -> [Maybe v]) -> Givens v -> [Maybe v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Maybe v]] -> [Maybe v]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Maybe v]] -> [Maybe v])
-> (Givens v -> [[Maybe v]]) -> Givens v -> [Maybe v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint v -> [Maybe v]
forall v. Ord v => Constraint v -> [Maybe v]
vars (Constraint v -> [Maybe v]) -> [Constraint v] -> [[Maybe v]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([Constraint v] -> [[Maybe v]])
-> (Givens v -> [Constraint v]) -> Givens v -> [[Maybe v]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Givens v -> [Constraint v]
forall v. Givens v -> [Constraint v]
unGivens

-- REMOVE VARIABLE

rmVar :: Ord v => Maybe v -> Givens v -> Givens v
rmVar :: Maybe v -> Givens v -> Givens v
rmVar Maybe v
v (Givens [Constraint v]
gs) = [Constraint v] -> Givens v
forall v. [Constraint v] -> Givens v
Givens ([Constraint v] -> Givens v)
-> (([Constraint v], [Constraint v]) -> [Constraint v])
-> ([Constraint v], [Constraint v])
-> Givens v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint v] -> [Constraint v]
forall a. Ord a => [a] -> [a]
sort ([Constraint v] -> [Constraint v])
-> (([Constraint v], [Constraint v]) -> [Constraint v])
-> ([Constraint v], [Constraint v])
-> [Constraint v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Constraint v]] -> [Constraint v]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Constraint v]] -> [Constraint v])
-> (([Constraint v], [Constraint v]) -> [[Constraint v]])
-> ([Constraint v], [Constraint v])
-> [Constraint v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Constraint v] -> [[Constraint v]] -> [[Constraint v]])
-> ([Constraint v], [[Constraint v]]) -> [[Constraint v]]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (:)
	(([Constraint v], [[Constraint v]]) -> [[Constraint v]])
-> (([Constraint v], [Constraint v])
    -> ([Constraint v], [[Constraint v]]))
-> ([Constraint v], [Constraint v])
-> [[Constraint v]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Constraint v] -> [[Constraint v]])
-> ([Constraint v], [Constraint v])
-> ([Constraint v], [[Constraint v]])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (([Constraint v] -> Bool)
-> ([Constraint v] -> ([Constraint v], [Constraint v]))
-> [Constraint v]
-> [[Constraint v]]
forall s r. (s -> Bool) -> (s -> (r, s)) -> s -> [r]
unfoldUntil [Constraint v] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Maybe v -> [Constraint v] -> ([Constraint v], [Constraint v])
forall v.
Ord v =>
Maybe v -> [Constraint v] -> ([Constraint v], [Constraint v])
rvStep Maybe v
v)) (([Constraint v], [Constraint v]) -> Givens v)
-> ([Constraint v], [Constraint v]) -> Givens v
forall a b. (a -> b) -> a -> b
$ (Constraint v -> Bool)
-> [Constraint v] -> ([Constraint v], [Constraint v])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Bool -> Bool
not (Bool -> Bool) -> (Constraint v -> Bool) -> Constraint v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint v -> Maybe v -> Bool
forall v. Ord v => Constraint v -> Maybe v -> Bool
`has` Maybe v
v)) [Constraint v]
gs

rvStep :: Ord v => Maybe v -> [Constraint v] -> ([Constraint v], [Constraint v])
rvStep :: Maybe v -> [Constraint v] -> ([Constraint v], [Constraint v])
rvStep Maybe v
_ [] = ([], [])
rvStep Maybe v
v (Constraint v
c : [Constraint v]
cs) = [Either (Constraint v) (Constraint v)]
-> ([Constraint v], [Constraint v])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either (Constraint v) (Constraint v)]
 -> ([Constraint v], [Constraint v]))
-> [Either (Constraint v) (Constraint v)]
-> ([Constraint v], [Constraint v])
forall a b. (a -> b) -> a -> b
$ Maybe v
-> Constraint v
-> Constraint v
-> Either (Constraint v) (Constraint v)
forall v.
Ord v =>
Maybe v
-> Constraint v
-> Constraint v
-> Either (Constraint v) (Constraint v)
rmVar1 Maybe v
v Constraint v
c (Constraint v -> Either (Constraint v) (Constraint v))
-> [Constraint v] -> [Either (Constraint v) (Constraint v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Constraint v]
cs

rmVar1 :: Ord v => Maybe v -> Constraint v ->
	Constraint v -> Either (Constraint v) (Constraint v)
rmVar1 :: Maybe v
-> Constraint v
-> Constraint v
-> Either (Constraint v) (Constraint v)
rmVar1 Maybe v
v Constraint v
c0 Constraint v
c = Either (Constraint v) (Constraint v)
-> (Constraint v -> Either (Constraint v) (Constraint v))
-> Maybe (Constraint v)
-> Either (Constraint v) (Constraint v)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Constraint v -> Either (Constraint v) (Constraint v)
forall a b. b -> Either a b
Right Constraint v
c) Constraint v -> Either (Constraint v) (Constraint v)
forall a b. a -> Either a b
Left (Maybe (Constraint v) -> Either (Constraint v) (Constraint v))
-> Maybe (Constraint v) -> Either (Constraint v) (Constraint v)
forall a b. (a -> b) -> a -> b
$ Maybe v -> Constraint v -> Constraint v -> Maybe (Constraint v)
forall v.
Ord v =>
Maybe v -> Constraint v -> Constraint v -> Maybe (Constraint v)
eliminate Maybe v
v Constraint v
c0 Constraint v
c

unfoldUntil :: (s -> Bool) -> (s -> (r, s)) -> s -> [r]
unfoldUntil :: (s -> Bool) -> (s -> (r, s)) -> s -> [r]
unfoldUntil s -> Bool
p s -> (r, s)
f = (s -> Maybe (r, s)) -> s -> [r]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr ((s -> Maybe (r, s)) -> s -> [r])
-> (s -> Maybe (r, s)) -> s -> [r]
forall a b. (a -> b) -> a -> b
$ (Maybe (r, s) -> Maybe (r, s) -> Bool -> Maybe (r, s))
-> Maybe (r, s) -> Maybe (r, s) -> Bool -> Maybe (r, s)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Maybe (r, s) -> Maybe (r, s) -> Bool -> Maybe (r, s)
forall a. a -> a -> Bool -> a
bool Maybe (r, s)
forall a. Maybe a
Nothing (Maybe (r, s) -> Bool -> Maybe (r, s))
-> (s -> Maybe (r, s)) -> s -> Bool -> Maybe (r, s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (r, s) -> Maybe (r, s)
forall a. a -> Maybe a
Just ((r, s) -> Maybe (r, s)) -> (s -> (r, s)) -> s -> Maybe (r, s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> (r, s)
f (s -> Bool -> Maybe (r, s)) -> (s -> Bool) -> s -> Maybe (r, s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> s -> Bool
p

---------------------------------------------------------------------------
-- WANTED
---------------------------------------------------------------------------

newtype Wanted v = Wanted { Wanted v -> [Wanted1 v]
unWanted :: [Wanted1 v] } deriving Int -> Wanted v -> ShowS
[Wanted v] -> ShowS
Wanted v -> String
(Int -> Wanted v -> ShowS)
-> (Wanted v -> String) -> ([Wanted v] -> ShowS) -> Show (Wanted v)
forall v. Show v => Int -> Wanted v -> ShowS
forall v. Show v => [Wanted v] -> ShowS
forall v. Show v => Wanted v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Wanted v] -> ShowS
$cshowList :: forall v. Show v => [Wanted v] -> ShowS
show :: Wanted v -> String
$cshow :: forall v. Show v => Wanted v -> String
showsPrec :: Int -> Wanted v -> ShowS
$cshowsPrec :: forall v. Show v => Int -> Wanted v -> ShowS
Show

type Wanted1 v = Constraint v

instance IsString s => Loggable s v (Wanted v) where
	log :: Wanted v -> Log s v
log (Wanted [Wanted1 v]
cs) = Log s v
"(Wanted [" Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v -> [Log s v] -> Log s v
forall s v. Log s v -> [Log s v] -> Log s v
intersperse Log s v
", " (Wanted1 v -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log (Wanted1 v -> Log s v) -> [Wanted1 v] -> [Log s v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Wanted1 v]
cs) Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Log s v
"])"

wanted :: forall s v . (IsString s, Ord v) =>
	Exp v 'Boolean -> Try (Log s v) (Log s v) (Wanted v)
wanted :: Exp v 'Boolean -> Try (Log s v) (Log s v) (Wanted v)
wanted Exp v 'Boolean
w = do
	Log s v -> Try (Log s v) (Log s v) ()
forall e. Log s v -> Try e (Log s v) ()
t (Log s v -> Try (Log s v) (Log s v) ())
-> Log s v -> Try (Log s v) (Log s v) ()
forall a b. (a -> b) -> a -> b
$ Log s v
"wanted (Exp v 'Boolean): " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Exp v 'Boolean -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Exp v 'Boolean
w
	(Either (Log s v) (Constraint v)
e, [Constraint v]
s) <- VarBool v
-> Exp v 'Boolean
-> Try
     (Log s v)
     (Log s v)
     (Either (Log s v) (Constraint v), [Constraint v])
forall w s v.
(Monoid w, IsString s, Ord v) =>
VarBool v
-> Exp v 'Boolean
-> Try
     (Log s v) w (Either (Log s v) (Constraint v), [Constraint v])
constraint VarBool v
forall k a. Map k a
empty Exp v 'Boolean
w
	Wanted v
w' <- (Log s v -> Try (Log s v) (Log s v) (Wanted v))
-> (Constraint v -> Try (Log s v) (Log s v) (Wanted v))
-> Either (Log s v) (Constraint v)
-> Try (Log s v) (Log s v) (Wanted v)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Log s v -> Try (Log s v) (Log s v) (Wanted v)
forall w e a. Monoid w => e -> Try e w a
throw (Wanted v -> Try (Log s v) (Log s v) (Wanted v)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Wanted v -> Try (Log s v) (Log s v) (Wanted v))
-> (Constraint v -> Wanted v)
-> Constraint v
-> Try (Log s v) (Log s v) (Wanted v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constraint v] -> Wanted v
forall v. [Wanted1 v] -> Wanted v
Wanted ([Constraint v] -> Wanted v)
-> (Constraint v -> [Constraint v]) -> Constraint v -> Wanted v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint v -> [Constraint v] -> [Constraint v]
forall a. a -> [a] -> [a]
: [Constraint v]
s)) Either (Log s v) (Constraint v)
e
	Wanted v
w' Wanted v
-> Try (Log s v) (Log s v) () -> Try (Log s v) (Log s v) (Wanted v)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Log s v -> Try (Log s v) (Log s v) ()
forall e. Log s v -> Try e (Log s v) ()
t (Log s v
"wanted (Wanted v): " Log s v -> Log s v -> Log s v
forall s v. Log s v -> Log s v -> Log s v
.+. Wanted v -> Log s v
forall s v a. Loggable s v a => a -> Log s v
log Wanted v
w')
	where t :: Log s v -> Try e (Log s v) ()
t = forall ws e. Set (Log s v) ws => Log s v -> Try e ws ()
forall w ws e. Set w ws => w -> Try e ws ()
tell @(Log s v)