You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
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.
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.
The text was updated successfully, but these errors were encountered: