Maude-help mailing list

[Edgar Honing <ephoning AT gmail.com>]

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
>
>