Maude-help mailing list

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

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