b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovaDescription : Implementation of functions necessary to instantiate
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova Logic.hs for object logics defined in LF
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovaCopyright : (c) Kristina Sojakova, DFKI Bremen 2011
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovaLicense : GPLv2 or higher, see LICENSE.txt
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovaMaintainer : k.sojakova@jacobs-university.de
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovaStability : experimental
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovaPortability : portable
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova ( basicAnalysisOL
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova , inducedFromToMorphismOL
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakovaimport qualified Data.Map as Map
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova-- basic analysis for object logics of LF
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovabasicAnalysisOL :: Morphism -> (BASIC_SPEC, Sign, GlobalAnnos) ->
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovabasicAnalysisOL ltruth (bs@(Basic_spec items), initsig, _) = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let (sig, sens) = unsafePerformIO $ makeSigSenOL ltruth initsig items
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let syms = getSymbols sig
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let fs = makeNamedForms sens $ map r_annos $ getSenItems items
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova return (bs, ExtSign sig syms, fs)
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova-- constructs the signatures and sentences
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovamakeSigSenOL :: Morphism -> Sign -> [Annoted BASIC_ITEM] ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IO (Sign, [(NAME, Sentence)])
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovamakeSigSenOL ltruth sig items = do
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova -- make a Twelf file
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let sen_type = case mapSymbol sen_type_symbol ltruth of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> error badSenTypeError
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova Just t -> show $ pretty t
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let lSyn = target ltruth
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova file <- mkImport lSyn
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova let imp = mkRead file
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova let cont1 = if sig == lSyn then "" else printLocalDefs sig
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let cont2 = printSigItems $ getSigItems items
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let cont3 = printSenItems sen_type $ getSenItems items
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let s1 = mkSig gen_sig1 $ mkIncl (sigModule lSyn) ++ cont1 ++ cont2
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let s2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont3
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let contents = imp ++ "\n" ++ s1 ++ "\n" ++ s2
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova writeFile gen_file contents
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova -- run Twelf on the created file
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova libs <- twelf2SigMor HETS gen_file
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova -- construct the signature and sentences
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova sig1 <- getSigFromLibs gen_sig1 libs
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova sig2 <- getSigFromLibs gen_sig2 libs
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let sens = getSens sig2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (sig1, sens)
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina SojakovamkImport :: Sign -> IO String
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina SojakovamkImport lSyn = do
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova file <- fromLibName LATIN $ sigBase lSyn
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova toRelativeURI file
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina SojakovaprintLocalDefs :: Sign -> String
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina SojakovaprintLocalDefs sig =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if null (getLocalDefs sig) then "" else
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder show (vcat $ map pretty $ getLocalDefs sig) ++ "\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ---------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder--------------------------------------------------------------- -}
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova-- induced_from_to_morphism for object logics
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovainducedFromToMorphismOL :: Morphism -> Map.Map RAW_SYM RAW_SYM ->
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova ExtSign Sign Symbol -> ExtSign Sign Symbol ->
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova Result Morphism
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovainducedFromToMorphismOL ltruth m (ExtSign sig1 _) (ExtSign sig2 _) =
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova inducedFromToMorphism (translMapAnalysisOL ltruth m sig1 sig2) sig1 sig2
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova{- converts a mapping of raw symbols to a mapping of symbols to expressions
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova annotated with their type -}
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovatranslMapAnalysisOL :: Morphism -> Map.Map RAW_SYM RAW_SYM -> Sign ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Sign -> Map.Map Symbol (EXP, EXP)
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovatranslMapAnalysisOL ltruth m sig1 sig2 =
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova let syms = getUnknownSyms (Map.keys m) sig1
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova in if not (null syms) then error $ badSymsError syms else
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova unsafePerformIO $ codAnalysisOL ltruth m sig2
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovacodAnalysisOL :: Morphism -> Map.Map RAW_SYM RAW_SYM -> Sign ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IO (Map.Map Symbol (EXP, EXP))
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovacodAnalysisOL ltruth m sig2 = do
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova -- make a Twelf file
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova let lSyn = target ltruth
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova file <- mkImport lSyn
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova let imp = mkRead file
52ec6e9a9bdc1f0a24a84a9f7d1090e7ffb28e7aKristina Sojakova let cont1 = if sig2 == lSyn then "" else printLocalDefs sig2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let cont2 = concatMap (\ (k, v) -> genPref k ++ " = " ++ v ++ ".\n") $
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let s1 = mkSig gen_sig1 $ mkIncl (sigModule lSyn) ++ cont1
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let s2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont2
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova let contents = imp ++ "\n" ++ s1 ++ "\n" ++ s2
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova writeFile gen_file contents
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova -- run Twelf on the created file
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova libs <- twelf2SigMor HETS gen_file
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova -- construct the mapping
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova sig' <- getSigFromLibs gen_sig2 libs
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova return $ getMap sig'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- -------------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------------------------------------------------------------- -}
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina Sojakova-- ERROR MESSAGES
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovabadSenTypeError :: String
b3bacd257ffcdd346b70ab690f03b28ad5f33fdcKristina SojakovabadSenTypeError = "Sentence type cannot be constructed."