Maude-help mailing list

[Steven <steveneker AT gmail.com>]

The problem is that operations on floating point numbers work with different data and have different properties to operations on integers so they need to be different operators. For example _+_ is associative on integers but not on floating point numbers.

If the reason for bashing the two types together is that you need a union type, you could use a pair of injections; for example:

fmod NUMBER is
  pr INT .
  pr FLOAT .
  sort Number .
  op [_] : Int -> Number [ctor] .
  op [_] : Float -> Number [ctor] .
endfm

You could even define rules for operations on dissimilar types, by defining operations on Number.

fmod NUMBER is
  pr CONVERSION .
  sort Number .
  op [_] : Int -> Number [ctor] .
  op [_] : Float -> Number [ctor] .
  op _+_ : Number Number -> Number .
  vars X Y : Int .
  vars F G : Float .
  eq [X] + [Y] = [X + Y] .
  eq [F] + [G] = [F + G] .
  eq [X] + [G] = [float(X) + G] .
  eq [F] + [Y] = [F + float(Y)] .
endfm

red [3.142] + [3] .

If you really need Int and Float to be in the same kind, you must rename the clashing operations, for example:

fmod NUMBER is
  pr INT .
  pr FLOAT * (
    op -_ to fp-neg,
    op _+_ to fp-add,
    op _-_ to fp-sub,
    op _*_ to fp-mul,
    op _rem_ to fp-rem,
    op _^_ to fp-exp,
    op abs to fp-abs,
    op min to fp-min,
    op max to fp-max,
    op _<_ to fp-lt,
    op _<=_ to fp-le,
    op _>_ to fp-gt,
    op _>=_ to fp-ge) .
  sort Number .
  subsort Int Float < Number .
endfm

But then you need to make sure you only apply the built-in operations to arguments of the correct sort.

Steven

On Thu, Aug 7, 2025 at 4:53 AM Francisco Jurado <pacopocopico AT tutamail.com> wrote:

¿How to solve conflicts beetwen INT an FLOAT modules when we need a common
supersort?