CASL.Sign

Description

Synopsis

• data OpType = OpType {
  • opKind :: OpKind
  • opArgs :: [SORT]
  • opRes :: SORT
  }
• opSorts :: OpType -> [SORT]
• mkTotOpType :: [SORT] -> SORT -> OpType
• sortToOpType :: SORT -> OpType
• isSingleArgOp :: OpType -> Bool
• data PredType = PredType {
  • predArgs :: [SORT]
  }
• sortToPredType :: SORT -> PredType
• isBinPredType :: PredType -> Bool
• type OpMap = MapSet OP_NAME OpType
• type PredMap = MapSet PRED_NAME PredType
• type AnnoMap = MapSet Symbol Annotation
• data SymbType
  • = SortAsItemType
  • | SubsortAsItemType SORT
  • | OpAsItemType OpType
  • | PredAsItemType PredType
• symbolKind :: SymbType -> SYMB_KIND
• data Symbol = Symbol {
  • symName :: Id
  • symbType :: SymbType
  }
• idToSortSymbol :: Id -> Symbol
• idToOpSymbol :: Id -> OpType -> Symbol
• idToPredSymbol :: Id -> PredType -> Symbol
• type CASLSign = Sign () ()
• data Sign f e = Sign {
  • sortRel :: Rel SORT
  • revSortRel :: Maybe (Rel SORT)
  • emptySortSet :: Set SORT
  • opMap :: OpMap
  • assocOps :: OpMap
  • predMap :: PredMap
  • varMap :: Map SIMPLE_ID SORT
  • sentences :: [Named (FORMULA f)]
  • declaredSymbols :: Set Symbol
  • envDiags :: [Diagnosis]
  • annoMap :: AnnoMap
  • globAnnos :: GlobalAnnos
  • extendedInfo :: e
  }
• sortSet :: Sign f e -> Set SORT
• emptySign :: e -> Sign f e
• embedSign :: e -> Sign f1 e1 -> Sign f e
• mapForm :: f -> FORMULA f1 -> FORMULA f
• mapFORMULA :: FORMULA f1 -> FORMULA f
• embedTheory :: (FORMULA f1 -> FORMULA f) -> e -> (Sign f1 e1, [Named (FORMULA f1)]) -> (Sign f e, [Named (FORMULA f)])
• embedCASLTheory :: e -> (Sign f1 e1, [Named (FORMULA f1)]) -> (Sign f e, [Named (FORMULA f)])
• getSyntaxTable :: Sign f e -> (PrecMap, AssocMap)
• class SignExtension e where
  • isSubSignExtension :: e -> e -> Bool
• subsortsOf :: SORT -> Sign f e -> Set SORT
• setRevSortRel :: Sign f e -> Sign f e
• supersortsOf :: SORT -> Sign f e -> Set SORT
• toOP_TYPE :: OpType -> OP_TYPE
• toPRED_TYPE :: PredType -> PRED_TYPE
• toOpType :: OP_TYPE -> OpType
• toPredType :: PRED_TYPE -> PredType
• eqAndSubsorts :: Bool -> Rel SORT -> ([[SORT]], [(SORT, [SORT])])
• singleAndRelatedSorts :: Rel SORT -> ([SORT], [[SORT]])
• printSign :: (e -> Doc) -> Sign f e -> Doc
• closeSortRel :: Sign f e -> Sign f e
• nonEmptySortSet :: Sign f e -> Set Id
• setOpKind :: OpKind -> OpType -> OpType
• mkPartial :: OpType -> OpType
• mkTotal :: OpType -> OpType
• isTotal :: OpType -> Bool
• isPartial :: OpType -> Bool
• makePartial :: Set OpType -> Set OpType
• rmOrAddParts :: Bool -> Set OpType -> Set OpType
• rmOrAddPartsMap :: Bool -> OpMap -> OpMap
• diffMapSet :: PredMap -> PredMap -> PredMap
• diffOpMapSet :: OpMap -> OpMap -> OpMap
• diffSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
• addOpMapSet :: OpMap -> OpMap -> OpMap
• addMapSet :: PredMap -> PredMap -> PredMap
• addSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
• uniteCASLSign :: CASLSign -> CASLSign -> CASLSign
• interRel :: Ord a => Rel a -> Rel a -> Rel a
• interOpMapSet :: OpMap -> OpMap -> OpMap
• interMapSet :: PredMap -> PredMap -> PredMap
• interSig :: (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
• isSubOpMap :: OpMap -> OpMap -> Bool
• isSubMap :: PredMap -> PredMap -> Bool
• isSubSig :: (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
• mapSetToList :: MapSet a b -> [(a, b)]
• addDiags :: [Diagnosis] -> State (Sign f e) ()
• addAnnoSet :: Annoted a -> Symbol -> State (Sign f e) ()
• addSymbol :: Symbol -> State (Sign f e) ()
• addSymbToDeclSymbs :: Sign e f -> Symbol -> Sign e f
• addSort :: SortsKind -> Annoted a -> SORT -> State (Sign f e) ()
• hasSort :: Sign f e -> SORT -> [Diagnosis]
• checkSorts :: [SORT] -> State (Sign f e) ()
• addSubsort :: SORT -> SORT -> State (Sign f e) ()
• addSubsortOrIso :: Bool -> SORT -> SORT -> State (Sign f e) ()
• closeSubsortRel :: State (Sign f e) ()
• checkNamePrefix :: Id -> [Diagnosis]
• alsoWarning :: String -> String -> Id -> [Diagnosis]
• checkWithMap :: String -> String -> Map Id a -> Id -> [Diagnosis]
• checkWithOtherMap :: String -> String -> MapSet Id a -> Id -> [Diagnosis]
• addVars :: VAR_DECL -> State (Sign f e) ()
• addVar :: SORT -> SIMPLE_ID -> State (Sign f e) ()
• addOpTo :: Id -> OpType -> OpMap -> OpMap
• type VarSet = Set (VAR, SORT)
• class TermExtension f where
  • freeVarsOfExt :: Sign f e -> f -> VarSet
  • optTermSort :: f -> Maybe SORT
  • sortOfTerm :: f -> SORT
  • termToFormula :: TERM f -> Result (FORMULA f)
• optSortOfTerm :: (f -> Maybe SORT) -> TERM f -> Maybe SORT
• mkAxName :: String -> SORT -> SORT -> String
• mkAxNameSingle :: String -> SORT -> String
• mkSortGenName :: [SORT] -> String
• toSortGenNamed :: FORMULA f -> [SORT] -> Named (FORMULA f)
• getConstructors :: [Named (FORMULA f)] -> Set (Id, OpType)
• addSymbToSign :: Sign e f -> Symbol -> Result (Sign e f)

Documentation