More Flexibility for LDT Bindings

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

The loading of key files is not homogenous. A special type of files, the logic-datatype files (LDT) are treated specially. The reason is, that these files are also have a Java counterpart, the LDT classes, e.g. SeqLDT. The LDT classes are used to bind the declared logical entities (functions, predicates, etc...) to Java variables. The binding is established after all LDT files have been loaded.

A drawback of this approach is the lack of extensibility and complexity in the file loading logic.

I suggest following change:

• Syntax: We add a new keyword and command to key files:

  \binding "classname"; 
  

• Semantics: After the loading stages: ground entities (variables, choices, ...), 2nd level (predicate, functions, transformers) and the third level (taclets), the bindings are evaluated.

  Evaluation of a binding means, that the given class (with the given name) is instantiated with the current constructed Services object.

  If the given class is of type LDT, it is added to the list of type converters (LDTs).

  LDTs can be queried by classname to receive an instance.

---

Information:

• created_at: 2020-07-02T22:59:27.506Z
• updated_at: 2022-04-06T09:49:53.280Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 9