{- |

Module : ./LF/ImplOL.hs

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 = concatMap (\ (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."