1e83c8de3aa48b316b28057d53995272baf1260cwrowe{- |

1e83c8de3aa48b316b28057d53995272baf1260cwroweModule : ./Framework/Analysis.hs

1e83c8de3aa48b316b28057d53995272baf1260cwroweDescription : Analyzes a logic definition

1e83c8de3aa48b316b28057d53995272baf1260cwroweCopyright : (c) Kristina Sojakova, DFKI Bremen 2010

1e83c8de3aa48b316b28057d53995272baf1260cwroweLicense : GPLv2 or higher, see LICENSE.txt

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweMaintainer : k.sojakova@jacobs-university.de

1e83c8de3aa48b316b28057d53995272baf1260cwroweStability : experimental

1e83c8de3aa48b316b28057d53995272baf1260cwrowePortability : portable

1e83c8de3aa48b316b28057d53995272baf1260cwrowe-}

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwrowemodule Framework.Analysis

1e83c8de3aa48b316b28057d53995272baf1260cwrowe ( anaLogicDef

1e83c8de3aa48b316b28057d53995272baf1260cwrowe , anaComorphismDef

1e83c8de3aa48b316b28057d53995272baf1260cwrowe , addLogic2LogicList

1e83c8de3aa48b316b28057d53995272baf1260cwrowe ) where

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Framework.AS

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Framework.Logic_Framework

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport qualified LF.Logic_LF as Logic_LF

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport qualified Isabelle.Logic_Isabelle as Logic_Isabelle

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport qualified Maude.Logic_Maude as Logic_Maude

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Data.List

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Data.Maybe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport qualified Data.Map as Map

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Static.DevGraph

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Static.DgUtils

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Static.GTheory

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport System.Directory

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Logic.Grothendieck

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Logic.ExtSign

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Logic.Logic

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Logic.Comorphism

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Logic.Coerce

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Common.Result

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Common.Parsec

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Common.AnnoState

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Common.Lexer

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Common.Token

56e85d89d42a6980f31b800266649efbed338da3wroweimport Common.Id

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Common.IRI (iriToStringUnsecure, nullIRI)

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Common.Keywords

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Common.ExtSign

37ad54b8fd2611b7a4f2b269eec3d27ed784a25dwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport Text.ParserCombinators.Parsec

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweimport LF.Framework ()

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

94b262d3639149df0b02642a9daa6db8bff58577wrowedynLogicsDir :: FilePath

94b262d3639149df0b02642a9daa6db8bff58577wrowedynLogicsDir = "Comorphisms"

94b262d3639149df0b02642a9daa6db8bff58577wrowe

94b262d3639149df0b02642a9daa6db8bff58577wrowedynLogicsFile :: FilePath

94b262d3639149df0b02642a9daa6db8bff58577wrowedynLogicsFile = "DynLogicList.hs"

94b262d3639149df0b02642a9daa6db8bff58577wrowe

94b262d3639149df0b02642a9daa6db8bff58577wrowedynLogicsCon :: String

94b262d3639149df0b02642a9daa6db8bff58577wrowedynLogicsCon = "dynLogicList"

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwrowedynComorphismsDir :: FilePath

1e83c8de3aa48b316b28057d53995272baf1260cwrowedynComorphismsDir = "Comorphisms"

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwrowedynComorphismsFile :: FilePath

1e83c8de3aa48b316b28057d53995272baf1260cwrowedynComorphismsFile = "DynComorphismList.hs"

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwrowedynComorphismsCon :: String

1e83c8de3aa48b316b28057d53995272baf1260cwrowedynComorphismsCon = "dynComorphismList"

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwrowe{- ----------------------------------------------------------------------------

1e83c8de3aa48b316b28057d53995272baf1260cwroweLogic analysis -}

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwrowe-- analyzes a logic definition

5ac28f3fe2417368757f29cf381338357605fd52wroweanaLogicDef :: LogicDef -> DGraph -> IO DGraph

e1ad80c048e29e968221817698529d73098f07a4wroweanaLogicDef ld dg =

1e83c8de3aa48b316b28057d53995272baf1260cwrowe case meta ld of

1e83c8de3aa48b316b28057d53995272baf1260cwrowe LF -> anaLogicDefH Logic_LF.LF ld dg

1e83c8de3aa48b316b28057d53995272baf1260cwrowe Isabelle -> anaLogicDefH Logic_Isabelle.Isabelle ld dg

37ad54b8fd2611b7a4f2b269eec3d27ed784a25dwrowe Maude -> anaLogicDefH Logic_Maude.Maude ld dg

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwroweanaLogicDefH :: LogicalFramework lid sublogics basic_spec sentence symb_items

1e83c8de3aa48b316b28057d53995272baf1260cwrowe symb_map_items sign morphism symbol raw_symbol

1e83c8de3aa48b316b28057d53995272baf1260cwrowe proof_tree

94b262d3639149df0b02642a9daa6db8bff58577wrowe => lid -> LogicDef -> DGraph -> IO DGraph

94b262d3639149df0b02642a9daa6db8bff58577wroweanaLogicDefH ml ld dg =

94b262d3639149df0b02642a9daa6db8bff58577wrowe case retrieveDiagram ml ld dg of

94b262d3639149df0b02642a9daa6db8bff58577wrowe Result _ (Just (ltruth, lmod, found, lpf)) -> do

94b262d3639149df0b02642a9daa6db8bff58577wrowe let l = iriToStringUnsecure $ newlogicName ld

94b262d3639149df0b02642a9daa6db8bff58577wrowe buildLogic ml l ltruth lmod found lpf

94b262d3639149df0b02642a9daa6db8bff58577wrowe addLogic2LogicList l

94b262d3639149df0b02642a9daa6db8bff58577wrowe return $ addLogicDef2DG ld dg

1e83c8de3aa48b316b28057d53995272baf1260cwrowe _ -> error ""

1e83c8de3aa48b316b28057d53995272baf1260cwrowe

1e83c8de3aa48b316b28057d53995272baf1260cwrowe{- constructs the diagram in the signature category of the meta logic

1e83c8de3aa48b316b28057d53995272baf1260cwrowe which represents the object logic -}

1e83c8de3aa48b316b28057d53995272baf1260cwroweretrieveDiagram :: LogicalFramework lid sublogics basic_spec sentence symb_items

1e83c8de3aa48b316b28057d53995272baf1260cwrowe symb_map_items sign morphism symbol raw_symbol

1e83c8de3aa48b316b28057d53995272baf1260cwrowe proof_tree

1e83c8de3aa48b316b28057d53995272baf1260cwrowe => lid -> LogicDef -> DGraph ->

1e83c8de3aa48b316b28057d53995272baf1260cwrowe Result (morphism, Maybe morphism,

1e83c8de3aa48b316b28057d53995272baf1260cwrowe Maybe sign, Maybe morphism)

1e83c8de3aa48b316b28057d53995272baf1260cwroweretrieveDiagram ml (LogicDef _ _ s m f p _) dg = do

1e83c8de3aa48b316b28057d53995272baf1260cwrowe ltruth <- lookupMorph ml s dg

1e83c8de3aa48b316b28057d53995272baf1260cwrowe lmod <- if m == nullIRI

8c8173f49dd7122e10636b3d20ae841551bd0b43wrowe then return Nothing

1e83c8de3aa48b316b28057d53995272baf1260cwrowe else do v <- lookupMorph ml m dg

1e83c8de3aa48b316b28057d53995272baf1260cwrowe return $ Just v

1e83c8de3aa48b316b28057d53995272baf1260cwrowe found <- if f == nullIRI

then return Nothing

else do v <- lookupSig ml f dg

return $ Just v

lpf <- if p == nullIRI

then return Nothing

else do v <- lookupMorph ml p dg

return $ Just v

{- if (dom ltruth /= base_sig ml) then

error $ "The morphism " ++ (show s) ++

" must originate from the Base signature for " ++

(show ml) ++ "." else do -}

if isJust lmod && dom (fromJust lmod) /= cod ltruth then

error $ "The morphisms " ++ show s ++

" and " ++ show m ++ " must be composable."

else if isJust lpf && dom (fromJust lpf) /= cod ltruth then

error $ "The morphisms " ++ show s ++

" and " ++ show p ++ " must be composable."

else return (ltruth, lmod, found, lpf)

-- creates a node for the logic definition

addLogicDef2DG :: LogicDef -> DGraph -> DGraph

addLogicDef2DG ld dg =

let node = getNewNodeDG dg

name = newlogicName ld

nodeName = emptyNodeName { getName = name }

info = newNodeInfo DGBasic

extSign = makeExtSign Framework ld

gth = noSensGTheory Framework extSign startSigId

nodeLabel = newInfoNodeLab nodeName info gth

dg1 = insNodeDG (node, nodeLabel) dg

emptyNode = EmptyNode $ Logic Framework

genSig = GenSig emptyNode [] emptyNode

nodeSig = NodeSig node $ G_sign Framework extSign startSigId

gEntry = SpecEntry $ ExtGenSig genSig nodeSig

dg2 = dg1 { globalEnv = Map.insert name gEntry $ globalEnv dg1 }

in dg2

-- constructs the logic instance for the object logic

buildLogic :: LogicalFramework lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol proof_tree

=> lid -> String -> morphism -> Maybe morphism ->

Maybe sign -> Maybe morphism -> IO ()

buildLogic ml l ltruth maybeMod _ maybePf = do

exists <- doesDirectoryExist l

if exists then

error $ "The directory " ++ l ++ " already exists.\n" ++

"Please choose a different object logic name." else do

createDirectory l

let logicCl = write_logic ml l

writeFile (l ++ "/" ++ "Logic_" ++ l ++ ".hs") logicCl

let syntaxCl = write_syntax ml l ltruth

writeFile (l ++ "/" ++ "Syntax.hs") syntaxCl

if isNothing maybeMod then

error $ "Please provide a model theory for " ++ l ++ "\n" else do

let modCl = write_model ml l $ fromJust maybeMod

writeFile (l ++ "/" ++ "Model.hs") modCl

if isNothing maybePf then

error $ "Please provide a proof theory for " ++ l ++ "\n" else do

let proofCl = write_proof ml l $ fromJust maybePf

writeFile (l ++ "/" ++ "Proof.hs") proofCl

return ()

-- includes the newly-defined logic in the logic list

addLogic2LogicList :: String -> IO ()

addLogic2LogicList l = do

let file = dynLogicsDir ++ "/" ++ dynLogicsFile

contentsOld <- readFile file

let res = runParser (parser l) (emptyAnnos ()) "" contentsOld

case res of

Right contentsNew -> if isInfixOf ("import " ++ l ++ ".Logic_" ++ l) contentsOld

then

error $ show $ l ++ " already in DynLogicList"

else

writeFile file contentsNew

Left er -> error $ show er

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

Comorphism analysis -}

anaComorphismDef :: ComorphismDef -> DGraph -> IO DGraph

anaComorphismDef cd dg =

case metaC cd of

LF -> anaComorphismDefH Logic_LF.LF cd dg

Isabelle -> anaComorphismDefH Logic_Isabelle.Isabelle cd dg

Maude -> anaComorphismDefH Logic_Maude.Maude cd dg

anaComorphismDefH :: LogicalFramework lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol

proof_tree

=> lid -> ComorphismDef -> DGraph -> IO DGraph

anaComorphismDefH ml (ComorphismDef nc m sL tL sM pM mM) dg =

let c = iriToStringUnsecure nc

s = iriToStringUnsecure sL

t = iriToStringUnsecure tL

in case anaComH ml (ComorphismDef nc m sL tL sM pM mM) dg of

Result _ (Just (symM, pfM, modM)) -> do

buildComorphism ml c s t symM pfM modM

addComorphism2ComorphismList c

return $ addComorphismDef2DG (ComorphismDef nc m sL tL sM pM mM) dg

_ -> error ""

anaComH :: LogicalFramework lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol

proof_tree

=> lid -> ComorphismDef -> DGraph -> Result (morphism,

morphism, morphism)

anaComH ml (ComorphismDef _ _ sL tL sM pM mM) dg =

let sLName = iriToStringUnsecure sL

tLName = iriToStringUnsecure tL

sLSyn = getMorphL ml sLName "Syntax"

sLPf = getMorphL ml sLName "Proof"

sLMod = getMorphL ml sLName "Model"

tLSyn = getMorphL ml tLName "Syntax"

tLPf = getMorphL ml tLName "Proof"

tLMod = getMorphL ml tLName "Model" in do

synM <- lookupMorph ml sM dg

pfM <- lookupMorph ml pM dg

modM <- lookupMorph ml mM dg

if cod sLSyn /= dom synM then error $

"the domain of the syntax morphism has" ++

" to be the syntax of the source logic.\n"

else if cod tLSyn /= cod synM then error $

"the codomain of the syntax morphism has" ++

" to be the syntax of the target logic.\n"

else if cod sLPf /= dom pfM then error $

"the domain of the proof morphism has to be the" ++

" proof theory of the source logic.\n" ++ show (cod sLPf) ++

"\n\n" ++ show (dom pfM) ++ "\n"

else if cod tLPf /= cod pfM then error $

"the codomain of the proof morphism has" ++

" to be the proof theory of the target logic.\n"

else if cod sLMod /= dom modM

then error $ "the domain of the model morphism" ++

" has to be the model theory of the source logic.\n"

++ show (cod sLMod) ++ "\n" ++ show (dom modM)

++ "\n"

else if cod tLMod /= cod modM then error $

"the codomain of the model morphism has" ++

" to be the model theory of the target logic.\n"

else case (composeMorphisms synM tLPf,

composeMorphisms sLPf pfM) of

(Result _ comM1, Result _ comM2) ->

if comM1 /= comM2 then error $

"the syntax - proof diagram does" ++

" not commute.\n"

else case (composeMorphisms synM tLMod,

composeMorphisms sLPf modM) of

(Result _ comM3, Result _ comM4) ->

if comM3 /= comM4 then error $

"the syntax - model diagram" ++

" does not commute.\n"

else return (synM, pfM, modM)

getMorphL :: LogicalFramework lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol

proof_tree

=> lid -> String -> String -> morphism

getMorphL ml logicName fileName =

let file = logicName ++ "/" ++ fileName ++ ".hs"

in read_morphism ml file

addComorphismDef2DG :: ComorphismDef -> DGraph -> DGraph

addComorphismDef2DG cd dg =

let node = getNewNodeDG dg

name = newcomorphismName cd

nodeName = emptyNodeName { getName = name }

info = newNodeInfo DGBasic

extSign = makeExtSign FrameworkCom cd

gth = noSensGTheory FrameworkCom extSign startSigId

nodeLabel = newInfoNodeLab nodeName info gth

dg1 = insNodeDG (node, nodeLabel) dg

emptyNode = EmptyNode $ Logic FrameworkCom

genSig = GenSig emptyNode [] emptyNode

nodeSig = NodeSig node $ G_sign FrameworkCom extSign startSigId

gEntry = SpecEntry $ ExtGenSig genSig nodeSig

dg2 = dg1 { globalEnv = Map.insert name gEntry $ globalEnv dg1 }

in dg2

buildComorphism :: LogicalFramework lid sublogics basic_spec sentence symb_items

symb_map_items sign morphism symbol raw_symbol proof_tree

=> lid -> String -> String -> String

-> morphism -> morphism -> morphism -> IO ()

buildComorphism ml c s t synM pfM modM = do

exists <- doesFileExist ("Comorphisms" ++ "/" ++ c ++ ".hs")

if exists

then error $ "The comorphism " ++ c ++ "already exists.\n"

else do

let comorphismC = write_comorphism ml c s t synM pfM modM

writeFile ("Comorphisms" ++ "/" ++ c ++ ".hs") comorphismC

return ()

addComorphism2ComorphismList :: String -> IO ()

addComorphism2ComorphismList c = do

let file = dynComorphismsDir ++ "/" ++ dynComorphismsFile

contentsOld <- readFile file

let res = runParser (parserc c) (emptyAnnos ()) "" contentsOld -- !!

case res of

Right contentsNew -> writeFile file contentsNew

Left er -> error $ show er

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

Auxiliary functions -}

-- looks up a signature by name

lookupSig :: Logic lid sublogics basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

=> lid -> SIG_NAME -> DGraph -> Result sign

lookupSig l n dg = do

let extSig = case lookupGlobalEnvDG n dg of

Just (SpecEntry es) -> es

_ -> error $ "The signature " ++ show n ++

" could not be found."

case extSig of

ExtGenSig _ (NodeSig _ (G_sign l' (ExtSign sig _) _)) ->

if Logic l /= Logic l'

then error $ "The signature " ++ show n ++

" is not in the logic " ++ show l ++ "."

else coercePlainSign l' l "" sig

-- looks up a morphism by name

lookupMorph :: Logic lid sublogics basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

=> lid -> MORPH_NAME -> DGraph -> Result morphism

lookupMorph l n dg = do

let extView = case lookupGlobalEnvDG n dg of

Just (ViewOrStructEntry _ ev) -> ev

_ -> error $ "The morphism " ++ show n ++

" could not be found."

case extView of

ExtViewSig _ (GMorphism c _ _ morph _) _ -> do

let l' = targetLogic c

if Logic l /= Logic l'

then error $ "The morphism " ++ show n ++

" is not in the logic " ++ show l ++ "."

else coerceMorphism l' l "" morph

parser :: String -> AParser st String

parser l = do

let l_imp = "import " ++ l ++ "." ++ "Logic_" ++ l

let l_log = "Logic " ++ l

header <- skipUntil "module"

mod_decl <- do m <- asStr "module"

n <- moduleName

w <- asStr "where"

return $ unwords [m, n, w]

imps <- many1 $ do

i <- asStr "import"

n <- moduleName

return $ unwords [i, n]

log_var_decl <- do v <- asStr dynLogicsCon

s <- asStr "::"

t <- do oBracketT

asStr "AnyLogic"

cBracketT

return "[AnyLogic]"

return $ unwords [v, s, t]

log_var_def <- do v <- asStr dynLogicsCon

s <- asStr "="

return $ unwords [v, s]

log_list <- do oBracketT

(do cBracketT

return [])

<|>

do (xs, _) <- logParser `separatedBy` commaT

cBracketT

return xs

return $ header ++ mod_decl ++ "\n\n" ++

intercalate "\n" (imps ++ [l_imp]) ++ "\n\n" ++

log_var_decl ++ "\n" ++ log_var_def ++ " " ++ "[" ++

intercalate ", " (log_list ++ [l_log]) ++ "]"

parserc :: String -> AParser st String

parserc c = do

let com_imp = "import " ++ "Comorphisms." ++ c

let com_c = "Comorphism " ++ c

header <- skipUntil "module"

mod_decl <- do m <- asStr "module"

n <- moduleName

w <- asStr "where"

return $ unwords [m, n, w]

imps <- many1 $ do

i <- asStr "import"

n <- moduleName

return $ unwords [i, n]

com_var_decl <- do v <- asStr dynComorphismsCon

s <- asStr "::"

t <- do oBracketT

asStr "AnyComorphism"

cBracketT

return "[AnyComorphism]"

return $ unwords [v, s, t]

com_var_def <- do v <- asStr dynComorphismsCon

s <- asStr "="

return $ unwords [v, s]

com_list <- do oBracketT

(do cBracketT

return [])

<|>

do (xs, _) <- comParser `separatedBy` commaT

cBracketT

return xs

return $ header ++ mod_decl ++ "\n\n" ++

intercalate "\n" (imps ++ [com_imp]) ++ "\n\n" ++

com_var_decl ++ "\n" ++

com_var_def ++ " " ++ "[" ++

intercalate ", " (com_list ++ [com_c]) ++ "]"

skipUntil :: String -> AParser st String

skipUntil lim = do

res <- many $ reserved [lim] (many1 $ noneOf whiteChars) <|>

many1 (oneOf whiteChars)

return $ concat res

asStr :: String -> AParser st String

asStr x = do

res <- asKey x

return $ tokStr res

moduleName :: AParser st String

moduleName = do

m <- simpleId

dotT

n <- simpleId

return $ tokStr m ++ "." ++ tokStr n

logParser :: AParser st String

logParser = do

l <- asKey "Logic"

n <- simpleId

return $ tokStr l ++ " " ++ tokStr n

comParser :: AParser st String

comParser = do

c <- asKey "Comorphism"

n <- simpleId

return $ tokStr c ++ " " ++ tokStr n