-
Notifications
You must be signed in to change notification settings - Fork 0
/
test-hm.ss
65 lines (58 loc) · 3.69 KB
/
test-hm.ss
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
(import (unweave type-inference)
(unweave invariant-inference)
(unweave external labeling)
(only (scheme-tools) pretty-print))
;; (define expr (label-transform
;; `(letrec ([id (lambda (x) x)])
;; (id (lambda (x) (id (+ x 1)))))))
;; (define expr (anf (label-transform
;; `(letrec ([geometric (lambda ()
;; (if (flip) 0
;; (letrec ([x (geometric)])
;; (+ 1 x))))])
;; (geometric)))))
;; (define expr (anf (label-transform
;; `(letrec ([geometric (lambda () (if (flip) 0 (+ 1 (geometric))))]) (geometric)))))
;; (define expr (anf (label-transform
;; `(letrec ([max (lambda (x y) (if (> x y) x y))])
;; max))))
(define expr (anf (label-transform
`(letrec ([map (lambda (f xs)
(if (null? xs) '()
(cons (f (car xs))
(map f (cdr xs)))))])
(map (lambda (x) (+ x 1))
(cons 1 (cons 2 (cons 3 '()))))))))
(pretty-print expr)
(define types (infer-types expr `((+ . (-> Int (-> Int Int)))
(- . (-> Int (-> Int Int)))
(* . (-> Int (-> Int Int)))
(= . (-> Int (-> Int Bool)))
(> . (-> Int (-> Int Bool)))
(cons . (-> a (-> (Lst a) (Lst a))))
(() . (Lst a))
(car . (-> (Lst a) a))
(cdr . (-> (Lst a) (Lst a)))
(null? . (-> (Lst a) Bool))
(flip . (-> () Bool)))))
(pretty-print types)
;; (define label-type-map (cadr types))
;; (pretty-print (infer-invariants expr label-type-map '((unit . (: (rf (V unit) true) unit ()))
;; (flip . (-> () (: (rf (V Bool) (or (= true V) (= false V))) Bool ())))
;; (+ . (-> (: (rf (V Int) true) Int x)
;; (-> (: (rf (V Int) true) Int y)
;; (: (rf (V Int) (= V (+ x y))) Int ()))))
;; (- . (-> (: (rf (V Int) true) Int x)
;; (-> (: (rf (V Int) true) Int y)
;; (: (rf (V Int) (= V (- x y))) Int ()))))
;; (* . (-> (: (rf (V Int) true) Int x)
;; (-> (: (rf (V Int) true) Int y)
;; (: (rf (V Int) (= V (* x y))) Int ()))))
;; (= . (-> (: (rf (V Int) true) Int x)
;; (-> (: (rf (V Int) true) Int y)
;; (: (rf (V Bool) (= V (= x y))) Bool ()))))
;; (> . (-> (: (rf (V Int) true) Int x)
;; (-> (: (rf (V Int) true) Int y)
;; (: (rf (V Bool) (= V (> x y))) Bool ())))))))
;;
;;