thoughts.rkt (4530B)
1 #lang type-expander/lang 2 3 #| 4 Adding fields to the prefix path makes it weaker 5 Adding fields to the postfix path makes it stronger 6 7 (Expand prefix postfix) 8 => (and prefixᵢ postfix) … 9 Also could be expanded as: 10 => (and prefix postfixᵢ) … 11 12 Rewording ((u pre_x pre_x2) pre_a _ post_b (u post_c post_c2) 13 => property holds iff 14 pre1 = a 15 and (pre2 = x or pre2 = x2) 16 and post1 = b 17 and (post2 = c or post2 = c2) 18 |# 19 20 (define-type (F A) (I (I A))) 21 (define-type (I A) (→ A Void)) 22 23 (define-type eqA1 (F (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) 24 (List (G 'b) (G 'c))))) 25 26 (define-type eqB1 (F (∩ (Pairof (List* (G 'a1) (∩ (G 'u1) (G 'u2))) 27 (List (G 'b) (G 'c))) 28 (Pairof (List* (G 'a2) (∩ (G 'u1) (G 'u2))) 29 (List (G 'b) (G 'c)))))) 30 31 (define-type eqC1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1))) 32 (List (G 'b) (G 'c))) 33 (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u2))) 34 (List (G 'b) (G 'c)))))) 35 36 (define-type weakerD1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1))) 37 (List (G 'b) (G 'c)))))) 38 39 (define-type strongerE1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) 40 (∩ (List (G 'b) (G 'c)) 41 (List (G 'b2) (G 'c))))))) 42 43 (define-type strongerF1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) 44 (Pairof (G 'b) (∩ (List (G 'c)) 45 (List (G 'c2)))))))) 46 47 (define-type altF1 (F (∩ (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) 48 (Pairof (G 'b) (List (G 'c)))) 49 (Pairof (List* (∩ (G 'a1) (G 'a2)) (∩ (G 'u1) (G 'u2))) 50 (Pairof (G 'b) (List (G 'c2))))))) 51 52 (ann (ann (λ (x) (void)) eqA1) eqB1) 53 (ann (ann (λ (x) (void)) eqA1) eqC1) 54 (ann (ann (λ (x) (void)) eqB1) eqA1) 55 (ann (ann (λ (x) (void)) eqB1) eqC1) 56 (ann (ann (λ (x) (void)) eqC1) eqA1) 57 (ann (ann (λ (x) (void)) eqC1) eqB1) 58 (ann (ann (λ (x) (void)) eqA1) weakerD1) 59 (ann (ann (λ (x) (void)) eqB1) weakerD1) 60 (ann (ann (λ (x) (void)) eqC1) weakerD1) 61 ;(ann (ann (λ (x) (void)) eqA1) strongerD1) ;; rejected, as it should 62 (ann (ann (λ (x) (void)) strongerE1) eqA1) 63 ;(ann (ann (λ (x) (void)) eqA1) strongerE1) ;; rejected, as it should 64 (ann (ann (λ (x) (void)) strongerF1) eqA1) 65 ;(ann (ann (λ (x) (void)) eqA1) strongerF1) ;; rejected, as it should 66 (ann (ann (λ (x) (void)) altF1) eqA1) 67 ;(ann (ann (λ (x) (void)) eqA1) altF1) ;; rejected, as it should 68 (ann (ann (λ (x) (void)) altF1) strongerF1) 69 (ann (ann (λ (x) (void)) strongerF1) altF1) 70 71 72 73 74 (let () 75 (define-type eqA2 (F (case→ (→ (List 'b 'c) 'a1) 76 (→ (List 'b 'c) 'a2)))) 77 78 (define-type eqB2 (F (case→ (→ (List 'b 'c) 79 (U 'a1 'a2))))) 80 81 (ann (ann (λ (x) (void)) eqA2) eqB2) 82 #;(ann (ann (λ (x) (void)) eqB2) eqA2)) 83 84 ;(let () 85 (define-type (G A) (F A)) 86 (define-type-expander (+ stx) (syntax-case stx () [(_ . rest) #'(∩ . rest)])) 87 (define-type-expander (* stx) (syntax-case stx () [(_ . rest) #'(U . rest)])) 88 89 (define-type eqA2 (F (+ (* (G 'b) (G 'c) (G 'a1)) 90 (* (G 'b) (G 'c) (G 'a2))))) 91 92 (define-type eqB2 (F (+ (* (G 'b) (G 'c) (+ (G 'a1) (G 'a2)))))) 93 94 (define-type Weaker2 (F (+ (* (G 'b) (G 'c) (G 'a1))))) 95 96 (ann (ann (λ (x) (void)) eqA2) eqB2) 97 (ann (ann (λ (x) (void)) eqB2) eqA2) 98 (ann (ann (λ (x) (void)) eqA2) Weaker2) 99 (ann (ann (λ (x) (void)) eqB2) Weaker2) 100 ;(ann (ann (λ (x) (void)) Weaker2) eqA2) 101 ;(ann (ann (λ (x) (void)) Weaker2) eqB2) 102 ;) 103 104 105 106 (let () 107 (define-type weaker3 108 (F (∩ (G (Rec R (List* 'a Any R))) 109 (G (Rec R (List* Any 'b R)))))) 110 (define-type stronger3 111 (F (∩ (G (List* 'a Any (Rec R (List* 'a Any R)))) 112 (G (List* Any 'b (Rec R (List* Any 'b R))))))) 113 114 (ann (ann (λ (x) (void)) stronger3) weaker3) 115 ) 116 117 #| 118 Put the U ∩ inside the positional list? 119 What about loops of different sizes => won't work 120 What about merging all the invariants blindly => won't work, but we can 121 special-case merging these regexp-like invariants, as long as the merging 122 doesn't need any info about the regexp itself 123 (e.g. all are "merge the second elements") 124 |#