CasEnv

CasEnv is a format for the CASL global environment, based on ATerms.

CASENV ::= casenv ( global-entry-tuple* ( GLOBAL-ENTRY-TUPLE* ) )

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

GLOBAL-ENTRY ::= spec-defn-env ( GENERICITY-ENV, SPEC-LENV )
| view-defn-env ( GENERICITY-ENV, SPEC-LENV, MORPHISM,
SPEC-LENV )
| arch-spec-defn-env ( ARCH-SIGNATURE )
| unit-spec-defn-env ( UNIT-SIGNATURE )

SIGNATURE ::= signature ( LOCAL-ENV, anno* ( ANNO* ) )

GENERICITY-ENV ::= genericity-env ( SPEC-LENV, spec-lenv* ( SPEC-LENV* ), SIGNATURE )
(* use:
(list of envs for imports,
list of envs for formal parameters,
signature union of all imports and all formal parameters) *)

SPEC-LENV ::= spec-lenv ( SIGNATURE, SIGNATURE, SPEC-ENV )
(* use: flattened env, flattened hidden env, structured env *)

SPEC-ENV ::= basic-env ( SIGNATURE, formula* ( FORMULA* ) )
| translate-env ( SPEC-ENV, MORPHISM )
| derive-env ( SPEC-ENV, MORPHISM )
| union-env ( spec-env* ( SPEC-ENV* ) )
| extension-env ( spec-env* ( SPEC-ENV* ) )
| free-spec-env ( SPEC-ENV )
| closed-spec-env ( SPEC-ENV )
| spec-inst-env ( SPEC-NAME, SPEC-ENV, MORPHISM,
spec-env* ( SPEC-ENV* ) )
(* use: name of genric spec, env for body, fitting morphism, env for actual args *)
| dummy-spec-env



ARCH-SIGNATURE ::= arch-sig ( NAMED-UNIT-SIGS, UNIT-SIGNATURE )

UNIT-SIGNATURE ::= unit-sig ( COMP-SUB-SIGS, SUB-SIG )

COMP-SUB-SIGS ::= comp-sub-sigs ( sub-sig* ( SUB-SIG* ) )

NAMED-UNIT-SIGS ::= named-unit-sigs ( unit-tag-sig-tuple*
( UNIT-TAG-SIG-TUPLE* ) )

UNIT-TAG-SIG-TUPLE ::= unit-tag-sig-tuple ( SIMPLE_ID, UNIT-TAG-SIG )

UNIT-TAG-SIG ::= unit-tag-sig ( COMP-TAG-SIGS, TAG-SIG )

COMP-TAG-SIGS ::= comp-tag-sigs ( tag-sig* ( TAG-SIG* ) )

TAG-SIG ::= tag-sig ( SUB-SIG, TAGGING-MAP )

TAGGING-MAP ::= tagging-map ( ref-sym-list-tuple* ( REF-SYM-LIST-TUPLE* ) )

REF-SYM-LIST-TUPLE ::= ref-sym-list-tuple ( E-SYMBOL, ref-sym* ( REF-SYM* ) )

E-SYMBOL ::= sym-esymbol ( TSYMBOL )
| emb-esymbol ( SORT, SORT )

TSYMBOL ::= sort-symbol ( SORT )
| total-fun-symbol ( OP-NAME, SORTS-SORT )
| partial-fun-symbol ( OP-NAME, SORTS-SORT )
| pred-symbol ( PRED-NAME, sort* ( SORT ) )

SORTS-SORT ::= sorts-sort ( sort* ( SORT* ), SORT )

REF-SYM ::= ref-sym ( UNIT-NAME, E-SYMBOL )

SUB-SIG ::= sub-sig ( LOCAL-ENV )
Further rules are contained in the common part of CasEnv and FCasEnv.