Libraries in hol90

A library is intended to provide an environment for doing HOL work in. There are three components that an environment provided by a library may have: logical theories, code, and help. When a library is loaded, new theories may become available for use, new code may be loaded in, and the online help manual ought to be augmented. It may be that a library depends on other libraries; these are recursively loaded in before the library itself loads.

Warning: the hol90 implementation of libraries is quite different from that of hol88!

User Manual Table of Contents

Getting a library

A library is represented by a group of files on disk, and by a corresponding internal representation: a value of type lib. It is values of this type that the hol90 library functions manipulate; therefore, to use a library, one must first get its description so that hol90 knows what it is dealing with. There are several ways to get a library description:

Beginning of Libraries.
User Manual Table of Contents.

Using a library

Once one has a library description, the environment provided by the library can be set up. This is simply done with a call to the function load_library.
    val load_library: {lib :lib, theory :string} -> unit
There is a subtlety in load_library having to do with the relationship between the current theory and the theories that the library provides. (If the library doesn't provide any theories, there is no difficulty.) The question is whether we want to load the theories provided by the library, or make them new parents. The distinction is technical, but it can easily be the case that one can not load a theory provided by a library because it is not a descendant of the current theory at the time of invocation. One may simply be in the wrong part of the theory graph for load_theory to work.

It is much more robust to make the theories of a library parents of the current theory (if they are not already, that is). The problem then becomes the fact that new_parent must be invoked in draft mode, i.e., the user must already be in an "unclosed" theory. Suppose the current theory is not in draft mode. Then the simplest thing to do is to make a call to new_theory with a suitable name. We force the user to give this name at the time load_library is called; this is the theory field of the call. (If the library to be loaded has no theories, or the system is already in draft_mode, then theory is ignored; putting a "-" would cohere with the use of "-" as an abbreviation for the current theory.)


If one just starts up hol90, one is in the HOL theory, which is not in draft mode. If we want to play around with the theory of strings, then we would do
    load_library{lib = Sys_lib.string_lib, theory = "foo"}
This places us in a new theory foo, with the theory string as its parent.

With that discussion out of the way, what happens in a call to load_library? First, the parent libraries are recursively loaded, if there are any. Then we check if there are any theories provided by the library. If there are, we are either in draft mode, or we put ourselves into draft mode (if the theories are not already parents!) by the mechanism just discussed. Now the theories are made new parents of the current theory (if they are not already). Then any ML code provided by the library is loaded. Then any help paths for the library are added to the system help path.

If failure occurs along the way, we clean up so that the theories and paths are as they were before the invocation of load_library.

If one knows that a) the library to be loaded supplies no theories, or b) has theories that are already parents of the current theory, or c) the session is currently in draft mode, then one may call

    load_library_in_place : lib -> unit
to load a library.

A current shortcoming of hol90 libraries is that any code loaded will be source, not object, so loading will be slower. As soon as SML/NJ's separate compilation facility settles down, this will be fixed. In the meantime, one solution would be for users to load commonly used libraries and then dump the image with save_hol.

Beginning of Libraries.
User Manual Table of Contents.

Declaring a library

Now we turn to how a library is made available for loading. Once the theory files of a library have been produced and the code made ready for loading (perhaps by separate compilation), and the help files written, the library implementor can declare the library. But first, the library must be in the right arrangement on disk. The library disk format is:
A library is a directory with subdirectories src, help, and theories (which itself must have subdirectories src and ascii (and possibly sun4, mipsb, ... if one uses binary theory format)).
When one wishes to make a library available for use, it is declared by a call to new_library.
    val new_library : {name : string,
                       doc : string,
                       path : string,
                       parents : lib list,
                       theories : string list,
                       code : string list,
                       help : string list,
                       loaded : string} -> lib
The name is the name of the library. It goes into making up a unique identifier which is used in many internal operations. The doc field gives a short description of the library. The path is the path to where the library can be found. The parents of a library are the libraries that it needs loaded before it can be used. These could have been represented by strings but representing them as values of type lib, besides being correct, allows easy computation of library properties.

The theories of a library are the HOL theories that it provides for one to use. This is a list of strings which are interpreted as relative paths from path, and to which the proper suffixes get added. For example, note the theories field in the following, which is the system declaration of the set library.

    val set_lib = Library.new_library
       {name = "set",
        doc = "The system library of sets, 
               due to Tom Melham and P. Leveilley",
        path = (!Globals.HOLdir)^"library/set/",
        parents = [num_lib],
        theories = ["set"],
        code = ["gspec.sig","gspec.sml",
        help = ["entries/"],
        loaded = "fn() => ()"};
When the library is loaded, (assuming an ASCII theory file regime) the theory files will be looked for in (path^"theories/ascii/set.holsig") and (path^"theories/ascii/set.thms").

The code of a library is the SML code that becomes available for one to use. It is loaded in left-to-right order, as, by the way, are the contents of the fields parents, theories, and help. The code is currently expected to be found at prefix (path^"src/"). In a separate compilation regime, this prefix will probably be different.

The help of a library represents the directories of its documentation files (written so as to be usable by the system function help). Each member of the help field is suffixed to (path^"help/"), and that is prepended to help_path. If the help list is empty, the directory (path^"help/") is prepended to help_path.

The loaded field of a library representation is a function that is called at the end of the loading of the library; it is intended to provide any functionality not catered to by the first part of the loading process. This ought to be an ML function of type unit -> unit, but currently this must instead be represented as a string that will compile into an ML function of type unit -> unit in the environment current at the time new_library is called.

When a library is declared, there are these side effects:

It is allowed that there be more than one known library with the same name: libraries are known internally by unique identifiers.

Beginning of Libraries.
User Manual Table of Contents.

Other library operations

The function dest_library will return many parts of the internal representation of a library.
   val dest_library : lib -> {name : string,
                              doc : string,
                              path : string,
                              parents : lib list,
                              theories : string list,
                              code : string list,
                              help : string list}
There is a function for pretty printing some bits of information about a library. This has been installed into the system prettyprinter table so that users can easily see some helpful identifying information about a library.
   val pp_library : System.PrettyPrint.ppstream -> lib -> unit
Here is a simple example of this "self-documentation":
    - Sys_lib.integer_lib;
    val it =
      library name: integer
      short description: The system library of integers, 
                         by Elsa Gunter
      parents: [group]
       : lib
It can happen that loading a library will cause documentation for a function in another library to become inaccessible. This will happen if two libraries both provide a function with the same name, and both are loaded. In that case, one should use lib_help, which provides library-specific help.
   val lib_help : {lib:lib, topic:string} -> unit

At times, the system needs to be informed that the disk location of a library has changed. The function for this is move_library, which updates the internal representation of a library to reflect the external change. It needs an absolute path name in its second argument.
    val move_library : lib * string  -> unit
We emphasize that move_library has nothing to do with the location of a .hol_lib file on disk. move_library only deals with the location of the group of files comprising the library. One would track the movement of a .hol_lib file by changing the library path, if necessary.
One can also delete a library. It will be removed from the list of known libraries if there are no other known libraries that have it as a parent. It is not allowed to delete a loaded library.
    val delete_library : lib -> unit
One can test libraries for equality with the function lib_eq.
    lib_eq : lib -> lib -> bool

Beginning of Libraries.
User Manual Table of Contents.

System libraries

The following lists the libraries that hol90 knows about when it starts up. A quick listing can be achieved by performing
    open Sys_lib;
in the hol90 top level.

Caution! The documentation for almost every library has been written for hol88 and has not yet been translated to hol90. As wretched as this situation is, perhaps it is better than the alternative, i.e., no documentation at all! Seriously, if you find it difficult to use a library because its documentation makes no sense in the context of hol90, please inform the author of this document, or the author of the library.

string_lib: ASCII character strings
reduce_lib: Normalize terms of type bool and num.
arith_lib: A linear-arithmetic decision procedure
set_lib: Polymorphic type of sets
pred_set_lib: Sets-as-predicates
unwind_lib: Support for unwinding hardware lines
taut_lib: Support for tautology proofs
ind_def_lib: Inductive definitions
utils_lib : General-purpose proof support
group_lib : Group theory
integer_lib : Integers
abs_theory_lib : Abstract theories
unity_lib : Chandy and Misra's UNITY formalism
pair_lib : Proof support for pairs
real_lib : The real numbers
wellorder_lib : Wellorderings and wellfounded recursion
window_lib : A window inference proof manager
list_lib : Extended support for lists
res_quan_lib : Support for restricted quantification
word_lib : Support for reasoning about bit vectors
prog_logic_lib : Programming logics
num_lib : Proof support for numbers
hol88_lib : Backwards compatibility for hol88
Derived rules and such. Preloaded.
Supplies numbers and pairs. Preloaded.
Arithmetic, lists, trees, and recursive types. Preloaded.

Beginning of Libraries.
User Manual Table of Contents.
Konrad Slind,