Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

Hi Konrad,

This is a slightly subtle case. What you need here is a view that goes from
a theory to another theory, so as to transform the theory TRIV that 
ARRAY has
for its first parameter into the theory BASE-UNITS, for which you have a 
parameter
from the enclosing module.

There is an example of this in the prelude where SORTABLE-LIST is 
defined using
a theory to theory view, STRICT-TOTAL-ORDER, which maps the parameter of
WEAKLY-SORTABLE-LIST from STRICT-WEAK-ORDER to STRICT-TOTAL-ORDER which
can then be instantiated by parameter from SORTABLE-LIST.

Note that all this instantiating makes for some very complex sort names!

So I would write your example as

fth BASE-UNITS is
  sort BaseUnit .
endfth

view BASE-UNITS from TRIV to BASE-UNITS is
  sort Elt to BaseUnit .
endv

fmod UNITS{B :: BASE-UNITS} is

  protecting ARRAY{BASE-UNITS, Int0}{B} *
    (sort Array{BASE-UNITS,Int0}{B} to UnitPowers) .

  sort Unit CompositeUnit .
    subsorts B$BaseUnit CompositeUnit < Unit .

endfm

Note that there is no requirement to name the theory-to-theory view 
after the
target theory - you could call it something else - it is merely a 
convention.

Instantiating ARRAY with the views BASE-UNITS and Int0, giving the module
expression ARRAY{BASE-UNITS, Int0} yields a module with one free parameter
of theory BASE-UNITS that must be instantiated before the module can be 
imported.
Thus the module expression ARRAY{BASE-UNITS, Int0}{B} instantiates this 
module
with the parameter B from UNITS.
The fully instantiated module ends up with parametrized sorts having the 
rather
complex {BASE-UNITS,Int0}{B} instantiation.

Youe can then instantiate the module UNITS thus:

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

view SI-BASE-UNITS from BASE-UNITS to SI-BASE-UNITS is
  *** if SI-BASE-UNITS used a different sort name you would map it here
endv

fmod TEST is
  protecting UNITS{SI-BASE-UNITS} .
endfm

Steven

On 9/5/14 8:03 AM, Konrad Hinsen wrote:
> 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.
>
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help