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