;;; 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
           ;;  show
           ;;  check
           ;;  system->scheme
           ;;  load-system
           ;;  system-primitives
           ;;  system-functions
           ;;  system-macros
           ;;  system-theorems
           ;;  system-axioms
           ;;  system-totality-claims
           ;;  define-system
           ;;  define-axiom
           ;;  define-theorem
           ;;  define-primitive-function
           ;;  define-function
           ;;  define-scheme-function
           ;;  define-proof
           ;;  define-totality-claim
           ;;  define-syntax-rules
           ;;  system-eval)
  #:use-module (ice-9 match)
  #:use-module (ice-9 format)
  #:use-module (ice-9 control)
  #:use-module (ice-9 exceptions)
  #:use-module ((srfi srfi-1)
                #:select (every any member lset-union fold append-map
                                find))
  #:use-module (srfi srfi-8)
  #:use-module (srfi srfi-11)
  #:use-module (srfi srfi-26)
  #:use-module (ice-9 pretty-print)
  #:use-module (oop goops))

(define-class <system> ()
  (definitions #:getter system-definitions #:init-keyword #:definitions)
  (total-cliam-method #:getter system-total-claim-method
                      #:init-keyword #:total-cliam-method))

(define-class <definition> ()
  (name #:getter definition-name #:init-keyword #:name))

(define-class <condition> ()
  (expressions #:getter condition-expressions #:init-keyword #:expressions))

(define-class <function> (<definition>)
  (variables #:getter function-variables #:init-keyword #:variables)
  (condition #:getter function-condition #:init-keyword #:condition))

(define-class <total-function> ())

(define-class <core-function> (<function>)
  (procedure #:getter core-function-procedure #:init-keyword #:procedure))

(define-class <defined-function> (<function>)
  (expression #:getter defined-function-expression #:init-keyword #:expression)
  (code #:getter defined-function-code #:init-keyword #:code))

(define-class <total-function> (<defined-function>)
  (proof #:getter theorem-proof #:init-keyword #:proof))

(define-class <primitive-function> (<defined-function>))

(define-generic total-function?)
(define-method (total-function? x)
  (or (is-a? x <core-function>)
      (is-a? x <primitive-function>)
      (is-a? x <total-function>)))

(define-class <proposition> (<definition>)
  (variables #:getter proposition-variables #:init-keyword #:variables)
  (expression #:getter proposition-expression #:init-keyword #:expression))

(define-class <conjecture> (<proposition>))
(define-class <theorem> (<proposition>)
  (proof #:getter theorem-proof #:init-keyword #:proof))
(define-class <axiom> (<theorem>))

(define (theorem? x)
  (or (is-a? x <theorem>)
      (is-a? x <axiom>)))

(define-generic lookup)
(define-method (lookup (name <symbol>) (s <system>))
  (find (lambda (x) (eq? name (definition-name x)))
        (system-definitions s)))

(define-generic add-definition)
(define-method (add-definition (d <definition>) (s <system>))
  (if (lookup (definition-name d) s)
      (raise-exception
       (make-exception
        (make-exception-with-message
         "(vikalpa) add-definition: duplicated definition")
        (make-exception-with-irritants (definition-name s))))
      (make <system>
        #:definitions (cons d (system-definitions s))
        #:total-cliam-method (system-total-claim-method s))))

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

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

(define-syntax define-type
  (syntax-rules ()
    ((_ name
        constractor
        (m p?)
        (n t? getter-var getter) ...)
     (begin
       (define len (+ 1 (length (list n ...))))
       (define (constractor getter-var ...)
         (let ((data (make-list len)))
           (list-set! data m 'name)
           (list-set! data n getter-var)
           ...
           data))
       (define (p? x)
         (and (list? x)
              (= len (length x))
              (eq? 'name (list-ref x m))
              (t? (list-ref x n)) ...))
       (define (getter x)
         (list-ref x n))
       ...))))

;; (natural? x) -> boolean?
(define (natural? x)
  (and (exact-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 (natural? (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 args)
  (cons name args))

(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
   ((expr-quoted? expr) '())
   ((if-form? expr)
    (lset-union eq?
                (expression-vars (if-form-test expr))
                (expression-vars (if-form-then expr))
                (expression-vars (if-form-else expr))))
   ((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))

(define-type rule
  rule
  (0 rule?)
  (1 (lambda (vars)
       (and (list? vars)
            (every variable? vars)))
     vars
     rule-vars)
  (2 (lambda (ps)
       (and (list? ps)
            (every expression? ps)))
     ps
     rule-preconds)
  (3 expression?
     lhs
     rule-lhs)
  (4 expression?
     rhs
     rule-rhs))

(define (binding? x)
  (and (pair? x)
       (symbol? (car x))
       (expression? (cdr x))))

(define (env? x)
  ((list-of binding?) x))

(define/guard (substitute (env env?) (expr (const #t)))
  (debug "substitute: ~s ~s~%" 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-begin lhs expr env)
    (reset (mat lhs expr env)))
  (define (mat lhs expr env)
    (debug "lhs ~a, expr ~a, env ~a~%" lhs expr env)
    (cond ((expr-quoted? lhs)
           (if (expr-quoted? expr)
               (if (equal? lhs expr)
                   env
                   (fail))
               (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)
         (let search ((ps preconds))
           (if (null? ps)
               (shift k ((car k+env) #f))
               (let ((env (mat-begin (car rlps) (car ps) (cdr k+env))))
                 (cond
                  ((mat-begin (car rlps) (car ps) (cdr k+env))
                   => (lambda (env)
                        (shift k0
                               (reset
                                (or (shift k (k0 (cons k env)))
                                    (k0 (search (cdr ps))))))))
                  (else (search (cdr ps))))))))))
  (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 k0
          (match (mat-preconds (rule-preconds rl) (cons k0 env))
            ((k . env)
             (cond
              ((mat-begin (rule-lhs rl) expr env)
               => (lambda (env)
                    (if (valid? env (rule-rhs rl))
                        env
                        (k #f))))
              (else (k #f))))
            (else #f)))))

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

(define-type code
  code
  (0 code?)
  (1 (const #t)
     expr
     code-expr))

(define-type mrule
  mrule
  (0 mrule?)
  (1 (const #t) lhs mrule-lhs)
  (2 (const #t) rhs mrule-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-type macro
  macro
  (1 macro?)
  (0 variable? name macro-name)
  (2 (lambda (mrls)
       (and (list? mrls)
            (every mrule? mrls)))
     mruls
     macro-mrules)
  (3 (list-of symbol?)
     literals
     macro-literals))

(define (apply-mrule rl ls expr)
  (define (literal? x)
    (member x ls))
  (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)
                  (if (equal? lhs expr)
                      env
                      (k #f))
                  (k #f)))
             ((and (pair? lhs) (pair? expr))
              (mat-map lhs expr env))
             ((literal? lhs)
              (if (eq? lhs expr)
                  env
                  (k #f)))
             ((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))))
             ((literal? expr) 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)
                  (error "(vikalpa) macro fail" m expr))
                 ((apply-mrule (car rs) (macro-literals m) expr) => identity)
                 (else (loop (cdr rs))))))
        (else #f)))

(define (expand ms expr)
  (let loop ((ms ms)
             (expr expr))
    (cond
     ((null? ms) expr)
     (else (expand (cdr ms)
                   (cond
                    ((apply-macro (car ms) expr) => identity)
                    (else expr)))))))

(define (expand* ms expr)
  (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
   ((null? x) x)
   ((expr-quoted? x) x)
   ((pair? x)
    (cons (quote-all (car x))
          (quote-all (cdr x))))
   ((symbol? x) x)
   (else `',x)))

(define (let? x)
  (and (list? x)
       (= 3 (length x))
       (eq? 'let (list-ref x 0))
       ((list-of (lambda (x)
                   (and (list? x)
                        (= 2 (length x))
                        (symbol? (car x)))))
        (list-ref x 1))))

(define (expand-let x)
  (define (let-substitute env expr)
    (cond ((expr-quoted? expr) expr)
          ((let? expr)
           (let-substitute
            (append (map (lambda (binding)
                           (cons (car binding)
                                 (let-substitute env
                                                 (cadr binding))))
                         (list-ref expr 1))
                    env)
            (list-ref expr 2)))
          ((pair? expr)
           (cons (let-substitute env (car expr))
                 (let-substitute env (cdr expr))))
          ((assoc expr env) => cdr)
          (else expr)))
  (cond
   ((expr-quoted? x) x)
   ((let? x)
    (expand-let
     (let-substitute (map (lambda (binding) (cons (car binding)
                                                  (cadr binding)))
                          (list-ref x 1))
                     (list-ref x 2))))
   ((pair? x)
    (cons (expand-let (car x))
          (expand-let (cdr x))))
   (else x)))

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

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

(define (theorem-rules x)
  (expression->rules (theorem-variables x)
                     '()
                     (theorem-expression x)))

(define (rewrite/eval expr sys)
  (let eval ((expr expr))
    (cond
     ((expr-quoted? expr) expr)
     ((app-form? expr)
      (let ((args (map eval (app-form-args expr)))
            (name (app-form-name expr)))
        (or (find error? args)
            (eval (rewrite1 sys
                            `(,name ,@args)
                            (lambda args
                              (cons* 'error rewrite name args))
                            (rewriter '() `(,name)))))))
     ((if-form? expr)
      (let ((test (eval (if-form-test expr))))
        (if (error? test)
            test
            (if (expr-unquote test)
                (eval (if-form-then expr))
                (eval (if-form-else expr))))))
     (else
      `(error eval invalid-expression ,expr)))))

;; (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))

;; (define/guard (system-eval (expr (const #t)) (sys system?))
;;   (rewrite/eval (parameterize ((current-system sys))
;;                   (convert-to-expression expr))
;;                 sys))

;; (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 (prop-not (prop-not precond))
                                   extracted-preconds))
                        ((3) (cons (prop-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-variables x)
              (condition-expressions (function-condition x))
              (function-app-form x)
              (defined-function-expression x))
        (rule (function-variables x)
              (condition-expressions (function-condition x))
              (defined-function-expression x)
              (function-app-form x))))

(define (apply-function f args)
  (apply-rule '()
              (rule (function-variables f)
                    '()
                    (defined-function-app-form f)
                    (defined-function-expression f))
              (app-form (definition-name f) args)
              '()))

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

(define (rewrite/theorem cmd b thm preconds expr fail)
  (receive (env)
      (parse-options/theorem (command-options cmd) fail)
    (cond
     ((any (cut apply-rule preconds <> expr env)
           (theorem-rules thm)) => identity)
     (else
      (fail 'apply-theorem cmd expr)))))

(define (rewrite/induction sys fname vars expr fail)
  (cond
   ((lookup fname sys)
    (cut make-induction-claim <> vars expr))
   (else (fail 'induction 'not-found fname))))

(define (rewrite1 sys expr fail r)
  (let* ((cmd (rewriter-command r))
         (cmd/name (command-name cmd)))
    (debug "~%~%cmd: ~a~%" cmd)
    (receive (extracted-expr preconds builder)
        (extract (rewriter-path r) expr fail)
      (builder
       (cond
        ((equal? '(eval) cmd/name)
         (rewrite/eval extracted-expr sys))
        ((match cmd/name
           (`(induction ,(f . vars))
            (rewrite/induction sys f vars extracted-expr fail))
           (`(induction . ,x)
            (fail 'induction x))
           (else #f)) => identity)
        ((eq? 'error cmd/name) (fail extracted-expr))
        ((and (symbol? cmd/name)
              (lookup cmd/name sys))
         => (lambda (x)
              (cond
               ((is-a? x <proposition>)
                (rewrite/theorem cmd sys x preconds extracted-expr fail))
               ((and (total-function? x)
                     (is-a? x <defined-function>))
                (cond
                 ((any (cut apply-rule '() <> extracted-expr '())
                       (function->rules x)) => identity)
                 (else
                  (fail 'apply-function cmd extracted-expr))))
               (else
                (fail 'invalid-command cmd extracted-expr)))))
        (else (fail 'command-not-found cmd extracted-expr)))))))

#;
(define/guard (rewrite (sys system?) (expr (const #t)) (seq sequence?))
  (let ((expr (convert-to-expression expr)))
    (let loop ((expr expr)
               (seq seq))
      (reset
       (if (null? seq)
           expr
           (loop (rewrite1 sys
                           expr
                           (lambda args
                             (shift k (cons 'error args)))
                           (car seq))
                 (cdr seq)))))))

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

(define (prop-not x)
  (match x
    (('not ('not expr)) (prop-not expr))
    (('not expr) expr)
    (expr (expr-not expr))))

(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 (prop-not
                                        (prop-not
                                         (if-form-test expr)))
                                       preconds)
                                 (if-form-then expr))
              (expression->rules vars
                                 (cons (prop-not (if-form-test expr))
                                       preconds)
                                 (if-form-else expr))
              (expression->rules vars
                                 preconds
                                 (if-form-test 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-variables def)
                     '()
                     (theorem-expression def)))

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


;; (define (add-definition x)
;;   (let ((sys (current-system)))
;;     (current-system
;;      (cond ((lookup (definition-name x) sys)
;;             => (lambda (d)
;;                  (if (equal? x d)
;;                      sys
;;                      (error "(vikalpa) add-definition: duplicated"
;;                             (definition-name d)))))
;;            (else (make-system (cons x (system-definitions sys))
;;                               (system-proofs sys)
;;                               (system-totality-claim-list 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: duplicated"))))
;;            (else (make-system (system-definitions sys)
;;                               (cons x (system-proofs sys))
;;                               (system-totality-claim-list sys)))))
;;     x))

;; (define reserved-symbols '(quote let if error))
;; (define (reserved? x)
;;   (member x reserved-symbols))

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

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

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

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

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

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

;; (define (find-totality-claim name sys)
;;   (assoc name (system-totality-claim-list sys)))

;; (define (add-totality-claim tc)
;;   (let ((sys (current-system)))
;;     (cond ((find-totality-claim (totality-claim-id tc) sys)
;;            => (lambda (tc2)
;;                 (unless (equal? tc tc2)
;;                   (error "(vikalpa) define-totality-claim: duplicated"
;;                          tc)))))
;;     (unless (and (symbol? (totality-claim-id tc))
;;                  (cond ((lookup (totality-claim-natural tc) sys)
;;                         => function*?)
;;                        (else #f))
;;                  (cond ((lookup (totality-claim-less-than tc) sys)
;;                         => function*?)
;;                        (else #f)))
;;       (error "(vikalpa) define-totality-claim: invalid totality-claim"
;;              tc))
;;     (current-system
;;      (make-system (system-definitions sys)
;;                   (system-proofs sys)
;;                   (cons tc (system-totality-claim-list sys))))))

;; (define-syntax-rule (define-totality-claim name nat? <)
;;   (add-totality-claim (totality-claim 'name 'nat? '<)))

;; (define core-function-names
;;   '(not equal? pair? cons car cdr integer? < binary-+ unary--))

;; (define (core-function-name? x)
;;   (member x core-function-names))

;; (define (rewrite/core name extracted-expr fail)
;;   (case name
;;     ((not)
;;      (match extracted-expr
;;        (('not `(quote ,x))
;;         (expr-quote (not x)))
;;        (else
;;         (fail 'not extracted-expr))))
;;     ((equal?)
;;      (match extracted-expr
;;        (('equal? `(quote ,x) `(quote ,y))
;;         (expr-quote (equal? x y)))
;;        (else
;;         (fail 'equal? extracted-expr))))
;;     ((pair?)
;;      (match extracted-expr
;;        (('pair? `(quote ,x))
;;         (expr-quote (pair? x)))
;;        (else
;;         (fail 'pair? extracted-expr))))
;;     ((cons)
;;      (match extracted-expr
;;        (('cons `(quote ,x) `(quote ,y))
;;         (expr-quote (cons x y)))
;;        (else
;;         (fail 'cons extracted-expr))))
;;     ((car)
;;      (match extracted-expr
;;        (('car `(quote ,x))
;;         (if (pair? x)
;;             (expr-quote (car x))
;;             ''()))
;;        (else
;;         (fail 'car extracted-expr))))
;;     ((cdr)
;;      (match extracted-expr
;;        (('cdr `(quote ,x))
;;         (if (pair? x)
;;             (expr-quote (cdr x))
;;             ''()))
;;        (else
;;         (fail 'cdr extracted-expr))))
;;     ((integer?)
;;      (match extracted-expr
;;        (('integer? `(quote ,x))
;;         (expr-quote (integer? x)))
;;        (else
;;         (fail 'integer? extracted-expr))))
;;     ((<)
;;      (match extracted-expr
;;        (('< `(quote ,x) `(quote ,y))
;;         (let ((x (if (integer? x) x 0))
;;               (y (if (integer? y) y 0)))
;;           (expr-quote (< x y))))
;;        (else
;;         (fail '< extracted-expr))))
;;     ((succ)
;;      (match extracted-expr
;;        (('binary-+ `(quote ,x) `(quote ,y))
;;         (if (integer? x)
;;             (if (integer? y)
;;                 (expr-quote (+ x y))
;;                 (expr-quote x))
;;             (if (integer? y)
;;                 (expr-quote y)
;;                 (expr-quote 0))))
;;        (else
;;         (fail 'binary-+ extracted-expr))))
;;     ((unary--)
;;      (match extracted-expr
;;        (('unary-- `(quote ,x))
;;         (if (integer? x)
;;             (expr-quote (- x))
;;             (expr-quote 0)))
;;        (else
;;         (fail 'unary-- extracted-expr))))
;;     (else (fail 'rewrite/core 'invalid))))

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

(define (defined-function-app-form f)
  (cons (definition-name f) (function-variables f)))

(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-totality-claim tc m-expr f)
;;   (let* ((name (function-name f)))
;;     (define (convert app-form)
;;       (cond
;;        ((apply-rule '()
;;                     (rule (function-vars f)
;;                           '()
;;                           (function-app-form f)
;;                           m-expr)
;;                     app-form
;;                     '())
;;         => identity)
;;        (else (error "make-totality-claim: convert error"
;;                     (function-name f)
;;                     m-expr
;;                     app-form))))
;;     (if/if `(,(totality-claim-natural tc) ,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 `(,(totality-claim-less-than tc)
;;                                ,(convert expr)
;;                                ,m-expr)
;;                              rest)
;;                      rest)))
;;               (else (error "(vikalpa) make-totality-claim: error"
;;                            (function-name f)
;;                            m-expr))))
;;            ''#f)))

;; (define (make-guard-claim expr sys)
;;   (define (find-preconds expr)
;;     (cond
;;      ((app-form? expr)
;;       (let ((rest (append-map find-preconds (cdr expr))))
;;         (append (cond ((lookup (car expr) sys) =>
;;                        (lambda (f)
;;                          (let ((preconds (function-guard f)))
;;                            (map (lambda (precond)
;;                                   (substitute (map cons
;;                                                    (function-vars f)
;;                                                    (cdr expr))
;;                                               precond))
;;                                 preconds))))
;;                       (else (error "make-guard-claim: error")))
;;                 rest)))
;;      ((if-form? expr)
;;       (find-preconds (if-form-test expr)))
;;      (else '())))
;;   (define (build/find-if expr)
;;     (cond
;;      ((if-form? expr)
;;       (if/if (build/find-if (if-form-test expr))
;;              (build (if-form-then expr))
;;              (build (if-form-else expr))))
;;      ((app-form? expr)
;;       (apply and/if (map build/find-if (app-form-args expr))))
;;      (else ''#t)))
;;   (define (build expr)
;;     (cond
;;      ((if-form? expr)
;;       (apply and/if
;;              (append (find-preconds (if-form-test expr))
;;                      (list (if/if (if-form-test expr)
;;                                   (build (if-form-then expr))
;;                                   (build (if-form-else expr)))))))
;;      ((app-form? expr)
;;       (apply and/if
;;              (append (find-preconds expr)
;;                      (list (build/find-if expr)))))
;;      (else ''#t)))
;;   (if/if (build expr)
;;          ''#t
;;          ''#f))

(define (make-induction-claim f vars c)
  (define (find-app-forms expr)
    (cond
     ((app-form? expr)
      (let ((rest (append-map find-app-forms (cdr expr))))
        (if (eq? (definition-name f) (app-form-name expr))
            (cons expr rest)
            rest)))
     ((if-form? expr)
      (error "make-induction-claim(find-app-forms): not supported"
             expr))
     (else '())))
  (define (prop app-form)
    (cond
     ((apply-rule '()
                  (rule vars
                        '()
                        (app-form (definition-name f) vars)
                        c)
                  app-form
                  '())
      => identity)
     (else
      (error "make-induction-claim: fail" app-form))))
  (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 c))))

;; (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 ()
;;     ((_ name
;;         (((n ...) cmd ...) ...))
;;      (add-proof (proof 'name
;;                        '()
;;                        '(((n ...) cmd ...) ...))))
;;     ((_ name
;;         (seed ...)
;;         (((n ...) cmd ...) ...))
;;      (add-proof (proof 'name
;;                        '(seed ...)
;;                        '(((n ...) cmd ...) ...))))))

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

;; (define (validate-expression sys name vars expr)
;;   (let* ((expr-fnames (expression-functions expr))
;;          (expr-vars (expression-vars expr)))
;;     (when (reserved? name)
;;       (error (format #f "(vikalpa) ~a: reserved name" name)))
;;     (for-each (lambda (x)
;;                 (when (member x expr-fnames)
;;                   (error (format #f "(vikalpa) ~a: invalid variable name" name)
;;                          x)))
;;               vars)
;;     (for-each (lambda (x)
;;                 (unless (cond ((lookup x sys) => function*?)
;;                               (else #f))
;;                   (error (format #f "(vikalpa) ~a: undefined function" name)
;;                          x)))
;;               expr-fnames)
;;     (for-each (lambda (x)
;;                 (unless (member x vars)
;;                   (error (format #f "(vikalpa) ~a: undefined variable" name)
;;                          x)))
;;               expr-vars)))

;; (define (validate-definition d)
;;   (let* ((vars (definition-vars d))
;;          (name (definition-name d))
;;          (expr (definition-expression d)))
;;     (validate-expression (current-system) name vars expr)))

;; (define (recur? f)
;;   (member (function-name f)
;;           (expression-functions (function-expression f))))

;; (define (p x)
;;   (format #t "p:~%~y" x)
;;   x)

;; (define (trivial-total? f sys)
;;   (and (not (recur? 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)
;;   (let ((sys-without-self
;;          (make-system (filter (lambda (d) (not (equal? t d)))
;;                               (system-definitions sys))
;;                       (system-proofs sys)
;;                       (system-totality-claim-list sys))))
;;     (rewrite sys-without-self
;;              (theorem-expression t)
;;              (proof-sequence pf))))

;; (define (prove/function sys f pf)
;;   (match (proof-seed pf)
;;     (()
;;      (error "prove/function error"))
;;     ((id m-expr)
;;      (cond
;;       ((find-totality-claim id sys)
;;        => (lambda (tc)
;;             (let ((claim (make-totality-claim tc m-expr f)))
;;               (validate-expression sys
;;                                    `(claim-of ,(function-name f))
;;                                    (function-vars f)
;;                                    claim)
;;               (rewrite sys
;;                        claim
;;                        (proof-sequence pf)))))
;;       (else
;;        (error "(vikalpa) define-proof: totality-claim is not found:"
;;               (proof-name pf)
;;               (proof-seed pf)))))
;;     (else
;;      (error "define-proof: fail"
;;             (proof-name pf) (proof-seed pf)))))

;; (define (system->scheme sys)
;;   `(begin
;;      ,@(map (lambda (f)
;;               `(define (,(function-name f) ,@(function-vars f))
;;                  ,(code-expr (function-code f))))
;;             (reverse (filter (lambda (x)
;;                                (and (function*? x)
;;                                     (function-code x)))
;;                              (system-definitions sys))))))

;; (define/guard (check (sys system?))
;;   (let loop ((sys sys)
;;              (fails '()))
;;     (let ((defs (system-definitions sys)))
;;       (define* (next #:optional fail)
;;         (loop (make-system (cdr defs)
;;                            (system-proofs sys)
;;                            (system-totality-claim-list 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) sys))
;;           (next))
;;          (else
;;           (cond
;;            ((find-proof (definition-name (car defs)) sys)
;;             => (lambda (pf)
;;                  (let ((result (prove sys (car defs) pf)))
;;                    (cond
;;                     ((equal? result ''#t)
;;                      (next))
;;                     (else
;;                      (next (list (definition-name (car defs))
;;                                  result)))))))
;;            (else
;;             (next (list (definition-name (car defs)))))))))
;;        (else
;;         (next))))))

;; (define/guard (show (sys system?) (name symbol?))
;;   (cond
;;    ((lookup name sys)
;;     => (lambda (def)
;;          (cond
;;           ((function? def)
;;            `(define-function ,(function-name def) ,(function-vars def)
;;               ,(function-expression def)))
;;           ((theorem? 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)))
;;           ((primitive-function? def)
;;            `(define-primitive-function
;;               ,(function-name def)
;;               ,(function-vars def)))
;;           ((macro? def)
;;            `(define-syntax-rules ,(macro-name def)))
;;           (else
;;            `(error 'fatal-error ,name)))))
;;    (else
;;     `(error 'not-found ,name))))

;; (define/guard (load-system (sys system?))
;;   (primitive-eval (system->scheme sys)))

;; (define/guard (system-primitives (sys system?))
;;   (append reserved-symbols
;;           (map function-name
;;                (filter primitive-function?
;;                        (system-definitions sys)))))

;; (define/guard (system-functions (sys system?))
;;   (map function-name
;;        (filter function?
;;                (system-definitions sys))))

;; (define/guard (system-theorems (sys system?))
;;   (map theorem-name
;;        (filter theorem?
;;                (system-definitions sys))))

;; (define/guard (system-axioms (sys system?))
;;   (map theorem-name
;;        (filter axiom?
;;                (system-definitions sys))))

;; (define/guard (system-macros (sys system?))
;;   (map macro-name
;;        (filter macro?
;;                (system-definitions sys))))

;; (define/guard (system-totality-claims (sys system?))
;;   (system-totality-claim-list sys))