;; The first three lines of this file were inserted by DrScheme. ;; They record information about the language level. #reader(lib "plai-pretty-big-reader.ss" "plai")((modname tinfer-support) (read-case-sensitive #t) (teachpacks ())) (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-id symbol?) (bound-body Expr?) (body Expr?)] [rec-with (bound-id symbol?) (bound-body Expr?) (body Expr?)] [fun (arg-id 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?)]) (define-type Type [t-num] [t-bool] [t-list (elem Type?)] [t-fun (arg Type?) (result Type?)] [t-var (v symbol?)]) ; parse :: S-exp -> Expr #;(define parse ...) ; generate-constraints :: #;(define generate-constraints ...) ; unify :: #;(define unify ...) ; infer-type :: Expr -> Type #;(define infer-type ...) ; 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 war-grading. So, you are free to modify this function as you see fit. (define ((type=? t1) t2) (local ([define ht1 (make-hash-table)] ; maps vars in t1 to vars in t2 [define ht2 (make-hash-table)] ; 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-table-get ht1 (t-var-v t1) (lambda () ; if t1 doesn't map to anything, it's the first time ; we're seeing it, so map it to t2 (hash-table-put! ht1 (t-var-v t1) (t-var-v t2)) (t-var-v t2)))] [define v2 (hash-table-get ht2 (t-var-v t2) (lambda () (hash-table-put! ht2 (t-var-v t2) (t-var-v t1)) (t-var-v 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-v t2) v1) (symbol=? (t-var-v t1) v2)))] [(and (Type? t1) (Type? t2)) false] [else (error 'type=? "either ~a or ~a is not a Type" t1 t2)])]) (or (teq? t1 t2) ; Unfortunately, test/pred simply prints false; this helps us see ; what t2 was. (error 'type=? "~s and ~a are not equal (modulo renaming)" 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")