;;;; Copyright (C) 2020 Julien Lepiller <julien@lepiller.eu>
;;;; 
;;;; This library is free software; you can redistribute it and/or
;;;; modify it under the terms of the GNU Lesser General Public
;;;; License as published by the Free Software Foundation; either
;;;; version 3 of the License, or (at your option) any later version.
;;;; 
;;;; This library 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
;;;; Lesser General Public License for more details.
;;;; 
;;;; You should have received a copy of the GNU Lesser General Public
;;;; License along with this library; if not, write to the Free Software
;;;; Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
;;;; 

(define-module (rdf entailment d)
  #:use-module (ice-9 match)
  #:use-module (rdf rdf)
  #:use-module ((rdf entailment simple) #:prefix simple:)
  #:use-module (srfi srfi-1)
  #:export (consistent-graph?
            entails?))

(define (consistent-graph? graph vocabulary)
  (define consistent-data?
    (match-lambda
      (($ rdf-literal form ($ rdf-datatype _ _ lexical? _ _ _) _)
       (lexical? form))
      (_ #t)))

  (match (recognize graph vocabulary)
    ('() #t)
    ((($ rdf-triple subject predicate object) graph ...)
     (and (consistent-data? subject) (consistent-data? object)
          (consistent-graph? graph vocabulary)))))

;; G entails E if E has an instance (where blank nodes are replaced by literals
;; or IRIs) that is a subgraph of G.
;;
;; We re-use similar procedures to verifying isomorphism of graphs, but this time
;; blank nodes can also map to literals and IRIs.

(define (sat? equivalences)
  "Return whether the set of equivalences satisfies the condition that it represents
an isomorphism between two blank node sets: for every equality, check that the
first component is always associated to the same second component, and that the
second component is always associated with the first."
  (match equivalences
    ('() #t)
    (((first . second) equivalences ...)
     (if (and (null? (filter
                       (lambda (eq)
                         (and (equal? (car eq) first)
                              (not (equal? (cdr eq) second))))
                       equivalences))
              (null? (filter
                       (lambda (eq)
                         (and (not (equal? (car eq) first))
                              (equal? (cdr eq) second)))
                       equivalences)))
         (sat? equivalences)
         #f))))

(define (merge-joins l1 l2)
  (cond
    ((null? l1) l2)
    ((null? l2) l1)
    (else
      (fold
        (lambda (e1 res)
          (append
            (map (lambda (e2)
                   (append e1 e2))
                 l2)
            res))
        '()
        l1))))

(define (to-disjunctions constraints)
  (match constraints
    (('equiv b1 b2) (list (list (cons b1 b2))))
    ('none (list (list)))
    ('bot 'bot)
    (('or e1 e2)
     (let ((e1 (to-disjunctions e1))
           (e2 (to-disjunctions e2)))
       (cond
         ((equal? e2 'bot)
          e1)
         ((equal? e1 'bot)
          e2)
         (else
           (append e1 e2)))))
    (('and e1 e2)
     (let ((e1 (to-disjunctions e1))
           (e2 (to-disjunctions e2)))
       (cond
         ((equal? e1 'bot)
          'bot)
         ((equal? e2 'bot)
          'bot)
         (else
           (merge-joins e1 e2)))))))

(define (generate-triple-constraints t1 t2)
  (match t1
    (($ rdf-triple s1 p1 o1)
     (match t2
       (($ rdf-triple s2 p2 o2)
        (if (and (or (equiv? s1 s2) (blank-node? s1))
                 (equal? p1 p2)
                 (or (equiv? o1 o2) (blank-node? o1)))
            (list 'and
                  (if (blank-node? s1)
                      (list 'equiv s1 s2)
                      'none)
                  (if (blank-node? o1)
                      (list 'equiv o1 o2)
                      'none))
            #f))))))

(define (generate-constraints t1 g2)
  (match g2
    ('() 'bot)
    ((t2 g2 ...)
     (let ((c (generate-triple-constraints t1 t2)))
       (if c
         (list 'or c (generate-constraints t1 g2))
         (generate-constraints t1 g2))))))

(define (equiv? n1 n2)
  (match (list n1 n2)
    ((($ rdf-literal l1 ($ rdf-datatype _ _ _ _ lexical->value1 _) lang1)
      ($ rdf-literal l2 ($ rdf-datatype _ _ _ _ lexical->value2 _) lang2))
     (and (equal? (and lang1 (string-downcase lang1))
                  (and lang2 (string-downcase lang2)))
          (equal? (lexical->value1 l1))
          (equal? (lexical->value2 l2))))
    (_ (equal? n1 n2))))

(define (validate-mapping mapping g1 g2)
  (match g1
    ('() #t)
    ((t1 g1 ...)
     (and (not (null? (filter
                        (lambda (t2)
                          (let ((s1 (rdf-triple-subject t1))
                                (s2 (rdf-triple-subject t2))
                                (p1 (rdf-triple-predicate t1))
                                (p2 (rdf-triple-predicate t2))
                                (o1 (rdf-triple-object t1))
                                (o2 (rdf-triple-object t2)))
                            (and
                              (if (blank-node? s1)
                                  (equiv? (assoc-ref mapping s1) s2)
                                  (equiv? s1 s2))
                              (equal? p1 p2)
                              (if (blank-node? o1)
                                  (equiv? (assoc-ref mapping o1) o2)
                                  (equiv? o1 o2)))))
                        g2)))
          (validate-mapping mapping g1 g2)))))

(define (entails? g e vocabulary)
  "Return true if g entails e"
  (let ((g (recognize g vocabulary)))
    (or (not (consistent-graph? g vocabulary))
        (let* ((constraints (fold (lambda (t constraints)
                                    (list 'and (generate-constraints t g)
                                          constraints))
                                  'none e))
               (disjunctions (to-disjunctions constraints)))
          (if (equal? disjunctions 'bot)
              #f
              (let loop ((disjunctions (filter sat? disjunctions)))
                (match disjunctions
                  ('() #f)
                  ((mapping disjunctions ...)
                   (if (validate-mapping mapping e g)
                     #t
                     (loop disjunctions))))))))))