Support multiple ellipses

Issue #24 resolved
Alex Knauth
created an issue

In places like the target clause here:

   [() ([state : State  state-] ...)  
    [[init-state  init-state-]  : State]
    [[target  target-]  : State] ... ...]

The implementation will have to use something like stx-append*-lens to flatten and un-flatten the syntax list while preserving the structure, similar to how this works around the problem:

   [#:with (t ...) 
           (lens-view stx-append*-lens #'((target ...) ...))]
   [() ([state : State  state-] ...)  
    [[init-state  init-state-]  : State]
    [[t  t-]  : State] ...]
   [#:with ((target- ...) ...) 
           (lens-set stx-append*-lens #'((target ...) ...) #'(t- ...))]

Comments (2)

  1. Stephen Chang repo owner

    The above example now works but this does not:

    (define-typed-syntax let-symbolic
      [(_ ([(x:id ...+) pred : ty:type] ...) e) 
       [ [pred  pred-  : (C→ ty.norm Bool)] ...]
       [([x  x- : ty.norm] ... ...)  [e  e-  τ_out]]
       --------
       [ [_  (ro:let-values 
                ([(x- ...) (ro:let () 
                             (ro:define-symbolic x ... pred) 
                             (values x ...))] ...) 
                e-)  : τ_out]]])
    
  2. Log in to comment