Go backward to 1 Introduction
Go up to Top
Go forward to 3 Mapping from CASL to ELAN
2 ELAN Programs
The required inputs for ELAN are:
- A rewrite program including a signature, a set of rules and a
set of strategies.
- A query term expressed in the signature of the rewrite
program.
The ELAN outputs are the normal forms of the query term, with
respect to the rewrite program.
Note that because the set of rules is not required to be terminating
nor confluent, a query term may have several normal forms, or may not
terminate.
Actually, we may find two different kinds of syntax in the ELAN
system for rewrite programs:
- A user-friendly syntax that allows us to use mixfix notation for
terms in the program. For this syntax, we need a sophisticated
earley-based mixfix parser implemented in the ELAN interpreter.
- A "computer-friendly" syntax, to represent the internal
structure of a rewrite program. This syntax, called REF, is rather
difficult to handle directly since it looks like an encoding of the
program [BJMR98]. It provides a term-like representation
of the ELAN
working memory associated to a rewrite program. In a REF program, we
may find some tables for identifiers, module names, sort names, rule
names and strategy names, some grammar rules for the mixfix parser,
the encoding of rules, strategies, and the query term. A REF
program is usually generated by the ELAN interpreter, and can be
executed both by the interpreter and the compiler.
The idea is to compile CASL equational specifications into REF
programs that are executable in the ELAN system.
CoFI
Note: T-9 -- Version: 1 -- November 10, 2000.
Comments to FirstName.LastName@loria.fr
Go backward to 1 Introduction
Go up to Top
Go forward to 3 Mapping from CASL to ELAN