Maude-help mailing list

[Francisco Durán <duran AT lcc.uma.es>]

Hi Edgar,

The situation is different for a nat term. The (least) sort of the
term 4 is Nat, without any possible ambiguity. But given the
declarations for (_,_) there are two possible sorts for term (2, 3).
Adding the subsort declaration Tuple{Nat, Nat} < Tuple{List{Nat},
List{Nat}} makes the least sort of (2,3) unique.

Francisco

On Thu, Apr 15, 2010 at 4:48 PM, Edgar Honing 
<ephoning AT gmail.com>
 wrote:
> Hi Francisco,
>
> Thanks for your quick feedback. And, yes, I realized the possible dual
> interpretation. But as I do not see the same kind of clash when reducing a
> single stand-alone 'Nat' (as it could be interpreted both as a Nat instance
> and a List{Nat} instance of length 1), I figured things would be fine as
> well when it appears wrapped in a tuple. So is it that these sort orderings
> do not "carry" when these sorts are used as components of yet other sorts?
> Anyways, introducing the (sub)sort ordering as you suggested did the trick -
> thanks much!
>
> Cheerio,
> Edgar
>
> On Thu, Apr 15, 2010 at 1:53 AM, Francisco Durán 
> <duran AT lcc.uma.es>
>  wrote:
>>
>> Hi Edgar,
>>
>> I don't think you are doing anything wrong, it is just that you are
>> getting some conflict you need to take care of.
>>
>> What is happening is that you are getting two operators
>>
>> op (_,_) : Nat Nat -> Tuple{Nat, Nat} .
>> op (_,_) : List{Nat} List{Nat} -> Tuple{List{Nat}, List{Nat}} .
>>
>> for which, as the message given indicates, you have the same domain
>> kinds but a different range kind. The problem is that if you have a
>> term like (2, 3) it can be both a Tuple{Nat, Nat} and a
>> Tuple{List{Nat}, List{Nat}}.
>>
>> Depending on what you need you may go for making the range sorts
>> related (Tuple{Nat, Nat} < Tuple{List{Nat}, List{Nat}}) or just making
>> the operators different, e.g., with
>>
>> (fmod SOMETYPES is
>>    pr TUPLE[2]{Nat,Nat} .
>>    pr TUPLE[2]{List{Nat},List{Nat}} * (op `(_`,_`) to `[_`,_`]) .
>> endfm)
>>
>> Cheers,
>>
>> Francisco
>>
>> On Thu, Apr 15, 2010 at 7:34 AM, Edgar Honing 
>> <ephoning AT gmail.com>
>>  wrote:
>> > Hi,
>> >
>> > In the context of trying to implement some standard func. programming
>> > idioms
>> > (such as fold/zip/zipWith/etc.) I have a need for parameterized
>> > types/sorts
>> > for such constructs as lists of 2-tuples and 2-tuples of lists. When
>> > trying
>> > to define these I keep getting presented with the following warning
>> > (followed up by parsing issues):
>> >
>> > Warning: <metalevel>: declaration for `(_`,_`) has the same domain kinds
>> > as
>> > the declaration on <metalevel> but a different range kind.
>> >
>> > In order to try and get to the bottom of this I came up with the
>> > following
>> > minimalistic full maude text that results in this same problem:
>> >
>> >
>> > (view List{A :: TRIV} from TRIV to LIST{A} is
>> >     sort Elt to List{A} .
>> > endv)
>> >
>> > (fmod SOMETYPES is
>> >     pr TUPLE[2]{Nat,Nat} .
>> >     pr TUPLE[2]{List{Nat},List{Nat}} .
>> > endfm)
>> >
>> > (red (1,2) .)           <- gives parse error
>> > (red (1 2,3 4) .)     <- gives parse error
>> >
>> >
>> > Changing 'pr TUPLE[2]{Nat,Nat} .' to, say, 'pr TUPLE[2]{String,String}
>> > .',
>> > or 'pr TUPLE[2]{Nat,String} .' avoids this "clash" / warning + parsing
>> > issue.
>> > Any pointers on what I am doing wrong  / how to resolve this would be
>> > much
>> > appreciated!
>> >
>> > Thanks much in advance,
>> > Edgar
>> >
>> > _______________________________________________
>> > Maude-help mailing list
>> > Maude-help AT cs.uiuc.edu
>> > http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>> >
>> >
>
>