Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: David Shepherd <des@uk.co.inmos>
Message-Id: <24250.9206160842@frogland.inmos.co.uk>
Subject: Re: [Wishnu Prasetya: bad varstruct??]
To: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Tue, 16 Jun 92 9:42:11 BST
Cc: wishnu@nl.ruu.cs
In-Reply-To: <"swan.cl.ca.737:15.05.92.15.44.12"@cl.cam.ac.uk>; from "Tom Melham" at Jun 15, 92 4:43 pm

Tom Melham has said:
> > I'm trying to define a simple function called root, which given an
> > ltree of something, will return the root of the tree.  Here is how I
> > have coded my definition:
> > 
> > 	new_definition(`root_def`, 
> > 		"(root:((*)ltree->*)) (Node a t) = a") ;;
> > 
> > but then I got an error saying
> > 
> > 	evaluation failed     bad varstruct
> > 
> > What's that supposed to mean? What was wrong with my definition?
> 
> The function new_definition works only for definitions of a specific
> form, namely:
> 
>      fun v1 v2 ... vn = term
> 
> where v1,v2,...,vn are either variables or tuples of variables (the latter
> are called "varstructs").  Your definition has the form:
> 
>      root (Node a t) = t
> 
> and "Node a t" is NOT a varstruct. See the REFERENCE manual for more details.
> 
> By the way, you can define your root function as follows:
> 
>   let th1 = theorem `ltree` `ltree_Axiom` in
>   let th2 = ISPEC "\x:(*)list.\v:*.\tl:((*)ltree)list.v" th1 in
>   let th3 = EXISTENCE (BETA_RULE th2) in
>       new_specification `root_DEF` [`constant`,`root`] th3;;

isn't the problem more likely to be that (*)ltree is a type specified
using 'define_type' and that you're using the wrong definition function here?


supposing we've had

	# let ltree_def = define_type `ltree = Empty | Node * ltree`;;

then what you want is

	# new_recursive_definition false ltree_def `Node' 
                                   "(root:((*)ltree->*)) (Node a t) = a";;


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"i speak latin to god,   spanish to men,   french to women 
		 and german to my horse."             - charles v of spain