summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--MeaningSubst.hs141
-rw-r--r--TermNet.hs27
2 files changed, 168 insertions, 0 deletions
diff --git a/MeaningSubst.hs b/MeaningSubst.hs
new file mode 100644
index 0000000..f52e2e0
--- /dev/null
+++ b/MeaningSubst.hs
@@ -0,0 +1,141 @@
+import System.Environment( getArgs )
+import Text.Printf
+import Parse
+import ProofGraph
+import GraphPart
+import TermNet( TermNet )
+import qualified TermNet as TermNet
+import qualified Data.Graph.Inductive.Graph as Graph
+
+
+
+data Step = Step { from :: Node
+ , to :: Node
+ , sub :: Substitution }
+
+
+
+createSubst :: Theorem -> Theorem -> Maybe Substitution
+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)
+
+ 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')
+
+ maps = g one two Map.empty Map.empty
+
+ in if (Set.size . thmHyp $ one /= Set.size . thmHyp $ two || isNothing maps)
+ then Nothing
+ else do (t,v) <- maps
+ return (Map.toList t, Map.toList v)
+
+
+
+checkNode :: PGraph -> TermNet -> Node -> (TermNet, Maybe (GraphPart, GraphPart))
+checkNode graph termnet node =
+ let (termnet', list) = TermNet.addThm termnet graph node
+ (working, possibles) = partition (\x -> snd x == node) list
+
+ canBeSubbed = (\inn out ->
+ if (inn == [])
+ then out
+ else let sub = createSubst (fst working) (fst . head $ inn)
+ out' = if (isNothing sub)
+ then out
+ else (Step (snd working) (snd . head $ inn) (fromJust sub)) : out
+ in canBeSubbed (tail inn) out'
+
+ maxPositiveBenefit = (\list ->
+ let sortVal = (\x -> (size . snd x) - (addedSize (fst x) graph) - (overlap (fst x) (snd x)))
+ sorted = sortBy (\x y -> compare (sortVal x) (sortVal y)) list
+ check = head sorted
+ in if (sortVal check > 0) then check else Nothing)
+
+ step = maxPositiveBenefit . (map (stepGen graph)) $ (canBeSubbed possibles [])
+
+ in (termnet', step)
+
+
+
+stepGen :: PGraph -> Step -> (GraphPart, GraphPart)
+stepGen graph step =
+ let unused = graphPart (findUnused graph (Graph.suc graph (to step))) [] Nothing Nothing
+
+ base = doGraphGen (substitutionGen . sub $ step)
+ num = Graph.newNodes 1 base
+ node = (num, "subst")
+ cons = head (filter (\x -> Graph.indeg base x == 0) (Graph.nodes base))
+ edge = (num, cons, (2,1))
+
+ substGraph = (Graph.insEdge edge) . (Graph.insNode node) $ base
+ subst = makeGraphPart substGraph (Just (node,1)) (Just (node,1))
+
+ in (subst, unused)
+
+
+
+findUnused :: PGraph -> [Node] -> [Node]
+findUnused graph nodeList =
+ let nextLayer = concat . (map (Graph.suc graph)) $ nodeList
+ unused = filter (\x -> all (\y -> y `elem` nodeList) (Graph.pre graph x)) nextLayer
+ in nodeList ++ (findUnused graph usused)
+
+
+
+doMeaningSubst :: PGraph -> PGraph
+doMeaningSubst graph =
+ let f = (\g termnet nodeList ->
+ if (nodeList == [])
+ then g
+ else let working = head nodeList
+ (termnet', step) = checkNode g termnet working
+ (g', nodeList') = if (isNothing step)
+ then (g, nodeList)
+ else let (subst, unused) = fromJust step
+ in ((graphAdd subst () ()) . (graphDel unused) $ g, nodeList \\ (nodes unused))
+ in f g' termnet' nodeList')
+
+ in f graph TermNet.empty (Graph.nodes graph)
+
+
+
+main = do
+ args <- getArgs
+ list <- getLines (head args)
+ let graph = doGraphGen (map stripReturn list)
+ result = doMeaningSubst graph
+ printf $ (show result) ++ "\n"
diff --git a/TermNet.hs b/TermNet.hs
new file mode 100644
index 0000000..fd21008
--- /dev/null
+++ b/TermNet.hs
@@ -0,0 +1,27 @@
+module TermNet(
+ TermNet,
+ empty,
+ addThm
+ ) where
+
+
+
+import ProofGraph
+import Object
+import Theorem
+
+
+
+data TermNet = Empty | Leaf Object Node | Branch String [TermNet]
+
+
+
+empty :: TermNet
+empty = Empty
+
+
+
+addThm :: TermNet -> PGraph -> Node -> (TermNet, [(Theorem, Node)])
+addThm net graph node =
+
+