preserve class annotations in Leon's AST

[larsrh]

Follow-up to 3e4281d. Uses mutable state to imitate similar other properties of ClassDefs.

[manoskouk]

Why do you need this? In my opinion, it seems more elegant to have a specific class that captures the functionality we want, as in FunDef, rather than a Map[String, Seq[Option[Any]]]. Unless you really need the general case.

[larsrh]

You mean like FunctionFlag, or just giving a dedicated type to (String, Seq[Option[Any]])?

[manoskouk]

Like FunctionFlag

[larsrh]

Okay, I can do that. Although it'll have only one subclass now, namely Annotation.

[larsrh]

@manoskouk See now 19a6960.

Why do you need this?

Forgot to answer this: Function annotations can be used for declaring a mapping of Leon functions to Isabelle functions. For example, I can specify that List#map should be mapped to List.list.map in Isabelle. Class annotations can be used in the same way for declaring datatype mappings. With those, I specify that Leon's List ADT gets mapped to the List.list datatype.

[colder]

Merged, thanks!