feat: F/T as consts, minor fixes and tests

lisp-inference.asd

@@ -50,6 +50,7 @@
  (:file "test-equivalence-rules")
  (:file "test-inference-rules")
  (:file "test-infix-parsing")
+ (:file "test-truth-table")
  (:file "test-pratt"))
  :perform (test-op (o c)
  (symbol-call :rove :run c)))

roswell/inference-server.ros

@@ -5,18 +5,17 @@ exec ros -Q -- $0 "$@"
 |#
 
 #+quicklisp
-(defun ensure-dist-installed-and-updated (dist nick)
+(defun ensure-dist-installed (dist nick)
  (let ((d (ql-dist:find-dist nick)))
- (if (not (and d (ql-dist:installedp d)))
+ (when (not (and d (ql-dist:installedp d)))
  (ql-dist:install-dist dist
- :prompt nil))
- (ql:update-dist nick :prompt nil)))
+ :prompt nil))))
 
 (progn ;;init forms
  (ros:ensure-asdf)
  #+quicklisp
  (progn
- (ensure-dist-installed-and-updated "http://dist.ultralisp.org" "ultralisp")
+ (ensure-dist-installed "http://dist.ultralisp.org" "ultralisp")
  (ql:quickload '(lisp-inference/web)))
  )
 

src/truth-table.lisp

@@ -11,7 +11,8 @@
 (defun propositionp (symbol)
  "Check if the given SYMBOL can be a proposition (letters)"
  (and (atom symbol)
- (not (valid-operatorp symbol))))
+ (not (valid-operatorp symbol))
+ (not (member (symbol-name symbol) '("T" "F") :test #'string-equal))))
 
 (defun set-of-propositions (exp)
  "Given a propositional expression EXP return the list of
@@ -91,6 +92,14 @@
  (t nil)))
 
 
+(defun replace-tf (exp)
+ (cond ((atom exp)
+ (cond ((string-equal (symbol-name exp) "T") t)
+ ((string-equal (symbol-name exp) "F") nil)
+ (t exp)))
+ (t (cons (replace-tf (car exp))
+ (replace-tf (cdr exp))))))
+
 (defun eval-operations (exp-tree)
  "Generate all the truth-table cases and evaluated it based on EXP-TREE"
  (let ((cases (group-cases-to-propositions exp-tree)))
@@ -99,7 +108,7 @@
  (let ((prop (car pair))
  (value (cadr pair)))
  (nsubst value prop exp)))
- (eval exp)))
+ (eval (replace-tf exp))))
  (let ((exps (stack-of-expressions exp-tree)))
  (loop for case in cases
  collect (append case
@@ -203,11 +212,11 @@ a tautology."
  "A easy way to generate a truth table"
  `(print-truth-table (quote ,exp)))
 
-;; TODO: implement a pratt parser
-(defmacro truth-infix (exp)
+
+(defmacro truth-infix (&rest exp)
  "A easy and infix way of EXP generate a truth table.
  Ex.: (truth-infix (p ^ q)) "
- `(print-truth-table (infix-to-prefix (quote , exp))))
+ `(print-truth-table (parse-logic (format nil "~a" (quote ,exp)))))
 
 
 (defun main ()

t/test-truth-table.lisp

@@ -0,0 +1,49 @@
+(in-package :lisp-inference/tests/test-truth-table)
+
+(deftest truth-table-tests
+ (testing "== Truth-table tests!"
+ (ok (equal (eval-expression '(^ p q))
+ "TFFF")
+ "AND OPERATION: p ^ q")
+
+ (ok (equal (eval-expression '(v p q))
+ "TTTF")
+ "OR OPERATION: p v q")
+
+ (ok (equal (eval-expression '(=> p q))
+ "TFTT")
+ "CONDITIONAL OPERATION: p => q")
+
+ (ok (equal (eval-expression '(<=> p q))
+ "TFFT")
+ "BICONDITIONAL OPERATION: p <=> q")
+
+ (ok (equal (eval-expression '([+] p q))
+ "FTTF")
+ "XOR OPERATION: p [+] q")
+
+ (ok (equal (eval-expression '(~ p))
+ "FT")
+ "NOT OPERATION: ~ p")
+
+ (ok (equal-expression '(^ p q)
+ (de-morgan '(^ p q)))
+ "EQUAL EXPRESSION 1")
+
+ (ok (equal-expression '(~ (~ p))
+ 'p)
+ "EQUAL EXPRESSION 2")))
+
+(deftest truth-table-tests-with-false-and-true
+ (testing "== Truth-table tests with F and T as constant!"
+ (ok (equal (eval-expression '(^ p f))
+ "FF")
+ "CONTRADICTION: p ^ f")
+
+ (ok (equal (eval-expression '(v p t))
+ "TT")
+ "TAUTOLOGY: p v t")
+
+ (ok (equal (eval-expression (parse-logic "(~p v q <=> p => q) <=> t"))
+ "TTTT")
+ "TAUTOLOGY OF CONDITIONAL DEFINITION")))

t/tests.lisp

@@ -13,6 +13,11 @@
  #:lisp-inference
  #:rove))
 
+(defpackage #:lisp-inference/tests/test-truth-table
+ (:use #:cl
+ #:lisp-inference
+ #:rove))
+
 (defpackage #:lisp-inference/tests/test-pratt
  (:use #:cl
  #:lisp-inference
@@ -23,4 +28,5 @@
  (:import-from #:lisp-inference/tests/test-equivalence-rules)
  (:import-from #:lisp-inference/tests/test-inference-rules)
  (:import-from #:lisp-inference/tests/test-infix-parsing)
+ (:import-from #:lisp-inference/tests/test-truth-table)
  (:import-from #:lisp-inference/tests/test-pratt))

web/webapp.lisp

@@ -46,6 +46,25 @@
  :initform nil
  :accessor truth)))
 
+(defmacro js-share-button-function ()
+ "
+var prop = document.getElementById('prop-input').value || document.getElementById('prop-input').placeholder;
+var url = window.location.origin + window.location.pathname + '?prop=' + encodeURIComponent(prop);
+var shareUrlInput = document.getElementById('share-url');
+shareUrlInput.value = url;
+shareUrlInput.style.display = 'block';
+try {
+ navigator.clipboard.writeText(url).then(function() {
+ /* clipboard successfully set */
+ }, function() {
+ /* clipboard write failed */
+ });
+} catch (e) {
+ // ignore
+}
+")
+
+
 (defun truth-table (exp)
  (with-output-to-string (s)
  (let ((inference:*output-stream* s))
@@ -74,30 +93,16 @@
  (update-table table prop)))
  (:input :type "text"
  :id "prop-input"
+ :style "text-align:center;"
  :name "prop"
  :placeholder (prop table))
  (:input :type "submit"
  :value "Eval")
  (:input :type "button"
  :value "Share"
- :onclick "
-var prop = document.getElementById('prop-input').value || document.getElementById('prop-input').placeholder;
-var url = window.location.origin + window.location.pathname + '?prop=' + encodeURIComponent(prop);
-var shareUrlInput = document.getElementById('share-url');
-shareUrlInput.value = url;
-shareUrlInput.style.display = 'block';
-try {
- navigator.clipboard.writeText(url).then(function() {
- /* clipboard successfully set */
- }, function() {
- /* clipboard write failed */
- });
-} catch (e) {
- // ignore
-}
-"))
+ :onclick (js-share-button-function)))
  (:input :type "text" :id "share-url" :style "display: none; width: 100%; margin-top: 10px;" :readonly "readonly")
- (:pre :style "font-size: 25px" (truth table))
+ (:pre :style "font-size: 20px" (truth table))
  (:pre (format nil "Operators: ~a" inference:*valid-operators*)))
  (:p "Some notes: "
  (:ul