Copyright	(c) Stef Joosten Christian Maeder DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (import Logic.Logic)
Safe Haskell	None

Adl.Logic_Adl

Contents

Orphan instances

Description

see Stef Joosten: Deriving Functional Specifications from Business Requirements with Ampersand

and https:/lab.cs.ru.nlBusinessRules/Requirements_engineering

Documentation

data Adl Source #

Constructors

Adl

Instances

Instances details

Show Adl Source #
Instance details Defined in Adl.Logic_Adl Methods showsPrec :: Int -> Adl -> ShowS show :: Adl -> String showList :: [Adl] -> ShowS
Language Adl Source #
Instance details Defined in Adl.Logic_Adl Methods language_name :: Adl -> String Source # description :: Adl -> String Source #
Sentences Adl Sen Sign Morphism Symbol Source #
Instance details Defined in Adl.Logic_Adl Methods map_sen :: Adl -> Morphism -> Sen -> Result Sen Source # simplify_sen :: Adl -> Sign -> Sen -> Sen Source # negation :: Adl -> Sen -> Maybe Sen Source # print_sign :: Adl -> Sign -> Doc Source # print_named :: Adl -> Named Sen -> Doc Source # sym_of :: Adl -> Sign -> [Set Symbol] Source # mostSymsOf :: Adl -> Sign -> [Symbol] Source # symmap_of :: Adl -> Morphism -> EndoMap Symbol Source # sym_name :: Adl -> Symbol -> Id Source # sym_label :: Adl -> Symbol -> Maybe String Source # fullSymName :: Adl -> Symbol -> String Source # symKind :: Adl -> Symbol -> String Source # symsOfSen :: Adl -> Sign -> Sen -> [Symbol] Source # pair_symbols :: Adl -> Symbol -> Symbol -> Result Symbol Source #
Syntax Adl Context Symbol () () Source #
Instance details Defined in Adl.Logic_Adl Methods parsersAndPrinters :: Adl -> Map String (PrefixMap -> AParser st Context, Context -> Doc) Source # parse_basic_spec :: Adl -> Maybe (PrefixMap -> AParser st Context) Source # parseSingleSymbItem :: Adl -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_items :: Adl -> Maybe (PrefixMap -> AParser st ()) Source # parse_symb_map_items :: Adl -> Maybe (PrefixMap -> AParser st ()) Source # toItem :: Adl -> Context -> Item Source # symb_items_name :: Adl -> () -> [String] Source #
StaticAnalysis Adl Context Sen () () Sign Morphism Symbol RawSymbol Source #
Instance details Defined in Adl.Logic_Adl Methods basic_analysis :: Adl -> Maybe ((Context, Sign, GlobalAnnos) -> Result (Context, ExtSign Sign Symbol, [Named Sen])) Source # sen_analysis :: Adl -> Maybe ((Context, Sign, Sen) -> Result Sen) Source # extBasicAnalysis :: Adl -> IRI -> LibName -> Context -> Sign -> GlobalAnnos -> Result (Context, ExtSign Sign Symbol, [Named Sen]) Source # stat_symb_map_items :: Adl -> Sign -> Maybe Sign -> [()] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Adl -> Sign -> [()] -> Result [RawSymbol] Source # convertTheory :: Adl -> Maybe ((Sign, [Named Sen]) -> Context) Source # ensures_amalgamability :: Adl -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Adl -> Morphism -> [Named Sen] -> Result (Sign, [Named Sen]) Source # signature_colimit :: Adl -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source # qualify :: Adl -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sen]) Source # symbol_to_raw :: Adl -> Symbol -> RawSymbol Source # id_to_raw :: Adl -> Id -> RawSymbol Source # matches :: Adl -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Adl -> Sign Source # add_symb_to_sign :: Adl -> Sign -> Symbol -> Result Sign Source # signature_union :: Adl -> Sign -> Sign -> Result Sign Source # signatureDiff :: Adl -> Sign -> Sign -> Result Sign Source # intersection :: Adl -> Sign -> Sign -> Result Sign Source # final_union :: Adl -> Sign -> Sign -> Result Sign Source # morphism_union :: Adl -> Morphism -> Morphism -> Result Morphism Source # is_subsig :: Adl -> Sign -> Sign -> Bool Source # subsig_inclusion :: Adl -> Sign -> Sign -> Result Morphism Source # generated_sign :: Adl -> Set Symbol -> Sign -> Result Morphism Source # cogenerated_sign :: Adl -> Set Symbol -> Sign -> Result Morphism Source # induced_from_morphism :: Adl -> EndoMap RawSymbol -> Sign -> Result Morphism Source # induced_from_to_morphism :: Adl -> EndoMap RawSymbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source # is_transportable :: Adl -> Morphism -> Bool Source # is_injective :: Adl -> Morphism -> Bool Source # theory_to_taxonomy :: Adl -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sen] -> Result MMiSSOntology Source # corresp2th :: Adl -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sen], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Adl -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Adl -> [IRI] -> (Sign, [Named Sen]) -> Result (Sign, [Named Sen]) Source #
Logic Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree Source #
Instance details Defined in Adl.Logic_Adl Methods parse_basic_sen :: Adl -> Maybe (Context -> AParser st Sen) Source # stability :: Adl -> Stability Source # data_logic :: Adl -> Maybe AnyLogic Source # top_sublogic :: Adl -> () Source # all_sublogics :: Adl -> [()] Source # bottomSublogic :: Adl -> Maybe () Source # sublogicDimensions :: Adl -> [[()]] Source # parseSublogic :: Adl -> String -> Maybe () Source # proj_sublogic_epsilon :: Adl -> () -> Sign -> Morphism Source # provers :: Adl -> [Prover Sign Sen Morphism () ProofTree] Source # default_prover :: Adl -> String Source # cons_checkers :: Adl -> [ConsChecker Sign Sen () Morphism ProofTree] Source # conservativityCheck :: Adl -> [ConservativityChecker Sign Sen Morphism] Source # empty_proof_tree :: Adl -> ProofTree Source # syntaxTable :: Adl -> Sign -> Maybe SyntaxTable Source # omdoc_metatheory :: Adl -> Maybe OMCD Source # export_symToOmdoc :: Adl -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Adl -> NameMap Symbol -> Sen -> Result TCorOMElement Source # export_theoryToOmdoc :: Adl -> SigMap Symbol -> Sign -> [Named Sen] -> Result [TCElement] Source # omdocToSym :: Adl -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Adl -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sen)) Source # addOMadtToTheory :: Adl -> SigMapI Symbol -> (Sign, [Named Sen]) -> [[OmdADT]] -> Result (Sign, [Named Sen]) Source # addOmdocToTheory :: Adl -> SigMapI Symbol -> (Sign, [Named Sen]) -> [TCElement] -> Result (Sign, [Named Sen]) Source # sublogicOfTheo :: Adl -> (Sign, [Sen]) -> () Source #
Comorphism Adl2CASL Adl () Context Sen () () Sign Morphism Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Source #
Instance details Defined in Comorphisms.Adl2CASL Methods sourceLogic :: Adl2CASL -> Adl Source # sourceSublogic :: Adl2CASL -> () Source # sourceSublogicLossy :: Adl2CASL -> () Source # minSourceTheory :: Adl2CASL -> Maybe (LibName, String) Source # targetLogic :: Adl2CASL -> CASL Source # mapSublogic :: Adl2CASL -> () -> Maybe CASL_Sublogics Source # map_theory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # mapMarkedTheory :: Adl2CASL -> (Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA]) Source # map_morphism :: Adl2CASL -> Morphism -> Result CASLMor Source # map_sentence :: Adl2CASL -> Sign -> Sen -> Result CASLFORMULA Source # map_symbol :: Adl2CASL -> Sign -> Symbol -> Set Symbol0 Source # extractModel :: Adl2CASL -> Sign -> ProofTree -> Result (Sign, [Named Sen]) Source # is_model_transportable :: Adl2CASL -> Bool Source # has_model_expansion :: Adl2CASL -> Bool Source # is_weakly_amalgamable :: Adl2CASL -> Bool Source # constituents :: Adl2CASL -> [String] Source # isInclusionComorphism :: Adl2CASL -> Bool Source # rps :: Adl2CASL -> Bool Source # eps :: Adl2CASL -> Bool Source # isGTC :: Adl2CASL -> Bool Source #

type Morphism = DefaultMorphism Sign Source #

Orphan instances

Semigroup Context Source #
Instance details Methods (<>) :: Context -> Context -> Context # sconcat :: NonEmpty Context -> Context stimes :: Integral b => b -> Context -> Context
Monoid Context Source #
Instance details Methods mempty :: Context mappend :: Context -> Context -> Context mconcat :: [Context] -> Context