Analysis.hs revision 6e2dba19f0c5ef183c1ac9cf1dff55b9626aeabd
{-# OPTIONS -fallow-undecidable-instances #-}
{- |
Module : $Header$
Description : Instance of class Logic for propositional logic
Copyright : (c) Dominik Luecke, Uni Bremen 2007
License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
Maintainer : luecke@tzi.de
Stability : experimental
Portability : portable
Basic and static analysis for propositional logic
Ref.
-}
module Propositional.Analysis
(
basicPropositionalAnalysis
,mkStatSymbItems
,mkStatSymbMapItem
,inducedFromMorphism
,inducedFromToMorphism
)
where
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import qualified Propositional.Sign as Sign
import qualified Common.GlobalAnnotations as GlobalAnnos
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Result as Result
import qualified Common.Id as Id
import qualified Data.List as List
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Propositional.Symbol as Symbol
import qualified Propositional.Morphism as Morphism
import Common.Doc()
import Common.DocUtils
-- | 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
}
-- | Retrieves the signature out of a basic spec
makeSig ::
AS_BASIC.BASIC_SPEC -- Input SPEC
-> Sign.Sign -- Input Signature
-> Sign.Sign -- Output Signature
makeSig (AS_BASIC.Basic_spec spec) sig = List.foldl retrieveBasicItem sig spec
-- Helper for makeSig
retrieveBasicItem ::
Sign.Sign -- Input Signature
-> AS_Anno.Annoted (AS_BASIC.BASIC_ITEMS) -- Input Item
-> Sign.Sign -- Output Signature
retrieveBasicItem sig x =
case (AS_Anno.item x) of
(AS_BASIC.Pred_decl apred) -> List.foldl
(\asig ax-> Sign.addToSig asig $ Id.simpleIdToId ax)
sig $ (\(AS_BASIC.Pred_item xs _)-> xs) apred
(AS_BASIC.Axiom_items _) -> sig
-- | 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
| label == "" = AS_Anno.NamedSen
{
AS_Anno.senName = "Ax_" ++ show i
, AS_Anno.isAxiom = True
, AS_Anno.isDef = False
, AS_Anno.sentence = AS_Anno.item f
}
| otherwise = AS_Anno.NamedSen
{
AS_Anno.senName = label
, AS_Anno.isAxiom = True
, AS_Anno.isDef = False
, AS_Anno.sentence = AS_Anno.item f
}
where
label = AS_Anno.getRLabel f
-- 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 propostional logic
basicAnalysis :: AS_BASIC.BASIC_SPEC
-> Sign.Sign
-> Result.Result (
)
basicAnalysis bs sig _
| exErrs == False = Result.Result diags $ Just (bs, bsSig, formulae)
| otherwise = Result.Result diags $ Nothing
where
bsSig = makeSig bs sig
bsForm = makeFormulas bs bsSig
formulae = map (\x -> formula x) bsForm
diags = map (\x -> diagnosis x) bsForm
exErrs = Result.hasErrors diags
-- | Wrapper for the interface defined in Logic.Logic
basicPropositionalAnalysis :: (
)
-> Result.Result (
)
basicPropositionalAnalysis (bs, sig, ga) = basicAnalysis bs sig ga
-- | 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
-> Sign.Sign
-> Sign.Sign
inducedFromToMorphism imap sig 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
}