Generating Lisp Code

Lisp code can be generated by constructing a Metaslang unit containing a target-code term (using generate lisp) and by processing such unit via the proc command.

The Specware Shell provides a command to accomplish the same result without actually creating a separate Metaslang unit. The command is:

gen-lisp [spec-term [filename] ]

The spec term is processed by Specware. If this argument is missing, the last spec term processed is used. If the spec is successfully processed, Specware generates Lisp code from it (according to the semantics of generate lisp) and deposits the resulting code into the file whose path is given by the filename. The .lisp file extension can be omitted.

The filename to gen-lisp is also optional. If it is not given, a file name is inferred. If the spec term given as argument is a unit identifier, Specware deposits the generated code into the file U.lisp, where U is the rightmost path element comprising the unit identifier. The U.lisp file is deposited in a lisp subdirectory immediately under the directory of the file containing the unit term of the spec identified by the unit identifier given as argument to gen-lisp.

For example, suppose that the first directory in SWPATH is C:\users\me\specware and that a spec is defined in the single-unit file C:\users\me\specware\two\A.sw. If the user gives the command:

gen-lisp /two/A

the Lisp code is deposited into the file C:\users\me\specware\two\lisp\A.lisp.

As another example, suppose that SWPATH is as before and that a spec is defined in the multiple-unit file C:\users\me\specware\two\F.sw, and that B is the path element associated with the spec. If the user then gives the command:

gen-lisp /two/F#B

the Lisp code is deposited into the file C:\users\me\specware\two\lisp\B.lisp.

If the spec term given as argument is not a unit identifier, Specware deposits the generated code in a file under C:\tmp\sw\lisp, if possible. In all cases the name of the Lisp file is shown on the output.

The shell command

lgen-lisp [spec-term [filename] ]

is like gen-lisp, but generates code only for the local definitions of the spec and not any of the imports. It is intended for incremental development. Note that if you have not generated code for the imported specs and loaded it, trying to run the code generated by this command will give undefined function errors. Also, if the spec is unqualified but it is imported into a spec that is qualified, the package used will be :SW-USER instead of the package of the qualifier. To avoid this problem, qualification can be added to the spec.