1 files changed, 214 insertions, 0 deletions
diff --git a/src/Library/TermNet.hs b/src/Library/TermNet.hs
new file mode 100644
index 0000000..16b5446
--- /dev/null
+++ b/src/Library/TermNet.hs
@@ -0,0 +1,214 @@
+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)
+