Date: Tue, 17 Sep 91 11:16:43 MDT
From: slind@ca.ucalgary.cpsc (Konrad Slind)
Message-Id: <9109171716.AA03290@fsa.cpsc.ucalgary.ca>
To: info-hol@edu.uidaho.cs.ted

hol90 beta-release notes.


0. How to get it.

The beta-release of hol90 is available by ftp from the University of Calgary.
It currently only runs on the sun4. The userid is "hol90" and the password is
123456. The tar'ed and compress'ed file is hol90.tar.Z. An example session
would be

    ftp fsd.cpsc.ucalgary.ca
    <login as hol90 >
    get hol90.tar.Z
    <logout>

Once you have unpacked it, you have to set the theory path. This is done by
editing the variable "theory_path" in the file hol90/globals.sml. The prefix of
the path must be changed; the prefix is "/home/vlsi/hol90". Replace it with the
absolute path to where you put the hol90 directory.

The shell script make_hol will make the system. It takes about 35 minutes on
a 48 Meg. machine.

The directory has a version of NJSML that is needed to build the system. It has
a prettyprinter that is still a bit berserk on some SML values, but is legible.

If you have problems getting or building hol90, please let me know.


1. Structure of the system.

hol90 comprises a set of about 40 structures, all loaded into the image, plus a
collection of theories. All the structures are open, so the system should
appear to be the same as before, i.e., totally without form. If you wish to
browse around, or have to track down a bug, a quick reference to the structures
follows.

  Globals - global flags
  Exception - HOL_ERR defined
  Lib - utility routines
  String_utils - utility routines for strings
  Stk - ADT of stacks
  Type - HOL types
  Term - HOL terms
  Subst - subst
  Subst_occs - subst_occs
  Inst - inst
  Match - matching for types and terms
  Term_ops - derived syntax for terms
  Parse - parsing of types and terms
  Thm - "ADT" of theorems
  Goal_stack - the goal stack
  Theory - theory operations
  Const_spec - principle of constant specification
  Type_def - principle of type definition
  Mk_exists - defining ?
  Const_def - principle of constant definition
  Mk_bool - basic logical constants defined
  Drule1, Drule2, Drule3, Drule4 - derived rules of inference and theorems
  Conv - conversions
  Tactical - tacticals
  Net - discrimination nets for terms
  Rewrite - rewriting functions
  Thm_cont - theorem continuations
  Tactic - tactics
  Taut - some tautologies
  Inductive_def - Tom Melham's inductive definitions pkg
  Resolve - HOL-style resolution rules of inference
  Type_def_support - helps prove useful thms from a type definition
  Induct_then - generalized induction tactic
  Prim_rec - generalized primitive recursive definition
  Num_conv - num_CONV
  Let_conv - let_CONV and PAIRED_BETA_CONV
  Rec_type_support - helps prove useful thms from a "define_type" definition
  Define_type - derived principle of definition for concrete recursive types
  Add_to_sml - a form of autoloading
  Compat - structure for compatibility with hol88

Every bound identifier that is not in the pervasive environment of NJSML should
be in one of the above structures.


2. Quotations.

A major difference in the "feel" of the interface is the syntax of quotations.
In NJSML, a quotation is delimited by quote marks, for example

    `A /\ B`

In NJSML, quotations are a more general notion than in hol88. There can be
quotations from many different object languages in the same NJSML session. A
consequence of this is that quotations must be parsed explicitly, instead of
implicitly, as in hol88. There is a term parser and a type parser provided with
hol90 as shown in the signature for the structure Parse:

    signature Parse_sig =
    sig
      structure Term : Public_term_sig
      val term_parser : Term.term frag list -> Term.term
      val type_parser : Term.term frag list -> Term.Type.hol_type
      val -- : Term.term frag list -> 'a -> Term.term
      val == : Term.term frag list -> 'a -> Term.Type.hol_type
    end;

For example, the above quotation could be parsed as:

    term_parser `A /\ B`

or, since the function "--" is a bit of syntactic sugaring for term_parser
(suggested to me by Richard Boulton of Cambridge University), as

    --`A /\ B`--

Similarly, types would be parsed as

    type_parser `:(bool -> 'a) -> ('a # 'b) list`

or

    ==`:(bool -> 'a) -> ('a # 'b) list`==


For terms, antiquotes are much the same as in hol88. So

    val tm = --`A /\ B`--;
    val tm' = --`C /\ ^tm`--;

gives the same result as parsing

    val tm' = --`C /\ A /\ B`--

For types, it is necessary to use a somewhat more devious approach: if you are
going to use a type as an antiquotation, you must wrap the constructor
"ty_antiq" around it:

    val ty = ty_antiq(==`:('a -> 'b) -> 'a list -> 'b list`==)
    val tm = --`(MAP:^ty) f`--;


3. Changes to the concrete syntax.

First, type variables are now like SML type variables:

    :* -> **

from hol88 would be

    :'a -> 'b

in hol90. This change was forced by the lexical structure of SML: comments and
star-style type variables don't "commute". Say I wanted to specify, inside a
quotation, the type of MAP for a theory of lists in the logic:

    MAP:(* -> **) -> * list -> ** list

The SML compiler would interpret the "(* -> **)" fragment from the type as a
comment, and the quotation would mysteriously fail to typecheck.

Second, the lexical structure for constants has been revamped to be much like
that for SML: constants can be alphanumeric or symbolic, which is already the
case for hol88. The difference is that a symbolic identifier is any
concatenation of the characters in the following list

    explode "#$?+*/\\=<>&%@!,:;_|-";

with the exception of the keywords

    ["\\", ";", "=>", "|", ":" ]

and with the added exception that the first character not be "$". Any
alphanumeric can be a constant except the keywords

    ["let", "in", "and"].

There are also two infinite families of constants: numbers and strings (if you
have loaded the string library). Numbers are exactly the same, while strings
will be the same as SML strings.


4. Exceptions.

With the "structuring" of hol90, it becomes more feasible to have HOL be a
subcomponent of a larger system. This raises the question: what is the
interface to HOL? Towards answering this, the multitude of exceptions that
hol90 can raise have been shepherded into one:

    exception HOL_ERR of string*string*string;

The three string fields are, in order: the name of the structure that the
raising routine inhabits; the name of the raising routine; and the message. Any
exception that propagates to the top level should either be HOL_ERR or defined
in the NJSML pervasive environment. (This is a goal not wholly attained:
parsing errors still propagate to the top level.)

Unfortunately, NJSML does not automatically print the values of exceptions that
propagate to the top level. To help in this, the structure Exception (where
HOL_ERR is defined) provides the routines

    print_HOL_ERR: exn -> unit
    Raise : exn -> 'a

The first prints out HOL_ERR in a fashion prescribed by the (assignable)
function Globals.output_HOL_ERR. The second does the same (provided
Globals.print_exceptions is set to true), but also raises the exception again.
This feature is handy for debugging derived rules of inference and also for
reporting HOL_ERR, since it saves on finding a value of the proper type to
return:

    el 3 ["foo","bar"] handle e => (print_HOL_ERR e; "blag");
    el 3 ["foo","bar"] handle e => Raise e;


5. Theories.

The theory hierarchy is nearly the same as that of hol88, except that the
theory of pairs is now distinct from the theory "bool". Theories are held on
disk in binary format. They are architecture specific: a theory built on a sun4
will not be usable on a sun3. They are probably an order of magnitude larger
than the corresponding hol88 theory files. It is planned that there be some
method for translating theory files between architectures.


6. export_theory versus quit.

In hol88, the call "quit();;" is used to end a session. It has the side-effect
of writing the current theory to disk. In hol90, "quit" is not available;
instead, "export_theory" will write the current theory to disk. Until it is
called, the disk file will not be written. Ending the session is via ^D. If
you are building a theory and hit ^D before calling "export_theory", nothing
will be saved on the theory file.


7. Autoloading.

In hol90 autoloading is not available. The replacement for it is found
in the structure Add_to_sml.

    val add_to_sml : (string * thm) list -> unit
    val add_axioms_to_sml : string -> unit
    val add_definitions_to_sml : string -> unit
    val add_theorems_to_sml : string -> unit
    val add_theory_to_sml : string -> unit

These calls map theory-level bindings which are of type :string * thm to
SML-level bindings. Their argument string must be an ancestor of the current
theory. For example,

    - Add_to_sml.add_definitions_to_sml "one";
    [opening <instream>]
    val one_DEF = |- one = (@x. T) : thm
    [closing <instream>]

    [opening <instream>]
    val oneTY_DEF = |- ?rep. TYPE_DEFINITION (\b. b) rep : thm
    [closing <instream>]
    val it = () : unit
    -


8. Non-confluence in rewriting.

In both hol88 and hol90, the rewriting process will occasionally encounter a
term to which more than one rewrite will be applicable. The first match will be
the one used to rewrite the term. It can happen (rarely) that hol90 will choose
a different first match than hol88, and that the result will be different. This
is an example of non-confluence. Some proofs may not port as a result.


9. Compatibility.

In the course of writing hol90, I used a different set of library routines and
some different conventions (the main one being that the free variables of a
term are a set, i.e., their order makes no difference), with the result that
some common routines behave a bit differently than in hol88. The structure
Compat is supposed to provide hol88-compatibility. I expect that it will grow
as the differences between the two implementations become known.


10. Libraries.

There are no libraries available as yet. Several have been ported to hol90, but
I haven't yet gotten around to giving them a coherent organization.


11. Paths.

There is a theory path, but that is the only useful path available in the
system at the moment.


12. Precedence.

Infixes in hol90 now have precedence. To give constant c1 a higher precedence
than constant c2, give it a higher number. The current precedences are

          $,  ---> 50
          $=  ---> 100
        $==>  ---> 200
         $\/  ---> 300
         $/\  ---> 400
      $>, $<  ---> 450
    $>=, $<=  ---> 450
      $+, $-  ---> 500
    $*, $DIV  ---> 600
        $MOD  ---> 650
        $EXP  ---> 700

Routines that now take an extra argument for precedence are:

    Theory.new_infix : (string * hol_type * int) -> unit
    Const_spec.new_specification : string ->
                                     (string*string*int) list -> thm -> thm
    Const_def.new_infix_definition : (string * term * int) -> thm
    Prim_rec.new_recursive_definition : (bool*int) ->
                                            thm -> string -> term -> thm

The HOL prettyprinter also uses precedence to eliminate as many brackets as
possible. Sometimes this can result in ambiguous-looking terms being displayed.


13. Flags.

All assignable variables in the system (except for Rewrite.basic_rewrites) are
held in the structure Globals. Most of them are directly assignable, for
example

    show_types := true;

This is another structure that will grow as the hol90 implementation matures.


14. Converting between the two languages.

SML has a Core Language subset that is quite close to ML. A comparative reading
of the hol88 and hol90 sources will go a long way towards making one "Core
SML-fluent". Adjusting to the Modules system is a more daunting task, but very
rewarding! I recommend the SML Definition and the Commentary for those who wish
to be seriously well-informed about the language. Larry Paulson has a good
textbook out on SML as well.


15. Inductive definitions.

Tom Melham's new inductive definitions package has been ported to hol90, but
you will have to send mail to him in order to obtain the source for it, since
he is working on some improvements to it.


16. Examples.

The multiplier benchmark resides in the "bmark" sub-directory of hol90. The shell
script "run_bmark" will run the thing for you. You will have to load the file
"unwind.sml" and dump it to the file "h91" beforehand, though. Instructions are
in "run_bmark".

Some Knuth-Bendix benchmarks reside in the "kb" sub-directory. Load the file
"kb_sys.sml", then run any of the functions test1, test3, test4, test5a,
test5b, test6, test12, test16, test17.


17. Help.

Other than this document, no help functions exist in hol90. The documentation
from the hol88 release should, in general, be applicable.


18. Other stuff.

There are some other more-or-less glaring omissions. In the "more" part, we
have absolutely non-informative errors when type inference fails. In the "less"
part, we have not implemented type abbreviations, interface maps, or constant
hiding.


Finally, I would like to thank Jim Grundy and John Van Tassel of Cambridge
University for porting some libraries, and Kevin Mitchell of Edinburgh
University for finding many bugs and inconsistencies.


Konrad Slind.