Bingham, Jesse D wrote:
> I've defined a nested record type structure my_type that contains 8
> type variables 'typevar1,...,'typevar8. Whenever I mention this
> type, I have to do something like
>
('typevar1,'typevar2,'typevar3,'typevar4,'typevar5,'typevar6,'typevar7,'typevar8)my_type
> which is obviously a little messy. My question (and I'm not sure if
> this even makes sense): is there a way to make type variables have
> scope as being a whole theory? I suppose what I'm after is the
> ability to simply write
> my_type
> or something slimilar and have HOL interpret this as the messy type
> expression above. Thanks
Assuming the type-variables above are all different, the best way to
achieve this would be with anti-quotation.
Do
val my_type = ``:('ty1,'ty2,...) my_type``
val my_type_t = ty_antiq my_type
then if you need to provide type annotations within terms, you can do
things like
val t = ``P (x:^my_type_t)``
if you need to quote your type in a type context, as in declaring
another datatype, you use my_type:
val new_type = Hol_datatype `new_type = C of ^my_type => num
| D of bool`
If there is significant overlap within the type variables, e.g., if
you are often dealing with
('a,'b','c,'a,'a,'a,'b,'c) my_type
then I'd use type abbreviation to generate a ternary operator
type_abbrev( "my_type'", ``:('a,'b','c,'a,'a,'a,'b,'c) my_type``)
you could then write ``:('a,'b,'c) my_type'`` to get the more involved
expansion, as well as ``:(num,bool,char) my_type'`` to get the obvious
instantiation thereof. (This ability to get the instantiation is the
advantage of using a type abbreviation.)
Michael.
-------------------------------------------------------------------------
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems? Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >> http://get.splunk.com/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
