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

(module assertions mzscheme
  
  (provide (all-defined))
  
  (require "inference-environments.ss")
  
  ;; Assertions
  
  ;; 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 null (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)))))

  )