cdonovick
commented
3 years ago (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
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.