Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Oops! I was missing a colon; it should have been:

view Term from TRIV to META-TERM *
  (op empty : -> TermList to emptyTermList,
   op _,_ : TermList TermList -> TermList to _|_) is
  sort Elt to Term .
endv

fmod RENAME-TEST is

  including SET{Term} *
    (op empty : -> Set{Term} to emptySet ,
     op _,_ : Set{Term} Set{Term} -> Set{Term} to _;_ ,
     op _|_ : TermList TermList -> TermList to (_,_) ,
     op emptyTermList : -> TermList to empty) .

endfm

On 3/21/13 9:01 PM, Steven Eker wrote:
> The clash on the empty and _,_ operators is coming from the formation 
> of SET{Term} - this module cannot be constructed
> because of the clash and so the later renaming is irrelevant.
>
> Since modules with free parameters cannot be renamed, the only thing I 
> can think of is to rename the operators in META-TERM,
> do the instantiation, then rename everything the way you want it:
>
> view Term from TRIV to META-TERM *
>   (op empty : -> TermList to emptyTermList,
>    op _,_ : TermList TermList -> TermList to _|_) is
>   sort Elt to Term .
> endv
>
> fmod RENAME-TEST is
>
>   including SET{Term} *
>     (op empty : -> Set{Term} to emptySet ,
>      op _,_ : Set{Term} Set{Term} -> Set{Term} to _;_ ,
>      op _|_ : TermList TermList -> TermList to (_,_) ,
>      op emptyTermList -> TermList to empty) .
>
> endfm
>
> Kind of ugly though...
>
> Steven
>
> On 3/21/13 4:40 PM, Daniel Selsam wrote:
> > Hi,
> >
> > [Code below]
> >
> > Why doesn't the module renaming address this problem? How should I 
> > address it?
> >
> > Thanks,
> >
> > Dan
> >
> > view Term from TRIV to META-TERM is sort Elt to Term . endv
> >
> > fmod RENAME-TEST is
> >
> > including SET{Term} *
> > (  op empty : ->  Set{Term} to emptySet ,
> >     op _,_ : Set{Term} Set{Term} ->  Set{Term} to _;_ ,
> >     op _,_ : NeSet{Term} Set{Term} ->  Set{Term} to _;_
> > ) .
> >
> > endfm
> >
> > ***(
> >
> > Maude>  load set.maude
> > Advisory:<automatic>: operator empty has been imported from both
> >      "prelude.maude", line 1540 (fmod META-TERM) and "prelude.maude", 
> > line 1135
> >      (fmod SET) with no common ancestor.
> > Warning: "prelude.maude", line 1136 (fmod SET): declaration for _`,_ has
> >      different attributes from declaration on "prelude.maude", line 
> > 1541 (fmod
> >      META-TERM).
> > Advisory:<automatic>: operator _`,_ has been imported from both
> >      "prelude.maude", line 1541 (fmod META-TERM) and "prelude.maude", 
> > line 1136
> >      (fmod SET) with no common ancestor.
> > Warning: "prelude.maude", line 1136 (fmod SET): declaration for _`,_ has
> >      different attributes from declaration on "prelude.maude", line 
> > 1541 (fmod
> >      META-TERM).
> > Advisory:<automatic>: unable to make module instantiation SET{Term} 
> > due to
> >      earlier errors.
> >
> > )
> > _______________________________________________
> > Maude-help mailing list
> > Maude-help AT cs.uiuc.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help