{- |
Module : ./CommonLogic/Analysis.hs
Description : Basic analysis for common logic
Copyright : (c) Eugen Kuksa, Karl Luc, Uni Bremen 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : eugenk@informatik.uni-bremen.de
Stability : experimental
Portability : portable
Basic and static analysis for common logic
-}
module CommonLogic.Analysis
( basicCommonLogicAnalysis
, negForm
, symsOfTextMeta
, mkStatSymbItems
, mkStatSymbMapItem
, inducedFromMorphism
, inducedFromToMorphism
, signColimit
)
where
import Common.ExtSign
import Common.Result as Result
import Common.GlobalAnnotations
import qualified Common.AS_Annotation as AS_Anno
import Common.Id as Id
import Common.IRI (parseIRIReference)
import Common.DocUtils
import Common.Lib.Graph
import Common.SetColimit
import CommonLogic.Symbol as Symbol
import qualified CommonLogic.AS_CommonLogic as AS
import CommonLogic.Morphism as Morphism
import CommonLogic.Sign as Sign
import CommonLogic.ExpandCurie
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Common.Lib.MapSet as MapSet
import qualified Data.List as List
import Data.Graph.Inductive.Graph as Graph
data DIAG_FORM = DiagForm
{
formula :: AS_Anno.Named AS.TEXT_META,
diagnosis :: Result.Diagnosis
}
-- | retrieves the signature out of a basic spec
makeSig :: AS.BASIC_SPEC -> Sign.Sign -> Sign.Sign
makeSig (AS.Basic_spec spec) sig = List.foldl retrieveBasicItem sig spec
retrieveBasicItem :: Sign.Sign -> AS_Anno.Annoted AS.BASIC_ITEMS -> Sign.Sign
retrieveBasicItem sig x = case AS_Anno.item x of
AS.Axiom_items xs -> List.foldl retrieveSign sig xs
retrieveSign :: Sign.Sign -> AS_Anno.Annoted AS.TEXT_META -> Sign.Sign
retrieveSign sig (AS_Anno.Annoted tm _ _ _) =
Sign.unite (Sign.unite sig $ nondiscItems $ AS.nondiscourseNames tm)
(propsOfFormula $ AS.getText tm)
nondiscItems :: Maybe (Set.Set AS.NAME) -> Sign.Sign
nondiscItems s = case s of
Nothing -> Sign.emptySig
Just ns -> Sign.emptySig {Sign.nondiscourseNames = Set.map Id.simpleIdToId ns}
-- | retrieve sentences
makeFormulas :: AS.BASIC_SPEC -> Sign.Sign -> [DIAG_FORM]
makeFormulas (AS.Basic_spec bspec) sig =
List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec
retrieveFormulaItem :: [DIAG_FORM] -> AS_Anno.Annoted AS.BASIC_ITEMS
-> Sign.Sign -> [DIAG_FORM]
retrieveFormulaItem axs x sig =
case AS_Anno.item x of
AS.Axiom_items ax ->
List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
data NUM_FORM = NumForm
{
nfformula :: AS_Anno.Annoted AS.TEXT_META
, nfnum :: Int
}
numberFormulae :: [AS_Anno.Annoted AS.TEXT_META] -> Int -> [NUM_FORM]
numberFormulae [] _ = []
numberFormulae (x : xs) i =
if null $ AS_Anno.getRLabel x
then NumForm {nfformula = x, nfnum = i} : numberFormulae xs (i + 1)
else NumForm {nfformula = x, nfnum = 0} : numberFormulae xs i
addFormula :: [DIAG_FORM]
-> NUM_FORM
-> Sign.Sign
-> [DIAG_FORM]
addFormula formulae nf _ = formulae ++
[DiagForm {
formula = makeNamed (setTextIRI f) i
, diagnosis = Result.Diag
{
Result.diagKind = Result.Hint
, Result.diagString = "All fine"
, Result.diagPos = lnum
}
}]
where
f = nfformula nf
i = nfnum nf
lnum = AS_Anno.opt_pos f
-- | extract comment from text, used as formula label
getComment :: AS.TEXT -> String
getComment (AS.Text ((AS.Comment_text (AS.Comment s _) _ _) :_) _)= s
getComment (AS.Text (_:rest) pos) = getComment (AS.Text rest pos)
getComment _ = ""
stripQuote :: String -> String
stripQuote ('"':rest) = rest
stripQuote s = s
stripQuotes :: String -> String
stripQuotes ('"':rest) = reverse (stripQuote (reverse rest))
stripQuotes s = s
-- | generates a named formula
makeNamed :: AS_Anno.Annoted AS.TEXT_META -> Int
-> AS_Anno.Named AS.TEXT_META
makeNamed f i =
(AS_Anno.makeNamed (
if null label2
then case text of
AS.Named_text n _ _ -> Id.tokStr n
_ -> "Ax_" ++ show i
else label2
) $ AS_Anno.item f)
{ AS_Anno.isAxiom = not isTheorem }
where
text = AS.getText $ AS_Anno.item f
label = AS_Anno.getRLabel f
label2 = if null label then stripQuotes $ getComment text
else label
annos = AS_Anno.r_annos f
isImplies = any AS_Anno.isImplies annos
isImplied = any AS_Anno.isImplied annos
isTheorem = isImplies || isImplied
setTextIRI :: AS_Anno.Annoted AS.TEXT_META -> AS_Anno.Annoted AS.TEXT_META
setTextIRI atm@(AS_Anno.Annoted { AS_Anno.item = tm }) =
let mi = case AS.getText tm of
AS.Named_text n _ _ -> parseIRIReference $ init $ tail $ Id.tokStr n
_ -> Nothing
in atm { AS_Anno.item = tm { AS.textIri = mi } }
-- | Retrives the signature of a sentence
propsOfFormula :: AS.TEXT -> Sign.Sign
propsOfFormula (AS.Named_text _ txt _) = propsOfFormula txt
propsOfFormula (AS.Text phrs _) = Sign.uniteL $ map propsOfPhrase phrs
propsOfPhrase :: AS.PHRASE -> Sign.Sign
propsOfPhrase (AS.Module m) = propsOfModule m
propsOfPhrase (AS.Sentence s) = propsOfSentence s
propsOfPhrase (AS.Comment_text _ txt _) = propsOfFormula txt
propsOfPhrase (AS.Importation _) = Sign.emptySig
propsOfModule :: AS.MODULE -> Sign.Sign
propsOfModule m = case m of
(AS.Mod n txt _) -> Sign.unite (propsOfFormula txt) $ nameToSign n
(AS.Mod_ex n exs txt _) -> Sign.unite (propsOfFormula txt)
$ Sign.uniteL $ nameToSign n : map nameToSign exs
where nameToSign x = Sign.emptySig {
Sign.discourseNames = Set.singleton $ Id.simpleIdToId x
}
propsOfSentence :: AS.SENTENCE -> Sign.Sign
propsOfSentence (AS.Atom_sent form _) = case form of
AS.Equation term1 term2 -> Sign.unite (propsOfTerm term1)
(propsOfTerm term2)
AS.Atom term ts -> Sign.unite (propsOfTerm term)
(uniteMap propsOfTermSeq ts)
propsOfSentence (AS.Quant_sent _ xs s _) =
Sign.sigDiff (propsOfSentence s) (uniteMap propsOfNames xs)
propsOfSentence (AS.Bool_sent bs _) = case bs of
AS.Junction _ xs -> uniteMap propsOfSentence xs
AS.Negation x -> propsOfSentence x
AS.BinOp _ s1 s2 -> Sign.unite (propsOfSentence s1) (propsOfSentence s2)
propsOfSentence (AS.Comment_sent _ s _) = propsOfSentence s
propsOfSentence (AS.Irregular_sent s _) = propsOfSentence s
propsOfTerm :: AS.TERM -> Sign.Sign
propsOfTerm term = case term of
AS.Name_term x -> Sign.emptySig {
Sign.discourseNames = Set.singleton $ Id.simpleIdToId x
}
AS.Funct_term t ts _ -> Sign.unite (propsOfTerm t)
(uniteMap propsOfTermSeq ts)
AS.Comment_term t _ _ -> propsOfTerm t -- fix
AS.That_term s _ -> propsOfSentence s
propsOfNames :: AS.NAME_OR_SEQMARK -> Sign.Sign
propsOfNames (AS.Name x) = Sign.emptySig {
Sign.discourseNames = Set.singleton $ Id.simpleIdToId x
}
propsOfNames (AS.SeqMark x) = Sign.emptySig {
Sign.sequenceMarkers = Set.singleton $ Id.simpleIdToId x
}
propsOfTermSeq :: AS.TERM_SEQ -> Sign.Sign
propsOfTermSeq s = case s of
AS.Term_seq term -> propsOfTerm term
AS.Seq_marks x -> Sign.emptySig {
Sign.sequenceMarkers = Set.singleton $ Id.simpleIdToId x
}
uniteMap :: (a -> Sign.Sign) -> [a] -> Sign
uniteMap p = List.foldl (\ sig -> Sign.unite sig . p)
Sign.emptySig
-- | Common Logic static analysis
basicCommonLogicAnalysis :: (AS.BASIC_SPEC, Sign.Sign, GlobalAnnos)
-> Result (AS.BASIC_SPEC,
ExtSign Sign.Sign Symbol.Symbol,
[AS_Anno.Named AS.TEXT_META])
basicCommonLogicAnalysis (bs', sig, ga) =
Result.Result [] $ if exErrs then Nothing else
Just (bs', ExtSign sigItems newSyms, sentences)
where
bs = expandCurieBS (prefix_map ga) bs'
sigItems = makeSig bs sig
newSyms = Set.map Symbol.Symbol
$ Set.difference (Sign.allItems sigItems) $ Sign.allItems sig
bsform = makeFormulas bs sigItems
-- [DIAG_FORM] signature and list of sentences
sentences = map formula bsform
-- Annoted Sentences (Ax_), numbering, DiagError
exErrs = False
-- | creates a morphism from a symbol map
inducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
-> Sign.Sign
-> Result.Result Morphism.Morphism
inducedFromMorphism m s = let
p = Map.mapKeys symName $ Map.map symName m
t = Sign.emptySig { discourseNames = Set.map (applyMap p) $ discourseNames s
, nondiscourseNames = Set.map (applyMap p) $ nondiscourseNames s
, sequenceMarkers = Set.map (applyMap p) $ sequenceMarkers s
}
in return $ mkMorphism s t p
splitFragment :: Id -> (String, String)
splitFragment = span (/= '#') . show
inducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
-> ExtSign Sign.Sign Symbol.Symbol
-> ExtSign Sign.Sign Symbol.Symbol
-> Result.Result Morphism.Morphism
inducedFromToMorphism m (ExtSign s sys) (ExtSign t ty) = let
tsy = Set.fold (\ r -> let (q, f) = splitFragment $ symName r
in MapSet.insert f q) MapSet.empty ty
p = Set.fold (\ sy -> let n = symName sy in case Map.lookup sy m of
Just r -> Map.insert n $ symName r
Nothing -> if Set.member sy ty then id else
let (_, f) = splitFragment n
in case Set.toList $ MapSet.lookup f tsy of
[q] -> Map.insert n $ simpleIdToId
$ mkSimpleId $ q ++ f
_ -> id) Map.empty sys
t2 = Sign.emptySig
{ discourseNames = Set.map (applyMap p) $ discourseNames s
, nondiscourseNames = Set.map (applyMap p) $ nondiscourseNames s
, sequenceMarkers = Set.map (applyMap p) $ sequenceMarkers s
}
in if isSubSigOf t2 t then return $ mkMorphism s t p else
fail $ "cannot map symbols from\n" ++ showDoc (sigDiff t2 t) "\nto\n"
++ showDoc t ""
-- | negate sentence (text) - propagates negation to sentences
negForm :: AS.TEXT_META -> AS.TEXT_META
negForm tm = tm { AS.getText = negForm_txt $ AS.getText tm }
negForm_txt :: AS.TEXT -> AS.TEXT
negForm_txt t = case t of
AS.Text phrs r -> AS.Text (map negForm_phr phrs) r
AS.Named_text n txt r -> AS.Named_text n (negForm_txt txt) r
-- negate phrase - propagates negation to sentences
negForm_phr :: AS.PHRASE -> AS.PHRASE
negForm_phr phr = case phr of
AS.Module m -> AS.Module $ negForm_mod m
AS.Sentence s -> AS.Sentence $ negForm_sen s
AS.Comment_text c t r -> AS.Comment_text c (negForm_txt t) r
x -> x
-- negate module - propagates negation to sentences
negForm_mod :: AS.MODULE -> AS.MODULE
negForm_mod m = case m of
AS.Mod n t r -> AS.Mod n (negForm_txt t) r
AS.Mod_ex n exs t r -> AS.Mod_ex n exs (negForm_txt t) r
-- negate sentence
negForm_sen :: AS.SENTENCE -> AS.SENTENCE
negForm_sen f = case f of
AS.Quant_sent _ _ _ r -> AS.Bool_sent (AS.Negation f) r
AS.Bool_sent bs r -> case bs of
AS.Negation s -> s
_ -> AS.Bool_sent (AS.Negation f) r
_ -> AS.Bool_sent (AS.Negation f) Id.nullRange
-- | Static analysis for symbol maps
mkStatSymbMapItem :: [AS.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.Symb_map_items sitem _ ->
Map.union smap $ statSymbMapItem sitem
)
Map.empty
xs
}
statSymbMapItem :: [AS.SYMB_OR_MAP] -> Map.Map Symbol.Symbol Symbol.Symbol
statSymbMapItem =
foldl
(
\ mmap x ->
case x of
AS.Symb sym -> Map.insert (nosToSymbol sym) (nosToSymbol sym) mmap
AS.Symb_mapN s1 s2 _
-> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
AS.Symb_mapS s1 s2 _
-> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
)
Map.empty
-- | Retrieve raw symbols
mkStatSymbItems :: [AS.SYMB_ITEMS] -> Result.Result [Symbol.Symbol]
mkStatSymbItems a = Result.Result
{
Result.diags = []
, Result.maybeResult = Just $ statSymbItems a
}
statSymbItems :: [AS.SYMB_ITEMS] -> [Symbol.Symbol]
statSymbItems = concatMap symbItemsToSymbol
symbItemsToSymbol :: AS.SYMB_ITEMS -> [Symbol.Symbol]
symbItemsToSymbol (AS.Symb_items syms _) = map nosToSymbol syms
nosToSymbol :: AS.NAME_OR_SEQMARK -> Symbol.Symbol
nosToSymbol nos = case nos of
AS.Name tok -> symbToSymbol tok
AS.SeqMark tok -> symbToSymbol tok
symbToSymbol :: Id.Token -> Symbol.Symbol
symbToSymbol tok = Symbol.Symbol {Symbol.symName = Id.simpleIdToId tok}
-- | retrieves all symbols from the text
symsOfTextMeta :: AS.TEXT_META -> [Symbol.Symbol]
symsOfTextMeta tm =
Set.toList $ Symbol.symOf $ retrieveSign Sign.emptySig $ AS_Anno.emptyAnno tm
-- | compute colimit of CL signatures
signColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
-> Result (Sign.Sign, Map.Map Int Morphism.Morphism)
signColimit diag = do
let mor2fun (x,mor) = (x, Morphism.propMap mor)
dGraph = emap mor2fun $ nmap Sign.discourseNames diag
(dCol, dmap) = addIntToSymbols $ computeColimitSet dGraph
ndGraph = emap mor2fun $ nmap Sign.nondiscourseNames diag
(ndCol, ndmap) = addIntToSymbols $ computeColimitSet ndGraph
sGraph = emap mor2fun $ nmap Sign.sequenceMarkers diag
(sCol, smap) = addIntToSymbols $ computeColimitSet sGraph
sig = Sign { Sign.discourseNames = dCol
, Sign.nondiscourseNames = ndCol
, Sign.sequenceMarkers = sCol
}
mors = Map.unions $ map (\ (x, nsig) ->
let m = Morphism.Morphism {
Morphism.source = nsig
, Morphism.target = sig
, Morphism.propMap = Map.unions
[ Map.findWithDefault (error "dmap") x dmap,
Map.findWithDefault (error "ndmap") x ndmap,
Map.findWithDefault (error "smap") x smap]
}
in Map.insert x m Map.empty) $ labNodes diag
return (sig, mors)