4.2 Efix

We have developed in collaboration with the ASF+SDF group, an ATerm-like format dedicated to ELAN programs. The notion of Efix ATerms is similar to the one developed for CASL with Casfix ATerms. The current tools related to Efix are

• An ELAN parser developed by the ASF+SDF group with the new ASDF2 environment, and the new parser generator. The output of this parser is an Efix ATerm.
• A translator from Efix to REF, called efix2ref that allows us to execute some Efix programs with ELAN. The current prototype handles simple modules with no importation, no labelled rules, and so without any strategy. However, despite all these limitations, this tool is already sufficient, for our purpose, to consider conditional rewrite systems, written in the Efix syntax.

module(simple_formal_module_name("Module"), 
       empty_import, 
       sort_definition([... simple_sort_name("s") ...]),
       operator_definition([global_symbol_decl( 
         [...
          operator_decl(simple_formal_module_name("Module"), 
                        e_name(["f", 
                                "(", 
                                placeholder, 
                                ... , 
                                placeholder,
                                ")" 
                                ]), 
                               sorts_to_sort(
                                     [simple_sort_name("s1"), 
                                      ...,
                                      simple_sort_name("sn")
                                      ], 
                                     simple_sort_name("s")),
                        options(global_option, 
                                pri_option (0), 
                                no_assoc_option,
                                free_matching, 
                                no_built_in)
                        )
          ...]                                 )]), 
       empty_strategy_definition , 
       [...
        rules_family(simple_sort_name("sort(phi)"), 
                     [...
                      variable_declare([simple_variable("v")], 
                                       simple_sort_name("sort(v)"))
                      ...],
        global_rules( 
          [non_labelled_rule(EFIX-rule(phi))]
                     ),
 
        empty_local_rules)
        ...], 
        [])

Subterms with EFIX-rule top symbol denote terms which are not detailed here for sake of conciseness.

Efix is used as an intermediate format between FCasEnv, and REF, the ELAN executable format.