Maude-help mailing list

[ZHANG Min <zhmtechie AT gmail.com>]

Dear all:

I found there are two forms of meta-representations of the same term by using 
metaParse or upTerm respectively. How could we obtain a uniform term? Here is 
an example:

fmod TEST is 
        sort Test .
        op _,_ : Test Test -> Test [assoc] .
        
        ops a b c : -> Test .
endfm 

fmod TEST-META is 
    inc TEST .
    inc META-LEVEL .
endfm 


When I used the following command, I got:

red upTerm((a,b,c)) .

result GroundTerm: '_`,_['a.Test,'b.Test,'c.Test]


The following command gave me the different form:

red getTerm(metaParse(upModule('TEST, false), 'a '`, 'b '`, 'c, anyType)) .

result GroundTerm: '_`,_['a.Test,'_`,_['b.Test,'c.Test]]


But at object level, it was  a,b,c. How could I get a uniform 
meta-representation of a term? 


http://www.jaist.ac.jp/~zhangmin
Research Center for Software Verification 
Japan Advanced Institute of Science and Technology (JAIST)