Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Fri, 15 Jan 1993 19:24:18 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA01618;
          Fri, 15 Jan 93 09:07:16 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA01613;
          Fri, 15 Jan 93 09:07:07 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA22278;
          Fri, 15 Jan 93 09:05:44 -0800
Message-Id: <9301151705.AA22278@maui.cs.ucla.edu>
To: John Harrison <John.Harrison@uk.ac.cam.cl>
Subject: Re: autoload
Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Date: Fri, 15 Jan 93 09:05:39 PST
From: chou@edu.ucla.cs

Thanks for your comments, John!

> However the code which implements actual autoloading (as used by
> |autoload_theory|) has a side-effect of removing the token just acted 

> on from the autoload list (which is a natural optimization). 


I think I did include |undo_autoload| as part of the autoload action.
The relevant codes are listed below:

let autoload_term_prefix = `autoload_term_`
and autoload_type_prefix = `autoload_type_`
;;

let term_msg_lfn [thy; name] =
  ( if (get_flag_value `print_load`) then
    ( print_string (`Term `^name^` autoloaded from theory \``^thy^`\`.`) ;
      print_newline () ) ) ;
  undo_autoload name ;
  (lhs o snd o strip_forall o concl)
    (theorem thy (autoload_term_prefix^name))
;;

let autoload_term [thy; name] =
  let_before (name, `term_msg_lfn`, [thy; name])
;;

let type_msg_lfn [thy; name] =
  ( if (get_flag_value `print_load`) then
    ( print_string (`Type `^name^` autoloaded from theory \``^thy^`\`.`) ;
      print_newline () ) ) ;
  undo_autoload name ;
  (type_of o lhs o snd o strip_forall o concl)
    (theorem thy (autoload_type_prefix^name))
;;

let autoload_type [thy; name] =
  let_before (name, `type_msg_lfn`, [thy; name])
;;

let gen_autoload_theory (kind, thy, name) =
  if (mem kind [`axiom`; `definition`; `theorem`]) then
    autoload_theory (kind, thy, name)
  if (kind = `term`) then
    autoload (name, `autoload_term`, [thy; name])
  if (kind = `type`) then
    autoload (name, `autoload_type`, [thy; name])
  else
    failwith (`gen_autoload_theory: unknown kind: `^kind)
;;


- Ching Tsun