{- | 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 :: 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 :: 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 :: SInfo a -> KVar -> Subst -> Subst
remakeSubst SInfo a
fi KVar
k Subst
su = (Subst -> Symbol -> Subst) -> Subst -> [Symbol] -> Subst
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 Expr
su) Symbol
sym
  = case Symbol -> HashMap Symbol Expr -> Maybe Expr
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 (HashMap Symbol Expr -> Subst) -> HashMap Symbol Expr -> Subst
forall a b. (a -> b) -> a -> b
$ Symbol -> HashMap Symbol Expr -> HashMap Symbol Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete Symbol
sym (HashMap Symbol Expr -> HashMap Symbol Expr)
-> HashMap Symbol Expr -> HashMap Symbol Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr -> HashMap Symbol Expr -> HashMap Symbol Expr
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 (HashMap Symbol Expr -> Subst) -> HashMap Symbol Expr -> Subst
forall a b. (a -> b) -> a -> b
$                Symbol -> Expr -> HashMap Symbol Expr -> HashMap Symbol Expr
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
ksym (Symbol -> Expr
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 :: 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 :: SInfo a -> WfC a -> SInfo a
updateWfc SInfo a
fi WfC a
w    = SInfo a
fi'' { ws :: HashMap KVar (WfC a)
ws = KVar -> WfC a -> HashMap KVar (WfC a) -> HashMap KVar (WfC a)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert KVar
k WfC a
w' (SInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
ws SInfo a
fi) }
  where
    w' :: WfC a
w'            = (Expr -> Expr) -> WfC a -> WfC a
forall a. (Expr -> Expr) -> WfC a -> WfC a
updateWfCExpr (Subst -> Expr -> Expr
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 IBindEnv
forall a. Monoid a => a
mempty, wrft :: (Symbol, Sort, KVar)
wrft = (Symbol
v', Sort
t, KVar
k) }
    (BindId
_, SInfo a
fi'')     = Symbol -> SortedReft -> SInfo a -> (BindId, SInfo a)
forall a. Symbol -> SortedReft -> SInfo a -> (BindId, SInfo a)
newTopBind Symbol
v' (Sort -> SortedReft
trueSortedReft Sort
t) SInfo a
fi'
    (SInfo a
fi', [BindId]
newIds) = ((SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId]))
-> (SInfo a, [BindId]) -> [BindId] -> (SInfo a, [BindId])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (KVar -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
forall a.
KVar -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBindsIfValid KVar
k) (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, Expr)] -> Subst
mkSubst ((Symbol
v, Symbol -> Expr
EVar Symbol
v')(Symbol, Expr) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. a -> [a] -> [a]
:[(Symbol
x, Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar (Symbol -> Expr) -> Symbol -> Expr
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])

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

accumBinds :: KVar -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBinds :: KVar -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
accumBinds KVar
k (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) = BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv BindId
i (SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
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 -> SInfo a -> (BindId, SInfo a)
forall a. Symbol -> SortedReft -> SInfo a -> (BindId, SInfo a)
newTopBind Symbol
newSym SortedReft
sr SInfo a
fi

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