Logic.hs revision a2e054b20027cb83c35f4a97f308de8ebe32b23c
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- needs ghc -fglasgow-exts -fallow-overlapping-instances -package data
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Till Mossakowski, Christian Maeder
5d801400993c9671010d244646936d8fd435638cChristian Maeder Provides data structures for logics (with symbols). Logics are
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance a type class with an "identitiy" type (usually interpreted
5d801400993c9671010d244646936d8fd435638cChristian Maeder by a singleton set) which serves to treat logics as
aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Mance data. All the functions in the type class take the
5d801400993c9671010d244646936d8fd435638cChristian Maeder identity as first argument in order to determine the logic.
5d801400993c9671010d244646936d8fd435638cChristian Maeder For logic representations see LogicRepr.hs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance J. A. Goguen and R. M. Burstall
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Institutions: Abstract Model Theory for Specification and
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance JACM 39, p. 95--146, 1992
feab1106bbee4f2ea2fd48bca7106dd041e4211dFelix Gabriel Mance (general notion of logic - model theory only)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance General Logics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Logic Colloquium 87, p. 275--329, North Holland, 1989
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (general notion of logic - also proof theory;
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance notion of logic representation, called map there)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance T. Mossakowski:
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Specification in an arbitrary institution with symbols
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance 14th WADT 1999, LNCS 1827, p. 252--270
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (treatment of symbols and raw symbols, see also CASL semantics)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance T. Mossakowski, B. Klin:
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Institution Independent Static Analysis for CASL
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance (what is needed for static anaylsis)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance S. Autexier and T. Mossakowski
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder Integrating HOLCASL into the Development Graph Manager MAYA
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder FroCoS 2002, to appear
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (interface to provers)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Weak amalgamability
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maedermodule Logic where
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport GlobalAnnotations
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport FiniteMap
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance--import Parsec
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Prover -- for one half of class Sentences
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maederimport PrettyPrint
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- for coercion used in LogicGraph.hs and Grothendieck.hs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport UnsafeCoerce
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maedertype EndoMap a = FiniteMap a a
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder-- diagrams are just graphs
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mancedata Diagram object morphism = Graph object morphism
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance-- languages, define like "data CASL = CASL deriving Show"
4c684d7a2343be7350eba088f8be42888f86a495Felix Gabriel Manceclass Show id => Language id where
1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel Mance language_name :: id -> String
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance language_name i = show i
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- (a bit unsafe) coercion using the language name
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancecoerce :: (Language id1, Language id2) => id1 -> id2 -> a -> Maybe b
8526b5a83ad3e1434d49e67f2dfc4af9ec91a7e4Christian Maedercoerce i1 i2 a = if language_name i1 == language_name i2 then
8526b5a83ad3e1434d49e67f2dfc4af9ec91a7e4Christian Maeder (Just $ unsafeCoerce a) else Nothing
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- Categories are given by a quotient,
e93f944968a75becbfb496994b85263b9cc1669fFrancisc Nicolae Bungiu-- i.e. we need equality
be2439588008221e691321fdf4f75432cfb72878Felix Gabriel Mance-- Should we allow arbitrary composition graphs and build paths?
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceclass (Language id, Eq sign, Show sign, Eq morphism) =>
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Category id sign morphism | id -> sign, id -> morphism where
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance ide :: id -> sign -> morphism
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance o :: id -> morphism -> morphism -> Maybe morphism
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance dom, cod :: id -> morphism -> sign
dd3c105fcc30b5d6b750d8fbe32250207b996109Felix Gabriel Mance legal_obj :: id -> sign -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance legal_mor :: id -> morphism -> Bool
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- abstract syntax, parsing and printing
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mancetype ParseFun a = FilePath -> Int -> Int -> String -> (a,String,Int,Int)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance -- args: filename, line, column, input text
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance -- result: value, remaining text, line, column
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Manceclass (Language id, PrettyPrint basic_spec, Eq basic_spec,
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance PrettyPrint symb_items, Eq symb_items,
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance PrettyPrint symb_map_items, Eq symb_map_items) =>
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance Syntax id basic_spec symb_items symb_map_items
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance | id -> basic_spec, id -> symb_items,
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance id -> symb_map_items
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance parse_basic_spec :: id -> Maybe(ParseFun basic_spec)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance parse_symb_items :: id -> Maybe(ParseFun symb_items)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance parse_symb_map_items :: id -> Maybe(ParseFun symb_map_items)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceclass (Category id sign morphism, Show sentence,
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Ord symbol, Show symbol)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance => Sentences id sentence sign morphism symbol
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance | id -> sentence, id -> sign, id -> morphism,
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- sentence translation
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance map_sen :: id -> morphism -> sentence -> Result sentence
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- parsing of sentences
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance parse_sentence :: id -> sign -> String -> Result sentence
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- is a term parser needed as well?
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance provers :: id -> [Prover sentence symbol]
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance cons_checkers :: id -> [Cons_checker
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance (TheoryMorphism sign sentence morphism)]
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance-- static analysis
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceclass ( Syntax id basic_spec symb_items symb_map_items
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance , Sentences id sentence sign morphism symbol
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance , Show raw_symbol, Eq raw_symbol)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance => StaticAnalysis id
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder sign morphism symbol raw_symbol
a921ae1da1302f673204e7b63cdce01439a9bd5eFelix Gabriel Mance | id -> basic_spec, id -> sentence, id -> symb_items,
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id -> symb_map_items,
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id -> sign, id -> morphism, id -> symbol, id -> raw_symbol
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- static analysis of basic specifications and symbol maps
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance basic_analysis :: id ->
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Maybe((basic_spec, -- abstract syntax tree
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance sign, -- efficient table for env signature
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance GlobalAnnos) -> -- global annotations
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Result (sign,sign,[(String,sentence)]))
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- the first output sign is the accumulated sign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- the second output sign united with the input sing
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- should yield the first output sign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance stat_symb_map_items ::
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id -> symb_map_items -> Result (EndoMap raw_symbol)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance stat_symb_items :: id -> symb_items -> Result [raw_symbol]
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- architectural sharing analysis for one morphism
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance ensures_amalgamability :: id ->
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance (Diagram sign morphism, Node, sign, LEdge morphism, morphism) ->
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Result (Diagram sign morphism)
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance -- do we need it also for sinks consisting of two morphisms?
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- symbols and symbol maps
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance symbol_to_raw :: id -> symbol -> raw_symbol
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id_to_raw :: id -> Id -> raw_symbol
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance sym_of :: id -> sign -> Set symbol
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance symmap_of :: id -> morphism -> EndoMap symbol
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance matches :: id -> symbol -> raw_symbol -> Bool
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance sym_name :: id -> symbol -> Id
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- operations on signatures and morphisms
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance add_sign :: id -> sign -> sign -> sign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance empty_signature :: id -> sign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance signature_union :: id -> sign -> sign -> Result sign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance final_union :: id -> sign -> sign -> Result sign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance is_subsig :: id -> sign -> sign -> Bool
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance generated_sign, cogenerated_sign ::
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id -> [raw_symbol] -> sign -> Result morphism
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance induced_from_morphism ::
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id -> EndoMap raw_symbol -> sign -> Result morphism
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance induced_from_to_morphism ::
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id -> EndoMap raw_symbol -> sign -> sign -> Result morphism
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance extend_morphism ::
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id -> sign -> morphism -> sign -> sign -> Result morphism
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceclass Ord l => LatticeWithTop l where
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance meet, join :: l -> l -> l
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceclass (StaticAnalysis id
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign morphism symbol raw_symbol,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance LatticeWithTop sublogics) =>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Logic id sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign morphism symbol raw_symbol
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | id -> sublogics, id -> basic_spec, id -> sentence, id -> symb_items,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance id -> symb_map_items,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance id -> sign, id -> morphism, id ->symbol, id -> raw_symbol
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sublogic_names :: id -> sublogics -> [String]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- the first name is the principal name
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance all_sublogics :: id -> [sublogics]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance is_in_basic_spec :: id -> sublogics -> basic_spec -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance is_in_sentence :: id -> sublogics -> sentence -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance is_in_symb_items :: id -> sublogics -> symb_items -> Bool
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maeder is_in_symb_map_items :: id -> sublogics -> symb_map_items -> Bool
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maeder is_in_sign :: id -> sublogics -> sign -> Bool
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maeder is_in_morphism :: id -> sublogics -> morphism -> Bool
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maeder is_in_symbol :: id -> sublogics -> symbol -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance min_sublogic_basic_spec :: id -> basic_spec -> sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance min_sublogic_sentence :: id -> sentence -> sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance min_sublogic_symb_items :: id -> symb_items -> sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance min_sublogic_symb_map_items :: id -> symb_map_items -> sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance min_sublogic_sign :: id -> sign -> sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance min_sublogic_morphism :: id -> morphism -> sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance min_sublogic_symbol :: id -> symbol -> sublogics
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance proj_sublogic_basic_spec :: id -> sublogics -> basic_spec -> basic_spec
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance proj_sublogic_symb_items :: id -> sublogics -> symb_items -> Maybe symb_items
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder proj_sublogic_symb_map_items :: id -> sublogics -> symb_map_items -> Maybe symb_map_items
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance proj_sublogic_sign :: id -> sublogics -> sign -> sign
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance proj_sublogic_morphism :: id -> sublogics -> morphism -> morphism
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance proj_sublogic_epsilon :: id -> sublogics -> sign -> morphism
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance proj_sublogic_symbol :: id -> sublogics -> symbol -> Maybe symbol
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance{- class hierarchy:
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Sentences Syntax
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance StaticAnalysis (no sublogics)