{- |

Module : $Header$

Description : Static analysis for the Edinburgh Logical Framework

Copyright : (c) Kristina Sojakova, DFKI Bremen 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : k.sojakova@jacobs-university.de

Stability : experimental

Portability : portable

-}

module LF.Analysis where

import LF.AS

import LF.Sign

import LF.Twelf2GR

import Common.ExtSign

import Common.GlobalAnnotations

import Common.AS_Annotation

import Common.Result

import Common.DocUtils

import Data.List

import qualified Data.Map as Map

import qualified Data.Set as Set

import System.IO.Unsafe

sen_type_exp :: EXP

sen_type_exp = Type

gen_file :: String

gen_file = gen_base

gen_sig1 :: String

gen_sig1 = gen_module

gen_sig2 :: String

gen_sig2 = gen_module ++ "'"

gen :: String

gen = "gen_"

genPref :: String -> String

genPref s = gen ++ s

gen_ax :: String

gen_ax = genPref "ax"

numSuf :: String -> Int -> String

numSuf s i = s ++ "_" ++ show i

mkSig :: String -> String -> String

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

mkIncl :: String -> String

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

mkRead :: String -> String

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

getSigItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]

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

case i of

Decl _ -> True

Form _ -> False )

getSenItems :: [Annoted BASIC_ITEM] -> [Annoted BASIC_ITEM]

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

case i of

Decl _ -> False

Form _ -> True )

printSigItems :: [Annoted BASIC_ITEM] -> String

printSigItems =

concatMap (\ (Annoted i _ _ _) ->

case i of

Decl d -> d ++ ".\n"

_ -> ""

)

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

printSenItems sen_type = printSenItemsH sen_type 0

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

printSenItemsH _ _ [] = ""

printSenItemsH sen_type num (i : is) =

case i of

Annoted (Form f) _ _ _ ->

let lab = getRLabel i

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

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

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

printSenItemsH sen_type num' is

_ -> printSenItemsH sen_type num is

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

makeNamedForms = zipWith (curry makeNamedForm)

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

makeNamedForm ((n, s), annos) =

let implies = any isImplies annos

implied = any isImplied annos

isTheorem = implies || implied

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

getSigFromLibs :: MODULE -> LIBS -> IO Sign

getSigFromLibs n libs = do

lname <- toLibName HETS gen_file

let (sigs, _) = Map.findWithDefault (error badLibError) lname libs

return $ Map.findWithDefault (error $ badSigError n) n sigs

getUnknownSyms :: [RAW_SYM] -> Sign -> [RAW_SYM]

getUnknownSyms syms sig =

syms \\ Set.toList (Set.map symName $ getLocalSyms sig)

{- ---------------------------------------------------------------

--------------------------------------------------------------- -}

-- basic analysis for LF

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

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

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

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

let syms = getSymbols sig

let fs = makeNamedForms sens $ map r_annos $ getSenItems items

return (bs, ExtSign sig syms, fs)

-- constructs the signatures and sentences

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

makeSigSen sig items = do

-- make a Twelf file

let sen_type = show $ pretty sen_type_exp

let cont1 = if null (getDefs sig) then "" else show (pretty sig) ++ "\n"

let cont2 = printSigItems $ getSigItems items

let cont3 = printSenItems sen_type $ getSenItems items

let s1 = mkSig gen_sig1 $ cont1 ++ cont2

let s2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont3

let contents = s1 ++ "\n" ++ s2

writeFile gen_file contents

-- run Twelf on the created file

libs <- twelf2SigMor HETS gen_file

-- construct the signature and sentences

sig1 <- getSigFromLibs gen_sig1 libs

sig2 <- getSigFromLibs gen_sig2 libs

let sens = getSens sig2

return (sig1, sens)

getSens :: Sign -> [(NAME, Sentence)]

getSens sig =

map (\ (Def s _ v) ->

case v of

Nothing -> error $ badValError $ symName s

Just v' -> (symName s, v')

) $ getLocalDefs sig

{- ---------------------------------------------------------------

--------------------------------------------------------------- -}

-- symbol analysis for LF

symbAnalysis :: [SYMB_ITEMS] -> Result [RAW_SYM]

symbAnalysis ss = Result [] $ Just $ concatMap (\ (Symb_items s) -> s) ss

-- symbol map analysis for LF

symbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result (Map.Map RAW_SYM RAW_SYM)

symbMapAnalysis ss = Result [] $ Just $

foldl (\ m s -> Map.union m (makeSymbMap s)) Map.empty ss

makeSymbMap :: SYMB_MAP_ITEMS -> Map.Map RAW_SYM RAW_SYM

makeSymbMap (Symb_map_items ss) =

foldl (\ m s -> case s of

Symb s1 -> Map.insert s1 s1 m

Symb_map s1 s2 -> Map.insert s1 s2 m

) Map.empty ss

{- ---------------------------------------------------------------

--------------------------------------------------------------- -}

-- converts a mapping of raw symbols to a mapping of symbols

renamMapAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> Map.Map Symbol Symbol

renamMapAnalysis m sig =

let syms1 = getUnknownSyms (Map.keys m) sig

syms2 = filter (not . isSym) $ Map.elems m

syms = syms1 ++ syms2

in if not (null syms) then error $ badSymsError syms else

Map.fromList $ map (\ (k, v) -> (toSym k, toSym v)) $ Map.toList m

{- converts a mapping of raw symbols to a mapping of symbols to expressions

annotated with their type -}

translMapAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> Sign ->

Map.Map Symbol (EXP, EXP)

translMapAnalysis m sig1 sig2 =

let syms = getUnknownSyms (Map.keys m) sig1

in if not (null syms) then error $ badSymsError syms else

unsafePerformIO $ codAnalysis m sig2

codAnalysis :: Map.Map RAW_SYM RAW_SYM -> Sign -> IO (Map.Map Symbol (EXP, EXP))

codAnalysis m sig2 = do

-- make a Twelf file

let cont1 = show (pretty sig2) ++ "\n"

let cont2 = concatMap (\ (k, v) -> genPref k ++ " = " ++ v ++ ".\n") $

Map.toList m

let s1 = mkSig gen_sig1 cont1

let s2 = mkSig gen_sig2 $ mkIncl gen_sig1 ++ cont2

let contents = s1 ++ "\n" ++ s2

writeFile gen_file contents

-- run Twelf on the created file

libs <- twelf2SigMor HETS gen_file

-- construct the mapping

sig' <- getSigFromLibs gen_sig2 libs

return $ getMap sig'

getMap :: Sign -> Map.Map Symbol (EXP, EXP)

getMap sig = Map.fromList $ map

(\ (Def s t v) ->

case v of

Nothing -> error $ badValError $ symName s

Just v' -> let Just n = stripPrefix gen $ symName s

in (toSym n, (v', t))

) $ getLocalDefs sig

{- -------------------------------------------------------------------------

------------------------------------------------------------------------- -}

-- ERROR MESSAGES

badLibError :: String

badLibError = "Library " ++ gen_file ++ " not found."

badSigError :: MODULE -> String

badSigError n = "Signature " ++ n ++ " not found."

badSymsError :: [String] -> String

badSymsError ss = "Symbols " ++ show ss ++

" are unknown or are not locally accessible."

badValError :: String -> String

badValError s = "Symbol " ++ s ++ "does not have a value."