;;; PLT Scheme Inference Collection
;;; assertions.ss
;;; Copyright (c) 2006 M. Douglas Williams
;;;
;;; 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 2.1 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., 59 Temple Place, Suite 330, Boston, MA
;;; 02111-1307 USA.
;;;
;;; Version Date     Comments
;;; 1.0.1   07/22/06 Added custom printing for assertion structs.
;;;                  (Doug Williams)

(module assertions mzscheme
  
  (provide (all-defined))
  
  (require "inference-environments.ss")
  
  ;; Assertions
  
  (define (assertion-print assertion port write?)
    (when write? (write-string "<" port))
    (if write?
        (fprintf port "assertion-~a: ~s"
                 (assertion-id assertion)
                 (assertion-fact assertion))
        (fprintf port "assertion-~a: ~a"
                 (assertion-id assertion)
                 (assertion-fact assertion)))
    (when (assertion-reason assertion)
      (fprintf port "; ~a"
                (assertion-reason assertion)))
    (when write? (write-string ">" port)))
  
  ;; assertion struct
  ;;   id            - unique id (order chronologically)
  ;;   fact          - the fact asserted
  ;;   reason        - currently unused
  ;; (define-struct assertion (fact reason) (make-inspector))
  (define-values (struct:assertion
                  assertion-constructor
                  assertion?
                  assertion-field-ref
                  set-assertion-field!)
    (make-struct-type 'assertion #f 3 0 #f
                      (list (cons prop:custom-write assertion-print))
                      (make-inspector)))
  
  ;; id field
  (define assertion-id
    (make-struct-field-accessor
     assertion-field-ref 0 'id))
  
  (define set-assertion-id!
    (make-struct-field-mutator
     set-assertion-field! 0 'id))
  
  ;; fact field
  (define assertion-fact
    (make-struct-field-accessor
     assertion-field-ref 1 'fact))
  
  (define set-assertion-fact!
    (make-struct-field-mutator
     set-assertion-field! 1 'fact))
  
  ;; reason field
  (define assertion-reason
    (make-struct-field-accessor
     assertion-field-ref 2 'reason))
  
  (define set-assertion-reason!
    (make-struct-field-mutator
     set-assertion-field! 2 'reason))
  
  ;; make-assertion: fact? x any -> assertion?
  (define (make-assertion fact reason)
    (let ((assertion (assertion-constructor
                      (current-inference-next-assertion-id)
                      fact reason)))
      (current-inference-next-assertion-id
       (+ (current-inference-next-assertion-id) 1))
      assertion))
  
  ;; assertions-subset? list x list -> boolean
  ;; A predicate function that returns true if the first list of
  ;; assertions is a subset of the second.  Used to implement
  ;; match-subset?.
  (define (assertions-subset? assertions-1 assertions-2)
    (cond ((null? assertions-1) #t)
          ((null? assertions-2) #f)
          ((not (eq? (car assertions-1) (car assertions-2))) #f)
          (else
           (assertions-subset? (cdr assertions-1) (cdr assertions-2)))))

  )