Maude-help mailing list

[Marko Schuetz-Schmuck <MarkoSchuetz AT web.de>]

Dear All,

if I define

(fth TICK-SIZE is protecting FLOAT . op ticksize : -> Float . endfth)
(fmod X-AXIS-TICK-SIZE is protecting FLOAT . op ticksize : -> Float . eq 
ticksize = 0.01 . endfm)
(view X-AXIS-TICK-SIZE from TICK-SIZE to X-AXIS-TICK-SIZE is op ticksize to 
ticksize . endv)
(fmod TICK{X :: TICK-SIZE} is
    protecting CONVERSION .
    op toFloat : Nat -> Float .
    var T : Nat .
    eq toFloat(T) = float(T) * ticksize .
endfm)

then I can

Maude> (red in TICK{X-AXIS-TICK-SIZE} : toFloat(10) .)
reduce in TICK{X-AXIS-TICK-SIZE}:
  toFloat(10)
result FiniteFloat :
  1.0000000000000001e-1

But maybe I want to constrain the ticks, say to less than 100:

(fmod TICK{X :: TICK-SIZE} is
    protecting CONVERSION .
    sort Tick .
    subsort Tick < Nat .
    var N : Nat .
    cmb N : Tick if N < 100 .
    op toFloat : Tick -> Float .
    var T : Tick .
    eq toFloat(T) = float(T) * ticksize .
endfm)

then I get

Maude> (red in TICK{X-AXIS-TICK-SIZE} : toFloat(10) .)
<warnings removed>
reduce in TICK{X-AXIS-TICK-SIZE}:
  toFloat(10)
result [Float] :
  toFloat(10)

I do not see why the reduction stops there and why

(red in TICK{X-AXIS-TICK-SIZE} : 0 :: Tick .)

is false. Is this related to the warnings about membership axioms in the
presence of associative and/or iterated symbols with declarations not at
the kind level?

Best regards,

Marko
-- 
Prof. Dr. Marko Schütz-Schmuck
Department of Computer Science and Engineering
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681

Attachment: signature.asc
Description: PGP signature