Code complete, but buggy

2 files changed, 160 insertions, 41 deletions

diff --git a/Library/TermNet.hs b/Library/TermNet.hs
index 4d0b107..11a6992 100644
--- a/Library/TermNet.hs
+++ b/Library/TermNet.hs
@@ -1,27 +1,146 @@
 module Library.TermNet(
-	TermNet,
-	empty,
-	addThm
-	) where
+    TermNet,
 
+    empty,
+    getLeafList,
+    getBranchList,
 
+    termToTermString,
+    thmToTermString,
 
+    addThm,
+    addThmFromNode
+    ) 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 = Empty | Leaf Object Node | Branch String [TermNet]
+data TermNet = Leaf [(Theorem, Node)] | Branch [(String, TermNet)] deriving (Eq, Show)
 
 
 
 empty :: TermNet
-empty = Empty
+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"] ++ (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, [(Theorem, Node)])
+addThm net theorem node =
+    let stringThm = thmToTermString theorem
+        add = (\net list ->
+                let branchList = fromJust . getBranchList $ net
+                in case list of
+                        [] ->
+                            (net, [])
+
+                        x:[] ->
+                            let (check, rest) = partition (\(y,z) -> y == x && isLeaf z) branchList
+                            in if (check == [])
+                                then (Branch ((x,(Leaf [(theorem,node)])):rest), [(theorem,node)])
+                                else let leaf = snd . head $ check
+                                         leafList = fromJust . getLeafList $ leaf
+                                     in --if ((theorem,node) `elem` leafList)
+                                        --then (Branch ((x,leaf):rest), leafList)
+                                        --else
+                                        (Branch ((x,(Leaf ((theorem,node):leafList))):rest), (theorem,node):leafList)
+
+                        x:xs ->
+                            let (check, rest) = partition (\(y,z) -> y == x && isBranch z) branchList
+                            in if (check == [])
+                                then let (net', resultList) = add empty xs
+                                     in (Branch ((x,net'):rest), resultList)
+                                else let nextStepDown = snd . head $ check
+                                         (net', resultList) = add nextStepDown xs
+                                     in (Branch ((head check):rest), resultList))
+
+    in add net stringThm
 
 
 
-addThm :: TermNet -> PGraph -> Node -> (TermNet, [(Theorem, Node)])
-addThm net graph node =
+addThmFromNode :: TermNet -> PGraph -> Node -> (TermNet, [(Theorem, Node)])
+addThmFromNode net graph node =
+    let theorem = genThm graph node
+    in addThm net theorem node
 
 
diff --git a/MeaningSubst.hs b/MeaningSubst.hs
index f1c97eb..ea8797d 100644
--- a/MeaningSubst.hs
+++ b/MeaningSubst.hs
@@ -20,41 +20,41 @@ createSubst one two =
     let alreadyMatched = (\x y m -> (Map.member x m || y `elem` Map.elems m) && Map.lookup x m /= Just y)
 
         f = (\x y tymap varmap ->
-            case (x,y) of
-                (TConst a1 ty1, TConst a2 ty2) ->
-                    if (alreadyMatch ty1 ty2 tymap || a1 /= a2)
-                    then Nothing
-                    else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
-                         in Just (tymap', varmap')
-
-                (TApp a1 b1, TApp a2 b2) ->
-                    do (tymap', varmap') <- f a1 a2 tymap varmap
-                       f b1 b2 tymap' varmap'
-
-                (TAbs (TVar (Var n1 ty1)) b1, TAbs (TVar (Var n2 ty2)) b2) ->
-                    if (alreadyMatched ty1 ty2 tymap || alreadyMatched n1 n2 varmap)
-                    then Nothing
-                    else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
-                             varmap' = if (n1 == n2) then varmap else Map.insert n1 n2 varmap
-                         in f b1 b2 tymap' varmap'
-
-                (TVar (Var n1 ty1), TVar (Var n2 ty2)) ->
-                    if (alreadyMatched ty1 ty2 tymap || alreadyMatched n1 n2 varmap)
-                    then Nothing
-                    else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
-                             varmap' = if (n1 == n2) then varmap else Map.insert n1 n2 varmap
-                         in Just (tymap', varmap')
-
-                (other, combination) -> Nothing)
+                case (x,y) of
+                    (TConst a1 ty1, TConst a2 ty2) ->
+                        if (alreadyMatch ty1 ty2 tymap || a1 /= a2)
+                        then Nothing
+                        else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
+                             in Just (tymap', varmap')
+
+                    (TApp a1 b1, TApp a2 b2) ->
+                        do (tymap', varmap') <- f a1 a2 tymap varmap
+                           f b1 b2 tymap' varmap'
+
+                    (TAbs (TVar (Var n1 ty1)) b1, TAbs (TVar (Var n2 ty2)) b2) ->
+                        if (alreadyMatched ty1 ty2 tymap || alreadyMatched n1 n2 varmap)
+                        then Nothing
+                        else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
+                                 varmap' = if (n1 == n2) then varmap else Map.insert n1 n2 varmap
+                             in f b1 b2 tymap' varmap'
+
+                    (TVar (Var n1 ty1), TVar (Var n2 ty2)) ->
+                        if (alreadyMatched ty1 ty2 tymap || alreadyMatched n1 n2 varmap)
+                        then Nothing
+                        else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
+                                 varmap' = if (n1 == n2) then varmap else Map.insert n1 n2 varmap
+                             in Just (tymap', varmap')
+
+                    (other, combination) -> Nothing)
 
         g = (\x y tymap varmap ->
-            let (hyp1,hyp2) = (Set.fromList . thmHyp $ x, Set.fromList . thmHyp $ y)
-                if (hyp1 == [])
-                then f (thmCon x) (thmCon y) tymap varmap
-                else do (tymap', varmap') <- f (head hyp1) (head hyp2) tymap varmap
-                        g (Theorem (Set.fromList . tail $ hyp1) (thmCon x))
-                          (Theorem (Set.fromList . tail $ hyp2) (thmCon y))
-                          tymap' varmap')
+                let (hyp1,hyp2) = (Set.fromList . thmHyp $ x, Set.fromList . thmHyp $ y)
+                    if (hyp1 == [])
+                    then f (thmCon x) (thmCon y) tymap varmap
+                    else do (tymap', varmap') <- f (head hyp1) (head hyp2) tymap varmap
+                            g (Theorem (Set.fromList . tail $ hyp1) (thmCon x))
+                              (Theorem (Set.fromList . tail $ hyp2) (thmCon y))
+                              tymap' varmap')
 
         maps = g one two Map.empty Map.empty