Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 23 Feb 1994 18:42:20 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28743;
          Wed, 23 Feb 1994 11:27:49 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from panther.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA28739;
          Wed, 23 Feb 1994 11:27:48 -0700
Received: from localhost by panther.cs.byu.edu with SMTP (1.37.109.8/16.2) 
          id AA20952; Wed, 23 Feb 1994 11:28:19 -0700
To: info-hol@leopard.cs.byu.edu
Subject: Partial evaluation in ML?
Date: Wed, 23 Feb 1994 11:28:18 -0700
From: Phil Windley <windley@leopard.cs.byu.edu>
Message-ID: <"swan.cl.cam.:251380:940223184300"@cl.cam.ac.uk>


Perhaps I'm missing something obvious, but....

When I do the following:


    let dist_thm_list = 
	let thms = CONJUNCTS Instruction_distinct in
	thms @ (map GSYM thms);;


    let INST_DIST_TAC = REWRITE_TAC dist_thm_list;;

HOL responds with:

    INST_DIST_TAC = - : tactic
    Run time: 14.9s
    Garbage collection time: 31.4s
    Intermediate theorems generated: 12792


Notice the "Intermediate theorems generated: 12792".  This implies that HOL
is doing partial evaluation on curried arguments, doesn't it?  Is it
really, or is it doing something simpler which I'm missing?

In either event, the upshot is that for large theorem lists, one can save
proof time by preevaluating the REWRITE_TAC's.   This proof actually breaks
out into 729 cases where INST_DIST_TAC is used, so the savings is
VERY significant.

--phil--