Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@cs.uidaho.edu, reetz@ira.uka.de
Cc: schneide@ira.uka.de
In-Reply-To: reetz's message of Thu, 9 Dec 1993 23:28:26 +0100 <"i80fs2.ira.005:09.11.93.16.28.29"@ira.uka.de>
Subject: define_type within hol90.5 and hol90.6
Message-Id: <93Dec9.182838met.8086@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 9 Dec 1993 18:28:28 +0100


> new_theory "demo";
>
> define_type
>    {fixities =[Prefix,Prefix,Prefix],
>    name     ="CompTree",
>    type_spec=`CompTree=C_Compnode  of CompTree#CompTree#('M->'M->'M)|
>                        C_Varleaf   of 'VN|
>                        C_Constleaf of 'M`};
> 
> using hol90.6, I get the following:
> 
> define_type
>   {fixities =[Prefix,Prefix,Prefix],
>    name     ="CompTree",
>    type_spec=`CompTree=C_Compnode  of CompTree#CompTree#('M->'M->'M)|
>                        C_Varleaf   of 'VN|
>                        C_Constleaf of 'M`};
>
> Exception raised at Parse_support.make_type_clause.check:
> recursive occurrence of defined type is deeper than the first level
>  
> uncaught exception HOL_ERR
>
> does anybody have an idea?

Yes, I do: try 

> define_type
  {fixities =[Prefix,Prefix,Prefix],
   name     ="CompTree",
   type_spec=`CompTree=C_Compnode  of CompTree => CompTree|
                       C_Varleaf   of 'VN|
                       C_Constleaf of 'M`};

This is a difference between version5 and version6: it is noted in the
file doc/5.changes in the hol90.6 distribution. The change notice reads

> 7. Changed the parsing of type specifications. The syntax of the hol88
>    version is more subtle than I thought; it allows the defined constructor
>    to be curried or not. My boneheaded version in hol90.5 wouldn't allow
>    type constructors that took paired arguments. Now that has been fixed,
>    at the cost of some special syntax. A curried constructor has "=>"
>    between its arguments, while an uncurried constructor has just a single
>    argument, which can have the form of any type. The "=>" is merely a
>    delimiter that makes parsing simple, plus I hope that it has an
>    intuitive reading if one confuses the "=>" with "->".

Since C_Compnode is a curried constructor of type 

    :('VN,'M)CompTree -> ('VN,'M)CompTree -> ('VN,'M)CompTree

it needs to appear as 

    C_Compnode  of CompTree => CompTree

in the type specification. If it had been uncurried, it would appear as 

    C_Compnode  of CompTree#CompTree

in the type specification.

Konrad.