Via:  uk.ac.ucl.cs.nss; 13 Nov 88 23:08 GMT  (UK.AC.Cam.Cl.scaup)
Date: Sun, 13 Nov 88 22:51 GMT
From: Mike Gordon <mjcg%uk.co.sri@com.sri.ai.warbucks>
To: info-hol@edu.ucdavis.clover
Subject: HOL88
Message-Id: <mjcg.88.11.13.22:51.900@gwyndir>
Sender: mjcg <mjcg%uk.co.sri%com.sri.ai.warbucks@edu.ucdavis.clover>
Status: R


                 |============================|
                 |                            |
                 |   HOL88 PROGRESS REPORT    |
                 |   ----------------------   |
                 |                            |
                 |        Mike Gordon         |
                 |   Cambridge, 13 Nov 1988   |
                 |                            |
                 |============================|


At the end of this note I give a Lisp patch that will improve the error
messages from the HOL typechecker.  The code for this is a bit tricky, and may
contain bugs that crash HOL -- I would thus appreciate any testing you could
do.

First, here are some details of new features that will be in Version-1
HOL88.


Some Unix commands from ML
--------------------------

Files changed: lisp/hol-pars.l

   unix : string -> int

      Executes the string argument in a separate process. The number returned
      by the process is returned by the function unix. For example, if foo14
      exists on the current directory, then:

         #unix `rm foo14`;;
         0 : int

         #unix `rm foo14`;;
         rm: foo14: No such file or directory
         1 : int


   host_name : void -> string

     Returns the name of the host machine.


   link : string # string -> void

     link(`old`,`new`) links the file `old` to `new`; failure
     if `old` does not exist.


   unlink : string -> void

     Unlinks a file; failure if the file doesn't exist.


Input and output from ML
------------------------

Files changed: lisp/hol-pars.l


   openi : string -> string

     openi`file` returns a string that can be used by read
     to read characters from the file `file`; failure if the
     file doesn't exist.


   openw : string -> string

     openw`file` returns a string that can be used by write
     to write characters to the file `file`. If `file` exists
     it is overwritten.


   append_openw : string -> string

     append_openw`file` returns a string that can be used by write
     to write characters to the end of the file `file`.


   read : string -> string

     Reads a character from a port which has been produced with openi.


   write : string # string -> void

     write(`port`,`chars`) writes `chars` to port `port` (which have been
     produced by openw or append_openw).

   close : string -> void

     Closes a port.


   tty_read : void -> string

     Reads a character from the terminal.


   tty_write : string -> void

     Writes a character to the terminal.


Hiding constants
----------------

Files changed: lisp/hol-pars.l
               lisp/constp.l
               theories/mk_num.ml

The function:

   hide_constant : string -> void

makes the parser treat its argument as a variable (lexical rules
permitting). This is useful if one wants to use as variables
names that have been declared as built-in constants
(eg "o", "I", "S" etc). The name is still a constant for the
constructors, theory package etc; hide_constant only effects parsing.

Note that hiding a constant and then attempting to declare it as a
new constant will fail (as it has to if the system is to remain sound).

The function:

   unhide_constant : string -> void

undoes the hiding; it fails if its argument is not a previously
hidden constant.


Changes to sticky types
-----------------------

Files changed: lisp/F-typeol.l
               ml/tyfns.ml ("b" explicitly typed)


The sticky type feature has been made optional in HOL88.  Normally it is
switched off, but it can be reinstated with the function:

   sticky_types : bool -> bool

Applying this to true causes sticky types to be automatically set up as in old
HOL; applying it to false switches of the automatic setting of sticky types by
the HOL typechecker.  Variables can be explicitly given sticky types with the
function:

   set_sticky_type : string # type -> void

The sets sticky types whether or not the system is in automatic stickytype
mode.  Sticky types can be removed with:

   remove_sticky_type : string -> type

The sticky type is returned (failure if the variable does not
have a sticky type). A function to return the sticky type of a variable
can be defined by:

   let sticky_type v =
    let ty = remove_sticky_type v
    in
    (set_sticky_type(v,ty);ty)

The list of sticky types active in a session is given by the function:

   sticky_list : void -> (string # type) list


Better error messages from the typechecker
------------------------------------------

Files changed: lisp/F-ol-syntax.l


The HOL typechecker has been modified to produce better error messages.
For example:


   #"SUC T";;
   Badly typed application of:  "SUC"
   which has type:              ":num -> num"

   to the argument term:  "T"
   which has type:        ":bool"

   evaluation failed     mk_comb in quotation

   #"x /\ (x=1)";;
   Badly typed application of:  "$= x"
   which has type:              ":bool -> bool"

   to the argument term:  "1"
   which has type:        ":num"

   evaluation failed     mk_comb in quotation

These verbose messages can be switched off using the ML function:

   show_type_errors : bool -> bool

Applying show_type_errors to false switches the messages off; applying
it to true switches them on. The truthvalue returned gives the previous
status (true = messages being printed).

I plan to experiment with eliminating the need  for the message:

   evaluation failed     types indeterminate in quotation

by inferring most general types in the logic (as the ML typechecker does).


-----------------------------------------------------------------------------

The Lisp file that follows implements the changes to the typechecker messages
described above. To try it out do the following:

   1. Create a file called patch.l containg the Lisp code below.

   2. Run HOL on the directory where you have put patch.l

   3. In ML execute:

         lisp`(load 'patch)`;;

Please let me know about all the bugs you find!


;========================= patch.l =========================


; Some system macros
(defmacro dml (ml-fn n lisp-fn mty)
  `(declare-ml-fun (quote ,ml-fn) (quote ,n) (quote ,lisp-fn) (quote ,mty)))

(defmacro new-exit (name . body)
  `(throw (progn ,@body) ,name))

(defmacro make-var (name ty) `(cons 'var (cons ,name ,ty)))
(defmacro is-var (tm) `(eq(car ,tm)'var))
(defmacro get-var-name (tm) `(cadr ,tm))

(defmacro make-const (name ty) `(cons 'const (cons ,name ,ty)))
(defmacro is-const (tm) `(eq(car ,tm)'const))
(defmacro get-const-name (tm) `(cadr ,tm))

(defmacro make-abs (var body ty) `(cons 'abs (cons (cons ,var ,body) ,ty)))
(defmacro is-abs (tm) `(eq (car ,tm) 'abs))
(defmacro get-abs-var (tm) `(caadr ,tm))
(defmacro get-abs-body (tm) `(cdadr ,tm))

(defmacro make-comb
 (rator rand ty) `(cons 'comb (cons (cons ,rator ,rand) ,ty)))
(defmacro is-comb (tm) `(eq (car ,tm) 'comb))
(defmacro get-rator (tm) `(caadr ,tm))
(defmacro get-rand (tm) `(cdadr ,tm))

(defmacro get-type (tm) `(cddr ,tm))
(defmacro put-type (tm ty) `(rplacd (cdr ,tm) ,ty)) ; used in F-thyfns

(defmacro term-class (tm) `(car ,tm))

; types

(defmacro make-type (tyop tyargs) `(cons ,tyop ,tyargs))
(defmacro get-type-op (ty) `(car ,ty))
(defmacro get-type-args (ty) `(cdr ,ty))

(defmacro make-vartype (name) `(cons '%VARTYPE ,name))
(defmacro is-vartype (ty) `(eq (car ,ty) '%VARTYPE))

(defmacro type-class (ty) `(car ,ty))

(defmacro ptoken (str)
  `(pstringlen (quote ,str) ,(flatc str)))

(defmacro failwith (tok)
  `(new-exit evaluation ,tok))


; MJCG 13/11/88 for HOL88
; Function for making a partially evaluated term printable
; (remove antiquotations etc)
(defun prep-term-for-print (tm)
 (selectq (term-class tm)
   (var tm)
   (const tm)
   (comb (make-comb (prep-term-for-print(get-rator tm))
                    (prep-term-for-print(get-rand tm))
                    (get-type tm)))
   (abs (make-abs (get-abs-var tm)
                  (prep-term-for-print(get-abs-body tm))
                  (get-type tm)))
   (%ANTIQUOT (prep-term-for-print(cdr tm)))
   (t  (failwith "Error1 in HOL88 typechecker -- please report"))))

; MJCG 13/11/88 for HOL88
; Function for making a partially typechecked type printable
; (remove antiquotations, %LINK, %VARTYPE etc)
(defun prep-ty-for-print (ty)
 (selectq (type-class ty)
   (%ANTIQUOT (cdr ty))
   (%VARTYPE ty)
   (%LINK (prep-ty-for-print(cdr ty)))
   (t (make-type (get-type-op ty)
                 (mapcar (function prep-ty-for-print) (get-type-args ty))))))

; MJCG 13/11/88 for HOL88
; Get type (stripping off %ANTIQUOT if necessary)
(defun prep-term-ty (tm)
 (if (eq (car tm) '%ANTIQUOT) (get-type(cdr tm)) (get-type tm)))

; MJCG 13/11/88 for HOL88
; Function for printing error messages
(defun print-type-error (tm1 tm2)
 (progn (ptoken "Badly typed application of:")
        (pbreak 2 4)
        (ml-print_term(prep-term-for-print tm1))
        (pnewline)
        (ptoken "which has type:            ")
        (pbreak 2 4)
        (ml-print_type(prep-ty-for-print(prep-term-ty tm1)))
        (pnewline)
        (pnewline)
        (ptoken "to the argument term:")
        (pbreak 2 4)
        (ml-print_term(prep-term-for-print tm2))
        (pnewline)
        (ptoken "which has type:      ")
        (pbreak 2 4)
        (ml-print_type(prep-ty-for-print(prep-term-ty tm2)))
        (pnewline)
        (pnewline)))

; MJCG 13/11/88 for HOL88
; Flag to control printing of type errors
(setq %type-error-flag t)
(defun ml-show_type_errors (x)
 (prog1 %type-error-flag (setq %type-error-flag x)))
(dml |show_type_errors| 1 ml-show_type_errors (|bool| -> |bool|))

; MJCG 10/11/88 for HOL88
; add error message printing
; combinations

(defun q-mk_comb (tm1 tm2)
  (let ((ty (genlink)))
       (if (unify (q-typeof tm1) (make-type '|fun| (list (q-typeof tm2) ty)))
           (make-comb tm1 tm2 ty)
           (prog2 (if %type-error-flag (print-type-error tm1 tm2))
                  (failwith '|mk_comb|)))))  ;q-mk_comb