Maude-help mailing list

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

Now I think of it, Maude's immediate predecessor, OBJ3 had the notional 
of principal sorts, and the ability to guess views. I imagine something 
similar could be done in Maude by taking the largest user sort in a 
target module as principal.

Steven

On 12/2/14, 1:56 PM, Steven Eker wrote:
> Core Maude doesn't support parameterized views, though in principle 
> it's not a difficult feature to add. I believe Full Maude does, so 
> there is a worked out design. On-the-fly views would certainly be 
> doable but there are no plans to add them.
>
> Steven
>
> On 11/26/14, 3:25 AM, Konrad Hinsen wrote:
> > 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.
> > _______________________________________________
> > Maude-help mailing list
> > Maude-help AT cs.uiuc.edu
> > http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help