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; Tue, 3 Jan 1995 18:07:18 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA16865;
          Tue, 3 Jan 1995 11:01:16 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA16860;
          Tue, 3 Jan 1995 11:01:14 -0700
Received: from tuminfo2.informatik.tu-muenchen.de (tuminfo2.informatik.tu-muenchen.de [131.159.0.81]) 
          by dworshak.cs.uidaho.edu (8.6.9/1.0) with ESMTP id JAA25666 
          for <info-hol@cs.uidaho.edu>; Tue, 3 Jan 1995 09:59:00 -0800
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <56-2>;
          Tue, 3 Jan 1995 18:57:05 +0100
Received: by sunbroy14.informatik.tu-muenchen.de id <8082>;
          Tue, 3 Jan 1995 18:56:58 +0100
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@cs.uidaho.edu, schneide@ira.uka.de
In-Reply-To: <"i80fs2.ira.535:03.01.95.16.54.53"@ira.uka.de> (message from schneide on Tue, 3 Jan 1995 17:54:48 +0100)
Subject: Re: term structure
Message-Id: <95Jan3.185658met.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 3 Jan 1995 18:56:53 +0100


> The definition of this datatype [the type of terms] allows to write
> functions on terms with pattern matching. This is not possible with
> the terms of HOL.  Why can't we have the above type of terms in the
> HOL system?

Pattern matching against abstract datatypes is not allowed in SML, for
good reason. The datatype of HOL terms needs to be abstract so that
every term is well-typed (at the HOL level).

A (very!) experimental alternative can be found by looking at the type
"lambda" and the function "dest_term: term -> lambda" in the structure
"Term". It gives you pattern matching, but the programmer must
explicitly decompose the term by calling "dest_term". 

Example:

    - val COMB{Rator,Rand} = dest_term(concl LET_DEF);

    val Rand = `\f x. f x` : term
    val Rator = `$= LET` : term


Konrad.