Logic_CommonLogic.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringModule : $Header$
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringDescription : Instance of class Logic for common logic
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringCopyright : (c) Karl Luc, DFKI Bremen 2010
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringLicense : GPLv2 or higher, see LICENSE.txt
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringMaintainer : kluc@informatik.uni-bremen.de
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringStability : experimental
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringPortability : non-portable (imports Logic.Logic)
ee8c45689526ca973407cbb77bce7b96a062c40bLennart PoetteringInstance of class Logic for the common logic
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringmodule CommonLogic.Logic_CommonLogic where
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringimport qualified Data.Map as Map
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringdata CommonLogic = CommonLogic deriving Show
81fd1dd3a2cf4cc90a6898d562c9bb0fb238cbd7Tom Gunderseninstance Language CommonLogic where
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering description _ = "CommonLogic Logic\n"
d8500c53789eafefe28d4ace088bf4b912280bf9Tom Gunderseninstance Category Sign Morphism
9085f64a6694f2928c79fcce365edb1dca6937d4Lennart Poettering isInclusion = Map.null . propMap
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering legal_mor = isLegalMorphism
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering composeMorphisms = composeMor
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringinstance Sentences CommonLogic
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering negation CommonLogic = Just . negForm
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering sym_of CommonLogic = singletonList . symOf
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering symmap_of CommonLogic = getSymbolMap -- returns the symbol map
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering sym_name CommonLogic = getSymbolName -- returns the name of a symbol
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering map_sen CommonLogic = mapSentence -- TODO
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringinstance Syntax CommonLogic
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering SYMB_MAP_ITEMS
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering parse_basic_spec CommonLogic = Just basicSpec
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering parse_symb_items CommonLogic = Nothing -- Just symbItems -- TODO
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering parse_symb_map_items CommonLogic = Nothing -- Just symbMapItems -- TODO
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringinstance Logic CommonLogic
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering () -- Sublogics
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering BASIC_SPEC -- basic_spec
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering SENTENCE -- sentence
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering NAME -- symb_items
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering SYMB_MAP_ITEMS -- symb_map_items
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering Morphism -- morphism
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering Symbol -- symbol
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering Symbol -- raw_symbol
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering ProofTree -- proof_tree
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering empty_proof_tree CommonLogic = emptyProofTree
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering provers CommonLogic = []
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering omdoc_metatheory CommonLogic = Just clMetaTheory
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering export_senToOmdoc CommonLogic = exportSenToOmdoc
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering export_symToOmdoc CommonLogic = exportSymToOmdoc
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering omdocToSen CommonLogic = omdocToSen
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering omdocToSym CommonLogic = omdocToSym
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poetteringinstance StaticAnalysis CommonLogic
ee8c45689526ca973407cbb77bce7b96a062c40bLennart Poettering SYMB_MAP_ITEMS
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering basic_analysis CommonLogic = Just basicCommonLogicAnalysis
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering empty_signature CommonLogic = emptySig
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering is_subsig CommonLogic = isSubSigOf
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering signature_union CommonLogic = sigUnion
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering symbol_to_raw CommonLogic = symbolToRaw
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering id_to_raw CommonLogic = idToRaw
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering matches CommonLogic = Symbol.matches
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering induced_from_morphism CommonLogic = inducedFromMorphism -- TODO
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering induced_from_to_morphism CommonLogic = inducedFromToMorphism -- TODO
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering add_symb_to_sign CommonLogic = addSymbToSign -- TODO
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering stat_symb_items CommonLogic = ()
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering stat_symb_map_items CommonLogic = ()
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering morphism_union CommonLogic = ()
6d0c65ffb4f82e8c6dceb453919b3db54343fc27Lennart Poettering signature_colimit CommonLogic = ()