{-# LANGUAGE DeriveDataTypeable #-} -- for GHC <= 7.8
-- |
-- Module      : Test.Extrapolate.Expr
-- Copyright   : (c) 2017-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part of Extrapolate,
-- a library for generalization of counter-examples.
--
-- This module re-exports functionality from
-- "Data.Express" and "Test.Speculate.Expr"
-- along with some extra utilities.
module Test.Extrapolate.Expr
  ( module Data.Express
  , module Test.Speculate.Expr

  , canonicalizeUsingHoles
  , canonicalizeUsingHolesWith
  , unand
  , replaceFun

  -- * misc re-exports
  , (-&&-)
  , false
  )
where

import Data.Express
import Data.Express.Fixtures
import Test.Speculate.Expr

-- |
-- Like 'canonicalize' but uses holes for unrepeated variables.
canonicalizeUsingHoles :: Expr -> Expr
canonicalizeUsingHoles :: Expr -> Expr
canonicalizeUsingHoles  =  (Expr -> [String]) -> Expr -> Expr
canonicalizeUsingHolesWith ([Expr] -> Expr -> [String]
lookupNames [Expr]
preludeNameInstances)

-- |
-- Like 'canonicalizeWith' but uses holes for unrepeated variables.
canonicalizeUsingHolesWith :: (Expr -> [String]) -> Expr -> Expr
canonicalizeUsingHolesWith :: (Expr -> [String]) -> Expr -> Expr
canonicalizeUsingHolesWith Expr -> [String]
namesFor  =  Expr -> Expr
c1 (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
unrepeatedToHole1
  where
  c1 :: Expr -> Expr
c1 Expr
e  =  Expr
e Expr -> [(Expr, Expr)] -> Expr
//- Expr -> [(Expr, Expr)]
cn Expr
e
  cn :: Expr -> [(Expr, Expr)]
cn Expr
e  =  (Expr -> [String]) -> Expr -> [(Expr, Expr)]
canonicalizationWith Expr -> [String]
namesFor
        (Expr -> [(Expr, Expr)]) -> Expr -> [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$  [Expr] -> Expr
fold [Expr
v | Expr
v <- Expr -> [Expr]
vars Expr
e, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Expr -> Bool
isHole Expr
v]
  unrepeatedToHole1 :: Expr -> Expr
unrepeatedToHole1 Expr
e = Expr
e Expr -> [(Expr, Expr)] -> Expr
//- [(Expr
v, Expr -> Expr
holeAsTypeOf Expr
v) | (Expr
v,Int
1) <- Expr -> [(Expr, Int)]
countVars Expr
e]
  countVars :: Expr -> [(Expr, Int)]
countVars Expr
e = (Expr -> (Expr, Int)) -> [Expr] -> [(Expr, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (\Expr
e' -> (Expr
e',[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 -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e') ([Expr] -> Int) -> [Expr] -> Int
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
vars Expr
e)) ([Expr] -> [(Expr, Int)]) -> [Expr] -> [(Expr, Int)]
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr]
nubVars Expr
e

unand :: Expr -> (Expr,Expr)
unand :: Expr -> (Expr, Expr)
unand ((Expr
op :$ Expr
e1) :$ Expr
e2) | Expr
op Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
andE  =  (Expr
e1,Expr
e2)
unand Expr
_  =  String -> (Expr, Expr)
forall a. HasCallStack => String -> a
error String
"unand: not an implication"

-- | /O(n)/.
-- Replaces the function in the given 'Expr'.
--
-- > replaceFun timesE (plusE :$ one :$ two) = timesE :$ one :$ two
-- > replaceFun absE (idE :$ one) = absE :$ one
-- > replaceFun two (one) = two
replaceFun :: Expr -> Expr -> Expr
replaceFun :: Expr -> Expr -> Expr
replaceFun Expr
ef Expr
e = [Expr] -> Expr
foldApp (Expr
efExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr] -> [Expr]
forall a. [a] -> [a]
tail [Expr]
es)
  where
  es :: [Expr]
es = Expr -> [Expr]
unfoldApp Expr
e