Switch branches/tags
Nothing to show
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
476 lines (410 sloc) 20.2 KB
#lang eopl
;; Exercise 7.26 [★★] Extend the inferencer to handle EXPLICIT-REFS, as in exercise 7.10.
;; Grammar.
(define the-lexical-spec
'([whitespace (whitespace) skip]
[comment ("%" (arbno (not #\newline))) skip]
[identifier (letter (arbno (or letter digit "_" "-" "?"))) symbol]
[number (digit (arbno digit)) number]
[number ("-" digit (arbno digit)) number]))
(define the-grammar
'([program (expression) a-program]
[expression (number) const-exp]
[expression ("-" "(" expression "," expression ")") diff-exp]
[expression ("zero?" "(" expression ")") zero?-exp]
[expression ("if" expression "then" expression "else" expression) if-exp]
[expression (identifier) var-exp]
[expression ("let" identifier "=" expression "in" expression) let-exp]
[expression ("proc" "(" identifier ":" optional-type ")" expression) proc-exp]
[expression ("(" expression expression ")") call-exp]
[expression ("letrec" optional-type identifier "(" identifier ":" optional-type ")" "=" expression "in" expression)
[expression ("begin" expression (arbno ";" expression) "end") begin-exp]
[expression ("newref" "(" expression ")") newref-exp]
[expression ("deref" "(" expression ")") deref-exp]
[expression ("setref" "(" expression "," expression ")") setref-exp]
[optional-type ("?") no-type]
[optional-type (type) a-type]
[type ("int") int-type]
[type ("bool") bool-type]
[type ("(" type "->" type ")") proc-type]
[type ("refto" type) ref-type]
[type ("void") void-type]
[type ("%tvar-type" number) tvar-type]))
(sllgen:make-define-datatypes the-lexical-spec the-grammar)
(define scan&parse (sllgen:make-string-parser the-lexical-spec the-grammar))
(define proc-type?
(lambda (ty)
(cases type ty
[proc-type (t1 t2) #t]
[else #f])))
(define ref-type?
(lambda (ty)
(cases type ty
[ref-type (t1) #t]
[else #f])))
(define tvar-type?
(lambda (ty)
(cases type ty
[tvar-type (serial-number) #t]
[else #f])))
(define proc-type->arg-type
(lambda (ty)
(cases type ty
[proc-type (arg-type result-type) arg-type]
[else (eopl:error 'proc-type->arg-type "Not a proc type: ~s" ty)])))
(define proc-type->result-type
(lambda (ty)
(cases type ty
[proc-type (arg-type result-type) result-type]
[else (eopl:error 'proc-type->result-types "Not a proc type: ~s" ty)])))
(define ref-type->base-type
(lambda (ty)
(cases type ty
[ref-type (ty1) ty1]
[else (eopl:error 'ref-type->base-type "Not a ref type: ~s" ty)])))
(define type-to-external-form
(lambda (ty)
(cases type ty
[int-type () 'int]
[bool-type () 'bool]
[proc-type (arg-type result-type) (list (type-to-external-form arg-type) '-> (type-to-external-form result-type))]
[ref-type (ty1) (list 'refto (type-to-external-form ty1))]
[void-type () 'void]
[tvar-type (serial-number) (string->symbol (string-append "tvar" (number->string serial-number)))])))
;; Data structures - expressed values.
(define-datatype proc proc?
[procedure [bvar symbol?]
[body expression?]
[env environment?]])
(define-datatype expval expval?
[num-val [value number?]]
[bool-val [boolean boolean?]]
[proc-val [proc proc?]]
[ref-val [ref reference?]])
(define expval-extractor-error
(lambda (variant value)
(eopl:error 'expval-extractors "Looking for a ~s, found ~s" variant value)))
(define expval->num
(lambda (v)
(cases expval v
[num-val (num) num]
[else (expval-extractor-error 'num v)])))
(define expval->bool
(lambda (v)
(cases expval v
[bool-val (bool) bool]
[else (expval-extractor-error 'bool v)])))
(define expval->proc
(lambda (v)
(cases expval v
[proc-val (proc) proc]
[else (expval-extractor-error 'proc v)])))
(define expval->ref
(lambda (v)
(cases expval v
[ref-val (ref) ref]
[else (expval-extractor-error 'ref v)])))
;; Data structures - environment.
(define-datatype environment environment?
[extend-env [bvar symbol?]
[bval expval?]
[saved-env environment?]]
[extend-env-rec [p-name symbol?]
[b-var symbol?]
[p-body expression?]
[saved-env environment?]])
(define apply-env
(lambda (env search-sym)
(cases environment env
[empty-env () (eopl:error 'apply-env "No binding for ~s" search-sym)]
[extend-env (bvar bval saved-env) (if (eqv? search-sym bvar)
(apply-env saved-env search-sym))]
[extend-env-rec (p-name b-var p-body saved-env) (if (eqv? search-sym p-name)
(proc-val (procedure b-var p-body env))
(apply-env saved-env search-sym))])))
;; Data structures - store.
(define the-store 'uninitialized)
(define empty-store
(lambda ()
(define initialize-store!
(lambda ()
(set! the-store (empty-store))))
(define reference?
(lambda (v)
(integer? v)))
(define newref
(lambda (val)
(let ([next-ref (length the-store)])
(set! the-store (append the-store (list val)))
(define deref
(lambda (ref)
(list-ref the-store ref)))
(define report-invalid-reference
(lambda (ref the-store)
(eopl:error 'setref "illegal reference ~s in store ~s" ref the-store)))
(define setref!
(lambda (ref val)
(set! the-store (letrec ([setref-inner (lambda (store1 ref1)
(cond [(null? store1) (report-invalid-reference ref the-store)]
[(zero? ref1) (cons val (cdr store1))]
[else (cons (car store1) (setref-inner (cdr store1) (- ref1 1)))]))])
(setref-inner the-store ref)))))
;; Data structures - type environment.
(define-datatype type-environment type-environment?
[extended-tenv-record [sym symbol?]
[type type?]
[tenv type-environment?]])
(define empty-tenv empty-tenv-record)
(define extend-tenv extended-tenv-record)
(define apply-tenv
(lambda (tenv sym)
(cases type-environment tenv
[empty-tenv-record () (eopl:error 'apply-tenv "Unbound variable ~s" sym)]
[extended-tenv-record (sym1 val1 old-env) (if (eqv? sym sym1)
(apply-tenv old-env sym))])))
;; Data structures - substitution.
(define pair-of
(lambda (pred1 pred2)
(lambda (val)
(and (pair? val) (pred1 (car val)) (pred2 (cdr val))))))
(define substitution?
(list-of (pair-of tvar-type? type?)))
(define empty-subst
(lambda ()
(define apply-one-subst
(lambda (ty0 tvar ty1)
(cases type ty0
[int-type () (int-type)]
[bool-type () (bool-type)]
[proc-type (arg-type result-type) (proc-type (apply-one-subst arg-type tvar ty1)
(apply-one-subst result-type tvar ty1))]
[ref-type (ty) (ref-type (apply-one-subst ty tvar ty1))]
[void-type () (void-type)]
[tvar-type (sn) (if (equal? ty0 tvar) ty1 ty0)])))
(define extend-subst
(lambda (subst tvar ty)
(cons (cons tvar ty)
(map (lambda (p)
(let ([oldlhs (car p)]
[oldrhs (cdr p)])
(cons oldlhs (apply-one-subst oldrhs tvar ty))))
(define apply-subst-to-type
(lambda (ty subst)
(cases type ty
[int-type () (int-type)]
[bool-type () (bool-type)]
[proc-type (t1 t2) (proc-type (apply-subst-to-type t1 subst) (apply-subst-to-type t2 subst))]
[ref-type (ty1) (ref-type (apply-subst-to-type ty1 subst))]
[void-type () (void-type)]
[tvar-type (sn) (let ([tmp (assoc ty subst)])
(if tmp
(cdr tmp)
;; Data structures - answer.
(define-datatype answer answer?
[an-answer [type type?]
[subst substitution?]])
;; Unifier.
(define no-occurrence?
(lambda (tvar ty)
(cases type ty
[int-type () #t]
[bool-type () #t]
[proc-type (arg-type result-type) (and (no-occurrence? tvar arg-type)
(no-occurrence? tvar result-type))]
[ref-type (ty1) (no-occurrence? tvar ty1)]
[void-type () #t]
[tvar-type (serial-number) (not (equal? tvar ty))])))
(define report-no-occurrence-violation
(lambda (ty1 ty2 exp)
(eopl:error 'check-no-occurence!
"Can't unify: type variable ~s occurs in type ~s in expression ~s~%"
(type-to-external-form ty1)
(type-to-external-form ty2)
(define report-unification-failure
(lambda (ty1 ty2 exp)
(eopl:error 'unification-failure
"Type mismatch: ~s doesn't match ~s in ~s~%"
(type-to-external-form ty1)
(type-to-external-form ty2)
(define unifier
(lambda (ty1 ty2 subst exp)
(let ([ty1 (apply-subst-to-type ty1 subst)]
[ty2 (apply-subst-to-type ty2 subst)])
(cond [(equal? ty1 ty2) subst]
[(tvar-type? ty1) (if (no-occurrence? ty1 ty2)
(extend-subst subst ty1 ty2)
(report-no-occurrence-violation ty1 ty2 exp))]
[(tvar-type? ty2) (if (no-occurrence? ty2 ty1)
(extend-subst subst ty2 ty1)
(report-no-occurrence-violation ty2 ty1 exp))]
[(and (proc-type? ty1) (proc-type? ty2)) (let ([subst (unifier (proc-type->arg-type ty1)
(proc-type->arg-type ty2)
(let ([subst (unifier (proc-type->result-type ty1)
(proc-type->result-type ty2)
[(and (ref-type? ty1) (ref-type? ty2)) (unifier (ref-type->base-type ty1)
(ref-type->base-type ty2)
[else (report-unification-failure ty1 ty2 exp)]))))
;; Inferrer.
(define sn 'uninitialized)
(define fresh-tvar-type
(let ([sn 0])
(lambda ()
(set! sn (+ sn 1))
(tvar-type sn))))
(define otype->type
(lambda (otype)
(cases optional-type otype
[no-type () (fresh-tvar-type)]
[a-type (ty) ty])))
(define type-of
(lambda (exp tenv subst)
(cases expression exp
[const-exp (num) (an-answer (int-type) subst)]
[zero?-exp (exp1) (cases answer (type-of exp1 tenv subst)
[an-answer (type1 subst1) (let ([subst2 (unifier type1 (int-type) subst1 exp)])
(an-answer (bool-type) subst2))])]
[diff-exp (exp1 exp2) (cases answer (type-of exp1 tenv subst)
[an-answer (type1 subst1) (let ([subst1 (unifier type1 (int-type) subst1 exp1)])
(cases answer (type-of exp2 tenv subst1)
[an-answer (type2 subst2) (let ([subst2 (unifier type2
(an-answer (int-type)
[if-exp (exp1 exp2 exp3)
(cases answer (type-of exp1 tenv subst)
[an-answer (ty1 subst) (let ([subst (unifier ty1 (bool-type) subst exp1)])
(cases answer (type-of exp2 tenv subst)
[an-answer (ty2 subst) (cases answer (type-of exp3 tenv subst)
[an-answer (ty3 subst) (let ([subst (unifier ty2
(an-answer ty2
[var-exp (var) (an-answer (apply-tenv tenv var) subst)]
[let-exp (var exp1 body) (cases answer (type-of exp1 tenv subst)
[an-answer (rhs-type subst) (type-of body (extend-tenv var rhs-type tenv) subst)])]
[proc-exp (var otype body) (let ([arg-type (otype->type otype)])
(cases answer (type-of body (extend-tenv var arg-type tenv) subst)
[an-answer (result-type subst)
(an-answer (proc-type arg-type result-type) subst)]))]
[call-exp (rator rand)
(let ([result-type (fresh-tvar-type)])
(cases answer (type-of rator tenv subst)
[an-answer (rator-type subst)
(cases answer (type-of rand tenv subst)
[an-answer (rand-type subst) (let ([subst (unifier rator-type
(proc-type rand-type result-type)
(an-answer result-type subst))])]))]
[letrec-exp (proc-result-otype proc-name bvar proc-arg-otype proc-body letrec-body)
(let ([proc-result-type (otype->type proc-result-otype)]
[proc-arg-type (otype->type proc-arg-otype)])
(let ([tenv-for-letrec-body (extend-tenv proc-name
(proc-type proc-arg-type proc-result-type)
(cases answer (type-of proc-body (extend-tenv bvar proc-arg-type tenv-for-letrec-body) subst)
[an-answer (proc-body-type subst) (let ([subst (unifier proc-body-type
(type-of letrec-body tenv-for-letrec-body subst))])))]
[begin-exp (exp1 exps) (let loop ([subst subst]
[exp1 exp1]
[exps exps])
(if (null? exps)
(type-of exp1 tenv subst)
(cases answer (type-of exp1 tenv subst)
[an-answer (ty1 subst) (loop subst
(car exps)
(cdr exps))])))]
[newref-exp (exp1) (cases answer (type-of exp1 tenv subst)
[an-answer (ty1 subst) (an-answer (ref-type ty1) subst)])]
[deref-exp (exp1) (cases answer (type-of exp1 tenv subst)
[an-answer (ty1 subst) (let ([ty2 (fresh-tvar-type)])
(an-answer ty2 (unifier ty1 (ref-type ty2) subst exp1)))])]
[setref-exp (exp1 exp2) (cases answer (type-of exp1 tenv subst)
[an-answer (ty1 subst) (cases answer (type-of exp2 tenv subst)
[an-answer (ty2 subst) (an-answer (void-type)
(unifier ty1
(ref-type ty2)
(define type-of-program
(lambda (pgm)
(cases program pgm
[a-program (exp1) (cases answer (type-of exp1 (empty-tenv) (empty-subst))
[an-answer (ty subst) (apply-subst-to-type ty subst)])])))
;; Interpreter.
(define apply-procedure
(lambda (proc1 arg)
(cases proc proc1
[procedure (var body saved-env) (value-of body (extend-env var arg saved-env))])))
(define value-of
(lambda (exp env)
(cases expression exp
[const-exp (num) (num-val num)]
[var-exp (var) (apply-env env var)]
[diff-exp (exp1 exp2) (let ([val1 (expval->num (value-of exp1 env))]
[val2 (expval->num (value-of exp2 env))])
(num-val (- val1 val2)))]
[zero?-exp (exp1) (let ([val1 (expval->num (value-of exp1 env))])
(if (zero? val1)
(bool-val #t)
(bool-val #f)))]
[if-exp (exp0 exp1 exp2) (if (expval->bool (value-of exp0 env))
(value-of exp1 env)
(value-of exp2 env))]
[let-exp (var exp1 body) (let ([val (value-of exp1 env)])
(value-of body (extend-env var val env)))]
[proc-exp (bvar ty body) (proc-val (procedure bvar body env))]
[call-exp (rator rand) (let ([proc (expval->proc (value-of rator env))]
[arg (value-of rand env)])
(apply-procedure proc arg))]
[letrec-exp (ty1 p-name b-var ty2 p-body letrec-body) (value-of letrec-body
(extend-env-rec p-name b-var p-body env))]
[begin-exp (exp1 exps) (let loop ([exp1 exp1]
[exps exps])
(if (null? exps)
(value-of exp1 env)
(begin (value-of exp1 env)
(loop (car exps)
(cdr exps)))))]
[newref-exp (exp1) (ref-val (newref (value-of exp1 env)))]
[deref-exp (exp1) (deref (expval->ref (value-of exp1 env)))]
[setref-exp (exp1 exp2) (setref! (expval->ref (value-of exp1 env)) (value-of exp2 env))])))
(define value-of-program
(lambda (pgm)
(cases program pgm
[a-program (body) (value-of body (empty-env))])))
;; Interface.
(define check
(lambda (string)
(type-to-external-form (type-of-program (scan&parse string)))))
(define run
(lambda (string)
(value-of-program (scan&parse string))))
(provide check num-val run)