CASL.AS_Basic_CASL

Contents

• short cuts for terms and formulas
• type synonyms

Description

Synopsis

• 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
  • = NonEmptySorts
  • | PossiblyEmptySorts
• 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
  • = Sort_decl [SORT] Range
  • | Subsort_decl [SORT] SORT Range
  • | Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) Range
  • | Iso_decl [SORT] Range
• data OP_ITEM f
  • = Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] Range
  • | Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) Range
• data OpKind
  • = Total
  • | Partial
• 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
  • = Assoc_op_attr
  • | Comm_op_attr
  • | Idem_op_attr
  • | Unit_op_attr (TERM f)
• data PRED_ITEM f
  • = Pred_decl [PRED_NAME] PRED_TYPE Range
  • | Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) Range
• 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
  • = Alt_construct OpKind OP_NAME [COMPONENTS] Range
  • | Subsorts [SORT] Range
• data COMPONENTS
  • = Cons_select OpKind [OP_NAME] SORT Range
  • | Sort SORT
• data VAR_DECL = Var_decl [VAR] SORT Range
• varDeclRange :: VAR_DECL -> [Pos]
• data Junctor
  • = Con
  • | Dis
• data Relation
  • = Implication
  • | RevImpl
  • | Equivalence
• data Equality
  • = Strong
  • | Existl
• 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 {
  • newSort :: SORT
  • opSymbs :: [(OP_SYMB, [Int])]
  • origSort :: SORT
  }
• 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
  • = Universal
  • | Existential
  • | Unique_existential
• data PRED_SYMB
  • = Pred_name PRED_NAME
  • | Qual_pred_name PRED_NAME PRED_TYPE Range
• 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
  • = Op_name OP_NAME
  • | Qual_op_name OP_NAME OP_TYPE Range
• 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
  • = Implicit
  • | Sorts_kind
  • | Ops_kind
  • | Preds_kind
• data SYMB
  • = Symb_id Id
  • | Qual_id Id TYPE Range
• data TYPE
  • = O_type OP_TYPE
  • | P_type PRED_TYPE
  • | A_type SORT
• data SYMB_OR_MAP
  • = Symb SYMB
  • | Symb_map SYMB SYMB Range

Documentation

short cuts for terms and formulas

type synonyms