module Hint.Match(readMatch) where
import Control.Applicative
import Data.List.Extra
import Data.Maybe
import Data.Data
import Unsafe.Coerce
import Settings
import Hint.Type
import Control.Monad
import Data.Tuple.Extra
import Util
import qualified Data.Set as Set
import Prelude
fmapAn = fmap (const an)
readMatch :: [HintRule] -> DeclHint
readMatch settings = findIdeas (concatMap readRule settings)
readRule :: HintRule -> [HintRule]
readRule (m@HintRule{hintRuleLHS=(fmapAn -> hintRuleLHS), hintRuleRHS=(fmapAn -> hintRuleRHS), hintRuleSide=(fmap fmapAn -> hintRuleSide)}) =
(:) m{hintRuleLHS=hintRuleLHS,hintRuleSide=hintRuleSide,hintRuleRHS=hintRuleRHS} $ fromMaybe [] $ do
(l,v1) <- dotVersion hintRuleLHS
(r,v2) <- dotVersion hintRuleRHS
guard $ v1 == v2 && l /= [] && (length l > 1 || length r > 1) && Set.notMember v1 (freeVars $ maybeToList hintRuleSide ++ l ++ r)
if r /= [] then return
[m{hintRuleLHS=dotApps l, hintRuleRHS=dotApps r, hintRuleSide=hintRuleSide}
,m{hintRuleLHS=dotApps (l++[toNamed v1]), hintRuleRHS=dotApps (r++[toNamed v1]), hintRuleSide=hintRuleSide}]
else if length l > 1 then return
[m{hintRuleLHS=dotApps l, hintRuleRHS=toNamed "id", hintRuleSide=hintRuleSide}
,m{hintRuleLHS=dotApps (l++[toNamed v1]), hintRuleRHS=toNamed v1, hintRuleSide=hintRuleSide}]
else
Nothing
dotVersion :: Exp_ -> Maybe ([Exp_], String)
dotVersion (view -> Var_ v) | isUnifyVar v = Just ([], v)
dotVersion (fromApps -> xs) | length xs > 1 = first (apps (init xs) :) <$> dotVersion (fromParen $ last xs)
dotVersion _ = Nothing
findIdeas :: [HintRule] -> Scope -> Module S -> Decl_ -> [Idea]
findIdeas matches s _ decl =
[ (idea (hintRuleSeverity m) (hintRuleName m) x y){ideaNote=notes}
| decl <- case decl of InstDecl{} -> children decl; _ -> [decl]
, (parent,x) <- universeParentExp decl, not $ isParen x, let x2 = fmapAn x
, m <- matches, Just (y,notes) <- [matchIdea s decl m parent x2]]
matchIdea :: Scope -> Decl_ -> HintRule -> Maybe (Int, Exp_) -> Exp_ -> Maybe (Exp_,[Note])
matchIdea s decl HintRule{..} parent x = do
let nm a b = scopeMatch (hintRuleScope,a) (s,b)
u <- unifyExp nm True hintRuleLHS x
u <- check u
let e = subst u hintRuleRHS
let res = addBracket parent $ unqualify hintRuleScope s u $ performEval e
guard $ (freeVars e Set.\\ Set.filter (not . isUnifyVar) (freeVars hintRuleRHS))
`Set.isSubsetOf` freeVars x
guard $ checkSide hintRuleSide $ ("original",x) : ("result",res) : u
guard $ checkDefine decl parent res
return (res,hintRuleNotes)
type NameMatch = QName S -> QName S -> Bool
nmOp :: NameMatch -> QOp S -> QOp S -> Bool
nmOp nm (QVarOp _ x) (QVarOp _ y) = nm x y
nmOp nm (QConOp _ x) (QConOp _ y) = nm x y
nmOp nm _ _ = False
unify :: Data a => NameMatch -> Bool -> a -> a -> Maybe [(String,Exp_)]
unify nm root x y | Just x <- cast x = unifyExp nm root x (unsafeCoerce y)
| Just x <- cast x = unifyPat nm x (unsafeCoerce y)
| otherwise = unifyDef nm x y
unifyDef :: Data a => NameMatch -> a -> a -> Maybe [(String,Exp_)]
unifyDef nm x y = fmap concat . sequence =<< gzip (unify nm False) x y
unifyExp :: NameMatch -> Bool -> Exp_ -> Exp_ -> Maybe [(String,Exp_)]
unifyExp nm root x y | isParen x || isParen y = unifyExp nm root (fromParen x) (fromParen y)
unifyExp nm root (Var _ (fromNamed -> v)) y | isUnifyVar v = Just [(v,y)]
unifyExp nm root (Var _ x) (Var _ y) | nm x y = Just []
unifyExp nm root x@(App _ x1 x2) (App _ y1 y2) =
liftM2 (++) (unifyExp nm False x1 y1) (unifyExp nm False x2 y2) `mplus`
(do guard $ not root; InfixApp _ y11 dot y12 <- return $ fromParen y1; guard $ isDot dot; unifyExp nm root x (App an y11 (App an y12 y2)))
unifyExp nm root x (InfixApp _ lhs2 op2 rhs2)
| InfixApp _ lhs1 op1 rhs1 <- x = guard (nmOp nm op1 op2) >> liftM2 (++) (unifyExp nm False lhs1 lhs2) (unifyExp nm False rhs1 rhs2)
| isDol op2 = unifyExp nm root x $ App an lhs2 rhs2
| otherwise = unifyExp nm root x $ App an (App an (opExp op2) lhs2) rhs2
unifyExp nm root x y | isOther x, isOther y = unifyDef nm x y
unifyExp nm root _ _ = Nothing
unifyPat :: NameMatch -> Pat_ -> Pat_ -> Maybe [(String,Exp_)]
unifyPat nm (PVar _ x) (PVar _ y) = Just [(fromNamed x, toNamed $ fromNamed y)]
unifyPat nm (PVar _ x) PWildCard{} = Just [(fromNamed x, toNamed $ "_" ++ fromNamed x)]
unifyPat nm x y = unifyDef nm x y
isOther Var{} = False
isOther App{} = False
isOther InfixApp{} = False
isOther _ = True
check :: [(String,Exp_)] -> Maybe [(String,Exp_)]
check = mapM f . groupSort
where f (x,ys) = if allSame ys then Just (x,head ys) else Nothing
subst :: [(String,Exp_)] -> Exp_ -> Exp_
subst bind = transform g . transformBracket f
where
f (Var _ (fromNamed -> x)) | isUnifyVar x = lookup x bind
f _ = Nothing
g (App _ np x) | np ~= "_noParen_" = fromParen x
g x = x
checkSide :: Maybe Exp_ -> [(String,Exp_)] -> Bool
checkSide x bind = maybe True f x
where
f (InfixApp _ x op y)
| opExp op ~= "&&" = f x && f y
| opExp op ~= "||" = f x || f y
f (App _ x y) | x ~= "not" = not $ f y
f (Paren _ x) = f x
f (App _ cond (sub -> y))
| 'i':'s':typ <- fromNamed cond
= isType typ y
f (App _ (App _ cond (sub -> x)) (sub -> y))
| cond ~= "notIn" = and [x `notElem` universe y | x <- list x, y <- list y]
| cond ~= "notEq" = x /= y
f x | x ~= "noTypeCheck" = True
f x | x ~= "noQuickCheck" = True
f x = error $ "Hint.Match.checkSide, unknown side condition: " ++ prettyPrint x
isType "Compare" x = True
isType "Atom" x = isAtom x
isType "WHNF" x = isWHNF x
isType "Wildcard" x = any isFieldWildcard $ universeS x
isType "Nat" (asInt -> Just x) | x >= 0 = True
isType "Pos" (asInt -> Just x) | x > 0 = True
isType "Neg" (asInt -> Just x) | x < 0 = True
isType "NegZero" (asInt -> Just x) | x <= 0 = True
isType ('L':'i':'t':typ@(_:_)) (Lit _ x) = head (words $ show x) == typ
isType typ x = head (words $ show x) == typ
asInt :: Exp_ -> Maybe Integer
asInt (Paren _ x) = asInt x
asInt (NegApp _ x) = negate <$> asInt x
asInt (Lit _ (Int _ x _)) = Just x
asInt _ = Nothing
list :: Exp_ -> [Exp_]
list (List _ xs) = xs
list x = [x]
sub :: Exp_ -> Exp_
sub = transform f
where f (view -> Var_ x) | Just y <- lookup x bind = y
f x = x
checkDefine :: Decl_ -> Maybe (Int, Exp_) -> Exp_ -> Bool
checkDefine x Nothing y = fromNamed x /= fromNamed (transformBi unqual $ head $ fromApps y)
checkDefine _ _ _ = True
performEval :: Exp_ -> Exp_
performEval (App _ e x) | e ~= "_eval_" = evaluate x
performEval x = x
unqualify :: Scope -> Scope -> [(String,Exp_)] -> Exp_ -> Exp_
unqualify from to subs = transformBi f
where
f (Qual _ (ModuleName _ [m]) x) | Just y <- fromNamed <$> lookup [m] subs
= if null y then UnQual an x else Qual an (ModuleName an y) x
f x = scopeMove (from,x) to
addBracket :: Maybe (Int,Exp_) -> Exp_ -> Exp_
addBracket (Just (i,p)) c | needBracket i p c = Paren an c
addBracket _ x = x