4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Propositional/Analysis.hs
9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Basic analysis for propositional logic
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeCopyright : (c) Dominik Luecke, Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : luecke@informatik.uni-bremen.de
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeStability : experimental
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckePortability : portable
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeBasic and static analysis for propositional logic
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke Ref.
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke <http://en.wikipedia.org/wiki/Propositional_logic>
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-}
da955132262baab309a50fdffe228c9efe68251dCui Jian
da955132262baab309a50fdffe228c9efe68251dCui Jianmodule Propositional.Analysis
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder ( basicPropositionalAnalysis
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , mkStatSymbItems
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , mkStatSymbMapItem
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , inducedFromMorphism
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , inducedFromToMorphism
abb3850e1a3b30fc05a072a371c77395b3b40927Mihai Codescu , signatureColimit
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , pROPsen_analysis
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke )
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke where
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport Common.ExtSign
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport Common.Lib.Graph
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport Common.SetColimit
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport Data.Graph.Inductive.Graph
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maederimport Propositional.Sign as Sign
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Common.AS_Annotation as AS_Anno
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport qualified Common.GlobalAnnotations as GlobalAnnos
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Common.Id as Id
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport qualified Common.Result as Result
548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckeimport qualified Data.List as List
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Lueckeimport qualified Data.Map as Map
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport qualified Data.Set as Set
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Lueckeimport qualified Propositional.Morphism as Morphism
c3f7e132e0c214b755c6c4b485f4748c4dd1595cChristian Maederimport qualified Propositional.Symbol as Symbol
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke-- | Datatype for formulas with diagnosis data
da955132262baab309a50fdffe228c9efe68251dCui Jiandata DIAG_FORM = DiagForm
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke {
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder formula :: AS_Anno.Named AS_BASIC.FORMULA,
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke diagnosis :: Result.Diagnosis
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke }
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke-- | Formula annotated with a number
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Lueckedata NUM_FORM = NumForm
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke {
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder nfformula :: AS_Anno.Annoted AS_BASIC.FORMULA
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , nfnum :: Integer
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke }
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Lueckedata TEST_SIG = TestSig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke msign :: Sign.Sign
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke , occurence :: Int
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke , tdiagnosis :: [Result.Diagnosis]
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke }
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- | Retrieves the signature out of a basic spec
da955132262baab309a50fdffe228c9efe68251dCui JianmakeSig ::
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke AS_BASIC.BASIC_SPEC -- Input SPEC
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke -> Sign.Sign -- Input Signature
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke -> TEST_SIG -- Output Signature
da955132262baab309a50fdffe228c9efe68251dCui JianmakeSig (AS_BASIC.Basic_spec spec) sig = List.foldl retrieveBasicItem
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder TestSig { msign = sig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , occurence = 0
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke , tdiagnosis = []
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder }
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke spec
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- Helper for makeSig
da955132262baab309a50fdffe228c9efe68251dCui JianretrieveBasicItem ::
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke TEST_SIG -- Input Signature
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder -> AS_Anno.Annoted AS_BASIC.BASIC_ITEMS -- Input Item
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke -> TEST_SIG -- Output Signature
da955132262baab309a50fdffe228c9efe68251dCui JianretrieveBasicItem tsig x =
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke let
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke occ = occurence tsig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder nocc = occ == 0
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke in
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder case AS_Anno.item x of
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder AS_BASIC.Pred_decl apred -> List.foldl (\ asig ax -> TestSig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , occurence = occ
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , tdiagnosis = tdiagnosis tsig ++
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder [ Result.Diag
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { Result.diagKind = if nocc then Result.Hint else Result.Error
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Result.diagString = if nocc then "All fine" else
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder "Definition of proposition " ++ show (pretty ax)
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder ++ " after first axiom"
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Result.diagPos = AS_Anno.opt_pos x }]
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder }) tsig $ (\ (AS_BASIC.Pred_item xs _) -> xs) apred
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder AS_BASIC.Axiom_items _ -> TestSig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { msign = msign tsig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , occurence = occ + 1
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , tdiagnosis = tdiagnosis tsig ++
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder [ Result.Diag
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { Result.diagKind = Result.Hint
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Result.diagString = "First axiom"
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Result.diagPos = AS_Anno.opt_pos x }]
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder }
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- | Retrieve the formulas out of a basic spec
da955132262baab309a50fdffe228c9efe68251dCui JianmakeFormulas ::
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke AS_BASIC.BASIC_SPEC
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> Sign.Sign
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> [DIAG_FORM]
da955132262baab309a50fdffe228c9efe68251dCui JianmakeFormulas (AS_BASIC.Basic_spec bspec) sig =
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- Helper for makeFormulas
da955132262baab309a50fdffe228c9efe68251dCui JianretrieveFormulaItem ::
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke [DIAG_FORM]
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder -> AS_Anno.Annoted AS_BASIC.BASIC_ITEMS
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> Sign.Sign
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke -> [DIAG_FORM]
da955132262baab309a50fdffe228c9efe68251dCui JianretrieveFormulaItem axs x sig =
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder case AS_Anno.item x of
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder AS_BASIC.Pred_decl _ -> axs
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder AS_BASIC.Axiom_items ax ->
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-- Number formulae
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaedernumberFormulae :: [AS_Anno.Annoted AS_BASIC.FORMULA] -> Integer -> [NUM_FORM]
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckenumberFormulae [] _ = []
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaedernumberFormulae (x : xs) i
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder | label == "" = NumForm {nfformula = x, nfnum = i}
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder : numberFormulae xs (i + 1)
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder | otherwise = NumForm {nfformula = x, nfnum = 0} : numberFormulae xs i
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke where
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke label = AS_Anno.getRLabel x
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder-- Add a formula to a named list of formulas
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckeaddFormula :: [DIAG_FORM]
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke -> NUM_FORM
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> Sign.Sign
da955132262baab309a50fdffe228c9efe68251dCui Jian -> [DIAG_FORM]
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik LueckeaddFormula formulae nf sign
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder | isLegal = formulae ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke [DiagForm
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke {
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder formula = makeNamed f i
da955132262baab309a50fdffe228c9efe68251dCui Jian , diagnosis = Result.Diag
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke Result.diagKind = Result.Hint
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke , Result.diagString = "All fine"
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Result.diagPos = lnum
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke }
da955132262baab309a50fdffe228c9efe68251dCui Jian }]
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder | otherwise = formulae ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke [DiagForm
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke {
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder formula = makeNamed f i
da955132262baab309a50fdffe228c9efe68251dCui Jian , diagnosis = Result.Diag
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { Result.diagKind = Result.Error
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Result.diagString = "Unknown propositions "
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder ++ show (pretty difference)
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke ++ " in formula "
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder ++ show (pretty nakedFormula)
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Result.diagPos = lnum
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder }
da955132262baab309a50fdffe228c9efe68251dCui Jian }]
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke where
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder f = nfformula nf
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder i = nfnum nf
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder nakedFormula = AS_Anno.item f
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke varsOfFormula = propsOfFormula nakedFormula
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder isLegal = Sign.isSubSigOf varsOfFormula sign
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder difference = Sign.sigDiff varsOfFormula sign
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder lnum = AS_Anno.opt_pos f
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-- generates a named formula
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaedermakeNamed :: AS_Anno.Annoted AS_BASIC.FORMULA -> Integer
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder -> AS_Anno.Named AS_BASIC.FORMULA
61091743da1a9ed6dfd5e077fdcc972553358962Christian MaedermakeNamed f i = (AS_Anno.makeNamed (if label == "" then "Ax_" ++ show i
61091743da1a9ed6dfd5e077fdcc972553358962Christian Maeder else label) $ AS_Anno.item f)
61091743da1a9ed6dfd5e077fdcc972553358962Christian Maeder { AS_Anno.isAxiom = not isTheorem }
da955132262baab309a50fdffe228c9efe68251dCui Jian where
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke label = AS_Anno.getRLabel f
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke annos = AS_Anno.r_annos f
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder isImplies = foldl (\ y x -> AS_Anno.isImplies x || y) False annos
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder isImplied = foldl (\ y x -> AS_Anno.isImplied x || y) False annos
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke isTheorem = isImplies || isImplied
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-- Retrives the signature of a formula
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula :: AS_BASIC.FORMULA -> Sign.Sign
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.Negation form _) = propsOfFormula form
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederpropsOfFormula (AS_BASIC.Implication form1 form2 _) =
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder Sign.unite (propsOfFormula form1) (propsOfFormula form2)
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederpropsOfFormula (AS_BASIC.Equivalence form1 form2 _) =
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder Sign.unite (propsOfFormula form1) (propsOfFormula form2)
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederpropsOfFormula (AS_BASIC.True_atom _) = Sign.emptySig
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.False_atom _) = Sign.emptySig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederpropsOfFormula (AS_BASIC.Predication x) = Sign.Sign
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { Sign.items = Set.singleton $ Id.simpleIdToId x }
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederpropsOfFormula (AS_BASIC.Conjunction xs _) = List.foldl
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder (\ sig frm -> Sign.unite sig $ propsOfFormula frm) Sign.emptySig xs
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederpropsOfFormula (AS_BASIC.Disjunction xs _) = List.foldl
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder (\ sig frm -> Sign.unite sig $ propsOfFormula frm) Sign.emptySig xs
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder-- Basic analysis for propositional logic
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaederbasicPropositionalAnalysis
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder :: (AS_BASIC.BASIC_SPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder -> Result.Result (AS_BASIC.BASIC_SPEC,
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder ExtSign Sign.Sign Symbol.Symbol,
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder [AS_Anno.Named AS_BASIC.FORMULA])
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaederbasicPropositionalAnalysis (bs, sig, _) =
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder Result.Result diags $ if exErrs then Nothing else
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder Just (bs, ExtSign sigItems declaredSyms, formulae)
da955132262baab309a50fdffe228c9efe68251dCui Jian where
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder bsSig = makeSig bs sig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder sigItems = msign bsSig
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder declaredSyms = Set.map Symbol.Symbol
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder $ Set.difference (items sigItems) $ items sig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder bsForm = makeFormulas bs sigItems
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder formulae = map formula bsForm
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder diags = map diagnosis bsForm ++ tdiagnosis bsSig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder exErrs = Result.hasErrors diags
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke-- | Static analysis for symbol maps
da955132262baab309a50fdffe228c9efe68251dCui JianmkStatSymbMapItem :: [AS_BASIC.SYMB_MAP_ITEMS]
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckemkStatSymbMapItem xs =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke Result.Result
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke Result.diags = []
da955132262baab309a50fdffe228c9efe68251dCui Jian , Result.maybeResult = Just $
da955132262baab309a50fdffe228c9efe68251dCui Jian foldl
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke (
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke \ smap x ->
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke case x of
da955132262baab309a50fdffe228c9efe68251dCui Jian AS_BASIC.Symb_map_items sitem _ ->
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke Map.union smap $ statSymbMapItem sitem
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke )
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke Map.empty
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke xs
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckestatSymbMapItem :: [AS_BASIC.SYMB_OR_MAP]
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke -> Map.Map Symbol.Symbol Symbol.Symbol
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederstatSymbMapItem =
da955132262baab309a50fdffe228c9efe68251dCui Jian foldl
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke (
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke \ mmap x ->
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke case x of
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder AS_BASIC.Symb sym ->
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder Map.insert (symbToSymbol sym) (symbToSymbol sym) mmap
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder AS_BASIC.Symb_map s1 s2 _ ->
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke )
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke Map.empty
da955132262baab309a50fdffe228c9efe68251dCui Jian
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke-- | Retrieve raw symbols
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckemkStatSymbItems :: [AS_BASIC.SYMB_ITEMS] -> Result.Result [Symbol.Symbol]
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckemkStatSymbItems a = Result.Result
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke Result.diags = []
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke , Result.maybeResult = Just $ statSymbItems a
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckestatSymbItems :: [AS_BASIC.SYMB_ITEMS] -> [Symbol.Symbol]
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederstatSymbItems = concatMap symbItemsToSymbol
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckesymbItemsToSymbol :: AS_BASIC.SYMB_ITEMS -> [Symbol.Symbol]
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckesymbItemsToSymbol (AS_BASIC.Symb_items syms _) = map symbToSymbol syms
da955132262baab309a50fdffe228c9efe68251dCui Jian
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckesymbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol
da955132262baab309a50fdffe228c9efe68251dCui JiansymbToSymbol (AS_BASIC.Symb_id tok) =
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder Symbol.Symbol {Symbol.symName = Id.simpleIdToId tok}
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaedermakePMap :: Map.Map Symbol.Symbol Symbol.Symbol -> Sign.Sign
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder -> Map.Map Id.Id Id.Id
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaedermakePMap imap sig = Set.fold ( \ x ->
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder let symOf = Symbol.Symbol { Symbol.symName = x }
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder y = Symbol.symName $ Symbol.applySymMap imap symOf
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder in Map.insert x y ) Map.empty $ Sign.items sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke-- | Induce a signature morphism from a source signature and a raw symbol map
da955132262baab309a50fdffe228c9efe68251dCui JianinducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
da955132262baab309a50fdffe228c9efe68251dCui Jian -> Sign.Sign
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke -> Result.Result Morphism.Morphism
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian MaederinducedFromMorphism imap sig = let pMap = makePMap imap sig in
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder return
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke Morphism.Morphism
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { Morphism.source = sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke , Morphism.propMap = pMap
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Morphism.target = Sign.Sign
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { Sign.items = Set.map (Morphism.applyMap pMap)
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder $ Sign.items sig }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke-- | Induce a signature morphism from a source signature and a raw symbol map
da955132262baab309a50fdffe228c9efe68251dCui JianinducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder -> ExtSign Sign.Sign Symbol.Symbol
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder -> ExtSign Sign.Sign Symbol.Symbol
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke -> Result.Result Morphism.Morphism
67869d63d1725c79e4c07b51acd466a31932b275Christian MaederinducedFromToMorphism imap (ExtSign sig _) (ExtSign tSig _) =
da955132262baab309a50fdffe228c9efe68251dCui Jian let
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke sigItems = Sign.items sig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder pMap :: Map.Map Id.Id Id.Id
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder pMap = Set.fold ( \ x ->
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder let symOf = Symbol.Symbol { Symbol.symName = x }
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder y = Symbol.symName $ Symbol.applySymMap imap symOf
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder in Map.insert x y ) Map.empty sigItems
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke targetSig = Sign.Sign
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { Sign.items = Set.map (Morphism.applyMap pMap)
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder $ Sign.items sig }
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder isSub = Sign.items targetSig `Set.isSubsetOf` Sign.items tSig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder in if isSub then return Morphism.Morphism
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder { Morphism.source = sig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Morphism.propMap = makePMap imap sig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder , Morphism.target = tSig
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder }
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder else fail "Incompatible mapping"
abb3850e1a3b30fc05a072a371c77395b3b40927Mihai Codescu
abb3850e1a3b30fc05a072a371c77395b3b40927Mihai CodescusignatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
abb3850e1a3b30fc05a072a371c77395b3b40927Mihai Codescu -> Result.Result (Sign.Sign, Map.Map Int Morphism.Morphism)
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian MaedersignatureColimit graph = do
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder let graph1 = nmap Sign.items $ emap (\ (x, y) -> (x, Morphism.propMap y)) graph
803425dfe6a5da41b9cea480788980fa104545adMihai Codescu (set, maps) = addIntToSymbols $ computeColimitSet graph1
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder cSig = Sign.Sign {Sign.items = set}
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder return (cSig,
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder Map.fromList $ map (\ (i, n) ->
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder (i, Morphism.Morphism {
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder Morphism.source = n,
abb3850e1a3b30fc05a072a371c77395b3b40927Mihai Codescu Morphism.target = cSig,
abb3850e1a3b30fc05a072a371c77395b3b40927Mihai Codescu Morphism.propMap = maps Map.! i
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder })) $ labNodes graph)
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder
81f49ee02aaa3bc870401f8883bf52742eb3ea7aJonathan von Schroeder
4ab6ebe3181f6e202aa0db327dc6670fda1cf5b6Christian MaederpROPsen_analysis :: (AS_BASIC.BASIC_SPEC, Sign.Sign, AS_BASIC.FORMULA)
4ab6ebe3181f6e202aa0db327dc6670fda1cf5b6Christian Maeder -> Result.Result AS_BASIC.FORMULA
4ab6ebe3181f6e202aa0db327dc6670fda1cf5b6Christian MaederpROPsen_analysis (_, s, f) =
4ab6ebe3181f6e202aa0db327dc6670fda1cf5b6Christian Maeder let x = addFormula [] (NumForm annoF 0) s
4ab6ebe3181f6e202aa0db327dc6670fda1cf5b6Christian Maeder h = return . diagnosis . head
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder g = Just . AS_Anno.sentence . formula . head
4ab6ebe3181f6e202aa0db327dc6670fda1cf5b6Christian Maeder annoF = AS_Anno.Annoted f Id.nullRange [] []
847ce4e1c2ab9ab3a229450e11e55c2ad9de1393Christian Maeder in Result.Result (h x) (g x)