Logic.hs revision 8ddc7a5666b6887cf3a2c7c29e4691e04373545f
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster{-# OPTIONS -fallow-undecidable-instances #-}
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterModule : $Header$
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2003
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterMaintainer : till@tzi.de
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterStability : provisional
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterPortability : non-portable (various -fglasgow-exts extensions)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Provides data structures for logics (with symbols). Logics are
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster a type class with an "identitiy" type (usually interpreted
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster by a singleton set) which serves to treat logics as
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster data. All the functions in the type class take the
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster identity as first argument in order to determine the logic.
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster For logic (co)morphisms see Comorphism.hs
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster J. A. Goguen and R. M. Burstall
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Institutions: Abstract Model Theory for Specification and
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster JACM 39, p. 95--146, 1992
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (general notion of logic - model theory only)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster General Logics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Logic Colloquium 87, p. 275--329, North Holland, 1989
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (general notion of logic - also proof theory;
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster notion of logic representation, called map there)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster T. Mossakowski:
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Specification in an arbitrary institution with symbols
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster 14th WADT 1999, LNCS 1827, p. 252--270
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (treatment of symbols and raw symbols, see also CASL semantics)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster T. Mossakowski, B. Klin:
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Institution Independent Static Analysis for CASL
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (what is needed for static anaylsis)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster S. Autexier and T. Mossakowski
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna Integrating HOLCASL into the Development Graph Manager MAYA
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna FroCoS 2002, to appear
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna (interface to provers)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Weak amalgamability
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster raw symbols are now symbols, symbols are now signature symbols
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster provide both signature symbol set and symbol set of a signature
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Logic.Prover -- for one half of class Sentences
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- for coercion used in Grothendieck.hs and Analysis modules
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport UnsafeCoerce
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- for Conversion to ATerms
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Common.ATerm.Lib -- (ATermConvertible)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- for HetcatsOpts passed to ensures_amalgamability
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport Options
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- diagrams are just graphs
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fostertype Diagram object morphism = Graph object morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | Amalgamability analysis might be undecidable, so we need
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- a special type for the result of ensures_amalgamability
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata Amalgamates = Yes
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster | No String -- ^ failure description
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster | DontKnow String -- ^ the reason for unknown status
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- | The default value for 'DontKnow' amalgamability result
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterdefaultDontKnow :: Amalgamates
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterdefaultDontKnow = DontKnow "Unable to assert that amalgamability is ensured"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- languages, define like "data CASL = CASL deriving Show"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass Show lid => Language lid where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster language_name :: lid -> String
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster language_name i = show i
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster description :: lid -> String
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- default implementation
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster description _ = "No description available"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- (a bit unsafe) coercion using the language name
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fostercoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Monad m) => lid1 -> lid2 -> a -> m b
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fostercoerce i1 i2 a = if language_name i1 == language_name i2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster then return $ unsafeCoerce a
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster else fail ("Logic "++ language_name i1 ++ " expected, but "
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ++ language_name i2 ++ " found")
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterrcoerce :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid1 -> lid2 -> Pos-> a -> Result b
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterrcoerce i1 i2 pos a = adjustPos pos $ coerce i1 i2 a
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- Categories are given by a quotient,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- i.e. we need equality
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- Should we allow arbitrary composition graphs and build paths?
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass (PrintLaTeX a, Typeable a, ATermConvertible a) => PrintTypeConv a
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass (Eq a, PrintTypeConv a) => EqPrintTypeConv a
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance (PrintLaTeX a, Typeable a, ATermConvertible a) => PrintTypeConv a
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance (Eq a, PrintTypeConv a) => EqPrintTypeConv a
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass (Language lid, Eq sign, Eq morphism)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => Category lid sign morphism | lid -> sign, lid -> morphism where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ide :: lid -> sign -> morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster comp :: lid -> morphism -> morphism -> Maybe morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- diagrammatic order
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster dom, cod :: lid -> morphism -> sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster legal_obj :: lid -> sign -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster legal_mor :: lid -> morphism -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- abstract syntax, parsing and printing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass (Language lid, PrintTypeConv basic_spec,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster EqPrintTypeConv symb_items,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster EqPrintTypeConv symb_map_items)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => Syntax lid basic_spec symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster | lid -> basic_spec, lid -> symb_items,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster parse_basic_spec :: lid -> Maybe(AParser basic_spec)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster parse_symb_items :: lid -> Maybe(AParser symb_items)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster parse_symb_map_items :: lid -> Maybe(AParser symb_map_items)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- default implementations
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster parse_basic_spec _ = Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster parse_symb_items _ = Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster parse_symb_map_items _ = Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass (Category lid sign morphism, Ord sentence,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster PrintTypeConv sign, PrintTypeConv morphism,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster PrintTypeConv sentence, PrintTypeConv symbol,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Eq proof_tree, Show proof_tree, ATermConvertible proof_tree,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Typeable proof_tree)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => Sentences lid sentence proof_tree sign morphism symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster | lid -> sentence, lid -> sign, lid -> morphism,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> symbol, lid -> proof_tree
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- sentence translation
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster map_sen :: lid -> morphism -> sentence -> Result sentence
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster map_sen l _ _ = statErr l "map_sen"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- simplification of sentences (leave out qualifications)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster simplify_sen :: lid -> sign -> sentence -> sentence
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster simplify_sen _ _ = id -- default implementation
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- parsing of sentences
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster parse_sentence :: lid -> Maybe (sign -> String -> Result sentence)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster parse_sentence _ = Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- print a sentence with comments
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster print_named :: lid -> GlobalAnnos -> Named sentence -> Doc
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster print_named _ = printText0
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sym_of :: lid -> sign -> Set symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster symmap_of :: lid -> morphism -> EndoMap symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sym_name :: lid -> symbol -> Id
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster provers :: lid -> [Prover sign sentence proof_tree symbol]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster provers _ = []
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster cons_checkers :: lid -> [ConsChecker
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (TheoryMorphism sign sentence morphism)]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster cons_checkers _ = []
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster consCheck :: lid -> Theory sign sentence ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster morphism -> [Named sentence] -> Result (Maybe Bool)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster consCheck l _ _ _ = statErr l "consCheck"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- static analysis
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterstatErr :: (Language lid, Monad m) => lid -> String -> m a
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterstatErr lid str = fail ("Logic." ++ str ++ " nyi for: " ++ language_name lid)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass ( Syntax lid basic_spec symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , Sentences lid sentence proof_tree sign morphism symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , Ord raw_symbol, PrintLaTeX raw_symbol, Typeable raw_symbol)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => StaticAnalysis lid
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basic_spec sentence proof_tree symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster | lid -> basic_spec, lid -> sentence, lid -> symb_items,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> symb_map_items, lid -> proof_tree,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- static analysis of basic specifications and symbol maps
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basic_analysis :: lid ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Maybe((basic_spec, -- abstract syntax tree
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign, -- efficient table for env signature
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster GlobalAnnos) -> -- global annotations
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Result (basic_spec,sign,sign,[Named sentence]))
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- the resulting bspec has analyzed axioms in it
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- sign's: sigma_local, sigma_complete, i.e.
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- the second output sign united with the input sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- should yield the first output sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- the second output sign is the accumulated sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- default implementation
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basic_analysis _ = Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- Shouldn't the following deliver Maybes???
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign_to_basic_spec :: lid -> sign -> [Named sentence] -> basic_spec
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster stat_symb_map_items ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster stat_symb_map_items _ _ = fail "Logic.stat_symb_map_items"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster stat_symb_items l _ = statErr l "stat_symb_items"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- architectural sharing analysis
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ensures_amalgamability :: lid ->
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster (HetcatsOpts, -- the program options
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Diagram sign morphism, -- the diagram to be analyzed
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster [(Node, morphism)], -- the sink
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Diagram String String) -- the descriptions of nodes and edges
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -> Result Amalgamates
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ensures_amalgamability l _ = statErr l "ensures_amalgamability"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- symbols and symbol maps
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster symbol_to_raw :: lid -> symbol -> raw_symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster id_to_raw :: lid -> Id -> raw_symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster matches :: lid -> symbol -> raw_symbol -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- operations on signatures and morphisms
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster empty_signature :: lid -> sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster signature_union :: lid -> sign -> sign -> Result sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster signature_union l _ _ = statErr l "signature_union"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster morphism_union :: lid -> morphism -> morphism -> Result morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster morphism_union l _ _ = statErr l "morphism_union"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster final_union :: lid -> sign -> sign -> Result sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster final_union l _ _ = statErr l "final_union"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- see CASL reference manual, III.4.1.2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_subsig :: lid -> sign -> sign -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster inclusion :: lid -> sign -> sign -> Result morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster inclusion l _ _ = statErr l "inclusion"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster generated_sign, cogenerated_sign ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> Set symbol -> sign -> Result morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster generated_sign l _ _ = statErr l "generated_sign"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster cogenerated_sign l _ _ = statErr l "cogenerated_sign"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster induced_from_morphism ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> EndoMap raw_symbol -> sign -> Result morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster induced_from_morphism l _ _ = statErr l "induced_from_morphism"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster induced_from_to_morphism ::
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster induced_from_to_morphism l _ _ _ =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster statErr l "induced_from_to_morphism"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass (Ord l, Show l) => LatticeWithTop l where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster meet, join :: l -> l -> l
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- a dummy instance
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance LatticeWithTop () where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster meet _ _ = ()
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster join _ _ = ()
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterclass (StaticAnalysis lid
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basic_spec sentence proof_tree symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster LatticeWithTop sublogics, ATermConvertible sublogics,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Typeable sublogics)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster => Logic lid sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster | lid -> sublogics, lid -> basic_spec, lid -> sentence,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> symb_items, lid -> symb_map_items, lid -> proof_tree,
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> sign, lid -> morphism, lid ->symbol, lid -> raw_symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- for a process logic, return its data logic
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster data_logic :: lid -> Maybe AnyLogic
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster data_logic _ = Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sublogic_names :: lid -> sublogics -> [String]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sublogic_names lid _ = [language_name lid]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster -- the first name is the principal name
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster all_sublogics :: lid -> [sublogics]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster all_sublogics _ = [top]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_basic_spec :: lid -> sublogics -> basic_spec -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_basic_spec _ _ _ = False
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_sentence :: lid -> sublogics -> sentence -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_sentence _ _ _ = False
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_symb_items :: lid -> sublogics -> symb_items -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_symb_items _ _ _ = False
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_symb_map_items :: lid -> sublogics -> symb_map_items -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_symb_map_items _ _ _ = False
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_sign :: lid -> sublogics -> sign -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_sign _ _ _ = False
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_morphism :: lid -> sublogics -> morphism -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_morphism _ _ _ = False
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_symbol :: lid -> sublogics -> symbol -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster is_in_symbol _ _ _ = False
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_basic_spec :: lid -> basic_spec -> sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_basic_spec _ _ = top
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_sentence :: lid -> sentence -> sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_sentence _ _ = top
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_symb_items :: lid -> symb_items -> sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_symb_items _ _ = top
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_symb_map_items :: lid -> symb_map_items -> sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_symb_map_items _ _ = top
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_sign :: lid -> sign -> sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_sign _ _ = top
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_morphism :: lid -> morphism -> sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_morphism _ _ = top
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_symbol :: lid -> symbol -> sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster min_sublogic_symbol _ _ = top
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_basic_spec :: lid -> sublogics
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna -> basic_spec -> basic_spec
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_basic_spec _ _ b = b
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_symb_items :: lid -> sublogics
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna -> symb_items -> Maybe symb_items
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_symb_items _ _ _ = Nothing
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_symb_map_items :: lid -> sublogics
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna -> symb_map_items -> Maybe symb_map_items
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_symb_map_items _ _ _ = Nothing
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_sign :: lid -> sublogics -> sign -> sign
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_sign _ _ s = s
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proj_sublogic_morphism :: lid -> sublogics -> morphism -> morphism
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_morphism _ _ m = m
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_epsilon li _ s = ide li s
57a1b25dcdf865eacb2fe2e17c5ca83e942da047David Luna proj_sublogic_symbol :: lid -> sublogics -> symbol -> Maybe symbol
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster proj_sublogic_symbol _ _ _ = Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster top_sublogic :: lid -> sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster top_sublogic _ = top
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster----------------------------------------------------------------
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- Derived functions
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster----------------------------------------------------------------
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterempty_theory :: StaticAnalysis lid
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basic_spec sentence proof_tree symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol =>
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster lid -> Theory sign sentence
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterempty_theory lid = (empty_signature lid,[])
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster----------------------------------------------------------------
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- Existential type covering any logic
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster----------------------------------------------------------------
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata AnyLogic = forall lid sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree .
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Logic lid sublogics
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster basic_spec sentence symb_items symb_map_items
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sign morphism symbol raw_symbol proof_tree =>
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Show AnyLogic where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster show (Logic lid) = language_name lid
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Eq AnyLogic where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Logic lid1 == Logic lid2 = language_name lid1 == language_name lid2
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostertyconAnyLogic :: TyCon
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostertyconAnyLogic = mkTyCon "Logic.Logic.AnyLogic"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Typeable AnyLogic where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster typeOf _ = mkTyConApp tyconAnyLogic []
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster----------------------------------------------------------------
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- Typeable instances
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster----------------------------------------------------------------
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosternamedTc :: TyCon
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosternamedTc = mkTyCon "Common.AS_Annotation.Named"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Typeable s => Typeable (Named s) where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster typeOf s = mkTyConApp namedTc [typeOf ((undefined :: Named a -> a) s)]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostersetTc :: TyCon
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostersetTc = mkTyCon "Common.Lib.Set.Set"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance Typeable a => Typeable (Set a) where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster typeOf s = mkTyConApp setTc [typeOf ((undefined:: Set a -> a) s)]
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermapTc :: TyCon
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostermapTc = mkTyCon "Common.Lib.Map.Map"
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterinstance (Typeable a, Typeable b) => Typeable (Map a b) where
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster typeOf m = mkTyConApp mapTc [typeOf ((undefined :: Map a b -> a) m),
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster typeOf ((undefined :: Map a b -> b) m)]
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster{- class hierarchy:
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Sentences Syntax
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster StaticAnalysis (no sublogics)