Maude-help mailing list

[Lorenzo Capra <capra AT di.unimi.it>]

Dear Maude's designers/programmers
I'm very interested in Maude and I'm extensively using it in a project
on rewritable Petri Nets 
(https://urldefense.com/v3/__https://github.com/lgcapra/rewpt__;!!DZ3fjg!4kEcX0wIREkD3_ruCzU85fX4QYYWfnStHcuzL3cIP-L4sirAeDOkYB9IIrUsNEWjEKmVxSCycG9fa21cvtgmLIzEZxqt$
  )

There is a question about sort renaming that I cannot solve and for
which I need your help.
The Maude code is below (and attached as a separated file)

I'm using the prelude's LIST module and (for particular reasons) I'd
like to define lists of lists. But I don't need "generalized" lists.

For that I defined the ELIST module, which defines an "embeddable"
list through a simple unary operator {_} embedding an ordinary list,
and the NESTED-LIST module which defines a "nested" list just as a
list of embeddable ones.
A parameterized view Elist view allows one to link ELIST to NESTED-LIST.

Then I defined a module COMPARABLE-LIST{X :: STRICT-WEAK-ORDER}
(the core of the question)  which extends  (in a protected  way) both
the built-in module WEAKLY-SORTABLE-LIST{X :: STRICT-WEAK-ORDER}  and
NESTED-LIST{X :: TRIV}.
This module defines a pseudo-lexicographic order among lists (below I
omit all related stuff because the point is another; let me also omit
the reasons why I need to use NESTED-LIST).
To instantiate the module NESTED-LIST{X :: TRIV} I need to use the
built-in view STRICT-WEAK-ORDER from TRIV to the homonym theory

For convenience, I'd like to do some sort renaming in COMPARABLE-LIST,
but this works only partially (probably because there is something I
don't understand about renaming and module instantiation)

In particular ...
* (sort List{Elist{STRICT-WEAK-ORDER}{X}} to List{Elist{X}}, sort
NeList{Elist{STRICT-WEAK-ORDER}{X}} to NeList{Elist{X}})
doesn't apply, whereas the other renaming works

but all seems fine: the show command tells me that there are in fact two sorts
List{Elist{STRICT-WEAK-ORDER}{X}}
NeList{Elist{STRICT-WEAK-ORDER}{X}}
(among the others) and that is confirmed by reducing
Maude> red {nil} {nil} {} .
reduce in COMPARABLE-LIST : {nil} {nil} .
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
result NeList{Elist{STRICT-WEAK-ORDER}{X}}: {nil} {nil}

Module's instantiation seems to interfere with renaming but I cannot
explain (also after carefully reading chap 6 of online manual)  why
the above renaming fails also if the involved sorts do apparently
exist.
(but if I try to use one of these sorts, e.g., to define an operator,
the Maude's interpreter tells me that it doesn't exist !)

Any help will be be greatly appreciated.

Thanks in advance.
My best regards

Lorenzo Capra

*** "embedded" list definition (useful to define nested lists) by @Lorenzo 
Capra
fmod ELIST{X :: TRIV} is
    pr LIST{X} .
    sort Elist{X} .
    op {_} : List{X} -> Elist{X}  [ctor] .
    op join : Elist{X} Elist{X} -> Elist{X} [assoc] .
    vars L L' : List{X} .
    eq join({L}, {L'}) = {L L'} .
 endfm

 view Elist{X :: TRIV} from TRIV to ELIST{X} is
   sort Elt to Elist{X} .
endv

fmod NESTED-LIST{X :: TRIV} is
  pr LIST{Elist{X}} * (op nil : -> List{Elist{X}} to {}) .
endfm


fmod COMPARABLE-LIST{X :: STRICT-WEAK-ORDER} is
  pr WEAKLY-SORTABLE-LIST{X} .
  pr NESTED-LIST{STRICT-WEAK-ORDER}{X} * (sort
List{STRICT-WEAK-ORDER}{X} to List{X}, sort
NeList{STRICT-WEAK-ORDER}{X} to NeList{X})
                                       * (sort
List{Elist{STRICT-WEAK-ORDER}{X}} to List{Elist{X}}, sort
NeList{Elist{STRICT-WEAK-ORDER}{X}} to NeList{Elist{X}})
                                       * (sort
Elist{STRICT-WEAK-ORDER}{X} to Elist{X})
                                      .
  *** op partition : List{X} -> List{Elist{STRICT-WEAK-ORDER}{X}} .
endfm

Attachment: COMPARABLE-LIST2.maude
Description: Binary data