suzanne.soy/remix
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

split up files

Browse Source
This commit is contained in:
Jay McCarthy 2016-01-06 18:55:43 -05:00
parent 9993a038f2
commit decdb6d3ff
13 changed files with 1214 additions and 1190 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

65
remix/class0.rkt Normal file
View File

@ -0,0 +1,65 @@
#lang racket/base
(require (for-syntax racket/base
syntax/parse
remix/stx/singleton-struct0
(prefix-in remix: remix/stx0))
racket/stxparam
remix/theory0
(prefix-in remix: remix/stx0))
(struct object (interface->implementation rep))
(define-syntax interface
(singleton-struct
#:property prop:procedure
(λ (_ stx)
(raise-syntax-error 'interface "Illegal outside def" stx))
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
(syntax-parse stx
#:literals (remix:#%brackets remix:def interface)
;; XXX support parameters?
[(remix:def (remix:#%brackets interface int:id)
;; XXX support properties?
;; XXX make expandable position
v:id ...)
(syntax/loc stx
;; XXX instead, make an int-vtable and then a separate int
;; def transformer that looks at objects.
(remix:def (remix:#%brackets theory int)
;; XXX add a property for interfaces
;; XXX support defaults?
v ...))]))]))
(define-syntax-parameter representation
(λ (stx)
(raise-syntax-error 'representation "Illegal outside class" stx)))
(define-syntax-parameter new
(λ (stx)
(raise-syntax-error 'new "Illegal outside class" stx)))
(define-syntax-parameter this
(λ (stx)
(raise-syntax-error 'this "Illegal outside class" stx)))
(define-syntax-parameter implementation
(λ (stx)
(raise-syntax-error 'implementation "Illegal outside class" stx)))
(define-syntax class
(singleton-struct
#:property prop:procedure
(λ (_ stx)
(raise-syntax-error 'class "Illegal outside def" stx))
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
;; XXX ensure everything is expandable
;; XXX
#'(void))]))
(provide interface
representation
(rename-out [representation rep])
new
this
implementation
(rename-out [implementation impl])
class)

538
remix/data0.rkt
View File

@ -1,538 +0,0 @@
#lang racket/base
(require (for-syntax racket/base
syntax/quote
syntax/parse
racket/syntax
racket/generic
racket/format
racket/list
racket/match
(prefix-in remix: remix/stx0)
remix/stx/singleton-struct0
(for-syntax racket/base
racket/syntax
syntax/parse
racket/generic
(prefix-in remix: remix/stx0)))
racket/stxparam
racket/unsafe/ops
racket/performance-hint
(prefix-in remix: remix/stx0))
(begin-for-syntax
(define-generics static-interface
(static-interface-members static-interface))
(module interface-member racket/base
(require syntax/parse)
(define-syntax-class interface-member
(pattern x:id)
(pattern x:keyword))
(provide interface-member))
(require (submod "." interface-member)
(for-syntax
(submod "." interface-member)))
(define-syntax (phase1:static-interface stx)
(syntax-parse stx
#:literals (remix:#%brackets)
[(_si
;; XXX make expandable position
(remix:#%brackets
lhs:interface-member rhs:id
(~optional
(~seq #:is rhs-dt:id)
#:defaults ([rhs-dt #'#f])))
...
(~optional
(~seq #:extensions
extension ...)
#:defaults ([[extension 1] '()])))
(with-syntax* ([int-name (or (syntax-local-name) 'static-interface)]
[(def-rhs ...)
(for/list ([lhs (in-list
(map syntax->datum
(syntax->list #'(lhs ...))))])
(format-id #f "~a-~a-for-def" #'int-name
(if (keyword? lhs) (keyword->string lhs)
lhs)))]
[(full-def-rhs ...)
(for/list ([def-rhs (in-list (syntax->list #'(def-rhs ...)))]
[rhs-dt (in-list (syntax->list #'(rhs-dt ...)))])
(if (syntax-e rhs-dt)
(list def-rhs '#:is rhs-dt)
(list def-rhs)))])
(syntax/loc stx
(let ()
(define int-id->orig
(make-immutable-hasheq
(list (cons 'lhs (cons #'rhs #'rhs-dt))
...)))
(define available-ids
(sort (hash-keys int-id->orig)
string<=?
#:key ~a))
(define (get-rhs stx x)
(define xv (syntax->datum x))
(hash-ref int-id->orig
xv
(λ ()
(raise-syntax-error
'int-name
(format "Unknown component ~v, expected one of ~v"
xv
available-ids)
stx
x))))
(define (get-rhs-id stx x)
(car (get-rhs stx x)))
(define (get-rhs-is stx x)
(define r (cdr (get-rhs stx x)))
(if (syntax-e r)
r
#f))
(define (get-rhs-def stx x-stx)
(define xd (get-rhs-is stx x-stx))
(with-syntax* ([xb (get-rhs-id stx x-stx)]
[x-def
(if xd xd #'remix:stx)]
[x-def-v
(if xd #'xb #'(make-rename-transformer #'xb))])
(quasisyntax/loc stx
(remix:def (remix:#%brackets x-def #,x-stx) x-def-v))))
(singleton-struct
#:methods gen:static-interface
[(define (static-interface-members _)
available-ids)]
#: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)))
(quasisyntax/loc stx
(remix:block
#,(get-rhs-def stx #'x)
#,(syntax/loc #'x+more
(remix:#%dot x . more))))]))]
#: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))]
[(_app (_dot me:id x:interface-member . more) . body)
(quasisyntax/loc stx
(remix:block
#,(get-rhs-def stx #'x)
(remix:#%app (remix:#%dot x . more) . body)))]))]
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
(syntax-parse stx
#:literals (remix:#%brackets)
[(def (remix:#%brackets me:id i:id) . body)
(with-syntax ([real-i (generate-temporary #'i)])
(syntax/loc stx
(begin
(remix:def real-i . body)
(remix:def (remix:#%brackets remix:stx def-rhs)
(λ (stx)
(syntax-parse stx
[_:id
(syntax/loc stx
(rhs real-i))]
[(_ . blah)
(syntax/loc stx
(rhs real-i . blah))])))
...
(remix:def (remix:#%brackets remix:stx i)
(phase1:static-interface
(remix:#%brackets lhs . full-def-rhs)
...
#:extensions
;; NB I don't pass on other
;; extensions... I don't think
;; it can possibly make sense,
;; because I don't know what
;; they might be.
#:property prop:procedure
(λ (_ stx)
(syntax-parse stx
[_:id
(syntax/loc stx
real-i)]
[(_ . blah)
(syntax/loc stx
(real-i . blah))])))))))]))]
extension ...))))])))
(define-syntax (define-phase0-def->phase1-macro stx)
(syntax-parse stx
[(_ base:id)
(with-syntax ([phase0:base (format-id #'base "phase0:~a" #'base)]
[phase1:base (format-id #'base "phase1:~a" #'base)])
(syntax/loc stx
(define-syntax phase0:base
(singleton-struct
#:property prop:procedure
(λ (_ stx)
(raise-syntax-error 'base "Illegal outside def" stx))
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
(syntax-parse stx
#:literals (remix:#%brackets)
[(def (remix:#%brackets me:id i:id) . body)
(syntax/loc stx
(remix:def (remix:#%brackets remix:stx i)
(phase1:base . body)))]))]))))]))
(define-phase0-def->phase1-macro static-interface)
(provide (rename-out [phase0:static-interface static-interface])
(for-syntax (rename-out [phase1:static-interface static-interface])
gen:static-interface
static-interface?
static-interface-members))
(begin-for-syntax
(define-generics layout
(layout-planner-id layout)
;; xxx the accessors seem to not be around anyways, so instead,
;; this should just be a mapping produced by the planner.
(layout-field->acc layout))
(define-generics layout-planner
(layout-planner-mutable? layout-planner))
(define-syntax-class field
#:attributes (name dt)
#:literals (remix:#%brackets)
(pattern name:id
#:attr dt #f)
(pattern (remix:#%brackets dt:id name:id)
;; XXX This can't be here because it disallows mutual
;; recursion... move the check somewhere else?
;; #:declare dt (static remix:def-transformer? "def transformer")
)))
(define-syntax layout-immutable
(singleton-struct
#:methods gen:layout-planner
[(define (layout-planner-mutable? lp) #f)]))
(define-syntax layout-mutable
(singleton-struct
#:methods gen:layout-planner
[(define (layout-planner-mutable? lp) #t)]))
(define-syntax phase0:layout
(singleton-struct
#:property prop:procedure
(λ (_ stx)
(raise-syntax-error 'layout "Illegal outside def" stx))
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
(syntax-parse stx
#:literals (remix:#%brackets)
[(def (remix:#%brackets me:id name:id)
(~optional (~and (~seq #:parent (~var parent (static layout? "layout")))
(~bind [parent-va (attribute parent.value)]))
#:defaults ([parent-va #f]))
(~optional (~and (~seq #:rep (~var rep (static layout-planner?
"layout planner"))))
#:defaults ([rep #f]))
;; XXX make expandable position
F:field ...)
(define parent-v (attribute parent-va))
(define this-rep-id (attribute rep))
(define parent-rep-id (and parent-v (layout-planner-id parent-v)))
(unless (or (not this-rep-id)
(not parent-rep-id)
(bound-identifier=? this-rep-id parent-rep-id))
(raise-syntax-error
'layout
(format "Parent (~v) and child (~v) representation planner must match"
parent-rep-id
this-rep-id)
stx))
(define the-planner-id
(or parent-rep-id
this-rep-id
#'layout-immutable))
(define the-planner
(syntax-local-value the-planner-id))
(define parent-f->acc
(or (and parent-v (layout-field->acc parent-v))
(hasheq)))
(define f->acc
(for/fold ([base parent-f->acc])
([the-f (in-list (syntax->datum #'(F.name ...)))]
[the-dt (in-list (attribute F.dt))]
[the-idx (in-naturals (hash-count parent-f->acc))])
(when (hash-has-key? base the-f)
(raise-syntax-error 'layout
(format "duplicate field ~a in layout"
the-f)
stx
the-f))
(define the-name-f (format-id #f "~a-~a" #'name the-f))
(hash-set base the-f (vector the-name-f the-dt the-idx))))
(with-syntax* ([name-alloc (format-id #f "~a-alloc" #'name)]
[name-set (format-id #f "~a-set" #'name)]
[name-set! (format-id #f "~a-set!" #'name)]
[((all-f all-name-f all-f-si-rhs all-f-idx) ...)
(for/list ([(the-f v) (in-hash f->acc)])
(match-define (vector the-name-f the-dt the-f-idx) v)
(list the-f the-name-f
(if the-dt
(list the-name-f '#:is the-dt)
(list the-name-f))
the-f-idx))]
[stx-the-planner-id the-planner-id]
[stx-f->acc f->acc]
[(rep-constructor
rep-accessor rep-mutate
(mutation-interface ...))
;; XXX This should work differently
(if (layout-planner-mutable? the-planner)
(list #'vector
#'unsafe-vector*-ref
#'unsafe-vector*-set!
#'((remix:#%brackets #:set! name-set!)
(remix:#%brackets #:! name-set!)))
(list #'vector-immutable
#'unsafe-vector*-ref
#'void
#'()))])
(syntax/loc stx
(begin
(begin-for-syntax
(define f->acc stx-f->acc)
(define available-fields
(sort (hash-keys f->acc)
string<=?
#:key symbol->string))
(define ordered-fields
(sort (hash-keys f->acc)
<=
#:key (λ (x)
(vector-ref (hash-ref f->acc x) 2))))
(define-syntax-class name-arg
#:attributes (lhs rhs)
#:literals (remix:#%brackets)
(pattern (remix:#%brackets lhs:id rhs:expr)
#:do [(define lhs-v (syntax->datum #'lhs))]
#:fail-unless
(hash-has-key? f->acc lhs-v)
(format "invalid field given: ~a, valid fields are: ~a"
lhs-v
available-fields)))
(define-syntax-class name-args
#:attributes (f->rhs)
(pattern (a:name-arg (... ...))
#:do [(define first-dupe
(check-duplicates
(syntax->datum #'(a.lhs (... ...)))))]
#:fail-when first-dupe
(format "field occurs twice: ~a" first-dupe)
#:attr f->rhs
(for/hasheq ([l (syntax->list #'(a.lhs (... ...)))]
[r (syntax->list #'(a.rhs (... ...)))])
(values (syntax->datum l) r)))))
(define-syntax (name-alloc stx)
(syntax-parse stx
[(_ . args:name-args)
(with-syntax ([(f-val (... ...))
(for/list ([this-f (in-list ordered-fields)])
(hash-ref (attribute args.f->rhs)
this-f
(λ ()
(raise-syntax-error
'name-alloc
(format "missing initializer for ~a"
this-f)
stx))))])
(syntax/loc stx
(rep-constructor f-val (... ...))))]))
(define-syntax (name-set stx)
(syntax-parse stx
[(_ base:expr . args:name-args)
(with-syntax* ([base-id (generate-temporary #'base)]
[(f-val (... ...))
(for/list ([this-f (in-list ordered-fields)])
(define this-name-f
(vector-ref
(hash-ref f->acc this-f)
0))
(hash-ref (attribute args.f->rhs)
this-f
(λ ()
(quasisyntax/loc stx
(#,this-name-f base-id)))))])
(syntax/loc stx
(let ([base-id base])
(rep-constructor f-val (... ...)))))]))
(define-syntax (name-set! stx)
(syntax-parse stx
[(_ base:expr . args:name-args)
(with-syntax* ([base-id (generate-temporary #'base)]
[((f-val-id f-val f-idx) (... ...))
(for/list ([(this-f this-f-val)
(in-hash (attribute args.f->rhs))])
(match-define
(vector this-name-f _ this-idx)
(hash-ref f->acc this-f))
(list
(generate-temporary this-f)
this-f-val
this-idx))])
(syntax/loc stx
(let ([f-val-id f-val]
(... ...))
(let ([base-id base])
(rep-mutate base-id f-idx f-val-id)
(... ...)
(void)))))]))
;; xxx add per-field mutators with a set! macro
(begin-encourage-inline
(define (all-name-f v) (rep-accessor v all-f-idx))
...)
(define-syntax name
(phase1:static-interface
(remix:#%brackets #:alloc name-alloc)
(remix:#%brackets #:set name-set)
(remix:#%brackets #:= name-set)
mutation-interface ...
(remix:#%brackets all-f . all-f-si-rhs)
...
#:extensions
#:methods gen:layout
[(define (layout-planner-id _)
#'stx-the-planner-id)
(define (layout-field->acc _)
f->acc)])))))]))]))
(provide (rename-out [phase0:layout layout])
(for-syntax gen:layout
layout?
gen:layout-planner
layout-planner?
layout-planner-mutable?)
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)
;; XXX support parameters
[(remix:def (remix:#%brackets theory thy:id)
;; XXX support properties (including type)
;; XXX make expandable position
v:id ...)
(syntax/loc stx
(remix:def (remix:#%brackets phase0:layout thy)
;; XXX add a property for theories
;; XXX support defaults
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)
;; XXX make expandable position
(remix:#%brackets f:id v:expr) ...)
;; XXX support verification of properties
;; XXX support theory parameters
;; XXX check that thy is a theory
;; XXX check that f is complete and apply defaults if not
(syntax/loc stx
(remix:def (remix:#%brackets thy mod)
(remix:#%app
(remix:#%dot thy #:alloc)
(remix:#%brackets f v) ...)))]))]))
(provide theory
model)
;; Interfaces & Classes
(struct object (interface->implementation rep))
(define-syntax interface
(singleton-struct
#:property prop:procedure
(λ (_ stx)
(raise-syntax-error 'interface "Illegal outside def" stx))
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
(syntax-parse stx
#:literals (remix:#%brackets remix:def interface)
;; XXX support parameters?
[(remix:def (remix:#%brackets interface int:id)
;; XXX support properties?
;; XXX make expandable position
v:id ...)
(syntax/loc stx
;; XXX instead, make an int-vtable and then a separate int
;; def transformer that looks at objects.
(remix:def (remix:#%brackets theory int)
;; XXX add a property for interfaces
;; XXX support defaults?
v ...))]))]))
(define-syntax-parameter representation
(λ (stx)
(raise-syntax-error 'representation "Illegal outside class" stx)))
(define-syntax-parameter new
(λ (stx)
(raise-syntax-error 'new "Illegal outside class" stx)))
(define-syntax-parameter this
(λ (stx)
(raise-syntax-error 'this "Illegal outside class" stx)))
(define-syntax-parameter implementation
(λ (stx)
(raise-syntax-error 'implementation "Illegal outside class" stx)))
(define-syntax class
(singleton-struct
#:property prop:procedure
(λ (_ stx)
(raise-syntax-error 'class "Illegal outside def" stx))
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
;; XXX ensure everything is expandable
;; XXX
#'(void))]))
(provide interface
representation
(rename-out [representation rep])
new
this
implementation
(rename-out [implementation impl])
class)
;; xxx data (fixed set of interfaces)

25
remix/exp/list.rkt
View File

@ -1,25 +0,0 @@
#lang remix
(data seq
(struct empty)
(def (first t)
(error))
(def (rest t)
(error))
(def (empty? t)
#t)
(def (cons x t)
((outer cons) x t))
(def (snoc t x)
((outer cons) x t)))
(data seq
(struct cons
[racket car]
[racket cdr])
(def (first t)
t.car)
(def (rest t)
t.cdr)
(def (empty? t)
#f))

248
remix/layout0.rkt Normal file
View File

@ -0,0 +1,248 @@
#lang racket/base
(require (for-syntax racket/base
syntax/quote
syntax/parse
racket/syntax
racket/generic
racket/format
racket/list
racket/match
(prefix-in remix: remix/stx0)
remix/stx/singleton-struct0
(for-syntax racket/base
racket/syntax
syntax/parse
racket/generic
(prefix-in remix: remix/stx0)))
racket/stxparam
racket/unsafe/ops
racket/performance-hint
remix/static-interface0
(prefix-in remix: remix/stx0))
(begin-for-syntax
(define-generics layout
(layout-planner-id layout)
;; xxx the accessors seem to not be around anyways, so instead,
;; this should just be a mapping produced by the planner.
(layout-field->acc layout))
(define-generics layout-planner
(layout-planner-mutable? layout-planner))
(define-syntax-class field
#:attributes (name dt)
#:literals (remix:#%brackets)
(pattern name:id
#:attr dt #f)
(pattern (remix:#%brackets dt:id name:id)
;; XXX This can't be here because it disallows mutual
;; recursion... move the check somewhere else?
;; #:declare dt (static remix:def-transformer? "def transformer")
)))
(define-syntax layout-immutable
(singleton-struct
#:methods gen:layout-planner
[(define (layout-planner-mutable? lp) #f)]))
(define-syntax layout-mutable
(singleton-struct
#:methods gen:layout-planner
[(define (layout-planner-mutable? lp) #t)]))
(define-syntax phase0:layout
(singleton-struct
#:property prop:procedure
(λ (_ stx)
(raise-syntax-error 'layout "Illegal outside def" stx))
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
(syntax-parse stx
#:literals (remix:#%brackets)
[(def (remix:#%brackets me:id name:id)
(~optional (~and (~seq #:parent (~var parent (static layout? "layout")))
(~bind [parent-va (attribute parent.value)]))
#:defaults ([parent-va #f]))
(~optional (~and (~seq #:rep (~var rep (static layout-planner?
"layout planner"))))
#:defaults ([rep #f]))
;; XXX make expandable position
F:field ...)
(define parent-v (attribute parent-va))
(define this-rep-id (attribute rep))
(define parent-rep-id (and parent-v (layout-planner-id parent-v)))
(unless (or (not this-rep-id)
(not parent-rep-id)
(bound-identifier=? this-rep-id parent-rep-id))
(raise-syntax-error
'layout
(format "Parent (~v) and child (~v) representation planner must match"
parent-rep-id
this-rep-id)
stx))
(define the-planner-id
(or parent-rep-id
this-rep-id
#'layout-immutable))
(define the-planner
(syntax-local-value the-planner-id))
(define parent-f->acc
(or (and parent-v (layout-field->acc parent-v))
(hasheq)))
(define f->acc
(for/fold ([base parent-f->acc])
([the-f (in-list (syntax->datum #'(F.name ...)))]
[the-dt (in-list (attribute F.dt))]
[the-idx (in-naturals (hash-count parent-f->acc))])
(when (hash-has-key? base the-f)
(raise-syntax-error 'layout
(format "duplicate field ~a in layout"
the-f)
stx
the-f))
(define the-name-f (format-id #f "~a-~a" #'name the-f))
(hash-set base the-f (vector the-name-f the-dt the-idx))))
(with-syntax* ([name-alloc (format-id #f "~a-alloc" #'name)]
[name-set (format-id #f "~a-set" #'name)]
[name-set! (format-id #f "~a-set!" #'name)]
[((all-f all-name-f all-f-si-rhs all-f-idx) ...)
(for/list ([(the-f v) (in-hash f->acc)])
(match-define (vector the-name-f the-dt the-f-idx) v)
(list the-f the-name-f
(if the-dt
(list the-name-f '#:is the-dt)
(list the-name-f))
the-f-idx))]
[stx-the-planner-id the-planner-id]
[stx-f->acc f->acc]
[(rep-constructor
rep-accessor rep-mutate
(mutation-interface ...))
;; XXX This should work differently
(if (layout-planner-mutable? the-planner)
(list #'vector
#'unsafe-vector*-ref
#'unsafe-vector*-set!
#'((remix:#%brackets #:set! name-set!)
(remix:#%brackets #:! name-set!)))
(list #'vector-immutable
#'unsafe-vector*-ref
#'void
#'()))])
(syntax/loc stx
(begin
(begin-for-syntax
(define f->acc stx-f->acc)
(define available-fields
(sort (hash-keys f->acc)
string<=?
#:key symbol->string))
(define ordered-fields
(sort (hash-keys f->acc)
<=
#:key (λ (x)
(vector-ref (hash-ref f->acc x) 2))))
(define-syntax-class name-arg
#:attributes (lhs rhs)
#:literals (remix:#%brackets)
(pattern (remix:#%brackets lhs:id rhs:expr)
#:do [(define lhs-v (syntax->datum #'lhs))]
#:fail-unless
(hash-has-key? f->acc lhs-v)
(format "invalid field given: ~a, valid fields are: ~a"
lhs-v
available-fields)))
(define-syntax-class name-args
#:attributes (f->rhs)
(pattern (a:name-arg (... ...))
#:do [(define first-dupe
(check-duplicates
(syntax->datum #'(a.lhs (... ...)))))]
#:fail-when first-dupe
(format "field occurs twice: ~a" first-dupe)
#:attr f->rhs
(for/hasheq ([l (syntax->list #'(a.lhs (... ...)))]
[r (syntax->list #'(a.rhs (... ...)))])
(values (syntax->datum l) r)))))
(define-syntax (name-alloc stx)
(syntax-parse stx
[(_ . args:name-args)
(with-syntax ([(f-val (... ...))
(for/list ([this-f (in-list ordered-fields)])
(hash-ref (attribute args.f->rhs)
this-f
(λ ()
(raise-syntax-error
'name-alloc
(format "missing initializer for ~a"
this-f)
stx))))])
(syntax/loc stx
(rep-constructor f-val (... ...))))]))
(define-syntax (name-set stx)
(syntax-parse stx
[(_ base:expr . args:name-args)
(with-syntax* ([base-id (generate-temporary #'base)]
[(f-val (... ...))
(for/list ([this-f (in-list ordered-fields)])
(define this-name-f
(vector-ref
(hash-ref f->acc this-f)
0))
(hash-ref (attribute args.f->rhs)
this-f
(λ ()
(quasisyntax/loc stx
(#,this-name-f base-id)))))])
(syntax/loc stx
(let ([base-id base])
(rep-constructor f-val (... ...)))))]))
(define-syntax (name-set! stx)
(syntax-parse stx
[(_ base:expr . args:name-args)
(with-syntax* ([base-id (generate-temporary #'base)]
[((f-val-id f-val f-idx) (... ...))
(for/list ([(this-f this-f-val)
(in-hash (attribute args.f->rhs))])
(match-define
(vector this-name-f _ this-idx)
(hash-ref f->acc this-f))
(list
(generate-temporary this-f)
this-f-val
this-idx))])
(syntax/loc stx
(let ([f-val-id f-val]
(... ...))
(let ([base-id base])
(rep-mutate base-id f-idx f-val-id)
(... ...)
(void)))))]))
;; xxx add per-field mutators with a set! macro
(begin-encourage-inline
(define (all-name-f v) (rep-accessor v all-f-idx))
...)
(define-syntax name
(static-interface
(remix:#%brackets #:alloc name-alloc)
(remix:#%brackets #:set name-set)
(remix:#%brackets #:= name-set)
mutation-interface ...
(remix:#%brackets all-f . all-f-si-rhs)
...
#:extensions
#:methods gen:layout
[(define (layout-planner-id _)
#'stx-the-planner-id)
(define (layout-field->acc _)
f->acc)])))))]))]))
(provide (rename-out [phase0:layout layout])
(for-syntax gen:layout
layout?
gen:layout-planner
layout-planner?
layout-planner-mutable?)
layout-immutable
layout-mutable)

207
remix/static-interface0.rkt Normal file
View File

@ -0,0 +1,207 @@
#lang racket/base
(require (for-syntax racket/base
syntax/quote
syntax/parse
racket/syntax
racket/generic
racket/format
racket/list
racket/match
(prefix-in remix: remix/stx0)
remix/stx/singleton-struct0
(for-syntax racket/base
racket/syntax
syntax/parse
racket/generic
(prefix-in remix: remix/stx0)))
racket/stxparam
racket/unsafe/ops
racket/performance-hint
(prefix-in remix: remix/stx0))
(begin-for-syntax
(define-generics static-interface
(static-interface-members static-interface))
(module interface-member racket/base
(require syntax/parse)
(define-syntax-class interface-member
(pattern x:id)
(pattern x:keyword))
(provide interface-member))
(require (submod "." interface-member)
(for-syntax
(submod "." interface-member)))
(define-syntax (phase1:static-interface stx)
(syntax-parse stx
#:literals (remix:#%brackets)
[(_si
;; XXX make expandable position
(remix:#%brackets
lhs:interface-member rhs:id
(~optional
(~seq #:is rhs-dt:id)
#:defaults ([rhs-dt #'#f])))
...
(~optional
(~seq #:extensions
extension ...)
#:defaults ([[extension 1] '()])))
(with-syntax* ([int-name (or (syntax-local-name) 'static-interface)]
[(def-rhs ...)
(for/list ([lhs (in-list
(map syntax->datum
(syntax->list #'(lhs ...))))])
(format-id #f "~a-~a-for-def" #'int-name
(if (keyword? lhs) (keyword->string lhs)
lhs)))]
[(full-def-rhs ...)
(for/list ([def-rhs (in-list (syntax->list #'(def-rhs ...)))]
[rhs-dt (in-list (syntax->list #'(rhs-dt ...)))])
(if (syntax-e rhs-dt)
(list def-rhs '#:is rhs-dt)
(list def-rhs)))])
(syntax/loc stx
(let ()
(define int-id->orig
(make-immutable-hasheq
(list (cons 'lhs (cons #'rhs #'rhs-dt))
...)))
(define available-ids
(sort (hash-keys int-id->orig)
string<=?
#:key ~a))
(define (get-rhs stx x)
(define xv (syntax->datum x))
(hash-ref int-id->orig
xv
(λ ()
(raise-syntax-error
'int-name
(format "Unknown component ~v, expected one of ~v"
xv
available-ids)
stx
x))))
(define (get-rhs-id stx x)
(car (get-rhs stx x)))
(define (get-rhs-is stx x)
(define r (cdr (get-rhs stx x)))
(if (syntax-e r)
r
#f))
(define (get-rhs-def stx x-stx)
(define xd (get-rhs-is stx x-stx))
(with-syntax* ([xb (get-rhs-id stx x-stx)]
[x-def
(if xd xd #'remix:stx)]
[x-def-v
(if xd #'xb #'(make-rename-transformer #'xb))])
(quasisyntax/loc stx
(remix:def (remix:#%brackets x-def #,x-stx) x-def-v))))
(singleton-struct
#:methods gen:static-interface
[(define (static-interface-members _)
available-ids)]
#: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)))
(quasisyntax/loc stx
(remix:block
#,(get-rhs-def stx #'x)
#,(syntax/loc #'x+more
(remix:#%dot x . more))))]))]
#: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))]
[(_app (_dot me:id x:interface-member . more) . body)
(quasisyntax/loc stx
(remix:block
#,(get-rhs-def stx #'x)
(remix:#%app (remix:#%dot x . more) . body)))]))]
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
(syntax-parse stx
#:literals (remix:#%brackets)
[(def (remix:#%brackets me:id i:id) . body)
(with-syntax ([real-i (generate-temporary #'i)])
(syntax/loc stx
(begin
(remix:def real-i . body)
(remix:def (remix:#%brackets remix:stx def-rhs)
(λ (stx)
(syntax-parse stx
[_:id
(syntax/loc stx
(rhs real-i))]
[(_ . blah)
(syntax/loc stx
(rhs real-i . blah))])))
...
(remix:def (remix:#%brackets remix:stx i)
(phase1:static-interface
(remix:#%brackets lhs . full-def-rhs)
...
#:extensions
;; NB I don't pass on other
;; extensions... I don't think
;; it can possibly make sense,
;; because I don't know what
;; they might be.
#:property prop:procedure
(λ (_ stx)
(syntax-parse stx
[_:id
(syntax/loc stx
real-i)]
[(_ . blah)
(syntax/loc stx
(real-i . blah))])))))))]))]
extension ...))))])))
(define-syntax (define-phase0-def->phase1-macro stx)
(syntax-parse stx
[(_ base:id)
(with-syntax ([phase0:base (format-id #'base "phase0:~a" #'base)]
[phase1:base (format-id #'base "phase1:~a" #'base)])
(syntax/loc stx
(define-syntax phase0:base
(singleton-struct
#:property prop:procedure
(λ (_ stx)
(raise-syntax-error 'base "Illegal outside def" stx))
#:methods remix:gen:def-transformer
[(define (def-transform _ stx)
(syntax-parse stx
#:literals (remix:#%brackets)
[(def (remix:#%brackets me:id i:id) . body)
(syntax/loc stx
(remix:def (remix:#%brackets remix:stx i)
(phase1:base . body)))]))]))))]))
(define-phase0-def->phase1-macro static-interface)
(provide (rename-out [phase0:static-interface static-interface])
(for-syntax (rename-out [phase1:static-interface static-interface])
gen:static-interface
static-interface?
static-interface-members))
;; xxx data (fixed set of interfaces)

69
remix/tests/class.rkt Normal file
View File

@ -0,0 +1,69 @@
#lang remix
(require remix/stx0
remix/class0
remix/num/gen0)
(module+ test
(require remix/test0))
(def [interface 2d<%>]
translate
area)
(def [interface Circle<%>]
;; xxx make a macro for "interface of layout's fields"
c r)
;; A class is a representation, a constructor, and implementations of
;; interfaces.
(def [class Circle]
(def [rep] circle) ;; rep = representation
(def ([new] x y r)
(this.#:alloc [c (posn.#:alloc [x x] [y y])]
[r r]))
;; xxx make a macro from "layout's fields implements this interface"
(def [implementation Circle<%>]
[(c) this.c]
[(r) this.r])
(def [impl 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}]))
;; XXX allow w/o #:new?, like layout
#;(def [Circle C1] (Circle.#:new 1 2 3))
#;
(module+ test
;; If you know something is a particular class, then you can access
;; its implementations directly. This is more efficient.
{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}
;; In contrast, when you access them as their interfaces, a lookup
;; is done.
(def [2d<%> C1-as-2d] C1)
{C1-as-2d.(area) ≡ 27}
(def [Circle<%> C1-as-Circ] C1)
{C1-as-Circ.c.x ≡ 1}
{C1-as-Circ.c.y ≡ 2}
{C1-as-Circ.r ≡ 3})
#;
(module+ test
;; Like theories, you can define functions that are generic over an
;; interface.
(def (squarea [2d<%> o])
{o.(area) * o.(area)})
{(squarea C1) ≡ 729}
;; The default behavior of class dot-transformers on unknown methods
;; is to treat it as a generic function.
{C1.(squarea) ≡ 729})

160
remix/tests/layout.rkt Normal file
View File

@ -0,0 +1,160 @@
#lang remix
(require remix/stx0
remix/layout0
remix/num/gen0
"static-interface.rkt")
(module+ test
(require remix/test0))
;; A layout is a container with no sealing or representation
;; guarantees. This means you can't necessarily protect the contents
;; nor can you necessarily tell that you have one when you do.
;; layout is a def-transformer (XXX I wish I could make it phase1
;; macro also but it needs to define some functions that could be
;; called)
;;
;; XXX maybe I can expand to a submodule and local-require
;; The most basic syntax is a list of fields, which are identifiers.
(def [layout posn]
x y)
(module+ test
;; You will get an allocation function named #:alloc
(def [posn p1] (posn.#:alloc [x 5] [y 7]))
;; XXX (def [posn p1] #:alloc [x 5] [y 7]) <--- def transformer for allocation
;; XXX (def [posn p1] (posn [x 5] [y 7])) <--- default use is allocation
;; And accessors
{p1.x ≡ 5}
{p1.y ≡ 7}
;; You may not have noticed, but posn was just a def transformer
;; that gave us access to these. We can, of course, just call them
;; directly through posn.
{(posn.x p1) ≡ 5}
;; You will also get a copying function
(def [posn p2] (p1.#:set [y {p1.y + 2}]))
;; XXX (def [posn p2] (posn p1 [y {p1.y + 2}])) <---- default use with expr is copy
;; Notice that these built-in functions are keywords, so that they
;; can't conflict with the fields you've defined.
{p2.x ≡ 5}
{p2.y ≡ 9}
;; This is aliased to =, which I expect is nicer to use.
(def [posn p3] (p1.#:= [x 8]))
{p3.x ≡ 8}
{p3.y ≡ 7})
;; A layout can have a parent, which provides the guarantee that the
;; parent's functions will work on the child---meaning that whatever
;; the layout ends up being (and you can't decide that), the two will
;; overlap in this specific way. A layout has one or zero parents.
(def [layout quat]
#:parent posn
z)
(module+ test
(def [quat q1] (quat.#:alloc [x 1] [y 2] [z 3]))
{q1.x ≡ 1}
{q1.y ≡ 2}
{q1.z ≡ 3}
;; We can consider to be posn (imaging calling some function that
;; expects one) and it just works
(def [posn qp1] q1)
{qp1.x ≡ 1}
{qp1.y ≡ 2}
;; However, that casting is computation-less, so it can be cast back
;; and we can get all the fields. However, if we changed it, it
;; wouldn't have stayed a quat.
(def [quat qpq1] qp1)
{qpq1.x ≡ 1}
{qpq1.y ≡ 2}
{qpq1.z ≡ 3})
;; XXX Does it do the "right thing" for copying? (i.e. when a parent
;; copies, do the child's fields get copied as is)
;; A layout's fields may be specified as other layouts. When the first
;; field is a layout, this is not necessarily the same thing as a
;; parent (like C structs) but it may be. (No matter what, you'd never
;; be able to tell, since layout doesn't make representation promises
;; as a rule.)
(def [layout circle]
[posn c] r)
(module+ test
(def [circle c1] (circle.#:alloc [c p1] [r 8]))
{c1.c.x ≡ 5}
{c1.c.y ≡ 7}
{c1.r ≡ 8})
;; A layout's fields can _actually_ just be any def transformer, and
;; thus could be static interfaces
(def [layout weird]
[example^ e])
(module+ test
(def [weird wr1] (weird.#:alloc [e 1]))
{(wr1.e.f 2) ≡ 1}
{(wr1.e.g 2) ≡ 2})
;; Now, the big reveal, layout has an extensible representation
;; planner system. At the moment, the only representations are
;;
;; layout-immutable : The default, backed by immutable vectors
;; layout-mutable : Backed by mutable vectors, with mutation support
;;
;; I expect to produce a few more
;;
;; (XXX) layout-c : Compatible with C
;; (XXX) layout-optimize : Optimize for removing padding and have
;; cache-line-aligned accesses
;; (XXX) layout-enumerate : Use data/enumerate
;;
;; It would be possible to make layout-c right now, but define-cstruct
;; is really slow. It is trivial to have layout-optimize if you have
;; layout-c, but it would not be useful to use. mflatt and I talked
;; about a fast way of implementing them in Racket. The basic idea is
;; to have a new type of object in the VM where the pointer goes to
;; the middle of the allocated space which looks like
;;
;; [ <raw-values> | <tag> <vector layout> ]
;;
;; There may be necessary padding, but then the existing vector
;; functions would work. The raw values would use computed offsets to
;; get the values. The goal would be that parent structs would just
;; work and it would be easy to pass to C by sorting the _racket
;; pointers to the end.
;;
;; Anyways, here's a mutable example.
(def [layout world]
#:rep layout-mutable
[circle c1] [circle c2])
(module+ test
(def [world w1] (world.#:alloc [c1 c1] [c2 (c1.#:set [r 3])]))
{w1.c1.r ≡ 8}
{w1.c2.r ≡ 3}
;; The set! is simultaneous
(w1.#:set! [c1 w1.c2] [c2 w1.c1])
{w1.c1.r ≡ 3}
{w1.c2.r ≡ 8}
;; It is aliased to !
(w1.#:! [c1 w1.c2] [c2 w1.c1])
{w1.c1.r ≡ 8}
{w1.c2.r ≡ 3})
;; These support mutual recursion
(def [layout even]
#:rep layout-mutable
e [odd o])
(def [layout odd]
#:rep layout-mutable
[even e] o)
(module+ test
(def [even even1]
(even.#:alloc
[e 0]
[o (odd.#:alloc
[e #f]
[o 1])]))
(even1.o.#:set! [e even1])
{even1.e ≡ 0}
{even1.o.o ≡ 1}
{even1.o.e.e ≡ 0}
{even1.o.e.o.o ≡ 1}
{even1.o.e.o.e.e ≡ 0})

22
remix/tests/rocket.rkt
View File

@ -1,22 +0,0 @@
#lang remix
(require remix/struct.0
remix/match.0
num/int.0
gfx/2d.0
big-bang.0)
(struct #rocket
([int h]
[int dh]))
(data rocket
#:this [#rocket r]
(def (rocket [int (~opt h 0)] [int (~opt dh 1)])
(#rocket.alloc [h h] [dh dh]))
#:implements world/anim^
(def (tick)
(r.= [h {r.h + r.dh}]))
(def (draw)
(circle 'yellow 5)))
(big-bang (rocket.new))

605
remix/tests/simple.rkt
View File

@ -1,605 +0,0 @@
#lang remix
;; Remix comments start with ;;
;; #lang remix only contains two bindings: #%module-begin and require
;;
;; We use require to get everything else. most of it comes from stx0
require remix/stx0
remix/num/gen0;
;; A semi introduces a set of parens to its left
;; As usual `unquote` escapes from its context, in the case of a
;; semi-sequence, this means that the term is not wrapped.
,(module+ test
;; This introduces ≡ as a testing form
;; XXX Drop this and instead have a macro for writing down
;; properties that communicates with boolean forms, etc. Supports ∀,
;; etc.
(require remix/test0))
;; define is replaced with def
def z 42;
module+ test
{z ≡ 42};
;; when def has more forms than one, they are put inside of a block
def x
(def a 40)
(def b 2)
(+ a b) ;
,(module+ test
{x ≡ 42})
;; If you would like to use ;-syntax in the inside of def, then you
;; need more punctuation. You have two choices.
def x2
[def a 40;
def b 2;
(+ a b)];
,(module+ test
{x2 ≡ 42})
def x3
[def a 40;
def b 2;
{a + b}];
,(module+ test
{x3 ≡ 42})
def x4
[,{a := 40}
def b 2 ;
{a + b}];
(module+ test
{x4 ≡ 42})
;; but of course def supports function definitions. [] is NOT the same
;; as (), it parses as #%brackets and defaults to expanding to a block
;; definition
(def (f x y)
(+ [(def z (+ x x))
z]
y))
(module+ test
{(f x x) ≡ 126})
;; That's the same as just 'block' if you want to be specific
(def (other-f x y)
(+ (block (def z (+ x x))
z)
y))
(module+ test
{(other-f x x) ≡ 126})
;; cond requires []s for the question-answer pairs. It uses this to
;; make any code in between clauses go in between the `if`s that pop
;; out of the cond macro.
(def (g x)
(cond
[(< x 100) "100"]
(def z (/ x 2))
[(< z 100) "div 100"]
[#:else z]))
(module+ test
{(g 50) ≡ "100"}
{(g 199) ≡ "div 100"}
{(g 200) ≡ 100})
;; If cond reaches the end without an else, then a runtime error is
;; generated
(def (g2 x)
(cond
[(< x 100) "100"]
(def z (/ x 2))
[(< z 100) "div 100"]))
(module+ test
{(g2 50) ≡ "100"}
{(g2 199) ≡ "div 100"}
;; This is the error test:
#;(g2 200))
;; This functionality is provided by ☠ (aka impossible!)
(def (g3)
☠)
(module+ test
#;(g3))
;; the @ reader is always on. One fun thing about this is that you can
;; make non-() macros. I wrote a little helper function to turn the
;; string arguments that @{} produces into a string port that has
;; accurate source location information for the original file. datalog
;; uses this to make all the source locations correct, so errors in
;; datalog will give accurate source locations.
(require remix/datalog0)
(def graph (make-theory))
@datalog[graph]{
edge(a, b). edge(b, c). edge(c, d). edge(d, a).
path(X, Y) :- edge(X, Y).
path(X, Y) :- edge(X, Z), path(Z, Y).
path(X, Y)?
}
;; {} is also not (), it is parsed as #%braces, and by default is an
;; infix macro
(def v7
{3 + 4})
(module+ test
{v7 ≡ 7})
;; {} use C's precedence and considers the things you expect to be
;; operators. there's a syntax-time struct property that allows you to
;; specify what you want the precedence of an operator to be.
(def v-26
{2 * 3 - 48 / 4 - 4 * 5})
(module+ test
{v-26 ≡ -26})
;; if a symbol contains no alphabetic or numeric characters, then it
;; is considered an operator. This means you can automatically use
;; stuff like & and →, but you won't confuse it with symbols like z
(def v85
{z * 2 + 1})
(module+ test
{v85 ≡ 85})
(def v1
(def & bitwise-and)
{5 & 1})
(module+ test
{v1 ≡ 1})
(def v56
(def (→ x y) (+ (* x x) y))
{v7 → v7})
(module+ test
{v56 ≡ 56})
;; However, if you use , then you can force anything to be a binary
;; operator and force something that would have been a binary operator
;; into an argument.
(def v14
(def (f x y) (+ x y))
{v7 ,f v7})
(module+ test
{v14 ≡ 14})
(def v14b
{v7 ,(λ (x y) (+ x y)) v7})
(module+ test
{v14b ≡ 14})
(def v9
(def & 2)
{v7 + ,&})
(module+ test
{v9 ≡ 9})
;; λ is a dot-transformer for cut
(def f11
λ.(+ 10 1))
(def v11
(f11 'ignored))
(module+ test
{v11 ≡ 11})
(def v11b
;; ((#%dot λ (+ 10 1)) 'ignored)
(λ.(+ 10 1) 'ignored))
(module+ test
{v11b ≡ 11})
(def v11c
(λ.(+ $ 1) 10))
(module+ test
{v11c ≡ 11})
;; ≙ and := are synonyms for def, and because of the {} rules, is a
;; binary operator.
{v33a ≙ 33}
{v33b := 33}
(module+ test
{v33a ≡ 33}
{v33b ≡ 33})
(def v28
{(f x) ≙ x + x}
(f 14))
(module+ test
{v28 ≡ 28})
;; def* allows nested binding inside blocks. This is aliased to nest
;; for def* transformers like parameterize that would look strange
;; otherwise.
(def v64
(def* x 2)
(def* x {x + x})
(def* x {x + x})
(nest x {x + x})
(def* x {x + x})
(def* x {x + x})
x)
(module+ test
{v64 ≡ 64})
;; The lambda and def syntax allow all the normal forms of Racket
;; function arguments. The main exception being rest arguments are
;; specified differently because the . would be parsed incorrectly
;; otherwise.
(def (f-no-args) 42)
(def (f-one-arg x) x)
;; => (def f-one-arg (λ (x1) (def x x1) x))
(def (f-kw-arg #:x x) x)
(def (f-kw-args #:x x y) (+ x y))
(def (f-def-arg (x 20) (y 22)) (+ x y))
(def (f-two-arg x y) (+ x y))
;; (f-rest-args . x) => ((#%dot f-rest-args x))
(def (f-rest-args #%rest x) 42)
(module+ test
{(f-no-args) ≡ 42}
{(f-one-arg 42) ≡ 42}
{(f-kw-arg #:x 42) ≡ 42}
{(f-kw-args #:x 22 20) ≡ 42}
{(f-two-arg 20 22) ≡ 42}
{(f-def-arg) ≡ 42}
{(f-def-arg 21) ≡ 43}
{(f-def-arg 21 21) ≡ 42}
{(f-rest-args) ≡ 42}
{(f-rest-args 1) ≡ 42}
{(f-rest-args 1 2 3) ≡ 42})
;; def supports a variety of "def transformers" that change from
;; defining a phase-0 value to something else.
;; val ensures that a function is NOT defined
(def [val v99] 99)
(module+ test
{v99 ≡ 99})
;; stx is define-syntax
(require (for-syntax remix/stx0))
(def [stx stx42] 42)
;; mac is define-simple-macro
(def [mac (flip f x y)]
(f y x))
(module+ test
{(flip - 5 0) ≡ (- 0 5)})
;; ... => (#%dot #%dot #%dot)
;; … (\ldots) is ... (because that doesn't work with cdots)
;; or dotdotdot or ***
(def [mac (flipper1 f x … y)]
(f y x …))
(def [mac (flipper2 f x dotdotdot y)]
(f y x dotdotdot))
(def [mac (flipper3 f x *** y)]
(f y x ***))
(module+ test
{(flipper1 - 5 9 0) ≡ (- 0 5 9)}
{(flipper2 - 5 9 0) ≡ (- 0 5 9)}
{(flipper3 - 5 9 0) ≡ (- 0 5 9)})
;; data gives us interfaces, compound data, and data types and that
;; sort of thing
(require remix/data0)
;; First, we can define static interfaces, which associate dot-terms
;; with particular functions.
(def (example-f x y) x)
(def (example-g x y) y)
(def [stx example^]
(static-interface
[f example-f]
[g example-g]))
(module+ test
{(example^.f 1 2) ≡ 1}
{(example^.g 1 2) ≡ 2})
;; These static interfaces allow nesting
(def example2-h 19)
(def [stx example2^]
(static-interface
[fg example^]
[h example2-h]))
(module+ test
{(example2^.fg.f 1 2) ≡ 1}
{(example2^.fg.g 1 2) ≡ 2}
{example2^.h ≡ 19}
;; Notice that cut works with nested dots
{(λ.example2^.h 'ignored) ≡ 19})
;; They are also def transformers and when used in that way, they
;; implicitly pass the binding on as the first argument to functions
;; when used.
(def [example^ ee] 1)
;; => (begin (define real-ee 1) (define-syntax ee ...magic...))
(module+ test
{(ee.f 2) ≡ 1}
;; => {(example^.f real-ee 2) ≡ 2}
;; => {(example^.f 1 2) ≡ 1}
{(ee.g 2) ≡ 2})
;; This is especially useful inside of functions
(def (f-using-example [example^ ee])
(ee.f 2))
(module+ test
{(f-using-example 1) ≡ 1})
;; Sometimes a static-interface's binding's result is another
;; static-interface, rather than the binding itself. In that case, we
;; use the keyword #:is and specify another def transformer for
;; contexts where the value is in tail position.
(def [stx example3^]
(static-interface
;; NB Perhaps it would be more punny to us [def id]?
[fg example2-fg #:is example^]
[h example2-h]))
(def example2-fg 1)
(module+ test
{(example3^.fg.f 2) ≡ 1}
{(example3^.fg.g 2) ≡ 2}
{example3^.h ≡ 19})
;; XXX show an example where it isn't an interface but any def
;; transformer.
;; The syntax of interface members is not limited to identifiers. In
;; particular, #:keywords are useful. Furthermore, static-interface is
;; a def transformer itself, to clean up the syntax a little bit. I
;; expect that most people will use it this way.
(def example4-kw-key '#:key)
(def example4-key 'key)
(def [static-interface example4^]
[#:key example4-kw-key]
[key example4-key])
(module+ test
{example4^.#:key ≡ '#:key}
{example4^.key ≡ 'key})
;; A layout is a container with no sealing or representation
;; guarantees. This means you can't necessarily protect the contents
;; nor can you necessarily tell that you have one when you do.
;; layout is a def-transformer (XXX I wish I could make it phase1
;; macro also but it needs to define some functions that could be
;; called)
;;
;; XXX maybe I can expand to a submodule and local-require
;; The most basic syntax is a list of fields, which are identifiers.
(def [layout posn]
x y)
(module+ test
;; You will get an allocation function named #:alloc
(def [posn p1] (posn.#:alloc [x 5] [y 7]))
;; XXX (def [posn p1] #:alloc [x 5] [y 7]) <--- def transformer for allocation
;; XXX (def [posn p1] (posn [x 5] [y 7])) <--- default use is allocation
;; And accessors
{p1.x ≡ 5}
{p1.y ≡ 7}
;; You may not have noticed, but posn was just a def transformer
;; that gave us access to these. We can, of course, just call them
;; directly through posn.
{(posn.x p1) ≡ 5}
;; You will also get a copying function
(def [posn p2] (p1.#:set [y {p1.y + 2}]))
;; XXX (def [posn p2] (posn p1 [y {p1.y + 2}])) <---- default use with expr is copy
;; Notice that these built-in functions are keywords, so that they
;; can't conflict with the fields you've defined.
{p2.x ≡ 5}
{p2.y ≡ 9}
;; This is aliased to =, which I expect is nicer to use.
(def [posn p3] (p1.#:= [x 8]))
{p3.x ≡ 8}
{p3.y ≡ 7})
;; A layout can have a parent, which provides the guarantee that the
;; parent's functions will work on the child---meaning that whatever
;; the layout ends up being (and you can't decide that), the two will
;; overlap in this specific way. A layout has one or zero parents.
(def [layout quat]
#:parent posn
z)
(module+ test
(def [quat q1] (quat.#:alloc [x 1] [y 2] [z 3]))
{q1.x ≡ 1}
{q1.y ≡ 2}
{q1.z ≡ 3}
;; We can consider to be posn (imaging calling some function that
;; expects one) and it just works
(def [posn qp1] q1)
{qp1.x ≡ 1}
{qp1.y ≡ 2}
;; However, that casting is computation-less, so it can be cast back
;; and we can get all the fields. However, if we changed it, it
;; wouldn't have stayed a quat.
(def [quat qpq1] qp1)
{qpq1.x ≡ 1}
{qpq1.y ≡ 2}
{qpq1.z ≡ 3})
;; XXX Does it do the "right thing" for copying? (i.e. when a parent
;; copies, do the child's fields get copied as is)
;; A layout's fields may be specified as other layouts. When the first
;; field is a layout, this is not necessarily the same thing as a
;; parent (like C structs) but it may be. (No matter what, you'd never
;; be able to tell, since layout doesn't make representation promises
;; as a rule.)
(def [layout circle]
[posn c] r)
(module+ test
(def [circle c1] (circle.#:alloc [c p1] [r 8]))
{c1.c.x ≡ 5}
{c1.c.y ≡ 7}
{c1.r ≡ 8})
;; A layout's fields can _actually_ just be any def transformer, and
;; thus could be static interfaces
(def [layout weird]
[example^ e])
(module+ test
(def [weird wr1] (weird.#:alloc [e 1]))
{(wr1.e.f 2) ≡ 1}
{(wr1.e.g 2) ≡ 2})
;; Now, the big reveal, layout has an extensible representation
;; planner system. At the moment, the only representations are
;;
;; layout-immutable : The default, backed by immutable vectors
;; layout-mutable : Backed by mutable vectors, with mutation support
;;
;; I expect to produce a few more
;;
;; (XXX) layout-c : Compatible with C
;; (XXX) layout-optimize : Optimize for removing padding and have
;; cache-line-aligned accesses
;; (XXX) layout-enumerate : Use data/enumerate
;;
;; It would be possible to make layout-c right now, but define-cstruct
;; is really slow. It is trivial to have layout-optimize if you have
;; layout-c, but it would not be useful to use. mflatt and I talked
;; about a fast way of implementing them in Racket. The basic idea is
;; to have a new type of object in the VM where the pointer goes to
;; the middle of the allocated space which looks like
;;
;; [ <raw-values> | <tag> <vector layout> ]
;;
;; There may be necessary padding, but then the existing vector
;; functions would work. The raw values would use computed offsets to
;; get the values. The goal would be that parent structs would just
;; work and it would be easy to pass to C by sorting the _racket
;; pointers to the end.
;;
;; Anyways, here's a mutable example.
(def [layout world]
#:rep layout-mutable
[circle c1] [circle c2])
(module+ test
(def [world w1] (world.#:alloc [c1 c1] [c2 (c1.#:set [r 3])]))
{w1.c1.r ≡ 8}
{w1.c2.r ≡ 3}
;; The set! is simultaneous
(w1.#:set! [c1 w1.c2] [c2 w1.c1])
{w1.c1.r ≡ 3}
{w1.c2.r ≡ 8}
;; It is aliased to !
(w1.#:! [c1 w1.c2] [c2 w1.c1])
{w1.c1.r ≡ 8}
{w1.c2.r ≡ 3})
;; These support mutual recursion
(def [layout even]
#:rep layout-mutable
e [odd o])
(def [layout odd]
#:rep layout-mutable
[even e] o)
(module+ test
(def [even even1]
(even.#:alloc
[e 0]
[o (odd.#:alloc
[e #f]
[o 1])]))
(even1.o.#:set! [e even1])
{even1.e ≡ 0}
{even1.o.o ≡ 1}
{even1.o.e.e ≡ 0}
{even1.o.e.o.o ≡ 1}
{even1.o.e.o.e.e ≡ 0})
;; Theories & Models
;; A theory is a specification of some values
(def [theory Monoid]
op id)
(module+ test
;; You can write generic functions over a theory. This imposes a
;; single constant cost to access the operations (basically, a
;; vector-ref) and the operation couldn't be inlined. (Although if
;; the generic function were inlined, then it could, presumably.)
(def (monoid-id-test [Monoid m] a)
;; Notice the syntax `m.(op x y)` as short-hand for `((m.op) x y)`
{((m.op) a m.id) ≡ m.(op m.id a)}))
;; A model is an object that satisfies the theory
(def [model Monoid Monoid-Nat:+]
[op +]
[id 0])
(def [model Monoid Monoid-Nat:*]
[op *]
[id 1])
(module+ test
;; You can pass the model explicitly to functions over the theory
(monoid-id-test Monoid-Nat:+ 5)
(monoid-id-test Monoid-Nat:* 5)
;; Or you can use it directly. This works exactly the same, although
;; we can imagine it might be inlinable.
{((Monoid-Nat:+.op) 6 Monoid-Nat:+.id) ≡ Monoid-Nat:+.(op Monoid-Nat:+.id 6)})
;; Interfaces & Classes
(def [interface 2d<%>]
translate
area)
(def [interface Circle<%>]
;; xxx make a macro for "interface of layout's fields"
c r)
;; A class is a representation, a constructor, and implementations of
;; interfaces.
(def [class Circle]
(def [rep] circle) ;; rep = representation
(def ([new] x y r)
(this.#:alloc [c (posn.#:alloc [x x] [y y])]
[r r]))
;; xxx make a macro from "layout's fields implements this interface"
(def [implementation Circle<%>]
[(c) this.c]
[(r) this.r])
(def [impl 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}]))
;; XXX allow w/o #:new?, like layout
(def [Circle C1] (Circle.#:new 1 2 3))
(module+ test
;; If you know something is a particular class, then you can access
;; its implementations directly. This is more efficient.
{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}
;; In contrast, when you access them as their interfaces, a lookup
;; is done.
(def [2d<%> C1-as-2d] C1)
{C1-as-2d.(area) ≡ 27}
(def [Circle<%> C1-as-Circ] C1)
{C1-as-Circ.c.x ≡ 1}
{C1-as-Circ.c.y ≡ 2}
{C1-as-Circ.r ≡ 3})
(module+ test
;; Like theories, you can define functions that are generic over an
;; interface.
(def (squarea [2d<%> o])
{o.(area) * o.(area)})
{(squarea C1) ≡ 729}
;; The default behavior of class dot-transformers on unknown methods
;; is to treat it as a generic function.
{C1.(squarea) ≡ 729})

82
remix/tests/static-interface.rkt Normal file
View File

@ -0,0 +1,82 @@
#lang remix
(require remix/stx0
remix/static-interface0
remix/num/gen0
(for-syntax remix/stx0))
(module+ test
(require remix/test0))
;; First, we can define static interfaces, which associate dot-terms
;; with particular functions.
(def (example-f x y) x)
(def (example-g x y) y)
(def [stx example^]
(static-interface
[f example-f]
[g example-g]))
(module+ test
{(example^.f 1 2) ≡ 1}
{(example^.g 1 2) ≡ 2})
;; These static interfaces allow nesting
(def example2-h 19)
(def [stx example2^]
(static-interface
[fg example^]
[h example2-h]))
(module+ test
{(example2^.fg.f 1 2) ≡ 1}
{(example2^.fg.g 1 2) ≡ 2}
{example2^.h ≡ 19}
;; Notice that cut works with nested dots
{(λ.example2^.h 'ignored) ≡ 19})
;; They are also def transformers and when used in that way, they
;; implicitly pass the binding on as the first argument to functions
;; when used.
(def [example^ ee] 1)
;; => (begin (define real-ee 1) (define-syntax ee ...magic...))
(module+ test
{(ee.f 2) ≡ 1}
;; => {(example^.f real-ee 2) ≡ 2}
;; => {(example^.f 1 2) ≡ 1}
{(ee.g 2) ≡ 2})
;; This is especially useful inside of functions
(def (f-using-example [example^ ee])
(ee.f 2))
(module+ test
{(f-using-example 1) ≡ 1})
;; Sometimes a static-interface's binding's result is another
;; static-interface, rather than the binding itself. In that case, we
;; use the keyword #:is and specify another def transformer for
;; contexts where the value is in tail position.
(def [stx example3^]
(static-interface
;; NB Perhaps it would be more punny to us [def id]?
[fg example2-fg #:is example^]
[h example2-h]))
(def example2-fg 1)
(module+ test
{(example3^.fg.f 2) ≡ 1}
{(example3^.fg.g 2) ≡ 2}
{example3^.h ≡ 19})
;; XXX show an example where it isn't an interface but any def
;; transformer.
;; The syntax of interface members is not limited to identifiers. In
;; particular, #:keywords are useful. Furthermore, static-interface is
;; a def transformer itself, to clean up the syntax a little bit. I
;; expect that most people will use it this way.
(def example4-kw-key '#:key)
(def example4-key 'key)
(def [static-interface example4^]
[#:key example4-kw-key]
[key example4-key])
(module+ test
{example4^.#:key ≡ '#:key}
{example4^.key ≡ 'key})
(provide example^)

282
remix/tests/stx.rkt Normal file
View File

@ -0,0 +1,282 @@
#lang remix
;; Remix comments start with ;;
;; #lang remix only contains two bindings: #%module-begin and require
;;
;; We use require to get everything else. most of it comes from stx0
require remix/stx0
remix/num/gen0;
;; A semi introduces a set of parens to its left
;; As usual `unquote` escapes from its context, in the case of a
;; semi-sequence, this means that the term is not wrapped.
,(module+ test
;; This introduces ≡ as a testing form
;; XXX Drop this and instead have a macro for writing down
;; properties that communicates with boolean forms, etc. Supports ∀,
;; etc.
(require remix/test0))
;; define is replaced with def
def z 42;
module+ test
{z ≡ 42};
;; when def has more forms than one, they are put inside of a block
def x
(def a 40)
(def b 2)
(+ a b) ;
,(module+ test
{x ≡ 42})
;; If you would like to use ;-syntax in the inside of def, then you
;; need more punctuation. You have two choices.
def x2
[def a 40;
def b 2;
(+ a b)];
,(module+ test
{x2 ≡ 42})
def x3
[def a 40;
def b 2;
{a + b}];
,(module+ test
{x3 ≡ 42})
def x4
[,{a := 40}
def b 2 ;
{a + b}];
(module+ test
{x4 ≡ 42})
;; but of course def supports function definitions. [] is NOT the same
;; as (), it parses as #%brackets and defaults to expanding to a block
;; definition
(def (f x y)
(+ [(def z (+ x x))
z]
y))
(module+ test
{(f x x) ≡ 126})
;; That's the same as just 'block' if you want to be specific
(def (other-f x y)
(+ (block (def z (+ x x))
z)
y))
(module+ test
{(other-f x x) ≡ 126})
;; cond requires []s for the question-answer pairs. It uses this to
;; make any code in between clauses go in between the `if`s that pop
;; out of the cond macro.
(def (g x)
(cond
[(< x 100) "100"]
(def z (/ x 2))
[(< z 100) "div 100"]
[#:else z]))
(module+ test
{(g 50) ≡ "100"}
{(g 199) ≡ "div 100"}
{(g 200) ≡ 100})
;; If cond reaches the end without an else, then a runtime error is
;; generated
(def (g2 x)
(cond
[(< x 100) "100"]
(def z (/ x 2))
[(< z 100) "div 100"]))
(module+ test
{(g2 50) ≡ "100"}
{(g2 199) ≡ "div 100"}
;; This is the error test:
#;(g2 200))
;; This functionality is provided by ☠ (aka impossible!)
(def (g3)
☠)
(module+ test
#;(g3))
;; the @ reader is always on. One fun thing about this is that you can
;; make non-() macros. I wrote a little helper function to turn the
;; string arguments that @{} produces into a string port that has
;; accurate source location information for the original file. datalog
;; uses this to make all the source locations correct, so errors in
;; datalog will give accurate source locations.
(require remix/datalog0)
(def graph (make-theory))
@datalog[graph]{
edge(a, b). edge(b, c). edge(c, d). edge(d, a).
path(X, Y) :- edge(X, Y).
path(X, Y) :- edge(X, Z), path(Z, Y).
path(X, Y)?
}
;; {} is also not (), it is parsed as #%braces, and by default is an
;; infix macro
(def v7
{3 + 4})
(module+ test
{v7 ≡ 7})
;; {} use C's precedence and considers the things you expect to be
;; operators. there's a syntax-time struct property that allows you to
;; specify what you want the precedence of an operator to be.
(def v-26
{2 * 3 - 48 / 4 - 4 * 5})
(module+ test
{v-26 ≡ -26})
;; if a symbol contains no alphabetic or numeric characters, then it
;; is considered an operator. This means you can automatically use
;; stuff like & and →, but you won't confuse it with symbols like z
(def v85
{z * 2 + 1})
(module+ test
{v85 ≡ 85})
(def v1
(def & bitwise-and)
{5 & 1})
(module+ test
{v1 ≡ 1})
(def v56
(def (→ x y) (+ (* x x) y))
{v7 → v7})
(module+ test
{v56 ≡ 56})
;; However, if you use , then you can force anything to be a binary
;; operator and force something that would have been a binary operator
;; into an argument.
(def v14
(def (f x y) (+ x y))
{v7 ,f v7})
(module+ test
{v14 ≡ 14})
(def v14b
{v7 ,(λ (x y) (+ x y)) v7})
(module+ test
{v14b ≡ 14})
(def v9
(def & 2)
{v7 + ,&})
(module+ test
{v9 ≡ 9})
;; λ is a dot-transformer for cut
(def f11
λ.(+ 10 1))
(def v11
(f11 'ignored))
(module+ test
{v11 ≡ 11})
(def v11b
;; ((#%dot λ (+ 10 1)) 'ignored)
(λ.(+ 10 1) 'ignored))
(module+ test
{v11b ≡ 11})
(def v11c
(λ.(+ $ 1) 10))
(module+ test
{v11c ≡ 11})
;; ≙ and := are synonyms for def, and because of the {} rules, is a
;; binary operator.
{v33a ≙ 33}
{v33b := 33}
(module+ test
{v33a ≡ 33}
{v33b ≡ 33})
(def v28
{(f x) ≙ x + x}
(f 14))
(module+ test
{v28 ≡ 28})
;; def* allows nested binding inside blocks. This is aliased to nest
;; for def* transformers like parameterize that would look strange
;; otherwise.
(def v64
(def* x 2)
(def* x {x + x})
(def* x {x + x})
(nest x {x + x})
(def* x {x + x})
(def* x {x + x})
x)
(module+ test
{v64 ≡ 64})
;; The lambda and def syntax allow all the normal forms of Racket
;; function arguments. The main exception being rest arguments are
;; specified differently because the . would be parsed incorrectly
;; otherwise.
(def (f-no-args) 42)
(def (f-one-arg x) x)
;; => (def f-one-arg (λ (x1) (def x x1) x))
(def (f-kw-arg #:x x) x)
(def (f-kw-args #:x x y) (+ x y))
(def (f-def-arg (x 20) (y 22)) (+ x y))
(def (f-two-arg x y) (+ x y))
;; (f-rest-args . x) => ((#%dot f-rest-args x))
(def (f-rest-args #%rest x) 42)
(module+ test
{(f-no-args) ≡ 42}
{(f-one-arg 42) ≡ 42}
{(f-kw-arg #:x 42) ≡ 42}
{(f-kw-args #:x 22 20) ≡ 42}
{(f-two-arg 20 22) ≡ 42}
{(f-def-arg) ≡ 42}
{(f-def-arg 21) ≡ 43}
{(f-def-arg 21 21) ≡ 42}
{(f-rest-args) ≡ 42}
{(f-rest-args 1) ≡ 42}
{(f-rest-args 1 2 3) ≡ 42})
;; def supports a variety of "def transformers" that change from
;; defining a phase-0 value to something else.
;; val ensures that a function is NOT defined
(def [val v99] 99)
(module+ test
{v99 ≡ 99})
;; stx is define-syntax
(require (for-syntax remix/stx0))
(def [stx stx42] 42)
;; mac is define-simple-macro
(def [mac (flip f x y)]
(f y x))
(module+ test
{(flip - 5 0) ≡ (- 0 5)})
;; ... => (#%dot #%dot #%dot)
;; … (\ldots) is ... (because that doesn't work with cdots)
;; or dotdotdot or ***
(def [mac (flipper1 f x … y)]
(f y x …))
(def [mac (flipper2 f x dotdotdot y)]
(f y x dotdotdot))
(def [mac (flipper3 f x *** y)]
(f y x ***))
(module+ test
{(flipper1 - 5 9 0) ≡ (- 0 5 9)}
{(flipper2 - 5 9 0) ≡ (- 0 5 9)}
{(flipper3 - 5 9 0) ≡ (- 0 5 9)})

35
remix/tests/theory.rkt Normal file
View File

@ -0,0 +1,35 @@
#lang remix
(require remix/stx0
remix/theory0
remix/num/gen0)
(module+ test
(require remix/test0))
;; A theory is a specification of some values
(def [theory Monoid]
op id)
(module+ test
;; You can write generic functions over a theory. This imposes a
;; single constant cost to access the operations (basically, a
;; vector-ref) and the operation couldn't be inlined. (Although if
;; the generic function were inlined, then it could, presumably.)
(def (monoid-id-test [Monoid m] a)
;; Notice the syntax `m.(op x y)` as short-hand for `((m.op) x y)`
{((m.op) a m.id) ≡ m.(op m.id a)}))
;; A model is an object that satisfies the theory
(def [model Monoid Monoid-Nat:+]
[op +]
[id 0])
(def [model Monoid Monoid-Nat:*]
[op *]
[id 1])
(module+ test
;; You can pass the model explicitly to functions over the theory
(monoid-id-test Monoid-Nat:+ 5)
(monoid-id-test Monoid-Nat:* 5)
;; Or you can use it directly. This works exactly the same, although
;; we can imagine it might be inlinable.
{((Monoid-Nat:+.op) 6 Monoid-Nat:+.id) ≡ Monoid-Nat:+.(op Monoid-Nat:+.id 6)})

66
remix/theory0.rkt Normal file
View File

@ -0,0 +1,66 @@
#lang racket/base
(require (for-syntax racket/base
syntax/quote
syntax/parse
racket/syntax
racket/generic
racket/format
racket/list
racket/match
(prefix-in remix: remix/stx0)
remix/stx/singleton-struct0
(for-syntax racket/base
racket/syntax
syntax/parse
racket/generic
(prefix-in remix: remix/stx0)))
racket/stxparam
racket/unsafe/ops
racket/performance-hint
(prefix-in remix: remix/stx0)
remix/layout0)
(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)
;; XXX support parameters
[(remix:def (remix:#%brackets theory thy:id)
;; XXX support properties (including type)
;; XXX make expandable position
v:id ...)
(syntax/loc stx
(remix:def (remix:#%brackets layout thy)
;; XXX add a property for theories
;; XXX support defaults
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)
;; XXX make expandable position
(remix:#%brackets f:id v:expr) ...)
;; XXX support verification of properties
;; XXX support theory parameters
;; XXX check that thy is a theory
;; XXX check that f is complete and apply defaults if not
(syntax/loc stx
(remix:def (remix:#%brackets thy mod)
(remix:#%app
(remix:#%dot thy #:alloc)
(remix:#%brackets f v) ...)))]))]))
(provide theory
model)