;; The first three lines of this file were inserted by DrScheme. They record metadata
;; about the language level of this file in a form that our tools can easily process.
#reader(lib "reader.ss" "plai" "lang")
;; Group members: arjun aleks aoates apantel (fill in as appropriate)

(define-type Expr
  [num (n number?)]
  [id (v symbol?)]
  [bool (b boolean?)]
  [bin-num-op (op procedure?) (lhs Expr?) (rhs Expr?)]
  [iszero (e Expr?)]
  [bif (test Expr?) (then Expr?) (else Expr?)]
  [with (bound-name symbol?) (bound-body Expr?) (body Expr?)]
  [rec (bound-name symbol?) (bound-body Expr?) (body Expr?)]
  [fun (arg-name symbol?) (body Expr?)]
  [app (fun-expr Expr?) (arg-expr Expr?)]
  [tempty]
  [tcons (first Expr?) (rest Expr?)]
  [tfirst (e Expr?)]
  [trest (e Expr?)]
  [istempty (e Expr?)])

; parse :: S-exp -> Expr
#;(define (parse sexp)
  ...)

(define-type Type
  [t-num]
  [t-bool]
  [t-list (elem Type?)]
  [t-fun (arg Type?) (result Type?)]
  [t-var (name symbol?)])

; generate-constraints :: < you pick the contract >
#;(define generate-constraints
    ...)

; unify :: < you pick the contract >
#;(define unify
    ...)

; infer-type :: Expr -> Type
#;(define (infer-type expr)
    ...)

; type=? Type -> Type -> Bool
; signals an error if arguments are not variants of Type
; If you use this function in your test suite, include it with your test suite
; for the testfest.  So, you are free to modify this function as you see fit.
(define ((type=? t1) t2)
  (local ([define ht1 (make-hash)] ; maps vars in t1 to vars in t2
          [define ht2 (make-hash)] ; vice versa
          [define (teq? t1 t2)
            (cond
              [(and (t-num? t1) (t-num? t2)) true]
              [(and (t-bool? t1) (t-bool? t2)) true]
              [(and (t-list? t1) (t-list? t2))
               (teq? (t-list-elem t1) (t-list-elem t2))]
              [(and (t-fun? t1) (t-fun? t2))
               (and (teq? (t-fun-arg t1) (t-fun-arg t2))
                    (teq? (t-fun-result t1) (t-fun-result t2)))]
              [(and (t-var? t1) (t-var? t2))
               (local ([define v1 ; the symbol that ht1 says that t1 maps to
                         (hash-ref 
                          ht1 (t-var-name t1)
                          (lambda ()
                            ; if t1 doesn't map to anything, it's the first time
                            ; we're seeing it, so map it to t2
                            (hash-set! ht1 (t-var-name t1) (t-var-name t2))
                            (t-var-name t2)))]
                       [define v2
                         (hash-ref
                          ht2 (t-var-name t2)
                          (lambda ()
                            (hash-set! ht2 (t-var-name t2) (t-var-name t1))
                            (t-var-name t1)))])
                 ; we have to check both mappings, so that distinct variables
                 ; are kept distinct. i.e. a -> b should not be isomorphic to
                 ; c -> c under the one-way mapping a => c, b => c.
                 (and (symbol=? (t-var-name t2) v1) (symbol=? (t-var-name t1) v2)))]
              [(and (Type? t1) (Type? t2)) false]
              [else (error 'type=? "either ~a or ~a is not a Type" t1 t2)])])
    (teq? t1 t2)))


(test/pred (t-var 'a) 
           (type=? (t-var 'b)))
(test/pred (t-fun (t-var 'a) (t-var 'b)) 
           (type=? (t-fun (t-var (gensym)) (t-var (gensym)))))
(test/pred (t-fun (t-var 'a) (t-var 'b)) 
           (type=? (t-fun (t-var (gensym)) (t-var (gensym)))))
(test/pred (t-fun (t-var 'a) (t-var 'a)) ; fails
           (type=? (t-fun (t-var (gensym)) (t-var (gensym)))))
(test/pred (t-fun (t-var 'a) (t-var 'b)) ;fails
           (type=? (t-fun (t-var 'c) (t-var 'c))))
(test/exn ((type=? 34) 34) "not a Type")