{-# LANGUAGE DeriveFoldable            #-}
{-# LANGUAGE DeriveTraversable         #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeSynonymInstances      #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE DeriveFunctor             #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ImplicitParams            #-}

-- | This module defines the representation of Subtyping and WF Constraints, and
-- the code for syntax-directed constraint generation.

module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints ) where

import Prelude hiding (error, undefined)

import GHC.Stack
import CoreUtils     (exprType)
import MkCore
import Coercion
import DataCon
import Pair
import CoreSyn
import SrcLoc
import Type
import TyCon
import PrelNames
import TypeRep
import Class            (className)
import Var
import Kind
import Id
import IdInfo
import Name
import NameSet
import Unify
import VarSet
-- import Unique


import Text.PrettyPrint.HughesPJ hiding (first)
import Control.Monad.State
-- import Control.Applicative      ((<$>), (<*>), Applicative)
-- import Data.Monoid              (mconcat, mempty, mappend)
import Data.Maybe               (fromMaybe, catMaybes, fromJust, isJust)
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S
import qualified Data.List           as L

import Data.Bifunctor
import qualified Data.Foldable    as F
import qualified Data.Traversable as T





import qualified Language.Haskell.Liquid.UX.CTags       as Tg



import Language.Fixpoint.Types.Visitor

import Language.Haskell.Liquid.Constraint.Fresh
import Language.Haskell.Liquid.Constraint.Env
import Language.Haskell.Liquid.Constraint.Monad
import Language.Haskell.Liquid.Constraint.Split

import qualified Language.Fixpoint.Types            as F

import Language.Haskell.Liquid.WiredIn          (dictionaryVar)
import Language.Haskell.Liquid.Types.Dictionaries

import qualified Language.Haskell.Liquid.GHC.SpanStack as Sp
import Language.Haskell.Liquid.Types            hiding (binds, Loc, loc, freeTyVars, Def)
import Language.Haskell.Liquid.Types.Strata
import Language.Haskell.Liquid.Types.Names

import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.Visitors         hiding (freeVars)
import Language.Haskell.Liquid.Types.PredType         hiding (freeTyVars)
import Language.Haskell.Liquid.Types.Meet
import Language.Haskell.Liquid.GHC.Misc          ( isInternal, collectArguments, tickSrcSpan
                                                 , hasBaseTypeVar, showPpr, isDataConId)
import Language.Haskell.Liquid.Misc
import Language.Fixpoint.Misc
import Language.Haskell.Liquid.Types.Literals

import Language.Haskell.Liquid.Constraint.Axioms
import Language.Haskell.Liquid.Constraint.Types
import Language.Haskell.Liquid.Constraint.Constraint

-- import Debug.Trace (trace)

-----------------------------------------------------------------------
------------- Constraint Generation: Toplevel -------------------------
-----------------------------------------------------------------------

generateConstraints      :: GhcInfo -> CGInfo
generateConstraints info = {-# SCC "ConsGen" #-} execState act $ initCGI cfg info
  where
    act                  = consAct info
    cfg                  = config $ spec info

consAct :: GhcInfo -> CG ()
consAct info
  = do γ'    <- initEnv      info
       sflag <- scheck   <$> get
       tflag <- trustghc <$> get
       γ     <- if expandProofsMode then addCombine τProof γ' else return γ'
       cbs'  <- if expandProofsMode then mapM (expandProofs info (mkSigs γ)) $ cbs info else return $ cbs info
       let trustBinding x = tflag && (x `elem` derVars info || isInternal x)
       foldM_ (consCBTop trustBinding) γ cbs'
       hcs   <- hsCs  <$> get
       hws   <- hsWfs <$> get
       scss  <- sCs   <$> get
       annot <- annotMap <$> get
       scs   <- if sflag then concat <$> mapM splitS (hcs ++ scss)
                         else return []
       let smap = if sflag then solveStrata scs else []
       let hcs' = if sflag then subsS smap hcs else hcs
       fcs <- concat <$> mapM splitC (subsS smap hcs')
       fws <- concat <$> mapM splitW hws
       let annot' = if sflag then subsS smap <$> annot else annot
       modify $ \st -> st { fEnv = fixEnv γ, fixCs = fcs , fixWfs = fws , annotMap = annot'}
  where
    expandProofsMode = autoproofs $ config $ spec info
    τProof           = proofType $ spec info
    fixEnv           = feEnv . fenv
    mkSigs γ         = toListREnv (renv  γ) ++
                       toListREnv (assms γ) ++
                       toListREnv (intys γ) ++
                       toListREnv (grtys γ)

addCombine τ γ
  = do t <- trueTy combineType
       γ ++= ("combineProofs", combineSymbol, t)
  where
    combineType   = makeCombineType τ
    combineVar    = makeCombineVar  combineType
    combineSymbol = F.symbol combineVar

------------------------------------------------------------------------------------
initEnv :: GhcInfo -> CG CGEnv
------------------------------------------------------------------------------------
initEnv info
  = do let tce   = tcEmbeds sp
       let fVars = impVars info
       let dcs   = filter isConLikeId ((snd <$> freeSyms sp))
       let dcs'  = filter isConLikeId fVars
       defaults <- forM fVars $ \x -> liftM (x,) (trueTy $ varType x)
       dcsty    <- forM dcs   $ makeDataConTypes
       dcsty'   <- forM dcs'  $ makeDataConTypes
       (hs,f0)  <- refreshHoles $ grty info                  -- asserted refinements     (for defined vars)
       f0''     <- refreshArgs' =<< grtyTop info             -- default TOP reftype      (for exported vars without spec)
       let f0'   = if notruetypes $ config sp then [] else f0''
       f1       <- refreshArgs'   defaults                   -- default TOP reftype      (for all vars)
       f1'      <- refreshArgs' $ makedcs dcsty
       f2       <- refreshArgs' $ assm info                  -- assumed refinements      (for imported vars)
       f3       <- refreshArgs' $ vals asmSigs sp            -- assumed refinedments     (with `assume`)
       f40      <- refreshArgs' $ vals ctors sp              -- constructor refinements  (for measures)
       f5       <- refreshArgs' $ vals inSigs sp             -- internal refinements     (from Haskell measures)
       (invs1, f41) <- mapSndM refreshArgs' $ makeAutoDecrDataCons dcsty  (autosize sp) dcs
       (invs2, f42) <- mapSndM refreshArgs' $ makeAutoDecrDataCons dcsty' (autosize sp) dcs'
       let f4    = mergeDataConTypes (mergeDataConTypes f40 (f41 ++ f42)) (filter (isDataConId . fst) f2)
       sflag    <- scheck <$> get
       let senv  = if sflag then f2 else []
       let tx    = mapFst F.symbol . addRInv ialias . strataUnify senv . predsUnify sp
       let bs    = (tx <$> ) <$> [f0 ++ f0', f1 ++ f1', f2, f3, f4, f5]
       lts      <- lits <$> get
       let tcb   = mapSnd (rTypeSort tce) <$> concat bs
       let γ0    = measEnv sp (head bs) (cbs info) (tcb ++ lts) (bs!!3) (bs!!5) hs (invs1 ++ invs2)
       globalize <$> foldM (++=) γ0 [("initEnv", x, y) | (x, y) <- concat $ tail bs]
  where
    sp           = spec info
    ialias       = mkRTyConIAl $ ialiases sp
    vals f       = map (mapSnd val) . f
    mapSndM f (x,y) = (x,) <$> f y
    makedcs      = map strengthenDataConType

makeDataConTypes x = (x,) <$> (trueTy $ varType x)

makeAutoDecrDataCons dcts specenv dcs
  = (simplify invs, tys)
  where
    (invs, tys) = unzip $ concatMap go tycons
    tycons      = L.nub $ catMaybes $ map idTyCon dcs

    go tycon
      | S.member tycon specenv =  zipWith (makeSizedDataCons dcts) (tyConDataCons tycon) [0..]
    go _
      = []
    idTyCon x = dataConTyCon <$> case idDetails x of {DataConWorkId d -> Just d; DataConWrapId d -> Just d; _ -> Nothing}

    simplify invs = dummyLoc . (`strengthen` invariant) .  fmap (\_ -> mempty) <$> L.nub invs
    invariant = MkUReft (F.Reft (F.vv_, F.PAtom F.Ge (lenOf F.vv_) (F.ECon $ F.I 0)) ) mempty mempty

lenOf x = F.mkEApp lenLocSymbol [F.EVar x]

makeSizedDataCons dcts x' n = (toRSort $ ty_res trep, (x, fromRTypeRep trep{ty_res = tres}))
    where
      x      = dataConWorkId x'
      t      = fromMaybe (impossible Nothing "makeSizedDataCons: this should never happen") $ L.lookup x dcts
      trep   = toRTypeRep t
      tres   = ty_res trep `strengthen` MkUReft (F.Reft (F.vv_, F.PAtom F.Eq (lenOf F.vv_) computelen)) mempty mempty

      recarguments = filter (\(t,_) -> (toRSort t == toRSort tres)) (zip (ty_args trep) (ty_binds trep))
      computelen   = foldr (F.EBin F.Plus) (F.ECon $ F.I n) (lenOf .  snd <$> recarguments)

mergeDataConTypes ::  [(Var, SpecType)] -> [(Var, SpecType)] -> [(Var, SpecType)]
mergeDataConTypes xts yts = merge (L.sortBy f xts) (L.sortBy f yts)
  where
    f (x,_) (y,_) = compare x y
    merge [] ys = ys
    merge xs [] = xs
    merge (xt@(x, tx):xs) (yt@(y, ty):ys)
      | x == y    = (x, mXY x tx y ty) : merge xs ys
      | x <  y    = xt : merge xs (yt : ys)
      | otherwise = yt : merge (xt : xs) ys
    mXY x tx y ty = meetVarTypes (pprint x) (getSrcSpan x, tx) (getSrcSpan y, ty)

refreshHoles vts = first catMaybes . unzip . map extract <$> mapM refreshHoles' vts
refreshHoles' (x,t)
  | noHoles t = return (Nothing, x, t)
  | otherwise = (Just $ F.symbol x,x,) <$> mapReftM tx t
  where
    tx r | hasHole r = refresh r
         | otherwise = return r
extract (a,b,c) = (a,(b,c))

refreshArgs' = mapM (mapSndM refreshArgs)

strataUnify :: [(Var, SpecType)] -> (Var, SpecType) -> (Var, SpecType)
strataUnify senv (x, t) = (x, maybe t (mappend t) pt)
  where
    pt                  = fmap (\(MkUReft _ _ l) -> MkUReft mempty mempty l) <$> L.lookup x senv


-- | TODO: All this *should* happen inside @Bare@ but appears
--   to happen after certain are signatures are @fresh@-ed,
--   which is why they are here.

-- NV : still some sigs do not get TyConInfo

predsUnify :: GhcSpec -> (Var, RRType RReft) -> (Var, RRType RReft)
predsUnify sp = second (addTyConInfo tce tyi) -- needed to eliminate some @RPropH@
  where
    tce            = tcEmbeds sp
    tyi            = tyconEnv sp

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

measEnv sp xts cbs lts asms itys hs autosizes
  = CGE { cgLoc = Sp.empty
        , renv  = fromListREnv (second val <$> meas sp) []
        , syenv = F.fromListSEnv $ freeSyms sp
        , fenv  = initFEnv $ lts ++ (second (rTypeSort tce . val) <$> meas sp)
        , denv  = dicts sp
        , recs  = S.empty
        , invs  = mkRTyConInv    $ (invariants sp ++ autosizes)
        , ial   = mkRTyConIAl    $ ialiases   sp
        , grtys = fromListREnv xts  []
        , assms = fromListREnv asms []
        , intys = fromListREnv itys []
        , emb   = tce
        , tgEnv = Tg.makeTagEnv cbs
        , tgKey = Nothing
        , trec  = Nothing
        , lcb   = M.empty
        , holes = fromListHEnv hs
        , lcs   = mempty
        , aenv  = axiom_map $ logicMap sp
        , cerr  = Nothing 
        }
    where
      tce = tcEmbeds sp

assm = assmGrty impVars
grty = assmGrty defVars

assmGrty f info = [ (x, val t) | (x, t) <- sigs, x `S.member` xs ]
  where
    xs          = S.fromList $ f info
    sigs        = tySigs     $ spec info

grtyTop info     = forM topVs $ \v -> (v,) <$> trueTy (varType v)
  where
    topVs        = filter isTop $ defVars info
    isTop v      = isExportedId v && not (v `S.member` sigVs)
    isExportedId = flip elemNameSet (exports $ spec info) . getName
    sigVs        = S.fromList [v | (v,_) <- tySigs (spec info) ++ asmSigs (spec info) ++ inSigs (spec info)]

initCGI cfg info = CGInfo {
    fEnv       = F.emptySEnv
  , hsCs       = []
  , sCs        = []
  , hsWfs      = []
  , fixCs      = []
  , isBind     = []
  , fixWfs     = []
  , freshIndex = 0
  , binds      = F.emptyBindEnv
  , annotMap   = AI M.empty
  , tyConInfo  = tyi
  , tyConEmbed = tce
  , kuts       = mempty -- F.ksEmpty
  , lits       = coreBindLits tce info ++  (map (mapSnd F.sr_sort) $ map mkSort $ meas spc)
  , termExprs  = M.fromList $ texprs spc
  , specDecr   = decr spc
  , specLVars  = lvars spc
  , specLazy   = dictionaryVar `S.insert` lazy spc
  , tcheck     = not $ notermination cfg
  , scheck     = strata cfg
  , trustghc   = trustinternals cfg
  , pruneRefs  = not $ noPrune cfg
  , logErrors  = []
  , kvProf     = emptyKVProf
  , recCount   = 0
  , bindSpans  = M.empty
  , autoSize   = autosize spc
  , allowHO    = higherorder cfg   
  }
  where
    tce        = tcEmbeds spc
    spc        = spec info
    tyi        = tyconEnv spc
    mkSort = mapSnd (rTypeSortedReft tce . val)

coreBindLits :: F.TCEmb TyCon -> GhcInfo -> [(F.Symbol, F.Sort)]
coreBindLits tce info
  = sortNub      $ [ (F.symbol x, F.strSort) | (_, Just (F.ESym x)) <- lconsts ]    -- strings
                ++ [ (dconToSym dc, dconToSort dc) | dc <- dcons ]                  -- data constructors
  where
    lconsts      = literalConst tce <$> literals (cbs info)
    dcons        = filter isDCon freeVs
    freeVs       = impVars info ++ (snd <$> freeSyms (spec info))
    dconToSort   = typeSort tce . expandTypeSynonyms . varType
    dconToSym    = F.symbol . idDataCon
    isDCon x     = isDataConId x && not (hasBaseTypeVar x)

-------------------------------------------------------------------
-- | Generation: Freshness ---------------------------------------
-------------------------------------------------------------------

-- | Right now, we generate NO new pvars. Rather than clutter code
--   with `uRType` calls, put it in one place where the above
--   invariant is /obviously/ enforced.
--   Constraint generation should ONLY use @freshTy_type@ and @freshTy_expr@

freshTy_type        :: KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_type k _ τ  = freshTy_reftype k $ ofType τ

freshTy_expr        :: KVKind -> CoreExpr -> Type -> CG SpecType
freshTy_expr k e _  = freshTy_reftype k $ exprRefType e

freshTy_reftype     :: KVKind -> SpecType -> CG SpecType
freshTy_reftype k t = (fixTy t >>= refresh) =>> addKVars k

-- | Used to generate "cut" kvars for fixpoint. Typically, KVars for recursive
--   definitions, and also to update the KVar profile.
addKVars        :: KVKind -> SpecType -> CG ()
addKVars !k !t  = do when (True)    $ modify $ \s -> s { kvProf = updKVProf k kvars (kvProf s) }
                     when (isKut k) $ modify $ \s -> s { kuts   = mappend   kvars   (kuts s)   }
  where
     kvars      = F.KS $ S.fromList $ specTypeKVars t

isKut          :: KVKind -> Bool
isKut RecBindE = True
isKut _        = False

specTypeKVars :: SpecType -> [F.KVar]
specTypeKVars = foldReft (\ _ r ks -> (kvars $ ur_reft r) ++ ks) []

trueTy  :: Type -> CG SpecType
trueTy = ofType' >=> true

ofType' :: Type -> CG SpecType
ofType' = fixTy . ofType

fixTy :: SpecType -> CG SpecType
fixTy t = do tyi   <- tyConInfo  <$> get
             tce   <- tyConEmbed <$> get
             return $ addTyConInfo tce tyi t

refreshArgsTop :: (Var, SpecType) -> CG SpecType
refreshArgsTop (x, t)
  = do (t', su) <- refreshArgsSub t
       modify $ \s -> s {termExprs = M.adjust (F.subst su <$>) x $ termExprs s}
       return t'

refreshArgs :: SpecType -> CG SpecType
refreshArgs t
  = fst <$> refreshArgsSub t


-- NV TODO: this does not refresh args if they are wrapped in an RRTy
refreshArgsSub :: SpecType -> CG (SpecType, F.Subst)
refreshArgsSub t
  = do ts     <- mapM refreshArgs ts_u
       xs'    <- mapM (\_ -> fresh) xs
       let sus = F.mkSubst <$> (L.inits $ zip xs (F.EVar <$> xs'))
       let su  = last sus
       let ts' = zipWith F.subst sus ts
       let t'  = fromRTypeRep $ trep {ty_binds = xs', ty_args = ts', ty_res = F.subst su tbd}
       return (t', su)
    where
       trep    = toRTypeRep t
       xs      = ty_binds trep
       ts_u    = ty_args  trep
       tbd     = ty_res   trep

-------------------------------------------------------------------------------
-- | TERMINATION TYPE --------------------------------------
-------------------------------------------------------------------------------

makeDecrIndex :: (Var, Template SpecType)-> CG [Int]
makeDecrIndex (x, Assumed t)
  = do dindex <- makeDecrIndexTy x t
       case dindex of
         Left _  -> return []
         Right i -> return i
makeDecrIndex (x, Asserted t)
  = do dindex <- makeDecrIndexTy x t
       case dindex of
         Left msg -> addWarning msg >> return []
         Right i  -> return i
makeDecrIndex _ = return []

makeDecrIndexTy x t
  = do spDecr <- specDecr <$> get
       autosz <- autoSize <$> get
       hint   <- checkHint' autosz (L.lookup x $ spDecr)
       case dindex autosz of
         Nothing -> return $ Left msg
         Just i  -> return $ Right $ fromMaybe [i] hint
    where
       ts         = ty_args trep
       checkHint' = \autosz -> checkHint x ts (isDecreasing autosz cenv)
       dindex     = \autosz -> L.findIndex    (isDecreasing autosz cenv) ts
       msg        = ErrTermin (getSrcSpan x) [pprint x] (text "No decreasing parameter")
       cenv       = makeNumEnv ts
       trep       = toRTypeRep $ unOCons t


recType _ ((_, []), (_, [], t))
  = t

recType autoenv ((vs, indexc), (_, index, t))
  = makeRecType autoenv t v dxt index
  where v    = (vs !!)  <$> indexc
        dxt  = (xts !!) <$> index
        xts  = zip (ty_binds trep) (ty_args trep)
        trep = toRTypeRep $ unOCons t

-- checkIndex :: (Var, _, _ , _) -> _
checkIndex (x, vs, t, index)
  = do mapM_ (safeLogIndex msg1 vs) index
       mapM  (safeLogIndex msg2 ts) index
    where
       loc   = getSrcSpan x
       ts    = ty_args $ toRTypeRep $ unOCons $ unTemplate t
       msg1  = ErrTermin loc [xd] ("No decreasing" <+>  pprint index <> "-th argument on" <+> xd <+> "with" <+> (pprint vs))
       msg2  = ErrTermin loc [xd] "No decreasing parameter"
       xd    = pprint x

makeRecType autoenv t vs dxs is
  = mergecondition t $ fromRTypeRep $ trep {ty_binds = xs', ty_args = ts'}
  where
    (xs', ts') = unzip $ replaceN (last is) (makeDecrType autoenv vdxs) xts
    vdxs       = zip vs dxs
    xts        = zip (ty_binds trep) (ty_args trep)
    trep       = toRTypeRep $ unOCons t

unOCons (RAllT v t)        = RAllT v $ unOCons t
unOCons (RAllP p t)        = RAllP p $ unOCons t
unOCons (RFun x tx t r)    = RFun x (unOCons tx) (unOCons t) r
unOCons (RRTy _ _ OCons t) = unOCons t
unOCons t                  = t


mergecondition (RAllT _ t1) (RAllT v t2)
  = RAllT v $ mergecondition t1 t2
mergecondition (RAllP _ t1) (RAllP p t2)
  = RAllP p $ mergecondition t1 t2
mergecondition (RRTy xts r OCons t1) t2
  = RRTy xts r OCons (mergecondition t1 t2)
mergecondition (RFun _ t11 t12 _) (RFun x2 t21 t22 r2)
  = RFun x2 (mergecondition t11 t21) (mergecondition t12 t22) r2
mergecondition _ t
  = t

safeLogIndex err ls n
  | n >= length ls = addWarning err >> return Nothing
  | otherwise      = return $ Just $ ls !! n

checkHint _ _ _ Nothing
  = return Nothing

checkHint x _ _ (Just ns) | L.sort ns /= ns
  = addWarning (ErrTermin loc [dx] (text "The hints should be increasing")) >> return Nothing
  where
    loc = getSrcSpan x
    dx  = pprint x

checkHint x ts f (Just ns)
  = (mapM (checkValidHint x ts f) ns) >>= (return . Just . catMaybes)

checkValidHint x ts f n
  | n < 0 || n >= length ts = addWarning err >> return Nothing
  | f (ts L.!! n)           = return $ Just n
  | otherwise               = addWarning err >> return Nothing
  where
    err = ErrTermin loc [xd] (vcat [ "Invalid Hint" <+> pprint (n+1) <+> "for" <+> xd
                                   , "in"
                                   , pprint ts ])
    loc = getSrcSpan x
    xd  = pprint x

--------------------------------------------------------------------------------
consCBLet :: CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
consCBLet γ cb
  = do oldtcheck <- tcheck <$> get
       strict    <- specLazy <$> get
       let tflag  = oldtcheck
       let isStr  = tcond cb strict
       -- TODO: yuck.
       modify $ \s -> s { tcheck = tflag && isStr }
       γ' <- consCB (tflag && isStr) isStr γ cb
       modify $ \s -> s{tcheck = oldtcheck}
       return γ'

--------------------------------------------------------------------------------
-- | Constraint Generation: Corebind -------------------------------------------
--------------------------------------------------------------------------------
consCBTop :: (Var -> Bool) -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------
consCBTop trustBinding γ cb | all trustBinding xs
  = do ts <- mapM trueTy (varType <$> xs)
       foldM (\γ xt -> (γ, "derived") += xt) γ (zip xs' ts)
    where
       xs  = bindersOf cb
       xs' = F.symbol <$> xs

consCBTop _ γ cb
  = do oldtcheck <- tcheck <$> get
       strict    <- specLazy <$> get
       let tflag  = oldtcheck
       let isStr  = tcond cb strict
       modify $ \s -> s { tcheck = tflag && isStr}
       γ' <- consCB (tflag && isStr) isStr γ cb
       modify $ \s -> s { tcheck = oldtcheck}
       return γ'

tcond cb strict
  = not $ any (\x -> S.member x strict || isInternal x) (binds cb)
  where
    binds (NonRec x _) = [x]
    binds (Rec xes)    = fst $ unzip xes

--------------------------------------------------------------------------------
consCB :: Bool -> Bool -> CGEnv -> CoreBind -> CG CGEnv
--------------------------------------------------------------------------------

-- RJ: AAAAAAARGHHH!!!!!! THIS CODE IS HORRIBLE!!!!!!!!!
consCBSizedTys γ xes
  = do xets''    <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))
       sflag     <- scheck <$> get
       autoenv   <- autoSize <$> get
       let cmakeFinType = if sflag then makeFinType else id
       let cmakeFinTy   = if sflag then makeFinTy   else snd
       let xets = mapThd3 (fmap cmakeFinType) <$> xets''
       ts'      <- mapM (T.mapM refreshArgs) $ (thd3 <$> xets)
       let vs    = zipWith collectArgs ts' es
       is       <- mapM makeDecrIndex (zip xs ts') >>= checkSameLens
       let ts = cmakeFinTy  <$> zip is ts'
       let xeets = (\vis -> [(vis, x) | x <- zip3 xs is $ map unTemplate ts]) <$> (zip vs is)
       (L.transpose <$> mapM checkIndex (zip4 xs vs ts is)) >>= checkEqTypes
       let rts   = (recType autoenv <$>) <$> xeets
       let xts   = zip xs ts
       γ'       <- foldM extender γ xts
       let γs    = [γ' `setTRec` (zip xs rts') | rts' <- rts]
       let xets' = zip3 xs es ts
       mapM_ (uncurry $ consBind True) (zip γs xets')
       return γ'
  where
       (xs, es)       = unzip xes
       dxs            = pprint <$> xs
       collectArgs    = collectArguments . length . ty_binds . toRTypeRep . unOCons . unTemplate
       checkEqTypes :: [[Maybe SpecType]] -> CG [[SpecType]]
       checkEqTypes x = mapM (checkAll err1 toRSort) (catMaybes <$> x)
       checkSameLens  = checkAll err2 length
       err1           = ErrTermin loc dxs $ text "The decreasing parameters should be of same type"
       err2           = ErrTermin loc dxs $ text "All Recursive functions should have the same number of decreasing parameters"
       loc            = getSrcSpan (head xs)

       checkAll _   _ []            = return []
       checkAll err f (x:xs)
         | all (==(f x)) (f <$> xs) = return (x:xs)
         | otherwise                = addWarning err >> return []

consCBWithExprs γ xes
  = do xets'     <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))
       texprs <- termExprs <$> get
       let xtes = catMaybes $ (`lookup` texprs) <$> xs
       sflag     <- scheck <$> get
       let cmakeFinType = if sflag then makeFinType else id
       let xets  = mapThd3 (fmap cmakeFinType) <$> xets'
       let ts    = safeFromAsserted err . thd3 <$> xets
       ts'      <- mapM refreshArgs ts
       let xts   = zip xs (Asserted <$> ts')
       γ'       <- foldM extender γ xts
       let γs    = makeTermEnvs γ' xtes xes ts ts'
       let xets' = zip3 xs es (Asserted <$> ts')
       mapM_ (uncurry $ consBind True) (zip γs xets')
       return γ'
  where (xs, es) = unzip xes
        lookup k m | Just x <- M.lookup k m = Just (k, x)
                   | otherwise              = Nothing
        err      = "Constant: consCBWithExprs"

makeFinTy (ns, t) = fmap go t
  where
    go t = fromRTypeRep $ trep {ty_args = args'}
      where
        trep = toRTypeRep t
        args' = mapNs ns makeFinType $ ty_args trep

makeTermEnvs γ xtes xes ts ts' = setTRec γ . zip xs <$> rts
  where
    vs   = zipWith collectArgs ts es
    ys   = (fst4 . bkArrowDeep) <$> ts
    ys'  = (fst4 . bkArrowDeep) <$> ts'
    sus' = zipWith mkSub ys ys'
    sus  = zipWith mkSub ys ((F.symbol <$>) <$> vs)
    ess  = (\x -> (safeFromJust (err x) $ (x `L.lookup` xtes))) <$> xs
    tes  = zipWith (\su es -> F.subst su <$> es)  sus ess
    tes' = zipWith (\su es -> F.subst su <$> es)  sus' ess
    rss  = zipWith makeLexRefa tes' <$> (repeat <$> tes)
    rts  = zipWith (addObligation OTerm) ts' <$> rss
    (xs, es)     = unzip xes
    mkSub ys ys' = F.mkSubst [(x, F.EVar y) | (x, y) <- zip ys ys']
    collectArgs  = collectArguments . length . ty_binds . toRTypeRep
    err x        = "Constant: makeTermEnvs: no terminating expression for " ++ showPpr x

addObligation :: Oblig -> SpecType -> RReft -> SpecType
addObligation o t r  = mkArrow αs πs ls xts $ RRTy [] r o t2
  where
    (αs, πs, ls, t1) = bkUniv t
    (xs, ts, rs, t2) = bkArrow t1
    xts              = zip3 xs ts rs


consCB tflag _ γ (Rec xes) | tflag
  = do texprs <- termExprs <$> get
       modify $ \i -> i { recCount = recCount i + length xes }
       let xxes = catMaybes $ (`lookup` texprs) <$> xs
       if null xxes
         then consCBSizedTys γ xes
         else check xxes <$> consCBWithExprs γ xes
    where
      xs = fst $ unzip xes
      check ys r | length ys == length xs = r
                 | otherwise              = panic (Just loc) $ msg
      msg        = "Termination expressions must be provided for all mutually recursive binders"
      loc        = getSrcSpan (head xs)
      lookup k m = (k,) <$> M.lookup k m

consCB _ str γ (Rec xes) | not str
  = do xets'   <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))
       sflag     <- scheck <$> get
       let cmakeDivType = if sflag then makeDivType else id
       let xets = mapThd3 (fmap cmakeDivType) <$> xets'
       modify $ \i -> i { recCount = recCount i + length xes }
       let xts = [(x, to) | (x, _, to) <- xets]
       γ'     <- foldM extender (γ `setRecs` (fst <$> xts)) xts
       mapM_ (consBind True γ') xets
       return γ'

consCB _ _ γ (Rec xes)
  = do xets   <- forM xes $ \(x, e) -> liftM (x, e,) (varTemplate γ (x, Just e))
       modify $ \i -> i { recCount = recCount i + length xes }
       let xts = [(x, to) | (x, _, to) <- xets]
       γ'     <- foldM extender (γ `setRecs` (fst <$> xts)) xts
       mapM_ (consBind True γ') xets
       return γ'

-- | NV: Dictionaries are not checked, because
-- | class methods' preconditions are not satisfied
consCB _ _ γ (NonRec x _) | isDictionary x
  = do t  <- trueTy (varType x)
       extender γ (x, Assumed t)
  where
    isDictionary = isJust . dlookup (denv γ)


consCB _ _ γ (NonRec x (App (Var w) (Type τ)))
  | Just d <- dlookup (denv γ) w
  = do t      <- trueTy τ
       addW    $ WfC γ t
       let xts = dmap (f t) d
       let  γ' = γ{denv = dinsert (denv γ) x xts }
       t      <- trueTy (varType x)
       extender γ' (x, Assumed t)
   where
       f t' (RAllT α te) = subsTyVar_meet' (α, t') te
       f _ _ = impossible Nothing "consCB on Dictionary: this should not happen"

consCB _ _ γ (NonRec x e)
  = do to  <- varTemplate γ (x, Nothing)
       to' <- consBind False γ (x, e, to) >>= (addPostTemplate γ)
       extender γ (x, to')

--------------------------------------------------------------------------------
consBind :: Bool
         -> CGEnv
         -> (Var, CoreExpr ,Template SpecType)
         -> CG (Template SpecType)
--------------------------------------------------------------------------------
consBind _ _ (x, _, t)
  | RecSelId {} <- idDetails x -- don't check record selectors
  = return t

consBind isRec γ (x, e, Asserted spect)
  = do let γ'         = γ `setBind` x
           (_,πs,_,_) = bkUniv spect
       γπ    <- foldM addPToEnv γ' πs
       cconsE γπ e spect
       when (F.symbol x `elemHEnv` holes γ) $
         -- have to add the wf constraint here for HOLEs so we have the proper env
         addW $ WfC γπ $ fmap killSubst spect
       addIdA x (defAnn isRec spect)
       return $ Asserted spect -- Nothing

consBind isRec γ (x, e, Internal spect)
  = do let γ'         = γ `setBind` x
           (_,πs,_,_) = bkUniv spect
       γπ    <- foldM addPToEnv γ' πs
       let γπ' = γπ {cerr = Just $ ErrHMeas (getLocation γπ) (pprint x) (text explanation)}
       cconsE γπ' e spect
       when (F.symbol x `elemHEnv` holes γ) $
         -- have to add the wf constraint here for HOLEs so we have the proper env
         addW $ WfC γπ $ fmap killSubst spect
       addIdA x (defAnn isRec spect)
       return $ Internal spect -- Nothing
  where
    explanation = "Cannot give singleton type to the function definition."


consBind isRec γ (x, e, Assumed spect)
  = do let γ' = γ `setBind` x
       γπ    <- foldM addPToEnv γ' πs
       cconsE γπ e =<< true spect
       addIdA x (defAnn isRec spect)
       return $ Asserted spect -- Nothing
  where πs   = ty_preds $ toRTypeRep spect

consBind isRec γ (x, e, Unknown)
  = do t     <- consE (γ `setBind` x) e
       addIdA x (defAnn isRec t)
       return $ Asserted t


noHoles = and . foldReft (\_ r bs -> not (hasHole r) : bs) []

killSubst :: RReft -> RReft
killSubst = fmap killSubstReft

killSubstReft :: F.Reft -> F.Reft
killSubstReft = trans kv () ()
  where
    kv    = defaultVisitor { txExpr = ks }
    ks _ (F.PKVar k _) = F.PKVar k mempty
    ks _ p             = p

    -- tx (F.Reft (s, rs)) = F.Reft (s, map f rs)
    -- f (F.RKvar k _)     = F.RKvar k mempty
    -- f (F.RConc p)       = F.RConc p

defAnn True  = AnnRDf
defAnn False = AnnDef

addPToEnv γ π
  = do γπ <- γ ++= ("addSpec1", pname π, pvarRType π)
       foldM (++=) γπ [("addSpec2", x, ofRSort t) | (t, x, _) <- pargs π]

extender γ (x, Asserted t) = γ ++= ("extender", F.symbol x, t)
extender γ (x, Assumed t)  = γ ++= ("extender", F.symbol x, t)
extender γ _               = return γ


data Template a = Asserted a | Assumed a | Internal a | Unknown deriving (Functor, F.Foldable, T.Traversable)

deriving instance (Show a) => (Show (Template a))

unTemplate (Asserted t) = t
unTemplate (Assumed t)  = t
unTemplate (Internal t) = t 
unTemplate _ = panic Nothing "Constraint.Generate.unTemplate called on `Unknown`"

addPostTemplate γ (Asserted t) = Asserted <$> addPost γ t
addPostTemplate γ (Assumed  t) = Assumed  <$> addPost γ t
addPostTemplate γ (Internal t) = Internal  <$> addPost γ t
addPostTemplate _ Unknown      = return Unknown

safeFromAsserted _ (Asserted t) = t
safeFromAsserted msg _ = panic Nothing $ "safeFromAsserted:" ++ msg

-- | @varTemplate@ is only called with a `Just e` argument when the `e`
-- corresponds to the body of a @Rec@ binder.
varTemplate :: CGEnv -> (Var, Maybe CoreExpr) -> CG (Template SpecType)
varTemplate γ (x, eo)
  = case (eo, lookupREnv (F.symbol x) (grtys γ), lookupREnv (F.symbol x) (assms γ), lookupREnv (F.symbol x) (intys γ)) of
      (_, Just t, _, _) -> Asserted <$> refreshArgsTop (x, t)
      (_, _, _, Just t) -> Internal <$> refreshArgsTop (x, t)
      (_, _, Just t, _) -> Assumed  <$> refreshArgsTop (x, t)
      (Just e, _, _, _) -> do t  <- freshTy_expr RecBindE e (exprType e)
                              addW (WfC γ t)
                              Asserted <$> refreshArgsTop (x, t)
      (_,      _, _, _) -> return Unknown

--------------------------------------------------------------------------------
-- | Constraint Generation: Checking -------------------------------------------
--------------------------------------------------------------------------------
cconsE :: CGEnv -> Expr Var -> SpecType -> CG ()
--------------------------------------------------------------------------------
cconsE g e t = do
  -- Note: tracing goes here
  -- traceM $ printf "cconsE:\n  expr = %s\n  exprType = %s\n  lqType = %s\n" (showPpr e) (showPpr (exprType e)) (showpp t)
  cconsE' g e t

cconsE' :: CGEnv -> Expr Var -> SpecType -> CG ()
cconsE' γ e@(Let b@(NonRec x _) ee) t
  = do sp <- specLVars <$> get
       if (x `S.member` sp) || isDefLazyVar x
        then cconsLazyLet γ e t
        else do γ'  <- consCBLet γ b
                cconsE γ' ee t
  where
       isDefLazyVar = L.isPrefixOf "fail" . showPpr

cconsE' γ e (RAllP p t)
  = cconsE γ' e t''
  where
    t'         = replacePredsWithRefs su <$> t
    su         = (uPVar p, pVartoRConc p)
    (css, t'') = splitConstraints t'
    γ'         = L.foldl' addConstraints γ css

cconsE' γ (Let b e) t
  = do γ'  <- consCBLet γ b
       cconsE γ' e t

cconsE' γ (Case e x _ cases) t
  = do γ'  <- consCBLet γ (NonRec x e)
       forM_ cases $ cconsCase γ' x t nonDefAlts
    where
       nonDefAlts = [a | (a, _, _) <- cases, a /= DEFAULT]

cconsE' γ (Lam α e) (RAllT _ t) | isKindVar α
  = cconsE γ e t

cconsE' γ (Lam α e) (RAllT α' t) | isTyVar α
  = cconsE γ e $ subsTyVar_meet' (α', rVar α) t

cconsE' γ (Lam x e) (RFun y ty t _)
  | not (isTyVar x)
  = do γ' <- (γ, "cconsE") += (F.symbol x, ty)
       cconsE γ' e (t `F.subst1` (y, F.EVar $ F.symbol x))
       addIdA x (AnnDef ty)

cconsE' γ (Tick tt e) t
  = cconsE (γ `setLocation` (Sp.Tick tt)) e t

cconsE' γ (Cast e co) t
  -- See Note [Type classes with a single method]
  | Just f <- isClassConCo co
  = cconsE γ (f e) t

cconsE' γ e@(Cast e' _) t
  = do t' <- castTy γ (exprType e) e'
       addC (SubC γ t' t) ("cconsE Cast: " ++ showPpr e)

cconsE' γ e t
  = do te  <- consE γ e
       te' <- instantiatePreds γ e te >>= addPost γ
       addC (SubC γ te' t) ("cconsE: " ++ showPpr e)


splitConstraints (RRTy cs _ OCons t)
  = let (css, t') = splitConstraints t in (cs:css, t')
splitConstraints (RFun x tx@(RApp c _ _ _) t r) | isClass c
  = let (css, t') = splitConstraints t in (css, RFun x tx t' r)
splitConstraints t
  = ([], t)

-------------------------------------------------------------------
-- | @instantiatePreds@ peels away the universally quantified @PVars@
--   of a @RType@, generates fresh @Ref@ for them and substitutes them
--   in the body.
-------------------------------------------------------------------
instantiatePreds γ e (RAllP π t)
  = do r     <- freshPredRef γ e π
       instantiatePreds γ e $ replacePreds "consE" t [(π, r)]

instantiatePreds _ _ t0
  = return t0

-------------------------------------------------------------------
-- | @instantiateStrata@ generates fresh @Strata@ vars and substitutes
--   them inside the body of the type.
-------------------------------------------------------------------

instantiateStrata ls t = substStrata t ls <$> mapM (\_ -> fresh) ls

substStrata t ls ls'   = F.substa f t
  where
    f x                = fromMaybe x $ L.lookup x su
    su                 = zip ls ls'

-------------------------------------------------------------------
cconsLazyLet γ (Let (NonRec x ex) e) t
  = do tx <- trueTy (varType x)
       γ' <- (γ, "Let NonRec") +++= (x', ex, tx)
       cconsE γ' e t
    where
       x' = F.symbol x

cconsLazyLet _ _ _
  = panic Nothing "Constraint.Generate.cconsLazyLet called on invalid inputs"

--------------------------------------------------------------------------------
-- | Type Synthesis ------------------------------------------------------------
--------------------------------------------------------------------------------
consE :: CGEnv -> Expr Var -> CG SpecType
--------------------------------------------------------------------------------

-- NV this is a hack to type polymorphic axiomatized functions
-- no need to check this code with flag, the axioms environment withh 
-- be empty if there is no axiomatization

consE γ e'@(App e@(Var x) (Type τ)) | (M.member x $ aenv γ)
  = do RAllT α te <- checkAll ("Non-all TyApp with expr", e) <$> consE γ e
       t          <- if isGeneric α te then freshTy_type TypeInstE e τ else trueTy τ
       addW        $ WfC γ t
       t'         <- refreshVV t
       tt <- instantiatePreds γ e' $ subsTyVar_meet' (α, t') te
       return $ strengthenS tt (singletonReft (M.lookup x $ aenv γ) x)

{-
consE γ (Lam β (e'@(App e@(Var x) (Type τ)))) | (M.member x $ aenv γ) && isTyVar β 
  = do RAllT α te <- checkAll ("Non-all TyApp with expr", e) <$> consE γ e
       t          <- if isGeneric α te then freshTy_type TypeInstE e τ else trueTy τ
       addW        $ WfC γ t
       t'         <- refreshVV t
       tt  <- instantiatePreds γ e' $ subsTyVar_meet' (α, t') te
       return $ RAllT (rTyVar β) 
                  $ strengthenS tt (singletonReft (M.lookup x $ aenv γ) x)
-}
-- NV END HACK 

consE γ (Var x)
  = do t <- varRefType γ x
       addLocA (Just x) (getLocation γ) (varAnn γ x t)
       return t

consE _ (Lit c)
  = refreshVV $ uRType $ literalFRefType c

consE γ (App e (Type τ)) | isKind τ
  = consE γ e


consE γ e'@(App e (Type τ))
  = do RAllT α te <- checkAll ("Non-all TyApp with expr", e) <$> consE γ e
       t          <- if isGeneric α te then freshTy_type TypeInstE e τ else trueTy τ
       addW        $ WfC γ t
       t'         <- refreshVV t
       instantiatePreds γ e' $ subsTyVar_meet' (α, t') te

-- RJ: The snippet below is *too long*. Please pull stuff from the where-clause
-- out to the top-level.
consE γ e'@(App e a) | isDictionary a
  = if isJust tt
      then return $ fromJust tt
      else do ([], πs, ls, te) <- bkUniv <$> consE γ e
              te0              <- instantiatePreds γ e' $ foldr RAllP te πs
              te'              <- instantiateStrata ls te0
              (γ', te''')      <- dropExists γ te'
              te''             <- dropConstraints γ te'''
              updateLocA {- πs -}  (exprLoc e) te''
              let RFun x tx t _ = checkFun ("Non-fun App with caller ", e') te''
              pushConsBind      $ cconsE γ' a tx
              addPost γ'        $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)
  where
    grepfunname (App x (Type _)) = grepfunname x
    grepfunname (Var x)          = x
    grepfunname e                = panic Nothing $ "grepfunname on \t" ++ showPpr e
    mdict w                      = case w of
                                     Var x    -> case dlookup (denv γ) x of {Just _ -> Just x; Nothing -> Nothing}
                                     Tick _ e -> mdict e
                                     _        -> Nothing
    isDictionary _               = isJust (mdict a)
    d = fromJust (mdict a)
    dinfo = dlookup (denv γ) d
    tt = dhasinfo dinfo $ grepfunname e

consE γ e'@(App e a)
  = do ([], πs, ls, te) <- bkUniv <$> consE γ e
       te0              <- instantiatePreds γ e' $ foldr RAllP te πs
       te'              <- instantiateStrata ls te0
       (γ', te''')      <- dropExists γ te'
       te''             <- dropConstraints γ te'''
       updateLocA {- πs -}  (exprLoc e) te''
       let RFun x tx t _ = checkFun ("Non-fun App with caller ", e') te''
       pushConsBind      $ cconsE γ' a tx
       addPost γ'        $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)
       {- 
       tt <- addPost γ'        $ maybe (checkUnbound γ' e' x t a) (F.subst1 t . (x,)) (argExpr γ a)
       let rr = case (argExpr γ e, argExpr γ a) of 
                 (Just e', Just a') -> uTop $ F.Reft (F.vv_, F.PAtom F.Eq (F.EVar F.vv_) (F.EApp e' a'))
                 _                  -> mempty
       return $ tt `strengthen` rr 
       -}


consE γ (Lam α e) | isTyVar α
  = liftM (RAllT (rTyVar α)) (consE γ e)

consE γ  e@(Lam x e1)
  = do tx      <- freshTy_type LamE (Var x) τx
       γ'      <- ((γ, "consE") += (F.symbol x, tx))
       t1      <- consE γ' e1
       addIdA x $ AnnDef tx
       addW     $ WfC γ tx
       return   $ rFun (F.symbol x) tx t1
    where
      FunTy τx _ = exprType e

consE γ e@(Let _ _)
  = cconsFreshE LetE γ e

consE γ e@(Case _ _ _ _)
  = cconsFreshE CaseE γ e

consE γ (Tick tt e)
  = do t <- consE (setLocation γ (Sp.Tick tt)) e
       addLocA Nothing (tickSrcSpan tt) (AnnUse t)
       return t

consE γ (Cast e co)
  -- See Note [Type classes with a single method]
  | Just f <- isClassConCo co
  = consE γ (f e)

consE γ e@(Cast e' _)
  = castTy γ (exprType e) e'

consE _ e@(Coercion _)
   = trueTy $ exprType e

consE _ e@(Type t)
  = panic Nothing $ "consE cannot handle type " ++ showPpr (e, t)

castTy _ τ (Var x)
  = do t <- trueTy τ
       return $  t `strengthen` (uTop $ F.uexprReft $ F.expr x)

castTy g t (Tick _ e)
  = castTy g t e

castTy _ _ e
  = panic Nothing $ "castTy cannot handle expr " ++ showPpr e

isClassConCo :: Coercion -> Maybe (Expr Var -> Expr Var)
-- See Note [Type classes with a single method]
isClassConCo co
  --- | trace ("isClassConCo: " ++ showPpr (coercionKind co)) False
  --- = undefined

  | Pair t1 t2 <- coercionKind co
  , isClassPred t2
  , (tc,ts) <- splitTyConApp t2
  , [dc]    <- tyConDataCons tc
  , [tm]    <- dataConOrigArgTys dc
               -- tcMatchTy because we have to instantiate the class tyvars
  , Just _  <- tcMatchTy (mkVarSet $ tyConTyVars tc) tm t1
  = Just (\e -> mkCoreConApps dc $ map Type ts ++ [e])

  | otherwise
  = Nothing

----------------------------------------------------------------------
-- Note [Type classes with a single method]
----------------------------------------------------------------------
-- GHC 7.10 encodes type classes with a single method as newtypes and
-- `cast`s between the method and class type instead of applying the
-- class constructor. Just rewrite the core to what we're used to
-- seeing..
--
-- specifically, we want to rewrite
--
--   e `cast` ((a -> b) ~ C)
--
-- to
--
--   D:C e
--
-- but only when
--
--   D:C :: (a -> b) -> C

-- | @consElimE@ is used to *synthesize* types by **existential elimination**
--   instead of *checking* via a fresh template. That is, assuming
--      γ |- e1 ~> t1
--   we have
--      γ |- let x = e1 in e2 ~> Ex x t1 t2
--   where
--      γ, x:t1 |- e2 ~> t2
--   instead of the earlier case where we generate a fresh template `t` and check
--      γ, x:t1 |- e <~ t

-- consElimE γ xs e
--   = do t     <- consE γ e
--        xts   <- forM xs $ \x -> (x,) <$> (γ ??= x)
--        return $ rEx xts t

-- | @consFreshE@ is used to *synthesize* types with a **fresh template** when
--   the above existential elimination is not easy (e.g. at joins, recursive binders)

cconsFreshE kvkind γ e
  = do t   <- freshTy_type kvkind e $ exprType e
       addW $ WfC γ t
       cconsE γ e t
       return t

checkUnbound γ e x t a
  | x `notElem` (F.syms t) = t
  | otherwise              = panic (Just $ getLocation γ) msg
  where
    msg = unlines [ "checkUnbound: " ++ show x ++ " is elem of syms of " ++ show t
                         , "In", showPpr e, "Arg = " , show a ]


dropExists γ (REx x tx t) = liftM (, t) $ (γ, "dropExists") += (x, tx)
dropExists γ t            = return (γ, t)

dropConstraints :: CGEnv -> SpecType -> CG SpecType
dropConstraints γ (RFun x tx@(RApp c _ _ _) t r) | isClass c
  = (flip (RFun x tx)) r <$> dropConstraints γ t
dropConstraints γ (RRTy cts _ OCons t)
  = do γ' <- foldM (\γ (x, t) -> γ `addSEnv` ("splitS", x,t)) γ xts
       addC (SubC  γ' t1 t2)  "dropConstraints"
       dropConstraints γ t
  where
    (xts, t1, t2) = envToSub cts

dropConstraints _ t = return t

-------------------------------------------------------------------------------------
cconsCase :: CGEnv -> Var -> SpecType -> [AltCon] -> (AltCon, [Var], CoreExpr) -> CG ()
-------------------------------------------------------------------------------------
cconsCase γ x t acs (ac, ys, ce)
  = do cγ <- caseEnv γ x acs ac ys
       cconsE cγ ce t

--------------------------------------------------------------------------------
refreshTy :: SpecType -> CG SpecType
--------------------------------------------------------------------------------
refreshTy t = refreshVV t >>= refreshArgs

refreshVV (RAllT a t) = liftM (RAllT a) (refreshVV t)
refreshVV (RAllP p t) = liftM (RAllP p) (refreshVV t)

refreshVV (REx x t1 t2)
  = do [t1', t2'] <- mapM refreshVV [t1, t2]
       liftM (shiftVV (REx x t1' t2')) fresh

refreshVV (RFun x t1 t2 r)
  = do [t1', t2'] <- mapM refreshVV [t1, t2]
       liftM (shiftVV (RFun x t1' t2' r)) fresh

refreshVV (RAppTy t1 t2 r)
  = do [t1', t2'] <- mapM refreshVV [t1, t2]
       liftM (shiftVV (RAppTy t1' t2' r)) fresh

refreshVV (RApp c ts rs r)
  = do ts' <- mapM refreshVV ts
       rs' <- mapM refreshVVRef rs
       liftM (shiftVV (RApp c ts' rs' r)) fresh

refreshVV t
  = return t

refreshVVRef (RProp ss (RHole r))
  = return $ RProp ss (RHole r)

refreshVVRef (RProp ss t)
  = do xs    <- mapM (\_ -> fresh) (fst <$> ss)
       let su = F.mkSubst $ zip (fst <$> ss) (F.EVar <$> xs)
       liftM (RProp (zip xs (snd <$> ss)) . F.subst su) (refreshVV t)




-------------------------------------------------------------------------------------
caseEnv   :: CGEnv -> Var -> [AltCon] -> AltCon -> [Var] -> CG CGEnv
-------------------------------------------------------------------------------------
caseEnv γ x _   (DataAlt c) ys
  = do let (x' : ys')    = F.symbol <$> (x:ys)
       xt0              <- checkTyCon ("checkTycon cconsCase", x) <$> γ ??= x
       let xt            = shiftVV xt0 x'
       tdc              <- γ ??= ({- F.symbol -} dataConWorkId c) >>= refreshVV
       let (rtd, yts, _) = unfoldR tdc xt ys
       let r1            = dataConReft   c   ys'
       let r2            = dataConMsReft rtd ys'
       let xt            = (xt0 `F.meet` rtd) `strengthen` (uTop (r1 `F.meet` r2))
       let cbs           = safeZip "cconsCase" (x':ys') (xt0:yts)
       cγ'              <- addBinders γ x' cbs
       cγ               <- addBinders cγ' x' [(x', xt)]
       return cγ

caseEnv γ x acs a _
  = do let x'  = F.symbol x
       xt'    <- (`strengthen` uTop (altReft γ acs a)) <$> (γ ??= x)
       cγ     <- addBinders γ x' [(x', xt')]
       return cγ

altReft _ _ (LitAlt l)   = literalFReft l
altReft γ acs DEFAULT    = mconcat [notLiteralReft l | LitAlt l <- acs]
  where notLiteralReft   = maybe mempty F.notExprReft . snd . literalConst (emb γ)
altReft _ _ _            = panic Nothing "Constraint : altReft"

unfoldR td (RApp _ ts rs _) ys = (t3, tvys ++ yts, ignoreOblig rt)
  where
        tbody              = instantiatePvs (instantiateTys td ts) $ reverse rs
        (ys0, yts', _, rt) = safeBkArrow $ instantiateTys tbody tvs'
        yts''              = zipWith F.subst sus (yts'++[rt])
        (t3,yts)           = (last yts'', init yts'')
        sus                = F.mkSubst <$> (L.inits [(x, F.EVar y) | (x, y) <- zip ys0 ys'])
        (αs, ys')          = mapSnd (F.symbol <$>) $ L.partition isTyVar ys
        tvs'               = rVar <$> αs
        tvys               = ofType . varType <$> αs

unfoldR _  _                _  = panic Nothing "Constraint.hs : unfoldR"

instantiateTys = L.foldl' go
  where go (RAllT α tbody) t = subsTyVar_meet' (α, t) tbody
        go _ _               = panic Nothing "Constraint.instanctiateTy"

instantiatePvs = L.foldl' go
  where go (RAllP p tbody) r = replacePreds "instantiatePv" tbody [(p, r)]
        go _ _               = panic Nothing "Constraint.instanctiatePv"

checkTyCon _ t@(RApp _ _ _ _) = t
checkTyCon x t                = checkErr x t

checkFun _ t@(RFun _ _ _ _)   = t
checkFun x t                  = checkErr x t

checkAll _ t@(RAllT _ _)      = t
checkAll x t                  = checkErr x t

checkErr (msg, e) t          = panic Nothing $ msg ++ showPpr e ++ ", type: " ++ showpp t

varAnn γ x t
  | x `S.member` recs γ      = AnnLoc (getSrcSpan x)
  | otherwise                = AnnUse t

-----------------------------------------------------------------------
-- | Helpers: Creating Fresh Refinement -------------------------------
-----------------------------------------------------------------------

freshPredRef :: CGEnv -> CoreExpr -> PVar RSort -> CG SpecProp
freshPredRef γ e (PV _ (PVProp τ) _ as)
  = do t    <- freshTy_type PredInstE e (toType τ)
       args <- mapM (\_ -> fresh) as
       let targs = [(x, s) | (x, (s, y, z)) <- zip args as, (F.EVar y) == z ]
       γ' <- foldM (++=) γ [("freshPredRef", x, ofRSort τ) | (x, τ) <- targs]
       addW $ WfC γ' t
       return $ RProp targs t

freshPredRef _ _ (PV _ PVHProp _ _)
  = todo Nothing "EFFECTS:freshPredRef"

--------------------------------------------------------------------------------
-- | Helpers: Creating Refinement Types For Various Things ---------------------
--------------------------------------------------------------------------------

argExpr :: CGEnv -> CoreExpr -> Maybe F.Expr
argExpr _ (Var vy)    = Just $ F.eVar vy
argExpr γ (Lit c)     = snd  $ literalConst (emb γ) c
argExpr γ (Tick _ e)  = argExpr γ e
argExpr _ _           = Nothing


--------------------------------------------------------------------------------
(??=) :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
γ ??= x = case M.lookup x' (lcb γ) of
            Just e  -> consE (γ -= x') e
            Nothing -> refreshTy tx
          where
            x' = F.symbol x
            tx = fromMaybe tt (γ ?= x')
            tt = ofType $ varType x


--------------------------------------------------------------------------------
varRefType :: (?callStack :: CallStack) => CGEnv -> Var -> CG SpecType
--------------------------------------------------------------------------------
varRefType γ x = do
  xt <- varRefType' γ x <$> (γ ??= x)
  return xt -- F.tracepp (printf "varRefType x = [%s]" (showpp x))

varRefType' :: CGEnv -> Var -> SpecType -> SpecType
varRefType' γ x t'
  | Just tys <- trec γ, Just tr  <- M.lookup x' tys
  = tr `strengthenS` xr
  | otherwise
  = t' `strengthenS` xr
  where
    xr = singletonReft (M.lookup x $ aenv γ) x
    x' = F.symbol x

singletonReft (Just x) _ = uTop $ F.symbolReft x
singletonReft Nothing  v = uTop $ F.symbolReft $ F.symbol v

-- | RJ: `nomeet` replaces `strengthenS` for `strengthen` in the definition
--   of `varRefType`. Why does `tests/neg/strata.hs` fail EVEN if I just replace
--   the `otherwise` case? The fq file holds no answers, both are sat.
strengthenS :: (PPrint r, F.Reftable r) => RType c tv r -> r -> RType c tv r
strengthenS (RApp c ts rs r) r'  = RApp c ts rs $ topMeet r r'
strengthenS (RVar a r) r'        = RVar a       $ topMeet r r'
strengthenS (RFun b t1 t2 r) r'  = RFun b t1 t2 $ topMeet r r'
strengthenS (RAppTy t1 t2 r) r'  = RAppTy t1 t2 $ topMeet r r'
strengthenS t _                  = t

topMeet :: (PPrint r, F.Reftable r) => r -> r -> r
topMeet r r' = {- F.tracepp msg $ -} F.top r `F.meet` r'
  -- where
    -- msg = printf "topMeet r = [%s] r' = [%s]" (showpp r) (showpp r')

  -- traceM $ printf "cconsE:\n  expr = %s\n  exprType = %s\n  lqType = %s\n" (showPpr e) (showPpr (exprType e)) (showpp t)
--------------------------------------------------------------------------------
-- | Cleaner Signatures For Rec-bindings ---------------------------------------
--------------------------------------------------------------------------------

exprLoc                         :: CoreExpr -> Maybe SrcSpan

exprLoc (Tick tt _)             = Just $ tickSrcSpan tt
exprLoc (App e a) | isType a    = exprLoc e
exprLoc _                       = Nothing

isType (Type _)                 = True
isType a                        = eqType (exprType a) predType


exprRefType :: CoreExpr -> SpecType
exprRefType = exprRefType_ M.empty

exprRefType_ :: M.HashMap Var SpecType -> CoreExpr -> SpecType
exprRefType_ γ (Let b e)
  = exprRefType_ (bindRefType_ γ b) e

exprRefType_ γ (Lam α e) | isTyVar α
  = RAllT (rTyVar α) (exprRefType_ γ e)

exprRefType_ γ (Lam x e)
  = rFun (F.symbol x) (ofType $ varType x) (exprRefType_ γ e)

exprRefType_ γ (Tick _ e)
  = exprRefType_ γ e

exprRefType_ γ (Var x)
  = M.lookupDefault (ofType $ varType x) x γ

exprRefType_ _ e
  = ofType $ exprType e

bindRefType_ γ (Rec xes)
  = extendγ γ [(x, exprRefType_ γ e) | (x,e) <- xes]

bindRefType_ γ (NonRec x e)
  = extendγ γ [(x, exprRefType_ γ e)]

extendγ γ xts
  = foldr (\(x,t) m -> M.insert x t m) γ xts

isGeneric :: RTyVar -> SpecType -> Bool
isGeneric α t =  all (\(c, α') -> (α'/=α) || isOrd c || isEq c ) (classConstrs t)
  where classConstrs t = [(c, α') | (c, ts) <- tyClasses t
                                  , t'      <- ts
                                  , α'      <- freeTyVars t']
        isOrd          = (ordClassName ==) . className
        isEq           = (eqClassName ==) . className