Logic_Fpl.hs revision cdcf5d3f1e79d8798d77efa29e6193af94ea0604
a530dde7009b0a808300c420def741354a4d13d2Martin Kühl{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
a530dde7009b0a808300c420def741354a4d13d2Martin KühlDescription : logic instance for FPL
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Christian Maeder, DFKI GmbH 2011
a530dde7009b0a808300c420def741354a4d13d2Martin KühlLicense : GPLv2 or higher, see LICENSE.txt
a530dde7009b0a808300c420def741354a4d13d2Martin KühlMaintainer : Christian.Maeder@dfki.de
a530dde7009b0a808300c420def741354a4d13d2Martin KühlStability : provisional
a530dde7009b0a808300c420def741354a4d13d2Martin KühlPortability : non-portable
a530dde7009b0a808300c420def741354a4d13d2Martin KühlInstance of class Logic for FPL.
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescodata Fpl = Fpl deriving Show
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoinstance Language Fpl where
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco description _ = unlines
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco [ "logic of functional programs (FPL) as CASL extension" ]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoinstance SignExtension SignExt where
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco isSubSignExtension = isSubFplSign
223be434693e8c97e2522ac19155a284b3536035Adrián Riescoinstance Syntax Fpl FplBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco parse_basic_spec Fpl = Just $ basicSpec fplReservedWords
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco parse_symb_items Fpl = Just $ symbItems fplReservedWords
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco parse_symb_map_items Fpl = Just $ symbMapItems fplReservedWords
223be434693e8c97e2522ac19155a284b3536035Adrián Riescoinstance Sentences Fpl FplForm FplSign FplMor Symbol where
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco map_sen Fpl m = return . mapFplSen m
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sym_of Fpl = symOf
51c15129e8118fed5c33c334f8df82619ce98e7dAdrián Riesco symmap_of Fpl = morphismToSymbMap
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco sym_name Fpl = symName
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco simplify_sen Fpl = simplifySen minFplTerm simplifyTermExt . addBuiltins
0f35e410ce3d3202f6769e9d139ad26d1de69b8eAdrián Riescoinstance StaticAnalysis Fpl FplBasicSpec FplForm
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco SYMB_ITEMS SYMB_MAP_ITEMS
6d498b6f56ed9f71cced898b6c42fb48f6e60583Adrián Riesco Symbol RawSymbol where
6e121321775373fe11161d23c541437456df19b4Adrián Riesco basic_analysis Fpl = Just basicFplAnalysis
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco stat_symb_map_items Fpl = statSymbMapItems
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco stat_symb_items Fpl = statSymbItems
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco symbol_to_raw Fpl = symbolToRaw
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco id_to_raw Fpl = idToRaw
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco empty_signature Fpl = emptySign emptyFplSign
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco signature_union Fpl s = return . addSig addFplSign s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco signatureDiff Fpl s = return . diffSig diffFplSign s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco intersection Fpl s = return . interSig interFplSign s
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco morphism_union Fpl = plainMorphismUnion addFplSign
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder final_union Fpl = finalUnion addFplSign
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco is_subsig Fpl = isSubSig isSubFplSign
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco subsig_inclusion Fpl = sigInclusion emptyMorExt
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco cogenerated_sign Fpl = cogeneratedSign emptyMorExt
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco generated_sign Fpl = generatedSign emptyMorExt
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco induced_from_morphism Fpl = inducedFromMorphism emptyMorExt
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco induced_from_to_morphism Fpl =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco inducedFromToMorphism emptyMorExt isSubFplSign diffFplSign
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco theory_to_taxonomy Fpl = convTaxo
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riescoinstance Logic Fpl ()
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco FplBasicSpec FplForm SYMB_ITEMS SYMB_MAP_ITEMS
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Symbol RawSymbol () where
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco stability _ = Experimental
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco empty_proof_tree _ = ()