-- |
-- Module      : Conjure.Defn.Redundancy
-- Copyright   : (c) 2021-2024 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of "Conjure".
--
-- This module exports functions that check redundancy in 'Defn's.
--
-- You are probably better off importing "Conjure".
module Conjure.Defn.Redundancy
  ( isRedundantDefn
  , isRedundantBySubsumption
  , isRedundantByRepetition
  , isRedundantByIntroduction
  , isRedundantModuloRewriting
  , hasRedundantRecursion
  , subsumedWith
  , simplifyDefn
  , introduceVariableAt
  )
where

import Conjure.Defn

-- | Returns whether the given 'Defn' is redundant
--   with regards to repetitions on RHSs.
--
-- Here is an example of a redundant 'Defn':
--
-- > 0 ? 0  =  1
-- > 0 ? x  =  1
-- > x ? 0  =  x
-- > x ? y  =  x
--
-- It is redundant because it is equivalent to:
--
-- > 0 ? _  =  1
-- > x ? _  =  x
--
-- This function safely handles holes on the RHSs
-- by being conservative in cases these are found:
-- nothing can be said before their fillings.
isRedundantDefn :: Defn -> Bool
isRedundantDefn :: Defn -> Bool
isRedundantDefn Defn
d  =  Defn -> Bool
isRedundantBySubsumption Defn
d
                   Bool -> Bool -> Bool
|| Defn -> Bool
isRedundantByRepetition Defn
d
                   Bool -> Bool -> Bool
|| Defn -> Bool
isRedundantByRootRecursions Defn
d
--                 || isRedundantByIntroduction d
-- we do not use isRedundantByIntroduction above
-- as it does not pay off in terms of runtime vs number of pruned candidates
--
-- The number of candidates is reduced usually by less than 1%
-- and the runtime increases by 50% or sometimes 100%.


-- | Returns whether the given 'Defn' is redundant
--   with regards to repetitions on RHSs.
--
-- Here is an example of a redundant 'Defn':
--
-- > 0 ? 0  =  1
-- > 0 ? x  =  1
-- > x ? 0  =  x
-- > x ? y  =  x
--
-- It is redundant because it is equivalent to:
--
-- > 0 ? _  =  1
-- > x ? _  =  x
--
-- @1@ and @x@ are repeated in the results for when
-- the first arguments are @0@ and @x@.
isRedundantByRepetition :: Defn -> Bool
isRedundantByRepetition :: Defn -> Bool
isRedundantByRepetition Defn
d  =  ((Expr -> Expr) -> Bool) -> [Expr -> Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr -> Expr) -> Bool
anyAllEqual [Expr -> Expr]
shovels
  where
  nArgs :: Int
nArgs  =  [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> (Bndn -> [Expr]) -> Bndn -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
forall a. HasCallStack => [a] -> [a]
tail ([Expr] -> [Expr]) -> (Bndn -> [Expr]) -> Bndn -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp (Expr -> [Expr]) -> (Bndn -> Expr) -> Bndn -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bndn -> Expr
forall a b. (a, b) -> a
fst (Bndn -> Int) -> Bndn -> Int
forall a b. (a -> b) -> a -> b
$ Defn -> Bndn
forall a. HasCallStack => [a] -> a
head Defn
d
  shovels :: [Expr -> Expr]
  shovels :: [Expr -> Expr]
shovels  =  [Int -> Expr -> Expr
digApp Int
n | Int
n <- [Int
1..Int
nArgs]]
  anyAllEqual :: (Expr -> Expr) -> Bool
  anyAllEqual :: (Expr -> Expr) -> Bool
anyAllEqual Expr -> Expr
shovel  =  (Defn -> Bool) -> [Defn] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Defn
bs -> Defn -> Bool
forall a. Eq a => [a] -> Bool
allEqual2 Defn
bs Bool -> Bool -> Bool
&& Defn -> Bool
isDefined Defn
bs)
                      ([Defn] -> Bool) -> (Defn -> [Defn]) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Bndn -> Expr) -> Defn -> [Defn]
forall b a. Eq b => (a -> b) -> [a] -> [[a]]
classifyOn Bndn -> Expr
forall a b. (a, b) -> a
fst
                      (Defn -> [Defn]) -> (Defn -> Defn) -> Defn -> [Defn]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Bndn -> Bndn) -> Defn -> Defn
forall a b. (a -> b) -> [a] -> [b]
map (Bndn -> Bndn
canonicalizeBndn (Bndn -> Bndn) -> (Bndn -> Bndn) -> Bndn -> Bndn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> Bndn -> Bndn
forall a a' b. (a -> a') -> (a, b) -> (a', b)
first Expr -> Expr
shovel)
                      (Defn -> Bool) -> Defn -> Bool
forall a b. (a -> b) -> a -> b
$  Defn
d

-- | Returns whether the given 'Defn' is redundant
--   with regards to case elimination
--
-- The following is redundant according to this criterium:
--
-- > foo []  =  []
-- > foo (x:xs)  =  x:xs
--
-- It is equivalent to:
--
-- > foo xs = xs
--
-- The following is also redundant:
--
-- > [] ?? xs  =  []
-- > (x:xs) ?? ys  =  x:xs
--
-- as it is equivalent to:
--
-- > xs ?? ys == xs
--
-- This function is not used as one of the criteria in 'isRedundantDefn'
-- because it does not pay-off
-- in terms of runtime vs number of pruned candidates.
isRedundantByIntroduction :: Defn -> Bool
isRedundantByIntroduction :: Defn -> Bool
isRedundantByIntroduction Defn
d  =  (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Int -> Bool
anyAllEqual [Int
1..Int
nArgs]
  where
  nArgs :: Int
nArgs  =  [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> (Bndn -> [Expr]) -> Bndn -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
forall a. HasCallStack => [a] -> [a]
tail ([Expr] -> [Expr]) -> (Bndn -> [Expr]) -> Bndn -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
unfoldApp (Expr -> [Expr]) -> (Bndn -> Expr) -> Bndn -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bndn -> Expr
forall a b. (a, b) -> a
fst (Bndn -> Int) -> Bndn -> Int
forall a b. (a -> b) -> a -> b
$ Defn -> Bndn
forall a. HasCallStack => [a] -> a
head Defn
d
  anyAllEqual :: Int -> Bool
  anyAllEqual :: Int -> Bool
anyAllEqual Int
i  =  (Defn -> Bool) -> [Defn] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Defn
bs -> Defn -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Defn
bs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 Bool -> Bool -> Bool
&& Defn -> Bool
isDefined Defn
bs Bool -> Bool -> Bool
&& Int -> Defn -> Bool
noConflicts Int
i Defn
bs)
                 ([Defn] -> Bool) -> (Defn -> [Defn]) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Bndn -> Expr) -> Defn -> [Defn]
forall b a. Eq b => (a -> b) -> [a] -> [[a]]
classifyOn (Int -> Expr -> Expr
digApp Int
i (Expr -> Expr) -> (Bndn -> Expr) -> Bndn -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bndn -> Expr
forall a b. (a, b) -> a
fst)
                 (Defn -> [Defn]) -> (Defn -> Defn) -> Defn -> [Defn]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (Bndn -> Bndn) -> Defn -> Defn
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Bndn -> Bndn
canonicalizeBndnLast Int
i)
                 (Defn -> Bool) -> Defn -> Bool
forall a b. (a -> b) -> a -> b
$  Defn
d
  noConflicts :: Int -> [Bndn] -> Bool
  noConflicts :: Int -> Defn -> Bool
noConflicts Int
i Defn
bs  =  case [Expr] -> [[Expr]]
listConflicts ((Bndn -> Expr) -> Defn -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Bndn -> Expr
forall a b. (a, b) -> b
snd Defn
bs) of
                       [] -> Bool
True
                       [[Expr]
es] -> [Expr]
es [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr
efxs Expr -> Int -> Expr
$!! Int
i | (Expr
efxs,Expr
_) <- Defn
bs]
                       [[Expr]]
_ -> Bool
False

-- | Returns whether the given 'Defn' is redundant
--   with regards to recursions
--
-- The following is redundant:
--
-- > xs ?? []  =  []
-- > xs ?? (x:ys)  =  xs ?? []
--
-- The LHS of a base-case pattern, matches the RHS of a recursive pattern.
-- The second RHS may be replaced by simply @[]@ which makes it redundant.
hasRedundantRecursion :: Defn -> Bool
hasRedundantRecursion :: Defn -> Bool
hasRedundantRecursion Defn
d  =  Bool -> Bool
not (Defn -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Defn
rs) Bool -> Bool -> Bool
&& (Bndn -> Bool) -> Defn -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bndn -> Bool
forall {b}. (Expr, b) -> Bool
matchesRHS Defn
bs
  where
  (Defn
bs,Defn
rs)  =  (Bndn -> Bool) -> Defn -> (Defn, Defn)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Bndn -> Bool
isBaseCase Defn
d
  matchesRHS :: (Expr, b) -> Bool
matchesRHS (Expr
lhs,b
_)  =  (Bndn -> Bool) -> Defn -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Expr -> Expr -> Bool
`hasAppInstanceOf` Expr
lhs) (Expr -> Bool) -> (Bndn -> Expr) -> Bndn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bndn -> Expr
forall a b. (a, b) -> b
snd) Defn
rs

-- | Returns whether a given 'Defn' is redundant
--   with regards to root recursions.
--
-- When there is a single constant base case and all recursive calls
-- are at the root: we have a redundant function.
-- (Modulo error functions, which are undesired anyway.)
--
-- > xs ? []  =  []
-- > xs ? (x:ys)  =  xs ? ys
--
-- Above it does not really pays off to follow the recursive calls,
-- at the end we always reach an empty list.
isRedundantByRootRecursions :: Defn -> Bool
isRedundantByRootRecursions :: Defn -> Bool
isRedundantByRootRecursions Defn
d  =  case (Expr -> Bool) -> [Expr] -> ([Expr], [Expr])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Expr -> Bool
isGround ([Expr] -> ([Expr], [Expr])) -> [Expr] -> ([Expr], [Expr])
forall a b. (a -> b) -> a -> b
$ (Bndn -> Expr) -> Defn -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Bndn -> Expr
forall a b. (a, b) -> b
snd Defn
d of
  ([Expr
b], rs :: [Expr]
rs@(Expr
_:[Expr]
_))  ->  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isHole [Expr]
rs
  (bs :: [Expr]
bs@(Expr
_:[Expr]
_), rs :: [Expr]
rs@(Expr
_:[Expr]
_))  -> (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isHole [Expr]
rs Bool -> Bool -> Bool
&& (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isGround [Expr]
bs Bool -> Bool -> Bool
&& [Expr] -> Bool
forall a. Eq a => [a] -> Bool
allEqual [Expr]
bs
  ([Expr], [Expr])
_  -> Bool
False

-- | Introduces a hole at a given position in the binding:
--
-- > > introduceVariableAt 1 (xxs -?- (yy -:- yys), (yy -:- yys) -++- (yy -:- yys))
-- > (xs ? (y:ys) :: [Int],(y:ys) ++ (y:ys) :: [Int])
--
-- > > introduceVariableAt 2 (xxs -?- (yy -:- yys), (yy -:- yys) -++- (yy -:- yys))
-- > (xs ? x :: [Int],x ++ x :: [Int])
--
-- Relevant occurrences are replaced.
introduceVariableAt :: Int -> Bndn -> Bndn
introduceVariableAt :: Int -> Bndn -> Bndn
introduceVariableAt Int
i b :: Bndn
b@(Expr
l,Expr
r)
  | Expr -> Bool
isVar Expr
p    =  Bndn
b -- already a variable
-- | isGround p  =  (newVar, r)  -- enabling catches a different set of candidates
  | Bool
otherwise  =  Expr -> Bndn
unfoldPair
               (Expr -> Bndn) -> Expr -> Bndn
forall a b. (a -> b) -> a -> b
$  Bndn -> Expr
foldPair Bndn
b Expr -> Defn -> Expr
// [(Expr
p,Expr
newVar)]
  where
  p :: Expr
p  =  Expr
l Expr -> Int -> Expr
$!! Int
i
  newVar :: Expr
newVar  =  String
newName String -> Expr -> Expr
`varAsTypeOf` Expr
p
  newName :: String
newName  =  [String] -> String
forall a. HasCallStack => [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
variableNamesFromTemplate String
"x" [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ Expr -> [String]
varnames Expr
l
  varnames :: Expr -> [String]
  varnames :: Expr -> [String]
varnames Expr
e  =  [String
n | Value (Char
'_':String
n) Dynamic
_ <- Expr -> [Expr]
vars Expr
e]

-- | Returns whether the given 'Defn' is redundant
--   with regards to subsumption by latter patterns
--
-- Here is an example of a redundant 'Defn' by this criterium:
--
-- > foo 0  =  0
-- > foo x  =  x
isRedundantBySubsumption :: Defn -> Bool
isRedundantBySubsumption :: Defn -> Bool
isRedundantBySubsumption  =  [Expr] -> Bool
is ([Expr] -> Bool) -> (Defn -> [Expr]) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bndn -> Expr) -> Defn -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Bndn -> Expr
foldPair (Defn -> [Expr]) -> (Defn -> Defn) -> Defn -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bndn -> Bool) -> Defn -> Defn
forall a. (a -> Bool) -> [a] -> [a]
filter Bndn -> Bool
isCompleteBndn
  -- above, we could have used noUnbound instead of isCompleteBndn
  -- we use isCompleteBndn as it is faster
  where
  is :: [Expr] -> Bool
is []  =  Bool
False
  is (Expr
b:[Expr]
bs)  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr
b Expr -> Expr -> Bool
`isInstanceOf`) [Expr]
bs Bool -> Bool -> Bool
|| [Expr] -> Bool
is [Expr]
bs

-- | Returns whether the given 'Defn' is redundant modulo
--   subsumption and rewriting.
--
-- (cf. 'subsumedWith')
isRedundantModuloRewriting :: (Expr -> Expr) -> Defn -> Bool
isRedundantModuloRewriting :: (Expr -> Expr) -> Defn -> Bool
isRedundantModuloRewriting Expr -> Expr
normalize  =  Defn -> Bool
is
  where
  is :: Defn -> Bool
is []  =  Bool
False
  is (Bndn
b:Defn
bs)  =  (Bndn -> Bool) -> Defn -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Expr -> Expr) -> Bndn -> Bndn -> Bool
subsumedWith Expr -> Expr
normalize Bndn
b) Defn
bs
             Bool -> Bool -> Bool
|| Defn -> Bool
is Defn
bs

-- | Simplifies a definition by removing redundant patterns
--
-- This may be useful in the following case:
--
-- > 0 ^^^ 0  =  0
-- > 0 ^^^ x  =  x
-- > x ^^^ 0  =  x
-- > _ ^^^ _  =  0
--
-- The first pattern is subsumed by the last pattern.
simplifyDefn :: Defn -> Defn
simplifyDefn :: Defn -> Defn
simplifyDefn []  =  []
simplifyDefn (Bndn
b:Defn
bs)  =  [Bndn
b | (Expr -> Bool) -> [Expr] -> Bool
forall a. (a -> Bool) -> [a] -> Bool
none (Bndn -> Expr
foldPair Bndn
b Expr -> Expr -> Bool
`isInstanceOf`) ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ (Bndn -> Expr) -> Defn -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Bndn -> Expr
foldPair Defn
bs]
                     Defn -> Defn -> Defn
forall a. [a] -> [a] -> [a]
++ Defn -> Defn
simplifyDefn Defn
bs

-- | Returns whether a binding is subsumed by another modulo rewriting
--
-- > > let normalize = (// [(zero -+- zero, zero)])
-- > > subsumedWith normalize (ff zero, zero) (ff xx, xx -+- xx)
-- > True
--
-- > > subsumedWith normalize (ff zero, zero) (ff xx, xx -+- one)
-- > False
--
-- > > subsumedWith normalize (zero -?- xx, zero) (xx -?- yy, xx -+- xx)
-- > True
--
-- (cf. 'isRedundantModuloRewriting')
subsumedWith :: (Expr -> Expr) -> Bndn -> Bndn -> Bool
subsumedWith :: (Expr -> Expr) -> Bndn -> Bndn -> Bool
subsumedWith Expr -> Expr
normalize (Expr
lhs1,Expr
rhs1) (Expr
lhs2,Expr
rhs2)
  | Expr -> Bool
hasHole Expr
rhs2  =  Bool
False
  | Bool
otherwise  =  case Expr
lhs1 Expr -> Expr -> Maybe Defn
`match` Expr
lhs2 of
                  Maybe Defn
Nothing -> Bool
False
                  Just Defn
bs -> Bndn -> Expr
forall a b. (a, b) -> b
snd (Bndn -> Bndn
canonicalizeBndn (Expr
lhs2, Expr -> Expr
normalize (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
rhs2 Expr -> Defn -> Expr
//- Defn
bs))
                          Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Bndn -> Expr
forall a b. (a, b) -> b
snd (Bndn -> Bndn
canonicalizeBndn (Expr
lhs1, Expr
rhs1))