    {-# 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 rul :: RDFRule
    rul ants :: [RDFFormula]
    ants con :: 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 rsets :: [RDFRuleset]
    rsets base :: RDFFormula
    base goal :: RDFFormula
    goal steps :: [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 name :: ScopedName
    name vocab :: [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 vocab :: [RDFLabel]
    vocab ante :: [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 ls :: [(k, k)]
    ls = (k -> k) -> NSGraph k -> NSGraph k
    forall lb. Ord lb => (lb -> lb) -> NSGraph lb -> NSGraph lb
    fmapNSGraph
                       (\l :: 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 vocab :: [RDFLabel]
    vocab cons :: 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 ante :: [RDFGraph]
    ante cons :: 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 rs :: [a]
    rs ps :: [[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 rs :: [a]
    rs rss :: [[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 len :: Int
    len rs :: [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 name :: 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 ante :: [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 ante :: [RDFGraph]
    ante cons :: 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 name :: 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 ante :: [RDFGraph]
    ante cons :: 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
    --
    --------------------------------------------------------------------------------