Maude-help mailing list

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

Hi everyone,

I have spent another hour in vain trying to figure out how to do
something with Maude, and like in all the other cases, it's related to
views. What I need is a view from TRIV to a parameterized module.
That sounds simple, but I didn't find anything that works.

Background: I want to implement numerical formulas that I can
evaluate using either RAT or FLOAT for the numbers. So I define
a theory VALUE:

    fth VALUE is
        protecting RAT .
        protecting FLOAT .
        sort Value .
        op fromRat : Rat -> Value .
        op fromFloat : Float -> Value .
        op -_ : Value -> Value .
        op _+_ : Value Value -> Value .
        op _-_ : Value Value -> Value .
        op _*_ : Value Value -> Value .
        op _/_ : Value Value -> Value .
        op _^_ : Value Int -> Value .
    endfth

To make RAT compatible with this, I need a minor addition:

    fmod RAT-WITH-ID is
        protecting RAT .
        protecting CONVERSION .
        var X : Rat .
        op id : Rat -> Rat .
        eq id(X) = X .
    endfm

    view RAT from VALUE to RAT-WITH-ID is
        sort Value to Rat .
        op fromRat to id .
        op fromFloat to rat .
    endv

and a similar extension for FLOAT to provide integer powers. Next, I want
to do some geometry:

    fmod VECTOR{V :: VALUE} is
        sort Vector{V} .
        op [_, _, _] : V$Value V$Value V$Value -> Vector{V} .
        op _+_ : Vector{V} Vector{V} -> Vector{V} .
        op _-_ : Vector{V} Vector{V} -> Vector{V} .
        op _*_ : Vector{V} Vector{V} -> V$Value .
        vars x1 y1 z1 x2 y2 z2 : V$Value .
        eq [x1, y1, z1] + [x2, y2, z2] = [(x1 + x2), (y1 + y2), (z1 + z2)] .
        eq [x1, y1, z1] - [x2, y2, z2] = [(x1 - x2), (y1 - y2), (z1 - z2)] .
        eq [x1, y1, z1] * [x2, y2, z2] = ((x1 * x2) + (y1 * y2)) + (z1 * z2) .
    endfm

Up to there, no problem. But next I need a list of vectors. My current
attempt is

    fmod CONFIGURATION{V :: VALUE} is
        protecting VECTOR{V} .
        protecting LIST{VECTOR{V}} * (sort List{Vector{V}} to 
Configuration{V}) .
    endfm

but I can't define a view VECTOR{V}. What's the trick?


More generally, I wonder why Maude requires views to be defined with a
global name. Especially for the frequent views from TRIV, it would be
so much more convenient if views could be defined "on the fly" as
expressions. I find myself often abandoning LIST or ARRAY and defining
my own special-purpose structures instead, just to avoid having to
cut a module in two parts separated by a view definition.

Konrad.