{-# LANGUAGE CPP                        #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE TupleSections              #-}

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

-- | This module contains the top-level SOLUTION data types,
--   including various indices used for solving.

module Language.Fixpoint.Types.Graduals (
  uniquify,

  makeSolutions,

  GSol,

  Gradual (..)
  ) where

import Language.Fixpoint.Types.Refinements
import Language.Fixpoint.Types.Constraints
import Language.Fixpoint.Types.Config
import Language.Fixpoint.Types.PrettyPrint
import Language.Fixpoint.Types.Environments
import Language.Fixpoint.Types.Substitutions
import Language.Fixpoint.Types.Visitor
import Language.Fixpoint.Types.Spans
import Language.Fixpoint.Types.Theories
import Language.Fixpoint.Types.Names        (gradIntSymbol, tidySymbol)
import Language.Fixpoint.Misc               (allCombinations, errorstar)

import Control.DeepSeq

import qualified Data.HashMap.Strict       as M
import qualified Data.List                 as L

import Control.Monad.State.Lazy
import Data.Maybe (fromMaybe)
import qualified Language.Fixpoint.SortCheck       as So
import Language.Fixpoint.Solver.Sanitize (symbolEnv)


data GSol = GSol !SymEnv !(M.HashMap KVar (Expr, GradInfo))

instance Semigroup GSol where
  (GSol SymEnv
e1 HashMap KVar (Expr, GradInfo)
m1) <> :: GSol -> GSol -> GSol
<> (GSol SymEnv
e2 HashMap KVar (Expr, GradInfo)
m2) = SymEnv -> HashMap KVar (Expr, GradInfo) -> GSol
GSol (SymEnv
e1 forall a. Semigroup a => a -> a -> a
<> SymEnv
e2) (HashMap KVar (Expr, GradInfo)
m1 forall a. Semigroup a => a -> a -> a
<> HashMap KVar (Expr, GradInfo)
m2)

instance Monoid GSol where
  mempty :: GSol
mempty = SymEnv -> HashMap KVar (Expr, GradInfo) -> GSol
GSol forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty

instance Show GSol where
  show :: GSol -> String
show (GSol SymEnv
_ HashMap KVar (Expr, GradInfo)
m) = String
"GSOL = \n" forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((\(KVar
k,(Expr
e, GradInfo
i)) -> forall a. PPrint a => a -> String
showpp KVar
k forall a. [a] -> [a] -> [a]
++ forall {a}. Show a => a -> String
showInfo GradInfo
i forall a. [a] -> [a] -> [a]
++  String
" |-> " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp (forall {a}. Subable a => a -> a
tx Expr
e)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. HashMap k v -> [(k, v)]
M.toList HashMap KVar (Expr, GradInfo)
m)
    where
      tx :: a -> a
tx a
e = forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ [(Symbol
x, Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
tidySymbol Symbol
x) | Symbol
x <- forall a. Subable a => a -> [Symbol]
syms a
e]) a
e
      showInfo :: a -> String
showInfo a
i = forall {a}. Show a => a -> String
show a
i


makeSolutions :: (NFData a, Fixpoint a, Show a)
              => Config -> SInfo a
              -> [(KVar, (GWInfo, [[Expr]]))]
              -> Maybe [GSol]

makeSolutions :: forall a.
(NFData a, Fixpoint a, Show a) =>
Config -> SInfo a -> [(KVar, (GWInfo, [[Expr]]))] -> Maybe [GSol]
makeSolutions Config
_ SInfo a
_ []
  = forall a. Maybe a
Nothing
makeSolutions Config
cfg SInfo a
fi [(KVar, (GWInfo, [[Expr]]))]
kes
  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (SymEnv -> HashMap KVar (Expr, GradInfo) -> GSol
GSol SymEnv
env forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList) (forall a. [[a]] -> [[a]]
allCombinations (forall {a}. (a, (GWInfo, [[Expr]])) -> [(a, (Expr, GradInfo))]
go  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(KVar, (GWInfo, [[Expr]]))]
kes))
  where
    go :: (a, (GWInfo, [[Expr]])) -> [(a, (Expr, GradInfo))]
go (a
k, (GWInfo
i, [[Expr]]
es)) = [(a
k, ([Expr] -> Expr
pAnd (GWInfo -> Expr
gexpr GWInfo
iforall a. a -> [a] -> [a]
:[Expr]
e'), GWInfo -> GradInfo
ginfo GWInfo
i)) | [Expr]
e' <- [[Expr]]
es]
    env :: SymEnv
env = forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
fi


-------------------------------------------------------------------------------
-- |  Make each gradual appearence unique -------------------------------------
-------------------------------------------------------------------------------
uniquify :: (NFData a, Fixpoint a, Loc a) => SInfo a -> SInfo a

uniquify :: forall a. (NFData a, Fixpoint a, Loc a) => SInfo a -> SInfo a
uniquify SInfo a
fi = SInfo a
fi{cm :: HashMap SubcId (SimpC a)
cm = HashMap SubcId (SimpC a)
cm', ws :: HashMap KVar (WfC a)
ws = HashMap KVar (WfC a)
ws', bs :: BindEnv a
bs = BindEnv a
bs'}
  where
  (HashMap SubcId (SimpC a)
cm', HashMap KVar [(KVar, Maybe SrcSpan)]
km, BindEnv a
bs') = forall a.
(NFData a, Fixpoint a, Loc a) =>
BindEnv a
-> HashMap SubcId (SimpC a)
-> (HashMap SubcId (SimpC a), HashMap KVar [(KVar, Maybe SrcSpan)],
    BindEnv a)
uniquifyCS (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi) (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi)
  ws' :: HashMap KVar (WfC a)
ws'            = forall a.
(NFData a, Fixpoint a) =>
HashMap KVar [(KVar, Maybe SrcSpan)]
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
expandWF HashMap KVar [(KVar, Maybe SrcSpan)]
km (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
fi)

uniquifyCS :: (NFData a, Fixpoint a, Loc a)
           => BindEnv a
           -> M.HashMap SubcId (SimpC a)
           -> (M.HashMap SubcId (SimpC a), M.HashMap KVar [(KVar, Maybe SrcSpan)], BindEnv a)
uniquifyCS :: forall a.
(NFData a, Fixpoint a, Loc a) =>
BindEnv a
-> HashMap SubcId (SimpC a)
-> (HashMap SubcId (SimpC a), HashMap KVar [(KVar, Maybe SrcSpan)],
    BindEnv a)
uniquifyCS BindEnv a
bs HashMap SubcId (SimpC a)
cs
  = (HashMap SubcId (SimpC a)
x, HashMap KVar [(KVar, Maybe SrcSpan)]
km, forall a. UniqueST a -> BindEnv a
benv UniqueST a
st)
  where
    (HashMap SubcId (SimpC a)
x, UniqueST a
st) = forall s a. State s a -> s -> (a, s)
runState (forall ann a. Unique ann a => a -> UniqueM ann a
uniq HashMap SubcId (SimpC a)
cs) (forall a. BindEnv a -> UniqueST a
initUniqueST BindEnv a
bs)
    km :: HashMap KVar [(KVar, Maybe SrcSpan)]
km      = forall a. UniqueST a -> HashMap KVar [(KVar, Maybe SrcSpan)]
kmap UniqueST a
st


class Unique ann a where
   uniq :: a -> UniqueM ann a

instance Unique ann a => Unique ann (M.HashMap SubcId a) where
  uniq :: HashMap SubcId a -> UniqueM ann (HashMap SubcId a)
uniq HashMap SubcId a
m = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(SubcId
i,a
x) -> (SubcId
i,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann a. Unique ann a => a -> UniqueM ann a
uniq a
x) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId a
m)

instance Loc a => Unique a (SimpC a) where
  uniq :: SimpC a -> UniqueM a (SimpC a)
uniq SimpC a
cs = do
    forall ann. SrcSpan -> UniqueM ann ()
updateLoc forall a b. (a -> b) -> a -> b
$ forall a. Loc a => a -> SrcSpan
srcSpan forall a b. (a -> b) -> a -> b
$ forall a. SimpC a -> a
_cinfo SimpC a
cs
    Expr
rhs <- forall ann a. Unique ann a => a -> UniqueM ann a
uniq (forall a. SimpC a -> Expr
_crhs SimpC a
cs)
    IBindEnv
env <- forall ann a. Unique ann a => a -> UniqueM ann a
uniq (forall a. SimpC a -> IBindEnv
_cenv SimpC a
cs)
    forall (m :: * -> *) a. Monad m => a -> m a
return SimpC a
cs{_crhs :: Expr
_crhs = Expr
rhs, _cenv :: IBindEnv
_cenv = IBindEnv
env}

instance Unique ann IBindEnv where
  uniq :: IBindEnv -> UniqueM ann IBindEnv
uniq IBindEnv
env = forall ann a. UniqueM ann a -> UniqueM ann a
withCache ([Int] -> IBindEnv
fromListIBindEnv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall ann a. Unique ann a => a -> UniqueM ann a
uniq (IBindEnv -> [Int]
elemsIBindEnv IBindEnv
env))

instance Unique ann BindId where
  uniq :: Int -> UniqueM ann Int
uniq Int
i = do
    BindEnv ann
bs <- forall a. UniqueST a -> BindEnv a
benv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
    let (Symbol
x, SortedReft
t, ann
ann) = forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
i BindEnv ann
bs
    forall ann. UniqueM ann ()
resetChange
    SortedReft
t' <- forall ann a. Unique ann a => a -> UniqueM ann a
uniq SortedReft
t
    Bool
hasChanged <- forall a. UniqueST a -> Bool
change forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
    if Bool
hasChanged
      then do let (Int
i', BindEnv ann
bs') = forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (Int, BindEnv a)
insertBindEnv Symbol
x SortedReft
t' ann
ann BindEnv ann
bs
              forall a. Int -> BindEnv a -> UniqueM a ()
updateBEnv Int
i BindEnv ann
bs'
              forall (m :: * -> *) a. Monad m => a -> m a
return Int
i'
      else forall (m :: * -> *) a. Monad m => a -> m a
return Int
i

instance Unique ann SortedReft where
  uniq :: SortedReft -> UniqueM ann SortedReft
uniq (RR Sort
s Reft
r) = Sort -> Reft -> SortedReft
RR Sort
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann a. Unique ann a => a -> UniqueM ann a
uniq Reft
r

instance Unique ann Reft where
  uniq :: Reft -> UniqueM ann Reft
uniq (Reft (Symbol
x,Expr
e)) = (Symbol, Expr) -> Reft
Reft forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
x,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall ann a. Unique ann a => a -> UniqueM ann a
uniq Expr
e

instance Unique ann Expr where
  uniq :: Expr -> UniqueM ann Expr
uniq = forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
mapMExpr forall ann. Expr -> UniqueM ann Expr
go
   where
    go :: Expr -> StateT (UniqueST a) Identity Expr
go (PGrad KVar
k Subst
su GradInfo
i Expr
e) = do
      KVar
k'  <- forall ann. KVar -> UniqueM ann KVar
freshK KVar
k
      Maybe SrcSpan
src <- forall a. UniqueST a -> Maybe SrcSpan
uloc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad KVar
k' Subst
su (GradInfo
i{gused :: Maybe SrcSpan
gused = Maybe SrcSpan
src}) Expr
e
    go Expr
e              = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

-------------------------------------------------------------------------------
-- | The Unique Monad ---------------------------------------------------------
-------------------------------------------------------------------------------

type UniqueM ann = State (UniqueST ann)
data UniqueST a
  = UniqueST { forall a. UniqueST a -> SubcId
freshId :: Integer
             , forall a. UniqueST a -> HashMap KVar [(KVar, Maybe SrcSpan)]
kmap    :: M.HashMap KVar [(KVar, Maybe SrcSpan)]
             , forall a. UniqueST a -> Bool
change  :: Bool
             , forall a. UniqueST a -> HashMap KVar KVar
cache   :: M.HashMap KVar KVar
             , forall a. UniqueST a -> Maybe SrcSpan
uloc    :: Maybe SrcSpan
             , forall a. UniqueST a -> [Int]
ubs     :: [BindId]
             , forall a. UniqueST a -> BindEnv a
benv    :: BindEnv a
             }

updateLoc :: SrcSpan -> UniqueM ann ()
updateLoc :: forall ann. SrcSpan -> UniqueM ann ()
updateLoc SrcSpan
x = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \UniqueST ann
s -> UniqueST ann
s{uloc :: Maybe SrcSpan
uloc = forall a. a -> Maybe a
Just SrcSpan
x}

withCache :: UniqueM ann a -> UniqueM ann a
withCache :: forall ann a. UniqueM ann a -> UniqueM ann a
withCache UniqueM ann a
act = do
  forall ann. UniqueM ann ()
emptyCache
  a
a <- UniqueM ann a
act
  forall ann. UniqueM ann ()
emptyCache
  forall (m :: * -> *) a. Monad m => a -> m a
return a
a

emptyCache :: UniqueM ann ()
emptyCache :: forall ann. UniqueM ann ()
emptyCache = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \UniqueST ann
s -> UniqueST ann
s{cache :: HashMap KVar KVar
cache = forall a. Monoid a => a
mempty}

addCache :: KVar -> KVar -> UniqueM ann ()
addCache :: forall ann. KVar -> KVar -> UniqueM ann ()
addCache KVar
k KVar
k' = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \UniqueST ann
s -> UniqueST ann
s{cache :: HashMap KVar KVar
cache = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert KVar
k KVar
k' (forall a. UniqueST a -> HashMap KVar KVar
cache UniqueST ann
s)}

updateBEnv :: BindId -> BindEnv a -> UniqueM a ()
updateBEnv :: forall a. Int -> BindEnv a -> UniqueM a ()
updateBEnv Int
i BindEnv a
bs = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \UniqueST a
s -> UniqueST a
s{benv :: BindEnv a
benv = BindEnv a
bs, ubs :: [Int]
ubs = Int
i forall a. a -> [a] -> [a]
: forall a. UniqueST a -> [Int]
ubs UniqueST a
s}

setChange :: UniqueM ann ()
setChange :: forall ann. UniqueM ann ()
setChange = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \UniqueST ann
s -> UniqueST ann
s{change :: Bool
change = Bool
True}

resetChange :: UniqueM ann ()
resetChange :: forall ann. UniqueM ann ()
resetChange = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \UniqueST ann
s -> UniqueST ann
s{change :: Bool
change = Bool
False}

initUniqueST :: BindEnv a ->  UniqueST a
initUniqueST :: forall a. BindEnv a -> UniqueST a
initUniqueST = forall a.
SubcId
-> HashMap KVar [(KVar, Maybe SrcSpan)]
-> Bool
-> HashMap KVar KVar
-> Maybe SrcSpan
-> [Int]
-> BindEnv a
-> UniqueST a
UniqueST SubcId
0 forall a. Monoid a => a
mempty Bool
False forall a. Monoid a => a
mempty forall a. Maybe a
Nothing forall a. Monoid a => a
mempty

freshK, freshK' :: KVar -> UniqueM ann KVar
freshK :: forall ann. KVar -> UniqueM ann KVar
freshK KVar
k  = do
  forall ann. UniqueM ann ()
setChange
  HashMap KVar KVar
cached <- forall a. UniqueST a -> HashMap KVar KVar
cache forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
  case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k HashMap KVar KVar
cached of
    {- OPTIMIZATION: Only create one fresh occurence of ? per constraint environment. -}
    Just KVar
k' -> forall (m :: * -> *) a. Monad m => a -> m a
return  KVar
k'
    Maybe KVar
Nothing -> forall ann. KVar -> UniqueM ann KVar
freshK' KVar
k

freshK' :: forall ann. KVar -> UniqueM ann KVar
freshK' KVar
k = do
  SubcId
i <- forall a. UniqueST a -> SubcId
freshId forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\UniqueST ann
s -> UniqueST ann
s{freshId :: SubcId
freshId = SubcId
i forall a. Num a => a -> a -> a
+ SubcId
1})
  let k' :: KVar
k' = Symbol -> KVar
KV forall a b. (a -> b) -> a -> b
$ SubcId -> Symbol
gradIntSymbol SubcId
i
  forall ann. KVar -> KVar -> UniqueM ann ()
addK KVar
k KVar
k'
  forall ann. KVar -> KVar -> UniqueM ann ()
addCache KVar
k KVar
k'
  forall (m :: * -> *) a. Monad m => a -> m a
return KVar
k'

addK :: KVar -> KVar -> UniqueM ann ()
addK :: forall ann. KVar -> KVar -> UniqueM ann ()
addK KVar
key KVar
val =
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\UniqueST ann
s -> UniqueST ann
s{kmap :: HashMap KVar [(KVar, Maybe SrcSpan)]
kmap = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith forall a. [a] -> [a] -> [a]
(++) KVar
key [(KVar
val, forall a. UniqueST a -> Maybe SrcSpan
uloc UniqueST ann
s)] (forall a. UniqueST a -> HashMap KVar [(KVar, Maybe SrcSpan)]
kmap UniqueST ann
s)})

-------------------------------------------------------------------------------
-- | expandWF -----------------------------------------------------------------
-------------------------------------------------------------------------------

expandWF :: (NFData a, Fixpoint a)
         => M.HashMap KVar [(KVar, Maybe SrcSpan)]
         -> M.HashMap KVar (WfC a)
         -> M.HashMap KVar (WfC a)
expandWF :: forall a.
(NFData a, Fixpoint a) =>
HashMap KVar [(KVar, Maybe SrcSpan)]
-> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
expandWF HashMap KVar [(KVar, Maybe SrcSpan)]
km HashMap KVar (WfC a)
ws
  = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
       ([(KVar
k, forall {a}. KVar -> Maybe SrcSpan -> WfC a -> WfC a
updateKVar KVar
k Maybe SrcSpan
src WfC a
w) | (KVar
i, WfC a
w) <- [(KVar, WfC a)]
gws, (KVar
kw, [(KVar, Maybe SrcSpan)]
ks) <- [(KVar, [(KVar, Maybe SrcSpan)])]
km', KVar
kw forall a. Eq a => a -> a -> Bool
== KVar
i, (KVar
k, Maybe SrcSpan
src) <- [(KVar, Maybe SrcSpan)]
ks]
        forall a. [a] -> [a] -> [a]
++ [(KVar, WfC a)]
kws)
  where
    ([(KVar, WfC a)]
gws, [(KVar, WfC a)]
kws)       = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (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 HashMap KVar (WfC a)
ws
    km' :: [(KVar, [(KVar, Maybe SrcSpan)])]
km'              = forall k v. HashMap k v -> [(k, v)]
M.toList HashMap KVar [(KVar, Maybe SrcSpan)]
km

    updateKVar :: KVar -> Maybe SrcSpan -> WfC a -> WfC a
updateKVar KVar
k Maybe SrcSpan
src WfC a
wfc = let wrft' :: (Symbol, Sort, KVar)
wrft' = (\(Symbol
v,Sort
s,KVar
_) -> (Symbol
v,Sort
s,KVar
k)) forall a b. (a -> b) -> a -> b
$ forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
wfc in
      case WfC a
wfc of
        GWfC{} -> WfC a
wfc { wrft :: (Symbol, Sort, KVar)
wrft = (Symbol, Sort, KVar)
wrft', wloc :: GradInfo
wloc = (forall a. WfC a -> GradInfo
wloc WfC a
wfc){gused :: Maybe SrcSpan
gused = Maybe SrcSpan
src} }
        WfC{}  -> WfC a
wfc { wrft :: (Symbol, Sort, KVar)
wrft = (Symbol, Sort, KVar)
wrft' }

-------------------------------------------------------------------------------
-- |  Substitute Gradual Solution ---------------------------------------------
-------------------------------------------------------------------------------

class Gradual a where
  gsubst :: GSol -> a -> a

instance Gradual Expr where
  gsubst :: GSol -> Expr -> Expr
gsubst (GSol SymEnv
env HashMap KVar (Expr, GradInfo)
m) Expr
e   = forall t. Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t
mapGVars' (\(KVar
k, Subst
_) -> forall a. a -> Maybe a
Just (forall a. a -> Maybe a -> a
fromMaybe (forall {a} {a}. PPrint a => a -> a
err KVar
k) (KVar -> Maybe Expr
mknew KVar
k))) Expr
e
    where
      mknew :: KVar -> Maybe Expr
mknew KVar
k = forall a. Elaborate a => Located String -> SymEnv -> a -> a
So.elaborate Located String
"initBGind.mkPred" SymEnv
env forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup KVar
k HashMap KVar (Expr, GradInfo)
m
      err :: a -> a
err   a
k = forall a. (?callStack::CallStack) => String -> a
errorstar (String
"gradual substitution: Cannot find " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
showpp a
k)

instance Gradual Reft where
  gsubst :: GSol -> Reft -> Reft
gsubst GSol
su (Reft (Symbol
x, Expr
e)) = (Symbol, Expr) -> Reft
Reft (Symbol
x, forall a. Gradual a => GSol -> a -> a
gsubst GSol
su Expr
e)

instance Gradual SortedReft where
  gsubst :: GSol -> SortedReft -> SortedReft
gsubst GSol
su SortedReft
r = SortedReft
r {sr_reft :: Reft
sr_reft = forall a. Gradual a => GSol -> a -> a
gsubst GSol
su (SortedReft -> Reft
sr_reft SortedReft
r)}

instance Gradual (SimpC a) where
  gsubst :: GSol -> SimpC a -> SimpC a
gsubst GSol
su SimpC a
c = SimpC a
c {_crhs :: Expr
_crhs = forall a. Gradual a => GSol -> a -> a
gsubst GSol
su (forall a. SimpC a -> Expr
_crhs SimpC a
c)}

instance Gradual (BindEnv a) where
  gsubst :: GSol -> BindEnv a -> BindEnv a
gsubst GSol
su = forall a.
(Int -> (Symbol, SortedReft, a) -> (Symbol, SortedReft, a))
-> BindEnv a -> BindEnv a
mapBindEnv (\Int
_ (Symbol
x, SortedReft
r, a
l) -> (Symbol
x, forall a. Gradual a => GSol -> a -> a
gsubst GSol
su SortedReft
r, a
l))

instance Gradual v => Gradual (M.HashMap k v) where
  gsubst :: GSol -> HashMap k v -> HashMap k v
gsubst GSol
su = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall a. Gradual a => GSol -> a -> a
gsubst GSol
su)

instance Gradual (SInfo a) where
  gsubst :: GSol -> SInfo a -> SInfo a
gsubst GSol
su SInfo a
fi = SInfo a
fi { bs :: BindEnv a
bs = forall a. Gradual a => GSol -> a -> a
gsubst GSol
su (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi)
                    , cm :: HashMap SubcId (SimpC a)
cm = forall a. Gradual a => GSol -> a -> a
gsubst GSol
su (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi)
                    }