Logic_CASL.hs revision 4c53fae3e5be041e963bbfeef09f917032fedccb
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly Authors: Klaus L�ttich
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly Here is the place where the class Logic is instantiated for CASL.
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly Also the instances for Syntax an Category.
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly - writing real functions
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reillyimport Common.AnnoState(emptyAnnos)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederimport qualified CASL.Static
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder-- a dummy datatype for the LogicGraph and for identifying the right
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillydata CASL = CASL deriving (Show)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Language CASL -- default definition is okay
fa373bc327620e08861294716b4454be8d25669fChristian Maederinstance Category CASL Sign Morphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder -- ide :: id -> object -> morphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ide CASL sigma = Morphism { msource = sigma,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly mtarget = sigma,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly sort_map = empty,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly fun_map = empty,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly pred_map = empty
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- o :: id -> morphism -> morphism -> Maybe morphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder comp CASL sigma1 _sigma2 = Just sigma1 -- ???
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- dom, cod :: id -> morphism -> object
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder dom CASL _ = emptySign
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder cod CASL _ = emptySign
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- legal_obj :: id -> object -> Bool
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder legal_obj CASL _ = fun_err "legall_obj"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- legal_mor :: id -> morphism -> Bool
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder legal_mor CASL _ = fun_err "legal_mor"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- abstract syntax, parsing (and printing)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maederinstance Syntax CASL BASIC_SPEC
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parse_basic_spec CASL = Just(toParseFun basicSpec emptyAnnos)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly parse_symb_items CASL = Just(toParseFun symbItems ())
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly parse_symb_map_items CASL = Just(toParseFun symbMapItems ())
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- lattices (for sublogics)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederinstance LatticeWithTop CASL.Sublogics.CASL_Sublogics where
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -- meet, join :: l -> l -> l
fa373bc327620e08861294716b4454be8d25669fChristian Maederinstance Sentences CASL Sentence () Sign Morphism Symbol where
fa373bc327620e08861294716b4454be8d25669fChristian Maeder map_sen CASL _morphism s = return s
fa373bc327620e08861294716b4454be8d25669fChristian Maeder parse_sentence CASL _sign str =
fa373bc327620e08861294716b4454be8d25669fChristian Maeder case runParser (aFormula << eof) emptyAnnos "" str of
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Right _ -> return $ Axiom $ Annoted
fa373bc327620e08861294716b4454be8d25669fChristian Maeder (AxiomDecl [] (TrueAtom []) []) [] [] []
fa373bc327620e08861294716b4454be8d25669fChristian Maeder Left err -> fail $ show err
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder provers CASL = []
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder cons_checkers CASL = []
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederinstance StaticAnalysis CASL BASIC_SPEC Sentence ()
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Symbol RawSymbol where
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder basic_analysis CASL = Just CASL.Static.basicAnalysis
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder stat_symb_map_items CASL = CASL.Static.statSymbMapItems
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder stat_symb_items CASL = CASL.Static.statSymbItems
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- ensures_amalgamability :: id
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- -> (Diagram Sign Morphism, Node, Sign, LEdge Morphism, Morphism)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- -> Result (Diagram Sign Morphism)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ensures_amalgamability CASL _ = fail "ensures_amalgamability nyi"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sign_to_basic_spec CASL _sigma _sens = Basic_spec []
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder symbol_to_raw CASL = CASL.Static.symbolToRaw
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder -- add_sign :: id -> Sign -> Sign -> Sign
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder add_sign CASL s1 s2 = s1 {getMap = union (getMap s1) (getMap s2)}
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder empty_signature CASL = emptySign
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder signature_union CASL sigma1 _sigma2 = return sigma1 -- ??? incorrect
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder morphism_union CASL mor1 _mor2 = return mor1 -- ??? incorrect
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder -- final_union :: id -> Sign -> Sign -> Result Sign
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder final_union CASL s1 s2 = return $
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder s1 {getMap = union (getMap s1) (getMap s2)}
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder cogenerated_sign CASL _rsys sigma = return (ide CASL sigma)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder generated_sign CASL _rsys sigma = return (ide CASL sigma)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- generated_sign, cogenerated_sign :: id -> [RawSymbol]
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- -> Sign -> Result Morphism
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder induced_from_morphism CASL _rmap sigma = return (ide CASL sigma)-- ???
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder induced_from_to_morphism CASL _rmap sigmaS _sigmaT =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder return (ide CASL sigmaS) -- ???
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder --induced_from_to_morphism :: id -> EndoMap RawSymbol
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- -> Sign -> Sign -> Result Morphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- extend_morphism :: id -> Sign -> Morphism -> Sign -> Sign
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -- -> Result Morphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder extend_morphism CASL _s m _s1 _s2 = return m
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedercasl_SublocigsTc, sentenceTc, signTc, morphismTc, symbolTc, rawSymbolTc
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedercasl_SublocigsTc = mkTyCon "CASL.Sublogics.CASL_Sublogics"
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillysentenceTc = mkTyCon "CASL.Sign.Sentence"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedersignTc = mkTyCon "CASL.Sign.Sign"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedermorphismTc = mkTyCon "CASL.Sign.Morphism"
648fe1220044aac847acbdfbc4155af5556063ebChristian MaedersymbolTc = mkTyCon "CASL.Sign.Symbol"
648fe1220044aac847acbdfbc4155af5556063ebChristian MaederrawSymbolTc = mkTyCon "CASL.Sign.RawSymbol"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederinstance Typeable CASL.Sublogics.CASL_Sublogics where
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder typeOf _ = mkAppTy casl_SublocigsTc []
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederinstance Typeable Sentence where
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder typeOf _ = mkAppTy sentenceTc []
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederinstance Typeable Sign where
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder typeOf _ = mkAppTy signTc []
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederinstance Typeable Morphism where
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder typeOf _ = mkAppTy morphismTc []
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederinstance Typeable Symbol where
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder typeOf _ = mkAppTy symbolTc []
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Typeable RawSymbol where
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder typeOf _ = mkAppTy rawSymbolTc []
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederinstance Logic CASL CASL.Sublogics.CASL_Sublogics
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Symbol RawSymbol () where
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sublogic_names CASL = CASL.Sublogics.sublogics_name
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder all_sublogics CASL = CASL.Sublogics.sublogics_all
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder is_in_basic_spec CASL = CASL.Sublogics.in_basic_spec
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder is_in_sentence CASL = CASL.Sublogics.in_sentence
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder is_in_symb_items CASL = CASL.Sublogics.in_symb_items
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly is_in_symb_map_items CASL = CASL.Sublogics.in_symb_map_items
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly is_in_sign CASL = CASL.Sublogics.in_sign
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder is_in_morphism CASL = CASL.Sublogics.in_morphism
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder is_in_symbol CASL = CASL.Sublogics.in_symbol
fa373bc327620e08861294716b4454be8d25669fChristian Maeder min_sublogic_basic_spec CASL = CASL.Sublogics.sl_basic_spec
fa373bc327620e08861294716b4454be8d25669fChristian Maeder min_sublogic_sentence CASL = CASL.Sublogics.sl_sentence
fa373bc327620e08861294716b4454be8d25669fChristian Maeder min_sublogic_symb_items CASL = CASL.Sublogics.sl_symb_items
fa373bc327620e08861294716b4454be8d25669fChristian Maeder min_sublogic_symb_map_items CASL = CASL.Sublogics.sl_symb_map_items
fa373bc327620e08861294716b4454be8d25669fChristian Maeder min_sublogic_sign CASL = CASL.Sublogics.sl_sign
fa373bc327620e08861294716b4454be8d25669fChristian Maeder min_sublogic_morphism CASL = CASL.Sublogics.sl_morphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder min_sublogic_symbol CASL = CASL.Sublogics.sl_symbol
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proj_sublogic_basic_spec CASL = CASL.Sublogics.pr_basic_spec
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proj_sublogic_symb_items CASL = CASL.Sublogics.pr_symb_items
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proj_sublogic_symb_map_items CASL = CASL.Sublogics.pr_symb_map_items
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proj_sublogic_sign CASL = CASL.Sublogics.pr_sign
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proj_sublogic_morphism CASL = CASL.Sublogics.pr_morphism
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proj_sublogic_epsilon CASL = CASL.Sublogics.pr_epsilon
fa373bc327620e08861294716b4454be8d25669fChristian Maeder proj_sublogic_symbol CASL = CASL.Sublogics.pr_symbol
fa373bc327620e08861294716b4454be8d25669fChristian Maeder---- helpers ---------------------------------
fa373bc327620e08861294716b4454be8d25669fChristian Maederfun_err :: String -> a
fa373bc327620e08861294716b4454be8d25669fChristian Maederfun_err fname =
fa373bc327620e08861294716b4454be8d25669fChristian Maeder error ("*** Function \"" ++ fname ++ "\" is not yet implemented!")
fa373bc327620e08861294716b4454be8d25669fChristian Maeder----------------------------------------------