{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

--------------------------------------------------------------------------------
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
--  Module      :  Proof
--  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin,
--                 2011, 2012, 2014, 2016 Douglas Burke
--  License     :  GPL V2
--
--  Maintainer  :  Douglas Burke
--  Stability   :  experimental
--  Portability :  CPP, FlexibleInstances, UndecidableInstances
--
--  This module instantiates the 'Proof' framework for
--  constructing proofs over 'RDFGraph' expressions.
--  The intent is that this can be used to test some
--  correspondences between the RDF Model theory and
--  corresponding proof theory based on closure rules
--  applied to the graph, per <http://www.w3.org/TR/rdf-mt/>.
--
--------------------------------------------------------------------------------

module Swish.RDF.Proof
    ( RDFProof, RDFProofStep
    , makeRDFProof, makeRDFProofStep
    , makeRdfInstanceEntailmentRule
    , makeRdfSubgraphEntailmentRule
    , makeRdfSimpleEntailmentRule )
where

import Swish.GraphClass (Label(..), LDGraph(..))
import Swish.Namespace (ScopedName)
import Swish.Proof (Proof(..), Step(..))
import Swish.Rule (Expression(..), Rule(..))
import Swish.VarBinding (makeVarBinding)

import Swish.RDF.Graph (RDFLabel(..), RDFGraph, fmapNSGraph)
import Swish.RDF.Graph (merge, allLabels, remapLabelList)
import Swish.RDF.Query (rdfQueryInstance, rdfQuerySubs)
import Swish.RDF.Ruleset (RDFFormula, RDFRule, RDFRuleset)

import Swish.Utils.ListHelpers (flist)

import Data.List (subsequences)

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

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

------------------------------------------------------------
--  Type instantiation of Proof framework for RDFGraph data
------------------------------------------------------------
--
--  This is a partial instantiation of the proof framework.
--  Details for applying inference rules are specific to the
--  graph instance type.

------------------------------------------------------------
--  Proof datatypes for graph values
------------------------------------------------------------

-- The following is an orphan instance

-- |Instances of 'LDGraph' are also instance of the
--  @Expression@ class, for which proofs can be constructed.
--  The empty RDF graph is always @True@ (other enduring
--  truths are asserted as axioms).

instance (LDGraph lg lb, Eq (lg lb)) => Expression (lg lb) where
    isValid :: lg lb -> Bool
isValid = Set (Arc lb) -> Bool
forall a. Set a -> Bool
S.null (Set (Arc lb) -> Bool) -> (lg lb -> Set (Arc lb)) -> lg lb -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lg lb -> Set (Arc lb)
forall (lg :: * -> *) lb. LDGraph lg lb => lg lb -> ArcSet lb
getArcs 

------------------------------------------------------------
--  Define RDF-specific types for proof framework
------------------------------------------------------------

-- | An RDF proof.
type RDFProof     = Proof RDFGraph

-- | A step in an RDF proof.
type RDFProofStep = Step RDFGraph

------------------------------------------------------------
--  Helper functions for constructing proofs on RDF graphs
------------------------------------------------------------

-- |Make an RDF graph proof step.
--
makeRDFProofStep ::
    RDFRule  -- ^ rule to use for this step
    -> [RDFFormula] -- ^ antecedent RDF formulae for this step
    -> RDFFormula -- ^ RDF formula that is the consequent for this step 
    -> RDFProofStep
makeRDFProofStep :: RDFRule -> [RDFFormula] -> RDFFormula -> RDFProofStep
makeRDFProofStep RDFRule
rul [RDFFormula]
ants RDFFormula
con = Step :: forall ex. Rule ex -> [Formula ex] -> Formula ex -> Step ex
Step
    { stepRule :: RDFRule
stepRule = RDFRule
rul
    , stepAnt :: [RDFFormula]
stepAnt  = [RDFFormula]
ants
    , stepCon :: RDFFormula
stepCon  = RDFFormula
con
    }

-- |Make an RDF proof.
--
makeRDFProof ::
    [RDFRuleset]      -- ^ RDF rulesets that constitute a proof context for this proof
    -> RDFFormula     -- ^ initial statement from which the goal is claimed to be proven
    -> RDFFormula     -- ^ statement that is claimed to be proven
    -> [RDFProofStep] -- ^ the chain of inference rules in the proof.
    -> RDFProof
makeRDFProof :: [RDFRuleset]
-> RDFFormula -> RDFFormula -> [RDFProofStep] -> RDFProof
makeRDFProof [RDFRuleset]
rsets RDFFormula
base RDFFormula
goal [RDFProofStep]
steps = Proof :: forall ex.
[Ruleset ex] -> Formula ex -> Formula ex -> [Step ex] -> Proof ex
Proof
    { proofContext :: [RDFRuleset]
proofContext = [RDFRuleset]
rsets
    , proofInput :: RDFFormula
proofInput   = RDFFormula
base
    , proofResult :: RDFFormula
proofResult  = RDFFormula
goal
    , proofChain :: [RDFProofStep]
proofChain   = [RDFProofStep]
steps
    }

------------------------------------------------------------
--  RDF instance entailment inference rule
------------------------------------------------------------

-- |Make an inference rule dealing with RDF instance entailment;
--  i.e. entailments that are due to replacement of a URI or literal
--  node with a blank node.
--
--  The part of this rule expected to be useful is 'checkInference'.
--  The 'fwdApply' and 'bwdApply' functions defined here may return
--  rather large results if applied to graphs with many variables or
--  a large vocabulary, and are defined for experimentation.
--
--  Forward and backward chaining is performed with respect to a
--  specified vocabulary.  In the case of backward chaining, it would
--  otherwise be impossible to bound the options thus generated.
--  In the case of forward chaining, it is often not desirable to
--  have the properties generalized.  If forward or backward backward
--  chaining will not be used, supply an empty vocabulary.
--  Note:  graph method 'Swish.RDF.Graph.allNodes' can be used to obtain a list of all
--  the subjects and objects used in a  graph, not counting nested
--  formulae;  use a call of the form:
--
--  >  allNodes (not . labelIsVar) graph
--
makeRdfInstanceEntailmentRule :: 
  ScopedName     -- ^ name
  -> [RDFLabel]  -- ^ vocabulary
  -> RDFRule
makeRdfInstanceEntailmentRule :: ScopedName -> [RDFLabel] -> RDFRule
makeRdfInstanceEntailmentRule ScopedName
name [RDFLabel]
vocab = RDFRule
newrule
    where
        newrule :: RDFRule
newrule = Rule :: forall ex.
ScopedName
-> ([ex] -> [ex])
-> (ex -> [[ex]])
-> ([ex] -> ex -> Bool)
-> Rule ex
Rule
            { ruleName :: ScopedName
ruleName = ScopedName
name
            , fwdApply :: [RDFGraph] -> [RDFGraph]
fwdApply = [RDFLabel] -> [RDFGraph] -> [RDFGraph]
rdfInstanceEntailFwdApply [RDFLabel]
vocab
            , bwdApply :: RDFGraph -> [[RDFGraph]]
bwdApply = [RDFLabel] -> RDFGraph -> [[RDFGraph]]
rdfInstanceEntailBwdApply [RDFLabel]
vocab
            , checkInference :: [RDFGraph] -> RDFGraph -> Bool
checkInference = [RDFGraph] -> RDFGraph -> Bool
rdfInstanceEntailCheckInference
            }

--  Instance entailment forward chaining
--
--  Note:  unless the initial graph is small, the total result
--  here could be very large.  The existential generalizations are
--  sequenced in increasing number of substitutions applied.
--
--  The instances generated are all copies of the merge of the
--  supplied graphs, with some or all of the non-variable nodes
--  replaced by blank nodes.
rdfInstanceEntailFwdApply :: [RDFLabel] -> [RDFGraph] -> [RDFGraph]
rdfInstanceEntailFwdApply :: [RDFLabel] -> [RDFGraph] -> [RDFGraph]
rdfInstanceEntailFwdApply [RDFLabel]
vocab [RDFGraph]
ante =
    let
        --  Merge antecedents to single graph, renaming bnodes if needed.
        --  (Null test and using 'foldl1' to avoid merging if possible.)
        mergeGraph :: RDFGraph
mergeGraph  = if [RDFGraph] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RDFGraph]
ante then RDFGraph
forall a. Monoid a => a
mempty
                        else (RDFGraph -> RDFGraph -> RDFGraph) -> [RDFGraph] -> RDFGraph
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 RDFGraph -> RDFGraph -> RDFGraph
forall lb. Label lb => NSGraph lb -> NSGraph lb -> NSGraph lb
merge [RDFGraph]
ante
        --  Obtain lists of variable and non-variable nodes
        --  (was: nonvarNodes = allLabels (not . labelIsVar) mergeGraph)
        nonvarNodes :: [RDFLabel]
nonvarNodes = [RDFLabel]
vocab
        varNodes :: [RDFLabel]
varNodes    = Set RDFLabel -> [RDFLabel]
forall a. Set a -> [a]
S.toList (Set RDFLabel -> [RDFLabel]) -> Set RDFLabel -> [RDFLabel]
forall a b. (a -> b) -> a -> b
$ (RDFLabel -> Bool) -> RDFGraph -> Set RDFLabel
forall lb. Label lb => (lb -> Bool) -> NSGraph lb -> Set lb
allLabels RDFLabel -> Bool
forall lb. Label lb => lb -> Bool
labelIsVar RDFGraph
mergeGraph
        --  Obtain list of possible remappings for non-variable nodes
        mapList :: [(RDFLabel, RDFLabel)]
mapList     = [RDFLabel] -> [RDFLabel] -> [(RDFLabel, RDFLabel)]
forall lb. Label lb => [lb] -> [lb] -> [(lb, lb)]
remapLabelList [RDFLabel]
nonvarNodes [RDFLabel]
varNodes
        mapSubLists :: [[(RDFLabel, RDFLabel)]]
mapSubLists = ([[(RDFLabel, RDFLabel)]] -> [[(RDFLabel, RDFLabel)]]
forall a. [a] -> [a]
tail ([[(RDFLabel, RDFLabel)]] -> [[(RDFLabel, RDFLabel)]])
-> ([(RDFLabel, RDFLabel)] -> [[(RDFLabel, RDFLabel)]])
-> [(RDFLabel, RDFLabel)]
-> [[(RDFLabel, RDFLabel)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RDFLabel, RDFLabel)] -> [[(RDFLabel, RDFLabel)]]
forall a. [a] -> [[a]]
subsequences) [(RDFLabel, RDFLabel)]
mapList
        mapGr :: [(k, k)] -> NSGraph k -> NSGraph k
mapGr [(k, k)]
ls = (k -> k) -> NSGraph k -> NSGraph k
forall lb. Ord lb => (lb -> lb) -> NSGraph lb -> NSGraph lb
fmapNSGraph 
                   (\k
l -> k -> k -> Map k k -> k
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault k
l k
l
                          ([(k, k)] -> Map k k
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(k, k)]
ls))
    in
        --  Return all remappings of the original merged graph
        [RDFGraph -> RDFGraph] -> RDFGraph -> [RDFGraph]
forall a b. [a -> b] -> a -> [b]
flist (([(RDFLabel, RDFLabel)] -> RDFGraph -> RDFGraph)
-> [[(RDFLabel, RDFLabel)]] -> [RDFGraph -> RDFGraph]
forall a b. (a -> b) -> [a] -> [b]
map [(RDFLabel, RDFLabel)] -> RDFGraph -> RDFGraph
forall k. Ord k => [(k, k)] -> NSGraph k -> NSGraph k
mapGr [[(RDFLabel, RDFLabel)]]
mapSubLists) RDFGraph
mergeGraph

--  Instance entailment backward chaining (for specified vocabulary)
--
--  [[[TODO:  this is an incomplete implementation, there being no
--  provision for instantiating some variables and leaving others
--  alone.  This can be overcome in many cases by combining instance
--  and subgraph chaining.
--  Also, there is no provision for instantiating some variables in
--  a triple and leaving others alone.  This may be fixed later if
--  this function is really needed to be completely faithful to the
--  precise notion of instance entailment.]]]
rdfInstanceEntailBwdApply :: [RDFLabel] -> RDFGraph -> [[RDFGraph]]
rdfInstanceEntailBwdApply :: [RDFLabel] -> RDFGraph -> [[RDFGraph]]
rdfInstanceEntailBwdApply [RDFLabel]
vocab RDFGraph
cons =
    let
        --  Obtain list of variable nodes
        varNodes :: [RDFLabel]
varNodes     = Set RDFLabel -> [RDFLabel]
forall a. Set a -> [a]
S.toList (Set RDFLabel -> [RDFLabel]) -> Set RDFLabel -> [RDFLabel]
forall a b. (a -> b) -> a -> b
$ (RDFLabel -> Bool) -> RDFGraph -> Set RDFLabel
forall lb. Label lb => (lb -> Bool) -> NSGraph lb -> Set lb
allLabels RDFLabel -> Bool
forall lb. Label lb => lb -> Bool
labelIsVar RDFGraph
cons
        --  Generate a substitution for each combination of variable
        --  and vocabulary node.
        varBindings :: [VarBinding RDFLabel RDFLabel]
varBindings  = ([RDFLabel] -> VarBinding RDFLabel RDFLabel)
-> [[RDFLabel]] -> [VarBinding RDFLabel RDFLabel]
forall a b. (a -> b) -> [a] -> [b]
map ([(RDFLabel, RDFLabel)] -> VarBinding RDFLabel RDFLabel
forall a b. (Ord a, Ord b) => [(a, b)] -> VarBinding a b
makeVarBinding ([(RDFLabel, RDFLabel)] -> VarBinding RDFLabel RDFLabel)
-> ([RDFLabel] -> [(RDFLabel, RDFLabel)])
-> [RDFLabel]
-> VarBinding RDFLabel RDFLabel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RDFLabel] -> [RDFLabel] -> [(RDFLabel, RDFLabel)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RDFLabel]
varNodes) [[RDFLabel]]
vocSequences
        vocSequences :: [[RDFLabel]]
vocSequences = Int -> [RDFLabel] -> [[RDFLabel]]
forall a. Int -> [a] -> [[a]]
powerSequencesLen ([RDFLabel] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RDFLabel]
varNodes) [RDFLabel]
vocab
    in
        --  Generate a substitution for each combination of variable
        --  and vocabulary:
        [ [VarBinding RDFLabel RDFLabel] -> RDFGraph -> [RDFGraph]
rdfQuerySubs [VarBinding RDFLabel RDFLabel
v] RDFGraph
cons | VarBinding RDFLabel RDFLabel
v <- [VarBinding RDFLabel RDFLabel]
varBindings ]

--  Instance entailment inference checker
rdfInstanceEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool
rdfInstanceEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool
rdfInstanceEntailCheckInference [RDFGraph]
ante RDFGraph
cons =
    let
        mante :: RDFGraph
mante = if [RDFGraph] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RDFGraph]
ante then RDFGraph
forall a. Monoid a => a
mempty        -- merged antecedents
                    else (RDFGraph -> RDFGraph -> RDFGraph) -> [RDFGraph] -> RDFGraph
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 RDFGraph -> RDFGraph -> RDFGraph
forall lb. Label lb => NSGraph lb -> NSGraph lb -> NSGraph lb
merge [RDFGraph]
ante
        qvars :: [VarBinding RDFLabel RDFLabel]
qvars = RDFGraph -> RDFGraph -> [VarBinding RDFLabel RDFLabel]
rdfQueryInstance RDFGraph
cons RDFGraph
mante     -- all query matches
        bsubs :: [RDFGraph]
bsubs = [VarBinding RDFLabel RDFLabel] -> RDFGraph -> [RDFGraph]
rdfQuerySubs [VarBinding RDFLabel RDFLabel]
qvars RDFGraph
cons         -- all back substitutions
    in
        --  Return True if any back-substitution matches the original
        --  merged antecendent graph.
        RDFGraph -> [RDFGraph] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem RDFGraph
mante [RDFGraph]
bsubs

------------------------------------------------------------
--  Powersequence (?) -- all sequences from some base values
------------------------------------------------------------

-- |Construct list of lists of sequences of increasing length
powerSeqBylen :: [a] -> [[a]] -> [[[a]]]
powerSeqBylen :: [a] -> [[a]] -> [[[a]]]
powerSeqBylen [a]
rs [[a]]
ps = [[a]]
ps [[a]] -> [[[a]]] -> [[[a]]]
forall a. a -> [a] -> [a]
: [a] -> [[a]] -> [[[a]]]
forall a. [a] -> [[a]] -> [[[a]]]
powerSeqBylen [a]
rs ([a] -> [[a]] -> [[a]]
forall a. [a] -> [[a]] -> [[a]]
powerSeqNext [a]
rs [[a]]
ps)

-- |Return sequences of length n+1 given original sequence
--  and list of all sequences of length n
powerSeqNext :: [a] -> [[a]] -> [[a]]
powerSeqNext :: [a] -> [[a]] -> [[a]]
powerSeqNext [a]
rs [[a]]
rss = [ a
ha -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
t | [a]
t <- [[a]]
rss, a
h <- [a]
rs ]

-- |Return all powersequences of a given length
powerSequencesLen :: Int -> [a] -> [[a]]
powerSequencesLen :: Int -> [a] -> [[a]]
powerSequencesLen Int
len [a]
rs = [a] -> [[a]] -> [[[a]]]
forall a. [a] -> [[a]] -> [[[a]]]
powerSeqBylen [a]
rs [[]] [[[a]]] -> Int -> [[a]]
forall a. [a] -> Int -> a
!! Int
len

--  Instance entailment notes.
--
--  Relation to simple entailment (s-entails):
--
--  (1) back-substitution yields original graph
--  ex:s1 ex:p1 ex:o1  s-entails  ex:s1 ex:p1 _:o1  by [_:o1/ex:o1]
--
--  (2) back-substitution yields original graph
--  ex:s1 ex:p1 ex:o1  s-entails  ex:s1 ex:p1 _:o2  by [_:o2/ex:o1]
--  ex:s1 ex:p1  _:o1             ex:s1 ex:p1 _:o3     [_:o3/_:o1]
--
--  (3) back-substitution does not yield original graph
--  ex:s1 ex:p1 ex:o1  s-entails  ex:s1 ex:p1 _:o2  by [_:o2/ex:o1]
--  ex:s1 ex:p1  _:o1             ex:s1 ex:p1 _:o3     [_:o3/ex:o1]
--
--  (4) consider
--  ex:s1 ex:p1 ex:o1  s-entails  ex:s1 ex:p1 ex:o1
--  ex:s1 ex:p1 ex:o2             ex:s1 ex:p1 ex:o2
--  ex:s1 ex:p1 ex:o3             ex:s1 ex:p1 _:o1
--                                ex:s1 ex:p1 _:o2
--  where [_:o1/ex:o1,_:o2/ex:o2] yields a simple entailment but not
--  an instance entailment, but [_:o1/ex:o3,_:o2/ex:o3] is also
--  (arguably) an instance entailment.  Therefore, it is not sufficient
--  to look only at the "largest" substitutions to determine instance
--  entailment.
--
--  All this means that when checking for instance entailment by
--  back substitution, all of the query results must be checked.
--  This seems clumsy.  If this function is heavily used with
--  multiple query matches, a modified query that uses each
--  triple of the target graph exactly once may be required.

------------------------------------------------------------
--  RDF subgraph entailment inference rule
------------------------------------------------------------

-- |Make an inference rule dealing with RDF subgraph entailment.
--  The part of this rule expected to be useful is 'checkInference'.
--  The 'fwdApply' function defined here may return rather large
--  results.  But in the name of completeness and experimentation
--  with the possibilities of lazy evaluation, it has been defined.
--
--  Backward chaining is not performed, as there is no reasonable way
--  to choose a meaningful supergraph of that supplied.
makeRdfSubgraphEntailmentRule :: ScopedName -> RDFRule
makeRdfSubgraphEntailmentRule :: ScopedName -> RDFRule
makeRdfSubgraphEntailmentRule ScopedName
name = RDFRule
newrule
    where
        newrule :: RDFRule
newrule = Rule :: forall ex.
ScopedName
-> ([ex] -> [ex])
-> (ex -> [[ex]])
-> ([ex] -> ex -> Bool)
-> Rule ex
Rule
            { ruleName :: ScopedName
ruleName = ScopedName
name
            , fwdApply :: [RDFGraph] -> [RDFGraph]
fwdApply = [RDFGraph] -> [RDFGraph]
rdfSubgraphEntailFwdApply
            , bwdApply :: RDFGraph -> [[RDFGraph]]
bwdApply = [[RDFGraph]] -> RDFGraph -> [[RDFGraph]]
forall a b. a -> b -> a
const []
            , checkInference :: [RDFGraph] -> RDFGraph -> Bool
checkInference = [RDFGraph] -> RDFGraph -> Bool
rdfSubgraphEntailCheckInference
            }

--  Subgraph entailment forward chaining
--
--  Note:  unless the initial graph is small, the total result
--  here could be very large.  The subgraphs are sequenced in
--  increasing size of the sub graph.
rdfSubgraphEntailFwdApply :: [RDFGraph] -> [RDFGraph]
rdfSubgraphEntailFwdApply :: [RDFGraph] -> [RDFGraph]
rdfSubgraphEntailFwdApply [RDFGraph]
ante =
    let
        --  Merge antecedents to single graph, renaming bnodes if needed.
        --  (Null test and using 'foldl1' to avoid merging if possible.)
        mergeGraph :: RDFGraph
mergeGraph  = if [RDFGraph] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RDFGraph]
ante then RDFGraph
forall a. Monoid a => a
mempty
                        else (RDFGraph -> RDFGraph -> RDFGraph) -> [RDFGraph] -> RDFGraph
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 RDFGraph -> RDFGraph -> RDFGraph
forall lb. Label lb => NSGraph lb -> NSGraph lb -> NSGraph lb
merge [RDFGraph]
ante
    in
        --  Return all subgraphs of the full graph constructed above
        -- TODO: update to use sets as appropriate
        ([Arc RDFLabel] -> RDFGraph) -> [[Arc RDFLabel]] -> [RDFGraph]
forall a b. (a -> b) -> [a] -> [b]
map (RDFGraph -> ArcSet RDFLabel -> RDFGraph
forall (lg :: * -> *) lb.
LDGraph lg lb =>
lg lb -> ArcSet lb -> lg lb
setArcs RDFGraph
mergeGraph (ArcSet RDFLabel -> RDFGraph)
-> ([Arc RDFLabel] -> ArcSet RDFLabel)
-> [Arc RDFLabel]
-> RDFGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arc RDFLabel] -> ArcSet RDFLabel
forall a. Ord a => [a] -> Set a
S.fromList) ([[Arc RDFLabel]] -> [[Arc RDFLabel]]
forall a. [a] -> [a]
init ([[Arc RDFLabel]] -> [[Arc RDFLabel]])
-> [[Arc RDFLabel]] -> [[Arc RDFLabel]]
forall a b. (a -> b) -> a -> b
$ [[Arc RDFLabel]] -> [[Arc RDFLabel]]
forall a. [a] -> [a]
tail ([[Arc RDFLabel]] -> [[Arc RDFLabel]])
-> [[Arc RDFLabel]] -> [[Arc RDFLabel]]
forall a b. (a -> b) -> a -> b
$ [Arc RDFLabel] -> [[Arc RDFLabel]]
forall a. [a] -> [[a]]
subsequences ([Arc RDFLabel] -> [[Arc RDFLabel]])
-> [Arc RDFLabel] -> [[Arc RDFLabel]]
forall a b. (a -> b) -> a -> b
$ ArcSet RDFLabel -> [Arc RDFLabel]
forall a. Set a -> [a]
S.toList (ArcSet RDFLabel -> [Arc RDFLabel])
-> ArcSet RDFLabel -> [Arc RDFLabel]
forall a b. (a -> b) -> a -> b
$ RDFGraph -> ArcSet RDFLabel
forall (lg :: * -> *) lb. LDGraph lg lb => lg lb -> ArcSet lb
getArcs RDFGraph
mergeGraph)

--  Subgraph entailment inference checker
--
--  This is of dubious utiltiy, as it doesn't allow for node renaming.
--  The simple entailment inference rule is probably more useful here.
rdfSubgraphEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool
rdfSubgraphEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool
rdfSubgraphEntailCheckInference [RDFGraph]
ante RDFGraph
cons =
    let
        --  Combine antecedents to single graph, renaming bnodes if needed.
        --  (Null test and using 'foldl1' to avoid merging if possible.)
        fullGraph :: RDFGraph
fullGraph  = if [RDFGraph] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RDFGraph]
ante then RDFGraph
forall a. Monoid a => a
mempty
                        else (RDFGraph -> RDFGraph -> RDFGraph) -> [RDFGraph] -> RDFGraph
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 RDFGraph -> RDFGraph -> RDFGraph
forall (lg :: * -> *) lb.
(LDGraph lg lb, Ord lb) =>
lg lb -> lg lb -> lg lb
addGraphs [RDFGraph]
ante
    in
        --  Check each consequent graph arc is in the antecedent graph
        RDFGraph -> ArcSet RDFLabel
forall (lg :: * -> *) lb. LDGraph lg lb => lg lb -> ArcSet lb
getArcs RDFGraph
cons ArcSet RDFLabel -> ArcSet RDFLabel -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` RDFGraph -> ArcSet RDFLabel
forall (lg :: * -> *) lb. LDGraph lg lb => lg lb -> ArcSet lb
getArcs RDFGraph
fullGraph

------------------------------------------------------------
--  RDF simple entailment inference rule
------------------------------------------------------------

-- |Make an inference rule dealing with RDF simple entailment.
--  The part of this rule expected to be useful is 'checkInference'.
--  The 'fwdApply' and 'bwdApply' functions defined return null
--  results, indicating that they are not useful for the purposes
--  of proof discovery.
makeRdfSimpleEntailmentRule :: ScopedName -> RDFRule
makeRdfSimpleEntailmentRule :: ScopedName -> RDFRule
makeRdfSimpleEntailmentRule ScopedName
name = RDFRule
newrule
    where
        newrule :: RDFRule
newrule = Rule :: forall ex.
ScopedName
-> ([ex] -> [ex])
-> (ex -> [[ex]])
-> ([ex] -> ex -> Bool)
-> Rule ex
Rule
            { ruleName :: ScopedName
ruleName = ScopedName
name
            , fwdApply :: [RDFGraph] -> [RDFGraph]
fwdApply = [RDFGraph] -> [RDFGraph] -> [RDFGraph]
forall a b. a -> b -> a
const []
            , bwdApply :: RDFGraph -> [[RDFGraph]]
bwdApply = [[RDFGraph]] -> RDFGraph -> [[RDFGraph]]
forall a b. a -> b -> a
const []
            , checkInference :: [RDFGraph] -> RDFGraph -> Bool
checkInference = [RDFGraph] -> RDFGraph -> Bool
rdfSimpleEntailCheckInference
            }

--  Simple entailment inference checker
--
--  Note:  antecedents here are presumed to share bnodes.
--         (Use 'merge' instead of 'add' for non-shared bnodes)
--
rdfSimpleEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool
rdfSimpleEntailCheckInference :: [RDFGraph] -> RDFGraph -> Bool
rdfSimpleEntailCheckInference [RDFGraph]
ante RDFGraph
cons =
    let agr :: RDFGraph
agr = if [RDFGraph] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RDFGraph]
ante then RDFGraph
forall a. Monoid a => a
mempty else (RDFGraph -> RDFGraph -> RDFGraph) -> [RDFGraph] -> RDFGraph
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 RDFGraph -> RDFGraph -> RDFGraph
forall (lg :: * -> *) lb.
(LDGraph lg lb, Ord lb) =>
lg lb -> lg lb -> lg lb
addGraphs [RDFGraph]
ante
    in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [VarBinding RDFLabel RDFLabel] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([VarBinding RDFLabel RDFLabel] -> Bool)
-> [VarBinding RDFLabel RDFLabel] -> Bool
forall a b. (a -> b) -> a -> b
$ RDFGraph -> RDFGraph -> [VarBinding RDFLabel RDFLabel]
rdfQueryInstance RDFGraph
cons RDFGraph
agr

{- original..
        not $ null $ rdfQueryInstance cons (foldl1 merge ante)
-}

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