Not quite finished work on instantiation optimisation

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 =
+
+