Analysis.hs revision ccaa75089b23c0f043cdbd4001cba4e076ca4fd3
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Static analysis for the Edinburgh Logical Framework
c4cd5501ab6853608f700a2765a73ae16261f96cChristian MaederCopyright : (c) Kristina Sojakova, DFKI Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b463427f6976f49999a07231105cc2747a21cd7bChristian MaederMaintainer : k.sojakova@jacobs-university.de
c4cd5501ab6853608f700a2765a73ae16261f96cChristian MaederStability : experimental
c4cd5501ab6853608f700a2765a73ae16261f96cChristian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski Currently not used; requires refactoring of Twelf2DG.hs
ad602cf9fc48c213018a82f87f6f92575866061eTill Mossakowski ( basicAnalysis
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaeder , symbAnalysis
b463427f6976f49999a07231105cc2747a21cd7bChristian Maeder , symbMapAnalysis
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederimport qualified Data.Set as Set
fabb65de6a1d71c8519bd153fadc83cb935e9311Christian Maederimport qualified Data.Map as Map
6f449482b2ca9189ac5fe5d3b2e1cb8de6e10cbcMarkus Grossgen_file :: String
79720ebb1315d79df06c83b31b6f0158f83679f3cmaedergen_sig :: String
dbc1dad13708ae8bba42eac4eff53a11346b2391Christian Maedergen_sig = "GEN_SIG"
482d08605917ba2e28b6c780d6e405bc97203ccdChristian Maedergen_ax :: String
6f449482b2ca9189ac5fe5d3b2e1cb8de6e10cbcMarkus Grossgen_ax = "gen_ax"
cd2265c1c7279c901e34383275e0ca44a11d5d6cMingyi LiusenSuf :: String -> String
15fb3ebbbc5e26b5b389ac49a0abdc5f2cc05955Christian MaedersenSuf sn = sn ++ "_SEN"
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian MaedernumSuf :: String -> Int -> String
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian MaedernumSuf s i = s ++ "_" ++ show i
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian MaederwrapInSig :: String -> String -> String
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian MaederwrapInSig sn cont = "%sig " ++ sn ++ " = {\n" ++ cont ++ "}."
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian MaederwrapInIncl :: String -> String
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian MaederwrapInIncl sn = "%include " ++ sn ++ " %open."
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian MaedergetSentenceAnnos :: [Annoted BASIC_ITEM] ->
8b32a507c12da7310d156de55322eb05c9314676cmaeder-----------------------------------------------------------------
8b32a507c12da7310d156de55322eb05c9314676cmaeder-----------------------------------------------------------------
a5e1617d14b530f09732afbb3ef71f59ea0d2123Christian Maeder-- basic analysis for LF
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian MaederbasicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->
482d08605917ba2e28b6c780d6e405bc97203ccdChristian Maeder Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederbasicAnalysis (bs, initsig, _) =
8b32a507c12da7310d156de55322eb05c9314676cmaeder if initsig /= emptySig
b2686b2e4779d302fd5e7ebfd20126511613dfe7Markus Gross then error "Structuring for LF nyi."
0abb18fa401863f1f738b68e37e2753b334560d4Christian Maeder else do makeTwelfFile gen_file gen_sig bs
0abb18fa401863f1f738b68e37e2753b334560d4Christian Maeder (sig,sen) <- getSigSen gen_file
0abb18fa401863f1f738b68e37e2753b334560d4Christian Maeder let syms = getAllSymbols sig
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian Maeder let fs = makeNamedFormulas sen
4f81ba7f36814cda63fbd75351abe3f9d88dcb97Christian Maeder return $ Just $ (bs, ExtSign sig syms, fs)
42c48d599c91a7cdec2bcfb5385684712e627907cmaedermakeNamedFormulas :: Sign -> [Named EXP]
bf28fda4cb91c15978baf8543314642f46c3476ccmaedermakeNamedFormulas (Sign _ _ ds) =
42c48d599c91a7cdec2bcfb5385684712e627907cmaedermakeNamedFormula :: DEF -> Named EXP
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedermakeNamedFormula (Def s t _) =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let isImplies = or $ map isImplies annos
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaeder isImplied = or $ map isImplied annos
bf28fda4cb91c15978baf8543314642f46c3476ccmaeder isTheorem = isImplies || isImplied
6eca9a49786384e7573736cac1a6430afd0e1b3bcmaeder-- converts the basic spec into a Twelf file
22b9153fa40713977fa959bd752184204a9c041dcmaedermakeTwelfFile :: FilePath -> String -> BASIC_SPEC -> IO ()
22b9153fa40713977fa959bd752184204a9c041dcmaedermakeTwelfFile file sn (Basic_spec items) = do
22b9153fa40713977fa959bd752184204a9c041dcmaeder let sig = wrapInSig sn $ printSigItems items
6eca9a49786384e7573736cac1a6430afd0e1b3bcmaeder let sen = wrapInSig (senSuf sn) $
6eca9a49786384e7573736cac1a6430afd0e1b3bcmaeder wrapInIncl sn ++ printSenItems items
e5bf1cecd6f65e5c36b033d9d3f93938846a9ec9cmaeder writeFile file $ sig ++ "\n\n" ++ sen
6eca9a49786384e7573736cac1a6430afd0e1b3bcmaederprintSigItems :: [Annoted BASIC_ITEM] -> String
6eca9a49786384e7573736cac1a6430afd0e1b3bcmaederprintSigItems [] = ""
6eca9a49786384e7573736cac1a6430afd0e1b3bcmaederprintSigItems (i:is) =
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaeder Annoted (Decl d) _ _ _ -> d ++ ".\n" ++ printSigItems is
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaeder _ -> printSigItems is
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaederprintSenItems :: [Annoted BASIC_ITEM] -> String
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaederprintSenItems items = printSenItemsH 0 items
6eca9a49786384e7573736cac1a6430afd0e1b3bcmaederprintSenItemsH :: Int -> [Annoted BASIC_ITEM] -> String
6eca9a49786384e7573736cac1a6430afd0e1b3bcmaederprintSenItemsH _ [] = ""
c127b5cc51ba9dd992c3c3d14444a6ed1ce88c67cmaederprintSenItemsH num (i:is) =
c127b5cc51ba9dd992c3c3d14444a6ed1ce88c67cmaeder Annoted (Form f) _ _ _ ->
c127b5cc51ba9dd992c3c3d14444a6ed1ce88c67cmaeder let label = getRLabel i
c127b5cc51ba9dd992c3c3d14444a6ed1ce88c67cmaeder nam = if null label then numSuf gen_ax num else label
c127b5cc51ba9dd992c3c3d14444a6ed1ce88c67cmaeder num' = if null label then num + 1 else num
c127b5cc51ba9dd992c3c3d14444a6ed1ce88c67cmaeder in nam ++ " : " ++ f ++ ".\n" ++ printSenItemsH num' is
22b9153fa40713977fa959bd752184204a9c041dcmaeder _ -> printSenItemsH num is
22b9153fa40713977fa959bd752184204a9c041dcmaeder-- retrieves the signatures containing basic spec declarations and sentences
22b9153fa40713977fa959bd752184204a9c041dcmaedergetSigSen :: FilePath -> String -> IO (Sign,Sign)
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaedergetSigSen fp sn = do
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaeder file <- resolveToCur fp
2c99ff994b966dc293a1592c7c7e3cc09acdaac4cmaeder runTwelf file
b2686b2e4779d302fd5e7ebfd20126511613dfe7Markus Gross (_,_,(sigmap,_)) <- buildGraph file (emptyLibEnv,emptyGrMap)
b2686b2e4779d302fd5e7ebfd20126511613dfe7Markus Gross let base = dropExtension file
b2686b2e4779d302fd5e7ebfd20126511613dfe7Markus Gross let sn' = senSuf sn
b2686b2e4779d302fd5e7ebfd20126511613dfe7Markus Gross let sig1 = Map.findWithDefault (error $ sn ++ " not found.")
fddece8c9a8ccf6113561535d8365989a238fc86cmaeder (base,sn) sigmap
c698ca3d47b105a82ec1f19e8c6bc29ab1d1b63dChristian Maeder let sig2 = Map.findWithDefault (error $ sn' ++ " not found.")
fddece8c9a8ccf6113561535d8365989a238fc86cmaeder (base,sn') sigmap
b2686b2e4779d302fd5e7ebfd20126511613dfe7Markus Gross return (sig1,sig2)