Logic_Fpl.hs revision a38f3d84e592184830fa308c5dab3f7c71e4464f
af1cb109bce240bcafe3823df022d6088cbfc438Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederModule : $Header$
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederDescription : logic instance for FPL
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2011
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederMaintainer : Christian.Maeder@dfki.de
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederStability : provisional
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederPortability : non-portable
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederInstance of class Logic for FPL.
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederdata Fpl = Fpl deriving Show
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederinstance Language Fpl where
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder description _ = unlines
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder [ "logic of functional programs (FPL) as CASL extension" ]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maedertype FplSign = Sign TermExt SignExt
9d3c461220f8076ef80ca48f7b0574ded9b23e7aChristian Maedertype FplMor = Morphism TermExt SignExt (DefMorExt SignExt)
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederinstance SignExtension SignExt
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederinstance Syntax Fpl FplBasicSpec SYMB_ITEMS SYMB_MAP_ITEMS where
af1cb109bce240bcafe3823df022d6088cbfc438Christian Maeder parse_basic_spec Fpl = Just $ basicSpec fplReservedWords
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder parse_symb_items Fpl = Just $ symbItems fplReservedWords
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder parse_symb_map_items Fpl = Just $ symbMapItems fplReservedWords
9d3c461220f8076ef80ca48f7b0574ded9b23e7aChristian Maederinstance Sentences Fpl FplForm FplSign FplMor Symbol where
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder sym_of Fpl = symOf
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder symmap_of Fpl = morphismToSymbMap
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder sym_name Fpl = symName
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder print_sign Fpl = printSign pretty
ce59e0cc5c7221245ed323290bfccbda4ee32dd9Christian Maederinstance StaticAnalysis Fpl FplBasicSpec FplForm
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Symbol RawSymbol where
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder stat_symb_map_items Fpl = statSymbMapItems
798a3d6fdcb8c17b0bc3502a150be75c9ec8799bChristian Maeder stat_symb_items Fpl = statSymbItems
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder symbol_to_raw Fpl = symbolToRaw
af1cb109bce240bcafe3823df022d6088cbfc438Christian Maeder id_to_raw Fpl = idToRaw
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder empty_signature Fpl = emptySign emptyFplSign
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder signature_union Fpl s = return . addSig addFplSign s
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder morphism_union Fpl = morphismUnion (const id) addFplSign
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder final_union Fpl = finalUnion addFplSign
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder is_subsig Fpl = isSubSig isSubFplSign
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder subsig_inclusion Fpl = sigInclusion emptyMorExt
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder cogenerated_sign Fpl = cogeneratedSign emptyMorExt
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder generated_sign Fpl = generatedSign emptyMorExt
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder induced_from_morphism Fpl = inducedFromMorphism emptyMorExt
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder theory_to_taxonomy Fpl = convTaxo
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederinstance Logic Fpl ()
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Symbol RawSymbol () where
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder stability _ = Unstable
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder empty_proof_tree _ = ()