Maude-help mailing list

[Guodong Li <ligd AT cs.utah.edu>]

This problem has been solved. Basically it is sort problem. 

Thanks,
Guodong 

On Wed, 25 Jun 2008, Guodong Li wrote:

> Dear Maude Developers:
>   I encountered a problem when attepting to build a interface to access 
> the native C++ functions in the Maude source. Basically my goal is to 
> build terms on the fly and call the reduce and rewrite functions to 
> simplify these terms and then read back the results. Note that I do not 
> use the Maude interative environment at all.
>   In order to build a term I first need to locate the symbol of the 
> operator $op$ in the symbol tables constructed by the parser. 
> If $op$ is monomorphic, then this task is easy. However, consider the 
> following simple example:
>   the input expression is: 2 + e + 5, where e is an expression of sort 
> $expr$, and by definition nat is a subsort of $expr$, i.e. $expr$ 
> subsorts nat < $expr$. To build a term for this expression I find the 
> symbol (say $symbol_1$) for these two $+$s. $symbol_1$ is associated with 
> sorts like $expr$ $expr$.
>   The problem is that this expression won't be reduced (in my 
> implementation) to 7 + e because the equations in the INT module are not 
> applied: the equations attached to 
> $symbol_1$ do not contain the INT equations.  
>   My question is how to make a term for expression 2:expr + e:expr + 
> 5:expr which can be reduced to 7 + e. More specifically, how to look up 
> the symbols for the first and second plus operator? Or, is there another 
> way to get around it?
> 
> Thanks,
> Guodong
>