maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

Re: [Maude-help] Problem with QID in META-MODULEs

From: Jay McCarthy <jay.mccarthy AT gmail.com>
To: eker AT csl.sri.com
Cc: maude-help AT peepal.cs.uiuc.edu
Subject: Re: [Maude-help] Problem with QID in META-MODULEs
Date: Fri, 3 Dec 2004 23:00:05 -0500
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:references; b=Zlo7C96l84fvBKi3v9SpzJ9HlLpR9toPArFf8DPi6SfDVp518aFb8eTq9FmRHcKzEh4C0XzrrPS2EyviboYuLdXPNs9esBwmtQ/2h7urKuDngrCyk+6rgIYaXjjBlD3vBSYv6du5bINioX1JCLOH2Z9Mc6RIXMiNEK8NiwiuayU=
List-archive: <http://maude.cs.uiuc.edu/pipermail/maude-help>
List-id: Maude help list <maude-help.maude.cs.uiuc.edu>

I ended up solving the problem. Perhaps I should have been more clear
with what I expected would happen.

This code contains three tests. The first two fail, but for different
reasons. The second succeeds. I was trying to use the auto-creation of
QID constants in a meta-module, but I had not realize 'T.Qid was not
correct, it is ''T.Qid.

Thank you,

Jay

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

op _+_ : Qid String -> Qid .
op addsort : Qid Qid -> Qid .
op metaQid : Qid -> Qid .

var Q T : Qid .
var S : String .
eq Q + S = qid(string(Q) + S) .
eq addsort( Q, T ) = Q + ("." + string(T)) .
eq metaQid( Q ) = qid("'" + string(Q) + ".Qid") .

op Test-1 : Qid -> ResultPair .
op Test-2 : Qid -> ResultPair .
op Test-3 : Qid -> ResultPair .

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

eq Test-2( Q ) =
metaReduce(
(mod 'META-TEST is
nil
sorts 'Qid ; 'Thing .
none
op Q : nil -> 'Qid [ctor] .
op Q : nil -> 'Thing [ctor] .
op 'convert : 'Thing -> 'Qid [none] .
none
eq 'convert[ addsort( Q, 'Thing ) ]
= addsort(Q, 'Qid ) [none] .
none
endm),
'convert[ addsort(Q, 'Thing) ]
)
.

eq Test-3( Q ) =
metaReduce(
(mod 'META-TEST is
including 'QID .
sorts 'Thing .
none
op Q : nil -> 'Thing [ctor] .
op 'convert : 'Thing -> 'Qid [none] .
none
eq 'convert[ addsort(Q, 'Thing) ]
= metaQid(Q) [none] .
none
endm),
'convert[ addsort(Q, 'Thing) ]
)
.

endm

reduce downTerm( getTerm( Test-1( 'T ) ), 'error ) .
reduce downTerm( getTerm( Test-2( 'T ) ), 'error ) .
reduce downTerm( getTerm( Test-3( 'T ) ), 'error ) .

On Fri, 3 Dec 2004 11:43:44 -0700, Steven Eker
<eker AT csl.sri.com>
wrote:
> 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
>

--
Jay McCarthy
<jay.mccarthy AT gmail.com>
http://www.makeoutcity.com/

[Maude-help] Problem with QID in META-MODULEs, Jay McCarthy, 12/03/2004
- Re: [Maude-help] Problem with QID in META-MODULEs, Steven Eker, 12/03/2004
  - Re: [Maude-help] Problem with QID in META-MODULEs, Jay McCarthy, 12/03/2004