-- |
-- 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
  , 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 ((-:>)) -- for toDynamicWithDefn

-- | 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
. ((Expr, Expr) -> String) -> Defn -> [String]
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 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  =  " String -> String -> 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  =  ((Int, Memo, Dynamic) -> Dynamic)
-> Maybe (Int, Memo, Dynamic) -> Maybe Dynamic
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 (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (((Expr, Expr) -> Int) -> Defn -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Int
size (Expr -> Int) -> ((Expr, Expr) -> Expr) -> (Expr, Expr) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd) Defn
cx)) []
  where
  (Expr
ef':[Expr]
_)  =  Expr -> [Expr]
unfoldApp (Expr -> [Expr])
-> ((Expr, Expr) -> Expr) -> (Expr, Expr) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr) -> Expr
forall a b. (a, b) -> a
fst ((Expr, Expr) -> [Expr]) -> (Expr, Expr) -> [Expr]
forall a b. (a -> b) -> a -> b
$ Defn -> (Expr, Expr)
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
_  | Memo -> 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 (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 :: 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  =  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 :: (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 (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 :: (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 :: (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a
devalFast Expr -> Expr
_ Int
n [(Expr, Expr)
defn] a
x  =  (Expr, Expr) -> Int -> a -> Expr -> a
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 :: (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