;;; Vikalpa --- Proof Assistant
;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
;;;
;;; This file is part of Vikalpa.
;;;
;;; Vikalpa is free software; you can redistribute it and/or modify it
;;; under the terms of the GNU General Public License as published by
;;; the Free Software Foundation; either version 3 of the License, or
;;; (at your option) any later version.
;;;
;;; Vikalpa is distributed in the hope that it will be useful, but
;;; WITHOUT ANY WARRANTY; without even the implied warranty of
;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
;;; General Public License for more details.
;;;
;;; You should have received a copy of the GNU General Public License
;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.

(define-module (vikalpa)
  #:export (rewrite)
  #:use-module (ice-9 match)
  #:use-module (ice-9 format)
  #:use-module (ice-9 control)
  #:use-module ((srfi srfi-1) #:select (every any member lset-union fold append-map))
  #:use-module (srfi srfi-8)
  #:use-module (srfi srfi-11)
  #:use-module (srfi srfi-26))

(define (debug f . args)
  (if #f
      (apply format #t f args)
      #t))

(define-syntax-rule (define/guard (name (var pred?) ...) b b* ...)
  (define (name var ...)
    (unless (pred? var)
      (error (format #f
                     "~a:~%  expected:  ~a~%  given: "
                     'name
                     'pred?)
             var))
    ...
    b b* ...))

;; (natural? x) -> boolean?
(define (natural? x)
  (and (integer? x)
       (not (negative? x))))

(define (option p?)
  (lambda (x)
    (or (p? x) (not x))))

(define (list-of p?)
  (lambda (x)
    (and (list? x)
         (every p? x))))

;; (expression? x) -> boolean?
(define (expression? expr)
  (cond ((expr-quoted? expr)
         (or (integer? (expr-unquote expr))
             (boolean? (expr-unquote expr))
             (symbol? (expr-unquote expr))
             (null? (expr-unquote expr))))
        ((if-form? expr)
         (and (expression? (if-form-test expr))
              (expression? (if-form-then expr))
              (expression? (if-form-else expr))))
        ((app-form? expr)
         (and (symbol? (car expr))
              (list? (cdr expr))
              (every expression? (cdr expr))))
        ((variable? expr) #t)
        (else #f)))

(define (app-form? expr)
  (and (pair? expr)
       (not (eq? (car expr) 'quote))
       (not (eq? (car expr) 'if))))

(define (app-form-name expr)
  (car expr))

(define (app-form-args expr)
  (cdr expr))

(define (if-form test then else)
  (list 'if test then else))

(define (if-form? x)
  (and (pair? x)
       (eq? (car x) 'if)))

(define (if-form-test expr)
  (list-ref expr 1))

(define (if-form-then expr)
  (list-ref expr 2))

(define (if-form-else expr)
  (list-ref expr 3))

(define (expression-functions expr)
  (cond
   ((if-form? expr)
    (apply lset-union
           eq?
           (map expression-functions
                (list (if-form-test expr)
                      (if-form-then expr)
                      (if-form-else expr)))))
   ((app-form? expr)
    (cons (app-form-name expr)
          (apply lset-union
                 eq?
                 (map expression-functions (app-form-args expr)))))
   (else '())))

(define (expression-vars expr)
  (cond
   ((app-form? expr)
    (apply lset-union eq?
           (map expression-vars (app-form-args expr))))
   ((variable? expr) (list expr))
   (else '())))

;; (expr-quoted? x) -> boolean?
(define (expr-quoted? expr)
  (and (pair? expr)
       (eq? 'quote (car expr))
       (pair? (cdr expr))
       ((const #t) (car (cdr expr)))
       (null? (cdr (cdr expr)))))

(define (expr-unquote expr)
  (car (cdr expr)))

;; (expr-quoted? x) -> boolean?
(define (expr-quote expr)
  (list 'quote expr))

;; (variable? x) -> boolean?
(define (variable? x)
  (symbol? x))

;; (variable=? variable? variable?) -> boolean?
(define (variable=? v1 v2)
  (eq? v1 v2))

;; (rule? x) -> boolean?
(define (rule? x)
  (and (list? x)
       (= 5 (length x))
       (eq? (car x) 'rule)
       (let ((vars (list-ref x 1)))
         (and (list? vars)
              (every variable? vars)))
       (let ((preconds (list-ref x 2)))
         (and (list? preconds)
              (every expression? preconds)))
       (expression? (list-ref x 3))
       (expression? (list-ref x 4))))

;; (rule (list-of variable?) expression? expression?) -> rule?
(define (rule vars preconds lhs rhs)
  (list 'rule vars preconds lhs rhs))

;; (rule-vars rule?) -> (list-of variable?)
(define (rule-vars r)
  (list-ref r 1))

;; (rule-preconds rule?) -> expression?
(define (rule-preconds r)
  (list-ref r 2))

;; (rule-lhs rule?) -> expression?
(define (rule-lhs r)
  (list-ref r 3))

;; (rule-rhs rule?) -> expression?
(define (rule-rhs r)
  (list-ref r 4))

;; (environment x) -> boolean?
;; environment is alist
(define (environment x)
  (cond ((null? x) #t)
        ((pair? x)
         (and (pair? (car x))
              (variable? (car (car x)))
              (expression? (cdr (car x)))
              (environment (cdr x))))
        (else #f)))

(define* (rebuild expr preconds
                  #:key
                  (quoted-proc (lambda (expr preconds) expr))
                  (variable-proc (lambda (expr preconds) expr))
                  (if-proc (lambda (expr preconds next) (next)))
                  (app-form-proc (lambda (expr preconds next) (next))))
  (let rec ((expr expr)
            (preconds preconds))
    (cond
     ((expr-quoted? expr)
      (quoted-proc expr preconds))
     ((variable? expr)
      (variable-proc expr preconds))
     ((if-form? expr)
      (letrec ((next
                (lambda* (#:optional (expr expr))
                  (let* ((expr/test (rec (if-form-test expr) preconds))
                         (expr/then (rec (if-form-then expr) (cons (if-form-test expr) preconds)))
                         (expr/else (rec (if-form-else expr) (cons (expr-not (if-form-test expr)) preconds))))
                    (if-form expr/test expr/then expr/else)))))
        (if-proc expr preconds next)))
     ((app-form? expr)
      (letrec ((next
                (lambda* (#:optional (expr expr))
                  (let f ((expr-args (app-form-args expr)))
                    (cond ((null? expr-args) '())
                          (else
                           (cons (rec (car expr-args) preconds)
                                 (f (cdr expr-args)))))))))
        (app-form-proc expr preconds next)))
     (else
      (error "(vikalpa) rebuild: error")))))

(define* (expr-fold expr acc preconds
                    #:key
                    (quoted-proc (lambda (expr acc preconds) acc))
                    (variable-proc (lambda (expr acc preconds) acc))
                    (if-proc (lambda (expr acc preconds next) (next)))
                    (app-form-proc (lambda (expr acc preconds next) (next))))
  (let rec ((expr expr)
            (acc acc)
            (preconds preconds))
    (cond
     ((expr-quoted? expr)
      (quoted-proc expr acc preconds))
     ((variable? expr)
      (variable-proc expr acc preconds))
     ((if-form? expr)
      (letrec ((next
                (lambda* (#:optional (expr expr) (acc acc) (preconds preconds))
                  (let* ((acc/test
                          (rec (if-form-test expr) acc preconds))
                         (acc/then
                          (rec (if-form-then expr) acc/test (cons (if-form-test expr) preconds))))
                    (rec (if-form-else expr) acc/then (cons (expr-not (if-form-test expr)) preconds))))))
        (if-proc expr acc preconds next)))
     ((app-form? expr)
      (letrec ((next
                (lambda* (#:optional (expr expr) (acc acc) (preconds preconds))
                  (let fold ((expr-args (app-form-args expr))
                             (acc acc))
                    (cond ((null? expr-args) acc)
                          (else
                           (fold (cdr expr-args)
                                 (rec (car expr-args)
                                      acc
                                      preconds))))))))
        (app-form-proc expr acc preconds next)))
     (else
      (error "(vikalpa) expr-fold: error")))))

(define (substitute env expr)
  (cond ((expr-quoted? expr) expr)
        ((pair? expr)
         (cons (substitute env (car expr))
               (substitute env (cdr expr))))
        ((assoc expr env) => cdr)
        (else expr)))

(define (match-rule preconds rl expr env)
  (define (fail)
    (shift k #f))
  (define (var? v)
    (and (member v (rule-vars rl))
         #t))
  (define (add-env var expr env)
    (cond
     ((assoc var env)
      => (match-lambda
           ((env-var . env-expr)
            (if (equal? env-expr expr)
                env
                (fail)))))
     (else
      (cons (cons var expr)
            env))))
  (define (mat-fold lhss exprs env)
    (cond ((and (pair? lhss) (pair? exprs))
           (mat-fold (cdr lhss)
                     (cdr exprs)
                     (mat (car lhss)
                          (car exprs)
                          env)))
          ((and (null? lhss) (null? exprs)) env)
          (else (fail))))
  (define (mat lhs expr env)
    (debug "lhs ~a, expr ~a, env ~a~%" lhs expr env)
    (cond ((expr-quoted? lhs)
           (if (expr-quoted? expr)
               (and (equal? lhs expr) env)
               (fail)))
          ((and (if-form? lhs)
                (if-form? expr))
           (mat-fold (list (if-form-test lhs)
                           (if-form-then lhs)
                           (if-form-else lhs))
                     (list (if-form-test expr)
                           (if-form-then expr)
                           (if-form-else expr))
                     env))
          ((app-form? lhs)
           (if (and (app-form? expr)
                    (symbol? (app-form-name lhs))
                    (eqv? (app-form-name lhs) (app-form-name expr)))
               (mat-fold (app-form-args lhs) (app-form-args expr) env)
               (fail)))
          ((var? lhs) (add-env lhs expr env))
          (else (fail))))
  (define (mat-preconds rlps k+env)
    (if (null? rlps)
        k+env
        (mat-preconds (cdr rlps)
                      (any (lambda (p)
                             (shift k
                                    (cond
                                     ((reset (mat (car rlps) p (cdr k+env)))
                                      => (lambda (env) (k (cons k env))))
                                     (else (k #f)))))
                           preconds))))
  (define (valid? env expr)
    (cond ((expr-quoted? expr) #t)
          ((pair? expr)
           (and (valid? env (car expr))
                (valid? env (cdr expr))))
          ((var? expr)
           (cond ((assoc expr env) => (const #t))
                 (else #f)))
          (else #t)))
  (debug "rule: ~a~%" rl)
  (debug "preconds: ~a~%" preconds)
  (debug "expr: ~a~%" expr)
  (reset
   (shift k
          (match (mat-preconds (rule-preconds rl) (cons k env))
            ((k . env)
             (cond
              ((reset (mat (rule-lhs rl) expr env))
               => (lambda (env)
                    (if (valid? env (rule-rhs rl))
                        env
                        #f)))
              (else (k #f))))
            (else #f)))))

;; (apply-rule preconds rule? expression?) -> (or (cons rhs environment) #f)
(define (apply-rule preconds rl expr env)
  (cond
   ((match-rule preconds rl expr env)
    => (cut substitute <> (rule-rhs rl)))
   (else #f)))


(define (system? x)
  (and (list? x)
       (= 3 (length x))
       (eq? 'system (list-ref x 0))
       (system-definitions? (system-definitions x))
       (system-proofs? (system-proofs x))))

(define (make-system defs prfs)
  (list 'system defs prfs))

(define (system-definitions sys)
  (list-ref sys 1))

(define (system-proofs sys)
  (list-ref sys 2))

(define (lookup x sys)
  (assoc x (system-definitions sys)))

(define (find-proof x sys)
  (assoc x (system-proofs sys)))

;; (system-definitions? x) -> boolean?
(define (system-definitions? x)
  (cond ((null? x) #t)
        ((pair? x)
         (and (pair? (car x))
              (or (theorem*? (car x))
                  (primitive-function? (car x))
                  (macro? (car x))
                  (function? (car x)))
              (system-definitions? (cdr x))))
        (else #f)))

;; (system-proofs? x) -> boolean?
(define (system-proofs? x)
  (cond ((null? x) #t)
        ((pair? x)
         (and (pair? (car x))
              (proof? (car x))
              (system-proofs? (cdr x))))
        (else #f)))

(define (primitive-function? x)
  (and (list? x)
       (= 3 (length x))
       (variable? (primitive-function-name x))
       (eq? 'primitive-function (list-ref x 1))
       (vars? (primitive-function-vars x))))

;; (primitive-function variable? vars?) -> primitive-function?
(define (primitive-function name vs)
  (list name 'primitive-function vs))

(define (primitive-function-name pf)
  (list-ref pf 0))

(define (primitive-function-vars pf)
  (list-ref pf 2))

(define (function? x)
  (and (list? x)
       (= 4 (length x))
       (variable? (function-name x))
       (eq? 'function (list-ref x 1))
       (vars? (function-vars x))
       (expression? (function-expression x))))

;; (function variable? vars? expression?) -> function?
(define/guard (function (name variable?) (vars vars?) (expr expression?))
  (list name 'function vars expr))

(define (function-name f)
  (list-ref f 0))

(define (function-vars f)
  (list-ref f 2))

(define (function-expression f)
  (list-ref f 3))

(define (definition-name d)
  (list-ref d 0))

(define (mrule? x)
  (and (list? x)
       (= 3 (length x))
       (eq? 'mrule (list-ref x 0))
       ((const #t) (mrule-lhs x))
       ((const #t) (mrule-rhs x))))

(define (mrule lhs rhs)
  (list 'mrule lhs rhs))

(define (mrule-vars mrl)
  (define (all-vars x)
    (cond ((expr-quoted? x) '())
          ((pair? x)
           (append (all-vars (car x))
                   (all-vars (cdr x))))
          ((variable? x) (list x))
          (else '())))
  (all-vars (mrule-lhs mrl)))

(define (mrule-lhs mrl)
  (list-ref mrl 1))

(define (mrule-rhs mrl)
  (list-ref mrl 2))

(define (macro? x)
  (and (list? x)
       (= 3 (length x))
       (eq? 'macro (list-ref x 1))
       (variable? (macro-name x))
       (let ((mrls (macro-mrules x)))
         (and (list? mrls)
              (every mrule? mrls)))))

(define (macro-name m)
  (list-ref m 0))

(define (macro-mrules m)
  (list-ref m 2))

(define (macro name rules)
  (list name 'macro rules))

(define (apply-mrule rl expr)
  (define (var? v)
    (and (member v (mrule-vars rl))
         #t))
  (call/cc
   (lambda (k)
     (define (mat-map lhs-tree expr-tree env)
       (cond ((and (pair? lhs-tree)
                   (pair? expr-tree))
              (mat-map (car lhs-tree)
                       (car expr-tree)
                       (mat-map (cdr lhs-tree)
                                (cdr expr-tree)
                                env)))
             (else (mat lhs-tree expr-tree env))))
     (define (mat lhs expr env)
       (cond ((expr-quoted? lhs)
              (if (expr-quoted? expr)
                  (and (equal? lhs expr)
                       env)
                  (k #f)))
             ((and (pair? lhs)
                   (pair? expr))
              (mat-map lhs expr env))
             ((var? lhs)
              (cond
               ((assoc lhs env)
                => (match-lambda
                     ((env-var . env-expr)
                      (if (equal? env-expr expr)
                          env
                          (k #f)))))
               (else
                (cons (cons lhs expr)
                      env))))
             ((eqv? lhs expr) env)
             (else (k #f))))
     (define (mrule-substitute env expr)
       (cond ((expr-quoted? expr) expr)
             ((pair? expr)
              (cons (mrule-substitute env (car expr))
                    (mrule-substitute env (cdr expr))))
             ((and (variable? expr) (assoc expr env)) => cdr)
             (else expr)))
     (mrule-substitute (mat (mrule-lhs rl)
                            expr
                            '())
                       (mrule-rhs rl)))))

(define (apply-macro m expr)
  (cond ((and (pair? expr)
              (eq? (macro-name m) (car expr)))
         (let loop ((rs (macro-mrules m)))
           (cond ((null? rs) expr)
                 ((apply-mrule (car rs) expr) => identity)
                 (else (loop (cdr rs))))))
        (else #f)))

(define/guard (expand (ms (list-of macro?)) (expr (const #t)))
  (let loop ((ms ms)
             (expr expr))
    (cond
     ((null? ms) expr)
     (else (expand (cdr ms)
                   (cond
                    ((apply-macro (car ms) expr) => identity)
                    (else expr)))))))

(define/guard (expand* (ms (list-of macro?)) (expr (const #t)))
  (let loop ((ms ms)
             (expr expr))
    (let ((new-expr (expand ms expr)))
      (if (equal? expr new-expr)
          (if (pair? new-expr)
              (cons (expand* ms (car new-expr))
                    (expand* ms (cdr new-expr)))
              new-expr)
          (expand* ms new-expr)))))

(define (quote-all x)
  (cond
   ((expr-quoted? x) x)
   ((if-form? x)
    (if-form (quote-all (if-form-test x))
             (quote-all (if-form-then x))
             (quote-all (if-form-else x))))
   ((app-form? x)
    (cons (app-form-name x)
          (map quote-all (app-form-args x))))
   ((variable? x) x)
   (else `',x)))

(define (convert-to-expression x)
  (quote-all
   (expand* (filter macro? (system-definitions (current-system)))
            x)))

;; (axiom variable? vars? expression?) -> axiom?
;; axiom? is theorem*
(define/guard (axiom (name variable?) (vars vars?) (expr expression?))
  (list name 'axiom vars expr))

(define (vars? x)
  (and (list? x)
       (every variable? x)))

;; (axiom? x) -> boolean?
(define (axiom? x)
  (and (list? x)
       (= 4 (length x))
       (variable?  (list-ref x 0))
       (eq? 'axiom (list-ref x 1))
       (vars? (list-ref x 2))
       (expression? (list-ref x 3))))

;; (theorem name vars? expression?) -> theorem?
(define/guard (theorem (name variable?) (vars vars?) (expr expression?))
  (list name 'theorem vars expr))

;; (theorem? x) -> boolean?
;; theorem? is theorem*
(define (theorem? x)
  (and (list? x)
       (= 4 (length x))
       (variable? (list-ref x 0))
       (eq? 'theorem (list-ref x 1))
       (vars? (list-ref x 2))
       (expression? (list-ref x 3))))

(define (theorem-name x)
  (list-ref x 0))

;; (theorem*? x) -> boolean?
(define (theorem*? x)
  (or (axiom? x)
      (theorem? x)))

(define (theorem*-name x)
  (list-ref x 0))

(define (theorem*-vars x)
  (list-ref x 2))

(define (theorem*-expression x)
  (list-ref x 3))

(define (theorem*-rules x)
  (expression->rules (theorem*-vars x)
                     '()
                     (theorem*-expression x)))

;; (rewriter path? command?) -> rewriter?
(define (rewriter p c)
  (cons p c))

(define (rewriter-path r)
  (car r))

(define (rewriter-command r)
  (cdr r))

(define (rewriter? x)
  (and (pair? x)
       (path? (car x))
       (command? (cdr x))))

;; (sequence? x) -> boolean?
(define (sequence? x)
  (and (list? x)
       (every rewriter? x)))

;; (path? x) -> boolean?
;; path is list
(define (path? x)
  (and (list? x)
       (every natural? x)))

;; (command-name? x) -> booelan?
(define (command? x)
  (and (pair? x)
       (command-name? (car x))
       ((list-of command-option?) (cdr x))))

;; (command-name? x) -> booelan?
(define (command-name? x)
  (or (symbol? x)
      ((list-of symbol?) x)))

;; (command-option? x) -> boolean?
(define (command-option? x)
  (and (pair? x)
       (case (car x)
         ((set) (and (list? x)
                     (= 3 (length x))
                     (variable? (list-ref x 1))
                     (expression? (list-ref x 2))))
         (else #f))))

(define (command-name x)
  (car x))

(define (command-options x)
  (cdr x))

;; (extract path? expression? preconds? procedure?) -> (values expression? procedure?)
(define (extract path expr fail)
  (if (null? path)
      (values expr '() identity)
      (let ((i (car path)))
        (cond
         ((if-form? expr)
          (let ((precond (if-form-test expr)))
            (receive (extracted-expr extracted-preconds builder)
                (extract (cdr path) (list-ref expr i) fail)
              (values extracted-expr
                      (case i
                        ((1) '())
                        ((2) (cons precond extracted-preconds))
                        ((3) (cons (expr-not precond) extracted-preconds))
                        (else (fail "(if) invaild path" path)))
                      (lambda (x)
                        (append (list-head expr i)
                                (list (builder x))
                                (list-tail expr (+ i 1))))))))
         ((< i (length expr))
          (receive (extracted-expr preconds builder)
              (extract (cdr path) (list-ref expr i) fail)
            (values extracted-expr
                    preconds
                    (lambda (x)
                      (append (list-head expr i)
                              (list (builder x))
                              (list-tail expr (+ i 1)))))))
         (else
          (fail "invalid path" path))))))

(define (function->rules x)
  (list (rule (function-vars x)
              '()
              (function-app-form x)
              (function-expression x))
        (rule (function-vars x)
              '()
              (function-expression x)
              (function-app-form x))))

(define (apply-function f args)
  (apply-rule '()
              (rule (function-vars f)
                    '()
                    (function-app-form f)
                    (function-expression f))
              (cons (function-name f) args)
              '()))

(define (parse-options/theorem ops)
  (if (null? ops)
      (values '())
      (receive (env)
          (parse-options/theorem (cdr ops))
        (case (caar ops)
          ((set) (let ((op (car ops)))
                   (cons (cons (list-ref op 1)
                               (list-ref op 2))
                         env)))
          (else
           (error "invalid option:" (car ops)))))))

(define (rewrite/theorem cmd b thm preconds expr fail)
  (receive (env)
      (parse-options/theorem (command-options cmd))
    (cond
     ((any (cut apply-rule preconds <> expr env)
           (theorem*-rules thm)) => identity)
     (else
      (fail (format #f "no match-rule (~a)" cmd))))))

;; (rewrite system? rewriter? expression? procedure?) -> expr
(define (rewrite1 sys expr fail r)
  (let* ((cmd (rewriter-command r))
         (cmd/name (command-name cmd)))
    (debug "~%~%cmd: ~a~%" cmd)
    #;(format #t "~%~%cmd: ~a~%" cmd)
    (receive (extracted-expr preconds builder)
        (extract (rewriter-path r) expr fail)
      (builder
       (cond
        ((and (symbol? cmd/name)
              (lookup cmd/name sys))
         => (lambda (x)
              (cond
               ((theorem*? x)
                (rewrite/theorem cmd sys x preconds extracted-expr fail))
               ((function? x)
                (debug "FUNCTION: ~y" x)
                (cond
                 ((any (cut apply-rule '() <> extracted-expr '())
                       (function->rules x)) => identity)
                 (else
                  (fail (format #f "no match-function (~a)" cmd)))))
               ((primitive-function? x)
                (fail "primitive-function fail"))
               ((macro? x)
                (fail "macro fail"))
               (else
                (fail "rewrite error")))))
        (else (fail "no cmd (~a)" cmd)))))))

(define/guard (rewrite (sys system?) (expr expression?) (seq sequence?))
  (debug "rewrite ~y~%" expr)
  (let loop ((expr expr)
             (seq seq))
    (debug "~y~%" expr)
    #;(format #t "~y~%" expr)
    (if (null? seq)
        expr
        (loop (rewrite1 sys
                        expr
                        (lambda (x . args)
                          (apply error
                                 (format #f "rewrite: ~a" x)
                                 args))
                        (car seq))
              (cdr seq)))))

(define (expr-not x)
  (list 'not x))

(define (expr-equal? x)
  (and (list? x)
       (= 3 (length x))
       (eq? 'equal? (list-ref x 0))
       (expression? (list-ref x 1))
       (expression? (list-ref x 2))))

(define (expr-equal-lhs x)
  (list-ref x 1))

(define (expr-equal-rhs x)
  (list-ref x 2))

(define (expression->rules vars preconds expr)
  (if (if-form? expr)
      (append (expression->rules vars
                                 (cons (if-form-test expr) preconds)
                                 (if-form-then expr))
              (expression->rules vars
                                 (cons (expr-not (if-form-test expr)) preconds)
                                 (if-form-else expr)))
      (if (expr-equal? expr)
          (list (rule vars
                      preconds
                      (expr-equal-lhs expr)
                      (expr-equal-rhs expr))
                (rule vars
                      preconds
                      (expr-equal-rhs expr)
                      (expr-equal-lhs expr)))
          '())))

(define (theorem*->rules def)
  (expression->rules (theorem*-vars def)
                     '()
                     (theorem*-expression def)))

(define current-system (make-parameter (make-system '() '())))

(define (add-definition x)
  (let ((sys (current-system)))
    (current-system
     (cond ((lookup (theorem*-name x) sys)
            => (lambda (thm)
                 (if (equal? x thm)
                     sys
                     (error "add-definition: error"))))
           (else (make-system (cons x (system-definitions sys))
                              (system-proofs sys)))))
    x))

(define (add-proof x)
  (let ((sys (current-system)))
    (current-system
     (cond ((find-proof (proof-name x) sys)
            => (lambda (prf)
                 (if (equal? x prf)
                     sys
                     (error "add-proof: error"))))
           (else (make-system (system-definitions sys)
                              (cons x (system-proofs sys))))))
    x))

(define-syntax define-axiom
  (syntax-rules ()
    ((_ name (var ...) expr)
     (let ((t (axiom 'name '(var ...)
                     (convert-to-expression 'expr))))
       (validate-theorem t)
       (add-definition t)
       t))))

(define-syntax define-theorem
  (syntax-rules ()
    ((_ name (var ...) expr)
     (let ((t (theorem 'name '(var ...)
                       (convert-to-expression 'expr))))
       (validate-theorem t)
       (add-definition t)
       t))))

(define-syntax define-function
  (syntax-rules ()
    ((_ name (var ...) expr)
     (let ((f (function 'name '(var ...)
                        (convert-to-expression 'expr))))
       (validate-function f)
       (add-definition f)
       f))))

(define-syntax define-primitive-function
  (syntax-rules ()
    ((_ name (var ...))
     (let ((f (primitive-function 'name '(var ...))))
       (add-definition f)
       f))))

(define-syntax define-macro
  (syntax-rules ()
    ((_ name () ((lhs1 . lhs2) rhs) ...)
     (let ((m (macro 'name
                (list (mrule '(lhs1 . lhs2) 'rhs)
                      ...))))
       (add-definition m)
       m))))

(define-syntax define-system
  (syntax-rules ()
    ((_ name (systems ...) expr ...)
     (define* (name #:optional (parent (make-system '() '())))
       (parameterize ([current-system
                       ((compose systems ... identity) parent)])
         expr
         ...
         (unless (system? (current-system))
           (error "define-system: error"))
         (current-system))))))

(define-syntax system
  (syntax-rules ()
    ((_ (systems ...) expr ...)
     (lambda* (#:optional (parent (make-system '() '())))
       (parameterize ([current-system
                       ((compose systems ... identity) parent)])
         expr
         ...
         (unless (system? (current-system))
           (error "define-system: error"))
         (current-system))))))

(define (atom? x)
  (not (pair? x)))

(define (any? x) #t)

(define-system prelude ()
  (define-primitive-function natural? (x))
  (define-primitive-function equal? (x y))
  (define-primitive-function atom? (x))
  (define-primitive-function cons (x y))
  (define-primitive-function car (x))
  (define-primitive-function cdr (x))
  (define-primitive-function size (x))
  (define-primitive-function < (x y))
  (define-primitive-function not (x))

  (define-axiom equal-same (x)
    (equal? (equal? x x) '#t))
  (define-axiom equal-swap (x y)
    (equal? (equal? x y) (equal? y x)))
  (define-axiom equal-if (x y)
    (if (equal? x y) (equal? x y) '#t))
  (define-axiom atom/cons (x y)
    (equal? (atom? (cons x y)) '#f))
  (define-axiom car/cons (x y)
    (equal? (car (cons x y)) x))
  (define-axiom cdr/cons (x y)
    (equal? (cdr (cons x y)) y))
  (define-axiom cons/car+cdr (x)
    (if (atom? x)
        '#t
        (equal? (cons (car x) (cdr x)) x)))
  (define-axiom if-nest (x y z)
    (if x
        (equal? (if x y z) y)
        (equal? (if x y z) z)))
  (define-axiom if-nest-t (x y z)
    (if x
        (equal? (if x y z) y)
        '#t))
  (define-axiom if-nest-f (x y z)
    (if x
        '#t
        (equal? (if x y z) z)))
  (define-axiom if-false (x y)
    (equal? (if '#f x y) y))
  (define-axiom if-same (x y)
    (equal? (if x y y) y))
  (define-axiom natural/size (x)
    (equal? (natural? (size x))
            '#t))
  (define-axiom size/car (x)
    (if (atom? x)
        '#t
        (equal? (< (size (car x)) (size x))
                '#t)))
  (define-axiom size/cdr (x)
    (if (atom? x)
        '#t
        (equal? (< (size (cdr x)) (size x))
                '#t)))
  (define-axiom if-not (x y z)
    (equal? (if (not x) y z)
            (if x z y)))

  (define-macro list ()
    ((list) '())
    ((list x . y) (cons x (list . y))))

  (define-macro and ()
    ((and) '#t)
    ((and x) x)
    ((and x . xs) (if x (and . xs) #f)))

  (define-macro or ()
    ((or) '#f)
    ((or x) x)
    ((or x . xs) (if x x (or . xs))))

  #;
  (define-macro + ()
    ((+) '0)
    ((+ x) x)
    ((+ x . xs) (b+ x (+ . xs))))
  #;
  (define-macro - ()
    ((- x) (u- x))
    ((- x . xs) (+ x . (u- (+ . xs)))))
)

(define (measure? x)
  (and (pair? x)
       (variable? (car x))
       (list? (cdr x))
       (<= 1 (length (cdr x)))))

(define (measure-function-name m)
  (car m))

(define (measure-function-vars m)
  (cdr m))

(define (function-app-form f)
  (cons (function-name f) (function-vars f)))

(define (expand-all b expr)
  (expand* (filter macro? b) expr))

(define (single? x)
  (and (pair? x)
       (null? (cdr x))))

(define (if/if x y z)
  (cond
   ((equal? y z) y)
   ((equal? x ''#t) y)
   ((equal? x ''#f) z)
   (else `(if ,x ,y ,z))))

(define (and/if . args)
  (cond
   ((null? args) ''#t)
   ((equal? ''#t (car args)) (apply and/if (cdr args)))
   (else
    (let ((rest (apply and/if (cdr args))))
      (if (equal? ''#t rest)
          (car args)
          (if/if (car args)
                 rest
                 ''#f))))))

(define (implies/if x y)
  (cond
   ((equal? ''#f x) ''#t)
   ((equal? ''#t y) ''#t)
   (else
    (if/if x y ''#t))))

(define (make-total-claim/natural m vars f)
  (let ((name (function-name f))
        (m-expr (cons (function-name m) vars)))
    (define (convert app-form)
      (cond
       ((apply-rule '()
                    (rule (function-vars f)
                          '()
                          (function-app-form f)
                          m-expr)
                    app-form
                    '())
        => identity)
       (else (error "make-total-claim/natural: convert error"
                    app-form))))
    (if/if `(natural? ,m-expr)
           (let loop ((expr (function-expression f)))
             (cond
              ((expr-quoted? expr) ''#t)
              ((variable? expr) ''#t)
              ((if-form? expr)
               (let ((test/result (loop (if-form-test expr)))
                     (then/result (loop (if-form-then expr)))
                     (else/result (loop (if-form-else expr))))
                 (and/if test/result
                         (if/if (if-form-test expr)
                                then/result
                                else/result))))
              ((app-form? expr)
               (let ((rest
                      (let f ((args (app-form-args expr)))
                        (cond ((null? args) ''#t)
                              ((single? args) (loop (car args)))
                              (else (and/if (loop (car args))
                                            (f (cdr args))))))))
                 (if (eq? name (app-form-name expr))
                     (and/if `(< ,(convert expr) ,m-expr)
                             rest)
                     rest)))
              (else (error "(vikalpa) make-total-claim: error"))))
           ''#t)))

(define/guard (make-induction-claim (f function*?)
                                    (vars (list-of variable?))
                                    (t theorem?))
  (define (find-app-forms expr)
    (cond
     ((app-form? expr)
      (let ((rest (append-map find-app-forms (cdr expr))))
        (if (eq? (function-name f) (app-form-name expr))
            (cons expr rest)
            rest)))
     ((if-form? expr)
      (error "make-induction-claim: FAILED m(- -)m"))
     (else '())))
  (let ((c (theorem*-expression t)))
    (define (prop app-form)
      (cond
       ((apply-rule '()
                    (rule (function-vars f)
                          '()
                          (cons (function-name f) vars)
                          c)
                    app-form
                    '())
        => identity)
       (else
        (error "make-induction-claim: fail"))))
    (cond
     ((apply-function f vars)
      => (lambda (expr)
           (let build ((expr expr))
             (cond
              ((if-form? expr)
               (let ((app-forms (find-app-forms (if-form-test expr))))
                 (implies/if (if (null? app-forms)
                                 ''#t
                                 (fold implies/if c (map prop app-forms)))
                             (if/if (if-form-test expr)
                                    (build (if-form-then expr))
                                    (build (if-form-else expr))))))
              (else
               (let ((app-forms (find-app-forms expr)))
                 (fold implies/if c (map prop app-forms))))))))
     (else (error "make-induction-claim: invalid"
                  f vars t)))))

(define (proof? x)
  (and (list? x)
       (= 4 (length x))
       (symbol? (proof-name x))
       (eq? 'proof (list-ref x 1))
       (seed? (proof-seed x))
       (sequence? (proof-sequence x))))

(define (proof name seed sequence)
  (list name 'proof seed sequence))

(define (proof-name x)
  (list-ref x 0))

(define (proof-seed x)
  (list-ref x 2))

(define (proof-sequence x)
  (list-ref x 3))

(define seed? (const #t))

(define-syntax define-proof
  (syntax-rules (total natural? induction)
    ((_ name
        (total natural? (measure var ...))
        (((n ...) cmd ...) ...))
     (add-proof (proof 'name
                       '(total natural? (measure var ...))
                       '(((n ...) cmd ...) ...))))
    ((_ name
        (induction (f var ...))
        (((n ...) cmd ...) ...))
     (add-proof (proof 'name
                       '(induction (f var ...))
                       '(((n ...) cmd ...) ...))))
    ((_ name
        ()
        (((n ...) cmd ...) ...))
     (add-proof (proof 'name
                       '()
                       '(((n ...) cmd ...) ...))))))

(define (function*? x)
  (or (function? x)
      (primitive-function? x)))

(define (validate-function f)
  (let ((fexpr (function-expression f))
        (fvars (function-vars f))
        (fname (function-name f)))
    (for-each (lambda (x)
                (unless (cond
                         ((lookup x (current-system)) => function*?)
                         (else (eq? fname x)))
                  (error (format #f "(vikalpa) ~a: undefined function" fname)
                         x)))
              (expression-functions fexpr))
    (for-each (lambda (x)
                (unless (member x fvars)
                  (error (format #f "(vikalpa) ~a: undefined variable" fname)
                         x)))
              (expression-vars fexpr))))

(define (validate-theorem t)
  (let ((texpr (function-expression t))
        (tvars (function-vars t))
        (tname (function-name t)))
    (for-each (lambda (x)
                (unless (cond ((lookup x (current-system)) => function*?)
                              (else #f))
                  (error (format #f "~a: undefined function" tname)
                         x)))
              (expression-functions texpr))
    (for-each (lambda (x)
                (unless (member x tvars)
                  (error (format #f "~a: undefined variable" tname)
                         x)))
              (expression-vars texpr))))

(define (trivial-total? f)
  (not (member (function-name f)
               (expression-functions (function-expression f)))))

(define (prove sys def pf)
  (cond
   ((theorem? def)
    (prove/theorem sys def pf))
   ((function? def)
    (prove/function sys def pf))
   (else (error "prove" def pf))))

(define (prove/theorem sys t pf)
  (match (proof-seed pf)
    (('induction (f . vars))
     (rewrite sys
              (make-induction-claim (lookup f sys)
                                    vars
                                    t)
              (proof-sequence pf)))
    (()
     (rewrite sys
              (theorem*-expression t)
              (proof-sequence pf)))
    (else
     (error "prove/theorem: fail"))))

(define (prove/function sys f pf)
  (match (proof-seed pf)
    (('total 'natural? (m . vars))
     (rewrite sys
              (make-total-claim/natural (lookup m sys)
                                        vars
                                        f)
              (proof-sequence pf)))
    (else
     (error "prove/function: fail"))))

(define-system app/system (prelude)
  (define-function app (x y)
    (if (atom? x)
        y
        (cons (car x) (app (cdr x) y))))

  (define-theorem associate-app (x y z)
    (equal? (app (app x y) z)
            (app x (app y z))))

  (define-proof app
    (total natural? (size x))
    (((2 3) size/cdr)
     ((2) if-same)
     (() if-same)))
    
  (define-proof associate-app
    (induction (app x y))
    (((2 2) app)
     ((2 2) if-nest-t)
     ((2 1 1) app)
     ((2 1 1) if-nest-t)
     ((2) equal-same)
     ((3 2 1 1) app)
     ((3 2 1 1) if-nest-f)
     ((3 2 2) app)
     ((3 2 2) if-nest-f)
     ((3 2 2 2) equal-if)
     ((3 2 1) app)
     ((3 2 1 3 1) car/cons)
     ((3 2 1 3 2 1) cdr/cons)
     ((3 2 1 1) atom/cons)
     ((3 2 1) if-false)
     ((3 2) equal-same)
     ((3) if-same)
     (() if-same))))

(define (size x)
  (if (pair? x)
      (+ 1
         (size (car x))
         (size (cdr x)))
      0))

(define (app x y)
  (if (atom? x)
      y
      (cons (car x) (app (cdr x) y))))

(define (check sys)
  (let loop ((sys sys)
             (fails '()))
    (let ((defs (system-definitions sys)))
      (define* (next #:optional fail)
        (loop (make-system (cdr defs)
                           (system-proofs sys))
              (if fail
                  (cons fail fails)
                  fails)))
      (cond
       ((null? defs) fails)
       ((or (theorem? (car defs))
            (function? (car defs)))
        (cond
         ((and (function? (car defs))
               (trivial-total? (car defs)))
          (format #t "`~a` is trivial total function.~%"
                  (definition-name (car defs)))
          (next))
         (else
          (cond
           ((find-proof (definition-name (car defs)) sys)
            => (lambda (pf)
                 (let ((result (prove sys (car defs) pf)))
                   (cond
                    ((equal? result ''#t)
                     (format #t "`~a` is ~a.~%"
                             (definition-name (car defs))
                             (if (function? (car defs))
                                 "total function"
                                 "true"))
                     (next))
                    (else
                     (format #t "`~a`'s proof is failed:~%~y"
                             (definition-name (car defs))
                             result)
                     (next (definition-name (car defs))))))))
           (else
            (format #t "`~a`'s proof is not found.~%"
                    (definition-name (car defs)))
            (next (definition-name (car defs))))))))
       (else
        (next))))))