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) outside ac.uk; Fri, 29 Jan 1993 19:44:43 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA18556;
          Fri, 29 Jan 93 11:30:12 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from crl.dec.com by ted.cs.uidaho.edu (16.6/1.34) id AA18551;
          Fri, 29 Jan 93 11:29:15 -0800
Received: by crl.dec.com; id AA27578; Fri, 29 Jan 93 14:28:24 -0500
Received: by easynet.crl.dec.com; id AA04146; Fri, 29 Jan 93 14:28:19 -0500
Message-Id: <9301291928.AA04146@easynet.crl.dec.com>
Received: from ricks.enet; by crl.enet; Fri, 29 Jan 93 14:28:20 EST
Date: Fri, 29 Jan 93 14:28:20 EST
From: "Tim Leonard, DTN 225-5809, HLO2-3/C11 29-Jan-1993 1425" 
      <leonard@com.dec.enet.ricks> 
To: info-hol@edu.uidaho.cs.ted
Cc: leonard@com.dec.enet.ricks
Apparently-To: info-hol@ted.cs.uidaho.edu
Subject: Bug in "parents"

I think the ML functions "parents" and "ancestors" are broken.  It looks as
though "parents" fails on a theory with no parents, rather than returning an
empty list (see the examples below).  "ancestors" always fails.  My guess is
it tries to recursively call "parents" until an empty list is returned.  Note
that "ancestry", which uses a different mechanism, works properly.

Tim

% hol
===============================================================================
         HOL88 Version 2.01 (DECstation/Lucid Lisp), built on 8/1/93
===============================================================================

#print_theory `-`;;
The Theory HOL
Parents --  BASIC-HOL     one     sum     tydefs     
******************** HOL ********************

() : void

#ancestry();;
[`one`;
 `sum`;
 `num`;
 `prim_rec`;
 `arithmetic`;
 `list`;
 `tree`;
 `combin`;
 `ltree`;
 `tydefs`;
 `HOL`;
 `PPLAMB`;
 `bool`;
 `ind`;
 `BASIC-HOL`]
: string list

#parents `BASIC-HOL`;;
[`ind`] : string list

#parents `ind`;;
error -- 
evaluation failed     parents -- ind theory missing

#mapfilter parents (ancestry());;
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
[[`BASIC-HOL`];
 [`ltree`; `BASIC-HOL`];
 [`tydefs`; `sum`; `one`; `BASIC-HOL`];
 [`PPLAMB`];
 [`ind`]]
: string list list

#mapfilter ancestors (ancestry());;
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
error -- 
[] : string list list

#