Reorganising source code

1 files changed, 0 insertions, 214 deletions

diff --git a/Library/TermNet.hs b/Library/TermNet.hs
deleted file mode 100644
index 16b5446..0000000
--- a/Library/TermNet.hs
+++ /dev/null
@@ -1,214 +0,0 @@
-module Library.TermNet(
-    TermNet,
-
-    empty,
-    getLeafList,
-    getBranchList,
-
-    genThm,
-    termToTermString,
-    thmToTermString,
-
-    addThm,
-    addThmFromNode,
-    matchThm
-    ) where
-
-
-
-import Data.Maybe
-import Data.List
-import qualified Data.Set as Set
-import Data.Graph.Inductive.Graph( Node )
-import qualified Data.Graph.Inductive.Graph as Graph
-import Library.ProofGraph
-import Library.WriteProof
-import Library.Object
-import Library.Theorem
-import Library.Term
-import Library.Parse
-import Library.Semantic
-import Library.Stack( Stack, at, (<:>) )
-import qualified Library.Stack as Stack
-
-
-
-data TermNet = Leaf [(Theorem, Node)] | Branch [(String, TermNet)]
-    deriving (Eq, Show)
-
-
-
-empty :: TermNet
-empty = Branch []
-
-
-
-isLeaf :: TermNet -> Bool
-isLeaf (Leaf _) = True
-isLeaf _ = False
-
-
-
-isBranch :: TermNet -> Bool
-isBranch (Branch _) = True
-isBranch _ = False
-
-
-
-getLeafList :: TermNet -> Maybe [(Theorem, Node)]
-getLeafList net =
-    case net of
-        Leaf list -> Just list
-        Branch list -> Nothing
-
-
-
-getBranchList :: TermNet -> Maybe [(String, TermNet)]
-getBranchList net =
-    case net of 
-        Leaf list -> Nothing
-        Branch list -> Just list
-
-
-
-genThm :: PGraph -> Node -> Theorem
-genThm graph node =
-    let gen g n num = 
-            let edge = filter (\x -> (fst . thd3 $ x) == num) (Graph.out g n)
-                node = (snd3 . head $ edge)
-                listing = write g node
-            in fromJust (((\(a,_,_,_) -> a) . fromJust $ (eval listing)) `at` 0)
-
-        hypList = map (fromJust . objTerm) (fromJust . objList $ (gen graph node 2))
-        con = fromJust . objTerm $ (gen graph node 1)
-
-    in Theorem (Set.fromList hypList) con
-
-
-
-termToTermString :: Term -> [String]
-termToTermString term =
-    case term of
-        (TConst _ _) ->
-            ["const"]
-
-        (TApp func arg) ->
-            ["app"] ++ (termToTermString func) ++ (termToTermString arg)
-
-        (TAbs var body) ->
-            ["abs", "var"] ++ (termToTermString body)
-
-        (TVar var) ->
-            ["var"]
-
-
-
-thmToTermString :: Theorem -> [String]
-thmToTermString theorem =
-    let hypList = Set.toList (thmHyp theorem)
-        f soFar hyp = soFar ++ ["hyp"] ++ (termToTermString hyp)
-    in (foldl' f [] hypList) ++ ["con"] ++ (termToTermString . thmCon $ theorem)
-
-
-
-addThm :: TermNet -> Theorem -> Node -> TermNet
-addThm net theorem node =
-    addThmImp net (theorem,node) (thmToTermString theorem)
-
-
-
-addThmFromNode :: TermNet -> PGraph -> Node -> TermNet
-addThmFromNode net graph node =
-    let theorem = genThm graph node
-    in addThmImp net (theorem,node) (thmToTermString theorem)
-
-
-
-addThmImp :: TermNet -> (Theorem,Node) -> [String] -> TermNet
-addThmImp (Branch branchList) item (x:[]) =
-    let (sameKey, rest) = partition (\(y,z) -> y == x && isLeaf z) branchList
-    in if (sameKey == [])
-       then let leaf' = Leaf [item]
-            in Branch ((x,leaf'):rest)
-       else let leaf = snd . head $ sameKey
-                leafList = fromJust . getLeafList $ leaf
-            in if (item `elem` leafList)
-               then Branch branchList
-               else let leaf' = Leaf (item:leafList)
-                    in Branch ((x,leaf'):rest)
-
-addThmImp (Branch branchList) item (x:xs) =
-    let (sameKey, rest) = partition (\(y,z) -> y == x) branchList
-    in if (sameKey == [])
-       then let net' = addThmImp empty item xs
-            in Branch ((x,net'):rest)
-       else let nextStepDown = snd . head $ sameKey
-                net' = addThmImp nextStepDown item xs
-            in Branch ((x,net'):rest)
-
-
-
-matchThm :: TermNet -> Theorem -> [(Theorem,Node)]
-matchThm net theorem =
-    let hyp = Set.toList (thmHyp theorem)
-        con = thmCon theorem
-        (curPrefix, curTerm) = if (hyp == [])
-                               then ("con", con)
-                               else ("hyp", head hyp)
-
-        r = do a <- matchImp curPrefix net
-               let b = matchTermImp curTerm a
-                   (branches, leaves) = partition (\x -> isBranch x) b
-
-               c <- if (hyp == [])
-                    then getLeafList (foldl' unify (Leaf []) leaves)
-                    else let theorem' = Theorem (Set.fromList (tail hyp)) con
-                         in return (matchThm (foldl' unify empty branches) theorem')
-               return c
-
-    in if (isNothing r) then [] else fromJust r
-
-
-
-matchImp :: String -> TermNet -> Maybe TermNet
-matchImp key net =
-    do list <- getBranchList net
-       let result = filter (\(x,y) -> x == key) list
-       r <- if (result == []) then Nothing else Just (snd . head $ result)
-       return r
-
-
-
-matchTermImp :: Term -> TermNet -> [TermNet]
-matchTermImp term net =
-    let list = getBranchList net
-        var = matchImp "var" net
-        result =
-            case term of
-                (TConst c ty) -> 
-                    do a <- matchImp "const" net
-                       return [a]
-
-                (TApp f x) ->
-                    do a <- matchImp "app" net
-                       let b = matchTermImp f a
-                       return (concat (map (matchTermImp x) b))
-
-                (TAbs v x) ->
-                    do a <- matchImp "abs" net
-                       b <- matchImp "var" a
-                       return (matchTermImp x b)
-
-                (TVar v) -> Nothing --don't need to do anything because variables are already taken care of
-
-        var' = if (isNothing var) then [] else [fromJust var]
-        result' = if (isNothing result) then [] else fromJust result
-
-    in var' ++ result'
-
-
-
-unify :: TermNet -> TermNet -> TermNet
-unify (Branch a) (Branch b) = Branch (a ++ b)
-unify (Leaf a) (Leaf b) = Leaf (a ++ b)
-