module Gradual.Refinements (makeGMap) where

import Gradual.Types
import Gradual.Misc 
-- import Gradual.PrettyPrinting

import Language.Fixpoint.Types
import Language.Fixpoint.Types.Config
import Language.Fixpoint.Solver.Monad
import Language.Fixpoint.Solver.Solve (solverInfo)
import Language.Fixpoint.Utils.Files 
import Language.Fixpoint.SortCheck (exprSort_maybe)


import Control.Monad (filterM)
-- import Control.Monad.IO.Class

makeGMap :: GConfig -> Config -> SInfo a -> [(KVar, (GWInfo, [Expr]))] -> IO (GMap GWInfo)
makeGMap :: GConfig
-> Config
-> SInfo a
-> [(KVar, (GWInfo, [Expr]))]
-> IO (GMap GWInfo)
makeGMap GConfig
gcfg Config
cfg SInfo a
sinfo [(KVar, (GWInfo, [Expr]))]
mes = [(KVar, (GWInfo, [Expr]))] -> GMap GWInfo
forall a. [(KVar, (a, [Expr]))] -> GMap a
toGMap ([(KVar, (GWInfo, [Expr]))] -> GMap GWInfo)
-> IO [(KVar, (GWInfo, [Expr]))] -> IO (GMap GWInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config
-> SolverInfo a Any
-> SolveM [(KVar, (GWInfo, [Expr]))]
-> IO [(KVar, (GWInfo, [Expr]))]
forall b c a. Config -> SolverInfo b c -> SolveM a -> IO a
runSolverM Config
cfg' SolverInfo a Any
forall b. SolverInfo a b
sI SolveM [(KVar, (GWInfo, [Expr]))]
act 
  where
    sI :: SolverInfo a b
sI   = Config -> SInfo a -> SolverInfo a b
forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg' SInfo a
sinfo
    act :: SolveM [(KVar, (GWInfo, [Expr]))]
act  = ((KVar, (GWInfo, [Expr]))
 -> StateT SolverState IO (KVar, (GWInfo, [Expr])))
-> [(KVar, (GWInfo, [Expr]))] -> SolveM [(KVar, (GWInfo, [Expr]))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (GConfig
-> (KVar, (GWInfo, [Expr]))
-> StateT SolverState IO (KVar, (GWInfo, [Expr]))
concretize GConfig
gcfg) [(KVar, (GWInfo, [Expr]))]
mes
    cfg' :: Config
cfg' = Config
cfg { srcFile :: FilePath
srcFile = Config -> FilePath
srcFile Config
cfg FilePath -> Ext -> FilePath
`withExt` Ext
Pred 
               , gradual :: Bool
gradual = Bool
True -- disable mbqi
           }

concretize :: GConfig -> (KVar, (GWInfo, [Expr])) -> SolveM (KVar, (GWInfo,[Expr]))
concretize :: GConfig
-> (KVar, (GWInfo, [Expr]))
-> StateT SolverState IO (KVar, (GWInfo, [Expr]))
concretize GConfig
cfg (KVar
kv, (GWInfo
info, [Expr]
es))
  = (\[Expr]
es' -> (KVar
kv,(GWInfo
info,[Expr]
es'))) ([Expr] -> (KVar, (GWInfo, [Expr])))
-> StateT SolverState IO [Expr]
-> StateT SolverState IO (KVar, (GWInfo, [Expr]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 
     (Expr -> StateT SolverState IO Bool)
-> [Expr] -> StateT SolverState IO [Expr]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (GWInfo -> Expr -> StateT SolverState IO Bool
isGoodInstance GWInfo
info) 
             (Expr
PTrueExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:([Expr] -> Expr
pAnd ([Expr] -> Expr) -> [[Expr]] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Expr] -> [[Expr]]
forall a. Int -> [a] -> [[a]]
powersetUpTo (GConfig -> Int
depth GConfig
cfg) [Expr]
es))

isGoodInstance :: GWInfo -> Expr -> SolveM Bool 
isGoodInstance :: GWInfo -> Expr -> StateT SolverState IO Bool
isGoodInstance GWInfo
info Expr
e 
  | Expr -> Bool
isSensible Expr
e -- heuristic to delete stupit instantiations
  = Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> StateT SolverState IO Bool
-> StateT SolverState IO (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GWInfo -> Expr -> StateT SolverState IO Bool
isLocal GWInfo
info Expr
e) StateT SolverState IO (Bool -> Bool)
-> StateT SolverState IO Bool -> StateT SolverState IO Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (GWInfo -> Expr -> StateT SolverState IO Bool
isMoreSpecific GWInfo
info Expr
e) 
  | Bool
otherwise 
  = Bool -> StateT SolverState IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False 

isSensible :: Expr -> Bool 
isSensible :: Expr -> Bool
isSensible (PIff Expr
_ (PAtom Brel
_ Expr
e1 Expr
e2))
  | Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e2 
  = Bool
False 
isSensible (PAtom Brel
cmp Expr
e Expr
_)
  | Brel
cmp Brel -> [Brel] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Brel
Gt,Brel
Ge,Brel
Lt,Brel
Le]
  , Just Sort
s <- Expr -> Maybe Sort
exprSort_maybe Expr
e 
  , Sort
boolSort Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
s
  = Bool
False 
isSensible Expr
_ 
  = Bool
True 

isLocal :: GWInfo -> Expr -> SolveM Bool 
isLocal :: GWInfo -> Expr -> StateT SolverState IO Bool
isLocal GWInfo
i Expr
e = Expr -> StateT SolverState IO Bool
isValid ([(Symbol, Sort)] -> Expr -> Expr
PExist [(GWInfo -> Symbol
gsym GWInfo
i, GWInfo -> Sort
gsort GWInfo
i)] Expr
e)

isMoreSpecific :: GWInfo -> Expr -> SolveM Bool
isMoreSpecific :: GWInfo -> Expr -> StateT SolverState IO Bool
isMoreSpecific GWInfo
i Expr
e = Expr -> StateT SolverState IO Bool
isValid ([Expr] -> Expr
pAnd [Expr
e, GWInfo -> Expr
gexpr GWInfo
i] Expr -> Expr -> Expr
`PImp` GWInfo -> Expr
gexpr GWInfo
i)


isValid :: Expr -> SolveM Bool
isValid :: Expr -> StateT SolverState IO Bool
isValid Expr
e 
  | Expr -> Bool
isContraPred Expr
e = Bool -> StateT SolverState IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False 
  | Expr -> Bool
isTautoPred  Expr
e = Bool -> StateT SolverState IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True 
  | PImp (PAnd [Expr]
es) Expr
e2 <- Expr
e 
  , Expr
e2 Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
es    = Bool -> StateT SolverState IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True    
isValid Expr
e = Bool -> Bool
not (Bool -> Bool)
-> StateT SolverState IO Bool -> StateT SolverState IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT SolverState IO Bool
checkSat (Expr -> Expr
PNot Expr
e)