Processing a Unit

The command to process a unit is:

proc [unit-term]

The argument can be any unit term: a simple unit identifier, a diagram colimit, a proof term, and so on.

If the argument is not a syntactically valid unit term, or some unit identifier in the term fails to resolve as explained in the Section called SWPATH-Based Unit Identifier, an error is signaled by Specware.

Otherwise Specware parses and elaborates the unit term that results from resolution. Parsing and elaboration carry out the computations to construct the unit; they are Specware's "core" functionality. Parsing and elaboration implement the semantics of the Metaslang language.

In this process, Specware performs further checks on the requirements as stated in the language manual, such as non-ambiguity of names. If any errors are found, they are signaled

If the unit term references other units, Specware recursively resolves the unit identifiers and parses and elaborates their unit terms.

Finally, if all went well, Specware typechecks the unit resulting from the elaboration process, if applicable, and signals any errors detected.

The elaboration of some unit terms may have side effects: code generation; prover invocation. This is only done if no error was encountered. Code can also be generated directly from the Specware Shell using the gen-Language commands. For proving properties in specs, see Chapter 6.

Without argument, the proc command re-processes the last unit term given. It is an error if no unit term was given before.

It is also possible to process a multiple-unit file all at once:

proc multi-unit-identifier

The unit identifier must not contain "#" and the file must not contain a unit of the same name as the file (without the directory and extension). Specware attempts to resolve the unit identifier. If it is a relative unit identifier, it is resolved as if it occurred inside a single-unit file in the current directory. However, the file obtained at the third step must be a multi-unit file, and not a single-unit file. If it is indeed a multi-unit file, Specware parses and elaborates all the unit definitions inside the file.

The command proc may be abbreviated to p.

The values of processed units are kept in the unit cache. To clear the unit cache, as mentioned before, use:

cinit

(Cache INITialize).