{-# LANGUAGE PatternGuards, ViewPatterns, RecordWildCards, FlexibleContexts, ScopedTypeVariables #-}

{-
The matching does a fairly simple unification between the two terms, treating
any single letter variable on the left as a free variable. After the matching
we substitute, transform and check the side conditions. We also "see through"
both ($) and (.) functions on the right.

TRANSFORM PATTERNS
_eval_ - perform deep evaluation, must be used at the top of a RHS
_noParen_ - don't bracket this particular item

SIDE CONDITIONS
(&&), (||), not - boolean connectives
isAtom x - does x never need brackets
isFoo x - is the root constructor of x a "Foo"
notEq x y - are x and y not equal
notIn xs ys - are all x variables not in ys expressions
noTypeCheck, noQuickCheck - no semantics, a hint for testing only

($) AND (.)
We see through ($)/(.) by expanding it if nothing else matches.
We also see through (.) by translating rules that have (.) equivalents
to separate rules. For example:

concat (map f x) ==> concatMap f x
-- we spot both these rules can eta reduce with respect to x
concat . map f ==> concatMap f
-- we use the associativity of (.) to add
concat . map f . x ==> concatMap f . x
-- currently 36 of 169 rules have (.) equivalents

We see through (.) if the RHS is dull using id, e.g.

not (not x) ==> x
not . not ==> id
not . not . x ==> x
-}

module Hint.Match(readMatch) where

import Control.Applicative
import Data.List.Extra
import Data.Maybe
import Config.Type
import Hint.Type
import Control.Monad
import Data.Tuple.Extra
import HSE.Unify
import Util
import Timing
import qualified Data.Set as Set
import Prelude
import qualified Refact.Types as R


fmapAn :: Exp b -> Exp SrcSpanInfo
fmapAn = (b -> SrcSpanInfo) -> Exp b -> Exp SrcSpanInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SrcSpanInfo -> b -> SrcSpanInfo
forall a b. a -> b -> a
const SrcSpanInfo
an)


---------------------------------------------------------------------
-- READ THE RULE

readMatch :: [HintRule] -> DeclHint
readMatch :: [HintRule] -> DeclHint
readMatch settings :: [HintRule]
settings = [HintRule] -> DeclHint
findIdeas ((HintRule -> [HintRule]) -> [HintRule] -> [HintRule]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap HintRule -> [HintRule]
readRule [HintRule]
settings)


readRule :: HintRule -> [HintRule]
readRule :: HintRule -> [HintRule]
readRule m :: HintRule
m@HintRule{hintRuleLHS :: HintRule -> Exp SrcSpanInfo
hintRuleLHS=(Exp SrcSpanInfo -> Exp SrcSpanInfo
forall b. Exp b -> Exp SrcSpanInfo
fmapAn -> Exp SrcSpanInfo
hintRuleLHS), hintRuleRHS :: HintRule -> Exp SrcSpanInfo
hintRuleRHS=(Exp SrcSpanInfo -> Exp SrcSpanInfo
forall b. Exp b -> Exp SrcSpanInfo
fmapAn -> Exp SrcSpanInfo
hintRuleRHS), hintRuleSide :: HintRule -> Maybe (Exp SrcSpanInfo)
hintRuleSide=((Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Maybe (Exp SrcSpanInfo) -> Maybe (Exp SrcSpanInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Exp SrcSpanInfo -> Exp SrcSpanInfo
forall b. Exp b -> Exp SrcSpanInfo
fmapAn -> Maybe (Exp SrcSpanInfo)
hintRuleSide)} =
    (:) HintRule
m{hintRuleLHS :: Exp SrcSpanInfo
hintRuleLHS=Exp SrcSpanInfo
hintRuleLHS,hintRuleSide :: Maybe (Exp SrcSpanInfo)
hintRuleSide=Maybe (Exp SrcSpanInfo)
hintRuleSide,hintRuleRHS :: Exp SrcSpanInfo
hintRuleRHS=Exp SrcSpanInfo
hintRuleRHS} ([HintRule] -> [HintRule]) -> [HintRule] -> [HintRule]
forall a b. (a -> b) -> a -> b
$ do
        (l :: [Exp SrcSpanInfo]
l,v1 :: String
v1) <- Exp SrcSpanInfo -> [([Exp SrcSpanInfo], String)]
dotVersion Exp SrcSpanInfo
hintRuleLHS
        (r :: [Exp SrcSpanInfo]
r,v2 :: String
v2) <- Exp SrcSpanInfo -> [([Exp SrcSpanInfo], String)]
dotVersion Exp SrcSpanInfo
hintRuleRHS
        Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ String
v1 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
v2 Bool -> Bool -> Bool
&& [Exp SrcSpanInfo]
l [Exp SrcSpanInfo] -> [Exp SrcSpanInfo] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] Bool -> Bool -> Bool
&& ([Exp SrcSpanInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp SrcSpanInfo]
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 Bool -> Bool -> Bool
|| [Exp SrcSpanInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp SrcSpanInfo]
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1) Bool -> Bool -> Bool
&& String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember String
v1 ([Exp SrcSpanInfo] -> Set String
forall a. FreeVars a => a -> Set String
freeVars ([Exp SrcSpanInfo] -> Set String)
-> [Exp SrcSpanInfo] -> Set String
forall a b. (a -> b) -> a -> b
$ Maybe (Exp SrcSpanInfo) -> [Exp SrcSpanInfo]
forall a. Maybe a -> [a]
maybeToList Maybe (Exp SrcSpanInfo)
hintRuleSide [Exp SrcSpanInfo] -> [Exp SrcSpanInfo] -> [Exp SrcSpanInfo]
forall a. [a] -> [a] -> [a]
++ [Exp SrcSpanInfo]
l [Exp SrcSpanInfo] -> [Exp SrcSpanInfo] -> [Exp SrcSpanInfo]
forall a. [a] -> [a] -> [a]
++ [Exp SrcSpanInfo]
r)
        if [Exp SrcSpanInfo]
r [Exp SrcSpanInfo] -> [Exp SrcSpanInfo] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] then
            [HintRule
m{hintRuleLHS :: Exp SrcSpanInfo
hintRuleLHS=[Exp SrcSpanInfo] -> Exp SrcSpanInfo
dotApps [Exp SrcSpanInfo]
l, hintRuleRHS :: Exp SrcSpanInfo
hintRuleRHS=[Exp SrcSpanInfo] -> Exp SrcSpanInfo
dotApps [Exp SrcSpanInfo]
r, hintRuleSide :: Maybe (Exp SrcSpanInfo)
hintRuleSide=Maybe (Exp SrcSpanInfo)
hintRuleSide}
            ,HintRule
m{hintRuleLHS :: Exp SrcSpanInfo
hintRuleLHS=[Exp SrcSpanInfo] -> Exp SrcSpanInfo
dotApps ([Exp SrcSpanInfo]
l[Exp SrcSpanInfo] -> [Exp SrcSpanInfo] -> [Exp SrcSpanInfo]
forall a. [a] -> [a] -> [a]
++[String -> Exp SrcSpanInfo
forall a. Named a => String -> a
toNamed String
v1]), hintRuleRHS :: Exp SrcSpanInfo
hintRuleRHS=[Exp SrcSpanInfo] -> Exp SrcSpanInfo
dotApps ([Exp SrcSpanInfo]
r[Exp SrcSpanInfo] -> [Exp SrcSpanInfo] -> [Exp SrcSpanInfo]
forall a. [a] -> [a] -> [a]
++[String -> Exp SrcSpanInfo
forall a. Named a => String -> a
toNamed String
v1]), hintRuleSide :: Maybe (Exp SrcSpanInfo)
hintRuleSide=Maybe (Exp SrcSpanInfo)
hintRuleSide}]
         else if [Exp SrcSpanInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Exp SrcSpanInfo]
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then
            [HintRule
m{hintRuleLHS :: Exp SrcSpanInfo
hintRuleLHS=[Exp SrcSpanInfo] -> Exp SrcSpanInfo
dotApps [Exp SrcSpanInfo]
l, hintRuleRHS :: Exp SrcSpanInfo
hintRuleRHS=String -> Exp SrcSpanInfo
forall a. Named a => String -> a
toNamed "id", hintRuleSide :: Maybe (Exp SrcSpanInfo)
hintRuleSide=Maybe (Exp SrcSpanInfo)
hintRuleSide}
            ,HintRule
m{hintRuleLHS :: Exp SrcSpanInfo
hintRuleLHS=[Exp SrcSpanInfo] -> Exp SrcSpanInfo
dotApps ([Exp SrcSpanInfo]
l[Exp SrcSpanInfo] -> [Exp SrcSpanInfo] -> [Exp SrcSpanInfo]
forall a. [a] -> [a] -> [a]
++[String -> Exp SrcSpanInfo
forall a. Named a => String -> a
toNamed String
v1]), hintRuleRHS :: Exp SrcSpanInfo
hintRuleRHS=String -> Exp SrcSpanInfo
forall a. Named a => String -> a
toNamed String
v1, hintRuleSide :: Maybe (Exp SrcSpanInfo)
hintRuleSide=Maybe (Exp SrcSpanInfo)
hintRuleSide}]
         else []


-- find a dot version of this rule, return the sequence of app prefixes, and the var
dotVersion :: Exp_ -> [([Exp_], String)]
dotVersion :: Exp SrcSpanInfo -> [([Exp SrcSpanInfo], String)]
dotVersion (Exp SrcSpanInfo -> Var_
forall a b. View a b => a -> b
view -> Var_ v :: String
v) | String -> Bool
isUnifyVar String
v = [([], String
v)]
dotVersion (App l :: SrcSpanInfo
l ls :: Exp SrcSpanInfo
ls rs :: Exp SrcSpanInfo
rs) = ([Exp SrcSpanInfo] -> [Exp SrcSpanInfo])
-> ([Exp SrcSpanInfo], String) -> ([Exp SrcSpanInfo], String)
forall a a' b. (a -> a') -> (a, b) -> (a', b)
first (Exp SrcSpanInfo
ls Exp SrcSpanInfo -> [Exp SrcSpanInfo] -> [Exp SrcSpanInfo]
forall a. a -> [a] -> [a]
:) (([Exp SrcSpanInfo], String) -> ([Exp SrcSpanInfo], String))
-> [([Exp SrcSpanInfo], String)] -> [([Exp SrcSpanInfo], String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp SrcSpanInfo -> [([Exp SrcSpanInfo], String)]
dotVersion (Exp SrcSpanInfo -> Exp SrcSpanInfo
fromParen Exp SrcSpanInfo
rs)
dotVersion (InfixApp l :: SrcSpanInfo
l x :: Exp SrcSpanInfo
x op :: QOp SrcSpanInfo
op y :: Exp SrcSpanInfo
y) = (([Exp SrcSpanInfo] -> [Exp SrcSpanInfo])
-> ([Exp SrcSpanInfo], String) -> ([Exp SrcSpanInfo], String)
forall a a' b. (a -> a') -> (a, b) -> (a', b)
first (SrcSpanInfo
-> Exp SrcSpanInfo -> QOp SrcSpanInfo -> Exp SrcSpanInfo
forall l. l -> Exp l -> QOp l -> Exp l
LeftSection SrcSpanInfo
l Exp SrcSpanInfo
x QOp SrcSpanInfo
op Exp SrcSpanInfo -> [Exp SrcSpanInfo] -> [Exp SrcSpanInfo]
forall a. a -> [a] -> [a]
:) (([Exp SrcSpanInfo], String) -> ([Exp SrcSpanInfo], String))
-> [([Exp SrcSpanInfo], String)] -> [([Exp SrcSpanInfo], String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp SrcSpanInfo -> [([Exp SrcSpanInfo], String)]
dotVersion Exp SrcSpanInfo
y) [([Exp SrcSpanInfo], String)]
-> [([Exp SrcSpanInfo], String)] -> [([Exp SrcSpanInfo], String)]
forall a. [a] -> [a] -> [a]
++
                                 (([Exp SrcSpanInfo] -> [Exp SrcSpanInfo])
-> ([Exp SrcSpanInfo], String) -> ([Exp SrcSpanInfo], String)
forall a a' b. (a -> a') -> (a, b) -> (a', b)
first (SrcSpanInfo
-> QOp SrcSpanInfo -> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall l. l -> QOp l -> Exp l -> Exp l
RightSection SrcSpanInfo
l QOp SrcSpanInfo
op Exp SrcSpanInfo
yExp SrcSpanInfo -> [Exp SrcSpanInfo] -> [Exp SrcSpanInfo]
forall a. a -> [a] -> [a]
:) (([Exp SrcSpanInfo], String) -> ([Exp SrcSpanInfo], String))
-> [([Exp SrcSpanInfo], String)] -> [([Exp SrcSpanInfo], String)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp SrcSpanInfo -> [([Exp SrcSpanInfo], String)]
dotVersion Exp SrcSpanInfo
x)
dotVersion _ = []


---------------------------------------------------------------------
-- PERFORM THE MATCHING

findIdeas :: [HintRule] -> Scope -> Module S -> Decl_ -> [Idea]
findIdeas :: [HintRule] -> DeclHint
findIdeas matches :: [HintRule]
matches s :: Scope
s _ decl :: Decl_
decl = String -> String -> [Idea] -> [Idea]
forall a. String -> String -> a -> a
timed "Hint" "Match apply" ([Idea] -> [Idea]) -> [Idea] -> [Idea]
forall a b. (a -> b) -> a -> b
$ [Idea] -> [Idea]
forall a. [a] -> [a]
forceList
    [ (Severity
-> String
-> Exp SrcSpanInfo
-> Exp SrcSpanInfo
-> [Refactoring SrcSpan]
-> Idea
forall (ast :: * -> *) a.
(Annotated ast, Pretty a, Pretty (ast SrcSpanInfo)) =>
Severity
-> String -> ast SrcSpanInfo -> a -> [Refactoring SrcSpan] -> Idea
idea (HintRule -> Severity
hintRuleSeverity HintRule
m) (HintRule -> String
hintRuleName HintRule
m) Exp SrcSpanInfo
x Exp SrcSpanInfo
y [Refactoring SrcSpan
r]){ideaNote :: [Note]
ideaNote=[Note]
notes}
    | Decl_
decl <- case Decl_
decl of InstDecl{} -> Decl_ -> [Decl_]
forall on. Uniplate on => on -> [on]
children Decl_
decl; _ -> [Decl_
decl]
    , (parent :: Maybe (Int, Exp SrcSpanInfo)
parent,x :: Exp SrcSpanInfo
x) <- Decl_ -> [(Maybe (Int, Exp SrcSpanInfo), Exp SrcSpanInfo)]
forall a.
Data a =>
a -> [(Maybe (Int, Exp SrcSpanInfo), Exp SrcSpanInfo)]
universeParentExp Decl_
decl, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> Bool
forall l. Exp l -> Bool
isParen Exp SrcSpanInfo
x
    , HintRule
m <- [HintRule]
matches, Just (y :: Exp SrcSpanInfo
y,notes :: [Note]
notes, subst :: [(String, SrcSpan)]
subst) <- [Scope
-> Decl_
-> HintRule
-> Maybe (Int, Exp SrcSpanInfo)
-> Exp SrcSpanInfo
-> Maybe (Exp SrcSpanInfo, [Note], [(String, SrcSpan)])
matchIdea Scope
s Decl_
decl HintRule
m Maybe (Int, Exp SrcSpanInfo)
parent Exp SrcSpanInfo
x]
    , let r :: Refactoring SrcSpan
r = RType
-> SrcSpan -> [(String, SrcSpan)] -> String -> Refactoring SrcSpan
forall a. RType -> a -> [(String, a)] -> String -> Refactoring a
R.Replace RType
R.Expr (Exp SrcSpanInfo -> SrcSpan
forall (a :: * -> *). Annotated a => a SrcSpanInfo -> SrcSpan
toSS Exp SrcSpanInfo
x) [(String, SrcSpan)]
subst (Exp SrcSpanInfo -> String
forall a. Pretty a => a -> String
prettyPrint (Exp SrcSpanInfo -> String) -> Exp SrcSpanInfo -> String
forall a b. (a -> b) -> a -> b
$ HintRule -> Exp SrcSpanInfo
hintRuleRHS HintRule
m) ]

matchIdea :: Scope -> Decl_ -> HintRule -> Maybe (Int, Exp_) -> Exp_ -> Maybe (Exp_, [Note], [(String, R.SrcSpan)])
matchIdea :: Scope
-> Decl_
-> HintRule
-> Maybe (Int, Exp SrcSpanInfo)
-> Exp SrcSpanInfo
-> Maybe (Exp SrcSpanInfo, [Note], [(String, SrcSpan)])
matchIdea s :: Scope
s decl :: Decl_
decl HintRule{..} parent :: Maybe (Int, Exp SrcSpanInfo)
parent x :: Exp SrcSpanInfo
x = do
    let nm :: QName SrcSpanInfo -> QName SrcSpanInfo -> Bool
nm a :: QName SrcSpanInfo
a b :: QName SrcSpanInfo
b = (Scope, QName SrcSpanInfo) -> (Scope, QName SrcSpanInfo) -> Bool
scopeMatch (Scope
hintRuleScope,QName SrcSpanInfo
a) (Scope
s,QName SrcSpanInfo
b)
    Subst (Exp SrcSpanInfo)
u <- (QName SrcSpanInfo -> QName SrcSpanInfo -> Bool)
-> Bool
-> Exp SrcSpanInfo
-> Exp SrcSpanInfo
-> Maybe (Subst (Exp SrcSpanInfo))
unifyExp QName SrcSpanInfo -> QName SrcSpanInfo -> Bool
nm Bool
True Exp SrcSpanInfo
hintRuleLHS Exp SrcSpanInfo
x
    Subst (Exp SrcSpanInfo)
u <- (Exp SrcSpanInfo -> Exp SrcSpanInfo -> Bool)
-> Subst (Exp SrcSpanInfo) -> Maybe (Subst (Exp SrcSpanInfo))
forall a. (a -> a -> Bool) -> Subst a -> Maybe (Subst a)
validSubst Exp SrcSpanInfo -> Exp SrcSpanInfo -> Bool
forall (a :: * -> *) l1 l2.
(Annotated a, Eq (a ())) =>
a l1 -> a l2 -> Bool
(=~=) Subst (Exp SrcSpanInfo)
u
    -- need to check free vars before unqualification, but after subst (with e)
    -- need to unqualify before substitution (with res)
    let e :: Exp SrcSpanInfo
e = Subst (Exp SrcSpanInfo) -> Exp SrcSpanInfo -> Exp SrcSpanInfo
substitute Subst (Exp SrcSpanInfo)
u Exp SrcSpanInfo
hintRuleRHS
        res :: Exp SrcSpanInfo
res = Maybe (Int, Exp SrcSpanInfo) -> Exp SrcSpanInfo -> Exp SrcSpanInfo
addBracket Maybe (Int, Exp SrcSpanInfo)
parent (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> Exp SrcSpanInfo
performSpecial (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall a b. (a -> b) -> a -> b
$ Subst (Exp SrcSpanInfo) -> Exp SrcSpanInfo -> Exp SrcSpanInfo
substitute Subst (Exp SrcSpanInfo)
u (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall a b. (a -> b) -> a -> b
$ Scope -> Scope -> Exp SrcSpanInfo -> Exp SrcSpanInfo
unqualify Scope
hintRuleScope Scope
s Exp SrcSpanInfo
hintRuleRHS
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Exp SrcSpanInfo -> Set String
forall a. FreeVars a => a -> Set String
freeVars Exp SrcSpanInfo
e Set String -> Set String -> Set String
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ (String -> Bool) -> Set String -> Set String
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
isUnifyVar) (Exp SrcSpanInfo -> Set String
forall a. FreeVars a => a -> Set String
freeVars Exp SrcSpanInfo
hintRuleRHS))
            Set String -> Set String -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Exp SrcSpanInfo -> Set String
forall a. FreeVars a => a -> Set String
freeVars Exp SrcSpanInfo
x
        -- check no unexpected new free variables

    -- check it isn't going to get broken by QuasiQuotes as per #483
    -- if we have lambdas we might be moving, and QuasiQuotes, we might inadvertantly break free vars
    -- because quasi quotes don't show what free vars they make use of
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not ((Exp SrcSpanInfo -> Bool) -> [Exp SrcSpanInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Exp SrcSpanInfo -> Bool
forall l. Exp l -> Bool
isLambda ([Exp SrcSpanInfo] -> Bool) -> [Exp SrcSpanInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> [Exp SrcSpanInfo]
forall on. Uniplate on => on -> [on]
universe Exp SrcSpanInfo
hintRuleLHS) Bool -> Bool -> Bool
|| Bool -> Bool
not ((Exp SrcSpanInfo -> Bool) -> [Exp SrcSpanInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Exp SrcSpanInfo -> Bool
forall l. Exp l -> Bool
isQuasiQuote ([Exp SrcSpanInfo] -> Bool) -> [Exp SrcSpanInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> [Exp SrcSpanInfo]
forall on. Uniplate on => on -> [on]
universe Exp SrcSpanInfo
x)

    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Maybe (Exp SrcSpanInfo) -> [(String, Exp SrcSpanInfo)] -> Bool
checkSide Maybe (Exp SrcSpanInfo)
hintRuleSide ([(String, Exp SrcSpanInfo)] -> Bool)
-> [(String, Exp SrcSpanInfo)] -> Bool
forall a b. (a -> b) -> a -> b
$ ("original",Exp SrcSpanInfo
x) (String, Exp SrcSpanInfo)
-> [(String, Exp SrcSpanInfo)] -> [(String, Exp SrcSpanInfo)]
forall a. a -> [a] -> [a]
: ("result",Exp SrcSpanInfo
res) (String, Exp SrcSpanInfo)
-> [(String, Exp SrcSpanInfo)] -> [(String, Exp SrcSpanInfo)]
forall a. a -> [a] -> [a]
: Subst (Exp SrcSpanInfo) -> [(String, Exp SrcSpanInfo)]
forall a. Subst a -> [(String, a)]
fromSubst Subst (Exp SrcSpanInfo)
u
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Decl_ -> Maybe (Int, Exp SrcSpanInfo) -> Exp SrcSpanInfo -> Bool
checkDefine Decl_
decl Maybe (Int, Exp SrcSpanInfo)
parent Exp SrcSpanInfo
res
    (Exp SrcSpanInfo, [Note], [(String, SrcSpan)])
-> Maybe (Exp SrcSpanInfo, [Note], [(String, SrcSpan)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp SrcSpanInfo
res, [Note]
hintRuleNotes, [(String
s, Exp SrcSpanInfo -> SrcSpan
forall (a :: * -> *). Annotated a => a SrcSpanInfo -> SrcSpan
toSS Exp SrcSpanInfo
pos) | (s :: String
s, pos :: Exp SrcSpanInfo
pos) <- Subst (Exp SrcSpanInfo) -> [(String, Exp SrcSpanInfo)]
forall a. Subst a -> [(String, a)]
fromSubst Subst (Exp SrcSpanInfo)
u, Exp SrcSpanInfo -> SrcSpanInfo
forall (ast :: * -> *) l. Annotated ast => ast l -> l
ann Exp SrcSpanInfo
pos SrcSpanInfo -> SrcSpanInfo -> Bool
forall a. Eq a => a -> a -> Bool
/= SrcSpanInfo
an])


---------------------------------------------------------------------
-- SIDE CONDITIONS

checkSide :: Maybe Exp_ -> [(String, Exp_)] -> Bool
checkSide :: Maybe (Exp SrcSpanInfo) -> [(String, Exp SrcSpanInfo)] -> Bool
checkSide x :: Maybe (Exp SrcSpanInfo)
x bind :: [(String, Exp SrcSpanInfo)]
bind = Bool
-> (Exp SrcSpanInfo -> Bool) -> Maybe (Exp SrcSpanInfo) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Exp SrcSpanInfo -> Bool
bool Maybe (Exp SrcSpanInfo)
x
    where
        bool :: Exp_ -> Bool
        bool :: Exp SrcSpanInfo -> Bool
bool (InfixApp _ x :: Exp SrcSpanInfo
x op :: QOp SrcSpanInfo
op y :: Exp SrcSpanInfo
y)
            | QOp SrcSpanInfo -> Exp SrcSpanInfo
opExp QOp SrcSpanInfo
op Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "&&" = Exp SrcSpanInfo -> Bool
bool Exp SrcSpanInfo
x Bool -> Bool -> Bool
&& Exp SrcSpanInfo -> Bool
bool Exp SrcSpanInfo
y
            | QOp SrcSpanInfo -> Exp SrcSpanInfo
opExp QOp SrcSpanInfo
op Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "||" = Exp SrcSpanInfo -> Bool
bool Exp SrcSpanInfo
x Bool -> Bool -> Bool
|| Exp SrcSpanInfo -> Bool
bool Exp SrcSpanInfo
y
            | QOp SrcSpanInfo -> Exp SrcSpanInfo
opExp QOp SrcSpanInfo
op Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "==" = Exp SrcSpanInfo -> Exp SrcSpanInfo
expr (Exp SrcSpanInfo -> Exp SrcSpanInfo
fromParen1 Exp SrcSpanInfo
x) Exp SrcSpanInfo -> Exp SrcSpanInfo -> Bool
forall (a :: * -> *) l1 l2.
(Annotated a, Eq (a ())) =>
a l1 -> a l2 -> Bool
=~= Exp SrcSpanInfo -> Exp SrcSpanInfo
expr (Exp SrcSpanInfo -> Exp SrcSpanInfo
fromParen1 Exp SrcSpanInfo
y)
        bool (App _ x :: Exp SrcSpanInfo
x y :: Exp SrcSpanInfo
y) | Exp SrcSpanInfo
x Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "not" = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> Bool
bool Exp SrcSpanInfo
y
        bool (Paren _ x :: Exp SrcSpanInfo
x) = Exp SrcSpanInfo -> Bool
bool Exp SrcSpanInfo
x

        bool (App _ cond :: Exp SrcSpanInfo
cond (Exp SrcSpanInfo -> Exp SrcSpanInfo
sub -> Exp SrcSpanInfo
y))
            | 'i':'s':typ :: String
typ <- Exp SrcSpanInfo -> String
forall a. Named a => a -> String
fromNamed Exp SrcSpanInfo
cond = String -> Exp SrcSpanInfo -> Bool
isType String
typ Exp SrcSpanInfo
y
        bool (App _ (App _ cond :: Exp SrcSpanInfo
cond (Exp SrcSpanInfo -> Exp SrcSpanInfo
sub -> Exp SrcSpanInfo
x)) (Exp SrcSpanInfo -> Exp SrcSpanInfo
sub -> Exp SrcSpanInfo
y))
            | Exp SrcSpanInfo
cond Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "notIn" = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Exp SrcSpanInfo
x Exp SrcSpanInfo -> [Exp SrcSpanInfo] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Exp SrcSpanInfo -> [Exp SrcSpanInfo]
forall on. Uniplate on => on -> [on]
universe Exp SrcSpanInfo
y | Exp SrcSpanInfo
x <- Exp SrcSpanInfo -> [Exp SrcSpanInfo]
list Exp SrcSpanInfo
x, Exp SrcSpanInfo
y <- Exp SrcSpanInfo -> [Exp SrcSpanInfo]
list Exp SrcSpanInfo
y]
            | Exp SrcSpanInfo
cond Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "notEq" = Exp SrcSpanInfo
x Exp SrcSpanInfo -> Exp SrcSpanInfo -> Bool
forall (a :: * -> *) l1 l2.
(Annotated a, Eq (a ())) =>
a l1 -> a l2 -> Bool
/=~= Exp SrcSpanInfo
y
        bool x :: Exp SrcSpanInfo
x | Exp SrcSpanInfo
x Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "noTypeCheck" = Bool
True
        bool x :: Exp SrcSpanInfo
x | Exp SrcSpanInfo
x Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "noQuickCheck" = Bool
True
        bool x :: Exp SrcSpanInfo
x = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "Hint.Match.checkSide, unknown side condition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Exp SrcSpanInfo -> String
forall a. Pretty a => a -> String
prettyPrint Exp SrcSpanInfo
x

        expr :: Exp_ -> Exp_
        expr :: Exp SrcSpanInfo -> Exp SrcSpanInfo
expr (App _ (Exp SrcSpanInfo -> String
forall a. Named a => a -> String
fromNamed -> String
"subst") x :: Exp SrcSpanInfo
x) = Exp SrcSpanInfo -> Exp SrcSpanInfo
sub (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> Exp SrcSpanInfo
fromParen1 Exp SrcSpanInfo
x
        expr x :: Exp SrcSpanInfo
x = Exp SrcSpanInfo
x

        isType :: String -> Exp SrcSpanInfo -> Bool
isType "Compare" x :: Exp SrcSpanInfo
x = Bool
True -- just a hint for proof stuff
        isType "Atom" x :: Exp SrcSpanInfo
x = Exp SrcSpanInfo -> Bool
forall a. Brackets a => a -> Bool
isAtom Exp SrcSpanInfo
x
        isType "WHNF" x :: Exp SrcSpanInfo
x = Exp SrcSpanInfo -> Bool
isWHNF Exp SrcSpanInfo
x
        isType "Wildcard" x :: Exp SrcSpanInfo
x = (FieldUpdate SrcSpanInfo -> Bool)
-> [FieldUpdate SrcSpanInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FieldUpdate SrcSpanInfo -> Bool
forall l. FieldUpdate l -> Bool
isFieldWildcard ([FieldUpdate SrcSpanInfo] -> Bool)
-> [FieldUpdate SrcSpanInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> [FieldUpdate SrcSpanInfo]
forall x (f :: * -> *).
(Data x, Data (f SrcSpanInfo)) =>
x -> [f SrcSpanInfo]
universeS Exp SrcSpanInfo
x
        isType "Nat" (Exp SrcSpanInfo -> Maybe Integer
asInt -> Just x :: Integer
x) | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 = Bool
True
        isType "Pos" (Exp SrcSpanInfo -> Maybe Integer
asInt -> Just x :: Integer
x) | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>  0 = Bool
True
        isType "Neg" (Exp SrcSpanInfo -> Maybe Integer
asInt -> Just x :: Integer
x) | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<  0 = Bool
True
        isType "NegZero" (Exp SrcSpanInfo -> Maybe Integer
asInt -> Just x :: Integer
x) | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = Bool
True
        isType ('L':'i':'t':typ :: String
typ@(_:_)) (Lit _ x :: Literal SrcSpanInfo
x) = [String] -> String
forall a. [a] -> a
head (String -> [String]
words (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Literal SrcSpanInfo -> String
forall a. Show a => a -> String
show Literal SrcSpanInfo
x) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
typ
        isType typ :: String
typ x :: Exp SrcSpanInfo
x = [String] -> String
forall a. [a] -> a
head (String -> [String]
words (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> String
forall a. Show a => a -> String
show Exp SrcSpanInfo
x) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
typ

        asInt :: Exp_ -> Maybe Integer
        asInt :: Exp SrcSpanInfo -> Maybe Integer
asInt (Paren _ x :: Exp SrcSpanInfo
x) = Exp SrcSpanInfo -> Maybe Integer
asInt Exp SrcSpanInfo
x
        asInt (NegApp _ x :: Exp SrcSpanInfo
x) = Integer -> Integer
forall a. Num a => a -> a
negate (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp SrcSpanInfo -> Maybe Integer
asInt Exp SrcSpanInfo
x
        asInt (Lit _ (Int _ x :: Integer
x _)) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
x
        asInt _ = Maybe Integer
forall a. Maybe a
Nothing

        list :: Exp_ -> [Exp_]
        list :: Exp SrcSpanInfo -> [Exp SrcSpanInfo]
list (List _ xs :: [Exp SrcSpanInfo]
xs) = [Exp SrcSpanInfo]
xs
        list x :: Exp SrcSpanInfo
x = [Exp SrcSpanInfo
x]

        sub :: Exp_ -> Exp_
        sub :: Exp SrcSpanInfo -> Exp SrcSpanInfo
sub = (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall on. Uniplate on => (on -> on) -> on -> on
transform Exp SrcSpanInfo -> Exp SrcSpanInfo
f
            where f :: Exp SrcSpanInfo -> Exp SrcSpanInfo
f (Exp SrcSpanInfo -> Var_
forall a b. View a b => a -> b
view -> Var_ x :: String
x) | Just y :: Exp SrcSpanInfo
y <- String -> [(String, Exp SrcSpanInfo)] -> Maybe (Exp SrcSpanInfo)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
x [(String, Exp SrcSpanInfo)]
bind = Exp SrcSpanInfo
y
                  f x :: Exp SrcSpanInfo
x = Exp SrcSpanInfo
x


-- does the result look very much like the declaration
checkDefine :: Decl_ -> Maybe (Int, Exp_) -> Exp_ -> Bool
checkDefine :: Decl_ -> Maybe (Int, Exp SrcSpanInfo) -> Exp SrcSpanInfo -> Bool
checkDefine x :: Decl_
x Nothing y :: Exp SrcSpanInfo
y = Decl_ -> String
forall a. Named a => a -> String
fromNamed Decl_
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= Exp SrcSpanInfo -> String
forall a. Named a => a -> String
fromNamed ((QName SrcSpanInfo -> QName SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall from to. Biplate from to => (to -> to) -> from -> from
transformBi QName SrcSpanInfo -> QName SrcSpanInfo
unqual (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall a b. (a -> b) -> a -> b
$ [Exp SrcSpanInfo] -> Exp SrcSpanInfo
forall a. [a] -> a
head ([Exp SrcSpanInfo] -> Exp SrcSpanInfo)
-> [Exp SrcSpanInfo] -> Exp SrcSpanInfo
forall a b. (a -> b) -> a -> b
$ Exp SrcSpanInfo -> [Exp SrcSpanInfo]
fromApps Exp SrcSpanInfo
y)
checkDefine _ _ _ = Bool
True


---------------------------------------------------------------------
-- TRANSFORMATION

-- if it has _eval_ do evaluation on it
performSpecial :: Exp_ -> Exp_
performSpecial :: Exp SrcSpanInfo -> Exp SrcSpanInfo
performSpecial = (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall on. Uniplate on => (on -> on) -> on -> on
transform Exp SrcSpanInfo -> Exp SrcSpanInfo
fNoParen (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> (Exp SrcSpanInfo -> Exp SrcSpanInfo)
-> Exp SrcSpanInfo
-> Exp SrcSpanInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp SrcSpanInfo -> Exp SrcSpanInfo
fEval
    where
        fEval :: Exp SrcSpanInfo -> Exp SrcSpanInfo
fEval (App _ e :: Exp SrcSpanInfo
e x :: Exp SrcSpanInfo
x) | Exp SrcSpanInfo
e Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "_eval_" = Exp SrcSpanInfo -> Exp SrcSpanInfo
reduce Exp SrcSpanInfo
x
        fEval x :: Exp SrcSpanInfo
x = Exp SrcSpanInfo
x

        fNoParen :: Exp SrcSpanInfo -> Exp SrcSpanInfo
fNoParen (App _ e :: Exp SrcSpanInfo
e x :: Exp SrcSpanInfo
x) | Exp SrcSpanInfo
e Exp SrcSpanInfo -> String -> Bool
forall a. Named a => a -> String -> Bool
~= "_noParen_" = Exp SrcSpanInfo -> Exp SrcSpanInfo
fromParen Exp SrcSpanInfo
x
        fNoParen x :: Exp SrcSpanInfo
x = Exp SrcSpanInfo
x

-- contract Data.List.foo ==> foo, if Data.List is loaded
unqualify :: Scope -> Scope -> Exp_ -> Exp_
unqualify :: Scope -> Scope -> Exp SrcSpanInfo -> Exp SrcSpanInfo
unqualify from :: Scope
from to :: Scope
to = (QName SrcSpanInfo -> QName SrcSpanInfo)
-> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall from to. Biplate from to => (to -> to) -> from -> from
transformBi QName SrcSpanInfo -> QName SrcSpanInfo
f
    where
        f :: QName SrcSpanInfo -> QName SrcSpanInfo
f x :: QName SrcSpanInfo
x@(UnQual _ (Ident _ s :: String
s)) | String -> Bool
isUnifyVar String
s = QName SrcSpanInfo
x
        f x :: QName SrcSpanInfo
x = (Scope, QName SrcSpanInfo) -> Scope -> QName SrcSpanInfo
scopeMove (Scope
from,QName SrcSpanInfo
x) Scope
to


addBracket :: Maybe (Int,Exp_) -> Exp_ -> Exp_
addBracket :: Maybe (Int, Exp SrcSpanInfo) -> Exp SrcSpanInfo -> Exp SrcSpanInfo
addBracket (Just (i :: Int
i,p :: Exp SrcSpanInfo
p)) c :: Exp SrcSpanInfo
c | Int -> Exp SrcSpanInfo -> Exp SrcSpanInfo -> Bool
needBracketOld Int
i Exp SrcSpanInfo
p Exp SrcSpanInfo
c = SrcSpanInfo -> Exp SrcSpanInfo -> Exp SrcSpanInfo
forall l. l -> Exp l -> Exp l
Paren SrcSpanInfo
an Exp SrcSpanInfo
c
addBracket _ x :: Exp SrcSpanInfo
x = Exp SrcSpanInfo
x