{-# LANGUAGE OverloadedStrings #-}

--------------------------------------------------------------------------------
--  See end of this file for licence information.
--------------------------------------------------------------------------------
-- |
--  Module      :  RDFRuleset
--  Copyright   :  (c) 2003, Graham Klyne, 2009 Vasili I Galchin, 2011 Douglas Burke
--  License     :  GPL V2
--
--  Maintainer  :  Douglas Burke
--  Stability   :  experimental
--  Portability :  OverloadedStrings
--
--  This module defines some datatypes and functions that are
--  used to define rules and rulesets over RDF graphs.
--
--  For the routines that accept a graph in N3 format, the following
--  namespaces are pre-defined for use by the graph:
--     @rdf:@ and @rdfs:@.
--
--------------------------------------------------------------------------------

module Swish.RDF.RDFRuleset
    ( RDFFormula, RDFRule, RDFRuleMap
    , RDFClosure, RDFRuleset, RDFRulesetMap
    , nullRDFFormula
    , GraphClosure(..), makeGraphClosureRule
    , makeRDFGraphFromN3Builder
    , makeRDFFormula
    , makeRDFClosureRule
      -- * Create rules using Notation3 statements
    , makeN3ClosureRule
    , makeN3ClosureSimpleRule
    , makeN3ClosureModifyRule
    , makeN3ClosureAllocatorRule
    , makeNodeAllocTo
      -- * Debugging
    , graphClosureFwdApply, graphClosureBwdApply
    )
where

import Swish.RDF.RDFQuery
    ( rdfQueryFind
    , rdfQueryBack, rdfQueryBackModify
    , rdfQuerySubs
    , rdfQuerySubsBlank
    )

import Swish.RDF.RDFGraph
    ( RDFLabel(..), RDFGraph
    , makeBlank, newNodes
    , merge, allLabels
    , toRDFGraph, emptyRDFGraph )

import Swish.RDF.RDFVarBinding (RDFVarBinding, RDFVarBindingModify)
import Swish.RDF.N3Parser (parseN3)
import Swish.RDF.Ruleset (Ruleset(..), RulesetMap)

import Swish.RDF.Rule
    ( Formula(..), Rule(..), RuleMap
    , fwdCheckInference
    , nullSN
    )

import Swish.RDF.VarBinding
    ( makeVarBinding
    , applyVarBinding, joinVarBindings
    , VarBindingModify(..)
    , vbmCompose
    , varBindingId
    )

import Swish.Utils.Namespace (Namespace, ScopedName, makeNSScopedName, namespaceToBuilder)
import Swish.RDF.Vocabulary (swishName, namespaceRDF, namespaceRDFS)

{-
import Swish.RDF.Proof
    ( Proof(..), Step(..) )
-}

import Swish.RDF.GraphClass (Label(..), Arc(..), LDGraph(..))
import Swish.Utils.ListHelpers (equiv, flist)

import Data.List (nub)
import Data.Maybe (fromMaybe)
import Data.Monoid (Monoid(..))

import qualified Data.Text as T
import qualified Data.Text.Lazy.Builder as B

------------------------------------------------------------
--  Datatypes for RDF ruleset
------------------------------------------------------------

type RDFFormula     = Formula RDFGraph

type RDFRule        = Rule RDFGraph

type RDFRuleMap     = RuleMap RDFGraph

type RDFClosure     = GraphClosure RDFLabel

type RDFRuleset     = Ruleset RDFGraph

type RDFRulesetMap  = RulesetMap RDFGraph

------------------------------------------------------------
--  Declare null RDF formula
------------------------------------------------------------

-- | The null RDF formula.
nullRDFFormula :: Formula RDFGraph
nullRDFFormula = Formula
    { formName = nullSN "nullRDFGraph"
    , formExpr = emptyRDFGraph
    }

------------------------------------------------------------
--  Datatype for graph closure rule
------------------------------------------------------------

-- |Datatype for constructing a graph closure rule
data GraphClosure lb = GraphClosure
    { nameGraphRule :: ScopedName   -- ^ Name of rule for proof display
    , ruleAnt       :: [Arc lb]     -- ^ Antecedent triples pattern
                                    --   (may include variable nodes)
    , ruleCon       :: [Arc lb]     -- ^ Consequent triples pattern
                                    --   (may include variable nodes)
    , ruleModify    :: VarBindingModify lb lb
                                    -- ^ Structure that defines additional
                                    --   constraints and/or variable
                                    --   bindings based on other matched
                                    --   query variables.  Matching the
                                    --   antecedents.  Use 'varBindingId' if
                                    --   no additional variable constraints
                                    --   or bindings are added beyond those
                                    --   arising from graph queries.
    }

instance (Label lb) => Eq (GraphClosure lb) where
    c1 == c2 = nameGraphRule c1 == nameGraphRule c2 &&
               ruleAnt c1 `equiv` ruleAnt c2 &&
               ruleCon c1 `equiv` ruleCon c2

instance (Label lb) => Show (GraphClosure lb) where
    show c = "GraphClosure " ++ show (nameGraphRule c)

------------------------------------------------------------
--  Define inference rule based on RDF graph closure rule
------------------------------------------------------------

-- |Define a value of type Rule based on an RDFClosure value.
makeGraphClosureRule :: GraphClosure RDFLabel -> Rule RDFGraph
makeGraphClosureRule grc = newrule
    where
        newrule = Rule
            { ruleName       = nameGraphRule grc
            , fwdApply       = graphClosureFwdApply grc
            , bwdApply       = graphClosureBwdApply grc
            , checkInference = fwdCheckInference newrule
            }

-- | Forward chaining function based on RDF graph closure description
--
--  Note:  antecedents here are presumed to share bnodes.
--
graphClosureFwdApply :: 
  GraphClosure RDFLabel 
  -> [RDFGraph] 
  -> [RDFGraph]
graphClosureFwdApply grc grs =
    let gr   = if null grs then emptyRDFGraph else foldl1 add grs
        vars = queryFind (ruleAnt grc) gr
        varm = vbmApply (ruleModify grc) vars
        cons = querySubs varm (ruleCon grc)
    in
        {-
        seq cons $
        seq (trace "\ngraphClosureFwdApply") $
        seq (traceShow "\nvars: " vars) $
        seq (traceShow "\nvarm: " varm) $
        seq (traceShow "\ncons: " cons) $
        seq (trace "\n") $
        -}
        --  Return null list or single result graph that is the union
        --  (not merge) of individual results:
        if null cons then [] else [foldl1 add cons]
        -- cons {- don't merge results -}

-- | Backward chaining function based on RDF graph closure description
graphClosureBwdApply :: GraphClosure RDFLabel -> RDFGraph -> [[RDFGraph]]
graphClosureBwdApply grc gr =
    let vars = rdfQueryBackModify (ruleModify grc) $
               queryBack (ruleCon grc) gr
        --  This next function eliminates duplicate variable bindings.
        --  It is strictly redundant, but comparing variable
        --  bindings is much cheaper than comparing graphs.
        --  I don't know if many duplicate graphs will be result
        --  of exact duplicate variable bindings, so this may be
        --  not very effective.
        varn = map nub vars
    in
        --  The 'nub ante' below eliminates duplicate antecedent graphs,
        --  based on graph matching, which tests for equivalence under
        --  bnode renaming, with a view to reducing redundant arcs in
        --  the merged antecedent graph, hence less to prove in
        --  subsequent back-chaining steps.
        --
        --  Each antecedent is reduced to a single RDF graph, when
        --  bwdApply specifies a list of expressions corresponding to
        --  each antecedent.
        [ [foldl1 merge (nub ante)]
          | vs <- varn
          , let ante = querySubsBlank vs (ruleAnt grc) ]

------------------------------------------------------------
--  RDF graph query and substitution support functions
------------------------------------------------------------

queryFind :: [Arc RDFLabel] -> RDFGraph -> [RDFVarBinding]
queryFind qas = rdfQueryFind (toRDFGraph qas)

queryBack :: [Arc RDFLabel] -> RDFGraph -> [[RDFVarBinding]]
queryBack qas = rdfQueryBack (toRDFGraph qas)

querySubs :: [RDFVarBinding] -> [Arc RDFLabel] -> [RDFGraph]
querySubs vars = rdfQuerySubs vars . toRDFGraph

querySubsBlank :: [RDFVarBinding] -> [Arc RDFLabel] -> [RDFGraph]
querySubsBlank vars = rdfQuerySubsBlank vars . toRDFGraph

------------------------------------------------------------
--  Method for creating an RDF formula value from N3 text
------------------------------------------------------------

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

prefixRDF :: B.Builder
prefixRDF = 
  mconcat 
  [ mkPrefix namespaceRDF
  , mkPrefix namespaceRDFS
    ]

-- |Helper function to parse a string containing Notation3
--  and return the corresponding RDFGraph value.
--
makeRDFGraphFromN3Builder :: B.Builder -> RDFGraph
makeRDFGraphFromN3Builder b = 
  let t = B.toLazyText (prefixRDF `mappend` b)
  in case parseN3 t Nothing of
    Left  msg -> error msg
    Right gr  -> gr

-- |Create an RDF formula.
makeRDFFormula ::
    Namespace     -- ^ namespace to which the formula is allocated
    -> T.Text     -- ^ local name for the formula in the namespace
    -> B.Builder  -- ^ graph in Notation 3 format
    -> RDFFormula
makeRDFFormula scope local gr = 
  Formula
    { formName = makeNSScopedName scope local
    , formExpr = makeRDFGraphFromN3Builder gr
    }

------------------------------------------------------------
--  Create an RDF closure rule from supplied graphs
------------------------------------------------------------

-- |Constructs an RDF graph closure rule.  That is, a rule that
--  given some set of antecedent statements returns new statements
--  that may be added to the graph.
--
makeRDFClosureRule ::
    ScopedName -- ^ scoped name for the new rule
    -> [RDFGraph] -- ^ RDFGraphs that are the entecedent of the rule.
                  --
                  -- (Note:  bnodes and variable names are assumed to be shared
                  -- by all the entecedent graphs supplied.  /is this right?/)
    -> RDFGraph   -- ^ the consequent graph
    -> RDFVarBindingModify -- ^ is a variable binding modifier value that may impose
    --          additional conditions on the variable bindings that
    --          can be used for this inference rule, or which may
    --          cause new values to be allocated for unbound variables.
    --          These modifiers allow for certain inference patterns
    --          that are not captured by simple "closure rules", such
    --          as the allocation of bnodes corresponding to literals,
    --          and are an extension point for incorporating datatypes
    --          into an inference process.
    --
    --          If no additional constraints or variable bindings are
    --          to be applied, use value 'varBindingId'
    --
    -> RDFRule
makeRDFClosureRule sname antgrs congr vmod = makeGraphClosureRule
    GraphClosure
        { nameGraphRule = sname
        , ruleAnt       = concatMap getArcs antgrs
        , ruleCon       = getArcs congr
        , ruleModify    = vmod
        }

------------------------------------------------------------
--  Methods to create an RDF closure rule from N3 input
------------------------------------------------------------
--
--  These functions are used internally by Swish to construct
--  rules from textual descriptions.

-- |Constructs an RDF graph closure rule.  That is, a rule that
--  given some set of antecedent statements returns new statements
--  that may be added to the graph.  This is the basis for
--  implementation of most of the inference rules given in the
--  RDF formal semantics document.
--
makeN3ClosureRule ::
    Namespace -- ^ namespace to which the rule is allocated
    -> T.Text -- ^ local name for the rule in the namespace
    -> B.Builder 
    -- ^ the Notation3 representation
    --   of the antecedent graph.  (Note: multiple antecedents
    --   can be handled by combining multiple graphs.)
    -> B.Builder -- ^ the Notation3 representation of the consequent graph.
    -> RDFVarBindingModify
    -- ^ a variable binding modifier value that may impose
    --   additional conditions on the variable bindings that
    --   can be used for this inference rule, or which may
    --   cause new values to be allocated for unbound variables.
    --   These modifiers allow for certain inference patterns
    --   that are not captured by simple closure rules, such
    --   as the allocation of bnodes corresponding to literals,
    --   and are an extension point for incorporating datatypes
    --   into an inference process.
    --
    --   If no additional constraints or variable bindings are
    --   to be applied, use a value of 'varBindingId', or use
    --   'makeN3ClosureSimpleRule'.
    -> RDFRule
makeN3ClosureRule scope local ant con =
    makeRDFClosureRule (makeNSScopedName scope local) [antgr] congr
    where
        antgr = makeRDFGraphFromN3Builder ant
        congr = makeRDFGraphFromN3Builder con

-- |Construct a simple RDF graph closure rule without
--  additional node allocations or variable binding constraints.
--
makeN3ClosureSimpleRule ::
    Namespace -- ^ namespace to which the rule is allocated
    -> T.Text -- ^ local name for the rule in the namepace
    -> B.Builder
    -- ^ the Notation3 representation
    --   of the antecedent graph.  (Note: multiple antecedents
    --   can be handled by combining multiple graphs.)
    -> B.Builder  -- ^ the Notation3 representation of the consequent graph.
    -> RDFRule
makeN3ClosureSimpleRule scope local ant con =
    makeN3ClosureRule scope local ant con varBindingId

-- |Constructs an RDF graph closure rule that incorporates
--  a variable binding filter and a variable binding modifier.
--
makeN3ClosureModifyRule ::
    Namespace -- ^ namespace to which the rule is allocated
    -> T.Text -- ^ local name for the rule in the given namespace
    -> B.Builder -- ^ the Notation3 representation
    --                of the antecedent graph.  (Note: multiple antecedents
    --                can be handled by combining multiple graphs.)
    -> B.Builder -- ^ the Notation3 representation of the consequent graph.
    -> RDFVarBindingModify
    -- ^ a variable binding modifier value that may impose
    --   additional conditions on the variable bindings that
    --   can be used for this inference rule (@vflt@).
    --
    --   These modifiers allow for certain inference patterns
    --   that are not captured by simple closure rules, such
    --   as deductions that pertain only to certain kinds of
    --   nodes in a graph.
    -> RDFVarBindingModify
    -- ^ a variable binding modifier that is applied to the
    --   variable bindings obtained, typically to create some
    --   additional variable bindings.  This is applied before
    --   the preceeding filter rule (@vflt@).
    -> RDFRule
makeN3ClosureModifyRule scope local ant con vflt vmod =
    makeN3ClosureRule scope local ant con modc
    where
        modc  = fromMaybe varBindingId $ vbmCompose vmod vflt

{-
    makeRDFClosureRule (ScopedName scope local) [antgr] congr modc
    where
        antgr = makeRDFGraphFromN3String ant
        congr = makeRDFGraphFromN3String con
        modc  = case vbmCompose vmod vflt of
            Just x  -> x
            Nothing -> varBindingId
-}

-- |Construct an RDF graph closure rule with a bnode allocator.
--
--  This function is rather like 'makeN3ClosureModifyRule', except that
--  the variable binding modifier is a function from the variables in
--  the variables and bnodes contained in the antecedent graph.
--
makeN3ClosureAllocatorRule ::
    Namespace -- ^ namespace to which the rule is allocated
    -> T.Text -- ^ local name for the rule in the given namespace
    -> B.Builder -- ^ the Notation3 representation
    --                of the antecedent graph.  (Note: multiple antecedents
    --                can be handled by combining multiple graphs.)
    -> B.Builder -- ^ the Notation3 representation of the consequent graph.
    -> RDFVarBindingModify
    -- ^ variable binding modifier value that may impose
    --   additional conditions on the variable bindings that
    --   can be used for this inference rule (@vflt@).
    -> ( [RDFLabel] -> RDFVarBindingModify )
    -- ^ function applied to a list of nodes to yield a
    --   variable binding modifier value.
    --
    --   The supplied parameter is applied to a list of all of
    --   the variable nodes (including all blank nodes) in the
    --   antecedent graph, and then composed with the @vflt@
    --   value.  This allows any node allocation
    --   function to avoid allocating any blank nodes that
    --   are already used in the antecedent graph.
    --   (See 'makeNodeAllocTo').
    -> RDFRule
makeN3ClosureAllocatorRule scope local ant con vflt aloc =
    makeRDFClosureRule (makeNSScopedName scope local) [antgr] congr modc
    where
        antgr = makeRDFGraphFromN3Builder ant
        congr = makeRDFGraphFromN3Builder con
        vmod  = aloc (allLabels labelIsVar antgr)
        modc  = fromMaybe varBindingId $ vbmCompose vmod vflt

------------------------------------------------------------
--  Query binding modifier for "allocated to" logic
------------------------------------------------------------

-- |This function defines a variable binding modifier that
--  allocates a new blank node for each value bound to
--  a query variable, and binds it to another variable
--  in each query binding.
--
--  This provides a single binding for query variables that would
--  otherwise be unbound by a query.  For example, consider the
--  inference pattern:
--        
--  >  ?a hasUncle ?c => ?a hasFather ?b . ?b hasBrother ?c .
--        
--  For a given @?a@ and @?c@, there is insufficient information
--  here to instantiate a value for variable @?b@.  Using this
--  function as part of a graph instance closure rule allows
--  forward chaining to allocate a single bnode for each
--  occurrence of @?a@, so that given:
--        
--  >  Jimmy hasUncle Fred .
--  >  Jimmy hasUncle Bob .
--
--  leads to exactly one bnode inference of:
--
--  >  Jimmy hasFather _:f .
--
--  giving:
--
--  >  Jimmy hasFather _:f .
--  >  _:f   hasBrother Fred .
--  >  _:f   hasBrother Bob .
--
--  rather than:
--
--  >  Jimmy hasFather _:f1 .
--  >  _:f1  hasBrother Fred .
--  >  Jimmy hasFather _:f2 .
--  >  _:f2  hasBrother Bob .
--
--  This form of constrained allocation of bnodes is also required for
--  some of the inference patterns described by the RDF formal semantics,
--  particularly those where bnodes are substituted for URIs or literals.
--
makeNodeAllocTo ::
    RDFLabel      -- ^ variable node to which a new blank node is bound
    -> RDFLabel   -- ^ variable which is bound in each query to a graph
                  --  node to which new blank nodes are allocated.
    -> [RDFLabel]
    -> RDFVarBindingModify
makeNodeAllocTo bindvar alocvar exbnode = VarBindingModify
        { vbmName   = swishName "makeNodeAllocTo"
        , vbmApply  = applyNodeAllocTo bindvar alocvar exbnode
        , vbmVocab  = [alocvar,bindvar]
        , vbmUsage  = [[bindvar]]
        }

--  Auxiliary function that performs the node allocation defined
--  by makeNodeAllocTo.
--
--  bindvar is a variable node to which a new blank node is bound
--  alocvar is a variable which is bound in each query to a graph
--          node to which new blank nodes are allocated.
--  exbnode is a list of existing blank nodes, to be avoided by
--          the new blank node allocator.
--  vars    is a list of variable bindings to which new bnode
--          allocations for the indicated bindvar are to be added.
--
applyNodeAllocTo ::
    RDFLabel -> RDFLabel -> [RDFLabel] -> [RDFVarBinding] -> [RDFVarBinding]
applyNodeAllocTo bindvar alocvar exbnode vars =
    let
        app       = applyVarBinding
        alocnodes = zip (nub $ flist (map app vars) alocvar)
                        (newNodes (makeBlank bindvar) exbnode)
        newvb var = joinVarBindings
            ( makeVarBinding $ head
              [ [(bindvar,b)] | (v,b) <- alocnodes, app var alocvar == v ] )
            var
    in
        map newvb vars


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