Copyright	(c) Christian Maeder DFKI GmbH 2011
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

Fpl.Sign

Description

signature extension for FPL to keep track of constructors

Documentation

boolSort :: Id Source #

trueC :: Id Source #

falseC :: Id Source #

boolType :: OpType Source #

data SignExt Source #

Constructors

SignExt
Fields constr :: OpMap

Instances

Instances details

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

emptyFplSign :: SignExt Source #

diffFplSign :: SignExt -> SignExt -> SignExt Source #

addFplSign :: SignExt -> SignExt -> SignExt Source #

interFplSign :: SignExt -> SignExt -> SignExt Source #

isSubFplSign :: SignExt -> SignExt -> Bool Source #

type FplSign = Sign TermExt SignExt Source #

addBools :: OpMap -> OpMap Source #

addConsts :: SignExt -> SignExt Source #

addBuiltins :: FplSign -> FplSign Source #

delBuiltins :: FplSign -> FplSign Source #