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.