hets -- a heterogenous Specification (CASL) tool setContentsIndex
CASL.AS_Basic_CASL
Portability portable
Stability provisional
Maintainer hets@tzi.de
Description
This is the Abstract Syntax tree of CASL Basic_specs, Symb_items and Symb_map_items.
Synopsis
data BASIC_SPEC = Basic_spec [Annoted BASIC_ITEMS]
data BASIC_ITEMS
= Sig_items SIG_ITEMS
| Free_datatype [Annoted DATATYPE_DECL] [Pos]
| Sort_gen [Annoted SIG_ITEMS] [Pos]
| Var_items [VAR_DECL] [Pos]
| Local_var_axioms [VAR_DECL] [Annoted FORMULA] [Pos]
| Axiom_items [Annoted FORMULA] [Pos]
data SIG_ITEMS
= Sort_items [Annoted SORT_ITEM] [Pos]
| Op_items [Annoted OP_ITEM] [Pos]
| Pred_items [Annoted PRED_ITEM] [Pos]
| Datatype_items [Annoted DATATYPE_DECL] [Pos]
data SORT_ITEM
= Sort_decl [SORT] [Pos]
| Subsort_decl [SORT] SORT [Pos]
| Subsort_defn SORT VAR SORT (Annoted FORMULA) [Pos]
| Iso_decl [SORT] [Pos]
data OP_ITEM
= Op_decl [OP_NAME] OP_TYPE [OP_ATTR] [Pos]
| Op_defn OP_NAME OP_HEAD (Annoted TERM) [Pos]
data OP_TYPE
= Total_op_type [SORT] SORT [Pos]
| Partial_op_type [SORT] SORT [Pos]
data OP_HEAD
= Total_op_head [ARG_DECL] SORT [Pos]
| Partial_op_head [ARG_DECL] SORT [Pos]
data ARG_DECL = Arg_decl [VAR] SORT [Pos]
data OP_ATTR
= Assoc_op_attr
| Comm_op_attr
| Idem_op_attr
| Unit_op_attr TERM
data PRED_ITEM
= Pred_decl [PRED_NAME] PRED_TYPE [Pos]
| Pred_defn PRED_NAME PRED_HEAD (Annoted FORMULA) [Pos]
data PRED_TYPE = Pred_type [SORT] [Pos]
data PRED_HEAD = Pred_head [ARG_DECL] [Pos]
data DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] [Pos]
data ALTERNATIVE
= Total_construct OP_NAME [COMPONENTS] [Pos]
| Partial_construct OP_NAME [COMPONENTS] [Pos]
| Subsorts [SORT] [Pos]
data COMPONENTS
= Total_select [OP_NAME] SORT [Pos]
| Partial_select [OP_NAME] SORT [Pos]
| Sort SORT
data VAR_DECL = Var_decl [VAR] SORT [Pos]
data FORMULA
= Quantification QUANTIFIER [VAR_DECL] FORMULA [Pos]
| Conjunction [FORMULA] [Pos]
| Disjunction [FORMULA] [Pos]
| Implication FORMULA FORMULA [Pos]
| Equivalence FORMULA FORMULA [Pos]
| Negation FORMULA [Pos]
| True_atom [Pos]
| False_atom [Pos]
| Predication PRED_SYMB [TERM] [Pos]
| Definedness TERM [Pos]
| Existl_equation TERM TERM [Pos]
| Strong_equation TERM TERM [Pos]
| Membership TERM SORT [Pos]
| Mixfix_formula TERM
| Unparsed_formula String [Pos]
data QUANTIFIER
= Universal
| Existential
| Unique_existential
data PRED_SYMB
= Pred_name PRED_NAME
| Qual_pred_name PRED_NAME PRED_TYPE [Pos]
data TERM
= Simple_id SIMPLE_ID
| Qual_var VAR SORT [Pos]
| Application OP_SYMB [TERM] [Pos]
| Sorted_term TERM SORT [Pos]
| Cast TERM SORT [Pos]
| Conditional TERM FORMULA TERM [Pos]
| Unparsed_term String [Pos]
| Mixfix_qual_pred PRED_SYMB
| Mixfix_term [TERM]
| Mixfix_token Token
| Mixfix_sorted_term SORT [Pos]
| Mixfix_cast SORT [Pos]
| Mixfix_parenthesized [TERM] [Pos]
| Mixfix_bracketed [TERM] [Pos]
| Mixfix_braced [TERM] [Pos]
data OP_SYMB
= Op_name OP_NAME
| Qual_op_name OP_NAME OP_TYPE [Pos]
type OP_NAME = Id
type PRED_NAME = Id
type SORT = Id
type VAR = SIMPLE_ID
data SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] [Pos]
data SYMB_ITEMS_LIST = Symb_items_list [SYMB_ITEMS] [Pos]
data SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] [Pos]
data SYMB_MAP_ITEMS_LIST = Symb_map_items_list [SYMB_MAP_ITEMS] [Pos]
data SYMB_KIND
= Implicit
| Sorts_kind
| Ops_kind
| Preds_kind
data SYMB
= Symb_id Id
| Qual_id Id TYPE [Pos]
data TYPE
= O_type OP_TYPE
| P_type PRED_TYPE
| A_type SORT
data SYMB_OR_MAP
= Symb SYMB
| Symb_map SYMB SYMB [Pos]
Produced by Haddock version 0.6