From 36d6630906017ec62c323059cba4eca459e59096 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Fri, 12 May 2017 22:05:20 +0200 Subject: [PATCH] =?UTF-8?q?Managed=20to=20force=20TR=20to=20propagate=20No?= =?UTF-8?q?thing=20types=20(by=20intersecting=20with=20a=20(=E2=88=80)=20t?= =?UTF-8?q?ype=20which=20has=20the=20same=20shape=20as=20the=20desired=20o?= =?UTF-8?q?ne,=20deep=20enough=20to=20cause=20the=20containers=20of=20Noth?= =?UTF-8?q?ing=20types=20to=20be=20re-examined?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- flexible-with-generalized-ctor-test.rkt | 26 ++++++ flexible-with-generalized-ctor.hl.rkt | 101 +++++++----------------- 2 files changed, 55 insertions(+), 72 deletions(-) create mode 100644 flexible-with-generalized-ctor-test.rkt diff --git a/flexible-with-generalized-ctor-test.rkt b/flexible-with-generalized-ctor-test.rkt new file mode 100644 index 0000000..d793b76 --- /dev/null +++ b/flexible-with-generalized-ctor-test.rkt @@ -0,0 +1,26 @@ +#lang type-expander +(require (lib "phc-graph/flexible-with-generalized-ctor.hl.rkt")) +(define-type τ-4-2 (builder-τ 4 2)) +(: f τ-4-2) +(define (f kx x ky y) + (error "Not Yet")) +(define-syntax-rule (F KX X KY Y) + (inst f propagate-τ + KX X KY Y)) +(ann (F 0 Number 1 String) + (-> 0 Number 1 String + (List + (Pairof Zero (Some Number)) + (Pairof One (Some String)) + (Pairof 2 (None (List Zero One))) + (Pairof 3 (None (List Zero One)))))) + + +#| +(: g (∀ (A) (case→ [→ (Some A) A] + [→ (None Any) 'none]))) +(define (g a) + (if (Some? a) + (Some-f a) + 'none)) +|# \ No newline at end of file diff --git a/flexible-with-generalized-ctor.hl.rkt b/flexible-with-generalized-ctor.hl.rkt index fdd1876..b1d31c3 100644 --- a/flexible-with-generalized-ctor.hl.rkt +++ b/flexible-with-generalized-ctor.hl.rkt @@ -9,7 +9,7 @@ Some Some? Some-f - N/S) + propagate-τ) (require racket/require (for-syntax (subtract-in racket/base subtemplate/override) @@ -17,9 +17,8 @@ racket/function subtemplate/override)) -(struct N/S ()) -(struct (T) Some N/S ([f : T])) -(struct (T) None N/S ([f : T])) +(struct (T) Some ([f : T])) +(struct (T) None ([f : T])) (define-type-expander BinaryTree (syntax-parser @@ -35,6 +34,7 @@ #: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 Ms (Mⱼ …)) ;(define/with-syntax exceptⱼ (remove Mⱼ Ns)) … @@ -45,81 +45,38 @@ ((map (const (remove Nᵢ Ns)) Ms) …)) #'(∀ (A (?@ Kⱼ Xⱼ) …) - (→ A - (?@ Kⱼ Xⱼ) … + (→ (?@ (∩ Kⱼ (U Nⱼᵢ …)) Xⱼ) … (BinaryTree - (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ᵢⱼ}} …)) - A)) - (∩ (Pairof Kᵢⱼ (Some Xᵢⱼ)) - (Pairof Nᵢⱼ A)) - …) + (∩ (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ᵢⱼ}} …))) + (∩ (Pairof Kᵢⱼ (Some Xᵢⱼ)) + (Pairof Nᵢⱼ Any)) + …) + A) …)))])) -; ../../../.racket/snapshot/pkgs/typed-racket-lib/typed-racket/types/overlap.rkt:40:0: mask-accessor: contract violation +(define-type propagate-τ + (Pairof Natural + (U (None (Listof Natural)) + (Some Any)))) + +; ../../../.racket/snapshot/pkgs/typed-racket-lib/typed-racket/types/overlap.rkt +;:40:0: mask-accessor: contract violation ; expected: mask? ; given: #f ;(define-type τ-4-2 (builder-τ 4 2)) -(define-type t-4-2 - (All (A 0/K 0/X 1/K 1/X) - (-> A - 0/K - 0/X - 1/K - 1/X - (List - (U (Pairof (∩ 0/K Zero) (∩ (Some 0/X) A)) - (Pairof (∩ 1/K Zero) (∩ (Some 1/X) A)) - (Pairof - Zero - (∩ - (None - (List - (U (∩ 0/K 2) (∩ 0/K 3) (∩ 0/K One)) - (U (∩ 1/K 2) (∩ 1/K 3) (∩ 1/K One)))) - A))) - (U (Pairof (∩ 0/K One) (∩ (Some 0/X) A)) - (Pairof (∩ 1/K One) (∩ (Some 1/X) A)) - (Pairof - One - (∩ - (None - (List - (U (∩ 0/K 2) (∩ 0/K 3) (∩ 0/K Zero)) - (U (∩ 1/K 2) (∩ 1/K 3) (∩ 1/K Zero)))) - A))) - (U (Pairof (∩ 0/K 2) (∩ (Some 0/X) A)) - (Pairof (∩ 1/K 2) (∩ (Some 1/X) A)) - (Pairof - 2 - (∩ - (None - (List - (U (∩ 0/K 3) (∩ 0/K One) (∩ 0/K Zero)) - (U (∩ 1/K 3) (∩ 1/K One) (∩ 1/K Zero)))) - A))) - (U (Pairof (∩ 0/K 3) (∩ (Some 0/X) A)) - (Pairof (∩ 1/K 3) (∩ (Some 1/X) A)) - (Pairof - 3 - (∩ - (None - (List - (U (∩ 0/K 2) (∩ 0/K One) (∩ 0/K Zero)) - (U (∩ 1/K 2) (∩ 1/K One) (∩ 1/K Zero)))) - A))))))) ;]