;;; Vikalpa --- Proof Assistant
;;; Copyright © 2020, 2021 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 (system?
            system-rewrite
            system-check
            system-apropos
            system-eval
            system-lookup
            set-measure-predicate
            set-measure-less-than
            core-system
            core-system/equal-t-nil
            define-system
            define-proof
            define-core-function
            define-core-function/guard
            define-function
            define-function
            define-function/guard
            define-axiom-function
            define-axiom-function/guard
            define-syntax-rules
            define-axiom
            define-theorem
            define-guard-theorem
            admit)
  #:use-module (ice-9 match)
  #:use-module (ice-9 format)
  #:use-module (ice-9 control)
  #:use-module (ice-9 exceptions)
  #:use-module (ice-9 regex)
  #:use-module (ice-9 pretty-print)
  #:use-module ((srfi srfi-1)
                #:select (every any lset-union fold append-map find
                                filter-map))
  #:use-module (srfi srfi-8)
  #:use-module (srfi srfi-11)
  #:use-module (srfi srfi-26)
  #:use-module (oop goops))

(define-class <system> ()
  (definitions
    #:getter get-definitions
    #:init-keyword #:definitions
    #:init-value '())
  (equal-symbol #:getter get-equal-symbol
                #:init-value 'equal?
                #:init-keyword #:equal-symbol)
  (true-object #:getter get-true-object
               #:init-value ''#t
               #:init-keyword #:true-object)
  (false-object #:getter get-false-object
                #:init-value ''#f
                #:init-keyword #:false-object)
  (measure-predicate #:getter get-measure-predicate
                     #:init-value #f)
  (measure-less-than #:getter get-measure-less-than
                     #:init-value #f))

(define-syntax-rule (true) (get-true-object (current-system)))
(define-syntax-rule (false) (get-false-object (current-system)))

(define-class <definition> ()
  (name #:getter get-name
        #:init-keyword #:name)
  (variables #:getter get-variables
             #:init-keyword #:variables
             #:init-value '()))

(define-class <provable> ())

(define-class <proved> (<provable>)
  (claim #:getter get-claim #:init-keyword #:claim)
  (proof #:getter get-proof #:init-keyword #:proof))

(define-class <admitted> ())

(define-class <theorem*> (<definition>)
  (expression #:getter get-expression #:init-keyword #:expression))

(define-class <conjecture> (<theorem*> <provable>))
(define-class <theorem> (<theorem*> <proved>))
(define-class <axiom> (<theorem*>))
(define-class <admitted-theorem> (<theorem*> <proved> <admitted>))

(define-class <function*> (<definition>)
  (guards #:getter get-guards #:init-keyword #:guards))
(define-class <core-function> (<function*>)
  (procedure #:getter get-procedure #:init-keyword #:procedure))
(define-class <expandable-function> (<function*>)
  (expression #:getter get-expression #:init-keyword #:expression)
  (code #:getter get-code #:init-keyword #:code))
(define-class <function> (<expandable-function> <provable>))
(define-class <total-function> (<expandable-function> <proved>))
(define-class <admitted-function> (<expandable-function> <proved> <admitted>))

(define-class <macro> (<definition>)
  (mrules #:getter macro-mrules #:init-keyword #:mrules)
  (literals #:getter macro-literals #:init-keyword #:literals))

(define (write-definition sym d port)
  (format port "#<~a: ~s>"
          sym (cons (get-name d) (get-variables d))))

(define-method (display (s <system>) port)
  (format port "#<system: function: ~a theorem: ~a macro: ~a>"
          (length (filter (cut is-a? <> <function*>)
                          (get-definitions s)))
          (length (filter (cut is-a? <> <theorem*>)
                          (get-definitions s)))
          (length (filter (cut is-a? <> <macro>)
                          (get-definitions s)))))

(define-method (write (s <system>) port)
  (format port "#<system: function: ~a theorem: ~a macro: ~a>"
          (length (filter (cut is-a? <> <function*>)
                          (get-definitions s)))
          (length (filter (cut is-a? <> <theorem*>)
                          (get-definitions s)))
          (length (filter (cut is-a? <> <macro>)
                          (get-definitions s)))))

(define-method (lookup name (s <system>))
  (find (lambda (x)
          (equal? name (get-name x)))
        (get-definitions s)))

(define-method (update-measure-predicate (s <symbol>) (sys <system>))
  (let ((new (shallow-clone sys)))
    (slot-set! new 'measure-predicate s)
    new))

(define-method (update-measure-less-than (s <symbol>) (sys <system>))
  (let ((new (shallow-clone sys)))
    (slot-set! new 'measure-less-than s)
    new))

(define-method (update-definition (d <definition>) (sys <system>))
  (define (update d defs)
    (if (null? defs)
        (raise-exception
         (make-exception
          (make-exception-with-origin 'update-definition)
          (make-exception-with-message "not found")
          (make-exception-with-irritants (list d defs))))
        (if (equal? (get-name d) (get-name (car defs)))
            (cons d (cdr defs))
            (cons (car defs) (update d (cdr defs))))))
  (let ((new (shallow-clone sys)))
    (slot-set! new 'definitions
               (update d (get-definitions sys)))
    new))

(define-method (remove-first-definition (sys <system>))
  (let ((new (shallow-clone sys)))
    (slot-set! new 'definitions
               (cdr (get-definitions sys)))
    new))

(define-method (first-definition (sys <system>))
  (car (get-definitions sys)))

(define-method (system-empty? (sys <system>))
  (null? (get-definitions sys)))

(define-method (add-definition (d <definition>) (s <system>))
  (if (lookup (get-name d) s)
      (raise-exception
       (make-exception
        (make-exception-with-origin 'add-definition)
        (make-exception-with-message "duplicated definition")
        (make-exception-with-irritants (get-name d))))
      (if (reserved? (get-name d))
          (raise-exception
           (make-exception
            (make-exception-with-origin 'add-definition)
            (make-exception-with-message "reserved name")
            (make-exception-with-irritants (get-name d))))
          (let ((new (shallow-clone s)))
            (slot-set! new 'definitions
                       (cons d (get-definitions s)))
            new))))

(define-method (validate (d <definition>))
  (let* ((vars (get-variables d))
         (name (get-name d)))
    (validate-vars (format #f "~a" name) vars)))

(define-method (validate (d <expandable-function>))
  (let* ((vars (get-variables d))
         (name (get-name d))
         (expr (get-expression d)))
    (validate-expression name vars expr)
    (next-method)))

(define-method (validate (d <theorem*>))
  (let* ((vars (get-variables d))
         (name (get-name d))
         (expr (get-expression d)))
    (validate-expression name vars expr)
    (next-method)))

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

(define (expression? expr)
  (cond ((expr-quoted? expr) #t)
        ((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-app-forms expr)
  (cond
   ((if-form? expr)
    (append-map expression-app-forms
                (list (if-form-test expr)
                      (if-form-then expr)
                      (if-form-else expr))))
   ((app-form? expr)
    (cons expr
          (append-map expression-app-forms
                      (app-form-args expr))))
   (else '())))

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

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

(define (expr-quote expr)
  (list 'quote expr))

(define (variable? x)
  (symbol? x))

(define (variable=? v1 v2)
  (eq? v1 v2))

(define-class <rule> ()
  (vars #:getter rule-vars #:init-keyword #:vars)
  (preconds #:getter rule-preconds #:init-keyword #:preconds)
  (lhs #:getter rule-lhs #:init-keyword #:lhs)
  (rhs #:getter rule-rhs #:init-keyword #:rhs))

(define (rule var preconds lhs rhs)
  (make <rule>
    #:vars var
    #:preconds preconds
    #:lhs lhs
    #:rhs rhs))

(define (rule? x)
  (is-a? x <rule>))

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

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

(define (code x)
  (list 'code x))

(define (code-expr x)
  (cadr x))

(define-class <mrule> ()
  (lhs #:getter mrule-lhs #:init-keyword #:lhs)
  (rhs #:getter mrule-rhs #:init-keyword #:rhs))

(define (mrule lhs rhs)
  (make <mrule> #:lhs lhs #:rhs 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 (macro name mrules literals)
  (make <macro>
    #:name name
    #:variables '()
    #:mrules mrules
    #:literals 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? (get-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 (and (not (expr-quoted? new-expr))
                   (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 (cut is-a? <> <macro>)
                    (get-definitions (current-system)))
            (expand-let x))))

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

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

(define (result? x)
  (or (result/error? x)
      (result/expr? x)))

(define (result/error? x)
  (and (pair? x)
       (eq? 'result/error (car x))))

(define (result/error . args)
  (cons* 'result/error args))

(define (result/expr? x)
  (and (list? x)
       (= 2 (length x))
       (eq? 'result/expr (car x))
       (expression? (cadr x))))

(define (result/expr x)
  (list 'result/expr x))

(define/guard (result/expr-expr (x result/expr?))
  (cadr x))

(define (rewrite/eval expr)
  (let eval ((result (result/expr expr)))
    (cond
     ((result/error? result) result)
     ((result/expr? result)
      (let ((expr (result/expr-expr result)))
        (cond
         ((expr-quoted? expr) (result/expr expr))
         ((app-form? expr)
          (let ((args/result (map (compose eval result/expr)
                                  (app-form-args expr)))
                (name (app-form-name expr)))
            (cond
             ((find error? args/result) => identity)
             ((lookup name (current-system))
              => (lambda (f)
                   (let ((args (map result/expr-expr args/result))
                         (gs (get-guards f))
                         (vars (get-variables f))
                         (form (defined-function-app-form f)))
                     (define (guard-ok? vars form g)
                       (let ((result (eval (apply-rule '()
                                                       (rule vars '() form g)
                                                       `(,name ,@args)
                                                       '()))))
                         (if (result/error? result)
                             result
                             (expr-unquote (result/expr-expr result)))))
                     (if (every (lambda (g) (guard-ok? vars form g)) gs)
                         (eval (rewrite1 `(,name ,@args)
                                         `(rewrite () ,name)))
                         (result/error 'guard-error `(,name ,@args) `(and ,@gs))))))
             (else (result/error 'function-not-found name)))))
         ((if-form? expr)
          (let ((test/result (eval (result/expr (if-form-test expr)))))
            (if (result/error? test/result)
                test/result
                (if (equal? (result/expr-expr test/result)
                            (false))
                    (eval (result/expr (if-form-else expr)))
                    (eval (result/expr (if-form-then expr)))))))
         ((variable? expr)
          (result/error 'eval 'variable-found expr))
         (else
          (result/error 'eval 'invalid-expression expr)))))
     (else (result/error 'eval 'invalid-result result)))))

(define (rewriter? x)
  (match x
    (('rewrite path command-name command-ops ...)
     (and (path? path)
          (command-name? command-name)
          (every command-option? command-ops)))
    (('eval path) (path? path))
    #;
    (('induction path (fname vars ...))
     (and (path? path)
          (symbol? fname)
          (every variable? vars)))
    (else #f)))

(define (sequence? x)
  (and (list? x)
       (every rewriter? x)))

(define (path? x)
  (and (list? x)
       (every natural? x)))

(define (command-name? x) #t)

(define (command-option? x)
  (and (pair? x)
       (case (car x)
         ((=) (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 (sys system?) (expr (const #t)))
  (parameterize ((current-system sys))
    (rewrite/eval (convert-to-expression expr))))

(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 preconds builder)
                (extract (cdr path) (list-ref expr i) fail)
              (values extracted-expr
                      (case i
                        ((1) preconds)
                        ((2) (cons (prop-not (prop-not precond))
                                   preconds))
                        ((3) (cons (prop-not precond) 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 (get-variables x)
              (list)
              (defined-function-app-form x)
              (get-expression x))
        (rule (get-variables x)
              (list)
              (get-expression x)
              (defined-function-app-form x))))

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

(define (parse-options/theorem ops fail)
  (if (null? ops)
      (values '())
      (receive (env)
          (parse-options/theorem (cdr ops) fail)
        (case (caar ops)
          ((=)
           (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-name cmd-ops thm preconds expr)
  (call/cc
   (lambda (k)
     (define (fail . args)
       (k (apply result/error args)))
     (receive (env)
         (parse-options/theorem cmd-ops fail)
       (cond
        ((any (cut apply-rule preconds <> expr env)
              (theorem-rules thm)) => result/expr)
        (else
         (result/error 'apply-theorem cmd-name expr)))))))

(define (rewrite/core-function f expr)
  (if (and (app-form? expr)
           (eq? (get-name f) (app-form-name expr))
           (= (length (get-variables f)) (length (app-form-args expr)))
           (every expr-quoted? (app-form-args expr)))
      (result/expr
       (expr-quote (apply (get-procedure f)
                          (map expr-unquote (app-form-args expr)))))
      (result/error 'apply-core-function (get-name f) expr)))

(define (rewrite/function fname f expr)
  (cond
   ((any (cut apply-rule '() <> expr '())
         (function->rules f))
    => result/expr)
   (else
    (result/error 'apply-function fname expr))))

(define (rewrite1 expr r)
  (call/cc
   (lambda (k)
     (define (fail . args)
       (k (apply result/error args)))
     (define (result->expr x)
       (cond
        ((result/error? x) (fail (cdr x)))
        (else
         (result/expr-expr x))))
     (match r
       (('eval path)
        (receive (extracted-expr preconds builder)
            (extract path expr fail)
          (result/expr
           (builder
            (result->expr (rewrite/eval extracted-expr))))))
       #;
       (('induction path (fname vars ...))
        (receive (extracted-expr preconds builder)
            (extract path expr fail)
          (result/expr
           (builder
            (result->expr
             (rewrite/induction sys fname vars preconds extracted-expr))))))
       (('rewrite path cmd-name cmd-ops ...)
        (receive (extracted-expr preconds builder)
            (extract path expr fail)
          (result/expr
           (builder
            (result->expr
             (cond
              ((lookup cmd-name (current-system))
               => (lambda (x)
                    (cond
                     ((is-a? x <core-function>)
                      (rewrite/core-function x extracted-expr))
                     ((is-a? x <theorem*>)
                      (rewrite/theorem cmd-name cmd-ops x preconds extracted-expr))
                     ((is-a? x <expandable-function>)
                      (rewrite/function cmd-name x extracted-expr))
                     (else
                      (result/error 'invalid-command cmd-name extracted-expr)))))
              (else (result/error 'command-not-found cmd-name extracted-expr))))))))))))

(define (rewrite expr seq)
  (let loop ((result (result/expr expr))
             (seq seq))
    (cond
     ((result/error? result) result)
     ((result/expr? result)
      (if (null? seq)
          result
          (loop (rewrite1 (result/expr-expr result)
                          (car seq))
                (cdr seq))))
     (else (result/error 'invalid-result result)))))

(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? (get-equal-symbol (current-system)) (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 current-system (make-parameter (make <system>)))
(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 (make <axiom>
                #:name 'name
                #:variables '(var ...)
                #:expression (convert-to-expression 'expr))))
       (current-system (add-definition t (current-system)))
       (validate t)
       t))))

(define-syntax define-theorem
  (syntax-rules ()
    ((_ name (var ...) expr)
     (match 'name
       (`(guard . ,_)
        (raise-exception (make-exception
                          (make-exception-with-origin "define-theorem")
                          (make-exception-with-message "invalid theorem name (guard _ ...)")
                          (make-exception-with-irritants 'name))))
       (else
        (let ((t (make <conjecture>
                   #:name 'name
                   #:variables '(var ...)
                   #:expression (convert-to-expression 'expr))))
          (current-system (add-definition t (current-system)))
          (validate t)
          t))))))

(define (add-guard-theorem name)
  (cond
   ((lookup name (current-system))
    => (lambda (f)
         (if (is-a? f <expandable-function>)
             (add-definition (make <conjecture>
                               #:name `(guard ,name)
                               #:variables (get-variables f)
                               #:expression (fold smart-implies
                                                  (make-guard-claim
                                                   (get-expression f))
                                                  (get-guards f)))
                             (current-system))
             (raise-exception
              (make-exception
               (make-exception-with-origin 'define-guard-theorem)
               (make-exception-with-message "not expandable function")
               (make-exception-with-irritants name))))))
   (else
    (raise-exception
              (make-exception
               (make-exception-with-origin 'define-guard-theorem)
               (make-exception-with-message "not found")
               (make-exception-with-irritants name))))))

(define-syntax define-guard-theorem
  (syntax-rules ()
    ((_ name)
     (current-system (add-guard-theorem 'name)))))

(define-syntax define-core-function/guard
  (syntax-rules (and)
    ((_ name (var ...) (and guard ...) proc)
     (let ((f (make <core-function>
                #:name 'name
                #:variables '(var ...)
                #:guards (map convert-to-expression (list 'guard ...))
                #:procedure proc)))
       (current-system (add-definition f (current-system)))
       (validate f)
       f))
    ((_ name (var ...) guard proc)
     (define-core-function/guard name (var ...) (and guard) proc))))

(define-syntax define-core-function
  (syntax-rules ()
    ((_ name (var ...) proc)
     (define-core-function/guard name (var ...) (and) proc))))

(define (recursive? f)
  (member (get-name f) (expression-functions (get-expression f))))

(define-syntax define-function/guard
  (syntax-rules (and)
    ((_ name (var ...) (and guard-expr ...) expr)
     (let* ((expression (convert-to-expression 'expr))
            (guard-expressions (map convert-to-expression
                                    (list 'guard-expr ...)))
            (f (make <function>
                 #:name 'name
                 #:variables '(var ...)
                 #:guards guard-expressions
                 #:expression expression
                 #:code (code 'expr))))
       (current-system (add-definition f (current-system)))
       (validate f)
       (when (not (recursive? f))
         (let ((g (make <total-function>
                    #:name (get-name f)
                    #:variables (get-variables f)
                    #:guards (get-guards f)
                    #:expression (get-expression f)
                    #:code (get-code f)
                    #:claim (true)
                    #:proof '())))
           (current-system (update-definition g (current-system)))
           (validate g)))
       ))
    ((_ name (var ...) guard expr)
     (define-function/guard name (var ...) (and guard) expr))))

(define-syntax define-function
  (syntax-rules ()
    ((_ name (var ...) expr)
     (define-function/guard name (var ...) (and) expr))))

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

(define-syntax admit
  (syntax-rules (and)
    ((_ name)
     (cond
      ((lookup 'name (current-system))
       => (lambda (d)
            (unless (or (is-a? d <conjecture>)
                        (is-a? d <function>))
              (raise-exception
               (make-exception
                (make-exception-with-origin 'name)
                (make-exception-with-message "not provable definition")
                (make-exception-with-irritants 'name))))
            (let ((g (if (is-a? d <conjecture>)
                         (make <admitted-theorem>
                           #:name (get-name d)
                           #:variables (get-variables d)
                           #:expression (get-expression d)
                           #:claim (true)
                           #:proof '())
                         (make <admitted-function>
                           #:name (get-name d)
                           #:variables (get-variables d)
                           #:guards (get-guards d)
                           #:expression (get-expression d)
                           #:code (get-code d)
                           #:claim (true)
                           #:proof '()))))
              (validate g)
              (current-system (update-definition g (current-system))))))
      (else
       (raise-exception
        (make-exception
         (make-exception-with-origin 'name)
         (make-exception-with-message "not found")
         (make-exception-with-irritants 'name))))))))

(define (core-system)
  (parameterize ((current-system (make <system>)))
    (define-syntax-rules and ()
      ((and) '#t)
      ((and x) x)
      ((and x . xs) (if x (and . xs) #f)))
    (define-core-function not (x) not)
    (define-core-function equal? (x y) equal?)
    (current-system)))

(define (core-system/equal-t-nil)
  (parameterize ((current-system (make <system>
                                   #:equal-symbol 'equal
                                   #:true-object ''t
                                   #:false-object ''nil)))
    (define-syntax-rules and ()
      ((and) 't)
      ((and x) x)
      ((and x . xs) (if x (and . xs) 'nil)))
    (define-core-function equal (x y) (lambda (x y)
                                        (if (equal? x y)
                                            't
                                            'nil)))
    (define-core-function not (x)
      (lambda (x)
        (if (eq? x 'nil)
            't
            'nil)))
    (current-system)))

(define-syntax define-system
  (syntax-rules ()
    ((_ name (system) expr ...)
     (begin
       (define (name)
         (when (equal? 'name 'system)
           (raise-exception
            (make-exception
             (make-exception-with-origin 'name)
             (make-exception-with-message "recursive system")
             (make-exception-with-irritants 'system))))
         (parameterize
             ((current-system (system)))
           expr
           ...
           (current-system)))
       (let ((result (system-check (name))))
         (unless (null? result)
           (pretty-print result)))))))

(define (validate-function-name desc name)
  (define (err)
    (raise-exception
     (make-exception
      (make-exception-with-origin 'desc)
      (make-exception-with-message "unbound function")
      (make-exception-with-irritants name))))
  (cond
   ((lookup name (current-system))
    => (lambda (f)
         (if (is-a? f <function*>)
             name
             (err))))
   (else (err))))

(define-syntax set-measure-predicate
  (syntax-rules ()
    ((_ name)
     (begin
       (validate-function-name 'set-measure-predicate 'name)
       (current-system (update-measure-predicate 'name (current-system)))))))

(define-syntax set-measure-less-than
  (syntax-rules ()
    ((_ name)
     (begin
       (validate-function-name 'set-measure-less-than 'name)
       (current-system
        (update-measure-less-than 'name (current-system)))))))

(define (defined-function-app-form f)
  (app-form (get-name f) (get-variables f)))

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

(define (smart-if x y z)
  (cond
   ((equal? y z) y)
   ((equal? x (true)) y)
   ((equal? x (false)) z)
   (else `(if ,x ,y ,z))))

(define (smart-and . args)
  (cond
   ((null? args) (true))
   ((equal? (true) (car args)) (apply smart-and (cdr args)))
   (else
    (let ((rest (apply smart-and (cdr args))))
      (if (equal? (true) rest)
          (car args)
          (smart-if (car args)
                    rest
                    (false)))))))

(define (smart-implies x y)
  (cond
   ((equal? (false) x) (true))
   ((equal? (true) y) (true))
   (else
    (smart-if x y (true)))))

(define (make-totality-claim* m-expr f)
  (let* ((name (get-name f)))
    (define (convert app-form)
      (cond
       ((apply-rule '()
                    (rule (get-variables f)
                          '()
                          (defined-function-app-form f)
                          m-expr)
                    app-form
                    '())
        => identity)
       (else (error "make-totality-claim: convert error"
                    (get-name f)
                    m-expr
                    app-form))))
    (smart-if `(,(get-measure-predicate (current-system)) ,m-expr)
              (let loop ((expr (get-expression f)))
                (cond
                 ((expr-quoted? expr) (true))
                 ((variable? expr) (true))
                 ((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))))
                    (smart-and test/result
                               (smart-if (if-form-test expr)
                                         then/result
                                         else/result))))
                 ((app-form? expr)
                  (let ((rest
                         (let f ((args (app-form-args expr)))
                           (cond ((null? args) (true))
                                 ((single? args) (loop (car args)))
                                 (else (smart-and (loop (car args))
                                                  (f (cdr args))))))))
                    (if (eq? name (app-form-name expr))
                        (smart-and `(,(get-measure-less-than (current-system))
                                     ,(convert expr)
                                     ,m-expr)
                                   rest)
                        rest)))
                 (else (error "(vikalpa) make-totality-claim: error"
                              (get-name f)
                              m-expr))))
              (false))))

(define (make-guard-claim expr)
  (define (find-preconds expr)
    (cond
     ((app-form? expr)
      (let ((rest (append-map find-preconds (cdr expr))))
        (append (cond ((lookup (car expr) (current-system)) =>
                       (lambda (f)
                         (let ((preconds (get-guards f)))
                           (map (lambda (precond)
                                  (substitute (map cons
                                                   (get-variables f)
                                                   (cdr expr))
                                              precond))
                                preconds))))
                      (else (error "make-guard-claim: error" (car expr))))
                rest)))
     ((if-form? expr)
      (find-preconds (if-form-test expr)))
     (else '())))
  (define (build/find-if expr)
    (cond
     ((if-form? expr)
      (smart-if (build/find-if (if-form-test expr))
                (build (if-form-then expr))
                (build (if-form-else expr))))
     ((app-form? expr)
      (apply smart-and (map build/find-if (app-form-args expr))))
     (else (true))))
  (define (build expr)
    (cond
     ((if-form? expr)
      (apply smart-and
             (append (find-preconds (if-form-test expr))
                     (list (smart-if (if-form-test expr)
                                     (build (if-form-then expr))
                                     (build (if-form-else expr)))))))
     ((app-form? expr)
      (apply smart-and
             (append (find-preconds expr)
                     (list (build/find-if expr)))))
     (else (true))))
  (build expr))

(define (make-induction-claim f vars c)
  (unless (is-a? f <expandable-function>)
    (raise-exception
     (make-exception
      (make-exception-with-origin 'define-proof)
      (make-exception-with-message
       "measure function must be expandable function")
      (make-exception-with-irritants (get-name f)))))
  (define (find-app-forms expr)
    (cond
     ((app-form? expr)
      (let ((rest (append-map find-app-forms (cdr expr))))
        (if (eq? (get-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 form)
    (cond
     ((apply-rule '()
                  (rule vars
                        '()
                        (app-form (get-name f) vars)
                        c)
                  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))))
               (smart-implies (if (null? app-forms)
                                  (true)
                                  (fold smart-implies
                                        c
                                        (map prop app-forms)))
                              (smart-if (if-form-test expr)
                                        (build (if-form-then expr))
                                        (build (if-form-else expr))))))
            (else
             (let ((app-forms (find-app-forms expr)))
               (fold smart-implies c (map prop app-forms))))))))
   (else (error "make-induction-claim: invalid"
                f vars c))))

(define (validate-sequence d seq)
  (for-each (lambda (r)
              (match r
                (('rewrite _ _ . command-ops)
                 (for-each (lambda (x)
                             (match x
                               (('= var expr)
                                (validate-expression 
                                                     `(define-proof ,(get-name d))
                                                     (get-variables d)
                                                     expr))
                               (else #f)))
                           command-ops))
                (else #f)))
            seq))

(define (add-proof/function f seed seq)
  (define (update-claim claim)
    (update-definition (make <total-function>
                         #:name (get-name f)
                         #:variables (get-variables f)
                         #:guards (get-guards f)
                         #:expression (get-expression f)
                         #:code (get-code f)
                         #:claim claim
                         #:proof seq)
                       (current-system)))
  (validate-sequence f seq)
  (if seed
      (begin
        (validate-expression `(defien-proof ,(get-name f))
                             (get-variables f)
                             seed)
        (update-claim
         (fold smart-implies
               (make-totality-claim* seed f)
               (get-guards f))))
      (raise-exception
       (make-exception
        (make-exception-with-origin 'define-proof)
        (make-exception-with-message "need measure expression")
        (make-exception-with-irritants (get-expression f))))))

(define (add-proof/theorem t seed seq)
  (define (seed-error m)
    (raise-exception
     (make-exception
      (make-exception-with-origin 'define-proof)
      (make-exception-with-message (string-append "invalid seed: " m))
      (make-exception-with-irritants (list (get-name t) seed)))))
  (validate-sequence t seq)
  (let ((claim
         (if seed
             (match seed
               ((fname vars ...)
                (cond
                 ((lookup fname (current-system))
                  => (cut make-induction-claim <> vars (get-expression t)))
                 (else (seed-error "function not found"))))
               (else (seed-error "format error")))
             (get-expression t))))
    (update-definition (make <theorem>
                         #:name (get-name t)
                         #:variables (get-variables t)
                         #:expression (get-expression t)
                         #:claim claim
                         #:proof seq)
                       (current-system))))

(define (add-proof name seed seq)
  (cond
   ((not (sequence? seq))
    (raise-exception
     (make-exception
      (make-exception-with-origin 'define-proof)
      (make-exception-with-message "not sequence")
      (make-exception-with-irritants seq))))
   ((lookup name (current-system))
    => (lambda (def)
         (current-system
          (if (and (is-a? def <provable>)
                   (not (is-a? def <proved>)))
              (cond
               ((is-a? def <function>)
                (add-proof/function def seed seq))
               ((is-a? def <conjecture>)
                (add-proof/theorem def seed seq))
               (else
                (raise-exception
                 (make-exception
                  (make-exception-with-origin 'define-proof)
                  (make-exception-with-message "error")
                  (make-exception-with-irritants def)))))
              (raise-exception
               (make-exception
                (make-exception-with-origin 'define-proof)
                (make-exception-with-message "not provable definition")
                (make-exception-with-irritants def)))))))
   (else
    (raise-exception
     (make-exception
      (make-exception-with-origin 'define-proof)
      (make-exception-with-message "definition is not found")
      (make-exception-with-irritants name))))))

(define-syntax define-proof
  (syntax-rules ()
    ((_ name
        seed
        seq)
     (add-proof 'name
                'seed
                'seq))
    ((_ name seq)
     (define-proof name #f seq))))

(define (validate-expression/error name vars expr)
  (with-exception-handler
      (lambda (e)
        (if (eq? 'validate-expression/error (exception-origin e))
            `(error ,name ,vars ,expr))
        (raise-exception e))
    (lambda ()
      (validate-expression 'validate-expression/error vars expr)
      #f)))

(define (validate-expression name vars expr)
  (let* ((expr-fnames (expression-functions expr))
         (expr-vars (expression-vars expr))
         (expr-app-forms (expression-app-forms expr)))
    (define (err msg x)
      (raise-exception
       (make-exception
        (make-exception-with-origin name)
        (make-exception-with-message msg)
        (make-exception-with-irritants x))))
    (for-each (lambda (x)
                (when (member x expr-fnames)
                  (err "invalid variable" x)))
              vars)
    (for-each (lambda (fname)
                (unless (cond
                         ((lookup fname (current-system)) =>
                          (lambda (f)
                            (for-each
                             (lambda (app-form)
                               (when (equal? fname (app-form-name app-form))
                                 (unless (= (length (get-variables f))
                                            (length (app-form-args app-form)))
                                   (err (format
                                         #f
                                         "~a :wrong number of arguments ~s"
                                         (get-name f)
                                         (get-variables f))
                                        (app-form-args app-form)))))
                             expr-app-forms)
                            #t))
                         (else #f))
                  (err "undefined function" fname)))
              expr-fnames)
    (for-each (lambda (x)
                (unless (member x vars)
                  (err "undefined variable" x)))
              expr-vars)))

(define (dup? xs)
  (if (null? xs)
      #f
      (if (member (car xs) (cdr xs))
          #t
          (dup? (cdr xs)))))

(define (validate-vars desc vars)
  (define (err)
    (raise-exception
     (make-exception
      (make-exception-with-message
       (string-append "(vikalpa) " desc ": duplicated variable"))
      (make-exception-with-irritants vars))))
  (when (dup? vars)
    (err)))

(define-method (get-type (s <axiom>)) 'axiom)
(define-method (get-type (s <theorem>)) 'theorem)
(define-method (get-type (s <conjecture>)) 'conjecture)
(define-method (get-type (s <core-function>)) 'core-function)
(define-method (get-type (s <function>)) 'function)
(define-method (get-type (s <total-function>)) 'total-function)
(define-method (get-type (s <admitted-function>)) 'admitted-function)
(define-method (get-type (s <admitted-theorem>)) 'admitted-theorem)
(define-method (get-type (s <macro>)) 'macro)

(define-method (show (d <macro>))
  (list (get-type d)))
(define-method (show (d <theorem*>))
  (list (get-type d)
        (get-variables d)
        (get-expression d)))
(define-method (show (d <core-function>))
  (list (get-type d)
        (get-variables d)))
(define-method (show (d <expandable-function>))
  (list (get-type d)
        (get-variables d)
        (get-expression d)))
(define-method (show (d <admitted-function>))
  (list (get-type d)
        (get-variables d)
        (get-expression d)))

(define* (system-apropos sys str)
  (pretty-print
   (filter-map (lambda (d)
                 (let ((name (format #f "~a" (get-name d))))
                   (if (string-match (string-append ".*"
                                                    (regexp-quote str)
                                                    ".*")
                                     name)
                       (list (get-name d) (show d))
                       #f)))
               (get-definitions sys))))

(define (system-check/guard)
  (filter-map (lambda (f)
                (if (lookup `(guard ,(get-name f)) (current-system))
                    #f
                    (if (equal? (make-guard-claim (get-expression f))
                                (true))
                        #f
                        `((guard ,(get-name f))
                          (add (define-guard-theorem ,(get-name f)))))))
              (filter (cut is-a? <> <expandable-function>)
                      (get-definitions (current-system)))))

(define (system-check sys)
  (append
   (parameterize ((current-system sys))
     (system-check/guard))
   (let loop ((sys sys)
              (fails '()))
     (if (system-empty? sys)
         fails
         (let ((d (first-definition sys))
               (sys-without-first (remove-first-definition sys)))
           (define* (next #:optional fail)
             (loop sys-without-first
                   (if fail
                       (cons fail fails)
                       fails)))
           (cond
            ((is-a? d <proved>)
             (let ((result
                    (if (is-a? d <theorem>)
                        (parameterize ((current-system sys-without-first))
                          (rewrite (get-claim d)
                                   (get-proof d)))
                        (parameterize ((current-system sys))
                          (rewrite (get-claim d)
                                   (get-proof d))))))
               (cond
                ((equal? result
                         (parameterize ((current-system sys))
                           (result/expr (true))))
                 (next))
                (else
                 (next (list (get-name d) result))))))
            ((is-a? d <provable>)
             (next (list (get-name d))))
            (else (next))))))))

(define (system? x)
  (is-a? x <system>))

(define/guard (system-lookup (sys system?) (name (const #t)))
  (cond
   ((lookup name sys) => show)
   (else #f)))

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