From 8f13786bf00a22abf92eb974b0f44f7de3bf776e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Wed, 17 May 2017 16:31:08 +0200 Subject: [PATCH] Implemented builder-f, cleanup. --- flexible-with-generalized-ctor-test.rkt | 101 ++---------------------- flexible-with-generalized-ctor.hl.rkt | 93 ++++++++++++++-------- 2 files changed, 65 insertions(+), 129 deletions(-) diff --git a/flexible-with-generalized-ctor-test.rkt b/flexible-with-generalized-ctor-test.rkt index c4eb7ce..0b0176c 100644 --- a/flexible-with-generalized-ctor-test.rkt +++ b/flexible-with-generalized-ctor-test.rkt @@ -1,100 +1,13 @@ #lang type-expander (require (lib "phc-graph/flexible-with-generalized-ctor.hl.rkt")) -(define-type τ-4-2 (builder-τ 4 2)) +(provide f g) -#;(τ (U (Pairof Any (None (Listof (Some Any)))) - (Some Any)) - (Some0 Any) Number (Some1 Any) String) -#| -(: 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 Any (Some Number)) - (Pairof Any (Some String)) - (Pairof Any (None (List Zero One))) - (Pairof Any (None (List Zero One)))))) -|# +(builder-f f 4 2) -#| -(: g (∀ (A) (case→ [→ (Some A) A] - [→ (None Any) 'none]))) -(define (g a) - (if (Some? a) - (Some-f a) - 'none)) -|# +#;((inst f propagate-τ '|1| Number '|3| String) + oracle '|1| 100 '|3| "bee") +(builder-f g 8 3) - - - - - - - - - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Actual good implementation: - -;(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: -#;(Pairof Any (U (Some Any) (None (Listof Any)))) - -(: f (builder-τ 4 2)) - -(define (f oracle kx x ky y) - (list (cond - [((make-predicate '|0|) kx) - (ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|0| Any))) (cons kx (Some x))) - (∩ (Pairof 0/K (Some 0/X)) (Pairof '|0| Any) A))] - [((make-predicate '|0|) ky) - (ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|0| Any))) (cons ky (Some y))) - (∩ (Pairof 1/K (Some 1/X)) (Pairof '|0| Any) A))] - [else - ((inst oracle (Pairof '|0| (None (List (∩ 0/K (U '|1| '|2| '|3|)) (∩ 1/K (U '|1| '|2| '|3|)))))) - (cons '|0| (None (list kx ky))))]) - (cond - [((make-predicate '|1|) kx) - (ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|1| Any))) (cons kx (Some x))) - (∩ (Pairof 0/K (Some 0/X)) (Pairof '|1| Any) A))] - [((make-predicate '|1|) ky) - (ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|1| Any))) (cons ky (Some y))) - (∩ (Pairof 1/K (Some 1/X)) (Pairof '|1| Any) A))] - [else - ((inst oracle (Pairof '|1| (None (List (∩ 0/K (U '|0| '|2| '|3|)) (∩ 1/K (U '|0| '|2| '|3|)))))) - (cons '|1| (None (list kx ky))))]) - (cond - [((make-predicate '|2|) kx) - (ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|2| Any))) (cons kx (Some x))) - (∩ (Pairof 0/K (Some 0/X)) (Pairof '|2| Any) A))] - [((make-predicate '|2|) ky) - (ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|2| Any))) (cons ky (Some y))) - (∩ (Pairof 1/K (Some 1/X)) (Pairof '|2| Any) A))] - [else - ((inst oracle (Pairof '|2| (None (List (∩ 0/K (U '|0| '|1| '|3|)) (∩ 1/K (U '|0| '|1| '|3|)))))) - (cons '|2| (None (list kx ky))))]) - (cond - [((make-predicate '|3|) kx) - (ann ((inst oracle (∩ (Pairof 0/K (Some 0/X)) (Pairof '|3| Any))) (cons kx (Some x))) - (∩ (Pairof 0/K (Some 0/X)) (Pairof '|3| Any) A))] - [((make-predicate '|3|) ky) - (ann ((inst oracle (∩ (Pairof 1/K (Some 1/X)) (Pairof '|3| Any))) (cons ky (Some y))) - (∩ (Pairof 1/K (Some 1/X)) (Pairof '|3| Any) A))] - [else - ((inst oracle (Pairof '|3| (None (List (∩ 0/K (U '|0| '|1| '|2|)) (∩ 1/K (U '|0| '|1| '|2|)))))) - (cons '|3| (None (list kx ky))))]))) +#;((inst g propagate-τ '|1| Number '|3| String '|7| Symbol) + oracle '|1| 100 '|3| "bee" '|7| 'buzz) \ No newline at end of file diff --git a/flexible-with-generalized-ctor.hl.rkt b/flexible-with-generalized-ctor.hl.rkt index a97181f..ab8dd78 100644 --- a/flexible-with-generalized-ctor.hl.rkt +++ b/flexible-with-generalized-ctor.hl.rkt @@ -10,10 +10,9 @@ ꩜chunk[<*> (provide builder-τ None - Some - Some? - Some-f - propagate-τ) + propagate-τ + oracle + builder-f) (require racket/require (for-syntax (subtract-in racket/base subtemplate/override) @@ -23,8 +22,7 @@ subtemplate/override) (for-meta 2 racket/base)) - (struct (T) Some ([f : T])) - (struct (T) None ([f : T])) + (struct (T) None ([f : (Promise T)])) (define-type-expander BinaryTree (syntax-parser @@ -32,20 +30,11 @@ ;; TODO: implement BinaryTree. #'(List leafⱼ …)])) - (define-syntax (def-SomeNone* stx) - (syntax-case stx () - [(_ Some n) - (with-syntax ([(Someᵢ …) (map (λ (i) (format-id #'Some "Some~a" i)) - (range n))]) - #`(begin - (provide Someᵢ …) - (struct (T) Someᵢ Some ()) …))])) - - (def-SomeNone* Some 4) - + + + - - ] + ] We first define the builder function's type. Since this type is rather complex, we define it using a macro. The type expander takes two arguments. @@ -95,7 +84,7 @@ corresponding ꩜racket[Kⱼ] matches the leaf name, and ꩜racket[None] otherwi ꩜chunk[|| (U |<(Some Xⱼ) if Kⱼ = NSymᵢ>| - ||)] + ||)] This type-level conditional is achieved via a trick involving intersection types. The ꩜racket[Kⱼ] type should be a singleton type containing exactly one @@ -110,14 +99,14 @@ pair. ꩜chunk[|<(Some Xⱼ) if Kⱼ = NSymᵢ>| (Pairof (∩ Kᵢⱼ 'NSymᵢⱼ) - (Some Xᵢⱼ)) + Xᵢⱼ) …] where ꩜racket[Kᵢⱼ], ꩜racket[Xᵢⱼ] and ꩜racket[NSymᵢⱼ] are defined as follows: ꩜chunk[ - #:with ((Kᵢⱼ …) …) (map (const (Kⱼ …)) (Nᵢ …)) - #:with ((Xᵢⱼ …) …) (map (const (Xⱼ …)) (Nᵢ …)) + #:with ((Kᵢⱼ …) …) (map (const #'(Kⱼ …)) (Nᵢ …)) + #:with ((Xᵢⱼ …) …) (map (const #'(Xⱼ …)) (Nᵢ …)) #:with ((NSymᵢⱼ …) …) (map λni.(map (const ni) (Xⱼ …)) (NSymᵢ …))] We use this fact to construct a pair above. Its first element is either @@ -148,9 +137,8 @@ The resulting type should therefore be ꩜racket[Nothing] only if there is no ꩜racket[Kⱼ] equal to ꩜racket[Nᵢ], and be the list of symbols ꩜racket[(List . exceptᵢ)] otherwise. -꩜chunk[|| - (Pairof 'NSymᵢ - (None (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …)))] +꩜chunk[|| + (None (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …))] This approach relies on the fact that occurrences of ꩜racket[Nothing] within structs and pairs containing collapse the entire struct or pair type to @@ -192,9 +180,8 @@ instantiated. ꩜chunk[ (define-type propagate-τ - (Pairof Any - (U (None (Listof Natural)) - (Some Any))))] + (U (Pairof Any Any) + (None (Listof Any))))] ꩜;Use chunkref instead of ꩜racket[||] ? @@ -209,18 +196,27 @@ an ꩜racket[oracle] function, which transforms an element with the type ꩜racket[(∩ A B)], where ꩜racket[B] is the original type of the value to upgrade. -꩜chunk[ - (∀ (B) (→ (∩ B - (Pairof Any (U (Some Any) (None (Listof Any))))) - (∩ A B)))] +꩜chunk[ + (define-type (oracle-τ A) + (∀ (B) (→ (∩ B + (U (Pairof Any Any) + (None (Listof Any)))) + (∩ A B))))] -The builder function type is updated as follows: +The oracle does nothing more than return its argument unchanged: + +꩜chunk[ + (: oracle (oracle-τ propagate-τ)) + (define (oracle v) v)] + +We update the builder function type to accept an extra argument for the +oracle: ꩜hlite[|| {/(∀(_ _ _)(→ + _ _ / _ _ ooo _))} (∀ (A {?@ Kⱼ Xⱼ} …) (→ (code:comment "; Oracle:") - + (oracle-τ A) (code:comment "; Keys and values:") {?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} … ;; Result type: @@ -228,3 +224,30 @@ The builder function type is updated as follows: + + +꩜chunk[ + (define-syntax builder-f + (syntax-parser + [(_ name n m) + + + + + #'(begin ||)]))] + +꩜chunk[ + #:with ((kᵢⱼ …) …) (map (const #'(kⱼ …)) (Nᵢ …)) + #:with ((xᵢⱼ …) …) (map (const #'(xⱼ …)) (Nᵢ …))] + +꩜chunk[ + (: name || #;(builder-τ n m)) + (define (name oracle {?@ kⱼ xⱼ} …) + (list (cond + [((make-predicate 'NSymᵢⱼ) kᵢⱼ) + ((inst oracle (Pairof (∩ Kᵢⱼ 'NSymᵢⱼ) Xᵢⱼ)) (cons kᵢⱼ xᵢⱼ))] + … + [else + ((inst oracle (None (List (∩ Kᵢⱼ (U 'exceptᵢⱼ …)) …))) + (None (delay (list kᵢⱼ …))))]) + …))] \ No newline at end of file