From 46822c2b908001d531974f6f6ca34b8aba1b0c42 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 29 Nov 2020 04:05:34 +0900
Subject: wip38 (refactor)

---
 vikalpa.scm         | 64 ++++++++++++++++++++++-------------------------------
 vikalpa/prelude.scm |  4 ++--
 2 files changed, 28 insertions(+), 40 deletions(-)

diff --git a/vikalpa.scm b/vikalpa.scm
index dc5b6de..0264ba9 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -412,28 +412,16 @@
 (define (primitive-function? x)
   (and (list? x)
        (= 5 (length x))
-       (variable? (primitive-function-name x))
+       (variable? (function-name x))
        (eq? 'primitive-function (list-ref x 1))
-       (vars? (primitive-function-vars x))
-       ((option expression?) (primitive-function-expression x))
-       ((option code?) (primitive-function-code x))))
+       (vars? (function-vars x))
+       ((option expression?) (function-expression x))
+       ((option code?) (function-code x))))
 
 ;; (primitive-function variable? vars?) -> primitive-function?
 (define (primitive-function name vs expr code)
   (list name 'primitive-function vs expr code))
 
-(define (primitive-function-name pf)
-  (list-ref pf 0))
-
-(define (primitive-function-vars pf)
-  (list-ref pf 2))
-
-(define (primitive-function-expression pf)
-  (list-ref pf 3))
-
-(define (primitive-function-code pf)
-  (list-ref pf 4))
-
 (define (function? x)
   (and (list? x)
        (= 5 (length x))
@@ -730,19 +718,19 @@
   (or (axiom? x)
       (theorem? x)))
 
-(define (theorem*-name x)
+(define (theorem-name x)
   (list-ref x 0))
 
-(define (theorem*-vars x)
+(define (theorem-vars x)
   (list-ref x 2))
 
-(define (theorem*-expression x)
+(define (theorem-expression x)
   (list-ref x 3))
 
-(define (theorem*-rules x)
-  (expression->rules (theorem*-vars x)
+(define (theorem-rules x)
+  (expression->rules (theorem-vars x)
                      '()
-                     (theorem*-expression x)))
+                     (theorem-expression x)))
 
 (define (error? x)
   (and (pair? x)
@@ -900,7 +888,7 @@
       (parse-options/theorem (command-options cmd) fail)
     (cond
      ((any (cut apply-rule preconds <> expr env)
-           (theorem*-rules thm)) => identity)
+           (theorem-rules thm)) => identity)
      (else
       (fail 'apply-theorem cmd expr)))))
 
@@ -925,7 +913,7 @@
                 (rewrite/theorem cmd sys x preconds extracted-expr fail))
                ((or (function? x)
                     (and (primitive-function? x)
-                         (primitive-function-expression x)))
+                         (function-expression x)))
                 (cond
                  ((any (cut apply-rule '() <> extracted-expr '())
                        (function->rules x)) => identity)
@@ -997,10 +985,10 @@
                       (expr-equal-lhs expr)))
           '())))
 
-(define (theorem*->rules def)
-  (expression->rules (theorem*-vars def)
+(define (theorem->rules def)
+  (expression->rules (theorem-vars def)
                      '()
-                     (theorem*-expression def)))
+                     (theorem-expression def)))
 
 (define current-system (make-parameter (make-system '() '() '())))
 
@@ -1321,7 +1309,7 @@
       (error "make-induction-claim(find-app-forms): not supported"
              expr))
      (else '())))
-  (let ((c (theorem*-expression t)))
+  (let ((c (theorem-expression t)))
     (define (prop app-form)
       (cond
        ((apply-rule '()
@@ -1442,7 +1430,7 @@
               (let ((claim (make-induction-claim seed vars t)))
                 (validate-expression sys
                                      `(claim-of ,(proof-name pf))
-                                     (theorem*-vars t)
+                                     (theorem-vars t)
                                      claim)
                 (rewrite sys-without-self claim (proof-sequence pf)))))
         (else (error "(vikalpa) define-proof: induction function is not found."
@@ -1450,7 +1438,7 @@
                      (cons f vars)))))
       (()
        (rewrite sys-without-self
-                (theorem*-expression t)
+                (theorem-expression t)
                 (proof-sequence pf)))
       (else
        (error "prove/theorem: fail")))))
@@ -1536,15 +1524,15 @@
            `(define-function ,(function-name def) ,(function-vars def)
               ,(function-expression def)))
           ((theorem? def)
-           `(define-theorem ,(theorem*-name def) ,(theorem*-vars def)
-              ,(theorem*-expression def)))
+           `(define-theorem ,(theorem-name def) ,(theorem-vars def)
+              ,(theorem-expression def)))
           ((axiom? def)
-           `(define-axiom ,(theorem*-name def) ,(theorem*-vars def)
-              ,(theorem*-expression def)))
+           `(define-axiom ,(theorem-name def) ,(theorem-vars def)
+              ,(theorem-expression def)))
           ((primitive-function? def)
            `(define-primitive-function
-              ,(primitive-function-name def)
-              ,(primitive-function-vars def)))
+              ,(function-name def)
+              ,(function-vars def)))
           ((macro? def)
            `(define-syntax-rules ,(macro-name def)))
           (else
@@ -1557,7 +1545,7 @@
 
 (define/guard (system-primitives (sys system?))
   (append reserved-symbols
-          (map primitive-function-name
+          (map function-name
                (filter primitive-function?
                        (system-definitions sys)))))
 
@@ -1572,7 +1560,7 @@
                (system-definitions sys))))
 
 (define/guard (system-axioms (sys system?))
-  (map theorem*-name
+  (map theorem-name
        (filter axiom?
                (system-definitions sys))))
 
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 9a25348..83f3b6a 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -83,7 +83,7 @@
 
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
-  
+
   (define-axiom if-not (x y z)
     (equal? (if (not x) y z)
             (if x z y)))
@@ -112,7 +112,7 @@
   (define-axiom pred/succ (x)
     (implies (natural? x)
              (equal? (pred (succ x)) x)))
-  
+
   (define-axiom succ/pred (x)
     (implies (natural? x)
              (not (zero? x))
-- 
cgit v1.2.3