Maude-help mailing list

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

Hi,

You forgot to declare a constant  T of sort Qid in the metamodule that you 
construct (you only have a constant T of sort Thing but you use both). The 
corrected code is:

mod TEST is
        including META-LEVEL .
        including META-MODULE .
        including QID .

        op Test : Qid -> ResultPair .

        vars Q : Qid .

        eq Test( Q ) =
                metaReduce(
                        (mod 'TEST is
                                including 'QID .
                                sorts 'Thing .
                                none
                                op Q : nil -> 'Thing [ctor] .
                                op Q : nil -> 'Qid [ctor] .
                                op 'convert : 'Thing -> 'Qid [none] .
                                none
                                eq 'convert[ qid(string(Q) + ".Thing") ]
                                        = qid(string(Q) + ".Qid") [none] .
                                none
                        endm),
                        'convert[ qid(string(Q) + ".Thing") ]
                )
        .
endm

reduce Test( 'T ) .

Steven


On Friday 03 December 2004 06:31 am, Jay McCarthy wrote:
> Can someone explain why the following error is generated?
>
> ----
>
> mod TEST is
>       including META-LEVEL .
>       including META-MODULE .
>       including QID .
>
>       op Test : Qid -> ResultPair .
>
>       vars Q : Qid .
>
>       eq Test( Q ) =
>               metaReduce(
>                       (mod 'TEST is
>                               including 'QID .
>                               sorts 'Thing .
>                               none
>                               op Q : nil -> 'Thing [ctor] .
>                               op 'convert : 'Thing -> 'Qid [none] .
>                               none
>                               eq 'convert[ qid(string(Q) + ".Thing") ]
>                                       = qid(string(Q) + ".Qid") [none] .
>                               none
>                       endm),
>                       'convert[ qid(string(Q) + ".Thing") ]
>               )
>       .
> endm
>
> reduce Test( 'T ) .
>
> -----
>
> ==========================================
> reduce in TEST : Test('T) .
> Advisory: could not find a constant T of sort Qid in meta-module TEST.
> rewrites: 6 in 0ms cpu (6ms real) (~ rewrites/second)
> result [ResultPair?]: metaReduce(mod 'TEST is
>   including 'QID .
>   sorts 'Thing .
>   none
>   op 'T : nil -> 'Thing [ctor] .
>   op 'convert : 'Thing -> 'Qid [none] .
>   none
>   eq 'convert['T.Thing] = 'T.Qid [none] .
>   none
> endm, 'convert['T.Thing])
> Maude>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help