;;; $Id: lambda-1-exp.scm,v 1.4 2006/01/05 22:24:09 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" "typedscm")

(provide expression? 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-expression)

;; type predicate
(deftype expression? (type-predicate-for expression))

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

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

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

;; parsing/bless input correctness
(deftype parse-expression (-> (datum) expression))

(defrep (expression datum))

(define expression?
  (lambda (exp)
    ;; ENSURES: result is true just when d represents a expression
    (has-type-trusted
      boolean
      (or (var-exp? exp)
          (and (lambda-exp? exp) 
               (expression? (lambda-exp->body exp)))
          (and (app-exp? exp)
               (expression? (app-exp->rator exp))
               (expression? (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
    (test-type
      boolean?
      (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)
        (test-type symbol? 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)
        (test-type symbol? (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)
        (test-type datum? (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)
        (test-type datum? (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)
        (test-type datum? (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
    (has-type datum id)))

(define lambda-exp
  (lambda (id body)
    ;; ENSURES: result is a representation of a lambda-exp with formal id
    ;;          and body body
    (has-type datum (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
    (has-type datum (list rator rand))))
  
(define parse-expression
  (lambda (exp)
    ;; ENSURES: if exp has the syntax of a expression,
    ;;          then result is the representation of exp as a expression,
    ;;          otherwise an error message is given.
    (test-type
      datum?
      (cond
       ((symbol? exp) (var-exp exp))
       ((lambda-exp? exp)
        (lambda-exp (caadr exp)
                    (parse-expression (caddr exp))))
       ((app-exp? exp)
        (app-exp (parse-expression (car exp))
                 (parse-expression (cadr exp))))
       (else (error "parse-expression: bad syntax for expression: " exp))))))

) ;; end module