content: {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
  
  module Logic where
  
  import Data.Dynamic as Dynamic
  import Text.ParserCombinators.Parsec
  
  -- the identity of a language
  class (Show id, Typeable id) => Language id where
      language_name :: id -> String
      language_name = show
  
  -- categories, needed for signatures and signature morphisms
  class (Language id, Eq sign, Show sign, Eq morphism) =>
        Category id sign morphism | id -> sign, id -> morphism where
           identity :: id -> sign -> morphism
           o :: id -> morphism -> morphism -> Maybe morphism
           dom, cod :: id -> morphism -> sign
  
  -- abstract syntax, parsing and printing
  class (Language id, Show basic_spec, Eq basic_spec, Typeable basic_spec,
                      Show symbol_mapping, Eq symbol_mapping, Typeable symbol_mapping,
                      Show sentence, Eq sentence) =>
        Syntax id sign sentence basic_spec symbol_mapping
          | id -> sign, id -> basic_spec, id -> symbol_mapping, id -> sentence where
           parse_basic_spec :: id -> CharParser st basic_spec
           parse_symbol_mapping :: id -> CharParser st symbol_mapping
           parse_sentence :: id -> sign -> String -> sentence
  
  
  -- module Logic continued
  
  -- a theory consists of a signature and a set of sentences
  type Theory sign sentence = (sign, [sentence])
  
  -- static analysis
  class (Syntax id sign sentence basic_spec symbol_mapping,
         Typeable sign, Typeable morphism, Typeable sentence) =>
        StaticAnalysis id sign morphism sentence basic_spec symbol_mapping
          | id -> morphism where
           basic_analysis ::
              id -> sign -> basic_spec -> Maybe (Theory sign sentence)
                  -- the input signature contains imported stuff
           stat_symbol_mapping ::
              id -> symbol_mapping -> sign -> Maybe morphism
  
  -- Proofs
  data Proof_status = Open | Disproved | Proved deriving Show
  
  -- logic (entailment system)
  class (Category id sign morphism,
         StaticAnalysis id sign morphism sentence basic_spec symbol_mapping) =>
        Logic id sign morphism sentence basic_spec symbol_mapping
        where empty_signature :: id -> sign
              empty_theory :: id -> Theory sign sentence
              empty_theory i = (empty_signature i, [])
              map_sentence :: id -> morphism -> sentence -> Maybe sentence
              inv_map_sentence :: id -> morphism -> sentence -> Maybe sentence
              prover :: id -> Theory sign sentence -- theory that shall be assumed
                           -> sentence                -- the proof goal
                           -> IO Proof_status
  
  -- logic translations
  data Logic_translation id1 s1 m1 sen1 b1 sy1 id2 s2 m2 sen2 b2 sy2 =
       Logic_translation { source :: id1,
                           target :: id2,
                           tr_sign :: s1 -> s2,
                           tr_mor :: m1 -> m2,
                           tr_sen :: s1 -> sen1 -> Maybe sen2,
                           inv_tr_sen :: s1 -> sen2 -> Maybe sen1 }
  