4.1 Casfix

Casfix ATerms are term-like structures used to represent the output parse trees of CASL specifications. Casfix format³, is generated by the available CASL parsers, like the parser ⁴. developed in Bremen [MKKB97], For instance, given the CASL specification given in Section 3.1, we obtain the following Casfix:

spec-defn( SIMPLE-ID(WORDS("Module")),
           genericity(params(SPEC*([])),
                      imports(SPEC*([]))),
           BASIC-SPEC (
            basic-spec(
             BASIC-ITEMS*(
               SIG-ITEMS(sort-items(SORT-ITEM+( 
                 [sort-decl(SORT+(
                   [...
                    TOKEN-ID(TOKEN(WORDS("si") ) )
                    ...]))
                  ]))),

               SIG-ITEMS(
                op-items(OP-ITEM+( 
                 [...
                  op-decl(
                     OP-NAME+([ID(TOKEN-ID(TOKEN(WORDS("fk"))))]),
                     total-op-type (
                        sorts(SORT*(
                                [... 
                                 TOKEN-ID(TOKEN(WORDS("sk,1"))) 
                                 ...])),
                        TOKEN-ID(TOKEN(WORDS("sk,ar(fk)")))
                        ),
                     OP-ATTR*([]))
                  ...]))),


             local-var-axioms(
                VAR-DECL+(
                          [...
                           var-decl(VAR+([SIMPLE-ID(WORDS("vj"))]), 
                                    TOKEN-ID(TOKEN(WORDS("svj")))) 
                           ...]),

                FORMULA+(
                         [...
                          parseCaslEq(lo :  slo = ro if go = do) 
                          ...]) 
                 )
             ) 
            ) 
           )
          )

Here, we do not detail the parse trees of CASL (conditional) axioms. The function parseCaslEq is already implemented for terms with prefix/mixfix operators in the Bremen parser.