[bitc-dev] Addition of DEFREPR

[Swaroop Sridhar]

Jonathan S. Shapiro wrote:
> Here is another possible way to handle this (I am simply thinking out
> loud here):
> 
> 1. Adopt the view that the tags are arity-0 enumeration constructors, as
> I described above.
> 
> 2. Assign field names to the tags, so my example above would now change
> to:
> 
> (defrepr dr
>    (swizzled: (tag yes no)
>     d:double
>     direction: (tag left right)
>     (case ((swizzled yes) (i:int32 j:int32))
>           ((swizzled no)(b:bool)))
>     (case ((or (swizzled yes)
>                (direction left)) (k:int32)))))

If the cases do not completely cover the tag values, I guess it will 
result in a structure containing only the invariant positions.

For example:
  (defrepr dr
     (swizzled: (tag yes no)
      d:double
      direction: (tag left right)
      (case ((and (swizzled yes)
                  (direction left)) (k:int32))))

However, we need to check for overlap for the same tags within the same 
case, because at a time, only one leg of the case must be active.

For example:
  (defrepr dr
     (swizzled: (tag yes no)
      d:double
      direction: (tag left right)
      (case ((and (swizzled yes)
                  (direction left)) (k:int32))
	   ((or (swizzled yes)
                  (direction left)) (p:int64))))

This is especially true if we move to the design where we allow things like:
  (defrepr dr
     (swizzled: (tag bool)
      d:double
      swizzled2: (tag int32)
      ... )

Also, in this case, we may need an otherwise clause.

> 3. Take your strategy, but drop the wrapping defunion. Instead, convert
> them into:
> 
>     (defstruct __con_dr-swizzled-right
>         swizzled:__tag_dr_swizzled
>         d:double
>         direction:__tag_dr_direction
>         i:int32 j:int32))
> 
> 4. Now introduce a special rule into the type checker stating that if
> "dr" is a DEFREPR type and "__con_dr_xxxxx" is a structure type, then
> 
>     dr <- __con_dr_xxxxx
> 
> is a legal assignment/binding (but not the other way).

This can be done, I don't see any problem at this time.

>>So,
>>(reprcase e ((id swizzled right  id.d))
>>              (otherwise 0.0))
>>
>>||
>>V
>>
>>(reprcase e ((id:__dr-swizzled-right swizzled right  id.d))
>>              (otherwise 0.0))
>>
>>As you have noted in the spec, we may do this for all unions as well.
> 
> Not quite, but I figured out this morning how to deal with the last
> complication, and it becomes very easy if the tag slots have names.

Are you saying that there is a problem for repcase, or for unions?


> Not quite, but I figured out this morning how to deal with the last
> complication, and it becomes very easy if the tag slots have names.
> Given a DEFREPR of the form: 
>   (defrepr something
>          ...
>          tagname : (tag id1 id2)
>          (case ((tagname id1) ...)
>                ...)
>          ...)
> 
> we can add a declaration of some sort indicating that the tag can be
> Cardelified. Perhaps:
> 
>   (defrepr something
>          ...
>          tagname : (tag id1 id2)
>          (declare (cardelli tagname))
>          (case ((tagname id1) ...)
>                ...)
>          ...)
> 
> This applies only to the CASE form that positionally follows the tag.

Doesn't this also require that no other case forms use the tag values?
Unless there is a compelling example, I actually liked the fact that 
defreprs will not be Cardellified. Or, are you are thinking about a way 
to move towards defreprs and remove defstructs and defunions?


> I also thought that this could be made to work, but it has strange
> consequences. Consider:
> 
>   (let ((yes 1))
>     (dr yes 2.0 left 5 6))
> 
> where the intention is that this will turn into:
> 
>   (__con_dr-swizzled-right __tag_dr-swizzled-yes 2.0
>         __tag-dr-direction-left 5 6)
> 
> but it is not clear why the original "yes" tag is not hidden here. I
> believe that this is essentially the same ambiguity that arises for
> constructors in applicative position elsewhere in the type checker.
> 
> Can you articulate a clear-cut story for this, or if not, should we
> consider making the initializer labels bound in the defining scope.

Actually, lifting them to the defining scope does not help. That will 
prevent a top-level definition from overriding that name, but a 
let/letrec definition is able to override value constructors or other 
bindings.

However, if the tags are treated as value matching,

  (defrepr dr
     (swizzled: (tag bool)
      d:double
      swizzled2: (tag int32)
      ... )

(dr #t 2.0 .. )

(let ((yes #t))
   (dr yes 2.0 ... )

then there is nothing to bind, and this issue goes away.

>>Is the rule:
>>
>>>A case form may make reference to any tagid that is mentioned in any 
>>>lexically preceding tag form within the same defrepr
>>
>>necessary? Conceptually, the compiler can process all tag forms first, 
>>so that all legs can make use all tags. I think, in the case of GDT 
>>entries, some fields come before the tag.
> 
> 
> Hmm. Now that is an *excellent* question, and I need to think about
> that. It follows from the ability to flatten to structures that you hvae
> identified, and that I had completely failed to see. Even if we decide
> to do named fields for tags, we can adopt the rule that they "hoist to
> the left in preorder" for purpose of forming constructor arguments.
> 
> However, I think that we must impose the requirement that a CASE form
> can only reference a tag that appears in a lexically containing BODY
> form. Otherwise it will not be possible to do case-dispatch reliably in
> REPRCASE.

I agree.


Swaroop.