-- |
-- 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
  , defnApparentlyTerminates
  , isRedundantDefn
  , 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> String
show1
  where
  show1 :: (Expr, Expr) -> String
show1 (Expr
lhs,Expr
rhs)  =  Expr -> String
showExpr Expr
lhs forall a. [a] -> [a] -> [a]
++ String
"  =  " forall a. [a] -> [a] -> [a]
++ Expr -> String
showExpr Expr
rhs

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  =  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
_,Memo
_,Dynamic
d) -> Dynamic
d) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)
re (Int
mx forall a. Num a => a -> a -> a
* forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Int
size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Defn
cx)) []
  where
  (Expr
ef':[Expr]
_)  =  Expr -> [Expr]
unfoldApp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. [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
_  | forall (t :: * -> *) a. Foldable t => t a -> Int
length Memo
m forall a. Ord a => a -> a -> Bool
> Int
mx  =  forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: recursion limit reached"
  re Int
n Memo
m Expr
_  | Int
n forall a. Ord a => a -> a -> Bool
<= Int
0  =  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 forall a. Typeable a => Int -> Memo -> Expr -> Maybe (Int, Memo, a)
rev Int
n Memo
m Expr
ec of
    Maybe (Int, Memo, Bool)
Nothing    -> 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 forall a. Typeable a => Int -> Memo -> Expr -> Maybe (Int, Memo, a)
rev Int
n Memo
m Expr
ep of
    Maybe (Int, Memo, Bool)
Nothing        -> forall a. Maybe a
Nothing
    Just (Int
n,Memo
m,Bool
True)  -> (Int
n,Memo
m,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic (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 forall a. Typeable a => Int -> Memo -> Expr -> Maybe (Int, Memo, a)
rev Int
n Memo
m Expr
ep of
    Maybe (Int, Memo, Bool)
Nothing    -> 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,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic (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
    [] -> forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: empty application unfold"  -- should never happen
    [Expr
e] -> (Int
nforall a. Num a => a -> a -> a
-Int
1,Memo
m,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Maybe Dynamic
toDynamic Expr
e
    (Expr
ef:[Expr]
exs) | Expr
ef 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
efforall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
exprExpr [Expr]
exs))
             | Bool
otherwise -> 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    -> forall a. Maybe a
Nothing
                Just (Int
n,Memo
m,Dynamic
d) -> case forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
                                Maybe a
Nothing -> forall a. Maybe a
Nothing
                                Just a
x  -> 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 forall a. Ord a => a -> a -> Bool
> Int
n  =  forall a. HasCallStack => String -> a
error String
"toDynamicWithDefn: argument-size limit reached"
  red Int
n Memo
m Expr
e  =  case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
e Memo
m of
    Just Maybe Dynamic
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"toDynamicWithDefn: loop detected " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Expr
e
    Just (Just Dynamic
d) -> 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,forall a. Maybe a
Nothing)forall a. a -> [a] -> [a]
:Memo
m) 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
               [] -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"toDynamicWithDefn: unhandled pattern " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Expr
e
               (Maybe (Int, Memo, Dynamic)
Nothing:[Maybe (Int, Memo, Dynamic)]
_) -> forall a. Maybe a
Nothing
               (Just (Int
n,Memo
m,Dynamic
d):[Maybe (Int, Memo, Dynamic)]
_) -> forall a. a -> Maybe a
Just (Int
n,[(Expr
e',if Expr
e forall a. Eq a => a -> a -> Bool
== Expr
e' then 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 -> forall a. Maybe a
Nothing
                          Just (Int
n', Memo
m', Dynamic
d2) -> (Int
n',Memo
m',) 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
_               =  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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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  =  forall a. a -> Maybe a -> a
fromMaybe a
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 [(Expr, Expr)
defn] a
x  =  forall a. Typeable a => (Expr, Expr) -> Int -> a -> Expr -> a
reval (Expr, Expr)
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  =  forall a.
Typeable a =>
(Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
deval Expr -> Expr
ee Int
n Defn
fxpr (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 its patterns.
--
-- Here is an example of a redundant 'Defn':
--
-- > 0 ? 0  =  0
-- > 0 ? x  =  0
-- > x ? 0  =  x
-- > x ? y  =  x
--
-- It is redundant because it is equivalent to:
--
-- > 0 ? _  =  0
-- > x ? _  =  x
--
-- If the given expression is incomplete ('hasHole')
-- this function returns 'True' as nothing can be said.
isRedundantDefn :: Defn -> Bool
isRedundantDefn :: Defn -> Bool
isRedundantDefn Defn
d  =  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isComplete (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd Defn
d)
                   Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Defn -> Bool
isRedundant1 (Defn -> [Defn]
unfoldDefnArgs Defn
d)
  where
  isRedundant1 :: [(Expr,Expr)] -> Bool
  isRedundant1 :: Defn -> Bool
isRedundant1  =  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Eq a => [a] -> Bool
allEqual
                forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd)
                forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall b a. Eq b => (a -> b) -> [a] -> [[a]]
classifyOn forall a b. (a, b) -> a
fst
                forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a b. (a -> b) -> [a] -> [b]
map (Expr -> (Expr, Expr)
unfoldPair forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
canonicalize forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr) -> Expr
foldPair)

  -- Returns a list of degenerate 'Defn'
  -- whose patterns have been "lensed" on each argument.
  unfoldDefnArgs :: Defn -> [[(Expr,Expr)]]
  unfoldDefnArgs :: Defn -> [Defn]
unfoldDefnArgs  =  forall a. [[a]] -> [[a]]
transpose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Expr, Expr) -> Defn
unfoldBndnArgs
    where
    unfoldBndnArgs :: Bndn -> [(Expr,Expr)]
    unfoldBndnArgs :: (Expr, Expr) -> Defn
unfoldBndnArgs (Expr
p,Expr
r)  =  forall a b. (a -> b) -> [a] -> [b]
map (\Expr
a -> (Expr
a,Expr
r)) [Expr]
as
      where
      (Expr
_:[Expr]
as)  =  Expr -> [Expr]
unfoldApp Expr
p