Maude-help mailing list

[Konrad Hinsen <konrad.hinsen AT fastmail.net>]

Hi everyone,

I am trying to describe physical units in Maude, which worked very
well until I tried to handle multiple unit systems. My approach is to
turn my UNITS module into a parametrized module, and pass in the unit
system as a parameter. But that requires me to provide a view from
TRIV to a sort defined in a module parameter, which I can't figure out
how to do.

Perhaps this is clearer with some code. I have a theory defining a
unit system:

  fth BASE-UNITS is
      sort BaseUnit .
  endfth

and several modules compatible with that theory, e.g.

  fmod SI-BASE-UNITS is
      sort BaseUnit .
      ops m kg s A K cd mol : -> BaseUnit .
  endfm

Next, I have a module that handles unit composition:

  fmod UNITS{B :: BASE-UNITS} is

      protecting ARRAY{!!!, Int0} *
                 (sort Array{!!!, Int0} to UnitPowers) .
      sort Unit CompositeUnit .
      subsorts B$BaseUnit CompositeUnit < Unit .

     ...
  endfm

My question is what to put in place of the three exclamation marks.
It must be a view from TRIV to whatever B stands for, mapping Elt
to B$BaseUnits. But views must be defined outside of the module,
so I can't make a view referring to B.

Note that in this code BASE-UNITS is no different from TRIV in
defining nothing but a sort, and therefore I could probably
find a workaround eliminating BASE-UNITS altogether. But I expect
BASE-UNITS to become more elaborate as I add features to my system,
so I'd prefer to keep it.

Konrad.