Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <19606.9302081246@frogland.inmos.co.uk>
Subject: Re: Theory loading
To: Wai.Wong@uk.ac.cam.cl (Wai Wong)
Date: Mon, 8 Feb 1993 12:46:11 +0000 (GMT)
Cc: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
In-Reply-To: <"swan.cl.ca.372:08.02.93.12.38.43"@cl.cam.ac.uk> from "Wai Wong" at Feb 8, 93 12:37:53 pm
Content-Type: text
Content-Length: 2129

Wai Wong has said:
> The problem of recursively up the theory tree activating binders
> has NOT been fixed yet!!! This is still part of the reasons why loading
> theories take so long.
> 
> Unlike infix, which is stored in the theory data part of a
> theory, binders are stored in the theorem part. This means if you
> want to find out whether there are any binders in a theory, you need
> to load the whole theorem part. This takes most of the time. Once a
> theory is loaded into the theory cache, it will take much less time
> to access if it is needed again. However repeatedly activating binders
> in the ancester thoeries still wastes time.
> 
> Unless we change the format of the theory file, which will
> probably introduce incompatibility and not many people will like it,
> this problem is difficult to solve.

Well, ... this was one of the changes I made to the HOL system I use
here. Binders are now stored as a seperate chapter (?) in the theory
file. 

> A way to fix the recursively up the theory tree activating binders
> problem without changing the theory file format
> is to reimplement the activate_all_binders function in the system
> which I have just done. In the new implementation, I first get the
> names for all the ancesters of the theory whose binders are to be
> activated and then activate the binders in each of them.

I sort of did that fix as well ... I had thought that that one had been
incorporated into HOL.

> I use a
> global variable to store the names of all the theories which has
> been visited to activate their binders.

Instead of this you can just modify the ancestors functions so that has
an "accumulating parameter" into which ancestor theories get added with
a check on each recursion to abandon a search up the tree if the
current theory is already in the list.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		Life doesn't imitate art, it imitates bad television
						      - Husbands and Wives