content: {-# 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 fi = updateWfcs $ remakeSubsts fi
  
  
  
  -- mapKVarSubsts (\k su -> restrict table k su xs)
  --------------------------------------------------------------------------------
  remakeSubsts :: SInfo a -> SInfo a
  --------------------------------------------------------------------------------
  remakeSubsts fi = mapKVarSubsts (remakeSubst fi) fi
  
  remakeSubst :: SInfo a -> KVar -> Subst -> Subst
  remakeSubst fi k su = foldl' (updateSubst k) su (kvarDomain fi k)
  
  updateSubst :: KVar -> Subst -> Symbol -> Subst
  updateSubst k (Su su) sym
    = case M.lookup sym su of
        Just z  -> Su $ M.delete sym $ M.insert ksym z          su
        Nothing -> Su $                M.insert ksym (eVar sym) su
      where
        kx      = kv k
        ksym    = kArgSymbol sym 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 fi = M.foldl' updateWfc fi (ws fi)
  
  updateWfc :: SInfo a -> WfC a -> SInfo a
  updateWfc fi w    = fi'' { ws = M.insert k w' (ws fi) }
    where
      w'            = updateWfCExpr (subst su) w''
      w''           = w { wenv = insertsIBindEnv newIds mempty, wrft = (v', t, k) }
      (_, fi'')     = newTopBind v' (trueSortedReft t) a fi'
      (fi', newIds) = foldl' (accumBindsIfValid k a) (fi, []) (elemsIBindEnv $ wenv w)
      (v, t, k)     = wrft w
      v'            = kArgSymbol v (kv k)
      su            = mkSubst ((v, EVar v'):[(x, eVar $ kArgSymbol x (kv k)) | x <- kvarDomain fi k])
      a             = winfo w
  
  accumBindsIfValid :: KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
  accumBindsIfValid k a (fi, ids) i = if renamable then accumBinds k a (fi, ids) i else (fi, i : ids)
    where
      (_, sr, _)                    = lookupBindEnv i      (bs fi)
      renamable                   = isValidInRefinements (sr_sort sr)
  
  accumBinds :: KVar -> a -> (SInfo a, [BindId]) -> BindId -> (SInfo a, [BindId])
  accumBinds k a (fi, ids) i = (fi', i' : ids)
    where
      (oldSym, sr,_) = lookupBindEnv i (bs fi)
      newSym       = {- tracepp "kArgSymbol" $ -}  kArgSymbol oldSym (kv k)
      (i', fi')    = newTopBind newSym sr 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 x sr a fi = (i', fi {bs = be'})
    where
      (i', be')        = insertBindEnv x (sr {sr_reft = trueReft}) a (bs fi)
  
  --------------------------------------------------------------
  
  isValidInRefinements :: Sort -> Bool
  isValidInRefinements FInt        = True
  isValidInRefinements FReal       = True
  isValidInRefinements FNum        = False
  isValidInRefinements FFrac       = False
  isValidInRefinements (FObj _)    = True
  isValidInRefinements (FVar _)    = True
  isValidInRefinements (FFunc _ _) = True -- False
  isValidInRefinements (FAbs  _ t) = isValidInRefinements t
  isValidInRefinements (FTC _)     = True --TODO is this true? seems to be required for e.g. ResolvePred.hs
  isValidInRefinements (FApp _ _)  = True
  