Implemented builder-f, cleanup.
This commit is contained in:
Georges Dupéron
parent
e3074a37e4
commit
8f13786bf0
|
|
@ -1,100 +1,13 @@
|
||||||
#lang type-expander
|
#lang type-expander
|
||||||
(require (lib "phc-graph/flexible-with-generalized-ctor.hl.rkt"))
|
(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))))
|
(builder-f f 4 2)
|
||||||
(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))))))
|
|
||||||
|#
|
|
||||||
|
|
||||||
#|
|
#;((inst f propagate-τ '|1| Number '|3| String)
|
||||||
(: g (∀ (A) (case→ [→ (Some A) A]
|
oracle '|1| 100 '|3| "bee")
|
||||||
[→ (None Any) 'none])))
|
|
||||||
(define (g a)
|
|
||||||
(if (Some? a)
|
|
||||||
(Some-f a)
|
|
||||||
'none))
|
|
||||||
|#
|
|
||||||
|
|
||||||
|
(builder-f g 8 3)
|
||||||
|
|
||||||
|
#;((inst g propagate-τ '|1| Number '|3| String '|7| Symbol)
|
||||||
|
oracle '|1| 100 '|3| "bee" '|7| 'buzz)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; 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))))])))
|
|
||||||
|
|
@ -10,10 +10,9 @@
|
||||||
꩜chunk[<*>
|
꩜chunk[<*>
|
||||||
(provide builder-τ
|
(provide builder-τ
|
||||||
None
|
None
|
||||||
Some
|
propagate-τ
|
||||||
Some?
|
oracle
|
||||||
Some-f
|
builder-f)
|
||||||
propagate-τ)
|
|
||||||
|
|
||||||
(require racket/require
|
(require racket/require
|
||||||
(for-syntax (subtract-in racket/base subtemplate/override)
|
(for-syntax (subtract-in racket/base subtemplate/override)
|
||||||
|
|
@ -23,8 +22,7 @@
|
||||||
subtemplate/override)
|
subtemplate/override)
|
||||||
(for-meta 2 racket/base))
|
(for-meta 2 racket/base))
|
||||||
|
|
||||||
(struct (T) Some ([f : T]))
|
(struct (T) None ([f : (Promise T)]))
|
||||||
(struct (T) None ([f : T]))
|
|
||||||
|
|
||||||
(define-type-expander BinaryTree
|
(define-type-expander BinaryTree
|
||||||
(syntax-parser
|
(syntax-parser
|
||||||
|
|
@ -32,20 +30,11 @@
|
||||||
;; TODO: implement BinaryTree.
|
;; TODO: implement BinaryTree.
|
||||||
#'(List leafⱼ …)]))
|
#'(List leafⱼ …)]))
|
||||||
|
|
||||||
(define-syntax (def-SomeNone* stx)
|
<propagate-τ>
|
||||||
(syntax-case stx ()
|
<oracle-τ>
|
||||||
[(_ Some n)
|
<oracle>
|
||||||
(with-syntax ([(Someᵢ …) (map (λ (i) (format-id #'Some "Some~a" i))
|
|
||||||
(range n))])
|
|
||||||
#`(begin
|
|
||||||
(provide Someᵢ …)
|
|
||||||
(struct (T) Someᵢ Some ()) …))]))
|
|
||||||
|
|
||||||
(def-SomeNone* Some 4)
|
|
||||||
|
|
||||||
<builder-τ>
|
<builder-τ>
|
||||||
|
<builder-f>]
|
||||||
<propagate-τ>]
|
|
||||||
|
|
||||||
We first define the builder function's type. Since this type is rather
|
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.
|
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[|<Some or None>|
|
꩜chunk[|<Some or None>|
|
||||||
(U |<(Some Xⱼ) if Kⱼ = NSymᵢ>|
|
(U |<(Some Xⱼ) if Kⱼ = NSymᵢ>|
|
||||||
|<None if ∀ k ∈ Kⱼ, k ≠ NSymᵢ>|)]
|
|<None if ∀ k ∈ Kⱼ , k ≠ NSymᵢ>|)]
|
||||||
|
|
||||||
This type-level conditional is achieved via a trick involving intersection
|
This type-level conditional is achieved via a trick involving intersection
|
||||||
types. The ꩜racket[Kⱼ] type should be a singleton type containing exactly one
|
types. The ꩜racket[Kⱼ] type should be a singleton type containing exactly one
|
||||||
|
|
@ -110,14 +99,14 @@ pair.
|
||||||
|
|
||||||
꩜chunk[|<(Some Xⱼ) if Kⱼ = NSymᵢ>|
|
꩜chunk[|<(Some Xⱼ) if Kⱼ = NSymᵢ>|
|
||||||
(Pairof (∩ Kᵢⱼ 'NSymᵢⱼ)
|
(Pairof (∩ Kᵢⱼ 'NSymᵢⱼ)
|
||||||
(Some Xᵢⱼ))
|
Xᵢⱼ)
|
||||||
…]
|
…]
|
||||||
|
|
||||||
where ꩜racket[Kᵢⱼ], ꩜racket[Xᵢⱼ] and ꩜racket[NSymᵢⱼ] are defined as follows:
|
where ꩜racket[Kᵢⱼ], ꩜racket[Xᵢⱼ] and ꩜racket[NSymᵢⱼ] are defined as follows:
|
||||||
|
|
||||||
꩜chunk[<builder-τ-with-3>
|
꩜chunk[<builder-τ-with-3>
|
||||||
#:with ((Kᵢⱼ …) …) (map (const (Kⱼ …)) (Nᵢ …))
|
#:with ((Kᵢⱼ …) …) (map (const #'(Kⱼ …)) (Nᵢ …))
|
||||||
#:with ((Xᵢⱼ …) …) (map (const (Xⱼ …)) (Nᵢ …))
|
#:with ((Xᵢⱼ …) …) (map (const #'(Xⱼ …)) (Nᵢ …))
|
||||||
#:with ((NSymᵢⱼ …) …) (map λni.(map (const ni) (Xⱼ …)) (NSymᵢ …))]
|
#:with ((NSymᵢⱼ …) …) (map λni.(map (const ni) (Xⱼ …)) (NSymᵢ …))]
|
||||||
|
|
||||||
We use this fact to construct a pair above. Its first element is either
|
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[Kⱼ] equal to ꩜racket[Nᵢ], and be the list of symbols
|
||||||
꩜racket[(List . exceptᵢ)] otherwise.
|
꩜racket[(List . exceptᵢ)] otherwise.
|
||||||
|
|
||||||
꩜chunk[|<None if ∀ k ∈ Kⱼ, k ≠ NSymᵢ>|
|
꩜chunk[|<None if ∀ k ∈ Kⱼ , k ≠ NSymᵢ>|
|
||||||
(Pairof 'NSymᵢ
|
(None (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …))]
|
||||||
(None (List {∩ Kᵢⱼ {U 'exceptᵢⱼ …}} …)))]
|
|
||||||
|
|
||||||
This approach relies on the fact that occurrences of ꩜racket[Nothing] within
|
This approach relies on the fact that occurrences of ꩜racket[Nothing] within
|
||||||
structs and pairs containing collapse the entire struct or pair type to
|
structs and pairs containing collapse the entire struct or pair type to
|
||||||
|
|
@ -192,9 +180,8 @@ instantiated.
|
||||||
|
|
||||||
꩜chunk[<propagate-τ>
|
꩜chunk[<propagate-τ>
|
||||||
(define-type propagate-τ
|
(define-type propagate-τ
|
||||||
(Pairof Any
|
(U (Pairof Any Any)
|
||||||
(U (None (Listof Natural))
|
(None (Listof Any))))]
|
||||||
(Some Any))))]
|
|
||||||
|
|
||||||
꩜;Use chunkref instead of ꩜racket[|<Some or None>|] ?
|
꩜;Use chunkref instead of ꩜racket[|<Some or None>|] ?
|
||||||
|
|
||||||
|
|
@ -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
|
꩜racket[(∩ A B)], where ꩜racket[B] is the original type of the value to
|
||||||
upgrade.
|
upgrade.
|
||||||
|
|
||||||
꩜chunk[<oracle-type>
|
꩜chunk[<oracle-τ>
|
||||||
(∀ (B) (→ (∩ B
|
(define-type (oracle-τ A)
|
||||||
(Pairof Any (U (Some Any) (None (Listof Any)))))
|
(∀ (B) (→ (∩ B
|
||||||
(∩ A 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 (oracle-τ propagate-τ))
|
||||||
|
(define (oracle v) v)]
|
||||||
|
|
||||||
|
We update the builder function type to accept an extra argument for the
|
||||||
|
oracle:
|
||||||
|
|
||||||
꩜hlite[|<builder-function-type''>|
|
꩜hlite[|<builder-function-type''>|
|
||||||
{/(∀(_ _ _)(→ + _ _ / _ _ ooo _))}
|
{/(∀(_ _ _)(→ + _ _ / _ _ ooo _))}
|
||||||
(∀ (A {?@ Kⱼ Xⱼ} …)
|
(∀ (A {?@ Kⱼ Xⱼ} …)
|
||||||
(→ (code:comment "; Oracle:")
|
(→ (code:comment "; Oracle:")
|
||||||
<oracle-type>
|
(oracle-τ A)
|
||||||
(code:comment "; Keys and values:")
|
(code:comment "; Keys and values:")
|
||||||
{?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
|
{?@ (∩ Kⱼ (U 'NSymⱼᵢ …)) Xⱼ} …
|
||||||
;; Result type:
|
;; Result type:
|
||||||
|
|
@ -228,3 +224,30 @@ The builder function type is updated as follows:
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
꩜chunk[<builder-f>
|
||||||
|
(define-syntax builder-f
|
||||||
|
(syntax-parser
|
||||||
|
[(_ name n m)
|
||||||
|
<builder-τ-with-1>
|
||||||
|
<builder-τ-with-2>
|
||||||
|
<builder-τ-with-3>
|
||||||
|
<builder-τ-with-4>
|
||||||
|
#'(begin |<builder-function-implementation>|)]))]
|
||||||
|
|
||||||
|
꩜chunk[<builder-τ-with-4>
|
||||||
|
#:with ((kᵢⱼ …) …) (map (const #'(kⱼ …)) (Nᵢ …))
|
||||||
|
#:with ((xᵢⱼ …) …) (map (const #'(xⱼ …)) (Nᵢ …))]
|
||||||
|
|
||||||
|
꩜chunk[<builder-function-implementation>
|
||||||
|
(: name |<builder-function-type''>| #;(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ᵢⱼ …))))])
|
||||||
|
…))]
|
||||||
Loading…
Reference in New Issue
Block a user