-- |
-- Module      : Conjure.Red
-- 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 defines functions that deal with recursive descent and deconstructions
module Conjure.Red
  ( conjureIsDeconstruction
  , descends
  , candidateDeconstructionsFrom
  , candidateDeconstructionsFromHoled
  )
where

import Conjure.Defn
import Conjure.Conjurable
import Test.LeanCheck.Error (errorToFalse)

-- | Checks if an expression is a deconstruction.
--
-- There should be a single 'hole' in the expression.
--
-- It should decrease the size of all arguments that have
-- a size greater than 0.
conjureIsDeconstruction :: Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstruction :: forall f. Conjurable f => f -> Int -> Expr -> Bool
conjureIsDeconstruction f
f Int
maxTests Expr
ed
  =  [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Expr -> [Expr]
holes Expr
ed) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1  -- Well formed deconstruction, single hole.
  Bool -> Bool -> Bool
&& Expr -> TypeRep
typ Expr
h TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
ed         -- We can only deconstruct to the same type.
  Bool -> Bool -> Bool
&& ((Int, Int) -> Bool) -> [(Int, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int, Int) -> Bool
forall {a}. (Num a, Ord a) => (a, a) -> Bool
is [(Int, Int)]
sizes            -- Do we always reduce size?
  Bool -> Bool -> Bool
&& Bool -> Bool
not (((Int, Int) -> Bool) -> [(Int, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int, Int) -> Bool
forall {a} {a}. (Eq a, Eq a, Num a, Num a) => (a, a) -> Bool
iz [(Int, Int)]
sizes)      -- Disallow always mapping to values of size 0.
                             -- In this case, we are better off not recursing
                             -- and returning a constant value!
  where
  a
x << :: a -> a -> Bool
<< a
0  =  Bool
True
  a
x << a
y  =  a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
y
  is :: (a, a) -> Bool
is (a
sd,a
sx)  =  Bool -> Bool
errorToFalse (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a
sd a -> a -> Bool
forall {a}. (Num a, Ord a) => a -> a -> Bool
<< a
sx
  iz :: (a, a) -> Bool
iz (a
sd,a
sx)  =  Bool -> Bool
errorToFalse (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a
sd a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 Bool -> Bool -> Bool
|| a
sx a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0
  -- We cannot simply conjureTiers for h here, because the deconstruction
  -- expression may contain variables, e.g.: @x `mod` _@.
  -- So conjureGrounds and the holeValue trick are required.
  sizes :: [(Int, Int)]
sizes  =  (Expr -> (Int, Int)) -> [Expr] -> [(Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> (Int, Int)
evalSize2 ([Expr] -> [(Int, Int)])
-> ([Expr] -> [Expr]) -> [Expr] -> [(Int, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
take Int
maxTests ([Expr] -> [(Int, Int)]) -> [Expr] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ f -> Expr -> [Expr]
forall f. Conjurable f => f -> Expr -> [Expr]
conjureGrounds f
f Expr
ed
  [Expr
h]  =  Expr -> [Expr]
holes Expr
ed
  evalSize2 :: Expr -> (Int, Int)
evalSize2 Expr
e  =  (Expr -> Int
evalSize Expr
e, Expr -> Int
evalSize (Expr -> Int) -> Expr -> Int
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
holeValue Expr
e)
  evalSize :: Expr -> Int
evalSize Expr
e  =  Int -> Expr -> Int
forall a. Typeable a => a -> Expr -> a
eval (Int
0::Int) (Expr
esize Expr -> Expr -> Expr
:$ Expr
e)
  esize :: Expr
esize  =  f -> Expr -> Expr
forall f. Conjurable f => f -> Expr -> Expr
conjureSizeFor f
f Expr
h
  holeValue :: Expr -> Expr
holeValue Expr
e  =  Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe Expr
forall {a}. a
err (Maybe Expr -> Expr)
-> (Maybe [(Expr, Expr)] -> Maybe Expr)
-> Maybe [(Expr, Expr)]
-> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [(Expr, Expr)] -> Maybe Expr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Expr
h ([(Expr, Expr)] -> Maybe Expr)
-> (Maybe [(Expr, Expr)] -> [(Expr, Expr)])
-> Maybe [(Expr, Expr)]
-> Maybe Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Expr, Expr)] -> Maybe [(Expr, Expr)] -> [(Expr, Expr)]
forall a. a -> Maybe a -> a
fromMaybe [(Expr, Expr)]
forall {a}. a
err (Maybe [(Expr, Expr)] -> Expr) -> Maybe [(Expr, Expr)] -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e Expr -> Expr -> Maybe [(Expr, Expr)]
`match` Expr
ed
  err :: a
err  =  [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"Conjure.conjureIsDeconstruction: the impossible happened"

-- | Returns whether a non-empty subset of arguments
--   descends arguments by deconstruction.
--
-- > > descends isDec (xxs -++- yys) (xxs -++- tail' yys)
-- > True
--
-- > > descends isDec (xxs -++- yys) (xxs -++- yys)
-- > False
--
-- > > descends isDec (xxs -++- yys) (head' xxs -:- tail xxs  -++-  head' yys -:- tail yys)
-- > False

-- > > descends isDec (xxs -\/- yys) (yys -\/- tail' xxs)
-- > True
--
-- The following are not so obvious:
--
-- > > descends isDec (xxs -++- yys) (tail' yys -++- yys)
-- > False
--
-- > > descends isDec (xxs -++- yys) (xx-:-xxs -++- tail' yys)
-- > True
--
-- For all possible sets of arguments (2^n - 1 elements: 1 3 7 15 31),
-- see if any projects the same variables while only using deconstructions
-- and where there is at least a single deconstruction.
descends :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
descends :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool
descends Expr -> Expr -> Bool
isDecOf Expr
efls Expr
efrs  =  ([(Expr, Expr)] -> Bool) -> [[(Expr, Expr)]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any [(Expr, Expr)] -> Bool
hasDeconstruction
                            ([[(Expr, Expr)]] -> Bool) -> [[(Expr, Expr)]] -> Bool
forall a b. (a -> b) -> a -> b
$  ((Expr, Expr) -> TypeRep) -> [(Expr, Expr)] -> [[(Expr, Expr)]]
forall b a. Eq b => (a -> b) -> [a] -> [[a]]
classifyOn (Expr -> TypeRep
typ (Expr -> TypeRep)
-> ((Expr, Expr) -> Expr) -> (Expr, Expr) -> TypeRep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, Expr) -> Expr
forall a b. (a, b) -> a
fst) ([Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
ls [Expr]
rs)
  where
  (Expr
_:[Expr]
ls)  =  Expr -> [Expr]
unfoldApp Expr
efls
  (Expr
_:[Expr]
rs)  =  Expr -> [Expr]
unfoldApp Expr
efrs

  hasDeconstruction :: [(Expr,Expr)] -> Bool
  hasDeconstruction :: [(Expr, Expr)] -> Bool
hasDeconstruction [(Expr, Expr)]
lrs  =  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [(Expr, Expr)
b (Expr, Expr) -> [(Expr, Expr)] -> Bool
*<< [(Expr, Expr)]
bs | ((Expr, Expr)
b,[(Expr, Expr)]
bs) <- [(Expr, Expr)] -> [((Expr, Expr), [(Expr, Expr)])]
forall a. [a] -> [(a, [a])]
choices [(Expr, Expr)]
lrs]

  Expr
r << :: Expr -> Expr -> Bool
<< Expr
l  =  (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr
r Expr -> Expr -> Bool
`isDecOf`) (Expr -> [Expr]
rvars Expr
l)
          Bool -> Bool -> Bool
|| Expr
r Expr -> Expr -> Bool
`isStrictSubexprOf` Expr
l
          Bool -> Bool -> Bool
|| Expr -> Bool
isGround Expr
r Bool -> Bool -> Bool
&& Bool -> Bool
not (Expr -> Bool
isGround Expr
l) Bool -> Bool -> Bool
&& Expr -> Int
size Expr
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Expr -> Int
size Expr
l

  Expr
r <<= :: Expr -> Expr -> Bool
<<= Expr
l  =  Expr
r Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
l
           Bool -> Bool -> Bool
|| Expr
r Expr -> Expr -> Bool
<< Expr
l

  (Expr
l,Expr
r) *<< :: (Expr, Expr) -> [(Expr, Expr)] -> Bool
*<< [(Expr, Expr)]
bs  =  Expr
r Expr -> Expr -> Bool
<< Expr
l
                Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ (Expr
l',Expr
r) (Expr, Expr) -> [(Expr, Expr)] -> Bool
*<<= [(Expr, Expr)]
bs'
                      | ((Expr
l',Expr
r'),[(Expr, Expr)]
bs') <- [(Expr, Expr)] -> [((Expr, Expr), [(Expr, Expr)])]
forall a. [a] -> [(a, [a])]
choices [(Expr, Expr)]
bs
                      , Expr
r' Expr -> Expr -> Bool
<< Expr
l
                      ]

  (Expr
l,Expr
r) *<<= :: (Expr, Expr) -> [(Expr, Expr)] -> Bool
*<<= [(Expr, Expr)]
bs  =  Expr
r Expr -> Expr -> Bool
<<= Expr
l
                 Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ (Expr
l',Expr
r) (Expr, Expr) -> [(Expr, Expr)] -> Bool
*<<= [(Expr, Expr)]
bs'
                       | ((Expr
l',Expr
r'),[(Expr, Expr)]
bs') <- [(Expr, Expr)] -> [((Expr, Expr), [(Expr, Expr)])]
forall a. [a] -> [(a, [a])]
choices [(Expr, Expr)]
bs
                       , Expr
r' Expr -> Expr -> Bool
<<= Expr
l
                       ]

-- | Compute candidate deconstructions from an 'Expr'.
--
-- This is used in the implementation of 'Conjure.Engine.candidateDefnsC'
-- followed by 'conjureIsDeconstruction'.
--
-- > > candidateDeconstructionsFrom (xx `mod'` yy)
-- > [ _ `mod` y
-- > , x `mod` _
-- > ]
--
-- To be constrasted with 'candidateDeconstructionsFromHoled'.
candidateDeconstructionsFrom :: Expr -> [Expr]
candidateDeconstructionsFrom :: Expr -> [Expr]
candidateDeconstructionsFrom Expr
e  =
  [ Expr
e'
  | Expr
v <- Expr -> [Expr]
vars Expr
e
  , Expr -> TypeRep
typ Expr
v TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
e
  , let e' :: Expr
e' = Expr
e Expr -> [(Expr, Expr)] -> Expr
//- [(Expr
v, Expr -> Expr
holeAsTypeOf Expr
v)]
  , [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Expr -> [Expr]
holes Expr
e') Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
  ]

-- | Compute candidate deconstructions from an 'Expr'.
--
-- This is used in the implementation of 'Conjure.Engine.candidateExprs'
-- followed by 'conjureIsDeconstruction'.
--
-- This is similar to 'canonicalVariations'
-- but always leaves a hole
-- of the same return type as the given expression.
--
-- > > candidateDeconstructionsFrom (i_ `mod'` i_)
-- > [ _ `mod` x
-- > , x `mod` _
-- > ]
--
-- To be contrasted with 'candidateDeconstructionsFrom'
candidateDeconstructionsFromHoled :: Expr -> [Expr]
candidateDeconstructionsFromHoled :: Expr -> [Expr]
candidateDeconstructionsFromHoled Expr
e  =  (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> [(Expr, Expr)] -> Expr
//- [(Expr
v, Expr
h)])
                                     ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$  (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
canonicalVariations
                                     ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$  Expr -> Expr -> [Expr]
deholings Expr
v Expr
e
  where
  h :: Expr
h  =  Expr -> Expr
holeAsTypeOf Expr
e
  v :: Expr
v  =  [Char]
"_#_" [Char] -> Expr -> Expr
`varAsTypeOf` Expr
e  -- a marker variable with an invalid name
  -- at some point I should get rid of candidateDeconstructionsFrom in favour
  -- of this one