{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE OverloadedStrings         #-}

-- | This module contains the functions that convert /from/ descriptions of
--   symbols, names and types (over freshly parsed /bare/ Strings),
--   /to/ representations connected to GHC 'Var's, 'Name's, and 'Type's.
--   The actual /representations/ of bare and real (refinement) types are all
--   in 'RefType' -- they are different instances of 'RType'.

module Language.Haskell.Liquid.Bare (
  -- * Creating a TargetSpec
  -- $creatingTargetSpecs
    makeTargetSpec

  -- * Loading and Saving lifted specs from/to disk
  , loadLiftedSpec
  , saveLiftedSpec
  ) where

import           Prelude                                    hiding (error)
import           Optics
import           Control.Monad                              (forM)
import           Control.Applicative                        ((<|>))
import qualified Control.Exception                          as Ex
import qualified Data.Binary                                as B
import qualified Data.Maybe                                 as Mb
import qualified Data.List                                  as L
import qualified Data.HashMap.Strict                        as M
import qualified Data.HashSet                               as S
import           Text.PrettyPrint.HughesPJ                  hiding (first, (<>)) -- (text, (<+>))
import           System.FilePath                            (dropExtension)
import           System.Directory                           (doesFileExist)
import           System.Console.CmdArgs.Verbosity           (whenLoud)
import           Language.Fixpoint.Utils.Files              as Files
import           Language.Fixpoint.Misc                     as Misc
import           Language.Fixpoint.Types                    hiding (dcFields, DataDecl, Error, panic)
import qualified Language.Fixpoint.Types                    as F
import qualified Language.Haskell.Liquid.Misc               as Misc -- (nubHashOn)
import qualified Liquid.GHC.Misc           as GM
import qualified Liquid.GHC.API            as Ghc
import           Liquid.GHC.Types          (StableName)
import           Language.Haskell.Liquid.Types
import           Language.Haskell.Liquid.WiredIn
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.DataType      as Bare
import           Language.Haskell.Liquid.Bare.Elaborate
import qualified Language.Haskell.Liquid.Bare.Expand        as Bare
import qualified Language.Haskell.Liquid.Bare.Measure       as Bare
import qualified Language.Haskell.Liquid.Bare.Plugged       as Bare
import qualified Language.Haskell.Liquid.Bare.Axiom         as Bare
import qualified Language.Haskell.Liquid.Bare.ToBare        as Bare
import qualified Language.Haskell.Liquid.Bare.Class         as Bare
import qualified Language.Haskell.Liquid.Bare.Check         as Bare
import qualified Language.Haskell.Liquid.Bare.Laws          as Bare
import qualified Language.Haskell.Liquid.Bare.Typeclass     as Bare
import qualified Language.Haskell.Liquid.Transforms.CoreToLogic as CoreToLogic
import           Control.Arrow                    (second)
import Data.Hashable (Hashable)
import qualified Language.Haskell.Liquid.Bare.Slice as Dg

--------------------------------------------------------------------------------
-- | De/Serializing Spec files
--------------------------------------------------------------------------------

loadLiftedSpec :: Config -> FilePath -> IO (Maybe Ms.BareSpec)
loadLiftedSpec cfg srcF
  | noLiftedImport cfg = putStrLn "No LIFTED Import" >> return Nothing
  | otherwise          = do
      let specF = extFileName BinSpec srcF
      ex  <- doesFileExist specF
      whenLoud $ putStrLn $ "Loading Binary Lifted Spec: " ++ specF ++ " " ++ "for source-file: " ++ show srcF ++ " " ++ show ex
      lSp <- if ex
               then Just <$> B.decodeFile specF
               else {- warnMissingLiftedSpec srcF specF >> -} return Nothing
      Ex.evaluate lSp

-- warnMissingLiftedSpec :: FilePath -> FilePath -> IO () 
-- warnMissingLiftedSpec srcF specF = do 
--   incDir <- Misc.getIncludeDir 
--   unless (Misc.isIncludeFile incDir srcF)
--     $ Ex.throw (errMissingSpec srcF specF) 

saveLiftedSpec :: FilePath -> Ms.BareSpec -> IO ()
saveLiftedSpec srcF lspec = do
  ensurePath specF
  B.encodeFile specF lspec
  -- print (errorP "DIE" "HERE" :: String) 
  where
    specF = extFileName BinSpec srcF

{- $creatingTargetSpecs

/Liquid Haskell/ operates on 'TargetSpec's, so this module provides a single function called
'makeTargetSpec' to produce a 'TargetSpec', alongside the 'LiftedSpec'. The former will be used by
functions like 'liquid' or 'liquidOne' to verify our program is correct, the latter will be serialised
to disk so that we can retrieve it later without having to re-check the relevant Haskell file.
-}

-- | 'makeTargetSpec' constructs the 'TargetSpec' and then validates it. Upon success, the 'TargetSpec'
-- and the 'LiftedSpec' are returned. We perform error checking in \"two phases\": during the first phase,
-- we check for errors and warnings in the input 'BareSpec' and the dependencies. During this phase we ideally
-- want to short-circuit in case the validation failure is found in one of the dependencies (to avoid
-- printing potentially endless failures).
-- The second phase involves creating the 'TargetSpec', and returning either the full list of diagnostics
-- (errors and warnings) in case things went wrong, or the final 'TargetSpec' and 'LiftedSpec' together
-- with a list of 'Warning's, which shouldn't abort the compilation (modulo explicit request from the user,
-- to treat warnings and errors).
makeTargetSpec :: Config
               -> LogicMap
               -> TargetSrc
               -> BareSpec
               -> TargetDependencies
               -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec cfg lmap targetSrc bareSpec dependencies = do
  let targDiagnostics     = Bare.checkTargetSrc cfg targetSrc
  let depsDiagnostics     = mapM (uncurry Bare.checkBareSpec) legacyDependencies
  let bareSpecDiagnostics = Bare.checkBareSpec (giTargetMod targetSrc) legacyBareSpec
  case targDiagnostics >> depsDiagnostics >> bareSpecDiagnostics of
   Left d | noErrors d -> secondPhase (allWarnings d)
   Left d              -> return $ Left d
   Right ()            -> secondPhase mempty
  where
    secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
    secondPhase phaseOneWarns = do

      -- we should be able to setContext regardless of whether
      -- we use the ghc api. However, ghc will complain
      -- if the filename does not match the module name
      -- when (typeclass cfg) $ do
      --   Ghc.setContext [iimport |(modName, _) <- allSpecs legacyBareSpec,
      --                   let iimport = if isTarget modName
      --                                 then Ghc.IIModule (getModName modName)
      --                                 else Ghc.IIDecl (Ghc.simpleImportDecl (getModName modName))]
      --   void $ Ghc.execStmt
      --     "let {infixr 1 ==>; True ==> False = False; _ ==> _ = True}"
      --     Ghc.execOptions
      --   void $ Ghc.execStmt
      --     "let {infixr 1 <=>; True <=> False = False; _ <=> _ = True}"
      --     Ghc.execOptions
      --   void $ Ghc.execStmt
      --     "let {infix 4 ==; (==) :: a -> a -> Bool; _ == _ = undefined}"
      --     Ghc.execOptions
      --   void $ Ghc.execStmt
      --     "let {infix 4 /=; (/=) :: a -> a -> Bool; _ /= _ = undefined}"
      --     Ghc.execOptions
      --   void $ Ghc.execStmt
      --     "let {infixl 7 /; (/) :: Num a => a -> a -> a; _ / _ = undefined}"
      --     Ghc.execOptions        
      --   void $ Ghc.execStmt
      --     "let {len :: [a] -> Int; len _ = undefined}"
      --     Ghc.execOptions        

      diagOrSpec <- makeGhcSpec cfg (review targetSrcIso targetSrc) lmap (allSpecs legacyBareSpec)
      return $ do
        (warns, ghcSpec) <- diagOrSpec
        let (targetSpec, liftedSpec) = view targetSpecGetter ghcSpec
        pure (phaseOneWarns <> warns, targetSpec, liftedSpec)

    toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, Ms.BareSpec)
    toLegacyDep (sm, ls) = (ModName SrcImport (Ghc.moduleName . Ghc.unStableModule $ sm), unsafeFromLiftedSpec ls)

    toLegacyTarget :: Ms.BareSpec -> (ModName, Ms.BareSpec)
    toLegacyTarget validatedSpec = (giTargetMod targetSrc, validatedSpec)

    legacyDependencies :: [(ModName, Ms.BareSpec)]
    legacyDependencies = map toLegacyDep . M.toList . getDependencies $ dependencies

    allSpecs :: Ms.BareSpec -> [(ModName, Ms.BareSpec)]
    allSpecs validSpec = toLegacyTarget validSpec : legacyDependencies

    legacyBareSpec :: Spec LocBareType F.LocSymbol
    legacyBareSpec = review bareSpecIso bareSpec

-------------------------------------------------------------------------------------
-- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
--   validates it using @checkGhcSpec@.
-------------------------------------------------------------------------------------
makeGhcSpec :: Config
            -> GhcSrc
            -> LogicMap
            -> [(ModName, Ms.BareSpec)]
            -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec))
-------------------------------------------------------------------------------------
makeGhcSpec cfg src lmap validatedSpecs = do
  (dg0, sp) <- makeGhcSpec0 cfg src lmap validatedSpecs
  let diagnostics = Bare.checkTargetSpec (map snd validatedSpecs)
                                         (view targetSrcIso src)
                                         (ghcSpecEnv sp)
                                         (_giCbs src)
                                         (fst . view targetSpecGetter $ sp)
  pure $ if not (noErrors dg0) then Left dg0 else
           case diagnostics of
             Left dg1
               | noErrors dg1 -> pure (allWarnings dg1, sp)
               | otherwise    -> Left dg1
             Right ()         -> pure (mempty, sp)


ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv sp = F.notracepp "RENV" $ fromListSEnv binds
  where
    emb       = gsTcEmbeds (_gsName sp)
    binds     = F.notracepp "binds" $ concat
                 [ [(x,        rSort t) | (x, Loc _ _ t)  <- gsMeas     (_gsData sp)]
                 , [(symbol v, rSort t) | (v, Loc _ _ t)  <- gsCtors    (_gsData sp)]
                 , [(symbol v, vSort v) | v               <- gsReflects (_gsRefl sp)]
                 , [(x,        vSort v) | (x, v)          <- gsFreeSyms (_gsName sp), Ghc.isConLikeId v ]
                 , [(x, RR s mempty)    | (x, s)          <- wiredSortedSyms       ]
                 , [(x, RR s mempty)    | (x, s)          <- _gsImps sp       ]
                 ]
    vSort     = rSort . classRFInfoType (typeclass $ getConfig sp) .
                (ofType :: Ghc.Type -> SpecType) . Ghc.varType
    rSort     = rTypeSortedReft    emb


-------------------------------------------------------------------------------------
-- | @makeGhcSpec0@ slurps up all the relevant information needed to generate 
--   constraints for a target module and packages them into a @GhcSpec@ 
--   See [NOTE] LIFTING-STAGES to see why we split into lSpec0, lSpec1, etc.
--   essentially, to get to the `BareRTEnv` as soon as possible, as thats what
--   lets us use aliases inside data-constructor definitions.
-------------------------------------------------------------------------------------
makeGhcSpec0 :: Config -> GhcSrc ->  LogicMap -> [(ModName, Ms.BareSpec)] ->
                Ghc.TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 cfg src lmap mspecsNoCls = do
  -- build up environments
  tycEnv <- makeTycEnv1 name env (tycEnv0, datacons) coreToLg simplifier
  let tyi      = Bare.tcTyConMap   tycEnv
  let sigEnv   = makeSigEnv  embs tyi (_gsExports src) rtEnv
  let lSpec1   = lSpec0 <> makeLiftedSpec1 cfg src tycEnv lmap mySpec1
  let mySpec   = mySpec2 <> lSpec1
  let specs    = M.insert name mySpec iSpecs2
  let myRTE    = myRTEnv       src env sigEnv rtEnv
  let (dg5, measEnv) = withDiagnostics $ makeMeasEnv      env tycEnv sigEnv       specs
  let (dg4, sig) = withDiagnostics $ makeSpecSig cfg name specs env sigEnv   tycEnv measEnv (_giCbs src)
  elaboratedSig <-
    if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods
                              >>= elaborateSig sig
               else pure sig
  let qual     = makeSpecQual cfg env tycEnv measEnv rtEnv specs
  let sData    = makeSpecData  src env sigEnv measEnv elaboratedSig specs
  let (dg1, spcVars) = withDiagnostics $ makeSpecVars cfg src mySpec env measEnv
  let (dg2, spcTerm) = withDiagnostics $ makeSpecTerm cfg     mySpec env       name
  let (dg3, refl)    = withDiagnostics $ makeSpecRefl cfg src measEnv specs env name elaboratedSig tycEnv
  let laws     = makeSpecLaws env sigEnv (gsTySigs elaboratedSig ++ gsAsmSigs elaboratedSig) measEnv specs
  let finalLiftedSpec = makeLiftedSpec name src env refl sData elaboratedSig qual myRTE lSpec1
  let diags    = mconcat [dg0, dg1, dg2, dg3, dg4, dg5]

  pure (diags, SP
    { _gsConfig = cfg
    , _gsImps   = makeImports mspecs
    , _gsSig    = addReflSigs env name rtEnv refl elaboratedSig
    , _gsRefl   = refl
    , _gsLaws   = laws
    , _gsData   = sData
    , _gsQual   = qual
    , _gsName   = makeSpecName env     tycEnv measEnv   name
    , _gsVars   = spcVars
    , _gsTerm   = spcTerm

    , _gsLSpec  = finalLiftedSpec
                { impSigs   = makeImports mspecs
                , expSigs   = [ (F.symbol v, F.sr_sort $ Bare.varSortedReft embs v) | v <- gsReflects refl ]
                , dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec
                , measures  = Ms.measures mySpec
                  -- We want to export measures in a 'LiftedSpec', especially if they are
                  -- required to check termination of some 'liftedSigs' we export. Due to the fact
                  -- that 'lSpec1' doesn't contain the measures that we compute via 'makeHaskellMeasures',
                  -- we take them from 'mySpec', which has those.
                , asmSigs = Ms.asmSigs finalLiftedSpec ++ Ms.asmSigs mySpec
                  -- Export all the assumptions (not just the ones created out of reflection) in
                  -- a 'LiftedSpec'.
                , imeasures = Ms.imeasures finalLiftedSpec ++ Ms.imeasures mySpec
                  -- Preserve user-defined 'imeasures'.
                , dvariance = Ms.dvariance finalLiftedSpec ++ Ms.dvariance mySpec
                  -- Preserve user-defined 'dvariance'.
                , rinstance = Ms.rinstance finalLiftedSpec ++ Ms.rinstance mySpec
                  -- Preserve rinstances.
                }
    })
  where
    -- typeclass elaboration

    coreToLg ce =
      case CoreToLogic.runToLogic
             embs
             lmap
             dm
             (\x -> todo Nothing ("coreToLogic not working " ++ x))
             (CoreToLogic.coreToLogic allowTC ce) of
        Left msg -> panic Nothing (F.showpp msg)
        Right e -> e
    elaborateSig si auxsig = do
      tySigs <-
        forM (gsTySigs si) $ \(x, t) ->
          if GM.isFromGHCReal x then
            pure (x, t)
          else do t' <- traverse (elaborateSpecType coreToLg simplifier) t
                  pure (x, t')
      -- things like len breaks the code
      -- asmsigs should be elaborated only if they are from the current module
      -- asmSigs <- forM (gsAsmSigs si) $ \(x, t) -> do
      --   t' <- traverse (elaborateSpecType (pure ()) coreToLg) t
      --   pure (x, fst <$> t')
      pure
        si
          { gsTySigs = F.notracepp ("asmSigs" ++ F.showpp (gsAsmSigs si)) tySigs ++ auxsig  }

    simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
    simplifier = pure -- no simplification
    allowTC  = typeclass cfg
    mySpec2  = Bare.qualifyExpand env name rtEnv l [] mySpec1    where l = F.dummyPos "expand-mySpec2"
    iSpecs2  = Bare.qualifyExpand env name rtEnv l [] iSpecs0    where l = F.dummyPos "expand-iSpecs2"
    rtEnv    = Bare.makeRTEnv env name mySpec1 iSpecs0 lmap
    mspecs   = if allowTC then M.toList $ M.insert name mySpec0 iSpecs0 else mspecsNoCls
    (mySpec0, instMethods)  = if allowTC
                              then Bare.compileClasses src env (name, mySpec0NoCls) (M.toList iSpecs0)
                              else (mySpec0NoCls, [])
    mySpec1  = mySpec0 <> lSpec0
    lSpec0   = makeLiftedSpec0 cfg src embs lmap mySpec0
    embs     = makeEmbeds          src env ((name, mySpec0) : M.toList iSpecs0)
    dm       = Bare.tcDataConMap tycEnv0
    (dg0, datacons, tycEnv0) = makeTycEnv0   cfg name env embs mySpec2 iSpecs2
    -- extract name and specs
    env      = Bare.makeEnv cfg src lmap mspecsNoCls
    (mySpec0NoCls, iSpecs0) = splitSpecs name src mspecsNoCls
    -- check barespecs 
    name     = F.notracepp ("ALL-SPECS" ++ zzz) $ _giTargetMod  src
    zzz      = F.showpp (fst <$> mspecs)

splitSpecs :: ModName -> GhcSrc -> [(ModName, Ms.BareSpec)] -> (Ms.BareSpec, Bare.ModSpecs)
splitSpecs name src specs = (mySpec, iSpecm)
  where
    iSpecm             = fmap mconcat . Misc.group $ iSpecs
    iSpecs             = Dg.sliceSpecs src mySpec iSpecs'
    mySpec             = mconcat (snd <$> mySpecs)
    (mySpecs, iSpecs') = L.partition ((name ==) . fst) specs


makeImports :: [(ModName, Ms.BareSpec)] -> [(F.Symbol, F.Sort)]
makeImports specs = concatMap (expSigs . snd) specs'
  where specs' = filter (isSrcImport . fst) specs


makeEmbeds :: GhcSrc -> Bare.Env -> [(ModName, Ms.BareSpec)] -> F.TCEmb Ghc.TyCon
makeEmbeds src env
  = Bare.addClassEmbeds (_gsCls src) (_gsFiTcs src)
  . mconcat
  . map (makeTyConEmbeds env)

makeTyConEmbeds :: Bare.Env -> (ModName, Ms.BareSpec) -> F.TCEmb Ghc.TyCon
makeTyConEmbeds env (name, spec)
  = F.tceFromList [ (tc, t) | (c,t) <- F.tceToList (Ms.embeds spec), tc <- symTc c ]
    where
      symTc = Mb.maybeToList . Bare.maybeResolveSym env name "embed-tycon"

--------------------------------------------------------------------------------
-- | [NOTE]: REFLECT-IMPORTS
--
-- 1. MAKE the full LiftedSpec, which will eventually, contain:
--      makeHaskell{Inlines, Measures, Axioms, Bounds}
-- 2. SAVE the LiftedSpec, which will be reloaded
-- 
--   This step creates the aliases and inlines etc. It must be done BEFORE
--   we compute the `SpecType` for (all, including the reflected binders),
--   as we need the inlines and aliases to properly `expand` the SpecTypes.
--------------------------------------------------------------------------------
makeLiftedSpec1 :: Config -> GhcSrc -> Bare.TycEnv -> LogicMap -> Ms.BareSpec
                -> Ms.BareSpec
makeLiftedSpec1 config src tycEnv lmap mySpec = mempty
  { Ms.measures  = Bare.makeHaskellMeasures (typeclass config) src tycEnv lmap mySpec }

--------------------------------------------------------------------------------
-- | [NOTE]: LIFTING-STAGES 
-- 
-- We split the lifting up into stage:
-- 0. Where we only lift inlines,
-- 1. Where we lift reflects, measures, and normalized tySigs
-- 
-- This is because we need the inlines to build the @BareRTEnv@ which then
-- does the alias @expand@ business, that in turn, lets us build the DataConP,
-- i.e. the refined datatypes and their associate selectors, projectors etc,
-- that are needed for subsequent stages of the lifting.
--------------------------------------------------------------------------------
makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
                -> Ms.BareSpec
makeLiftedSpec0 cfg src embs lmap mySpec = mempty
  { Ms.ealiases  = lmapEAlias . snd <$> Bare.makeHaskellInlines (typeclass cfg) src embs lmap mySpec
  , Ms.reflects  = Ms.reflects mySpec
  , Ms.dataDecls = Bare.makeHaskellDataDecls cfg name mySpec tcs
  , Ms.embeds    = Ms.embeds mySpec
  -- We do want 'embeds' to survive and to be present into the final 'LiftedSpec'. The
  -- caveat is to decide which format is more appropriate. We obviously cannot store
  -- them as a 'TCEmb TyCon' as serialising a 'TyCon' would be fairly exponsive. This
  -- needs more thinking.
  , Ms.cmeasures = Ms.cmeasures mySpec
  -- We do want 'cmeasures' to survive and to be present into the final 'LiftedSpec'. The
  -- caveat is to decide which format is more appropriate. This needs more thinking.
  }
  where
    tcs          = uniqNub (_gsTcs src ++ refTcs)
    refTcs       = reflectedTyCons cfg embs cbs  mySpec
    cbs          = _giCbs       src
    name         = _giTargetMod src

uniqNub :: (Ghc.Uniquable a) => [a] -> [a]
uniqNub xs = M.elems $ M.fromList [ (index x, x) | x <- xs ]
  where
    index  = Ghc.getKey . Ghc.getUnique

-- | 'reflectedTyCons' returns the list of `[TyCon]` that must be reflected but
--   which are defined *outside* the current module e.g. in Base or somewhere
--   that we don't have access to the code.

reflectedTyCons :: Config -> TCEmb Ghc.TyCon -> [Ghc.CoreBind] -> Ms.BareSpec -> [Ghc.TyCon]
reflectedTyCons cfg embs cbs spec
  | exactDCFlag cfg = filter (not . isEmbedded embs)
                    $ concatMap varTyCons
                    $ reflectedVars spec cbs ++ measureVars spec cbs
  | otherwise       = []

-- | We cannot reflect embedded tycons (e.g. Bool) as that gives you a sort
--   conflict: e.g. what is the type of is-True? does it take a GHC.Types.Bool
--   or its embedding, a bool?
isEmbedded :: TCEmb Ghc.TyCon -> Ghc.TyCon -> Bool
isEmbedded embs c = F.tceMember c embs

varTyCons :: Ghc.Var -> [Ghc.TyCon]
varTyCons = specTypeCons . ofType . Ghc.varType

specTypeCons           :: SpecType -> [Ghc.TyCon]
specTypeCons         = foldRType tc []
  where
    tc acc t@RApp {} = rtc_tc (rt_tycon t) : acc
    tc acc _         = acc

reflectedVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
reflectedVars spec cbs = fst <$> xDefs
  where
    xDefs              = Mb.mapMaybe (`GM.findVarDef` cbs) reflSyms
    reflSyms           = val <$> S.toList (Ms.reflects spec)

measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
measureVars spec cbs = fst <$> xDefs
  where
    xDefs              = Mb.mapMaybe (`GM.findVarDef` cbs) measureSyms
    measureSyms        = val <$> S.toList (Ms.hmeas spec)

------------------------------------------------------------------------------------------
makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
             -> Bare.Lookup GhcSpecVars
------------------------------------------------------------------------------------------
makeSpecVars cfg src mySpec env measEnv = do
  tgtVars     <-   mapM (resolveStringVar  env name)              (checks     cfg)
  igVars      <-  sMapM (Bare.lookupGhcVar env name "gs-ignores") (Ms.ignores mySpec)
  lVars       <-  sMapM (Bare.lookupGhcVar env name "gs-lvars"  ) (Ms.lvars   mySpec)
  return (SpVar tgtVars igVars lVars cMethods)
  where
    name       = _giTargetMod src
    cMethods   = snd3 <$> Bare.meMethods measEnv

sMapM :: (Monad m, Eq b, Hashable b) => (a -> m b) -> S.HashSet a -> m (S.HashSet b)
sMapM f xSet = do
 ys <- mapM f (S.toList xSet)
 return (S.fromList ys)

sForM :: (Monad m, Eq b, Hashable b) =>S.HashSet a -> (a -> m b) -> m (S.HashSet b)
sForM xs f = sMapM f xs

qualifySymbolic :: (F.Symbolic a) => ModName -> a -> F.Symbol
qualifySymbolic name s = GM.qualifySymbol (F.symbol name) (F.symbol s)

resolveStringVar :: Bare.Env -> ModName -> String -> Bare.Lookup Ghc.Var
resolveStringVar env name s = Bare.lookupGhcVar env name "resolve-string-var" lx
  where
    lx                      = dummyLoc (qualifySymbolic name s)



------------------------------------------------------------------------------------------
makeSpecQual :: Config -> Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> BareRTEnv -> Bare.ModSpecs
             -> GhcSpecQual
------------------------------------------------------------------------------------------
makeSpecQual _cfg env tycEnv measEnv _rtEnv specs = SpQual
  { gsQualifiers = filter okQual quals
  , gsRTAliases  = [] -- makeSpecRTAliases env rtEnv -- TODO-REBARE
  }
  where
    quals        = concatMap (makeQualifiers env tycEnv) (M.toList specs)
    -- mSyms        = F.tracepp "MSYMS" $ M.fromList (Bare.meSyms measEnv ++ Bare.meClassSyms measEnv)
    okQual q     = F.notracepp ("okQual: " ++ F.showpp q)
                   $ all (`S.member` mSyms) (F.syms q)
    mSyms        = F.notracepp "MSYMS" . S.fromList
                   $  (fst <$> wiredSortedSyms)
                   ++ (fst <$> Bare.meSyms measEnv)
                   ++ (fst <$> Bare.meClassSyms measEnv)

makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec ty bndr) -> [F.Qualifier]
makeQualifiers env tycEnv (modn, spec)
  = fmap        (Bare.qualifyTopDummy env        modn)
  . Mb.mapMaybe (resolveQParams       env tycEnv modn)
  $ Ms.qualifiers spec


-- | @resolveQualParams@ converts the sorts of parameters from, e.g. 
--     'Int' ===> 'GHC.Types.Int' or 
--     'Ptr' ===> 'GHC.Ptr.Ptr'  
--   It would not be required if _all_ qualifiers are scraped from 
--   function specs, but we're keeping it around for backwards compatibility.

resolveQParams :: Bare.Env -> Bare.TycEnv -> ModName -> F.Qualifier -> Maybe F.Qualifier
resolveQParams env tycEnv name q = do
     qps   <- mapM goQP (F.qParams q)
     return $ q { F.qParams = qps }
  where
    goQP qp          = do { s <- go (F.qpSort qp) ; return qp { F.qpSort = s } }
    go               :: F.Sort -> Maybe F.Sort
    go (FAbs i s)    = FAbs i <$> go s
    go (FFunc s1 s2) = FFunc  <$> go s1 <*> go s2
    go (FApp  s1 s2) = FApp   <$> go s1 <*> go s2
    go (FTC c)       = qualifyFTycon env tycEnv name c
    go s             = Just s

qualifyFTycon :: Bare.Env -> Bare.TycEnv -> ModName -> F.FTycon -> Maybe F.Sort
qualifyFTycon env tycEnv name c
  | isPrimFTC           = Just (FTC c)
  | otherwise           = tyConSort embs . F.atLoc tcs <$> ty
  where
    ty                  = Bare.maybeResolveSym env name "qualify-FTycon" tcs
    isPrimFTC           = F.val tcs `elem` F.prims
    tcs                 = F.fTyconSymbol c
    embs                = Bare.tcEmbs tycEnv

tyConSort :: F.TCEmb Ghc.TyCon -> F.Located Ghc.TyCon -> F.Sort
tyConSort embs lc = Mb.maybe s0 fst (F.tceLookup c embs)
  where
    c             = F.val lc
    s0            = tyConSortRaw lc

tyConSortRaw :: F.Located Ghc.TyCon -> F.Sort
tyConSortRaw = FTC . F.symbolFTycon . fmap F.symbol

------------------------------------------------------------------------------------------
makeSpecTerm :: Config -> Ms.BareSpec -> Bare.Env -> ModName ->
                Bare.Lookup GhcSpecTerm
------------------------------------------------------------------------------------------
makeSpecTerm cfg mySpec env name = do
  sizes  <- if structuralTerm cfg then pure mempty else makeSize env name mySpec
  lazies <- makeLazy     env name mySpec
  autos  <- makeAutoSize env name mySpec
  decr   <- makeDecrs env name mySpec
  gfail  <- makeFail env name mySpec
  return  $ SpTerm
    { gsLazy       = S.insert dictionaryVar (lazies `mappend` sizes)
    , gsFail       = gfail
    , gsStTerm     = sizes
    , gsAutosize   = autos
    , gsDecr       = decr
    , gsNonStTerm  = mempty
    }

-- formerly, makeHints
makeDecrs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Int])]
makeDecrs env name mySpec =
  forM (Ms.decr mySpec) $ \(lx, z) -> do
    v <- Bare.lookupGhcVar env name "decreasing" lx
    return (v, z)

makeRelation :: Bare.Env -> ModName -> Bare.SigEnv ->
  [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr, RelExpr)] -> Bare.Lookup [(Ghc.Var, Ghc.Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation env name sigEnv = mapM go
 where
  go (x, y, tx, ty, a, e) = do
    vx <- Bare.lookupGhcVar env name "Var" x
    vy <- Bare.lookupGhcVar env name "Var" y
    return  
        ( vx
        , vy
        , Bare.cookSpecType env sigEnv name (Bare.HsTV vx) tx
        , Bare.cookSpecType env sigEnv name (Bare.HsTV vy) ty
        , a
        , e
        )


makeLazy :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeLazy env name spec =
  sMapM (Bare.lookupGhcVar env name "Var") (Ms.lazy spec)

makeFail :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeFail env name spec =
  sForM (Ms.fails spec) $ \x -> do
    vx <- Bare.lookupGhcVar env name "Var" x
    return x { val = vx }

makeRewrite :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeRewrite env name spec =
  sForM (Ms.rewrites spec) $ \x -> do
    vx <-  Bare.lookupGhcVar env name "Var" x
    return x { val = vx }

makeRewriteWith :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var [Ghc.Var])
makeRewriteWith env name spec = M.fromList <$> makeRewriteWith' env name spec

makeRewriteWith' :: Bare.Env -> ModName -> Spec ty bndr -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' env name spec =
  forM (M.toList $ Ms.rewriteWith spec) $ \(x, xs) -> do
    xv  <- Bare.lookupGhcVar env name "Var1" x
    xvs <- mapM (Bare.lookupGhcVar env name "Var2") xs
    return (xv, xvs)

makeAutoSize :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.TyCon)
makeAutoSize env name
  = fmap S.fromList
  . mapM (Bare.lookupGhcTyCon env name "TyCon")
  . S.toList
  . Ms.autosize

makeSize :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeSize env name
  = fmap S.fromList
  . mapM (Bare.lookupGhcVar env name "Var")
  . Mb.mapMaybe getSizeFuns
  . Ms.dataDecls

getSizeFuns :: DataDecl -> Maybe LocSymbol
getSizeFuns decl
  | Just x       <- tycSFun decl
  , SymSizeFun f <- x
  = Just f
  | otherwise
  = Nothing


------------------------------------------------------------------------------------------
makeSpecLaws :: Bare.Env -> Bare.SigEnv -> [(Ghc.Var,LocSpecType)] -> Bare.MeasEnv -> Bare.ModSpecs
             -> GhcSpecLaws
------------------------------------------------------------------------------------------
makeSpecLaws env sigEnv sigs menv specs = SpLaws
  { gsLawDefs = second (map (\(_,x,y) -> (x,y))) <$> Bare.meCLaws menv
  , gsLawInst = Bare.makeInstanceLaws env sigEnv sigs specs
  }

------------------------------------------------------------------------------------------
makeSpecRefl :: Config -> GhcSrc -> Bare.MeasEnv -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
             -> Bare.Lookup GhcSpecRefl
------------------------------------------------------------------------------------------
makeSpecRefl cfg src menv specs env name sig tycEnv = do
  autoInst <- makeAutoInst env name mySpec
  rwr      <- makeRewrite env name mySpec
  rwrWith  <- makeRewriteWith env name mySpec
  wRefls   <- Bare.wiredReflects cfg env name sig
  xtes     <- Bare.makeHaskellAxioms cfg src env tycEnv name lmap sig mySpec
  let myAxioms =
        [ Bare.qualifyTop
            env
            name
            (F.loc lt)
            e {eqName = s, eqRec = S.member s (exprSymbolsSet (eqBody e))}
        | (x, lt, e) <- xtes
        , let s = symbol x
        ]
  let sigVars  = F.notracepp "SIGVARS" $ (fst3 <$> xtes)            -- reflects
                                      ++ (fst  <$> gsAsmSigs sig)   -- assumes
                                      ++ (fst  <$> gsRefSigs sig)
  return SpRefl
    { gsLogicMap   = lmap
    , gsAutoInst   = autoInst
    , gsImpAxioms  = concatMap (Ms.axeqs . snd) (M.toList specs)
    , gsMyAxioms   = F.notracepp "gsMyAxioms" myAxioms
    , gsReflects   = F.notracepp "gsReflects" (lawMethods ++ filter (isReflectVar rflSyms) sigVars ++ wRefls)
    , gsHAxioms    = F.notracepp "gsHAxioms" xtes
    , gsWiredReft  = wRefls
    , gsRewrites   = rwr
    , gsRewritesWith = rwrWith
    }
  where
    lawMethods   = F.notracepp "Law Methods" $ concatMap Ghc.classMethods (fst <$> Bare.meCLaws menv)
    mySpec       = M.lookupDefault mempty name specs
    rflSyms      = S.fromList (getReflects specs)
    lmap         = Bare.reLMap env

isReflectVar :: S.HashSet F.Symbol -> Ghc.Var -> Bool
isReflectVar reflSyms v = S.member vx reflSyms
  where
    vx                  = GM.dropModuleNames (symbol v)

getReflects :: Bare.ModSpecs -> [Symbol]
getReflects  = fmap val . S.toList . S.unions . fmap (names . snd) . M.toList
  where
    names  z = S.unions [ Ms.reflects z, Ms.inlines z, Ms.hmeas z ]

------------------------------------------------------------------------------------------
-- | @updateReflSpecSig@ uses the information about reflected functions to update the 
--   "assumed" signatures. 
------------------------------------------------------------------------------------------
addReflSigs :: Bare.Env -> ModName -> BareRTEnv -> GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
------------------------------------------------------------------------------------------
addReflSigs env name rtEnv refl sig =
  sig { gsRefSigs = F.notracepp ("gsRefSigs for " ++ F.showpp name) $ map expandReflectedSignature reflSigs
      , gsAsmSigs = F.notracepp ("gsAsmSigs for " ++ F.showpp name) (wreflSigs ++ filter notReflected (gsAsmSigs sig))
      }
  where

    -- See T1738. We need to expand and qualify any reflected signature /here/, after any
    -- relevant binder has been detected and \"promoted\". The problem stems from the fact that any input
    -- 'BareSpec' will have a 'reflects' list of binders to reflect under the form of an opaque 'Var', that
    -- qualifyExpand can't touch when we do a first pass in 'makeGhcSpec0'. However, once we reflected all
    -- the functions, we are left with a pair (Var, LocSpecType). The latter /needs/ to be qualified and
    -- expanded again, for example in case it has expression aliases derived from 'inlines'.
    expandReflectedSignature :: (Ghc.Var, LocSpecType) -> (Ghc.Var, LocSpecType)
    expandReflectedSignature = fmap (Bare.qualifyExpand env name rtEnv (F.dummyPos "expand-refSigs") [])

    (wreflSigs, reflSigs)   = L.partition ((`elem` gsWiredReft refl) . fst)
                                 [ (x, t) | (x, t, _) <- gsHAxioms refl ]
    reflected       = fst <$> (wreflSigs ++ reflSigs)
    notReflected xt = fst xt `notElem` reflected

makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec ->
                Bare.Lookup (M.HashMap Ghc.Var (Maybe Int))
makeAutoInst env name spec = M.fromList <$> kvs
  where
    kvs = forM (M.toList (Ms.autois spec)) $ \(k, val) -> do
            vk <- Bare.lookupGhcVar env name "Var" k
            return (vk, val)


----------------------------------------------------------------------------------------
makeSpecSig :: Config -> ModName -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]
            -> Bare.Lookup GhcSpecSig
----------------------------------------------------------------------------------------
makeSpecSig cfg name specs env sigEnv tycEnv measEnv cbs = do
  mySigs     <- makeTySigs  env sigEnv name mySpec
  aSigs      <- F.notracepp ("makeSpecSig aSigs " ++ F.showpp name) $ makeAsmSigs env sigEnv name specs
  let asmSigs =  Bare.tcSelVars tycEnv
              ++ aSigs
              ++ [ (x,t) | (_, x, t) <- concatMap snd (Bare.meCLaws measEnv) ]
  let tySigs  = strengthenSigs . concat $
                  [ [(v, (0, t)) | (v, t,_) <- mySigs                         ]   -- NOTE: these weights are to priortize 
                  , [(v, (1, t)) | (v, t  ) <- makeMthSigs measEnv            ]   -- user defined sigs OVER auto-generated 
                  , [(v, (2, t)) | (v, t  ) <- makeInlSigs env rtEnv allSpecs ]   -- during the strengthening, i.e. to KEEP 
                  , [(v, (3, t)) | (v, t  ) <- makeMsrSigs env rtEnv allSpecs ]   -- the binders used in USER-defined sigs 
                  ]                                                               -- as they appear in termination metrics
  newTys     <-  makeNewTypes env sigEnv allSpecs
  relation   <-  makeRelation env name sigEnv (Ms.relational mySpec)
  asmRel     <-  makeRelation env name sigEnv (Ms.asmRel mySpec)
  return SpSig
    { gsTySigs   = tySigs
    , gsAsmSigs  = asmSigs
    , gsRefSigs  = []
    , gsDicts    = dicts
    -- , gsMethods  = if noclasscheck cfg then [] else Bare.makeMethodTypes dicts (Bare.meClasses  measEnv) cbs 
    , gsMethods  = if noclasscheck cfg then [] else Bare.makeMethodTypes (typeclass cfg) dicts (Bare.meClasses  measEnv) cbs
    , gsInSigs   = mempty
    , gsNewTypes = newTys
    , gsTexprs   = [ (v, t, es) | (v, t, Just es) <- mySigs ]
    , gsRelation = relation
    , gsAsmRel   = asmRel
  }
  where
    dicts      = Bare.makeSpecDictionaries env sigEnv specs
    mySpec     = M.lookupDefault mempty name specs
    allSpecs   = M.toList specs
    rtEnv      = Bare.sigRTEnv sigEnv
    -- hmeas      = makeHMeas    env allSpecs 

strengthenSigs :: [(Ghc.Var, (Int, LocSpecType))] ->[(Ghc.Var, LocSpecType)]
strengthenSigs sigs = go <$> Misc.groupList sigs
  where
    go (v, ixs)     = (v,) $ L.foldl1' (flip meetLoc) (F.notracepp ("STRENGTHEN-SIGS: " ++ F.showpp v) (prio ixs))
    prio            = fmap snd . Misc.sortOn fst
    meetLoc         :: LocSpecType -> LocSpecType -> LocSpecType
    meetLoc t1 t2   = t1 {val = val t1 `F.meet` val t2}

makeMthSigs :: Bare.MeasEnv -> [(Ghc.Var, LocSpecType)]
makeMthSigs measEnv = [ (v, t) | (_, v, t) <- Bare.meMethods measEnv ]

makeInlSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeInlSigs env rtEnv
  = makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env)))
  . makeFromSet "hinlines" Ms.inlines env

makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeMsrSigs env rtEnv
  = makeLiftedSigs rtEnv (CoreToLogic.inlineSpecType (typeclass (getConfig env)))
  . makeFromSet "hmeas" Ms.hmeas env

makeLiftedSigs :: BareRTEnv -> (Ghc.Var -> SpecType) -> [Ghc.Var] -> [(Ghc.Var, LocSpecType)]
makeLiftedSigs rtEnv f xs
  = [(x, lt) | x <- xs
             , let lx = GM.locNamedThing x
             , let lt = expand $ lx {val = f x}
    ]
  where
    expand   = Bare.specExpandType rtEnv

makeFromSet :: String -> (Ms.BareSpec -> S.HashSet LocSymbol) -> Bare.Env -> [(ModName, Ms.BareSpec)]
            -> [Ghc.Var]
makeFromSet msg f env specs = concat [ mk n xs | (n, s) <- specs, let xs = S.toList (f s)]
  where
    mk name                 = Mb.mapMaybe (Bare.maybeResolveSym env name msg)

makeTySigs :: Bare.Env -> Bare.SigEnv -> ModName -> Ms.BareSpec
           -> Bare.Lookup [(Ghc.Var, LocSpecType, Maybe [Located F.Expr])]
makeTySigs env sigEnv name spec = do
  bareSigs   <- bareTySigs env name                spec
  expSigs    <- makeTExpr  env name bareSigs rtEnv spec
  let rawSigs = Bare.resolveLocalBinds env expSigs
  return [ (x, cook x bt, z) | (x, bt, z) <- rawSigs ]
  where
    rtEnv     = Bare.sigRTEnv sigEnv
    cook x bt = Bare.cookSpecType env sigEnv name (Bare.HsTV x) bt

bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
bareTySigs env name spec = checkDuplicateSigs <$> vts
  where
    vts = forM ( Ms.sigs spec ++ Ms.localSigs spec ) $ \ (x, t) -> do
            v <- F.notracepp "LOOKUP-GHC-VAR" $ Bare.lookupGhcVar env name "rawTySigs" x
            return (v, t)

-- checkDuplicateSigs :: [(Ghc.Var, LocSpecType)] -> [(Ghc.Var, LocSpecType)] 
checkDuplicateSigs :: (Symbolic x) => [(x, F.Located t)] -> [(x, F.Located t)]
checkDuplicateSigs xts = case Misc.uniqueByKey symXs  of
  Left (k, ls) -> uError (errDupSpecs (pprint k) (GM.sourcePosSrcSpan <$> ls))
  Right _      -> xts
  where
    symXs = [ (F.symbol x, F.loc t) | (x, t) <- xts ]


makeAsmSigs :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.ModSpecs -> Bare.Lookup [(Ghc.Var, LocSpecType)]
makeAsmSigs env sigEnv myName specs = do
  raSigs <- rawAsmSigs env myName specs
  return [ (x, t) | (name, x, bt) <- raSigs, let t = Bare.cookSpecType env sigEnv name (Bare.LqTV x) bt ]

rawAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs -> Bare.Lookup [(ModName, Ghc.Var, LocBareType)]
rawAsmSigs env myName specs = do
  aSigs <- allAsmSigs env myName specs
  return [ (m, v, t) | (v, sigs) <- aSigs, let (m, t) = myAsmSig v sigs ]

myAsmSig :: Ghc.Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig v sigs = Mb.fromMaybe errImp (Misc.firstMaybes [mbHome, mbImp])
  where
    mbHome      = takeUnique mkErr                  sigsHome
    mbImp       = takeUnique mkErr (Misc.firstGroup sigsImp) -- see [NOTE:Prioritize-Home-Spec] 
    sigsHome    = [(m, t)      | (True,  m, t) <- sigs ]
    sigsImp     = F.notracepp ("SIGS-IMP: " ++ F.showpp v)
                  [(d, (m, t)) | (False, m, t) <- sigs, let d = nameDistance vName m]
    mkErr ts    = ErrDupSpecs (Ghc.getSrcSpan v) (F.pprint v) (GM.sourcePosSrcSpan . F.loc . snd <$> ts) :: UserError
    errImp      = impossible Nothing "myAsmSig: cannot happen as sigs is non-null"
    vName       = GM.takeModuleNames (F.symbol v)

makeTExpr :: Bare.Env -> ModName -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec
          -> Bare.Lookup [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
makeTExpr env name tySigs rtEnv spec = do
  vExprs       <- M.fromList <$> makeVarTExprs env name spec
  let vSigExprs = Misc.hashMapMapWithKey (\v t -> (t, M.lookup v vExprs)) vSigs
  return [ (v, t, qual t <$> es) | (v, (t, es)) <- M.toList vSigExprs ]
  where
    qual t es   = qualifyTermExpr env name rtEnv t <$> es
    vSigs       = M.fromList tySigs

qualifyTermExpr :: Bare.Env -> ModName -> BareRTEnv -> LocBareType -> Located F.Expr
                -> Located F.Expr
qualifyTermExpr env name rtEnv t le
        = F.atLoc le (Bare.qualifyExpand env name rtEnv l bs e)
  where
    l   = F.loc le
    e   = F.val le
    bs  = ty_binds . toRTypeRep . val $ t

makeVarTExprs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
makeVarTExprs env name spec =
  forM (Ms.termexprs spec) $ \(x, es) -> do
    vx <- Bare.lookupGhcVar env name "Var" x
    return (vx, es)

----------------------------------------------------------------------------------------
-- [NOTE:Prioritize-Home-Spec] Prioritize spec for THING defined in 
-- `Foo.Bar.Baz.Quux.x` over any other specification, IF GHC's 
-- fully qualified name for THING is `Foo.Bar.Baz.Quux.x`. 
--
-- For example, see tests/names/neg/T1078.hs for example, 
-- which assumes a spec for `head` defined in both 
-- 
--   (1) Data/ByteString.spec
--   (2) Data/ByteString/Char8.spec 
-- 
-- We end up resolving the `head` in (1) to the @Var@ `Data.ByteString.Char8.head` 
-- even though there is no exact match, just to account for re-exports of "internal"
-- modules and such (see `Resolve.matchMod`). However, we should pick the closer name
-- if its available.
----------------------------------------------------------------------------------------
nameDistance :: F.Symbol -> ModName -> Int
nameDistance vName tName
  | vName == F.symbol tName = 0
  | otherwise               = 1


takeUnique :: Ex.Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique _ []  = Nothing
takeUnique _ [x] = Just x
takeUnique f xs  = Ex.throw (f xs)

allAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs ->
              Bare.Lookup [(Ghc.Var, [(Bool, ModName, LocBareType)])]
allAsmSigs env myName specs = do
  let aSigs = [ (name, must, x, t) | (name, spec) <- M.toList specs
                                   , (must, x, t) <- getAsmSigs myName name spec ]
  vSigs    <- forM aSigs $ \(name, must, x, t) -> do
                vMb <- resolveAsmVar env name must x
                return (vMb, (must, name, t))
  return    $ Misc.groupList [ (v, z) | (Just v, z) <- vSigs ]

resolveAsmVar :: Bare.Env -> ModName -> Bool -> LocSymbol -> Bare.Lookup (Maybe Ghc.Var)
resolveAsmVar env name True  lx = Just  <$> Bare.lookupGhcVar env name "resolveAsmVar-True"  lx
resolveAsmVar env name False lx = return $  Bare.maybeResolveSym     env name "resolveAsmVar-False" lx  <|> GM.maybeAuxVar (F.val lx)


getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, LocSymbol, LocBareType)]
getAsmSigs myName name spec
  | myName == name = [ (True,  x,  t) | (x, t) <- Ms.asmSigs spec ] -- MUST    resolve, or error
  | otherwise      = [ (False, x', t) | (x, t) <- Ms.asmSigs spec
                                                  ++ Ms.sigs spec
                                      , let x' = qSym x           ]  -- MAY-NOT resolve
  where
    qSym           = fmap (GM.qualifySymbol ns)
    ns             = F.symbol name

-- TODO-REBARE: grepClassAssumes
_grepClassAssumes :: [RInstance t] -> [(Located F.Symbol, t)]
_grepClassAssumes  = concatMap go
  where
    go    xts              = Mb.mapMaybe goOne (risigs xts)
    goOne (x, RIAssumed t) = Just (fmap (F.symbol . (".$c" ++ ) . F.symbolString) x, t)
    goOne (_, RISig _)     = Nothing

makeSigEnv :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> S.HashSet StableName -> BareRTEnv -> Bare.SigEnv
makeSigEnv embs tyi exports rtEnv = Bare.SigEnv
  { sigEmbs     = embs
  , sigTyRTyMap = tyi
  , sigExports  = exports
  , sigRTEnv    = rtEnv
  }

makeNewTypes :: Bare.Env -> Bare.SigEnv -> [(ModName, Ms.BareSpec)] ->
                Bare.Lookup [(Ghc.TyCon, LocSpecType)]
makeNewTypes env sigEnv specs = do
  fmap concat $
    forM nameDecls $ uncurry (makeNewType env sigEnv)
  where
    nameDecls = [(name, d) | (name, spec) <- specs, d <- Ms.newtyDecls spec]

makeNewType :: Bare.Env -> Bare.SigEnv -> ModName -> DataDecl ->
               Bare.Lookup [(Ghc.TyCon, LocSpecType)]
makeNewType env sigEnv name d = do
  tcMb <- Bare.lookupGhcDnTyCon env name "makeNewType" tcName
  case tcMb of
    Just tc -> return [(tc, lst)]
    _       -> return []
  where
    tcName                    = tycName d
    lst                       = Bare.cookSpecType env sigEnv name Bare.GenTV bt
    bt                        = getTy tcName (tycSrcPos d) (Mb.fromMaybe [] (tycDCons d))
    getTy _ l [c]
      | [(_, t)] <- dcFields c = Loc l l t
    getTy n l _                = Ex.throw (mkErr n l)
    mkErr n l                  = ErrOther (GM.sourcePosSrcSpan l) ("Bad new type declaration:" <+> F.pprint n) :: UserError

------------------------------------------------------------------------------------------
makeSpecData :: GhcSrc -> Bare.Env -> Bare.SigEnv -> Bare.MeasEnv -> GhcSpecSig -> Bare.ModSpecs
             -> GhcSpecData
------------------------------------------------------------------------------------------
makeSpecData src env sigEnv measEnv sig specs = SpData
  { gsCtors      = F.notracepp "GS-CTORS"
                   [ (x, if allowTC then t else tt)
                       | (x, t) <- Bare.meDataCons measEnv
                       , let tt  = Bare.plugHoles (typeclass $ getConfig env) sigEnv name (Bare.LqTV x) t
                   ]
  , gsMeas       = [ (F.symbol x, uRType <$> t) | (x, t) <- measVars ]
  , gsMeasures   = Bare.qualifyTopDummy env name <$> (ms1 ++ ms2)
  , gsInvariants = Misc.nubHashOn (F.loc . snd) invs
  , gsIaliases   = concatMap (makeIAliases env sigEnv) (M.toList specs)
  , gsUnsorted   = usI ++ concatMap msUnSorted (concatMap measures specs)
  }
  where
    allowTC      = typeclass (getConfig env)
    measVars     = Bare.meSyms      measEnv -- ms'
                ++ Bare.meClassSyms measEnv -- cms' 
                ++ Bare.varMeasures env
    measuresSp   = Bare.meMeasureSpec measEnv
    ms1          = M.elems (Ms.measMap measuresSp)
    ms2          = Ms.imeas   measuresSp
    mySpec       = M.lookupDefault mempty name specs
    name         = _giTargetMod      src
    (minvs,usI)  = makeMeasureInvariants env name sig mySpec
    invs         = minvs ++ concatMap (makeInvariants env sigEnv) (M.toList specs)

makeIAliases :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(LocSpecType, LocSpecType)]
makeIAliases env sigEnv (name, spec)
  = [ z | Right z <- mkIA <$> Ms.ialiases spec ]
  where
    -- mkIA :: (LocBareType, LocBareType) -> Either _ (LocSpecType, LocSpecType)
    mkIA (t1, t2) = (,) <$> mkI' t1 <*> mkI' t2
    mkI'          = Bare.cookSpecTypeE env sigEnv name Bare.GenTV

makeInvariants :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(Maybe Ghc.Var, Located SpecType)]
makeInvariants env sigEnv (name, spec) =
  [ (Nothing, t)
    | (_, bt) <- Ms.invariants spec
    , Bare.knownGhcType env name bt
    , let t = Bare.cookSpecType env sigEnv name Bare.GenTV bt
  ] ++
  concat [ (Nothing,) . makeSizeInv l <$>  ts
    | (bts, l) <- Ms.dsize spec
    , all (Bare.knownGhcType env name) bts
    , let ts = Bare.cookSpecType env sigEnv name Bare.GenTV <$> bts
  ]

makeSizeInv :: F.LocSymbol -> Located SpecType -> Located SpecType
makeSizeInv s lst = lst{val = go (val lst)}
  where go (RApp c ts rs r) = RApp c ts rs (r `meet` nat)
        go (RAllT a t r)    = RAllT a (go t) r
        go t = t
        nat  = MkUReft (Reft (vv_, PAtom Le (ECon $ I 0) (EApp (EVar $ val s) (eVar vv_))))
                       mempty

makeMeasureInvariants :: Bare.Env -> ModName -> GhcSpecSig -> Ms.BareSpec
                      -> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants env name sig mySpec
  = mapSnd Mb.catMaybes $
    unzip (measureTypeToInv env name <$> [(x, (y, ty)) | x <- xs, (y, ty) <- sigs
                                         , isSymbolOfVar (val x) y ])
  where
    sigs = gsTySigs sig
    xs   = S.toList (Ms.hmeas  mySpec)

isSymbolOfVar :: Symbol -> Ghc.Var -> Bool
isSymbolOfVar x v = x == symbol' v
  where
    symbol' :: Ghc.Var -> Symbol
    symbol' = GM.dropModuleNames . symbol . Ghc.getName

measureTypeToInv :: Bare.Env -> ModName -> (LocSymbol, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv env name (x, (v, t))
  = notracepp "measureTypeToInv" ((Just v, t {val = Bare.qualifyTop env name (F.loc x) mtype}), usorted)
  where
    trep = toRTypeRep (val t)
    rts  = ty_args  trep
    args = ty_binds trep
    res  = ty_res   trep
    z    = last args
    tz   = last rts
    usorted = if isSimpleADT tz then Nothing else mapFst (:[]) <$> mkReft (dummyLoc $ F.symbol v) z tz res
    mtype
      | null rts
      = uError $ ErrHMeas (GM.sourcePosSrcSpan $ loc t) (pprint x) "Measure has no arguments!"
      | otherwise
      = mkInvariant x z tz res
    isSimpleADT (RApp _ ts _ _) = all isRVar ts
    isSimpleADT _               = False

mkInvariant :: LocSymbol -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant x z t tr = strengthen (top <$> t) (MkUReft reft' mempty)
      where
        reft' = Mb.maybe mempty Reft mreft
        mreft = mkReft x z t tr


mkReft :: LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft x z _t tr
  | Just q <- stripRTypeBase tr
  = let Reft (v, p) = toReft q
        su          = mkSubst [(v, mkEApp x [EVar v]), (z,EVar v)]
        -- p'          = pAnd $ filter (\e -> z `notElem` syms e) $ conjuncts p
    in  Just (v, subst su p)
mkReft _ _ _ _
  = Nothing


-- REBARE: formerly, makeGhcSpec3
-------------------------------------------------------------------------------------------
makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> ModName -> GhcSpecNames
-------------------------------------------------------------------------------------------
makeSpecName env tycEnv measEnv name = SpNames
  { gsFreeSyms = Bare.reSyms env
  , gsDconsP   = [ F.atLoc dc (dcpCon dc) | dc <- datacons ++ cls ]
  , gsTconsP   = Bare.qualifyTopDummy env name <$> tycons
  -- , gsLits = mempty                                              -- TODO-REBARE, redundant with gsMeas
  , gsTcEmbeds = Bare.tcEmbs     tycEnv
  , gsADTs     = Bare.tcAdts     tycEnv
  , gsTyconEnv = Bare.tcTyConMap tycEnv
  }
  where
    datacons, cls :: [DataConP]
    datacons   = Bare.tcDataCons tycEnv
    cls        = F.notracepp "meClasses" $ Bare.meClasses measEnv
    tycons     = Bare.tcTyCons   tycEnv


-- REBARE: formerly, makeGhcCHOP1
-- split into two to break circular dependency. we need dataconmap for core2logic
-------------------------------------------------------------------------------------------
makeTycEnv0 :: Config -> ModName -> Bare.Env -> TCEmb Ghc.TyCon -> Ms.BareSpec -> Bare.ModSpecs
           -> (Diagnostics,  [Located DataConP], Bare.TycEnv)
-------------------------------------------------------------------------------------------
makeTycEnv0 cfg myName env embs mySpec iSpecs = (diag0 <> diag1, datacons, Bare.TycEnv
  { tcTyCons      = tycons
  , tcDataCons    = mempty -- val <$> datacons 
  , tcSelMeasures = dcSelectors
  , tcSelVars     = mempty -- recSelectors            
  , tcTyConMap    = tyi
  , tcAdts        = adts
  , tcDataConMap  = dm
  , tcEmbs        = embs
  , tcName        = myName
  })
  where
    (tcDds, dcs)   = conTys
    (diag0, conTys) = withDiagnostics $ Bare.makeConTypes myName env specs
    specs         = (myName, mySpec) : M.toList iSpecs
    tcs           = Misc.snd3 <$> tcDds
    tyi           = Bare.qualifyTopDummy env myName (makeTyConInfo embs fiTcs tycons)
    -- tycons        = F.tracepp "TYCONS" $ Misc.replaceWith tcpCon tcs wiredTyCons
    -- datacons      =  Bare.makePluggedDataCons embs tyi (Misc.replaceWith (dcpCon . val) (F.tracepp "DATACONS" $ concat dcs) wiredDataCons)
    tycons        = tcs ++ knownWiredTyCons env myName
    datacons      = Bare.makePluggedDataCon (typeclass cfg) embs tyi <$> (concat dcs ++ knownWiredDataCons env myName)
    tds           = [(name, tcpCon tcp, dd) | (name, tcp, Just dd) <- tcDds]
    (diag1, adts) = Bare.makeDataDecls cfg embs myName tds       datacons
    dm            = Bare.dataConMap adts
    dcSelectors   = concatMap (Bare.makeMeasureSelectors cfg dm) (if reflection cfg then charDataCon:datacons else datacons)
    fiTcs         = _gsFiTcs (Bare.reSrc env)



makeTycEnv1 ::
     ModName
  -> Bare.Env
  -> (Bare.TycEnv, [Located DataConP])
  -> (Ghc.CoreExpr -> F.Expr)
  -> (Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr)
  -> Ghc.TcRn Bare.TycEnv
makeTycEnv1 myName env (tycEnv, datacons) coreToLg simplifier = do
  -- fst for selector generation, snd for dataconsig generation
  lclassdcs <- forM classdcs $ traverse (Bare.elaborateClassDcp coreToLg simplifier)
  let recSelectors = Bare.makeRecordSelectorSigs env myName (dcs ++ (fmap . fmap) snd lclassdcs)
  pure $
    tycEnv {Bare.tcSelVars = recSelectors, Bare.tcDataCons = F.val <$> ((fmap . fmap) fst lclassdcs ++ dcs )}
  where
    (classdcs, dcs) =
      L.partition
        (Ghc.isClassTyCon . Ghc.dataConTyCon . dcpCon . F.val) datacons


knownWiredDataCons :: Bare.Env -> ModName -> [Located DataConP]
knownWiredDataCons env name = filter isKnown wiredDataCons
  where
    isKnown                 = Bare.knownGhcDataCon env name . GM.namedLocSymbol . dcpCon . val

knownWiredTyCons :: Bare.Env -> ModName -> [TyConP]
knownWiredTyCons env name = filter isKnown wiredTyCons
  where
    isKnown               = Bare.knownGhcTyCon env name . GM.namedLocSymbol . tcpCon


-- REBARE: formerly, makeGhcCHOP2
-------------------------------------------------------------------------------------------
makeMeasEnv :: Bare.Env -> Bare.TycEnv -> Bare.SigEnv -> Bare.ModSpecs ->
               Bare.Lookup Bare.MeasEnv
-------------------------------------------------------------------------------------------
makeMeasEnv env tycEnv sigEnv specs = do
  laws        <- Bare.makeCLaws env sigEnv name specs
  (cls, mts)  <- Bare.makeClasses        env sigEnv name specs
  let dms      = Bare.makeDefaultMethods env mts
  measures0   <- mapM (Bare.makeMeasureSpec env sigEnv name) (M.toList specs)
  let measures = mconcat (Ms.mkMSpec' dcSelectors : measures0)
  let (cs, ms) = Bare.makeMeasureSpec'  (typeclass $ getConfig env)   measures
  let cms      = Bare.makeClassMeasureSpec measures
  let cms'     = [ (x, Loc l l' $ cSort t)  | (Loc l l' x, t) <- cms ]
  let ms'      = [ (F.val lx, F.atLoc lx t) | (lx, t) <- ms
                                            , Mb.isNothing (lookup (val lx) cms') ]
  let cs'      = [ (v, txRefs v t) | (v, t) <- Bare.meetDataConSpec (typeclass (getConfig env)) embs cs (datacons ++ cls)]
  return Bare.MeasEnv
    { meMeasureSpec = measures
    , meClassSyms   = cms'
    , meSyms        = ms'
    , meDataCons    = cs'
    , meClasses     = cls
    , meMethods     = mts ++ dms
    , meCLaws       = laws
    }
  where
    txRefs v t    = Bare.txRefSort tyi embs (t <$ GM.locNamedThing v)
    tyi           = Bare.tcTyConMap    tycEnv
    dcSelectors   = Bare.tcSelMeasures tycEnv
    datacons      = Bare.tcDataCons    tycEnv
    embs          = Bare.tcEmbs        tycEnv
    name          = Bare.tcName        tycEnv

-----------------------------------------------------------------------------------------
-- | @makeLiftedSpec@ is used to generate the BareSpec object that should be serialized 
--   so that downstream files that import this target can access the lifted definitions, 
--   e.g. for measures, reflected functions etc.
-----------------------------------------------------------------------------------------
makeLiftedSpec :: ModName -> GhcSrc -> Bare.Env
               -> GhcSpecRefl -> GhcSpecData -> GhcSpecSig -> GhcSpecQual -> BareRTEnv
               -> Ms.BareSpec -> Ms.BareSpec
-----------------------------------------------------------------------------------------
makeLiftedSpec name src _env refl sData sig qual myRTE lSpec0 = lSpec0
  { Ms.asmSigs    = F.notracepp   ("makeLiftedSpec : ASSUMED-SIGS " ++ F.showpp name ) (xbs ++ myDCs)
  , Ms.reflSigs   = F.notracepp "REFL-SIGS"         xbs
  , Ms.sigs       = F.notracepp   ("makeLiftedSpec : LIFTED-SIGS " ++ F.showpp name )  $ mkSigs (gsTySigs sig)
  , Ms.invariants = [ (varLocSym <$> x, Bare.specToBare <$> t)
                       | (x, t) <- gsInvariants sData
                       , isLocInFile srcF t
                    ]
  , Ms.axeqs      = gsMyAxioms refl
  , Ms.aliases    = F.notracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE
  , Ms.ealiases   = M.elems . exprAliases $ myRTE
  , Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual)
  }
  where
    myDCs         = [(x,t) | (x,t) <- mkSigs (gsCtors sData)
                           , F.symbol name == fst (GM.splitModuleName $ val x)]
    mkSigs xts    = [ toBare (x, t) | (x, t) <- xts
                    ,  S.member x sigVars && isExportedVar (view targetSrcIso src) x
                    ]
    toBare (x, t) = (varLocSym x, Bare.specToBare <$> t)
    xbs           = toBare <$> reflTySigs
    sigVars       = S.difference defVars reflVars
    defVars       = S.fromList (_giDefVars src)
    reflTySigs    = [(x, t) | (x,t,_) <- gsHAxioms refl, x `notElem` gsWiredReft refl]
    reflVars      = S.fromList (fst <$> reflTySigs)
    -- myAliases fld = M.elems . fld $ myRTE 
    srcF          = _giTarget src

-- | Returns 'True' if the input determines a location within the input file. Due to the fact we might have
-- Haskell sources which have \"companion\" specs defined alongside them, we also need to account for this
-- case, by stripping out the extensions and check that the LHS is a Haskell source and the RHS a spec file.
isLocInFile :: (F.Loc a) => FilePath -> a ->  Bool
isLocInFile f lx = f == lifted || isCompanion
  where
    lifted :: FilePath
    lifted = locFile lx

    isCompanion :: Bool
    isCompanion =
      (==) (dropExtension f) (dropExtension lifted)
       &&  isExtFile Hs f
       &&  isExtFile Files.Spec lifted

locFile :: (F.Loc a) => a -> FilePath
locFile = Misc.fst3 . F.sourcePosElts . F.sp_start . F.srcSpan

varLocSym :: Ghc.Var -> LocSymbol
varLocSym v = F.symbol <$> GM.locNamedThing v

-- makeSpecRTAliases :: Bare.Env -> BareRTEnv -> [Located SpecRTAlias]
-- makeSpecRTAliases _env _rtEnv = [] -- TODO-REBARE 


--------------------------------------------------------------------------------
-- | @myRTEnv@ slices out the part of RTEnv that was generated by aliases defined 
--   in the _target_ file, "cooks" the aliases (by conversion to SpecType), and 
--   then saves them back as BareType.
--------------------------------------------------------------------------------
myRTEnv :: GhcSrc -> Bare.Env -> Bare.SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv src env sigEnv rtEnv = mkRTE tAs' eAs
  where
    tAs'                     = normalizeBareAlias env sigEnv name <$> tAs
    tAs                      = myAliases typeAliases
    eAs                      = myAliases exprAliases
    myAliases fld            = filter (isLocInFile srcF) . M.elems . fld $ rtEnv
    srcF                     = _giTarget    src
    name                     = _giTargetMod src

mkRTE :: [Located (RTAlias x a)] -> [Located (RTAlias F.Symbol F.Expr)] -> RTEnv x a
mkRTE tAs eAs   = RTE
  { typeAliases = M.fromList [ (aName a, a) | a <- tAs ]
  , exprAliases = M.fromList [ (aName a, a) | a <- eAs ]
  }
  where aName   = rtName . F.val

normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> Located BareRTAlias
                   -> Located BareRTAlias
normalizeBareAlias env sigEnv name lx = fixRTA <$> lx
  where
    fixRTA  :: BareRTAlias -> BareRTAlias
    fixRTA  = mapRTAVars fixArg . fmap fixBody

    fixArg  :: Symbol -> Symbol
    fixArg  = F.symbol . GM.symbolTyVar

    fixBody :: BareType -> BareType
    fixBody = Bare.specToBare
            . F.val
            . Bare.cookSpecType env sigEnv name Bare.RawTV
            . F.atLoc lx


withDiagnostics :: (Monoid a) => Bare.Lookup a -> (Diagnostics, a)
withDiagnostics (Left es) = (mkDiagnostics [] es, mempty)
withDiagnostics (Right v) = (emptyDiagnostics, v)