Maude-help mailing list

[Richard Graham <rickhg12hs AT gmail.com>]

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
http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help