bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{-# OPTIONS -fallow-undecidable-instances #-}

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$

75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiDescription : Instance of class Logic for propositional logic

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : luecke@tzi.de

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : experimental

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability : portable

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederBasic and static analysis for propositional logic

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder Ref.

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder <http://en.wikipedia.org/wiki/Propositional_logic>

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maedermodule Propositional.Analysis

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder (

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder basicPropositionalAnalysis

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder ,mkStatSymbItems

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder ,mkStatSymbMapItem

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder ,inducedFromMorphism

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder ,inducedFromToMorphism

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder )

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder where

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maeder

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Propositional.AS_BASIC_Propositional as AS_BASIC

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Propositional.Sign as Sign

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Common.GlobalAnnotations as GlobalAnnos

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maederimport qualified Common.AS_Annotation as AS_Anno

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Common.Result as Result

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport qualified Common.Id as Id

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Data.List as List

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Data.Set as Set

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport qualified Data.Map as Map

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Propositional.Symbol as Symbol

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport qualified Propositional.Morphism as Morphism

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport Common.Doc()

7abd0c58a5ce51db13f93de82407b2188d55d298Christian Maederimport Common.DocUtils

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-- | Datatype for formulas with diagnosis data

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederdata DIAG_FORM = DiagForm

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder {

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder formula :: AS_Anno.Named (AS_BASIC.FORMULA),

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder diagnosis :: Result.Diagnosis

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder }

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- | Formula annotated with a number

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederdata NUM_FORM = NumForm

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder {

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder nfformula :: AS_Anno.Annoted (AS_BASIC.FORMULA)

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder , nfnum :: Integer

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder }

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maederdata TEST_SIG = TestSig

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder {

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder msign :: Sign.Sign

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , occurence :: Int

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , tdiagnosis :: [Result.Diagnosis]

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder }

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-- | Retrieves the signature out of a basic spec

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaedermakeSig ::

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder AS_BASIC.BASIC_SPEC -- Input SPEC

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder -> Sign.Sign -- Input Signature

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder -> TEST_SIG -- Output Signature

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaedermakeSig (AS_BASIC.Basic_spec spec) sig = List.foldl retrieveBasicItem

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder (TestSig{ msign=sig

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder , occurence=0

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder , tdiagnosis = []

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder })

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder spec

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- Helper for makeSig

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederretrieveBasicItem ::

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder TEST_SIG -- Input Signature

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder -> AS_Anno.Annoted (AS_BASIC.BASIC_ITEMS) -- Input Item

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder -> TEST_SIG -- Output Signature

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederretrieveBasicItem tsig x =

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder let

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder occ = occurence tsig

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder in

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder case (AS_Anno.item x) of

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder (AS_BASIC.Pred_decl apred) ->

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder if (occ == 0)

bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder then

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder List.foldl

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder (\asig ax-> TestSig{

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder , occurence = occ

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder , tdiagnosis = tdiagnosis tsig ++

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder [Result.Diag

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder {

df638d53c2d5fe5e80b943a58609c8936848ed82Christian Maeder Result.diagKind = Result.Hint

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder , Result.diagString = "All fine"

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder , Result.diagPos = AS_Anno.opt_pos x

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder }]

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder })

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder tsig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder else

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder List.foldl

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder (\asig ax-> TestSig{

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder , occurence = occ

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder , tdiagnosis = tdiagnosis tsig ++

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder [Result.Diag

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder {

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder Result.diagKind = Result.Error

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder , Result.diagString = "Definition of proposition " ++

e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maeder (show $ pretty ax) ++

" after first axiom"

, Result.diagPos = AS_Anno.opt_pos x

}]

})

tsig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred

(AS_BASIC.Axiom_items _) -> TestSig { msign = msign tsig

, occurence = occ + 1

, tdiagnosis = tdiagnosis tsig ++

[Result.Diag

{

Result.diagKind = Result.Hint

, Result.diagString = "First axiom"

, Result.diagPos = AS_Anno.opt_pos x

}]

}

-- | Retrieve the formulas out of a basic spec

makeFormulas ::

AS_BASIC.BASIC_SPEC

-> Sign.Sign

-> [DIAG_FORM]

makeFormulas (AS_BASIC.Basic_spec bspec) sig =

List.foldl (\xs bs -> retrieveFormulaItem xs bs sig) [] bspec

-- Helper for makeFormulas

retrieveFormulaItem ::

[DIAG_FORM]

-> AS_Anno.Annoted (AS_BASIC.BASIC_ITEMS)

-> Sign.Sign

-> [DIAG_FORM]

retrieveFormulaItem axs x sig =

case (AS_Anno.item x) of

(AS_BASIC.Pred_decl _) -> axs

(AS_BASIC.Axiom_items ax) ->

List.foldl (\xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0

-- Number formulae

numberFormulae :: [AS_Anno.Annoted (AS_BASIC.FORMULA)] -> Integer -> [NUM_FORM]

numberFormulae [] _ = []

numberFormulae (x:xs) i

| label == "" = NumForm{nfformula = x, nfnum = i} : (numberFormulae xs $ i + 1)

| otherwise = NumForm{nfformula = x, nfnum = 0} : (numberFormulae xs $ i)

where

label = AS_Anno.getRLabel x

-- Add a formula to a named list of formulas

addFormula :: [DIAG_FORM]

-> NUM_FORM

-> Sign.Sign

-> [DIAG_FORM]

addFormula formulae nf sign

| isLegal == True = formulae ++

[DiagForm

{

formula = makeNamed f i

, diagnosis = Result.Diag

{

Result.diagKind = Result.Hint

, Result.diagString = "All fine"

, Result.diagPos = lnum

}

}]

| otherwise = formulae ++

[DiagForm

{

formula = makeNamed f i

, diagnosis = Result.Diag

{

Result.diagKind = Result.Error

, Result.diagString = "Unknown propositions "

++ (show $ pretty difference)

++ " in formula "

++ (show $ pretty nakedFormula)

, Result.diagPos = lnum

}

}]

where

f = nfformula nf

i = nfnum nf

nakedFormula = AS_Anno.item f

varsOfFormula = propsOfFormula nakedFormula

isLegal = Sign.isSubSigOf varsOfFormula sign

difference = Sign.sigDiff varsOfFormula sign

lnum = AS_Anno.opt_pos f

-- generates a named formula

makeNamed :: AS_Anno.Annoted (AS_BASIC.FORMULA) -> Integer -> AS_Anno.Named (AS_BASIC.FORMULA)

makeNamed f i = (AS_Anno.makeNamed (if label == "" then "Ax_" ++ show i

else label) $ AS_Anno.item f)

{ AS_Anno.isAxiom = not isTheorem }

where

label = AS_Anno.getRLabel f

annos = AS_Anno.r_annos f

isImplies = foldl (\y x -> AS_Anno.isImplies x || y) False annos

isImplied = foldl (\y x -> AS_Anno.isImplied x || y) False annos

isTheorem = isImplies || isImplied

-- Retrives the signature of a formula

propsOfFormula :: AS_BASIC.FORMULA -> Sign.Sign

propsOfFormula (AS_BASIC.Negation form _) = propsOfFormula form

propsOfFormula (AS_BASIC.Implication form1 form2 _) = Sign.unite (propsOfFormula form1)

(propsOfFormula form2)

propsOfFormula (AS_BASIC.Equivalence form1 form2 _) = Sign.unite (propsOfFormula form1)

(propsOfFormula form2)

propsOfFormula (AS_BASIC.True_atom _) = Sign.emptySig

propsOfFormula (AS_BASIC.False_atom _) = Sign.emptySig

propsOfFormula (AS_BASIC.Predication x) = Sign.Sign{Sign.items = Set.singleton $

Id.simpleIdToId x }

propsOfFormula (AS_BASIC.Conjunction xs _) = List.foldl (\ sig frm -> Sign.unite sig $

propsOfFormula frm)

Sign.emptySig xs

propsOfFormula (AS_BASIC.Disjunction xs _) = List.foldl (\ sig frm -> Sign.unite sig $

propsOfFormula frm)

Sign.emptySig xs

-- Basic analysis for propostional logic

basicAnalysis :: AS_BASIC.BASIC_SPEC

-> Sign.Sign

-> GlobalAnnos.GlobalAnnos

-> Result.Result (

AS_BASIC.BASIC_SPEC

,Sign.Sign

,[AS_Anno.Named (AS_BASIC.FORMULA)]

)

basicAnalysis bs sig _

| exErrs == False = Result.Result diags $ Just (bs, sigItems, formulae)

| otherwise = Result.Result diags $ Nothing

where

bsSig = makeSig bs sig

sigItems = msign bsSig

bsForm = makeFormulas bs sigItems

formulae = map (\x -> formula x) bsForm

diags = map (\x -> diagnosis x) bsForm ++ tdiagnosis bsSig

exErrs = Result.hasErrors diags

-- | Wrapper for the interface defined in Logic.Logic

basicPropositionalAnalysis :: (

AS_BASIC.BASIC_SPEC

, Sign.Sign

, GlobalAnnos.GlobalAnnos

)

-> Result.Result (

AS_BASIC.BASIC_SPEC

,Sign.Sign

,[AS_Anno.Named (AS_BASIC.FORMULA)]

)

basicPropositionalAnalysis (bs, sig, ga) = basicAnalysis bs sig ga

-- | Static analysis for symbol maps

mkStatSymbMapItem :: [AS_BASIC.SYMB_MAP_ITEMS]

-> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)

mkStatSymbMapItem xs =

Result.Result

{

Result.diags = []

, Result.maybeResult = Just $

foldl

(

\ smap x ->

case x of

AS_BASIC.Symb_map_items sitem _ ->

Map.union smap $ statSymbMapItem sitem

)

Map.empty

xs

}

statSymbMapItem :: [AS_BASIC.SYMB_OR_MAP]

-> Map.Map Symbol.Symbol Symbol.Symbol

statSymbMapItem xs =

foldl

(

\ mmap x ->

case x of

AS_BASIC.Symb sym -> Map.insert (symbToSymbol sym) (symbToSymbol sym) mmap

AS_BASIC.Symb_map s1 s2 _

-> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap

)

Map.empty

xs

-- | Retrieve raw symbols

mkStatSymbItems :: [AS_BASIC.SYMB_ITEMS] -> Result.Result [Symbol.Symbol]

mkStatSymbItems a = Result.Result

{

Result.diags = []

, Result.maybeResult = Just $ statSymbItems a

}

statSymbItems :: [AS_BASIC.SYMB_ITEMS] -> [Symbol.Symbol]

statSymbItems si = concat $ map symbItemsToSymbol si

symbItemsToSymbol :: AS_BASIC.SYMB_ITEMS -> [Symbol.Symbol]

symbItemsToSymbol (AS_BASIC.Symb_items syms _) = map symbToSymbol syms

symbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol

symbToSymbol (AS_BASIC.Symb_id tok) =

Symbol.Symbol{Symbol.symName = Id.simpleIdToId tok}

-- | Induce a signature morphism from a source signature and a raw symbol map

inducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol

-> Sign.Sign

-> Result.Result Morphism.Morphism

inducedFromMorphism imap sig =

Result.Result

{

Result.diags = []

, Result.maybeResult =

let

sigItems = Sign.items sig

pMap:: Map.Map Id.Id Id.Id

pMap =

Set.fold (

\ x ->

let

symOf = Symbol.Symbol { Symbol.symName = x }

y = Symbol.symName $ Symbol.applySymMap imap symOf

in

Map.insert x y

)

Map.empty sigItems

in

Just

Morphism.Morphism

{

Morphism.source = sig

, Morphism.propMap = pMap

, Morphism.target = Sign.Sign

{Sign.items =

Set.map (Morphism.applyMap pMap) $

Sign.items sig

}

}

}

-- | Induce a signature morphism from a source signature and a raw symbol map

inducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol

-> Sign.Sign

-> Sign.Sign

-> Result.Result Morphism.Morphism

inducedFromToMorphism imap sig tSig =

let

sigItems = Sign.items sig

pMap:: Map.Map Id.Id Id.Id

pMap =

Set.fold (

\ x ->

let

symOf = Symbol.Symbol { Symbol.symName = x }

y = Symbol.symName $ Symbol.applySymMap imap symOf

in

Map.insert x y

)

Map.empty sigItems

targetSig = Sign.Sign

{Sign.items =

Set.map (Morphism.applyMap pMap) $

Sign.items sig

}

isSub = (Sign.items targetSig) `Set.isSubsetOf` (Sign.items tSig)

in

case isSub of

True -> Result.Result

{

Result.diags = []

, Result.maybeResult =

Just

Morphism.Morphism

{

Morphism.source = sig

, Morphism.propMap = pMap

, Morphism.target = tSig

}

}

False -> Result.Result

{

Result.diags =

[

Result.Diag

{

Result.diagKind = Result.Error

, Result.diagString = "Incompatible mapping"

, Result.diagPos = Id.nullRange

}

]

, Result.maybeResult = Nothing

}