diff --git a/flexible-with-generalized-ctor-test.rkt b/flexible-with-generalized-ctor-test.rkt index 075ce63..6cf65c6 100644 --- a/flexible-with-generalized-ctor-test.rkt +++ b/flexible-with-generalized-ctor-test.rkt @@ -1,6 +1,10 @@ #lang type-expander (require (lib "phc-graph/flexible-with-generalized-ctor.hl.rkt")) (define-type τ-4-2 (builder-τ 4 2)) + +#;(τ (U (Pairof Any (None (Listof (Some Any)))) + (Some Any)) + (Some0 Any) Number (Some1 Any) String) #| (: f τ-4-2) (define (f kx x ky y) @@ -24,4 +28,78 @@ (if (Some? a) (Some-f a) 'none)) -|# \ No newline at end of file +|# + +(struct (A) Some ([f : A]) #:transparent) +(struct (A) Some0 Some () #:transparent) +(struct (A) Some1 Some () #:transparent) +(struct (A) Some2 Some () #:transparent) +(struct (A) Some3 Some () #:transparent) +(struct (A) None ([f : A]) #:transparent) + +;; A is: +#;(U (Pairof Any (None (Listof (Some Any)))) + (Some Any)) + +(struct |0| ()) +(struct |1| ()) +(struct |2| ()) +(struct |3| ()) + +(: f (∀ (A 0/K 0/X 1/K 1/X) + (→ (∩ 0/K (U |0| |1| |2| |3|)) + 0/X + (∩ 1/K (U |0| |1| |2| |3|)) + 1/X + (List + (∩ + (U + (Pairof |0| (None (List (∩ 0/K (U |1| |2| |3|)) (∩ 1/K (U |1| |2| |3|))))) + (∩ (Pairof 0/K (Some 0/X)) (Pairof |0| Any)) + (∩ (Pairof 1/K (Some 1/X)) (Pairof |0| Any))) + A) + (∩ + (U + (Pairof |1| (None (List (∩ 0/K (U |0| |2| |3|)) (∩ 1/K (U |0| |2| |3|))))) + (∩ (Pairof 0/K (Some 0/X)) (Pairof |1| Any)) + (∩ (Pairof 1/K (Some 1/X)) (Pairof |1| Any))) + A) + (∩ + (U + (Pairof |2| (None (List (∩ 0/K (U |0| |1| |3|)) (∩ 1/K (U |0| |1| |3|))))) + (∩ (Pairof 0/K (Some 0/X)) (Pairof |2| Any)) + (∩ (Pairof 1/K (Some 1/X)) (Pairof |2| Any))) + A) + (∩ + (U + (Pairof |3| (None (List (∩ 0/K (U |0| |1| |2|)) (∩ 1/K (U |0| |1| |2|))))) + (∩ (Pairof 0/K (Some 0/X)) (Pairof |3| Any)) + (∩ (Pairof 1/K (Some 1/X)) (Pairof |3| Any))) + A))))) + +(define (f kx x ky y) + (list (cond + [((make-predicate |0|) kx) (cons kx (Some x))] + [((make-predicate |0|) ky) (cons ky (Some y))] + [else (cons |0| (None (list kx ky)))]) + (cond + [((make-predicate |1|) kx) (cons kx (Some x))] + [((make-predicate |1|) ky) (cons ky (Some y))] + [else (cons |1| (None (list kx ky)))]) + (cond + [((make-predicate |2|) kx) (cons kx (Some x))] + [((make-predicate |2|) ky) (cons ky (Some y))] + [else (cons |2| (None (list kx ky)))]) + (cond + [((make-predicate |3|) kx) (cons kx (Some x))] + [((make-predicate |3|) ky) (cons ky (Some y))] + [else (cons |3| (None (list kx ky)))])) + ((λ () (error "not yet")))) + + + + + + + + diff --git a/flexible-with-generalized-ctor.hl.rkt b/flexible-with-generalized-ctor.hl.rkt index d82f607..dbdfcc0 100644 --- a/flexible-with-generalized-ctor.hl.rkt +++ b/flexible-with-generalized-ctor.hl.rkt @@ -9,7 +9,7 @@ Some Some? Some-f - #;propagate-τ) + propagate-τ) (require racket/require (for-syntax (subtract-in racket/base subtemplate/override) @@ -20,7 +20,7 @@ (for-meta 2 racket/base)) (struct (T) Some ([f : T])) -(struct None ()) +(struct (T) None ([f : T])) (define-type-expander BinaryTree (syntax-parser @@ -30,17 +30,14 @@ (define-syntax (def-SomeNone* stx) (syntax-case stx () - [(_ Some None n) + [(_ Some n) (with-syntax ([(Someᵢ …) (map (λ (i) (format-id #'Some "Some~a" i)) - (range n))] - [(Noneᵢ …) (map (λ (i) (format-id #'None "None~a" i)) (range n))]) #`(begin - (provide Someᵢ … Noneᵢ …) - (struct (T) Someᵢ Some ()) … - (struct Noneᵢ None ()) …))])) + (provide Someᵢ …) + (struct (T) Someᵢ Some ()) …))])) -(def-SomeNone* Some None 4) +(def-SomeNone* Some 4) (define-type-expander builder-τ (syntax-parser @@ -49,27 +46,38 @@ #:with (Mⱼ …) (range m) #:with (Someᵢ …) (map (λ (n) (format-id #'HERE? "Some~a" n)) (Nᵢ …)) #:with ((Someᵢⱼ …) …) (map λ.(map (const %) (Mⱼ …)) (#'Someᵢ …)) - #:with (Noneᵢ …) (map (λ (n) (format-id #'HERE? "None~a" n)) (Nᵢ …)) ;#:with ((Noneᵢⱼ …) …) (map (const #'(Noneᵢ …)) (Nᵢ …)) #:with ((Kᵢⱼ …) …) (map (const #'(Kⱼ …)) (Nᵢ …)) #:with ((Xᵢⱼ …) …) (map (const #'(Xⱼ …)) (Nᵢ …)) #:with ((Nᵢⱼ …) …) (map (λ (ni) (map (const ni) (Xⱼ …))) (Nᵢ …)) #:with ((Nⱼᵢ …) …) (map (const #'(Nᵢ …)) (Mⱼ …)) (define Ns (Nᵢ …)) - (define Nones (#'Noneᵢ …)) (define Ms (Mⱼ …)) + (define Somes (Someᵢ …)) ;(define/with-syntax exceptⱼ (remove Mⱼ Ns)) … ; (define/with-syntax ((exceptᵢⱼ …) …) ; (map (const (exceptⱼ …)) (Nᵢ …))) - (define/with-syntax ((exceptᵢ …) …) ((remove Noneᵢ Nones) …)) - (define/with-syntax ((exceptᵢⱼ …) …) - ((map (const (remove #'Noneᵢ Nones free-identifier=?)) Ms) …)) + (define/with-syntax (exceptᵢ …) ((remove Nᵢ Ns) …)) + (define/with-syntax (((exceptᵢⱼ …) …) …) + ((map (const (remove Someᵢ Somes)) Ms) …)) (define/with-syntax result #'(∀ (A (?@ Kⱼ Xⱼ) …) - (→ (?@ (∩ Kⱼ (U None (Some Any))) Xⱼ) … + (→ (?@ (∩ Kⱼ (Some Any)) (∩ Kⱼ Xⱼ)) … (BinaryTree - (∩ (U (∩ Noneᵢ Kᵢⱼ …) + (∩ (U (Pairof Nᵢ + ;; If Kⱼ is Nᵢ, then {∩ Kᵢⱼ {U . exceptᵢⱼ}} will + ;; Nothing. We multiply the Nothing together by + ;; building a List out of them (a single occurrence + ;; of Nothing should collapse the list), so that the + ;; result should be Nothing only if there is no Kⱼ + ;; equal to Nᵢ. To force TR to propagate Nothing as + ;; much as possible, we intersect it with + ;; (None Any), which should be a no-op, but makes + ;; sure the simplifier which runs with ∩ kicks in. + ;; Therefore, the (None whatever) should appear only + ;; if there is indeed no key provided for that leaf. + (None (List {∩ Kᵢⱼ {U (exceptᵢⱼ Any) …}} …))) (∩ Kᵢⱼ (Someᵢⱼ Xᵢⱼ)) …) A) @@ -77,10 +85,10 @@ (displayln (syntax->datum #'result)) #'result])) -#;(define-type propagate-τ - (Pairof Any - (U (None (Listof Natural)) - (Some Any)))) +(define-type propagate-τ + (Pairof Any + (U (None (Listof Natural)) + (Some Any)))) ; ../../../.racket/snapshot/pkgs/typed-racket-lib/typed-racket/types/overlap.rkt ;:40:0: mask-accessor: contract violation