Changeset 21052 in project


Ignore:
Timestamp:
10/26/10 03:45:50 (11 years ago)
Author:
Ivan Raikov
Message:

miniML version 1.0

Location:
release/4/miniML
Files:
1 edited
1 copied

Legend:

Unmodified
Added
Removed
  • release/4/miniML/branches/tiger/miniML.scm

    r20827 r21052  
    7474                  (Let0 (i v b) `(Let0 (,i = ,v) ,b)))))
    7575
    76 (define-record-type tyvar
    77   (make-tyvar repres level imperative)
    78   tyvar?
    79   (repres tyvar-repres tyvar-repres-set!) ;; representative, for union-find
    80   (level  tyvar-level tyvar-level-set!) ;; binding level, for generalization
    81   (imperative tyvar-imperative) ;; imperative type variables must not be generalized
    82                                 ;; for use w/ref and side effects
    83   )
    84        
    85 (define-datatype simple-type simple-type?
    86   (Tvar  (tv tyvar?))
    87   (Tcon  (p path?) (ts (lambda (x) (every simple-type? x)))))
    88 
    89 
    90 (define-record-printer (simple-type x out)
    91   (fprintf out "#<simple-type  ~S>"
    92            (cases simple-type x
    93                   (Tvar (tv) `(Tvar repres: ,(tyvar-repres tv)
    94                                     level: ,(tyvar-level tv)
    95                                     imperative: ,(tyvar-imperative tv)))
    96                   (Tcon (p ts) `(Tcon ,p . ,ts)))))
    97            
     76
     77
     78(define tyvar? symbol?)
     79(define (ty-list? x) (every ty? x))
     80(define (tyvar-list? x) (every tyvar? x))
     81(define (field-list? x) (every symbol? x))
     82
     83
     84(define-datatype ty ty?
     85  (Nil)
     86  (Tvar   (tv tyvar?))
     87  (Tapp   (p path?) (ts ty-list?))
     88  (Tpoly  (tvs tyvar-list?) (t ty?)))
     89
     90
     91(define tycon tycon?
     92  (Tprim (s string?))
     93  (Trecd (lst field-list?))
     94  (Tlam  (ts tyvar-list?) (t ty?))
     95  (Tuniq (tc tycon?) (u symbol?)))
     96 
    9897
    9998(define-record-type valtype
     
    104103  )
    105104
     105
    106106(define (make-valtype q b)
    107107  (if (not (list? q)) (error 'make-valtype "invalid quantified variables list" q))
     
    124124  )
    125125
    126 
    127 (define-record-type kind
    128   (make-kind arity)
    129   kind?
    130   (arity   kind-arity)
    131   )
    132 
    133 
    134 (define (subst-type ty subst)
    135   (cond ((simple-type? ty)
    136          (cases simple-type ty
    137                 (Tvar (tv)
    138                       (or (and (tyvar-repres tv) (subst-type (tyvar-repres tv) subst)) ty))
    139                 (Tcon (p ts) 
    140                       (Tcon (subst-path p subst) (map (lambda (x) (subst-type x subst)) ts)))
     126;; Substitution of paths in type constructors
     127
     128(define (subst-type-path t subst)
     129  (cond ((ty? t)
     130         (cases ty t
     131                (Tapp (p ts)   (Tapp (subst-path p subst)
     132                                     (map (lambda (x) (subst-type-path x subst)) ts)))
     133
     134                (Tpoly (tvs t) (Tpoly tvs (subst-type-path t subst)))
     135
     136                (else t)
    141137                ))
    142          (else (error 'subst-type "invalid type" ty))
     138         (else (error 'subst-type-path "invalid type" ty))
    143139        ))
    144140
    145141(define (subst-valtype vty subst)
    146142  (make-valtype (valtype-quantif vty)
    147                 (subst-type (valtype-body vty) subst)))
     143                (subst-type-path (valtype-body vty) subst)))
    148144
    149145(define (subst-deftype def subst)
    150146  (make-deftype (deftype-params def)
    151                 (subst-type (deftype-body def) subst)))
    152 
    153 (define (subst-kind kind subst) kind)
     147                (subst-type-path (deftype-body def) subst)))
    154148
    155149
     
    161155  (make-mod-env core-syntax))
    162156
    163 
    164 ;; The type-checker for mini-ML (Hindley-Milner type inference)
    165 
    166 (define (typerepr ty)
    167   (assert (simple-type? ty))
    168   (cases simple-type ty
    169          (Tvar (tv)
    170                (or (and (tyvar-repres tv)
    171                         (let ((r (typerepr (tyvar-repres tv))))
    172                           (tyvar-repres-set! tv r)
    173                           r))
    174                     ty))
    175          (else ty)))
    176 
    177 
    178 (define current-level (make-parameter 0))
    179 (define (begin-def) (current-level (+ 1 (current-level))))
    180 (define (end-def)   (current-level (- (current-level) 1)))
    181 (define (newvar . rest)    (make-tyvar #f (current-level)
    182                                        (if (null? rest) #f (car rest))))
    183 (define (unknown)   (Tvar (newvar)))
    184 
    185 (define (subst-vars ty subst)
    186   (let ((tyvar (typerepr ty)))
    187     (assert (simple-type? tyvar))
    188     (cases simple-type tyvar
    189            (Tvar (var) (let ((v (assq var subst)))
    190                          (or (and v (cadr v)) tyvar) ))
    191            (Tcon (p ts)
    192                  (let ((ts1 (map (lambda (t) (subst-vars t subst)) ts)))
    193                    (Tcon p ts1))))))
    194 
    195 
    196 (define (cannot-expand path)
    197   (make-property-condition 'Cannot_expand 'message path))
    198 (define cannot-expand?
    199   (condition-predicate 'Cannot_expand))
    200 
     157;; Substitution of type variables
     158
     159(define (subst-type-var t subst)
     160  (cond ((ty? t)
     161         (cases ty t
     162               
     163                (Nil ()  t)
     164
     165                (Tvar (tv) (cond ((assoc tv subst) => (lambda (ti) (cdr ti)))
     166                                 (else  t)))
     167               
     168                (Tapp (tc us) (cases tycon tc
     169                                     (Tlam (as t)
     170                                           (subst-type-var (subst-type-var t (zip as us)) subst))
     171                                     (else
     172                                      (Tapp tc (map (lambda (tt) (subst-type-var tt subst)) us)))))
     173
     174                (Tpoly (as u) (let* ((gs (list-tabulate (length tvs) (lambda (i) (gensym 'g))))
     175                                     (u1 (subst-type-var u (zip as (map Tvar gs)))))
     176                                (Poly gs (subst-type-var u1 subst))))
     177
     178                (else t)
     179                ))
     180         (else (error 'subst-type-var "invalid type" ty))
     181        ))
     182 
     183(define (cannot-expand path) (make-property-condition 'Cannot_expand 'message path))
     184
     185(define cannot-expand? (condition-predicate 'Cannot_expand))
     186
     187;; Find a type constructor identifier in the given environment, and
     188;; perform type parameter substitution
    201189
    202190(define (expand-manifest env path args)
     
    205193      (if (not m)
    206194          (signal (cannot-expand path))
    207           (subst-vars (deftype-body m)
    208                       (zip (deftype-params m) args )
    209                       )))))
    210 
    211 
    212 ;; Expand abbreviations in ty1 and ty2 until their top constructor match
    213 (define (scrape-types env ty1 ty2)
    214   (assert (simple-type? ty1))
    215   (assert (simple-type? ty2))
    216   (let ((repr1 (typerepr ty1))
    217         (repr2 (typerepr ty2)))
     195          (subst-type-var (deftype-body m)
     196                          (zip (deftype-params m) args )
     197                          )))))
     198
     199;; Expand type paths in ty1 and ty2 until their top constructors match
     200
     201(define (expand-type-paths env ty1 ty2)
     202  (assert (ty? ty1))
     203  (assert (ty? ty2))
     204  (let ((repr1 ty1)
     205        (repr2 ty2))
    218206    (cases simple-type repr1
    219            (Tcon (path1 args1)
     207           (Tapp (path1 args1)
    220208                 (cases simple-type repr2
    221                         (Tcon (path2 args2)
     209                        (Tapp (path2 args2)
    222210                              (if (path-equal? path1 path2)
    223211                                  (list repr1 repr2)
     
    232220                                                   (else (abort exn)))
    233221                                             (let ((m2 (expand-manifest env path2 args2)))
    234                                                (scrape-types env repr1 m2))))
     222                                               (expand-type-paths env repr1 m2))))
    235223                                           (else (abort exn)))
    236224                                     )
    237225                                   (let ((m1 (expand-manifest env path1 args1)))
    238                                      (scrape-types env m1 repr2)))
     226                                     (expand-type-paths env m1 repr2)))
    239227                                  ))
    240228                        (else
     
    247235                          (begin
    248236                            (let ((m1 (expand-manifest env path1 args1)))
    249                               (scrape-types env m1 repr2)))
     237                              (expand-type-paths env m1 repr2)))
    250238                          ))))
    251239           (else
    252240            (cases simple-type repr2
    253                (Tcon (path args)
    254                      (handle-exceptions
    255                       exn
    256                       (begin
    257                         (cond ((cannot-expand? exn)
    258                                (list repr1 repr2))
    259                               (else (abort exn))))
    260                       (let ((m2 (expand-manifest env path args)))
    261                         (scrape-types env repr1 m2))))
    262                       
    263                (else
    264                 (list repr1 repr2)))))
     241                   (Tapp (path args)
     242                         (handle-exceptions
     243                          exn
     244                          (begin
     245                            (cond ((cannot-expand? exn)
     246                                   (list repr1 repr2))
     247                                  (else (abort exn))))
     248                          (let ((m2 (expand-manifest env path args)))
     249                            (expand-type-paths env repr1 m2))))
     250                   
     251                   (else
     252                    (list repr1 repr2)))))
    265253    ))
    266254
    267 (define (occur-check var ty)
    268  (cases simple-type (typerepr ty)
    269         (Tvar (var1) (if (eq? var var1) (error 'occur-check "cycle in unification")))
    270         (Tcon (p tl) (for-each (lambda (t) (occur-check var t)) tl))))
    271 
    272 (define (update-levels level-max ty)
    273   (cases simple-type (typerepr ty)
    274          (Tvar (v)    (if (< level-max (tyvar-level v))
    275                           (tyvar-level-set! v level-max)))
    276          (Tcon (p tl) (for-each (lambda (t) (update-levels level-max t)) tl))))
    277 
    278 (define (unify env t1 t2)
    279   (let* ((rs (scrape-types env t1 t2))
     255(define (unify env ty1 ty2)
     256  (let* ((rs (expand-type-paths env ty1 ty2))
    280257         (r1 (car rs))
    281258         (r2 (cadr rs)))
    282 
    283     (assert (simple-type? r1))
    284     (assert (simple-type? r2))
    285     (if (equal? r1 r2) '()
    286         (cases simple-type r1
    287           (Tvar (v)
    288              (begin
    289                (occur-check v r2)
    290                (update-levels (tyvar-level v) r2)
    291                (tyvar-repres-set! v r2)))
    292           (else
    293            (cases simple-type r2
    294                   (Tvar (v)
    295                         (begin
    296                           (occur-check v r1)
    297                           (update-levels (tyvar-level v) r1)
    298                           (tyvar-repres-set! v r1)))
    299                   (else
    300                    (cases simple-type r1
    301                           (Tcon (path1 args1)
    302                                 (cases simple-type r2
    303                                        (Tcon (path2 args2)
    304                                              (if (path-equal? path1 path2)
    305                                                  (for-each (lambda (t1 t2) (unify env t1 t2)) args1 args2)
    306                                                  (error 'unify "type constructor mismatch in unification" t1 t2)))
    307                                        (else (error 'unify "type constructor mismatch in unification" t1 t2))
    308                                        ))
    309                           (else (error 'unify "type constructor mismatch in unification" t1 t2))))
    310                   ))
    311           ))))
    312 
    313 (define (generalize ty)
    314   (define (genvars vars ty)
    315     (cases simple-type ty
    316            (Tvar (v)
    317              (if (and (< (current-level) (tyvar-level v))
    318                       (not (tyvar-imperative v))
    319                       (member v vars))
    320                  (cons v vars)
    321                  vars))
    322            (Tcon (path tl)
    323                  (fold genvars tl vars))))
    324 
    325   (make-valtype (genvars '() ty) ty))
    326 
    327 (define (trivial-scheme ty)
    328   (make-valtype '() ty))
    329 
    330 (define (instance vty)
    331   (let ((vars (valtype-quantif vty)))
    332     (if (null? vars)
    333         (valtype-body vty)
    334         (subst-vars (valtype-body vty)
    335                     (map (lambda (v) (list v (unknown))) vars) ))))
     259   
     260   
     261    ))
     262       
     263
     264
    336265
    337266(define ident-arrow  (ident-create "->"))
     
    372301        ((bool)    (Tcon path-bool '()))
    373302        (else (error 'const-type "invalid constant" c)))))
     303
    374304
    375305(define (infer-type env t)
     
    825755
    826756
     757#|
     758(define-record-type tyvar
     759  (make-tyvar repres level imperative)
     760  tyvar?
     761  (repres tyvar-repres tyvar-repres-set!) ;; representative, for union-find
     762  (level  tyvar-level tyvar-level-set!) ;; binding level, for generalization
     763  (imperative tyvar-imperative) ;; imperative type variables must not be generalized
     764                                ;; for use w/ref and side effects
     765  )
     766
     767(define-record-printer (simple-type x out)
     768  (fprintf out "#<simple-type  ~S>"
     769           (cases simple-type x
     770                  (Tvar (tv) `(Tvar repres: ,(tyvar-repres tv)
     771                                    level: ,(tyvar-level tv)
     772                                    imperative: ,(tyvar-imperative tv)))
     773                  (Tcon (p ts) `(Tcon ,p . ,ts)))))
     774
     775
     776(define-record-type kind
     777  (make-kind arity)
     778  kind?
     779  (arity   kind-arity)
     780  )
     781           
     782|#
     783
    827784       
    828785       
Note: See TracChangeset for help on using the changeset viewer.