Analysis.hs revision ece3b1a5353a9af3c966a1d5453594ed35334f7b
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeModule : $Header$
9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Basic analysis for propositional logic extended with QBFs
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : jonathan.von_schroeder@dfki.de
b72a390042c19e630cf221494b60c9df2a60d187Dominik LueckeStability : experimental
b72a390042c19e630cf221494b60c9df2a60d187Dominik LueckePortability : portable
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeBasic and static analysis for propositional logic
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke <http://en.wikipedia.org/wiki/Propositional_logic>
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke basicPropositionalAnalysis
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke , mkStatSymbItems
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke , mkStatSymbMapItem
da955132262baab309a50fdffe228c9efe68251dCui Jian , inducedFromMorphism
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , inducedFromToMorphism
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , signatureColimit
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maederimport qualified Common.AS_Annotation as AS_Anno
16e124196c6b204769042028c74f533509c9b5d3Christian Maederimport qualified Common.GlobalAnnotations as GlobalAnnos
f90884915ff10ae83f59e709c68824de834e64f5Dominik Lueckeimport qualified Common.Id as Id
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeimport qualified Common.Result as Result
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeimport qualified Data.List as List
f90884915ff10ae83f59e709c68824de834e64f5Dominik Lueckeimport qualified Data.Map as Map
5b9f5c1b3592b99fc74d3438740ebcf9eb4c94beDominik Lueckeimport qualified Data.Set as Set
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Lueckeimport qualified QBF.AS_BASIC_QBF as AS_BASIC
5b9f5c1b3592b99fc74d3438740ebcf9eb4c94beDominik Lueckeimport qualified QBF.Morphism as Morphism
08056875f5f633ef432598d5245ea41c112d2178Dominik Lueckeimport qualified QBF.Symbol as Symbol
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke-- | Datatype for formulas with diagnosis data
da955132262baab309a50fdffe228c9efe68251dCui Jiandata DIAGFORM = DiagForm
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder-- | Formula annotated with a number
b72a390042c19e630cf221494b60c9df2a60d187Dominik Lueckedata NUMFORM = NumForm
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder nfformula :: AS_Anno.Annoted AS_BASIC.FORMULA
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke , nfnum :: Integer
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederdata TESTSIG = TestSig
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke , occurence :: Int
da955132262baab309a50fdffe228c9efe68251dCui Jian , tdiagnosis :: [Result.Diagnosis]
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-- | Retrieves the signature out of a basic spec
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> Sign.Sign -- Input Signature
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> TESTSIG -- Output Signature
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckemakeSig (AS_BASIC.BasicSpec spec) sig = List.foldl retrieveBasicItem
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke TestSig { msign = sig
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke , occurence = 0
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke , tdiagnosis = []
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke-- Helper for makeSig
08056875f5f633ef432598d5245ea41c112d2178Dominik LueckeretrieveBasicItem ::
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder TESTSIG -- Input Signature
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder -> AS_Anno.Annoted AS_BASIC.BASICITEMS -- Input Item
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke -> TESTSIG -- Output Signature
08056875f5f633ef432598d5245ea41c112d2178Dominik LueckeretrieveBasicItem tsig x =
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder occ = occurence tsig
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke (\ asig ax -> TestSig {
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke msign = Sign.addToSig (msign asig)
0859769b65851f4c06d6d32fac084b0f4db56c94Christian Maeder , occurence = occ
da955132262baab309a50fdffe228c9efe68251dCui Jian , tdiagnosis = tdiagnosis tsig ++
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke (\ asig ax -> TestSig {
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke msign = Sign.addToSig (msign asig)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , occurence = occ
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , tdiagnosis = tdiagnosis tsig ++
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder "Definition of proposition " ++
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder show (pretty ax) ++
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder " after first axiom"
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (AS_BASIC.AxiomItems _) -> TestSig { msign = msign tsig
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , occurence = occ + 1
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , tdiagnosis = tdiagnosis tsig ++
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder "First axiom"
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- | Retrieve the formulas out of a basic spec
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedermakeFormulas ::
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder -> [DIAGFORM]
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedermakeFormulas (AS_BASIC.BasicSpec bspec) sig =
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- Helper for makeFormulas
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaederretrieveFormulaItem ::
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder -> [DIAGFORM]
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaederretrieveFormulaItem axs x sig =
(AS_BASIC.PredDecl _) -> axs
(AS_BASIC.AxiomItems ax) ->
List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
label = AS_Anno.getRLabel x
-> Sign.Sign
, diagnosis = Result.Diag
, Result.diagString = "All fine"
, Result.diagPos = lnum
, diagnosis = Result.Diag
, Result.diagPos = lnum
nakedFormula = AS_Anno.item f
isLegal = Sign.isSubSigOf varsOfFormula sign
difference = Sign.sigDiff varsOfFormula sign
lnum = AS_Anno.opt_pos f
makeNamed f i = (AS_Anno.makeNamed (if label == "" then "Ax_" ++ show i
else label) $ AS_Anno.item f)
{ AS_Anno.isAxiom = not isTheorem }
label = AS_Anno.getRLabel f
annos = AS_Anno.r_annos f
isImplies = foldl (\ y x -> AS_Anno.isImplies x || y) False annos
isImplied = foldl (\ y x -> AS_Anno.isImplied x || y) False annos
propsOfFormula (AS_BASIC.Negation form _) = propsOfFormula form
Id.simpleIdToId x }
(\ sig frm -> Sign.unite sig
(\ sig frm -> Sign.unite sig
propsOfFormula (AS_BASIC.ForAll xs f _) = sigDiff
propsOfFormula (AS_BASIC.Exists xs f _) = sigDiff
Result.Result diags $ if exErrs then Nothing else
$ Set.difference (items sigItems) $ items sig
exErrs = Result.hasErrors diags
mkStatSymbMapItem :: [AS_BASIC.SYMBMAPITEMS]
Result.diags = []
, Result.maybeResult = Just $
AS_BASIC.SymbMapItems sitem _ ->
Map.union smap $ statSymbMapItem sitem
statSymbMapItem :: [AS_BASIC.SYMBORMAP]
AS_BASIC.SymbMap s1 s2 _
-> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
mkStatSymbItems a = Result.Result
Result.diags = []
, Result.maybeResult = Just $ statSymbItems a
symbItemsToSymbol (AS_BASIC.SymbItems syms _) = map symbToSymbol syms
symbToSymbol (AS_BASIC.SymbId tok) =
-> Sign.Sign
Result.diags = []
sigItems = Sign.items sig
Set.fold (
symOf = Symbol.Symbol
{ Symbol.symName = x }
y = Symbol.symName
$ Symbol.applySymMap imap symOf
Map.insert x y
Map.empty sigItems
Morphism.source = sig
, Morphism.propMap = pMap
{Sign.items =
$ Sign.items sig
sigItems = Sign.items sig
Set.fold (
symOf = Symbol.Symbol
{ Symbol.symName = x }
y = Symbol.symName
Map.insert x y
Map.empty sigItems
targetSig = Sign.Sign
{Sign.items =
(Morphism.applyMap pMap)
$ Sign.items sig
isSub = Sign.items targetSig
Sign.items tSig
Result.diags = []
Just Morphism.Morphism
Morphism.source = sig
, Morphism.propMap = pMap
, Morphism.target = tSig
, Result.maybeResult = Nothing
Map.fromList $ map (\ (i, n) ->
(i, Morphism.Morphism {
Morphism.source = n,
Morphism.target = cSig,
Morphism.propMap = maps Map.! i