Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9301291959.AA13478@draco.cs.pdx.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Re: Printing of assumptions
In-Reply-To: Your message of Thu, 28 Jan 93 23:35:11 -0800. <9301290735.AA14949@maui.cs.ucla.edu>
Date: Fri, 29 Jan 93 11:59:26 PST
From: schubert@edu.pdx.cs


Ching writes:
> With the subgoal package, is it possible to limit the printing of
> assumptions of a goal?  I often have goals which have more than 40

Yes, I've had this "problem" too (particularly over a 2400B line).  I made
some quick modifications to goals.ml and stack.ml to allow for selective
printing of the assumption list.  It's been a while since this code was
developed, but I believe that Jim Alves-Foss has since made some improvements
to this scheme.

With a minor amount of tinkering, you could adapt these changes so that only
new theorems to the assumption list are printed.  I haven't had time to insert
these changes into the new editions of goals.ml and stack.ml, so let me just
explain them.

BTW: You need not rebuild HOL, just load these two files as part of hol-init.ml

The changes add a few flags to goals.ml, an assignable variable, and
replacing the function print_hyps and print_goal.

     new flags	            if true
   print_asl_cnt 	enumerate the assumption list
   print_asl_list	print a subset of assumption list (see below)
   print_asl		print the assumption list
   print_gl		print the goal

By setting the new variable asl_print_list, only the specified subset will be
printed.  For example:

    set_flag(`print_asl_list`,true);;

    asl_print_list := [3;2;1];;

will cause only the last three assumptions to be printed.  To take advantage
of these changes, I also added a few functions to stack.ml (see below)

-Tom

-------- add to stack.ml --------
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);;


------- add/replace in goals.ml ------------

new_flag(`print_asl_cnt`,true);;
new_flag(`print_asl_list`,false);;
new_flag(`print_asl`, true);;
new_flag(`print_gl`, true);;

letref asl_print_list = []:int list;;

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


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