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

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)
#if !MIN_VERSION_base(4,14,0)
import           Data.Monoid                    ((<>))
#endif
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 :: Config -> SInfo a -> [(KVar, (GWInfo, [Expr]))]
init Config
cfg SInfo a
si = (WfC a -> (KVar, (GWInfo, [Expr])))
-> [WfC a] -> [(KVar, (GWInfo, [Expr]))]
forall a b. (a -> b) -> [a] -> [b]
map ((KVar, (GWInfo, [Expr])) -> (KVar, (GWInfo, [Expr]))
forall (f :: * -> *) b t.
(Functor f, Elaborate b) =>
(t, (GWInfo, f b)) -> (t, (GWInfo, f b))
elab ((KVar, (GWInfo, [Expr])) -> (KVar, (GWInfo, [Expr])))
-> (WfC a -> (KVar, (GWInfo, [Expr])))
-> WfC a
-> (KVar, (GWInfo, [Expr]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a
-> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, (GWInfo, [Expr]))
forall a.
SInfo a
-> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, (GWInfo, [Expr]))
refineG SInfo a
si [Qualifier]
qs SEnv Sort
genv) [WfC a]
gs [(KVar, (GWInfo, [Expr]))]
-> Strategy [(KVar, (GWInfo, [Expr]))]
-> [(KVar, (GWInfo, [Expr]))]
forall a. a -> Strategy a -> a
`using` Strategy (KVar, (GWInfo, [Expr]))
-> Strategy [(KVar, (GWInfo, [Expr]))]
forall a. Strategy a -> Strategy [a]
parList Strategy (KVar, (GWInfo, [Expr]))
forall a. NFData a => Strategy a
rdeepseq 
  where
    qs :: [Qualifier]
qs         = SInfo a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
F.quals SInfo a
si
    gs :: [WfC a]
gs         = (KVar, WfC a) -> WfC a
forall a b. (a, b) -> b
snd ((KVar, WfC a) -> WfC a) -> [(KVar, WfC a)] -> [WfC a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(KVar, WfC a)]
gs0
    genv :: SEnv Sort
genv       = SInfo a -> SEnv Sort
forall a. SInfo a -> SEnv Sort
instConstants SInfo a
si

    gs0 :: [(KVar, WfC a)]
gs0        = ((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
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) ([(KVar, WfC a)] -> [(KVar, WfC a)])
-> [(KVar, WfC a)] -> [(KVar, WfC a)]
forall a b. (a -> b) -> a -> b
$ 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
si)

    elab :: (t, (GWInfo, f b)) -> (t, (GWInfo, f b))
elab (t
k,(GWInfo
x,f b
es)) = ((t
k,) ((GWInfo, f b) -> (t, (GWInfo, f b)))
-> (f b -> (GWInfo, f b)) -> f b -> (t, (GWInfo, f b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GWInfo
x,)) (f b -> (t, (GWInfo, f b))) -> f b -> (t, (GWInfo, f b))
forall a b. (a -> b) -> a -> b
$ (Located String -> SymEnv -> b -> b
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (SrcSpan -> String -> Located String
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)) (b -> b) -> f b -> f b
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 = Symbol -> Sort -> SEnv Sort -> SEnv Sort
forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
x Sort
s (SymEnv -> SEnv Sort
F.seSort SymEnv
isEnv)}
    isEnv :: SymEnv
isEnv       = Config -> SInfo a -> SymEnv
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 :: SInfo a
-> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, (GWInfo, [Expr]))
refineG SInfo a
fi [Qualifier]
qs SEnv Sort
genv WfC a
w = (KVar
k, (WfC a -> GWInfo
forall a. WfC a -> GWInfo
F.gwInfo WfC a
w, QBind -> [Expr]
Sol.qbExprs QBind
qb))
  where 
    (KVar
k, QBind
qb) = SInfo a -> [Qualifier] -> SEnv Sort -> WfC a -> (KVar, QBind)
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 :: 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 (SInfo a -> Bool
forall (c :: * -> *) a. GInfo c a -> Bool
allowHOquals SInfo a
fi) SEnv Sort
env [Qualifier]
qs ((Symbol, Sort, KVar) -> (KVar, QBind))
-> (Symbol, Sort, KVar) -> (KVar, QBind)
forall a b. (a -> b) -> a -> b
$ WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
F.wrft WfC a
w
  where
    env :: SEnv Sort
env             = SEnv Sort
wenv SEnv Sort -> SEnv Sort -> SEnv Sort
forall a. Semigroup a => a -> a -> a
<> SEnv Sort
genv
    wenv :: SEnv Sort
wenv            = SortedReft -> Sort
F.sr_sort (SortedReft -> Sort) -> SEnv SortedReft -> SEnv Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)] -> SEnv SortedReft
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv (BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
F.envCs (SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
F.bs SInfo a
fi) (WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
F.wenv WfC a
w))

instConstants :: F.SInfo a -> F.SEnv F.Sort
instConstants :: SInfo a -> SEnv Sort
instConstants = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv ([(Symbol, Sort)] -> SEnv Sort)
-> (SInfo a -> [(Symbol, Sort)]) -> SInfo a -> SEnv Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol, Sort) -> Bool
forall b. (Symbol, b) -> Bool
notLit ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> (SInfo a -> [(Symbol, Sort)]) -> SInfo a -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
F.toListSEnv (SEnv Sort -> [(Symbol, Sort)])
-> (SInfo a -> SEnv Sort) -> SInfo a -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
F.gLits
  where
    notLit :: (Symbol, b) -> Bool
notLit    = Bool -> Bool
not (Bool -> Bool) -> ((Symbol, b) -> Bool) -> (Symbol, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Bool
F.isLitSymbol (Symbol -> Bool) -> ((Symbol, b) -> Symbol) -> (Symbol, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, b) -> Symbol
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 ([EQual] -> QBind)
-> ([Qualifier] -> [EQual]) -> [Qualifier] -> QBind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [EQual] -> [EQual]
unique ([EQual] -> [EQual])
-> ([Qualifier] -> [EQual]) -> [Qualifier] -> [EQual]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Qualifier -> [EQual]) -> [Qualifier] -> [EQual]
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       = (EQual -> EQual -> Bool) -> [EQual] -> [EQual]
forall a. (a -> a -> Bool) -> [a] -> [a]
L.nubBy (((Expr -> Bool) -> (EQual -> Expr) -> EQual -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EQual -> Expr
Sol.eqPred) ((Expr -> Bool) -> EQual -> Bool)
-> (EQual -> Expr -> Bool) -> EQual -> EQual -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Expr -> Expr -> Bool) -> (EQual -> Expr) -> EQual -> Expr -> 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
  = 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 (Sort -> Sort) -> [Sort] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
qts)
       EQual -> [EQual]
forall (m :: * -> *) a. Monad m => a -> m a
return     (EQual -> [EQual]) -> EQual -> [EQual]
forall a b. (a -> b) -> a -> b
$ Qualifier -> [Symbol] -> EQual
Sol.eQual Qualifier
q ([Symbol] -> [Symbol]
forall a. [a] -> [a]
reverse [Symbol]
xs)
    where
       Sort
qt : [Sort]
qts   = QualParam -> Sort
qpSort (QualParam -> Sort) -> [QualParam] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Qualifier -> [QualParam]
F.qParams Qualifier
q
       tyss :: [(Sort, [Symbol])]
tyss       = Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env
       senv :: Env
senv       = (Symbol -> SEnv Sort -> SESearch Sort
forall a. Symbol -> SEnv a -> SESearch a
`F.lookupSEnvWithDistance` SEnv Sort
env)

instCands :: Bool -> F.SEnv F.Sort -> [(F.Sort, [F.Symbol])]
instCands :: Bool -> SEnv Sort -> [(Sort, [Symbol])]
instCands Bool
ho SEnv Sort
env = ((Sort, [Symbol]) -> Bool)
-> [(Sort, [Symbol])] -> [(Sort, [Symbol])]
forall a. (a -> Bool) -> [a] -> [a]
filter (Sort, [Symbol]) -> Bool
forall b. (Sort, b) -> Bool
isOk [(Sort, [Symbol])]
tyss
  where
    tyss :: [(Sort, [Symbol])]
tyss      = [(Sort, Symbol)] -> [(Sort, [Symbol])]
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 Bool -> (Sort, b) -> Bool
forall a b. a -> b -> a
const Bool
True else Maybe ([Int], [Sort], Sort) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe ([Int], [Sort], Sort) -> Bool)
-> ((Sort, b) -> Maybe ([Int], [Sort], Sort)) -> (Sort, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Maybe ([Int], [Sort], Sort)
F.functionSort (Sort -> Maybe ([Int], [Sort], Sort))
-> ((Sort, b) -> Sort) -> (Sort, b) -> Maybe ([Int], [Sort], Sort)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sort, b) -> Sort
forall a b. (a, b) -> a
fst
    xts :: [(Symbol, Sort)]
xts       = SEnv Sort -> [(Symbol, Sort)]
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 Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
xs) (TVSubst -> Sort -> Sort
So.apply TVSubst
su (Sort -> Sort) -> [Sort] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
ts)
match Env
_   [(Sort, [Symbol])]
_   [Symbol]
xs []
  = [Symbol] -> [[Symbol]]
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      <- Maybe TVSubst -> [TVSubst]
forall a. Maybe a -> [a]
maybeToList (Maybe TVSubst -> [TVSubst]) -> Maybe TVSubst -> [TVSubst]
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 = Maybe Doc -> Bool
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            = SrcSpan -> SEnv Sort -> SortedReft -> Maybe Doc
forall a. Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc
So.checkSorted SrcSpan
F.dummySpan SEnv Sort
env SortedReft
sr