Compiles properly

1 files changed, 69 insertions, 44 deletions

diff --git a/MeaningSubst.hs b/MeaningSubst.hs
index ea8797d..a0821b5 100644
--- a/MeaningSubst.hs
+++ b/MeaningSubst.hs
@@ -3,9 +3,19 @@ import Text.Printf
 import Library.Parse
 import Library.ProofGraph
 import Library.GraphPart
+import Library.Theorem
+import Library.Term
+import Library.TypeVar
+import Library.Generator
 import Library.TermNet( TermNet )
 import qualified Library.TermNet as TermNet
+import Data.Graph.Inductive.Graph( Node, LNode )
 import qualified Data.Graph.Inductive.Graph as Graph
+import Data.Map( Map )
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import Data.List
+import Data.Maybe
 
 
 
@@ -15,94 +25,106 @@ data Step = Step { from :: Node
 
 
 
+alreadyMatchedElem :: (Ord a, Eq b) => a -> b -> Map a b -> Bool
+alreadyMatchedElem x y xymap =
+    Map.member x xymap && Map.lookup x xymap /= Just y
+
+
+
 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 ->
+    let f = (\x y tymap varmap ->
                 case (x,y) of
+                    (TVar (Var n ty), term) ->
+                        if (alreadyMatchedElem (Var n ty) term varmap)
+                        then Nothing
+                        else let varmap' = if (Map.lookup (Var n ty) varmap == Nothing)
+                                           then Map.insert (Var n ty) term varmap
+                                           else varmap
+                             in Just (tymap, varmap')
+
                     (TConst a1 ty1, TConst a2 ty2) ->
-                        if (alreadyMatch ty1 ty2 tymap || a1 /= a2)
+                        if (alreadyMatchedElem (typeVar ty1) ty2 tymap || a1 /= a2 || (ty1 /= ty2 && not (isTypeVar ty1)))
                         then Nothing
-                        else let tymap' = if (ty1 == ty2) then tymap else Map.insert ty1 ty2 tymap
-                             in Just (tymap', varmap')
+                        else let tymap' = if (ty1 /= ty2)
+                                          then Map.insert (typeVar ty1) ty2 tymap
+                                          else 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')
+                    (TAbs a1 b1, TAbs a2 b2) ->
+                        do (tymap', varmap') <- f a1 a2 tymap varmap
+                           f b1 b2 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.toList . thmHyp $ x, Set.toList . thmHyp $ y)
+                in if (hyp1 == [] && hyp2 == [])
+                   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)
+    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 :: PGraph -> TermNet -> Node -> (TermNet, Maybe (GraphPart, GraphPart), Maybe (Node,Node))
 checkNode graph termnet node =
-    let (termnet', list) = TermNet.addThm termnet graph node
-        (working, possibles) = partition (\x -> snd x == node) list
+    let theorem = TermNet.genThm graph node
+        possibles = TermNet.matchThm termnet theorem 
 
         canBeSubbed = (\inn out ->
             if (inn == [])
             then out
-            else let sub = createSubst (fst working) (fst . head $ inn)
+            else let sub = createSubst theorem (fst . head $ inn)
                      out' = if (isNothing sub)
                             then out
-                            else (Step (snd working) (snd . head $ inn) (fromJust sub)) : out
-                 in canBeSubbed (tail inn) out'
+                            else (Step node (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)))
+            let sortVal = (\x -> let added = fst . snd $ x
+                                     removed = snd . snd $ x
+                                     inn = from . fst $ x
+                                     out = to . fst $ x
+                                     outNodes = map (\(x,(y,z)) -> (x,y)) (Graph.lpre graph out)
+                                 in (size removed) - (addedSize added (Just (inn,1)) outNodes graph) - (overlap added removed))
                 sorted = sortBy (\x y -> compare (sortVal x) (sortVal y)) list
                 check = head sorted
-            in if (sortVal check > 0) then check else Nothing)
+            in if (sortVal check > 0) then (Just (snd check), Just (from . fst $ check, to . fst $ check)) else (Nothing, Nothing))
 
-        step = maxPositiveBenefit . (map (stepGen graph)) $ (canBeSubbed possibles [])
+        (step, between) = maxPositiveBenefit . (map (\x -> (x, stepGen graph x))) $ (canBeSubbed possibles [])
+        termnet' = TermNet.addThm termnet theorem node
 
-    in (termnet', step)
+    in (termnet', step, between)
 
 
 
 stepGen :: PGraph -> Step -> (GraphPart, GraphPart)
 stepGen graph step =
-    let unused = graphPart (findUnused graph (Graph.suc graph (to step))) [] Nothing Nothing
+    let unusedNodes = findUnused graph (Graph.suc graph (to step))
+        unusedLabNodes = filter (\(x,y) -> x `elem` unusedNodes) (Graph.labNodes graph)
+        unused = graphPart unusedLabNodes [] Nothing Nothing
 
         base = doGraphGen (substitutionGen . sub $ step)
-        num = Graph.newNodes 1 base
+        num = head (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))
+        subst = makeGraphPart substGraph (Just (num,1)) (Just (num,1))
 
     in (subst, unused)
 
@@ -112,7 +134,7 @@ 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)
+    in nodeList ++ (findUnused graph unused)
 
 
 
@@ -122,11 +144,14 @@ doMeaningSubst graph =
                 if (nodeList == [])
                 then g
                 else let working = head nodeList
-                         (termnet', step) = checkNode g termnet working
-                         (g', nodeList') = if (isNothing step)
+                         (termnet', step, between) = checkNode g termnet working
+                         (g', nodeList') = if (isNothing step || isNothing between)
                                            then (g, nodeList)
                                            else let (subst, unused) = fromJust step
-                                                in ((graphAdd subst () ()) . (graphDel unused) $ g, nodeList \\ (nodes unused))
+                                                    (from, to) = fromJust between
+                                                    toNodes = map (\(x,(y,z)) -> (x,y)) (Graph.lpre g to)
+                                                in ((graphAdd subst (Just (from, 1)) toNodes) . (graphDel unused) $ g,
+                                                    nodeList \\ (map (\(x,y) -> x) (nodes unused)))
                      in f g' termnet' nodeList')
 
     in f graph TermNet.empty (Graph.nodes graph)