module Term.Narrowing.Variants.Compute (
computeVariantsBound
, computeVariants
, compareSubstVariant
) where
import Term.LTerm
import Term.Substitution
import Term.Unification
import Term.Narrowing.Variants.Check (leqSubstVariant, variantsFrom)
import Extension.Prelude
import Data.Ord
import Data.List
import Data.Maybe
import Control.Arrow
import Control.Applicative
import Control.Monad.Reader
import Debug.Trace.Ignore
compareSubstVariant :: LNTerm -> LNSubstVFresh -> LNSubstVFresh
-> WithMaude (Maybe Ordering)
compareSubstVariant t s1 s2
| s1 == s2 = return $ Just EQ
| otherwise = do
isSmaller <- leqSubstVariant t s1 s2
isGreater <- leqSubstVariant t s2 s1
return $ case (isSmaller, isGreater) of
(True, True) -> Just EQ
(True, False) -> Just LT
(False, True) -> Just GT
(False, False) -> Nothing
data Variant = Variant {
varPos :: [Int]
, varSubst :: LNSubstVFresh
}
deriving (Eq, Ord, Show)
instance Sized Variant where
size = size . varSubst
narrowVariant :: LNTerm
-> Maybe Int
-> WithMaude (Either ([Variant], [Variant]) (Int, [Variant]))
narrowVariant tstart maxdepth0 =
reader $ \hnd -> go maxdepth [ Variant [] emptySubstVFresh ] [] hnd
where
maxdepth = fromMaybe (1) maxdepth0
go :: Int -> [Variant] -> [Variant] -> MaudeHandle
-> Either ([Variant], [Variant]) (Int, [Variant])
go n [] explored _ = Right (maxdepthn, explored)
go 0 unexplored explored _ = Left (explored, unexplored)
go n unexplored explored hnd = (\res -> (trace (show (n,unexplored, explored, res)) res)) $
go (n1) new explored' hnd
where
runWithMaude = (`runReader` hnd)
explored0 = explored++unexplored
new0 = filter (\newVariant -> varSubst newVariant `notElem` map varSubst explored0)
$ concatMap variantsFrom' unexplored
variants = reverse $ sortOn narrowSeqStepComplexity $ (tag False new0 ++ tag True explored0)
minimized = filterMaximalBy fst cmp variants
tag t xs = [ (t,a) | a <- xs]
(explored',new) = map snd *** map snd $ partition fst minimized
cmp a b = runWithMaude $ compareSubstVariant tstart (varSubst.snd $ a) (varSubst.snd $ b)
variantsFrom' (Variant pos0 substComposed) =
zipWith (\i substComposed' -> Variant (pos0++[i]) substComposed')
[1..]
(runWithMaude $ variantsFrom tstart substComposed)
filterMaximalBy :: Eq a
=> (a -> Bool)
-> (a -> a -> Maybe Ordering)
-> [a]
-> [a]
filterMaximalBy _ _ [] = []
filterMaximalBy alreadyFiltered cmp xs0 =
go (last xs0) (init xs0,[])
where
go x ([],[]) = [x]
go x (y:todo,done)
| alreadyFiltered x && alreadyFiltered y = go x (todo,y:done)
| otherwise
= case cmp x y of
Nothing -> go x (todo,y:done)
Just EQ | alreadyFiltered x -> keepx
| otherwise -> keepy
Just GT -> keepx
Just LT -> keepy
where keepx = go x (todo,done)
keepy = go y (todo++done,[])
go x ([],y:done) = x:(go y (reverse done,[]))
narrowSeqStepComplexity :: (Bool,Variant) -> (Bool,Int,Int,Int)
narrowSeqStepComplexity (checked, var@(Variant _ subst)) =
(not checked, length (varPos var), size subst, length (varsRangeVFresh subst))
computeVariantsBound :: LNTerm -> Maybe Int
-> WithMaude (Maybe [LNSubstVFresh])
computeVariantsBound t d = reader $ \hnd -> (\res -> trace (show ("ComputeVariantsBound", t, res)) res) $
case (`runReader` hnd) $ narrowVariant t d of
Left _ -> Nothing
Right (_,explored) ->
Just (map varSubst (sortBy (comparing size) explored))
computeVariants :: LNTerm -> WithMaude [LNSubstVFresh]
computeVariants t =
fromMaybe err <$> computeVariantsBound t Nothing
where
err = error "impossible: Variant computation failed without giving a bound"