{- |
Module      :  $Header$
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
