{-# LANGUAGE CPP                #-}
{-# LANGUAGE FlexibleInstances  #-}

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

module Language.Fixpoint.Solver.GradualSolution
  ( -- * Create Initial Solution
    init
  ) where

import           Control.Parallel.Strategies
import qualified Data.HashMap.Strict            as M
import qualified Data.List                      as L
import           Data.Maybe                     (maybeToList, isNothing)
import           Language.Fixpoint.Types.Config
import           Language.Fixpoint.Types.PrettyPrint ()
import qualified Language.Fixpoint.SortCheck          as So
import           Language.Fixpoint.Misc
import qualified Language.Fixpoint.Types              as F
import qualified Language.Fixpoint.Types.Solutions    as Sol
import           Language.Fixpoint.Types.Constraints  hiding (ws, bs)
import           Prelude                              hiding (init, lookup)
import           Language.Fixpoint.Solver.Sanitize  (symbolEnv)
import Language.Fixpoint.SortCheck

--------------------------------------------------------------------------------
-- | Initial Gradual Solution (from Qualifiers and WF constraints) -------------
--------------------------------------------------------------------------------
init :: (F.Fixpoint a) => Config -> F.SInfo a -> [(F.KVar, (F.GWInfo, [F.Expr]))]
--------------------------------------------------------------------------------
init :: forall a.
Fixpoint a =>
Config -> SInfo a -> [(KVar, (GWInfo, [Expr]))]
init Config
cfg SInfo a
si = forall a b. (a -> b) -> [a] -> [b]
map (forall {f :: * -> *} {b} {a}.
(Functor f, Elaborate b) =>
(a, (GWInfo, f b)) -> (a, (GWInfo, f b))
elab forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
SInfo a
-> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, (GWInfo, [Expr]))
refineG SInfo a
si [Qualifier]
qs SEnv Sort
genv) [WfC a]
gs forall a. a -> Strategy a -> a
`using` forall a. Strategy a -> Strategy [a]
parList forall a. NFData a => Strategy a
rdeepseq
  where
    qs :: [Qualifier]
qs         = forall (c :: * -> *) a. GInfo c a -> [Qualifier]
F.quals SInfo a
si
    gs :: [WfC a]
gs         = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(KVar, WfC a)]
gs0
    genv :: SEnv Sort
genv       = forall a. SInfo a -> SEnv Sort
instConstants SInfo a
si

    gs0 :: [(KVar, WfC a)]
gs0        = forall a. (a -> Bool) -> [a] -> [a]
L.filter (forall a. WfC a -> Bool
isGWfc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [(k, v)]
M.toList (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
F.ws SInfo a
si)

    elab :: (a, (GWInfo, f b)) -> (a, (GWInfo, f b))
elab (a
k, (GWInfo
x,f b
es)) = (a
k, (GWInfo
x, forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (forall l b. Loc l => l -> b -> Located b
F.atLoc SrcSpan
F.dummySpan String
"init") (Symbol -> Sort -> SymEnv
sEnv (GWInfo -> Symbol
gsym GWInfo
x) (GWInfo -> Sort
gsort GWInfo
x)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b
es))

    sEnv :: Symbol -> Sort -> SymEnv
sEnv Symbol
x Sort
s    = SymEnv
isEnv {seSort :: SEnv Sort
F.seSort = forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
x Sort
s (SymEnv -> SEnv Sort
F.seSort SymEnv
isEnv)}
    isEnv :: SymEnv
isEnv       = forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si


--------------------------------------------------------------------------------
refineG :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, (F.GWInfo, [F.Expr]))
refineG :: forall a.
SInfo a
-> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, (GWInfo, [Expr]))
refineG SInfo a
fi [Qualifier]
qs SEnv Sort
genv WfC a
w = (KVar
k, (forall a. WfC a -> GWInfo
F.gwInfo WfC a
w, QBind -> [Expr]
Sol.qbExprs QBind
qb))
  where
    (KVar
k, QBind
qb) = forall a.
SInfo a -> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, QBind)
refine SInfo a
fi [Qualifier]
qs SEnv Sort
genv WfC a
w

refine :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)
refine :: forall a.
SInfo a -> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, QBind)
refine SInfo a
fi [Qualifier]
qs SEnv Sort
genv WfC a
w = Bool
-> SEnv Sort
-> [Qualifier]
-> (Symbol, Sort, KVar)
-> (KVar, QBind)
refineK (forall (c :: * -> *) a. GInfo c a -> Bool
allowHOquals SInfo a
fi) SEnv Sort
env [Qualifier]
qs forall a b. (a -> b) -> a -> b
$ forall a. WfC a -> (Symbol, Sort, KVar)
F.wrft WfC a
w
  where
    env :: SEnv Sort
env             = SEnv Sort
wenv forall a. Semigroup a => a -> a -> a
<> SEnv Sort
genv
    wenv :: SEnv Sort
wenv            = SortedReft -> Sort
F.sr_sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv (forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (forall (c :: * -> *) a. GInfo c a -> BindEnv a
F.bs SInfo a
fi) (forall a. WfC a -> IBindEnv
F.wenv WfC a
w))

instConstants :: F.SInfo a -> F.SEnv F.Sort
instConstants :: forall a. SInfo a -> SEnv Sort
instConstants = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter forall {b}. (Symbol, b) -> Bool
notLit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits
  where
    notLit :: (Symbol, b) -> Bool
notLit    = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
F.isLitSymbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst


refineK :: Bool -> F.SEnv F.Sort -> [F.Qualifier] -> (F.Symbol, F.Sort, F.KVar) -> (F.KVar, Sol.QBind)
refineK :: Bool
-> SEnv Sort
-> [Qualifier]
-> (Symbol, Sort, KVar)
-> (KVar, QBind)
refineK Bool
ho SEnv Sort
env [Qualifier]
qs (Symbol
v, Sort
t, KVar
k) = (KVar
k, QBind
eqs')
   where
    eqs :: QBind
eqs                     = Bool -> SEnv Sort -> Symbol -> Sort -> [Qualifier] -> QBind
instK Bool
ho SEnv Sort
env Symbol
v Sort
t [Qualifier]
qs
    eqs' :: QBind
eqs'                    = (EQual -> Bool) -> QBind -> QBind
Sol.qbFilter (SEnv Sort -> Symbol -> Sort -> EQual -> Bool
okInst SEnv Sort
env Symbol
v Sort
t) QBind
eqs

--------------------------------------------------------------------------------
instK :: Bool
      -> F.SEnv F.Sort
      -> F.Symbol
      -> F.Sort
      -> [F.Qualifier]
      -> Sol.QBind
--------------------------------------------------------------------------------
instK :: Bool -> SEnv Sort -> Symbol -> Sort -> [Qualifier] -> QBind
instK Bool
ho SEnv Sort
env Symbol
v Sort
t = [EQual] -> QBind
Sol.qb forall b c a. (b -> c) -> (a -> b) -> a -> c
. [EQual] -> [EQual]
unique forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> SEnv Sort -> Symbol -> Sort -> Qualifier -> [EQual]
instKQ Bool
ho SEnv Sort
env Symbol
v Sort
t)
  where
    unique :: [EQual] -> [EQual]
unique       = forall a. (a -> a -> Bool) -> [a] -> [a]
L.nubBy ((forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> Expr
Sol.eqPred) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> Expr
Sol.eqPred)

instKQ :: Bool
       -> F.SEnv F.Sort
       -> F.Symbol
       -> F.Sort
       -> F.Qualifier
       -> [Sol.EQual]
instKQ :: Bool -> SEnv Sort -> Symbol -> Sort -> Qualifier -> [EQual]
instKQ Bool
ho SEnv Sort
env Symbol
v Sort
t Qualifier
q =
  case QualParam -> Sort
qpSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualifier -> [QualParam]
F.qParams Qualifier
q of
    (Sort
qt:[Sort]
qts) -> do
        (TVSubst
su0, Symbol
v0) <- Env -> [(Sort, [Symbol])] -> Sort -> [(TVSubst, Symbol)]
candidates Env
senv [(Sort
t, [Symbol
v])] Sort
qt
        [Symbol]
xs        <- Env -> [(Sort, [Symbol])] -> [Symbol] -> [Sort] -> [[Symbol]]
match Env
senv [(Sort, [Symbol])]
tyss [Symbol
v0] (TVSubst -> Sort -> Sort
So.apply TVSubst
su0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
qts)
        forall (m :: * -> *) a. Monad m => a -> m a
return     forall a b. (a -> b) -> a -> b
$ Qualifier -> [Symbol] -> EQual
Sol.eQual Qualifier
q (forall a. [a] -> [a]
reverse [Symbol]
xs)
      where
        tyss :: [(Sort, [Symbol])]
tyss       = Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env
        senv :: Env
senv       = (forall a. Symbol -> SEnv a -> SESearch a
`F.lookupSEnvWithDistance` SEnv Sort
env)
    [] -> forall a. HasCallStack => String -> a
error String
"Empty qpSort of qParams q"

instCands :: Bool -> F.SEnv F.Sort -> [(F.Sort, [F.Symbol])]
instCands :: Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env = forall a. (a -> Bool) -> [a] -> [a]
filter forall {b}. (Sort, b) -> Bool
isOk [(Sort, [Symbol])]
tyss
  where
    tyss :: [(Sort, [Symbol])]
tyss      = forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
groupList [(Sort
t, Symbol
x) | (Symbol
x, Sort
t) <- [(Symbol, Sort)]
xts]
    isOk :: (Sort, b) -> Bool
isOk      = if Bool
ho then forall a b. a -> b -> a
const Bool
True else forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe ([Int], [Sort], Sort)
F.functionSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
    xts :: [(Symbol, Sort)]
xts       = forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv SEnv Sort
env

match :: So.Env -> [(F.Sort, [F.Symbol])] -> [F.Symbol] -> [F.Sort] -> [[F.Symbol]]
match :: Env -> [(Sort, [Symbol])] -> [Symbol] -> [Sort] -> [[Symbol]]
match Env
env [(Sort, [Symbol])]
tyss [Symbol]
xs (Sort
t : [Sort]
ts)
  = do (TVSubst
su, Symbol
x) <- Env -> [(Sort, [Symbol])] -> Sort -> [(TVSubst, Symbol)]
candidates Env
env [(Sort, [Symbol])]
tyss Sort
t
       Env -> [(Sort, [Symbol])] -> [Symbol] -> [Sort] -> [[Symbol]]
match Env
env [(Sort, [Symbol])]
tyss (Symbol
x forall a. a -> [a] -> [a]
: [Symbol]
xs) (TVSubst -> Sort -> Sort
So.apply TVSubst
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts)
match Env
_   [(Sort, [Symbol])]
_   [Symbol]
xs []
  = forall (m :: * -> *) a. Monad m => a -> m a
return [Symbol]
xs

--------------------------------------------------------------------------------
candidates :: So.Env -> [(F.Sort, [F.Symbol])] -> F.Sort -> [(So.TVSubst, F.Symbol)]
--------------------------------------------------------------------------------
candidates :: Env -> [(Sort, [Symbol])] -> Sort -> [(TVSubst, Symbol)]
candidates Env
env [(Sort, [Symbol])]
tyss Sort
tx =
    [(TVSubst
su, Symbol
y) | (Sort
t, [Symbol]
ys) <- [(Sort, [Symbol])]
tyss
             , TVSubst
su      <- forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ Bool -> Env -> Sort -> Sort -> Maybe TVSubst
So.unifyFast Bool
mono Env
env Sort
tx Sort
t
             , Symbol
y       <- [Symbol]
ys                                   ]
  where
    mono :: Bool
mono = Sort -> Bool
So.isMono Sort
tx

--------------------------------------------------------------------------------
okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool
--------------------------------------------------------------------------------
okInst :: SEnv Sort -> Symbol -> Sort -> EQual -> Bool
okInst SEnv Sort
env Symbol
v Sort
t EQual
eq = forall a. Maybe a -> Bool
isNothing Maybe Doc
tc
  where
    sr :: SortedReft
sr            = Sort -> Reft -> SortedReft
F.RR Sort
t ((Symbol, Expr) -> Reft
F.Reft (Symbol
v, Expr
p))
    p :: Expr
p             = EQual -> Expr
Sol.eqPred EQual
eq
    tc :: Maybe Doc
tc            = forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
So.checkSorted SrcSpan
F.dummySpan SEnv Sort
env SortedReft
sr