Maude-help mailing list

[Martin Neuhaeusser <martin AT weh.RWTH-Aachen.de>]

Dear Sir or Madam,

we are working on a term rewriting based implementation of a semantic 
analysis tool for the "Erlang" programming language. Therefore we use
the intermediate code generated by the Erlang compiler ("Core-Erlang").

We use Maude to execute the term-rewrite system. The intermediate code
is input to the system using the LOOP-MODE and META-LEVEL modules of 
core maude. 

In order to parse core erlang modules, we specified the syntax as a maude
module and parse the intermediate code on the metalevel. To map the syntax
of the intermediate language to a maude module, we need to overload some 
operators whose sorts in the arities are pairwise in the same connected
components but whose co-arity sorts are in different CCs.
As is stated in the Maude Manual (version 2.1, p. 37), such an operator
overloading is not allowed in Maude. 

The first obvious solution would be to introduce a common supersort 
of the different co-arity sorts, thereby putting them into one connected
component. But this approach does not work out. First, the operators
need to have different attributes. Secondly, the additional supersort
would be highly artificial as the corresponding terms are not related
in any way.
Neither is it possible to split the connected components of the arities
such that the sorts in the arities fall into different CCs: 
The argument sorts are deeply involved in the intermediate code 
grammar. Splitting this component would be very cumbersome.

As we would like to feed the intermediate code directly from the
compiler to the rewrite system, the alternative of explicitly
supplying the sorts of the subterms in question (i.e. by giving
the sort name after the term written in parentheses) is not possible either.

Since we did not see any other possibility, we first ignored the requirement
concerning operator overloading. As it seems, this leads to ambiguities
when calculating the sort (or kind) of terms including these overloaded
operators. 

If you consider the following syntax definition, where the operator
symbol _=_ is (incorrectly) overloaded:

mod SYNTAX is
        sorts Token Fun Att Def Exp .
        subsort Token Fun < Exp .

        op token : -> Token .
        op _/_ : Token Token -> Fun .

        op _=_ : Fun Exp -> Def [format (b b b o)] .
        op _=_ : Token Exp -> Att [format (r r r o)] .

        sort NeDefList .
        subsort Def < NeDefList .
        op _,_ : Def Def -> NeDefList .
endm

The command 
        "red in SYNTAX : token / token = token ." 
yields an ambiguity: The term has sort Def as well as kind Att, 
because the sort Fun lies in the same connected component as 
the sort Token.

If one tries to reduce a comma-separated list of function
definitions (NeDefList), this works out (at least on level 0).
The command
        "red in SYNTAX : token / token = token , token / token = token ."
correctly displays the result term; the sort of the term (NeDefList) is 
correctly calculated.

Doing the same reductions on the meta-level (which is what we need) gives
quiet different results. It seems, as if the command

        "red in META-LEVEL : metaReduce(['SYNTAX], 
                getTerm(
                  metaParse(['SYNTAX], 'token '/ 'token '= 'token, 'Def))) ."

does not detect the sort ambiguity. At least, it displays only 
the first choice [Att]. If one reduces two comma-separated function 
definitions, like

        "red in META-LEVEL : metaReduce(['SYNTAX], 
                getTerm(metaParse(['SYNTAX], 'token '/ 'token '= 'token '`, 
                                  'token '/ 'token '= 'token, 'NeDefList))) ."

there is a warning message displayed stating that Maude could not find
an appropriate operator "_,_". In this case, no further sort calculation
takes place. It seems as if on the meta-level, the nondeterminism introduced
by the ambiguities in the subterms "token / token = token" is not taken 
into account.
This could explain the warning message: If the two subterms had kind Att, the
appropriate operator symbol "_,_ : Att Att ~> SomeSort" would be missing.

As I am new to the Maude system, I would highly appreciate any comments. Do
you think that the aforementioned problems are due to the incorrectly 
overloaded operators? And if so, do you have any idea how to circumvent this?

Again, any ideas are welcome! Thank you in advance. 
 
Sincerely,
Martin Neuhaeusser


-- 
                        \|||/
                        (o o)
            ---------ooO-(_)-Ooo---------

Martin Neuhaeusser           Tel.  : +49 241 9973278
Ruetscher Strasse 165        Mobil : +49 172 8966488
52072 Aachen, Germany        GnuPG : 0x16FDB298
mod SYNTAX is
        sorts Token Fun Att Def Exp .
        subsort Token Fun < Exp .
        
        op token : -> Token .  
        op _/_ : Token Token -> Fun .
        
        op _=_ : Fun Exp -> Def [format (b b b o)] .
        op _=_ : Token Exp -> Att [format (r r r o)] .

        sort NeDefList .
        subsort Def < NeDefList .
        op _,_ : Def Def -> NeDefList .
endm
red in SYNTAX : token / token = token .

red in SYNTAX : token / token = token , token / token = token .

red in META-LEVEL : metaReduce(['SYNTAX], getTerm(metaParse(['SYNTAX], 'token 
'/ 'token '= 'token, 'Def))) .

red in META-LEVEL : metaReduce(['SYNTAX], getTerm(metaParse(['SYNTAX], 'token 
'/ 'token '= 'token '`, 'token '/ 'token '= 'token , 'NeDefList))) .