{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}

--------------------------------------------------------------------------------
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
--  Module      :  VarBinding
--  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 
--                 2011, 2012, 2014, 2015, 2016, 2018, 2020, 2022, 2024 Douglas Burke
--  License     :  GPL V2
--
--  Maintainer  :  Douglas Burke
--  Stability   :  experimental
--  Portability :  CPP, FlexibleInstances, OverloadedStrings
--
--  This module defines functions for representing and manipulating query
--  binding variable sets.  This is the key data that mediates between
--  query and back substitution when performing inferences.  A framework
--  of query variable modifiers is provided that can be used to
--  implement richer inferences, such as filtering of  query results,
--  or replacing values based on known relationships.
--
--------------------------------------------------------------------------------

module Swish.VarBinding
    ( VarBinding(..), nullVarBinding
    , boundVars, subBinding, makeVarBinding
    , applyVarBinding, joinVarBindings, addVarBinding
    , VarBindingModify(..), OpenVarBindingModify
    , openVbmName
    , vbmCompatibility, vbmCompose
    , composeSequence, findCompositions, findComposition
    , VarBindingFilter(..)
    , makeVarFilterModify
    , makeVarTestFilter, makeVarCompareFilter
    , varBindingId, nullVarBindingModify
    , varFilterDisjunction, varFilterConjunction
    , varFilterEQ, varFilterNE
    )
where

import qualified Data.Map as M
import qualified Data.Set as S

#if (!defined(__GLASGOW_HASKELL__)) || (__GLASGOW_HASKELL__ < 710)
import Control.Applicative ((<$>), (<*>))
import Data.Monoid (Monoid(..), mconcat)
#endif

#if !(MIN_VERSION_base(4, 11, 0))
import Data.Semigroup
#endif

import Control.Monad (mplus)

import Data.Foldable(Foldable(..))
import Data.Function (on)
import Data.List (find, intersect, union, (\\), permutations)
import Data.Maybe (mapMaybe, fromMaybe, isJust, fromJust, listToMaybe)
import Data.Ord (comparing)

-- Avoid messages added in GHC 9.10 about foldl' import from Data.List
-- being redundant.
import Prelude hiding (Foldable(..))

import Swish.Namespace (ScopedName, getScopeLocal)
import Swish.QName (newLName, getLName)

import Swish.RDF.Vocabulary (swishName)

import Swish.Utils.ListHelpers (flist)

------------------------------------------------------------
--  Query variable bindings
------------------------------------------------------------

-- |VarBinding is the type of an arbitrary variable bindings
--  value, where the type of the bound values is not specified.
--
data VarBinding a b = VarBinding
    { forall a b. VarBinding a b -> a -> Maybe b
vbMap  :: a -> Maybe b
    , forall a b. VarBinding a b -> Set (a, b)
vbEnum :: S.Set (a,b)
    , forall a b. VarBinding a b -> Bool
vbNull :: Bool
    }

-- | The Eq instance is defined as the set equivalence of the
--   pairs of variables in the binding.
--
instance (Ord a, Ord b) => Eq (VarBinding a b) where
    == :: VarBinding a b -> VarBinding a b -> Bool
(==) = Set (a, b) -> Set (a, b) -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Set (a, b) -> Set (a, b) -> Bool)
-> (VarBinding a b -> Set (a, b))
-> VarBinding a b
-> VarBinding a b
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` VarBinding a b -> Set (a, b)
forall a b. VarBinding a b -> Set (a, b)
vbEnum

-- | The Ord instance is defined only on the pairs of
--   variables in the binding.
instance (Ord a, Ord b) => Ord (VarBinding a b) where
    compare :: VarBinding a b -> VarBinding a b -> Ordering
compare = (VarBinding a b -> Set (a, b))
-> VarBinding a b -> VarBinding a b -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing VarBinding a b -> Set (a, b)
forall a b. VarBinding a b -> Set (a, b)
vbEnum

-- | When combining instances, if there is an overlapping binding then
--   the  value from the first instance is used.
instance (Ord a, Ord b) => Semigroup (VarBinding a b) where
    <> :: VarBinding a b -> VarBinding a b -> VarBinding a b
(<>) = VarBinding a b -> VarBinding a b -> VarBinding a b
forall a b.
(Ord a, Ord b) =>
VarBinding a b -> VarBinding a b -> VarBinding a b
joinVarBindings
    
instance (Ord a, Ord b) => Monoid (VarBinding a b) where
    mempty :: VarBinding a b
mempty = VarBinding a b
forall a b. VarBinding a b
nullVarBinding
#if !(MIN_VERSION_base(4, 11, 0))
    mappend = (<>)
#endif

-- | The Show instance only displays the pairs of variables
--    in the binding.
--
instance (Show a, Show b) => Show (VarBinding a b) where
    show :: VarBinding a b -> String
show = [(a, b)] -> String
forall a. Show a => a -> String
show ([(a, b)] -> String)
-> (VarBinding a b -> [(a, b)]) -> VarBinding a b -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (a, b) -> [(a, b)]
forall a. Set a -> [a]
S.toList (Set (a, b) -> [(a, b)])
-> (VarBinding a b -> Set (a, b)) -> VarBinding a b -> [(a, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarBinding a b -> Set (a, b)
forall a b. VarBinding a b -> Set (a, b)
vbEnum

-- | The null, or empty, binding maps no query variables.
--   This is the 'mempty' instance of the Monoid.
--
nullVarBinding :: VarBinding a b
nullVarBinding :: forall a b. VarBinding a b
nullVarBinding = VarBinding
    { vbMap :: a -> Maybe b
vbMap  = Maybe b -> a -> Maybe b
forall a b. a -> b -> a
const Maybe b
forall a. Maybe a
Nothing
    , vbEnum :: Set (a, b)
vbEnum = Set (a, b)
forall a. Set a
S.empty
    , vbNull :: Bool
vbNull = Bool
True
    }

-- |Return a list of the variables bound by a supplied variable binding
--
-- The Ord instance on b is not needed (it was circa GHC 7.6) but is
-- kept in to avoid the need to increase the minor version number.
boundVars :: (Ord a, Ord b) => VarBinding a b -> S.Set a
boundVars :: forall a b. (Ord a, Ord b) => VarBinding a b -> Set a
boundVars = ((a, b) -> a) -> Set (a, b) -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (a, b) -> a
forall a b. (a, b) -> a
fst (Set (a, b) -> Set a)
-> (VarBinding a b -> Set (a, b)) -> VarBinding a b -> Set a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarBinding a b -> Set (a, b)
forall a b. VarBinding a b -> Set (a, b)
vbEnum

-- |VarBinding subset function, tests to see if one query binding
--  is a subset of another;  i.e. every query variable mapping defined
--  by one is also defined by the other.
--
subBinding :: (Ord a, Ord b) => VarBinding a b -> VarBinding a b -> Bool
subBinding :: forall a b.
(Ord a, Ord b) =>
VarBinding a b -> VarBinding a b -> Bool
subBinding = Set (a, b) -> Set (a, b) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
S.isSubsetOf (Set (a, b) -> Set (a, b) -> Bool)
-> (VarBinding a b -> Set (a, b))
-> VarBinding a b
-> VarBinding a b
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` VarBinding a b -> Set (a, b)
forall a b. VarBinding a b -> Set (a, b)
vbEnum

-- |Function to make a variable binding from a list of
--  pairs of variable and corresponding assigned value.
--
makeVarBinding :: (Ord a, Ord b) => [(a,b)] -> VarBinding a b
makeVarBinding :: forall a b. (Ord a, Ord b) => [(a, b)] -> VarBinding a b
makeVarBinding [] = VarBinding a b
forall a b. VarBinding a b
nullVarBinding
makeVarBinding [(a, b)]
vrbs =
    VarBinding
    { vbMap :: a -> Maybe b
vbMap  = (a -> Map a b -> Maybe b) -> Map a b -> a -> Maybe b
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Map a b -> Maybe b
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ([(a, b)] -> Map a b
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(a, b)]
vrbs)
    , vbEnum :: Set (a, b)
vbEnum = [(a, b)] -> Set (a, b)
forall a. Ord a => [a] -> Set a
S.fromList [(a, b)]
vrbs
    , vbNull :: Bool
vbNull = Bool
False
    }

-- |Apply query binding to a supplied value, returning the value
--  unchanged if no binding is defined
--
applyVarBinding :: VarBinding a a -> a -> a
applyVarBinding :: forall a. VarBinding a a -> a -> a
applyVarBinding VarBinding a a
vbind a
v = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
v (VarBinding a a -> a -> Maybe a
forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding a a
vbind a
v)

-- |Join a pair of query bindings, returning a new binding that
--  maps all variables recognized by either of the input bindings.
--  If the bindings should overlap, such overlap is not detected and
--  the value from the first binding provided is used.
--
joinVarBindings :: (Ord a, Ord b) => VarBinding a b -> VarBinding a b -> VarBinding a b
joinVarBindings :: forall a b.
(Ord a, Ord b) =>
VarBinding a b -> VarBinding a b -> VarBinding a b
joinVarBindings VarBinding a b
vb1 VarBinding a b
vb2
    | VarBinding a b -> Bool
forall a b. VarBinding a b -> Bool
vbNull VarBinding a b
vb1 = VarBinding a b
vb2
    | VarBinding a b -> Bool
forall a b. VarBinding a b -> Bool
vbNull VarBinding a b
vb2 = VarBinding a b
vb1
    | Bool
otherwise  = VarBinding
        { vbMap :: a -> Maybe b
vbMap  = a -> Maybe b
mv12
        , vbEnum :: Set (a, b)
vbEnum = (a -> (a, b)) -> Set a -> Set (a, b)
forall b a. Ord b => (a -> b) -> Set a -> Set b
S.map (\a
v -> (a
v,Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (a -> Maybe b
mv12 a
v))) Set a
bv12
        , vbNull :: Bool
vbNull = Bool
False
        }
    where
        mv12 :: a -> Maybe b
mv12 a
n = VarBinding a b -> a -> Maybe b
forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding a b
vb1 a
n Maybe b -> Maybe b -> Maybe b
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` VarBinding a b -> a -> Maybe b
forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding a b
vb2 a
n
        bv12 :: Set a
bv12 = VarBinding a b -> Set a
forall a b. (Ord a, Ord b) => VarBinding a b -> Set a
boundVars VarBinding a b
vb1 Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`S.union` VarBinding a b -> Set a
forall a b. (Ord a, Ord b) => VarBinding a b -> Set a
boundVars VarBinding a b
vb2

-- |Add a single new value to a variable binding and return the resulting
--  new variable binding.
--
addVarBinding :: 
    (Ord a, Ord b) 
    => a 
    -> b 
    -> VarBinding a b
    -> VarBinding a b
addVarBinding :: forall a b.
(Ord a, Ord b) =>
a -> b -> VarBinding a b -> VarBinding a b
addVarBinding a
lb b
val VarBinding a b
vbind = VarBinding a b -> VarBinding a b -> VarBinding a b
forall a b.
(Ord a, Ord b) =>
VarBinding a b -> VarBinding a b -> VarBinding a b
joinVarBindings VarBinding a b
vbind (VarBinding a b -> VarBinding a b)
-> VarBinding a b -> VarBinding a b
forall a b. (a -> b) -> a -> b
$ [(a, b)] -> VarBinding a b
forall a b. (Ord a, Ord b) => [(a, b)] -> VarBinding a b
makeVarBinding [(a
lb,b
val)]

------------------------------------------------------------
--  Datatypes for variable binding modifiers
------------------------------------------------------------

-- |Define the type of a function to modify variable bindings in
--  forward chaining based on rule antecedent matches.  This
--  function is used to implement the \"allocated to\" logic described
--  in Appendix B of the RDF semantics document, in which a specific
--  blank node is associated with all matches of some specific value
--  by applications of the rule on a given graph.
--  Use 'id' if no modification of the variable bindings is required.
--
--  This datatype consists of the modifier function itself, which
--  operates on a list of variable bindings rather than a single
--  variable binding (because some modifications share context across
--  a set of bindings), and some additional descriptive information
--  that allows possible usage patterns to be analyzed.
--
--  Some usage patterns (see 'vbmUsage' for more details):
--
--  [filter]  all variables are input variables, and the effect
--      of the modifier function is to drop variable bindings that
--      don't satisfy some criterion.
--      Identifiable by an empty element in @vbmUsage@.
--
--  [source]  all variables are output variables:  a raw query
--      could be viewed as a source of variable bindings.
--      Identifiable by an element of @vbmUsage@ equal to @vbmVocab@.
--
--  [modifier]  for each supplied variable binding, one or more
--      new variable bindings may be created that contain the
--      input variables bound as supplied plus some additional variables.
--      Identifiable by an element of @vbmUsage@ some subset of @vbmVocab@.
--
--  A variety of variable usage patterns may be supported by a given
--  modifier:  a modifier may be used to define new variable bindings
--  from existing bindings in a number of ways, or simply to check that
--  some required relationship between bindings is satisfied.
--  (Example, for @a + b = c@, any one variable can be deduced from the
--  other two, or all three may be supplied to check that the relationship
--  does indeed hold.)
--
data VarBindingModify a b = VarBindingModify
    { forall a b. VarBindingModify a b -> ScopedName
vbmName   :: ScopedName
                            -- ^Name used to identify this variable binding
                            --  modifier when building inference rules.
    , forall a b.
VarBindingModify a b -> [VarBinding a b] -> [VarBinding a b]
vbmApply  :: [VarBinding a b] -> [VarBinding a b]
                            -- ^Apply variable binding modifier to a
                            --  list of variable bindings, returning a
                            --  new list.  The result list is not
                            --  necessarily the same length as the
                            --  supplied list.
    , forall a b. VarBindingModify a b -> [a]
vbmVocab  :: [a]      -- ^List of variables used by this modifier.
                            --  All results of applying this modifier contain
                            --  bindings for these variables.
    , forall a b. VarBindingModify a b -> [[a]]
vbmUsage  :: [[a]]    -- ^List of binding modifier usage patterns
                            --  supported.  Each pattern is characterized as
                            --  a list of variables for which new bindings
                            --  may be created by some application of this
                            --  modifier, assuming that bindings for all other
                            --  variables in @vbmVocab@ are supplied.
    }

-- |Type for variable binding modifier that has yet to be instantiated
--  with respect to the variables that it operates upon.
--
type OpenVarBindingModify lb vn = [lb] -> VarBindingModify lb vn

-- |Extract variable binding name from @OpenVarBindingModify@ value
--
--  (Because only the name is required, the application to an undefined
--  list of variable labels should never be evaluated, as long as the
--  name is not dependent on the variable names in any way.)
--
--  NOT QUITE... some of the functions that create @OpenVarBindingModify@
--  instances also pattern-match the number of labels provided, forcing
--  evaluation of the labels parameter, even though it's not used.
--
openVbmName :: OpenVarBindingModify lb vn -> ScopedName
openVbmName :: forall lb vn. OpenVarBindingModify lb vn -> ScopedName
openVbmName OpenVarBindingModify lb vn
ovbm = VarBindingModify lb vn -> ScopedName
forall a b. VarBindingModify a b -> ScopedName
vbmName (OpenVarBindingModify lb vn
ovbm (String -> [lb]
forall a. HasCallStack => String -> a
error String
"Undefined labels in variable binding"))

-- | Displays the name of the modifier.
instance Show (OpenVarBindingModify a b)
    where
        show :: OpenVarBindingModify a b -> String
show = ScopedName -> String
forall a. Show a => a -> String
show (ScopedName -> String)
-> (OpenVarBindingModify a b -> ScopedName)
-> OpenVarBindingModify a b
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpenVarBindingModify a b -> ScopedName
forall lb vn. OpenVarBindingModify lb vn -> ScopedName
openVbmName

-- |Variable binding modifier compatibility test.
--
--  Given a list of bound variables and a variable binding modifier, return
--  a list of new variables that may be bound, or @Nothing@.
--
--  Note:  if the usage pattern component is well-formed (i.e. all
--  elements different) then at most one element can be compatible with
--  a given input variable set.
--
vbmCompatibility :: (Eq a) => VarBindingModify a b -> [a] -> Maybe [a]
vbmCompatibility :: forall a b. Eq a => VarBindingModify a b -> [a] -> Maybe [a]
vbmCompatibility VarBindingModify a b
vbm [a]
vars = ([a] -> Bool) -> [[a]] -> Maybe [a]
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find [a] -> Bool
compat (VarBindingModify a b -> [[a]]
forall a b. VarBindingModify a b -> [[a]]
vbmUsage VarBindingModify a b
vbm)
    where
        compat :: [a] -> Bool
compat = [a] -> [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> [a] -> Bool
vbmCompatibleVars [a]
vars (VarBindingModify a b -> [a]
forall a b. VarBindingModify a b -> [a]
vbmVocab VarBindingModify a b
vbm)

-- |Variable binding usage compatibility test.
--
--  Returns @True@ if the supplied variable bindings can be compatibly
--  processed by a variable binding usage with supplied vocabulary and
--  usage pattern.
--
vbmCompatibleVars ::
  (Eq a) 
  => [a] -- ^ variables supplied with bindings
  -> [a] -- ^ variables returned with bindings by a modifier
  -> [a] -- ^ variables assigned new bindings by a modifier
  -> Bool
vbmCompatibleVars :: forall a. Eq a => [a] -> [a] -> [a] -> Bool
vbmCompatibleVars [a]
bvars [a]
vocab [a]
ovars =
    [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a]
ivars [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [a]
ovars) Bool -> Bool -> Bool
&&       -- ivars and ovars don't overlap
    [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (([a]
vocab [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
ovars) [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
ivars)        -- ovars and ivars cover vocab
    where
        ivars :: [a]
ivars = [a]
bvars [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [a]
vocab

-- |Compose variable binding modifiers.
--
--  Returns @Just a@ new variable binding modifier that corresponds to
--  applying the first supplied modifier and then applying the second
--  one, or @Nothing@ if the two modifiers cannot be compatibly composed.
--
--  NOTE:  this function does not, in general, commute.
--
--  NOTE:  if there are different ways to achieve the same usage, that
--  usage is currently repeated in the result returned.
--
vbmCompose :: (Eq a) => VarBindingModify a b -> VarBindingModify a b
    -> Maybe (VarBindingModify a b)
vbmCompose :: forall a b.
Eq a =>
VarBindingModify a b
-> VarBindingModify a b -> Maybe (VarBindingModify a b)
vbmCompose
    (VarBindingModify ScopedName
nam1 [VarBinding a b] -> [VarBinding a b]
app1 [a]
voc1 [[a]]
use1)
    (VarBindingModify ScopedName
nam2 [VarBinding a b] -> [VarBinding a b]
app2 [a]
voc2 [[a]]
use2)
    | Bool -> Bool
not ([[a]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[a]]
use12) = VarBindingModify a b -> Maybe (VarBindingModify a b)
forall a. a -> Maybe a
Just VarBindingModify
        { vbmName :: ScopedName
vbmName  = ScopedName
name
        , vbmApply :: [VarBinding a b] -> [VarBinding a b]
vbmApply = [VarBinding a b] -> [VarBinding a b]
app2 ([VarBinding a b] -> [VarBinding a b])
-> ([VarBinding a b] -> [VarBinding a b])
-> [VarBinding a b]
-> [VarBinding a b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VarBinding a b] -> [VarBinding a b]
app1
        , vbmVocab :: [a]
vbmVocab = [a]
voc1 [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`union` [a]
voc2
        , vbmUsage :: [[a]]
vbmUsage = [[a]]
use12
        }
    | Bool
otherwise = Maybe (VarBindingModify a b)
forall a. Maybe a
Nothing
    where
        use12 :: [[a]]
use12 = [a] -> [[a]] -> [[a]] -> [[a]]
forall a. Eq a => [a] -> [[a]] -> [[a]] -> [[a]]
compatibleUsage [a]
voc1 [[a]]
use1 [[a]]
use2
        getName :: ScopedName -> Text
getName = LName -> Text
getLName (LName -> Text) -> (ScopedName -> LName) -> ScopedName -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopedName -> LName
getScopeLocal
        -- since _ is a valid LName component then we know the mconcat output
        -- is a valid LName and so can use fromJust
        name :: ScopedName
name = LName -> ScopedName
swishName (LName -> ScopedName) -> LName -> ScopedName
forall a b. (a -> b) -> a -> b
$ Maybe LName -> LName
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe LName -> LName) -> Maybe LName -> LName
forall a b. (a -> b) -> a -> b
$ Text -> Maybe LName
newLName (Text -> Maybe LName) -> Text -> Maybe LName
forall a b. (a -> b) -> a -> b
$ [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat [Text
"_", ScopedName -> Text
getName ScopedName
nam1, Text
"_", ScopedName -> Text
getName ScopedName
nam2, Text
"_"]

-- |Determine compatible ways in which variable binding modifiers may
--  be combined.
--
--  The total vocabulary of a modifier is the complete set of variables
--  that are used or bound by the modifier.  After the modifier has been
--  applied, bindings must exist for all of these variables.
--
--  A usage pattern of a modifier is a set of variables for which new
--  bindings may be generated by the modifier.
--
--  The only way in which two variable binding modifiers can be incompatible
--  with each other is when they both attempt to create a new binding for
--  the same variable.  (Note that this does not mean the composition will
--  be compatible with all inputs:  see @vbmCompatibleVars@.)
--
--  NOTE:  if there are different ways to achieve the same usage, that
--  usage is currently repeated in the result returned.
--
compatibleUsage ::
  (Eq a)
  => [a]   -- ^ the total vocabulary of the first modifier to be applied
  -> [[a]] -- ^ usage patterns for the first modifier
  -> [[a]] -- ^ usage patterns for the second modifier
  -> [[a]] -- ^ a list of possible usage patterns for the composition of
           --  the first modifier with the second modifier, or an empty list if
           --  the modifiers are incompatible.
compatibleUsage :: forall a. Eq a => [a] -> [[a]] -> [[a]] -> [[a]]
compatibleUsage [a]
voc1 [[a]]
use1 [[a]]
use2 =
    [ [a]
u1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
u2 | [a]
u2 <- [[a]]
use2, [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a]
voc1 [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [a]
u2), [a]
u1 <- [[a]]
use1 ]

-- |Find all compatible compositions of a list of variable binding
--  modifiers for a given set of supplied bound variables.
findCompositions :: 
    (Eq a) => [VarBindingModify a b] 
    -> [a]
    -> [VarBindingModify a b]
findCompositions :: forall a b.
Eq a =>
[VarBindingModify a b] -> [a] -> [VarBindingModify a b]
findCompositions [VarBindingModify a b]
vbms [a]
vars =
    ([VarBindingModify a b] -> Maybe (VarBindingModify a b))
-> [[VarBindingModify a b]] -> [VarBindingModify a b]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([a] -> [VarBindingModify a b] -> Maybe (VarBindingModify a b)
forall a b.
Eq a =>
[a] -> [VarBindingModify a b] -> Maybe (VarBindingModify a b)
composeCheckSequence [a]
vars) ([VarBindingModify a b] -> [[VarBindingModify a b]]
forall a. [a] -> [[a]]
permutations [VarBindingModify a b]
vbms)

-- |Compose sequence of variable binding modifiers, and check
--  that the result can be used compatibly with a supplied list
--  of bound variables, returning @Just (composed modifier)@,
--  or @Nothing@.
--
composeCheckSequence :: (Eq a) => [a] -> [VarBindingModify a b]
    -> Maybe (VarBindingModify a b)
composeCheckSequence :: forall a b.
Eq a =>
[a] -> [VarBindingModify a b] -> Maybe (VarBindingModify a b)
composeCheckSequence [a]
vars [VarBindingModify a b]
vbms = [a] -> Maybe (VarBindingModify a b) -> Maybe (VarBindingModify a b)
forall {a} {b}.
Eq a =>
[a] -> Maybe (VarBindingModify a b) -> Maybe (VarBindingModify a b)
useWith [a]
vars (Maybe (VarBindingModify a b) -> Maybe (VarBindingModify a b))
-> Maybe (VarBindingModify a b) -> Maybe (VarBindingModify a b)
forall a b. (a -> b) -> a -> b
$ [VarBindingModify a b] -> Maybe (VarBindingModify a b)
forall a b.
Eq a =>
[VarBindingModify a b] -> Maybe (VarBindingModify a b)
composeSequence [VarBindingModify a b]
vbms
    where
        --  Check that a Maybe modifier is compatible for use with an
        --  indicated set of bound variables, and return (Just modifier)
        --  or Nothing.
        useWith :: [a] -> Maybe (VarBindingModify a b) -> Maybe (VarBindingModify a b)
useWith [a]
_    Maybe (VarBindingModify a b)
Nothing    = Maybe (VarBindingModify a b)
forall a. Maybe a
Nothing
        useWith [a]
vs v :: Maybe (VarBindingModify a b)
v@(Just VarBindingModify a b
vbm)
            | Maybe [a] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [a] -> Bool) -> Maybe [a] -> Bool
forall a b. (a -> b) -> a -> b
$ VarBindingModify a b -> [a] -> Maybe [a]
forall a b. Eq a => VarBindingModify a b -> [a] -> Maybe [a]
vbmCompatibility VarBindingModify a b
vbm [a]
vs = Maybe (VarBindingModify a b)
v
            | Bool
otherwise                        = Maybe (VarBindingModify a b)
forall a. Maybe a
Nothing

-- |Compose sequence of variable binding modifiers.
--
composeSequence :: (Eq a) => [VarBindingModify a b]
    -> Maybe (VarBindingModify a b)
composeSequence :: forall a b.
Eq a =>
[VarBindingModify a b] -> Maybe (VarBindingModify a b)
composeSequence [] = VarBindingModify a b -> Maybe (VarBindingModify a b)
forall a. a -> Maybe a
Just VarBindingModify a b
forall a b. VarBindingModify a b
varBindingId
composeSequence (VarBindingModify a b
vbm:[VarBindingModify a b]
vbms) = (Maybe (VarBindingModify a b)
 -> VarBindingModify a b -> Maybe (VarBindingModify a b))
-> Maybe (VarBindingModify a b)
-> [VarBindingModify a b]
-> Maybe (VarBindingModify a b)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Maybe (VarBindingModify a b)
-> VarBindingModify a b -> Maybe (VarBindingModify a b)
forall a b.
Eq a =>
Maybe (VarBindingModify a b)
-> VarBindingModify a b -> Maybe (VarBindingModify a b)
composePair (VarBindingModify a b -> Maybe (VarBindingModify a b)
forall a. a -> Maybe a
Just VarBindingModify a b
vbm) [VarBindingModify a b]
vbms

-- |Compose a pair of variable binding modifiers, returning
--  @Just (composed modifier)@, or @Nothing@.
--
composePair :: (Eq a) => Maybe (VarBindingModify a b) -> VarBindingModify a b
    -> Maybe (VarBindingModify a b)
composePair :: forall a b.
Eq a =>
Maybe (VarBindingModify a b)
-> VarBindingModify a b -> Maybe (VarBindingModify a b)
composePair Maybe (VarBindingModify a b)
Nothing     VarBindingModify a b
_    = Maybe (VarBindingModify a b)
forall a. Maybe a
Nothing
composePair (Just VarBindingModify a b
vbm1) VarBindingModify a b
vbm2 = VarBindingModify a b
-> VarBindingModify a b -> Maybe (VarBindingModify a b)
forall a b.
Eq a =>
VarBindingModify a b
-> VarBindingModify a b -> Maybe (VarBindingModify a b)
vbmCompose VarBindingModify a b
vbm1 VarBindingModify a b
vbm2

-- |Return @Just a@ compatible composition of variable binding modifiers
--  for a given set of supplied bound variables, or @Nothing@ if there
--  is no compatible composition
--
findComposition :: (Eq a) => [VarBindingModify a b] -> [a]
    -> Maybe (VarBindingModify a b)
findComposition :: forall a b.
Eq a =>
[VarBindingModify a b] -> [a] -> Maybe (VarBindingModify a b)
findComposition = [VarBindingModify a b] -> Maybe (VarBindingModify a b)
forall a. [a] -> Maybe a
listToMaybe ([VarBindingModify a b] -> Maybe (VarBindingModify a b))
-> ([VarBindingModify a b] -> [a] -> [VarBindingModify a b])
-> [VarBindingModify a b]
-> [a]
-> Maybe (VarBindingModify a b)
forall {b} {c} {a} {a}. (b -> c) -> (a -> a -> b) -> a -> a -> c
`c2` [VarBindingModify a b] -> [a] -> [VarBindingModify a b]
forall a b.
Eq a =>
[VarBindingModify a b] -> [a] -> [VarBindingModify a b]
findCompositions
    where
        c2 :: (b -> c) -> (a -> a -> b) -> a -> a -> c
c2 = ((a -> b) -> a -> c) -> (a -> a -> b) -> a -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (((a -> b) -> a -> c) -> (a -> a -> b) -> a -> a -> c)
-> ((b -> c) -> (a -> b) -> a -> c)
-> (b -> c)
-> (a -> a -> b)
-> a
-> a
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)  -- compose with function of two arguments

-- |Variable binding modifier that returns exactly those
--  variable bindings presented.
--
varBindingId :: VarBindingModify a b
varBindingId :: forall a b. VarBindingModify a b
varBindingId = VarBindingModify
    { vbmName :: ScopedName
vbmName   = LName -> ScopedName
swishName LName
"varBindingId"
    , vbmApply :: [VarBinding a b] -> [VarBinding a b]
vbmApply  = [VarBinding a b] -> [VarBinding a b]
forall a. a -> a
id
    , vbmVocab :: [a]
vbmVocab  = []
    , vbmUsage :: [[a]]
vbmUsage  = [[]]
    }

-- |Null variable binding modifier
--
--  This is like 'varBindingId' except parameterized by some labels.
--  I think this is redundant, and should be eliminated.
--
nullVarBindingModify :: OpenVarBindingModify a b
nullVarBindingModify :: forall a b. OpenVarBindingModify a b
nullVarBindingModify [a]
lbs = VarBindingModify
    { vbmName :: ScopedName
vbmName   = LName -> ScopedName
swishName LName
"nullVarBindingModify"
    , vbmApply :: [VarBinding a b] -> [VarBinding a b]
vbmApply  = [VarBinding a b] -> [VarBinding a b]
forall a. a -> a
id
    , vbmVocab :: [a]
vbmVocab  = [a]
lbs
    , vbmUsage :: [[a]]
vbmUsage  = [[]]
    }

------------------------------------------------------------
--  Query binding filters
------------------------------------------------------------

-- |VarBindingFilter is a function type that tests to see if
--  a query binding satisfies some criterion.
--
--  Queries often want to apply some kind of filter or condition
--  to the variable bindings that are processed.  In inference rules,
--  it sometimes seems desirable to stipulate additional conditions on
--  the things that are matched.
--
--  This function type is used to perform such tests.
--  A number of simple implementations are included below.
data VarBindingFilter a b = VarBindingFilter
    { forall a b. VarBindingFilter a b -> ScopedName
vbfName   :: ScopedName
    , forall a b. VarBindingFilter a b -> [a]
vbfVocab  :: [a]
    , forall a b. VarBindingFilter a b -> VarBinding a b -> Bool
vbfTest   :: VarBinding a b -> Bool
    }

-- |Make a variable binding modifier from a variable binding filter value.
makeVarFilterModify :: VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify :: forall a b. VarBindingFilter a b -> VarBindingModify a b
makeVarFilterModify VarBindingFilter a b
vbf = VarBindingModify
    { vbmName :: ScopedName
vbmName   = VarBindingFilter a b -> ScopedName
forall a b. VarBindingFilter a b -> ScopedName
vbfName VarBindingFilter a b
vbf
    , vbmApply :: [VarBinding a b] -> [VarBinding a b]
vbmApply  = (VarBinding a b -> Bool) -> [VarBinding a b] -> [VarBinding a b]
forall a. (a -> Bool) -> [a] -> [a]
filter (VarBindingFilter a b -> VarBinding a b -> Bool
forall a b. VarBindingFilter a b -> VarBinding a b -> Bool
vbfTest VarBindingFilter a b
vbf)
    , vbmVocab :: [a]
vbmVocab  = VarBindingFilter a b -> [a]
forall a b. VarBindingFilter a b -> [a]
vbfVocab VarBindingFilter a b
vbf
    , vbmUsage :: [[a]]
vbmUsage  = [[]]
    }

-- |Make a variable test filter for a named variable using a
--  supplied value testing function.
makeVarTestFilter ::
    ScopedName -> (b -> Bool) -> a -> VarBindingFilter a b
makeVarTestFilter :: forall b a. ScopedName -> (b -> Bool) -> a -> VarBindingFilter a b
makeVarTestFilter ScopedName
nam b -> Bool
vtest a
var = VarBindingFilter
    { vbfName :: ScopedName
vbfName   = ScopedName
nam
    , vbfVocab :: [a]
vbfVocab  = [a
var]
    , vbfTest :: VarBinding a b -> Bool
vbfTest   = \VarBinding a b
vb -> Bool -> (b -> Bool) -> Maybe b -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False b -> Bool
vtest (VarBinding a b -> a -> Maybe b
forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding a b
vb a
var)
    }

-- |Make a variable comparison filter for named variables using
--  a supplied value comparison function.
makeVarCompareFilter ::
    ScopedName -> (b -> b -> Bool) -> a -> a -> VarBindingFilter a b
makeVarCompareFilter :: forall b a.
ScopedName -> (b -> b -> Bool) -> a -> a -> VarBindingFilter a b
makeVarCompareFilter ScopedName
nam b -> b -> Bool
vcomp a
v1 a
v2 = VarBindingFilter
    { vbfName :: ScopedName
vbfName   = ScopedName
nam
    , vbfVocab :: [a]
vbfVocab  = [a
v1,a
v2]
    , vbfTest :: VarBinding a b -> Bool
vbfTest   = \VarBinding a b
vb -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== (b -> b -> Bool
vcomp (b -> b -> Bool) -> Maybe b -> Maybe (b -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VarBinding a b -> a -> Maybe b
forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding a b
vb a
v1 Maybe (b -> Bool) -> Maybe b -> Maybe Bool
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VarBinding a b -> a -> Maybe b
forall a b. VarBinding a b -> a -> Maybe b
vbMap VarBinding a b
vb a
v2)
    }

------------------------------------------------------------
--  Declare some generally useful query binding filters
------------------------------------------------------------

-- |This function generates a query binding filter that ensures that
--  two indicated query variables are mapped to the same value.
varFilterEQ :: (Eq b) => a -> a -> VarBindingFilter a b
varFilterEQ :: forall b a. Eq b => a -> a -> VarBindingFilter a b
varFilterEQ =
    ScopedName -> (b -> b -> Bool) -> a -> a -> VarBindingFilter a b
forall b a.
ScopedName -> (b -> b -> Bool) -> a -> a -> VarBindingFilter a b
makeVarCompareFilter (LName -> ScopedName
swishName LName
"varFilterEQ") b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(==) 

-- |This function generates a query binding filter that ensures that
--  two indicated query variables are mapped to different values.
varFilterNE :: (Eq b) => a -> a -> VarBindingFilter a b
varFilterNE :: forall b a. Eq b => a -> a -> VarBindingFilter a b
varFilterNE =
    ScopedName -> (b -> b -> Bool) -> a -> a -> VarBindingFilter a b
forall b a.
ScopedName -> (b -> b -> Bool) -> a -> a -> VarBindingFilter a b
makeVarCompareFilter (LName -> ScopedName
swishName LName
"varFilterNE") b -> b -> Bool
forall a. Eq a => a -> a -> Bool
(/=) 

-- |This function composes a number of query binding filters
--  into a composite filter that accepts any query binding that
--  satisfies at least one of the component values.
varFilterDisjunction :: (Eq a) => [VarBindingFilter a b]
    -> VarBindingFilter a b
varFilterDisjunction :: forall a b. Eq a => [VarBindingFilter a b] -> VarBindingFilter a b
varFilterDisjunction [VarBindingFilter a b]
vbfs = VarBindingFilter
    { vbfName :: ScopedName
vbfName   = LName -> ScopedName
swishName LName
"varFilterDisjunction"
    , vbfVocab :: [a]
vbfVocab  = ([a] -> [a] -> [a]) -> [[a]] -> [a]
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
union ((VarBindingFilter a b -> [a]) -> [VarBindingFilter a b] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map VarBindingFilter a b -> [a]
forall a b. VarBindingFilter a b -> [a]
vbfVocab [VarBindingFilter a b]
vbfs)
    , vbfTest :: VarBinding a b -> Bool
vbfTest   = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool)
-> (VarBinding a b -> [Bool]) -> VarBinding a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VarBinding a b -> Bool] -> VarBinding a b -> [Bool]
forall a b. [a -> b] -> a -> [b]
flist ((VarBindingFilter a b -> VarBinding a b -> Bool)
-> [VarBindingFilter a b] -> [VarBinding a b -> Bool]
forall a b. (a -> b) -> [a] -> [b]
map VarBindingFilter a b -> VarBinding a b -> Bool
forall a b. VarBindingFilter a b -> VarBinding a b -> Bool
vbfTest [VarBindingFilter a b]
vbfs)
    }

-- |This function composes a number of query binding filters
--  into a composite filter that accepts any query binding that
--  satisfies all of the component values.
--
--  The same function could be achieved by composing the component
--  filter-based modifiers, but this function is more convenient
--  as it avoids the need to check for modifier compatibility.
--
varFilterConjunction :: (Eq a) => [VarBindingFilter a b]
    -> VarBindingFilter a b
varFilterConjunction :: forall a b. Eq a => [VarBindingFilter a b] -> VarBindingFilter a b
varFilterConjunction [VarBindingFilter a b]
vbfs = VarBindingFilter
    { vbfName :: ScopedName
vbfName   = LName -> ScopedName
swishName LName
"varFilterConjunction"
    , vbfVocab :: [a]
vbfVocab  = ([a] -> [a] -> [a]) -> [[a]] -> [a]
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
union ((VarBindingFilter a b -> [a]) -> [VarBindingFilter a b] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map VarBindingFilter a b -> [a]
forall a b. VarBindingFilter a b -> [a]
vbfVocab [VarBindingFilter a b]
vbfs)
    , vbfTest :: VarBinding a b -> Bool
vbfTest   = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool)
-> (VarBinding a b -> [Bool]) -> VarBinding a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VarBinding a b -> Bool] -> VarBinding a b -> [Bool]
forall a b. [a -> b] -> a -> [b]
flist ((VarBindingFilter a b -> VarBinding a b -> Bool)
-> [VarBindingFilter a b] -> [VarBinding a b -> Bool]
forall a b. (a -> b) -> [a] -> [b]
map VarBindingFilter a b -> VarBinding a b -> Bool
forall a b. VarBindingFilter a b -> VarBinding a b -> Bool
vbfTest [VarBindingFilter a b]
vbfs)
    }

--------------------------------------------------------------------------------
--
--  (c) 2003, Graham Klyne, 2009 Vasili I Galchin,
--    2011, 2012, 2020, 2022 Douglas Burke
--  All rights reserved.
--
--  This file is part of Swish.
--
--  Swish is free software; you can redistribute it and/or modify
--  it under the terms of the GNU General Public License as published by
--  the Free Software Foundation; either version 2 of the License, or
--  (at your option) any later version.
--
--  Swish is distributed in the hope that it will be useful,
--  but WITHOUT ANY WARRANTY; without even the implied warranty of
--  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
--  GNU General Public License for more details.
--
--  You should have received a copy of the GNU General Public License
--  along with Swish; if not, write to:
--    The Free Software Foundation, Inc.,
--    59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
--
--------------------------------------------------------------------------------