Family issues

[rdaly525]

This is a tracker for resolving family issues:

The major issue is that different codepaths make different assumptions regarding families

In a peak program there are 4 use cases of families.

(1) Type annotations on call
(2) Constant values
(3) Type matching for Sum/TaggedUnions
(4) Dynamic ADT constructors (family.get_constructor
(5) Type annotations on init values

We need to decide whether to use the passed in family or a particular kind of family (Py) for each of these 4 cases.

Constraints:
(2) needs to be the passed in family.
(4) needs to be the passed in family (I suspect)

Current state:
Some code paths assume (1) and (3) assume the family is Py and other assume it is the passed in family.

My preference is to have all 1-4 be using the passed in family.

[cdonovick]

(4) Type constructors

Assuming you mean ADT constructors (the only user facing type constructors in peak other than BitVector). They are agnostic to all types, so I don't understand the constraint you later reference.

Some code paths assume (1) and (3) assume the family is Py

Which code paths? (See constraints for the one place I am aware of)

other assume it is the passed in family

Which code paths?

Constraints:

• Magma requires the annotations be the assembled versions of an adt. To achieve this the magma family replaces the annotations with their assembled variants.
• The assembler can only assemble py adts. Its doesn't know how to handle a Bits or SMTBitVector field. As there is no way to convert them to other bitvector types.

[rdaly525]

Sorry, yeah for (4) I meant the dynamic ADT value constructor methods ( family.get_constructor(T) ). For Py, this just returns the same type, and for SMT/Magma, it returns the relevant Assembled type's from_fields method.