Via:  uk.ac.ucl.cs.nss; 1 Dec 88 19:19 GMT  (UK.AC.Cam.Cl.scaup)
Date: Thu, 1 Dec 88 17:04 GMT
From: Mike Gordon <mjcg%uk.co.sri@com.sri.ai.warbucks>
To: info-hol@edu.ucdavis.clover
Subject: HOL88
Message-Id: <mjcg.88.12.01.17:04.220@gwyndir>
Sender: mjcg <mjcg%uk.co.sri%com.sri.ai.warbucks@edu.ucdavis.clover>
Status: RO


                 |============================|
                 |                            |
                 |   HOL 88 PROGRESS REPORT   |
                 |   ----------------------   |
                 |                            |
                 |        Mike Gordon         |
                 |   Cambridge, 1 Dec 1988    |
                 |                            |
                 |============================|


On 28 October I sent a message to info-hol saying:

   The current plan is to finish implementing Version 1 HOL88
   in about two weeks, and to have a first draft of the new
   documentation ready at the end of November.

How accurate was this prediction?

Well, HOL88 Version 1 is still not quite finished, nor is the documentation.
However, we now have available HOL88 Version 0.9. This contains most of what
was planned for Version 1; the main things still to be done are:

   (i)   Support for ML style let-declarations in the logic
         (e.g. terms like "let f(x,y) = x+y in MAP f l").

   (ii)  Installation of various standard libraries (integers, n-bit words,
         sets and bags).

   (iii) Updating the help system and documentation.

   (iv)  Tuning the system (e.g. by adjusting various size parameters
         of Lisp). Version 0.9 seems to be a bit slow and NAMESTACK
         overflow happens suspiciously often.

In view of my poor record in making predictions, I will not predict when
Version 1 will be complete. However, working on HOL88 will be my main activity
until it is finished.

If anyone would like to experiment with Version 0.9, I would be happy to send
them a copy now. HOL users not running on SUNs might want to see if the new
system builds on their machine. If it does, then it is pretty likely that
Version 1 will build too.

Here is some news about the various HOL projects I briefly described at the
Users Meeting at the end of September.  Funds to support the HOL Tutorial and
Documentation project at SRI are almost in place. It is thus pretty likely
that there will be a professional quality manual and tutorial within the next
six months. The various other HOL based projects I described are all coming
along well. The EEC ESPRIT project (with IMEC and Philips) to interface HOL to
CATHEDRAL-II has been funded and should start next spring. The project (with
Praxis) to interface HOL to ELLA is looking promising, as is the project (with
INMOS and Oxford) to build a verified real-time application running via a
verified compiler on a verified processor. These last two projects are on the
short list for funding; whether or not they will be supported is unlikely to
be known for a month or two.

Finally, here is an improved version of the type checker error messages
that I sent earlier. This produces slighly different messages than before.
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

   #"FST SND";;
   Badly typed application of:  "FST"
      which has type:           ":?1 # ?2 -> ?1"
   to the argument term:        "SND"
      which has type:           ":?1 # ?2 -> ?2"

   evaluation failed     mk_comb in quotation

The ?1, ?2 etc indicate indeterminate types; i.e. types
that the type checker had not determined before the error
occurred. Note that type variables are not considered
to be indeterminate. For example:

   #"INL (x:*) INL";;
   Badly typed application of:  "INL x"
      which has type:           ":* + ?"
   to the argument term:        "INL"
      which has type:           ":?1 -> ?1 + ?2"

   evaluation failed     mk_comb in quotation

The system currently prints out a message whenever an attempt to
make a combination in a quotation fails, even if this failure is
trapped. For example:

   #let mk_comb_abs(t1,t2) = mk_comb(t1,t2) ? mk_abs(t1,t2);;
   mk_comb_abs = - : ((term # term) -> term)

   #mk_comb_abs("x:num","x+1");;
   "\x. x + 1" : term

   #let mk_comb_abs(t1,t2) = "^t1 ^t2" ? "\^t1.^t2";;
   mk_comb_abs = - : ((term # term) -> term)

   #mk_comb_abs("x:num","x+1");;
   Badly typed application of:  "x"
      which has type:           ":num"
   to the argument term:        "x + 1"
      which has type:           ":num"

   "\x. x + 1" : term

   #

The messages can be suppressed by turning off the error messages (with the ML
function show_type_errors). If this feature turns out to be a nuisance, I will
modify the code so that the error messages only get printed if the failure is
not trapped.

To load the Lisp file patch.l do:

   lisp`(load 'patch)`;;

in ML.

;========================= 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 "Error in Lisp function prep-term-for-print -- please report"))))

; MJCG 25/11/88 for HOL88
; Function for extracting %LINKs from a type
(defun get-links (ty)
 (selectq (type-class ty)
   ((%ANTIQUOT %VARTYPE) nil)
   (%LINK (if (numberp (cdr ty))
              (list (cdr ty))
              (get-links(cdr ty))))
   (t (apply (function append)
             (mapcar (function get-links) (get-type-args ty))))))

; MJCG 25/11/88 for HOL88
; Make a map from %LINK numbers to print names ?, ?1, ?2 ...
(defun make-link-names (l)
 (prog (ll link-names n)
       (cond ((null l)          (return (list nil)))
             ((eq (length l) 1) (return (list(cons (car l) '|?|)))))
       (setq n 1)
       (setq ll l)
       (setq link-names nil)
  loop (cond ((null ll) (return link-names))
             ((assoc (car ll) link-names))
             (t
              (setq link-names
              (cons (cons (car ll) (concat '|?| n)) link-names))
              (setq n (add1 n))))
       (setq ll (cdr ll))
       (go loop)))

; MJCG 13/11/88 for HOL88
; Function for making a partially typechecked type printable
; (remove antiquotations, %LINK, %VARTYPE etc)
; MJCG 25/11/88 for HOL88
; Code for ?, ?1, ?2, ?3 ... added

(defun prep-ty-fn (ty)
 (selectq (type-class ty)
   (%ANTIQUOT (cdr ty))
   (%VARTYPE ty)
   (%LINK (if (numberp (cdr ty))
              (make-vartype (cdr (assoc (cdr ty) %link-names)))
              (prep-ty-fn(cdr ty))))
   (t (make-type (get-type-op ty)
                 (mapcar (function prep-ty-fn)
                         (get-type-args ty))))))

(defun prep-ty-for-print (ty)
 (let ((%link-names (make-link-names(get-links ty))))
   (prep-ty-fn 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)
        (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)

; 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


; 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|))