view naming with : or . can break things.

[rjsun06]

Things can go weird when you use : or . in a view's name. see below:

fth ANIMAL is
endfth

fmod BASE{X :: ANIMAL} is
    sort Type{X} .
    op t : -> Type{X} .
    op s{X} : -> Type{X} .
endfm

--- I want to fit GOLDEN-RETRIEVER into a slot requiring an ANIMAL, 

fmod GOLDEN-RETRIEVER is
endfm

--- this naming is horrible
view GOLDEN-RETRIEVER-AS-ANIMAL from ANIMAL to GOLDEN-RETRIEVER is
endv
--- this naming is much better
view GOLDEN-RETRIEVER::AS::ANIMAL from ANIMAL to GOLDEN-RETRIEVER is
endv

fmod test is
    inc BASE{GOLDEN-RETRIEVER-AS-ANIMAL} * (op t to t1) .
    inc BASE{GOLDEN-RETRIEVER::AS::ANIMAL} * (op t to t2) .
endfm

red t1 . --- result Type{GOLDEN-RETRIEVER-AS-ANIMAL}: t1
red t2 . --- result Type`{GOLDEN-RETRIEVER::AS::ANIMAL`}: t2

notice the escaped bracket symbol in the resulting sort. Things goes even wilder when doing consecutive viewing .

fth DOG is
endfth

view DOG-AS-ANIMAL from ANIMAL to DOG is
endv
view GOLDEN-RETRIEVER-AS-DOG from DOG to GOLDEN-RETRIEVER is
endv


view DOG::AS::ANIMAL from ANIMAL to DOG is
endv
view GOLDEN-RETRIEVER::AS::DOG from DOG to GOLDEN-RETRIEVER is
endv

fmod test-double is
    inc BASE{DOG-AS-ANIMAL}{GOLDEN-RETRIEVER-AS-DOG} * (op t to t1) .
    inc BASE{DOG::AS::ANIMAL}{GOLDEN-RETRIEVER::AS::DOG} * (op t to t2) .
endfm

red t1 . --- result Type{DOG-AS-ANIMAL}{GOLDEN-RETRIEVER-AS-DOG}: t1
red t2 . --- result Type`{DOG::AS::ANIMAL`}`{X`}: t2 

--- also parameterized constant s{X} is not working .
red s{DOG-AS-ANIMAL}{GOLDEN-RETRIEVER-AS-DOG} . --- this works
red s{DOG::AS::ANIMAL}{GOLDEN-RETRIEVER::AS::DOG} . --- not this one

ps: the same happens on . as well

view DOG.AS.ANIMAL from ANIMAL to DOG is
endv
view GOLDEN-RETRIEVER.AS.DOG from DOG to GOLDEN-RETRIEVER is
endv
fmod test-dot is
    inc BASE{DOG.AS.ANIMAL}{GOLDEN-RETRIEVER.AS.DOG} * (op t to t3) .
endfm

red t3 . --- result Type`{DOG.AS.ANIMAL`}`{X`}: t3
red s{DOG.AS.ANIMAL}{GOLDEN-RETRIEVER.AS.DOG} .
red s`{DOG.AS.ANIMAL`}`{X`} . --- but this weird thing passes .

[ningit]

The Maude manual says in Section 3.3 that sort names must not include :, ., [, or ], and that {, }, and , can only be used in restricted ways. Something similar appears in the grammar of Section B.2. Indirectly, this limits what can be used in view identifiers, although this is not made explicit in the manual.

The strange behavior happens because Maude assumes those restrictions internally, and does not emit warnings on the naming violations. It can be reproduced with a simpler example:

fmod FOO{X :: TRIV} is
        sort Foo::Sort{X} .
endfm

fmod MAIN is
        including FOO{Nat} .
endfm

show sorts .

where the last command shows sort Foo::Sort`{X`} . among other sorts in MAIN.

We will look into it.

[stevenmeker]

The backquotes you are seeing are part of the single token version of the sort name. Because the sort name contains . or : it is not recognized as a parameterized sort name for pretty-printing, pretty-parsing or parameter substitution.

The bigger issue is that view names have fewer restrictions than sort names, and yet after instantiation, view names end up inside sort names. The branch viewFix resolves this by excluding ( ) [ ] { } , from base view names, and allowing : . in sort names as long as they are inside correctly nested {}s. This branch also fixes several other problems with views including the one you reported to the maude-bugs list.

[rjsun06]

That makes a LOT of sense, and I am personally ok with making my names bracketed, unless anyone argue that blacklisting :: is a language issue. Thanks. Oh And, I really hope Maude could blacklist all symbols like : and . in view/module/sort names when parsing, if they are special globally, because I would hope my names to be consistent with other names as long as they pass the parsing.