summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Library/TermNet.hs136
1 files changed, 100 insertions, 36 deletions
diff --git a/Library/TermNet.hs b/Library/TermNet.hs
index 11a6992..6d87aa9 100644
--- a/Library/TermNet.hs
+++ b/Library/TermNet.hs
@@ -5,11 +5,13 @@ module Library.TermNet(
getLeafList,
getBranchList,
+ genThm,
termToTermString,
thmToTermString,
addThm,
- addThmFromNode
+ addThmFromNode,
+ matchThm
) where
@@ -90,7 +92,7 @@ termToTermString term =
["app"] ++ (termToTermString func) ++ (termToTermString arg)
(TAbs var body) ->
- ["abs"] ++ (termToTermString body)
+ ["abs", "var"] ++ (termToTermString body)
(TVar var) ->
["var"]
@@ -105,42 +107,104 @@ thmToTermString theorem =
-addThm :: TermNet -> Theorem -> Node -> (TermNet, [(Theorem, Node)])
+addThm :: TermNet -> Theorem -> Node -> TermNet
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
-
-
-
-addThmFromNode :: TermNet -> PGraph -> Node -> (TermNet, [(Theorem, Node)])
+ addThmImp net (theorem,node) (thmToTermString theorem)
+
+
+
+addThmFromNode :: TermNet -> PGraph -> Node -> TermNet
addThmFromNode net graph node =
let theorem = genThm graph node
- in addThm net theorem 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)