{- |

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)