Logic_Fpl.hs revision 19defe35cc864caeb98dd4ea1d429b1f989ecdff
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
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesMaintainer : Christian.Maeder@dfki.de
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesStability : provisional
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesPortability : non-portable
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesInstance of class Logic for FPL.
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes-}
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesmodule Fpl.Logic_Fpl where
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Logic.Logic
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Fpl.As
e8f95a682820a599fe41b22977010636be5c2717jimimport Fpl.Sign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Fpl.StatAna
e8f95a682820a599fe41b22977010636be5c2717jimimport Fpl.Morphism
1747d30b98aa1bdbc43994c02cd46ab4cb9319e4fieldingimport Fpl.ATC_Fpl ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport CASL.Sign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport CASL.Morphism
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport CASL.SymbolMapAnalysis
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport CASL.AS_Basic_CASL
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport CASL.Parse_AS_Basic
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport CASL.SimplifySen
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport CASL.SymbolParser
11f2c481e1d57bedb3f758565307501e9a2730ddtrawickimport CASL.Taxonomy
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport CASL.Logic_CASL ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesimport Common.DocUtils
5c0419d51818eb02045cf923a9fe456127a44c60wrowe
5c0419d51818eb02045cf923a9fe456127a44c60wrowedata Fpl = Fpl deriving Show
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholesinstance Language Fpl where
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes description _ = unlines
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes [ "logic of functional programs (FPL) as CASL extension" ]
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sf
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sfinstance SignExtension SignExt where
cd3bbd6d2df78d6c75e5d159a81ef8bdd5f70df9trawick isSubSignExtension = isSubFplSign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sfinstance Syntax Fpl FplBasicSpec SYMB_ITEMS SYMB_MAP_ITEMS where
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sf parse_basic_spec Fpl = Just $ basicSpec fplReservedWords
5bfaaf573bacb45c1cf290ce85ecc676587e8a64jim parse_symb_items Fpl = Just $ symbItems fplReservedWords
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sf parse_symb_map_items Fpl = Just $ symbMapItems fplReservedWords
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sf
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sfinstance Sentences Fpl FplForm FplSign FplMor Symbol where
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sf map_sen Fpl m = return . mapFplSen m
ab86c68ce36c715e93f403dde41d0b9c1522c8b0sf sym_of Fpl = symOf
bede2929837dfd23863ad4b39199c63126566d61jorton symmap_of Fpl = morphismToSymbMap
0f60998368b493f90120180a93fc2e1e74490872covener sym_name Fpl = symName
0f60998368b493f90120180a93fc2e1e74490872covener simplify_sen Fpl = simplifySen minFplTerm simplifyTermExt
0f60998368b493f90120180a93fc2e1e74490872covener print_sign Fpl = printSign pretty
0f60998368b493f90120180a93fc2e1e74490872covener
0f60998368b493f90120180a93fc2e1e74490872covenerinstance StaticAnalysis Fpl FplBasicSpec FplForm
0f60998368b493f90120180a93fc2e1e74490872covener SYMB_ITEMS SYMB_MAP_ITEMS
0f60998368b493f90120180a93fc2e1e74490872covener FplSign
0f60998368b493f90120180a93fc2e1e74490872covener FplMor
5bfaaf573bacb45c1cf290ce85ecc676587e8a64jim Symbol RawSymbol where
60284a9f9158baa60cc8ab4a69066404b1dcae7acovener basic_analysis Fpl = Just basicFplAnalysis
87587593f1a53030e840acc0dec6cc881022ea40covener stat_symb_map_items Fpl = statSymbMapItems
87587593f1a53030e840acc0dec6cc881022ea40covener stat_symb_items Fpl = statSymbItems
87587593f1a53030e840acc0dec6cc881022ea40covener
a81c0c1ae464b2063a21b45f80c9da8d89bb840ecovener symbol_to_raw Fpl = symbolToRaw
a81c0c1ae464b2063a21b45f80c9da8d89bb840ecovener id_to_raw Fpl = idToRaw
a81c0c1ae464b2063a21b45f80c9da8d89bb840ecovener matches Fpl = CASL.Morphism.matches
97cd2f98ad4abe68aaaba96b5bfc9ebf7109a2c1covener
97cd2f98ad4abe68aaaba96b5bfc9ebf7109a2c1covener empty_signature Fpl = emptySign emptyFplSign
97cd2f98ad4abe68aaaba96b5bfc9ebf7109a2c1covener signature_union Fpl s = return . addSig addFplSign s
97cd2f98ad4abe68aaaba96b5bfc9ebf7109a2c1covener intersection Fpl s = return . interSig interFplSign s
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes morphism_union Fpl = morphismUnion (const id) addFplSign
43997561b2302d13dee973998e77743a3ddd2374trawick final_union Fpl = finalUnion addFplSign
fa123db15501821e36e513afa78e839775ad2800covener is_subsig Fpl = isSubSig isSubFplSign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes subsig_inclusion Fpl = sigInclusion emptyMorExt
0568280364eb026393be492ebc732795c4934643jorton cogenerated_sign Fpl = cogeneratedSign emptyMorExt
0568280364eb026393be492ebc732795c4934643jorton generated_sign Fpl = generatedSign emptyMorExt
0568280364eb026393be492ebc732795c4934643jorton induced_from_morphism Fpl = inducedFromMorphism emptyMorExt
0568280364eb026393be492ebc732795c4934643jorton induced_from_to_morphism Fpl =
0568280364eb026393be492ebc732795c4934643jorton inducedFromToMorphism emptyMorExt isSubFplSign diffFplSign
0568280364eb026393be492ebc732795c4934643jorton theory_to_taxonomy Fpl = convTaxo
0568280364eb026393be492ebc732795c4934643jorton
0568280364eb026393be492ebc732795c4934643jortoninstance Logic Fpl ()
0568280364eb026393be492ebc732795c4934643jorton FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes FplSign
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes FplMor
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes Symbol RawSymbol () where
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes stability _ = Unstable
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes empty_proof_tree _ = ()
d5b12fe8ae917e654a33247fd4e59dc9e75170aebnicholes