From bd9772daf2fe36de53fdc358ba3bb52bc416d562 Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Fri, 14 Sep 2012 10:15:04 +1000 Subject: Code complete, but buggy --- Library/TermNet.hs | 135 +++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 127 insertions(+), 8 deletions(-) (limited to 'Library/TermNet.hs') 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 -- cgit