Skip to content

Commit

Permalink
Add tests for tweaked expansion.
Browse files Browse the repository at this point in the history
  • Loading branch information
rpgoldman committed Jan 18, 2024
1 parent 2f88320 commit e29ce48
Showing 1 changed file with 34 additions and 7 deletions.
41 changes: 34 additions & 7 deletions shop3/tests/theorem-prover-tests.lisp
Original file line number Diff line number Diff line change
@@ -1,18 +1,18 @@
;;;
;;; Version: MPL 1.1/GPL 2.0/LGPL 2.1
;;;
;;;
;;; The contents of this file are subject to the Mozilla Public License
;;; Version 1.1 (the "License"); you may not use this file except in
;;; compliance with the License. You may obtain a copy of the License at
;;; http://www.mozilla.org/MPL/
;;;
;;;
;;; Software distributed under the License is distributed on an "AS IS"
;;; basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See the
;;; License for the specific language governing rights and limitations under
;;; the License.
;;;
;;; The Original Code is SHOP2.
;;;
;;;
;;; The Original Code is SHOP2.
;;;
;;; The Initial Developer of the Original Code is the University of
;;; Maryland. Portions created by the Initial Developer are Copyright (C)
;;; 2002,2003 the Initial Developer. All Rights Reserved.
Expand All @@ -21,8 +21,8 @@
;;; Portions created by Drs. Goldman and Kuter are Copyright (C)
;;; 2017 SIFT, LLC. These additions and modifications are also
;;; available under the MPL/GPL/LGPL licensing terms.
;;;
;;;
;;;
;;;
;;; Alternatively, the contents of this file may be used under the terms of
;;; either of the GNU General Public License Version 2 or later (the "GPL"),
;;; or the GNU Lesser General Public License Version 2.1 or later (the
Expand All @@ -44,6 +44,7 @@

(defpackage shop-theorem-prover-tests
(:shadowing-import-from #:shop3.theorem-prover #:fail)
(:import-from #:shop3.theorem-prover #:seek-satisfiers #:*domain*)
(:use common-lisp shop3.theorem-prover fiveam))

(in-package #:shop-theorem-prover-tests)
Expand Down Expand Up @@ -181,3 +182,29 @@
(first (sorted-bindings '?bs bindings))
:test 'equalp)))))

(test check-seek-satisfiers-expansion
;; make sure that we don't have vacuous IF form in
;; expansion...
(multiple-value-bind (expansion expanded-p)
(macroexpand-1
'(seek-satisfiers ((foo)) state nil 1 nil :domain domain))
(is-true expanded-p)
(when expanded-p
(is (eq (first expansion) 'let))
;; binding list
(is (eql (length (second expansion)) 1))
(is (eq (second ; the value
(first (second expansion))) ;the binding form
'domain))))
(multiple-value-bind (expansion expanded-p)
(macroexpand-1
'(seek-satisfiers ((foo)) state nil 1 nil))
(is-true expanded-p)
(when expanded-p
(is (eq (first expansion) 'let))
;; binding list
(is (eql (length (second expansion)) 1))
(is (eq (second ; the value
(first (second expansion))) ;the binding form
'*domain*)))))

0 comments on commit e29ce48

Please sign in to comment.