-- |
-- Module      : Conjure.Defn
-- Copyright   : (c) 2021 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 the 'Defn' type synonym and utilities involving it.
--
-- You are probably better off importing "Conjure".
{-# LANGUAGE TupleSections #-}
module Conjure.Defn
  ( Defn
  , Bndn
  , toDynamicWithDefn
  , devaluate
  , deval
  , devl
  , devalFast
  , showDefn
  , printDefn
  , defnApparentlyTerminates
  , isRedundantDefn
  , isRedundantBySubsumption
  , isRedundantByRepetition
  , isRedundantByIntroduction
  , hasRedundantRecursion
  , isCompleteDefn
  , isCompleteBndn
  , simplifyDefn
  , canonicalizeBndn
  , canonicalizeBndnLast
  , hasUnbound
  , noUnbound
  , isUndefined
  , isDefined
  , introduceVariableAt
  , isBaseCase
  , isRecursiveCase
  , isRecursiveDefn
  , module Conjure.Expr
  )
where

import Conjure.Utils
import Conjure.Expr
import Data.Express
import Data.Express.Express
import Data.Express.Fixtures
import Data.Dynamic
import Control.Applicative ((<$>)) -- for older GHCs
import Test.LeanCheck.Utils ((-:>), classifyOn)

-- | A function definition as a list of top-level case bindings ('Bndn').
--
-- Here is an example using the notation from "Data.Express.Fixtures":
--
-- > sumV :: Expr
-- > sumV  =  var "sum" (undefined :: [Int] -> Int)
-- >
-- > (=-) = (,)
-- > infixr 0 =-
-- >
-- > sumDefn :: Defn
-- > sumDefn  =  [ sum' nil           =-  zero
-- >             , sum' (xx -:- xxs)  =-  xx -+- (sumV :$ xxs)
-- >             ]  where  sum' e  =  sumV :$ e
type Defn  =  [Bndn]

-- | A single binding in a definition ('Defn').
type Bndn  =  (Expr,Expr)

-- | Pretty-prints a 'Defn' as a 'String':
--
-- > > putStr $ showDefn sumDefn
-- > sum []  =  0
-- > sum (x:xs)  =  x + sum xs
showDefn :: Defn -> String
showDefn :: Defn -> String
showDefn  =  [String] -> String
unlines ([String] -> String) -> (Defn -> [String]) -> Defn -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bndn -> String) -> Defn -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Bndn -> String
show1
  where
  show1 :: Bndn -> String
show1 (Expr
lhs,Value String
"if" Dynamic
_ :$ Expr
c :$ Expr
t :$ Expr
e)  =  String
lhseqs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"if " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
c
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
spaces String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"then " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
t
                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
spaces String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"else " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
e
                                              where
                                              lhseqs :: String
lhseqs  =  Expr -> String
showExpr Expr
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  =  "
                                              spaces :: String
spaces  =  (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (Char -> Char -> Char
forall a b. a -> b -> a
const Char
' ') String
lhseqs
  show1 (Expr
lhs,Expr
rhs)  =  Expr -> String
showExpr Expr
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  =  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
rhs

-- | Pretty-prints a 'Defn' to the screen.
--
-- > > printDefn sumDefn
-- > sum []  =  0
-- > sum (x:xs)  =  x + sum xs
printDefn :: Defn -> IO ()
printDefn :: Defn -> IO ()
printDefn  =  String -> IO ()
putStr (String -> IO ()) -> (Defn -> String) -> Defn -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> String
showDefn

type Memo  =  [(Expr, Maybe Dynamic)]

-- | Evaluates an 'Expr' to a 'Dynamic' value
--   using the given 'Defn' as definition
--   when a recursive call is found.
--
-- Arguments:
--
-- 1. a function that deeply reencodes an expression (cf. 'expr')
-- 2. the maximum number of recursive evaluations
-- 3. a 'Defn' to be used when evaluating the given 'Expr'
-- 4. an 'Expr' to be evaluated
--
-- This function cannot be used to evaluate a functional value for the given 'Defn'
-- and can only be used when occurrences of the given 'Defn' are fully applied.
--
-- The function the deeply reencodes an 'Expr' can be defined using
-- functionality present in "Conjure.Conjurable".  Here's a quick-and-dirty version
-- that is able to reencode 'Bool's, 'Int's and their lists:
--
-- > exprExpr :: Expr -> Expr
-- > exprExpr  =  conjureExpress (undefined :: Bool -> [Bool] -> Int -> [Int] -> ())
--
-- The maximum number of recursive evaluations counts in two ways:
--
-- 1. the maximum number of entries in the recursive-evaluation memo table;
-- 2. the maximum number of terminal values considered (but in this case the
--    limit is multiplied by the _size_ of the given 'Defn'.
--
-- These could be divided into two separate parameters but
-- then there would be an extra _dial_ to care about...
--
-- (cf. 'devaluate', 'deval', 'devl')
toDynamicWithDefn :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic
toDynamicWithDefn :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic
toDynamicWithDefn Expr -> Expr
exprExpr Int
mx Defn
cx  =  ((Int, Memo, Dynamic) -> Dynamic)
-> Maybe (Int, Memo, Dynamic) -> Maybe Dynamic
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
_,Memo
_,Dynamic
d) -> Dynamic
d) (Maybe (Int, Memo, Dynamic) -> Maybe Dynamic)
-> (Expr -> Maybe (Int, Memo, Dynamic)) -> Expr -> Maybe Dynamic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re (Int
mx Int -> Int -> Int
forall a. Num a => a -> a -> a
* [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Bndn -> Int) -> Defn -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Int
size (Expr -> Int) -> (Bndn -> Expr) -> Bndn -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bndn -> Expr
forall a b. (a, b) -> b
snd) Defn
cx)) []
  where
  (Expr
ef':[Expr]
_)  =  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 -> [Expr]) -> Bndn -> [Expr]
forall a b. (a -> b) -> a -> b
$ Defn -> Bndn
forall a. HasCallStack => [a] -> a
head Defn
cx

  -- recursively evaluate an expression, the entry point
  re :: Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
  re :: Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n Memo
m Expr
_  | Memo -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Memo
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
mx  =  String -> Maybe (Int, Memo, Dynamic)
forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: recursion limit reached"
  re Int
n Memo
m Expr
_  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0  =  String -> Maybe (Int, Memo, Dynamic)
forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: evaluation limit reached"
  re Int
n Memo
m (Value String
"if" Dynamic
_ :$ Expr
ec :$ Expr
ex :$ Expr
ey)  =  case Int -> Memo -> Expr -> Maybe (Int, Memo, Bool)
forall a. Typeable a => Int -> Memo -> Expr -> Maybe (Int, Memo, a)
rev Int
n Memo
m Expr
ec of
    Maybe (Int, Memo, Bool)
Nothing    -> Maybe (Int, Memo, Dynamic)
forall a. Maybe a
Nothing
    Just (Int
n,Memo
m,Bool
True)  -> Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n Memo
m Expr
ex
    Just (Int
n,Memo
m,Bool
False) -> Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n Memo
m Expr
ey
  re Int
n Memo
m (Value String
"||" Dynamic
_ :$ Expr
ep :$ Expr
eq)  =  case Int -> Memo -> Expr -> Maybe (Int, Memo, Bool)
forall a. Typeable a => Int -> Memo -> Expr -> Maybe (Int, Memo, a)
rev Int
n Memo
m Expr
ep of
    Maybe (Int, Memo, Bool)
Nothing        -> Maybe (Int, Memo, Dynamic)
forall a. Maybe a
Nothing
    Just (Int
n,Memo
m,Bool
True)  -> (Int
n,Memo
m,) (Dynamic -> (Int, Memo, Dynamic))
-> Maybe Dynamic -> Maybe (Int, Memo, Dynamic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic (Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
True)
    Just (Int
n,Memo
m,Bool
False) -> Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n Memo
m Expr
eq
  re Int
n Memo
m (Value String
"&&" Dynamic
_ :$ Expr
ep :$ Expr
eq)  =  case Int -> Memo -> Expr -> Maybe (Int, Memo, Bool)
forall a. Typeable a => Int -> Memo -> Expr -> Maybe (Int, Memo, a)
rev Int
n Memo
m Expr
ep of
    Maybe (Int, Memo, Bool)
Nothing    -> Maybe (Int, Memo, Dynamic)
forall a. Maybe a
Nothing
    Just (Int
n,Memo
m,Bool
True)  -> Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n Memo
m Expr
eq
    Just (Int
n,Memo
m,Bool
False) -> (Int
n,Memo
m,) (Dynamic -> (Int, Memo, Dynamic))
-> Maybe Dynamic -> Maybe (Int, Memo, Dynamic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic (Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False)
  re Int
n Memo
m Expr
e  =  case Expr -> [Expr]
unfoldApp Expr
e of
    [] -> String -> Maybe (Int, Memo, Dynamic)
forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: empty application unfold"  -- should never happen
    [Expr
e] -> (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Memo
m,) (Dynamic -> (Int, Memo, Dynamic))
-> Maybe Dynamic -> Maybe (Int, Memo, Dynamic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic Expr
e
    (Expr
ef:[Expr]
exs) | Expr
ef Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ef' -> Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
red Int
n Memo
m ([Expr] -> Expr
foldApp (Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:(Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
exprExpr [Expr]
exs))
             | Bool
otherwise -> (Maybe (Int, Memo, Dynamic) -> Expr -> Maybe (Int, Memo, Dynamic))
-> Maybe (Int, Memo, Dynamic)
-> [Expr]
-> Maybe (Int, Memo, Dynamic)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Maybe (Int, Memo, Dynamic) -> Expr -> Maybe (Int, Memo, Dynamic)
($$) (Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n Memo
m Expr
ef) [Expr]
exs

  -- like 're' but is bound to an actual Haskell value instead of a Dynamic
  rev :: Typeable a => Int -> Memo -> Expr -> Maybe (Int, Memo, a)
  rev :: forall a. Typeable a => Int -> Memo -> Expr -> Maybe (Int, Memo, a)
rev Int
n Memo
m Expr
e  =  case Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n Memo
m Expr
e of
                Maybe (Int, Memo, Dynamic)
Nothing    -> Maybe (Int, Memo, a)
forall a. Maybe a
Nothing
                Just (Int
n,Memo
m,Dynamic
d) -> case Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
                                Maybe a
Nothing -> Maybe (Int, Memo, a)
forall a. Maybe a
Nothing
                                Just a
x  -> (Int, Memo, a) -> Maybe (Int, Memo, a)
forall a. a -> Maybe a
Just (Int
n, Memo
m, a
x)

  -- evaluates by matching on one of cases of the actual definition
  -- should only be used to evaluate an expr of the form:
  -- ef' :$ exprExpr ex :$ exprExpr ey :$ ...
  red :: Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
  red :: Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
red Int
n Memo
m Expr
e  |  Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n  =  String -> Maybe (Int, Memo, Dynamic)
forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: argument-size limit reached"
  red Int
n Memo
m Expr
e  =  case Expr -> Memo -> Maybe (Maybe Dynamic)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
e Memo
m of
    Just Maybe Dynamic
Nothing -> String -> Maybe (Int, Memo, Dynamic)
forall a. HasCallStack => String -> a
error (String -> Maybe (Int, Memo, Dynamic))
-> String -> Maybe (Int, Memo, Dynamic)
forall a b. (a -> b) -> a -> b
$ String
"toDynamicWithDefn: loop detected " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e
    Just (Just Dynamic
d) -> (Int, Memo, Dynamic) -> Maybe (Int, Memo, Dynamic)
forall a. a -> Maybe a
Just (Int
n,Memo
m,Dynamic
d)
    Maybe (Maybe Dynamic)
Nothing -> case [Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n ((Expr
e,Maybe Dynamic
forall a. Maybe a
Nothing)(Expr, Maybe Dynamic) -> Memo -> Memo
forall a. a -> [a] -> [a]
:Memo
m) (Expr -> Maybe (Int, Memo, Dynamic))
-> Expr -> Maybe (Int, Memo, Dynamic)
forall a b. (a -> b) -> a -> b
$ Expr
e' Expr -> Defn -> Expr
//- Defn
bs | (Expr
a',Expr
e') <- Defn
cx, Just Defn
bs <- [Expr
e Expr -> Expr -> Maybe Defn
`match` Expr
a']] of
               [] -> String -> Maybe (Int, Memo, Dynamic)
forall a. HasCallStack => String -> a
error (String -> Maybe (Int, Memo, Dynamic))
-> String -> Maybe (Int, Memo, Dynamic)
forall a b. (a -> b) -> a -> b
$ String
"toDynamicWithDefn: unhandled pattern " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e
               (Maybe (Int, Memo, Dynamic)
Nothing:[Maybe (Int, Memo, Dynamic)]
_) -> Maybe (Int, Memo, Dynamic)
forall a. Maybe a
Nothing
               (Just (Int
n,Memo
m,Dynamic
d):[Maybe (Int, Memo, Dynamic)]
_) -> (Int, Memo, Dynamic) -> Maybe (Int, Memo, Dynamic)
forall a. a -> Maybe a
Just (Int
n,[(Expr
e',if Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e' then Dynamic -> Maybe Dynamic
forall a. a -> Maybe a
Just Dynamic
d else Maybe Dynamic
md) | (Expr
e',Maybe Dynamic
md) <- Memo
m],Dynamic
d)

  ($$) :: Maybe (Int,Memo,Dynamic) -> Expr -> Maybe (Int, Memo, Dynamic)
  Just (Int
n,Memo
m,Dynamic
d1) $$ :: Maybe (Int, Memo, Dynamic) -> Expr -> Maybe (Int, Memo, Dynamic)
$$ Expr
e2  =  case Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re Int
n Memo
m Expr
e2 of
                          Maybe (Int, Memo, Dynamic)
Nothing -> Maybe (Int, Memo, Dynamic)
forall a. Maybe a
Nothing
                          Just (Int
n', Memo
m', Dynamic
d2) -> (Int
n',Memo
m',) (Dynamic -> (Int, Memo, Dynamic))
-> Maybe Dynamic -> Maybe (Int, Memo, Dynamic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dynamic -> Dynamic -> Maybe Dynamic
dynApply Dynamic
d1 Dynamic
d2
  Maybe (Int, Memo, Dynamic)
_ $$ Expr
_               =  Maybe (Int, Memo, Dynamic)
forall a. Maybe a
Nothing

-- | Evaluates an 'Expr' expression into 'Just' a regular Haskell value
--   using a 'Defn' definition when it is found.
--   If there's a type-mismatch, this function returns 'Nothing'.
--
-- This function requires a 'Expr'-deep-reencoding function
-- and a limit to the number of recursive evaluations.
--
-- (cf. 'toDynamicWithDefn', 'deval', 'devl')
devaluate :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
devaluate :: forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
devaluate Expr -> Expr
ee Int
n Defn
fxpr Expr
e  =  (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic
toDynamicWithDefn Expr -> Expr
ee Int
n Defn
fxpr Expr
e Maybe Dynamic -> (Dynamic -> Maybe a) -> Maybe a
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Dynamic -> Maybe a
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic

-- | Evaluates an 'Expr' expression into a regular Haskell value
--   using a 'Defn' definition when it is found in the given expression.
--   If there's a type-mismatch, this function return a default value.
--
-- This function requires a 'Expr'-deep-reencoding function
-- and a limit to the number of recursive evaluations.
--
-- (cf. 'toDynamicWithDefn', 'devaluate', devl')
deval :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
deval :: forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
deval Expr -> Expr
ee Int
n Defn
fxpr a
x  =  a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
x (Maybe a -> a) -> (Expr -> Maybe a) -> Expr -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a
devaluate Expr -> Expr
ee Int
n Defn
fxpr

-- | Like 'deval' but only works for when the given 'Defn' definition
--   has no case breakdowns.
--
-- In other words, this only works when the given 'Defn' is a singleton list
-- whose first value of the only element is a simple application without
-- constructors.
devalFast :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
devalFast :: forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
devalFast Expr -> Expr
_ Int
n [Bndn
defn] a
x  =  Bndn -> Int -> a -> Expr -> a
forall a. Typeable a => Bndn -> Int -> a -> Expr -> a
reval Bndn
defn Int
n a
x

-- | Evaluates an 'Expr' expression into a regular Haskell value
--   using a 'Defn' definition when it is found in the given expression.
--   If there's a type-mismatch, this raises an error.
--
-- This function requires a 'Expr'-deep-reencoding function
-- and a limit to the number of recursive evaluations.
--
-- (cf. 'toDynamicWithDefn', 'devaluate', deval')
devl :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> a
devl :: forall a. Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> a
devl Expr -> Expr
ee Int
n Defn
fxpr  =  (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
deval Expr -> Expr
ee Int
n Defn
fxpr (String -> a
forall a. HasCallStack => String -> a
error String
"devl: incorrect type?")

-- | Returns whether the given definition 'apparentlyTerminates'.
defnApparentlyTerminates :: Defn -> Bool
defnApparentlyTerminates :: Defn -> Bool
defnApparentlyTerminates [(Expr
efxs, Expr
e)]  =  Expr -> Expr -> Bool
apparentlyTerminates Expr
efxs Expr
e
defnApparentlyTerminates Defn
_  =  Bool
True

-- | 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
--                 || 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

-- | 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 definition is complete,
--   i.e., whether it does not have any holes in the RHS.
isCompleteDefn :: Defn -> Bool
isCompleteDefn :: Defn -> Bool
isCompleteDefn  =  (Bndn -> Bool) -> Defn -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Bndn -> Bool
isCompleteBndn

-- | Returns whether the binding is complete,
--   i.e., whether it does not have any holes in the RHS.
isCompleteBndn :: Bndn -> Bool
isCompleteBndn :: Bndn -> Bool
isCompleteBndn (Expr
_,Expr
rhs)  =  Expr -> Bool
isComplete Expr
rhs

-- | 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

canonicalizeBndn :: Bndn -> Bndn
canonicalizeBndn :: Bndn -> Bndn
canonicalizeBndn  =  Expr -> Bndn
unfoldPair (Expr -> Bndn) -> (Bndn -> Expr) -> Bndn -> Bndn
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
canonicalize (Expr -> Expr) -> (Bndn -> Expr) -> Bndn -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bndn -> Expr
foldPair

canonicalizeBndnLast :: Int -> Bndn -> Bndn
canonicalizeBndnLast :: Int -> Bndn -> Bndn
canonicalizeBndnLast Int
i (Expr
lhs,Expr
rhs)  =  (Int -> (Expr -> Expr) -> Expr -> Expr
updateAppAt Int
i (Expr -> Expr -> Expr
forall a b. a -> b -> a
const Expr
ex') Expr
lhs', Expr
rhs')
  where
  (Expr
lhs_, Expr
ex)  =  Int -> Expr -> Bndn
extractApp Int
i Expr
lhs
  (Expr
lhs', Expr
ex', Expr
rhs')  =  Expr -> (Expr, Expr, Expr)
unfoldTrio (Expr -> (Expr, Expr, Expr))
-> ((Expr, Expr, Expr) -> Expr)
-> (Expr, Expr, Expr)
-> (Expr, Expr, Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
canonicalize (Expr -> Expr)
-> ((Expr, Expr, Expr) -> Expr) -> (Expr, Expr, Expr) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr, Expr) -> Expr
foldTrio ((Expr, Expr, Expr) -> (Expr, Expr, Expr))
-> (Expr, Expr, Expr) -> (Expr, Expr, Expr)
forall a b. (a -> b) -> a -> b
$ (Expr
lhs_, Expr
ex, Expr
rhs)

-- | Returns whether a binding has undefined variables,
--   i.e.,
--   there are variables in the RHS that are not declared in the LHS.
--
-- > > hasUnbound (xx -:- xxs, xxs)
-- > False
--
-- > > hasUnbound (xx -:- xxs, yys)
-- > True
--
-- For 'Defn's, use 'isUndefined'.
hasUnbound :: Bndn -> Bool
hasUnbound :: Bndn -> Bool
hasUnbound  =  Bool -> Bool
not (Bool -> Bool) -> (Bndn -> Bool) -> Bndn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bndn -> Bool
noUnbound

noUnbound :: Bndn -> Bool
noUnbound :: Bndn -> Bool
noUnbound (Expr
lhs,Expr
rhs)  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Expr]
nubVars Expr
lhs) (Expr -> [Expr]
vars Expr
rhs)

-- | Returns whether a 'Defn' has undefined variables,
--   i.e.,
--   there are variables in the RHSs that are not declared in the LHSs.
--
-- > > isUndefined [(nil, nil), (xx -:- xxs, xxs)]
-- > False
--
-- > > isUndefined [(nil, xxs), (xx -:- xxs, yys)]
-- > True
--
-- For single 'Bndn's, use 'hasUnbound'.
isUndefined :: Defn -> Bool
isUndefined :: Defn -> Bool
isUndefined  =  (Bndn -> Bool) -> Defn -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bndn -> Bool
hasUnbound

isDefined :: Defn -> Bool
isDefined :: Defn -> Bool
isDefined  =  Bool -> Bool
not (Bool -> Bool) -> (Defn -> Bool) -> Defn -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Bool
isUndefined

-- | Returns whether a binding is a base case.
--
-- > > isBaseCase (ff (xx -:- nil), xx)
-- > True
--
-- > > isBaseCase (ff (xx -:- xxs), ff xxs)
-- > False
--
-- (cf. 'isRecursiveCase')
isBaseCase :: Bndn -> Bool
isBaseCase :: Bndn -> Bool
isBaseCase (Expr
lhs,Expr
rhs)  =  Expr
f Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Expr -> [Expr]
values Expr
rhs
  where
  (Expr
f:[Expr]
_)  =  Expr -> [Expr]
unfoldApp Expr
lhs

-- | Returns whether a binding is a base case.
--
-- > > isRecursiveCase (ff (xx -:- nil), xx)
-- > False
--
-- > > isRecursiveCase (ff (xx -:- xxs), ff xxs)
-- > True
--
-- (cf. 'isBaseCase')
isRecursiveCase :: Bndn -> Bool
isRecursiveCase :: Bndn -> Bool
isRecursiveCase (Expr
lhs,Expr
rhs)  =  Expr
f Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Expr]
values Expr
rhs
  where
  (Expr
f:[Expr]
_)  =  Expr -> [Expr]
unfoldApp Expr
lhs

-- | Returns whether a definition is recursive
isRecursiveDefn :: Defn -> Bool
isRecursiveDefn :: Defn -> Bool
isRecursiveDefn  =  (Bndn -> Bool) -> Defn -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bndn -> Bool
isRecursiveCase