WIP

flexible-with-generalized-ctor-test.rkt

@@ -1,6 +1,7 @@
 #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"))
@@ -10,11 +11,11 @@
 (ann (F 0 Number 1 String)
      (-> 0 Number 1 String
          (List
-          (Pairof Zero (Some Number))
+          (Pairof Any (Some Number))
-          (Pairof One (Some String))
+          (Pairof Any (Some String))
-          (Pairof 2 (None (List Zero One)))
+          (Pairof Any (None (List Zero One)))
-          (Pairof 3 (None (List Zero One))))))
+          (Pairof Any (None (List Zero One))))))
-
+|#
 
 #|
 (: g (∀ (A) (case→ [→ (Some A) A]

flexible-with-generalized-ctor.hl.rkt

@@ -1,4 +1,4 @@
-#lang type-expander/lang
+#lang dotlambda/unhygienic type-expander/lang
 #|hyper-literate #:♦ #:no-auto-require (dotlambda/unhygienic
                                             . type-expander/lang)
 
@@ -9,16 +9,18 @@
          Some
          Some?
          Some-f
-         propagate-τ)
+         #;propagate-τ)
 
 (require racket/require
          (for-syntax (subtract-in racket/base subtemplate/override)
+                     syntax/stx
                      racket/list
                      racket/function
-                     subtemplate/override))
+                     subtemplate/override)
+         (for-meta 2 racket/base))
 
 (struct (T) Some ([f : T]))
-(struct (T) None ([f : T]))
+(struct None ())
 
 (define-type-expander BinaryTree
   (syntax-parser
@@ -26,48 +28,57 @@
      ;; TODO: implement BinaryTree.
      #'(List leafⱼ …)]))
 
+(define-syntax (def-SomeNone* stx)
+  (syntax-case stx ()
+    [(_ Some None 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 ()) …))]))
+
+(def-SomeNone* Some None 4)
+
 (define-type-expander builder-τ
   (syntax-parser
     [(_ n m)
      #:with (Nᵢ …) (range n)
      #:with (Mⱼ …) (range m)
-     #:with ((Kᵢⱼ …) …) (map (const (Kⱼ …)) (Nᵢ …))
+     #:with (Someᵢ …) (map (λ (n) (format-id #'HERE? "Some~a" n)) (Nᵢ …))
-     #:with ((Xᵢⱼ …) …) (map (const (Xⱼ …)) (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ⱼ …))
+     #:with ((Nⱼᵢ …) …) (map (const #'(Nᵢ …)) (Mⱼ …))
      (define Ns (Nᵢ …))
+     (define Nones (#'Noneᵢ …))
      (define Ms (Mⱼ …))
      ;(define/with-syntax exceptⱼ (remove Mⱼ Ns)) …
      ;     (define/with-syntax ((exceptᵢⱼ …) …)
      ;       (map (const (exceptⱼ …)) (Nᵢ …)))
-     (define/with-syntax (exceptᵢ …) ((remove Nᵢ Ns) …))
+     (define/with-syntax ((exceptᵢ …) …) ((remove Noneᵢ Nones) …))
      (define/with-syntax ((exceptᵢⱼ …) …)
-       ((map (const (remove Nᵢ Ns)) Ms) …))
+       ((map (const (remove #'Noneᵢ Nones free-identifier=?)) Ms) …))
 
+     (define/with-syntax result
        #'(∀ (A (?@ Kⱼ Xⱼ) …)
-          (→ (?@ (∩ Kⱼ (U Nⱼᵢ …)) Xⱼ) …
+            (→ (?@ (∩ Kⱼ (U None (Some Any))) Xⱼ) …
                (BinaryTree
-              (∩ (U (Pairof Nᵢ
+                (∩ (U (∩ Noneᵢ Kᵢⱼ …)
-                            ;; If Kⱼ is Nᵢ, then {∩ Kᵢⱼ {U . exceptᵢⱼ}} will
+                      (∩ Kᵢⱼ (Someᵢⱼ Xᵢⱼ))
-                            ;; 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)
-              …)))]))
+                …))))
+     (displayln (syntax->datum #'result))
+     #'result]))
 
-(define-type propagate-τ
+#;(define-type propagate-τ
-  (Pairof Natural
+    (Pairof Any
             (U (None (Listof Natural))
                (Some Any))))