Logic_Fpl.hs revision d6c6b2543c509ec7f6213e4cba675d96304a7fd6
842ae4bd224140319ae7feec1872b93dfd491143fielding{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
842ae4bd224140319ae7feec1872b93dfd491143fielding{- |
842ae4bd224140319ae7feec1872b93dfd491143fieldingModule : $Header$
842ae4bd224140319ae7feec1872b93dfd491143fieldingDescription : logic instance for FPL
842ae4bd224140319ae7feec1872b93dfd491143fieldingCopyright : (c) Christian Maeder, DFKI GmbH 2011
842ae4bd224140319ae7feec1872b93dfd491143fieldingLicense : GPLv2 or higher, see LICENSE.txt
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbMaintainer : Christian.Maeder@dfki.de
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndStability : provisional
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbPortability : non-portable
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndInstance of class Logic for FPL.
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd-}
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd
ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndmodule Fpl.Logic_Fpl where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Logic.Logic
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
9d129b55f5a43abf43865c6b0eb6dd19bc22aba8ianhimport Fpl.As
9d129b55f5a43abf43865c6b0eb6dd19bc22aba8ianhimport Fpl.Sign
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Fpl.StatAna
9d129b55f5a43abf43865c6b0eb6dd19bc22aba8ianhimport Fpl.Morphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Fpl.ATC_Fpl ()
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.Sign
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.Morphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.SymbolMapAnalysis
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.AS_Basic_CASL
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.Parse_AS_Basic
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.SimplifySen
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.SymbolParser
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.Taxonomy
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport CASL.Logic_CASL ()
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport Common.DocUtils
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
a72211e92bab814bfa28ee086ca9b2a1a6095c92chrisddata Fpl = Fpl deriving Show
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Language Fpl where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb description _ = unlines
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb [ "logic of functional programs (FPL) as CASL extension" ]
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance SignExtension SignExt where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb isSubSignExtension = isSubFplSign
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Syntax Fpl FplBasicSpec SYMB_ITEMS SYMB_MAP_ITEMS where
f888346b48f5e5b5e3f0a47dedb8cefd2759a4e2gregames parse_basic_spec Fpl = Just $ basicSpec fplReservedWords
750d12c59545dbbac70390988de94f7e901b08f2niq parse_symb_items Fpl = Just $ symbItems fplReservedWords
82632a19f2f9c346fee2b28a65920ba9737b3973minfrin parse_symb_map_items Fpl = Just $ symbMapItems fplReservedWords
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinstance Sentences Fpl FplForm FplSign FplMor Symbol where
db455cbc662c98dbbf53175393c50086ff63370cchrisd map_sen Fpl m = return . mapFplSen m
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sym_of Fpl = symOf
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb symmap_of Fpl = morphismToSymbMap
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sym_name Fpl = symName
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb simplify_sen Fpl = simplifySen minFplTerm simplifyTermExt . addBuiltins
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb print_sign Fpl = printSign pretty
7184de27ec1d62a83c41cdeac0953ca9fd661e8csf
7184de27ec1d62a83c41cdeac0953ca9fd661e8csfinstance StaticAnalysis Fpl FplBasicSpec FplForm
7184de27ec1d62a83c41cdeac0953ca9fd661e8csf SYMB_ITEMS SYMB_MAP_ITEMS
36ef8f77bffe75d1aa327882be1b5bdbe2ff567asf FplSign
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb FplMor
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Symbol RawSymbol where
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz basic_analysis Fpl = Just basicFplAnalysis
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz stat_symb_map_items Fpl = statSymbMapItems
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz stat_symb_items Fpl = statSymbItems
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz symbol_to_raw Fpl = symbolToRaw
18b5268e013574026b2503b1641baf3299045f45sf id_to_raw Fpl = idToRaw
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz matches Fpl = CASL.Morphism.matches
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz empty_signature Fpl = emptySign emptyFplSign
60a765cccbd3f3b5997b65b0034220c79f78369etrawick signature_union Fpl s = return . addSig addFplSign s
f4ca9f6f002fece336168a16355434ca966f96a9trawick intersection Fpl s = return . interSig interFplSign s
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb morphism_union Fpl = plainMorphismUnion addFplSign
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb final_union Fpl = finalUnion addFplSign
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb is_subsig Fpl = isSubSig isSubFplSign
4f9c22c4f27571d54197be9674e1fc0d528192aestriker subsig_inclusion Fpl = sigInclusion emptyMorExt
a2a0abd88b19e042a3eb2a9fa1702c25ad51303dwrowe cogenerated_sign Fpl = cogeneratedSign emptyMorExt
4f9c22c4f27571d54197be9674e1fc0d528192aestriker generated_sign Fpl = generatedSign emptyMorExt
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb induced_from_morphism Fpl = inducedFromMorphism emptyMorExt
4f9c22c4f27571d54197be9674e1fc0d528192aestriker induced_from_to_morphism Fpl =
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb inducedFromToMorphism emptyMorExt isSubFplSign diffFplSign
4f9c22c4f27571d54197be9674e1fc0d528192aestriker theory_to_taxonomy Fpl = convTaxo
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb
4f9c22c4f27571d54197be9674e1fc0d528192aestrikerinstance Logic Fpl ()
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS
4f9c22c4f27571d54197be9674e1fc0d528192aestriker FplSign
18b5268e013574026b2503b1641baf3299045f45sf FplMor
18b5268e013574026b2503b1641baf3299045f45sf Symbol RawSymbol () where
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb stability _ = Unstable
4f9c22c4f27571d54197be9674e1fc0d528192aestriker empty_proof_tree _ = ()
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb