diff options
| -rw-r--r-- | Library/TermNet.hs | 136 |
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) |