1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- |

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeModule :$Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : utilities for Hets commands

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederCopyright : uni-bremen and Razvan Pascanu

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeLicence : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : r.pascanu@iu-bremen.de

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeStability : provisional

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkePortability : portable

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeToghether with PGIP.Common, PGIP.Utils contains all the auxiliary functions

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeused throughout the interactive interface. The reason for dividing these

501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroederfunctions in two files was that otherwise we would've get a circular

501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroederinclusion (for example Proof.Automatic requieres some of these auxiliary

501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroederfunctions, but some other functions -- that appear now in PGIP.Common --

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkerequire some functions from Proof.Automatic)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroeder

501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroeder-}

501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroeder

501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroedermodule PGIP.Utils where

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Data.Graph.Inductive.Graph

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Logic.Grothendieck

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Static.DevGraph

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport Syntax.AS_Library

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maedertype GDataEdge = LEdge DGLinkLab

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maedertype GDataNode = LNode DGNodeLab

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederdata GraphGoals =

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder GraphNode GDataNode

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder | GraphEdge GDataEdge

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder deriving (Eq,Show)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- | The datatype GOAL contains all the information read by the parser from the

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- user

1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata GOAL =

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Node String

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke | Edge String String

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder | LabeledEdge String Int String

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke deriving (Eq,Show)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- | The function 'getGoalList' creates a graph goal list ( a graph goal is

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder-- defined by the datatype 'GraphGoals') that is a part of the list passed

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- as an argument that corresponds to the parsed goals ( see

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- 'GOAL' datatype)

1a38107941725211e7c3f051f7a8f5e12199f03acmaedergetGoalList :: [GOAL] -> [GraphGoals] -> [GraphGoals] -> IO [GraphGoals]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetGoalList goalList allg ll

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke = case goalList of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Node x):l -> do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder tmp <- extractGraphNode x allg

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke tmp2<- getGoalList l allg ll

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder case tmp of

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Just smth -> return (smth:tmp2)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Nothing -> do

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder putStr ("Couldn't find node "++x++"\n")

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke return []

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (Edge x y):l -> do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke tmp <- extractGraphEdge x y allg ll

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke tmp2<- getGoalList l allg ll

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder case tmp of

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Just smth -> return (smth:tmp2)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Nothing -> return tmp2

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (LabeledEdge x nb y):l -> do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke tmp <- extractGraphLabeledEdge x nb y allg ll

656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder tmp2<- getGoalList l allg ll

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke case tmp of

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Just smth -> return (smth:tmp2)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Nothing -> return tmp2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] -> return []

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | The function 'extractGraphNode' extracts the goal node defined by

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- the ID of the node as a string from the provided list of goals

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeextractGraphNode:: String->[GraphGoals]->IO (Maybe GraphGoals)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeextractGraphNode x allGoals

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke = case allGoals of

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke [] ->do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke return Nothing

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (GraphNode (nb,label)):l -> do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke if (( getDGNodeName label)==x)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke then return (Just (GraphNode (nb,label)))

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder else extractGraphNode x l

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke _:l -> extractGraphNode x l

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- | The function 'extractGraphEdge' extracts the goal edge determined by

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- the two nodes from the provided list of goals

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederextractGraphEdge:: String -> String -> [GraphGoals] -> [GraphGoals]

a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder -> IO (Maybe GraphGoals)

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederextractGraphEdge x y allGoals ll

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder = case allGoals of

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder [] -> do

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder return Nothing

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (GraphEdge (xx,yy,label)):l -> do

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ttt1 <- extractGraphNode x ll

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke ttt2 <- extractGraphNode y ll

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke case ttt1 of

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Nothing -> do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke putStr ("Couldn't find node "++x++"\n"++

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke "when looking for edge "++x++" -> "++y++"\n")

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke return Nothing

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Just t1 -> do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke case ttt2 of

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Nothing -> do

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder putStr ("Couldn't find node "++y++"\n"++

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder "when looking for edge "++x++" -> "++y++"\n")

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder return Nothing

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Just t2 -> do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke case t1 of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (GraphNode (tmp1_nb, _)) ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case t2 of

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (GraphNode (tmp2_nb, _)) ->

a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder if (tmp1_nb == xx)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke then if (tmp2_nb == yy)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke then return (Just (GraphEdge (xx,yy,label)))

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke else extractGraphEdge x y l ll

else extractGraphEdge x y l ll

_ -> extractGraphEdge x y l ll

_ -> extractGraphEdge x y l ll

_:l -> extractGraphEdge x y l ll

-- | Same as above but it tries to extract the edge between the nodes

-- with the given number in the order they are found

extractGraphLabeledEdge:: String -> Int -> String ->

[GraphGoals] -> [GraphGoals] -> IO (Maybe GraphGoals)

extractGraphLabeledEdge x nb y allGoals ll

= case allGoals of

[] ->return Nothing

(GraphEdge (xx,yy,label)):l -> do

ttt1<- extractGraphNode x ll

ttt2<- extractGraphNode y ll

case ttt1 of

Nothing -> do

putStr ("Couldn't find node "++x++"\n"++

"when looking for edge "++x++" - "++(show nb)++" -> "++y++"\n")

return Nothing

Just t1 -> do

case ttt2 of

Nothing -> do

putStr ("Couldn't find node "++y++"\n"++

"when looking for edge "++x++" - "++(show nb)++" -> "++y++"\n")

return Nothing

Just t2 -> do

case t1 of

(GraphNode (tmp1_nb, _)) ->

case t2 of

(GraphNode (tmp2_nb, _)) ->

if (tmp1_nb == xx)

then if (tmp2_nb == yy)

then if (nb==0)

then return (Just (GraphEdge (xx,yy,label)))

else extractGraphLabeledEdge x (nb-1) y l ll

else extractGraphLabeledEdge x nb y l ll

else extractGraphLabeledEdge x nb y l ll

_ -> extractGraphLabeledEdge x nb y l ll

_ -> extractGraphLabeledEdge x nb y l ll

_:l -> extractGraphLabeledEdge x nb y l ll

-- | The function 'getEdgeGoals' given a list of edges selects all edges that

-- are goals of the graph and returns them as 'GraphGoals'

getEdgeGoals :: [GDataEdge] -> [GraphGoals]

getEdgeGoals ls =

case ls of

(x,y,l):ll -> let labelInfo = getDGLinkType l in

case labelInfo of

"unproventhm" -> (GraphEdge (x,y,l)):(getEdgeGoals ll)

"localunproventhm" -> (GraphEdge (x,y,l)):(getEdgeGoals ll)

"hetunproventhm" -> (GraphEdge (x,y,l)):(getEdgeGoals ll)

"hetlocalunproventhm" -> (GraphEdge (x,y,l)):(getEdgeGoals ll)

_ -> getEdgeGoals ll

[] -> []

-- | The function 'convToGoal' converts a list of 'GDataNode'

-- into 'GraphGoals' list

convToGoal:: [GDataNode] -> [GraphGoals]

convToGoal ls

= case ls of

x:l -> (GraphNode x) : (convToGoal l)

[] -> []

-- | The function 'convEdgeToGoal' converts a list of 'GDataEdge'

-- into 'GraphGoals' list

convEdgeToGoal :: [GDataEdge] -> [GraphGoals]

convEdgeToGoal ls

= case ls of

x:l -> (GraphEdge x): (convEdgeToGoal l)

[] -> []

-- | The function 'getEdgeList' returns from a list of graph goals just the

-- edge goals as ['GDataEdge']

getEdgeList :: [GraphGoals] -> [GDataEdge]

getEdgeList ls =

case ls of

(GraphEdge x):l -> x:(getEdgeList l)

(GraphNode _):l -> getEdgeList l

[] -> []

-- | The function 'getDGLinkType' returns a String describing the type of the edge

getDGLinkType :: DGLinkLab -> String

getDGLinkType lnk = case dgl_morphism lnk of

GMorphism _ _ _ _ _->

{- if not (is_injective (targetLogic cid) mor) then trace "noninjective morphism found" "hetdef"

else -}

case dgl_type lnk of

GlobalDef ->

if isHomogeneous $ dgl_morphism lnk then "globaldef"

else "hetdef"

HidingDef -> "hidingdef"

LocalThm thmLnkState _ _ -> het++"local" ++ getThmType thmLnkState ++ "thm"

GlobalThm thmLnkState _ _ -> het++getThmType thmLnkState ++ "thm"

HidingThm _ thmLnkState -> getThmType thmLnkState ++ "hidingthm"

FreeThm _ bool -> if bool then "proventhm" else "unproventhm"

_ -> "def" -- LocalDef, FreeDef, CofreeDef

where het = if isHomogeneous $ dgl_morphism lnk then "" else "het"

getThmType :: ThmLinkStatus -> String

getThmType thmLnkState =

case thmLnkState of

Proven _ _ -> "proven"

LeftOpen -> "unproven"

-- | The function 'createAllGoalsList' given a library (defined by LIB_NAME and

-- LibEnv) generates the list of all goals (both edges and nodes) of the graph

-- coresponding to the library

createAllGoalsList :: LIB_NAME->LibEnv -> [GraphGoals]

createAllGoalsList ln libEnv

= let dgraph = lookupDGraph ln libEnv

edgeGoals = getEdgeGoals (labEdges dgraph)

nodeGoals = getNodeGoals (labNodes dgraph)

in edgeGoals ++ nodeGoals

-- | The function 'getNodeGoals' given a list of nodes selects all nodes that

-- are goals of the graph and returns them as 'GraphGoals'

getNodeGoals::[GDataNode] -> [GraphGoals]

getNodeGoals ls =

case ls of

(nb,x):l ->

let labelInfo = getDGNodeType x in

case labelInfo of

"open_cons__spec" -> (GraphNode (nb,x)):(getNodeGoals l)

"proven_cons__spec" -> (GraphNode (nb,x)):(getNodeGoals l)

"locallyEmpty__open_cons__spec" -> (GraphNode (nb,x)):(getNodeGoals l)

"open_cons__internal" -> (GraphNode (nb,x)):(getNodeGoals l)

"proven_cons__internal" -> (GraphNode (nb,x)):(getNodeGoals l)

"dg_ref" -> (GraphNode (nb,x)):(getNodeGoals l)

_ -> getNodeGoals l

[] -> []

-- | gets the type of a development graph edge as a string

getDGNodeType :: DGNodeLab -> String

getDGNodeType dgnodelab =

(if hasOpenGoals dgnodelab then "locallyEmpty__" else "")

++ case isDGRef dgnodelab of

True -> "dg_ref"

False -> (if hasOpenConsStatus dgnodelab

then "open_cons__"

else "proven_cons__")

++ if isInternalNode dgnodelab

then "internal"

else "spec"

where

hasOpenConsStatus dgn = dgn_cons dgn /= None &&

case dgn_cons_status dgn of

LeftOpen -> True

_ -> False

-- | The function 'extractGoals' given the list of 'GDataEdge' and

-- the list of goals finds all elemnts of in the first list that are

-- also in the second

extractGoals :: [GDataEdge] -> [GraphGoals] -> [GDataEdge]

extractGoals ls ll

= case ls of

[] -> []

y:l -> ((extractGoal y ll)++(extractGoals l ll))

extractGoal :: GDataEdge -> [GraphGoals] -> [GDataEdge]

extractGoal x ls

= case ls of

[] -> []

(GraphEdge y):l -> if (y==x) then [x]

else extractGoal x l

_:l -> extractGoal x l