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

{- | This module creates new bindings for each argument of each kvar.
     It also makes sure that all arguments to each kvar are explicit.

     For example,

```
bind 0 x
bind 1 v
constraint:
  env [0; 1]
  rhs $k_42 // implicit substitutions [x:=x], [v:=v]
wf:
  env [0]
  reft {v : int | [$k_42]}
```

becomes

```
bind 0 x
bind 1 v
bind 2 lq_karg$x$k_42
constraint:
  env [0; 1]
  rhs $k_42[lq_karg$x$k_42:=x][lq_karg$v$k_42:=v]

wf:
  env [2]
  reft {lq_karg$v$k_42 : int | [$k_42]}
```

-}

module Language.Fixpoint.Solver.UniqifyKVars (wfcUniqify) where

import           Language.Fixpoint.Types
import           Language.Fixpoint.Types.Visitor (mapKVarSubsts)
import qualified Data.HashMap.Strict as M
#if !MIN_VERSION_base(4,20,0)
import           Data.Foldable       (foldl')
#endif

--------------------------------------------------------------------------------
wfcUniqify    :: SInfo a -> SInfo a
wfcUniqify :: forall a. SInfo a -> SInfo a
wfcUniqify SInfo a
fi = SInfo a -> SInfo a
forall a. SInfo a -> SInfo a
updateWfcs (SInfo a -> SInfo a) -> SInfo a -> SInfo a
forall a b. (a -> b) -> a -> b
$ SInfo a -> SInfo a
forall a. SInfo a -> SInfo a
remakeSubsts SInfo a
fi



-- mapKVarSubsts (\k su -> restrict table k su xs)
--------------------------------------------------------------------------------
remakeSubsts :: SInfo a -> SInfo a
--------------------------------------------------------------------------------
remakeSubsts :: forall a. SInfo a -> SInfo a
remakeSubsts SInfo a
fi = (KVar -> Subst -> Subst) -> SInfo a -> SInfo a
forall t. Visitable t => (KVar -> Subst -> Subst) -> t -> t
mapKVarSubsts (SInfo a -> KVar -> Subst -> Subst
forall a. SInfo a -> KVar -> Subst -> Subst
remakeSubst SInfo a
fi) SInfo a
fi

remakeSubst :: SInfo a -> KVar -> Subst -> Subst
remakeSubst :: forall a. SInfo a -> KVar -> Subst -> Subst
remakeSubst SInfo a
fi KVar
k Subst
su = (Subst -> Symbol -> Subst) -> Subst -> [Symbol] -> Subst
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (KVar -> Subst -> Symbol -> Subst
updateSubst KVar
k) Subst
su (SInfo a -> KVar -> [Symbol]
forall a. SInfo a -> KVar -> [Symbol]
kvarDomain SInfo a
fi KVar
k)

updateSubst :: KVar -> Subst -> Symbol -> Subst
updateSubst :: KVar -> Subst -> Symbol -> Subst
updateSubst KVar
k (Su HashMap Symbol (ExprV Symbol)
su) Symbol
sym
  = case Symbol -> HashMap Symbol (ExprV Symbol) -> Maybe (ExprV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
sym HashMap Symbol (ExprV Symbol)
su of
      Just ExprV Symbol
z  -> HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (HashMap Symbol (ExprV Symbol) -> Subst)
-> HashMap Symbol (ExprV Symbol) -> Subst
forall a b. (a -> b) -> a -> b
$ Symbol
-> HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete Symbol
sym (HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol))
-> HashMap Symbol (ExprV Symbol) -> HashMap Symbol (ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ Symbol
-> ExprV Symbol
-> HashMap Symbol (ExprV Symbol)
-> HashMap Symbol (ExprV Symbol)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
ksym ExprV Symbol
z          HashMap Symbol (ExprV Symbol)
su
      Maybe (ExprV Symbol)
Nothing -> HashMap Symbol (ExprV Symbol) -> Subst
forall v. HashMap Symbol (ExprV v) -> SubstV v
Su (HashMap Symbol (ExprV Symbol) -> Subst)
-> HashMap Symbol (ExprV Symbol) -> Subst
forall a b. (a -> b) -> a -> b
$                Symbol
-> ExprV Symbol
-> HashMap Symbol (ExprV Symbol)
-> HashMap Symbol (ExprV Symbol)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
ksym (Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eVar Symbol
sym) HashMap Symbol (ExprV Symbol)
su
    where
      kx :: Symbol
kx      = KVar -> Symbol
kv KVar
k
      ksym :: Symbol
ksym    = Symbol -> Symbol -> Symbol
kArgSymbol Symbol
sym Symbol
kx

-- / | sym `M.member` su = Su $ M.delete sym $ M.insert ksym (su M.! sym) su
-- /  | otherwise         = Su $                M.insert ksym (eVar sym)   su

--------------------------------------------------------------------------------
updateWfcs :: SInfo a -> SInfo a
--------------------------------------------------------------------------------
updateWfcs :: forall a. SInfo a -> SInfo a
updateWfcs SInfo a
fi = (SInfo a -> WfC a -> SInfo a)
-> SInfo a -> HashMap KVar (WfC a) -> SInfo a
forall a v k. (a -> v -> a) -> a -> HashMap k v -> a
M.foldl' SInfo a -> WfC a -> SInfo a
forall a. SInfo a -> WfC a -> SInfo a
updateWfc SInfo a
fi (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
fi)

updateWfc :: SInfo a -> WfC a -> SInfo a
updateWfc :: forall a. SInfo a -> WfC a -> SInfo a
updateWfc SInfo a
fi WfC a
w    = SInfo a
fi'' { ws = M.insert k w' (ws fi) }
  where
    w' :: WfC a
w'            = (ExprV Symbol -> ExprV Symbol) -> WfC a -> WfC a
forall a. (ExprV Symbol -> ExprV Symbol) -> WfC a -> WfC a
updateWfCExpr (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su) WfC a
w''
    w'' :: WfC a
w''           = WfC a
w { wenv = insertsIBindEnv newIds mempty, wrft = (v', t, k) }
    (BindId
_, SInfo a
fi'')     = Symbol -> SortedReft -> a -> SInfo a -> (BindId, SInfo a)
forall a. Symbol -> SortedReft -> a -> SInfo a -> (BindId, SInfo a)
newTopBind Symbol
v' (Sort -> SortedReft
trueSortedReft Sort
t) a
a SInfo a
fi'
    (SInfo a
fi', [BindId]
newIds) = ((SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId]))
-> (SInfo a, [BindId]) -> [BindId] -> (SInfo a, [BindId])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
forall a.
KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBindsIfValid KVar
k a
a) (SInfo a
fi, []) (IBindEnv -> [BindId]
elemsIBindEnv (IBindEnv -> [BindId]) -> IBindEnv -> [BindId]
forall a b. (a -> b) -> a -> b
$ WfC a -> IBindEnv
forall a. WfC a -> IBindEnv
wenv WfC a
w)
    (Symbol
v, Sort
t, KVar
k)     = WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w
    v' :: Symbol
v'            = Symbol -> Symbol -> Symbol
kArgSymbol Symbol
v (KVar -> Symbol
kv KVar
k)
    su :: Subst
su            = [(Symbol, ExprV Symbol)] -> Subst
mkSubst ((Symbol
v, Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
v')(Symbol, ExprV Symbol)
-> [(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)]
forall a. a -> [a] -> [a]
:[(Symbol
x, Symbol -> ExprV Symbol
forall a. Symbolic a => a -> ExprV Symbol
eVar (Symbol -> ExprV Symbol) -> Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> Symbol
kArgSymbol Symbol
x (KVar -> Symbol
kv KVar
k)) | Symbol
x <- SInfo a -> KVar -> [Symbol]
forall a. SInfo a -> KVar -> [Symbol]
kvarDomain SInfo a
fi KVar
k])
    a :: a
a             = WfC a -> a
forall a. WfC a -> a
winfo WfC a
w

accumBindsIfValid :: KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBindsIfValid :: forall a.
KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBindsIfValid KVar
k a
a (SInfo a
fi, [BindId]
ids) BindId
i = if Bool
renamable then KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
forall a.
KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBinds KVar
k a
a (SInfo a
fi, [BindId]
ids) BindId
i else (SInfo a
fi, BindId
i BindId -> [BindId] -> [BindId]
forall a. a -> [a] -> [a]
: [BindId]
ids)
  where
    (Symbol
_, SortedReft
sr, a
_)                    = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i      (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi)
    renamable :: Bool
renamable                   = Sort -> Bool
isValidInRefinements (SortedReft -> Sort
sr_sort SortedReft
sr)

accumBinds :: KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBinds :: forall a.
KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBinds KVar
k a
a (SInfo a
fi, [BindId]
ids) BindId
i = (SInfo a
fi', BindId
i' BindId -> [BindId] -> [BindId]
forall a. a -> [a] -> [a]
: [BindId]
ids)
  where
    (Symbol
oldSym, SortedReft
sr,a
_) = BindId -> BindEnv a -> (Symbol, SortedReft, a)
forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi)
    newSym :: Symbol
newSym       = {- tracepp "kArgSymbol" $ -}  Symbol -> Symbol -> Symbol
kArgSymbol Symbol
oldSym (KVar -> Symbol
kv KVar
k)
    (BindId
i', SInfo a
fi')    = Symbol -> SortedReft -> a -> SInfo a -> (BindId, SInfo a)
forall a. Symbol -> SortedReft -> a -> SInfo a -> (BindId, SInfo a)
newTopBind Symbol
newSym SortedReft
sr a
a SInfo a
fi

-- | `newTopBind` ignores the actual refinements as they are not relevant
--   in the kvar parameters (as suggested by BLC.)
newTopBind :: Symbol -> SortedReft -> a -> SInfo a -> (BindId, SInfo a)
newTopBind :: forall a. Symbol -> SortedReft -> a -> SInfo a -> (BindId, SInfo a)
newTopBind Symbol
x SortedReft
sr a
a SInfo a
fi = (BindId
i', SInfo a
fi {bs = be'})
  where
    (BindId
i', BindEnv a
be')        = Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
insertBindEnv Symbol
x (SortedReft
sr {sr_reft = trueReft}) a
a (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi)

--------------------------------------------------------------

isValidInRefinements :: Sort -> Bool
isValidInRefinements :: Sort -> Bool
isValidInRefinements Sort
FInt        = Bool
True
isValidInRefinements Sort
FReal       = Bool
True
isValidInRefinements Sort
FNum        = Bool
False
isValidInRefinements Sort
FFrac       = Bool
False
isValidInRefinements (FObj Symbol
_)    = Bool
True
isValidInRefinements (FVar BindId
_)    = Bool
True
isValidInRefinements (FFunc Sort
_ Sort
_) = Bool
True -- False
isValidInRefinements (FAbs  BindId
_ Sort
t) = Sort -> Bool
isValidInRefinements Sort
t
isValidInRefinements (FTC FTycon
_)     = Bool
True --TODO is this true? seems to be required for e.g. ResolvePred.hs
isValidInRefinements (FApp Sort
_ Sort
_)  = Bool
True