Maude-help mailing list

[Hojjat Hossein <hossein.hojjat AT epfl.ch>]

Hi,

>From a comment from one of my friends I noticed that although you can access 
>the modules of (Core) Maude in FULL-MAUDE, but the views are lost. So as you 
>stated one should explicitly load the needed views.
For example, in machine-int.maude some views are defined for bit lengths, but 
I suppose that whenever you want to use any of them you have to redefine it 
in your program.
The following fmod is correct:

(view 32-BIT from BIT-WIDTH to RENAMED-INT is
  op $nrBits to term 32 .
endv)
(fmod machineint-FullMaude is
       protecting MACHINE-INT{32-BIT} .
       vars A, B : MachineInt .
       op plus : MachineInt MachineInt -> MachineInt .
       eq plus(A , B) = A + B .
endfm)

Best
________________________________________
From: Richard Graham 
[rickhg12hs AT gmail.com]
Sent: Sunday, January 18, 2009 3:33 AM
To: Hojjat Hossein
Cc: 
maude-help AT maude.cs.uiuc.edu;
 Jobstmann Barbara
Subject: Re: [Maude-help] Using MachineInt in Full-Maude

Hi,

I'm a complete Maude noob, but I found your question interesting.  I don't 
know a convenient answer but I can get your fmod to work in full-maude if I 
cut-paste each part of machine-int.maude into full-maude.  I.e.,

$ maude full-maude
...
....
Maude> (fmod RENAMED-INT is
  protecting INT * (
    sort Zero to MachineZero,
    sort NzNat to NzMachineNat,
    sort Nat to MachineNat,
    sort NzInt to NzMachineInt,
    sort Int to MachineInt,
...
....
endfm
)

Maude> (fth BIT-WIDTH is
  protecting RENAMED-INT .
  op $nrBits : -> NzMachineNat .

  var N : NzMachineNat .
  eq $divides(2, $nrBits) = true [nonexec] .
  ceq $divides(2, N) = true if $divides(N, $nrBits) /\ N > 1 [nonexec] .
endfth
)
...
....
and then

Maude> (fmod machineint-FullMaude is
       protecting MACHINE-INT{32-BIT} .
       vars A, B : MachineInt .

       op plus : MachineInt MachineInt -> MachineInt .

       eq plus(A , B) = A + B .

endfm)

Maude> ( red in machineint-FullMaude : plus(5,10) . )
rewrites: 1594 in 18ms cpu (20ms real) (83907 rewrites/second)
reduce in machineint-FullMaude :
  plus(5,10)
result NzMachineNat :
  15

Maude>

I'm hoping somebody will reply with a more sane way of using MACHINE-INT in 
full-maude.
[Why doesn't ( load machine-int . ) work?  It produces no errors/warnings but 
seems to do nothing.]

I hope this helps or inspires further replies.

Cheers!
Richard Graham

On Fri, Jan 16, 2009 at 12:32 PM, Hojjat Hossein 
<hossein.hojjat AT epfl.ch>
 wrote:
Hello,

I have problems using machineint with full-maude.
I am using Maude 2.4.
I can easily load the following module into core Maude and use it:

fmod machineint-CoreMaude is
       protecting MACHINE-INT{32-BIT} .
       vars A, B : MachineInt .

       op plus : MachineInt MachineInt -> MachineInt .

       eq plus(A , B) = A + B .

endfm

But as soon as I switch to full-maude there are errors when loading the 
module:

(fmod machineint-FullMaude is
       protecting MACHINE-INT{32-BIT} .
       vars A, B : MachineInt .

       op plus : MachineInt MachineInt -> MachineInt .

       eq plus(A , B) = A + B .

endfm)

Maude> load Examples/machineint-FullMaude
Advisory: could not find sort NzMachineInt in meta-module 
machineint-FullMaude.
Advisory: bad operator declaration op '$mask : nil -> 'NzMachineInt [memo 
strat(0)] . in meta-module machineint-FullMaude.
...
....

I'd be glad if someone can point out what I am missing in this program.

The best,
Hossein Hojjat
PhD Student
EPFL
_______________________________________________
Maude-help mailing list
Maude-help AT maude.cs.uiuc.edu<mailto:Maude-help AT maude.cs.uiuc.edu>
http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help