ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaDescription : Static analysis for the Edinburgh Logical Framework
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaCopyright : (c) Kristina Sojakova, DFKI Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaMaintainer : k.sojakova@jacobs-university.de
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaStability : experimental
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovaPortability : portable
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovaimport qualified Data.Map as Map
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakovaimport qualified Data.Set as Set
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakovasen_type_exp :: EXP
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakovasen_type_exp = Type
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovagen_file :: String
118add2c5ac398465f6f66adb165852dffe1264dKristina Sojakovagen_file = gen_base
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakovagen_sig1 :: String
118add2c5ac398465f6f66adb165852dffe1264dKristina Sojakovagen_sig1 = gen_module
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakovagen_sig2 :: String
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakovagen_sig2 = gen_module ++ "'"
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovagenPref :: String -> String
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovagenPref s = gen ++ s
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakovagen_ax :: String
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakovagen_ax = genPref "ax"
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovanumSuf :: String -> Int -> String
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovanumSuf s i = s ++ "_" ++ show i
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovamkSig :: String -> String -> String
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovamkSig n cont = "%sig " ++ n ++ " = {\n" ++ cont ++ "}.\n"
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovamkIncl :: String -> String
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovamkIncl n = "%include " ++ n ++ " %open.\n"
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovamkRead :: String -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermkRead n = "%read \"" ++ n ++ "\".\n"
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovagetSigItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovagetSigItems = filter ( \ (Annoted i _ _ _) ->
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova Decl _ -> True
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova Form _ -> False )
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovagetSenItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina SojakovagetSenItems = filter ( \ (Annoted i _ _ _) ->
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova Decl _ -> False
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova Form _ -> True )
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovaprintSigItems :: [Annoted BASIC_ITEM] -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder concatMap (\ (Annoted i _ _ _) ->
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova Decl d -> d ++ ".\n"
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovaprintSenItems :: String -> [Annoted BASIC_ITEM] -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintSenItems sen_type = printSenItemsH sen_type 0
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovaprintSenItemsH :: String -> Int -> [Annoted BASIC_ITEM] -> String
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovaprintSenItemsH _ _ [] = ""
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintSenItemsH sen_type num (i : is) =
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova Annoted (Form f) _ _ _ ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let lab = getRLabel i
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova lab' = if null lab then numSuf gen_ax num else lab
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova num' = if null lab then num + 1 else num
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova in lab' ++ " : " ++ sen_type ++ " = " ++ f ++ ".\n" ++
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova printSenItemsH sen_type num' is
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova _ -> printSenItemsH sen_type num is
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeNamedForms :: [(NAME, Sentence)] -> [[Annotation]] -> [Named Sentence]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeNamedForms = zipWith (curry makeNamedForm)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeNamedForm :: ((NAME, Sentence), [Annotation]) -> Named Sentence
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeNamedForm ((n, s), annos) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let implies = any isImplies annos
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder implied = any isImplied annos
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova isTheorem = implies || implied
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova in (makeNamed n s) {isAxiom = not isTheorem}
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina SojakovagetSigFromLibs :: MODULE -> LIBS -> IO Sign
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina SojakovagetSigFromLibs n libs = do
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova lname <- toLibName HETS gen_file
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let (sigs, _) = Map.findWithDefault (error badLibError) lname libs
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova return $ Map.findWithDefault (error $ badSigError n) n sigs
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina SojakovagetUnknownSyms :: [RAW_SYM] -> Sign -> [RAW_SYM]
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina SojakovagetUnknownSyms syms sig =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder syms \\ Set.toList (Set.map symName $ getLocalSyms sig)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ---------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder--------------------------------------------------------------- -}
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina Sojakova-- basic analysis for LF
ccaa75089b23c0f043cdbd4001cba4e076ca4fd3Kristina SojakovabasicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovabasicAnalysis (bs@(Basic_spec items), initsig, _) = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let (sig, sens) = unsafePerformIO $ makeSigSen initsig items
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova let syms = getSymbols sig
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova let fs = makeNamedForms sens $ map r_annos $ getSenItems items
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova return (bs, ExtSign sig syms, fs)
e8dd447a2aa5fbac10668749dfe4142c05ec3d7dKristina Sojakova-- constructs the signatures and sentences
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeSigSen :: Sign -> [Annoted BASIC_ITEM] -> IO (Sign, [(NAME, Sentence)])
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina SojakovamakeSigSen sig items = do
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova -- make a Twelf file
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let sen_type = show $ pretty sen_type_exp
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let cont1 = if null (getDefs sig) then "" else show (pretty sig) ++ "\n"
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let cont2 = printSigItems $ getSigItems items
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let cont3 = printSenItems sen_type $ getSenItems items
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let s1 = mkSig gen_sig1 $ cont1 ++ cont2
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let s2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont3
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let contents = s1 ++ "\n" ++ s2
5e35940c3516ccea02caa0450d2b075de0106fa5Kristina Sojakova writeFile gen_file contents
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova -- run Twelf on the created file
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova libs <- twelf2SigMor HETS gen_file
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova -- construct the signature and sentences
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova sig1 <- getSigFromLibs gen_sig1 libs
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova sig2 <- getSigFromLibs gen_sig2 libs
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova let sens = getSens sig2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (sig1, sens)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetSens :: Sign -> [(NAME, Sentence)]
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova map (\ (Def s _ v) ->
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova Nothing -> error $ badValError $ symName s
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova Just v' -> (symName s, v')
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova ) $ getLocalDefs sig
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ---------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder--------------------------------------------------------------- -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- symbol analysis for LF
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovasymbAnalysis :: [SYMB_ITEMS] -> Result [RAW_SYM]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersymbAnalysis ss = Result [] $ Just $ concatMap (\ (Symb_items s) -> s) ss
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- symbol map analysis for LF
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovasymbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result (Map.Map RAW_SYM RAW_SYM)
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovasymbMapAnalysis ss = Result [] $ Just $
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova foldl (\ m s -> Map.union m (makeSymbMap s)) Map.empty ss
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovamakeSymbMap :: SYMB_MAP_ITEMS -> Map.Map RAW_SYM RAW_SYM
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina SojakovamakeSymbMap (Symb_map_items ss) =
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova foldl (\ m s -> case s of
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova Symb s1 -> Map.insert s1 s1 m
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova Symb_map s1 s2 -> Map.insert s1 s2 m
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ---------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder--------------------------------------------------------------- -}
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova-- converts a mapping of raw symbols to a mapping of symbols
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina SojakovarenamMapAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> Map.Map Symbol Symbol
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina SojakovarenamMapAnalysis m sig =
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova let syms1 = getUnknownSyms (Map.keys m) sig
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder syms2 = filter (not . isSym) $ Map.elems m
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder syms = syms1 ++ syms2
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova in if not (null syms) then error $ badSymsError syms else
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.fromList $ map (\ (k, v) -> (toSym k, toSym v)) $ Map.toList m
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova{- converts a mapping of raw symbols to a mapping of symbols to expressions
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova annotated with their type -}
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovatranslMapAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> Sign ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.Map Symbol (EXP, EXP)
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovatranslMapAnalysis m sig1 sig2 =
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova let syms = getUnknownSyms (Map.keys m) sig1
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova in if not (null syms) then error $ badSymsError syms else
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova unsafePerformIO $ codAnalysis m sig2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercodAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> IO (Map.Map Symbol (EXP, EXP))
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovacodAnalysis m sig2 = do
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova -- make a Twelf file
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let cont1 = show (pretty sig2) ++ "\n"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let cont2 = concatMap (\ (k, v) -> genPref k ++ " = " ++ v ++ ".\n") $
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let s1 = mkSig gen_sig1 cont1
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let s2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont2
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova let contents = s1 ++ "\n" ++ s2
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova writeFile gen_file contents
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova -- run Twelf on the created file
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova libs <- twelf2SigMor HETS gen_file
d71bb9deea089887b4fd829c5b766e7e4de9f204Kristina Sojakova -- construct the mapping
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina Sojakova sig' <- getSigFromLibs gen_sig2 libs
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova return $ getMap sig'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetMap :: Sign -> Map.Map Symbol (EXP, EXP)
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovagetMap sig = Map.fromList $ map
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova (\ (Def s t v) ->
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova Nothing -> error $ badValError $ symName s
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova Just v' -> let Just n = stripPrefix gen $ symName s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in (toSym n, (v', t))
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova ) $ getLocalDefs sig
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- -------------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------------------------------------------------------------- -}
abd5fc85dc7e19b1614890182436940e922963a4Kristina Sojakova-- ERROR MESSAGES
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovabadLibError :: String
3c0bf20712a0f21aaedc0a9a9c8376bc1e90e799Kristina SojakovabadLibError = "Library " ++ gen_file ++ " not found."
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovabadSigError :: MODULE -> String
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovabadSigError n = "Signature " ++ n ++ " not found."
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina SojakovabadSymsError :: [String] -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederbadSymsError ss = "Symbols " ++ show ss ++
168d206b4e5fd436c98239a1b6629c651f54c8eeKristina Sojakova " are unknown or are not locally accessible."
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovabadValError :: String -> String
abd5fc85dc7e19b1614890182436940e922963a4Kristina SojakovabadValError s = "Symbol " ++ s ++ "does not have a value."