{-# 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 }
