source: project/release/4/miniML/trunk/miniML.scm @ 22026

Last change on this file since 22026 was 22026, checked in by Ivan Raikov, 10 years ago

miniML: removing vestigial sxml->term procedure

File size: 23.6 KB
Line 
1;;
2;;  A type checker and interpreter for a simple ML-like language.
3;;
4;;  Based on the code and paper by Xavier Leroy (2000): A modular
5;;  module system. Journal of Functional Programming, 10, pp 269-303
6;;  doi:10.1017/S0956796800003683
7;;
8;;
9;; Copyright 2010 Ivan Raikov and the Okinawa Institute of
10;; Science and Technology.
11;;
12;; This program is free software: you can redistribute it and/or
13;; modify it under the terms of the GNU General Public License as
14;; published by the Free Software Foundation, either version 3 of the
15;; License, or (at your option) any later version.
16;;
17;; This program is distributed in the hope that it will be useful, but
18;; WITHOUT ANY WARRANTY; without even the implied warranty of
19;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
20;; General Public License for more details.
21;;
22;; A full copy of the GPL license can be found at
23;; <http://www.gnu.org/licenses/>.
24;;
25
26(module miniML
27
28        (constant? term?
29         
30         Const Longid Function Apply Let0 
31         Tcon Tvar 
32
33         core-syntax
34         core-typing
35         core-scoping
36         core-initialize
37
38         core-utils
39
40         term->sxml modtype->sxml modspec->sxml modterm->sxml moddef->sxml const->sxml
41         )
42
43        (import scheme chicken 
44                (only srfi-1 fold filter combine every zip)
45                (only extras pp fprintf)
46                (only data-structures alist-ref ->string identity))
47        (require-extension extras datatype static-modules)
48
49
50(define (constant? c)
51  (and (pair? c) 
52       (let ((t (car c)) (v (cadr c)))
53         (case t ((real) (real? v))
54               ((nat)    (integer? v))
55               ((label)  (symbol? v))
56               ((bool)   (boolean? v))
57               (else #f)))))
58
59(define-datatype term term?
60  (Const     (c constant?)) 
61  (Longid    (p path?)) ;; id or mod.mod...id
62  (Function  (i ident?) (t term?))
63  (Apply     (t1 term?) (t2 term?))
64  (Let0      (i ident?) (v term?) (b term?))
65  )
66
67(define-record-printer (term x out)
68  (fprintf out "~S"
69           (cases term x
70                  (Const (c) `(Const ,c))
71                  (Longid (p) p)
72                  (Function (i t) `(Function ,i ,t))
73                  (Apply (t1 t2) `(Apply ,t1 ,t2))
74                  (Let0 (i v b) `(Let0 (,i = ,v) ,b)))))
75
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           
98
99(define-record-type valtype
100  (make-valtype0 quantif body)
101  valtype?
102  (quantif valtype-quantif) ;; quantified variables
103  (body    valtype-body) ;; body of type scheme
104  )
105
106(define (make-valtype q b)
107  (if (not (list? q)) (error 'make-valtype "invalid quantified variables list" q))
108  (if (not (simple-type? b)) (error 'make-valtype "invalid type body" b ))
109  (make-valtype0 q b))
110 
111
112(define-record-printer (valtype x out)
113  (fprintf out "#<valtype  quantif: ~S body: ~S>"
114           (valtype-quantif x)
115           (valtype-body x)))
116           
117
118
119(define-record-type deftype
120  (make-deftype params defbody)
121  deftype?
122  (params   deftype-params) ;; list of parameters
123  (defbody  deftype-body) ;; body of type definition
124  )
125
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)))
141                ))
142         (else (error 'subst-type "invalid type" ty))
143        ))
144
145(define (subst-valtype vty subst)
146  (make-valtype (valtype-quantif vty)
147                (subst-type (valtype-body vty) subst)))
148
149(define (subst-deftype def subst)
150  (make-deftype (deftype-params def)
151                (subst-type (deftype-body def) subst)))
152
153(define (subst-kind kind subst) kind)
154
155
156(define core-syntax
157  (make-core-syntax term? valtype? deftype? kind? make-valtype make-deftype subst-valtype subst-deftype subst-kind))
158
159(define-values ( env-binding? env-empty env-add-signature env-add-module env-add-type env-add-spec env-add-value
160                 env-find-value env-find-type env-find-module env-find)
161  (make-mod-env core-syntax))
162
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
201
202(define (expand-manifest env path args)
203  (let ((td (env-find-type path env)))
204    (let ((m (typedecl-manifest td)))
205      (if (not m) 
206          (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)))
218    (cases simple-type repr1 
219           (Tcon (path1 args1)
220                 (cases simple-type repr2
221                        (Tcon (path2 args2)
222                              (if (path-equal? path1 path2)
223                                  (list repr1 repr2)
224                                  (handle-exceptions 
225                                   exn
226                                   (begin
227                                     (cond ((cannot-expand? exn)
228                                            (handle-exceptions 
229                                             exn
230                                             (cond ((cannot-expand? exn)
231                                                    (list repr1 repr2))
232                                                   (else (abort exn)))
233                                             (let ((m2 (expand-manifest env path2 args2)))
234                                               (scrape-types env repr1 m2))))
235                                           (else (abort exn)))
236                                     )
237                                   (let ((m1 (expand-manifest env path1 args1)))
238                                     (scrape-types env m1 repr2)))
239                                  ))
240                        (else
241                         (handle-exceptions
242                          exn
243                          (begin
244                            (cond ((cannot-expand? exn)
245                                   (list repr1 repr2))
246                                  (else (abort exn))))
247                          (begin
248                            (let ((m1 (expand-manifest env path1 args1)))
249                              (scrape-types env m1 repr2)))
250                          ))))
251           (else
252            (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)))))
265    ))
266
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))
280         (r1 (car rs))
281         (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) ))))
336
337(define ident-arrow  (ident-create "->"))
338(define path-arrow   (Pident ident-arrow))
339(define (arrow-type t1 t2) (Tcon path-arrow (list t1 t2)))
340
341(define ident-star   (ident-create "*"))
342(define path-star    (Pident ident-star))
343(define star-type    (Tcon path-star '()))
344
345(define ident-list     (ident-create "list"))
346(define path-list      (Pident ident-list))
347(define (list-type t)  (Tcon path-list (list t)))
348
349(define ident-nat    (ident-create "nat"))
350(define path-nat     (Pident ident-nat))
351(define nat-type     (Tcon path-nat '()))
352
353(define ident-real   (ident-create "real"))
354(define path-real    (Pident ident-real))
355(define real-type    (Tcon path-real '()))
356
357(define ident-bool   (ident-create "bool"))
358(define path-bool    (Pident ident-bool))
359(define bool-type    (Tcon path-bool '()))
360
361(define ident-label   (ident-create "label"))
362(define path-label    (Pident ident-label))
363(define label-type    (Tcon path-label '()))
364
365(define ident-bot   (ident-create "bot"))
366(define path-bot    (Pident ident-bot))
367(define bot-type    (Tcon path-bot '()))
368
369
370(define (const-type c)
371  (if (constant? c)
372      (case (car c)
373        ((nat)    (Tcon path-nat   '()))
374        ((real)   (Tcon path-real  '()))
375        ((label)  (Tcon path-label '()))
376        ((bool)    (Tcon path-bool '()))
377        (else (error 'const-type "invalid constant" c)))))
378
379(define (infer-type env t)
380  (cases term t
381    (Const (n)    (const-type n))
382    (Longid (p)   (instance (env-find-value p env)))
383    (Function (param body)
384              (let* ((type-param (unknown))
385                     (type-body (infer-type (env-add-value param (trivial-scheme type-param) env) 
386                                            body)))
387                (arrow-type type-param type-body)))
388
389    (Apply (funct arg)
390           (let ((type-funct (infer-type env funct))
391                 (type-arg   (infer-type env arg))
392                 (type-res   (unknown)))
393             (unify env type-funct (arrow-type type-arg type-res))
394             type-res))
395
396    (Let0 (ident arg body)
397          (begin-def)
398          (let ((type-arg (infer-type env arg)))
399            (end-def)
400            (infer-type (env-add-value ident (generalize type-arg) env) body)))
401
402    ))
403
404(define (check-simple-type env params ty)
405  (cases simple-type (typerepr ty)
406         (Tvar (v)
407               (if (not (member v params)) (error 'check-simple-type "free type variable" v)))
408         (Tcon (path tl)
409               (let ((arity (kind-arity (typedecl-kind (env-find-type path env)))))
410                 (if (not (= (length tl) arity))
411                     (error 'check-simple-type "arity mismatch" path tl)
412                     (for-each (lambda (t) (check-simple-type env params t)) tl))))))
413                 
414
415(define (kind-deftype env def)
416  (check-simple-type env (deftype-params def) (deftype-body def))
417  (make-kind (length (deftype-params def))))
418
419(define (check-valtype env vty)
420  (check-simple-type env (valtype-quantif vty) (valtype-body vty)))
421
422(define (check-kind env kind) (begin))
423
424(define (type-term env term)
425  (begin-def)
426  (let ((ty (infer-type env term)))
427    (end-def)
428    (generalize ty)))
429
430(define (valtype-match env vty1 vty2)
431  (define (tyfilter ty1 ty2)
432    (assert (simple-type? ty1))
433    (assert (simple-type? ty2))
434    (let* ((rs (scrape-types env ty1 ty2))
435           (r1 (car rs))
436           (r2 (cadr rs)))
437      (cases simple-type r1
438             (Tvar (v)
439                   (if (member v (valtype-quantif r2)) #f
440                       (begin
441                         (tyvar-repres-set! v r2)
442                         #t)))
443             (Tcon (path1 tl1)
444                   (cases simple-type r2
445                          (Tcon (path2 tl2)
446                                (and (equal? path1 path2)
447                                     (every tyfilter tl1 tl2)))
448                          (else #f))))))
449
450  (tyfilter (instance vty1) (valtype-body vty2)))
451
452
453(define (deftype-equiv env kind def1 def2)
454  (define (equiv ty1 ty2)
455    (let* ((rs (scrape-types env ty1 ty2))
456           (r1 (car rs))
457           (r2 (cadr rs)))
458      (cases simple-type r1
459             (Tvar (v1)
460                   (cases simple-type r2
461                          (Tvar (v2) (equal? v1 v2))
462                          (else #f)))
463             (Tcon (path1 args1)
464                   (cases simple-type r2
465                          (Tcon (path2 args2)
466                                (and (equal? path1 path2)
467                                     (every equiv args1 args2)))
468                          (else #f))))))
469
470  (let ((subst (map (lambda (v1 v2) (list v2 (Tvar v1))) 
471                    (deftype-params def1)  (deftype-params def2))))
472    (equiv (deftype-body def1)
473           (subst-vars (deftype-body def2) subst ))))
474
475(define (kind-match env kind1 kind2)
476  (equal? (kind-arity kind1) (kind-arity kind2)))
477
478(define (deftype-of-path path kind)
479  (define (make-params n)
480    (if (<= n 0) '() (cons (newvar) (make-params (- n 1)))))
481  (let ((params (make-params (kind-arity kind))))
482    (make-deftype params
483                  (Tcon path (map (lambda (v) (Tvar v)) params)))))
484
485
486
487;; Elimination of dependencies on a given module identifier by
488;; repeated expansion of type paths rooted at that identifier.  Those
489;; functions are used only with the relaxed typing rule for functor
490;; applications described in section 5.5 and implemented in the file
491;; modules.ml.extended
492
493(define (is-rooted-at id p)
494  (cases path p
495         (Pident (id1) (ident-equal? id id1))
496         (Pdot (p s)   (is-rooted-at id p))))
497
498
499(define nondep-type
500  (letrec ((nondep-type 
501            (lambda (nondep-type env id ty)
502              (cases simple-type (typerepr ty)
503                     (Tvar (v) (Tvar v))
504                     (Tcon (path args)
505                           (if (is-rooted-at id path)
506                               (handle-exceptions 
507                                exn
508                                (cond ((cannot-expand? exn)
509                                       (error 'nondep-type "path not found" path)))
510                                (nondep-type env id (expand-manifest env path args)))
511                               (Tcon path (map (nondep-type env id) args))))))))
512    nondep-type))
513
514
515(define (nondep-valtype env id vty)
516  (make-valtype (valtype-quantif vty)
517                (nondep-type env id (valtype-body vty))))
518
519(define (nondep-deftype env id vty)
520  (make-deftype (deftype-params vty)
521                (nondep-type env id (deftype-body vty))))
522
523(define (nondep-kind env id kind)
524  kind)
525
526
527(define (scope-term sc t)
528  (cases term t
529         (Const (n)             (Const n))
530         (Longid (path)         (Longid (st-value-path path sc)))
531         (Function (id body)    (Function id (scope-term (st-enter-value id sc) body)))
532         (Apply (t1 t2)         (Apply (scope-term sc t1) (scope-term sc t2)))
533         (Let0 (id t1 t2)       (Let0 id (scope-term sc t1) 
534                                      (scope-term (st-enter-value id sc) t2)))
535         ))
536
537(define (scope-simple-type  sc ty)
538  (cases simple-type ty
539         (Tvar (v) (Tvar v))
540         (Tcon (path args)
541               (Tcon (st-type-path path sc)
542                     (map (lambda (ty) (scope-simple-type sc ty)) args)))))
543         
544(define (scope-valtype sc vty)
545  (make-valtype (valtype-quantif vty)
546                (scope-simple-type sc (valtype-body vty))))
547
548(define (scope-deftype sc def)
549  (make-deftype (deftype-params def)
550                (scope-simple-type sc (deftype-body def))))
551
552
553(define (scope-kind sc kind)
554  kind)
555
556
557(define core-typing
558  (make-core-typing type-term kind-deftype check-valtype check-kind
559                        valtype-match deftype-equiv kind-match deftype-of-path))
560 
561(define core-scoping
562  (make-core-scoping scope-term scope-valtype scope-deftype scope-kind))
563
564
565(define (core-initialize enter-type enter-val)
566  (enter-type ident-arrow (make-typedecl (make-kind 2) #f))
567  (enter-type ident-star  (make-typedecl (make-kind 2) #f))
568  (enter-type ident-list  (make-typedecl (make-kind 1) #f))
569  (enter-type ident-real  (make-typedecl (make-kind 0) #f))
570  (enter-type ident-bool  (make-typedecl (make-kind 0) #f))
571  (enter-type ident-label (make-typedecl (make-kind 0) #f))
572  (enter-type ident-bot   (make-typedecl (make-kind 0) #f))
573  (enter-type ident-nat   (make-typedecl (make-kind 0) #f))
574
575  (enter-val "false" (make-valtype '() bool-type))
576  (enter-val "true"  (make-valtype '() bool-type))
577  (enter-val "empty" (make-valtype '() bot-type))
578
579  (for-each
580   (lambda (name)
581     (enter-val name (make-valtype '() (arrow-type nat-type 
582                                                   (arrow-type  nat-type
583                                                                nat-type)))))
584   '("add" "sub" "mul" "div" ))
585
586  (for-each
587   (lambda (name)
588     (enter-val name (make-valtype '() (arrow-type nat-type 
589                                                   (arrow-type nat-type
590                                                               bool-type)))))
591   '("==" "<>" "<" "<=" ">" ">="))
592
593  (let* ((alpha (newvar)) (beta (newvar)) 
594         (alpha_i (make-tyvar (tyvar-repres alpha) (tyvar-level alpha) #t))
595         (talpha (Tvar alpha)) (tbeta (Tvar beta)) (talpha_i (Tvar alpha_i)))
596
597    (enter-val "pair" 
598               (make-valtype `(,alpha ,beta)
599                             (arrow-type talpha 
600                                         (arrow-type tbeta
601                                                     (Tcon path-star `(,talpha ,tbeta))))))
602    (enter-val "fst"
603               (make-valtype `(,alpha ,beta)
604                             (arrow-type (Tcon path-star `(,talpha ,tbeta)) talpha)))
605
606    (enter-val "snd"
607               (make-valtype `(,alpha ,beta)
608                             (arrow-type (Tcon path-star `(,talpha ,tbeta)) tbeta)))
609
610    (enter-val "null" (make-valtype `(,alpha) (Tcon path-list `(,talpha))))
611
612    (enter-val "cons" 
613               (make-valtype `(,alpha)
614                             (arrow-type talpha 
615                                         (arrow-type (Tcon path-list `(,talpha))
616                                                     (Tcon path-list `(,talpha))))))
617    (enter-val "head" 
618               (make-valtype `(,alpha)
619                             (arrow-type (Tcon path-list `(,talpha))
620                                         talpha)))
621    (enter-val "tail" 
622               (make-valtype `(,alpha)
623                             (arrow-type (Tcon path-list `(,talpha))
624                                         (Tcon path-list `(,talpha)))))
625
626
627    (enter-val "cond"
628               (make-valtype `(,alpha)
629                             (arrow-type bool-type
630                                         (arrow-type talpha (arrow-type talpha talpha)))))
631
632    )
633  )
634
635(define type-variables (make-parameter '()))
636
637(define (reset-type-variables) (type-variables '()))
638
639(define (find-type-variable name)
640  (or (assoc name (type-variables))
641      (let ((v (newvar)))
642        (type-variables (cons (name v) (type-variables)))
643        v)))
644
645(define (binop op arg1 arg2)
646  (Apply (Apply (Longid (Pident (ident-create op))) arg1) arg2))
647
648(define (ternop op arg1 arg2 arg3)
649  (Apply (Apply (Apply (Longid (Pident (ident-create op))) arg1) arg2) arg3))
650
651(define (core-utils) 
652  (values type-variables reset-type-variables
653          find-type-variable 
654          begin-def end-def newvar generalize
655          make-deftype make-valtype make-kind
656          binop ternop path-star path-list path-arrow
657          star-type list-type arrow-type label-type bot-type
658          ))
659
660(define variable-names (make-parameter '()))
661(define (reset-names)  (variable-names '()))
662
663(define-record-printer (simple-type ty out)
664  (cases simple-type (typerepr ty)
665         (Tvar (v) (let* ((name (or (assq v (variable-names))))
666                          (name (if (not name)
667                                    (let* ((n  (+ 1 (length (variable-names))))
668                                           (s  (string-append "t" (number->string n))))
669                                      (variable-names (cons (list n s) (variable-names)))
670                                      s))))
671                     (fprintf out "'~A" name)))
672         (Tcon (p lst)
673               (cond ((null? lst)
674                      (fprintf out "~S" p))
675                     ((and (path-equal? p path-arrow) 
676                           (pair? lst) (pair? (cdr lst)) (null? (cddr lst)))
677                      (fprintf out "~S -> ~S" (car lst) (cadr lst)))
678                     ((and (path-equal? p path-star) 
679                           (pair? lst) (pair? (cdr lst)) (null? (cddr lst)))
680                      (fprintf out "~S * ~S" (car lst) (cadr lst)))
681                     (else
682                      (begin
683                        (fprintf out "(~S" (car lst))
684                        (for-each (lambda (t) (fprintf out ", ~S" t)) (cdr lst))
685                        (fprintf out ") ~S" p)))
686                     ))
687         ))
688                             
689                             
690(define-record-printer (valtype vty out)
691  (begin
692    (reset-names)
693    (fprintf out "~S" (valtype-body vty))))
694
695(define-record-printer (modtype mty out)
696  (cases modtype mty
697         (Signature (sg) 
698                    (pp `(sig . ,sg) out))
699         (Functorty (param pty body)
700                    (pp `(functor (,param : ,pty) 
701                                  ,body) out))
702         ))
703
704
705(define-record-printer (modspec item out)
706  (cases modspec item
707         (Value_sig (id vty)
708                    (pp `(val ,id : ,vty) out))
709         (Type_sig (id decl)
710                   (pp `(type ,id = ,decl) out))
711         (Module_sig (id mty)
712                     (pp `(module ,id : ,mty) out))))
713
714
715(define-record-printer (modval x out)
716  (cases modval x
717         (Structure_v (env) (pp `(structure . ,env) out))
718         (Mclosure_v (body env) (pp  `(mclosure ,env ,body) out))))
719
720
721(define (const->sxml c)
722  (if (constant? c) (list (car c) (->string (cadr c)))
723      (else (error 'const->sxml "invalid constant" c))))
724
725
726(define (path->sxml p)
727  (cases path p
728         (Pident (id) `(pident (@ (name ,(ident-name id)))))
729         (Pdot (p s)  `(pdot (@ (name ,s)) (path ,(path->sxml p))))))
730
731
732(define (kind->sxml k)
733  `(kind (arity ,(->string (kind-arity k)))))
734
735
736(define (term->sxml t)
737  (cases term t
738         (Const     (c)     `(const ,(const->sxml c)))
739         (Longid    (p)     `(longid ,(path->sxml p)))
740         (Function  (i t)   `(function (@ (formal ,(ident-name i))) (body ,(term->sxml t))))
741         (Apply     (t1 t2) `(apply (left ,(term->sxml t1)) (right ,(term->sxml t2))))
742         (Let0      (i v b) `(let0  (@ (name ,(ident-name i))) 
743                                    (value ,(term->sxml v)) 
744                                    (body ,(term->sxml b))))
745         ))
746
747(define (tyvar->sxml tv)
748  (let ((repres (tyvar-repres tv))
749        (level  (tyvar-level tv))
750        (imp    (tyvar-imperative tv)))
751  `( 
752    ,(and repres `(repres ,(simple-type->sxml repres)))
753    (level ,level)
754    ,(and imp `(imperative)))))
755
756
757(define (simple-type->sxml ty)
758  (cases simple-type ty
759         (Tvar  (tv) `(tvar ,@(filter identity (tyvar->sxml tv))))
760         (Tcon (p ts) `(tcon (path ,(path->sxml p)) 
761                             ,@(map (lambda (x) `(t ,(simple-type->sxml x))) ts)))))
762
763
764(define (valtype->sxml x)
765  `(valtype ,@(map (lambda (q) `(qvar ,q)) (valtype-quantif x))
766            (body ,(simple-type->sxml (valtype-body x)))))
767
768
769(define (typedecl->sxml decl)
770  (let ((manifest (typedecl-manifest decl)))
771    `(typedecl ,(kind->sxml (typedecl-kind decl))
772               ,@(if manifest `((manifest ,(deftype->sxml manifest)))  `()))))
773
774
775(define (deftype->sxml x)
776  `(deftype ,@(map (lambda (p) `(param ,p)) (deftype-params x))
777            (body ,(simple-type->sxml (deftype-body x)))))
778
779
780(define (modspec->sxml x)
781  (cases modspec x
782         (Value_sig  (id valtype) `(value_sig (@ (name ,(ident-name id)))
783                                              ,(valtype->sxml valtype)))
784         (Type_sig   (id decl)    `(type_sig (@ (name ,(ident-name id)))
785                                             ,(typedecl->sxml decl)))
786         (Module_sig (id ty)      `(module_sig (@ (name ,(ident-name id)))
787                                               ,(modtype->sxml ty)))
788         ))
789
790
791(define (moddef->sxml d)
792  (cases moddef d
793    (Value_def  (id term) `(value_def (@ (name ,(ident-name id)) )
794                                      (term ,(term->sxml term))))
795    (Type_def   (id kind defty) `(type_def (@ (name ,(ident-name id)) )
796                                           ,(kind->sxml kind)
797                                           ,(deftype->sxml defty)))
798    (Module_def (id modterm) `(component_def (@ (name ,(ident-name id)) )
799                                             (term ,(modterm->sxml modterm))))
800    ))
801
802
803(define (modtype->sxml mt)
804  (cases modtype mt
805         (Signature (s) `(signature ,@(map modspec->sxml s)))
806         (Functorty (id arg body) 
807                    `(functorty (@ (name ,(ident-name id)))
808                                (arg ,(modtype->sxml arg))
809                                (body ,(modtype->sxml body))))))
810
811
812(define (modterm->sxml t)
813  (cases modterm t
814         (Modid      (p)        `(modid ,(path->sxml p)))
815         (Structure  (s)        `(structure ,@(map (lambda (x) `(def ,(moddef->sxml x))) s)))
816         (Functor    (id mty m) `(functor (@ (name ,(ident-name id))) 
817                                          (type ,(modtype->sxml mty))
818                                          (body ,(modterm->sxml m))))
819         (Mapply     (m1 m2) `(modapply (left ,(modterm->sxml m1)) 
820                                        (right ,(modterm->sxml m2))))
821         (Constraint (m mty) `(constraint (body ,(modterm->sxml m)) 
822                                          (type ,(modtype->sxml mty))))
823         ))
824
825)
826
Note: See TracBrowser for help on using the repository browser.