Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
To: info-hol@edu.uidaho.cs.ted
Subject: Printing assumptions containing type info
Date: Sat, 02 Nov 91 12:37:35 +0000
From: Richard.Boulton@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.139:02.10.91.12.37.41"@cl.cam.ac.uk>

Jim Alves-Foss (jimaf@ted.cs.uidaho.edu) writes:
> The problems I have come across in using ASSUME or LET arise in the type
> arena. When proving lemmas about polymorphic types (which I do all the time)
> it is much more difficult to use ASSUME than a number of an assumption.
>
> If I could cut and paste the textual output of HOL and put it into an
> ASSUME or LET without having to edit in all the type definitions, I would
> be very happy, and things would be much easier -- although the proof code
> would be longer.

In principle, setting the HOL system flag `show_types` to true should allow
an assumption to be printed with type information.

Consider the following session:

#g "!(x:*) y. (x = y) ==> (y = x)";;
"!x y. (x = y) ==> (y = x)"

() : void

#expand (REPEAT STRIP_TAC);;
OK..
"y = x"
    [ "x = y" ]

() : void

#print_term (el 1 (fst (top_goal ())));;
"x = y"() : void

#show_types true;;
false : bool

#print_term (el 1 (fst (top_goal ())));;
"x = y"() : void

#"x = y";;
Indeterminate types:  "$=:?1 -> (?2 -> bool)"

evaluation failed     types indeterminate in quotation

#

Unfortunately, as can be seen from the above, even with `show_types` set to
true, HOL does not include sufficient type information for the terms to be
cut-and-pasted.

The following solution seems to be overkill, but given the inadequacy of the
standard HOL pretty-printer, it may be the only one available (?).

First, load the pretty-printer library:

#load_library `prettyp`;;
Loading library `prettyp` ...
Updating help search path
...............................................................................
...............................................................................
...............................................................................
.......................................................
Library `prettyp` loaded.
() : void

The pretty-printers in this library are much slower than the standard ones, so
it is a good idea to restore the standard pretty-printers for normal use:

#top_print print_type;;
- : (type -> void)

#top_print print_term;;
- : (term -> void)

#top_print print_thm;;
- : (thm -> void)

#assignable_print_term := print_term;;
- : (term -> void)

Now we can use the new pretty-printer to print assumptions, and cut-and-paste
works:

#pp_print_term (el 1 (fst (top_goal ())));;
"x:* = y:*"() : void

#"x:* = y:*";;
"x = y" : term

Of course, having `show_types` set to true can be a nuisance, but the
following function will print an assumption with type information regardless
of the state of `show_types`:

#let print_assum n =
   let old_flag = set_flag (`show_types`,true)
   and assum = el n (fst (top_goal ()))
   in  do (pp_print_term assum;
           print_newline ();
           set_flag (`show_types`,old_flag));;
#####print_assum = - : (int -> void)

#print_assum 1;;
"x:* = y:*"
() : void

I think the pretty-printer in the prettyp library will always provide enough
type information to satisfy the HOL parser/type-checker, but if anyone finds
an example where it does n't, I can provide code that will print a term with
ALL type information included.


One further comment relating to the more general discussion that provoked this
message:

A mouse-window interface to HOL could be set up so that users can click on
the assumptions they wish to use. This could yield the number of the assumption,
but it could instead *automatically* include the full text of the assumption
in the log file. I am thinking here that the interface would produce a log
file of the session that could be replayed through HOL without the interface
being present.


Richard Boulton (rjb@cl.cam.ac.uk)