(Polymorphic) algebraic datatypes

[dariusf]

• In hiptypes.ml, the definition of types 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
• infer_types.ml has to be updated to produce those types when encountering values of ADTs
• forward_rules.ml has to be updated to for match to be aware of ADT types
• Both Z3 and Why3 have support for algebraic data types, so both can be implemented