FCasEnv

FCasEnv is a format for the CASL global environment, based on the CasEnv format. It contains, for each specification, a signature plus a set of axioms. Thus, the structure of the specification is not available. This is useful in connection with theorem provers or rewriting engines that can handle only flat specifications.
Within the CASl tool set, you can use the option -env=FCasEnv to generate the FCasEnv format.
The following grammar describes the FCasEnv format:

FCASENV ::= fcasenv ( f-global-entry-tuple* ( F-GLOBAL-ENTRY-TUPLE* )

F-GLOBAL-ENTRY-TUPLE ::= f-global-entry-tuple ( SIMPLE-ID, F-GLOBAL-ENTRY )

F-GLOBAL-ENTRY ::= f-spec-defn-env ( F-GENERICITY-ENV, EXT-SIGNATURE )
| f-view-defn-env ( F-GENERICITY-ENV, EXT-SIGNATURE,
MORPHISM, EXT-SIGNATURE )
| f-arch-spec-defn-env
| f-unit-spec-defn-env

F-GENERICITY-ENV ::= f-genericity-env ( EXT-SIGNATURE, ext-signature*
( EXT-SIGNATURE* ) )

EXT-SIGNATURE ::= ext-signature ( SIGNATURE, SIGNATURE,
formula* ( FORMULA* ) )




Further rules are contained in the common part of CasEnv and FCasEnv.