Logic.hs revision fbf80d5a0f83312673b660f28c461943196feb74
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
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance 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
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder 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)
b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maeder General Logics
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Logic Colloquium 87, p. 275--329, North Holland, 1989
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (general notion of logic - also proof theory;
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance notion of logic representation, called map there)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance T. Mossakowski:
668c9c725a11c0f77057152148570af853a1bc0dFelix 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.
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (what is needed for static anaylsis)
0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Mance S. Autexier and T. Mossakowski
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Integrating HOLCASL into the Development Graph Manager MAYA
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder FroCoS 2002, to appear
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder (interface to provers)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Weak amalgamability
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mancemodule Logic where
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maederimport AS_Annotation
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport FiniteMap
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Prover -- for one half of class Sentences
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport PrettyPrint
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- for coercion used in LogicGraph.hs and Grothendieck.hs
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceimport GlaExts(unsafeCoerce#)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mancetype EndoMap a = FiniteMap a a
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- diagrams are just graphs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata Diagram object morphism = Graph object morphism
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder-- languages, define like "data CASL = CASL deriving Show"
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maederclass Show id => Language id where
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder language_name :: id -> String
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder language_name i = show i
3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel Mance-- (a bit unsafe) coercion using the language name
52991d9b46a98ad6a9020421a3244950b0f8a522Felix Gabriel Mancecoerce :: (Language id1, Language id2) => id1 -> id2 -> a -> Maybe b
52991d9b46a98ad6a9020421a3244950b0f8a522Felix Gabriel Mancecoerce i1 i2 a = if language_name i1 == language_name i2 then
3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel Mance (Just $ unsafeCoerce# a) else Nothing
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance-- Categories are given by a quotient,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance-- i.e. we need equality
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance-- Should we allow arbitrary composition graphs and build paths?
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Manceclass (Language id, Eq sign, Show sign, Eq morphism) =>
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Category id sign morphism | id -> sign, id -> morphism where
1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel Mance ide :: id -> sign -> morphism
4c684d7a2343be7350eba088f8be42888f86a495Felix Gabriel Mance o :: id -> morphism -> morphism -> Maybe morphism
1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel Mance dom, cod :: id -> morphism -> sign
5a3ae0a9224276de25e709ef8788c1b9716cd206Christian Maeder legal_obj :: id -> sign -> Bool
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance legal_mor :: id -> morphism -> Bool
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance-- abstract syntax, parsing and printing
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Manceclass (Language id, PrettyPrint basic_spec, Eq basic_spec,
c298a419605037f5352b5ad0f67b3e06db094051Felix 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
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance parse_basic_spec :: id -> Maybe(GenParser Char st basic_spec)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance parse_symb_items :: id -> GenParser Char st symb_items
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance parse_symb_map_items :: id -> GenParser Char st symb_map_items
9cb6af1a7632f12b60f592ce5eb2ac51e6bd33bbFelix Gabriel Mance-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceclass (Category id sign morphism, Show sentence,
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder Show local_env, Ord symbol, Show symbol)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance => Sentences id sentence local_env sign morphism symbol
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance | id -> sentence, id -> local_env, id -> sign, id -> morphism,
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- sentence translation
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance map_sen :: id -> morphism -> sentence -> Result sentence
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance -- parsing of sentences
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance parse_sentence :: id -> local_env -> 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
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Manceclass ( Syntax id basic_spec symb_items symb_map_items
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , Sentences id sentence local_env sign morphism symbol
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance , Show raw_symbol, Eq raw_symbol)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance => StaticAnalysis id
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance local_env sign morphism symbol raw_symbol
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance | id -> basic_spec, id -> sentence, id -> symb_items,
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance id -> symb_map_items, id -> local_env,
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 local_env, -- efficient table for env signature
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance [Annotation]) -> -- global annotations
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Result (local_env,sign,[(String,sentence)]))
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder -- the output local env is expected to be
a921ae1da1302f673204e7b63cdce01439a9bd5eFelix Gabriel Mance -- just the input local env, united with the sign.
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- We have both just for efficiency reasons.
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance -- These include any new annotations
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance stat_symb_map_items ::
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance id -> symb_map_items -> Result (EndoMap raw_symbol)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix 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)
c298a419605037f5352b5ad0f67b3e06db094051Felix 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
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance sym_of :: id -> sign -> Set symbol
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance symmap_of :: id -> morphism -> EndoMap symbol
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance matches :: id -> symbol -> raw_symbol -> Bool
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance sym_name :: id -> symbol -> Id
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance -- operations on local envs, signatures and morphisms
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance empty_local_env :: id -> local_env
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance add_sign :: id -> sign -> local_env -> local_env
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance empty_signature :: id -> sign
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance signature_union :: id -> sign -> sign -> Result sign
8af00c8930672188ae80c8829428859160d329d0Felix 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
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Manceclass Ord l => LatticeWithTop l where
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance meet, join :: l -> l -> l
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Manceclass (StaticAnalysis id
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance local_env sign morphism symbol raw_symbol,
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance LatticeWithTop sublogics, Typeable sublogics) =>
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance Logic id sublogics
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance basic_spec sentence symb_items symb_map_items
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance local_env sign morphism symbol raw_symbol
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance | id -> sublogics, id -> basic_spec, id -> sentence, id -> symb_items,
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance id -> symb_map_items, id -> local_env,
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance id -> sign, id -> morphism, id ->symbol, id -> raw_symbol
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance sublogic_names :: id -> sublogics -> [String]
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance -- the first name is the principal name
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance all_sublogics :: id -> [sublogics]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance is_in_basic_spec :: id -> sublogics -> basic_spec -> Bool
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance is_in_sentence :: id -> sublogics -> sentence -> Bool
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance is_in_symb_items :: id -> sublogics -> symb_items -> Bool
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance is_in_symb_map_items :: id -> sublogics -> symb_map_items -> Bool
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance is_in_sign :: id -> sublogics -> sign -> Bool
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance is_in_morphism :: id -> sublogics -> morphism -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance is_in_symbol :: id -> sublogics -> symbol -> Bool
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance min_sublogic_basic_spec :: id -> basic_spec -> sublogics
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance min_sublogic_sentence :: id -> sentence -> sublogics
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance min_sublogic_symb_items :: id -> symb_items -> sublogics
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance min_sublogic_symb_map_items :: id -> symb_map_items -> sublogics
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maeder min_sublogic_sign :: id -> sign -> sublogics
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance min_sublogic_morphism :: id -> morphism -> sublogics
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance min_sublogic_symbol :: id -> symbol -> sublogics
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance proj_sublogic_basic_spec :: id -> sublogics -> basic_spec -> basic_spec
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance proj_sublogic_symb_items :: id -> sublogics -> symb_items -> Maybe symb_items
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance proj_sublogic_symb_map_items :: id -> sublogics -> symb_map_items -> Maybe symb_map_items
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance proj_sublogic_sign :: id -> sublogics -> sign -> sign
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance proj_sublogic_morphism :: id -> sublogics -> morphism -> morphism
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance proj_sublogic_epsilon :: id -> sublogics -> sign -> morphism
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance proj_sublogic_symbol :: id -> sublogics -> symbol -> Maybe symbol
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance{- class hierarchy:
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Sentences Syntax
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance StaticAnalysis (no sublogics)