Logic_CASL.hs revision 3b4439aa37e4229ad6e83d46bd303c2799784c80
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski{-# OPTIONS -fno-warn-missing-methods #-}
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Authors: Klaus L�ttich
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Here is the place where the class Logic is instantiated for CASL.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Also the instances for Syntax an Category.
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski - writing real functions
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule Logic_CASL where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport AS_Basic_CASL
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Print_AS_Basic
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Parse_AS_Basic
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport SymbolParser
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport ParsecInterface
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport AnnoState(emptyAnnos)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Static
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- a dummy datatype for the LogicGraph and for identifying the right
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskidata CASL = CASL deriving (Show)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Language CASL where -- default definition is okay
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Category CASL Sign Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- ide :: id -> object -> morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ide CASL sigma = Morphism { msource = sigma,
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mtarget = sigma
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- o :: id -> morphism -> morphism -> Maybe morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski comp CASL sigma1 sigma2 = Just sigma1 -- ???
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- dom, cod :: id -> morphism -> object
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski dom CASL _ = emptySign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cod CASL _ = emptySign
4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski -- legal_obj :: id -> object -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski legal_obj CASL _ = fun_err "legall_obj"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- legal_mor :: id -> morphism -> Bool
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski legal_mor CASL _ = fun_err "legal_mor"
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- abstract syntax, parsing (and printing)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Syntax CASL BASIC_SPEC
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski SYMB_ITEMS SYMB_MAP_ITEMS
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_basic_spec CASL = Just(toParseFun basicSpec emptyAnnos)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_symb_items CASL = Just(toParseFun symbItems ())
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski parse_symb_map_items CASL = Just(toParseFun symbMapItems ())
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- lattices (for sublogics)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance LatticeWithTop Sublogics.CASL_Sublogics where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- meet, join :: l -> l -> l
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Sentences CASL Sentence Sign Morphism Symbol where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance StaticAnalysis CASL BASIC_SPEC Sentence
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski SYMB_ITEMS SYMB_MAP_ITEMS
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Symbol RawSymbol where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski basic_analysis CASL = Just Static.basicAnalysis
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski stat_symb_map_items CASL = Static.statSymbMapItems
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski stat_symb_items CASL = Static.statSymbItems
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till Mossakowski -- ensures_amalgamability :: id
5e21bb46b24f477dafad6fdeff51aed7aaad0a47Till Mossakowski -- -> (Diagram Sign Morphism, Node, Sign, LEdge Morphism, Morphism)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- -> Result (Diagram Sign Morphism)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sign_to_basic_spec CASL sigma sens = Basic_spec []
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski symbol_to_raw CASL = Static.symbolToRaw
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski id_to_raw CASL = Static.idToRaw
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski symmap_of CASL = Static.symmapOf
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- add_sign :: id -> Sign -> Sign -> Sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski empty_signature CASL = emptySign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski signature_union CASL sigma1 sigma2 = return sigma1 -- ??? incorrect
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski morphism_union CASL mor1 mor2 = return mor1 -- ??? incorrect
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- final_union :: id -> Sign -> Sign -> Result Sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_subsig CASL = Static.isSubSig
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski cogenerated_sign CASL rsys sigma = return (ide CASL sigma)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski generated_sign CASL rsys sigma = return (ide CASL sigma)
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- generated_sign, cogenerated_sign :: id -> [RawSymbol]
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- -> Sign -> Result Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski induced_from_morphism CASL rmap sigma = return (ide CASL sigma) -- ???
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski induced_from_to_morphism CASL rmap sigmaS sigmaT =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (ide CASL sigmaS) -- ???
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski --induced_from_to_morphism :: id -> EndoMap RawSymbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- -> Sign -> Sign -> Result Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- extend_morphism :: id -> Sign -> Morphism -> Sign -> Sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- -> Result Morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiinstance Logic CASL Sublogics.CASL_Sublogics
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Symbol RawSymbol where
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski sublogic_names CASL = Sublogics.sublogics_name
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski all_sublogics CASL = Sublogics.sublogics_all
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_basic_spec CASL = Sublogics.in_basic_spec
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_sentence CASL = Sublogics.in_sentence
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_symb_items CASL = Sublogics.in_symb_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_symb_map_items CASL = Sublogics.in_symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_sign CASL = Sublogics.in_sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_morphism CASL = Sublogics.in_morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski is_in_symbol CASL = Sublogics.in_symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski min_sublogic_basic_spec CASL = Sublogics.sl_basic_spec
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski min_sublogic_sentence CASL = Sublogics.sl_sentence
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski min_sublogic_symb_items CASL = Sublogics.sl_symb_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski min_sublogic_symb_map_items CASL = Sublogics.sl_symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski min_sublogic_sign CASL = Sublogics.sl_sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski min_sublogic_morphism CASL = Sublogics.sl_morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski min_sublogic_symbol CASL = Sublogics.sl_symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski proj_sublogic_basic_spec CASL = Sublogics.pr_basic_spec
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski proj_sublogic_symb_items CASL = Sublogics.pr_symb_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski proj_sublogic_symb_map_items CASL = Sublogics.pr_symb_map_items
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski proj_sublogic_sign CASL = Sublogics.pr_sign
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski proj_sublogic_morphism CASL = Sublogics.pr_morphism
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski proj_sublogic_epsilon CASL = Sublogics.pr_epsilon
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski proj_sublogic_symbol CASL = Sublogics.pr_symbol
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski---- helpers ---------------------------------
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskifun_err :: String -> a
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskifun_err fname =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski error ("*** Function \"" ++ fname ++ "\" is not yet implemented!")
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski----------------------------------------------