Logic_CommonLogic.hs revision cacbb5e3100fb85d23d1614cace3a8662801f2e6
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart PoetteringModule : $Header$
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart PoetteringDescription : Instance of class Logic for common logic
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart PoetteringCopyright : (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart PoetteringLicense : GPLv2 or higher, see LICENSE.txt
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart PoetteringMaintainer : eugenk@informatik.uni-bremen.de
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart PoetteringStability : experimental
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart PoetteringPortability : non-portable (imports Logic.Logic)
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart PoetteringInstance of class Logic for the common logic
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringmodule CommonLogic.Logic_CommonLogic where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringimport qualified Data.Map as Map
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringimport CommonLogic.OMDocImport as OMDocImport
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringdata CommonLogic = CommonLogic deriving Show
ac720200b7e5b80cc4985087e38f3452e5b3b080Lennart Poetteringinstance Language CommonLogic where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering description _ = "CommonLogic Logic\n"
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance Category Sign Morphism
c3bc53e62459d7e566ffffeade41cd82bc6754f5Lennart Poettering isInclusion = Map.null . propMap
c3bc53e62459d7e566ffffeade41cd82bc6754f5Lennart Poettering legal_mor = isLegalMorphism
c3bc53e62459d7e566ffffeade41cd82bc6754f5Lennart Poettering composeMorphisms = composeMor
0d2cd47617b423f37d7425be7a56ae2fca8ff9f6Lennart Poetteringinstance Sentences CommonLogic
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering negation CommonLogic = Just . negForm
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering sym_of CommonLogic = singletonList . symOf
71d35b6b5563817dfbe757ab9e3b9f018b2db491Thomas Hindoe Paaboel Andersen symmap_of CommonLogic = getSymbolMap -- returns the symbol map
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering sym_name CommonLogic = getSymbolName -- returns the name of a symbol
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering map_sen CommonLogic = mapSentence -- TODO
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance Syntax CommonLogic
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering SYMB_MAP_ITEMS
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poettering parse_basic_spec CommonLogic = Just basicSpec
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering parse_symb_items CommonLogic = Just symbItems
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering parse_symb_map_items CommonLogic = Just symbMapItems
cbe4216dd1b76f26460c553aefeeebf29bce221cLennart Poetteringinstance Logic CommonLogic
a0c888c78c419cd49c05ee6d226568e6fea0a4f3Lennart Poettering CommonLogicSL -- Sublogics
a0c888c78c419cd49c05ee6d226568e6fea0a4f3Lennart Poettering BASIC_SPEC -- basic_spec
6e0684729420912df019cc64d3f8a3c8290cc5f1Lennart Poettering TEXT -- sentence
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering SYMB_ITEMS -- symb_items
ae6a4bbf318e197813227e50c245a00de03784a2Lennart Poettering SYMB_MAP_ITEMS -- symb_map_items
ae6a4bbf318e197813227e50c245a00de03784a2Lennart Poettering Morphism -- morphism
019036a47fcd10fcf0286800d144c706f3773e2fLennart Poettering Symbol -- symbol
c3bc53e62459d7e566ffffeade41cd82bc6754f5Lennart Poettering Symbol -- raw_symbol
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poettering ProofTree -- proof_tree
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poettering all_sublogics CommonLogic = sublogics_all
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poettering empty_proof_tree CommonLogic = emptyProofTree
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poettering provers CommonLogic = []
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poettering omdoc_metatheory CommonLogic = Just clMetaTheory
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poettering export_senToOmdoc CommonLogic = exportSenToOmdoc
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poettering export_symToOmdoc CommonLogic = exportSymToOmdoc
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poettering omdocToSen CommonLogic = OMDocImport.omdocToSen
931851e8e492a4d2715e22dcde50a5e7ccef4b49Lennart Poettering omdocToSym CommonLogic = OMDocImport.omdocToSym
105e151299dc1208855380be2b22d0db2d66ebc6Lennart Poetteringinstance StaticAnalysis CommonLogic
a9da14e1e97ff774761966c2e1d83b0c6750b367Daniel Mack SYMB_MAP_ITEMS
d20b1667dbab8bccf69735523a0d5fc645e81b80Tom Gundersen basic_analysis CommonLogic = Just basicCommonLogicAnalysis
4667e00a61c2f60922558bc5e33ac9d3073a482cLennart Poettering empty_signature CommonLogic = emptySig
8300ba218e3cf5049496937be8bce10f22d09bbcTom Gundersen is_subsig CommonLogic = isSubSigOf
8300ba218e3cf5049496937be8bce10f22d09bbcTom Gundersen subsig_inclusion CommonLogic s = return . inclusionMap s
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poettering signature_union CommonLogic = sigUnion
be808ea083fa07271116b4519c3c27fd20c5f077Tom Gundersen symbol_to_raw CommonLogic = symbolToRaw
be808ea083fa07271116b4519c3c27fd20c5f077Tom Gundersen id_to_raw CommonLogic = idToRaw
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering matches CommonLogic = Symbol.matches
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering induced_from_morphism CommonLogic = inducedFromMorphism
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering add_symb_to_sign CommonLogic = addSymbToSign -- TODO
801ad6a6a9cd8fbd58b9f9c27f20dbb3c87d47ddLennart Poettering stat_symb_items CommonLogic = ()
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poettering stat_symb_map_items CommonLogic = ()
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering morphism_union CommonLogic = ()
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering signature_colimit CommonLogic = ()
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poetteringinstance SemiLatticeWithTop CommonLogicSL where
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poettering join = sublogics_max
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poetteringinstance MinSublogic CommonLogicSL BASIC_SPEC where
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poettering minSublogic = sl_basic_spec bottom
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poetteringinstance MinSublogic CommonLogicSL Sign where
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poettering minSublogic = sl_sig bottom
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance SublogicName CommonLogicSL where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering sublogicName = sublogics_name
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance MinSublogic CommonLogicSL TEXT where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering minSublogic t = sublogic_text bottom t
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance MinSublogic CommonLogicSL NAME where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering minSublogic = sublogic_name bottom
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance MinSublogic CommonLogicSL Symbol where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering minSublogic = sl_sym bottom
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance MinSublogic CommonLogicSL Morphism where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering minSublogic = sl_mor bottom
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poetteringinstance MinSublogic CommonLogicSL SYMB_MAP_ITEMS where
547973dea7abd6c124ff6c79fe2bbe322a7314aeLennart Poettering minSublogic = sl_symmap bottom
a5784c498598348354543b23b13ee8639a8b9e35Lennart Poetteringinstance MinSublogic CommonLogicSL SYMB_ITEMS where
a5784c498598348354543b23b13ee8639a8b9e35Lennart Poettering minSublogic = sl_symitems bottom
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance ProjectSublogic CommonLogicSL BASIC_SPEC where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering projectSublogic = prBasicSpec
c3bc53e62459d7e566ffffeade41cd82bc6754f5Lennart Poetteringinstance ProjectSublogicM CommonLogicSL NAME where
c3bc53e62459d7e566ffffeade41cd82bc6754f5Lennart Poettering projectSublogicM = prName
6e0684729420912df019cc64d3f8a3c8290cc5f1Lennart Poetteringinstance ProjectSublogicM CommonLogicSL SYMB_MAP_ITEMS where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering projectSublogicM = prSymMapM
ea12bcc78911fd3531955a799dbf6c5ac33bf567Daniel Mackinstance ProjectSublogicM CommonLogicSL SYMB_ITEMS where
ea12bcc78911fd3531955a799dbf6c5ac33bf567Daniel Mack projectSublogicM = prSymItemsM
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance ProjectSublogic CommonLogicSL Sign where
3b31df8301fd7dfb78bf9eaf9227d40c9bf12182Tom Gundersen projectSublogic = prSig
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poetteringinstance ProjectSublogic CommonLogicSL Morphism where
ec2c5e4398f9d65e5dfe61530f2556224733d1e6Lennart Poettering projectSublogic = prMor
c3bc53e62459d7e566ffffeade41cd82bc6754f5Lennart Poetteringinstance ProjectSublogicM CommonLogicSL Symbol where