Message-Id: <9108162248.AA03866@iris.eecs.ucdavis.edu>
To: info-hol@edu.ucdavis.eecs.iris
Subject: user interface changes to HOL
Date: Fri, 16 Aug 91 15:48:02 PDT
From: schubert@edu.ucdavis.eecs.iris


During a recent proof effort, I became frustrated by the amount of time
required to print the new state after each step of an interactive proof.
Further, the volume of output produced was far greater than what I wanted
to see.  This problem was exacerbated by my wish to work over a 2400B
connection.

Setting max_print_depth to something small (like 9) was helpful, but with
the help of Jim Foss, I've made some (quick and dirty?) changes to goals.ml
and stack.ml that others might find beneficial.

Printing only the goal or assumption list:
    Frequently I only want the goal or assumption list to be printed.  Two new
    flags "print_gl" and "print_asl" control whether these are printed.  I've
    added a few commands to supplement the expand "e" command.  Using the
    commands "ea" or "eg" in place of "e", sets the appropriate flag to false.
    The new command "eu" resets both flags to true.

Printing a subset of the assumption list:
    Assumption lists can grow rather large and frequently, I'm only
    interested in viewing a subset of the assumption list -perhaps
    only the last one.  I added a new assignable variable "asl_print_list"
    and flag "print_asl_list" (feel free to change the names ;-) ).
    The following commands will cause only the last three assumptions to
    print out.

        set_flag(`print_asl_list`,true);;
        asl_print_list := [3;2;1];;

    To get more than you initially asked for, reset the variable (or flags)
    and submit the command "p 1;;"

Printing assumption list numbers:
    Though it's bad practice to frequently use (el ? asl), often its the
    quickest and easiest way to accomplish some purpose.  Setting the
    flag "print_asl_cnt" to true causes the assumption number to be printed
    to the left of the assumption.


Rather than change the system's version of goals.ml and stack.ml, I load
modified versions of these files after starting HOL.  This requires that
the declaration of the "old" flag "print_all_subgoals" is removed.

        loadf `goals.ml`;;
        loadf `stack.ml`;;


-Tom

(NOTE: The modifications were made for use with HOL 1.11.  I assume they'll
work with 1.12)

%------------ changes to goals.ml ------------- %

% these changes need to be made at the beginning of the file %


new_flag(`print_gl`,      true);;      % print goal %
new_flag(`print_asl`,     true);;      % print assumption list %
new_flag(`print_asl_cnt`, true);;      % print assumption list numbers %
new_flag(`print_asl_list`,false);;     % print (partial) list of assumptions %

letref asl_print_list = [3;2;1]:int list;;  % the partial list of assumptions %

% Print assumptions -- in reverse order so new assumptions appear last %
let print_hyps asl =
    letrec my_map fn cnt asl =
      (if not(null asl) then
        (fn cnt (hd asl);my_map fn (cnt-1) (tl asl))) in
    let print cnt as =
        ((if get_flag_value(`print_asl_cnt`) then
          ((if cnt < 10 then print_string ` `);
            print_int cnt)
         else print_string`   `);
         print_string ` [ `; print_term (as); print_string ` ]`;
         print_newline()) in
    letrec list_print plist asl =
      (if not(null asl) then
        (if not(null plist) then
         let thm_num =  (hd plist) in
         ((print thm_num (el thm_num asl) ); list_print (tl plist) asl)
        ))
    in
   (if get_flag_value(`print_asl_list`) then
       list_print asl_print_list asl
    else
       do (my_map print (length asl) (rev asl)) );;

%
 Already defined as a flag by system's goals.ml:
        new_flag(`print_all_subgoals`, true);;
%

let print_goal (asl,w) =
  let cnt = length asl in
  (if get_flag_value(`print_gl`) then print_term w
                                else print_string `..goal..`;
  print_newline();
  if get_flag_value(`print_asl`) then print_hyps asl
  else (print_string `..assumption list.. (`; print_int cnt ;
        print_string `) assumptions`);
  print_newline());;


%-----------------  additions to stack.ml ---------------------%

% add at the end of the file %

let ea tac = let x = set_flag(`print_asl`,false) in (x ; expand tac);;

let eg tac = let x = set_flag(`print_gl`,false) in (x ; expand tac);;

let eu tac = let x = set_flag(`print_asl`,true) in
             let y = set_flag(`print_gl`,true) in (x ; y ; expand tac);;