diff options
| -rw-r--r-- | Library/TermNet.hs | 135 | ||||
| -rw-r--r-- | MeaningSubst.hs | 66 |
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 |