Maude-help mailing list

[Francisco Durán <narudocap AT gmail.com>]

Hi Lorenzo,

There is some problem with out maude-help mailing list. Whilst I figure out 
what's going on, let me forward you an answer by Steven Eker 
(eker AT csl.sri.com). 

Best regards, 

Francisco 

--------
Hi Lorenzo,

It looks like you have found a bug in the sort handling. Essentially the sort
  List{Elist{STRICT-WEAK-ORDER}{X}}
created by the module system has an incorrect internal representation and is
different from the sort
  List{Elist{STRICT-WEAK-ORDER}{X}}
created by the parser which has the correct internal representation even 
though
they print to the same ASCII representation.

A simpler demonstration of the issue:

fmod FOO{X :: STRICT-WEAK-ORDER} is
  protecting LIST{Set{STRICT-WEAK-ORDER}{X}} .
  op a : -> NeList{Set{STRICT-WEAK-ORDER}{X}} .
endfm

show kinds .

Here there appear to be two sorts called
  NeList{Set{STRICT-WEAK-ORDER}{X}}
One created by the module system in the kind where you expect it and one
in a kind of its own created by the parser to patch the
  Warning: <standard input>, line 3 (fmod FOO): undeclared sort 
NeList{Set{STRICT-WEAK-ORDER}{X}}.
situation and avoid a cascade of warnings.

This is a critical bug and will be fixed in the next release.

A couple of other remarks on your specification. It looks like you are trying
to merge to sorts by importing
  WEAKLY-SORTABLE-LIST{X}
and trying to rename the sorts of
  NESTED-LIST{STRICT-WEAK-ORDER}{X}
to match. This is never allowed - the module system cannot be treated
like a macro preprocessor - it matters where sorts come from and while
operators can be overloaded sorts cannot, nor can they be merged.
Also there is no need to break your renaming into three pieces.

I'm guessing your are following the structure of the SORTABLE-LIST-AND-SET
module in the prelude. Here sorts are not being merged rather the double 
renaming
ensures the same exact instantiation and renaming of the LIST module is used 
so
it becomes just a single shared instance:
  SORTABLE-LIST{X}
generates
  LIST{STRICT-WEAK-ORDER}{X}
  *
  (sort NeList{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to 
NeList{STRICT-TOTAL-ORDER}{X},
   sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to 
List{STRICT-TOTAL-ORDER}{X})
  *
  (sort NeList{STRICT-TOTAL-ORDER}{X} to NeList{X},
   sort List{STRICT-TOTAL-ORDER}{X} to List{X}) .
where the double renaming arises from the nested importation and
  LIST-AND-SET{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} *
              (sort NeList{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to 
NeList{STRICT-TOTAL-ORDER}{X},
               sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to 
List{STRICT-TOTAL-ORDER}{X}) *
              (sort NeList{STRICT-TOTAL-ORDER}{X} to NeList{X},
               sort List{STRICT-TOTAL-ORDER}{X} to List{X},
           sort NeSet{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to NeSet{X},
               sort Set{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to Set{X}) .
generates
  LIST{STRICT-WEAK-ORDER}{X}
  *
  (sort NeList{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to 
NeList{STRICT-TOTAL-ORDER}{X},
   sort List{STRICT-WEAK-ORDER}{STRICT-TOTAL-ORDER}{X} to 
List{STRICT-TOTAL-ORDER}{X})
  *
  (sort NeList{STRICT-TOTAL-ORDER}{X} to NeList{X},
   sort List{STRICT-TOTAL-ORDER}{X} to List{X}) .
as well by doing the double renaming explicitly.

In your example,
  WEAKLY-SORTABLE-LIST{X}
generates
  LIST{STRICT-WEAK-ORDER}{X} *
              (sort NeList{STRICT-WEAK-ORDER}{X} to NeList{X},
               sort List{STRICT-WEAK-ORDER}{X} to List{X})
while
  NESTED-LIST{STRICT-WEAK-ORDER}{X}
generates
  LIST{Elist{X}} * (op nil : -> List{Elist{X}} to {})
and no amount of renaming can convert this into the same module expression
that will allow the instantiation of the LIST module to be shared.

Steven

> On 30 Sep 2022, at 17:28, Lorenzo Capra <capra AT di.unimi.it> wrote:
> 
> 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
> <COMPARABLE-LIST2.maude>