{- |
Module      :  ./OWL2/StaticAnalysis.hs
Copyright   :  Felix Gabriel Mance
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  f.mance@jacobs-university.de
Stability   :  provisional
Portability :  portable

Static analysis for OWL 2
-}

module OWL2.StaticAnalysis where

import OWL2.Sign
import OWL2.Morphism
import qualified OWL2.AS as AS
import OWL2.MS
import OWL2.Print ()
import OWL2.Theorem
import OWL2.Function
import OWL2.Symbols

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List

import Common.AS_Annotation hiding (Annotation)
import Common.DocUtils
import Common.Result
import Common.GlobalAnnotations as GA
import Common.ExtSign
import Common.Lib.State
import Common.IRI --(iriToStringUnsecure, setAngles)
import Common.SetColimit

import Control.Monad

import Logic.Logic

-- | Error messages for static analysis
failMsg :: AS.Entity -> AS.ClassExpression -> Result a
failMsg (AS.Entity _ ty e) desc =
  fatal_error
    ("undeclared `" ++ AS.showEntityType ty
          ++ " " ++ showIRI e ++ "` in the following ClassExpression:\n"
          ++ showDoc desc "") $ iriPos e

-- | checks if an entity is in the signature
checkEntity :: Sign -> AS.Entity -> Result ()
checkEntity s t@(AS.Entity _ ty e) =
  let errMsg = mkError ("unknown " ++ AS.showEntityType ty) e
  in case ty of
   AS.Datatype -> unless (Set.member e (datatypes s) || AS.isDatatypeKey e) errMsg
   AS.Class -> unless (Set.member e (concepts s) || AS.isThing e) errMsg
   AS.ObjectProperty -> unless (isDeclObjProp s $ AS.ObjectProp e) errMsg
   AS.DataProperty -> unless (isDeclDataProp s e) errMsg
   AS.AnnotationProperty -> unless (Set.member e (annotationRoles s)
        || AS.isPredefAnnoProp e) $ justWarn () $ showDoc t " unknown"
   _ -> return ()

-- | takes an iri and finds out what entities it belongs to
correctEntity :: Sign -> IRI -> [AS.Entity]
correctEntity s iri =
    [AS.mkEntity AS.AnnotationProperty iri | Set.member iri (annotationRoles s)] ++
    [AS.mkEntity AS.Class iri | Set.member iri (concepts s)] ++
    [AS.mkEntity AS.ObjectProperty iri | Set.member iri (objectProperties s)] ++
    [AS.mkEntity AS.DataProperty iri | Set.member iri (dataProperties s)] ++
    [AS.mkEntity AS.Datatype iri | Set.member iri (datatypes s)] ++
    [AS.mkEntity AS.NamedIndividual iri | Set.member iri (individuals s)]

checkLiteral :: Sign -> AS.Literal -> Result ()
checkLiteral s l = case l of
    AS.Literal _ (AS.Typed dt) -> checkEntity s $ AS.mkEntity AS.Datatype dt
    _ -> return ()

isDeclInd :: Sign -> AS.Individual -> Bool
isDeclInd s ind = Set.member ind $ individuals s

isDeclObjProp :: Sign -> AS.ObjectPropertyExpression -> Bool
isDeclObjProp s ope = let op = AS.objPropToIRI ope in
    Set.member op (objectProperties s) || AS.isPredefObjProp op

isDeclDataProp :: Sign -> AS.DataPropertyExpression -> Bool
isDeclDataProp s dp = Set.member dp (dataProperties s) || AS.isPredefDataProp dp

{- | takes a list of object properties and discards the ones
    which are not in the signature -}
filterObjProp :: Sign -> [AS.ObjectPropertyExpression]
    -> [AS.ObjectPropertyExpression]
filterObjProp = filter . isDeclObjProp

checkHasKey :: Sign -> [AS.ObjectPropertyExpression] -> [AS.DataPropertyExpression]
    -> Result ([AS.ObjectPropertyExpression], [AS.DataPropertyExpression])
checkHasKey s ol dl = do
    let (declaredObjProps, undeclaredObjs) = partition (isDeclObjProp s) ol
    let (declaredDProps, undeclaredDProps) = partition (isDeclDataProp s) dl

    let newDProps = map (AS.objPropToIRI) $ filter AS.isObjectProperty undeclaredObjs
    let newObjProps = map (AS.ObjectProp) undeclaredDProps

    checkObjPropList s newObjProps
    checkDataPropList s newDProps

    return (declaredObjProps ++ newObjProps, declaredDProps ++ newDProps)

    

checkObjPropList :: Sign -> [AS.ObjectPropertyExpression] -> Result ()
checkObjPropList s ol = do
    let ls = map (isDeclObjProp s) ol
    unless (and ls) $ fail $ "undeclared object properties:\n" ++
                      showDoc (map (\o -> case o of
                                     AS.ObjectProp _ -> o
                                     AS.ObjectInverseOf x -> x) (filter (not . isDeclObjProp s) ol)) ""

checkDataPropList :: Sign -> [AS.DataPropertyExpression] -> Result ()
checkDataPropList s dl = do
    let ls = map (isDeclDataProp s) dl
    unless (and ls) $ fail $ "undeclared data properties:\n" ++ showDoc (filter (not . isDeclDataProp s) dl) ""

-- | checks if a DataRange is valid
checkDataRange :: Sign -> AS.DataRange -> Result ()
checkDataRange s dr = case dr of
    AS.DataType dt rl -> do
        checkEntity s $ AS.mkEntity AS.Datatype dt
        mapM_ (checkLiteral s . snd) rl
    AS.DataJunction _ drl -> mapM_ (checkDataRange s) drl
    AS.DataComplementOf r -> checkDataRange s r
    AS.DataOneOf ll -> mapM_ (checkLiteral s) ll

{- | converts ClassExpression to DataRanges because some
     DataProperties may be parsed as ObjectProperties -}
classExpressionToDataRange :: Sign -> AS.ClassExpression -> Result AS.DataRange
classExpressionToDataRange s ce = case ce of
    AS.Expression u -> checkEntity s (AS.mkEntity AS.Datatype u)
        >> return (AS.DataType u [])
    AS.ObjectJunction jt cel -> fmap (AS.DataJunction jt)
        $ mapM (classExpressionToDataRange s) cel
    AS.ObjectComplementOf c -> fmap AS.DataComplementOf
        $ classExpressionToDataRange s c
    _ -> fail $ "cannot convert ClassExpression to DataRange\n"
            ++ showDoc ce ""

{- | checks a ClassExpression and recursively converts the
     (maybe inappropriately) parsed syntax to a one satisfying the signature -}
checkClassExpression :: Sign -> AS.ClassExpression -> Result AS.ClassExpression
checkClassExpression s desc =
    let errMsg i = failMsg i desc
        objErr i = errMsg $ AS.mkEntity AS.ObjectProperty i
        datErr i = errMsg $ AS.mkEntity AS.DataProperty i
    in case desc of
    AS.Expression u -> if AS.isThing u
        then return $ AS.Expression $ AS.setReservedPrefix u
        else checkEntity s (AS.mkEntity AS.Class u) >> return desc
    AS.ObjectJunction ty ds -> fmap (AS.ObjectJunction ty)
        $ mapM (checkClassExpression s) ds
    AS.ObjectComplementOf d -> fmap AS.ObjectComplementOf $ checkClassExpression s d
    AS.ObjectOneOf _ -> return desc
    AS.ObjectValuesFrom q opExpr d -> if isDeclObjProp s opExpr
        then fmap (AS.ObjectValuesFrom q opExpr) $ checkClassExpression s d
        else let iri = AS.objPropToIRI opExpr
             in if isDeclDataProp s iri then
                    fmap (AS.DataValuesFrom q [iri])
                      $ classExpressionToDataRange s d
                else objErr iri
    AS.ObjectHasSelf opExpr -> if isDeclObjProp s opExpr then return desc
        else objErr $ AS.objPropToIRI opExpr
    AS.ObjectHasValue opExpr _ -> if isDeclObjProp s opExpr then return desc
        else objErr $ AS.objPropToIRI opExpr
    AS.ObjectCardinality (AS.Cardinality a b opExpr md) -> do
        let iri = AS.objPropToIRI opExpr
            mbrOP = Set.member iri $ objectProperties s
        case md of
            Nothing
                | mbrOP -> return desc
                | isDeclDataProp s iri ->
                        return $ AS.DataCardinality $ AS.Cardinality a b iri Nothing
                | otherwise -> objErr iri
            Just d ->
                if mbrOP then fmap (AS.ObjectCardinality . AS.Cardinality a b opExpr
                            . Just) $ checkClassExpression s d
                else do
                    dr <- classExpressionToDataRange s d
                    if isDeclDataProp s iri then
                        return $ AS.DataCardinality
                          $ AS.Cardinality a b iri $ Just dr
                        else datErr iri
    AS.DataValuesFrom _ dExp r -> checkDataRange s r
        >> if isDeclDataProp s (head dExp) then return desc else datErr (head dExp)
    AS.DataHasValue dExp l -> do
        checkLiteral s l
        if isDeclDataProp s dExp then return desc
            else datErr dExp
    AS.DataCardinality (AS.Cardinality _ _ dExp mr) -> if isDeclDataProp s dExp
        then case mr of
            Nothing -> return desc
            Just d -> checkDataRange s d >> return desc
        else datErr dExp


checkAnnotation :: Sign -> AS.Annotation -> Result ()
checkAnnotation s (AS.Annotation ans apr av) = do
    checkAnnos s ans
    checkEntity s (AS.mkEntity AS.AnnotationProperty apr)
    case av of
        AS.AnnValLit lit -> checkLiteral s lit
        _ -> return ()

checkAnnos :: Sign -> [AS.Annotation] -> Result ()
checkAnnos = mapM_ . checkAnnotation

checkAssertion :: Sign -> IRI -> Annotations -> Result [Axiom]
checkAssertion s iri ans = do
    let entList = correctEntity s iri
        ab = AnnFrameBit ans $ AnnotationFrameBit Assertion
    if null entList
        then let misc = Misc [AS.Annotation [] iri $ AS.AnnValue iri]
             in return [PlainAxiom misc ab] -- only for anonymous individuals
        else return $ map (\ x -> PlainAxiom (SimpleEntity x) ab) entList

extractDGVariables :: [AS.DGAtom] -> [AS.Variable]
extractDGVariables = 
    let eIArg a = case a of
            AS.IVar v -> [v]
            _ -> []
    in
    
    concat . map (\atom -> case atom of
        AS.DGClassAtom _ a -> eIArg a
        AS.DGObjectPropertyAtom _ a1 a2 -> eIArg a1 ++ eIArg a2
    )

extractVariables :: [AS.Atom] -> [AS.Variable]
extractVariables = 
    let eIArg a = case a of
            AS.IVar v -> [v]
            _ -> []
        eDArg a = case a of
            AS.DVar v -> [v]
            _ -> []
        eUArg a = case a of
            AS.IndividualArg ia -> eIArg ia
            AS.DataArg da -> eDArg da
            AS.Variable v -> [v]
    in
    
    concat . map (\atom -> case atom of
        AS.ClassAtom _ a -> eIArg a
        AS.DataRangeAtom _ a -> eDArg a
        AS.ObjectPropertyAtom _ a1 a2 -> eIArg a1 ++ eIArg a2
        AS.DataPropertyAtom _ a1 a2 -> eIArg a1 ++ eDArg a2
        AS.BuiltInAtom _ args -> concat $ eDArg <$> args
        AS.SameIndividualAtom a1 a2 -> eIArg a1 ++ eIArg a2
        AS.DifferentIndividualsAtom a1 a2 -> eIArg a1 ++ eIArg a2
        AS.UnknownUnaryAtom _ a -> eUArg a
        AS.UnknownBinaryAtom _ a1 a2 -> eUArg a1 ++ eUArg a2
    )

checkIndividualArg :: Sign -> Maybe [AS.Variable] -> AS.IndividualArg -> Result ()
checkIndividualArg s mVars a = case a of
    AS.IArg i -> checkEntity s (AS.mkEntity AS.NamedIndividual i) >> return ()
    AS.IVar v -> case mVars of
        Nothing -> return ()
        Just vars -> unless (v `elem` vars) $ mkError "Unknown variable" v

checkDataArg :: Sign -> Maybe [AS.Variable] -> AS.DataArg -> Result ()
checkDataArg s mVars a = case a of
    AS.DArg l -> checkLiteral s l >> return ()
    AS.DVar v -> case mVars of
        Nothing -> return ()
        Just vars -> unless (v `elem` vars) $ mkError "Unknown variable" v

checkDGAtom :: Sign -> Maybe [AS.Variable] -> AS.DGAtom -> Result AS.DGAtom
checkDGAtom s mVars atom = case atom of
    AS.DGClassAtom c a -> do
        nExpr <- checkClassExpression s c
        checkIndividualArg s mVars a
        return $ AS.DGClassAtom nExpr a
    AS.DGObjectPropertyAtom o a1 a2 -> do
        checkObjPropList s [o]
        checkIndividualArg s mVars a1
        checkIndividualArg s mVars a2
        return atom


checkDLAtom :: Sign -> Maybe [AS.Variable] -> AS.Atom -> Result AS.Atom
checkDLAtom s mVars atom = case atom of
    AS.ClassAtom e a -> do
        newExpr <- checkClassExpression s e
        checkIndividualArg s mVars a
        return $ AS.ClassAtom newExpr a
    AS.DataRangeAtom r a -> do
        checkDataRange s r
        checkDataArg s mVars a
        return atom
    AS.ObjectPropertyAtom o a1 a2 -> do
        checkObjPropList s [o]
        checkIndividualArg s mVars a1
        checkIndividualArg s mVars a2
        return atom
    AS.DataPropertyAtom d a1 a2 -> do
        checkDataPropList s [d]
        checkIndividualArg s mVars a1
        checkDataArg s mVars a2
        return atom
    AS.BuiltInAtom _ args -> do
        mapM (checkDataArg s mVars) args
        return atom
    AS.SameIndividualAtom a1 a2 -> do
        checkIndividualArg s mVars a1
        checkIndividualArg s mVars a2
        return atom
    AS.DifferentIndividualsAtom a1 a2 -> do
        checkIndividualArg s mVars a1
        checkIndividualArg s mVars a2
        return atom
    AS.UnknownUnaryAtom i a -> case a of
        AS.Variable v -> if Set.member i (concepts s)
            then return $ AS.ClassAtom (AS.Expression i) (AS.IVar v)
            else return $ AS.BuiltInAtom i [AS.DVar v]
        _ -> mkError "Unknown unary atom" i
    AS.UnknownBinaryAtom i a1 a2 -> case a1 of
        AS.Variable v ->
            if Set.member i (objectProperties s) then case a2 of
                AS.Variable v2 -> return $ AS.ObjectPropertyAtom (AS.ObjectProp i) (AS.IVar v) (AS.IVar v2)
                AS.IndividualArg a -> return $ AS.ObjectPropertyAtom (AS.ObjectProp i) (AS.IVar v) a
                _ -> mkError "Unknown binary atom" i
            else if Set.member i (dataProperties s) then case a2 of
                AS.Variable v2 -> return $ AS.DataPropertyAtom i (AS.IVar v) (AS.DVar v2)
                AS.DataArg a -> return $ AS.DataPropertyAtom i (AS.IVar v) a
                _ -> mkError "Unknown binary atom" i
            else case a2 of
                AS.Variable v' -> return $ AS.BuiltInAtom i [AS.DVar v']
                AS.DataArg a -> return $ AS.BuiltInAtom i [a]
                _ -> mkError "Unknown binary atom" i 
        AS.IndividualArg a@(AS.IArg _) -> case a2 of
            AS.Variable v ->
                if Set.member i (objectProperties s) then return $ AS.ObjectPropertyAtom (AS.ObjectProp i) a (AS.IVar v)
                else if Set.member i (dataProperties s) then return $ AS.DataPropertyAtom i a (AS.DVar v)
                else mkError "Unknown binary atom" i
            _ -> mkError "Unknown binary atom" i
        _ -> mkError "Unknown binary atom" i


checkDGEdgeAssertion :: Sign -> AS.DGEdgeAssertion -> Result ()
checkDGEdgeAssertion s (AS.DGEdgeAssertion o _ _) = do
    checkObjPropList s [AS.ObjectProp o]
    return ()

-- | corrects the axiom according to the signature
checkAxiom :: Sign -> AS.Axiom -> Result [AS.Axiom]
checkAxiom s a = case a of
    (AS.Declaration anns entity) -> do
        checkAnnos s anns
        checkEntity s entity
        return [a]

    AS.ClassAxiom clAxiom -> case clAxiom of
        AS.SubClassOf anns subClExpr supClExpr -> do
            checkAnnos s anns
            nSubClExpr <- (checkClassExpression s) subClExpr
            nSupClExpr <- (checkClassExpression s) supClExpr
            return [AS.ClassAxiom $ AS.SubClassOf anns nSubClExpr nSupClExpr]

        AS.EquivalentClasses anns clExprs -> do
            checkAnnos s anns
            nClExprs <- mapM (checkClassExpression s) clExprs
            return [AS.ClassAxiom $ AS.EquivalentClasses anns nClExprs]
            
        AS.DisjointClasses anns clExprs -> do
            checkAnnos s anns
            nClExprs <- mapM (checkClassExpression s) clExprs
            return [AS.ClassAxiom $ AS.DisjointClasses anns nClExprs]

        AS.DisjointUnion anns clIRI clExprs -> do
            checkAnnos s anns
            checkEntity s (AS.mkEntity AS.Class clIRI)
            nClExprs <- mapM (checkClassExpression s) clExprs
            return [AS.ClassAxiom $ AS.DisjointUnion anns clIRI nClExprs]

    AS.ObjectPropertyAxiom opAxiom -> case opAxiom of
        AS.SubObjectPropertyOf anns subOpExpr supOpExpr -> do
            let subOpExpr2 = case subOpExpr of
                    AS.SubObjPropExpr_obj o -> [o]
                    AS.SubObjPropExpr_exprchain c -> c
            checkAnnos s anns
            checkObjPropList s (supOpExpr : subOpExpr2)
            return [a]

        AS.EquivalentObjectProperties anns opExprs -> do
            checkAnnos s anns
            checkObjPropList s opExprs
            return [a]

        AS.DisjointObjectProperties anns opExprs -> do
            checkAnnos s anns
            checkObjPropList s opExprs
            return [a]

        AS.InverseObjectProperties anns opExpr1 opExpr2 -> do
            checkAnnos s anns
            checkObjPropList s [opExpr1, opExpr2]
            return [a]

        AS.ObjectPropertyDomain anns opExpr clExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            nClExpr <- checkClassExpression s clExpr
            return [AS.ObjectPropertyAxiom
                $ AS.ObjectPropertyDomain anns opExpr nClExpr]

        AS.ObjectPropertyRange anns opExpr clExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            nClExpr <- checkClassExpression s clExpr
            return [AS.ObjectPropertyAxiom
                $ AS.ObjectPropertyRange anns opExpr nClExpr]

        AS.FunctionalObjectProperty anns opExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            return [a]

        AS.InverseFunctionalObjectProperty anns opExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            return [a]

        AS.ReflexiveObjectProperty anns opExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            return [a]

        AS.IrreflexiveObjectProperty anns opExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            return [a]

        AS.SymmetricObjectProperty anns opExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            return [a]

        AS.AsymmetricObjectProperty anns opExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            return [a]

        AS.TransitiveObjectProperty anns opExpr -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            return [a]

    (AS.DataPropertyAxiom dpAxiom) -> case dpAxiom of
        AS.SubDataPropertyOf anns subDpExpr supDpExpr -> do
            checkAnnos s anns
            checkDataPropList s [subDpExpr, supDpExpr]
            return [a]

        AS.EquivalentDataProperties anns dpExprs -> do
            checkAnnos s anns
            unless (length dpExprs >= 2) $ mkError "Incorrect number of Data Property Expressions (must be >= 2): " dpExprs
            checkDataPropList s dpExprs
            return [a]

        AS.DisjointDataProperties anns dpExprs -> do
            checkAnnos s anns
            unless (length dpExprs >= 2) $ mkError "Incorrect number of Data Property Expressions (must be >= 2): " dpExprs
            checkDataPropList s dpExprs
            return [a]

        AS.DataPropertyDomain anns dpExpr clExpr -> do
            checkAnnos s anns
            checkDataPropList s [dpExpr]
            nClExpr <- checkClassExpression s clExpr
            return [AS.DataPropertyAxiom
                $ AS.DataPropertyDomain anns dpExpr nClExpr]

        AS.DataPropertyRange anns dpExpr dr -> do
            checkAnnos s anns
            checkDataPropList s [dpExpr]
            checkDataRange s dr
            return [a]

        AS.FunctionalDataProperty anns dpExpr -> do
            checkAnnos s anns
            checkDataPropList s [dpExpr]
            return [a]
            
    AS.DatatypeDefinition anns dt dr -> do
        checkAnnos s anns
        checkEntity s $ AS.mkEntity AS.Datatype dt
        checkDataRange s dr
        return [a]

    AS.HasKey anns clExpr opExprs dpExprs -> do
        checkAnnos s anns
        nClExpr <- checkClassExpression s clExpr
        (nOpExprs, nDpExprs) <- checkHasKey s opExprs dpExprs
        return [AS.HasKey anns nClExpr nOpExprs nDpExprs]

    AS.Assertion assertionAxiom -> case assertionAxiom of 
        AS.SameIndividual anns inds -> do
            checkAnnos s anns
            unless (length inds >= 2) $ mkError "Incorrect number of Individuals (must be >= 2): " inds
            mapM_ (checkEntity s . AS.mkEntity AS.NamedIndividual) inds 
            return [a]
            
        AS.DifferentIndividuals anns inds -> do
            checkAnnos s anns
            unless (length inds >= 2) $ mkError "Incorrect number of Individuals (must be >= 2): " inds
            mapM_ (checkEntity s . AS.mkEntity AS.NamedIndividual) inds
            return [a]

        AS.ClassAssertion anns clExpr ind -> do
            checkAnnos s anns
            nClExpr <- checkClassExpression s clExpr
            checkEntity s $ AS.mkEntity AS.NamedIndividual ind
            return [AS.Assertion $ AS.ClassAssertion anns nClExpr ind]

        AS.ObjectPropertyAssertion anns opExpr sInd tInd -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            mapM_ (checkEntity s . AS.mkEntity AS.NamedIndividual) [sInd, tInd]
            return [a]

        AS.NegativeObjectPropertyAssertion anns opExpr sInd tInd -> do
            checkAnnos s anns
            checkObjPropList s [opExpr]
            mapM_ (checkEntity s . AS.mkEntity AS.NamedIndividual) [sInd, tInd]
            return [a]

        AS.DataPropertyAssertion anns dpExpr sInd tValue -> do
            checkAnnos s anns
            checkDataPropList s [dpExpr]
            checkEntity s $ AS.mkEntity AS.NamedIndividual sInd
            checkLiteral s tValue
            return [a]

        AS.NegativeDataPropertyAssertion anns dpExpr sInd tValue -> do
            checkAnnos s anns
            checkDataPropList s [dpExpr]
            checkEntity s $ AS.mkEntity AS.NamedIndividual sInd
            checkLiteral s tValue
            return [a]

    AS.AnnotationAxiom anAxiom -> case anAxiom of
        AS.AnnotationAssertion anns prop subj val -> do
            checkAnnos s anns
            checkEntity s (AS.mkEntity AS.AnnotationProperty prop)

            case subj of
                AS.AnnSubIri iri -> when (null $ correctEntity s iri)
                    $ mkError "Incorrect AnnotationAssertion axiom. Axiom subject is not declared: " (show iri)
                _ -> return ()
                
            case val of
                AS.AnnValLit lit -> checkLiteral s lit
                _ -> return ()
            return [a]
            

        AS.SubAnnotationPropertyOf anns subAnProp supAnProp -> do
            checkAnnos s anns
            mapM_ (checkEntity s . AS.mkEntity AS.AnnotationProperty) [subAnProp, supAnProp]
            return [a]

        AS.AnnotationPropertyDomain anns prop _ -> do
            checkAnnos s anns
            checkEntity s (AS.mkEntity AS.AnnotationProperty prop)
            return [a]

        AS.AnnotationPropertyRange anns prop _ -> do
            checkAnnos s anns
            checkEntity s (AS.mkEntity AS.AnnotationProperty prop)
            return [a]
        

    (AS.Rule rule) -> case rule of 
        AS.DLSafeRule anns body hea -> do
            checkAnnos s anns
            nBody <- mapM (checkDLAtom s Nothing) body
            let vars = extractVariables body
            nHead <- mapM (checkDLAtom s (Just vars)) hea
            return [AS.Rule $ AS.DLSafeRule anns nBody nHead]
        AS.DGRule anns body hea -> do
            checkAnnos s anns
            mapM (checkDGAtom s Nothing) body
            let vars = extractDGVariables body
            mapM (checkDGAtom s (Just vars)) hea
            return [a]
    (AS.DGAxiom anns _ _ edges _) -> do
        checkAnnos s anns
        mapM (checkDGEdgeAssertion s) edges
        return [a]



correctFrames :: Sign -> [AS.Axiom] -> Result [AS.Axiom]
correctFrames s = fmap concat . mapM (checkAxiom s)

collectEntities :: AS.Axiom -> State Sign ()
collectEntities f = case f of
    AS.Declaration _ e -> addEntity e
    _ -> return ()

-- | collects all entites from the aximoms
createSign :: [AS.Axiom] -> State Sign ()
createSign f = do
  pm <- gets prefixMap
  mapM_ (collectEntities . function Expand (StringMap pm)) f

noDecl :: AS.Axiom -> Bool
noDecl ax = case ax of
  AS.Declaration _ _ -> False
  _ -> True

-- | corrects the axioms according to the signature
createAxioms :: Sign -> [AS.Axiom] -> Result ([Named AS.Axiom], [AS.Axiom])
createAxioms s fl = do
    cf <- correctFrames s $ map (function Expand $ StringMap $ prefixMap s) fl
    return (map anaAxiom . filter noDecl $ cf, cf)

check1Prefix :: Maybe IRI -> IRI -> Bool
check1Prefix ms s = case ms of
      Nothing -> True
      Just iri -> iri == s

checkPrefixMap :: GA.PrefixMap -> Bool
checkPrefixMap pm =
    let pl = map (`Map.lookup` pm) ["owl", "rdf", "rdfs", "xsd"]
    in and $ zipWith check1Prefix pl
            (map snd $ Map.toList AS.predefPrefixesGA)

newODoc :: AS.OntologyDocument -> [AS.Axiom] -> Result AS.OntologyDocument
newODoc AS.OntologyDocument {
      AS.ontology = mo
    , AS.ontologyMetadata = md
    , AS.prefixDeclaration = pd} ax =
    if checkPrefixMap pd
        then return AS.OntologyDocument
                { AS.ontologyMetadata = md
                , AS.ontology = mo {AS.axioms = ax}
                , AS.prefixDeclaration = pd
                }
        else fail $ "Incorrect predefined prefixes " ++ showDoc pd "\n"

-- | static analysis of ontology with incoming sign.
basicOWL2Analysis :: (AS.OntologyDocument, Sign, GlobalAnnos)
    -> Result (AS.OntologyDocument, ExtSign Sign AS.Entity, [Named AS.Axiom])
basicOWL2Analysis (inOnt, inSign, ga) = do
    let pm = Map.union (AS.prefixDeclaration inOnt)
          . Map.delete "" $ prefix_map ga
        odoc = inOnt { AS.prefixDeclaration = pm }
        axs = AS.axioms $ AS.ontology odoc
        accSign = execState (createSign axs) inSign { prefixMap = AS.changePrefixMapTypeToString pm }
        syms = Set.difference (symOf accSign) $ symOf inSign
    (axl, nfl) <- createAxioms accSign axs
    newdoc <- newODoc odoc nfl
    return (newdoc
      , ExtSign accSign {labelMap = generateLabelMap accSign nfl} syms, axl)

-- | extract labels from Axiom-List (after processing with correctFrames)
generateLabelMap :: Sign -> [AS.Axiom] -> Map.Map IRI String
generateLabelMap sig = foldr (\ a -> case a of 
        AS.AnnotationAxiom ax -> case ax of
            AS.AnnotationAssertion _ apr sub (AS.AnnValLit (AS.Literal s' _))
                | prefixName apr == "rdfs" && show (iriPath apr) == "label"
                -> Map.insert (ir sub) s'
            _ -> id
        _ -> id) (labelMap sig)
    where ir sub = case sub of
            AS.AnnSubIri i -> i
            AS.AnnSubAnInd i -> i 

-- | adding annotations for theorems
anaAxiom :: AS.Axiom -> Named AS.Axiom
anaAxiom ax = findImplied ax $ makeNamed nm ax
   where names = getNames ax
         nm = concat $ intersperse "_" names
         
findImplied :: AS.Axiom -> Named AS.Axiom -> Named AS.Axiom
findImplied ax sent =
  if prove ax then sent
         { isAxiom = False
         , isDef = False
         , wasTheorem = False }
   else sent { isAxiom = True }

getNamesFromAnnos :: [AS.Annotation] -> [String]
getNamesFromAnnos = concat . fmap (\anno -> case anno of
      AS.Annotation _ aIRI (AS.AnnValLit (AS.Literal value _)) ->
          if show (iriPath aIRI) == "label"
             then [value]
             else []
      _ -> [])

getNames :: AS.Axiom -> [String]
getNames ax = case ax of
    AS.Declaration anns _ -> getNamesFromAnnos anns
    AS.ClassAxiom cax -> case cax of
        AS.SubClassOf anns _ _ -> getNamesFromAnnos anns
        AS.EquivalentClasses anns _ -> getNamesFromAnnos anns
        AS.DisjointClasses anns _ -> getNamesFromAnnos anns
        AS.DisjointUnion anns _ _ -> getNamesFromAnnos anns
    AS.ObjectPropertyAxiom opax -> case opax of
        AS.SubObjectPropertyOf anns _ _ -> getNamesFromAnnos anns
        AS.EquivalentObjectProperties anns _ -> getNamesFromAnnos anns
        AS.DisjointObjectProperties anns _ -> getNamesFromAnnos anns
        AS.InverseObjectProperties anns _ _ -> getNamesFromAnnos anns
        AS.ObjectPropertyDomain anns _ _ -> getNamesFromAnnos anns
        AS.ObjectPropertyRange anns _ _ -> getNamesFromAnnos anns
        AS.FunctionalObjectProperty anns _ -> getNamesFromAnnos anns
        AS.InverseFunctionalObjectProperty anns _ -> getNamesFromAnnos anns
        AS.ReflexiveObjectProperty anns _ -> getNamesFromAnnos anns
        AS.IrreflexiveObjectProperty anns _ -> getNamesFromAnnos anns
        AS.SymmetricObjectProperty anns _ -> getNamesFromAnnos anns
        AS.AsymmetricObjectProperty anns _ -> getNamesFromAnnos anns
        AS.TransitiveObjectProperty anns _ -> getNamesFromAnnos anns
    AS.DataPropertyAxiom a -> case a of
        AS.SubDataPropertyOf anns _ _ -> getNamesFromAnnos anns
        AS.EquivalentDataProperties anns _ -> getNamesFromAnnos anns
        AS.DisjointDataProperties anns _ -> getNamesFromAnnos anns
        AS.DataPropertyDomain anns _ _ -> getNamesFromAnnos anns
        AS.DataPropertyRange anns _ _ -> getNamesFromAnnos anns
        AS.FunctionalDataProperty anns _ -> getNamesFromAnnos anns
    AS.DatatypeDefinition anns _ _ -> getNamesFromAnnos anns
    AS.HasKey anns _ _ _ -> getNamesFromAnnos anns
    AS.Assertion a -> case a of
        AS.SameIndividual anns _ -> getNamesFromAnnos anns
        AS.DifferentIndividuals anns _ -> getNamesFromAnnos anns
        AS.ClassAssertion anns _ _ -> getNamesFromAnnos anns
        AS.ObjectPropertyAssertion anns _ _ _ -> getNamesFromAnnos anns
        AS.NegativeObjectPropertyAssertion anns _ _ _ -> getNamesFromAnnos anns
        AS.DataPropertyAssertion anns _ _ _ -> getNamesFromAnnos anns
        AS.NegativeDataPropertyAssertion anns _ _ _ -> getNamesFromAnnos anns
    AS.AnnotationAxiom a -> case a of
        AS.AnnotationAssertion anns _ _ _ -> getNamesFromAnnos anns
        AS.SubAnnotationPropertyOf anns _ _ -> getNamesFromAnnos anns
        AS.AnnotationPropertyDomain anns _ _ -> getNamesFromAnnos anns
        AS.AnnotationPropertyRange anns _ _ -> getNamesFromAnnos anns
    AS.DGAxiom anns _ _ _ _ -> getNamesFromAnnos anns
    AS.Rule r -> case r of
        AS.DLSafeRule anns _ _ -> getNamesFromAnnos anns
        AS.DGRule anns _ _ -> getNamesFromAnnos anns


addEquiv :: Sign -> Sign -> [SymbItems] -> [SymbItems] ->
            Result (Sign, Sign, Sign,
                     EndoMap AS.Entity, EndoMap AS.Entity)
addEquiv ssig tsig l1 l2 = do
  let l1' = statSymbItems ssig l1
      l2' = statSymbItems tsig l2
  case (l1', l2') of
    ([rs1], [rs2]) -> do
      let match1 = filter (`matchesSym` rs1) $ Set.toList $ symOf ssig
          match2 = filter (`matchesSym` rs2) $ Set.toList $ symOf tsig
      case
       (match1, match2) of
          ([e1], [e2]) ->
           if AS.entityKind e1 == AS.entityKind e2 then do
              s <- AS.pairSymbols e1 e2
              sig <- addSymbToSign emptySign s
              sig1 <- addSymbToSign emptySign e1
              sig2 <- addSymbToSign emptySign e2
              return (sig, sig1, sig2,
                         Map.insert e1 s Map.empty,
                         Map.insert e2 s Map.empty)
             else
              fail "only symbols of same kind can be equivalent in an alignment"
          _ -> fail $ "non-unique symbol match:" ++ showDoc l1 " "
                                                 ++  showDoc l2 " "
    _ -> fail "terms not yet supported in alignments"

corr2theo :: String -> Bool -> Sign -> Sign -> [SymbItems] -> [SymbItems] ->
             EndoMap AS.Entity -> EndoMap AS.Entity -> REL_REF ->
             Result (Sign, [Named AS.Axiom], Sign, Sign,
                     EndoMap AS.Entity, EndoMap AS.Entity)
corr2theo _aname flag ssig tsig l1 l2 eMap1 eMap2 rref = do
  let l1' = statSymbItems ssig l1
      l2' = statSymbItems tsig l2
  case (l1', l2') of
    ([rs1], [rs2]) -> do
      let match1 = filter (`matchesSym` rs1) $ Set.toList $ symOf ssig
          match2 = filter (`matchesSym` rs2) $ Set.toList $ symOf tsig
      case
       (match1, match2) of
          ([e1], [e2]) -> do
           let e1' = if flag then e1 {AS.cutIRI =  addString (AS.cutIRI e1, "_source")} else e1
               e2' = if flag then e2 {AS.cutIRI =  addString (AS.cutIRI e2, "_target")} else e2
               sig = emptySign
               eMap1' = Map.union eMap1 $ Map.fromAscList [(e1', e1)]
               eMap2' = Map.union eMap2 $ Map.fromAscList [(e2', e2)]
           sig1 <- addSymbToSign sig e1'
           sig2 <- addSymbToSign sig e2'
           sigB <- addSymbToSign sig1 e2'
           case rref of
            Equiv -> do
                let axiom = case (AS.entityKind e1', AS.entityKind e2') of
                        (AS.Class, AS.Class) -> AS.ClassAxiom $
                                AS.EquivalentClasses [] (AS.Expression . AS.cutIRI <$> [e1', e2'])
                        (AS.ObjectProperty, AS.ObjectProperty) -> AS.ObjectPropertyAxiom $
                            AS.EquivalentObjectProperties [] (AS.ObjectProp . AS.cutIRI <$> [e1', e2'])
                        (AS.NamedIndividual, AS.NamedIndividual) -> AS.Assertion $
                            AS.SameIndividual [] (AS.cutIRI <$> [e1', e2'])
                        _ -> error $ "use subsumption only between"
                                        ++ "classes or roles:" ++
                                        show l1 ++ " " ++ show l2
                return (sigB, [makeNamed "" axiom], sig1, sig2, eMap1', eMap2')
            Subs -> do
                let axiom = case (AS.entityKind e1', AS.entityKind e2') of
                        (AS.Class, AS.Class) -> AS.ClassAxiom $
                            AS.SubClassOf []
                                (AS.Expression . AS.cutIRI $ e1')
                                (AS.Expression . AS.cutIRI $ e2')
                        (AS.ObjectProperty, AS.ObjectProperty) -> AS.ObjectPropertyAxiom $
                            AS.SubObjectPropertyOf []
                                (AS.SubObjPropExpr_obj $ AS.ObjectProp $ AS.cutIRI e1')
                                (AS.ObjectProp $ AS.cutIRI e2')
                        _ -> error $ "use subsumption only between"
                                        ++ "classes or roles:" ++
                                        show l1 ++ " " ++ show l2
                return (sigB, [makeNamed "" axiom], sig1, sig2, eMap1', eMap2')
            Incomp -> do
                let axiom = AS.ClassAxiom $ AS.DisjointClasses [] (AS.Expression . AS.cutIRI <$> [e1', e2'])
                return (sigB, [makeNamed "" axiom], sig1, sig2, eMap1', eMap2')
            IsSubs -> do
                let axiom = AS.ClassAxiom $ AS.SubClassOf []
                        (AS.Expression . AS.cutIRI $ e1')
                        (AS.Expression . AS.cutIRI $ e2')
                return (sigB, [makeNamed "" axiom], sig1, sig2, eMap1', eMap2')
            InstOf -> do
                let axiom = AS.Assertion $ AS.ClassAssertion []
                        (AS.Expression . AS.cutIRI $ e1')
                        (AS.cutIRI $ e2')
                return
                    (sigB, [makeNamed "" axiom], sig1, sig2, eMap1', eMap2')
            HasInst -> do
                let axiom = AS.Assertion $ AS.ClassAssertion []
                        (AS.Expression . AS.cutIRI $ e2')
                        (AS.cutIRI $ e1')
                return
                    (sigB, [makeNamed "" axiom], sig1, sig2, eMap1', eMap2')
            RelName _r -> error "nyi" {- do
             let extPart = mkExtendedEntity e1'
                 rQName = QN "" (iriToStringUnsecure r)
                             Abbreviated (iriToStringUnsecure r) Id.nullRange
                 sym = mkEntity ObjectProperty rQName
                 rSyms = filter (== sym) $
                            Set.toList $ symOf tsig
             case rSyms of
               [] -> fail $ "relation " ++ show rQName ++
                                " not in " ++ show tsig
               [rsym] -> do
                 let sym'@(Entity _ ObjectProperty rQName') =
                             Map.findWithDefault rsym rsym eMap2'
                     axiom = PlainAxiom extPart $
                              ListFrameBit (Just SubClass) $
                               ExpressionBit [([],
                                ObjectValuesFrom
                                 SomeValuesFrom
                                 (ObjectProp rQName')
                                 (Expression $ cutIRI e2'))]
                 sigB' <- addSymbToSign sigB sym'
                 sig2' <- addSymbToSign sig2 rsym
                 return
                   (sigB', [makeNamed "" axiom], sig1, sig2', eMap1',
                      Map.union eMap2' $ Map.fromAscList [(rsym, sym')])
               _ -> fail $ "too many matches for " ++ show rQName -}
            _ -> fail $ "nyi:" ++ show rref
          _ -> fail $ "non-unique symbol match:" ++ showDoc l1 " "
                                                 ++ showDoc l2 " "
    _ -> fail "terms not yet supported in alignments"

