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); Thu, 14 Jan 1993 11:01:10 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28481;
          Thu, 14 Jan 93 02:45:28 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28476;
          Thu, 14 Jan 93 02:45:08 -0800
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Thu, 14 Jan 1993 10:44:15 +0000
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list)
Subject: Re: autoload
In-Reply-To: Your message of Wed, 13 Jan 93 13:26:23 -0800. <9301132126.AA25695@maui.cs.ucla.edu>
Date: Thu, 14 Jan 93 10:44:09 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.522:14.01.93.10.44.17"@cl.cam.ac.uk>


Ching Tsun asks:

> If I set up autoloading action for a string `abc` using the
> ML function autoload(`abc`, ...) and then type, say,
> 
> # abc, abc ;;
> 
> it seems that the ML parser will execute the autoloading action
> twice, once per occurrence of abc.  On the other hand, if I set
> up autoloading action using autoload_theory, it seems that the
> autoloading action will be executed only once no matter how many
> times abc occurs.  Why is this so?

I think the story is as follows.

Any autoload action is performed each time a token on the autoload
list is encountered. By using |autoload| you can set up actions more
general than just autoloading.

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

You can see the effect in action because |undo_autoload| returns
a flag saying if there was an action associated with that token. Note
how an autoload cancels it:

> /homes/jrh/hol$ hol
>
>
> =============================================================================
>          HOL88 Version 2.01 (SUN4/AKCL), built on 4/12/92
> =============================================================================
>
> #undo_autoload `ADD_SYM`;;
> true : bool
>
> #ADD_SYM;;
>
> unbound or non-assignable variable ADD_SYM
> 1 error in typing
> typecheck failed
>
> #quit();;
> Bye.
> /homes/jrh/hol$ hol
>
>
> =============================================================================
>          HOL88 Version 2.01 (SUN4/AKCL), built on 4/12/92
> =============================================================================
>
> #ADD_SYM;;
> Theorem ADD_SYM autoloading from theory `arithmetic` ...
> ADD_SYM = |- !m n. m + n = n + m
>
> |- !m n. m + n = n + m
>
> #undo_autoload `ADD_SYM`;;
> false : bool
>
> #quit();;
> Bye.

John.