Analysis.hs revision 81f49ee02aaa3bc870401f8883bf52742eb3ea7a
{- |
Module : $Header$
Description : Basic analysis for propositional logic
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : GPLv2 or higher, see LICENSE.txt
Maintainer : luecke@informatik.uni-bremen.de
Stability : experimental
Portability : portable
Basic and static analysis for propositional logic
Ref.
-}
module Propositional.Analysis
(
basicPropositionalAnalysis
,mkStatSymbItems
,mkStatSymbMapItem
,inducedFromMorphism
,inducedFromToMorphism
, signatureColimit
,pROPsen_analysis
)
where
import Common.ExtSign
import Common.Lib.Graph
import Common.SetColimit
import Data.Graph.Inductive.Graph
import Propositional.Sign as Sign
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.GlobalAnnotations as GlobalAnnos
import qualified Common.Id as Id
import qualified Common.Result as Result
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import qualified Propositional.Morphism as Morphism
import qualified Propositional.Symbol as Symbol
-- | Datatype for formulas with diagnosis data
data DIAG_FORM = DiagForm
{
formula :: AS_Anno.Named (AS_BASIC.FORMULA),
diagnosis :: Result.Diagnosis
}
-- | Formula annotated with a number
data NUM_FORM = NumForm
{
nfformula :: AS_Anno.Annoted (AS_BASIC.FORMULA)
, nfnum :: Integer
}
data TEST_SIG = TestSig
{
msign :: Sign.Sign
, occurence :: Int
, tdiagnosis :: [Result.Diagnosis]
}
-- | Retrieves the signature out of a basic spec
makeSig ::
AS_BASIC.BASIC_SPEC -- Input SPEC
-> Sign.Sign -- Input Signature
-> TEST_SIG -- Output Signature
makeSig (AS_BASIC.Basic_spec spec) sig = List.foldl retrieveBasicItem
(TestSig{ msign=sig
, occurence=0
, tdiagnosis = []
})
spec
-- Helper for makeSig
retrieveBasicItem ::
TEST_SIG -- Input Signature
-> AS_Anno.Annoted (AS_BASIC.BASIC_ITEMS) -- Input Item
-> TEST_SIG -- Output Signature
retrieveBasicItem tsig x =
let
occ = occurence tsig
in
case (AS_Anno.item x) of
(AS_BASIC.Pred_decl apred) ->
if (occ == 0)
then
(\asig ax-> TestSig{
msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax
, occurence = occ
, tdiagnosis = tdiagnosis tsig ++
{
, Result.diagString = "All fine"
}]
})
tsig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred
else
(\asig ax-> TestSig{
msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax
, occurence = occ
, tdiagnosis = tdiagnosis tsig ++
{
, Result.diagString = "Definition of proposition " ++
(show $ pretty ax) ++
" after first axiom"
}]
})
tsig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred
(AS_BASIC.Axiom_items _) -> TestSig { msign = msign tsig
, occurence = occ + 1
, tdiagnosis = tdiagnosis tsig ++
{
, Result.diagString = "First axiom"
}]
}
-- | Retrieve the formulas out of a basic spec
makeFormulas ::
-> 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]
-> 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.diagString = "All fine"
, Result.diagPos = lnum
}
}]
| otherwise = formulae ++
[DiagForm
{
formula = makeNamed f i
, diagnosis = Result.Diag
{
, 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 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
Id.simpleIdToId x }
propsOfFormula frm)
propsOfFormula frm)
-- Basic analysis for propositional logic
basicPropositionalAnalysis
ExtSign Sign.Sign Symbol.Symbol,
basicPropositionalAnalysis (bs, sig, _) =
Result.Result diags $ if exErrs then Nothing else
Just (bs, ExtSign sigItems declaredSyms, formulae)
where
bsSig = makeSig bs sig
sigItems = msign bsSig
declaredSyms = Set.map Symbol.Symbol
$ Set.difference (items sigItems) $ items sig
bsForm = makeFormulas bs sigItems
formulae = map formula bsForm
diags = map diagnosis bsForm ++ tdiagnosis bsSig
exErrs = Result.hasErrors diags
-- | Static analysis for symbol maps
mkStatSymbMapItem :: [AS_BASIC.SYMB_MAP_ITEMS]
mkStatSymbMapItem xs =
{
Result.diags = []
, Result.maybeResult = Just $
foldl
(
\ smap x ->
case x of
AS_BASIC.Symb_map_items sitem _ ->
Map.union smap $ statSymbMapItem sitem
)
xs
}
statSymbMapItem :: [AS_BASIC.SYMB_OR_MAP]
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
)
xs
-- | Retrieve raw symbols
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) =
-- | Induce a signature morphism from a source signature and a raw symbol map
-> Sign.Sign
inducedFromMorphism imap sig =
{
Result.diags = []
let
sigItems = Sign.items sig
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.source = sig
, Morphism.propMap = pMap
{Sign.items =
Set.map (Morphism.applyMap pMap) $
Sign.items sig
}
}
}
-- | Induce a signature morphism from a source signature and a raw symbol map
-> ExtSign Sign.Sign Symbol.Symbol
-> ExtSign Sign.Sign Symbol.Symbol
inducedFromToMorphism imap (ExtSign sig _) (ExtSign tSig _) =
let
sigItems = Sign.items sig
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
}
in
case isSub of
True -> Result.Result
{
Result.diags = []
Just
{
Morphism.source = sig
, Morphism.propMap = pMap
, Morphism.target = tSig
}
}
False -> Result.Result
{
[
{
, Result.diagString = "Incompatible mapping"
}
]
, Result.maybeResult = Nothing
}
signatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
signatureColimit graph = do
let graph1 = nmap Sign.items $ emap (\(x,y) -> (x, Morphism.propMap y)) graph
(set, maps) = addIntToSymbols $ computeColimitSet graph1
cSig = Sign.Sign{Sign.items = set}
return (cSig,
Map.fromList $ map (\(i, n) ->
(i, Morphism.Morphism{
Morphism.source = n,
Morphism.target = cSig,
Morphism.propMap = maps Map.! i
}))$ labNodes graph)
pROPsen_analysis (_,s,f) =
let x = addFormula [] (NumForm annoF 0) s in
Result.Result (h x) (g x)
where h = return . diagnosis . head
g = Just . AS_Anno.sentence .formula . head
annoF = AS_Anno.Annoted f Id.nullRange [] []