summaryrefslogtreecommitdiff
path: root/Library/TermNet.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Library/TermNet.hs')
-rw-r--r--Library/TermNet.hs214
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)
-