notes about data and adding theory & model

remix/data0.rkt

@@ -104,6 +104,9 @@
               #:methods remix:gen:dot-transformer
               [(define (dot-transform _ stx)
                  (syntax-parse stx
+                   [(_dot me:id (x:interface-member . args))
+                    (quasisyntax/loc stx
+                      (remix:#%app (remix:#%app (remix:#%dot me x)) . args))]
                    [(_dot me:id x:interface-member)
                     (get-rhs-id stx #'x)]
                    [(_dot me:id . (~and x+more (x:interface-member . more)))
@@ -115,6 +118,11 @@
               #:methods remix:gen:app-dot-transformer
               [(define (app-dot-transform _ stx)
                  (syntax-parse stx
+                   [(_app (_dot me:id (x:interface-member . args)) . body)
+                    (quasisyntax/loc stx
+                      (remix:#%app
+                       (remix:#%app (remix:#%app (remix:#%dot me x)) . args)
+                       . body))]
                    [(_app (_dot me:id x:interface-member) . body)
                     (quasisyntax/loc stx
                       (#,(get-rhs-id stx #'x) . body))]
@@ -417,5 +425,42 @@
          layout-immutable
          layout-mutable)
 
+;; theory & model
+
+(define-syntax theory
+  (singleton-struct
+   #:property prop:procedure
+   (λ (_ stx)
+     (raise-syntax-error 'theory "Illegal outside def" stx))
+   #:methods remix:gen:def-transformer
+   [(define (def-transform _ stx)
+      (syntax-parse stx
+        #:literals (remix:#%brackets remix:def theory)
+        [(remix:def (remix:#%brackets theory thy:id)
+                    v:id ...)
+         (syntax/loc stx
+           (remix:def (remix:#%brackets phase0:layout thy)
+                      v ...))]))]))
+
+(define-syntax model
+  (singleton-struct
+   #:property prop:procedure
+   (λ (_ stx)
+     (raise-syntax-error 'model "Illegal outside def" stx))
+   #:methods remix:gen:def-transformer
+   [(define (def-transform _ stx)
+      (syntax-parse stx
+        #:literals (remix:#%brackets remix:def model)
+        [(remix:def (remix:#%brackets model thy:id mod:id)
+                    (remix:#%brackets f:id v:expr) ...)
+         (syntax/loc stx
+           (remix:def (remix:#%brackets thy mod)
+                      (remix:#%app
+                       (remix:#%dot thy #:alloc)
+                       (remix:#%brackets f v) ...)))]))]))
+
+(provide theory
+         model)
+
 ;; xxx (dynamic-)interface
 ;; xxx data

remix/stx0.rkt

@@ -199,15 +199,18 @@
      #:declare dt (static dot-transformer? "dot transformer")
      (dot-transform (attribute dt.value) stx)]))
 
+;; XXX This should work differently... add a method to dot-transformer
+;; that has a sensible default and let it pass out a def block to put
+;; around the apply.
 (begin-for-syntax
   (define-generics app-dot-transformer
     (app-dot-transform app-dot-transformer stx)))
 (define-syntax (remix-#%app stx)
   (syntax-parse stx
     #:literals (#%dot)
-    [(_ (#%dot x ... (#%dot y ...)) . body)
+    [(_ (#%dot x ... (#%dot . y)) . body)
      (syntax/loc stx
-       (remix-#%app (#%dot x ... y ...) . body))]
+       (remix-#%app (#%dot x ... . y) . body))]
     [(_ (#%dot adt . (~not (x ... (#%dot . _) . _))) . body)
      #:declare adt (static app-dot-transformer? "app-dot transformer")
      (app-dot-transform (attribute adt.value) stx)]

remix/tests/data-ramble.rkt

@@ -1,16 +1,4 @@
 ;; THEORIES + MODELS
-;; A theory is a specification of some values
-(def [theory Monoid]
-  op id)
-;; XXX specify properties
-
-;; A model is an object that satisfies the theory
-(def zero 0)
-(def [model Monoid Nat+Monoid]
-  [op +]
-  ;; XXX lift non-identifiers
-  [id zero])
-;; XXX verify properties
 
 ;; INTERFACES + OBJECTS
 ;; An interface is just a vtable specification (theory)

remix/tests/data-ramble2.rkt

@@ -0,0 +1,37 @@
+;; Interfaces & Objects
+
+(def [interface 2d<%>]
+  translate
+  area)
+
+(def [interface Circle<%>]
+  (layout-interface circle))
+
+(def [class Circle]
+  #:layout circle
+  #:new
+  (λ (x y r)
+    (this.#:alloc [c (posn.#:alloc [x x] [y y])]
+                  [r r]))
+
+  (layout-implements Circle<%>)
+  
+  (def [implements 2d<%>]
+    [(translate x y)
+     {this.#:set
+      [c (this.c.#:set [x {x + this.c.x}]
+                       [y {y + this.c.y}])]}]
+    [(area)
+     {3 * this.r * this.r}]))
+
+(def [Circle C1] (Circle.#:new 1 2 3))
+(module+ test
+  {C1.Circle<%>.c.x ≡ 1}
+  {C1.Circle<%>.c.y ≡ 2}
+  {C1.Circle<%>.r ≡ 3}
+  {(C1.2d<%>.area) ≡ 27}
+  (def [Circle C1′] (C1.2d<%>.translate 3 2))
+  {C1′.Circle<%>.c.x ≡ 4}
+  {C1′.Circle<%>.c.y ≡ 4}
+  {C1′.Circle<%>.r ≡ 3})
+

remix/tests/simple.rkt

@@ -509,3 +509,29 @@ def x4
   {even1.o.e.o.o ≡ 1}
   {even1.o.e.o.e.e ≡ 0})
 
+;; Theories & Models
+
+;; A theory is a specification of some values
+;; XXX add parameters
+(def [theory Monoid]
+  op id)
+;; XXX specify properties
+
+;; A model is an object that satisfies the theory
+(def [model Monoid Monoid-Nat:+]
+  [op +]
+  [id 0])
+;; XXX verify properties
+
+(def [model Monoid Monoid-Nat:*]
+  [op *]
+  [id 1])
+
+(module+ test
+  (def (monoid-id-test [Monoid m] a)
+    (≡ ((m.op) a m.id) ;; (#%app (#%dot m op) a (#%dot m id))
+       m.(op m.id a)   ;;    (#%app (#%dot m (#%app op (#%dot m id) a)))
+                       ;; => (#%app (#%app (#%dot m op)) (#%dot m id) a)
+       ))
+  (monoid-id-test Monoid-Nat:+ 5)
+  (monoid-id-test Monoid-Nat:* 5))