Unit terms may reference units in the form of unit identifiers. A unit identifier is resolved to the unit's term, which is contained in a .sw file. Unit identifiers are either SWPATH-based or relative; these two kinds are syntactically distinguished from each other and are resolved in slightly different ways.
A SWPATH-based unit identifier starts with "/", followed by a "/"-separated sequence of one or more path elements, where the last separator may be "#". Examples are /a/b/c, /d, and /e#f.
Specware resolves a SWPATH-based unit identifier in the following steps:
If the unit identifier contains "#", the "#" itself and the path element following it are removed, obtaining a "/"-separated sequence of one or more path elements, preceded by "/". Otherwise, no removal takes place. Either way, the result of this first step is a "/"-separated sequence of path elements preceded by "/".
The "/" signs of the "/"-separated sequence of path elements preceded by "/", resulting from the previous step, are turned into "\"; in addition, .sw is appended at the end. The result of this second step is a (partial) path in the file system.
The path resulting from the previous step is appended after the first directory of SWPATH. If the resulting absolute path denotes an existing file, that is the result of this third step. Otherwise, the same attempt is made with the second directory of SWPATH (if any). Attempts continue until a directory is found in SWPATH such that the absolute path obtained by concatenating the directory with the result of the previous step denotes an existing file; such a file is the result of this step. If no such directory is found, the unit identifier cannot be resolved and an error is signaled by Specware.
There are two alternative steps here, depending on whether or not the original unit identifier contains "#".
This is the case that the original unit identifier does not contain "#". If the file resulting from the previous step is a single-unit file, i.e., it contains a unit term, that the final result of resolution. Otherwise, an error is signaled by Specware.
This is the case that the original unit identifier contains "#". The file resulting from the previous step must be a multiple-unit file, i.e., it must contain a sequence of one or more unit definitions. If this is not the case, the unit identifier cannot be resolved and an error is signaled by Specware. If that is the case, a unit definition is searched in the file, whose path elements (to the left of "=") is the same as the path element that follows "#" in the original unit identifier. If no such unit definition is found, the unit identifier cannot be resolved and an error is signaled by Specware. If such a unit definition is found, its unit term (at the right of "=") is the final result of resolution.
For example, consider a unit identifier /a/b/c. Since it does not contain "#", the first step does not do anything. The result of the second step is \a\b\c.sw. Suppose that SWPATH is c:\users\me\specware;c:\tmp, that c:\users\me\specware does not contain any a subdirectory, and that c:\tmp\a\b\c.sw exists. The result of the third step is the file c:\tmp\a\b\c.sw. If such a file is a single-unit file, its content is the result of the fourth step.
As another example, consider a unit identifier /e#f. The result of the first step is /e. The result of the second step is \e.sw. Assuming that SWPATH is as before and that c:\users\me\specware contains a file e.sw, the file c:\users\me\specware\e.sw is the result of the third step. The file must be a multiple-unit file. Assuming that this is the case and that it contains a unit definition with path element f, its unit term is the result of the fourth step.
The directories in SWPATH are searched in order during the third step of resolution. So, in the last example, if the directory c:\tmp also contains a file e.sw, such a file is ignored. This features can be used, for example, to shadow selected library units that populate certain file system directories in SWPATH.
For example, suppose that the first directory in SWPATH is c:\specware\libs and that the directory c:\specware\libs\data-structures contains files Sets.sw, Bags.sw, Lists.sw, etc. defining specs of sets, bags, lists, etc. The unit identifier /data-structures/Sets resolves to the content of the file c:\specware\libs\data-structures\Sets.sw. If the user wanted to experiment with a slightly different version of the spec for sets, it is sufficient to prepend another directory to SWPATH, e.g. c:\shadow-lib, and to create that slightly different version of the spec for sets in c:\shadow-lib\data-structures\Sets.sw. The same unit identifier /data-structures/Sets will now resolve to the new version.
A relative unit identifier is a "/"-separated sequence of one or more path elements, where the last separator can be "#". Examples are a/b/c, d, and e#f. So, SWPATH-based and relative unit identifiers can be distinguished by the presence or absence of "/" at the beginning.
The resolution of relative unit identifiers does not depend on SWPATH, but on the location of the file where the unit identifier occurs. There are two cases to consider: the unit identifier occurring in a single-unit file and the unit identifier occurring in a multiple-unit file.
Suppose that the relative unit identifier occurs in a single-unit file. Then Specware attempts to resolve the unit identifier in the following steps:
If the unit identifier contains "#", the "#" itself and the path element following it are removed, obtaining a "/"-separated sequence of one or more path elements. Otherwise, no removal takes place. Either way, the result of this first step is a "/"-separated sequence of path elements.
The "/" signs of the "/"-separated sequence of path elements, resulting from the previous step, are turned into "\"; in addition, .sw is appended at the end. The result of this second step is a (partial) path in the file system.
The path resulting from the previous step is appended after the absolute path of the directory of the file containing the relative unit identifier. If the resulting absolute path denotes an existing file, that is the result of this third step. Otherwise, the unit identifier cannot be resolved and an error is signaled by Specware.
There are two alternative steps here, depending on whether the original unit identifier contains "#" or not.
This is the case where the original unit identifier does not contain "#". If the file resulting from the previous step is a single-unit file, i.e., it contains a unit term, that is the final result of resolution. Otherwise, an error is signaled by Specware.
This is the case that the original unit identifier contains "#". The file resulting from the previous step must be a multiple-unit file, i.e., it must contain a sequence of one or more unit definitions. If this is not the case, the unit identifier cannot be resolved and an error is signaled by Specware. If that is the case, a unit definition is searched in the file, whose path element (at the left of "=") is the same as the path element that follows "#" in the original unit identifier. If no such unit definition is found, the unit identifier cannot be resolved and an error is signaled by Specware. If instead such a unit definition is found, its unit term (to the right of "=") is the final result of resolution.
So, resolution of a relative unit identifier occurring in a single-unit file is like resolution of a SWPATH-based unit identifier, except that the directory where the identifier occurs is used instead of SWPATH.
Suppose, instead, that the relative unit identifier occurs in a multiple-unit file. Then Specware attempts to resolve the unit identifier in the following steps:
If the relative unit identifier is a single path element, Specware attempts to find a unit definition with that path element inside the file where the unit identifier occurs. If such a unit definition is found, its unit term is the final result of resolution. Otherwise, the following steps are carried out:
If the unit identifier contains "#", the "#" itself and the path element following it are removed, obtaining a "/"-separated sequence of one or more path elements. Otherwise, no removal takes place. Either way, the result of this first step is a "/"-separated sequence of path elements.
The "/" signs of the "/"-separated sequence of path elements, resulting from the previous step, are turned into "\"; in addition, .sw is appended at the end. The result of this second step is a (partial) path in the file system.
The path resulting from the previous step is appended after the absolute path of the directory of the file containing the relative unit identifier. If the resulting absolute path denotes an existing file, that is the result of this third step. Otherwise, the unit identifier cannot be resolved and an error is signaled by Specware.
There are two alternative steps here, depending on whether the original unit identifier contains "#" or not.
This is the case that the original unit identifier does not contain "#". If the file resulting from the previous step is a single-unit file, i.e., it contains a unit term, that is the final result of resolution. Otherwise, an error is signaled by Specware.
This is the case that the original unit identifier contains "#". The file resulting from the previous step must be a multiple-unit file, i.e., it must contain a sequence of one or more unit definitions. If this is not the case, the unit identifier cannot be resolved and an error is signaled by Specware. If that is the case, a unit definition is searched in the file, whose path element (at the left of "=") is the same as the path element that follows "#" in the original unit identifier. If no such unit definition is found, the unit identifier cannot be resolved and an error is signaled by Specware. If instead such a unit definition is found, its unit term (to the right of "=") is the final result of resolution.
So, resolution of a relative unit identifier occurring in a multiple-unit file is like resolution of a relative unit identifier occurring in a single-unit file, preceded by an attempt to locate the unit in the file where the identifier occurs, only in case such a unit identifier is a path element.