#lang planet plai/plai
;; You need the PLAI language installed before you can run this.
;; To get it, evaluate the following expression with your PLT interpreter:
;; (require (planet plai/plai))

(define-type TRCFWAE
  [num (n number?)]
  [add (lhs TRCFWAE?) (rhs TRCFWAE?)]
  [with (name symbol?) (named-expr TRCFWAE?) (body TRCFWAE?)]
  [id (name symbol?)]
  [fun (arg-id symbol?) (arg-type Type?) (result-type Type?) (body TRCFWAE?)]
  [app (fun-expr TRCFWAE?) (arg-expr TRCFWAE?)]
  [bool (b symbol?)]
  [if-true (c TRCFWAE?) (t TRCFWAE?) (e TRCFWAE?)]
  [rec (name symbol?) (fun-type t-fun?) (named-expr TRCFWAE?) (body TRCFWAE?)])

(define-type Type
  [t-num]
  [t-bool]
  [t-fun (arg Type?) (result Type?)])

;; type=? : Type Type -> boolean
(define (type=? t1 t2)
  (error "not implemented"))

;; parse-type : s-expression -> Type
(define (parse-type t-expr)
  (error "not implemented"))

;; parse : s-expression -> TRCFWAE
(define (parse sexp)
  (error "not implemented"))

;; type-of : TRCFWAE -> Type
(define (type-of expr)
  (error "not implemented"))
