{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE BangPatterns #-}

module Language.Haskell.Liquid.Synthesize.Misc where

import qualified Language.Fixpoint.Types        as F 
import           Control.Monad.State.Lazy
import           CoreSyn
import           TyCoRep 
import           Text.PrettyPrint.HughesPJ (text, Doc, vcat, ($+$))
import           Language.Haskell.Liquid.Synthesize.GHC
import           Language.Haskell.Liquid.GHC.TypeRep
import           Language.Fixpoint.Types


isFunction :: Type -> Bool
isFunction :: Type -> Bool
isFunction FunTy{}    = Bool
True 
isFunction ForAllTy{} = Bool
True
isFunction Type
_          = Bool
False

(<$$>) :: (Functor m, Functor n) => (a -> b) -> m (n a) -> m (n b)
<$$> :: (a -> b) -> m (n a) -> m (n b)
(<$$>) = (n a -> n b) -> m (n a) -> m (n b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((n a -> n b) -> m (n a) -> m (n b))
-> ((a -> b) -> n a -> n b) -> (a -> b) -> m (n a) -> m (n b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> n a -> n b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

filterElseM :: Monad m => (a -> m Bool) -> [a] -> m [a] -> m [a]
filterElseM :: (a -> m Bool) -> [a] -> m [a] -> m [a]
filterElseM a -> m Bool
f [a]
as m [a]
ms = do
    [a]
rs <- (a -> m Bool) -> [a] -> m [a]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM a -> m Bool
f [a]
as
    if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
rs then
        m [a]
ms
    else
        [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a]
rs

-- Replaces    | old w   | new  | symbol name in expr.
substInFExpr :: F.Symbol -> F.Symbol -> F.Expr -> F.Expr
substInFExpr :: Symbol -> Symbol -> Expr -> Expr
substInFExpr Symbol
pn Symbol
nn Expr
e = Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
F.subst1 Expr
e (Symbol
pn, Symbol -> Expr
F.EVar Symbol
nn)


findM :: Monad m => (a -> m Bool) -> [a] -> m (Maybe a)
findM :: (a -> m Bool) -> [a] -> m (Maybe a)
findM a -> m Bool
_ []     = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
findM a -> m Bool
p (a
x:[a]
xs) = do Bool
b <- a -> m Bool
p a
x ; if Bool
b then Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a
forall a. a -> Maybe a
Just a
x) else (a -> m Bool) -> [a] -> m (Maybe a)
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM a -> m Bool
p [a]
xs 


composeM :: Monad m => (a -> m b) -> (b -> c) -> a -> m c
composeM :: (a -> m b) -> (b -> c) -> a -> m c
composeM a -> m b
f b -> c
g a
x = do 
    b
mx <- a -> m b
f a
x
    c -> m c
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> c
g b
mx)

----------------------------------------------------------------------------
----------------------------Printing----------------------------------------
----------------------------------------------------------------------------
solDelim :: String
solDelim :: String
solDelim = String
"*********************************************"

-- pprintMany :: (F.PPrint a) => [a] -> Doc
-- pprintMany xs = vcat [ F.pprint x $+$ text solDelim | x <- xs ]

pprintMany :: [String] -> Doc
pprintMany :: [String] -> Doc
pprintMany [String]
xs = [Doc] -> Doc
vcat [ String -> Doc
text String
x Doc -> Doc -> Doc
$+$ String -> Doc
text String
solDelim | String
x <- [String]
xs ]

showGoals :: [[String]] -> String
showGoals :: [[String]] -> String
showGoals []             = String
""
showGoals ([String]
goal : [[String]]
goals) = 
    [String] -> String
forall a. Show a => a -> String
show [String]
goal        String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
    String
"\n"             String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
    Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
12 Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ 
    [[String]] -> String
showGoals [[String]]
goals

showEmem :: (Show a1, Show a2) => [(Type, a1, a2)] -> String
showEmem :: [(Type, a1, a2)] -> String
showEmem  [(Type, a1, a2)]
emem = [(String, String, String)] -> String
forall a. Show a => a -> String
show ([(String, String, String)] -> String)
-> [(String, String, String)] -> String
forall a b. (a -> b) -> a -> b
$ [(Type, a1, a2)] -> [(String, String, String)]
forall a1 a2.
(Show a1, Show a2) =>
[(Type, a1, a2)] -> [(String, String, String)]
showEmem' [(Type, a1, a2)]
emem

showEmem' :: (Show a1, Show a2) => [(Type, a1, a2)] -> [(String, String, String)]
showEmem' :: [(Type, a1, a2)] -> [(String, String, String)]
showEmem' [(Type, a1, a2)]
emem = ((Type, a1, a2) -> (String, String, String))
-> [(Type, a1, a2)] -> [(String, String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Type
t, a1
e, a2
i) -> (a1 -> String
forall a. Show a => a -> String
show a1
e, Type -> String
showTy Type
t, a2 -> String
forall a. Show a => a -> String
show a2
i)) [(Type, a1, a2)]
emem

exprmemToExpr :: [(a2, CoreExpr, Int)] -> String
exprmemToExpr :: [(a2, CoreExpr, Int)] -> String
exprmemToExpr [(a2, CoreExpr, Int)]
em = [String] -> String
forall a. Show a => a -> String
show ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((a2, CoreExpr, Int) -> String)
-> [(a2, CoreExpr, Int)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(a2
_, CoreExpr
e, Int
i) -> (CoreExpr, Int) -> String
forall a. Show a => a -> String
show (CoreExpr -> CoreExpr
fromAnf CoreExpr
e, Int
i) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" * ") [(a2, CoreExpr, Int)]
em 

showCand :: (a, (Type, b)) -> (String, b)
showCand :: (a, (Type, b)) -> (String, b)
showCand (a
_, (Type
t, b
v)) = (Type -> String
showTy Type
t, b
v)

showCands :: [(a, (Type, b))] -> [(String, b)]
showCands :: [(a, (Type, b))] -> [(String, b)]
showCands = ((a, (Type, b)) -> (String, b))
-> [(a, (Type, b))] -> [(String, b)]
forall a b. (a -> b) -> [a] -> [b]
map (a, (Type, b)) -> (String, b)
forall a b. (a, (Type, b)) -> (String, b)
showCand

notrace :: String -> a -> a 
notrace :: String -> a -> a
notrace String
_ a
a = a
a 

instance PPrint AltCon

showCoreAlt :: CoreAlt -> String
showCoreAlt :: CoreAlt -> String
showCoreAlt (DataAlt DataCon
altCon, [CoreBndr]
vars, CoreExpr
expr) = 
  String
" For " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DataCon -> String
forall a. Show a => a -> String
show DataCon
altCon String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" vars " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [CoreBndr] -> String
forall a. Show a => a -> String
show [CoreBndr]
vars String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" expr " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CoreExpr -> String
forall a. Show a => a -> String
show CoreExpr
expr
showCoreAlt CoreAlt
_ = String
" No! "

showCoreAlts :: [CoreAlt] -> String
showCoreAlts :: [CoreAlt] -> String
showCoreAlts [CoreAlt]
alts = (CoreAlt -> String) -> [CoreAlt] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreAlt -> String
showCoreAlt [CoreAlt]
alts