Copyright | (c) Klaus Luettich, Christian Maeder, Uni Bremen 2002-2006 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe-Inferred |
Abstract Syntax of CASL Basic_specs, Symb_items and Symb_map_items.
Follows Sect. II:2.2 of the CASL Reference Manual.
- data BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]
- data BASIC_ITEMS b s f
- = Sig_items (SIG_ITEMS s f)
- | Free_datatype SortsKind [Annoted DATATYPE_DECL] Range
- | Sort_gen [Annoted (SIG_ITEMS s f)] Range
- | Var_items [VAR_DECL] Range
- | Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range
- | Axiom_items [Annoted (FORMULA f)] Range
- | Ext_BASIC_ITEMS b
- data SortsKind
- data SIG_ITEMS s f
- = Sort_items SortsKind [Annoted (SORT_ITEM f)] Range
- | Op_items [Annoted (OP_ITEM f)] Range
- | Pred_items [Annoted (PRED_ITEM f)] Range
- | Datatype_items SortsKind [Annoted DATATYPE_DECL] Range
- | Ext_SIG_ITEMS s
- data SORT_ITEM f
- data OP_ITEM f
- data OpKind
- data OP_TYPE = Op_type OpKind [SORT] SORT Range
- args_OP_TYPE :: OP_TYPE -> [SORT]
- res_OP_TYPE :: OP_TYPE -> SORT
- data OP_HEAD = Op_head OpKind [VAR_DECL] (Maybe SORT) Range
- data OP_ATTR f
- data PRED_ITEM f
- data PRED_TYPE = Pred_type [SORT] Range
- data PRED_HEAD = Pred_head [VAR_DECL] Range
- data DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] Range
- data ALTERNATIVE
- data COMPONENTS
- data VAR_DECL = Var_decl [VAR] SORT Range
- varDeclRange :: VAR_DECL -> [Pos]
- data Junctor
- data Relation
- data Equality
- data FORMULA f
- = Quantification QUANTIFIER [VAR_DECL] (FORMULA f) Range
- | Junction Junctor [FORMULA f] Range
- | Relation (FORMULA f) Relation (FORMULA f) Range
- | Negation (FORMULA f) Range
- | Atom Bool Range
- | Predication PRED_SYMB [TERM f] Range
- | Definedness (TERM f) Range
- | Equation (TERM f) Equality (TERM f) Range
- | Membership (TERM f) SORT Range
- | Mixfix_formula (TERM f)
- | Unparsed_formula String Range
- | Sort_gen_ax [Constraint] Bool
- | QuantOp OP_NAME OP_TYPE (FORMULA f)
- | QuantPred PRED_NAME PRED_TYPE (FORMULA f)
- | ExtFORMULA f
- mkSort_gen_ax :: [Constraint] -> Bool -> FORMULA f
- is_True_atom :: FORMULA f -> Bool
- is_False_atom :: FORMULA f -> Bool
- boolForm :: Bool -> FORMULA f
- trueForm :: FORMULA f
- falseForm :: FORMULA f
- data Constraint = Constraint {}
- sortConstraints :: [Constraint] -> [Constraint]
- isInjectiveList :: Ord a => [a] -> Bool
- recover_Sort_gen_ax :: [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
- recoverSortGen :: [Constraint] -> [(SORT, [OP_SYMB])]
- recover_free_Sort_gen_ax :: [Constraint] -> Maybe [(SORT, [OP_SYMB])]
- isSortGen :: FORMULA f -> Bool
- data QUANTIFIER
- data PRED_SYMB
- predSymbName :: PRED_SYMB -> PRED_NAME
- data TERM f
- = Qual_var VAR SORT Range
- | Application OP_SYMB [TERM f] Range
- | Sorted_term (TERM f) SORT Range
- | Cast (TERM f) SORT Range
- | Conditional (TERM f) (FORMULA f) (TERM f) Range
- | Unparsed_term String Range
- | Mixfix_qual_pred PRED_SYMB
- | Mixfix_term [TERM f]
- | Mixfix_token Token
- | Mixfix_sorted_term SORT Range
- | Mixfix_cast SORT Range
- | Mixfix_parenthesized [TERM f] Range
- | Mixfix_bracketed [TERM f] Range
- | Mixfix_braced [TERM f] Range
- | ExtTERM f
- varOrConst :: Token -> TERM f
- data OP_SYMB
- opSymbName :: OP_SYMB -> OP_NAME
- mkForallRange :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
- mkForall :: [VAR_DECL] -> FORMULA f -> FORMULA f
- mkExist :: [VAR_DECL] -> FORMULA f -> FORMULA f
- toQualVar :: VAR_DECL -> TERM f
- mkRel :: Relation -> FORMULA f -> FORMULA f -> FORMULA f
- mkImpl :: FORMULA f -> FORMULA f -> FORMULA f
- mkAnyEq :: Equality -> TERM f -> TERM f -> FORMULA f
- mkExEq :: TERM f -> TERM f -> FORMULA f
- mkStEq :: TERM f -> TERM f -> FORMULA f
- mkEqv :: FORMULA f -> FORMULA f -> FORMULA f
- mkAppl :: OP_SYMB -> [TERM f] -> TERM f
- mkPredication :: PRED_SYMB -> [TERM f] -> FORMULA f
- mkVarDecl :: VAR -> SORT -> VAR_DECL
- mkVarTerm :: VAR -> SORT -> TERM f
- conjunctRange :: [FORMULA f] -> Range -> FORMULA f
- conjunct :: [FORMULA f] -> FORMULA f
- disjunctRange :: [FORMULA f] -> Range -> FORMULA f
- disjunct :: [FORMULA f] -> FORMULA f
- mkQualOp :: OP_NAME -> OP_TYPE -> OP_SYMB
- mkQualPred :: PRED_NAME -> PRED_TYPE -> PRED_SYMB
- negateForm :: FORMULA f -> Range -> FORMULA f
- mkNeg :: FORMULA f -> FORMULA f
- mkVarDeclStr :: String -> SORT -> VAR_DECL
- type CASLFORMULA = FORMULA ()
- type CASLTERM = TERM ()
- type OP_NAME = Id
- type PRED_NAME = Id
- type SORT = Id
- type VAR = Token
- data SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] Range
- data SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] Range
- data SYMB_KIND
- data SYMB
- data TYPE
- data SYMB_OR_MAP
Documentation
data BASIC_SPEC b s f
Basic_spec [Annoted (BASIC_ITEMS b s f)] |
data BASIC_ITEMS b s f
Sig_items (SIG_ITEMS s f) | |
Free_datatype SortsKind [Annoted DATATYPE_DECL] Range | |
Sort_gen [Annoted (SIG_ITEMS s f)] Range | |
Var_items [VAR_DECL] Range | |
Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range | |
Axiom_items [Annoted (FORMULA f)] Range | |
Ext_BASIC_ITEMS b |
Typeable (* -> * -> * -> *) BASIC_ITEMS | |
(Data b, Data s, Data f) => Data (BASIC_ITEMS b s f) | |
(Show b, Show s, Show f) => Show (BASIC_ITEMS b s f) | |
(ShATermConvertible b, ShATermConvertible s, ShATermConvertible f) => ShATermConvertible (BASIC_ITEMS b s f) | |
(GetRange b, GetRange s, GetRange f) => GetRange (BASIC_ITEMS b s f) | |
(Pretty b, Pretty s, FormExtension f) => Pretty (BASIC_ITEMS b s f) | |
ATermConvertibleSML (BASIC_ITEMS a b c) |
data SortsKind
data SIG_ITEMS s f
Sort_items SortsKind [Annoted (SORT_ITEM f)] Range | |
Op_items [Annoted (OP_ITEM f)] Range | |
Pred_items [Annoted (PRED_ITEM f)] Range | |
Datatype_items SortsKind [Annoted DATATYPE_DECL] Range | |
Ext_SIG_ITEMS s |
(Data s, Data f) => Data (SIG_ITEMS s f) | |
(Show s, Show f) => Show (SIG_ITEMS s f) | |
(ShATermConvertible s, ShATermConvertible f) => ShATermConvertible (SIG_ITEMS s f) | |
(GetRange s, GetRange f) => GetRange (SIG_ITEMS s f) | |
(Pretty s, FormExtension f) => Pretty (SIG_ITEMS s f) | |
ATermConvertibleSML (SIG_ITEMS a b) | |
Typeable (* -> * -> *) SIG_ITEMS |
data SORT_ITEM f
data OP_ITEM f
data OpKind
data OP_TYPE
args_OP_TYPE :: OP_TYPE -> [SORT]
res_OP_TYPE :: OP_TYPE -> SORT
data OP_HEAD
data OP_ATTR f
data PRED_ITEM f
data PRED_TYPE
data PRED_HEAD
data DATATYPE_DECL
data ALTERNATIVE
data COMPONENTS
data VAR_DECL
varDeclRange :: VAR_DECL -> [Pos]
data Junctor
data Relation
data Equality
data FORMULA f
Quantification QUANTIFIER [VAR_DECL] (FORMULA f) Range | |
Junction Junctor [FORMULA f] Range | |
Relation (FORMULA f) Relation (FORMULA f) Range | |
Negation (FORMULA f) Range | |
Atom Bool Range | |
Predication PRED_SYMB [TERM f] Range | |
Definedness (TERM f) Range | |
Equation (TERM f) Equality (TERM f) Range | |
Membership (TERM f) SORT Range | |
Mixfix_formula (TERM f) | |
Unparsed_formula String Range | |
Sort_gen_ax [Constraint] Bool | |
QuantOp OP_NAME OP_TYPE (FORMULA f) | |
QuantPred PRED_NAME PRED_TYPE (FORMULA f) | |
ExtFORMULA f |
mkSort_gen_ax :: [Constraint] -> Bool -> FORMULA f
is_True_atom :: FORMULA f -> Bool
is_False_atom :: FORMULA f -> Bool
data Constraint
sortConstraints :: [Constraint] -> [Constraint]
isInjectiveList :: Ord a => [a] -> Bool
no duplicate sorts, i.e. injective sort map?
recover_Sort_gen_ax :: [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
from a Sort_gex_ax, recover: a traditional sort generation constraint plus a sort mapping
recoverSortGen :: [Constraint] -> [(SORT, [OP_SYMB])]
from a Sort_gen_ax, recover: the sorts, each paired with the constructors
recover_free_Sort_gen_ax :: [Constraint] -> Maybe [(SORT, [OP_SYMB])]
from a free Sort_gen_ax, recover: the sorts, each paired with the constructors fails (i.e. delivers Nothing) if the sort map is not injective
data QUANTIFIER
data PRED_SYMB
predSymbName :: PRED_SYMB -> PRED_NAME
data TERM f
Qual_var VAR SORT Range | |
Application OP_SYMB [TERM f] Range | |
Sorted_term (TERM f) SORT Range | |
Cast (TERM f) SORT Range | |
Conditional (TERM f) (FORMULA f) (TERM f) Range | |
Unparsed_term String Range | |
Mixfix_qual_pred PRED_SYMB | |
Mixfix_term [TERM f] | |
Mixfix_token Token | |
Mixfix_sorted_term SORT Range | |
Mixfix_cast SORT Range | |
Mixfix_parenthesized [TERM f] Range | |
Mixfix_bracketed [TERM f] Range | |
Mixfix_braced [TERM f] Range | |
ExtTERM f |
Eq f => Eq (TERM f) | |
Data f => Data (TERM f) | |
Ord f => Ord (TERM f) | |
Show f => Show (TERM f) | |
ShATermConvertible f => ShATermConvertible (TERM f) | |
GetRange f => GetRange (TERM f) | |
FormExtension f => Pretty (TERM f) | |
TermExtension f => TermExtension (TERM f) | |
ATermConvertibleSML (TERM a) | |
Typeable (* -> *) TERM |
varOrConst :: Token -> TERM f
state after mixfix- but before overload resolution
data OP_SYMB
opSymbName :: OP_SYMB -> OP_NAME
short cuts for terms and formulas
mkForallRange :: [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
create binding if variables are non-null
mkPredication :: PRED_SYMB -> [TERM f] -> FORMULA f
conjunctRange :: [FORMULA f] -> Range -> FORMULA f
optimized conjunction
disjunctRange :: [FORMULA f] -> Range -> FORMULA f
mkQualPred :: PRED_NAME -> PRED_TYPE -> PRED_SYMB
negateForm :: FORMULA f -> Range -> FORMULA f
mkVarDeclStr :: String -> SORT -> VAR_DECL
type synonyms
type CASLFORMULA = FORMULA ()
data SYMB_ITEMS
data SYMB_MAP_ITEMS
data SYMB_KIND
data SYMB
data TYPE