;;; $Id: lambda-1-exp.scm,v 1.3 2005/02/17 16:29:22 leavens Exp $
;;; An ADT for the untyped 1-argument lambda calculus without constants

;;; Grammar:
;;;  <expression> ::=
;;;       <identifier>                               "var-exp (id)"
;;;     | ( lambda ( <identifier> ) <expression> )   "lambda-exp (id body)"
;;;     | ( <expression> <expression> )              "app-exp (rator rand)"

(module lambda-1-exp (lib "typedscm.ss" "lib342")

(provide lambda-1-exp? var-exp? lambda-exp? app-exp?
	 var-exp->id lambda-exp->id lambda-exp->body
	 app-exp->rator app-exp->rand
	 var-exp lambda-exp app-exp
	 parse-lambda-1-exp)

;; type predicate
(deftype lambda-1-exp? (type-predicate-for lambda-1-exp))

;; case testers (discriminators)
(deftype var-exp? (-> (lambda-1-exp) boolean))
(deftype lambda-exp? (-> (lambda-1-exp) boolean))
(deftype app-exp? (-> (lambda-1-exp) boolean))

;; observers 
(deftype var-exp->id (-> (lambda-1-exp) symbol))
(deftype lambda-exp->id (-> (lambda-1-exp) symbol))
(deftype lambda-exp->body (-> (lambda-1-exp) lambda-1-exp))
(deftype app-exp->rator (-> (lambda-1-exp) lambda-1-exp))
(deftype app-exp->rand (-> (lambda-1-exp) lambda-1-exp))

;; constructors
(deftype var-exp (-> (symbol) lambda-1-exp))
(deftype lambda-exp (-> (symbol lambda-1-exp) lambda-1-exp))
(deftype app-exp (-> (lambda-1-exp lambda-1-exp) lambda-1-exp))

;; parsing/bless input correctness
(deftype parse-lambda-1-exp (-> (datum) lambda-1-exp))

(defrep (lambda-1-exp datum))

(define lambda-1-exp?
  (lambda (exp)
    ;; ENSURES: result is true just when d represents a lambda-1-exp
    (has-type-trusted
      boolean
      (or (var-exp? exp)
	  (and (lambda-exp? exp) 
	       (lambda-1-exp? (lambda-exp->body exp)))
	  (and (app-exp? exp)
	       (lambda-1-exp? (app-exp->rator exp))
	       (lambda-1-exp? (app-exp->rand exp)))))))

(define var-exp?
  (lambda (exp)
    ;; ENSURES: result is true just when exp represents a var-exp
    (symbol? exp)))

(define lambda-exp?
  (lambda (exp)
    ;; ENSURES: result is true just when exp represents a lambda-exp
    (has-type-trusted
      boolean
      (and (list? exp)
	   (= (length exp) 3)
	   (eq? (car exp) 'lambda)
	   (let ((formals (cadr exp)))
	     (and (list? formals)
		  (= 1 (length formals))
		  (symbol? (car formals))))))))

(define app-exp?
  (lambda (exp)
    ;; ENSURES: result is true just when exp represents an app-exp
    (and (list? exp)
	 (= (length exp) 2))))

(define var-exp->id
  (lambda (vr)
    ;; REQUIRES: vr represents a var-exp
    ;; ENSURES: result is the symbol represented by vr
    (if (var-exp? vr)
	vr
	(error "var-exp->id: not a var-exp:" vr))))

(define lambda-exp->id
  (lambda (lm)
    ;; REQUIRES: lm represents a lambda-exp
    ;; ENSURES: result is the formal in the representation of lm
    (if (lambda-exp? lm)
	(caadr lm)
	(error "lambda-exp->id: not a lambda-exp:" lm))))

(define lambda-exp->body
  (lambda (lm)
    ;; REQUIRES: lm represents a lambda-exp
    ;; ENSURES: result is the body in the representation of lm
    (if (lambda-exp? lm)
	(caddr lm)
	(error "lambda-exp->body: not a lambda-exp:" lm))))

(define app-exp->rator
  (lambda (ap)
    ;; REQUIRES: ap represents an app-exp
    ;; ENSURES: result is the operator in the representation of ap
    (if (app-exp? ap)
	(car ap)
	(error "app-exp->rator: not an app-exp:" ap))))

(define app-exp->rand
  (lambda (ap)
    ;; REQUIRES: ap represents an app-exp
    ;; ENSURES: result is the operand in the representation of ap
    (if (app-exp? ap)
	(cadr ap)
	(error "app-exp->rand: not an app-exp:" ap))))

(define var-exp
  (lambda (id)
    ;; ENSURES: result is a representation of a var-exp with symbol id
    id))

(define lambda-exp
  (lambda (id body)
    ;; ENSURES: result is a representation of a lambda-exp with formal id
    ;;          and body body
    (list 'lambda (list id) body)))

(define app-exp
  (lambda (rator rand)
    ;; ENSURES: result is a representation of an app-exp with operator rator
    ;;          and operand rand
    (list rator rand)))
  
(define parse-lambda-1-exp
  (lambda (exp)
    ;; ENSURES: if exp has the syntax of a lambda-1-exp,
    ;;          then result is the representation of exp as a lambda-1-exp,
    ;;          otherwise an error message is given.
    (has-type-trusted
      lambda-1-exp
      (cond
       ((symbol? exp) (var-exp exp))
       ((lambda-exp? exp)
	(lambda-exp (caadr exp)
		    (parse-lambda-1-exp (caddr exp))))
       ((app-exp? exp)
	(app-exp (parse-lambda-1-exp (car exp))
		 (parse-lambda-1-exp (cadr exp))))
       (else (error "parse-lambda-1-exp: bad syntax for expression: " exp))))))

) ; end module