summaryrefslogtreecommitdiff
path: root/MeaningSubst.hs
diff options
context:
space:
mode:
Diffstat (limited to 'MeaningSubst.hs')
-rw-r--r--MeaningSubst.hs113
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)