content: {- |
  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 qualified Control.Monad.Fail as Fail
  
  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.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)
  