summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Library/TermNet.hs135
-rw-r--r--MeaningSubst.hs66
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