{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE ImplicitParams            #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE TypeOperators             #-}

-- | This module defines the representation for Environments needed
--   during constraint generation.

module Language.Haskell.Liquid.Constraint.Env (

  -- * Insert
    (+++=)
  -- , (++=)
  , (+=)
  , extendEnvWithVV
  , addBinders
  , addSEnv
  , addEEnv
  , addRewritesForNextBinding
  , (-=)
  , globalize

  -- * Construction
  , fromListREnv
  , toListREnv
  , insertREnv -- TODO: remove this ASAP

  -- * Query
  , localBindsOfType
  , lookupREnv
  , (?=)

  -- * Pruning refinements (TODO: move!)
 , rTypeSortedReft'

  -- * Extend CGEnv
 , setLocation, setBind, setRecs, setTRec

  -- * Lookup CGEnv
 , getLocation

) where


-- import Name (getSrcSpan)
import Prelude hiding (error)
-- import Outputable
-- import FastString (fsLit)
import Control.Monad (foldM, msum)
import Control.Monad.State

-- import           GHC.Err.Located hiding (error)
import           GHC.Stack

import           Control.Arrow           (first)
import           Data.Maybe              -- (fromMaybe)
import qualified Data.List               as L
import qualified Data.HashSet            as S
import qualified Data.HashMap.Strict     as M
import qualified Language.Fixpoint.Types as F


import           Language.Fixpoint.SortCheck (pruneUnsortedReft)



import           Liquid.GHC.API hiding (get, panic)
import           Language.Haskell.Liquid.Types.RefType
import qualified Language.Haskell.Liquid.GHC.SpanStack as Sp
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Fresh
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Types hiding (binds)
import           Language.Haskell.Liquid.Constraint.Types
import           Language.Haskell.Liquid.Constraint.Fresh ()
import           Language.Haskell.Liquid.Transforms.RefSplit
import qualified Language.Haskell.Liquid.UX.CTags       as Tg

-- import Debug.Trace (trace)
--------------------------------------------------------------------------------
-- | Refinement Type Environments ----------------------------------------------
--------------------------------------------------------------------------------

-- updREnvLocal :: REnv -> (_ -> _) -> REnv
updREnvLocal :: REnv
             -> (M.HashMap F.Symbol SpecType -> M.HashMap F.Symbol SpecType)
             -> REnv
updREnvLocal :: REnv
-> (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
    -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> REnv
updREnvLocal REnv
rE HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
f      = REnv
rE { reLocal = f (reLocal rE) }

-- RJ: REnv-Split-Bug?
filterREnv :: (SpecType -> Bool) -> REnv -> REnv
filterREnv :: (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool) -> REnv -> REnv
filterREnv RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
f REnv
rE        = REnv
rE REnv
-> (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
    -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> REnv
`updREnvLocal` (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall v k. (v -> Bool) -> HashMap k v -> HashMap k v
M.filter RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool
f

fromListREnv :: [(F.Symbol, SpecType)] -> [(F.Symbol, SpecType)] -> REnv
fromListREnv :: [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)] -> REnv
fromListREnv [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
gXts [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
lXts = REnv
  { reGlobal :: HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
reGlobal = [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
gXts
  , reLocal :: HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
reLocal  = [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
lXts
  }

-- RJ: REnv-Split-Bug?
deleteREnv :: F.Symbol -> REnv -> REnv
deleteREnv :: Symbol -> REnv -> REnv
deleteREnv Symbol
x REnv
rE = REnv
rE REnv
-> (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
    -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> REnv
`updREnvLocal` Symbol
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall k v. Hashable k => k -> HashMap k v -> HashMap k v
M.delete Symbol
x

insertREnv :: F.Symbol -> SpecType -> REnv -> REnv
insertREnv :: Symbol -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> REnv -> REnv
insertREnv Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
y REnv
rE = {- trace ("insertREnv: " ++ show x) $ -} REnv
rE REnv
-> (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
    -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> REnv
`updREnvLocal` Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
x RTypeBV Symbol Symbol RTyCon RTyVar RReft
y

lookupREnv :: F.Symbol -> REnv -> Maybe SpecType
lookupREnv :: Symbol -> REnv -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
lookupREnv Symbol
x REnv
rE = [Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
 -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> [Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ Symbol
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
x (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> [HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> [Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REnv
-> [HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
renvMaps REnv
rE

memberREnv :: F.Symbol -> REnv -> Bool
memberREnv :: Symbol -> REnv -> Bool
memberREnv Symbol
x REnv
rE = (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> Bool)
-> [HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> Bool
forall k a. Hashable k => k -> HashMap k a -> Bool
M.member Symbol
x) (REnv
-> [HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
renvMaps REnv
rE)

globalREnv :: REnv -> REnv
globalREnv :: REnv -> REnv
globalREnv (REnv HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
gM HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
lM) = HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> REnv
forall t. HashMap Symbol t -> HashMap Symbol t -> AREnv t
REnv HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
gM' HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall k v. HashMap k v
M.empty
  where
    gM' :: HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
gM'  = (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith (\RTypeBV Symbol Symbol RTyCon RTyVar RReft
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
gM HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
lM

renvMaps :: REnv -> [M.HashMap F.Symbol SpecType]
renvMaps :: REnv
-> [HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
renvMaps REnv
rE = [REnv -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall t. AREnv t -> HashMap Symbol t
reLocal REnv
rE, REnv -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall t. AREnv t -> HashMap Symbol t
reGlobal REnv
rE]

--------------------------------------------------------------------------------
localBindsOfType :: RRType r  -> REnv -> [F.Symbol]
--------------------------------------------------------------------------------
localBindsOfType :: forall r. RRType r -> REnv -> [Symbol]
localBindsOfType RRType r
tx REnv
γ = (Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> Symbol)
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REnv -> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
localsREnv ((RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Bool) -> REnv -> REnv
filterREnv ((RSort -> RSort -> Bool
forall a. Eq a => a -> a -> Bool
== RRType r -> RSort
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort RRType r
tx) (RSort -> Bool)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> RSort)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft -> RSort
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort) REnv
γ)

-- RJ: REnv-Split-Bug?
localsREnv :: REnv -> [(F.Symbol, SpecType)]
localsREnv :: REnv -> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
localsREnv = HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
-> (REnv
    -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> REnv
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REnv -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall t. AREnv t -> HashMap Symbol t
reLocal

globalsREnv :: REnv -> [(F.Symbol, SpecType)]
globalsREnv :: REnv -> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
globalsREnv = HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)])
-> (REnv
    -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> REnv
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REnv -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall t. AREnv t -> HashMap Symbol t
reGlobal

toListREnv :: REnv -> [(F.Symbol, SpecType)]
toListREnv :: REnv -> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
toListREnv REnv
re = REnv -> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
globalsREnv REnv
re [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall a. [a] -> [a] -> [a]
++ REnv -> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
localsREnv REnv
re

--------------------------------------------------------------------------------
extendEnvWithVV :: CGEnv -> SpecType -> CG CGEnv
--------------------------------------------------------------------------------
extendEnvWithVV :: CGEnv -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> CG CGEnv
extendEnvWithVV CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  | Symbol -> Bool
F.isNontrivialVV Symbol
vv Bool -> Bool -> Bool
&& Bool -> Bool
not (Symbol
vv Symbol -> REnv -> Bool
`memberREnv` CGEnv -> REnv
renv CGEnv
γ)
  = CGEnv
γ CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
+= (String
"extVV", Symbol
vv, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  | Bool
otherwise
  = CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ
  where
    vv :: ReftBind RReft
vv = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ReftBind RReft
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

addBinders :: CGEnv -> F.Symbol -> [(F.Symbol, SpecType)] -> CG CGEnv
addBinders :: CGEnv
-> Symbol
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> CG CGEnv
addBinders CGEnv
γ0 Symbol
x' [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
cbs   = (CGEnv
 -> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> CG CGEnv)
-> CGEnv
-> [(String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> CG CGEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
(++=) (CGEnv
γ0 CGEnv -> Symbol -> CGEnv
-= Symbol
x') [(String
"addBinders", Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) | (Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) <- [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
cbs]

addBind :: SrcSpan -> F.Symbol -> F.SortedReft -> CG ((F.Symbol, F.Sort), F.BindId)
addBind :: SrcSpan -> Symbol -> SortedReft -> CG ((Symbol, Sort), BindId)
addBind SrcSpan
l Symbol
x SortedReft
r = do
  st          <- StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  let (i, bs') = F.insertBindEnv x r (Ci l Nothing Nothing) (binds st)
  put          $ st { binds = bs' } { bindSpans = M.insert i l (bindSpans st) }
  return ((x, F.sr_sort r), {- traceShow ("addBind: " ++ showpp x) -} i)

-- | Add local rewrites associated to the next binding that will be inserted.
addRewritesForNextBinding :: F.LocalRewrites -> CG ()
addRewritesForNextBinding :: LocalRewrites -> StateT CGInfo Identity ()
addRewritesForNextBinding LocalRewrites
rws = do
  st <- StateT CGInfo Identity CGInfo
forall s (m :: * -> *). MonadState s m => m s
get
  let bid = BindEnv Cinfo -> BindId
forall a. BindEnv a -> BindId
F.bindEnvSize (BindEnv Cinfo -> BindId) -> BindEnv Cinfo -> BindId
forall a b. (a -> b) -> a -> b
$ CGInfo -> BindEnv Cinfo
binds CGInfo
st
  put $ st { localRewrites = F.insertRewrites bid rws $ localRewrites st }


addClassBind :: CGEnv -> SrcSpan -> SpecType -> CG [((F.Symbol, F.Sort), F.BindId)]
addClassBind :: CGEnv
-> SrcSpan
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> CG [((Symbol, Sort), BindId)]
addClassBind CGEnv
γ SrcSpan
l = ((Symbol, SortedReft) -> CG ((Symbol, Sort), BindId))
-> [(Symbol, SortedReft)] -> CG [((Symbol, Sort), BindId)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Symbol -> SortedReft -> CG ((Symbol, Sort), BindId))
-> (Symbol, SortedReft) -> CG ((Symbol, Sort), BindId)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SrcSpan -> Symbol -> SortedReft -> CG ((Symbol, Sort), BindId)
addBind SrcSpan
l)) ([(Symbol, SortedReft)] -> CG [((Symbol, Sort), BindId)])
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> [(Symbol, SortedReft)])
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> CG [((Symbol, Sort), BindId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [(Symbol, SortedReft)]
classBinds (CGEnv -> TCEmb TyCon
emb CGEnv
γ)

{- see tests/pos/polyfun for why you need everything in fixenv -}
addCGEnv :: (SpecType -> SpecType) -> CGEnv -> (String, F.Symbol, SpecType) -> CG CGEnv
addCGEnv :: (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
addCGEnv RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx CGEnv
γ (String
eMsg, Symbol
x, REx Symbol
y RTypeBV Symbol Symbol RTyCon RTyVar RReft
tyy RTypeBV Symbol Symbol RTyCon RTyVar RReft
tyx) = do
  y' <- StateT CGInfo Identity Symbol
forall (m :: * -> *) a. Freshable m a => m a
fresh
  γ' <- addCGEnv tx γ (eMsg, y', tyy)
  addCGEnv tx γ' (eMsg, x, tyx `F.subst1` (y, F.EVar y'))

addCGEnv RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx CGEnv
γ (String
eMsg, Symbol
sym, RAllE Symbol
yy RTypeBV Symbol Symbol RTyCon RTyVar RReft
tyy RTypeBV Symbol Symbol RTyCon RTyVar RReft
tyx)
  = (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
addCGEnv RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx CGEnv
γ (String
eMsg, Symbol
sym, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  where
    xs :: [Symbol]
xs            = RTypeBV Symbol Symbol RTyCon RTyVar RReft -> REnv -> [Symbol]
forall r. RRType r -> REnv -> [Symbol]
localBindsOfType RTypeBV Symbol Symbol RTyCon RTyVar RReft
tyy (CGEnv -> REnv
renv CGEnv
γ)
    t :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t             = (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [RTypeBV Symbol Symbol RTyCon RTyVar RReft]
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r. Meet r => r -> r -> r
meet RTypeBV Symbol Symbol RTyCon RTyVar RReft
ttrue [ RTypeBV Symbol Symbol RTyCon RTyVar RReft
tyx' RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft),
    ExprBV
      (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
      (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a.
Subable a =>
a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a
`F.subst1` (Symbol
Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
yy, Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
x) | Symbol
x <- [Symbol]
xs]
    (RTypeBV Symbol Symbol RTyCon RTyVar RReft
tyx', RTypeBV Symbol Symbol RTyCon RTyVar RReft
ttrue) = Symbol
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft,
    RTypeBV Symbol Symbol RTyCon RTyVar RReft)
splitXRelatedRefs Symbol
yy RTypeBV Symbol Symbol RTyCon RTyVar RReft
tyx

addCGEnv RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx CGEnv
γ (String
_, Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t') = do
  idx   <- StateT CGInfo Identity Integer
forall (m :: * -> *) a. Freshable m a => m a
fresh
  -- allowHOBinders <- allowHO <$> get
  let t  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tx (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Integer
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
normalize Integer
idx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'
  let l  = CGEnv -> SrcSpan
getLocation CGEnv
γ
  let γ' = CGEnv
γ { renv = insertREnv x t (renv γ) }
  tem   <- getTemplates
  is    <- (:) <$> addBind l x (rTypeSortedReft' γ' tem t) <*> addClassBind γ' l t
  return $ γ' { fenv = insertsFEnv (fenv γ) is }

rTypeSortedReft' :: (PPrint r, IsReft r, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol, SubsTy RTyVar RSort r)
    => CGEnv -> F.Templates -> RRType r -> F.SortedReft
rTypeSortedReft' :: forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
CGEnv -> Templates -> RRType r -> SortedReft
rTypeSortedReft' CGEnv
γ Templates
t
  = SEnv Sort -> Templates -> SortedReft -> SortedReft
pruneUnsortedReft (FEnv -> SEnv Sort
feEnv (FEnv -> SEnv Sort) -> FEnv -> SEnv Sort
forall a b. (a -> b) -> a -> b
$ CGEnv -> FEnv
fenv CGEnv
γ) Templates
t (SortedReft -> SortedReft)
-> (RTypeBV Symbol Symbol RTyCon RTyVar r -> SortedReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar r
-> SortedReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar r -> SortedReft
forall {r}.
(ReftBind r ~ Symbol, ReftVar r ~ Symbol, PPrint r, IsReft r,
 SubsTy RTyVar RSort r) =>
RRType r -> SortedReft
f
   where
   f :: RRType r -> SortedReft
f         = TCEmb TyCon -> RRType r -> SortedReft
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar RSort r) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft (CGEnv -> TCEmb TyCon
emb CGEnv
γ)


normalize :: Integer -> SpecType -> SpecType
normalize :: Integer
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
normalize Integer
idx = Integer
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
normalizeVV Integer
idx (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall c tv r. OkRT c tv r => RType c tv r -> RType c tv r
normalizePds

normalizeVV :: Integer -> SpecType -> SpecType
normalizeVV :: Integer
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
normalizeVV Integer
idx t :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
t@RApp{}
  | Bool -> Bool
not (Symbol -> Bool
F.isNontrivialVV (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> ReftBind RReft
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar RTypeBV Symbol Symbol RTyCon RTyVar RReft
t))
  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Symbol -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall c (f :: * -> *) tv.
(TyConable c, IsReft (f Reft), Functor f, Subable (f Reft),
 Variable (f Reft) ~ Variable Reft,
 ReftBind (f Reft) ~ ReftBind Reft) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV RTypeBV Symbol Symbol RTyCon RTyVar RReft
t (Maybe Integer -> Symbol
F.vv (Maybe Integer -> Symbol) -> Maybe Integer -> Symbol
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
idx)

normalizeVV Integer
_ RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  = RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

--------------------------------------------------------------------------------
(+=) :: CGEnv -> (String, F.Symbol, SpecType) -> CG CGEnv
--------------------------------------------------------------------------------
CGEnv
γ += :: CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
+= (String
eMsg, Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
r)
  | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
F.dummySymbol
  = CGEnv -> CG CGEnv
forall a. a -> StateT CGInfo Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return CGEnv
γ
  -- // | x `memberREnv` (renv γ)
  -- // = _dupBindErr x γ
  | Bool
otherwise
  =  CGEnv
γ CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
++= (String
eMsg, Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
r)

_dupBindError :: String -> F.Symbol -> CGEnv -> SpecType -> a
_dupBindError :: forall a.
String
-> Symbol
-> CGEnv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> a
_dupBindError String
eMsg Symbol
x CGEnv
γ RTypeBV Symbol Symbol RTyCon RTyVar RReft
r = Maybe SrcSpan -> String -> a
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
s
  where
    s :: String
s = [String] -> String
unlines [ String
eMsg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" Duplicate binding for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
F.symbolString Symbol
x
                , String
"   New: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> String
forall a. PPrint a => a -> String
showpp RTypeBV Symbol Symbol RTyCon RTyVar RReft
r
                , String
"   Old: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> String
forall a. PPrint a => a -> String
showpp (Symbol
x Symbol -> REnv -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
`lookupREnv` CGEnv -> REnv
renv CGEnv
γ) ]

--------------------------------------------------------------------------------
globalize :: CGEnv -> CGEnv
--------------------------------------------------------------------------------
globalize :: CGEnv -> CGEnv
globalize CGEnv
γ = CGEnv
γ {renv = globalREnv (renv γ)}

--------------------------------------------------------------------------------
(++=) :: CGEnv -> (String, F.Symbol, SpecType) -> CG CGEnv
--------------------------------------------------------------------------------
++= :: CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
(++=) CGEnv
γ (String
eMsg, Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
  = (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
addCGEnv (RTyConInv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addRTyConInv (([RInv] -> [RInv] -> [RInv]) -> RTyConInv -> RTyConInv -> RTyConInv
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith [RInv] -> [RInv] -> [RInv]
forall a. Monoid a => a -> a -> a
mappend (CGEnv -> RTyConInv
invs CGEnv
γ) (CGEnv -> RTyConInv
ial CGEnv
γ))) CGEnv
γ (String
eMsg, Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)

--------------------------------------------------------------------------------
addSEnv :: CGEnv -> (String, F.Symbol, SpecType) -> CG CGEnv
--------------------------------------------------------------------------------
addSEnv :: CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
addSEnv CGEnv
γ = (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
addCGEnv (RTyConInv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addRTyConInv (CGEnv -> RTyConInv
invs CGEnv
γ)) CGEnv
γ

addEEnv :: CGEnv -> (F.Symbol, SpecType) -> CG CGEnv
addEEnv :: CGEnv
-> (Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> CG CGEnv
addEEnv CGEnv
γ (Symbol
x,RTypeBV Symbol Symbol RTyCon RTyVar RReft
t')= do
  idx   <- StateT CGInfo Identity Integer
forall (m :: * -> *) a. Freshable m a => m a
fresh
  -- allowHOBinders <- allowHO <$> get
  let t  = RTyConInv
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
addRTyConInv (CGEnv -> RTyConInv
invs CGEnv
γ) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ Integer
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
normalize Integer
idx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t'
  let l  = CGEnv -> SrcSpan
getLocation CGEnv
γ
  let γ' = CGEnv
γ { renv = insertREnv x t (renv γ) }
  tem   <- getTemplates
  is    <- (:) <$> addBind l x (rTypeSortedReft' γ' tem t) <*> addClassBind γ' l t
  modify (\CGInfo
s -> CGInfo
s { ebinds = ebinds s ++ (snd <$> is)})
  return $ γ' { fenv = insertsFEnv (fenv γ) is }


(+++=) :: (CGEnv, String) -> (F.Symbol, CoreExpr, SpecType) -> CG CGEnv
(CGEnv
γ, String
_) +++= :: (CGEnv, String)
-> (Symbol, CoreExpr, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
+++= (Symbol
x, CoreExpr
e, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t) = (CGEnv
γ {lcb = M.insert x e (lcb γ) }) CGEnv
-> (String, Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> CG CGEnv
+= (String
"+++=", Symbol
x, RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)

(-=) :: CGEnv -> F.Symbol -> CGEnv
CGEnv
γ -= :: CGEnv -> Symbol -> CGEnv
-= Symbol
x =  CGEnv
γ { renv = deleteREnv x (renv γ)
            , lcb  = M.delete   x (lcb  γ)
            -- , fenv = removeFEnv x (fenv γ)
            }

(?=) :: (?callStack :: CallStack) => CGEnv -> F.Symbol -> Maybe SpecType
CGEnv
γ ?= :: HasCallStack =>
CGEnv
-> Symbol -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
?= Symbol
x  = Symbol -> REnv -> Maybe (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
lookupREnv Symbol
x (CGEnv -> REnv
renv CGEnv
γ)

------------------------------------------------------------------------
setLocation :: CGEnv -> Sp.Span -> CGEnv
------------------------------------------------------------------------
setLocation :: CGEnv -> Span -> CGEnv
setLocation CGEnv
γ Span
p = CGEnv
γ { cgLoc = Sp.push p $ cgLoc γ }

------------------------------------------------------------------------
setBind :: CGEnv -> Var -> CGEnv
------------------------------------------------------------------------
setBind :: CGEnv -> Var -> CGEnv
setBind CGEnv
γ Var
x = CGEnv
γ CGEnv -> Span -> CGEnv
`setLocation` Var -> Span
Sp.Var Var
x CGEnv -> Var -> CGEnv
`setBind'` Var
x

setBind' :: CGEnv -> Tg.TagKey -> CGEnv
setBind' :: CGEnv -> Var -> CGEnv
setBind' CGEnv
γ Var
k
  | Var -> TagEnv -> Bool
Tg.memTagEnv Var
k (CGEnv -> TagEnv
tgEnv CGEnv
γ) = CGEnv
γ { tgKey = Just k }
  | Bool
otherwise                = CGEnv
γ

------------------------------------------------------------------------
setRecs :: CGEnv -> [Var] -> CGEnv
------------------------------------------------------------------------
setRecs :: CGEnv -> [Var] -> CGEnv
setRecs CGEnv
γ [Var]
xs   = CGEnv
γ { recs = L.foldl' (flip S.insert) (recs γ) xs }

------------------------------------------------------------------------
setTRec :: CGEnv -> [(Var, SpecType)] -> CGEnv
------------------------------------------------------------------------
setTRec :: CGEnv
-> [(Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft)] -> CGEnv
setTRec CGEnv
γ [(Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
xts  = CGEnv
γ' {trec = Just $ M.fromList xts' `M.union` trec'}
  where
    γ' :: CGEnv
γ'         = CGEnv
γ CGEnv -> [Var] -> CGEnv
`setRecs` ((Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> Var
forall a b. (a, b) -> a
fst ((Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft) -> Var)
-> [(Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
xts)
    trec' :: HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
trec'      = HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> Maybe
     (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a. a -> Maybe a -> a
fromMaybe HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall k v. HashMap k v
M.empty (Maybe (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
 -> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> Maybe
     (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall a b. (a -> b) -> a -> b
$ CGEnv
-> Maybe
     (HashMap Symbol (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
trec CGEnv
γ
    xts' :: [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
xts'       = (Var -> Symbol)
-> (Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ((Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> (Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> [(Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
-> [(Symbol, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
xts