5255N/A{- |

5255N/AModule : $Header$

5255N/ADescription : Static analysis for the Edinburgh Logical Framework

5255N/ACopyright : (c) Kristina Sojakova, DFKI Bremen 2010

5255N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

5255N/A

5255N/AMaintainer : k.sojakova@jacobs-university.de

5255N/AStability : experimental

5255N/APortability : portable

5255N/A

5255N/A Currently not used; requires refactoring of Twelf2DG.hs

5255N/A-}

5255N/A

5255N/Amodule LF.Analysis

5255N/A ( basicAnalysis

5255N/A , symbAnalysis

5255N/A , symbMapAnalysis

5255N/A ) where

5255N/A

5255N/Aimport LF.AS

5255N/Aimport LF.Sign

5255N/Aimport LF.Twelf2DG

5255N/A

5255N/Aimport Common.DocUtils

5255N/Aimport Common.ExtSign

5255N/Aimport Common.GlobalAnnotations

5255N/Aimport Common.AS_Annotation

5255N/Aimport Common.Id

5255N/Aimport Common.Result

5255N/A

5255N/Aimport qualified Data.Set as Set

5255N/Aimport qualified Data.Map as Map

5255N/A

5255N/Aimport Static.DevGraph

5255N/A

5255N/Aimport System.FilePath

5255N/A

5255N/Agen_file :: String

5255N/Agen_file = "gen_twelf_file.elf"

5255N/A

5255N/Agen_sig :: String

5255N/Agen_sig = "GEN_SIG"

5255N/A

5255N/Agen_ax :: String

5255N/Agen_ax = "gen_ax"

5255N/A

5255N/AsenSuf :: String -> String

5255N/AsenSuf sn = sn ++ "_SEN"

5255N/A

5255N/AnumSuf :: String -> Int -> String

5255N/AnumSuf s i = s ++ "_" ++ show i

5255N/A

5255N/AwrapInSig :: String -> String -> String

5255N/AwrapInSig sn cont = "%sig " ++ sn ++ " = {\n" ++ cont ++ "}."

5255N/A

5255N/AwrapInIncl :: String -> String

5255N/AwrapInIncl sn = "%include " ++ sn ++ " %open."

5255N/A

5255N/AgetSentenceAnnos :: [Annoted BASIC_ITEM] ->

5255N/A

5255N/A-----------------------------------------------------------------

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

-- basic analysis for LF

basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->

Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])

basicAnalysis (bs, initsig, _) =

if initsig /= emptySig

then error "Structuring for LF nyi."

else do makeTwelfFile gen_file gen_sig bs

(sig,sen) <- getSigSen gen_file

let syms = getAllSymbols sig

let fs = makeNamedFormulas sen

return $ Just $ (bs, ExtSign sig syms, fs)

makeNamedFormulas :: Sign -> [Named EXP]

makeNamedFormulas (Sign _ _ ds) =

map ( -> ds

makeNamedFormula :: DEF -> Named EXP

makeNamedFormula (Def s t _) =

let isImplies = or $ map isImplies annos

isImplied = or $ map isImplied annos

isTheorem = isImplies || isImplied

-- converts the basic spec into a Twelf file

makeTwelfFile :: FilePath -> String -> BASIC_SPEC -> IO ()

makeTwelfFile file sn (Basic_spec items) = do

let sig = wrapInSig sn $ printSigItems items

let sen = wrapInSig (senSuf sn) $

wrapInIncl sn ++ printSenItems items

writeFile file $ sig ++ "\n\n" ++ sen

printSigItems :: [Annoted BASIC_ITEM] -> String

printSigItems [] = ""

printSigItems (i:is) =

case i of

Annoted (Decl d) _ _ _ -> d ++ ".\n" ++ printSigItems is

_ -> printSigItems is

printSenItems :: [Annoted BASIC_ITEM] -> String

printSenItems items = printSenItemsH 0 items

printSenItemsH :: Int -> [Annoted BASIC_ITEM] -> String

printSenItemsH _ [] = ""

printSenItemsH num (i:is) =

case i of

Annoted (Form f) _ _ _ ->

let label = getRLabel i

nam = if null label then numSuf gen_ax num else label

num' = if null label then num + 1 else num

in nam ++ " : " ++ f ++ ".\n" ++ printSenItemsH num' is

_ -> printSenItemsH num is

-- retrieves the signatures containing basic spec declarations and sentences

getSigSen :: FilePath -> String -> IO (Sign,Sign)

getSigSen fp sn = do

file <- resolveToCur fp

runTwelf file

(_,_,(sigmap,_)) <- buildGraph file (emptyLibEnv,emptyGrMap)

let base = dropExtension file

let sn' = senSuf sn

let sig1 = Map.findWithDefault (error $ sn ++ " not found.")

(base,sn) sigmap

let sig2 = Map.findWithDefault (error $ sn' ++ " not found.")

(base,sn') sigmap

return (sig1,sig2)