commit 6221a5db83d7ea37dfb7399a57ae7c2273980ec5
parent 5cc510ebf6cb194411211e24b1cfc3b10d87df57
Author: Georges Dupéron <georges.duperon@gmail.com>
Date: Sun, 14 May 2017 03:50:35 +0200
Implementation for a version of the poly constructor
Diffstat:
2 files changed, 107 insertions(+), 22 deletions(-)
diff --git 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
@@ -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
