;;;; 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 rdfs)
  #:use-module (ice-9 match)
  #:use-module (rdf rdf)
  #:use-module ((rdf entailment d) #:prefix d:)
  #:use-module ((rdf entailment rdf) #:prefix rdf:)
  #:use-module ((rdf xsd) #:prefix xsd:)
  #: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 (rdfs-iri name)
  (string-append "http://www.w3.org/2000/01/rdf-schema#" name))

(define (consistent-graph? graph vocabulary)
  (define (valid-subclasses? graph)
    (match graph
      (() #t)
      ((($ rdf-triple (? rdf-datatype? s) p (? rdf-datatype? o)) graph ...)
       (if (is-iri? p (rdfs-iri "subClassOf"))
           (and ((rdf-vocabulary-order vocabulary) s o)
                (valid-subclasses? graph))
           (valid-subclasses? graph)))
      ((_ graph ...)
       (valid-subclasses? graph))))
  (and (valid-subclasses? (augment (recognize graph vocabulary)
                                   (rdf-vocabulary-datatypes vocabulary)))
       (rdf: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.

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

(define rdfs-axioms
  (list
     (make-rdf-triple (rdf-iri "type") (rdfs-iri "domain") (rdfs-iri "Resource"))
     (make-rdf-triple (rdfs-iri "domain") (rdfs-iri "domain") (rdf-iri "Property"))
     (make-rdf-triple (rdfs-iri "range") (rdfs-iri "domain") (rdf-iri "Property"))
     (make-rdf-triple (rdfs-iri "subPropertyOf") (rdfs-iri "domain")
                      (rdf-iri "Property"))
     (make-rdf-triple (rdfs-iri "subClassOf") (rdfs-iri "domain") (rdfs-iri "Class"))
     (make-rdf-triple (rdf-iri "subject") (rdfs-iri "domain") (rdf-iri "Statement"))
     (make-rdf-triple (rdf-iri "predicate") (rdfs-iri "domain") (rdf-iri "Statement"))
     (make-rdf-triple (rdf-iri "object") (rdfs-iri "domain") (rdf-iri "Statement"))
     (make-rdf-triple (rdfs-iri "member") (rdfs-iri "domain") (rdfs-iri "Resource"))
     (make-rdf-triple (rdf-iri "first") (rdfs-iri "domain") (rdf-iri "List"))
     (make-rdf-triple (rdf-iri "rest") (rdfs-iri "domain") (rdf-iri "List"))
     (make-rdf-triple (rdfs-iri "seeAlso") (rdfs-iri "domain") (rdfs-iri "Resource"))
     (make-rdf-triple (rdfs-iri "isDefinedBy") (rdfs-iri "domain")
                      (rdfs-iri "Resource"))
     (make-rdf-triple (rdfs-iri "comment") (rdfs-iri "domain") (rdfs-iri "Resource"))
     (make-rdf-triple (rdfs-iri "label") (rdfs-iri "domain") (rdfs-iri "Resource"))
     (make-rdf-triple (rdf-iri "value") (rdfs-iri "domain") (rdfs-iri "Resource"))

     (make-rdf-triple (rdf-iri "type") (rdfs-iri "range") (rdfs-iri "Class"))
     (make-rdf-triple (rdfs-iri "domain") (rdfs-iri "range") (rdfs-iri "Class"))
     (make-rdf-triple (rdfs-iri "range") (rdfs-iri "range") (rdfs-iri "Class"))
     (make-rdf-triple (rdfs-iri "subPropertyOf") (rdfs-iri "range")
                      (rdf-iri "Property"))
     (make-rdf-triple (rdfs-iri "subClassOf") (rdfs-iri "range") (rdfs-iri "Class"))
     (make-rdf-triple (rdf-iri "subject") (rdfs-iri "range") (rdfs-iri "Resource"))
     (make-rdf-triple (rdf-iri "predicate") (rdfs-iri "range") (rdfs-iri "Resource"))
     (make-rdf-triple (rdf-iri "object") (rdfs-iri "range") (rdfs-iri "Resource"))
     (make-rdf-triple (rdfs-iri "member") (rdfs-iri "range") (rdfs-iri "Resource"))
     (make-rdf-triple (rdf-iri "first") (rdfs-iri "range") (rdfs-iri "Resource"))
     (make-rdf-triple (rdf-iri "rest") (rdfs-iri "range") (rdf-iri "List"))
     (make-rdf-triple (rdfs-iri "seeAlso") (rdfs-iri "range") (rdfs-iri "Resource"))
     (make-rdf-triple (rdfs-iri "isDefinedBy") (rdfs-iri "range")
                      (rdfs-iri "Resource"))
     (make-rdf-triple (rdfs-iri "comment") (rdfs-iri "range") (rdfs-iri "Literal"))
     (make-rdf-triple (rdfs-iri "label") (rdfs-iri "range") (rdfs-iri "Literal"))
     (make-rdf-triple (rdf-iri "value") (rdfs-iri "range") (rdfs-iri "Resource"))

     (make-rdf-triple (rdf-iri "Alt") (rdfs-iri "subClassOf") (rdfs-iri "Container"))
     (make-rdf-triple (rdf-iri "Bag") (rdfs-iri "subClassOf") (rdfs-iri "Container"))
     (make-rdf-triple (rdf-iri "Seq") (rdfs-iri "subClassOf") (rdfs-iri "Container"))
     (make-rdf-triple (rdfs-iri "ContainerMembershipProperty")
                      (rdfs-iri "subClassOf") (rdf-iri "Property"))

     (make-rdf-triple (rdfs-iri "isDefinedBy") (rdfs-iri "subPropertyOf")
                      (rdfs-iri "seeAlso"))

     (make-rdf-triple (rdfs-iri "Datatype") (rdfs-iri "subClassOf")
                      (rdfs-iri "Class"))))

(define (rdfs-axioms-container container)
  (list
    (make-rdf-triple 
      container (rdf-iri "type") (rdfs-iri "ContainerMembershipProperty"))
    (make-rdf-triple
      container (rdfs-iri "domain") (rdfs-iri "Resource"))
    (make-rdf-triple
      container (rdfs-iri "range") (rdfs-iri "Resource"))))

(define (rdfs-axioms-types d)
  `(,@(if (and (member xsd:integer d) (member xsd:decimal d))
          (list (make-rdf-triple xsd:integer (rdfs-iri "subClassOf") xsd:decimal))
          '())))

(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
      (() (if (null? answer) (list (rdf-iri "_1")) 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 (is-iri? node iri)
  (or (and (string? node) (equal? node iri))
      (and (rdf-datatype? node) (member iri (rdf-datatype-iris node)))))

(define (get-entailments graph subclasses subprops ranges domains types)
  (let ((type-adds
          ;; rdfs 6 8 10 12 and 13
          (filter
            (lambda (a) a)
            (map
              (match-lambda
                (($ rdf-triple s _ o)
                 (cond
                   ((is-iri? o (rdf-iri "Property"))
                    (make-rdf-triple s (rdfs-iri "subPropertyOf") s))
                   ((is-iri? o (rdfs-iri "Class"))
                    (make-rdf-triple s (rdfs-iri "subClassOf") (rdfs-iri "Resource")))
                   ((is-iri? o (rdfs-iri "ContainerMembershipProperty"))
                    (make-rdf-triple s (rdfs-iri "subPropertyof")
                                     (rdfs-iri "member")))
                   ((is-iri? o (rdfs-iri "Datatype"))
                    (make-rdf-triple s (rdfs-iri "subClassOf")
                                     (rdfs-iri "Literal")))
                   (else #f))))
              types))))
    (append
      type-adds
      (append-map
        (match-lambda
          (($ rdf-triple s p o)
           `(;; grdf1
             ,@(if (and (rdf-literal? o)
                        (rdf-datatype? (rdf-literal-type o)))
                   (list (make-rdf-triple o (rdf-iri "type") (rdf-literal-type o)))
                   '())
             ;; rdf2
             ,(make-rdf-triple p (rdf-iri "type") (rdf-iri "Property"))
             ;; rdfs2
             ,@(append-map
                 (match-lambda
                   (($ rdf-triple subject predicate object)
                    (if (equal? subject p)
                        (list (make-rdf-triple s (rdf-iri "type") object))
                        '())))
                 domains)
             ;; rdfs3
             ,@(append-map
                 (match-lambda
                   (($ rdf-triple subject predicate object)
                    (if (equal? subject p)
                        (list (make-rdf-triple o (rdf-iri "type") object))
                        '())))
                 ranges)
             ;; rdfs4a
             ,(make-rdf-triple s (rdf-iri "type") (rdfs-iri "Resource"))
             ;; rdfs4b
             ,(make-rdf-triple o (rdf-iri "type") (rdfs-iri "Resource"))
             ;; rdfs5
             ,@(if (is-iri? p (rdfs-iri "subPropertyOf"))
                   (let ((candidates (filter
                                       (match-lambda
                                         (($ rdf-triple _ _ object)
                                          (equal? object s)))
                                       subprops)))
                     (map
                       (match-lambda
                         (($ rdf-triple subject _ _)
                          (make-rdf-triple subject (rdfs-iri "subPropertyOf")
                                           o)))
                       candidates))
                   '())
             ;; rdfs7
             ,@(map
                 (match-lambda
                   (($ rdf-triple _ _ object)
                    (make-rdf-triple s object o)))
                 (filter
                   (match-lambda
                     (($ rdf-triple subject _ _)
                      (equal? subject p)))
                   subprops))
             ;; rdfs9
             ,@(if (is-iri? p (rdf-iri "type"))
                   (let ((candidates (filter
                                       (match-lambda
                                         (($ rdf-triple subject _ _)
                                          (equal? subject o)))
                                       subprops)))
                     (map
                       (match-lambda
                         (($ rdf-triple _ _ object)
                          (make-rdf-triple s (rdf-iri "type") object)))
                       candidates))
                   '())
             ;; rdfs11
             ,@(if (is-iri? p (rdfs-iri "subClassOf"))
                   (let ((candidates (filter
                                       (match-lambda
                                         (($ rdf-triple _ _ object)
                                          (equal? object s)))
                                       subclasses)))
                     (map
                       (match-lambda
                         (($ rdf-triple subject _ _)
                          (make-rdf-triple subject (rdfs-iri "subClassOf")
                                           o)))
                       candidates))
                   '()))))
        graph))))

(define (augment g d)
  (let* ((g (append rdfs-axioms g))
         (g (append (rdfs-axioms-types d) g))
         (g (append
              ;; rdfs1
              (map
                (lambda (t)
                  (make-rdf-triple t (rdf-iri "type") (rdfs-iri "Datatype")))
                d)))
         (g (append
              (append-map rdfs-axioms-container (rdf-container-properties g))
              g)))
    (let loop ((graph '()) (subclasses '()) (subprops '()) (ranges '())
                         (domains '()) (types '()))
      (let inner-loop ((graph graph) (subclasses subclasses) (subprops subprops)
                                     (ranges ranges) (domains domains)
                                     (types types) (added? #f)
                                     (augment-set
                                       (if (null? graph)
                                           g
                                           (pk 'entailments
                                           (get-entailments
                                             graph subclasses subprops ranges
                                             domains types)))))
        (match augment-set
          (() (if added?
                  (loop graph subclasses subprops ranges domains types)
                  graph))
          ((t augment-set ...)
           (if (member t graph)
               (inner-loop graph subclasses subprops ranges domains types
                           added? augment-set)
               (let ((p (rdf-triple-predicate t)))
                 (cond
                   ((is-iri? p "subClassOf")
                    (inner-loop (cons t graph) (cons t subclasses) subprops
                                ranges domains types #t augment-set))
                   ((is-iri? p "subPropertyOf")
                    (inner-loop (cons t graph) subclasses (cons t subprops)
                                ranges domains types #t augment-set))
                   ((is-iri? p "range")
                    (inner-loop (cons t graph) subclasses subprops
                                (cons t ranges) domains types #t augment-set))
                   ((is-iri? p "domain")
                    (inner-loop (cons t graph) subclasses subprops
                                ranges (cons t domains) types #t augment-set))
                   ((is-iri? p "type")
                    (inner-loop (cons t graph) subclasses subprops
                                ranges domains (cons t types) #t augment-set))
                   (else
                     (inner-loop (cons t graph) subclasses subprops
                                 ranges domains types #t augment-set)))))))))))

(define (entails? g e vocabulary)
  "Return true if g entails e recognizing d"
  (let* ((g (recognize g vocabulary))
         (g (augment g (rdf-vocabulary-datatypes vocabulary)))
         (e (recognize e vocabulary)))
    (or (not (consistent-graph? g vocabulary))
        (d:entails? g e vocabulary))))