-- |
-- 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, TupleSections #-}
module Conjure.Expr
  ( module Data.Express
  , module Data.Express.Fixtures

  , rehole
  , (>$$<)
  , funToVar
  , recursexpr
  , apparentlyTerminates
  , mayNotEvaluateArgument
  , compareSimplicity
  , ifFor
  , caseForOrd
  , valuesBFS
  , holesBFS
  , fillBFS
  , ($$**)
  , ($$|<)
  , possibleHoles
  , revaluate
  , reval
  , useMatches
  , deholings

  , enumerateAppsFor
  , enumerateFillings

  , module Conjure.Utils
  )
where

import Conjure.Utils

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

import Data.Dynamic
import Control.Applicative ((<$>)) -- for GHC <= 7.8

import Test.LeanCheck (mapT, filterT, (\/), delay, productWith, productMaybeWith)
import Test.LeanCheck.Tiers (products)
import Test.LeanCheck.Utils.Types (A, B, C, D, E, F)

-- | /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  =  (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
values)
                   forall a. Semigroup a => a -> a -> a
<> (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
vars)
                   forall a. Semigroup a => a -> a -> a
<> (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall (t :: * -> *) a. Foldable t => t a -> Int
length 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  =  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 (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isVar (Expr
erfforall a. a -> [a] -> [a]
:[Expr]
vs))  =  forall {a}. a
err
        | Expr
e forall a. Eq a => a -> a -> Bool
== Expr
e' Bool -> Bool -> Bool
|| Expr -> Int
size Expr
e 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 forall a. Eq a => a -> a -> Bool
== Expr
erf -> Expr
e' Expr -> [(Expr, Expr)] -> Expr
//- forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
vs [Expr]
exs
                       | Bool
otherwise -> [Expr] -> Expr
foldApp (forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
re1 (Expr
efforall 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 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

-- | 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]
ifFor :: Typeable a => a -> Expr
ifFor :: forall a. Typeable a => a -> Expr
ifFor a
a  =  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 forall a. a -> a -> a
`asTypeOf` a
a)

-- | Creates a case 'Expr' of the type of the given proxy.
--
-- > > caseForOrd (undefined :: Int)
-- > case :: Bool -> Int -> Int -> Int -> Int
--
-- > > caseForOrd (undefined :: String)
-- > case :: Bool -> [Char] -> [Char] -> [Char] -> [Char]
caseForOrd :: Typeable a => a -> Expr
caseForOrd :: forall a. Typeable a => a -> Expr
caseForOrd a
a  =  forall a. Typeable a => String -> a -> Expr
value String
"case" (\Ordering
o a
x a
y a
z -> case Ordering
o of Ordering
LT -> a
x; Ordering
EQ -> a
y; Ordering
GT -> a
z 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  =  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?

-- | Lists terminal values in BFS order.
--
-- (cf. 'values', 'holesBFS', 'fillBFS')
valuesBFS :: Expr -> [Expr]
valuesBFS :: Expr -> [Expr]
valuesBFS  =  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat 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)  =  [] forall a. a -> [a] -> [a]
: 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.
--
-- (cf. 'holes', 'valuesBFS', 'fillBFS')
holesBFS :: Expr -> [Expr]
holesBFS :: Expr -> [Expr]
holesBFS  =  forall a. (a -> Bool) -> [a] -> [a]
filter Expr -> Bool
isHole forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Expr]
valuesBFS

-- | Fills holes in BFS order.
--
-- (cf. 'fill', 'valuesBFS', 'fillBFS')
fillBFS :: Expr -> Expr -> Expr
fillBFS :: Expr -> Expr -> Expr
fillBFS Expr
e Expr
e'  =  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, forall a. Maybe a
Nothing)
    (Just Int
lf, Maybe Int
Nothing)             -> (Expr
ef' Expr -> Expr -> Expr
:$ Expr
ex, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
lfforall a. Num a => a -> a -> a
+Int
1)
    (Maybe Int
Nothing, Just Int
lx)             -> (Expr
ef Expr -> Expr -> Expr
:$ Expr
ex', forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
lxforall a. Num a => a -> a -> a
+Int
1)
    (Just Int
lf, Just Int
lx) | Int
lf forall a. Ord a => a -> a -> Bool
<= Int
lx  -> (Expr
ef' Expr -> Expr -> Expr
:$ Expr
ex, forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
lfforall a. Num a => a -> a -> a
+Int
1)
                       | Bool
otherwise -> (Expr
ef Expr -> Expr -> Expr
:$ Expr
ex', forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
lxforall 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 forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
e'  =  (Expr
e', forall a. a -> Maybe a
Just Int
0)
      | Bool
otherwise                    =  (Expr
e, forall a. Maybe a
Nothing)
-- TODO: move BFS functions into Express?

-- | Like '$$' but always works regardless of type.
--
-- /Warning:/ just like ':$', this may produce ill-typed expressions.
--
-- > > zero $$** zero
-- > Just (0 0 :: ill-typed # Int $ Int #)
--
-- Together with '$$|<', this function is unused
-- but is useful when experiment with the source
-- to see the effect of type-corrected
-- on pruning the search space.
--
-- (cf. '$$', '$$|<')
($$**) :: Expr -> Expr -> Maybe Expr
Expr
e1 $$** :: Expr -> Expr -> Maybe Expr
$$** Expr
e2  =  forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2

-- | Like '$$' but relaxed to work on correct kinds.
--
-- > > ordE $$|< zero
-- > Just (ord 0 :: ill-typed # Char -> Int $ Int #)
--
-- > > zero $$|< zero
-- > Nothing
--
-- /Warning:/ just like ':$', this may produce ill-typed expressions.
--
-- Together with '$$**', this function is unused
-- but is useful when experiment with the source
-- to see the effect of type-corrected
-- on pruning the search space.
--
-- (cf. '$$', '$$**')
($$|<) :: 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) forall a. Eq a => a -> a -> Bool
== TypeRep -> Int
tyArity TypeRep
t2
               then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Expr
e1 Expr -> Expr -> Expr
:$ Expr
e2
               else 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


-- | Lists all distinct holes that are possible with the given 'Expr's.
--
-- > > possibleHoles [zero, one, plus]
-- > [_ :: Int,_ :: Int -> Int,_ :: Int -> Int -> Int]
--
-- > > possibleHoles [ae, ordE]
-- > [_ :: Char,_ :: Int,_ :: Char -> Int]
possibleHoles :: [Expr] -> [Expr]
possibleHoles :: [Expr] -> [Expr]
possibleHoles  =  forall a. Ord a => [a] -> [a]
nubSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> [Expr]
ph forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> [a]
nubSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
holeAsTypeOf
  where
  ph :: [Expr] -> [Expr]
ph [Expr]
hs  =  case forall a. Ord a => [a] -> [a]
nubSort forall a b. (a -> b) -> a -> b
$ [Expr]
hs forall a. [a] -> [a] -> [a]
++ [Expr -> Expr
holeAsTypeOf Expr
hfx | Expr
hf <- [Expr]
hs, Expr
hx <- [Expr]
hs, Just Expr
hfx <- [Expr
hf Expr -> Expr -> Maybe Expr
$$ Expr
hx]] of
            [Expr]
hs' | [Expr]
hs' forall a. Eq a => a -> a -> Bool
== [Expr]
hs -> [Expr]
hs
                | Bool
otherwise -> [Expr] -> [Expr]
ph [Expr]
hs'


-- -- Expression enumeration -- --

-- | Enumerate applications between values of the given list of primitives
--   and of the given expressions's type.
--
-- __Arguments:__
--
-- 1. an 'Expr' whose type we are interested in
-- 2. a filtering function, returning 'True' for the expressions to keep
-- 3. a list of primitives to be used in building expression.
--
-- __Result:__ a potentially infinite list of list of enumerated expressions
--
-- The enumeration here is type-directed for performance reasons.
enumerateAppsFor :: Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor :: Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]
enumerateAppsFor Expr
h Expr -> Bool
keep [Expr]
es  =  Expr -> [[Expr]]
for Expr
h
  where
  hs :: [Expr]
  hs :: [Expr]
hs  =  [Expr] -> [Expr]
possibleHoles [Expr]
es
  for :: Expr -> [[Expr]]
  for :: Expr -> [[Expr]]
for Expr
h  =  forall a. (a -> Bool) -> [a] -> [a]
filter (\Expr
e -> Expr -> TypeRep
typ Expr
h forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
e) [Expr]
es forall a. a -> [a] -> [a]
: [[Expr]]
apps
    where
    apps :: [[Expr]]
apps  =  forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. [[a]] -> [[a]] -> [[a]]
(\/) []
          [  forall a. (a -> Bool) -> [[a]] -> [[a]]
filterT Expr -> Bool
keep forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
fliproductWith Expr -> Expr -> Expr
(:$) (Expr -> [[Expr]]
for Expr
hf) (Expr -> [[Expr]]
for Expr
hx)
          |  Expr
hf <- [Expr]
hs
          ,  Expr
hx <- [Expr]
hs
          ,  Just Expr
hfx <- [Expr
hf Expr -> Expr -> Maybe Expr
$$ Expr
hx]
          ,  Expr -> TypeRep
typ Expr
h forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
hfx
          ]

-- | Given an expression whose holes are /all of the same type/
--   and an enumeration of 'Expr's of this same type,
--   enumerate all possible fillings of the original expression
--   with the 'Expr's in the enumeration.
enumerateFillings :: Expr -> [[Expr]] -> [[Expr]]
enumerateFillings :: Expr -> [[Expr]] -> [[Expr]]
enumerateFillings Expr
e  =  forall a b. (a -> b) -> [[a]] -> [[b]]
mapT (Expr -> [Expr] -> Expr
fill Expr
e)
                     forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. [[[a]]] -> [[[a]]]
products
                     forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
holes Expr
e)

-- | Evaluates an 'Expr' to a 'Dynamic' value
--   using the given recursive definition and
--   maximum number of recursive calls.
--
-- (cf. 'Conjure.Defn.toDynamicWithDefn')
recursiveToDynamic :: (Expr,Expr) -> Int -> Expr -> Maybe Dynamic
recursiveToDynamic :: (Expr, Expr) -> Int -> Expr -> Maybe Dynamic
recursiveToDynamic (Expr
efxs, Expr
ebody) Int
n  =  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
_,Int
_,Dynamic
d) -> Dynamic
d) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re (Int
n forall a. Num a => a -> a -> a
* Expr -> Int
size Expr
ebody) Int
n
  where
  (Expr
ef':[Expr]
exs')  =  Expr -> [Expr]
unfoldApp Expr
efxs

  rev :: Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
  rev :: forall a. Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
rev Int
m Int
n Expr
e  =  case Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
e of
                Maybe (Int, Int, Dynamic)
Nothing    -> forall a. Maybe a
Nothing
                Just (Int
m,Int
n,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
m, Int
n, a
x)

  re :: Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
  re :: Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
_  | Int
n forall a. Ord a => a -> a -> Bool
<= Int
0  =  forall a. HasCallStack => String -> a
error String
"recursiveToDynamic: recursion limit reached"
  re Int
m Int
n Expr
_  | Int
m forall a. Ord a => a -> a -> Bool
<= Int
0  =  forall a. HasCallStack => String -> a
error String
"recursiveToDynamic: evaluation limit reached"
  re Int
m Int
n (Value String
"if" Dynamic
_ :$ Expr
ec :$ Expr
ex :$ Expr
ey)  =  case forall a. Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
rev Int
m Int
n Expr
ec of
    Maybe (Int, Int, Bool)
Nothing    -> forall a. Maybe a
Nothing
    Just (Int
m,Int
n,Bool
True)  -> Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
ex
    Just (Int
m,Int
n,Bool
False) -> Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
ey
  re Int
m Int
n (Value String
"||" Dynamic
_ :$ Expr
ep :$ Expr
eq)  =  case forall a. Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
rev Int
m Int
n Expr
ep of
    Maybe (Int, Int, Bool)
Nothing        -> forall a. Maybe a
Nothing
    Just (Int
m,Int
n,Bool
True)  -> (Int
m,Int
n,) 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
m,Int
n,Bool
False) -> Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
eq
  re Int
m Int
n (Value String
"&&" Dynamic
_ :$ Expr
ep :$ Expr
eq)  =  case forall a. Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)
rev Int
m Int
n Expr
ep of
    Maybe (Int, Int, Bool)
Nothing    -> forall a. Maybe a
Nothing
    Just (Int
m,Int
n,Bool
True)  -> Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
eq
    Just (Int
m,Int
n,Bool
False) -> (Int
m,Int
n,) 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
m Int
n Expr
e  =  case Expr -> [Expr]
unfoldApp Expr
e of
    [] -> forall a. HasCallStack => String -> a
error String
"recursiveToDynamic: empty application unfold"  -- should never happen
    [Expr
e] -> (Int
mforall a. Num a => a -> a -> a
-Int
1,Int
n,) 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 -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m (Int
nforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ Expr
ebody Expr -> [(Expr, Expr)] -> Expr
//- forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
exs' [Expr]
exs
             | Bool
otherwise -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Maybe (Int, Int, Dynamic) -> Expr -> Maybe (Int, Int, Dynamic)
($$) (Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)
re Int
m Int
n Expr
ef) [Expr]
exs

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

-- | Evaluates an 'Expr' to a regular Haskell value
--   using the given recursive definition and
--   maximum number of recursive calls.
--   If there's a type mismatch, this function returns 'Nothing'.
--
-- (cf. 'evaluate', 'Conjure.Defn.devaluate')
revaluate :: Typeable a => (Expr,Expr) -> Int -> Expr -> Maybe a
revaluate :: forall a. Typeable a => (Expr, Expr) -> Int -> Expr -> Maybe a
revaluate (Expr, Expr)
dfn Int
n Expr
e  =  (Expr, Expr) -> Int -> Expr -> Maybe Dynamic
recursiveToDynamic (Expr, Expr)
dfn Int
n 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' to a regular Haskell value
--   using the given recursive definition and
--   maximum number of recursive calls.
--   If there's a type mismatch,
--   this function returns the given default value.
--
-- (cf. 'eval', 'Conjure.Defn.deval')
reval :: Typeable a => (Expr,Expr) -> Int -> a -> Expr -> a
reval :: forall a. Typeable a => (Expr, Expr) -> Int -> a -> Expr -> a
reval (Expr, Expr)
dfn Int
n 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 -> Expr -> Maybe a
revaluate (Expr, Expr)
dfn Int
n

-- | like 'productWith' but prefers enumerating from the second tiers first
fliproductWith :: (a->b->c) -> [[a]] -> [[b]] -> [[c]]
fliproductWith :: forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
fliproductWith a -> b -> c
_ [] [[b]]
_  =  []
fliproductWith a -> b -> c
_ [[a]]
_ []  =  []
fliproductWith a -> b -> c
f [[a]]
xss ([b]
ys:[[b]]
yss)  =  forall a b. (a -> b) -> [a] -> [b]
map ([a] -> [b] -> [c]
** [b]
ys) [[a]]
xss
                               forall a. [[a]] -> [[a]] -> [[a]]
\/ forall a. [[a]] -> [[a]]
delay (forall a b c. (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
productWith a -> b -> c
f [[a]]
xss [[b]]
yss)
  where
  [a]
xs ** :: [a] -> [b] -> [c]
** [b]
ys  =  [a
x a -> b -> c
`f` b
y | a
x <- [a]
xs, b
y <- [b]
ys]

-- |
--
-- > useMatches [xx,yy] [xx,yy]  =  [[(xx,xx), (yy,yy)]]
-- > useMatches [xx,yy] [yy,xx]  =  [[(xx,xx), (yy,yy)]]
-- > useMatches [yy,xx] [xx,yy]  =  [[(yy,yy), (xx,xx)]]
-- > useMatches [xx,yy] [xx,xx]  =  []
-- > useMatches [xx,yy] [abs' xx, abs' yy]  =  [[(xx,abs' xx), (yy, abs' yy)]]
-- > useMatches [xx-:-xxs, yy-:-yys] [abs' xx, abs' yy]
-- >   =  [(xx-:-xxs, abs' xx), (yy-:-yys, abs' yy)]
useMatches :: [Expr] -> [Expr] -> [[(Expr,Expr)]]
useMatches :: [Expr] -> [Expr] -> [[(Expr, Expr)]]
useMatches [] []  =  [[]]
useMatches [] [Expr]
es  =  [] -- no matches when lists have different lengths
useMatches [Expr]
es []  =  [] -- no matches when lists have different lengths
useMatches (Expr
e:[Expr]
es) [Expr]
es'  =  forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ forall a b. (a -> b) -> [a] -> [b]
map ((Expr
e,Expr
e')forall a. a -> [a] -> [a]
:) ([Expr] -> [Expr] -> [[(Expr, Expr)]]
useMatches [Expr]
es [Expr]
es')
  | (Expr
e',[Expr]
es') <- forall a. (a -> [a] -> Bool) -> [a] -> [(a, [a])]
choicesThat (\Expr
e' [Expr]
_ -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Expr]
vars Expr
e') (Expr -> [Expr]
vars Expr
e)) [Expr]
es'
  ]

-- | Turns all variables of an expression into holes.
--
-- > > rehole (xx -+- yy)
-- > _ + _ :: Int
rehole :: Expr -> Expr
rehole :: Expr -> Expr
rehole (Expr
e1 :$ Expr
e2)    = Expr -> Expr
rehole Expr
e1 Expr -> Expr -> Expr
:$ Expr -> Expr
rehole Expr
e2
rehole Expr
e | Expr -> Bool
isVar Expr
e   = String
"" String -> Expr -> Expr
`varAsTypeOf` Expr
e
         | Bool
otherwise = Expr
e

-- | Takes two expressions and returns all possible ways
--   in which the first expression can appear once in
--   one of the holes of the second expression.
--
-- > > deholings zero (i_ -+- i_ -+- i_)
-- > [ (0 + _) + _ :: Int
-- > , (_ + 0) + _ :: Int
-- > , (_ + _) + 0 :: Int
-- > ]
--
-- > > deholings zero (i_ -+- one -+- ord' c_)
-- > [(0 + 1) + ord _ :: Int]
deholings :: Expr -> Expr -> [Expr]
deholings :: Expr -> Expr -> [Expr]
deholings Expr
e'  =  Expr -> [Expr]
deh
  where
  deh :: Expr -> [Expr]
deh (Expr
e1 :$ Expr
e2)  =  forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Expr -> Expr
:$ Expr
e2) (Expr -> [Expr]
deh Expr
e1)
                  forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Expr
e1 Expr -> Expr -> Expr
:$) (Expr -> [Expr]
deh Expr
e2)
  deh Expr
e  =  if Expr -> TypeRep
typ Expr
e forall a. Eq a => a -> a -> Bool
== Expr -> TypeRep
typ Expr
e' Bool -> Bool -> Bool
&& Expr -> Bool
isHole Expr
e
            then [Expr
e']
            else []

instance Express A where  expr :: A -> Expr
expr  =  forall a. (Typeable a, Show a) => a -> Expr
val
instance Express B where  expr :: B -> Expr
expr  =  forall a. (Typeable a, Show a) => a -> Expr
val
instance Express C where  expr :: C -> Expr
expr  =  forall a. (Typeable a, Show a) => a -> Expr
val
instance Express D where  expr :: D -> Expr
expr  =  forall a. (Typeable a, Show a) => a -> Expr
val
instance Express E where  expr :: E -> Expr
expr  =  forall a. (Typeable a, Show a) => a -> Expr
val
instance Express F where  expr :: F -> Expr
expr  =  forall a. (Typeable a, Show a) => a -> Expr
val