content: {- |
  Module      :  ./Framework/Analysis.hs
  Description :  Analyzes a logic definition
  Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  k.sojakova@jacobs-university.de
  Stability   :  experimental
  Portability :  portable
  -}
  
  module Framework.Analysis
       ( anaLogicDef
       , anaComorphismDef
       , addLogic2LogicList
       ) where
  
  import Framework.AS
  import Framework.Logic_Framework
  
  import qualified LF.Logic_LF as Logic_LF
  import qualified Isabelle.Logic_Isabelle as Logic_Isabelle
  import qualified Maude.Logic_Maude as Logic_Maude
  
  import Data.List
  import Data.Maybe
  import qualified Data.Map as Map
  
  import Static.DevGraph
  import Static.DgUtils
  import Static.GTheory
  
  import System.Directory
  
  import Logic.Grothendieck
  import Logic.ExtSign
  import Logic.Logic
  import Logic.Comorphism
  import Logic.Coerce
  
  import Common.Result
  import Common.Parsec
  import Common.AnnoState
  import Common.Lexer
  import Common.Token
  import Common.Id
  import Common.IRI (iriToStringUnsecure, nullIRI)
  import Common.Keywords
  import Common.ExtSign
  
  import Text.ParserCombinators.Parsec
  
  import LF.Framework ()
  
  dynLogicsDir :: FilePath
  dynLogicsDir = "Comorphisms"
  
  dynLogicsFile :: FilePath
  dynLogicsFile = "DynLogicList.hs"
  
  dynLogicsCon :: String
  dynLogicsCon = "dynLogicList"
  
  dynComorphismsDir :: FilePath
  dynComorphismsDir = "Comorphisms"
  
  dynComorphismsFile :: FilePath
  dynComorphismsFile = "DynComorphismList.hs"
  
  dynComorphismsCon :: String
  dynComorphismsCon = "dynComorphismList"
  
  {- ----------------------------------------------------------------------------
  Logic analysis -}
  
  -- analyzes a logic definition
  anaLogicDef :: LogicDef -> DGraph -> IO DGraph
  anaLogicDef ld dg =
    case meta ld of
      LF -> anaLogicDefH Logic_LF.LF ld dg
      Isabelle -> anaLogicDefH Logic_Isabelle.Isabelle ld dg
      Maude -> anaLogicDefH Logic_Maude.Maude ld dg
  
  anaLogicDefH :: LogicalFramework lid sublogics basic_spec sentence symb_items
                         symb_map_items sign morphism symbol raw_symbol
                         proof_tree
                  => lid -> LogicDef -> DGraph -> IO DGraph
  anaLogicDefH ml ld dg =
    case retrieveDiagram ml ld dg of
         Result _ (Just (ltruth, lmod, found, lpf)) -> do
             let l = iriToStringUnsecure $ newlogicName ld
             buildLogic ml l ltruth lmod found lpf
             addLogic2LogicList l
             return $ addLogicDef2DG ld dg
         _ -> error ""
  
  {- constructs the diagram in the signature category of the meta logic
     which represents the object logic -}
  retrieveDiagram :: LogicalFramework lid sublogics basic_spec sentence symb_items
                            symb_map_items sign morphism symbol raw_symbol
                            proof_tree
                     => lid -> LogicDef -> DGraph ->
                        Result (morphism, Maybe morphism,
                                Maybe sign, Maybe morphism)
  retrieveDiagram ml (LogicDef _ _ s m f p _) dg = do
    ltruth <- lookupMorph ml s dg
    lmod <- if m == nullIRI
               then return Nothing
               else do v <- lookupMorph ml m dg
                       return $ Just v
    found <- if f == nullIRI
                then return Nothing
                else do v <- lookupSig ml f dg
                        return $ Just v
    lpf <- if p == nullIRI
              then return Nothing
              else do v <- lookupMorph ml p dg
                      return $ Just v
  {- if (dom ltruth /= base_sig ml) then
  error $ "The morphism " ++ (show s) ++
  " must originate from the Base signature for " ++
  (show ml) ++ "." else do -}
    if isJust lmod && dom (fromJust lmod) /= cod ltruth then
       error $ "The morphisms " ++ show s ++
               " and " ++ show m ++ " must be composable."
      else if isJust lpf && dom (fromJust lpf) /= cod ltruth then
       error $ "The morphisms " ++ show s ++
               " and " ++ show p ++ " must be composable."
      else return (ltruth, lmod, found, lpf)
  
  -- creates a node for the logic definition
  addLogicDef2DG :: LogicDef -> DGraph -> DGraph
  addLogicDef2DG ld dg =
    let node = getNewNodeDG dg
        name = newlogicName ld
        nodeName = emptyNodeName { getName = name }
        info = newNodeInfo DGBasic
        extSign = makeExtSign Framework ld
        gth = noSensGTheory Framework extSign startSigId
        nodeLabel = newInfoNodeLab nodeName info gth
        dg1 = insNodeDG (node, nodeLabel) dg
  
        emptyNode = EmptyNode $ Logic Framework
        genSig = GenSig emptyNode [] emptyNode
        nodeSig = NodeSig node $ G_sign Framework extSign startSigId
        gEntry = SpecEntry $ ExtGenSig genSig nodeSig
        dg2 = dg1 { globalEnv = Map.insert name gEntry $ globalEnv dg1 }
     in dg2
  
  -- constructs the logic instance for the object logic
  buildLogic :: LogicalFramework lid sublogics basic_spec sentence symb_items
                      symb_map_items sign morphism symbol raw_symbol proof_tree
                => lid -> String -> morphism -> Maybe morphism ->
                   Maybe sign -> Maybe morphism -> IO ()
  buildLogic ml l ltruth maybeMod _ maybePf = do
    exists <- doesDirectoryExist l
    if exists then
       error $ "The directory " ++ l ++ " already exists.\n" ++
               "Please choose a different object logic name." else do
        createDirectory l
        let logicCl = write_logic ml l
        writeFile (l ++ "/" ++ "Logic_" ++ l ++ ".hs") logicCl
        let syntaxCl = write_syntax ml l ltruth
        writeFile (l ++ "/" ++ "Syntax.hs") syntaxCl
        if isNothing maybeMod then
          error $ "Please provide a model theory for " ++ l ++ "\n" else do
            let modCl = write_model ml l $ fromJust maybeMod
            writeFile (l ++ "/" ++ "Model.hs") modCl
            if isNothing maybePf then
              error $ "Please provide a proof theory for " ++ l ++ "\n" else do
                  let proofCl = write_proof ml l $ fromJust maybePf
                  writeFile (l ++ "/" ++ "Proof.hs") proofCl
                  return ()
  
  -- includes the newly-defined logic in the logic list
  addLogic2LogicList :: String -> IO ()
  addLogic2LogicList l = do
    let file = dynLogicsDir ++ "/" ++ dynLogicsFile
    contentsOld <- readFile file
    let res = runParser (parser l) (emptyAnnos ()) "" contentsOld
    case res of
      Right contentsNew -> if isInfixOf ("import " ++ l ++ ".Logic_" ++ l) contentsOld
        then
        error $ show $ l ++ " already in DynLogicList"
        else
        writeFile file contentsNew
      Left er -> error $ show er
  {- ----------------------------------------------------------------------------
  Comorphism analysis -}
  
  anaComorphismDef :: ComorphismDef -> DGraph -> IO DGraph
  anaComorphismDef cd dg =
    case metaC cd of
      LF -> anaComorphismDefH Logic_LF.LF cd dg
      Isabelle -> anaComorphismDefH Logic_Isabelle.Isabelle cd dg
      Maude -> anaComorphismDefH Logic_Maude.Maude cd dg
  
  anaComorphismDefH :: LogicalFramework lid sublogics basic_spec sentence symb_items
                              symb_map_items sign morphism symbol raw_symbol
                              proof_tree
                       => lid -> ComorphismDef -> DGraph -> IO DGraph
  anaComorphismDefH ml (ComorphismDef nc m sL tL sM pM mM) dg =
     let c = iriToStringUnsecure nc
         s = iriToStringUnsecure sL
         t = iriToStringUnsecure tL
     in case anaComH ml (ComorphismDef nc m sL tL sM pM mM) dg of
          Result _ (Just (symM, pfM, modM)) -> do
               buildComorphism ml c s t symM pfM modM
               addComorphism2ComorphismList c
               return $ addComorphismDef2DG (ComorphismDef nc m sL tL sM pM mM) dg
          _ -> error ""
  
  anaComH :: LogicalFramework lid sublogics basic_spec sentence symb_items
                              symb_map_items sign morphism symbol raw_symbol
                              proof_tree
                       => lid -> ComorphismDef -> DGraph -> Result (morphism,
                              morphism, morphism)
  anaComH ml (ComorphismDef _ _ sL tL sM pM mM) dg =
       let sLName = iriToStringUnsecure sL
           tLName = iriToStringUnsecure tL
           sLSyn = getMorphL ml sLName "Syntax"
           sLPf = getMorphL ml sLName "Proof"
           sLMod = getMorphL ml sLName "Model"
           tLSyn = getMorphL ml tLName "Syntax"
           tLPf = getMorphL ml tLName "Proof"
           tLMod = getMorphL ml tLName "Model" in do
       synM <- lookupMorph ml sM dg
       pfM <- lookupMorph ml pM dg
       modM <- lookupMorph ml mM dg
       if cod sLSyn /= dom synM then error $
        "the domain of the syntax morphism has" ++
        " to be the syntax of the source logic.\n"
        else if cod tLSyn /= cod synM then error $
          "the codomain of the syntax morphism has" ++
          " to be the syntax of the target logic.\n"
              else if cod sLPf /= dom pfM then error $
                "the domain of the proof morphism has to be the" ++
                " proof theory of the source logic.\n" ++ show (cod sLPf) ++
                "\n\n" ++ show (dom pfM) ++ "\n"
                    else if cod tLPf /= cod pfM then error $
                      "the codomain of the proof morphism has" ++
                      " to be the proof theory of the target logic.\n"
                              else if cod sLMod /= dom modM
                              then error $ "the domain of the model morphism" ++
                              " has to be the model theory of the source logic.\n"
                              ++ show (cod sLMod) ++ "\n" ++ show (dom modM)
                              ++ "\n"
                                else if cod tLMod /= cod modM then error $
                                  "the codomain of the model morphism has" ++
                                  " to be the model theory of the target logic.\n"
                                     else case (composeMorphisms synM tLPf,
                                                composeMorphisms sLPf pfM) of
                                        (Result _ comM1, Result _ comM2) ->
                                         if comM1 /= comM2 then error $
                                             "the syntax - proof diagram does" ++
                                             " not commute.\n"
                                         else case (composeMorphisms synM tLMod,
                                                    composeMorphisms sLPf modM) of
                                               (Result _ comM3, Result _ comM4) ->
                                                if comM3 /= comM4 then error $
                                                  "the syntax - model diagram" ++
                                                  " does not commute.\n"
                                                else return (synM, pfM, modM)
  
  getMorphL :: LogicalFramework lid sublogics basic_spec sentence symb_items
                              symb_map_items sign morphism symbol raw_symbol
                              proof_tree
                       => lid -> String -> String -> morphism
  getMorphL ml logicName fileName =
       let file = logicName ++ "/" ++ fileName ++ ".hs"
       in read_morphism ml file
  
  addComorphismDef2DG :: ComorphismDef -> DGraph -> DGraph
  addComorphismDef2DG cd dg =
    let node = getNewNodeDG dg
        name = newcomorphismName cd
        nodeName = emptyNodeName { getName = name }
        info = newNodeInfo DGBasic
        extSign = makeExtSign FrameworkCom cd
        gth = noSensGTheory FrameworkCom extSign startSigId
        nodeLabel = newInfoNodeLab nodeName info gth
        dg1 = insNodeDG (node, nodeLabel) dg
  
        emptyNode = EmptyNode $ Logic FrameworkCom
        genSig = GenSig emptyNode [] emptyNode
        nodeSig = NodeSig node $ G_sign FrameworkCom extSign startSigId
        gEntry = SpecEntry $ ExtGenSig genSig nodeSig
        dg2 = dg1 { globalEnv = Map.insert name gEntry $ globalEnv dg1 }
    in dg2
  
  
  buildComorphism :: LogicalFramework lid sublogics basic_spec sentence symb_items
                      symb_map_items sign morphism symbol raw_symbol proof_tree
                => lid -> String -> String -> String
                     -> morphism -> morphism -> morphism -> IO ()
  buildComorphism ml c s t synM pfM modM = do
    exists <- doesFileExist ("Comorphisms" ++ "/" ++ c ++ ".hs")
    if exists
       then error $ "The comorphism " ++ c ++ "already exists.\n"
       else do
          let comorphismC = write_comorphism ml c s t synM pfM modM
          writeFile ("Comorphisms" ++ "/" ++ c ++ ".hs") comorphismC
          return ()
  
  addComorphism2ComorphismList :: String -> IO ()
  addComorphism2ComorphismList c = do
    let file = dynComorphismsDir ++ "/" ++ dynComorphismsFile
    contentsOld <- readFile file
    let res = runParser (parserc c) (emptyAnnos ()) "" contentsOld  -- !!
    case res of
        Right contentsNew -> writeFile file contentsNew
        Left er -> error $ show er
  
  
  {- ----------------------------------------------------------------------------
  Auxiliary functions -}
  
  -- looks up a signature by name
  lookupSig :: Logic lid sublogics basic_spec sentence symb_items symb_map_items
                     sign morphism symbol raw_symbol proof_tree
               => lid -> SIG_NAME -> DGraph -> Result sign
  lookupSig l n dg = do
    let extSig = case lookupGlobalEnvDG n dg of
                   Just (SpecEntry es) -> es
                   _ -> error $ "The signature " ++ show n ++
                                " could not be found."
    case extSig of
      ExtGenSig _ (NodeSig _ (G_sign l' (ExtSign sig _) _)) ->
        if Logic l /= Logic l'
           then error $ "The signature " ++ show n ++
                        " is not in the logic " ++ show l ++ "."
           else coercePlainSign l' l "" sig
  
  -- looks up a morphism by name
  lookupMorph :: Logic lid sublogics basic_spec sentence symb_items symb_map_items
                       sign morphism symbol raw_symbol proof_tree
                 => lid -> MORPH_NAME -> DGraph -> Result morphism
  lookupMorph l n dg = do
    let extView = case lookupGlobalEnvDG n dg of
                    Just (ViewOrStructEntry _ ev) -> ev
                    _ -> error $ "The morphism " ++ show n ++
                                 " could not be found."
    case extView of
      ExtViewSig _ (GMorphism c _ _ morph _) _ -> do
        let l' = targetLogic c
        if Logic l /= Logic l'
           then error $ "The morphism " ++ show n ++
                        " is not in the logic " ++ show l ++ "."
           else coerceMorphism l' l "" morph
  
  
  parser :: String -> AParser st String
  parser l = do
    let l_imp = "import " ++ l ++ "." ++ "Logic_" ++ l
    let l_log = "Logic " ++ l
  
    header <- skipUntil "module"
    mod_decl <- do m <- asStr "module"
                   n <- moduleName
                   w <- asStr "where"
                   return $ unwords [m, n, w]
    imps <- many1 $ do
               i <- asStr "import"
               n <- moduleName
               return $ unwords [i, n]
    log_var_decl <- do v <- asStr dynLogicsCon
                       s <- asStr "::"
                       t <- do oBracketT
                               asStr "AnyLogic"
                               cBracketT
                               return "[AnyLogic]"
                       return $ unwords [v, s, t]
    log_var_def <- do v <- asStr dynLogicsCon
                      s <- asStr "="
                      return $ unwords [v, s]
    log_list <- do oBracketT
                   (do cBracketT
                       return [])
                     <|>
                     do (xs, _) <- logParser `separatedBy` commaT
                        cBracketT
                        return xs
  
    return $ header ++ mod_decl ++ "\n\n" ++
             intercalate "\n" (imps ++ [l_imp]) ++ "\n\n" ++
             log_var_decl ++ "\n" ++ log_var_def ++ " " ++ "[" ++
             intercalate ", " (log_list ++ [l_log]) ++ "]"
  
  parserc :: String -> AParser st String
  parserc c = do
       let com_imp = "import " ++ "Comorphisms." ++ c
       let com_c = "Comorphism " ++ c
  
       header <- skipUntil "module"
       mod_decl <- do m <- asStr "module"
                      n <- moduleName
                      w <- asStr "where"
                      return $ unwords [m, n, w]
       imps <- many1 $ do
                  i <- asStr "import"
                  n <- moduleName
                  return $ unwords [i, n]
       com_var_decl <- do v <- asStr dynComorphismsCon
                          s <- asStr "::"
                          t <- do oBracketT
                                  asStr "AnyComorphism"
                                  cBracketT
                                  return "[AnyComorphism]"
                          return $ unwords [v, s, t]
       com_var_def <- do v <- asStr dynComorphismsCon
                         s <- asStr "="
                         return $ unwords [v, s]
       com_list <- do oBracketT
                      (do cBracketT
                          return [])
                          <|>
                          do (xs, _) <- comParser `separatedBy` commaT
                             cBracketT
                             return xs
       return $ header ++ mod_decl ++ "\n\n" ++
                intercalate "\n" (imps ++ [com_imp]) ++ "\n\n" ++
                com_var_decl ++ "\n" ++
                com_var_def ++ " " ++ "[" ++
                intercalate ", " (com_list ++ [com_c]) ++ "]"
  
  skipUntil :: String -> AParser st String
  skipUntil lim = do
    res <- many $ reserved [lim] (many1 $ noneOf whiteChars) <|>
                  many1 (oneOf whiteChars)
    return $ concat res
  
  asStr :: String -> AParser st String
  asStr x = do
    res <- asKey x
    return $ tokStr res
  
  moduleName :: AParser st String
  moduleName = do
    m <- simpleId
    dotT
    n <- simpleId
    return $ tokStr m ++ "." ++ tokStr n
  
  logParser :: AParser st String
  logParser = do
    l <- asKey "Logic"
    n <- simpleId
    return $ tokStr l ++ " " ++ tokStr n
  
  comParser :: AParser st String
  comParser = do
       c <- asKey "Comorphism"
       n <- simpleId
       return $ tokStr c ++ " " ++ tokStr n
  