{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RecordWildCards  #-}
{-# LANGUAGE TupleSections    #-}

-- | This module contains (most of) the code needed to lift Haskell entitites,
--   . code- (CoreBind), and data- (Tycon) definitions into the spec level.

module Language.Haskell.Liquid.Bare.Measure
  ( makeHaskellMeasures
  , makeHaskellInlines
  , makeHaskellDataDecls
  , makeMeasureSelectors
  , makeMeasureSpec
  , makeMeasureSpec'
  , varMeasures
  , makeClassMeasureSpec
  -- , makeHaskellBounds
  ) where

import Data.Default
import qualified Control.Exception as Ex
import Prelude hiding (mapM, error)
import Data.Bifunctor
import qualified Data.Maybe as Mb
import Text.PrettyPrint.HughesPJ (text)
-- import Text.Printf     (printf)

import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S

import           Language.Fixpoint.SortCheck (isFirstOrder)
import qualified Language.Fixpoint.Types as F
import           Language.Haskell.Liquid.Transforms.CoreToLogic
import qualified Language.Fixpoint.Misc                as Misc
import qualified Language.Haskell.Liquid.Misc          as Misc
import           Language.Haskell.Liquid.Misc             ((.||.))
import qualified Liquid.GHC.API       as Ghc
import qualified Liquid.GHC.Misc      as GM
import qualified Language.Haskell.Liquid.Types.RefType as RT
import           Language.Haskell.Liquid.Types
-- import           Language.Haskell.Liquid.Types.Bounds
import qualified Language.Haskell.Liquid.Measure       as Ms

import qualified Language.Haskell.Liquid.Bare.Types    as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve  as Bare
import qualified Language.Haskell.Liquid.Bare.Expand   as Bare
import qualified Language.Haskell.Liquid.Bare.DataType as Bare
import qualified Language.Haskell.Liquid.Bare.ToBare   as Bare
import Control.Monad (mapM)

--------------------------------------------------------------------------------
makeHaskellMeasures :: Bool -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
                    -> [Measure (Located BareType) LocSymbol]
--------------------------------------------------------------------------------
makeHaskellMeasures allowTC src tycEnv lmap spec
          = Bare.measureToBare <$> ms
  where
    ms    = makeMeasureDefinition allowTC tycEnv lmap cbs <$> mSyms
    cbs   = nonRecCoreBinds   (_giCbs src)
    mSyms = S.toList (Ms.hmeas spec)

makeMeasureDefinition :: Bool -> Bare.TycEnv -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
                      -> Measure LocSpecType Ghc.DataCon
makeMeasureDefinition allowTC tycEnv lmap cbs x =
  case GM.findVarDef (val x) cbs of
    Nothing        -> Ex.throw $ errHMeas x "Cannot extract measure from haskell function"
    Just (v, cexp) -> Ms.mkM vx vinfo mdef MsLifted (makeUnSorted allowTC (Ghc.varType v) mdef)
                     where
                       vx           = F.atLoc x (F.symbol v)
                       mdef         = coreToDef' allowTC tycEnv lmap vx v cexp
                       vinfo        = GM.varLocInfo (logicType allowTC) v

makeUnSorted :: Bool -> Ghc.Type -> [Def LocSpecType Ghc.DataCon] -> UnSortedExprs
makeUnSorted allowTC ty defs
  | isMeasureType ta
  = mempty
  | otherwise
  = map defToUnSortedExpr defs
  where
    ta = go $ Ghc.expandTypeSynonyms ty

    go (Ghc.ForAllTy _ t) = go t
    go Ghc.FunTy{ Ghc.ft_arg = p, Ghc.ft_res = t} | isErasable p = go t
    go Ghc.FunTy{ Ghc.ft_arg = t } = t
    go t                  = t -- this should never happen!

    isMeasureType (Ghc.TyConApp _ ts) = all Ghc.isTyVarTy ts
    isMeasureType _                   = False

    defToUnSortedExpr defn = (xx:(fst <$> binds defn),
                             Ms.bodyPred (F.mkEApp (measure defn) [F.expr xx]) (body defn))

    xx = F.vv $ Just 10000
    isErasable = if allowTC then GM.isEmbeddedDictType else Ghc.isClassPred

coreToDef' :: Bool -> Bare.TycEnv -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
           -> [Def LocSpecType Ghc.DataCon]
coreToDef' allowTC tycEnv lmap vx v defn =
  case runToLogic embs lmap dm (errHMeas vx) (coreToDef allowTC vx v defn) of
    Right l -> l
    Left e  -> Ex.throw e
  where
    embs    = Bare.tcEmbs       tycEnv
    dm      = Bare.tcDataConMap tycEnv

errHMeas :: LocSymbol -> String -> Error
errHMeas x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)

--------------------------------------------------------------------------------
makeHaskellInlines :: Bool -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
                   -> [(LocSymbol, LMap)]
--------------------------------------------------------------------------------
makeHaskellInlines allowTC src embs lmap spec
         = makeMeasureInline allowTC embs lmap cbs <$> inls
  where
    cbs  = nonRecCoreBinds (_giCbs src)
    inls = S.toList        (Ms.inlines spec)

makeMeasureInline :: Bool -> F.TCEmb Ghc.TyCon -> LogicMap -> [Ghc.CoreBind] -> LocSymbol
                  -> (LocSymbol, LMap)
makeMeasureInline allowTC embs lmap cbs x =
  case GM.findVarDef (val x) cbs of
    Nothing        -> Ex.throw $ errHMeas x "Cannot inline haskell function"
    Just (v, defn) -> (vx, coreToFun' allowTC embs Nothing lmap vx v defn ok)
                     where
                       vx         = F.atLoc x (F.symbol v)
                       ok (xs, e) = LMap vx (F.symbol <$> xs) (either id id e)

-- | @coreToFun'@ takes a @Maybe DataConMap@: we need a proper map when lifting 
--   measures and reflects (which have case-of, and hence, need the projection symbols),
--   but NOT when lifting inlines (which do not have case-of). 
--   For details, see [NOTE:Lifting-Stages] 

coreToFun' :: Bool -> F.TCEmb Ghc.TyCon -> Maybe Bare.DataConMap -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
           -> (([Ghc.Var], Either F.Expr F.Expr) -> a) -> a
coreToFun' allowTC embs dmMb lmap x v defn ok = either Ex.throw ok act
  where
    act  = runToLogic embs lmap dm err xFun
    xFun = coreToFun allowTC x v defn
    err  = errHMeas x
    dm   = Mb.fromMaybe mempty dmMb


nonRecCoreBinds :: [Ghc.CoreBind] -> [Ghc.CoreBind]
nonRecCoreBinds            = concatMap go
  where
    go cb@(Ghc.NonRec _ _) = [cb]
    go    (Ghc.Rec xes)    = [Ghc.NonRec x e | (x, e) <- xes]

-------------------------------------------------------------------------------
makeHaskellDataDecls :: Config -> ModName -> Ms.BareSpec -> [Ghc.TyCon]
                     -> [DataDecl]
--------------------------------------------------------------------------------
makeHaskellDataDecls cfg name spec tcs
  | exactDCFlag cfg = Bare.dataDeclSize spec
                    . Mb.mapMaybe tyConDataDecl
                    -- . F.tracepp "makeHaskellDataDecls-3"
                    . zipMap   (hasDataDecl name spec . fst)
                    -- . F.tracepp "makeHaskellDataDecls-2"
                    . liftableTyCons
                    -- . F.tracepp "makeHaskellDataDecls-1"
                    . filter isReflectableTyCon
                    $ tcs
  | otherwise       = []


isReflectableTyCon :: Ghc.TyCon -> Bool
isReflectableTyCon  = Ghc.isFamInstTyCon .||. Ghc.isVanillaAlgTyCon

liftableTyCons :: [Ghc.TyCon] -> [(Ghc.TyCon, DataName)]
liftableTyCons
  = F.notracepp "LiftableTCs 3"
  . zipMapMaybe (tyConDataName True)
  . F.notracepp "LiftableTCs 2"
  . filter   (not . Ghc.isBoxedTupleTyCon)
  . F.notracepp "LiftableTCs 1"
  -- . (`sortDiff` wiredInTyCons)
  -- . F.tracepp "LiftableTCs 0"

zipMap :: (a -> b) -> [a] -> [(a, b)]
zipMap f xs = zip xs (map f xs)

zipMapMaybe :: (a -> Maybe b) -> [a] -> [(a, b)]
zipMapMaybe f = Mb.mapMaybe (\x -> (x, ) <$> f x)

hasDataDecl :: ModName -> Ms.BareSpec -> Ghc.TyCon -> HasDataDecl
hasDataDecl modName spec
                 = \tc -> F.notracepp (msg tc) $ M.lookupDefault defn (tcName tc) decls
  where
    msg tc       = "hasDataDecl " ++ show (tcName tc)
    defn         = NoDecl Nothing
    tcName       = fmap (qualifiedDataName modName) . tyConDataName True
    dcName       =       qualifiedDataName modName  . tycName
    decls        = M.fromList [ (Just dn, hasDecl d)
                                | d     <- Ms.dataDecls spec
                                , let dn = dcName d]

qualifiedDataName :: ModName -> DataName -> DataName
qualifiedDataName modName (DnName lx) = DnName (qualifyModName modName <$> lx)
qualifiedDataName modName (DnCon  lx) = DnCon  (qualifyModName modName <$> lx)

{-tyConDataDecl :: {tc:TyCon | isAlgTyCon tc} -> Maybe DataDecl @-}
tyConDataDecl :: ((Ghc.TyCon, DataName), HasDataDecl) -> Maybe DataDecl
tyConDataDecl (_, HasDecl)
  = Nothing
tyConDataDecl ((tc, dn), NoDecl szF)
  = Just $ DataDecl
      { tycName   = dn
      , tycTyVars = F.symbol <$> GM.tyConTyVarsDef tc
      , tycPVars  = []
      , tycDCons  = Just (decls tc)
      , tycSrcPos = GM.getSourcePos tc
      , tycSFun   = szF
      , tycPropTy = Nothing
      , tycKind   = DataReflected
      }
      where decls = map dataConDecl . Ghc.tyConDataCons

tyConDataName :: Bool -> Ghc.TyCon -> Maybe DataName
tyConDataName full tc
  | vanillaTc  = Just (DnName (post . F.symbol <$> GM.locNamedThing tc))
  | d:_ <- dcs = Just (DnCon  (post . F.symbol <$> GM.locNamedThing d ))
  | otherwise  = Nothing
  where
    post       = if full then id else GM.dropModuleNamesAndUnique
    vanillaTc  = Ghc.isVanillaAlgTyCon tc
    dcs        = Misc.sortOn F.symbol (Ghc.tyConDataCons tc)

dataConDecl :: Ghc.DataCon -> DataCtor
dataConDecl d     = {- F.notracepp msg $ -} DataCtor dx (F.symbol <$> as) [] xts outT
  where
    isGadt        = not (Ghc.isVanillaDataCon d)
    -- msg           = printf "dataConDecl (gadt = %s)" (show isGadt)
    xts           = [(Bare.makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]
    dx            = F.symbol <$> GM.locNamedThing d
    its           = zip [1..] ts
    (as,_ps,ts,ty)  = Ghc.dataConSig d
    outT          = Just (RT.bareOfType ty :: BareType)
    _outT :: Maybe BareType
    _outT
      | isGadt    = Just (RT.bareOfType ty)
      | otherwise = Nothing





--------------------------------------------------------------------------------
-- | 'makeMeasureSelectors' converts the 'DataCon's and creates the measures for
--   the selectors and checkers that then enable reflection.
--------------------------------------------------------------------------------

makeMeasureSelectors :: Config -> Bare.DataConMap -> Located DataConP -> [Measure SpecType Ghc.DataCon]
makeMeasureSelectors cfg dm (Loc l l' c)
  = Misc.condNull (exactDCFlag cfg) (checker : Mb.mapMaybe go' fields) --  internal measures, needed for reflection
 ++ Misc.condNull autofields (Mb.mapMaybe go fields) --  user-visible measures.
  where
    dc         = dcpCon    c
    isGadt     = dcpIsGadt c
    xts        = dcpTyArgs c
    autofields = not isGadt
    go ((x, t), i)
      -- do not make selectors for functional fields
      | isFunTy t && not (higherOrderFlag cfg)
      = Nothing
      | otherwise
      = Just $ makeMeasureSelector (Loc l l' x) (projT i) dc n i

    go' ((_,t), i)
      -- do not make selectors for functional fields
      | isFunTy t && not (higherOrderFlag cfg)
      = Nothing
      | otherwise
      = Just $ makeMeasureSelector (Loc l l' (Bare.makeDataConSelector (Just dm) dc i)) (projT i) dc n i

    fields   = zip (reverse xts) [1..]
    n        = length xts
    checker  = makeMeasureChecker (Loc l l' (Bare.makeDataConChecker dc)) checkT dc n
    projT i  = dataConSel permitTC dc n (Proj i)
    checkT   = dataConSel permitTC dc n Check
    permitTC = typeclass cfg

dataConSel :: Bool -> Ghc.DataCon -> Int -> DataConSel -> SpecType
dataConSel permitTC dc n Check    = mkArrow (zip as (repeat mempty)) [] [] [xt] bareBool
  where
    (as, _, xt)          = {- traceShow ("dataConSel: " ++ show dc) $ -} bkDataCon permitTC dc n

dataConSel permitTC dc n (Proj i) = mkArrow (zip as (repeat mempty)) [] [] [xt] (mempty <$> ti)
  where
    ti                   = Mb.fromMaybe err $ Misc.getNth (i-1) ts
    (as, ts, xt)         = {- F.tracepp ("bkDatacon dc = " ++ F.showpp (dc, n)) $ -} bkDataCon permitTC dc n
    err                  = panic Nothing $ "DataCon " ++ show dc ++ "does not have " ++ show i ++ " fields"

-- bkDataCon :: DataCon -> Int -> ([RTVar RTyVar RSort], [SpecType], (Symbol, SpecType, RReft))
bkDataCon :: (F.Reftable (RTProp RTyCon RTyVar r), PPrint r, F.Reftable r) => Bool -> Ghc.DataCon -> Int -> ([RTVar RTyVar RSort], [RRType r], (F.Symbol, RFInfo, RRType r, r))
bkDataCon permitTC dcn nFlds  = (as, ts, (F.dummySymbol, classRFInfo permitTC, t, mempty))
  where
    ts                = RT.ofType <$> Misc.takeLast nFlds (map Ghc.irrelevantMult _ts)
    t                 = -- Misc.traceShow ("bkDataConResult" ++ GM.showPpr (dc, _t, _t0)) $
                          RT.ofType  $ Ghc.mkTyConApp tc tArgs'
    as                = makeRTVar . RT.rTyVar <$> (αs ++ αs')
    ((αs,αs',_,_,_ts,_t), _t0) = hammer dcn
    tArgs'            = take (nArgs - nVars) tArgs ++ (Ghc.mkTyVarTy <$> αs)
    nVars             = length αs
    nArgs             = length tArgs
    (tc, tArgs)       = Mb.fromMaybe err (Ghc.splitTyConApp_maybe _t)
    err               = GM.namedPanic dcn ("Cannot split result type of DataCon " ++ show dcn)
    hammer dc         = (Ghc.dataConFullSig dc, Ghc.varType . Ghc.dataConWorkId $ dc)

data DataConSel = Check | Proj Int

bareBool :: SpecType
bareBool = RApp (RTyCon Ghc.boolTyCon [] def) [] [] mempty


{- | NOTE:Use DataconWorkId

      dcWorkId :: forall a1 ... aN. (a1 ~ X1 ...) => T1 -> ... -> Tn -> T
      checkT   :: forall as. T -> Bool
      projT t  :: forall as. T -> t

-}

makeMeasureSelector :: (Show a1) => LocSymbol -> SpecType -> Ghc.DataCon -> Int -> a1 -> Measure SpecType Ghc.DataCon
makeMeasureSelector x s dc n i = M { msName = x, msSort = s, msEqns = [eqn], msKind = MsSelector, msUnSorted = mempty}
  where
    eqn                        = Def x dc Nothing args (E (F.EVar $ mkx i))
    args                       = (, Nothing) . mkx <$> [1 .. n]
    mkx j                      = F.symbol ("xx" ++ show j)

makeMeasureChecker :: LocSymbol -> SpecType -> Ghc.DataCon -> Int -> Measure SpecType Ghc.DataCon
makeMeasureChecker x s0 dc n = M { msName = x, msSort = s, msEqns = eqn : (eqns <$> filter (/= dc) dcs), msKind = MsChecker, msUnSorted = mempty }
  where
    s       = F.notracepp ("makeMeasureChecker: " ++ show x) s0
    eqn     = Def x dc Nothing ((, Nothing) . mkx <$> [1 .. n])       (P F.PTrue)
    eqns d  = Def x d  Nothing ((, Nothing) . mkx <$> [1 .. nArgs d]) (P F.PFalse)
    nArgs d = length (Ghc.dataConOrigArgTys d)
    mkx j   = F.symbol ("xx" ++ show j)
    dcs     = Ghc.tyConDataCons (Ghc.dataConTyCon dc)


----------------------------------------------------------------------------------------------
makeMeasureSpec' :: Bool -> MSpec SpecType Ghc.DataCon -> ([(Ghc.Var, SpecType)], [(LocSymbol, RRType F.Reft)])
----------------------------------------------------------------------------------------------
makeMeasureSpec' allowTC mspec0 = (ctorTys, measTys)
  where
    ctorTys             = Misc.mapSnd RT.uRType <$> ctorTys0
    (ctorTys0, measTys) = Ms.dataConTypes allowTC mspec
    mspec               = first (mapReft ur_reft) mspec0

----------------------------------------------------------------------------------------------
makeMeasureSpec :: Bare.Env -> Bare.SigEnv -> ModName -> (ModName, Ms.BareSpec) ->
                   Bare.Lookup (Ms.MSpec SpecType Ghc.DataCon)
----------------------------------------------------------------------------------------------
makeMeasureSpec env sigEnv myName (name, spec)
  = mkMeasureDCon env               name
  . mkMeasureSort env               name
  . first val
  . bareMSpec     env sigEnv myName name
  $ spec

bareMSpec :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> Ms.BareSpec -> Ms.MSpec LocBareType LocSymbol
bareMSpec env sigEnv myName name spec = Ms.mkMSpec ms cms ims
  where
    cms        = F.notracepp "CMS" $ filter inScope1 $             Ms.cmeasures spec
    ms         = F.notracepp "UMS" $ filter inScope2 $ expMeas <$> Ms.measures  spec
    ims        = F.notracepp "IMS" $ filter inScope2 $ expMeas <$> Ms.imeasures spec
    expMeas    = expandMeasure env name  rtEnv
    rtEnv      = Bare.sigRTEnv          sigEnv
    force      = name == myName
    inScope1 z = F.notracepp ("inScope1: " ++ F.showpp (msName z)) (force ||  okSort z)
    inScope2 z = F.notracepp ("inScope2: " ++ F.showpp (msName z)) (force || (okSort z && okCtors z))
    okSort     = Bare.knownGhcType env name . msSort
    okCtors    = all (Bare.knownGhcDataCon env name . ctor) . msEqns

mkMeasureDCon :: Bare.Env -> ModName -> Ms.MSpec t LocSymbol -> Bare.Lookup (Ms.MSpec t Ghc.DataCon)
mkMeasureDCon env name m = do
  let ns = measureCtors m
  dcs   <- mapM (Bare.lookupGhcDataCon env name "measure-datacon") ns
  return $ mkMeasureDCon_ m (zip (val <$> ns) dcs)

-- mkMeasureDCon env name m = mkMeasureDCon_ m [ (val n, symDC n) | n <- measureCtors m ]
--   where 
--     symDC                = Bare.lookupGhcDataCon env name "measure-datacon"

mkMeasureDCon_ :: Ms.MSpec t LocSymbol -> [(F.Symbol, Ghc.DataCon)] -> Ms.MSpec t Ghc.DataCon
mkMeasureDCon_ m ndcs = m' {Ms.ctorMap = cm'}
  where
    m'                = fmap (tx.val) m
    cm'               = Misc.hashMapMapKeys (F.symbol . tx) $ Ms.ctorMap m'
    tx                = Misc.mlookup (M.fromList ndcs)

measureCtors ::  Ms.MSpec t LocSymbol -> [LocSymbol]
measureCtors = Misc.sortNub . fmap ctor . concat . M.elems . Ms.ctorMap

mkMeasureSort :: Bare.Env -> ModName -> Ms.MSpec BareType LocSymbol
              -> Ms.MSpec SpecType LocSymbol
mkMeasureSort env name (Ms.MSpec c mm cm im) =
  Ms.MSpec (map txDef <$> c) (tx <$> mm) (tx <$> cm) (tx <$> im)
    where
      ofMeaSort :: F.SourcePos -> BareType -> SpecType
      ofMeaSort l = Bare.ofBareType env name l Nothing

      tx :: Measure BareType ctor -> Measure SpecType ctor
      tx (M n s eqs k u) = M n (ofMeaSort l s) (txDef <$> eqs) k u where l = GM.fSourcePos n

      txDef :: Def BareType ctor -> Def SpecType ctor
      txDef d = first (ofMeaSort l) d                              where l = GM.fSourcePos (measure d)



--------------------------------------------------------------------------------
-- | Expand Measures -----------------------------------------------------------
--------------------------------------------------------------------------------
-- type BareMeasure = Measure LocBareType LocSymbol

expandMeasure :: Bare.Env -> ModName -> BareRTEnv -> BareMeasure -> BareMeasure
expandMeasure env name rtEnv m = m
  { msSort = RT.generalize                   <$> msSort m
  , msEqns = expandMeasureDef env name rtEnv <$> msEqns m
  }

expandMeasureDef :: Bare.Env -> ModName -> BareRTEnv -> Def t LocSymbol -> Def t LocSymbol
expandMeasureDef env name rtEnv d = d
  { body  = F.notracepp msg $ Bare.qualifyExpand env name rtEnv l bs (body d) }
  where
    l     = loc (measure d)
    bs    = fst <$> binds d
    msg   = "QUALIFY-EXPAND-BODY" ++ F.showpp (bs, body d)

------------------------------------------------------------------------------
varMeasures :: (Monoid r) => Bare.Env -> [(F.Symbol, Located (RRType r))]
------------------------------------------------------------------------------
varMeasures env =
  [ (F.symbol v, varSpecType v)
      | v <- knownVars env
      , GM.isDataConId v
      , isSimpleType (Ghc.varType v) ]

knownVars :: Bare.Env -> [Ghc.Var]
knownVars env = [ v | (_, xThings)   <- M.toList (Bare._reTyThings env)
                    , (_,Ghc.AnId v) <- xThings
                ]

varSpecType :: (Monoid r) => Ghc.Var -> Located (RRType r)
varSpecType = fmap (RT.ofType . Ghc.varType) . GM.locNamedThing

isSimpleType :: Ghc.Type -> Bool
isSimpleType = isFirstOrder . RT.typeSort mempty

makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t
                     -> [(LocSymbol, CMeasure (RType c tv r2))]
makeClassMeasureSpec Ms.MSpec{..} = tx <$> M.elems cmeasMap
  where
    tx (M n s _ _ _) = (n, CM n (mapReft ur_reft s))


{- 
expandMeasureBody :: Bare.Env -> ModName -> BareRTEnv -> SourcePos -> Body -> Body
expandMeasureBody env name rtEnv l (P   p) = P   (Bare.expandQualify env name rtEnv l p) 
expandMeasureBody env name rtEnv l (R x p) = R x (Bare.expandQualify env name rtEnv l p) 
expandMeasureBody env name rtEnv l (E   e) = E   (Bare.expandQualify env name rtEnv l e) 


makeHaskellBounds :: F.TCEmb TyCon -> CoreProgram -> S.HashSet (Var, LocSymbol) -> BareM RBEnv  -- TODO-REBARE
makeHaskellBounds embs cbs xs = do
  lmap <- gets logicEnv
  M.fromList <$> mapM (makeHaskellBound embs lmap cbs) (S.toList xs)

makeHaskellBound :: F.TCEmb TyCon
                 -> LogicMap
                 -> [Bind Var]
                 -> (Var, Located Symbol)
                 -> BareM (LocSymbol, RBound)
makeHaskellBound embs lmap  cbs (v, x) =
  case filter ((v  `elem`) . GM.binders) cbs of
    (NonRec v def:_)   -> toBound v x <$> coreToFun' embs lmap x v def return
    (Rec [(v, def)]:_) -> toBound v x <$> coreToFun' embs lmap x v def return
    _                  -> throwError $ errHMeas x "Cannot make bound of haskell function"



toBound :: Var -> LocSymbol -> ([Var], Either F.Expr F.Expr) -> (LocSymbol, RBound)
toBound v x (vs, Left p) = (x', Bound x' fvs ps xs p)
  where
    x'         = capitalizeBound x
    (ps', xs') = L.partition (hasBoolResult . varType) vs
    (ps , xs)  = (txp <$> ps', txx <$> xs')
    txp v      = (dummyLoc $ simpleSymbolVar v, RT.ofType $ varType v)
    txx v      = (dummyLoc $ symbol v,          RT.ofType $ varType v)
    fvs        = (((`RVar` mempty) . RTV) <$> fst (splitForAllTys $ varType v)) :: [RSort]

toBound v x (vs, Right e) = toBound v x (vs, Left e)

capitalizeBound :: Located Symbol -> Located Symbol
capitalizeBound = fmap (symbol . toUpperHead . symbolString)
  where
    toUpperHead []     = []
    toUpperHead (x:xs) = toUpper x:xs

-}