content: {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE MagicHash #-}
  {-# LANGUAGE RecordWildCards  #-}
  {-# LANGUAGE TemplateHaskellQuotes #-}
  {-# 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'
    , makeOpaqueReflMeasures
    , getReflDCs
    , varMeasures
    , getMeasVars
    , makeClassMeasureSpec
    -- , makeHaskellBounds
    , varLocSym
    ) where
  
  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 Language.Haskell.Liquid.GHC.Misc      as GM
  import           Language.Haskell.Liquid.Types.DataDecl
  import           Language.Haskell.Liquid.Types.Errors
  import           Language.Haskell.Liquid.Types.Names
  import qualified Language.Haskell.Liquid.Types.RefType as RT
  import           Language.Haskell.Liquid.Types.RType
  import           Language.Haskell.Liquid.Types.RTypeOp
  import           Language.Haskell.Liquid.Types.Specs
  import           Language.Haskell.Liquid.Types.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           Language.Haskell.Liquid.UX.Config
  import Control.Monad (mapM)
  import qualified Data.List as L
  
  import GHC.Base (Int(I#))
  
  --------------------------------------------------------------------------------
  makeHaskellMeasures :: Config -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
                      -> [Measure (Located BareType) (Located LHName)]
  --------------------------------------------------------------------------------
  makeHaskellMeasures cfg src tycEnv lmap spec
            = Bare.measureToBare <$> ms
    where
      ms    = makeMeasureDefinition cfg tycEnv lmap cbs <$> mSyms
      cbs   = Ghc.flattenBinds (_giCbs src)
      mSyms = S.toList (Ms.hmeas spec)
  
  makeMeasureDefinition
    :: Config -> Bare.TycEnv -> LogicMap -> [(Ghc.Id, Ghc.CoreExpr)] -> Located LHName
    -> Measure LocSpecType Ghc.DataCon
  makeMeasureDefinition cfg tycEnv lmap cbs x =
    case L.find ((x ==) . makeGHCLHNameLocatedFromId . fst) 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           = reflectLHName (Ghc.nameModule $ Ghc.getName v) <$> x
                         mdef         = coreToDef' cfg tycEnv lmap vx v cexp
                         vinfo        = GM.varLocInfo (logicType allowTC) v
  
      where allowTC = typeclass cfg
  
  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.eApps (F.EVar $ lhNameToResolvedSymbol $ F.val $ measure defn) [F.expr xx]) (body defn))
  
      xx = F.vv $ Just 10000
      isErasable = if allowTC then GM.isEmbeddedDictType else Ghc.isClassPred
  
  coreToDef' :: Config -> Bare.TycEnv -> LogicMap -> Located LHName -> Ghc.Var -> Ghc.CoreExpr
             -> [Def LocSpecType Ghc.DataCon]
  coreToDef' cfg tycEnv lmap vx v defn =
    case runToLogic embs lmap dm cfg (errHMeas vx) (coreToDef vx v defn) of
      Right l -> l
      Left e  -> Ex.throw e
    where
      embs    = Bare.tcEmbs       tycEnv
      dm      = Bare.tcDataConMap tycEnv
  
  errHMeas :: Located LHName -> String -> Error
  errHMeas x str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)
  
  --------------------------------------------------------------------------------
  makeHaskellInlines :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
                     -> [(LocSymbol, LMap)]
  --------------------------------------------------------------------------------
  makeHaskellInlines cfg src embs lmap spec
           = makeMeasureInline cfg embs lmap cbs <$> inls
    where
      cbs  = Ghc.flattenBinds (_giCbs src)
      inls = S.toList        (Ms.inlines spec)
  
  makeMeasureInline
    :: Config -> F.TCEmb Ghc.TyCon -> LogicMap -> [(Ghc.Id, Ghc.CoreExpr)] -> Located LHName
    -> (LocSymbol, LMap)
  makeMeasureInline cfg embs lmap cbs x =
    case L.find ((val x ==) . makeGHCLHNameFromId . fst) cbs of
      Nothing        -> Ex.throw $ errHMeas x "Cannot inline haskell function"
      Just (v, defn) -> (vx, coreToFun' cfg 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' :: Config -> F.TCEmb Ghc.TyCon -> Maybe Bare.DataConMap -> LogicMap -> LocSymbol -> Ghc.Var -> Ghc.CoreExpr
             -> (([Ghc.Var], Either F.Expr F.Expr) -> a) -> a
  coreToFun' cfg embs dmMb lmap x v defn ok = either Ex.throw ok act
    where
      act  = runToLogic embs lmap dm cfg err xFun
      xFun = coreToFun x v defn
      err  str = ErrHMeas (GM.sourcePosSrcSpan $ loc x) (pprint $ val x) (text str)
      dm   = Mb.fromMaybe mempty dmMb
  
  
  -------------------------------------------------------------------------------
  makeHaskellDataDecls :: Config -> Ms.BareSpec -> [Ghc.TyCon]
                       -> [DataDecl]
  --------------------------------------------------------------------------------
  makeHaskellDataDecls cfg spec tcs
    | exactDCFlag cfg = Bare.dataDeclSize spec
                      . Mb.mapMaybe tyConDataDecl
                      -- . F.tracepp "makeHaskellDataDecls-3"
                      . zipMap   (hasDataDecl 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
    . 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 :: Ms.BareSpec -> Ghc.TyCon -> HasDataDecl
  hasDataDecl spec
                   = \tc -> F.notracepp (msg tc) $ M.lookupDefault defn (tyConDataName tc) decls
    where
      msg tc       = "hasDataDecl " ++ show (tyConDataName tc)
      defn         = NoDecl Nothing
      decls        = M.fromList [ (Just dn, hasDecl d)
                                  | d     <- Ms.dataDecls spec
                                  , let dn = tycName d]
  
  {-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 :: Ghc.TyCon -> Maybe DataName
  tyConDataName tc
    | vanillaTc  = Just $ DnName $ makeGHCLHNameLocated tc
    | d:_ <- dcs = Just $ DnCon $ makeGHCLHNameLocated d
    | otherwise  = Nothing
    where
      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           = [(makeGeneratedLogicLHName $ Bare.makeDataConSelector Nothing d i, RT.bareOfType t) | (i, t) <- its ]
      dx            = makeGHCLHNameLocated 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
          -- TODO: Use as origin module the module where the measure is created
        = 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' (makeGeneratedLogicLHName $ Bare.makeDataConSelector (Just dm) dc i)) (projT i) dc n i
  
      fields   = zip (reverse xts) [1..]
      n        = length xts
      checker  = makeMeasureChecker (Loc l l' (makeGeneratedLogicLHName $ 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 (map (, mempty) as) [] [xt] bareBool
    where
      (as, _, xt)          = {- traceShow ("dataConSel: " ++ show dc) $ -} bkDataCon permitTC dc n
  
  dataConSel permitTC dc n (Proj i) = mkArrow (map (, mempty) as) [] [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 :: (Reftable (RTProp RTyCon RTyVar r), PPrint r, 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 [] defaultTyConInfo) [] [] 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) => Located LHName -> 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 :: Located LHName -> 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)], [(Located LHName, RRType F.Reft)])
  ----------------------------------------------------------------------------------------------
  makeMeasureSpec' allowTC mspec0 = (ctorTys, measTys)
    where
      ctorTys             = fmap 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
    . mkMeasureSort env
    . first val
    . bareMSpec     env sigEnv myName name
    $ spec
  
  --- Returns all the reflected symbols.
  --- If Env is provided, the symbols are qualified using the environment.
  getLocReflects :: Bare.ModSpecs -> S.HashSet F.Symbol
  getLocReflects = S.unions . map names . M.elems
    where
      names modSpec = unqualified modSpec
      unqualified modSpec = S.unions
        [ S.map (lhNameToResolvedSymbol . val) (Ms.reflects modSpec)
        , S.map val $ Ms.privateReflects modSpec
        , S.fromList (lhNameToResolvedSymbol . val . snd <$> Ms.asmReflectSigs modSpec)
        , S.fromList (lhNameToResolvedSymbol . val . fst <$> Ms.asmReflectSigs modSpec)
        , S.map (lhNameToResolvedSymbol . val) (Ms.inlines modSpec)
        , S.map (lhNameToResolvedSymbol . val) (Ms.hmeas modSpec)
        ]
  
  -- Get all the symbols that are defined in the logic, based on the environment and the specs.
  getDefinedSymbolsInLogic :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs -> S.HashSet F.Symbol
  getDefinedSymbolsInLogic env measEnv specs =
    S.unions (uncurry getFromAxioms <$> specsList) -- reflections that ended up in equations
      `S.union` getLocReflects specs -- reflected symbols
      `S.union` measVars -- Get the data constructors, ex. for Lit00.0
      `S.union` S.unions (getDataDecls . snd <$> specsList) -- get the Predicated type defs, ex. for T1669.CSemigroup
      `S.union` S.unions (getAliases . snd <$> specsList) -- aliases, ex. for T1738Lib.incr
    where
      specsList = M.toList specs
      getFromAxioms _modName spec = S.fromList $
        F.eqName <$> Ms.axeqs spec
      measVars     = S.fromList $ fst <$> getMeasVars env measEnv
      getDataDecls spec = S.unions $
        getFromDataCtor <$>
          concat (tycDCons `Mb.mapMaybe` (dataDecls spec ++ newtyDecls spec))
      getFromDataCtor decl = S.fromList $
        map lhNameToResolvedSymbol $ val (dcName decl) : (fst <$> dcFields decl)
      getAliases spec = S.fromList $ lhNameToUnqualifiedSymbol . val . rtName <$> Ms.ealiases spec
  
  -- Get the set of `DataCon`s (DCs) needed for the reflection of a given list of variables,
  -- and which are not already present in the logic
  getReflDCs :: Bare.MeasEnv -> [Ghc.Var] -> S.HashSet Ghc.DataCon
  getReflDCs measEnv vars = dcsUndefinedInLogic
    where
      -- List of wired DCs that cannot be found in the measure environment as they are
      -- eliminated in the translation from core.
      -- Written as a list of symbols because that's easier than trying to get the corresponding DCs from GHC.
      wired = S.fromList $ F.symbol <$> [show 'True, show 'False, show 'I#]
      notWired dc = not $ GM.qualifiedNameSymbol (Ghc.getName dc) `S.member` wired
      -- Undefined ones are those that are not already defined in the measure environement and are not wired
      dcsUndefinedInLogic = S.filter notWired $ allDCInUnfoldings `S.difference` definedDCs
      -- Get the defined DataCons from the measure environement
      definedDCs = S.fromList $ (GM.idDataConM . fst) `Mb.mapMaybe` Bare.meDataCons measEnv
      allDCInUnfoldings = getDCsOfUnfoldingOfVars vars
  
  ----------------------------------------------------
  -- Looks at the given list of equations and finds any undefined symbol in the logic,
  -- for which we need to introduce an opaque reflection.
  -- Returns the corresponding measures. Second part of the returned tuple is the information to save
  -- to the `meOpaqueRefl` field of the measure environment.
  makeOpaqueReflMeasures :: Bare.Env -> Bare.MeasEnv -> Bare.ModSpecs ->
                [(Ghc.Var, LocSpecType, F.Equation)] ->
                ([MSpec SpecType Ghc.DataCon], [(Ghc.Var, Measure LocBareType ctor)])
  makeOpaqueReflMeasures env measEnv specs eqs =
    unzip $ createMeasureForVar <$> S.toList (varsUndefinedInLogic `S.union` requestedOpaqueRefl)
    where
      thisModule = Ghc.tcg_mod (Bare.reTcGblEnv env)
      -- Get the set of variables for the requested opaque reflections
      requestedOpaqueRefl = S.unions
        . map (S.map getVar . Ms.opaqueReflects . snd)
        . M.toList $ specs
      getVar sym = case Bare.lookupGhcIdLHName env sym of
        Right x -> x
        Left _ -> panic (Just $ GM.fSrcSpan sym) "function to reflect not in scope"
      definedSymbols = getDefinedSymbolsInLogic env measEnv specs
      undefinedInLogic v = not (S.member (F.symbol v) definedSymbols)
      -- Variables to consider
      varsUndefinedInLogic = S.unions $
        S.filter undefinedInLogic .
        (\(v, _, eq) -> getFreeVarsOfReflectionOfVar v eq) <$> eqs
      -- Main function: creates a (dummy) measure about a given variable
      createMeasureForVar :: Ghc.Var -> (MSpec SpecType Ghc.DataCon, (Ghc.Var, Measure LocBareType ctor))
      createMeasureForVar var =
        (Ms.mkMSpec' [smeas], (var, bmeas))
        where
          locSym = F.atLoc (loc specType) (reflectLHName thisModule $ makeGHCLHNameFromId var)
          specType = varSpecType var
          bareType = varBareType var
          bmeas = M locSym bareType [] MsReflect []
          smeas = M locSym (val specType) [] MsReflect []
  
  getUnfoldingOfVar :: Ghc.Var -> Maybe Ghc.CoreExpr
  getUnfoldingOfVar = getExpr . Ghc.realUnfoldingInfo . Ghc.idInfo
    where
      getExpr :: Ghc.Unfolding -> Maybe Ghc.CoreExpr
      getExpr (Ghc.CoreUnfolding expr _ _ _ _) = Just expr
      getExpr _ = Nothing
  
  -- Get the set of "free" symbols in the (reflection of the) unfolding of a given variable.
  -- Free symbols are those that are not already in the logic and that appear in
  -- the reflection of the unfolding.
  -- For this purpose, you need to give the variable naming the definition to reflect
  -- and its corresponding equation in the logic.
  getFreeVarsOfReflectionOfVar  :: Ghc.Var -> F.Equation -> S.HashSet Ghc.Var
  getFreeVarsOfReflectionOfVar var eq =
      S.filter (\v -> F.symbol v `S.member` freeSymbolsInReflectedBody) freeVarsInCoreExpr
    where
      reflExpr = getUnfoldingOfVar var
      getAllFreeVars = Ghc.exprSomeFreeVarsList (const True)
      freeVarsInCoreExpr = maybe S.empty (S.fromList . getAllFreeVars) reflExpr
      freeSymbolsInReflectedBody = F.exprSymbolsSet (F.eqBody eq)
  
  -- Collect all the DataCon that appear in the unfolding of a given variable.
  getDCsOfUnfoldingOfVars :: [Ghc.Var] -> S.HashSet Ghc.DataCon
  getDCsOfUnfoldingOfVars vars = S.unions $ collectDataCons <$> getUnfoldingOfVar `Mb.mapMaybe` vars
  
  -- Collect all DataCon that occur in case split alternatives of an expression
  collectDataCons :: Ghc.CoreExpr -> S.HashSet Ghc.DataCon
  collectDataCons expr = go expr S.empty
    where
      go (Ghc.Var _) acc = acc
      go (Ghc.Lit _) acc = acc
      go (Ghc.App f e) acc = go f (go e acc)
      go (Ghc.Lam _ e) acc = go e acc
      go (Ghc.Let bind e) acc = go e (goBind bind acc)
      go (Ghc.Case e _ _ alts) acc = foldr goAlt (go e acc) alts
      go (Ghc.Cast e _) acc = go e acc
      go (Ghc.Tick _ e) acc = go e acc
      go (Ghc.Type _) acc = acc
      go (Ghc.Coercion _) acc = acc
  
      -- Special auxiliary function for `Alt` which is precisely where we get the datacons
      goAlt (Ghc.Alt (Ghc.DataAlt dc) _ e) acc = S.insert dc (go e acc)
      goAlt (Ghc.Alt _ _ e) acc = go e acc
  
      goBind (Ghc.NonRec _ e) acc = go e acc
      goBind (Ghc.Rec binds) acc = foldr (go . snd) acc binds
  
  bareMSpec :: Bare.Env -> Bare.SigEnv -> ModName -> ModName -> Ms.BareSpec -> Ms.MSpec LocBareType (Located LHName)
  bareMSpec env sigEnv myName name spec = Ms.mkMSpec ms cms ims oms
    where
      cms        = F.notracepp "CMS" $ filter inScope $             Ms.cmeasures spec
      ms         = F.notracepp "UMS" $ filter inScope $ expMeas <$> Ms.measures  spec
      ims        = F.notracepp "IMS" $ filter inScope $ expMeas <$> Ms.imeasures spec
      oms        = F.notracepp "OMS" $ filter inScope $ expMeas <$> Ms.omeasures spec
      expMeas    = expandMeasure rtEnv
      rtEnv      = Bare.sigRTEnv          sigEnv
      force      = name == myName
      inScope z = F.notracepp ("inScope1: " ++ F.showpp (msName z)) (force ||  okSort z)
      okSort     = Bare.knownGhcType env . msSort
  
  mkMeasureDCon :: Bare.Env -> Ms.MSpec t (F.Located LHName) -> Bare.Lookup (Ms.MSpec t Ghc.DataCon)
  mkMeasureDCon env m = do
    let ns = measureCtors m
    dcs   <- mapM (Bare.lookupGhcDataConLHName env) 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 (F.Located LHName) -> [(LHName, Ghc.DataCon)] -> Ms.MSpec t Ghc.DataCon
  mkMeasureDCon_ m ndcs = fmap (tx . val) m
    where
      tx                = Misc.mlookup (M.fromList ndcs)
  
  measureCtors ::  Ms.MSpec t (F.Located LHName) -> [F.Located LHName]
  measureCtors = Misc.sortNub . fmap ctor . concat . M.elems . Ms.ctorMap
  
  mkMeasureSort :: Bare.Env -> Ms.MSpec BareType (F.Located LHName)
                -> Ms.MSpec SpecType (F.Located LHName)
  mkMeasureSort env (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 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 :: BareRTEnv -> BareMeasure -> BareMeasure
  expandMeasure rtEnv m = m
    { msSort = RT.generalize <$> msSort m
    , msEqns = expandMeasureDef rtEnv <$> msEqns m
    }
  
  expandMeasureDef :: BareRTEnv -> Def t (Located LHName) -> Def t (Located LHName)
  expandMeasureDef rtEnv d = d
    { body  = F.notracepp msg $ Bare.expand rtEnv l (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 <- Bare.reDataConIds env
        , GM.isDataConId v
        , isSimpleType (Ghc.varType v) ]
  
  getMeasVars :: Bare.Env -> Bare.MeasEnv -> [(F.Symbol, Located (RRType F.Reft))]
  getMeasVars env measEnv = Bare.meSyms measEnv -- ms'
                              ++ Bare.meClassSyms measEnv -- cms'
                              ++ varMeasures env
  
  varSpecType :: (Monoid r) => Ghc.Var -> Located (RRType r)
  varSpecType = fmap (RT.ofType . Ghc.varType) . GM.locNamedThing
  
  varBareType :: (Monoid r) => Ghc.Var -> Located (BRType r)
  varBareType = fmap (RT.bareOfType . Ghc.varType) . GM.locNamedThing
  
  varLocSym :: Ghc.Var -> LocSymbol
  varLocSym v = F.symbol <$> GM.locNamedThing v
  
  isSimpleType :: Ghc.Type -> Bool
  isSimpleType = isFirstOrder . RT.typeSort mempty
  
  makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t
                       -> [(Located LHName, 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 (splitForAllTyCoVars $ 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
  
  -}
  
  