842ae4bd224140319ae7feec1872b93dfd491143fielding{- |

842ae4bd224140319ae7feec1872b93dfd491143fieldingModule : $Header$

842ae4bd224140319ae7feec1872b93dfd491143fieldingDescription : Static analysis for the Edinburgh Logical Framework

842ae4bd224140319ae7feec1872b93dfd491143fieldingCopyright : (c) Kristina Sojakova, DFKI Bremen 2010

842ae4bd224140319ae7feec1872b93dfd491143fieldingLicense : GPLv2 or higher, see LICENSE.txt

842ae4bd224140319ae7feec1872b93dfd491143fielding

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzMaintainer : k.sojakova@jacobs-university.de

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndStability : experimental

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzPortability : portable

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd-}

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndmodule LF.Analysis where

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.AS

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndimport LF.Sign

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzimport LF.Twelf2GR

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzimport Common.ExtSign

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzimport Common.GlobalAnnotations

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzimport Common.AS_Annotation

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzimport Common.Result

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzimport Common.DocUtils

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzimport qualified Data.Map as Map

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzimport System.IO.Unsafe

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzsen_type_exp :: EXP

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzsen_type_exp = Type

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgen_file :: String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgen_file = "gen_twelf_file.elf"

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgen_sig1 :: String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgen_sig1 = "GEN_SIG"

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgen_sig2 :: String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgen_sig2 = "GEN_SIG_SEN"

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgen_ax :: String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgen_ax = "gen_ax"

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantznumSuf :: String -> Int -> String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantznumSuf s i = s ++ "_" ++ show i

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmkSig :: String -> String -> String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmkSig n cont = "%sig " ++ n ++ " = {\n" ++ cont ++ "}.\n"

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmkIncl :: String -> String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmkIncl n = "%include " ++ n ++ " %open.\n"

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmkRead :: String -> String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmkRead n = "%read \"" ++ n ++ "\".\n"

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSigItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSigItems = filter ( \ (Annoted i _ _ _) ->

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz case i of

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz Decl _ -> True

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz Form _ -> False )

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSenItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSenItems = filter ( \ (Annoted i _ _ _) ->

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz case i of

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz Decl _ -> False

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz Form _ -> True )

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSensFromDefs :: [DEF] -> [(NAME,Sentence)]

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSensFromDefs [] = []

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSensFromDefs ((Def s _ (Just v)):ds) = (symName s, v) : getSensFromDefs ds

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSensFromDefs _ = error "Sentences cannot be retrieved from definitions."

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmakeNamedForms :: [(NAME,Sentence)] -> [[Annotation]] -> [Named Sentence]

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmakeNamedForms ss as = map makeNamedForm $ zip ss as

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmakeNamedForm :: ((NAME,Sentence),[Annotation]) -> Named Sentence

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmakeNamedForm ((n,s),annos) =

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let implies = or $ map isImplies annos

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz implied = or $ map isImplied annos

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz isTheorem = implies || implied

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz in (makeNamed n s) {isAxiom = not isTheorem}

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz-----------------------------------------------------------------

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz-----------------------------------------------------------------

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz-- basic analysis for LF

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

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

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzbasicAnalysis (bs@(Basic_spec items), initsig, _) = do

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let (sig,sens) = unsafePerformIO $ makeSigSen initsig items

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let syms = getSymbols sig

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let fs = makeNamedForms sens $ map r_annos $ getSenItems items

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz return (bs, ExtSign sig syms, fs)

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz-- constructs the signatures and sentences

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmakeSigSen :: Sign -> [Annoted BASIC_ITEM] -> IO (Sign,[(NAME,Sentence)])

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmakeSigSen sig items = do

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let contents = makeFile sig (getSigItems items) (getSenItems items)

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz writeFile gen_file contents

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz libs <- twelf2SigMor gen_file

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz getSigSen libs

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz{- constructs the contents of a Twelf file used to analyze the signature

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz and sentences -}

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmakeFile :: Sign -> [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM] -> String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzmakeFile sig sig_items sen_items =

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let sen_type = show $ pretty sen_type_exp

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz cont1 = if (sig == emptySig) then "" else show (pretty sig) ++ "\n"

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz cont2 = printSigItems sig_items

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz cont3 = printSenItems sen_type sen_items

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz sig1 = mkSig gen_sig1 $ cont1 ++ cont2

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz sig2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont3

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz in sig1 ++ "\n" ++ sig2

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzprintSigItems :: [Annoted BASIC_ITEM] -> String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzprintSigItems [] = ""

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzprintSigItems (i:is) =

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz case i of

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

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz _ -> printSigItems is

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzprintSenItems :: String -> [Annoted BASIC_ITEM] -> String

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzprintSenItems sen_type items = printSenItemsH sen_type 0 items

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

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

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzprintSenItemsH _ _ [] = ""

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzprintSenItemsH sen_type num (i:is) =

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz case i of

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz Annoted (Form f) _ _ _ ->

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let lab = getRLabel i

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz lab' = if null lab then numSuf gen_ax num else lab

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz num' = if null lab then num + 1 else num

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz in lab' ++ " : " ++ sen_type ++ " = " ++ f ++ ".\n" ++

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz printSenItemsH sen_type num' is

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz _ -> printSenItemsH sen_type num is

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz{- retrieves the signature and sentences corresponding to the

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz original basic spec out of a Twelf file -}

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSigSen :: LIBS -> IO (Sign,[(NAME,Sentence)])

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantzgetSigSen libs = do

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz file <- resolveToCur gen_file

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let (sigs,_) = Map.findWithDefault (error "Library not found.")

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz (toLibName file) libs

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let sig1 = Map.findWithDefault (er gen_sig1) gen_sig1 sigs

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let sig2 = Map.findWithDefault (er gen_sig2) gen_sig2 sigs

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz let sens = getSensFromDefs $ filter (\ d -> isLocalSym (getSym d) sig2)

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz $ getDefs sig2

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz return (sig1,sens)

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz where er n = error $ "Signature " ++ n ++ " not found."

ea5f8cfbb7ef1d19318f6994c26dd73c38ffd8ddjerenkrantz