4632N/ADescription : Analyzes a logic definition
4632N/ACopyright : (c) Kristina Sojakova, DFKI Bremen 2010
4632N/AMaintainer : k.sojakova@jacobs-university.de
dynLogicsDir = "Comorphisms"
dynLogicsFile :: FilePath
dynLogicsCon = "dynLogicList"
dynComorphismsDir :: FilePath
dynComorphismsDir = "Comorphisms"
dynComorphismsFile :: FilePath
dynComorphismsCon :: String
dynComorphismsCon = "dynComorphismList"
{- ----------------------------------------------------------------------------
-- analyzes a logic definition
anaLogicDef :: LogicDef -> DGraph -> IO DGraph
anaLogicDefH :: LogicalFramework lid sublogics basic_spec sentence symb_items
symb_map_items sign morphism symbol raw_symbol
=> lid -> LogicDef -> DGraph -> IO DGraph
case retrieveDiagram ml ld dg of
Result _ (Just (ltruth, lmod, found, lpf)) -> do
let l = iriToStringUnsecure $ newlogicName ld
buildLogic ml l ltruth lmod found lpf
return $ addLogicDef2DG ld dg
{- constructs the diagram in the signature category of the meta logic
which represents the object logic -}
retrieveDiagram :: LogicalFramework lid sublogics basic_spec sentence symb_items
symb_map_items sign morphism symbol raw_symbol
=> lid -> LogicDef -> DGraph ->
Result (morphism, Maybe morphism,
Maybe sign, Maybe morphism)
retrieveDiagram ml (LogicDef _ _ s m f p _) dg = do
ltruth <- lookupMorph ml s dg
else do v <- lookupMorph ml m dg
else do v <- lookupSig ml f dg
else do v <- lookupMorph ml p dg
{- 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
let node = getNewNodeDG dg
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 }
-- 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
error $ "The directory " ++ l ++ " already exists.\n" ++
"Please choose a different object logic name." else do
let logicCl = write_logic ml l
writeFile (l ++ "/" ++ "Logic_" ++ l ++ ".hs") logicCl
let syntaxCl = write_syntax ml l ltruth
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
-- 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
Right contentsNew -> if isInfixOf ("import " ++ l ++ ".Logic_" ++ l) contentsOld
error $ show $ l ++ " already in DynLogicList"
writeFile file contentsNew
Left er -> error $ show er
{- ----------------------------------------------------------------------------
anaComorphismDef :: ComorphismDef -> DGraph -> IO DGraph
anaComorphismDefH :: LogicalFramework lid sublogics basic_spec sentence symb_items
symb_map_items sign morphism symbol raw_symbol
=> 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
anaComH :: LogicalFramework lid sublogics basic_spec sentence symb_items
symb_map_items sign morphism symbol raw_symbol
=> lid -> ComorphismDef -> DGraph -> Result (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)
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" ++
else case (composeMorphisms synM tLMod,
composeMorphisms sLPf modM) of
(Result _ comM3, Result _ comM4) ->
if comM3 /= comM4 then error $
"the syntax - model diagram" ++
else return (synM, pfM, modM)
getMorphL :: LogicalFramework lid sublogics basic_spec sentence symb_items
symb_map_items sign morphism symbol raw_symbol
=> lid -> String -> String -> morphism
getMorphL ml logicName fileName =
let file = logicName ++ "/" ++ fileName ++ ".hs"
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 }
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")
then error $ "The comorphism " ++ c ++ "already exists.\n"
let comorphismC = write_comorphism ml c s t synM pfM modM
writeFile ("Comorphisms" ++ "/" ++ c ++ ".hs") comorphismC
addComorphism2ComorphismList :: String -> IO ()
addComorphism2ComorphismList c = do
let file = dynComorphismsDir ++ "/" ++ dynComorphismsFile
contentsOld <- readFile file
let res = runParser (parserc c) (emptyAnnos ()) "" contentsOld -- !!
Right contentsNew -> writeFile file contentsNew
Left er -> error $ show er
{- ----------------------------------------------------------------------------
-- 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
let extSig = case lookupGlobalEnvDG n dg of
Just (SpecEntry es) -> es
_ -> error $ "The signature " ++ show n ++
ExtGenSig _ (NodeSig _ (G_sign l' (ExtSign sig _) _)) ->
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
let extView = case lookupGlobalEnvDG n dg of
Just (ViewOrStructEntry _ ev) -> ev
_ -> error $ "The morphism " ++ show n ++
ExtViewSig _ (GMorphism c _ _ morph _) _ -> do
then error $ "The morphism " ++ show n ++
" is not in the logic " ++ show l ++ "."
else coerceMorphism l' l "" morph
parser :: String -> AParser st String
let l_imp = "import " ++ l ++ "." ++ "Logic_" ++ l
let l_log = "Logic " ++ l
header <- skipUntil "module"
mod_decl <- do m <- asStr "module"
return $ unwords [m, n, w]
log_var_decl <- do v <- asStr dynLogicsCon
return $ unwords [v, s, t]
log_var_def <- do v <- asStr dynLogicsCon
do (xs, _) <- logParser `separatedBy` commaT
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
let com_imp = "import " ++ "Comorphisms." ++ c
let com_c = "Comorphism " ++ c
header <- skipUntil "module"
mod_decl <- do m <- asStr "module"
return $ unwords [m, n, w]
com_var_decl <- do v <- asStr dynComorphismsCon
return $ unwords [v, s, t]
com_var_def <- do v <- asStr dynComorphismsCon
do (xs, _) <- comParser `separatedBy` commaT
return $ header ++ mod_decl ++ "\n\n" ++
intercalate "\n" (imps ++ [com_imp]) ++ "\n\n" ++
com_var_def ++ " " ++ "[" ++
intercalate ", " (com_list ++ [com_c]) ++ "]"
skipUntil :: String -> AParser st String
res <- many $ reserved [lim] (many1 $ noneOf whiteChars) <|>
asStr :: String -> AParser st String
moduleName :: AParser st String
return $ tokStr m ++ "." ++ tokStr n
logParser :: AParser st String
return $ tokStr l ++ " " ++ tokStr n
comParser :: AParser st String
return $ tokStr c ++ " " ++ tokStr n