{-# 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
import           Data.Foldable       (foldl')

--------------------------------------------------------------------------------
wfcUniqify    :: SInfo a -> SInfo a
wfcUniqify :: forall a. SInfo a -> SInfo a
wfcUniqify SInfo a
fi = forall a. SInfo a -> SInfo a
updateWfcs forall a b. (a -> b) -> a -> b
$ 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 = forall t. Visitable t => (KVar -> Subst -> Subst) -> t -> t
mapKVarSubsts (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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (KVar -> Subst -> Symbol -> Subst
updateSubst KVar
k) Subst
su (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 Expr
su) Symbol
sym
  = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
sym HashMap Symbol Expr
su of
      Just Expr
z  -> HashMap Symbol Expr -> Subst
Su forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete Symbol
sym forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
ksym Expr
z          HashMap Symbol Expr
su
      Maybe Expr
Nothing -> HashMap Symbol Expr -> Subst
Su forall a b. (a -> b) -> a -> b
$                forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
ksym (forall a. Symbolic a => a -> Expr
eVar Symbol
sym) HashMap Symbol Expr
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 = forall a v k. (a -> v -> a) -> a -> HashMap k v -> a
M.foldl' forall a. SInfo a -> WfC a -> SInfo a
updateWfc SInfo a
fi (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 :: HashMap KVar (WfC a)
ws = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert KVar
k WfC a
w' (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
fi) }
  where
    w' :: WfC a
w'            = forall a. (Expr -> Expr) -> WfC a -> WfC a
updateWfCExpr (forall a. Subable a => Subst -> a -> a
subst Subst
su) WfC a
w''
    w'' :: WfC a
w''           = WfC a
w { wenv :: IBindEnv
wenv = [BindId] -> IBindEnv -> IBindEnv
insertsIBindEnv [BindId]
newIds forall a. Monoid a => a
mempty, wrft :: (Symbol, Sort, KVar)
wrft = (Symbol
v', Sort
t, KVar
k) }
    (BindId
_, SInfo a
fi'')     = 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) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a.
KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBindsIfValid KVar
k a
a) (SInfo a
fi, []) (IBindEnv -> [BindId]
elemsIBindEnv forall a b. (a -> b) -> a -> b
$ forall a. WfC a -> IBindEnv
wenv WfC a
w)
    (Symbol
v, Sort
t, KVar
k)     = 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, Expr)] -> Subst
mkSubst ((Symbol
v, Symbol -> Expr
EVar Symbol
v')forall a. a -> [a] -> [a]
:[(Symbol
x, forall a. Symbolic a => a -> Expr
eVar forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> Symbol
kArgSymbol Symbol
x (KVar -> Symbol
kv KVar
k)) | Symbol
x <- forall a. SInfo a -> KVar -> [Symbol]
kvarDomain SInfo a
fi KVar
k])
    a :: 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 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 forall a. a -> [a] -> [a]
: [BindId]
ids)
  where
    (Symbol
_, SortedReft
sr, a
_)                    = forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i      (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' forall a. a -> [a] -> [a]
: [BindId]
ids)
  where
    (Symbol
oldSym, SortedReft
sr,a
_) = forall a. BindId -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv BindId
i (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')    = 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 :: BindEnv a
bs = BindEnv a
be'})
  where
    (BindId
i', BindEnv a
be')        = forall a.
Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a)
insertBindEnv Symbol
x (forall r. Reftable r => r -> r
top SortedReft
sr) a
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