simple.rkt (4516B)
1 #lang typed/dotlambda 2 (require type-expander) 3 4 (require (lib "phc-graph/invariants-phantom.hl.rkt") 5 "util.rkt" 6 phc-graph/dot-lang 7 phc-toolkit) 8 9 (check-same-type 10 (Π .a.aa(.b.c)*.d.e) 11 (Rec 12 R1 13 (U (Pairof Any R1) 14 (Pairof 15 (Pairof 'a AnyType) 16 (Pairof 17 (Pairof 'aa AnyType) 18 (Rec 19 R2 20 (U (Pairof 21 (Pairof 'b AnyType) 22 (Pairof (Pairof 'c AnyType) R2)) 23 (List (Pairof 'd AnyType) (Pairof 'e AnyType))))))))) 24 25 (struct a AnyType ()); the node type a. 26 (struct b AnyType ()); the node type b. 27 28 (check-same-type 29 (Π :a.aa(.b.c)*.d.e) 30 (Rec 31 R1 32 (U (Pairof Any R1) 33 (Pairof 34 (Pairof AnyField a) 35 (Pairof 36 (Pairof 'aa AnyType) 37 (Rec 38 R2 39 (U (List (Pairof 'd AnyType) (Pairof 'e AnyType)) 40 (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R2))))))))) 41 (check-same-type 42 (Π :a(.b.c)*.d.e) 43 (Rec 44 R1 45 (U (Pairof Any R1) 46 (Pairof 47 (Pairof AnyField a) 48 (Rec 49 R2 50 (U (List (Pairof 'd AnyType) (Pairof 'e AnyType)) 51 (Pairof (Pairof 'b AnyType) (Pairof (Pairof 'c AnyType) R2)))))))) 52 53 (check-same-type 54 (Π :a(.b.c(.w)*.x.y)*.d.e) 55 (Rec 56 R1 57 (U (Pairof Any R1) 58 (Pairof 59 (Pairof AnyField a) 60 (Rec 61 R2 62 (U (List (Pairof 'd AnyType) (Pairof 'e AnyType)) 63 (Pairof 64 (Pairof 'b AnyType) 65 (Pairof 66 (Pairof 'c AnyType) 67 (Rec 68 R3 69 (U (Pairof (Pairof 'w AnyType) R3) 70 (Pairof 71 (Pairof 'x AnyType) 72 (Pairof (Pairof 'y AnyType) R2)))))))))))) 73 74 ;; TODO: test with deeper nesting of ()* 75 76 (check-same-type 77 (Invariant :a(.b.c(.w)*.x.y)*.d.e ≡ :a(.b.c)*.d.e) 78 (Invariant :a(.b.c(.w)*.x.y)*.d.e ≡ :a(.b.c)*.d.e)) 79 80 (check-same-type 81 (Invariant :a(.b.c(.w)*.x.y)*.d.e 82 ∈ 83 :a(.b.c)*.d.e) 84 (Invariant :a(.b.c)*.d.e 85 ∋ 86 :a(.b.c(.w)*.x.y)*.d.e)) 87 88 89 ;;; 90 91 (check-ann witness-value (Invariants)) ;; No invariants 92 (check-ann witness-value (Invariants (:a ≡ :a.b.c))) 93 94 (check-a-stronger-than-b (Invariants (:a ≡ :a.b.c)) 95 (Invariants)) 96 (check-a-same-as-b (Invariants (:a ≡ :a.b.c)) 97 (Invariants (:a.b.c ≡ :a))) 98 (check-a-stronger-than-b (Invariants (: ≡ :b.c) 99 (: ≡ :b.d)) 100 (Invariants (: ≡ :b.c))) 101 (check-a-stronger-than-b (Invariants (: ≡ :b.d) 102 (: ≡ :b.c)) 103 (Invariants (: ≡ :b.c))) 104 105 ;; ∀ .b.d(.a.b.>d)* of length ≥ 5 106 ;; is stronger than 107 ;; ∀ .b.d(.a.b.>d)* of length ≥ 8 108 ;; as the elements of the latter are included in the former, but 109 ;; the first element (length = 5) is missing in the latter, so the 110 ;; former constrains more paths. 111 (check-a-stronger-than-b (Invariants (: ≡ .b.d(.a.b.d)*)) 112 (Invariants (: ≡ .b.d.a.b.d(.a.b.d)*))) 113 114 (check-a-stronger-than-b (Invariants (: ≡ .a.b.c(.d.e)*)) 115 (Invariants (: ≡ .a.b.c.d.e))) 116 117 118 (check-a-stronger-than-b (Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 3))) 119 (Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 2)))) 120 121 (check-a-stronger-than-b (Invariants (.l ≥ (+ (length .a.b.c(.d.e)*) 1))) 122 (Invariants (.l ≥ (length .a.b.c(.d.e)*)))) 123 124 (check-a-stronger-than-b (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 2))) 125 (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 3)))) 126 127 (check-a-stronger-than-b (Invariants (.l ≤ (length .a.b.c(.d.e)*))) 128 (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 1)))) 129 130 (check-a-stronger-than-b (Invariants (.l = (length .a.b.c(.d.e)*))) 131 (Invariants (.l ≥ (length .a.b.c(.d.e)*)))) 132 133 (check-a-stronger-than-b (Invariants (.l = (+ (length .a.b.c(.d.e)*) 1))) 134 (Invariants (.l ≤ (+ (length .a.b.c(.d.e)*) 1)))) 135 136 (check-same-type (Invariants (.l = (length .a.b.c(.d.e)*))) 137 (Invariants (.l = (+ (length .a.b.c(.d.e)*) 0)))) 138 139 (check-a-stronger-than-b (Invariants (:a.l ≥ (+ (length :a.f.g) 3)) 140 (:a ≡ :a.f.h) 141 (:a ∉ :a.f.g)) 142 (Invariants (:a.l ≥ (+ (length :a.f.g) 2)) 143 (:a ≢ :a.f.g.0) 144 (:a ≢ :a.f.g.1)))