diff options
Diffstat (limited to 'MeaningSubst.hs')
| -rw-r--r-- | MeaningSubst.hs | 113 |
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) |