From 0f6bede2a2d24df2931e5c9ffc66c833c1a21cb7 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Wed, 15 Sep 2021 17:22:58 +0900
Subject: Add core-system/equal system.

---
 vikalpa.scm | 52 +++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 35 insertions(+), 17 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index 771d484..3bc3374 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -26,6 +26,7 @@
             set-measure-predicate
             set-measure-less-than
             core-system
+            core-system/equal
             define-system
             define-proof
             define-core-function
@@ -58,6 +59,8 @@
     #:getter get-definitions
     #:init-keyword #:definitions
     #:init-value '())
+  (equal-symbol #:getter get-equal-symbol
+                #:init-value 'equal?)
   (measure-predicate #:getter get-measure-predicate
                      #:init-value #f)
   (measure-less-than #:getter get-measure-less-than
@@ -128,6 +131,11 @@
           (equal? name (get-name x)))
         (get-definitions s)))
 
+(define-method (update-equal-symbol (s <symbol>) (sys <system>))
+  (let ((new (shallow-clone sys)))
+    (slot-set! new 'equal-symbol s)
+    new))
+
 (define-method (update-measure-predicate (s <symbol>) (sys <system>))
   (let ((new (shallow-clone sys)))
     (slot-set! new 'measure-predicate s)
@@ -640,10 +648,11 @@
   (and (list? x)
        (every variable? x)))
 
-(define (theorem-rules x)
+(define (theorem-rules x sys)
   (expression->rules (get-variables x)
                      '()
-                     (get-expression x)))
+                     (get-expression x)
+                     sys))
 
 (define (result? x)
   (or (result/error? x)
@@ -824,7 +833,7 @@
           (else
            (fail 'invalid-option (car ops)))))))
 
-(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr)
+(define (rewrite/theorem cmd-name cmd-ops b thm preconds expr sys)
   (call/cc
    (lambda (k)
      (define (fail . args)
@@ -833,7 +842,7 @@
          (parse-options/theorem cmd-ops fail)
        (cond
         ((any (cut apply-rule preconds <> expr env)
-              (theorem-rules thm)) => result/expr)
+              (theorem-rules thm sys)) => result/expr)
         (else
          (result/error 'apply-theorem cmd-name expr)))))))
 
@@ -893,7 +902,7 @@
                      ((is-a? x <core-function>)
                       (rewrite/core-function sys x extracted-expr))
                      ((is-a? x <theorem*>)
-                      (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr))
+                      (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr sys))
                      ((is-a? x <expandable-function>)
                       (rewrite/function sys cmd-name x extracted-expr))
                      (else
@@ -923,10 +932,10 @@
     (('not expr) expr)
     (expr (expr-not expr))))
 
-(define (expr-equal? x)
+(define (expr-equal? x sys)
   (and (list? x)
        (= 3 (length x))
-       (eq? 'equal? (list-ref x 0))
+       (eq? (get-equal-symbol sys) (list-ref x 0))
        (expression? (list-ref x 1))
        (expression? (list-ref x 2))))
 
@@ -936,22 +945,25 @@
 (define (expr-equal-rhs x)
   (list-ref x 2))
 
-(define (expression->rules vars preconds expr)
+(define (expression->rules vars preconds expr sys)
   (if (if-form? expr)
       (append (expression->rules vars
                                  (cons (prop-not
                                         (prop-not
                                          (if-form-test expr)))
                                        preconds)
-                                 (if-form-then expr))
+                                 (if-form-then expr)
+                                 sys)
               (expression->rules vars
                                  (cons (prop-not (if-form-test expr))
                                        preconds)
-                                 (if-form-else expr))
+                                 (if-form-else expr)
+                                 sys)
               (expression->rules vars
                                  preconds
-                                 (if-form-test expr)))
-      (if (expr-equal? expr)
+                                 (if-form-test expr)
+                                 sys))
+      (if (expr-equal? expr sys)
           (list (rule vars
                       preconds
                       (expr-equal-lhs expr)
@@ -962,11 +974,6 @@
                       (expr-equal-lhs expr)))
           '())))
 
-(define (theorem->rules def)
-  (expression->rules (get-variables def)
-                     '()
-                     (get-expression def)))
-
 (define current-system (make-parameter (make <system>)))
 (define reserved-symbols '(quote let if error))
 (define (reserved? x)
@@ -1145,6 +1152,17 @@
     (define-core-function equal? (x y) equal?)
     (current-system)))
 
+(define (core-system/equal)
+  (parameterize ((current-system (make <system>)))
+    (current-system (update-equal-symbol 'equal (current-system)))
+    (define-syntax-rules and ()
+      ((and) '#t)
+      ((and x) x)
+      ((and x . xs) (if x (and . xs) #f)))
+    (define-core-function not (x) not)
+    (define-core-function equal (x y) equal?)
+    (current-system)))
+
 (define-syntax define-system
   (syntax-rules ()
     ((_ name (system) expr ...)
-- 
cgit v1.2.3