; -*- Lisp -*-
; lambda-calculus: an EuLisp library that implements pure lambda calculus
; Copyright (c) 2001 Ian Hickson <ian@hixie.ch>
;
; This program 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 2 of the License, or
; (at your option) any later version.
;
; This program 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 this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

(defmodule lambda-calculus
  (import (level0 utilities))

  ;;; classes

  ; the lambda term superclass
  (defclass <lambda-term> ()
    () ; our superclass has no slots
    abstractp: t
    )

  ; variables (x)
  (defclass <variable> (<lambda-term>)
    ((name 
      keyword: name:
      reader: name
      writer: alpha-rename
      requiredp: t))
    predicate: variablep
    constructor: (variable name:))

  ; applications (MN)
  (defclass <application> (<lambda-term>)
    ((M 
      keyword: M:
      reader: M
      requiredp: t)
     (N 
      keyword: N:
      reader: N
      requiredp: t))
    predicate: applicationp
    constructor: (application M: N:))

  ; abstractions (Lx.M)
  (defclass <abstraction> (<lambda-term>)
    ((parameter
      keyword: parameter:
      reader: parameter
      requiredp: t)
     (body
      keyword: body:
      reader: body
      requiredp: t))
    predicate: abstractionp
    constructor: (abstraction parameter: body:))


  ;;; methods

  ;; the generic declarations
  (defgeneric substitute ((term <lambda-term>) (search <variable>) (replace <lambda-term>)))
  (defgeneric beta-reduce-step ((term <lambda-term>)))
  (defgeneric beta-reduced-p ((term <lambda-term>)))
  (defgeneric recurse-variables ((term <lambda-term>) function bound-variables))
  (defgeneric get-clashing-bound-variables-internal ((term <lambda-term>) bound-variables))
  (defgeneric get-free-variables-internal ((term <lambda-term>) bound-variables))
  (defgeneric clean-name-clashes ((term <lambda-term>)))


  ;; some default implementations
  (defmethod beta-reduce-step ((term <lambda-term>))
    term)

  (defmethod beta-reduced-p ((term <lambda-term>))
    t) ; by default lambda terms are considered to be in their reduced form

  (defmethod get-clashing-bound-variables-internal ((term <lambda-term>) bound-variables)
    (recurse-variables term get-clashing-bound-variables-internal bound-variables))

  (defmethod get-free-variables-internal ((term <lambda-term>) bound-variables)
    (recurse-variables term get-free-variables-internal bound-variables))

  ; make lambda-terms pretty-printable
  (defmethod generic-prin ((object <lambda-term>) stream)
    (generic-prin (convert object <string>) stream))


  ;; high-level name clash management
  (let ((last-name 0))
    (defun unique-name ()
      (concatenate "v" (convert (setq last-name (+ last-name 1)) <string>))))

  (defun rename (variable)
    (alpha-rename variable (unique-name)))

  (defun rename-variables (variables)
    (if (eq variables ()) ()
      ; XXX In euscheme order of evaluation is right-to-left (this is
      ; in violation of the EuLisp spec, where function calls evaluate
      ; arguments left-to-right), so we evaluate old-name first and
      ; then change, before calling ourselves again. If we don't do
      ; that, the order of renamings is such that the numbers of
      ; backwards, which looks very odd.
      (let* ((old-name (name (car variables)))
             (change (cons old-name (rename (car variables)))))
        (cons change (rename-variables (cdr variables))))))

  ; returns a list of pairs of old names to new names
  (defmethod clean-name-clashes ((term <lambda-term>))
    (rename-variables (get-clashing-bound-variables-internal term ()))) 


  ;; wrapper routines
  (defun beta-reduce (term)
    (thread-reschedule) ; yield
    (if (beta-reduced-p term)
        term
      (beta-reduce (beta-reduce-step term))))

  (defun get-clashing-bound-variables (term)
    (remove-duplicates (get-clashing-bound-variables term ())))

  (defun get-free-variables (term)
    (remove-duplicates (reverse (get-free-variables-internal term ()))))


  ;; variables
  (defmethod substitute ((term <variable>) (search <variable>) (replace <lambda-term>))
    (if (eq term search) replace term))

  (defmethod (converter <string>) ((instance <variable>))
    (convert (name instance) <string>)) ; (name instance) can be a <character> (as opposed to a <string>)

  (defmethod deep-copy ((object <variable>))
    (variable (name object)))

  (defun variable-has-name (candidate-variable search-name)
    (equal (name candidate-variable) search-name))

  (defmethod get-clashing-bound-variables-internal ((term <variable>) bound-variables)
    (if (eq bound-variables ()) ()
      (if (and (not (eq term (car bound-variables))) ; can't clash with yourself!
               (variable-has-name term (name (car bound-variables))))
          ; ok, we have clashed
          (cons (car bound-variables)
                (get-clashing-bound-variables-internal term (cdr bound-variables)))
        (get-clashing-bound-variables-internal term (cdr bound-variables)))))

  (defmethod get-free-variables-internal ((term <variable>) bound-variables)
    (if (eq bound-variables ())
        (list term) ; sweet, we're free!
      (if (eq (car bound-variables) term)
          () ; we're bound :-|
        (get-free-variables-internal term (cdr bound-variables)))))


  ;; applications
  (defmethod substitute ((term <application>) (search <variable>) (replace <lambda-term>))
    (application (substitute (M term) search replace) (substitute (N term) search replace)))

  ; beta reduction of applications explicitly knows about abstractions
  ; and how to apply stuff to them. This is a little suboptimal --
  ; ideally I would make any term know how to "apply" itself and have
  ; another method to determine whether this was possible. However,
  ; that is a lot of overhead considering it can be simply made
  ; explicit here. So for now, let's do it the quick way. XXX
  
  (defmethod beta-reduce-step ((term <application>))
    (cond ((not (beta-reduced-p (M term))) (application (beta-reduce-step (M term)) (N term)))
          ((abstractionp (M term)) (substitute (body (M term)) (parameter (M term)) (N term)))
          ((not (beta-reduced-p (N term))) (application (M term) (beta-reduce-step (N term))))
          (t term)))

  (defmethod beta-reduced-p ((term <application>))
    (and (beta-reduced-p (M term))
         (not (abstractionp (M term)))
         (beta-reduced-p (N term))))

  (defmethod (converter <string>) ((instance <application>))
    (concatenate (cond
                  ((abstractionp (M instance)) (concatenate "(" (convert (M instance) <string>) ")"))
                  (t (convert (M instance) <string>)))
                 (cond
                  ((applicationp (N instance)) (concatenate "(" (convert (N instance) <string>) ")"))
                  ((abstractionp (N instance)) (concatenate "(" (convert (N instance) <string>) ")"))
                  (t (convert (N instance) <string>)))))

  (defmethod deep-copy ((object <application>))
    (application (deep-copy (M object)) (deep-copy (N object))))

  (defmethod recurse-variables ((term <application>) function bound-variables)
    (concatenate (function (M term) bound-variables) 
                 (function (N term) bound-variables)))


  ;; abstractions
  (defmethod substitute ((term <abstraction>) (search <variable>) (replace <lambda-term>))
    (abstraction (substitute (parameter term) search replace) (substitute (body term) search replace)))

  ; beta reduction of abstractions simply propagates to the body term
  (defmethod beta-reduce-step ((term <abstraction>))
    (abstraction (parameter term) (beta-reduce-step (body term))))

  (defmethod beta-reduced-p ((term <abstraction>))
    (beta-reduced-p (body term)))

  (defun stringifyBody (instance)
    (if (not (abstractionp (body instance)))
        (concatenate (convert (parameter instance) <string>) "." (convert (body instance) <string>))
      (concatenate (convert (parameter instance) <string>) (stringifyBody (body instance)))))

  (defmethod (converter <string>) ((instance <abstraction>))
    (concatenate "L" (stringifyBody instance)))

  (defmethod deep-copy ((object <abstraction>))
    (application (deep-copy (parameter object)) (deep-copy (body object))))

  (defmethod recurse-variables ((term <abstraction>) function bound-variables)
    (function (body term) (cons (parameter term) bound-variables)))


  ;; export the important classes and methods
  (export variable ; takes an opaque string to use as the variable name
          variablep ; is the argument a variable?
          application ; takes two lambda terms
          applicationp ; is the argument an application?
          abstraction ; takes a variable and a lambda term
          abstractionp ; is the argument an a
          alpha-rename ; takes variable, new name
          variable-has-name ; takes variable and name and returns true if they match
          substitute ; takes lambda term, variable to replace, lambda term to replace it with
          beta-reduce ; reduce a term as far as it will go (may not return)
          beta-reduce-step ; reduce a term once
          clean-name-clashes ; takes lambda term and renames any clashing bound variables with names of the form v<number> (e.g., v34)
          get-free-variables) ; returns a list of the free variables in the argument (a lambda term)
)