55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Fpl/Logic_Fpl.hs
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederDescription : logic instance for FPL
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2011
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederMaintainer : Christian.Maeder@dfki.de
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederStability : provisional
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederPortability : non-portable
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian MaederInstance of class Logic for FPL.
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder-}
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maedermodule Fpl.Logic_Fpl where
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport Logic.Logic
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport Fpl.As
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport Fpl.Sign
c04cc42aa672aa49b45005e6eed77cc80e0d6ae0Christian Maederimport Fpl.StatAna
329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederimport Fpl.Morphism
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport Fpl.ATC_Fpl ()
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.Sign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.Morphism
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.SymbolMapAnalysis
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.AS_Basic_CASL
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.Parse_AS_Basic
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.SimplifySen
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.SymbolParser
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.Taxonomy
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederimport CASL.Logic_CASL ()
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
115e2751ba5bfd90a1a1954bd52d324eb9e6fca8mscodescuimport Common.DocUtils
115e2751ba5bfd90a1a1954bd52d324eb9e6fca8mscodescu
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederdata Fpl = Fpl deriving Show
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
ac4396c9f44a76c5c97925954ee49b4a91d8dd88Christian Maederinstance Language Fpl where
ac4396c9f44a76c5c97925954ee49b4a91d8dd88Christian Maeder description _ = unlines
ac4396c9f44a76c5c97925954ee49b4a91d8dd88Christian Maeder [ "logic of functional programs (FPL) as CASL extension" ]
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
c04cc42aa672aa49b45005e6eed77cc80e0d6ae0Christian Maederinstance SignExtension SignExt where
c04cc42aa672aa49b45005e6eed77cc80e0d6ae0Christian Maeder isSubSignExtension = isSubFplSign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
a65c6747c9acbbebc93baba7bae94d2e3d8cdafbTill Mossakowskiinstance Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
a38f3d84e592184830fa308c5dab3f7c71e4464fChristian Maeder parse_basic_spec Fpl = Just $ basicSpec fplReservedWords
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder parse_symb_items Fpl = Just $ symbItems fplReservedWords
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder parse_symb_map_items Fpl = Just $ symbMapItems fplReservedWords
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederinstance Sentences Fpl FplForm FplSign FplMor Symbol where
329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder map_sen Fpl m = return . mapFplSen m
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder sym_of Fpl = symOf
115e2751ba5bfd90a1a1954bd52d324eb9e6fca8mscodescu symKind Fpl = show . pretty . symbolKind . symbType
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder symmap_of Fpl = morphismToSymbMap
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder sym_name Fpl = symName
4bbd808612c2580ae6e0495a155997a6bb47ecf3Christian Maeder simplify_sen Fpl = simplifySen minFplTerm simplifyTermExt . addBuiltins
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederinstance StaticAnalysis Fpl FplBasicSpec FplForm
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder SYMB_ITEMS SYMB_MAP_ITEMS
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder FplSign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder FplMor
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder Symbol RawSymbol where
c04cc42aa672aa49b45005e6eed77cc80e0d6ae0Christian Maeder basic_analysis Fpl = Just basicFplAnalysis
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder stat_symb_map_items Fpl = statSymbMapItems
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder stat_symb_items Fpl = statSymbItems
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder symbol_to_raw Fpl = symbolToRaw
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder id_to_raw Fpl = idToRaw
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder matches Fpl = CASL.Morphism.matches
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder empty_signature Fpl = emptySign emptyFplSign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder signature_union Fpl s = return . addSig addFplSign s
d9be582b00d420e2fe0737fcb07c9aa3d235a774Christian Maeder signatureDiff Fpl s = return . diffSig diffFplSign s
19defe35cc864caeb98dd4ea1d429b1f989ecdffChristian Maeder intersection Fpl s = return . interSig interFplSign s
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder morphism_union Fpl = plainMorphismUnion addFplSign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder final_union Fpl = finalUnion addFplSign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder is_subsig Fpl = isSubSig isSubFplSign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder subsig_inclusion Fpl = sigInclusion emptyMorExt
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder cogenerated_sign Fpl = cogeneratedSign emptyMorExt
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder generated_sign Fpl = generatedSign emptyMorExt
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder induced_from_morphism Fpl = inducedFromMorphism emptyMorExt
19defe35cc864caeb98dd4ea1d429b1f989ecdffChristian Maeder induced_from_to_morphism Fpl =
19defe35cc864caeb98dd4ea1d429b1f989ecdffChristian Maeder inducedFromToMorphism emptyMorExt isSubFplSign diffFplSign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder theory_to_taxonomy Fpl = convTaxo
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maederinstance Logic Fpl ()
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder FplSign
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder FplMor
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder Symbol RawSymbol () where
cdcf5d3f1e79d8798d77efa29e6193af94ea0604Till Mossakowski stability _ = Experimental
bff4b3f816be4c1e1d8ded76f1d5af786839e1a9Christian Maeder empty_proof_tree _ = ()