;;;; 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 rdf)
  #:use-module (ice-9 match)
  #:use-module (rdf rdf)
  #:use-module ((rdf entailment d) #:prefix d:)
  #:use-module (srfi srfi-1)
  #:export (consistent-graph?
            entails?))

(define (rdf-iri name)
  (string-append "http://www.w3.org/1999/02/22-rdf-syntax-ns#" name))

(define (consistent-graph? graph)
  (define (non-overlapping-types? graph)
    (let loop ((graph graph) (type-mappings '()))
      (if (null? graph)
          #t
          (let* ((t (car graph)))
            (if (equal? (rdf-triple-predicate t) (rdf-iri "type"))
                (if (assoc-ref type-mappings (rdf-triple-subject t))
                    #f
                    (loop (cdr graph)
                          (cons
                            (cons (rdf-triple-subject t) (rdf-triple-object t))
                            type-mappings)))
                (loop (cdr graph) type-mappings))))))
  (and (d:consistent-graph? graph)
       (non-overlapping-types? graph)))

;; 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.

;; We follow appendix A and use a subgraph comparison (like the simple:entails?
;; procedure) after augmenting the graph with additional true triples.

(define rdf-axioms
  (list
    (make-rdf-triple (rdf-iri "type") (rdf-iri "type") (rdf-iri "Property"))
    (make-rdf-triple (rdf-iri "subject") (rdf-iri "type") (rdf-iri "Property"))
    (make-rdf-triple (rdf-iri "predicate") (rdf-iri "type") (rdf-iri "Property"))
    (make-rdf-triple (rdf-iri "object") (rdf-iri "type") (rdf-iri "Property"))
    (make-rdf-triple (rdf-iri "first") (rdf-iri "type") (rdf-iri "Property"))
    (make-rdf-triple (rdf-iri "rest") (rdf-iri "type") (rdf-iri "Property"))
    (make-rdf-triple (rdf-iri "value") (rdf-iri "type") (rdf-iri "Property"))
    (make-rdf-triple (rdf-iri "nil") (rdf-iri "type") (rdf-iri "List"))))

(define (rdf-axioms-container container)
  (list
    (make-rdf-triple 
      container (rdf-iri "type") (rdf-iri "Property"))))

(define (rdf-container-property? p)
  (define rdf-container-property-base (rdf-iri "_"))
  (and (string? p)
       (> (string-length p) (string-length rdf-container-property-base))
       (equal? (substring p 0 (string-length rdf-container-property-base))
               rdf-container-property-base)
       (string->number
         (substring p (string-length rdf-container-property-base)))))

(define (rdf-container-properties g)
  (let loop ((answer '()) (g g))
    (match g
      (() answer)
      ((($ rdf-triple subject predicate object) g ...)
       (let* ((answer (if (and (rdf-container-property? subject)
                               (not (member subject answer)))
                          (cons subject answer)
                          answer))
              (answer (if (and (rdf-container-property? predicate)
                               (not (member predicate answer)))
                          (cons predicate answer)
                          answer))
              (answer (if (and (rdf-container-property? object)
                               (not (member object answer)))
                          (cons object answer)
                          answer)))
         (loop answer g))))))

(define (augment g)
  (let* ((g (append rdf-axioms g))
         (g (append
              (append-map rdf-axioms-container (rdf-container-properties g))
              g)))
    (let loop ((g g))
      (let ((augment-set
             (let loop2 ((g2 g) (augment-set '()))
               (match g2
                 (() augment-set)
                 ((($ rdf-triple subject predicate object) g2 ...)
                  (let ((type-triple
                          (if (and (rdf-literal? object)
                                   (rdf-datatype? (rdf-literal-type object)))
                            (make-rdf-triple object (rdf-iri "type")
                                             (rdf-literal-type object))
                            #f))
                        (property-triple
                          (make-rdf-triple predicate (rdf-iri "type")
                                           (rdf-iri "Property"))))
                  (loop2
                    g2
                    (append
                      (if (or (not type-triple) (member type-triple g)
                              (member type-triple augment-set))
                          '()
                          (list type-triple))
                      (if (or (member property-triple g)
                              (member type-triple augment-set))
                          '()
                          (list property-triple))
                      augment-set))))))))
        (if (null? augment-set)
            g
            (loop (append augment-set g)))))))

(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? lang1 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)
  "Return true if g entails e"
  (or (not (consistent-graph? g))
      (d:entails? (augment g) e)))