feat: add implication equivalence + tests

Improve tests reporter to work over compilation mode of emacs and
click to goto error line

Fix #29

Author: ryukinix

run-test.lisp

@@ -1,5 +1,11 @@
 (load "fix-quicklisp")
 (ql:quickload :lisp-inference/tests :silent t)
+
+(defun rove/utils/reporter::print-source-location-as-file-path (stream file line column)
+  (declare (ignore column))
+  (format stream "~&at ~A~@[:~A~]~%"
+          (rove/utils/reporter::enough-namestring* file)
+          line))
 (setf rove:*enable-colors* t)
 (if (rove:run :lisp-inference/tests)
     (sb-ext:exit :code 0)

src/equivalences.lisp

@@ -49,3 +49,11 @@
           (make-negation (make-conjunction (make-negation (first-operand exp))
                                            (make-negation (second-operand exp)))))
          (t exp))))
+
+(defun implication (exp)
+  "Implication equivalence ::
+  (=> p q) <=> (v (~ p) q)"
+  (if (implicationp exp)
+      (make-disjunction (make-negation (first-operand exp))
+                        (second-operand exp))
+      exp))

src/package.lisp

@@ -7,6 +7,7 @@
   (:use #:cl #:cl-user)
   (:export #:double-negation ;; equivalences
            #:de-morgan
+           #:implication
            #:modus-ponens    ;; inferences
            #:modus-tollens
            #:syllogism-disjunctive
@@ -33,7 +34,9 @@
            #:^
            #:v
            #:=>
+           #:->
            #:<=>
+           #:<->
            #:[+]
            #:make-conjunction
            #:make-negation

src/parser.lisp

@@ -76,12 +76,14 @@
 (defun implicationp (exp)
   "Verify if the expression is an implication"
   (and (binary-operationp exp)
-       (operationp exp '=>)))
+       (or (operationp exp '=>)
+           (operationp exp '->))))
 
 (defun biconditionalp (exp)
   "Verify if the expression is a biconditional"
   (and (binary-operationp exp)
-       (operationp exp '<=>)))
+       (or (operationp exp '<=>)
+           (operationp exp '<->))))
 
 (defun swap-operand-operator (exp)
   (if (and (listp exp)

t/test-equivalence-rules.lisp

@@ -1,22 +1,31 @@
 (in-package #:lisp-inference/tests/test-equivalence-rules)
 
 (deftest test-equivalence-rules
-  (testing "== Equivalence rules!"
-    (ok (equal (de-morgan '(^ p q))
-               '(~ (v (~ p) (~ q))))
-        "Equivalence: DE-MORGAN 1")
-    (ok (equal (de-morgan '(~ (v p q)))
-               '(^ (~ p) (~ q)))
-        "Equivalence: DE-MORGAN 2")
+    (testing "== Equivalence rules!"
+             (ok (equal (de-morgan '(^ p q))
+                        '(~ (v (~ p) (~ q))))
+                 "Equivalence: DE-MORGAN 1")
+             (ok (equal (de-morgan '(~ (v p q)))
+                        '(^ (~ p) (~ q)))
+                 "Equivalence: DE-MORGAN 2")
 
-    (ok (equal (de-morgan '(~ (^ (~ p) (~ q))))
-               '(v p q))
-        "Equivalence: DE-MORGAN 3")
+             (ok (equal (de-morgan '(~ (^ (~ p) (~ q))))
+                        '(v p q))
+                 "Equivalence: DE-MORGAN 3")
 
-    (ok (equal (double-negation '(~ (~ p)))
-               'p)
-        "Equivalence: DOUBLE-NEGATION 1")
+             (ok (equal (double-negation '(~ (~ p)))
+                        'p)
+                 "Equivalence: DOUBLE-NEGATION 1")
 
-    (ok (equal (double-negation 'p)
-               'p)
-        "Equivalence: DOUBLE-NEGATION 2")))
+             (ok (equal (double-negation 'p)
+                        'p)
+                 "Equivalence: DOUBLE-NEGATION 2")
+             (ok (equal (implication '(=> p q))
+                        '(v (~ p) q))
+                 "Equivalence: IMPLICATION EQUIVALENCE")
+
+             (ok (equal (implication '(-> p (~ q)))
+                        '(v (~ p) (~ q)))
+                 "Equivalence: IMPLICATION EQUIVALENCE 2")
+
+             ))