Warning: the hol90 implementation of libraries is quite different from that of hol88!
Beginning of Libraries.
User Manual Table of Contents.
val load_library: {lib :lib, theory :string} -> unitThere 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.)
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 -> unitto 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.
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} -> libThe 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", "set_ind.sig","set_ind.sml", "fset_conv.sig","fset_conv.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:
load_theory "string"immediately on startup of hol90.
Beginning of Libraries.
User Manual Table of Contents.
val dest_library : lib -> {name : string, doc : string, path : string, parents : lib list, theories : string list, code : string list, help : string list}
val pp_library : System.PrettyPrint.ppstream -> lib -> unitHere 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
val lib_help : {lib:lib, topic:string} -> unit
val move_library : lib * string -> unitWe 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.
val delete_library : lib -> unit
lib_eq : lib -> lib -> bool
Beginning of Libraries.
User Manual Table of Contents.
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.