hets/Propositional/Analysis.hs

	Analysis.hs revision 67869d63d1725c79e4c07b51acd466a31932b275
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke{- |
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeModule      :  $Header$
9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription :  Basic analysis for propositional logic
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeCopyright   :  (c) Dominik Luecke, Uni Bremen 2007
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeLicense     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke    (
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke     basicPropositionalAnalysis
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    ,mkStatSymbItems
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    ,mkStatSymbMapItem
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    ,inducedFromMorphism
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    ,inducedFromToMorphism
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke    )
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke    where
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Propositional.Sign as Sign
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Common.GlobalAnnotations as GlobalAnnos
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Common.AS_Annotation as AS_Anno
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Common.Result as Result
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckeimport qualified Common.Id as Id
548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckeimport qualified Data.List as List
548f3850942936a8c6021185c8391dfcd3b03018Dominik Lueckeimport qualified Data.Set as Set
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Lueckeimport qualified Data.Map as Map
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Lueckeimport qualified Propositional.Symbol as Symbol
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Lueckeimport qualified Propositional.Morphism as Morphism
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederimport Common.Doc ()
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport Common.DocUtils
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederimport Common.ExtSign
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke-- | Datatype for formulas with diagnosis data
da955132262baab309a50fdffe228c9efe68251dCui Jiandata DIAG_FORM = DiagForm
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    {
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke      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    {
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke      nfformula :: AS_Anno.Annoted (AS_BASIC.FORMULA)
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke    , 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
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                         (TestSig{ msign=sig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                                 , occurence=0
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                                 , tdiagnosis = []
da955132262baab309a50fdffe228c9efe68251dCui Jian                                                 })
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                         spec
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- Helper for makeSig
da955132262baab309a50fdffe228c9efe68251dCui JianretrieveBasicItem ::
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    TEST_SIG                                      -- Input Signature
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    -> 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
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    in
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    case (AS_Anno.item x) of
da955132262baab309a50fdffe228c9efe68251dCui Jian      (AS_BASIC.Pred_decl apred) ->
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke          if (occ == 0)
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke          then
da955132262baab309a50fdffe228c9efe68251dCui Jian              List.foldl
da955132262baab309a50fdffe228c9efe68251dCui Jian                      (\asig ax-> TestSig{
da955132262baab309a50fdffe228c9efe68251dCui Jian                                   msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                 , occurence = occ
da955132262baab309a50fdffe228c9efe68251dCui Jian                                 , tdiagnosis = tdiagnosis tsig ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                   [Result.Diag
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                    {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                      Result.diagKind   = Result.Hint
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                    , Result.diagString = "All fine"
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                    , Result.diagPos    = AS_Anno.opt_pos x
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                    }]
da955132262baab309a50fdffe228c9efe68251dCui Jian                                 })
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                      tsig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke          else
da955132262baab309a50fdffe228c9efe68251dCui Jian              List.foldl
da955132262baab309a50fdffe228c9efe68251dCui Jian                      (\asig ax-> TestSig{
da955132262baab309a50fdffe228c9efe68251dCui Jian                                   msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                 , occurence = occ
da955132262baab309a50fdffe228c9efe68251dCui Jian                                 , tdiagnosis = tdiagnosis tsig ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                   [Result.Diag
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                    {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                      Result.diagKind   = Result.Error
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                    , Result.diagString = "Definition of proposition " ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                                          (show $ pretty ax) ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                                          " after first axiom"
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                    , Result.diagPos    = AS_Anno.opt_pos x
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                    }]
da955132262baab309a50fdffe228c9efe68251dCui Jian                                 })
da955132262baab309a50fdffe228c9efe68251dCui Jian                          tsig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      (AS_BASIC.Axiom_items _)   -> TestSig { msign = msign tsig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                          , occurence = occ + 1
da955132262baab309a50fdffe228c9efe68251dCui Jian                                          , tdiagnosis = tdiagnosis tsig ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                              [Result.Diag
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                               {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                                 Result.diagKind   = Result.Hint
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                               , Result.diagString = "First axiom"
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                               , Result.diagPos    = AS_Anno.opt_pos x
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                               }]
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                            }
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 =
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    List.foldl (\xs bs -> retrieveFormulaItem xs bs sig) []  bspec
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- Helper for makeFormulas
da955132262baab309a50fdffe228c9efe68251dCui JianretrieveFormulaItem ::
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    [DIAG_FORM]
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    -> AS_Anno.Annoted (AS_BASIC.BASIC_ITEMS)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    -> Sign.Sign
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    -> [DIAG_FORM]
da955132262baab309a50fdffe228c9efe68251dCui JianretrieveFormulaItem axs x sig =
da955132262baab309a50fdffe228c9efe68251dCui Jian    case (AS_Anno.item x) of
da955132262baab309a50fdffe228c9efe68251dCui Jian      (AS_BASIC.Pred_decl _)    -> axs
da955132262baab309a50fdffe228c9efe68251dCui Jian      (AS_BASIC.Axiom_items ax) ->
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke          List.foldl (\xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-- Number formulae
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik LueckenumberFormulae :: [AS_Anno.Annoted (AS_BASIC.FORMULA)] -> Integer -> [NUM_FORM]
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckenumberFormulae [] _ = []
da955132262baab309a50fdffe228c9efe68251dCui JiannumberFormulae (x:xs) i
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke    | label == "" =  NumForm{nfformula = x, nfnum = i} : (numberFormulae xs $ i + 1)
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke    | otherwise   =  NumForm{nfformula = x, nfnum = 0} : (numberFormulae xs $ i)
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    where
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke      label = AS_Anno.getRLabel x
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke--  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
da955132262baab309a50fdffe228c9efe68251dCui Jian    | isLegal == True = formulae ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                        [DiagForm
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                         {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           formula   = makeNamed f i
da955132262baab309a50fdffe228c9efe68251dCui Jian                         , diagnosis = Result.Diag
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                             Result.diagKind = Result.Hint
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           , Result.diagString = "All fine"
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           , Result.diagPos    = lnum
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           }
da955132262baab309a50fdffe228c9efe68251dCui Jian                         }]
da955132262baab309a50fdffe228c9efe68251dCui Jian    | otherwise       = formulae ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                        [DiagForm
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                         {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           formula   = makeNamed f i
da955132262baab309a50fdffe228c9efe68251dCui Jian                         , diagnosis = Result.Diag
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                       {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                         Result.diagKind = Result.Error
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                       , Result.diagString = "Unknown propositions "
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                         ++ (show $ pretty difference)
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                         ++ " in formula "
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                         ++ (show $ pretty nakedFormula)
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                       , Result.diagPos    = lnum
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                       }
da955132262baab309a50fdffe228c9efe68251dCui Jian                         }]
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    where
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke      f             = nfformula nf
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke      i             = nfnum nf
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke      nakedFormula  = AS_Anno.item f
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke      varsOfFormula = propsOfFormula nakedFormula
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke      isLegal       = Sign.isSubSigOf varsOfFormula sign
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke      difference    = Sign.sigDiff varsOfFormula sign
5b9f5c1b3592b99fc74d3438740ebcf9eb4c94beDominik Luecke      lnum          = AS_Anno.opt_pos f
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke-- generates a named formula
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckemakeNamed :: AS_Anno.Annoted (AS_BASIC.FORMULA) -> Integer -> 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
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      isImplies = foldl (\y x -> AS_Anno.isImplies x || y) False annos
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      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
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.Implication form1 form2 _) = Sign.unite (propsOfFormula form1)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                           (propsOfFormula form2)
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.Equivalence form1 form2 _) = Sign.unite (propsOfFormula form1)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                           (propsOfFormula form2)
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.True_atom _)  = Sign.emptySig
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.False_atom _) = Sign.emptySig
da955132262baab309a50fdffe228c9efe68251dCui JianpropsOfFormula (AS_BASIC.Predication x) = Sign.Sign{Sign.items = Set.singleton $
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                                                 Id.simpleIdToId x }
da955132262baab309a50fdffe228c9efe68251dCui JianpropsOfFormula (AS_BASIC.Conjunction xs _) = List.foldl (\ sig frm -> Sign.unite sig $
da955132262baab309a50fdffe228c9efe68251dCui Jian                                                                      propsOfFormula frm)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                             Sign.emptySig xs
da955132262baab309a50fdffe228c9efe68251dCui JianpropsOfFormula (AS_BASIC.Disjunction xs _) = List.foldl (\ sig frm -> Sign.unite sig $
da955132262baab309a50fdffe228c9efe68251dCui Jian                                                                      propsOfFormula frm)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                             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,
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder                    [AS_Anno.Named (AS_BASIC.FORMULA)])
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaederbasicPropositionalAnalysis (bs, sig, _) =
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder   Result.Result diags $ if exErrs then Nothing else
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder     Just (bs, mkExtSign sigItems, formulae)
da955132262baab309a50fdffe228c9efe68251dCui Jian    where
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke      bsSig     = makeSig bs sig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      sigItems  = msign bsSig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      bsForm    = makeFormulas bs sigItems
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder      formulae  = map formula bsForm
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder      diags     = map diagnosis bsForm ++ tdiagnosis bsSig
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke      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
da955132262baab309a50fdffe228c9efe68251dCui JianstatSymbMapItem xs =
da955132262baab309a50fdffe228c9efe68251dCui Jian    foldl
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    (
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke     \ mmap x ->
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke         case x of
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke           AS_BASIC.Symb sym -> Map.insert (symbToSymbol sym) (symbToSymbol sym) mmap
da955132262baab309a50fdffe228c9efe68251dCui Jian           AS_BASIC.Symb_map s1 s2 _
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke             -> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    )
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    Map.empty
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    xs
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]
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckestatSymbItems si = concat $ map symbItemsToSymbol si
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) =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    Symbol.Symbol{Symbol.symName = Id.simpleIdToId tok}
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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckeinducedFromMorphism imap sig =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    Result.Result
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke          {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke            Result.diags = []
da955132262baab309a50fdffe228c9efe68251dCui Jian          , Result.maybeResult =
da955132262baab309a50fdffe228c9efe68251dCui Jian              let
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  sigItems = Sign.items sig
da955132262baab309a50fdffe228c9efe68251dCui Jian                  pMap:: Map.Map Id.Id Id.Id
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  pMap =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                      Set.fold (
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                \ x ->
da955132262baab309a50fdffe228c9efe68251dCui Jian                                    let
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                        symOf = Symbol.Symbol { Symbol.symName = x }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                        y = Symbol.symName $ Symbol.applySymMap imap symOf
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                    in
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                      Map.insert x y
da955132262baab309a50fdffe228c9efe68251dCui Jian                               )
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                               Map.empty sigItems
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke              in
da955132262baab309a50fdffe228c9efe68251dCui Jian              Just
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke              Morphism.Morphism
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                          {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                            Morphism.source  = sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                          , Morphism.propMap = pMap
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                          , Morphism.target  = Sign.Sign
da955132262baab309a50fdffe228c9efe68251dCui Jian                                               {Sign.items =
da955132262baab309a50fdffe228c9efe68251dCui Jian                                                    Set.map (Morphism.applyMap pMap) $
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                       Sign.items sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                               }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                          }
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
da955132262baab309a50fdffe228c9efe68251dCui Jian                  pMap:: Map.Map Id.Id Id.Id
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  pMap =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                      Set.fold (
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                \ x ->
da955132262baab309a50fdffe228c9efe68251dCui Jian                                    let
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                        symOf = Symbol.Symbol { Symbol.symName = x }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                        y = Symbol.symName $ Symbol.applySymMap imap symOf
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                    in
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                      Map.insert x y
da955132262baab309a50fdffe228c9efe68251dCui Jian                               )
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                               Map.empty sigItems
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  targetSig = Sign.Sign
da955132262baab309a50fdffe228c9efe68251dCui Jian                                               {Sign.items =
da955132262baab309a50fdffe228c9efe68251dCui Jian                                                    Set.map (Morphism.applyMap pMap) $
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                       Sign.items sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                               }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  isSub = (Sign.items targetSig) `Set.isSubsetOf` (Sign.items tSig)
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke              in
da955132262baab309a50fdffe228c9efe68251dCui Jian                case isSub of
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                     True ->     Result.Result
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                 {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                   Result.diags = []
da955132262baab309a50fdffe228c9efe68251dCui Jian                                 , Result.maybeResult =
da955132262baab309a50fdffe228c9efe68251dCui Jian                                     Just
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                     Morphism.Morphism
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                 {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                   Morphism.source  = sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                 , Morphism.propMap = pMap
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                 , Morphism.target  = tSig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                 }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                 }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                     False -> Result.Result
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                              {
da955132262baab309a50fdffe228c9efe68251dCui Jian                                Result.diags =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                [
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                 Result.Diag
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                       {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                         Result.diagKind   = Result.Error
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                       , Result.diagString = "Incompatible mapping"
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                       , Result.diagPos    = Id.nullRange
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                       }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                ]
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                              , Result.maybeResult = Nothing
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                              }
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke