{-# LANGUAGE PatternGuards     #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}

--------------------------------------------------------------------------------
-- | Solve a system of horn-clause constraints ---------------------------------
--------------------------------------------------------------------------------

module Language.Fixpoint.Solver.Solve (solve, solverInfo) where

import           Control.Monad (when, filterM)
import           Control.Monad.Reader
import           Control.Monad.State.Strict (modify)
import           Language.Fixpoint.Misc
import qualified Language.Fixpoint.Misc            as Misc
import qualified Language.Fixpoint.Types           as F
import qualified Language.Fixpoint.Types.Solutions as Sol
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Config hiding (stats)
import           Language.Fixpoint.SortCheck          (ElabM)
import qualified Language.Fixpoint.Solver.Solution  as S
import qualified Language.Fixpoint.Smt.Types as T
import qualified Language.Fixpoint.Solver.Worklist  as W
import qualified Language.Fixpoint.Solver.Eliminate as E
import           Language.Fixpoint.Solver.Monad
import           Language.Fixpoint.Utils.Progress
import           Language.Fixpoint.Graph
import           Text.PrettyPrint.HughesPJ
import           Text.Printf
import           System.Console.CmdArgs.Verbosity -- (whenNormal, whenLoud)
import           Control.DeepSeq
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S
-- import qualified Data.Maybe          as Mb
import qualified Data.List           as L
import Language.Fixpoint.Types (resStatus, FixResult(Unsafe))
import qualified Language.Fixpoint.Types.Config as C
import Language.Fixpoint.Solver.Interpreter (instInterpreter)
import Language.Fixpoint.Solver.Instantiate (instantiate)
--import Debug.Trace                      (trace)

mytrace :: String -> a -> a
mytrace :: forall a. [Char] -> a -> a
mytrace [Char]
_ a
x = {- trace s -} a
x

--------------------------------------------------------------------------------
solve :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> IO (F.Result (Integer, a))
--------------------------------------------------------------------------------

solve :: forall a.
(NFData a, Fixpoint a, Show a, Loc a) =>
Config -> SInfo a -> IO (Result (Integer, a))
solve Config
cfg SInfo a
fi = do
    IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> [Char] -> IO ()
donePhase Moods
Misc.Loud [Char]
"Worklist Initialize"
    Verbosity
vb <- IO Verbosity
getVerbosity
    (Result (Integer, a)
res, Stats
stat) <- (if Verbosity
Quiet Verbosity -> Verbosity -> Bool
forall a. Eq a => a -> a -> Bool
== Verbosity
vb Bool -> Bool -> Bool
|| Config -> Bool
gradual Config
cfg then IO (Result (Integer, a), Stats) -> IO (Result (Integer, a), Stats)
forall a. a -> a
id else SolverInfo a (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
forall a b. SolverInfo a b -> IO b -> IO b
withProgressFI SolverInfo a (Result (Integer, a), Stats)
forall {b}. SolverInfo a b
sI) (IO (Result (Integer, a), Stats)
 -> IO (Result (Integer, a), Stats))
-> IO (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
forall a b. (a -> b) -> a -> b
$ Config
-> SolverInfo a Any
-> SolveM a (Result (Integer, a), Stats)
-> IO (Result (Integer, a), Stats)
forall ann c a. Config -> SolverInfo ann c -> SolveM ann a -> IO a
runSolverM Config
cfg SolverInfo a Any
forall {b}. SolverInfo a b
sI SolveM a (Result (Integer, a), Stats)
act
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
solverStats Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ SInfo a -> Worklist a -> Stats -> IO ()
forall a. SInfo a -> Worklist a -> Stats -> IO ()
printStats SInfo a
fi Worklist a
wkl Stats
stat
    -- print (numIter stat)
    Result (Integer, a) -> IO (Result (Integer, a))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Result (Integer, a)
res
  where
    act :: SolveM a (Result (Integer, a), Stats)
act = Config
-> SInfo a
-> Solution
-> HashSet KVar
-> Worklist a
-> SolveM a (Result (Integer, a), Stats)
forall a.
(NFData a, Fixpoint a, Loc a) =>
Config
-> SInfo a
-> Solution
-> HashSet KVar
-> Worklist a
-> SolveM a (Result (Integer, a), Stats)
solve_ Config
cfg SInfo a
fi Solution
forall {b}. Sol b QBind
s0 HashSet KVar
ks  Worklist a
wkl
    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
fi
    wkl :: Worklist a
wkl = SolverInfo a Any -> Worklist a
forall a b. SolverInfo a b -> Worklist a
W.init SolverInfo a Any
forall {b}. SolverInfo a b
sI
    s0 :: Sol b QBind
s0  = SolverInfo a b -> Sol b QBind
forall a b. SolverInfo a b -> Sol b QBind
siSol  SolverInfo a b
forall {b}. SolverInfo a b
sI
    ks :: HashSet KVar
ks  = SolverInfo a Any -> HashSet KVar
forall a b. SolverInfo a b -> HashSet KVar
siVars SolverInfo a Any
forall {b}. SolverInfo a b
sI


--------------------------------------------------------------------------------
-- | Progress Bar
--------------------------------------------------------------------------------
withProgressFI :: SolverInfo a b -> IO b -> IO b
withProgressFI :: forall a b. SolverInfo a b -> IO b -> IO b
withProgressFI = Int -> IO b -> IO b
forall a. Int -> IO a -> IO a
withProgress (Int -> IO b -> IO b)
-> (SolverInfo a b -> Int) -> SolverInfo a b -> IO b -> IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Int) -> (SolverInfo a b -> Int) -> SolverInfo a b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> (SolverInfo a b -> Int) -> SolverInfo a b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CDeps -> Int
cNumScc (CDeps -> Int)
-> (SolverInfo a b -> CDeps) -> SolverInfo a b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverInfo a b -> CDeps
forall a b. SolverInfo a b -> CDeps
siDeps
--------------------------------------------------------------------------------

printStats :: F.SInfo a ->  W.Worklist a -> Stats -> IO ()
printStats :: forall a. SInfo a -> Worklist a -> Stats -> IO ()
printStats SInfo a
fi Worklist a
w Stats
s = [Char] -> IO ()
putStrLn [Char]
"\n" IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [DocTable] -> IO ()
ppTs [ SInfo a -> DocTable
forall a. PTable a => a -> DocTable
ptable SInfo a
fi, Stats -> DocTable
forall a. PTable a => a -> DocTable
ptable Stats
s, Worklist a -> DocTable
forall a. PTable a => a -> DocTable
ptable Worklist a
w ]
  where
    ppTs :: [DocTable] -> IO ()
ppTs          = [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> ([DocTable] -> [Char]) -> [DocTable] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DocTable -> [Char]
forall a. PPrint a => a -> [Char]
showpp (DocTable -> [Char])
-> ([DocTable] -> DocTable) -> [DocTable] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DocTable] -> DocTable
forall a. Monoid a => [a] -> a
mconcat

--------------------------------------------------------------------------------
solverInfo :: Config -> F.SInfo a -> SolverInfo a b
--------------------------------------------------------------------------------
solverInfo :: forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg SInfo a
fI
  | Config -> Bool
useElim Config
cfg = Config -> SInfo a -> SolverInfo a b
forall a b. Config -> SInfo a -> SolverInfo a b
E.solverInfo Config
cfg SInfo a
fI
  | Bool
otherwise   = Sol b QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a b
forall a b.
Sol b QBind -> SInfo a -> CDeps -> HashSet KVar -> SolverInfo a b
SI Sol b QBind
forall a. Monoid a => a
mempty SInfo a
fI CDeps
cD (SInfo a -> HashSet KVar
forall a. SInfo a -> HashSet KVar
siKvars SInfo a
fI)
  where
    cD :: CDeps
cD          = SInfo a -> [CEdge] -> HashSet KVar -> HashSet Symbol -> CDeps
forall (c :: * -> *) a.
TaggedC c a =>
GInfo c a -> [CEdge] -> HashSet KVar -> HashSet Symbol -> CDeps
elimDeps SInfo a
fI (SInfo a -> [CEdge]
forall (c :: * -> *) a. TaggedC c a => GInfo c a -> [CEdge]
kvEdges SInfo a
fI) HashSet KVar
forall a. Monoid a => a
mempty HashSet Symbol
forall a. Monoid a => a
mempty

siKvars :: F.SInfo a -> S.HashSet F.KVar
siKvars :: forall a. SInfo a -> HashSet KVar
siKvars = [KVar] -> HashSet KVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([KVar] -> HashSet KVar)
-> (SInfo a -> [KVar]) -> SInfo a -> HashSet KVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap KVar (WfC a) -> [KVar]
forall k v. HashMap k v -> [k]
M.keys (HashMap KVar (WfC a) -> [KVar])
-> (SInfo a -> HashMap KVar (WfC a)) -> SInfo a -> [KVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws

doInterpret :: (F.Loc a) =>  Config -> F.SInfo a -> [F.SubcId] -> SolveM a (F.SInfo a)
doInterpret :: forall a.
Loc a =>
Config -> SInfo a -> [Integer] -> SolveM a (SInfo a)
doInterpret Config
cfg SInfo a
fi0 [Integer]
subcIds = do
  SInfo a
fi <- IO (SInfo a) -> SolveM a (SInfo a)
forall a. IO a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SInfo a) -> SolveM a (SInfo a))
-> IO (SInfo a) -> SolveM a (SInfo a)
forall a b. (a -> b) -> a -> b
$ Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
forall a.
Loc a =>
Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
instInterpreter Config
cfg SInfo a
fi0 ([Integer] -> Maybe [Integer]
forall a. a -> Maybe a
Just [Integer]
subcIds)
  (SolverState a -> SolverState a) -> StateT (SolverState a) IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SolverState a -> SolverState a) -> StateT (SolverState a) IO ())
-> (SolverState a -> SolverState a) -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ SInfo a -> SolverState a -> SolverState a
forall {ann} {ann}.
GInfo SimpC ann -> SolverState ann -> SolverState ann
update' SInfo a
fi
  SInfo a -> SolveM a (SInfo a)
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return SInfo a
fi
  where
    update' :: GInfo SimpC ann -> SolverState ann -> SolverState ann
update' GInfo SimpC ann
fi SolverState ann
ss = SolverState ann
ss{ssBinds = F.bs fi'}
      where
        fi' :: GInfo SimpC ann
fi' = (SolverInfo ann Any -> GInfo SimpC ann
forall a b. SolverInfo a b -> SInfo a
siQuery SolverInfo ann Any
forall {b}. SolverInfo ann b
sI) {F.hoInfo = F.HOI (C.allowHO cfg) (C.allowHOqs cfg)}
        sI :: SolverInfo ann b
sI  = Config -> GInfo SimpC ann -> SolverInfo ann b
forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg GInfo SimpC ann
fi

{-# SCC doPLE #-}
doPLE :: (F.Loc a) =>  Config -> F.SInfo a -> [F.SubcId] -> SolveM a ()
doPLE :: forall a. Loc a => Config -> SInfo a -> [Integer] -> SolveM a ()
doPLE Config
cfg SInfo a
fi0 [Integer]
subcIds = do
  SInfo a
fi <- IO (SInfo a) -> StateT (SolverState a) IO (SInfo a)
forall a. IO a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SInfo a) -> StateT (SolverState a) IO (SInfo a))
-> IO (SInfo a) -> StateT (SolverState a) IO (SInfo a)
forall a b. (a -> b) -> a -> b
$ Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
forall a.
Loc a =>
Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
instantiate Config
cfg SInfo a
fi0 ([Integer] -> Maybe [Integer]
forall a. a -> Maybe a
Just [Integer]
subcIds)
  (SolverState a -> SolverState a) -> SolveM a ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SolverState a -> SolverState a) -> SolveM a ())
-> (SolverState a -> SolverState a) -> SolveM a ()
forall a b. (a -> b) -> a -> b
$ SInfo a -> SolverState a -> SolverState a
forall {ann} {ann}.
GInfo SimpC ann -> SolverState ann -> SolverState ann
update' SInfo a
fi
  where
    update' :: GInfo SimpC ann -> SolverState ann -> SolverState ann
update' GInfo SimpC ann
fi SolverState ann
ss = SolverState ann
ss{ssBinds = F.bs fi'}
      where
        fi' :: GInfo SimpC ann
fi' = (SolverInfo ann Any -> GInfo SimpC ann
forall a b. SolverInfo a b -> SInfo a
siQuery SolverInfo ann Any
forall {b}. SolverInfo ann b
sI) {F.hoInfo = F.HOI (C.allowHO cfg) (C.allowHOqs cfg)}
        sI :: SolverInfo ann b
sI  = Config -> GInfo SimpC ann -> SolverInfo ann b
forall a b. Config -> SInfo a -> SolverInfo a b
solverInfo Config
cfg GInfo SimpC ann
fi

--------------------------------------------------------------------------------
{-# SCC solve_ #-}
solve_ :: (NFData a, F.Fixpoint a, F.Loc a)
       => Config
       -> F.SInfo a
       -> Sol.Solution
       -> S.HashSet F.KVar
       -> W.Worklist a
       -> SolveM a (F.Result (Integer, a), Stats)
--------------------------------------------------------------------------------
solve_ :: forall a.
(NFData a, Fixpoint a, Loc a) =>
Config
-> SInfo a
-> Solution
-> HashSet KVar
-> Worklist a
-> SolveM a (Result (Integer, a), Stats)
solve_ Config
cfg SInfo a
fi Solution
s0 HashSet KVar
ks Worklist a
wkl = do
  let s1 :: Solution
s1   = [Char] -> Solution -> Solution
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"solve_ " (Solution -> Solution) -> Solution -> Solution
forall a b. (a -> b) -> a -> b
$ {-# SCC "sol-init" #-} Config -> SInfo a -> HashSet KVar -> Solution
forall a.
Fixpoint a =>
Config -> SInfo a -> HashSet KVar -> Solution
S.init Config
cfg SInfo a
fi HashSet KVar
ks
  let s2 :: Solution
s2   = Solution -> Solution -> Solution
forall a. Monoid a => a -> a -> a
mappend Solution
s0 Solution
s1
  (Solution
s3, Result (Integer, a)
res0) <- IBindEnv
-> (IBindEnv -> SolveM a (Solution, Result (Integer, a)))
-> SolveM a (Solution, Result (Integer, a))
forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv ((IBindEnv -> SolveM a (Solution, Result (Integer, a)))
 -> SolveM a (Solution, Result (Integer, a)))
-> (IBindEnv -> SolveM a (Solution, Result (Integer, a)))
-> SolveM a (Solution, Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt -> do
    -- let s3   = solveEbinds fi s2
    Solution
s3       <- {- SCC "sol-refine" -} IBindEnv -> Solution -> Worklist a -> SolveM a Solution
forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s2 Worklist a
wkl
    Result (Integer, a)
res0     <- {- SCC "sol-result" -} IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg Worklist a
wkl Solution
s3
    (Solution, Result (Integer, a))
-> SolveM a (Solution, Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Solution
s3, Result (Integer, a)
res0)

  (SInfo a
fi1, Solution
s4, Result (Integer, a)
res1) <- case Result (Integer, a) -> FixResult (Integer, a)
forall a. Result a -> FixResult a
resStatus Result (Integer, a)
res0 of  {- first run the interpreter -}
    Unsafe Stats
_ [(Integer, a)]
bads | Bool -> Bool
not (Config -> Bool
noLazyPLE Config
cfg) Bool -> Bool -> Bool
&& Config -> Bool
rewriteAxioms Config
cfg Bool -> Bool -> Bool
&& Config -> Bool
interpreter Config
cfg -> do
      SInfo a
fi1 <- Config -> SInfo a -> [Integer] -> SolveM a (SInfo a)
forall a.
Loc a =>
Config -> SInfo a -> [Integer] -> SolveM a (SInfo a)
doInterpret Config
cfg SInfo a
fi (((Integer, a) -> Integer) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, a) -> Integer
forall a b. (a, b) -> a
fst ([(Integer, a)] -> [Integer]) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [Char] -> [(Integer, a)] -> [(Integer, a)]
forall a. [Char] -> a -> a
mytrace ([Char]
"before the Interpreter " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([(Integer, a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Integer, a)]
bads) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" constraints remain") [(Integer, a)]
bads)
      (Solution
s4, Result (Integer, a)
res1) <-  IBindEnv
-> (IBindEnv -> SolveM a (Solution, Result (Integer, a)))
-> SolveM a (Solution, Result (Integer, a))
forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv ((IBindEnv -> SolveM a (Solution, Result (Integer, a)))
 -> SolveM a (Solution, Result (Integer, a)))
-> (IBindEnv -> SolveM a (Solution, Result (Integer, a)))
-> SolveM a (Solution, Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt -> do
        Solution
s4    <- {- SCC "sol-refine" -} IBindEnv -> Solution -> Worklist a -> SolveM a Solution
forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s3 Worklist a
wkl
        Result (Integer, a)
res1  <- {- SCC "sol-result" -} IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg Worklist a
wkl Solution
s4
        (Solution, Result (Integer, a))
-> SolveM a (Solution, Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Solution
s4, Result (Integer, a)
res1)
      (SInfo a, Solution, Result (Integer, a))
-> StateT
     (SolverState a) IO (SInfo a, Solution, Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SInfo a
fi1, Solution
s4, Result (Integer, a)
res1)
    FixResult (Integer, a)
_ -> (SInfo a, Solution, Result (Integer, a))
-> StateT
     (SolverState a) IO (SInfo a, Solution, Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return  (SInfo a
fi, Solution
s3, [Char] -> Result (Integer, a) -> Result (Integer, a)
forall a. [Char] -> a -> a
mytrace [Char]
"all checked before interpreter" Result (Integer, a)
res0)

  Result (Integer, a)
res2  <- case Result (Integer, a) -> FixResult (Integer, a)
forall a. Result a -> FixResult a
resStatus Result (Integer, a)
res1 of  {- then run normal PLE on remaining unsolved constraints -}
    Unsafe Stats
_ [(Integer, a)]
bads2 | Bool -> Bool
not (Config -> Bool
noLazyPLE Config
cfg) Bool -> Bool -> Bool
&& Config -> Bool
rewriteAxioms Config
cfg -> do
      Config -> SInfo a -> [Integer] -> SolveM a ()
forall a. Loc a => Config -> SInfo a -> [Integer] -> SolveM a ()
doPLE Config
cfg SInfo a
fi1 (((Integer, a) -> Integer) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (Integer, a) -> Integer
forall a b. (a, b) -> a
fst ([(Integer, a)] -> [Integer]) -> [(Integer, a)] -> [Integer]
forall a b. (a -> b) -> a -> b
$ [Char] -> [(Integer, a)] -> [(Integer, a)]
forall a. [Char] -> a -> a
mytrace ([Char]
"before z3 PLE " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([(Integer, a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Integer, a)]
bads2) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" constraints remain") [(Integer, a)]
bads2)
      IBindEnv
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
F.emptyIBindEnv ((IBindEnv -> SolveM a (Result (Integer, a)))
 -> SolveM a (Result (Integer, a)))
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt -> do
        Solution
s5    <- {- SCC "sol-refine" -} IBindEnv -> Solution -> Worklist a -> SolveM a Solution
forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s4 Worklist a
wkl
        IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg Worklist a
wkl Solution
s5
    FixResult (Integer, a)
_ -> Result (Integer, a) -> SolveM a (Result (Integer, a))
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Integer, a) -> SolveM a (Result (Integer, a)))
-> Result (Integer, a) -> SolveM a (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ [Char] -> Result (Integer, a) -> Result (Integer, a)
forall a. [Char] -> a -> a
mytrace [Char]
"all checked with interpreter" Result (Integer, a)
res1

  Stats
st      <- SolveM a Stats
forall ann. SolveM ann Stats
stats
  let res3 :: Result (Integer, a)
res3 = {- SCC "sol-tidy" -} Result (Integer, a) -> Result (Integer, a)
forall a. Result a -> Result a
tidyResult Result (Integer, a)
res2
  (Result (Integer, a), Stats)
-> SolveM a (Result (Integer, a), Stats)
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Result (Integer, a), Stats)
 -> SolveM a (Result (Integer, a), Stats))
-> (Result (Integer, a), Stats)
-> SolveM a (Result (Integer, a), Stats)
forall a b. NFData a => (a -> b) -> a -> b
$!! (Result (Integer, a)
res3, Stats
st)


--------------------------------------------------------------------------------
-- | tidyResult ensures we replace the temporary kVarArg names introduced to
--   ensure uniqueness with the original names in the given WF constraints.
--------------------------------------------------------------------------------
tidyResult :: F.Result a -> F.Result a
tidyResult :: forall a. Result a -> Result a
tidyResult Result a
r = Result a
r
  { F.resSolution = tidySolution (F.resSolution r)
  , F.resNonCutsSolution = tidySolution (F.resNonCutsSolution r)
  }

tidySolution :: F.FixSolution -> F.FixSolution
tidySolution :: FixSolution -> FixSolution
tidySolution = (Pred -> Pred) -> FixSolution -> FixSolution
forall a b. (a -> b) -> HashMap KVar a -> HashMap KVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pred -> Pred
tidyPred

tidyPred :: F.Expr -> F.Expr
tidyPred :: Pred -> Pred
tidyPred = (Symbol -> Pred) -> Pred -> Pred
forall a. Subable a => (Symbol -> Pred) -> a -> a
F.substf (Symbol -> Pred
forall a. Symbolic a => a -> Pred
F.eVar (Symbol -> Pred) -> (Symbol -> Symbol) -> Symbol -> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
F.tidySymbol)

--------------------------------------------------------------------------------
{-# SCC refine #-}
refine
  :: (F.Loc a)
  => F.IBindEnv
  -> Sol.Solution
  -> W.Worklist a
  -> SolveM a Sol.Solution
--------------------------------------------------------------------------------
refine :: forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s Worklist a
w
  | Just (SimpC a
c, Worklist a
w', Bool
newScc, Int
rnk) <- Worklist a -> Maybe (SimpC a, Worklist a, Bool, Int)
forall a. Worklist a -> Maybe (SimpC a, Worklist a, Bool, Int)
W.pop Worklist a
w = do
     Int
i       <- Bool -> SolveM a Int
forall ann. Bool -> SolveM ann Int
tickIter Bool
newScc
     (Bool
b, Solution
s') <- IBindEnv -> Int -> Solution -> SimpC a -> SolveM a (Bool, Solution)
forall a.
Loc a =>
IBindEnv -> Int -> Solution -> SimpC a -> SolveM a (Bool, Solution)
refineC IBindEnv
bindingsInSmt Int
i Solution
s SimpC a
c
     IO () -> StateT (SolverState a) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (SolverState a) IO ())
-> IO () -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
writeLoud ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> SimpC a -> Bool -> Int -> [Char] -> [Char]
forall {t} {t} {t} {t} {c :: * -> *} {a} {a}.
(PrintfArg t, PrintfArg t, PrintfArg t, PrintfType t, TaggedC c a,
 Show a) =>
t -> c a -> a -> t -> t -> t
refineMsg Int
i SimpC a
c Bool
b Int
rnk (Solution -> [Char]
forall a. PPrint a => a -> [Char]
showpp Solution
s')
     let w'' :: Worklist a
w'' = if Bool
b then SimpC a -> Worklist a -> Worklist a
forall a. SimpC a -> Worklist a -> Worklist a
W.push SimpC a
c Worklist a
w' else Worklist a
w'
     IBindEnv -> Solution -> Worklist a -> SolveM a Solution
forall a.
Loc a =>
IBindEnv -> Solution -> Worklist a -> SolveM a Solution
refine IBindEnv
bindingsInSmt Solution
s' Worklist a
w''
  | Bool
otherwise = Solution -> SolveM a Solution
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Solution
s
  where
    -- DEBUG
    refineMsg :: t -> c a -> a -> t -> t -> t
refineMsg t
i c a
c a
b t
rnk t
s = [Char] -> t -> Integer -> [Char] -> t -> t -> t
forall r. PrintfType r => [Char] -> r
printf [Char]
"\niter=%d id=%d change=%s rank=%d s=%s\n"
                             t
i (c a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId c a
c) (a -> [Char]
forall a. Show a => a -> [Char]
show a
b) t
rnk t
s

---------------------------------------------------------------------------
-- | Single Step Refinement -----------------------------------------------
---------------------------------------------------------------------------
{-# SCC refineC #-}
refineC
  :: (F.Loc a)
  => F.IBindEnv
  -> Int
  -> Sol.Solution
  -> F.SimpC a
  -> SolveM a (Bool, Sol.Solution)
---------------------------------------------------------------------------
refineC :: forall a.
Loc a =>
IBindEnv -> Int -> Solution -> SimpC a -> SolveM a (Bool, Solution)
refineC IBindEnv
bindingsInSmt Int
_i Solution
s SimpC a
c =
  do ElabFlags
ef <- Context -> ElabFlags
T.ctxElabF (Context -> ElabFlags)
-> StateT (SolverState a) IO Context
-> StateT (SolverState a) IO ElabFlags
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (SolverState a) IO Context
forall ann. SolveM ann Context
getContext
     let ([KVar]
ks, Cand (KVar, EQual)
rhs) = Reader ElabFlags ([KVar], Cand (KVar, EQual))
-> ElabFlags -> ([KVar], Cand (KVar, EQual))
forall r a. Reader r a -> r -> a
runReader (Solution
-> SimpC a -> Reader ElabFlags ([KVar], Cand (KVar, EQual))
forall a.
Solution
-> SimpC a -> Reader ElabFlags ([KVar], Cand (KVar, EQual))
rhsCands Solution
s SimpC a
c) ElabFlags
ef
     if Cand (KVar, EQual) -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Cand (KVar, EQual)
rhs
        then (Bool, Solution) -> SolveM a (Bool, Solution)
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Solution
s)
        else do BindEnv a
be     <- SolveM a (BindEnv a)
forall ann. SolveM ann (BindEnv ann)
getBinds
                let lhs :: Pred
lhs = Reader ElabFlags Pred -> ElabFlags -> Pred
forall r a. Reader r a -> r -> a
runReader (IBindEnv
-> BindEnv a -> Solution -> SimpC a -> Reader ElabFlags Pred
forall a.
Loc a =>
IBindEnv
-> BindEnv a -> Solution -> SimpC a -> Reader ElabFlags Pred
S.lhsPred IBindEnv
bindingsInSmt (ElabFlags -> BindEnv a -> BindEnv a
forall a. ElabFlags -> BindEnv a -> BindEnv a
F.coerceBindEnv ElabFlags
ef BindEnv a
be) Solution
s SimpC a
c) ElabFlags
ef
                [(KVar, EQual)]
kqs    <- SrcSpan -> Pred -> Cand (KVar, EQual) -> SolveM a [(KVar, EQual)]
forall a ann. SrcSpan -> Pred -> Cand a -> SolveM ann [a]
filterValid (SimpC a -> SrcSpan
forall a. Loc a => SimpC a -> SrcSpan
cstrSpan SimpC a
c) Pred
lhs Cand (KVar, EQual)
rhs
                (Bool, Solution) -> SolveM a (Bool, Solution)
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return  ((Bool, Solution) -> SolveM a (Bool, Solution))
-> (Bool, Solution) -> SolveM a (Bool, Solution)
forall a b. (a -> b) -> a -> b
$ Solution -> [KVar] -> [(KVar, EQual)] -> (Bool, Solution)
forall a.
Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind)
S.update Solution
s [KVar]
ks [(KVar, EQual)]
kqs
  where
    _ci :: Integer
_ci       = SimpC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId SimpC a
c
    -- msg       = printf "refineC: iter = %d, sid = %s, soln = \n%s\n"
    --               _i (show (F.sid c)) (showpp s)
    _msg :: a -> t a -> t a -> t
_msg a
ks t a
xs t a
ys = [Char] -> Int -> [Char] -> [Char] -> Int -> Int -> t
forall r. PrintfType r => [Char] -> r
printf [Char]
"refineC: iter = %d, sid = %s, s = %s, rhs = %d, rhs' = %d \n"
                     Int
_i (Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
_ci) (a -> [Char]
forall a. PPrint a => a -> [Char]
showpp a
ks) (t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
xs) (t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ys)

rhsCands :: Sol.Solution -> F.SimpC a -> ElabM ([F.KVar], Sol.Cand (F.KVar, Sol.EQual))
rhsCands :: forall a.
Solution
-> SimpC a -> Reader ElabFlags ([KVar], Cand (KVar, EQual))
rhsCands Solution
s SimpC a
c    =
  do [Cand (KVar, EQual)]
pq <- ((KVar, Subst) -> ReaderT ElabFlags Identity (Cand (KVar, EQual)))
-> [(KVar, Subst)]
-> ReaderT ElabFlags Identity [Cand (KVar, EQual)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (KVar, Subst) -> ReaderT ElabFlags Identity (Cand (KVar, EQual))
cnd [(KVar, Subst)]
ks
     ([KVar], Cand (KVar, EQual))
-> Reader ElabFlags ([KVar], Cand (KVar, EQual))
forall a. a -> ReaderT ElabFlags Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((KVar, Subst) -> KVar
forall a b. (a, b) -> a
fst ((KVar, Subst) -> KVar) -> [(KVar, Subst)] -> [KVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(KVar, Subst)]
ks, [Cand (KVar, EQual)] -> Cand (KVar, EQual)
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Cand (KVar, EQual)]
pq)
  where
    cnd :: (F.KVar, F.Subst) -> ElabM [(F.Pred, (F.KVar, Sol.EQual))]
    cnd :: (KVar, Subst) -> ReaderT ElabFlags Identity (Cand (KVar, EQual))
cnd (KVar
k, Subst
su) = ((Pred, EQual) -> (Pred, (KVar, EQual)))
-> [(Pred, EQual)] -> Cand (KVar, EQual)
forall a b. (a -> b) -> [a] -> [b]
map (\(Pred
p , EQual
q) -> (Pred
p , (KVar
k , EQual
q))) ([(Pred, EQual)] -> Cand (KVar, EQual))
-> ReaderT ElabFlags Identity [(Pred, EQual)]
-> ReaderT ElabFlags Identity (Cand (KVar, EQual))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char]
-> Solution
-> Subst
-> QBind
-> ReaderT ElabFlags Identity [(Pred, EQual)]
forall a.
[Char]
-> Sol a QBind
-> Subst
-> QBind
-> ReaderT ElabFlags Identity [(Pred, EQual)]
Sol.qbPreds [Char]
msg Solution
s Subst
su (Solution -> KVar -> QBind
forall a. Sol a QBind -> KVar -> QBind
Sol.lookupQBind Solution
s KVar
k)
    ks :: [(KVar, Subst)]
ks          = Pred -> [(KVar, Subst)]
predKs (Pred -> [(KVar, Subst)])
-> (SimpC a -> Pred) -> SimpC a -> [(KVar, Subst)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> Pred
forall (c :: * -> *) a. TaggedC c a => c a -> Pred
F.crhs (SimpC a -> [(KVar, Subst)]) -> SimpC a -> [(KVar, Subst)]
forall a b. (a -> b) -> a -> b
$ SimpC a
c

    msg :: [Char]
msg         = [Char]
"rhsCands: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe Integer -> [Char]
forall a. Show a => a -> [Char]
show (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
F.sid SimpC a
c)

predKs :: F.Expr -> [(F.KVar, F.Subst)]
predKs :: Pred -> [(KVar, Subst)]
predKs (F.PAnd [Pred]
ps)    = (Pred -> [(KVar, Subst)]) -> [Pred] -> [(KVar, Subst)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Pred -> [(KVar, Subst)]
predKs [Pred]
ps
predKs (F.PKVar KVar
k Subst
su) = [(KVar
k, Subst
su)]
predKs Pred
_              = []

--------------------------------------------------------------------------------
-- | Convert Solution into Result ----------------------------------------------
--------------------------------------------------------------------------------
{-# SCC result #-}
result
  :: (F.Fixpoint a, F.Loc a, NFData a)
  => F.IBindEnv
  -> Config
  -> W.Worklist a
  -> Sol.Solution
  -> SolveM a (F.Result (Integer, a))
--------------------------------------------------------------------------------
result :: forall a.
(Fixpoint a, Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (Result (Integer, a))
result IBindEnv
bindingsInSmt Config
cfg Worklist a
wkl Solution
s =
  IBindEnv
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall ann a.
IBindEnv -> (IBindEnv -> SolveM ann a) -> SolveM ann a
sendConcreteBindingsToSMT IBindEnv
bindingsInSmt ((IBindEnv -> SolveM a (Result (Integer, a)))
 -> SolveM a (Result (Integer, a)))
-> (IBindEnv -> SolveM a (Result (Integer, a)))
-> SolveM a (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ \IBindEnv
bindingsInSmt2 -> do
    IO () -> StateT (SolverState a) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (SolverState a) IO ())
-> IO () -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
writeLoud [Char]
"Computing Result"
    FixResult (SimpC a)
stat    <- IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (FixResult (SimpC a))
forall a.
(Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (FixResult (SimpC a))
result_ IBindEnv
bindingsInSmt2 Config
cfg Worklist a
wkl Solution
s
    IO () -> StateT (SolverState a) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> StateT (SolverState a) IO ())
-> IO () -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"RESULT: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ FixResult (Maybe Integer) -> [Char]
forall a. Show a => a -> [Char]
show (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
F.sid (SimpC a -> Maybe Integer)
-> FixResult (SimpC a) -> FixResult (Maybe Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (SimpC a)
stat)

    FixResult (Integer, a)
-> FixSolution
-> FixSolution
-> GFixSolution
-> Result (Integer, a)
forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
F.Result (SimpC a -> (Integer, a)
forall {c :: * -> *} {b}. TaggedC c b => c b -> (Integer, b)
ci (SimpC a -> (Integer, a))
-> FixResult (SimpC a) -> FixResult (Integer, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FixResult (SimpC a)
stat) (FixSolution -> FixSolution -> GFixSolution -> Result (Integer, a))
-> StateT (SolverState a) IO FixSolution
-> StateT
     (SolverState a)
     IO
     (FixSolution -> GFixSolution -> Result (Integer, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config -> Solution -> StateT (SolverState a) IO FixSolution
forall ann. Config -> Solution -> SolveM ann FixSolution
solResult Config
cfg Solution
s StateT
  (SolverState a)
  IO
  (FixSolution -> GFixSolution -> Result (Integer, a))
-> StateT (SolverState a) IO FixSolution
-> StateT (SolverState a) IO (GFixSolution -> Result (Integer, a))
forall a b.
StateT (SolverState a) IO (a -> b)
-> StateT (SolverState a) IO a -> StateT (SolverState a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Solution -> StateT (SolverState a) IO FixSolution
forall ann. Solution -> SolveM ann FixSolution
solNonCutsResult Solution
s StateT (SolverState a) IO (GFixSolution -> Result (Integer, a))
-> StateT (SolverState a) IO GFixSolution
-> SolveM a (Result (Integer, a))
forall a b.
StateT (SolverState a) IO (a -> b)
-> StateT (SolverState a) IO a -> StateT (SolverState a) IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GFixSolution -> StateT (SolverState a) IO GFixSolution
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return GFixSolution
forall a. Monoid a => a
mempty
  where
    ci :: c b -> (Integer, b)
ci c b
c = (c b -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId c b
c, c b -> b
forall (c :: * -> *) a. TaggedC c a => c a -> a
F.sinfo c b
c)

solResult :: Config -> Sol.Solution -> SolveM ann (M.HashMap F.KVar F.Expr)
solResult :: forall ann. Config -> Solution -> SolveM ann FixSolution
solResult Config
cfg = Config -> FixSolution -> SolveM ann FixSolution
forall ann. Config -> FixSolution -> SolveM ann FixSolution
minimizeResult Config
cfg (FixSolution -> SolveM ann FixSolution)
-> (Solution -> FixSolution) -> Solution -> SolveM ann FixSolution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Solution -> FixSolution
forall a. Sol a QBind -> FixSolution
Sol.result

solNonCutsResult :: Sol.Solution -> SolveM ann (M.HashMap F.KVar F.Expr)
solNonCutsResult :: forall ann. Solution -> SolveM ann FixSolution
solNonCutsResult Solution
s = do
  BindEnv ann
be <- SolveM ann (BindEnv ann)
forall ann. SolveM ann (BindEnv ann)
getBinds
  ElabFlags
ef <- Context -> ElabFlags
T.ctxElabF (Context -> ElabFlags)
-> StateT (SolverState ann) IO Context
-> StateT (SolverState ann) IO ElabFlags
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (SolverState ann) IO Context
forall ann. SolveM ann Context
getContext
  FixSolution -> SolveM ann FixSolution
forall a. a -> StateT (SolverState ann) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FixSolution -> SolveM ann FixSolution)
-> FixSolution -> SolveM ann FixSolution
forall a b. (a -> b) -> a -> b
$ Reader ElabFlags FixSolution -> ElabFlags -> FixSolution
forall r a. Reader r a -> r -> a
runReader (BindEnv ann -> Solution -> Reader ElabFlags FixSolution
forall ann a.
BindEnv ann -> Sol a QBind -> Reader ElabFlags FixSolution
S.nonCutsResult BindEnv ann
be Solution
s) ElabFlags
ef

result_
  :: (F.Loc a, NFData a)
  => F.IBindEnv
  -> Config
  -> W.Worklist a
  -> Sol.Solution
  -> SolveM a (F.FixResult (F.SimpC a))
result_ :: forall a.
(Loc a, NFData a) =>
IBindEnv
-> Config
-> Worklist a
-> Solution
-> SolveM a (FixResult (SimpC a))
result_ IBindEnv
bindingsInSmt Config
cfg Worklist a
w Solution
s = do
  [SimpC a]
filtered <- (SimpC a -> StateT (SolverState a) IO Bool)
-> [SimpC a] -> StateT (SolverState a) IO [SimpC a]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (IBindEnv -> Solution -> SimpC a -> StateT (SolverState a) IO Bool
forall a.
(Loc a, NFData a) =>
IBindEnv -> Solution -> SimpC a -> SolveM a Bool
isUnsat IBindEnv
bindingsInSmt Solution
s) [SimpC a]
cs
  Stats
sts      <- SolveM a Stats
forall ann. SolveM ann Stats
stats
  FixResult (SimpC a) -> SolveM a (FixResult (SimpC a))
forall a. a -> StateT (SolverState a) IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FixResult (SimpC a) -> SolveM a (FixResult (SimpC a)))
-> FixResult (SimpC a) -> SolveM a (FixResult (SimpC a))
forall a b. (a -> b) -> a -> b
$ Stats -> [SimpC a] -> FixResult (SimpC a)
forall {a}. Stats -> [a] -> FixResult a
res Stats
sts [SimpC a]
filtered
  where
    cs :: [SimpC a]
cs          = Config -> [SimpC a] -> [SimpC a]
forall a. Config -> [SimpC a] -> [SimpC a]
isChecked Config
cfg (Worklist a -> [SimpC a]
forall a. Worklist a -> [SimpC a]
W.unsatCandidates Worklist a
w)
    res :: Stats -> [a] -> FixResult a
res Stats
sts []  = Stats -> FixResult a
forall a. Stats -> FixResult a
F.Safe Stats
sts
    res Stats
sts [a]
cs' = Stats -> [a] -> FixResult a
forall {a}. Stats -> [a] -> FixResult a
F.Unsafe Stats
sts [a]
cs'

isChecked :: Config -> [F.SimpC a] -> [F.SimpC a]
isChecked :: forall a. Config -> [SimpC a] -> [SimpC a]
isChecked Config
cfg [SimpC a]
cs = case Config -> [Integer]
checkCstr Config
cfg of
  []   -> [SimpC a]
cs
  [Integer]
ids  -> let s :: HashSet Integer
s = [Integer] -> HashSet Integer
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Integer]
ids in
          [SimpC a
c | SimpC a
c <- [SimpC a]
cs, Integer -> HashSet Integer -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (SimpC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId SimpC a
c) HashSet Integer
s ]

--------------------------------------------------------------------------------
-- | `minimizeResult` transforms each KVar's result by removing
--   conjuncts that are implied by others. That is,
--
--      minimizeConjuncts :: ps:[Pred] -> {qs:[Pred] | subset qs ps}
--
--   such that `minimizeConjuncts ps` is a minimal subset of ps where no
--   is implied by /\_{q' in qs \ qs}
--   see: tests/pos/min00.fq for an example.
--------------------------------------------------------------------------------
minimizeResult :: Config -> M.HashMap F.KVar F.Expr
               -> SolveM ann (M.HashMap F.KVar F.Expr)
--------------------------------------------------------------------------------
minimizeResult :: forall ann. Config -> FixSolution -> SolveM ann FixSolution
minimizeResult Config
cfg FixSolution
s
  | Config -> Bool
minimalSol Config
cfg = (Pred -> StateT (SolverState ann) IO Pred)
-> FixSolution -> StateT (SolverState ann) IO FixSolution
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> HashMap KVar a -> m (HashMap KVar b)
mapM Pred -> StateT (SolverState ann) IO Pred
forall ann. Pred -> SolveM ann Pred
minimizeConjuncts FixSolution
s
  | Bool
otherwise      = FixSolution -> StateT (SolverState ann) IO FixSolution
forall a. a -> StateT (SolverState ann) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FixSolution
s

minimizeConjuncts :: F.Expr -> SolveM ann F.Expr
minimizeConjuncts :: forall ann. Pred -> SolveM ann Pred
minimizeConjuncts Pred
p = [Pred] -> Pred
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd ([Pred] -> Pred)
-> StateT (SolverState ann) IO [Pred]
-> StateT (SolverState ann) IO Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
forall {ann}.
[Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go (Pred -> [Pred]
forall v. Eq v => ExprV v -> [ExprV v]
F.conjuncts Pred
p) []
  where
    go :: [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go []     [Pred]
acc   = [Pred] -> StateT (SolverState ann) IO [Pred]
forall a. a -> StateT (SolverState ann) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Pred]
acc
    go (Pred
p:[Pred]
ps) [Pred]
acc   = do Bool
b <- SrcSpan -> Pred -> Pred -> SolveM ann Bool
forall ann. SrcSpan -> Pred -> Pred -> SolveM ann Bool
isValid SrcSpan
F.dummySpan ([Pred] -> Pred
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
F.pAnd ([Pred]
acc [Pred] -> [Pred] -> [Pred]
forall a. [a] -> [a] -> [a]
++ [Pred]
ps)) Pred
p
                         if Bool
b then [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go [Pred]
ps [Pred]
acc
                              else [Pred] -> [Pred] -> StateT (SolverState ann) IO [Pred]
go [Pred]
ps (Pred
pPred -> [Pred] -> [Pred]
forall a. a -> [a] -> [a]
:[Pred]
acc)

--------------------------------------------------------------------------------
isUnsat
  :: (F.Loc a, NFData a) => F.IBindEnv -> Sol.Solution -> F.SimpC a -> SolveM a Bool
--------------------------------------------------------------------------------
isUnsat :: forall a.
(Loc a, NFData a) =>
IBindEnv -> Solution -> SimpC a -> SolveM a Bool
isUnsat IBindEnv
bindingsInSmt Solution
s SimpC a
c = do
  -- lift   $ printf "isUnsat %s" (show (F.subcId c))
  Int
_     <- Bool -> SolveM a Int
forall ann. Bool -> SolveM ann Int
tickIter Bool
True -- newScc
  BindEnv a
be    <- SolveM a (BindEnv a)
forall ann. SolveM ann (BindEnv ann)
getBinds
  ElabFlags
ef <- Context -> ElabFlags
T.ctxElabF (Context -> ElabFlags)
-> StateT (SolverState a) IO Context
-> StateT (SolverState a) IO ElabFlags
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (SolverState a) IO Context
forall ann. SolveM ann Context
getContext
  let lp :: Pred
lp = Reader ElabFlags Pred -> ElabFlags -> Pred
forall r a. Reader r a -> r -> a
runReader (IBindEnv
-> BindEnv a -> Solution -> SimpC a -> Reader ElabFlags Pred
forall a.
Loc a =>
IBindEnv
-> BindEnv a -> Solution -> SimpC a -> Reader ElabFlags Pred
S.lhsPred IBindEnv
bindingsInSmt (ElabFlags -> BindEnv a -> BindEnv a
forall a. ElabFlags -> BindEnv a -> BindEnv a
F.coerceBindEnv ElabFlags
ef BindEnv a
be) Solution
s SimpC a
c) ElabFlags
ef
  let rp :: Pred
rp = SimpC a -> Pred
forall a. SimpC a -> Pred
rhsPred        SimpC a
c
  Bool
res   <- Bool -> Bool
not (Bool -> Bool) -> SolveM a Bool -> SolveM a Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> Pred -> Pred -> SolveM a Bool
forall ann. SrcSpan -> Pred -> Pred -> SolveM ann Bool
isValid (SimpC a -> SrcSpan
forall a. Loc a => SimpC a -> SrcSpan
cstrSpan SimpC a
c) Pred
lp Pred
rp
  IO () -> StateT (SolverState a) IO ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (SolverState a) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift   (IO () -> StateT (SolverState a) IO ())
-> IO () -> StateT (SolverState a) IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Pred -> Pred -> IO ()
showUnsat Bool
res (SimpC a -> Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Integer
F.subcId SimpC a
c) Pred
lp Pred
rp
  Bool -> SolveM a Bool
forall a. a -> StateT (SolverState a) IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
res

showUnsat :: Bool -> Integer -> F.Pred -> F.Pred -> IO ()
showUnsat :: Bool -> Integer -> Pred -> Pred -> IO ()
showUnsat Bool
u Integer
i Pred
lP Pred
rP = {- when u $ -} do
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf   [Char]
"UNSAT id %s %s" (Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
i) (Bool -> [Char]
forall a. Show a => a -> [Char]
show Bool
u)
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. PPrint a => a -> [Char]
showpp (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ Doc
"LHS:" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. PPrint a => a -> Doc
pprint Pred
lP
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
forall a. PPrint a => a -> [Char]
showpp (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ Doc
"RHS:" Doc -> Doc -> Doc
<+> Pred -> Doc
forall a. PPrint a => a -> Doc
pprint Pred
rP

--------------------------------------------------------------------------------
-- | Predicate corresponding to RHS of constraint in current solution
--------------------------------------------------------------------------------
rhsPred :: F.SimpC a -> F.Expr
--------------------------------------------------------------------------------
rhsPred :: forall a. SimpC a -> Pred
rhsPred SimpC a
c
  | SimpC a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c = SimpC a -> Pred
forall (c :: * -> *) a. TaggedC c a => c a -> Pred
F.crhs SimpC a
c
  | Bool
otherwise  = [Char] -> Pred
forall a. (?callStack::CallStack) => [Char] -> a
errorstar ([Char] -> Pred) -> [Char] -> Pred
forall a b. (a -> b) -> a -> b
$ [Char]
"rhsPred on non-target: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe Integer -> [Char]
forall a. Show a => a -> [Char]
show (SimpC a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
F.sid SimpC a
c)

--------------------------------------------------------------------------------
isValid :: F.SrcSpan -> F.Expr -> F.Expr -> SolveM ann Bool
--------------------------------------------------------------------------------
isValid :: forall ann. SrcSpan -> Pred -> Pred -> SolveM ann Bool
isValid SrcSpan
sp Pred
p Pred
q = Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([()] -> Bool)
-> StateT (SolverState ann) IO [()]
-> StateT (SolverState ann) IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SrcSpan -> Pred -> Cand () -> StateT (SolverState ann) IO [()]
forall a ann. SrcSpan -> Pred -> Cand a -> SolveM ann [a]
filterValid SrcSpan
sp Pred
p [(Pred
q, ())]

cstrSpan :: (F.Loc a) => F.SimpC a -> F.SrcSpan
cstrSpan :: forall a. Loc a => SimpC a -> SrcSpan
cstrSpan = a -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan (a -> SrcSpan) -> (SimpC a -> a) -> SimpC a -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
F.sinfo

{-
---------------------------------------------------------------------------
donePhase' :: String -> SolveM ()
---------------------------------------------------------------------------
donePhase' msg = lift $ do
  threadDelay 25000
  putBlankLn
  donePhase Loud msg
-}


-- NV TODO Move to a new file
-------------------------------------------------------------------------------
-- | Interaction with the user when Solving -----------------------------------
-------------------------------------------------------------------------------

_iMergePartitions :: [(Int, F.SInfo a)] -> IO [(Int, F.SInfo a)]
_iMergePartitions :: forall a. [(Int, SInfo a)] -> IO [(Int, SInfo a)]
_iMergePartitions [(Int, SInfo a)]
ifis = do
  [Char] -> IO ()
putStrLn [Char]
"Current Partitions are: "
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ((Int, SInfo a) -> [Char]
forall a. (Int, SInfo a) -> [Char]
partitionInfo ((Int, SInfo a) -> [Char]) -> [(Int, SInfo a)] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, SInfo a)]
ifis)
  [Char] -> IO ()
putStrLn [Char]
"Merge Partitions? Y/N"
  Char
c <- IO Char
getChar
  if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'N'
    then do [Char] -> IO ()
putStrLn [Char]
"Solving Partitions"
            [(Int, SInfo a)] -> IO [(Int, SInfo a)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, SInfo a)]
ifis
    else do
      (Int
i, Int
j) <- Int -> IO (Int, Int)
getMergePartition ([(Int, SInfo a)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, SInfo a)]
ifis)
      [(Int, SInfo a)] -> IO [(Int, SInfo a)]
forall a. [(Int, SInfo a)] -> IO [(Int, SInfo a)]
_iMergePartitions (Int -> Int -> [(Int, SInfo a)] -> [(Int, SInfo a)]
forall a. Int -> Int -> [(Int, SInfo a)] -> [(Int, SInfo a)]
mergePartitions Int
i Int
j [(Int, SInfo a)]
ifis)

getMergePartition :: Int -> IO (Int, Int)
getMergePartition :: Int -> IO (Int, Int)
getMergePartition Int
n = do
  [Char] -> IO ()
putStrLn [Char]
"Which two partition to merge? (i, j)"
  [Char]
ic <- IO [Char]
getLine
  let (Int
i,Int
j) = [Char] -> (Int, Int)
forall a. Read a => [Char] -> a
read [Char]
ic :: (Int, Int)
  if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
i Bool -> Bool -> Bool
|| Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j
    then do [Char] -> IO ()
putStrLn ([Char]
"Invalid Partition numbers, write (i,j) with 1 <= i <= " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
            Int -> IO (Int, Int)
getMergePartition Int
n
    else (Int, Int) -> IO (Int, Int)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i,Int
j)

mergePartitions :: Int -> Int -> [(Int, F.SInfo a)] -> [(Int, F.SInfo a)]
mergePartitions :: forall a. Int -> Int -> [(Int, SInfo a)] -> [(Int, SInfo a)]
mergePartitions Int
i Int
j [(Int, SInfo a)]
fis
  = [Int] -> [SInfo a] -> [(Int, SInfo a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] ((Int -> SInfo a
takei Int
i SInfo a -> SInfo a -> SInfo a
forall a. Monoid a => a -> a -> a
`mappend` (Int -> SInfo a
takei Int
j){F.bs = mempty})SInfo a -> [SInfo a] -> [SInfo a]
forall a. a -> [a] -> [a]
:[SInfo a]
rest)
  where
    takei :: Int -> SInfo a
takei Int
i = (Int, SInfo a) -> SInfo a
forall a b. (a, b) -> b
snd ([(Int, SInfo a)]
fis [(Int, SInfo a)] -> Int -> (Int, SInfo a)
forall a. (?callStack::CallStack) => [a] -> Int -> a
L.!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
    rest :: [SInfo a]
rest = (Int, SInfo a) -> SInfo a
forall a b. (a, b) -> b
snd ((Int, SInfo a) -> SInfo a) -> [(Int, SInfo a)] -> [SInfo a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, SInfo a) -> Bool) -> [(Int, SInfo a)] -> [(Int, SInfo a)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
k,SInfo a
_) -> Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
i Bool -> Bool -> Bool
&& Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j) [(Int, SInfo a)]
fis

partitionInfo :: (Int, F.SInfo a) -> String
partitionInfo :: forall a. (Int, SInfo a) -> [Char]
partitionInfo (Int
i, SInfo a
fi)
  = [Char]
"Partition number " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
    [Char]
"Defined ?? " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [SrcSpan] -> [Char]
forall a. Show a => a -> [Char]
show [SrcSpan]
defs    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
    [Char]
"Used ?? "    [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Maybe SrcSpan] -> [Char]
forall a. Show a => a -> [Char]
show [Maybe SrcSpan]
uses
  where
    gs :: [GradInfo]
gs   = WfC a -> GradInfo
forall a. WfC a -> GradInfo
F.wloc (WfC a -> GradInfo)
-> ((KVar, WfC a) -> WfC a) -> (KVar, WfC a) -> GradInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar, WfC a) -> WfC a
forall a b. (a, b) -> b
snd ((KVar, WfC a) -> GradInfo) -> [(KVar, WfC a)] -> [GradInfo]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((KVar, WfC a) -> Bool) -> [(KVar, WfC a)] -> [(KVar, WfC a)]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (WfC a -> Bool
forall a. WfC a -> Bool
F.isGWfc (WfC a -> Bool)
-> ((KVar, WfC a) -> WfC a) -> (KVar, WfC a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KVar, WfC a) -> WfC a
forall a b. (a, b) -> b
snd) (HashMap KVar (WfC a) -> [(KVar, WfC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
fi))
    defs :: [SrcSpan]
defs = [SrcSpan] -> [SrcSpan]
forall a. Eq a => [a] -> [a]
L.nub (GradInfo -> SrcSpan
F.gsrc (GradInfo -> SrcSpan) -> [GradInfo] -> [SrcSpan]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GradInfo]
gs)
    uses :: [Maybe SrcSpan]
uses = [Maybe SrcSpan] -> [Maybe SrcSpan]
forall a. Eq a => [a] -> [a]
L.nub (GradInfo -> Maybe SrcSpan
F.gused (GradInfo -> Maybe SrcSpan) -> [GradInfo] -> [Maybe SrcSpan]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GradInfo]
gs)