content: {- |
  Module      :  ./NeSyPatterns/Analysis.hs
  Description :  Basic analysis for propositional logic
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Stability   :  experimental
  Portability :  portable
  
  Basic and static analysis for propositional logic
  
    Ref.
    <http://en.wikipedia.org/wiki/NeSyPatterns_logic>
  -}
  
  module NeSyPatterns.Analysis
      ( basicNeSyPatternsAnalysis
      , mkStatSymbItems
      , mkStatSymbMapItem
      , inducedFromMorphism
      , inducedFromToMorphism
      , signatureColimit
      , subClassRelation
      )
      where
  
  
  import Data.Maybe (fromMaybe)
  import Data.Foldable (foldrM, foldlM)
  import Data.List (stripPrefix)
  import Data.Bifunctor (bimap, Bifunctor (second))
  
  import Control.Applicative
  import Common.ExtSign
  import Common.IRI
  import Common.Lib.Graph
  import Common.Result (resultToMaybe)
  import Common.SetColimit
  import Common.Utils
  
  import NeSyPatterns.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.Graph.Inductive.Graph as Gr
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import qualified Data.Relation as Rel
  import qualified NeSyPatterns.AS as AS
  import qualified NeSyPatterns.Morphism as Morphism
  import qualified NeSyPatterns.Symbol as Symbol
  import qualified OWL2.AS as OWL2
  
  -- | Retrieves the signature out of a basic spec
  makeSig ::
      AS.BASIC_SPEC                         -- Input SPEC
      -> Sign.Sign                          -- Input Signature
      -> Result.Result Sign.Sign                   -- Output Signature
  makeSig bs sig = let spec' = genIds bs in
    foldrM retrieveBasicItem sig spec'
  
  addNodeToIdMap :: AS.Node -> Map.Map IRI IRI -> Map.Map IRI IRI
  addNodeToIdMap (AS.Node o mi _) m = case mi of
    Just i -> Map.insert i o m
    Nothing -> m
  
  addPathToIdMap :: AS.BASIC_ITEM -> Map.Map IRI IRI -> Map.Map IRI IRI
  addPathToIdMap (AS.Path ns) m = foldr addNodeToIdMap m ns
  
  extractIdMap :: AS.BASIC_SPEC -> Map.Map IRI IRI
  extractIdMap (AS.Basic_spec spec) = foldr addPathToIdMap Map.empty (AS_Anno.item <$> spec)
  
  genIds :: AS.BASIC_SPEC -> [AS.BASIC_ITEM]
  genIds (AS.Basic_spec paths) = snd $ foldr genIdsPath (0, []) $ AS_Anno.item <$> paths
  
  genIdsPath :: AS.BASIC_ITEM -> (Int, [AS.BASIC_ITEM]) -> (Int, [AS.BASIC_ITEM])
  genIdsPath (AS.Path ns) (genId, agg) = (: agg) . AS.Path <$> foldr genIdsNode (genId, []) ns
  
  genIdsNode :: AS.Node -> (Int, [AS.Node]) -> (Int, [AS.Node])
  genIdsNode node (genId, agg) = (: agg) <$> genIdNode genId node
  
  genIdNode :: Int -> AS.Node -> (Int, AS.Node)
  genIdNode genId node = case AS.nesyId node of
    Nothing -> (genId + 1, node { AS.nesyId = Just . idToIRI . Id.mkId $ [ Id.genNumVar "nesy" genId ] })
    Just _ -> (genId, node)
  
  
  -- Helper for makeSig
  retrieveBasicItem ::
      AS.BASIC_ITEM              -- Input Item
      -> Sign                                          -- Input Signature
      -> Result.Result Sign                                -- Output Signature
  retrieveBasicItem x sig = let sigM = Just sig in case x of
        AS.Path [] -> return sig
        AS.Path ns -> do
          let n0 = last ns
          n0' <- resolveNode sigM n0
          let sig' = addToSig sig n0'
          (_, sig'') <- foldrM (\f (t, s) -> do
              resolvedFrom <- resolveNode sigM f
              return (resolvedFrom, addEdgeToSig' s (resolvedFrom, t))
            ) (n0', sig') (init ns)
          return sig''
  
  
  {- | @resolveNode sm n@ converts @n@ to a @ResolvedNode@ if it's ontology term
    is declared in the data ontology @owlClasses s@. If @n@ does not contain an id,
    @findId@ is used to try to match it.
     -}
  resolveNode :: Maybe Sign -- ^ 
    -> AS.Node -- ^ 
    -> Result.Result ResolvedNode
  resolveNode sigM n@(AS.Node o mi r) = case mi of
      Just i -> case sigM of
        Just sig -> if Set.member o (owlClasses sig) then
            return $ ResolvedNode o i r
          else
            Result.mkError "Undefined class" n
  
        Nothing -> return $ ResolvedNode o i r
      Nothing -> case sigM of
        Just sig -> case findId o $ nodes sig of
          Just i -> return $ ResolvedNode o i r
          Nothing -> Result.mkError "Cannot uniquely resolve unset nesyid." n
        Nothing -> Result.mkError "Unset nesyid." n
  
  {- | @findId o f@ finds a the id used to refer to @o@ in @f@ if there is exactly
    one id used in @f@ to refer to @o@ -}
  findId :: Foldable t => IRI -- ^ Ontology term which id should be found
    -> t ResolvedNode -- ^ List of nodes in which @o@ should be searched
    -> Maybe IRI
  findId o = foldr (\n' r -> case (r, resolvedOTerm n' == o) of
            (Nothing, True)  -> Just $ resolvedNeSyId n'
            (Just i, True) | i /= resolvedNeSyId n' -> Nothing
            _ -> r) Nothing
  
  -- | Basic analysis 
  basicNeSyPatternsAnalysis
    :: (AS.BASIC_SPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
    -> Result.Result (AS.BASIC_SPEC,
                      ExtSign Sign.Sign Symbol.Symbol,
                      [AS_Anno.Named ()])
  basicNeSyPatternsAnalysis (spec, sig, _) = do
    let idm = extractIdMap spec
    sign <- makeSig spec sig { idMap = idm }
    return (spec, ExtSign sign (Set.map Symbol.Symbol $ Sign.nodes sign), [])
  
  -- | Static analysis for symbol maps
  mkStatSymbMapItem :: Sign -> Maybe Sign -> [AS.SYMB_MAP_ITEMS]
                    -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
  mkStatSymbMapItem sig sigM = return . foldr 
    (\(AS.Symb_map_items sitem _) -> Map.union $ statSymbMapItem sig sigM sitem)
    Map.empty
  
  statSymbMapItem :: Sign.Sign -> Maybe Sign -> [AS.SYMB_OR_MAP]
                   -> Map.Map Symbol.Symbol Symbol.Symbol
  statSymbMapItem sig sigM = let s = fromMaybe sig sigM in foldr (\x mmap ->
           case x of
             AS.Symb sym -> Map.insert (symbToSymbol sig sym) (symbToSymbol sig sym) mmap
             AS.Symb_map s1 s2 _ ->
                 Map.insert (symbToSymbol sig s1) (symbToSymbol s s2) mmap
      ) Map.empty
  
  -- | Retrieve raw symbols
  mkStatSymbItems :: Sign.Sign -> [AS.SYMB_ITEMS] -> Result.Result [Symbol.Symbol]
  mkStatSymbItems sig a = do
      resolvedSymbols <- mapM (resolveNode (Just sig)) [t | (AS.Symb_items r _) <- a, (AS.Symb_id t) <- r]
      return $ Symbol.Symbol <$> resolvedSymbols
  
  symbToSymbol :: Sign.Sign -> AS.SYMB -> Symbol.Symbol
  symbToSymbol sig (AS.Symb_id node) = let
      resolved = resolveNode (Just sig) node
      nextId = nextGenId sig
      (_, newId) = genIdNode nextId node
      nodeM = resultToMaybe $ resolved <|> resolveNode (Just sig) newId
    in case nodeM of
    Just n -> Symbol.Symbol n
    Nothing -> error "NeSyPatterns.Analysis.symbToSymbol: Cannot convert symbol"
  
  
  
  makePMapR :: Map.Map Symbol.Symbol Symbol.Symbol
    -> Map.Map ResolvedNode ResolvedNode
  makePMapR = Map.fromList . fmap (bimap Symbol.node Symbol.node) . Map.toList
  
  -- | Induce a signature morphism from a source signature and a raw symbol map
  inducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                      -> Sign.Sign
                      -> Result.Result Morphism.Morphism
  inducedFromMorphism imap sig = let pMap = makePMapR imap in
                return
                Morphism.Morphism
                            { Morphism.source = sig
                            , Morphism.owlMap = Map.empty
                            , Morphism.nodeMap = pMap
                            , Morphism.target = Sign.emptySig
                              { Sign.nodes = Set.map (Morphism.applyMap pMap)
                                $ Sign.nodes sig }
                            }
  
  -- | Induce a signature morphism from a source signature and a raw symbol map
  inducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                      -> ExtSign Sign.Sign Symbol.Symbol
                      -> ExtSign Sign.Sign Symbol.Symbol
                      -> Result.Result Morphism.Morphism
  inducedFromToMorphism imap (ExtSign sig _) (ExtSign tSig _) =
                let
                    targetSig = Sign.Sign {
                      Sign.owlClasses = Set.empty, --TODO
                      Sign.owlTaxonomy = Rel.empty, -- TODO
                      Sign.nodes = Set.empty, -- Set.map (Morphism.applyMap pMap) $ Sign.nodes sig,
                      Sign.edges = Rel.empty,
                      Sign.idMap = Map.empty } -- TODO: IMPLEMENT
                    isSub = Sign.nodes targetSig `Set.isSubsetOf` Sign.nodes tSig
                in if isSub then return Morphism.Morphism
                       { Morphism.source = sig
                       , Morphism.nodeMap = makePMapR imap
                       , Morphism.owlMap = Map.empty -- TODO
                       , Morphism.target = tSig
                       }
                       else fail "Incompatible mapping"
  
  -- | Retrieves a relation of simple classes from a set of axioms. If (a SubClassOf b) then (a ~ b)
  subClassRelation :: [OWL2.Axiom] -> Rel.Relation IRI IRI
  subClassRelation axs = Rel.fromList [ (cl1, cl2) | OWL2.ClassAxiom (OWL2.SubClassOf _ (OWL2.Expression cl1) (OWL2.Expression cl2)) <- axs]
  
  computeGLB :: (Ord a, Show a) => Rel.Relation a a -> Set.Set a -> Maybe a
  computeGLB r s =
   let getAllBounds aSet =
        let aBounds = Set.unions $ map (`Rel.lookupRan` r) $ Set.toList aSet
        in if Set.isSubsetOf aBounds aSet
              then aSet
              else getAllBounds $ Set.union aBounds aSet
       bounds = map (getAllBounds . (\x -> Set.union (Set.singleton x) $ Rel.lookupRan x r)) (Set.toList s)
   in case bounds of
        [] -> Nothing
        aSet : sets ->
          let intBounds = foldl Set.intersection aSet sets
          in if null intBounds then Nothing
             else let isLB y = let notR = Set.filter (\x -> Rel.notMember x y r && x /= y ) intBounds
                                in Set.null notR
                      gbs = Set.filter isLB intBounds
                  in case Set.toList gbs of
                      [x] -> Just x
                      _ -> Nothing
  
  allLabels :: [(Int, Set.Set ResolvedNode)] -- the graph nodes
            -> Map.Map Int (Map.Map IRI IRI) -- the structural morphisms f of the colimit on nodeIds
            -> IRI -- the nodeId N in the colimit 
            -> Set.Set ResolvedNode
            -- all resolved nodes in the graph whose nodeId is mapped to N 
            -- along the corresponding morphism in f
  allLabels nSets tMaps cId =
    foldl (\aSet (iMap, s) -> Set.union aSet $
                              Set.filter (\(ResolvedNode _ nId _) -> cId == Map.findWithDefault nId nId iMap) s)
          Set.empty $ map (\(i, s) -> (Map.findWithDefault (error "missing index") i tMaps, s))nSets
  
  signatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
                   -> Result.Result (Sign.Sign, Map.Map Int Morphism.Morphism)
  signatureColimit graph = do
    let owlGraph = Gr.nmap Sign.owlClasses $
                   Gr.emap (Data.Bifunctor.second Morphism.owlMap) graph
        (owlC, owlMors) = addIntToSymbols $ computeColimitSet owlGraph
        owlR = colimitRel ( map(second owlTaxonomy) $ Gr.labNodes graph) owlMors
        graph1 = Gr.nmap (Set.map Sign.resolvedNeSyId . Sign.nodes) $
                 Gr.emap (second Morphism.morphism2TokenMap) graph
        (nodeSet, maps) = addIntToSymbols $ computeColimitSet graph1
    resSet <- foldlM (\aSet aNode -> do
                          let labSet = Set.map Sign.resolvedOTerm $
                                       allLabels (map (second nodes) $ Gr.labNodes graph) maps aNode
                          case computeGLB owlR labSet of
                            Nothing -> fail "couldn't compute greatest lower bound"
                            Just glb -> return $ Set.insert (ResolvedNode glb aNode Id.nullRange) aSet
                       ) Set.empty nodeSet
    nMaps <- foldlM (\f (i, sig) -> do
                      let fi = Map.findWithDefault (error "missing morphism") i maps
                      gi <- Morphism.tokenMap2NodeMap (Sign.nodes sig) resSet fi
                      return $ Map.insert i gi f
                    )
             Map.empty $ Gr.labNodes graph
    let edgesC = colimitRel ( map(second edges) $ Gr.labNodes graph) nMaps
        colimSig = Sign{ owlClasses = owlC
                       , owlTaxonomy = owlR
                       , nodes = resSet
                       , edges = edgesC
                       , idMap = nesyIdMap resSet}
        colimMors = Map.fromList $
                    map (\(i, sig) -> let oi = Map.findWithDefault (error "owl map") i owlMors
                                          ni = Map.findWithDefault (error "node map") i nMaps
                                     in (i, Morphism.Morphism sig colimSig oi ni) ) $ Gr.labNodes graph
    return (colimSig, colimMors)
  
  nextGenId :: Sign.Sign -> Int
  nextGenId sig = foldr (\n genId -> fromMaybe genId $ do
        genId' <- genIdFromNode n
        return $ if genId' > genId then genId' else genId
      ) 0 (Sign.nodes sig) + 1
    where
      genIdFromNode :: Sign.ResolvedNode -> Maybe Int
      genIdFromNode n = do
        num <- stripPrefix (Id.genNamePrefix ++ "nesy") . iFragment . Sign.resolvedNeSyId $ n
        readMaybe num
  