8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{-# LANGUAGE MultiParamTypeClasses #-}
5e874259af7e1161240c70c3d2ed33e86c7da167Christian MaederDescription : instance of class Logic
67ebe351bf4578fa09c53dae43ba728e2650f652Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederStability : experimental
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian MaederPortability : non-portable (imports Logic.Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederHere is the place where the class Logic is instantiated for HasCASL.
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder Also the instances for Syntax and Category.
a669e4685b32ff5ca1bca785eacc5e30a545b010Christian Maedermodule HasCASL.Logic_HasCASL (HasCASL (HasCASL)) where
6d23c6f8a099ab258a28e44a721ac32cb0877e9eChristian Maederdata HasCASL = HasCASL deriving Show
05ca76b03b6d16bcfb3e7654c31e41a220e85663Till Mossakowskiinstance Language HasCASL where
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder description _ = unlines
602041e384342ea908c976a298e8b47774d3500cTill Mossakowski [ "HasCASL - Algebraic Specification + Functional Programming"
602041e384342ea908c976a298e8b47774d3500cTill Mossakowski , " = Environment for Formal Software Development"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , "This logic is based on the partial lambda calculus and"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " features subtyping, overloading and type class polymorphism"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , "See the HasCASL summary and further papers available at"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " http://www.informatik.uni-bremen.de/cofi/HasCASL"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , "Abbreviations of sublogic names indicate the following feature:"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " Sub -> with subtyping"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " P -> with partial functions"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " TyCl -> with simple type classes (a la Isabelle)"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " CoCl -> with constructor classes (a la Haskell)"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " Poly -> polymorphism without classes"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " TyCons -> user definable type constructors"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " HOL -> higher order logic (covers sort generation constraints)"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " FOL -> first order logic"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , "and others like for CASL"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , "Examples:"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " SubCFOL= -> the CASL logic without sort generation constraints"
70dd17fd1ceb698d8bac709c56ceb60efe95e264Christian Maeder , " PCoClTyConsHOL -> the Haskell type system fragment" ]
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederinstance Monoid BasicSpec where
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder mempty = BasicSpec []
e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder mappend (BasicSpec l1) (BasicSpec l2) = BasicSpec $ l1 ++ l2
1711f9cf0aa5b0564a0b5aa5e331e51e4c1b1a4cChristian Maederinstance Syntax HasCASL BasicSpec
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowski Symbol SymbItems SymbMapItems
3998bf8fd1b236d1a936b4a01688c3d9e1d49e05Christian Maeder parse_basic_spec HasCASL = Just $ const basicSpec
50895dae7d9849df2dc922651d93bbc6aa5529c1Christian Maeder parse_symb_items HasCASL = Just symbItems
50895dae7d9849df2dc922651d93bbc6aa5529c1Christian Maeder parse_symb_map_items HasCASL = Just symbMapItems
43a582fe35884e2c6f455e7bfa34f0f4ef8dfe2eChristian Maeder toItem HasCASL = bsToItem
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maederinstance Category Env Morphism where
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder composeMorphisms = compMor
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder isInclusion = isInclMor
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder dom = msource
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder cod = mtarget
2faad0c99d17a6ef53a464864caccbb20cf48409Christian Maeder legal_mor = legalMor
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettichinstance Sentences HasCASL Sentence Env Morphism Symbol where
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder map_sen HasCASL = mapSentence
af47051acb16b97b6bc0ff7295cae44eed87d63eChristian Maeder simplify_sen HasCASL = simplifySentence
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder print_named _ = printSemiAnno (changeGlobalAnnos addBuiltins . pretty) True
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maeder . fromLabelledSen
4b338e9d8a4e0bffb4d1bc6fb5fa371a8a0dec1aTill Mossakowski sym_name HasCASL = symName
fefdf8f5a314d2999934b4ad40035ac062ebcaa1Till Mossakowski symKind HasCASL = show . pretty . symbTypeToKind . symType
7d228ff8072e039be1f7b9630fee712733a80334Christian Maeder sym_of HasCASL = symOf
34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maeder mostSymsOf HasCASL = mostSyms
4b338e9d8a4e0bffb4d1bc6fb5fa371a8a0dec1aTill Mossakowski symmap_of HasCASL = morphismToSymbMap
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettichinstance StaticAnalysis HasCASL BasicSpec Sentence
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder SymbItems SymbMapItems
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Symbol RawSymbol where
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder basic_analysis HasCASL = Just basicAnalysis
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder signature_union HasCASL = merge
a8f87ac3a544ad741961b3ae494c729877203ebeChristian Maeder signatureDiff HasCASL s = return . diffEnv s
ef391a2936c4277e6d71f9887b834dfaaaf2291bChristian Maeder empty_signature HasCASL = initialEnv
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder induced_from_to_morphism HasCASL = inducedFromToMorphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder induced_from_morphism HasCASL = inducedFromMorphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder morphism_union HasCASL = morphismUnion
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder is_subsig HasCASL = isSubEnv
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder subsig_inclusion HasCASL s = return . mkMorphism s
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder cogenerated_sign HasCASL = cogeneratedSign
096b050a106eefe1093eb7659e4924b1d7850aa4Christian Maeder generated_sign HasCASL = generatedSign
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder stat_symb_map_items HasCASL e _ = statSymbMapItems e
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder stat_symb_items HasCASL = statSymbItems
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder symbol_to_raw HasCASL = symbolToRaw
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder id_to_raw HasCASL = idToRaw
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder matches HasCASL = matchSymb
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder final_union HasCASL = merge
296c6cdef9162217e9d9d1c17790dc71335b8d72Christian Maederinstance SemiLatticeWithTop Sublogic where
8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder lub s = sublogicUp . sublogic_max s
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maeder top = topLogic
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maederinstance SublogicName Sublogic where
4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder sublogicName = sublogic_name
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance MinSublogic Sublogic BasicSpec where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder minSublogic = sl_basicSpec
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance MinSublogic Sublogic Sentence where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder minSublogic = sl_sentence
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance MinSublogic Sublogic SymbItems where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder minSublogic = sl_symbItems
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance MinSublogic Sublogic SymbMapItems where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder minSublogic = sl_symbMapItems
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance MinSublogic Sublogic Env where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder minSublogic = sl_env
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance MinSublogic Sublogic Morphism where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder minSublogic = sl_morphism
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maederinstance MinSublogic Sublogic Symbol where
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder minSublogic = sl_symbol
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maederinstance ProjectSublogic Sublogic BasicSpec where
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maeder projectSublogic = error "ProjectSublogic Sublogic BasicSpec"
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maederinstance ProjectSublogicM Sublogic SymbItems where
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maeder projectSublogicM = error " ProjectSublogicM Sublogic SymbItems"
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maederinstance ProjectSublogicM Sublogic SymbMapItems where
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maeder projectSublogicM = error " ProjectSublogicM Sublogic SymbMapItems"
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maederinstance ProjectSublogic Sublogic Env where
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maeder projectSublogic = error "ProjectSublogic Sublogic Env"
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maederinstance ProjectSublogic Sublogic Morphism where
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maeder projectSublogic = error "ProjectSublogic Sublogic Morphism"
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maederinstance ProjectSublogicM Sublogic Symbol where
5e874259af7e1161240c70c3d2ed33e86c7da167Christian Maeder projectSublogicM = error " ProjectSublogicM Sublogic Symbol"
7c2d602a73afe304ac0ca225ecff42b2ae8bdab3Christian Maederinstance Logic HasCASL Sublogic
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder BasicSpec Sentence SymbItems SymbMapItems
7cee561116562e8ba231fd45d6066c0a97abf243Christian Maeder Symbol RawSymbol () where
cdcf5d3f1e79d8798d77efa29e6193af94ea0604Till Mossakowski stability _ = Stable
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder all_sublogics _ = sublogics_all
cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich empty_proof_tree _ = ()