-- |
-- Module      : Conjure.Expr
-- Copyright   : (c) 2021 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This internal module reexports 'Data.Express' along with a few other
-- utilities.
{-# LANGUAGE CPP #-}
module Conjure.Expr
  ( module Data.Express
  , module Data.Express.Fixtures

  , (>$$<)
  , funToVar
  , recursexpr
  , apparentlyTerminates
  , mayNotEvaluateArgument
  , applicationOld
  , compareSimplicity
  , ifFor
  , primitiveHoles
  , primitiveApplications
  , valuesBFS
  , holesBFS
  , fillBFS
  , showEq
  , lhs
  , rhs
  , ($$**)
  , ($$|<)

  , module Conjure.Utils
  )
where

import Conjure.Utils

import Data.Express
import Data.Express.Utils.Typeable
import Data.Express.Fixtures hiding ((-==-))

-- | /O(n)/.
-- Compares the simplicity of two 'Expr's.
-- An expression /e1/ is /strictly simpler/ than another expression /e2/
-- if the first of the following conditions to distingish between them is:
--
-- 1. /e1/ is smaller in size\/length than /e2/,
--    e.g.: @x + y < x + (y + z)@;
--
-- 2. or, /e1/ has less variable occurrences than /e2/,
--
-- 3. or, /e1/ has fewer distinct constants than /e2/,
--    e.g.: @1 + 1 < 0 + 1@.
--
-- They're otherwise considered of equal complexity,
-- e.g.: @x + y@ and @y + z@.
--
-- > > (xx -+- yy) `compareComplexity` (xx -+- (yy -+- zz))
-- > LT
--
-- > > (xx -+- yy) `compareComplexity` (xx -+- xx)
-- > EQ
--
-- > > (xx -+- xx) `compareComplexity` (one -+- xx)
-- > GT
--
-- > > (one -+- one) `compareComplexity` (zero -+- one)
-- > LT
--
-- > > (xx -+- yy) `compareComplexity` (yy -+- zz)
-- > EQ
--
-- > > (zero -+- one) `compareComplexity` (one -+- zero)
-- > EQ
compareSimplicity :: Expr -> Expr -> Ordering
compareSimplicity :: Expr -> Expr -> Ordering
compareSimplicity  =  (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Expr -> Int) -> Expr -> Expr -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> (Expr -> [Expr]) -> Expr -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
values)
                   (Expr -> Expr -> Ordering)
-> (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering
forall a. Semigroup a => a -> a -> a
<> (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Expr -> Int) -> Expr -> Expr -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> (Expr -> [Expr]) -> Expr -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
vars)
                   (Expr -> Expr -> Ordering)
-> (Expr -> Expr -> Ordering) -> Expr -> Expr -> Ordering
forall a. Semigroup a => a -> a -> a
<> (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> (Expr -> Int) -> Expr -> Expr -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> (Expr -> [Expr]) -> Expr -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
nubConsts)

-- | Makes the function in an application a variable
funToVar :: Expr -> Expr
funToVar :: Expr -> Expr
funToVar (Expr
ef :$ Expr
ex)  =  Expr -> Expr
funToVar Expr
ef Expr -> Expr -> Expr
:$ Expr
ex
funToVar ef :: Expr
ef@(Value String
nm Dynamic
_)  =  String
nm String -> Expr -> Expr
`varAsTypeOf` Expr
ef

-- | Expands recursive calls on an expression
--   until the given size limit is reached.
--
-- > > recursexpr 6 (ff xx) (ff xx)
-- > f x :: Int
--
-- > > recursexpr 6 (ff xx) (one -+- ff xx)
-- > 1 + (1 + (1 + (1 + f x))) :: Int
--
-- > > recursexpr 6 (ff xx) (if' pp one (xx -*- ff xx))
-- > (if p then 1 else x * (if p then 1 else x * f x)) :: Int
--
-- > > recursexpr 6 (ff xx) (if' pp one (xx -*- ff (gg xx)))
-- > (if p then 1 else x * (if p then 1 else g x * f (g (g x)))) :: Int
recursexpr :: Int -> Expr -> Expr -> Expr
recursexpr :: Int -> Expr -> Expr -> Expr
recursexpr Int
sz Expr
epat  =  Expr -> Expr
re
  where
  err :: a
err  =  String -> a
forall a. HasCallStack => String -> a
error String
"recursexpr: pattern must contain an application of variables"
  (Expr
erf:[Expr]
vs)  =  Expr -> [Expr]
unfoldApp Expr
epat
  re :: Expr -> Expr
re Expr
e' | Bool -> Bool
not ((Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isVar (Expr
erfExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
vs))  =  Expr
forall a. a
err
        | Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e' Bool -> Bool -> Bool
|| Expr -> Int
size Expr
e Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
sz    =  Expr
e
        | Bool
otherwise                 =  Expr -> Expr
re Expr
e
    where
    e :: Expr
e  =  Expr -> Expr
re1 Expr
e'
    re1 :: Expr -> Expr
re1 Expr
e  =  case Expr -> [Expr]
unfoldApp Expr
e of
              [Expr
e]                  -> Expr
e
              (Expr
ef:[Expr]
exs) | Expr
ef Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
erf -> Expr
e' Expr -> [(Expr, Expr)] -> Expr
//- [Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
vs [Expr]
exs
                       | Bool
otherwise -> [Expr] -> Expr
foldApp ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
re1 (Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
exs))

-- recursive call _only_ under an if
-- future-work: guess short-circuit operators

-- | Checks if the given recursive call apparently terminates.
--   The first argument indicates the functional variable indicating the
--   recursive call.
--
-- > > apparentlyTerminates ffE (ff xx)
-- > False
--
-- > > apparentlyTerminates ffE (if' pp zero (ff xx))
-- > True
--
-- This function only allows recursion in the else clause:
--
-- > > apparentlyTerminates ffE (if' pp (ff xx) zero)
-- > False
--
-- Of course, recursive calls as the condition are not allowed:
--
-- > > apparentlyTerminates ffE (if' (odd' (ff xx)) zero zero)
-- > False
apparentlyTerminates :: Expr -> Expr -> Bool
apparentlyTerminates :: Expr -> Expr -> Bool
apparentlyTerminates Expr
eRecursiveCall  =  Expr -> Bool
at
  where
  at :: Expr -> Bool
at (Expr
e1 :$ Expr
e2)  =  (Expr -> Bool
mayNotEvaluateArgument Expr
e1 Bool -> Bool -> Bool
|| Expr -> Bool
at Expr
e2) Bool -> Bool -> Bool
&& Expr -> Bool
at Expr
e1
  at Expr
e  =  Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
eRecursiveCall

-- | Checks if the given functional expression may refrain from evaluating its
--   next argument.
--
--
-- > > mayNotEvaluateArgument (plus :$ xx)
-- > False
--
-- > > mayNotEvaluateArgument (andE :$ pp)
-- > True
--
-- This returns false for non-funcional value even if it involves an
-- application which may not evaluate its argument.
--
-- > > mayNotEvaluateArgument (andE :$ pp :$ qq)
-- > False
--
-- This currently works by checking if the function is an if, '&&' or '||'.
mayNotEvaluateArgument :: Expr -> Bool
mayNotEvaluateArgument :: Expr -> Bool
mayNotEvaluateArgument (Value String
"if" Dynamic
ce :$ Expr
_ :$ Expr
_)  =  Bool
True
mayNotEvaluateArgument (Value String
"&&" Dynamic
ce :$ Expr
_)       =  Bool
True
mayNotEvaluateArgument (Value String
"||" Dynamic
ce :$ Expr
_)       =  Bool
True
mayNotEvaluateArgument Expr
_                          =  Bool
False

applicationOld :: Expr -> [Expr] -> Maybe Expr
applicationOld :: Expr -> [Expr] -> Maybe Expr
applicationOld Expr
ff [Expr]
es  =  Expr -> Maybe Expr
appn Expr
ff
  where
  appn :: Expr -> Maybe Expr
appn Expr
ff
    | Expr -> Bool
isFun Expr
ff   =  case [Expr
e | Just (Expr
_ :$ Expr
e) <- ((Expr -> Maybe Expr) -> [Expr] -> [Maybe Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr
ff Expr -> Expr -> Maybe Expr
$$)) [Expr]
es] of
                    [] -> Maybe Expr
forall a. Maybe a
Nothing  -- could not find type representative in es
                    (Expr
e:[Expr]
_) -> Expr -> Maybe Expr
appn (Expr
ff Expr -> Expr -> Expr
:$ Expr -> Expr
holeAsTypeOf Expr
e)
    | Bool
otherwise  =  Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
ff

-- | Creates an if 'Expr' of the type of the given proxy.
--
-- > > ifFor (undefined :: Int)
-- > if :: Bool -> Int -> Int -> Int
--
-- > > ifFor (undefined :: String)
-- > if :: Bool -> [Char] -> [Char] -> [Char]
--
-- You need to provide this as part of your building blocks on the primitives
-- if you want recursive functions to be considered and produced.
ifFor :: Typeable a => a -> Expr
ifFor :: a -> Expr
ifFor a
a  =  String -> (Bool -> a -> a -> a) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"if" (\Bool
p a
x a
y -> if Bool
p then a
x else a
y a -> a -> a
forall a. a -> a -> a
`asTypeOf` a
a)

-- | Application cross-product between lists of Exprs
(>$$<) :: [Expr] -> [Expr] -> [Expr]
[Expr]
exs >$$< :: [Expr] -> [Expr] -> [Expr]
>$$< [Expr]
eys  =  [Maybe Expr] -> [Expr]
forall a. [Maybe a] -> [a]
catMaybes [Expr
ex Expr -> Expr -> Maybe Expr
$$ Expr
ey | Expr
ex <- [Expr]
exs, Expr
ey <- [Expr]
eys]
-- TODO: move >$$< into Data.Express?

primitiveHoles :: [Expr] -> [Expr]
primitiveHoles :: [Expr] -> [Expr]
primitiveHoles [Expr]
prims  =  [Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
sort ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr] -> [Expr]
ph [Expr]
hs
  where
  hs :: [Expr]
hs  =  [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
holeAsTypeOf [Expr]
prims
  ph :: [Expr] -> [Expr]
ph  =  ([Expr] -> [Expr] -> Bool)
-> ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a. (a -> a -> Bool) -> (a -> a) -> a -> a
iterateUntil [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
(==) [Expr] -> [Expr]
ps
  ps :: [Expr] -> [Expr]
ps [Expr]
es  =  [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr] -> [Expr]
sq [Expr]
es
  sq :: [Expr] -> [Expr]
sq [Expr]
es  =  [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
nub ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
holeAsTypeOf ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr]
es [Expr] -> [Expr] -> [Expr]
>$$< [Expr]
es
-- FIXME: the function above is quite inefficient.
--        Should run fast for a small number of types,
--        but if this number increases runtime may start
--        to become significant.

primitiveApplications :: [Expr] -> [[Expr]]
primitiveApplications :: [Expr] -> [[Expr]]
primitiveApplications [Expr]
prims  =  ([Expr] -> Bool) -> [[Expr]] -> [[Expr]]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool) -> ([Expr] -> Bool) -> [Expr] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null)
                             ([[Expr]] -> [[Expr]]) -> [[Expr]] -> [[Expr]]
forall a b. (a -> b) -> a -> b
$  ([Expr] -> [Expr]) -> [Expr] -> [[Expr]]
forall a. (a -> a) -> a -> [a]
iterate ([Expr] -> [Expr] -> [Expr]
>$$< [Expr] -> [Expr]
primitiveHoles [Expr]
prims) [Expr]
prims

-- lists terminal values in BFS order
valuesBFS :: Expr -> [Expr]
valuesBFS :: Expr -> [Expr]
valuesBFS  =  [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Expr]] -> [Expr]) -> (Expr -> [[Expr]]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [[Expr]]
bfs
  where
  bfs :: Expr -> [[Expr]]
  bfs :: Expr -> [[Expr]]
bfs (Expr
ef :$ Expr
ex)  =  [] [Expr] -> [[Expr]] -> [[Expr]]
forall a. a -> [a] -> [a]
: [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. Monoid a => [a] -> [a] -> [a]
mzip (Expr -> [[Expr]]
bfs Expr
ef) (Expr -> [[Expr]]
bfs Expr
ex)
  bfs Expr
e  =  [[Expr
e]]

-- lists holes in BFS order
holesBFS :: Expr -> [Expr]
holesBFS :: Expr -> [Expr]
holesBFS  =  (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter Expr -> Bool
isHole ([Expr] -> [Expr]) -> (Expr -> [Expr]) -> Expr -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
valuesBFS

fillBFS :: Expr -> Expr -> Expr
fillBFS :: Expr -> Expr -> Expr
fillBFS Expr
e Expr
e'  =  (Expr, Maybe Int) -> Expr
forall a b. (a, b) -> a
fst (Expr -> (Expr, Maybe Int)
f Expr
e)
  where
  f :: Expr -> (Expr,Maybe Int)
  f :: Expr -> (Expr, Maybe Int)
f (Expr
ef :$ Expr
ex)  =  case (Maybe Int
mf, Maybe Int
mx) of
    (Maybe Int
Nothing, Maybe Int
Nothing)             -> (Expr
ef Expr -> Expr -> Expr
:$ Expr
ex, Maybe Int
forall a. Maybe a
Nothing)
    (Just Int
lf, Maybe Int
Nothing)             -> (Expr
ef' Expr -> Expr -> Expr
:$ Expr
ex, Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
lfInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
    (Maybe Int
Nothing, Just Int
lx)             -> (Expr
ef Expr -> Expr -> Expr
:$ Expr
ex', Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
lxInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
    (Just Int
lf, Just Int
lx) | Int
lf Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
lx  -> (Expr
ef' Expr -> Expr -> Expr
:$ Expr
ex, Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
lfInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
                       | Bool
otherwise -> (Expr
ef Expr -> Expr -> Expr
:$ Expr
ex', Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
lxInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
    where
    (Expr
ef', Maybe Int
mf)  =  Expr -> (Expr, Maybe Int)
f Expr
ef
    (Expr
ex', Maybe Int
mx)  =  Expr -> (Expr, Maybe Int)
f Expr
ex
  f Expr
e | Expr -> Bool
isHole Expr
e Bool -> Bool -> Bool
&& Expr -> TypeRep
typ Expr
e TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
e'  =  (Expr
e', Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0)
      | Bool
otherwise                    =  (Expr
e, Maybe Int
forall a. Maybe a
Nothing)
-- TODO: move BFS functions into Express?

showEq :: Expr -> String
showEq :: Expr -> String
showEq (((Value String
"==" Dynamic
_) :$ 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
showEq Expr
e  =  String
"not an Eq: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
e

lhs, rhs :: Expr -> Expr
lhs :: Expr -> Expr
lhs (((Value String
"==" Dynamic
_) :$ Expr
e) :$ Expr
_)  =  Expr
e
rhs :: Expr -> Expr
rhs (((Value String
"==" Dynamic
_) :$ Expr
_) :$ Expr
e)  =  Expr
e

-- Debug: application that always works
($$**) :: Expr -> Expr -> Maybe Expr
Expr
e1 $$** :: Expr -> Expr -> Maybe Expr
$$** Expr
e2  =  Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2

-- Debug: application that works for the correct kinds
($$|<) :: Expr -> Expr -> Maybe Expr
Expr
e1 $$|< :: Expr -> Expr -> Maybe Expr
$$|< Expr
e2  =  if TypeRep -> Bool
isFunTy TypeRep
t1 Bool -> Bool -> Bool
&& TypeRep -> Int
tyArity (TypeRep -> TypeRep
argumentTy TypeRep
t1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== TypeRep -> Int
tyArity TypeRep
t2
               then Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2
               else Maybe Expr
forall a. Maybe a
Nothing
  where
  t1 :: TypeRep
t1  =  Expr -> TypeRep
ktyp Expr
e1
  t2 :: TypeRep
t2  =  Expr -> TypeRep
ktyp Expr
e2

  ktyp :: Expr -> TypeRep
  ktyp :: Expr -> TypeRep
ktyp (Expr
e1 :$ Expr
e2)  =  TypeRep -> TypeRep
resultTy (Expr -> TypeRep
ktyp Expr
e1)
  ktyp Expr
e  =  Expr -> TypeRep
typ Expr
e