5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maedermodule Logic where
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maederimport Data.Dynamic as Dynamic
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- the identity of a language
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiclass (Show id, Typeable id) => Language id where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski language_name :: id -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder language_name = show
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- categories, needed for signatures and signature morphisms
da955132262baab309a50fdffe228c9efe68251dCui Jianclass (Language id, Eq sign, Show sign, Eq morphism) =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Category id sign morphism | id -> sign, id -> morphism where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski identity :: id -> sign -> morphism
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski o :: id -> morphism -> morphism -> Maybe morphism
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski dom, cod :: id -> morphism -> sign
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- abstract syntax, parsing and printing
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiclass (Language id, Show basic_spec, Eq basic_spec, Typeable basic_spec,
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Show symbol_mapping, Eq symbol_mapping, Typeable symbol_mapping,
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Show sentence, Eq sentence) =>
da955132262baab309a50fdffe228c9efe68251dCui Jian Syntax id sign sentence basic_spec symbol_mapping
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski | id -> sign, id -> basic_spec, id -> symbol_mapping, id -> sentence where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder parse_basic_spec :: id -> CharParser st basic_spec
601dc92e4c128d23a726593357c654fb776a63a7Till Mossakowski parse_symbol_mapping :: id -> CharParser st symbol_mapping
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder parse_sentence :: id -> sign -> String -> sentence
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- module Logic continued
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- a theory consists of a signature and a set of sentences
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype Theory sign sentence = (sign, [sentence])
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- static analysis
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiclass (Syntax id sign sentence basic_spec symbol_mapping,
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Typeable sign, Typeable morphism, Typeable sentence) =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski StaticAnalysis id sign morphism sentence basic_spec symbol_mapping
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski | id -> morphism where
da955132262baab309a50fdffe228c9efe68251dCui Jian basic_analysis ::
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski id -> sign -> basic_spec -> Maybe (Theory sign sentence)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski -- the input signature contains imported stuff
da955132262baab309a50fdffe228c9efe68251dCui Jian stat_symbol_mapping ::
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski id -> symbol_mapping -> sign -> Maybe morphism
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata Proof_status = Open | Disproved | Proved deriving Show
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- logic (entailment system)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiclass (Category id sign morphism,
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski StaticAnalysis id sign morphism sentence basic_spec symbol_mapping) =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Logic id sign morphism sentence basic_spec symbol_mapping
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder where empty_signature :: id -> sign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder empty_theory :: id -> Theory sign sentence
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder empty_theory i = (empty_signature i, [])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder map_sentence :: id -> morphism -> sentence -> Maybe sentence
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder inv_map_sentence :: id -> morphism -> sentence -> Maybe sentence
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder prover :: id -> Theory sign sentence -- theory that shall be assumed
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> sentence -- the proof goal
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> IO Proof_status
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- logic translations
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maederdata Logic_translation id1 s1 m1 sen1 b1 sy1 id2 s2 m2 sen2 b2 sy2 =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Logic_translation { source :: id1,
da955132262baab309a50fdffe228c9efe68251dCui Jian target :: id2,
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski tr_sign :: s1 -> s2,
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski tr_mor :: m1 -> m2,
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski tr_sen :: s1 -> sen1 -> Maybe sen2,
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski inv_tr_sen :: s1 -> sen2 -> Maybe sen1 }