{- |
Module      :  $Header$
Description :  Implementation of functions necessary to instantiate
               Logic.hs for object logics defined in LF
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}
module LF.ImplOL
  ( basicAnalysisOL
  , inducedFromToMorphismOL
  ) where

import LF.AS
import LF.Sign
import LF.Morphism
import LF.Analysis
import LF.Twelf2GR
import LF.Framework

import Common.ExtSign
import Common.GlobalAnnotations
import Common.AS_Annotation
import Common.Result
import Common.Doc
import Common.DocUtils

import System.IO.Unsafe

import qualified Data.Map as Map

-- basic analysis for object logics of LF
basicAnalysisOL :: Morphism -> (BASIC_SPEC, Sign, GlobalAnnos) ->
                   Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
basicAnalysisOL ltruth (bs@(Basic_spec items), initsig, _) = do
  let (sig,sens) = unsafePerformIO $ makeSigSenOL ltruth initsig items
  let syms = getSymbols sig
  let fs = makeNamedForms sens $ map r_annos $ getSenItems items
  return (bs, ExtSign sig syms, fs)

-- constructs the signatures and sentences
makeSigSenOL :: Morphism -> Sign -> [Annoted BASIC_ITEM] ->
                IO (Sign,[(NAME,Sentence)])
makeSigSenOL ltruth sig items = do
  -- make a Twelf file
  let sen_type = case mapSymbol sen_type_symbol ltruth of
                      Nothing -> error $ badSenTypeError
                      Just t -> show $ pretty t
  let lSyn = target ltruth
  file <- mkImport lSyn
  let imp = mkRead file
  let cont1 = if sig == lSyn then "" else printLocalDefs sig
  let cont2 = printSigItems $ getSigItems items
  let cont3 = printSenItems sen_type $ getSenItems items
  let s1 = mkSig gen_sig1 $ mkIncl (sigModule lSyn) ++ cont1 ++ cont2
  let s2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont3
  let contents = imp ++ "\n" ++ s1 ++ "\n" ++ s2
  writeFile gen_file contents
  
  -- run Twelf on the created file
  libs <- twelf2SigMor HETS gen_file
  
  -- construct the signature and sentences
  sig1 <- getSigFromLibs gen_sig1 libs
  sig2 <- getSigFromLibs gen_sig2 libs
  let sens = getSens sig2
  return (sig1,sens)

mkImport :: Sign -> IO String
mkImport lSyn = do
  file <- fromLibName LATIN $ sigBase lSyn
  toRelativeURI file

printLocalDefs :: Sign -> String
printLocalDefs sig =
  if (null $ getLocalDefs sig) then "" else
     (show $ vcat $ map pretty $ getLocalDefs sig) ++ "\n"

-----------------------------------------------------------------
-----------------------------------------------------------------

-- induced_from_to_morphism for object logics
inducedFromToMorphismOL :: Morphism -> Map.Map RAW_SYM RAW_SYM ->
                           ExtSign Sign Symbol -> ExtSign Sign Symbol ->
                           Result Morphism
inducedFromToMorphismOL ltruth m (ExtSign sig1 _) (ExtSign sig2 _) =
  inducedFromToMorphism (translMapAnalysisOL ltruth m sig1 sig2) sig1 sig2

{- converts a mapping of raw symbols to a mapping of symbols to expressions
   annotated with their type -}
translMapAnalysisOL :: Morphism -> Map.Map RAW_SYM RAW_SYM -> Sign ->
                       Sign -> Map.Map Symbol (EXP,EXP)
translMapAnalysisOL ltruth m sig1 sig2 =
  let syms = getUnknownSyms (Map.keys m) sig1
      in if not (null syms) then error $ badSymsError syms else
         unsafePerformIO $ codAnalysisOL ltruth m sig2

codAnalysisOL :: Morphism -> Map.Map RAW_SYM RAW_SYM -> Sign ->
                 IO (Map.Map Symbol (EXP,EXP))
codAnalysisOL ltruth m sig2 = do
  -- make a Twelf file
  let lSyn = target ltruth
  file <- mkImport lSyn
  let imp = mkRead file
  let cont1 = if sig2 == lSyn then "" else printLocalDefs sig2
  let cont2 = concat $ map (\ (k,v) -> (genPref k) ++ " = " ++ v ++ ".\n") $
                 Map.toList m
  let s1 = mkSig gen_sig1 $ mkIncl (sigModule lSyn) ++ cont1
  let s2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont2
  let contents = imp ++ "\n" ++ s1 ++ "\n" ++ s2
  writeFile gen_file contents

  -- run Twelf on the created file
  libs <- twelf2SigMor HETS gen_file
  
  -- construct the mapping
  sig' <- getSigFromLibs gen_sig2 libs
  return $ getMap sig'

---------------------------------------------------------------------------
---------------------------------------------------------------------------

-- ERROR MESSAGES
badSenTypeError :: String
badSenTypeError = "Sentence type cannot be constructed."
