HOL-CASL Parser

List of known problems

• In general, the static semantic checking is too liberal at some places
• The ATerm output of the global environment can become quite large. Use the -e option to suppress the output of the global environment as ATerms. The textual representation (xxx.env) is up to 90% shorter!
• Due to size problems, we have excluded some libraries from the built-in library of basic datatypes. If you need these libraries, you have to provide them explicitly under $CASL_LIB/Basic/ (they come with the distribution).

  Basic specifications

• Basic specifications admit non-linear visibility (while the Summary specifies linear visibility)
• The error messages of the static checker could be better
• The overload resolution is based on an old version of the overload relations, but only in relatively subtle cases, this makes a difference
• Bracket balancing within mixfix identifiers is not checked

  Structured specifications

• The static analysis of symbol maps does not handle qualifications
• The static analysis of instantiations of generics is implemented in an ad-hoc way, basically using just renaming, and is not (yet) what is specified in the Summary. In particular, implicit fitting maps and fitting views do not work.
• The static analysis of symbiols maps in views is missing

  Architectural specifications

• The static analysis is completely missing here.

  Libraries

• Libraries are only treated in a rudimentary way. You always have to use PATHs, which are interpreted relatively to directory specified with $CASL_LIB, except that PATHs of form Basic/xxx refer to the Basic Datatypes. Version numbers are just ignored.