;;;; 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 vocabulary)

  (define (alist-set lst key val)

    (match lst

      (() (list (cons key val)))

      (((k . v) lst ...)

       (if (equal? k key)

           (cons (cons key val) lst)

           (cons (cons k v) (alist-set lst key val))))))

  (define (compatible? types)

    (match types

      (() #t)

      ((_) #t)

      ((a b ...)

       (and (null? (filter

                     (lambda (t)

                       ((rdf-vocabulary-compatible? vocabulary) a t))

                     b))

            (compatible? b)))))

  (define (compatible-types? graph)

    (let loop ((graph graph) (type-mappings '()))

      (if (null? graph)

          (null?

            (filter

              (lambda (t)

                (not (compatible? (cdr t))))

              type-mappings))

          (let* ((t (car graph)))

            (if (equal? (rdf-triple-predicate t) (rdf-iri "type"))

                (loop

                  (cdr graph)

                  (alist-set type-mappings (rdf-triple-subject t)

                             (cons (rdf-triple-object t)

                                   (or

                                     (assoc-ref type-mappings

                                                (rdf-triple-subject t))

                                     '())))))))))

  (and (d:consistent-graph? graph vocabulary)

       (compatible-types? (augment (recognize 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 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

      (() (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 (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 vocabulary)

  "Return true if g entails e"

  (let* ((g (recognize g vocabulary))

         (g (augment g))

         (e (recognize e vocabulary)))

    (or (not (consistent-graph? g vocabulary))

        (d:entails? g e vocabulary))))