hets/Propositional/Analysis.hs

	Analysis.hs revision 61091743da1a9ed6dfd5e077fdcc972553358962
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke{-# OPTIONS -fallow-undecidable-instances #-}
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke{- |
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeModule      :  $Header$
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeDescription :  Instance of class Logic 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
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckeMaintainer  :  luecke@tzi.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-}
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Lueckemodule 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
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport Common.Doc()
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckeimport Common.DocUtils
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik Luecke-- | Datatype for formulas with diagnosis data
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Lueckedata 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
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckemakeSig ::
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke    AS_BASIC.BASIC_SPEC                  -- Input SPEC
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke    -> Sign.Sign                         -- Input Signature
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    -> TEST_SIG                          -- Output Signature
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik LueckemakeSig (AS_BASIC.Basic_spec spec) sig = List.foldl retrieveBasicItem
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                         (TestSig{ msign=sig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                                 , occurence=0
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                                 , tdiagnosis = []
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                                 })
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                         spec
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- Helper for makeSig
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckeretrieveBasicItem ::
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    TEST_SIG                                      -- Input Signature
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    -> AS_Anno.Annoted (AS_BASIC.BASIC_ITEMS)     -- Input Item
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    -> TEST_SIG                                   -- Output Signature
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik LueckeretrieveBasicItem tsig x =
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    let
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke        occ = occurence tsig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    in
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    case (AS_Anno.item x) of
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      (AS_BASIC.Pred_decl apred) ->
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke          if (occ == 0)
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke          then
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke              List.foldl
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                      (\asig ax-> TestSig{
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                   msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                 , occurence = occ
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                 , 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                                    }]
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                 })
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                      tsig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke          else
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke              List.foldl
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                      (\asig ax-> TestSig{
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                   msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                 , occurence = occ
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                 , 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                                    }]
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                 })
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                          tsig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      (AS_BASIC.Axiom_items _)   -> TestSig { msign = msign tsig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                          , occurence = occ + 1
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                                          , 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
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckemakeFormulas ::
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke    AS_BASIC.BASIC_SPEC
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    -> Sign.Sign
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    -> [DIAG_FORM]
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik LueckemakeFormulas (AS_BASIC.Basic_spec bspec) sig =
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    List.foldl (\xs bs -> retrieveFormulaItem xs bs sig) []  bspec
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke-- Helper for makeFormulas
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckeretrieveFormulaItem ::
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    [DIAG_FORM]
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    -> AS_Anno.Annoted (AS_BASIC.BASIC_ITEMS)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke    -> Sign.Sign
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    -> [DIAG_FORM]
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckeretrieveFormulaItem axs x sig =
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke    case (AS_Anno.item x) of
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke      (AS_BASIC.Pred_decl _)    -> axs
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      (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 [] _ = []
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckenumberFormulae (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
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke           -> [DIAG_FORM]
080f5fd32e4367ac0c8efb468bc9b75f8c08cc87Dominik LueckeaddFormula formulae nf sign
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    | isLegal == True = formulae ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                        [DiagForm
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                         {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           formula   = makeNamed f i
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                         , diagnosis = Result.Diag
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                             Result.diagKind = Result.Hint
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           , Result.diagString = "All fine"
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           , Result.diagPos    = lnum
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           }
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                         }]
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    | otherwise       = formulae ++
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                        [DiagForm
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                         {
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                           formula   = makeNamed f i
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                         , 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                                       }
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke                         }]
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 }
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    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
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.Predication x) = Sign.Sign{Sign.items = Set.singleton $
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                                                 Id.simpleIdToId x }
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.Conjunction xs _) = List.foldl (\ sig frm -> Sign.unite sig $
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                                                      propsOfFormula frm)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                             Sign.emptySig xs
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckepropsOfFormula (AS_BASIC.Disjunction xs _) = List.foldl (\ sig frm -> Sign.unite sig $
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                                                      propsOfFormula frm)
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                                             Sign.emptySig xs
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-- Basic analysis for propostional logic
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckebasicAnalysis :: AS_BASIC.BASIC_SPEC
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke              -> Sign.Sign
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke              -> GlobalAnnos.GlobalAnnos
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke              -> Result.Result (
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                                AS_BASIC.BASIC_SPEC
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                               ,Sign.Sign
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke                               ,[AS_Anno.Named (AS_BASIC.FORMULA)]
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                               )
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik LueckebasicAnalysis bs sig _
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke    | exErrs == False =  Result.Result diags $ Just (bs, sigItems, formulae)
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    | otherwise       =  Result.Result diags $ Nothing
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke    where
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke      bsSig     = makeSig bs sig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      sigItems  = msign bsSig
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      bsForm    = makeFormulas bs sigItems
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke      formulae  = map (\x -> formula x) bsForm
c5c3ba1d1735af9ae35b4b1cb6e60777c9ea2fb1Dominik Luecke      diags     = map (\x -> diagnosis x) bsForm ++ tdiagnosis bsSig
648e803bb79a00b1c246d093fe2a2707c6b2cf7bDominik Luecke      exErrs    = Result.hasErrors diags
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-- | Wrapper for the interface defined in Logic.Logic
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckebasicPropositionalAnalysis :: (
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                               AS_BASIC.BASIC_SPEC
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                              , Sign.Sign
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                              , GlobalAnnos.GlobalAnnos
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                              )
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                           -> Result.Result (
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                                             AS_BASIC.BASIC_SPEC
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                                            ,Sign.Sign
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                                            ,[AS_Anno.Named (AS_BASIC.FORMULA)]
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke                                            )
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik LueckebasicPropositionalAnalysis (bs, sig, ga) = basicAnalysis bs sig ga
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke-- | Static analysis for symbol maps
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckemkStatSymbMapItem :: [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 = []
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    , Result.maybeResult = Just $
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                           foldl
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                           (
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                            \ smap x ->
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                case x of
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                  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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckestatSymbMapItem xs =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke           AS_BASIC.Symb_map s1 s2 _
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke             -> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    )
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    Map.empty
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    xs
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke
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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckesymbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckesymbToSymbol (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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckeinducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                    -> Sign.Sign
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                    -> Result.Result Morphism.Morphism
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckeinducedFromMorphism imap sig =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke    Result.Result
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke          {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke            Result.diags = []
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke          , Result.maybeResult =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke              let
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  sigItems = Sign.items sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  pMap:: Map.Map Id.Id Id.Id
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  pMap =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                      Set.fold (
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                \ x ->
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                    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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                               )
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                               Map.empty sigItems
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke              in
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke              Just
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke              Morphism.Morphism
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                          {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                            Morphism.source  = sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                          , Morphism.propMap = pMap
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                          , Morphism.target  = Sign.Sign
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                               {Sign.items =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                    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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckeinducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                    -> Sign.Sign
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                    -> Sign.Sign
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                    -> Result.Result Morphism.Morphism
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik LueckeinducedFromToMorphism imap sig tSig =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke              let
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  sigItems = Sign.items sig
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  pMap:: Map.Map Id.Id Id.Id
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  pMap =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                      Set.fold (
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                \ x ->
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                    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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                               )
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                               Map.empty sigItems
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                  targetSig = Sign.Sign
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                               {Sign.items =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                                    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
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                case isSub of
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                     True ->     Result.Result
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                 {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                   Result.diags = []
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                 , Result.maybeResult =
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                     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                              {
6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabdDominik Luecke                                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