hets -- a heterogenous Specification (CASL) tool set
Contents
Index
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