Copyright	(c) Dominik Dietrich DFKI Bremen 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	dominik.dietrich@dfki.de
Stability	experimental
Portability	portable
Safe Haskell	Safe

CSL.Sign

Description

Types and functions for EnCL logic signatures

Synopsis

data Sign = Sign (Map Token OpType) (Map Token (Maybe APInt)) (Map Token EPDecl)
opIds :: Sign -> Set Id
data OpType = OpType {
- opArity :: Int
}
pretty :: Pretty a => a -> Doc
isLegalSignature :: Sign -> Bool
addToSig :: Sign -> Token -> OpType -> Sign
unite :: Sign -> Sign -> Sign
emptySig :: Sign
isSubSigOf :: Sign -> Sign -> Bool
sigDiff :: Sign -> Sign -> Sign
sigUnion :: Sign -> Sign -> Result Sign
lookupSym :: Sign -> Id -> Bool
optypeFromArity :: Int -> OpType
addEPDefValToSig :: Sign -> Token -> APInt -> Sign
addEPDeclToSig :: Sign -> Token -> EPDomain -> Sign
addEPDomVarDeclToSig :: Sign -> Token -> APInt -> Sign

Documentation

data Sign Source #

Datatype for EnCL Signatures Signatures are just sets of Tokens for the operators

Constructors

Sign (Map Token OpType) (Map Token (Maybe APInt)) (Map Token EPDecl)

Instances

Instances details

Eq Sign Source #
Instance details Defined in CSL.Sign Methods (==) :: Sign -> Sign -> Bool (/=) :: Sign -> Sign -> Bool
Data Sign Source #
Instance details Defined in CSL.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign toConstr :: Sign -> Constr dataTypeOf :: Sign -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sign) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign) gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign
Ord Sign Source #
Instance details Defined in CSL.Sign Methods compare :: Sign -> Sign -> Ordering (<) :: Sign -> Sign -> Bool (<=) :: Sign -> Sign -> Bool (>) :: Sign -> Sign -> Bool (>=) :: Sign -> Sign -> Bool max :: Sign -> Sign -> Sign min :: Sign -> Sign -> Sign
Show Sign Source #
Instance details Defined in CSL.Sign Methods showsPrec :: Int -> Sign -> ShowS show :: Sign -> String showList :: [Sign] -> ShowS
Generic Sign
Instance details Defined in CSL.ATC_CSL Associated Types type Rep Sign :: Type -> Type Methods from :: Sign -> Rep Sign x to :: Rep Sign x -> Sign
FromJSON Sign
Instance details Defined in CSL.ATC_CSL Methods parseJSON :: Value -> Parser Sign parseJSONList :: Value -> Parser [Sign]
ToJSON Sign
Instance details Defined in CSL.ATC_CSL Methods toJSON :: Sign -> Value toEncoding :: Sign -> Encoding toJSONList :: [Sign] -> Value toEncodingList :: [Sign] -> Encoding
ShATermConvertible Sign
Instance details Defined in CSL.ATC_CSL Methods toShATermAux :: ATermTable -> Sign -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Sign] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Sign) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Sign])
Pretty Sign Source #
Instance details Defined in CSL.Sign Methods pretty :: Sign -> Doc Source # pretties :: [Sign] -> Doc Source #
Category Sign Morphism Source #	Instance of Category for CSL logic
Instance details Defined in CSL.Logic_CSL Methods ide :: Sign -> Morphism Source # composeMorphisms :: Morphism -> Morphism -> Result Morphism Source # dom :: Morphism -> Sign Source # cod :: Morphism -> Sign Source # inverse :: Morphism -> Result Morphism Source # isInclusion :: Morphism -> Bool Source # legal_mor :: Morphism -> Result () Source #
Sentences CSL CMD Sign Morphism Symbol Source #	Instance of Sentences for reduce logic
Instance details Defined in CSL.Logic_CSL Methods map_sen :: CSL -> Morphism -> CMD -> Result CMD Source # simplify_sen :: CSL -> Sign -> CMD -> CMD Source # negation :: CSL -> CMD -> Maybe CMD Source # print_sign :: CSL -> Sign -> Doc Source # print_named :: CSL -> Named CMD -> Doc Source # sym_of :: CSL -> Sign -> [Set Symbol] Source # mostSymsOf :: CSL -> Sign -> [Symbol] Source # symmap_of :: CSL -> Morphism -> EndoMap Symbol Source # sym_name :: CSL -> Symbol -> Id Source # sym_label :: CSL -> Symbol -> Maybe String Source # fullSymName :: CSL -> Symbol -> String Source # symKind :: CSL -> Symbol -> String Source # symsOfSen :: CSL -> Sign -> CMD -> [Symbol] Source # pair_symbols :: CSL -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis CSL BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol Source #	Static Analysis for reduce logic
Instance details Defined in CSL.Logic_CSL Methods basic_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, GlobalAnnos) -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD])) Source # sen_analysis :: CSL -> Maybe ((BASIC_SPEC, Sign, CMD) -> Result CMD) Source # extBasicAnalysis :: CSL -> IRI -> LibName -> BASIC_SPEC -> Sign -> GlobalAnnos -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named CMD]) Source # stat_symb_map_items :: CSL -> Sign -> Maybe Sign -> [SYMB_MAP_ITEMS] -> Result (EndoMap Symbol) Source # stat_symb_items :: CSL -> Sign -> [SYMB_ITEMS] -> Result [Symbol] Source # convertTheory :: CSL -> Maybe ((Sign, [Named CMD]) -> BASIC_SPEC) Source # ensures_amalgamability :: CSL -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: CSL -> Morphism -> [Named CMD] -> Result (Sign, [Named CMD]) Source # signature_colimit :: CSL -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: CSL -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named CMD]) Source # symbol_to_raw :: CSL -> Symbol -> Symbol Source # id_to_raw :: CSL -> Id -> Symbol Source # matches :: CSL -> Symbol -> Symbol -> Bool Source # empty_signature :: CSL -> Sign Source # add_symb_to_sign :: CSL -> Sign -> Symbol -> Result Sign Source # signature_union :: CSL -> Sign -> Sign -> Result Sign Source # signatureDiff :: CSL -> Sign -> Sign -> Result Sign Source # intersection :: CSL -> Sign -> Sign -> Result Sign Source # final_union :: CSL -> Sign -> Sign -> Result Sign Source # morphism_union :: CSL -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: CSL -> Sign -> Sign -> Bool Source # subsig_inclusion :: CSL -> Sign -> Sign -> Result Morphism Source # generated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: CSL -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: CSL -> EndoMap Symbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: CSL -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: CSL -> Morphism -> Bool Source # is_injective :: CSL -> Morphism -> Bool Source # theory_to_taxonomy :: CSL -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named CMD] -> Result MMiSSOntology Source # corresp2th :: CSL -> String -> Bool -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named CMD], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: CSL -> Sign -> Sign -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: CSL -> [IRI] -> (Sign, [Named CMD]) -> Result (Sign, [Named CMD]) Source #
Logic CSL () BASIC_SPEC CMD SYMB_ITEMS SYMB_MAP_ITEMS Sign Morphism Symbol Symbol [EXPRESSION] Source #	Instance of Logic for reduce logc
Instance details Defined in CSL.Logic_CSL Methods parse_basic_sen :: CSL -> Maybe (BASIC_SPEC -> AParser st CMD) Source # stability :: CSL -> Stability Source # data_logic :: CSL -> Maybe AnyLogic Source # top_sublogic :: CSL -> () Source # all_sublogics :: CSL -> [()] Source # bottomSublogic :: CSL -> Maybe () Source # sublogicDimensions :: CSL -> [[()]] Source # parseSublogic :: CSL -> String -> Maybe () Source # proj_sublogic_epsilon :: CSL -> () -> Sign -> Morphism Source # provers :: CSL -> [Prover Sign CMD Morphism () [EXPRESSION]] Source # default_prover :: CSL -> String Source # cons_checkers :: CSL -> [ConsChecker Sign CMD () Morphism [EXPRESSION]] Source # conservativityCheck :: CSL -> [ConservativityChecker Sign CMD Morphism] Source # empty_proof_tree :: CSL -> [EXPRESSION] Source # syntaxTable :: CSL -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: CSL -> Maybe OMCD Source # export_symToOmdoc :: CSL -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: CSL -> NameMap Symbol -> CMD -> Result TCorOMElement Source # export_theoryToOmdoc :: CSL -> SigMap Symbol -> Sign -> [Named CMD] -> Result [TCElement] Source # omdocToSym :: CSL -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: CSL -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named CMD)) Source # addOMadtToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [[OmdADT]] -> Result (Sign, [Named CMD]) Source # addOmdocToTheory :: CSL -> SigMapI Symbol -> (Sign, [Named CMD]) -> [TCElement] -> Result (Sign, [Named CMD]) Source # sublogicOfTheo :: CSL -> (Sign, [CMD]) -> () Source #
type Rep Sign
Instance details Defined in CSL.ATC_CSL type Rep Sign = D1 ('MetaData "Sign" "CSL.Sign" "main" 'False) (C1 ('MetaCons "Sign" 'PrefixI 'True) (S1 ('MetaSel ('Just "items") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Token OpType)) :: (S1 ('MetaSel ('Just "epvars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Token (Maybe APInt))) :: S1 ('MetaSel ('Just "epdecls") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Token EPDecl)))))

opIds :: Sign -> Set Id Source #

data OpType Source #

Constructors

OpType
Fields opArity :: Int

Instances

Instances details

Eq OpType Source #
Instance details Defined in CSL.Sign Methods (==) :: OpType -> OpType -> Bool (/=) :: OpType -> OpType -> Bool
Data OpType Source #
Instance details Defined in CSL.Sign Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpType -> c OpType gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpType toConstr :: OpType -> Constr dataTypeOf :: OpType -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c OpType) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpType) gmapT :: (forall b. Data b => b -> b) -> OpType -> OpType gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpType -> r gmapQ :: (forall d. Data d => d -> u) -> OpType -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> OpType -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpType -> m OpType gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpType -> m OpType gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpType -> m OpType
Ord OpType Source #
Instance details Defined in CSL.Sign Methods compare :: OpType -> OpType -> Ordering (<) :: OpType -> OpType -> Bool (<=) :: OpType -> OpType -> Bool (>) :: OpType -> OpType -> Bool (>=) :: OpType -> OpType -> Bool max :: OpType -> OpType -> OpType min :: OpType -> OpType -> OpType
Show OpType Source #
Instance details Defined in CSL.Sign Methods showsPrec :: Int -> OpType -> ShowS show :: OpType -> String showList :: [OpType] -> ShowS
Generic OpType
Instance details Defined in CSL.ATC_CSL Associated Types type Rep OpType :: Type -> Type Methods from :: OpType -> Rep OpType x to :: Rep OpType x -> OpType
FromJSON OpType
Instance details Defined in CSL.ATC_CSL Methods parseJSON :: Value -> Parser OpType parseJSONList :: Value -> Parser [OpType]
ToJSON OpType
Instance details Defined in CSL.ATC_CSL Methods toJSON :: OpType -> Value toEncoding :: OpType -> Encoding toJSONList :: [OpType] -> Value toEncodingList :: [OpType] -> Encoding
ShATermConvertible OpType
Instance details Defined in CSL.ATC_CSL Methods toShATermAux :: ATermTable -> OpType -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [OpType] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, OpType) fromShATermList' :: Int -> ATermTable -> (ATermTable, [OpType])
type Rep OpType
Instance details Defined in CSL.ATC_CSL type Rep OpType = D1 ('MetaData "OpType" "CSL.Sign" "main" 'False) (C1 ('MetaCons "OpType" 'PrefixI 'True) (S1 ('MetaSel ('Just "opArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))

pretty :: Pretty a => a -> Doc Source #

isLegalSignature :: Sign -> Bool Source #

determines whether a signature is valid. all sets are ok, so glued to true

addToSig :: Sign -> Token -> OpType -> Sign Source #

Basic function to extend a given signature by adding an item (id) to it

unite :: Sign -> Sign -> Sign Source #

Union of signatures

emptySig :: Sign Source #

The empty signature, use this one to create new signatures

isSubSigOf :: Sign -> Sign -> Bool Source #

Determines if sig1 is subsignature of sig2

sigDiff :: Sign -> Sign -> Sign Source #

difference of Signatures

sigUnion :: Sign -> Sign -> Result Sign Source #

union of Signatures or do I have to care about more things here?

lookupSym :: Sign -> Id -> Bool Source #

checks whether a Id is declared in the signature

optypeFromArity :: Int -> OpType Source #

addEPDefValToSig :: Sign -> Token -> APInt -> Sign Source #

addEPDeclToSig :: Sign -> Token -> EPDomain -> Sign Source #

Adds an extended parameter declaration for a given domain and eventually implicitly defined EP domain vars, e.g., for 'I = [0, n]' n is implicitly added

addEPDomVarDeclToSig :: Sign -> Token -> APInt -> Sign Source #