This is about supporting declarations of algebraic data types and enabling reasoning about their values as pure terms.
In hiptypes.ml, the definition of types (typ) needs to change, same for the term language as ADT values/operations need to be added
Type declarations are structure items, so they can be handled by transform_str in core_lang.ml
The caller of transform_str is process_items in hiplib.ml. It updates prog, so adding the types there is one option. It's likely easier to use a global variable for them (globals.ml), as they need to be passed all the way down to the prover
forward_rules.ml has to be updated for match to be aware of ADT values
infer_types.ml has to be updated to produce those types when encountering ADT values
Both Z3 and Why3 have support for algebraic data types, so both can be implemented, but Z3 is easier to start with
This is about supporting declarations of algebraic data types and enabling reasoning about their values as pure terms.