{-# 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, 2024 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
    { 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
    { 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
            { ruleName :: ScopedName
ruleName = ScopedName
name
            , fwdApply :: [NSGraph RDFLabel] -> [NSGraph RDFLabel]
fwdApply = [RDFLabel] -> [NSGraph RDFLabel] -> [NSGraph RDFLabel]
rdfInstanceEntailFwdApply [RDFLabel]
vocab
            , bwdApply :: NSGraph RDFLabel -> [[NSGraph RDFLabel]]
bwdApply = [RDFLabel] -> NSGraph RDFLabel -> [[NSGraph RDFLabel]]
rdfInstanceEntailBwdApply [RDFLabel]
vocab
            , checkInference :: [NSGraph RDFLabel] -> NSGraph RDFLabel -> Bool
checkInference = [NSGraph RDFLabel] -> NSGraph RDFLabel -> 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] -> [NSGraph RDFLabel] -> [NSGraph RDFLabel]
rdfInstanceEntailFwdApply [RDFLabel]
vocab [NSGraph RDFLabel]
ante =
    let
        --  Merge antecedents to single graph, renaming bnodes if needed.
        --  (Null test and using 'foldl1' to avoid merging if possible.)
        mergeGraph :: NSGraph RDFLabel
mergeGraph  = if [NSGraph RDFLabel] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NSGraph RDFLabel]
ante then NSGraph RDFLabel
forall a. Monoid a => a
mempty
                      else (NSGraph RDFLabel -> NSGraph RDFLabel -> NSGraph RDFLabel)
-> [NSGraph RDFLabel] -> NSGraph RDFLabel
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NSGraph RDFLabel -> NSGraph RDFLabel -> NSGraph RDFLabel
forall lb. Label lb => NSGraph lb -> NSGraph lb -> NSGraph lb
merge [NSGraph RDFLabel]
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) -> NSGraph RDFLabel -> Set RDFLabel
forall lb. Label lb => (lb -> Bool) -> NSGraph lb -> Set lb
allLabels RDFLabel -> Bool
forall lb. Label lb => lb -> Bool
labelIsVar NSGraph RDFLabel
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 = (Int -> [[(RDFLabel, RDFLabel)]] -> [[(RDFLabel, RDFLabel)]]
forall a. Int -> [a] -> [a]
drop Int
1 ([[(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
        [NSGraph RDFLabel -> NSGraph RDFLabel]
-> NSGraph RDFLabel -> [NSGraph RDFLabel]
forall a b. [a -> b] -> a -> [b]
flist (([(RDFLabel, RDFLabel)] -> NSGraph RDFLabel -> NSGraph RDFLabel)
-> [[(RDFLabel, RDFLabel)]]
-> [NSGraph RDFLabel -> NSGraph RDFLabel]
forall a b. (a -> b) -> [a] -> [b]
map [(RDFLabel, RDFLabel)] -> NSGraph RDFLabel -> NSGraph RDFLabel
forall {k}. Ord k => [(k, k)] -> NSGraph k -> NSGraph k
mapGr [[(RDFLabel, RDFLabel)]]
mapSubLists) NSGraph RDFLabel
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] -> NSGraph RDFLabel -> [[NSGraph RDFLabel]]
rdfInstanceEntailBwdApply [RDFLabel]
vocab NSGraph RDFLabel
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) -> NSGraph RDFLabel -> Set RDFLabel
forall lb. Label lb => (lb -> Bool) -> NSGraph lb -> Set lb
allLabels RDFLabel -> Bool
forall lb. Label lb => lb -> Bool
labelIsVar NSGraph RDFLabel
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 a. [a] -> 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]
-> NSGraph RDFLabel -> [NSGraph RDFLabel]
rdfQuerySubs [VarBinding RDFLabel RDFLabel
v] NSGraph RDFLabel
cons | VarBinding RDFLabel RDFLabel
v <- [VarBinding RDFLabel RDFLabel]
varBindings ]

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

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

-- |Construct list of lists of sequences of increasing length
powerSeqBylen :: [a] -> [[a]] -> [[[a]]]
powerSeqBylen :: forall a. [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 :: forall a. [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 :: forall a. Int -> [a] -> [[a]]
powerSequencesLen Int
len [a]
rs = [a] -> [[a]] -> [[[a]]]
forall a. [a] -> [[a]] -> [[[a]]]
powerSeqBylen [a]
rs [[]] [[[a]]] -> Int -> [[a]]
forall a. HasCallStack => [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
            { ruleName :: ScopedName
ruleName = ScopedName
name
            , fwdApply :: [NSGraph RDFLabel] -> [NSGraph RDFLabel]
fwdApply = [NSGraph RDFLabel] -> [NSGraph RDFLabel]
rdfSubgraphEntailFwdApply
            , bwdApply :: NSGraph RDFLabel -> [[NSGraph RDFLabel]]
bwdApply = [[NSGraph RDFLabel]] -> NSGraph RDFLabel -> [[NSGraph RDFLabel]]
forall a b. a -> b -> a
const []
            , checkInference :: [NSGraph RDFLabel] -> NSGraph RDFLabel -> Bool
checkInference = [NSGraph RDFLabel] -> NSGraph RDFLabel -> 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 :: [NSGraph RDFLabel] -> [NSGraph RDFLabel]
rdfSubgraphEntailFwdApply [NSGraph RDFLabel]
ante =
    let
        --  Merge antecedents to single graph, renaming bnodes if needed.
        --  (Null test and using 'foldl1' to avoid merging if possible.)
        mergeGraph :: NSGraph RDFLabel
mergeGraph  = if [NSGraph RDFLabel] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NSGraph RDFLabel]
ante then NSGraph RDFLabel
forall a. Monoid a => a
mempty
                      else (NSGraph RDFLabel -> NSGraph RDFLabel -> NSGraph RDFLabel)
-> [NSGraph RDFLabel] -> NSGraph RDFLabel
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NSGraph RDFLabel -> NSGraph RDFLabel -> NSGraph RDFLabel
forall lb. Label lb => NSGraph lb -> NSGraph lb -> NSGraph lb
merge [NSGraph RDFLabel]
ante

        list :: [[Arc RDFLabel]]
list = [[Arc RDFLabel]] -> [[Arc RDFLabel]]
forall a. HasCallStack => [a] -> [a]
init ([[Arc RDFLabel]] -> [[Arc RDFLabel]])
-> [[Arc RDFLabel]] -> [[Arc RDFLabel]]
forall a b. (a -> b) -> a -> b
$ Int -> [[Arc RDFLabel]] -> [[Arc RDFLabel]]
forall a. Int -> [a] -> [a]
drop Int
1 ([[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
$ Set (Arc RDFLabel) -> [Arc RDFLabel]
forall a. Set a -> [a]
S.toList (Set (Arc RDFLabel) -> [Arc RDFLabel])
-> Set (Arc RDFLabel) -> [Arc RDFLabel]
forall a b. (a -> b) -> a -> b
$ NSGraph RDFLabel -> Set (Arc RDFLabel)
forall (lg :: * -> *) lb. LDGraph lg lb => lg lb -> ArcSet lb
getArcs NSGraph RDFLabel
mergeGraph

    in
        --  Return all subgraphs of the full graph constructed above
        -- TODO: update to use sets as appropriate
        ([Arc RDFLabel] -> NSGraph RDFLabel)
-> [[Arc RDFLabel]] -> [NSGraph RDFLabel]
forall a b. (a -> b) -> [a] -> [b]
map (NSGraph RDFLabel -> Set (Arc RDFLabel) -> NSGraph RDFLabel
forall (lg :: * -> *) lb.
LDGraph lg lb =>
lg lb -> ArcSet lb -> lg lb
setArcs NSGraph RDFLabel
mergeGraph (Set (Arc RDFLabel) -> NSGraph RDFLabel)
-> ([Arc RDFLabel] -> Set (Arc RDFLabel))
-> [Arc RDFLabel]
-> NSGraph RDFLabel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Arc RDFLabel] -> Set (Arc RDFLabel)
forall a. Ord a => [a] -> Set a
S.fromList) [[Arc RDFLabel]]
list

--  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 :: [NSGraph RDFLabel] -> NSGraph RDFLabel -> Bool
rdfSubgraphEntailCheckInference [NSGraph RDFLabel]
ante NSGraph RDFLabel
cons =
    let
        --  Combine antecedents to single graph, renaming bnodes if needed.
        --  (Null test and using 'foldl1' to avoid merging if possible.)
        fullGraph :: NSGraph RDFLabel
fullGraph  = if [NSGraph RDFLabel] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NSGraph RDFLabel]
ante then NSGraph RDFLabel
forall a. Monoid a => a
mempty
                        else (NSGraph RDFLabel -> NSGraph RDFLabel -> NSGraph RDFLabel)
-> [NSGraph RDFLabel] -> NSGraph RDFLabel
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NSGraph RDFLabel -> NSGraph RDFLabel -> NSGraph RDFLabel
forall (lg :: * -> *) lb.
(LDGraph lg lb, Ord lb) =>
lg lb -> lg lb -> lg lb
addGraphs [NSGraph RDFLabel]
ante
    in
        --  Check each consequent graph arc is in the antecedent graph
        NSGraph RDFLabel -> Set (Arc RDFLabel)
forall (lg :: * -> *) lb. LDGraph lg lb => lg lb -> ArcSet lb
getArcs NSGraph RDFLabel
cons Set (Arc RDFLabel) -> Set (Arc RDFLabel) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` NSGraph RDFLabel -> Set (Arc RDFLabel)
forall (lg :: * -> *) lb. LDGraph lg lb => lg lb -> ArcSet lb
getArcs NSGraph RDFLabel
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
            { ruleName :: ScopedName
ruleName = ScopedName
name
            , fwdApply :: [NSGraph RDFLabel] -> [NSGraph RDFLabel]
fwdApply = [NSGraph RDFLabel] -> [NSGraph RDFLabel] -> [NSGraph RDFLabel]
forall a b. a -> b -> a
const []
            , bwdApply :: NSGraph RDFLabel -> [[NSGraph RDFLabel]]
bwdApply = [[NSGraph RDFLabel]] -> NSGraph RDFLabel -> [[NSGraph RDFLabel]]
forall a b. a -> b -> a
const []
            , checkInference :: [NSGraph RDFLabel] -> NSGraph RDFLabel -> Bool
checkInference = [NSGraph RDFLabel] -> NSGraph RDFLabel -> 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 :: [NSGraph RDFLabel] -> NSGraph RDFLabel -> Bool
rdfSimpleEntailCheckInference [NSGraph RDFLabel]
ante NSGraph RDFLabel
cons =
    let agr :: NSGraph RDFLabel
agr = if [NSGraph RDFLabel] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NSGraph RDFLabel]
ante then NSGraph RDFLabel
forall a. Monoid a => a
mempty else (NSGraph RDFLabel -> NSGraph RDFLabel -> NSGraph RDFLabel)
-> [NSGraph RDFLabel] -> NSGraph RDFLabel
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 NSGraph RDFLabel -> NSGraph RDFLabel -> NSGraph RDFLabel
forall (lg :: * -> *) lb.
(LDGraph lg lb, Ord lb) =>
lg lb -> lg lb -> lg lb
addGraphs [NSGraph RDFLabel]
ante
    in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [VarBinding RDFLabel RDFLabel] -> Bool
forall a. [a] -> 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
$ NSGraph RDFLabel
-> NSGraph RDFLabel -> [VarBinding RDFLabel RDFLabel]
rdfQueryInstance NSGraph RDFLabel
cons NSGraph RDFLabel
agr

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

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