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

--------------------------------------------------------------------------------
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
--  Module      :  ClassRestrictionRule
--  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin,
--                 2011, 2012, 2014, 2018, 2022 Douglas Burke
--  License     :  GPL V2
--
--  Maintainer  :  Douglas Burke
--  Stability   :  experimental
--  Portability :  CPP, OverloadedStrings
--
--  This module implements an inference rule based on a restruction on class
--  membership of one or more values.
--
--------------------------------------------------------------------------------

module Swish.RDF.ClassRestrictionRule
       ( ClassRestriction(..), ClassRestrictionFn
       , makeDatatypeRestriction, makeDatatypeRestrictionFn
       , makeRDFClassRestrictionRules
       , makeRDFDatatypeRestrictionRules
       , falseGraph, falseGraphStr       
       )
       where

import Swish.Datatype (DatatypeVal(..), DatatypeRel(..), DatatypeRelFn)
import Swish.Namespace (Namespace, ScopedName, namespaceToBuilder)
import Swish.Rule (Rule(..), bwdCheckInference)
import Swish.VarBinding (VarBinding(..))

import Swish.RDF.Graph
    ( RDFLabel(..)
    , getScopedName
    , RDFGraph
    , getArcs
    , merge
    , toRDFGraph, emptyRDFGraph
    , Arc(..)
    , resRdfType
    , resRdfdMaxCardinality
    )

import Swish.RDF.Datatype (RDFDatatypeVal, fromRDFLabel, toRDFLabel)
import Swish.RDF.Ruleset (RDFRule, makeRDFGraphFromN3Builder)

import Swish.RDF.Query
    ( rdfQueryFind
    , rdfFindValSubj, rdfFindPredVal, rdfFindPredInt
    , rdfFindList
    )

import Swish.RDF.VarBinding (RDFVarBinding)
import Swish.RDF.Vocabulary (namespaceRDFD)

#if (!defined(__GLASGOW_HASKELL__)) || (__GLASGOW_HASKELL__ < 808)
import Control.Applicative ((<$>))
#endif

import Data.List (delete, nub, subsequences)
import Data.Maybe (fromJust, fromMaybe, mapMaybe)
import Data.Ord.Partial (minima, maxima, partCompareEq, partComparePair, partCompareListMaybe, partCompareListSubset)

#if (!defined(__GLASGOW_HASKELL__)) || (__GLASGOW_HASKELL__ < 710)
import Data.Monoid (Monoid (..))
#endif

import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.Text.Lazy.Builder as B

------------------------------------------------------------
--  Class restriction data type
------------------------------------------------------------

-- |Type of function that evaluates missing node values in a
--  restriction from those supplied.
type ClassRestrictionFn = [Maybe RDFLabel] -> Maybe [[RDFLabel]]

-- |Datatype for named class restriction
data ClassRestriction = ClassRestriction
    { ClassRestriction -> ScopedName
crName    :: ScopedName
    , ClassRestriction -> ClassRestrictionFn
crFunc    :: ClassRestrictionFn
    }

-- | Equality of class restrictions is based on the name of the restriction.
instance Eq ClassRestriction where
    ClassRestriction
cr1 == :: ClassRestriction -> ClassRestriction -> Bool
== ClassRestriction
cr2  =  ClassRestriction -> ScopedName
crName ClassRestriction
cr1 forall a. Eq a => a -> a -> Bool
== ClassRestriction -> ScopedName
crName ClassRestriction
cr2

instance Show ClassRestriction where
    show :: ClassRestriction -> String
show ClassRestriction
cr = String
"ClassRestriction:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ClassRestriction -> ScopedName
crName ClassRestriction
cr)

------------------------------------------------------------
--  Instantiate a class restriction from a datatype relation
------------------------------------------------------------

-- |Make a class restriction from a datatype relation.
--
--  This lifts application of the datatype relation to operate
--  on 'RDFLabel' values, which are presumed to contain appropriately
--  datatyped values.
--
makeDatatypeRestriction ::
    RDFDatatypeVal vt -> DatatypeRel vt -> ClassRestriction
makeDatatypeRestriction :: forall vt. RDFDatatypeVal vt -> DatatypeRel vt -> ClassRestriction
makeDatatypeRestriction RDFDatatypeVal vt
dtv DatatypeRel vt
dtrel = ClassRestriction
    { crName :: ScopedName
crName = forall vt. DatatypeRel vt -> ScopedName
dtRelName DatatypeRel vt
dtrel
    , crFunc :: ClassRestrictionFn
crFunc = forall vt.
RDFDatatypeVal vt -> DatatypeRelFn vt -> ClassRestrictionFn
makeDatatypeRestrictionFn RDFDatatypeVal vt
dtv (forall vt. DatatypeRel vt -> DatatypeRelFn vt
dtRelFunc DatatypeRel vt
dtrel)
    }

--  The core logic below is something like @(map toLabels . dtrelfn . map frLabel)@
--  but the extra lifting and catMaybes are needed to get the final result
--  type in the right form.

-- |Make a class restriction function from a datatype relation function.
--
makeDatatypeRestrictionFn ::
    RDFDatatypeVal vt -> DatatypeRelFn vt -> ClassRestrictionFn
makeDatatypeRestrictionFn :: forall vt.
RDFDatatypeVal vt -> DatatypeRelFn vt -> ClassRestrictionFn
makeDatatypeRestrictionFn RDFDatatypeVal vt
dtv DatatypeRelFn vt
dtrelfn =
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe [vt] -> Maybe [RDFLabel]
toLabels) forall b c a. (b -> c) -> (a -> b) -> a -> c
. DatatypeRelFn vt
dtrelfn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Maybe RDFLabel -> Maybe vt
frLabel
    where
        frLabel :: Maybe RDFLabel -> Maybe vt
frLabel Maybe RDFLabel
Nothing  = forall a. Maybe a
Nothing
        frLabel (Just RDFLabel
l) = forall vt. RDFDatatypeVal vt -> RDFLabel -> Maybe vt
fromRDFLabel RDFDatatypeVal vt
dtv RDFLabel
l
        toLabels :: [vt] -> Maybe [RDFLabel]
toLabels         = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM vt -> Maybe RDFLabel
toLabel   -- Maybe [RDFLabel]
        toLabel :: vt -> Maybe RDFLabel
toLabel          = forall vt. RDFDatatypeVal vt -> vt -> Maybe RDFLabel
toRDFLabel RDFDatatypeVal vt
dtv

------------------------------------------------------------
--  Make rules from supplied class restrictions and graph
------------------------------------------------------------

mkPrefix :: Namespace -> B.Builder
mkPrefix :: Namespace -> Builder
mkPrefix = Namespace -> Builder
namespaceToBuilder

ruleQuery :: RDFGraph
ruleQuery :: RDFGraph
ruleQuery = Builder -> RDFGraph
makeRDFGraphFromN3Builder forall a b. (a -> b) -> a -> b
$
            forall a. Monoid a => [a] -> a
mconcat
            [ Namespace -> Builder
mkPrefix Namespace
namespaceRDFD
            , Builder
" ?c a rdfd:GeneralRestriction ; "
            , Builder
"    rdfd:onProperties ?p ; "     
            , Builder
"    rdfd:constraint   ?r . "
            ]
            
-- | The graph
--
-- > _:a <http://id.ninebynine.org/2003/rdfext/rdfd#false> _:b .
--
-- Exported for testing.
falseGraph :: RDFGraph
falseGraph :: RDFGraph
falseGraph = Builder -> RDFGraph
makeRDFGraphFromN3Builder forall a b. (a -> b) -> a -> b
$
             Namespace -> Builder
mkPrefix Namespace
namespaceRDFD forall a. Monoid a => a -> a -> a
`mappend` Builder
falseGraphStr

-- | Exported for testing.
falseGraphStr :: B.Builder
falseGraphStr :: Builder
falseGraphStr = Builder
"_:a rdfd:false _:b . "

-- |Make a list of class restriction rules given a list of class restriction
--  values and a graph containing one or more class restriction definitions.
--
makeRDFClassRestrictionRules :: [ClassRestriction] -> RDFGraph -> [RDFRule]
makeRDFClassRestrictionRules :: [ClassRestriction] -> RDFGraph -> [RDFRule]
makeRDFClassRestrictionRules [ClassRestriction]
crs RDFGraph
gr =
    forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe RDFVarBinding -> Maybe RDFRule
constructRule (RDFGraph -> [RDFVarBinding]
queryForRules RDFGraph
gr)
    where
        queryForRules :: RDFGraph -> [RDFVarBinding]
queryForRules = RDFGraph -> RDFGraph -> [RDFVarBinding]
rdfQueryFind RDFGraph
ruleQuery
        constructRule :: RDFVarBinding -> Maybe RDFRule
constructRule = [ClassRestriction] -> RDFGraph -> RDFVarBinding -> Maybe RDFRule
makeRestrictionRule1 [ClassRestriction]
crs RDFGraph
gr

makeRestrictionRule1 ::
    [ClassRestriction] -> RDFGraph -> RDFVarBinding -> Maybe RDFRule
makeRestrictionRule1 :: [ClassRestriction] -> RDFGraph -> RDFVarBinding -> Maybe RDFRule
makeRestrictionRule1 [ClassRestriction]
crs RDFGraph
gr RDFVarBinding
vb =
    Maybe ClassRestriction
-> RDFLabel -> [RDFLabel] -> [Int] -> Maybe RDFRule
makeRestrictionRule2 Maybe ClassRestriction
rn RDFLabel
c [RDFLabel]
ps [Int]
cs
    where
        c :: RDFLabel
c  = forall a. a -> Maybe a -> a
fromMaybe RDFLabel
NoNode forall a b. (a -> b) -> a -> b
$ forall a b. VarBinding a b -> a -> Maybe b
vbMap RDFVarBinding
vb (String -> RDFLabel
Var String
"c")
        p :: RDFLabel
p  = forall a. a -> Maybe a -> a
fromMaybe RDFLabel
NoNode forall a b. (a -> b) -> a -> b
$ forall a b. VarBinding a b -> a -> Maybe b
vbMap RDFVarBinding
vb (String -> RDFLabel
Var String
"p")
        r :: RDFLabel
r  = forall a. a -> Maybe a -> a
fromMaybe RDFLabel
NoNode forall a b. (a -> b) -> a -> b
$ forall a b. VarBinding a b -> a -> Maybe b
vbMap RDFVarBinding
vb (String -> RDFLabel
Var String
"r")
        cs :: [Int]
cs = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Num a => Integer -> a
fromInteger forall a b. (a -> b) -> a -> b
$
             RDFLabel -> RDFLabel -> RDFGraph -> [Integer]
rdfFindPredInt RDFLabel
c RDFLabel
resRdfdMaxCardinality RDFGraph
gr
        ps :: [RDFLabel]
ps = RDFGraph -> RDFLabel -> [RDFLabel]
rdfFindList RDFGraph
gr RDFLabel
p

        -- TODO: do not need to go via a map since looking through a list
        rn :: Maybe ClassRestriction
rn = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (RDFLabel -> ScopedName
getScopedName RDFLabel
r) forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\ClassRestriction
cr -> (ClassRestriction -> ScopedName
crName ClassRestriction
cr, ClassRestriction
cr)) [ClassRestriction]
crs

makeRestrictionRule2 ::
    Maybe ClassRestriction -> RDFLabel -> [RDFLabel] -> [Int]
    -> Maybe RDFRule
makeRestrictionRule2 :: Maybe ClassRestriction
-> RDFLabel -> [RDFLabel] -> [Int] -> Maybe RDFRule
makeRestrictionRule2 (Just ClassRestriction
restriction) cls :: RDFLabel
cls@(Res ScopedName
cname) [RDFLabel]
props [Int]
cs =
    forall a. a -> Maybe a
Just RDFRule
restrictionRule
    where
        restrictionRule :: RDFRule
restrictionRule = Rule
            { ruleName :: ScopedName
ruleName = ScopedName
cname
              -- fwdApply :: [ex] -> [ex]
            , fwdApply :: [RDFGraph] -> [RDFGraph]
fwdApply = ClassRestriction
-> RDFLabel -> [RDFLabel] -> [Int] -> [RDFGraph] -> [RDFGraph]
fwdApplyRestriction ClassRestriction
restriction RDFLabel
cls [RDFLabel]
props [Int]
cs
              -- bwdApply :: ex -> [[ex]]
            , bwdApply :: RDFGraph -> [[RDFGraph]]
bwdApply = ClassRestriction
-> RDFLabel -> [RDFLabel] -> [Int] -> RDFGraph -> [[RDFGraph]]
bwdApplyRestriction ClassRestriction
restriction RDFLabel
cls [RDFLabel]
props [Int]
cs
            , checkInference :: [RDFGraph] -> RDFGraph -> Bool
checkInference = forall ex. Eq ex => Rule ex -> [ex] -> ex -> Bool
bwdCheckInference RDFRule
restrictionRule
            }
makeRestrictionRule2 Maybe ClassRestriction
_ RDFLabel
_ [RDFLabel]
_ [Int]
_ = forall a. Maybe a
Nothing
    -- trace "\nmakeRestrictionRule: missing class restriction"

--  Forward apply class restriction.
fwdApplyRestriction ::
    ClassRestriction -> RDFLabel -> [RDFLabel] -> [Int] -> [RDFGraph]
    -> [RDFGraph]
fwdApplyRestriction :: ClassRestriction
-> RDFLabel -> [RDFLabel] -> [Int] -> [RDFGraph] -> [RDFGraph]
fwdApplyRestriction ClassRestriction
restriction RDFLabel
cls [RDFLabel]
props [Int]
cs [RDFGraph]
antgrs =
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe [RDFGraph
falseGraph] forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat Maybe [[RDFGraph]]
newgrs
      where
        -- Instances of the named class in the graph:
        ris :: [RDFLabel]
ris = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ RDFLabel -> RDFLabel -> RDFGraph -> [RDFLabel]
rdfFindValSubj RDFLabel
resRdfType RDFLabel
cls RDFGraph
antgr
        --  Merge antecedent graphs into one (with bnode renaming):
        --  (Uses 'if' and 'foldl1' to avoid merging in the common case
        --  of just one graph supplied.)
        antgr :: RDFGraph
antgr = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RDFGraph]
antgrs then RDFGraph
emptyRDFGraph else forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 forall lb. Label lb => NSGraph lb -> NSGraph lb -> NSGraph lb
merge [RDFGraph]
antgrs
        --  Apply class restriction to single instance of the restricted class
        newgr :: RDFLabel -> Maybe [RDFGraph]
        newgr :: RDFLabel -> Maybe [RDFGraph]
newgr RDFLabel
ri = ClassRestriction
-> RDFLabel -> [RDFLabel] -> [Int] -> RDFGraph -> Maybe [RDFGraph]
fwdApplyRestriction1 ClassRestriction
restriction RDFLabel
ri [RDFLabel]
props [Int]
cs RDFGraph
antgr
        newgrs :: Maybe [[RDFGraph]]
        newgrs :: Maybe [[RDFGraph]]
newgrs = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RDFLabel -> Maybe [RDFGraph]
newgr [RDFLabel]
ris

--  Forward apply class restriction to single class instance (ci).
--  Return single set of inferred results, for each combination of
--  property values, or an empty list, or Nothing if the supplied values
--  are inconsistent with the restriction.
fwdApplyRestriction1 ::
    ClassRestriction -> RDFLabel -> [RDFLabel] -> [Int] -> RDFGraph
    -> Maybe [RDFGraph]
fwdApplyRestriction1 :: ClassRestriction
-> RDFLabel -> [RDFLabel] -> [Int] -> RDFGraph -> Maybe [RDFGraph]
fwdApplyRestriction1 ClassRestriction
restriction RDFLabel
ci [RDFLabel]
props [Int]
cs RDFGraph
antgr =
    if Bool
grConsistent then forall a. a -> Maybe a
Just [RDFGraph]
newgrs else forall a. Maybe a
Nothing
    where
        --  Apply restriction to graph
        (Bool
grConsistent,[[RDFLabel]]
_,[([Maybe RDFLabel], [[RDFLabel]])]
_,[[Maybe RDFLabel]]
sts) = ClassRestriction
-> RDFLabel
-> [RDFLabel]
-> [Int]
-> RDFGraph
-> (Bool, [[RDFLabel]], [([Maybe RDFLabel], [[RDFLabel]])],
    [[Maybe RDFLabel]])
applyRestriction ClassRestriction
restriction RDFLabel
ci [RDFLabel]
props [Int]
cs RDFGraph
antgr
        --  Select results, eliminate those with unknowns
        nts :: [[RDFLabel]]
        nts :: [[RDFLabel]]
nts = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[Maybe RDFLabel]]
sts
        --  Make new graph from results, including only newly generated arcs
        newarcs :: Set (Arc RDFLabel)
newarcs = forall a. Ord a => [a] -> Set a
S.fromList [forall lb. lb -> lb -> lb -> Arc lb
Arc RDFLabel
ci RDFLabel
p RDFLabel
v | [RDFLabel]
vs <- [[RDFLabel]]
nts, (RDFLabel
p,RDFLabel
v) <- forall a b. [a] -> [b] -> [(a, b)]
zip [RDFLabel]
props [RDFLabel]
vs ]
                  forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall (lg :: * -> *) lb. LDGraph lg lb => lg lb -> ArcSet lb
getArcs RDFGraph
antgr
        newgrs :: [RDFGraph]
newgrs  = if forall a. Set a -> Bool
S.null Set (Arc RDFLabel)
newarcs then [] else [Set (Arc RDFLabel) -> RDFGraph
toRDFGraph Set (Arc RDFLabel)
newarcs]

--  Backward apply class restriction.
--
--  Returns a list of alternatives, any one of which is sufficient to
--  satisfy the given consequent.
--
bwdApplyRestriction ::
    ClassRestriction -> RDFLabel -> [RDFLabel] -> [Int] -> RDFGraph
    -> [[RDFGraph]]
bwdApplyRestriction :: ClassRestriction
-> RDFLabel -> [RDFLabel] -> [Int] -> RDFGraph -> [[RDFGraph]]
bwdApplyRestriction ClassRestriction
restriction RDFLabel
cls [RDFLabel]
props [Int]
cs RDFGraph
congr =
    forall a. a -> Maybe a -> a
fromMaybe [[RDFGraph
falseGraph]] Maybe [[RDFGraph]]
newgrs
    where
        -- Instances of the named class in the graph:
        ris :: [RDFLabel]
ris = RDFLabel -> RDFLabel -> RDFGraph -> [RDFLabel]
rdfFindValSubj RDFLabel
resRdfType RDFLabel
cls RDFGraph
congr
        --  Apply class restriction to single instance of the restricted class
        newgr :: RDFLabel -> Maybe [[RDFGraph]]
        newgr :: RDFLabel -> Maybe [[RDFGraph]]
newgr RDFLabel
ri = ClassRestriction
-> RDFLabel
-> RDFLabel
-> [RDFLabel]
-> [Int]
-> RDFGraph
-> Maybe [[RDFGraph]]
bwdApplyRestriction1 ClassRestriction
restriction RDFLabel
cls RDFLabel
ri [RDFLabel]
props [Int]
cs RDFGraph
congr
        --  'map newgr ris' is conjunction of disjunctions, where
        --  each disjunction is itself a conjunction of conjunctions.
        --  'sequence' distributes the conjunction over the disjunction,
        --  yielding an equivalent disjunction of conjunctions
        --  map concat flattens the conjunctions of conjuctions
        newgrs :: Maybe [[RDFGraph]]
        newgrs :: Maybe [[RDFGraph]]
newgrs = forall a b. (a -> b) -> [a] -> [b]
map forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RDFLabel -> Maybe [[RDFGraph]]
newgr [RDFLabel]
ris

--  Backward apply a class restriction to single class instance (ci).
--  Return one or more sets of antecedent results from which the consequence
--  can be derived in the defined relation, an empty list if the supplied
--  consequence cannot be inferred, or Nothing if the consequence is
--  inconsistent with the restriction.
bwdApplyRestriction1 ::
    ClassRestriction -> RDFLabel -> RDFLabel -> [RDFLabel] -> [Int] -> RDFGraph
    -> Maybe [[RDFGraph]]
bwdApplyRestriction1 :: ClassRestriction
-> RDFLabel
-> RDFLabel
-> [RDFLabel]
-> [Int]
-> RDFGraph
-> Maybe [[RDFGraph]]
bwdApplyRestriction1 ClassRestriction
restriction RDFLabel
cls RDFLabel
ci [RDFLabel]
props [Int]
cs RDFGraph
congr =
    if Bool
grConsistent then forall a. a -> Maybe a
Just [[RDFGraph]]
grss else forall a. Maybe a
Nothing
    where
        --  Apply restriction to graph
        (Bool
grConsistent,[[RDFLabel]]
pvs,[([Maybe RDFLabel], [[RDFLabel]])]
cts,[[Maybe RDFLabel]]
_) =
            ClassRestriction
-> RDFLabel
-> [RDFLabel]
-> [Int]
-> RDFGraph
-> (Bool, [[RDFLabel]], [([Maybe RDFLabel], [[RDFLabel]])],
    [[Maybe RDFLabel]])
applyRestriction ClassRestriction
restriction RDFLabel
ci [RDFLabel]
props [Int]
cs RDFGraph
congr
        --  Build list of all full tuples consistent with the values supplied
        fts :: [[RDFLabel]]
        fts :: [[RDFLabel]]
fts = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd [([Maybe RDFLabel], [[RDFLabel]])]
cts
        --  Construct partial tuples from members of fts from which at least
        --  one of the supplied values can be derived
        pts :: [([Maybe RDFLabel],[RDFLabel])]
        pts :: [([Maybe RDFLabel], [RDFLabel])]
pts = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ClassRestriction -> [RDFLabel] -> [([Maybe RDFLabel], [RDFLabel])]
deriveTuple ClassRestriction
restriction) [[RDFLabel]]
fts
        --  Select combinations of members of pts from which all the
        --  supplied values can be derived
        dtss :: [[[Maybe RDFLabel]]]
        dtss :: [[[Maybe RDFLabel]]]
dtss = forall a. Eq a => [[a]] -> [([Maybe a], [a])] -> [[[Maybe a]]]
coverSets [[RDFLabel]]
pvs [([Maybe RDFLabel], [RDFLabel])]
pts
        --  Filter members of dtss that fully cover the values
        --  obtained from the consequence graph.
        ftss :: [[[Maybe RDFLabel]]]
        ftss :: [[[Maybe RDFLabel]]]
ftss = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\[[Maybe RDFLabel]]
t -> forall a b. (a -> [b] -> [b]) -> [[a]] -> [[b]] -> Bool
coversVals forall a. Eq a => Maybe a -> [a] -> [a]
deleteMaybe [[Maybe RDFLabel]]
t [[RDFLabel]]
pvs)) [[[Maybe RDFLabel]]]
dtss
        --  Make new graphs for all alternatives
        grss :: [[RDFGraph]]
        grss :: [[RDFGraph]]
grss = forall a b. (a -> b) -> [a] -> [b]
map ( [Arc RDFLabel] -> [RDFGraph]
makeGraphs forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Maybe RDFLabel]] -> [Arc RDFLabel]
newArcs ) [[[Maybe RDFLabel]]]
ftss

        --  Collect arcs for one alternative
        newArcs :: [[Maybe RDFLabel]] -> [Arc RDFLabel]
newArcs [[Maybe RDFLabel]]
dts =
            [ forall lb. lb -> lb -> lb -> Arc lb
Arc RDFLabel
ci RDFLabel
p RDFLabel
v | [Maybe RDFLabel]
mvs <- [[Maybe RDFLabel]]
dts, (RDFLabel
p,Just RDFLabel
v) <- forall a b. [a] -> [b] -> [(a, b)]
zip [RDFLabel]
props [Maybe RDFLabel]
mvs ]

        --  Make graphs for one alternative
        --  TODO: convert to sets
        makeGraphs :: [Arc RDFLabel] -> [RDFGraph]
makeGraphs = forall a b. (a -> b) -> [a] -> [b]
map (Set (Arc RDFLabel) -> RDFGraph
toRDFGraph forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[])) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall lb. lb -> lb -> lb -> Arc lb
Arc RDFLabel
ci RDFLabel
resRdfType RDFLabel
cls forall a. a -> [a] -> [a]
:)

--  Helper function to select sub-tuples from which some of a set of
--  values can be derived using a class restriction.
--
--  restriction is the restriction being evaluated.
--  ft          is a full tuple of values known to be consistent with
--              the restriction
--
--  The result returned is a list of pairs, whose first member is a partial
--  tuples from which the full tuple supplied can be derived, and the second
--  is the supplied tuple calculated from that input.
--
deriveTuple ::
    ClassRestriction -> [RDFLabel]
    -> [([Maybe RDFLabel], [RDFLabel])]
deriveTuple :: ClassRestriction -> [RDFLabel] -> [([Maybe RDFLabel], [RDFLabel])]
deriveTuple ClassRestriction
restriction [RDFLabel]
ft =
    forall a b. (a -> b) -> [a] -> [b]
map (forall {b} {a}. b -> a -> (a, b)
tosnd [RDFLabel]
ft) forall a b. (a -> b) -> a -> b
$ forall a. PartCompare a -> [a] -> [a]
minima forall a. Eq a => [Maybe a] -> [Maybe a] -> Maybe Ordering
partCompareListMaybe forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter [Maybe RDFLabel] -> Bool
derives [[Maybe RDFLabel]]
partials
    where
        partials :: [[Maybe RDFLabel]]
partials = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\RDFLabel
x -> [forall a. Maybe a
Nothing, forall a. a -> Maybe a
Just RDFLabel
x]) [RDFLabel]
ft
        derives :: [Maybe RDFLabel] -> Bool
derives  = ([[RDFLabel]
ft] forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClassRestriction -> ClassRestrictionFn
crFunc ClassRestriction
restriction
        tosnd :: b -> a -> (a, b)
tosnd    = forall a b c. (a -> b -> c) -> b -> a -> c
flip (,)

--  Helper function to apply a restriction to selected information from
--  a supplied graph, and returns a tuple containing:
--  (a) an indication of whether the graph is consistent with the
--      restriction
--  (b) a list of values specified in the graph for each property
--  (c) a complete list of tuples that use combinations of values from
--      the graph and are consistent with the restriction.
--      Each member is a pair consisting of some combination of input
--      values, and a list of complete tuple values that can be
--      calculated from those inputs, or an empty list if there is
--      insufficient information.
--  (d) a set of tuples that are consistent with the restriction and use
--      as much information from the graph as possible.  This set is
--      minimal in the sense that they must all correspond to different
--      complete input tuples satisfying the restriction.
--
--  This function factors out logic that is common to forward and
--  backward chaining of a class restriction.
--
--  restriction is the class restriction being applied
--  ci          is the identifier of a graph node to be tested
--  props       is a list of properties of the graph noode whose values
--              are constrained by the class restriction.
--  cs          is a list of max cardinality constraints on the restriction,
--              the minimum of which is used as the cardinality constraint
--              on the restriction.  If the list is null, no cardinality
--              constraint is applied.
--  gr          is the graph from which property values are extracted.
--
applyRestriction ::
    ClassRestriction -> RDFLabel -> [RDFLabel] -> [Int] -> RDFGraph
    -> ( Bool
       , [[RDFLabel]]
       , [([Maybe RDFLabel],[[RDFLabel]])]
       , [[Maybe RDFLabel]]
       )
applyRestriction :: ClassRestriction
-> RDFLabel
-> [RDFLabel]
-> [Int]
-> RDFGraph
-> (Bool, [[RDFLabel]], [([Maybe RDFLabel], [[RDFLabel]])],
    [[Maybe RDFLabel]])
applyRestriction ClassRestriction
restriction RDFLabel
ci [RDFLabel]
props [Int]
cs RDFGraph
gr =
    (forall a b. (a -> [b] -> [b]) -> [[a]] -> [[b]] -> Bool
coversVals forall a. Eq a => Maybe a -> [a] -> [a]
deleteMaybe [[Maybe RDFLabel]]
sts [[RDFLabel]]
pvs Bool -> Bool -> Bool
&& Bool
cardinalityOK, [[RDFLabel]]
pvs, [([Maybe RDFLabel], [[RDFLabel]])]
cts, [[Maybe RDFLabel]]
sts )
    where
        --  Extract from the antecedent graph all specified values of the
        --  restricted properties (constructs inner list for each property)
        pvs :: [[RDFLabel]]
        pvs :: [[RDFLabel]]
pvs = [ RDFLabel -> RDFLabel -> RDFGraph -> [RDFLabel]
rdfFindPredVal RDFLabel
ci RDFLabel
p RDFGraph
gr | RDFLabel
p <- [RDFLabel]
props ]
        --  Convert tuple of alternatives to list of alternative tuples
        --  (Each tuple is an inner list)
        pts :: [[Maybe RDFLabel]]
        pts :: [[Maybe RDFLabel]]
pts = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a. [a] -> [Maybe a]
allJustAndNothing [[RDFLabel]]
pvs
        --  Try class restriction calculation for each tuple
        --  For each, result may be:
        --    Nothing  (inconsistent)
        --    Just []  (underspecified)
        --    Just [t] (single tuple of values derived from given values)
        --    Just ts  (alternative tuples derived from given values)
        rts :: [Maybe [[RDFLabel]]]
        rts :: [Maybe [[RDFLabel]]]
rts = forall a b. (a -> b) -> [a] -> [b]
map (ClassRestriction -> ClassRestrictionFn
crFunc ClassRestriction
restriction) [[Maybe RDFLabel]]
pts
        
        --  Extract list of consistent tuples of given values
        cts :: [([Maybe RDFLabel],[[RDFLabel]])]
        cts :: [([Maybe RDFLabel], [[RDFLabel]])]
cts = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a b. (a, Maybe b) -> Maybe (a, b)
tupleConv (forall a b. [a] -> [b] -> [(a, b)]
zip [[Maybe RDFLabel]]
pts [Maybe [[RDFLabel]]]
rts)
        
        --  TODO: be more idiomatic?
        tupleConv :: (a, Maybe b) -> Maybe (a,b)
        tupleConv :: forall a b. (a, Maybe b) -> Maybe (a, b)
tupleConv (a
a, Just b
b)  = forall a. a -> Maybe a
Just (a
a,b
b)
        tupleConv (a, Maybe b)
_            = forall a. Maybe a
Nothing
        
        --  Build list of consistent tuples with maximum information
        --  based on that supplied and available
        -- mts = concatMap mostValues cts
        mts :: [[Maybe RDFLabel]]
mts = forall a b. (a -> b) -> [a] -> [b]
map forall a. ([Maybe a], [[a]]) -> [Maybe a]
mostOneValue [([Maybe RDFLabel], [[RDFLabel]])]
cts
        --  Eliminate consistent results subsumed by others.
        --  This results in a mimimal possible set of consistent inputs,
        --  because if any pair could be consistently unified then their
        --  common subsumer would still be in the list, and both would be
        --  thereby eliminated.
        sts :: [[Maybe RDFLabel]]
        sts :: [[Maybe RDFLabel]]
sts = forall a. PartCompare a -> [a] -> [a]
maxima forall a. Eq a => [Maybe a] -> [Maybe a] -> Maybe Ordering
partCompareListMaybe [[Maybe RDFLabel]]
mts
        --  Check the cardinality constraint
        cardinalityOK :: Bool
cardinalityOK = forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
cs Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Maybe RDFLabel]]
sts forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [Int]
cs
        
--  Map a non-empty list of values to a list of Just values,
--  preceding each with a Nothing element.
--
--  Nothing corresponds to an unknown value.  This logic is used
--  as part of constructing a list of alternative tuples of known
--  data values (either supplied or calculated from the class
--  restriction).
--
allJustAndNothing :: [a] -> [Maybe a]
allJustAndNothing :: forall a. [a] -> [Maybe a]
allJustAndNothing [a]
as = forall a. Maybe a
Nothingforall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Maybe a
Just [a]
as

{-
--  Get maximum information about possible tuple values from a
--  given pair of input tuple, which is known to be consistent with
--  the restriction, and calculated result tuples.  Where the result
--  tuple is not exactly calculated, return the input tuple.
--
--  imvs    tuple of Maybe element values, with Nothing for
--          unspecified values
--  movss   Maybe list of possible fully-specified result tuples,
--          an empty list if no result tuples can be computed
--          based on the input tuple, or Nothing if the input
--          tuple is inconsistent.
--
mostValues :: ([Maybe a],[[a]]) -> [[Maybe a]]
mostValues (imvs,([])) = [imvs]
mostValues (_,movss) = map (map Just) movss
-}

--  Get maximum information about possible tuple values from a
--  given pair of input and possible result tuples, which is
--  known to be consistent with the restriction.  If the result
--  tuple is not exactly calculated, return the input tuple.
--
--  This is a variant of mostValues that returns a single vector.
--  Multiple possible values are considered to be equivalent to
--  Just [], i.e. unknown result.
--
--  imvs    tuple of Maybe element values, with Nothing for
--          unspecified values
--  movss   Maybe list of possible fully-specified result tuples,
--          or an empty list if no result tuples can be computed
--          based on the input tuple.
--
mostOneValue :: ([Maybe a],[[a]]) -> [Maybe a]
mostOneValue :: forall a. ([Maybe a], [[a]]) -> [Maybe a]
mostOneValue ([Maybe a]
_,[[a]
movs]) = forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Maybe a
Just [a]
movs
mostOneValue ([Maybe a]
imvs,[[a]]
_)   = [Maybe a]
imvs

--  Helper function that returns subsets of dts that "cover" the indicated
--  values;  i.e. from which all of the supplied values can be deduced
--  by the enumerated function results.  The minima of all such subsets is
--  returned, as each of these corresponds to some minimum information needed
--  to deduce all of the given values.
--
--  pvs     is a list of lists of values to be covered.  The inner list
--          contains multiple values for each member of a tuple.
--  dts     is an enumerated list of function values from some subset of
--          the tuple space to complete tuples.  Each member is a pair
--          containing the partial tuple (using Nothing for unspecified
--          values) and the full tuple calculated from it.
--
--  The return value is a disjunction of conjunctions of partial tuples
--  that cover the indicated parameter values.
--
--  NOTE:
--  The result minimization is not perfect (cf. test2 below), but I believe
--  it is adequate for the practical situations I envisage, and in any
--  case will not result in incorrect values.  It's significance is for
--  search-tree pruning.  A perfect minimization might be achieved by
--  using a more subtle partial ordering that takes account of both subsets
--  and the partial ordering of set members in place of 'partCompareListSubset'.
--
coverSets  :: (Eq a) => [[a]] -> [([Maybe a],[a])] -> [[[Maybe a]]]
coverSets :: forall a. Eq a => [[a]] -> [([Maybe a], [a])] -> [[[Maybe a]]]
coverSets [[a]]
pvs [([Maybe a], [a])]
dts =
    forall a. PartCompare a -> [a] -> [a]
minima forall a. Eq a => [a] -> [a] -> Maybe Ordering
partCompareListSubset forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst) [[([Maybe a], [a])]]
ctss
    where
        ctss :: [[([Maybe a], [a])]]
ctss = forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. [(a, [a])] -> Bool
coverspvs forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
tail forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]]
subsequences [([Maybe a], [a])]
cts
        cts :: [([Maybe a], [a])]
cts  = forall a. PartCompare a -> [a] -> [a]
minima (forall a b.
PartCompare a
-> PartCompare b -> (a, b) -> (a, b) -> Maybe Ordering
partComparePair forall a. Eq a => [Maybe a] -> [Maybe a] -> Maybe Ordering
partCompareListMaybe forall a. Eq a => PartCompare a
partCompareEq) [([Maybe a], [a])]
dts
        coverspvs :: [(a, [a])] -> Bool
coverspvs [(a, [a])]
cs = forall a b. (a -> [b] -> [b]) -> [[a]] -> [[b]] -> Bool
coversVals forall a. Eq a => a -> [a] -> [a]
delete (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(a, [a])]
cs) [[a]]
pvs

--  Does a supplied list of tuples cover a list of possible alternative
--  values for each tuple member?
--
coversVals :: (a->[b]->[b]) -> [[a]] -> [[b]] -> Bool
coversVals :: forall a b. (a -> [b] -> [b]) -> [[a]] -> [[b]] -> Bool
coversVals a -> [b] -> [b]
dropVal [[a]]
ts [[b]]
vss =
    -- all null (foldr dropUsed vss ts)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (forall a b. (a -> b -> b) -> b -> [a] -> [b]
scanr [a] -> [[b]] -> [[b]]
dropUsed [[b]]
vss [[a]]
ts)
    where
        --  Remove single tuple values from the list of supplied values:
        dropUsed :: [a] -> [[b]] -> [[b]]
dropUsed []       []     = []
        dropUsed (a
a:[a]
as) ([b]
bs:[[b]]
bss) = a -> [b] -> [b]
dropVal a
a [b]
bs forall a. a -> [a] -> [a]
: [a] -> [[b]] -> [[b]]
dropUsed [a]
as [[b]]
bss
        dropUsed [a]
_ [[b]]
_ = forall a. HasCallStack => String -> a
error String
"coversVals.dropUsed: list length mismatch"

{-
--  Does a supplied list of possible alternative values for each
--  element of a tuple cover every tuple in a supplied list?
--
--  (See module spike-coverVals.hs for test cases)
--
coversAll :: ([a]->b->Bool) -> [[a]] -> [[b]] -> Bool
coversAll matchElem vss ts = all (invss vss) ts
    where
        --  Test if a given tuple is covered by vss
        invss vss t = and $ zipWith matchElem vss t

--  Test if the value in a Maybe is contained in a list.
maybeElem :: (Eq a) => Maybe a -> [a] -> Bool
maybeElem Nothing  = const True
maybeElem (Just t) = elem t
-}

-- |Delete a Maybe value from a list
deleteMaybe :: (Eq a) => Maybe a -> [a] -> [a]
deleteMaybe :: forall a. Eq a => Maybe a -> [a] -> [a]
deleteMaybe Maybe a
Nothing  [a]
as = [a]
as
deleteMaybe (Just a
a) [a]
as = forall a. Eq a => a -> [a] -> [a]
delete a
a [a]
as

-- | Make restriction rules from the supplied datatype and graph.

makeRDFDatatypeRestrictionRules :: RDFDatatypeVal vt -> RDFGraph -> [RDFRule]
makeRDFDatatypeRestrictionRules :: forall vt. RDFDatatypeVal vt -> RDFGraph -> [RDFRule]
makeRDFDatatypeRestrictionRules RDFDatatypeVal vt
dtval =
    [ClassRestriction] -> RDFGraph -> [RDFRule]
makeRDFClassRestrictionRules [ClassRestriction]
dcrs 
    where
        dcrs :: [ClassRestriction]
dcrs = forall a b. (a -> b) -> [a] -> [b]
map (forall vt. RDFDatatypeVal vt -> DatatypeRel vt -> ClassRestriction
makeDatatypeRestriction RDFDatatypeVal vt
dtval) (forall ex vt lb vn. DatatypeVal ex vt lb vn -> [DatatypeRel vt]
tvalRel RDFDatatypeVal vt
dtval)

--------------------------------------------------------------------------------
--
--  Copyright (c) 2003, Graham Klyne, 2009 Vasili I Galchin,
--    2011, 2012, 2014, 2018, 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
--
--------------------------------------------------------------------------------