{-# 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           Control.Monad                              (forM, mplus)
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 Language.Haskell.Liquid.GHC.Misc           as GM
import qualified Liquid.GHC.API            as Ghc
import           Language.Haskell.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 :: Config -> [Char] -> IO (Maybe (Spec (Located BareType) LocSymbol))
loadLiftedSpec Config
cfg [Char]
srcF
  | Config -> Bool
noLiftedImport Config
cfg = [Char] -> IO ()
putStrLn [Char]
"No LIFTED Import" IO ()
-> IO (Maybe (Spec (Located BareType) LocSymbol))
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (Spec (Located BareType) LocSymbol)
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Spec (Located BareType) LocSymbol)
forall a. Maybe a
Nothing
  | Bool
otherwise          = do
      let specF :: [Char]
specF = Ext -> [Char] -> [Char]
extFileName Ext
BinSpec [Char]
srcF
      Bool
ex  <- [Char] -> IO Bool
doesFileExist [Char]
specF
      IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Loading Binary Lifted Spec: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
specF [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"for source-file: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
srcF [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. Show a => a -> [Char]
show Bool
ex
      Maybe (Spec (Located BareType) LocSymbol)
lSp <- if Bool
ex
               then Spec (Located BareType) LocSymbol
-> Maybe (Spec (Located BareType) LocSymbol)
forall a. a -> Maybe a
Just (Spec (Located BareType) LocSymbol
 -> Maybe (Spec (Located BareType) LocSymbol))
-> IO (Spec (Located BareType) LocSymbol)
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO (Spec (Located BareType) LocSymbol)
forall a. Binary a => [Char] -> IO a
B.decodeFile [Char]
specF
               else {- warnMissingLiftedSpec srcF specF >> -} Maybe (Spec (Located BareType) LocSymbol)
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Spec (Located BareType) LocSymbol)
forall a. Maybe a
Nothing
      Maybe (Spec (Located BareType) LocSymbol)
-> IO (Maybe (Spec (Located BareType) LocSymbol))
forall a. a -> IO a
Ex.evaluate Maybe (Spec (Located BareType) LocSymbol)
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 :: [Char] -> Spec (Located BareType) LocSymbol -> IO ()
saveLiftedSpec [Char]
srcF Spec (Located BareType) LocSymbol
lspec = do
  [Char] -> IO ()
ensurePath [Char]
specF
  [Char] -> Spec (Located BareType) LocSymbol -> IO ()
forall a. Binary a => [Char] -> a -> IO ()
B.encodeFile [Char]
specF Spec (Located BareType) LocSymbol
lspec
  -- print (errorP "DIE" "HERE" :: String)
  where
    specF :: [Char]
specF = Ext -> [Char] -> [Char]
extFileName Ext
BinSpec [Char]
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 :: Config
-> LogicMap
-> TargetSrc
-> BareSpec
-> TargetDependencies
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec Config
cfg LogicMap
lmap TargetSrc
targetSrc BareSpec
bareSpec TargetDependencies
dependencies = do
  let targDiagnostics :: Either Diagnostics ()
targDiagnostics     = Config -> TargetSrc -> Either Diagnostics ()
Bare.checkTargetSrc Config
cfg TargetSrc
targetSrc
  let depsDiagnostics :: Either Diagnostics [()]
depsDiagnostics     = ((ModName, Spec (Located BareType) LocSymbol)
 -> Either Diagnostics ())
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Either Diagnostics [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((ModName
 -> Spec (Located BareType) LocSymbol -> Either Diagnostics ())
-> (ModName, Spec (Located BareType) LocSymbol)
-> Either Diagnostics ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ModName
-> Spec (Located BareType) LocSymbol -> Either Diagnostics ()
Bare.checkBareSpec) [(ModName, Spec (Located BareType) LocSymbol)]
legacyDependencies
  let bareSpecDiagnostics :: Either Diagnostics ()
bareSpecDiagnostics = ModName
-> Spec (Located BareType) LocSymbol -> Either Diagnostics ()
Bare.checkBareSpec (TargetSrc -> ModName
giTargetMod TargetSrc
targetSrc) Spec (Located BareType) LocSymbol
legacyBareSpec
  case Either Diagnostics ()
targDiagnostics Either Diagnostics ()
-> Either Diagnostics [()] -> Either Diagnostics [()]
forall a b.
Either Diagnostics a
-> Either Diagnostics b -> Either Diagnostics b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics [()]
depsDiagnostics Either Diagnostics [()]
-> Either Diagnostics () -> Either Diagnostics ()
forall a b.
Either Diagnostics a
-> Either Diagnostics b -> Either Diagnostics b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics ()
bareSpecDiagnostics of
   Left Diagnostics
d | Diagnostics -> Bool
noErrors Diagnostics
d -> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase (Diagnostics -> [Warning]
allWarnings Diagnostics
d)
   Left Diagnostics
d              -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
 -> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)))
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a b. (a -> b) -> a -> b
$ Diagnostics
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
forall a b. a -> Either a b
Left Diagnostics
d
   Right ()            -> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase [Warning]
forall a. Monoid a => a
mempty
  where
    secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
    secondPhase :: [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase [Warning]
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

      Either Diagnostics ([Warning], GhcSpec)
diagOrSpec <- Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg (TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
targetSrc) LogicMap
lmap (Spec (Located BareType) LocSymbol
-> [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs Spec (Located BareType) LocSymbol
legacyBareSpec)
      Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
 -> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)))
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a b. (a -> b) -> a -> b
$ do
        ([Warning]
warns, GhcSpec
ghcSpec) <- Either Diagnostics ([Warning], GhcSpec)
diagOrSpec
        let (TargetSpec
targetSpec, LiftedSpec
liftedSpec) = GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec GhcSpec
ghcSpec
        ([Warning], TargetSpec, LiftedSpec)
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
forall a. a -> Either Diagnostics a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
phaseOneWarns [Warning] -> [Warning] -> [Warning]
forall a. Semigroup a => a -> a -> a
<> [Warning]
warns, TargetSpec
targetSpec, LiftedSpec
liftedSpec)

    toLegacyDep :: (Ghc.StableModule, LiftedSpec) -> (ModName, Ms.BareSpec)
    toLegacyDep :: (StableModule, LiftedSpec)
-> (ModName, Spec (Located BareType) LocSymbol)
toLegacyDep (StableModule
sm, LiftedSpec
ls) = (ModType -> ModuleName -> ModName
ModName ModType
SrcImport (GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
Ghc.moduleName (GenModule Unit -> ModuleName)
-> (StableModule -> GenModule Unit) -> StableModule -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StableModule -> GenModule Unit
Ghc.unStableModule (StableModule -> ModuleName) -> StableModule -> ModuleName
forall a b. (a -> b) -> a -> b
$ StableModule
sm), LiftedSpec -> Spec (Located BareType) LocSymbol
unsafeFromLiftedSpec LiftedSpec
ls)

    toLegacyTarget :: Ms.BareSpec -> (ModName, Ms.BareSpec)
    toLegacyTarget :: Spec (Located BareType) LocSymbol
-> (ModName, Spec (Located BareType) LocSymbol)
toLegacyTarget Spec (Located BareType) LocSymbol
validatedSpec = (TargetSrc -> ModName
giTargetMod TargetSrc
targetSrc, Spec (Located BareType) LocSymbol
validatedSpec)

    legacyDependencies :: [(ModName, Ms.BareSpec)]
    legacyDependencies :: [(ModName, Spec (Located BareType) LocSymbol)]
legacyDependencies = ((StableModule, LiftedSpec)
 -> (ModName, Spec (Located BareType) LocSymbol))
-> [(StableModule, LiftedSpec)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map (StableModule, LiftedSpec)
-> (ModName, Spec (Located BareType) LocSymbol)
toLegacyDep ([(StableModule, LiftedSpec)]
 -> [(ModName, Spec (Located BareType) LocSymbol)])
-> (TargetDependencies -> [(StableModule, LiftedSpec)])
-> TargetDependencies
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)])
-> (TargetDependencies -> HashMap StableModule LiftedSpec)
-> TargetDependencies
-> [(StableModule, LiftedSpec)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies (TargetDependencies
 -> [(ModName, Spec (Located BareType) LocSymbol)])
-> TargetDependencies
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a b. (a -> b) -> a -> b
$ TargetDependencies
dependencies

    allSpecs :: Ms.BareSpec -> [(ModName, Ms.BareSpec)]
    allSpecs :: Spec (Located BareType) LocSymbol
-> [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs Spec (Located BareType) LocSymbol
validSpec = Spec (Located BareType) LocSymbol
-> (ModName, Spec (Located BareType) LocSymbol)
toLegacyTarget Spec (Located BareType) LocSymbol
validSpec (ModName, Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a. a -> [a] -> [a]
: [(ModName, Spec (Located BareType) LocSymbol)]
legacyDependencies

    legacyBareSpec :: Spec LocBareType F.LocSymbol
    legacyBareSpec :: Spec (Located BareType) LocSymbol
legacyBareSpec = BareSpec -> Spec (Located BareType) LocSymbol
fromBareSpec BareSpec
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 :: Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec (Located BareType) LocSymbol)]
validatedSpecs = do
  (Diagnostics
dg0, GhcSpec
sp) <- Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec (Located BareType) LocSymbol)]
validatedSpecs
  let diagnostics :: Either Diagnostics ()
diagnostics = [Spec (Located BareType) LocSymbol]
-> TargetSrc
-> SEnv SortedReft
-> [CoreBind]
-> TargetSpec
-> Either Diagnostics ()
Bare.checkTargetSpec (((ModName, Spec (Located BareType) LocSymbol)
 -> Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [Spec (Located BareType) LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd [(ModName, Spec (Located BareType) LocSymbol)]
validatedSpecs)
                                         (GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src)
                                         (GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp)
                                         (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
                                         ((TargetSpec, LiftedSpec) -> TargetSpec
forall a b. (a, b) -> a
fst ((TargetSpec, LiftedSpec) -> TargetSpec)
-> (GhcSpec -> (TargetSpec, LiftedSpec)) -> GhcSpec -> TargetSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpec -> (TargetSpec, LiftedSpec)
toTargetSpec (GhcSpec -> TargetSpec) -> GhcSpec -> TargetSpec
forall a b. (a -> b) -> a -> b
$ GhcSpec
sp)
  Either Diagnostics ([Warning], GhcSpec)
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Diagnostics ([Warning], GhcSpec)
 -> TcRn (Either Diagnostics ([Warning], GhcSpec)))
-> Either Diagnostics ([Warning], GhcSpec)
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
forall a b. (a -> b) -> a -> b
$ if Bool -> Bool
not (Diagnostics -> Bool
noErrors Diagnostics
dg0) then Diagnostics -> Either Diagnostics ([Warning], GhcSpec)
forall a b. a -> Either a b
Left Diagnostics
dg0 else
           case Either Diagnostics ()
diagnostics of
             Left Diagnostics
dg1
               | Diagnostics -> Bool
noErrors Diagnostics
dg1 -> ([Warning], GhcSpec) -> Either Diagnostics ([Warning], GhcSpec)
forall a. a -> Either Diagnostics a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics -> [Warning]
allWarnings Diagnostics
dg1, GhcSpec
sp)
               | Bool
otherwise    -> Diagnostics -> Either Diagnostics ([Warning], GhcSpec)
forall a b. a -> Either a b
Left Diagnostics
dg1
             Right ()         -> ([Warning], GhcSpec) -> Either Diagnostics ([Warning], GhcSpec)
forall a. a -> Either Diagnostics a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
forall a. Monoid a => a
mempty, GhcSpec
sp)


ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp = [Char] -> SEnv SortedReft -> SEnv SortedReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RENV" (SEnv SortedReft -> SEnv SortedReft)
-> SEnv SortedReft -> SEnv SortedReft
forall a b. (a -> b) -> a -> b
$ [(Symbol, SortedReft)] -> SEnv SortedReft
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [(Symbol, SortedReft)]
binds
  where
    emb :: TCEmb TyCon
emb       = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (GhcSpec -> GhcSpecNames
_gsName GhcSpec
sp)
    binds :: [(Symbol, SortedReft)]
binds     = [Char] -> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"binds" ([(Symbol, SortedReft)] -> [(Symbol, SortedReft)])
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a b. (a -> b) -> a -> b
$ [[(Symbol, SortedReft)]] -> [(Symbol, SortedReft)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                 [ [(Symbol
x,        SpecType -> SortedReft
forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort SpecType
t) | (Symbol
x, Loc SourcePos
_ SourcePos
_ SpecType
t)  <- GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas     (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
                 , [(TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v, SpecType -> SortedReft
forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort SpecType
t) | (TyVar
v, Loc SourcePos
_ SourcePos
_ SpecType
t)  <- GhcSpecData -> [(TyVar, LocSpecType)]
gsCtors    (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
                 , [(TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v, TyVar -> SortedReft
vSort TyVar
v) | TyVar
v               <- GhcSpecRefl -> [TyVar]
gsReflects (GhcSpec -> GhcSpecRefl
_gsRefl GhcSpec
sp)]
                 , [(Symbol
x,        TyVar -> SortedReft
vSort TyVar
v) | (Symbol
x, TyVar
v)          <- GhcSpecNames -> [(Symbol, TyVar)]
gsFreeSyms (GhcSpec -> GhcSpecNames
_gsName GhcSpec
sp), TyVar -> Bool
Ghc.isConLikeId TyVar
v ]
                 , [(Symbol
x, Sort -> Reft -> SortedReft
RR Sort
s Reft
forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)          <- [(Symbol, Sort)]
wiredSortedSyms       ]
                 , [(Symbol
x, Sort -> Reft -> SortedReft
RR Sort
s Reft
forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)          <- GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
sp       ]
                 ]
    vSort :: TyVar -> SortedReft
vSort     = SpecType -> SortedReft
forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort (SpecType -> SortedReft)
-> (TyVar -> SpecType) -> TyVar -> SortedReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SpecType -> SpecType
forall c tv r. Bool -> RType c tv r -> RType c tv r
classRFInfoType (Config -> Bool
typeclass (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ GhcSpec -> Config
forall t. HasConfig t => t -> Config
getConfig GhcSpec
sp) (SpecType -> SpecType) -> (TyVar -> SpecType) -> TyVar -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                (Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType :: Ghc.Type -> SpecType) (Type -> SpecType) -> (TyVar -> Type) -> TyVar -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType
    rSort :: RRType r -> SortedReft
rSort     = TCEmb TyCon -> RRType r -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft    TCEmb TyCon
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 :: Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec (Located BareType) LocSymbol)]
mspecsNoCls = do
  -- build up environments
  TycEnv
tycEnv <- ModName
-> Env
-> (TycEnv, [Located DataConP])
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> TcRn TycEnv
makeTycEnv1 ModName
name Env
env (TycEnv
tycEnv0, [Located DataConP]
datacons) CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier
  let tyi :: TyConMap
tyi      = TycEnv -> TyConMap
Bare.tcTyConMap   TycEnv
tycEnv
  let sigEnv :: SigEnv
sigEnv   = TCEmb TyCon
-> TyConMap -> HashSet StableName -> BareRTEnv -> SigEnv
makeSigEnv  TCEmb TyCon
embs TyConMap
tyi (GhcSrc -> HashSet StableName
_gsExports GhcSrc
src) BareRTEnv
rtEnv
  let lSpec1 :: Spec (Located BareType) LocSymbol
lSpec1   = Spec (Located BareType) LocSymbol
lSpec0 Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
forall a. Semigroup a => a -> a -> a
<> Config
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec1 Config
cfg GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec (Located BareType) LocSymbol
mySpec1
  let mySpec :: Spec (Located BareType) LocSymbol
mySpec   = Spec (Located BareType) LocSymbol
mySpec2 Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
forall a. Semigroup a => a -> a -> a
<> Spec (Located BareType) LocSymbol
lSpec1
  let specs :: HashMap ModName (Spec (Located BareType) LocSymbol)
specs    = ModName
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec (Located BareType) LocSymbol
mySpec HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs2
  let myRTE :: BareRTEnv
myRTE    = GhcSrc -> Env -> SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv       GhcSrc
src Env
env SigEnv
sigEnv BareRTEnv
rtEnv
  let (Diagnostics
dg5, MeasEnv
measEnv) = Lookup MeasEnv -> (Diagnostics, MeasEnv)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup MeasEnv -> (Diagnostics, MeasEnv))
-> Lookup MeasEnv -> (Diagnostics, MeasEnv)
forall a b. (a -> b) -> a -> b
$ Env
-> TycEnv
-> SigEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup MeasEnv
makeMeasEnv      Env
env TycEnv
tycEnv SigEnv
sigEnv       HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  let (Diagnostics
dg4, GhcSpecSig
sig) = Lookup GhcSpecSig -> (Diagnostics, GhcSpecSig)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup GhcSpecSig -> (Diagnostics, GhcSpecSig))
-> Lookup GhcSpecSig -> (Diagnostics, GhcSpecSig)
forall a b. (a -> b) -> a -> b
$ Config
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> Lookup GhcSpecSig
makeSpecSig Config
cfg ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs Env
env SigEnv
sigEnv   TycEnv
tycEnv MeasEnv
measEnv (GhcSrc -> [CoreBind]
_giCbs GhcSrc
src)
  GhcSpecSig
elaboratedSig <-
    if Bool
allowTC then (SpecType -> TcRn SpecType)
-> [Located DataConP]
-> [(ClsInst, [TyVar])]
-> TcRn [(TyVar, LocSpecType)]
Bare.makeClassAuxTypes ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier) [Located DataConP]
datacons [(ClsInst, [TyVar])]
instMethods
                              TcRn [(TyVar, LocSpecType)]
-> ([(TyVar, LocSpecType)]
    -> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig)
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
forall a b.
IOEnv (Env TcGblEnv TcLclEnv) a
-> (a -> IOEnv (Env TcGblEnv TcLclEnv) b)
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GhcSpecSig
-> [(TyVar, LocSpecType)]
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
elaborateSig GhcSpecSig
sig
               else GhcSpecSig -> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure GhcSpecSig
sig
  let qual :: GhcSpecQual
qual     = Config
-> Env
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecQual
makeSpecQual Config
cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
rtEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  let sData :: GhcSpecData
sData    = GhcSrc
-> Env
-> SigEnv
-> MeasEnv
-> GhcSpecSig
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecData
makeSpecData  GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
elaboratedSig HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  let (Diagnostics
dg1, GhcSpecVars
spcVars) = Lookup GhcSpecVars -> (Diagnostics, GhcSpecVars)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup GhcSpecVars -> (Diagnostics, GhcSpecVars))
-> Lookup GhcSpecVars -> (Diagnostics, GhcSpecVars)
forall a b. (a -> b) -> a -> b
$ Config
-> GhcSrc
-> Spec (Located BareType) LocSymbol
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec (Located BareType) LocSymbol
mySpec Env
env MeasEnv
measEnv
  let (Diagnostics
dg2, GhcSpecTerm
spcTerm) = Lookup GhcSpecTerm -> (Diagnostics, GhcSpecTerm)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup GhcSpecTerm -> (Diagnostics, GhcSpecTerm))
-> Lookup GhcSpecTerm -> (Diagnostics, GhcSpecTerm)
forall a b. (a -> b) -> a -> b
$ Config
-> Spec (Located BareType) LocSymbol
-> Env
-> ModName
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg     Spec (Located BareType) LocSymbol
mySpec Env
env       ModName
name
  let (Diagnostics
dg3, GhcSpecRefl
refl)    = Lookup GhcSpecRefl -> (Diagnostics, GhcSpecRefl)
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup GhcSpecRefl -> (Diagnostics, GhcSpecRefl))
-> Lookup GhcSpecRefl -> (Diagnostics, GhcSpecRefl)
forall a b. (a -> b) -> a -> b
$ Config
-> GhcSrc
-> MeasEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl Config
cfg GhcSrc
src MeasEnv
measEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs Env
env ModName
name GhcSpecSig
elaboratedSig TycEnv
tycEnv
  let laws :: GhcSpecLaws
laws     = Env
-> SigEnv
-> [(TyVar, LocSpecType)]
-> MeasEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
elaboratedSig [(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
elaboratedSig) MeasEnv
measEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  let finalLiftedSpec :: Spec (Located BareType) LocSymbol
finalLiftedSpec = ModName
-> GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec ModName
name GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
elaboratedSig GhcSpecQual
qual BareRTEnv
myRTE Spec (Located BareType) LocSymbol
lSpec1
  let diags :: Diagnostics
diags    = [Diagnostics] -> Diagnostics
forall a. Monoid a => [a] -> a
mconcat [Diagnostics
dg0, Diagnostics
dg1, Diagnostics
dg2, Diagnostics
dg3, Diagnostics
dg4, Diagnostics
dg5]

  (Diagnostics, GhcSpec) -> TcRn (Diagnostics, GhcSpec)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics
diags, SP
    { _gsConfig :: Config
_gsConfig = Config
cfg
    , _gsImps :: [(Symbol, Sort)]
_gsImps   = [(ModName, Spec (Located BareType) LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec (Located BareType) LocSymbol)]
mspecs
    , _gsSig :: GhcSpecSig
_gsSig    = Env
-> ModName -> BareRTEnv -> GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
addReflSigs Env
env ModName
name BareRTEnv
rtEnv GhcSpecRefl
refl GhcSpecSig
elaboratedSig
    , _gsRefl :: GhcSpecRefl
_gsRefl   = GhcSpecRefl
refl
    , _gsLaws :: GhcSpecLaws
_gsLaws   = GhcSpecLaws
laws
    , _gsData :: GhcSpecData
_gsData   = GhcSpecData
sData
    , _gsQual :: GhcSpecQual
_gsQual   = GhcSpecQual
qual
    , _gsName :: GhcSpecNames
_gsName   = Env -> TycEnv -> MeasEnv -> ModName -> GhcSpecNames
makeSpecName Env
env     TycEnv
tycEnv MeasEnv
measEnv   ModName
name
    , _gsVars :: GhcSpecVars
_gsVars   = GhcSpecVars
spcVars
    , _gsTerm :: GhcSpecTerm
_gsTerm   = GhcSpecTerm
spcTerm

    , _gsLSpec :: Spec (Located BareType) LocSymbol
_gsLSpec  = Spec (Located BareType) LocSymbol
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 :: CoreExpr -> Expr
coreToLg CoreExpr
ce =
      case TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> Error)
-> LogicM Expr
-> Either Error Expr
forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> ([Char] -> Error)
-> LogicM t
-> Either Error t
CoreToLogic.runToLogic
             TCEmb TyCon
embs
             LogicMap
lmap
             DataConMap
dm
             (\[Char]
x -> Maybe SrcSpan -> [Char] -> Error
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"coreToLogic not working " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
x))
             (Bool -> CoreExpr -> LogicM Expr
CoreToLogic.coreToLogic Bool
allowTC CoreExpr
ce) of
        Left Error
msg -> Maybe SrcSpan -> [Char] -> Expr
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (Error -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Error
msg)
        Right Expr
e -> Expr
e
    elaborateSig :: GhcSpecSig
-> [(TyVar, LocSpecType)]
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
elaborateSig GhcSpecSig
si [(TyVar, LocSpecType)]
auxsig = do
      [(TyVar, LocSpecType)]
tySigs <-
        [(TyVar, LocSpecType)]
-> ((TyVar, LocSpecType)
    -> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
-> TcRn [(TyVar, LocSpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
si) (((TyVar, LocSpecType)
  -> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
 -> TcRn [(TyVar, LocSpecType)])
-> ((TyVar, LocSpecType)
    -> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
-> TcRn [(TyVar, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ \(TyVar
x, LocSpecType
t) ->
          if TyVar -> Bool
forall a. NamedThing a => a -> Bool
GM.isFromGHCReal TyVar
x then
            (TyVar, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar
x, LocSpecType
t)
          else do LocSpecType
t' <- (SpecType -> TcRn SpecType)
-> LocSpecType -> IOEnv (Env TcGblEnv TcLclEnv) LocSpecType
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier) LocSpecType
t
                  (TyVar, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar
x, LocSpecType
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')
      GhcSpecSig -> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        GhcSpecSig
si
          { gsTySigs = F.notracepp ("asmSigs" ++ F.showpp (gsAsmSigs si)) tySigs ++ auxsig  }

    simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
    simplifier :: CoreExpr -> TcRn CoreExpr
simplifier = CoreExpr -> TcRn CoreExpr
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure -- no simplification
    allowTC :: Bool
allowTC  = Config -> Bool
typeclass Config
cfg
    mySpec2 :: Spec (Located BareType) LocSymbol
mySpec2  = Env
-> ModName
-> BareRTEnv
-> SourcePos
-> [Symbol]
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [] Spec (Located BareType) LocSymbol
mySpec1    where l :: SourcePos
l = [Char] -> SourcePos
F.dummyPos [Char]
"expand-mySpec2"
    iSpecs2 :: HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs2  = Env
-> ModName
-> BareRTEnv
-> SourcePos
-> [Symbol]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [] HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0    where l :: SourcePos
l = [Char] -> SourcePos
F.dummyPos [Char]
"expand-iSpecs2"
    rtEnv :: BareRTEnv
rtEnv    = Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> LogicMap
-> BareRTEnv
Bare.makeRTEnv Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec1 HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0 LogicMap
lmap
    mspecs :: [(ModName, Spec (Located BareType) LocSymbol)]
mspecs   = if Bool
allowTC then HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap ModName (Spec (Located BareType) LocSymbol)
 -> [(ModName, Spec (Located BareType) LocSymbol)])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a b. (a -> b) -> a -> b
$ ModName
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec (Located BareType) LocSymbol
mySpec0 HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0 else [(ModName, Spec (Located BareType) LocSymbol)]
mspecsNoCls
    (Spec (Located BareType) LocSymbol
mySpec0, [(ClsInst, [TyVar])]
instMethods)  = if Bool
allowTC
                              then GhcSrc
-> Env
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> (Spec (Located BareType) LocSymbol, [(ClsInst, [TyVar])])
Bare.compileClasses GhcSrc
src Env
env (ModName
name, Spec (Located BareType) LocSymbol
mySpec0NoCls) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0)
                              else (Spec (Located BareType) LocSymbol
mySpec0NoCls, [])
    mySpec1 :: Spec (Located BareType) LocSymbol
mySpec1  = Spec (Located BareType) LocSymbol
mySpec0 Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
forall a. Semigroup a => a -> a -> a
<> Spec (Located BareType) LocSymbol
lSpec0
    lSpec0 :: Spec (Located BareType) LocSymbol
lSpec0   = Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec (Located BareType) LocSymbol
mySpec0
    embs :: TCEmb TyCon
embs     = GhcSrc
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TCEmb TyCon
makeEmbeds          GhcSrc
src Env
env ((ModName
name, Spec (Located BareType) LocSymbol
mySpec0) (ModName, Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a. a -> [a] -> [a]
: HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0)
    dm :: DataConMap
dm       = TycEnv -> DataConMap
Bare.tcDataConMap TycEnv
tycEnv0
    (Diagnostics
dg0, [Located DataConP]
datacons, TycEnv
tycEnv0) = Config
-> ModName
-> Env
-> TCEmb TyCon
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0   Config
cfg ModName
name Env
env TCEmb TyCon
embs Spec (Located BareType) LocSymbol
mySpec2 HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs2
    -- extract name and specs
    env :: Env
env      = Config
-> GhcSrc
-> LogicMap
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Env
Bare.makeEnv Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec (Located BareType) LocSymbol)]
mspecsNoCls
    (Spec (Located BareType) LocSymbol
mySpec0NoCls, HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs0) = ModName
-> GhcSrc
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> (Spec (Located BareType) LocSymbol,
    HashMap ModName (Spec (Located BareType) LocSymbol))
splitSpecs ModName
name GhcSrc
src [(ModName, Spec (Located BareType) LocSymbol)]
mspecsNoCls
    -- check barespecs
    name :: ModName
name     = [Char] -> ModName -> ModName
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"ALL-SPECS" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
zzz) (ModName -> ModName) -> ModName -> ModName
forall a b. (a -> b) -> a -> b
$ GhcSrc -> ModName
_giTargetMod  GhcSrc
src
    zzz :: [Char]
zzz      = [ModName] -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp ((ModName, Spec (Located BareType) LocSymbol) -> ModName
forall a b. (a, b) -> a
fst ((ModName, Spec (Located BareType) LocSymbol) -> ModName)
-> [(ModName, Spec (Located BareType) LocSymbol)] -> [ModName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, Spec (Located BareType) LocSymbol)]
mspecs)

splitSpecs :: ModName -> GhcSrc -> [(ModName, Ms.BareSpec)] -> (Ms.BareSpec, Bare.ModSpecs)
splitSpecs :: ModName
-> GhcSrc
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> (Spec (Located BareType) LocSymbol,
    HashMap ModName (Spec (Located BareType) LocSymbol))
splitSpecs ModName
name GhcSrc
src [(ModName, Spec (Located BareType) LocSymbol)]
specs = (Spec (Located BareType) LocSymbol
mySpec, HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecm)
  where
    iSpecm :: HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecm             = ([Spec (Located BareType) LocSymbol]
 -> Spec (Located BareType) LocSymbol)
-> HashMap ModName [Spec (Located BareType) LocSymbol]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall a b. (a -> b) -> HashMap ModName a -> HashMap ModName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Spec (Located BareType) LocSymbol]
-> Spec (Located BareType) LocSymbol
forall a. Monoid a => [a] -> a
mconcat (HashMap ModName [Spec (Located BareType) LocSymbol]
 -> HashMap ModName (Spec (Located BareType) LocSymbol))
-> ([(ModName, Spec (Located BareType) LocSymbol)]
    -> HashMap ModName [Spec (Located BareType) LocSymbol])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(ModName, Spec (Located BareType) LocSymbol)]
-> HashMap ModName [Spec (Located BareType) LocSymbol]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group ([(ModName, Spec (Located BareType) LocSymbol)]
 -> HashMap ModName (Spec (Located BareType) LocSymbol))
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
forall a b. (a -> b) -> a -> b
$ [(ModName, Spec (Located BareType) LocSymbol)]
iSpecs
    iSpecs :: [(ModName, Spec (Located BareType) LocSymbol)]
iSpecs             = GhcSrc
-> Spec (Located BareType) LocSymbol
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
Dg.sliceSpecs GhcSrc
src Spec (Located BareType) LocSymbol
mySpec [(ModName, Spec (Located BareType) LocSymbol)]
iSpecs'
    mySpec :: Spec (Located BareType) LocSymbol
mySpec             = [Spec (Located BareType) LocSymbol]
-> Spec (Located BareType) LocSymbol
forall a. Monoid a => [a] -> a
mconcat ((ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd ((ModName, Spec (Located BareType) LocSymbol)
 -> Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [Spec (Located BareType) LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, Spec (Located BareType) LocSymbol)]
mySpecs)
    ([(ModName, Spec (Located BareType) LocSymbol)]
mySpecs, [(ModName, Spec (Located BareType) LocSymbol)]
iSpecs') = ((ModName, Spec (Located BareType) LocSymbol) -> Bool)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> ([(ModName, Spec (Located BareType) LocSymbol)],
    [(ModName, Spec (Located BareType) LocSymbol)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((ModName
name ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
==) (ModName -> Bool)
-> ((ModName, Spec (Located BareType) LocSymbol) -> ModName)
-> (ModName, Spec (Located BareType) LocSymbol)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol) -> ModName
forall a b. (a, b) -> a
fst) [(ModName, Spec (Located BareType) LocSymbol)]
specs


makeImports :: [(ModName, Ms.BareSpec)] -> [(F.Symbol, F.Sort)]
makeImports :: [(ModName, Spec (Located BareType) LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec (Located BareType) LocSymbol)]
specs = ((ModName, Spec (Located BareType) LocSymbol) -> [(Symbol, Sort)])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(Symbol, Sort)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Spec (Located BareType) LocSymbol -> [(Symbol, Sort)]
forall ty bndr. Spec ty bndr -> [(Symbol, Sort)]
expSigs (Spec (Located BareType) LocSymbol -> [(Symbol, Sort)])
-> ((ModName, Spec (Located BareType) LocSymbol)
    -> Spec (Located BareType) LocSymbol)
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd) [(ModName, Spec (Located BareType) LocSymbol)]
specs'
  where specs' :: [(ModName, Spec (Located BareType) LocSymbol)]
specs' = ((ModName, Spec (Located BareType) LocSymbol) -> Bool)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName -> Bool
isSrcImport (ModName -> Bool)
-> ((ModName, Spec (Located BareType) LocSymbol) -> ModName)
-> (ModName, Spec (Located BareType) LocSymbol)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol) -> ModName
forall a b. (a, b) -> a
fst) [(ModName, Spec (Located BareType) LocSymbol)]
specs


makeEmbeds :: GhcSrc -> Bare.Env -> [(ModName, Ms.BareSpec)] -> F.TCEmb Ghc.TyCon
makeEmbeds :: GhcSrc
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TCEmb TyCon
makeEmbeds GhcSrc
src Env
env
  = Maybe [ClsInst] -> [TyCon] -> TCEmb TyCon -> TCEmb TyCon
Bare.addClassEmbeds (GhcSrc -> Maybe [ClsInst]
_gsCls GhcSrc
src) (GhcSrc -> [TyCon]
_gsFiTcs GhcSrc
src)
  (TCEmb TyCon -> TCEmb TyCon)
-> ([(ModName, Spec (Located BareType) LocSymbol)] -> TCEmb TyCon)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TCEmb TyCon] -> TCEmb TyCon
forall a. Monoid a => [a] -> a
mconcat
  ([TCEmb TyCon] -> TCEmb TyCon)
-> ([(ModName, Spec (Located BareType) LocSymbol)]
    -> [TCEmb TyCon])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName, Spec (Located BareType) LocSymbol) -> TCEmb TyCon)
-> [(ModName, Spec (Located BareType) LocSymbol)] -> [TCEmb TyCon]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> (ModName, Spec (Located BareType) LocSymbol) -> TCEmb TyCon
makeTyConEmbeds Env
env)

makeTyConEmbeds :: Bare.Env -> (ModName, Ms.BareSpec) -> F.TCEmb Ghc.TyCon
makeTyConEmbeds :: Env -> (ModName, Spec (Located BareType) LocSymbol) -> TCEmb TyCon
makeTyConEmbeds Env
env (ModName
name, Spec (Located BareType) LocSymbol
spec)
  = [(TyCon, (Sort, TCArgs))] -> TCEmb TyCon
forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
F.tceFromList [ (TyCon
tc, (Sort, TCArgs)
t) | (LocSymbol
c,(Sort, TCArgs)
t) <- TCEmb LocSymbol -> [(LocSymbol, (Sort, TCArgs))]
forall a. TCEmb a -> [(a, (Sort, TCArgs))]
F.tceToList (Spec (Located BareType) LocSymbol -> TCEmb LocSymbol
forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
Ms.embeds Spec (Located BareType) LocSymbol
spec), TyCon
tc <- LocSymbol -> [TyCon]
forall {a}. ResolveSym a => LocSymbol -> [a]
symTc LocSymbol
c ]
    where
      symTc :: LocSymbol -> [a]
symTc = Maybe a -> [a]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe a -> [a]) -> (LocSymbol -> Maybe a) -> LocSymbol -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> ModName -> [Char] -> LocSymbol -> Maybe a
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"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
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec1 Config
config GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec (Located BareType) LocSymbol
mySpec = Spec (Located BareType) LocSymbol
forall a. Monoid a => a
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 :: Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec (Located BareType) LocSymbol
mySpec = Spec (Located BareType) LocSymbol
forall a. Monoid a => a
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 :: [TyCon]
tcs          = [TyCon] -> [TyCon]
forall a. Uniquable a => [a] -> [a]
uniqNub (GhcSrc -> [TyCon]
_gsTcs GhcSrc
src [TyCon] -> [TyCon] -> [TyCon]
forall a. [a] -> [a] -> [a]
++ [TyCon]
refTcs)
    refTcs :: [TyCon]
refTcs       = Config
-> TCEmb TyCon
-> [CoreBind]
-> Spec (Located BareType) LocSymbol
-> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs [CoreBind]
cbs  Spec (Located BareType) LocSymbol
mySpec
    cbs :: [CoreBind]
cbs          = GhcSrc -> [CoreBind]
_giCbs       GhcSrc
src
    name :: ModName
name         = GhcSrc -> ModName
_giTargetMod GhcSrc
src

uniqNub :: (Ghc.Uniquable a) => [a] -> [a]
uniqNub :: forall a. Uniquable a => [a] -> [a]
uniqNub [a]
xs = HashMap Int a -> [a]
forall k v. HashMap k v -> [v]
M.elems (HashMap Int a -> [a]) -> HashMap Int a -> [a]
forall a b. (a -> b) -> a -> b
$ [(Int, a)] -> HashMap Int a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (a -> Int
forall {a}. Uniquable a => a -> Int
index a
x, a
x) | a
x <- [a]
xs ]
  where
    index :: a -> Int
index  = Unique -> Int
Ghc.getKey (Unique -> Int) -> (a -> Unique) -> a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Unique
forall a. Uniquable a => a -> Unique
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 :: Config
-> TCEmb TyCon
-> [CoreBind]
-> Spec (Located BareType) LocSymbol
-> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs [CoreBind]
cbs Spec (Located BareType) LocSymbol
spec
  | Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg = (TyCon -> Bool) -> [TyCon] -> [TyCon]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TyCon -> Bool) -> TyCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs)
                    ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ (TyVar -> [TyCon]) -> [TyVar] -> [TyCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyVar -> [TyCon]
varTyCons
                    ([TyVar] -> [TyCon]) -> [TyVar] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ Spec (Located BareType) LocSymbol -> [CoreBind] -> [TyVar]
reflectedVars Spec (Located BareType) LocSymbol
spec [CoreBind]
cbs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ Spec (Located BareType) LocSymbol -> [CoreBind] -> [TyVar]
measureVars Spec (Located BareType) LocSymbol
spec [CoreBind]
cbs
  | Bool
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 :: TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs TyCon
c = TyCon -> TCEmb TyCon -> Bool
forall a. (Eq a, Hashable a) => a -> TCEmb a -> Bool
F.tceMember TyCon
c TCEmb TyCon
embs

varTyCons :: Ghc.Var -> [Ghc.TyCon]
varTyCons :: TyVar -> [TyCon]
varTyCons = SpecType -> [TyCon]
specTypeCons (SpecType -> [TyCon]) -> (TyVar -> SpecType) -> TyVar -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType (Type -> SpecType) -> (TyVar -> Type) -> TyVar -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType

specTypeCons           :: SpecType -> [Ghc.TyCon]
specTypeCons :: SpecType -> [TyCon]
specTypeCons         = ([TyCon] -> SpecType -> [TyCon]) -> [TyCon] -> SpecType -> [TyCon]
forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType [TyCon] -> SpecType -> [TyCon]
forall {tv} {r}. [TyCon] -> RType RTyCon tv r -> [TyCon]
tc []
  where
    tc :: [TyCon] -> RType RTyCon tv r -> [TyCon]
tc [TyCon]
acc t :: RType RTyCon tv r
t@RApp {} = RTyCon -> TyCon
rtc_tc (RType RTyCon tv r -> RTyCon
forall c tv r. RType c tv r -> c
rt_tycon RType RTyCon tv r
t) TyCon -> [TyCon] -> [TyCon]
forall a. a -> [a] -> [a]
: [TyCon]
acc
    tc [TyCon]
acc RType RTyCon tv r
_         = [TyCon]
acc

reflectedVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
reflectedVars :: Spec (Located BareType) LocSymbol -> [CoreBind] -> [TyVar]
reflectedVars Spec (Located BareType) LocSymbol
spec [CoreBind]
cbs = (TyVar, CoreExpr) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, CoreExpr) -> TyVar) -> [(TyVar, CoreExpr)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, CoreExpr)]
xDefs
  where
    xDefs :: [(TyVar, CoreExpr)]
xDefs              = (Symbol -> Maybe (TyVar, CoreExpr))
-> [Symbol] -> [(TyVar, CoreExpr)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Symbol -> [CoreBind] -> Maybe (TyVar, CoreExpr)
`GM.findVarDef` [CoreBind]
cbs) [Symbol]
reflSyms
    reflSyms :: [Symbol]
reflSyms           = LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol) -> [LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec (Located BareType) LocSymbol
spec)

measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
measureVars :: Spec (Located BareType) LocSymbol -> [CoreBind] -> [TyVar]
measureVars Spec (Located BareType) LocSymbol
spec [CoreBind]
cbs = (TyVar, CoreExpr) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, CoreExpr) -> TyVar) -> [(TyVar, CoreExpr)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, CoreExpr)]
xDefs
  where
    xDefs :: [(TyVar, CoreExpr)]
xDefs              = (Symbol -> Maybe (TyVar, CoreExpr))
-> [Symbol] -> [(TyVar, CoreExpr)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Symbol -> [CoreBind] -> Maybe (TyVar, CoreExpr)
`GM.findVarDef` [CoreBind]
cbs) [Symbol]
measureSyms
    measureSyms :: [Symbol]
measureSyms        = LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol) -> [LocSymbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Spec (Located BareType) LocSymbol
spec)

------------------------------------------------------------------------------------------
makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
             -> Bare.Lookup GhcSpecVars
------------------------------------------------------------------------------------------
makeSpecVars :: Config
-> GhcSrc
-> Spec (Located BareType) LocSymbol
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec (Located BareType) LocSymbol
mySpec Env
env MeasEnv
measEnv = do
  [TyVar]
tgtVars     <-   ([Char] -> Either [Error] TyVar)
-> [[Char]] -> Either [Error] [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> [Char] -> Either [Error] TyVar
resolveStringVar  Env
env ModName
name)              (Config -> [[Char]]
checks     Config
cfg)
  HashSet TyVar
igVars      <-  (LocSymbol -> Either [Error] TyVar)
-> HashSet LocSymbol -> Either [Error] (HashSet TyVar)
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"gs-ignores") (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.ignores Spec (Located BareType) LocSymbol
mySpec)
  HashSet TyVar
lVars       <-  (LocSymbol -> Either [Error] TyVar)
-> HashSet LocSymbol -> Either [Error] (HashSet TyVar)
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"gs-lvars"  ) (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lvars   Spec (Located BareType) LocSymbol
mySpec)
  GhcSpecVars -> Lookup GhcSpecVars
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TyVar] -> HashSet TyVar -> HashSet TyVar -> [TyVar] -> GhcSpecVars
SpVar [TyVar]
tgtVars HashSet TyVar
igVars HashSet TyVar
lVars [TyVar]
cMethods)
  where
    name :: ModName
name       = GhcSrc -> ModName
_giTargetMod GhcSrc
src
    cMethods :: [TyVar]
cMethods   = (ModName, TyVar, LocSpecType) -> TyVar
forall a b c. (a, b, c) -> b
snd3 ((ModName, TyVar, LocSpecType) -> TyVar)
-> [(ModName, TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(ModName, TyVar, LocSpecType)]
Bare.meMethods MeasEnv
measEnv

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

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

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

resolveStringVar :: Bare.Env -> ModName -> String -> Bare.Lookup Ghc.Var
resolveStringVar :: Env -> ModName -> [Char] -> Either [Error] TyVar
resolveStringVar Env
env ModName
name [Char]
s = Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"resolve-string-var" LocSymbol
lx
  where
    lx :: LocSymbol
lx                      = Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (ModName -> [Char] -> Symbol
forall a. Symbolic a => ModName -> a -> Symbol
qualifySymbolic ModName
name [Char]
s)



------------------------------------------------------------------------------------------
makeSpecQual :: Config -> Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> BareRTEnv -> Bare.ModSpecs
             -> GhcSpecQual
------------------------------------------------------------------------------------------
makeSpecQual :: Config
-> Env
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecQual
makeSpecQual Config
_cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
_rtEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs = SpQual
  { gsQualifiers :: [Qualifier]
gsQualifiers = (Qualifier -> Bool) -> [Qualifier] -> [Qualifier]
forall a. (a -> Bool) -> [a] -> [a]
filter Qualifier -> Bool
forall {a}. (PPrint a, Subable a) => a -> Bool
okQual [Qualifier]
quals
  , gsRTAliases :: [Located SpecRTAlias]
gsRTAliases  = [] -- makeSpecRTAliases env rtEnv -- TODO-REBARE
  }
  where
    quals :: [Qualifier]
quals        = ((ModName, Spec (Located BareType) LocSymbol) -> [Qualifier])
-> [(ModName, Spec (Located BareType) LocSymbol)] -> [Qualifier]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> TycEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [Qualifier]
forall ty bndr.
Env -> TycEnv -> (ModName, Spec ty bndr) -> [Qualifier]
makeQualifiers Env
env TycEnv
tycEnv) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
    -- mSyms        = F.tracepp "MSYMS" $ M.fromList (Bare.meSyms measEnv ++ Bare.meClassSyms measEnv)
    okQual :: a -> Bool
okQual a
q     = [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"okQual: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp a
q)
                   (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
mSyms) (a -> [Symbol]
forall a. Subable a => a -> [Symbol]
F.syms a
q)
    mSyms :: HashSet Symbol
mSyms        = [Char] -> HashSet Symbol -> HashSet Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"MSYMS" (HashSet Symbol -> HashSet Symbol)
-> ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
                   ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$  ((Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Symbol) -> [(Symbol, Sort)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
wiredSortedSyms)
                   [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Symbol, Located (RRType Reft)) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Located (RRType Reft)) -> Symbol)
-> [(Symbol, Located (RRType Reft))] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms MeasEnv
measEnv)
                   [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ ((Symbol, Located (RRType Reft)) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Located (RRType Reft)) -> Symbol)
-> [(Symbol, Located (RRType Reft))] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meClassSyms MeasEnv
measEnv)

makeQualifiers :: Bare.Env -> Bare.TycEnv -> (ModName, Ms.Spec ty bndr) -> [F.Qualifier]
makeQualifiers :: forall ty bndr.
Env -> TycEnv -> (ModName, Spec ty bndr) -> [Qualifier]
makeQualifiers Env
env TycEnv
tycEnv (ModName
modn, Spec ty bndr
spec)
  = (Qualifier -> Qualifier) -> [Qualifier] -> [Qualifier]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap        (Env -> ModName -> Qualifier -> Qualifier
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env        ModName
modn)
  ([Qualifier] -> [Qualifier])
-> ([Qualifier] -> [Qualifier]) -> [Qualifier] -> [Qualifier]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Qualifier -> Maybe Qualifier) -> [Qualifier] -> [Qualifier]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Env -> TycEnv -> ModName -> Qualifier -> Maybe Qualifier
resolveQParams       Env
env TycEnv
tycEnv ModName
modn)
  ([Qualifier] -> [Qualifier]) -> [Qualifier] -> [Qualifier]
forall a b. (a -> b) -> a -> b
$ Spec ty bndr -> [Qualifier]
forall ty bndr. Spec ty bndr -> [Qualifier]
Ms.qualifiers Spec ty bndr
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 -> ModName -> Qualifier -> Maybe Qualifier
resolveQParams Env
env TycEnv
tycEnv ModName
name Qualifier
q = do
     [QualParam]
qps   <- (QualParam -> Maybe QualParam) -> [QualParam] -> Maybe [QualParam]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM QualParam -> Maybe QualParam
goQP (Qualifier -> [QualParam]
F.qParams Qualifier
q)
     Qualifier -> Maybe Qualifier
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Qualifier -> Maybe Qualifier) -> Qualifier -> Maybe Qualifier
forall a b. (a -> b) -> a -> b
$ Qualifier
q { F.qParams = qps }
  where
    goQP :: QualParam -> Maybe QualParam
goQP QualParam
qp          = do { Sort
s <- Sort -> Maybe Sort
go (QualParam -> Sort
F.qpSort QualParam
qp) ; QualParam -> Maybe QualParam
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return QualParam
qp { F.qpSort = s } }
    go               :: F.Sort -> Maybe F.Sort
    go :: Sort -> Maybe Sort
go (FAbs Int
i Sort
s)    = Int -> Sort -> Sort
FAbs Int
i (Sort -> Sort) -> Maybe Sort -> Maybe Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s
    go (FFunc Sort
s1 Sort
s2) = Sort -> Sort -> Sort
FFunc  (Sort -> Sort -> Sort) -> Maybe Sort -> Maybe (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s1 Maybe (Sort -> Sort) -> Maybe Sort -> Maybe Sort
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> Maybe Sort
go Sort
s2
    go (FApp  Sort
s1 Sort
s2) = Sort -> Sort -> Sort
FApp   (Sort -> Sort -> Sort) -> Maybe Sort -> Maybe (Sort -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s1 Maybe (Sort -> Sort) -> Maybe Sort -> Maybe Sort
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Sort -> Maybe Sort
go Sort
s2
    go (FTC FTycon
c)       = Env -> TycEnv -> ModName -> FTycon -> Maybe Sort
qualifyFTycon Env
env TycEnv
tycEnv ModName
name FTycon
c
    go Sort
s             = Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
s

qualifyFTycon :: Bare.Env -> Bare.TycEnv -> ModName -> F.FTycon -> Maybe F.Sort
qualifyFTycon :: Env -> TycEnv -> ModName -> FTycon -> Maybe Sort
qualifyFTycon Env
env TycEnv
tycEnv ModName
name FTycon
c
  | Bool
isPrimFTC           = Sort -> Maybe Sort
forall a. a -> Maybe a
Just (FTycon -> Sort
FTC FTycon
c)
  | Bool
otherwise           = TCEmb TyCon -> Located TyCon -> Sort
tyConSort TCEmb TyCon
embs (Located TyCon -> Sort)
-> (TyCon -> Located TyCon) -> TyCon -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> TyCon -> Located TyCon
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
tcs (TyCon -> Sort) -> Maybe TyCon -> Maybe Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe TyCon
forall {a}. ResolveSym a => Maybe a
ty
  where
    ty :: Maybe a
ty                  = Env -> ModName -> [Char] -> LocSymbol -> Maybe a
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"qualify-FTycon" LocSymbol
tcs
    isPrimFTC :: Bool
isPrimFTC           = LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
tcs Symbol -> HashSet Symbol -> Bool
forall a. Eq a => a -> HashSet a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HashSet Symbol
F.prims
    tcs :: LocSymbol
tcs                 = FTycon -> LocSymbol
F.fTyconSymbol FTycon
c
    embs :: TCEmb TyCon
embs                = TycEnv -> TCEmb TyCon
Bare.tcEmbs TycEnv
tycEnv

tyConSort :: F.TCEmb Ghc.TyCon -> F.Located Ghc.TyCon -> F.Sort
tyConSort :: TCEmb TyCon -> Located TyCon -> Sort
tyConSort TCEmb TyCon
embs Located TyCon
lc = Sort -> ((Sort, TCArgs) -> Sort) -> Maybe (Sort, TCArgs) -> Sort
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Sort
s0 (Sort, TCArgs) -> Sort
forall a b. (a, b) -> a
fst (TyCon -> TCEmb TyCon -> Maybe (Sort, TCArgs)
forall a.
(Eq a, Hashable a) =>
a -> TCEmb a -> Maybe (Sort, TCArgs)
F.tceLookup TyCon
c TCEmb TyCon
embs)
  where
    c :: TyCon
c             = Located TyCon -> TyCon
forall a. Located a -> a
F.val Located TyCon
lc
    s0 :: Sort
s0            = Located TyCon -> Sort
tyConSortRaw Located TyCon
lc

tyConSortRaw :: F.Located Ghc.TyCon -> F.Sort
tyConSortRaw :: Located TyCon -> Sort
tyConSortRaw = FTycon -> Sort
FTC (FTycon -> Sort)
-> (Located TyCon -> FTycon) -> Located TyCon -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> FTycon
F.symbolFTycon (LocSymbol -> FTycon)
-> (Located TyCon -> LocSymbol) -> Located TyCon -> FTycon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon -> Symbol) -> Located TyCon -> LocSymbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol

------------------------------------------------------------------------------------------
makeSpecTerm :: Config -> Ms.BareSpec -> Bare.Env -> ModName ->
                Bare.Lookup GhcSpecTerm
------------------------------------------------------------------------------------------
makeSpecTerm :: Config
-> Spec (Located BareType) LocSymbol
-> Env
-> ModName
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg Spec (Located BareType) LocSymbol
mySpec Env
env ModName
name = do
  HashSet TyVar
sizes  <- if Config -> Bool
forall t. HasConfig t => t -> Bool
structuralTerm Config
cfg then HashSet TyVar -> Either [Error] (HashSet TyVar)
forall a. a -> Either [Error] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure HashSet TyVar
forall a. Monoid a => a
mempty else Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
makeSize Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
  HashSet TyVar
lazies <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
makeLazy     Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
  HashSet TyCon
autos  <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet TyCon)
makeAutoSize Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
  HashSet (Located TyVar)
gfail  <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet (Located TyVar))
makeFail Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
  GhcSpecTerm -> Lookup GhcSpecTerm
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return  (GhcSpecTerm -> Lookup GhcSpecTerm)
-> GhcSpecTerm -> Lookup GhcSpecTerm
forall a b. (a -> b) -> a -> b
$ SpTerm
    { gsLazy :: HashSet TyVar
gsLazy       = TyVar -> HashSet TyVar -> HashSet TyVar
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert TyVar
dictionaryVar (HashSet TyVar
lazies HashSet TyVar -> HashSet TyVar -> HashSet TyVar
forall a. Monoid a => a -> a -> a
`mappend` HashSet TyVar
sizes)
    , gsFail :: HashSet (Located TyVar)
gsFail       = HashSet (Located TyVar)
gfail
    , gsStTerm :: HashSet TyVar
gsStTerm     = HashSet TyVar
sizes
    , gsAutosize :: HashSet TyCon
gsAutosize   = HashSet TyCon
autos
    , gsNonStTerm :: HashSet TyVar
gsNonStTerm  = HashSet TyVar
forall a. Monoid a => a
mempty
    }

makeRelation :: Bare.Env -> ModName -> Bare.SigEnv ->
  [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr, RelExpr)] -> Bare.Lookup [(Ghc.Var, Ghc.Var, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation :: Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
     RelExpr, RelExpr)]
-> Lookup
     [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv = ((LocSymbol, LocSymbol, Located BareType, Located BareType,
  RelExpr, RelExpr)
 -> Either
      [Error] (TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr))
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
     RelExpr, RelExpr)]
-> Lookup
     [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (LocSymbol, LocSymbol, Located BareType, Located BareType, RelExpr,
 RelExpr)
-> Either
     [Error] (TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)
forall {e} {f}.
(LocSymbol, LocSymbol, Located BareType, Located BareType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
go
 where
  go :: (LocSymbol, LocSymbol, Located BareType, Located BareType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
go (LocSymbol
x, LocSymbol
y, Located BareType
tx, Located BareType
ty, e
a, f
e) = do
    TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
    TyVar
vy <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
y
    (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return
        ( TyVar
vx
        , TyVar
vy
        , Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.HsTV TyVar
vx) Located BareType
tx
        , Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.HsTV TyVar
vy) Located BareType
ty
        , e
a
        , f
e
        )


makeLazy :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeLazy :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
makeLazy Env
env ModName
name Spec (Located BareType) LocSymbol
spec =
  (LocSymbol -> Either [Error] TyVar)
-> HashSet LocSymbol -> Either [Error] (HashSet TyVar)
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var") (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lazy Spec (Located BareType) LocSymbol
spec)

makeFail :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeFail :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet (Located TyVar))
makeFail Env
env ModName
name Spec (Located BareType) LocSymbol
spec =
  HashSet LocSymbol
-> (LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar))
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.fails Spec (Located BareType) LocSymbol
spec) ((LocSymbol -> Either [Error] (Located TyVar))
 -> Lookup (HashSet (Located TyVar)))
-> (LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar))
forall a b. (a -> b) -> a -> b
$ \LocSymbol
x -> do
    TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
    Located TyVar -> Either [Error] (Located TyVar)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return LocSymbol
x { val = vx }

makeRewrite :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet (Located Ghc.Var))
makeRewrite :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet (Located TyVar))
makeRewrite Env
env ModName
name Spec (Located BareType) LocSymbol
spec =
  HashSet LocSymbol
-> (LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar))
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
HashSet a -> (a -> m b) -> m (HashSet b)
sForM (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.rewrites Spec (Located BareType) LocSymbol
spec) ((LocSymbol -> Either [Error] (Located TyVar))
 -> Lookup (HashSet (Located TyVar)))
-> (LocSymbol -> Either [Error] (Located TyVar))
-> Lookup (HashSet (Located TyVar))
forall a b. (a -> b) -> a -> b
$ \LocSymbol
x -> do
    TyVar
vx <-  Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
    Located TyVar -> Either [Error] (Located TyVar)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return LocSymbol
x { val = vx }

makeRewriteWith :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (M.HashMap Ghc.Var [Ghc.Var])
makeRewriteWith :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashMap TyVar [TyVar])
makeRewriteWith Env
env ModName
name Spec (Located BareType) LocSymbol
spec = [(TyVar, [TyVar])] -> HashMap TyVar [TyVar]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(TyVar, [TyVar])] -> HashMap TyVar [TyVar])
-> Either [Error] [(TyVar, [TyVar])]
-> Lookup (HashMap TyVar [TyVar])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] [(TyVar, [TyVar])]
forall ty bndr.
Env -> ModName -> Spec ty bndr -> Either [Error] [(TyVar, [TyVar])]
makeRewriteWith' Env
env ModName
name Spec (Located BareType) LocSymbol
spec

makeRewriteWith' :: Bare.Env -> ModName -> Spec ty bndr -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' :: forall ty bndr.
Env -> ModName -> Spec ty bndr -> Either [Error] [(TyVar, [TyVar])]
makeRewriteWith' Env
env ModName
name Spec ty bndr
spec =
  [(LocSymbol, [LocSymbol])]
-> ((LocSymbol, [LocSymbol]) -> Either [Error] (TyVar, [TyVar]))
-> Either [Error] [(TyVar, [TyVar])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])])
-> HashMap LocSymbol [LocSymbol] -> [(LocSymbol, [LocSymbol])]
forall a b. (a -> b) -> a -> b
$ Spec ty bndr -> HashMap LocSymbol [LocSymbol]
forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
Ms.rewriteWith Spec ty bndr
spec) (((LocSymbol, [LocSymbol]) -> Either [Error] (TyVar, [TyVar]))
 -> Either [Error] [(TyVar, [TyVar])])
-> ((LocSymbol, [LocSymbol]) -> Either [Error] (TyVar, [TyVar]))
-> Either [Error] [(TyVar, [TyVar])]
forall a b. (a -> b) -> a -> b
$ \(LocSymbol
x, [LocSymbol]
xs) -> do
    TyVar
xv  <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var1" LocSymbol
x
    [TyVar]
xvs <- (LocSymbol -> Either [Error] TyVar)
-> [LocSymbol] -> Either [Error] [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var2") [LocSymbol]
xs
    (TyVar, [TyVar]) -> Either [Error] (TyVar, [TyVar])
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
xv, [TyVar]
xvs)

makeAutoSize :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.TyCon)
makeAutoSize :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet TyCon)
makeAutoSize Env
env ModName
name
  = ([TyCon] -> HashSet TyCon)
-> Either [Error] [TyCon] -> Lookup (HashSet TyCon)
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TyCon] -> HashSet TyCon
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
  (Either [Error] [TyCon] -> Lookup (HashSet TyCon))
-> (Spec (Located BareType) LocSymbol -> Either [Error] [TyCon])
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet TyCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol -> Either [Error] TyCon)
-> [LocSymbol] -> Either [Error] [TyCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyCon
Bare.lookupGhcTyCon Env
env ModName
name [Char]
"TyCon")
  ([LocSymbol] -> Either [Error] [TyCon])
-> (Spec (Located BareType) LocSymbol -> [LocSymbol])
-> Spec (Located BareType) LocSymbol
-> Either [Error] [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList
  (HashSet LocSymbol -> [LocSymbol])
-> (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> Spec (Located BareType) LocSymbol
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.autosize

makeSize :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeSize :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
makeSize Env
env ModName
name
  = ([TyVar] -> HashSet TyVar)
-> Either [Error] [TyVar] -> Either [Error] (HashSet TyVar)
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
  (Either [Error] [TyVar] -> Either [Error] (HashSet TyVar))
-> (Spec (Located BareType) LocSymbol -> Either [Error] [TyVar])
-> Spec (Located BareType) LocSymbol
-> Either [Error] (HashSet TyVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol -> Either [Error] TyVar)
-> [LocSymbol] -> Either [Error] [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var")
  ([LocSymbol] -> Either [Error] [TyVar])
-> (Spec (Located BareType) LocSymbol -> [LocSymbol])
-> Spec (Located BareType) LocSymbol
-> Either [Error] [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> Maybe LocSymbol) -> [DataDecl] -> [LocSymbol]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe LocSymbol
getSizeFuns
  ([DataDecl] -> [LocSymbol])
-> (Spec (Located BareType) LocSymbol -> [DataDecl])
-> Spec (Located BareType) LocSymbol
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec (Located BareType) LocSymbol -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls

getSizeFuns :: DataDecl -> Maybe LocSymbol
getSizeFuns :: DataDecl -> Maybe LocSymbol
getSizeFuns DataDecl
decl
  | Just SizeFun
x       <- DataDecl -> Maybe SizeFun
tycSFun DataDecl
decl
  , SymSizeFun LocSymbol
f <- SizeFun
x
  = LocSymbol -> Maybe LocSymbol
forall a. a -> Maybe a
Just LocSymbol
f
  | Bool
otherwise
  = Maybe LocSymbol
forall a. Maybe a
Nothing


------------------------------------------------------------------------------------------
makeSpecLaws :: Bare.Env -> Bare.SigEnv -> [(Ghc.Var,LocSpecType)] -> Bare.MeasEnv -> Bare.ModSpecs
             -> GhcSpecLaws
------------------------------------------------------------------------------------------
makeSpecLaws :: Env
-> SigEnv
-> [(TyVar, LocSpecType)]
-> MeasEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv [(TyVar, LocSpecType)]
sigs MeasEnv
menv HashMap ModName (Spec (Located BareType) LocSymbol)
specs = SpLaws
  { gsLawDefs :: [(Class, [(TyVar, LocSpecType)])]
gsLawDefs = ([(ModName, TyVar, LocSpecType)] -> [(TyVar, LocSpecType)])
-> (Class, [(ModName, TyVar, LocSpecType)])
-> (Class, [(TyVar, LocSpecType)])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (((ModName, TyVar, LocSpecType) -> (TyVar, LocSpecType))
-> [(ModName, TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a b. (a -> b) -> [a] -> [b]
map (\(ModName
_,TyVar
x,LocSpecType
y) -> (TyVar
x,LocSpecType
y))) ((Class, [(ModName, TyVar, LocSpecType)])
 -> (Class, [(TyVar, LocSpecType)]))
-> [(Class, [(ModName, TyVar, LocSpecType)])]
-> [(Class, [(TyVar, LocSpecType)])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.meCLaws MeasEnv
menv
  , gsLawInst :: [LawInstance]
gsLawInst = Env
-> SigEnv
-> [(TyVar, LocSpecType)]
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [LawInstance]
Bare.makeInstanceLaws Env
env SigEnv
sigEnv [(TyVar, LocSpecType)]
sigs HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  }

------------------------------------------------------------------------------------------
makeSpecRefl :: Config -> GhcSrc -> Bare.MeasEnv -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
             -> Bare.Lookup GhcSpecRefl
------------------------------------------------------------------------------------------
makeSpecRefl :: Config
-> GhcSrc
-> MeasEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl Config
cfg GhcSrc
src MeasEnv
menv HashMap ModName (Spec (Located BareType) LocSymbol)
specs Env
env ModName
name GhcSpecSig
sig TycEnv
tycEnv = do
  HashMap TyVar (Maybe Int)
autoInst <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashMap TyVar (Maybe Int))
makeAutoInst Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
  HashSet (Located TyVar)
rwr      <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashSet (Located TyVar))
makeRewrite Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
  HashMap TyVar [TyVar]
rwrWith  <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashMap TyVar [TyVar])
makeRewriteWith Env
env ModName
name Spec (Located BareType) LocSymbol
mySpec
  [TyVar]
wRefls   <- Config -> Env -> ModName -> GhcSpecSig -> Either [Error] [TyVar]
Bare.wiredReflects Config
cfg Env
env ModName
name GhcSpecSig
sig
  [(TyVar, LocSpecType, Equation)]
xtes     <- Config
-> GhcSrc
-> Env
-> TycEnv
-> ModName
-> LogicMap
-> GhcSpecSig
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, LocSpecType, Equation)]
Bare.makeHaskellAxioms Config
cfg GhcSrc
src Env
env TycEnv
tycEnv ModName
name LogicMap
lmap GhcSpecSig
sig Spec (Located BareType) LocSymbol
mySpec
  let myAxioms :: [Equation]
myAxioms =
        [ Env -> ModName -> SourcePos -> Equation -> Equation
forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop
            Env
env
            ModName
name
            (LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc LocSpecType
lt)
            Equation
e {eqName = s, eqRec = S.member s (exprSymbolsSet (eqBody e))}
        | (TyVar
x, LocSpecType
lt, Equation
e) <- [(TyVar, LocSpecType, Equation)]
xtes
        , let s :: Symbol
s = TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
x
        ]
  let sigVars :: [TyVar]
sigVars  = [Char] -> [TyVar] -> [TyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SIGVARS" ([TyVar] -> [TyVar]) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ ((TyVar, LocSpecType, Equation) -> TyVar
forall a b c. (a, b, c) -> a
fst3 ((TyVar, LocSpecType, Equation) -> TyVar)
-> [(TyVar, LocSpecType, Equation)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType, Equation)]
xtes)            -- reflects
                                      [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ ((TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst  ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
sig)   -- assumes
                                      [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ ((TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst  ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, LocSpecType)]
gsRefSigs GhcSpecSig
sig)
  GhcSpecRefl -> Lookup GhcSpecRefl
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return SpRefl
    { gsLogicMap :: LogicMap
gsLogicMap   = LogicMap
lmap
    , gsAutoInst :: HashMap TyVar (Maybe Int)
gsAutoInst   = HashMap TyVar (Maybe Int)
autoInst
    , gsImpAxioms :: [Equation]
gsImpAxioms  = ((ModName, Spec (Located BareType) LocSymbol) -> [Equation])
-> [(ModName, Spec (Located BareType) LocSymbol)] -> [Equation]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Spec (Located BareType) LocSymbol -> [Equation]
forall ty bndr. Spec ty bndr -> [Equation]
Ms.axeqs (Spec (Located BareType) LocSymbol -> [Equation])
-> ((ModName, Spec (Located BareType) LocSymbol)
    -> Spec (Located BareType) LocSymbol)
-> (ModName, Spec (Located BareType) LocSymbol)
-> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
    , gsMyAxioms :: [Equation]
gsMyAxioms   = [Char] -> [Equation] -> [Equation]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsMyAxioms" [Equation]
myAxioms
    , gsReflects :: [TyVar]
gsReflects   = [Char] -> [TyVar] -> [TyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsReflects" ([TyVar]
lawMethods [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (HashSet Symbol -> TyVar -> Bool
isReflectVar HashSet Symbol
rflSyms) [TyVar]
sigVars [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
wRefls)
    , gsHAxioms :: [(TyVar, LocSpecType, Equation)]
gsHAxioms    = [Char]
-> [(TyVar, LocSpecType, Equation)]
-> [(TyVar, LocSpecType, Equation)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsHAxioms" [(TyVar, LocSpecType, Equation)]
xtes
    , gsWiredReft :: [TyVar]
gsWiredReft  = [TyVar]
wRefls
    , gsRewrites :: HashSet (Located TyVar)
gsRewrites   = HashSet (Located TyVar)
rwr
    , gsRewritesWith :: HashMap TyVar [TyVar]
gsRewritesWith = HashMap TyVar [TyVar]
rwrWith
    }
  where
    lawMethods :: [TyVar]
lawMethods   = [Char] -> [TyVar] -> [TyVar]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"Law Methods" ([TyVar] -> [TyVar]) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ (Class -> [TyVar]) -> [Class] -> [TyVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Class -> [TyVar]
Ghc.classMethods ((Class, [(ModName, TyVar, LocSpecType)]) -> Class
forall a b. (a, b) -> a
fst ((Class, [(ModName, TyVar, LocSpecType)]) -> Class)
-> [(Class, [(ModName, TyVar, LocSpecType)])] -> [Class]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.meCLaws MeasEnv
menv)
    mySpec :: Spec (Located BareType) LocSymbol
mySpec       = Spec (Located BareType) LocSymbol
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Spec (Located BareType) LocSymbol
forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
    rflSyms :: HashSet Symbol
rflSyms      = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (HashMap ModName (Spec (Located BareType) LocSymbol) -> [Symbol]
getReflects HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
    lmap :: LogicMap
lmap         = Env -> LogicMap
Bare.reLMap Env
env

isReflectVar :: S.HashSet F.Symbol -> Ghc.Var -> Bool
isReflectVar :: HashSet Symbol -> TyVar -> Bool
isReflectVar HashSet Symbol
reflSyms TyVar
v = Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
vx HashSet Symbol
reflSyms
  where
    vx :: Symbol
vx                  = Symbol -> Symbol
GM.dropModuleNames (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v)

getReflects :: Bare.ModSpecs -> [Symbol]
getReflects :: HashMap ModName (Spec (Located BareType) LocSymbol) -> [Symbol]
getReflects  = (LocSymbol -> Symbol) -> [LocSymbol] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LocSymbol -> Symbol
forall a. Located a -> a
val ([LocSymbol] -> [Symbol])
-> (HashMap ModName (Spec (Located BareType) LocSymbol)
    -> [LocSymbol])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (HashSet LocSymbol -> [LocSymbol])
-> (HashMap ModName (Spec (Located BareType) LocSymbol)
    -> HashSet LocSymbol)
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [HashSet LocSymbol] -> HashSet LocSymbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet LocSymbol] -> HashSet LocSymbol)
-> (HashMap ModName (Spec (Located BareType) LocSymbol)
    -> [HashSet LocSymbol])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> HashSet LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName, Spec (Located BareType) LocSymbol) -> HashSet LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [HashSet LocSymbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
names (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> ((ModName, Spec (Located BareType) LocSymbol)
    -> Spec (Located BareType) LocSymbol)
-> (ModName, Spec (Located BareType) LocSymbol)
-> HashSet LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall a b. (a, b) -> b
snd) ([(ModName, Spec (Located BareType) LocSymbol)]
 -> [HashSet LocSymbol])
-> (HashMap ModName (Spec (Located BareType) LocSymbol)
    -> [(ModName, Spec (Located BareType) LocSymbol)])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [HashSet LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList
  where
    names :: Spec ty bndr -> HashSet LocSymbol
names  Spec ty bndr
z = [HashSet LocSymbol] -> HashSet LocSymbol
forall a. Eq a => [HashSet a] -> HashSet a
S.unions [ Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec ty bndr
z, Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines Spec ty bndr
z, Spec ty bndr -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Spec ty bndr
z ]

------------------------------------------------------------------------------------------
-- | @updateReflSpecSig@ uses the information about reflected functions to update the
--   "assumed" signatures.
------------------------------------------------------------------------------------------
addReflSigs :: Bare.Env -> ModName -> BareRTEnv -> GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
------------------------------------------------------------------------------------------
addReflSigs :: Env
-> ModName -> BareRTEnv -> GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
addReflSigs Env
env ModName
name BareRTEnv
rtEnv GhcSpecRefl
refl GhcSpecSig
sig =
  GhcSpecSig
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 :: (TyVar, LocSpecType) -> (TyVar, LocSpecType)
expandReflectedSignature = (LocSpecType -> LocSpecType)
-> (TyVar, LocSpecType) -> (TyVar, LocSpecType)
forall a b. (a -> b) -> (TyVar, a) -> (TyVar, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env
-> ModName
-> BareRTEnv
-> SourcePos
-> [Symbol]
-> LocSpecType
-> LocSpecType
forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv ([Char] -> SourcePos
F.dummyPos [Char]
"expand-refSigs") [])

    ([(TyVar, LocSpecType)]
wreflSigs, [(TyVar, LocSpecType)]
reflSigs)   = ((TyVar, LocSpecType) -> Bool)
-> [(TyVar, LocSpecType)]
-> ([(TyVar, LocSpecType)], [(TyVar, LocSpecType)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((TyVar -> [TyVar] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GhcSpecRefl -> [TyVar]
gsWiredReft GhcSpecRefl
refl) (TyVar -> Bool)
-> ((TyVar, LocSpecType) -> TyVar) -> (TyVar, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst)
                                 [ (TyVar
x, LocSpecType
t) | (TyVar
x, LocSpecType
t, Equation
_) <- GhcSpecRefl -> [(TyVar, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl ]
    reflected :: [TyVar]
reflected       = (TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(TyVar, LocSpecType)]
wreflSigs [(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
reflSigs)
    notReflected :: (TyVar, b) -> Bool
notReflected (TyVar, b)
xt = (TyVar, b) -> TyVar
forall a b. (a, b) -> a
fst (TyVar, b)
xt TyVar -> [TyVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [TyVar]
reflected

makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec ->
                Bare.Lookup (M.HashMap Ghc.Var (Maybe Int))
makeAutoInst :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup (HashMap TyVar (Maybe Int))
makeAutoInst Env
env ModName
name Spec (Located BareType) LocSymbol
spec = [(TyVar, Maybe Int)] -> HashMap TyVar (Maybe Int)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(TyVar, Maybe Int)] -> HashMap TyVar (Maybe Int))
-> Either [Error] [(TyVar, Maybe Int)]
-> Lookup (HashMap TyVar (Maybe Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either [Error] [(TyVar, Maybe Int)]
kvs
  where
    kvs :: Either [Error] [(TyVar, Maybe Int)]
kvs = [(LocSymbol, Maybe Int)]
-> ((LocSymbol, Maybe Int) -> Either [Error] (TyVar, Maybe Int))
-> Either [Error] [(TyVar, Maybe Int)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (HashMap LocSymbol (Maybe Int) -> [(LocSymbol, Maybe Int)]
forall k v. HashMap k v -> [(k, v)]
M.toList (Spec (Located BareType) LocSymbol -> HashMap LocSymbol (Maybe Int)
forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
Ms.autois Spec (Located BareType) LocSymbol
spec)) (((LocSymbol, Maybe Int) -> Either [Error] (TyVar, Maybe Int))
 -> Either [Error] [(TyVar, Maybe Int)])
-> ((LocSymbol, Maybe Int) -> Either [Error] (TyVar, Maybe Int))
-> Either [Error] [(TyVar, Maybe Int)]
forall a b. (a -> b) -> a -> b
$ \(LocSymbol
k, Maybe Int
val) -> do
            TyVar
vk <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
k
            (TyVar, Maybe Int) -> Either [Error] (TyVar, Maybe Int)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
vk, Maybe Int
val)


----------------------------------------------------------------------------------------
makeSpecSig :: Config -> ModName -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]
            -> Bare.Lookup GhcSpecSig
----------------------------------------------------------------------------------------
makeSpecSig :: Config
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> Lookup GhcSpecSig
makeSpecSig Config
cfg ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs Env
env SigEnv
sigEnv TycEnv
tycEnv MeasEnv
measEnv [CoreBind]
cbs = do
  [(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs     <- Env
-> SigEnv
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs  Env
env SigEnv
sigEnv ModName
name Spec (Located BareType) LocSymbol
mySpec
  [(TyVar, LocSpecType)]
aSigs      <- [Char]
-> Lookup [(TyVar, LocSpecType)] -> Lookup [(TyVar, LocSpecType)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"makeSpecSig aSigs " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ModName -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp ModName
name) (Lookup [(TyVar, LocSpecType)] -> Lookup [(TyVar, LocSpecType)])
-> Lookup [(TyVar, LocSpecType)] -> Lookup [(TyVar, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  let asmSigs :: [(TyVar, LocSpecType)]
asmSigs =  TycEnv -> [(TyVar, LocSpecType)]
Bare.tcSelVars TycEnv
tycEnv
              [(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
aSigs
              [(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [ (TyVar
x,LocSpecType
t) | (ModName
_, TyVar
x, LocSpecType
t) <- ((Class, [(ModName, TyVar, LocSpecType)])
 -> [(ModName, TyVar, LocSpecType)])
-> [(Class, [(ModName, TyVar, LocSpecType)])]
-> [(ModName, TyVar, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Class, [(ModName, TyVar, LocSpecType)])
-> [(ModName, TyVar, LocSpecType)]
forall a b. (a, b) -> b
snd (MeasEnv -> [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.meCLaws MeasEnv
measEnv) ]
  let tySigs :: [(TyVar, LocSpecType)]
tySigs  = [(TyVar, (Int, LocSpecType))] -> [(TyVar, LocSpecType)]
strengthenSigs ([(TyVar, (Int, LocSpecType))] -> [(TyVar, LocSpecType)])
-> ([[(TyVar, (Int, LocSpecType))]]
    -> [(TyVar, (Int, LocSpecType))])
-> [[(TyVar, (Int, LocSpecType))]]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(TyVar, (Int, LocSpecType))]] -> [(TyVar, (Int, LocSpecType))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(TyVar, (Int, LocSpecType))]] -> [(TyVar, LocSpecType)])
-> [[(TyVar, (Int, LocSpecType))]] -> [(TyVar, LocSpecType)]
forall a b. (a -> b) -> a -> b
$
                  [ [(TyVar
v, (Int
0, LocSpecType
t)) | (TyVar
v, LocSpecType
t,Maybe [Located Expr]
_) <- [(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs                         ]   -- NOTE: these weights are to priortize
                  , [(TyVar
v, (Int
1, LocSpecType
t)) | (TyVar
v, LocSpecType
t  ) <- MeasEnv -> [(TyVar, LocSpecType)]
makeMthSigs MeasEnv
measEnv            ]   -- user defined sigs OVER auto-generated
                  , [(TyVar
v, (Int
2, LocSpecType
t)) | (TyVar
v, LocSpecType
t  ) <- Env
-> BareRTEnv
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs ]   -- during the strengthening, i.e. to KEEP
                  , [(TyVar
v, (Int
3, LocSpecType
t)) | (TyVar
v, LocSpecType
t  ) <- Env
-> BareRTEnv
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs ]   -- the binders used in USER-defined sigs
                  ]                                                               -- as they appear in termination metrics
  [(TyCon, LocSpecType)]
newTys     <-  Env
-> SigEnv
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs
  [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
relation   <-  Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
     RelExpr, RelExpr)]
-> Lookup
     [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv (Spec (Located BareType) LocSymbol
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
     RelExpr, RelExpr)]
forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Ms.relational Spec (Located BareType) LocSymbol
mySpec)
  [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
asmRel     <-  Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
     RelExpr, RelExpr)]
-> Lookup
     [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv (Spec (Located BareType) LocSymbol
-> [(LocSymbol, LocSymbol, Located BareType, Located BareType,
     RelExpr, RelExpr)]
forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Ms.asmRel Spec (Located BareType) LocSymbol
mySpec)
  GhcSpecSig -> Lookup GhcSpecSig
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return SpSig
    { gsTySigs :: [(TyVar, LocSpecType)]
gsTySigs   = [(TyVar, LocSpecType)]
tySigs
    , gsAsmSigs :: [(TyVar, LocSpecType)]
gsAsmSigs  = [(TyVar, LocSpecType)]
asmSigs
    , gsRefSigs :: [(TyVar, LocSpecType)]
gsRefSigs  = []
    , gsDicts :: DEnv TyVar LocSpecType
gsDicts    = DEnv TyVar LocSpecType
dicts
    -- , gsMethods  = if noclasscheck cfg then [] else Bare.makeMethodTypes dicts (Bare.meClasses  measEnv) cbs
    , gsMethods :: [(TyVar, MethodType LocSpecType)]
gsMethods  = if Config -> Bool
noclasscheck Config
cfg then [] else Bool
-> DEnv TyVar LocSpecType
-> [DataConP]
-> [CoreBind]
-> [(TyVar, MethodType LocSpecType)]
Bare.makeMethodTypes (Config -> Bool
typeclass Config
cfg) DEnv TyVar LocSpecType
dicts (MeasEnv -> [DataConP]
Bare.meClasses  MeasEnv
measEnv) [CoreBind]
cbs
    , gsInSigs :: [(TyVar, LocSpecType)]
gsInSigs   = [(TyVar, LocSpecType)]
forall a. Monoid a => a
mempty
    , gsNewTypes :: [(TyCon, LocSpecType)]
gsNewTypes = [(TyCon, LocSpecType)]
newTys
    , gsTexprs :: [(TyVar, LocSpecType, [Located Expr])]
gsTexprs   = [ (TyVar
v, LocSpecType
t, [Located Expr]
es) | (TyVar
v, LocSpecType
t, Just [Located Expr]
es) <- [(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs ]
    , gsRelation :: [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsRelation = [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
relation
    , gsAsmRel :: [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
gsAsmRel   = [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
asmRel
  }
  where
    dicts :: DEnv TyVar LocSpecType
dicts      = Env
-> SigEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> DEnv TyVar LocSpecType
Bare.makeSpecDictionaries Env
env SigEnv
sigEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs
    mySpec :: Spec (Located BareType) LocSymbol
mySpec     = Spec (Located BareType) LocSymbol
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Spec (Located BareType) LocSymbol
forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
    allSpecs :: [(ModName, Spec (Located BareType) LocSymbol)]
allSpecs   = HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs
    rtEnv :: BareRTEnv
rtEnv      = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
    -- hmeas      = makeHMeas    env allSpecs

strengthenSigs :: [(Ghc.Var, (Int, LocSpecType))] ->[(Ghc.Var, LocSpecType)]
strengthenSigs :: [(TyVar, (Int, LocSpecType))] -> [(TyVar, LocSpecType)]
strengthenSigs [(TyVar, (Int, LocSpecType))]
sigs = (TyVar, [(Int, LocSpecType)]) -> (TyVar, LocSpecType)
forall {a} {b}.
(PPrint a, Ord b) =>
(a, [(b, LocSpecType)]) -> (a, LocSpecType)
go ((TyVar, [(Int, LocSpecType)]) -> (TyVar, LocSpecType))
-> [(TyVar, [(Int, LocSpecType)])] -> [(TyVar, LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, (Int, LocSpecType))] -> [(TyVar, [(Int, LocSpecType)])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(TyVar, (Int, LocSpecType))]
sigs
  where
    go :: (a, [(b, LocSpecType)]) -> (a, LocSpecType)
go (a
v, [(b, LocSpecType)]
ixs)     = (a
v,) (LocSpecType -> (a, LocSpecType))
-> LocSpecType -> (a, LocSpecType)
forall a b. (a -> b) -> a -> b
$ (LocSpecType -> LocSpecType -> LocSpecType)
-> [LocSpecType] -> LocSpecType
forall a. HasCallStack => (a -> a -> a) -> [a] -> a
L.foldl1' ((LocSpecType -> LocSpecType -> LocSpecType)
-> LocSpecType -> LocSpecType -> LocSpecType
forall a b c. (a -> b -> c) -> b -> a -> c
flip LocSpecType -> LocSpecType -> LocSpecType
meetLoc) ([Char] -> [LocSpecType] -> [LocSpecType]
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"STRENGTHEN-SIGS: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp a
v) ([(b, LocSpecType)] -> [LocSpecType]
forall {b} {b}. Ord b => [(b, b)] -> [b]
prio [(b, LocSpecType)]
ixs))
    prio :: [(b, b)] -> [b]
prio            = ((b, b) -> b) -> [(b, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b, b) -> b
forall a b. (a, b) -> b
snd ([(b, b)] -> [b]) -> ([(b, b)] -> [(b, b)]) -> [(b, b)] -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b) -> b) -> [(b, b)] -> [(b, b)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn (b, b) -> b
forall a b. (a, b) -> a
fst
    meetLoc         :: LocSpecType -> LocSpecType -> LocSpecType
    meetLoc :: LocSpecType -> LocSpecType -> LocSpecType
meetLoc LocSpecType
t1 LocSpecType
t2   = LocSpecType
t1 {val = val t1 `F.meet` val t2}

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

makeInlSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeInlSigs :: Env
-> BareRTEnv
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv
  = BareRTEnv
-> (TyVar -> SpecType) -> [TyVar] -> [(TyVar, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv (Bool -> TyVar -> SpecType
CoreToLogic.inlineSpecType (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)))
  ([TyVar] -> [(TyVar, LocSpecType)])
-> ([(ModName, Spec (Located BareType) LocSymbol)] -> [TyVar])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [TyVar]
makeFromSet [Char]
"hinlines" Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines Env
env

makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeMsrSigs :: Env
-> BareRTEnv
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv
  = BareRTEnv
-> (TyVar -> SpecType) -> [TyVar] -> [(TyVar, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv (Bool -> TyVar -> SpecType
CoreToLogic.inlineSpecType (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)))
  ([TyVar] -> [(TyVar, LocSpecType)])
-> ([(ModName, Spec (Located BareType) LocSymbol)] -> [TyVar])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [TyVar]
makeFromSet [Char]
"hmeas" Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas Env
env

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

makeFromSet :: String -> (Ms.BareSpec -> S.HashSet LocSymbol) -> Bare.Env -> [(ModName, Ms.BareSpec)]
            -> [Ghc.Var]
makeFromSet :: [Char]
-> (Spec (Located BareType) LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [TyVar]
makeFromSet [Char]
msg Spec (Located BareType) LocSymbol -> HashSet LocSymbol
f Env
env [(ModName, Spec (Located BareType) LocSymbol)]
specs = [[TyVar]] -> [TyVar]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ ModName -> [LocSymbol] -> [TyVar]
forall {b}. ResolveSym b => ModName -> [LocSymbol] -> [b]
mk ModName
n [LocSymbol]
xs | (ModName
n, Spec (Located BareType) LocSymbol
s) <- [(ModName, Spec (Located BareType) LocSymbol)]
specs, let xs :: [LocSymbol]
xs = HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
f Spec (Located BareType) LocSymbol
s)]
  where
    mk :: ModName -> [LocSymbol] -> [b]
mk ModName
name                 = (LocSymbol -> Maybe b) -> [LocSymbol] -> [b]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Env -> ModName -> [Char] -> LocSymbol -> Maybe b
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
msg)

makeTySigs :: Bare.Env -> Bare.SigEnv -> ModName -> Ms.BareSpec
           -> Bare.Lookup [(Ghc.Var, LocSpecType, Maybe [Located F.Expr])]
makeTySigs :: Env
-> SigEnv
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs Env
env SigEnv
sigEnv ModName
name Spec (Located BareType) LocSymbol
spec = do
  [(TyVar, Located BareType)]
bareSigs   <- Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, Located BareType)]
bareTySigs Env
env ModName
name                Spec (Located BareType) LocSymbol
spec
  [(TyVar, Located BareType, Maybe [Located Expr])]
expSigs    <- Env
-> ModName
-> [(TyVar, Located BareType)]
-> BareRTEnv
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, Located BareType, Maybe [Located Expr])]
makeTExpr  Env
env ModName
name [(TyVar, Located BareType)]
bareSigs BareRTEnv
rtEnv Spec (Located BareType) LocSymbol
spec
  let rawSigs :: [(TyVar, Located BareType, Maybe [Located Expr])]
rawSigs = Env
-> [(TyVar, Located BareType, Maybe [Located Expr])]
-> [(TyVar, Located BareType, Maybe [Located Expr])]
Bare.resolveLocalBinds Env
env [(TyVar, Located BareType, Maybe [Located Expr])]
expSigs
  [(TyVar, LocSpecType, Maybe [Located Expr])]
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
x, TyVar -> Located BareType -> LocSpecType
cook TyVar
x Located BareType
bt, Maybe [Located Expr]
z) | (TyVar
x, Located BareType
bt, Maybe [Located Expr]
z) <- [(TyVar, Located BareType, Maybe [Located Expr])]
rawSigs ]
  where
    rtEnv :: BareRTEnv
rtEnv     = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
    cook :: TyVar -> Located BareType -> LocSpecType
cook TyVar
x Located BareType
bt = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.HsTV TyVar
x) Located BareType
bt

bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
bareTySigs :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, Located BareType)]
bareTySigs Env
env ModName
name Spec (Located BareType) LocSymbol
spec = [(TyVar, Located BareType)] -> [(TyVar, Located BareType)]
forall x t. Symbolic x => [(x, Located t)] -> [(x, Located t)]
checkDuplicateSigs ([(TyVar, Located BareType)] -> [(TyVar, Located BareType)])
-> Lookup [(TyVar, Located BareType)]
-> Lookup [(TyVar, Located BareType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lookup [(TyVar, Located BareType)]
vts
  where
    vts :: Lookup [(TyVar, Located BareType)]
vts = [(LocSymbol, Located BareType)]
-> ((LocSymbol, Located BareType)
    -> Either [Error] (TyVar, Located BareType))
-> Lookup [(TyVar, Located BareType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs Spec (Located BareType) LocSymbol
spec [(LocSymbol, Located BareType)]
-> [(LocSymbol, Located BareType)]
-> [(LocSymbol, Located BareType)]
forall a. [a] -> [a] -> [a]
++ Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.localSigs Spec (Located BareType) LocSymbol
spec ) (((LocSymbol, Located BareType)
  -> Either [Error] (TyVar, Located BareType))
 -> Lookup [(TyVar, Located BareType)])
-> ((LocSymbol, Located BareType)
    -> Either [Error] (TyVar, Located BareType))
-> Lookup [(TyVar, Located BareType)]
forall a b. (a -> b) -> a -> b
$ \ (LocSymbol
x, Located BareType
t) -> do
            TyVar
v <- [Char] -> Either [Error] TyVar -> Either [Error] TyVar
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"LOOKUP-GHC-VAR" (Either [Error] TyVar -> Either [Error] TyVar)
-> Either [Error] TyVar -> Either [Error] TyVar
forall a b. (a -> b) -> a -> b
$ Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"rawTySigs" LocSymbol
x
            (TyVar, Located BareType)
-> Either [Error] (TyVar, Located BareType)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
v, Located BareType
t)

-- checkDuplicateSigs :: [(Ghc.Var, LocSpecType)] -> [(Ghc.Var, LocSpecType)]
checkDuplicateSigs :: (Symbolic x) => [(x, F.Located t)] -> [(x, F.Located t)]
checkDuplicateSigs :: forall x t. Symbolic x => [(x, Located t)] -> [(x, Located t)]
checkDuplicateSigs [(x, Located t)]
xts = case [(Symbol, SourcePos)] -> Either (Symbol, [SourcePos]) [SourcePos]
forall k v. (Eq k, Hashable k) => [(k, v)] -> Either (k, [v]) [v]
Misc.uniqueByKey [(Symbol, SourcePos)]
symXs  of
  Left (Symbol
k, [SourcePos]
ls) -> UserError -> [(x, Located t)]
forall a. UserError -> a
uError (Doc -> ListNE SrcSpan -> UserError
forall t. Doc -> ListNE SrcSpan -> TError t
errDupSpecs (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
k) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> [SourcePos] -> ListNE SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SourcePos]
ls))
  Right [SourcePos]
_      -> [(x, Located t)]
xts
  where
    symXs :: [(Symbol, SourcePos)]
symXs = [ (x -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol x
x, Located t -> SourcePos
forall a. Located a -> SourcePos
F.loc Located t
t) | (x
x, Located t
t) <- [(x, Located t)]
xts ]


makeAsmSigs :: Bare.Env -> Bare.SigEnv -> ModName -> Bare.ModSpecs -> Bare.Lookup [(Ghc.Var, LocSpecType)]
makeAsmSigs :: Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs = do
  [(ModName, TyVar, Located BareType)]
raSigs <- Env
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(ModName, TyVar, Located BareType)]
rawAsmSigs Env
env ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  [(TyVar, LocSpecType)] -> Lookup [(TyVar, LocSpecType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
x, LocSpecType
t) | (ModName
name, TyVar
x, Located BareType
bt) <- [(ModName, TyVar, Located BareType)]
raSigs, let t :: LocSpecType
t = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.LqTV TyVar
x) Located BareType
bt ]

rawAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs -> Bare.Lookup [(ModName, Ghc.Var, LocBareType)]
rawAsmSigs :: Env
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(ModName, TyVar, Located BareType)]
rawAsmSigs Env
env ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs = do
  [(TyVar, [(Bool, ModName, Located BareType)])]
aSigs <- Env
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
allAsmSigs Env
env ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  [(ModName, TyVar, Located BareType)]
-> Lookup [(ModName, TyVar, Located BareType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (ModName
m, TyVar
v, Located BareType
t) | (TyVar
v, [(Bool, ModName, Located BareType)]
sigs) <- [(TyVar, [(Bool, ModName, Located BareType)])]
aSigs, let (ModName
m, Located BareType
t) = TyVar
-> [(Bool, ModName, Located BareType)]
-> (ModName, Located BareType)
myAsmSig TyVar
v [(Bool, ModName, Located BareType)]
sigs ]

myAsmSig :: Ghc.Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig :: TyVar
-> [(Bool, ModName, Located BareType)]
-> (ModName, Located BareType)
myAsmSig TyVar
v [(Bool, ModName, Located BareType)]
sigs = (ModName, Located BareType)
-> Maybe (ModName, Located BareType) -> (ModName, Located BareType)
forall a. a -> Maybe a -> a
Mb.fromMaybe (ModName, Located BareType)
forall {a}. a
errImp (Maybe (ModName, Located BareType)
mbHome Maybe (ModName, Located BareType)
-> Maybe (ModName, Located BareType)
-> Maybe (ModName, Located BareType)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (ModName, Located BareType)
mbImp)
  where
    mbHome :: Maybe (ModName, Located BareType)
mbHome      = ([(ModName, Located BareType)] -> UserError)
-> [(ModName, Located BareType)]
-> Maybe (ModName, Located BareType)
forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [(ModName, Located BareType)] -> UserError
forall {a} {a}. [(a, Located a)] -> UserError
mkErr                  [(ModName, Located BareType)]
sigsHome
    mbImp :: Maybe (ModName, Located BareType)
mbImp       = ([(ModName, Located BareType)] -> UserError)
-> [(ModName, Located BareType)]
-> Maybe (ModName, Located BareType)
forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [(ModName, Located BareType)] -> UserError
forall {a} {a}. [(a, Located a)] -> UserError
mkErr ([(Int, (ModName, Located BareType))]
-> [(ModName, Located BareType)]
forall k a. (Eq k, Ord k, Hashable k) => [(k, a)] -> [a]
Misc.firstGroup [(Int, (ModName, Located BareType))]
sigsImp) -- see [NOTE:Prioritize-Home-Spec]
    sigsHome :: [(ModName, Located BareType)]
sigsHome    = [(ModName
m, Located BareType
t)      | (Bool
True,  ModName
m, Located BareType
t) <- [(Bool, ModName, Located BareType)]
sigs ]
    sigsImp :: [(Int, (ModName, Located BareType))]
sigsImp     = [Char]
-> [(Int, (ModName, Located BareType))]
-> [(Int, (ModName, Located BareType))]
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"SIGS-IMP: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyVar -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp TyVar
v)
                  [(Int
d, (ModName
m, Located BareType
t)) | (Bool
False, ModName
m, Located BareType
t) <- [(Bool, ModName, Located BareType)]
sigs, let d :: Int
d = Symbol -> ModName -> Int
nameDistance Symbol
vName ModName
m]
    mkErr :: [(a, Located a)] -> UserError
mkErr [(a, Located a)]
ts    = SrcSpan -> Doc -> ListNE SrcSpan -> UserError
forall t. SrcSpan -> Doc -> ListNE SrcSpan -> TError t
ErrDupSpecs (TyVar -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan TyVar
v) (TyVar -> Doc
forall a. PPrint a => a -> Doc
F.pprint TyVar
v) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan)
-> ((a, Located a) -> SourcePos) -> (a, Located a) -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> SourcePos
forall a. Located a -> SourcePos
F.loc (Located a -> SourcePos)
-> ((a, Located a) -> Located a) -> (a, Located a) -> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Located a) -> Located a
forall a b. (a, b) -> b
snd ((a, Located a) -> SrcSpan) -> [(a, Located a)] -> ListNE SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Located a)]
ts) :: UserError
    errImp :: a
errImp      = Maybe SrcSpan -> [Char] -> a
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"myAsmSig: cannot happen as sigs is non-null"
    vName :: Symbol
vName       = Symbol -> Symbol
GM.takeModuleNames (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v)

makeTExpr :: Bare.Env -> ModName -> [(Ghc.Var, LocBareType)] -> BareRTEnv -> Ms.BareSpec
          -> Bare.Lookup [(Ghc.Var, LocBareType, Maybe [Located F.Expr])]
makeTExpr :: Env
-> ModName
-> [(TyVar, Located BareType)]
-> BareRTEnv
-> Spec (Located BareType) LocSymbol
-> Lookup [(TyVar, Located BareType, Maybe [Located Expr])]
makeTExpr Env
env ModName
name [(TyVar, Located BareType)]
tySigs BareRTEnv
rtEnv Spec (Located BareType) LocSymbol
spec = do
  HashMap TyVar [Located Expr]
vExprs       <- [(TyVar, [Located Expr])] -> HashMap TyVar [Located Expr]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(TyVar, [Located Expr])] -> HashMap TyVar [Located Expr])
-> Either [Error] [(TyVar, [Located Expr])]
-> Either [Error] (HashMap TyVar [Located Expr])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] [(TyVar, [Located Expr])]
makeVarTExprs Env
env ModName
name Spec (Located BareType) LocSymbol
spec
  let vSigExprs :: HashMap TyVar (Located BareType, Maybe [Located Expr])
vSigExprs = (TyVar
 -> Located BareType -> (Located BareType, Maybe [Located Expr]))
-> HashMap TyVar (Located BareType)
-> HashMap TyVar (Located BareType, Maybe [Located Expr])
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
Misc.hashMapMapWithKey (\TyVar
v Located BareType
t -> (Located BareType
t, TyVar -> HashMap TyVar [Located Expr] -> Maybe [Located Expr]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup TyVar
v HashMap TyVar [Located Expr]
vExprs)) HashMap TyVar (Located BareType)
vSigs
  [(TyVar, Located BareType, Maybe [Located Expr])]
-> Lookup [(TyVar, Located BareType, Maybe [Located Expr])]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
v, Located BareType
t, Located BareType -> [Located Expr] -> [Located Expr]
forall {f :: * -> *}.
Functor f =>
Located BareType -> f (Located Expr) -> f (Located Expr)
qual Located BareType
t ([Located Expr] -> [Located Expr])
-> Maybe [Located Expr] -> Maybe [Located Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Located Expr]
es) | (TyVar
v, (Located BareType
t, Maybe [Located Expr]
es)) <- HashMap TyVar (Located BareType, Maybe [Located Expr])
-> [(TyVar, (Located BareType, Maybe [Located Expr]))]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap TyVar (Located BareType, Maybe [Located Expr])
vSigExprs ]
  where
    qual :: Located BareType -> f (Located Expr) -> f (Located Expr)
qual Located BareType
t f (Located Expr)
es   = Env
-> ModName
-> BareRTEnv
-> Located BareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv Located BareType
t (Located Expr -> Located Expr)
-> f (Located Expr) -> f (Located Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Located Expr)
es
    vSigs :: HashMap TyVar (Located BareType)
vSigs       = [(TyVar, Located BareType)] -> HashMap TyVar (Located BareType)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(TyVar, Located BareType)]
tySigs

qualifyTermExpr :: Bare.Env -> ModName -> BareRTEnv -> LocBareType -> Located F.Expr
                -> Located F.Expr
qualifyTermExpr :: Env
-> ModName
-> BareRTEnv
-> Located BareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv Located BareType
t Located Expr
le
        = Located Expr -> Expr -> Located Expr
forall l b. Loc l => l -> b -> Located b
F.atLoc Located Expr
le (Env
-> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> Expr -> Expr
forall a.
(PPrint a, Expand a, Qualify a) =>
Env -> ModName -> BareRTEnv -> SourcePos -> [Symbol] -> a -> a
Bare.qualifyExpand Env
env ModName
name BareRTEnv
rtEnv SourcePos
l [Symbol]
bs Expr
e)
  where
    l :: SourcePos
l   = Located Expr -> SourcePos
forall a. Located a -> SourcePos
F.loc Located Expr
le
    e :: Expr
e   = Located Expr -> Expr
forall a. Located a -> a
F.val Located Expr
le
    bs :: [Symbol]
bs  = RTypeRep BTyCon BTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds (RTypeRep BTyCon BTyVar RReft -> [Symbol])
-> (Located BareType -> RTypeRep BTyCon BTyVar RReft)
-> Located BareType
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareType -> RTypeRep BTyCon BTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (BareType -> RTypeRep BTyCon BTyVar RReft)
-> (Located BareType -> BareType)
-> Located BareType
-> RTypeRep BTyCon BTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located BareType -> BareType
forall a. Located a -> a
val (Located BareType -> [Symbol]) -> Located BareType -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Located BareType
t

makeVarTExprs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
makeVarTExprs :: Env
-> ModName
-> Spec (Located BareType) LocSymbol
-> Either [Error] [(TyVar, [Located Expr])]
makeVarTExprs Env
env ModName
name Spec (Located BareType) LocSymbol
spec =
  [(LocSymbol, [Located Expr])]
-> ((LocSymbol, [Located Expr])
    -> Either [Error] (TyVar, [Located Expr]))
-> Either [Error] [(TyVar, [Located Expr])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec (Located BareType) LocSymbol -> [(LocSymbol, [Located Expr])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
Ms.termexprs Spec (Located BareType) LocSymbol
spec) (((LocSymbol, [Located Expr])
  -> Either [Error] (TyVar, [Located Expr]))
 -> Either [Error] [(TyVar, [Located Expr])])
-> ((LocSymbol, [Located Expr])
    -> Either [Error] (TyVar, [Located Expr]))
-> Either [Error] [(TyVar, [Located Expr])]
forall a b. (a -> b) -> a -> b
$ \(LocSymbol
x, [Located Expr]
es) -> do
    TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
    (TyVar, [Located Expr]) -> Either [Error] (TyVar, [Located Expr])
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
vx, [Located Expr]
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 :: Symbol -> ModName -> Int
nameDistance Symbol
vName ModName
tName
  | Symbol
vName Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
tName = Int
0
  | Bool
otherwise               = Int
1


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

allAsmSigs :: Bare.Env -> ModName -> Bare.ModSpecs ->
              Bare.Lookup [(Ghc.Var, [(Bool, ModName, LocBareType)])]
allAsmSigs :: Env
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
allAsmSigs Env
env ModName
myName HashMap ModName (Spec (Located BareType) LocSymbol)
specs = do
  let aSigs :: [(ModName, Bool, LocSymbol, Located BareType)]
aSigs = [ (ModName
name, Bool
locallyDefined, LocSymbol
x, Located BareType
t) | (ModName
name, Spec (Located BareType) LocSymbol
spec) <- HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs
                                   , (Bool
locallyDefined, LocSymbol
x, Located BareType
t) <- ModName
-> ModName
-> Spec (Located BareType) LocSymbol
-> [(Bool, LocSymbol, Located BareType)]
getAsmSigs ModName
myName ModName
name Spec (Located BareType) LocSymbol
spec ]
  [(Maybe TyVar, (Bool, ModName, Located BareType))]
vSigs    <- [(ModName, Bool, LocSymbol, Located BareType)]
-> ((ModName, Bool, LocSymbol, Located BareType)
    -> Either [Error] (Maybe TyVar, (Bool, ModName, Located BareType)))
-> Either
     [Error] [(Maybe TyVar, (Bool, ModName, Located BareType))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, Bool, LocSymbol, Located BareType)]
aSigs (((ModName, Bool, LocSymbol, Located BareType)
  -> Either [Error] (Maybe TyVar, (Bool, ModName, Located BareType)))
 -> Either
      [Error] [(Maybe TyVar, (Bool, ModName, Located BareType))])
-> ((ModName, Bool, LocSymbol, Located BareType)
    -> Either [Error] (Maybe TyVar, (Bool, ModName, Located BareType)))
-> Either
     [Error] [(Maybe TyVar, (Bool, ModName, Located BareType))]
forall a b. (a -> b) -> a -> b
$ \(ModName
name, Bool
locallyDefined, LocSymbol
x, Located BareType
t) -> do
                -- Qualified assumes that refer to module aliases import declarations
                -- are resolved looking at import declarations
                let (Maybe Symbol
mm, Symbol
s) = Symbol -> (Maybe Symbol, Symbol)
Bare.unQualifySymbol (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x)
                Maybe TyVar
vMb <- if Bool -> Bool
not (Maybe Symbol -> Bool
isAbsoluteQualifiedSym Maybe Symbol
mm) then Env -> ModName -> Bool -> LocSymbol -> Lookup (Maybe TyVar)
resolveAsmVar Env
env ModName
name Bool
locallyDefined LocSymbol
x
                       else if Bool
locallyDefined then
                         -- Fully qualified assumes that are locally defined produce an error if they aren't found
                         LocSymbol -> (Maybe Symbol, Symbol) -> Lookup (Maybe TyVar)
lookupImportedSym LocSymbol
x (Maybe Symbol
mm, Symbol
s)
                       else
                         -- Imported fully qualified assumes do not produce an error if they
                         -- aren't found, and we looked them anyway without considering
                         -- import declarations.
                         -- LH seems to send here assumes for data constructors that
                         -- yield Nothing, like for GHC.Types.W#
                         Maybe TyVar -> Lookup (Maybe TyVar)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TyVar -> Lookup (Maybe TyVar))
-> Maybe TyVar -> Lookup (Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ (Maybe Symbol, Symbol) -> Maybe TyVar
lookupImportedSymMaybe (Maybe Symbol
mm, Symbol
s)
                (Maybe TyVar, (Bool, ModName, Located BareType))
-> Either [Error] (Maybe TyVar, (Bool, ModName, Located BareType))
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TyVar
vMb, (Bool
locallyDefined, ModName
name, Located BareType
t))
  [(TyVar, [(Bool, ModName, Located BareType)])]
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return    ([(TyVar, [(Bool, ModName, Located BareType)])]
 -> Lookup [(TyVar, [(Bool, ModName, Located BareType)])])
-> [(TyVar, [(Bool, ModName, Located BareType)])]
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
forall a b. (a -> b) -> a -> b
$ [(TyVar, (Bool, ModName, Located BareType))]
-> [(TyVar, [(Bool, ModName, Located BareType)])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [ (TyVar
v, (Bool, ModName, Located BareType)
z) | (Just TyVar
v, (Bool, ModName, Located BareType)
z) <- [(Maybe TyVar, (Bool, ModName, Located BareType))]
vSigs ]
  where
    lookupImportedSym :: LocSymbol -> (Maybe Symbol, Symbol) -> Lookup (Maybe TyVar)
lookupImportedSym LocSymbol
x (Maybe Symbol, Symbol)
qp =
      let errRes :: Either [Error] b
errRes = [Error] -> Either [Error] b
forall a b. a -> Either a b
Left [Doc -> [Char] -> LocSymbol -> Error
Bare.errResolve Doc
"variable" [Char]
"Var" LocSymbol
x]
       in Lookup (Maybe TyVar)
-> (TyVar -> Lookup (Maybe TyVar))
-> Maybe TyVar
-> Lookup (Maybe TyVar)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Lookup (Maybe TyVar)
forall {b}. Either [Error] b
errRes (Maybe TyVar -> Lookup (Maybe TyVar)
forall a b. b -> Either a b
Right (Maybe TyVar -> Lookup (Maybe TyVar))
-> (TyVar -> Maybe TyVar) -> TyVar -> Lookup (Maybe TyVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just) (Maybe TyVar -> Lookup (Maybe TyVar))
-> Maybe TyVar -> Lookup (Maybe TyVar)
forall a b. (a -> b) -> a -> b
$
            (Maybe Symbol, Symbol) -> Maybe TyVar
lookupImportedSymMaybe (Maybe Symbol, Symbol)
qp
    lookupImportedSymMaybe :: (Maybe Symbol, Symbol) -> Maybe TyVar
lookupImportedSymMaybe (Maybe Symbol
mm, Symbol
s) = do
      [(Symbol, TyThing)]
mts <- Symbol
-> HashMap Symbol [(Symbol, TyThing)] -> Maybe [(Symbol, TyThing)]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
s (Env -> HashMap Symbol [(Symbol, TyThing)]
Bare._reTyThings Env
env)
      Symbol
m <- Maybe Symbol
mm
      [TyVar] -> Maybe TyVar
forall a. [a] -> Maybe a
Mb.listToMaybe [ TyVar
v | (Symbol
k, Ghc.AnId TyVar
v) <- [(Symbol, TyThing)]
mts, Symbol
k Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
m ]

    isAbsoluteQualifiedSym :: Maybe Symbol -> Bool
isAbsoluteQualifiedSym (Just Symbol
m) =
       Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> HashMap Symbol [Symbol] -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
m (HashMap Symbol [Symbol] -> Bool)
-> HashMap Symbol [Symbol] -> Bool
forall a b. (a -> b) -> a -> b
$ QImports -> HashMap Symbol [Symbol]
qiNames (Env -> QImports
Bare.reQualImps Env
env)
    isAbsoluteQualifiedSym Maybe Symbol
Nothing =
       Bool
False

resolveAsmVar :: Bare.Env -> ModName -> Bool -> LocSymbol -> Bare.Lookup (Maybe Ghc.Var)
resolveAsmVar :: Env -> ModName -> Bool -> LocSymbol -> Lookup (Maybe TyVar)
resolveAsmVar Env
env ModName
name Bool
True  LocSymbol
lx = TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just  (TyVar -> Maybe TyVar)
-> Either [Error] TyVar -> Lookup (Maybe TyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> ModName -> [Char] -> LocSymbol -> Either [Error] TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"resolveAsmVar-True"  LocSymbol
lx
resolveAsmVar Env
env ModName
name Bool
False LocSymbol
lx = Maybe TyVar -> Lookup (Maybe TyVar)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TyVar -> Lookup (Maybe TyVar))
-> Maybe TyVar -> Lookup (Maybe TyVar)
forall a b. (a -> b) -> a -> b
$  Env -> ModName -> [Char] -> LocSymbol -> Maybe TyVar
forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym     Env
env ModName
name [Char]
"resolveAsmVar-False" LocSymbol
lx  Maybe TyVar -> Maybe TyVar -> Maybe TyVar
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Maybe TyVar
GM.maybeAuxVar (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx)


getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, LocSymbol, LocBareType)]
getAsmSigs :: ModName
-> ModName
-> Spec (Located BareType) LocSymbol
-> [(Bool, LocSymbol, Located BareType)]
getAsmSigs ModName
myName ModName
name Spec (Located BareType) LocSymbol
spec
  | ModName
myName ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
name = [ (Bool
True,  LocSymbol
x,  Located BareType
t) | (LocSymbol
x, Located BareType
t) <- Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec (Located BareType) LocSymbol
spec ] -- MUST    resolve, or error
  | Bool
otherwise      = [ (Bool
False, LocSymbol
x', Located BareType
t) | (LocSymbol
x, Located BareType
t) <- Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec (Located BareType) LocSymbol
spec
                                                  [(LocSymbol, Located BareType)]
-> [(LocSymbol, Located BareType)]
-> [(LocSymbol, Located BareType)]
forall a. [a] -> [a] -> [a]
++ Spec (Located BareType) LocSymbol
-> [(LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs Spec (Located BareType) LocSymbol
spec
                                      , let x' :: LocSymbol
x' = LocSymbol -> LocSymbol
forall {f :: * -> *}. Functor f => f Symbol -> f Symbol
qSym LocSymbol
x           ]  -- MAY-NOT resolve
  where
    qSym :: f Symbol -> f Symbol
qSym           = (Symbol -> Symbol) -> f Symbol -> f Symbol
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol -> Symbol -> Symbol
GM.qualifySymbol Symbol
ns)
    ns :: Symbol
ns             = ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name

-- TODO-REBARE: grepClassAssumes
_grepClassAssumes :: [RInstance t] -> [(Located F.Symbol, t)]
_grepClassAssumes :: forall t. [RInstance t] -> [(LocSymbol, t)]
_grepClassAssumes  = (RInstance t -> [(LocSymbol, t)])
-> [RInstance t] -> [(LocSymbol, t)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RInstance t -> [(LocSymbol, t)]
forall {b}. RInstance b -> [(LocSymbol, b)]
go
  where
    go :: RInstance b -> [(LocSymbol, b)]
go    RInstance b
xts              = ((LocSymbol, RISig b) -> Maybe (LocSymbol, b))
-> [(LocSymbol, RISig b)] -> [(LocSymbol, b)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (LocSymbol, RISig b) -> Maybe (LocSymbol, b)
forall {f :: * -> *} {b}.
Functor f =>
(f Symbol, RISig b) -> Maybe (f Symbol, b)
goOne (RInstance b -> [(LocSymbol, RISig b)]
forall t. RInstance t -> [(LocSymbol, RISig t)]
risigs RInstance b
xts)
    goOne :: (f Symbol, RISig b) -> Maybe (f Symbol, b)
goOne (f Symbol
x, RIAssumed b
t) = (f Symbol, b) -> Maybe (f Symbol, b)
forall a. a -> Maybe a
Just ((Symbol -> Symbol) -> f Symbol -> f Symbol
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> (Symbol -> [Char]) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
".$c" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ) ([Char] -> [Char]) -> (Symbol -> [Char]) -> Symbol -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
F.symbolString) f Symbol
x, b
t)
    goOne (f Symbol
_, RISig b
_)     = Maybe (f Symbol, b)
forall a. Maybe a
Nothing

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

makeNewTypes :: Bare.Env -> Bare.SigEnv -> [(ModName, Ms.BareSpec)] ->
                Bare.Lookup [(Ghc.TyCon, LocSpecType)]
makeNewTypes :: Env
-> SigEnv
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec (Located BareType) LocSymbol)]
specs = do
  ([[(TyCon, LocSpecType)]] -> [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
-> Lookup [(TyCon, LocSpecType)]
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(TyCon, LocSpecType)]] -> [(TyCon, LocSpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Either [Error] [[(TyCon, LocSpecType)]]
 -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
-> Lookup [(TyCon, LocSpecType)]
forall a b. (a -> b) -> a -> b
$
    [(ModName, DataDecl)]
-> ((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, DataDecl)]
nameDecls (((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
 -> Either [Error] [[(TyCon, LocSpecType)]])
-> ((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
forall a b. (a -> b) -> a -> b
$ (ModName -> DataDecl -> Lookup [(TyCon, LocSpecType)])
-> (ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Env
-> SigEnv -> ModName -> DataDecl -> Lookup [(TyCon, LocSpecType)]
makeNewType Env
env SigEnv
sigEnv)
  where
    nameDecls :: [(ModName, DataDecl)]
nameDecls = [(ModName
name, DataDecl
d) | (ModName
name, Spec (Located BareType) LocSymbol
spec) <- [(ModName, Spec (Located BareType) LocSymbol)]
specs, DataDecl
d <- Spec (Located BareType) LocSymbol -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.newtyDecls Spec (Located BareType) LocSymbol
spec]

makeNewType :: Bare.Env -> Bare.SigEnv -> ModName -> DataDecl ->
               Bare.Lookup [(Ghc.TyCon, LocSpecType)]
makeNewType :: Env
-> SigEnv -> ModName -> DataDecl -> Lookup [(TyCon, LocSpecType)]
makeNewType Env
env SigEnv
sigEnv ModName
name DataDecl
d = do
  Maybe TyCon
tcMb <- Env -> ModName -> [Char] -> DataName -> Lookup (Maybe TyCon)
Bare.lookupGhcDnTyCon Env
env ModName
name [Char]
"makeNewType" DataName
tcName
  case Maybe TyCon
tcMb of
    Just TyCon
tc -> [(TyCon, LocSpecType)] -> Lookup [(TyCon, LocSpecType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyCon
tc, LocSpecType
lst)]
    Maybe TyCon
_       -> [(TyCon, LocSpecType)] -> Lookup [(TyCon, LocSpecType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  where
    tcName :: DataName
tcName                    = DataDecl -> DataName
tycName DataDecl
d
    lst :: LocSpecType
lst                       = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV Located BareType
bt
    bt :: Located BareType
bt                        = DataName -> SourcePos -> [DataCtor] -> Located BareType
forall {a}.
PPrint a =>
a -> SourcePos -> [DataCtor] -> Located BareType
getTy DataName
tcName (DataDecl -> SourcePos
tycSrcPos DataDecl
d) ([DataCtor] -> Maybe [DataCtor] -> [DataCtor]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] (DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
d))
    getTy :: a -> SourcePos -> [DataCtor] -> Located BareType
getTy a
_ SourcePos
l [DataCtor
c]
      | [(Symbol
_, BareType
t)] <- DataCtor -> [(Symbol, BareType)]
dcFields DataCtor
c = SourcePos -> SourcePos -> BareType -> Located BareType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l BareType
t
    getTy a
n SourcePos
l [DataCtor]
_                = UserError -> Located BareType
forall a e. Exception e => e -> a
Ex.throw (a -> SourcePos -> UserError
forall {a}. PPrint a => a -> SourcePos -> UserError
mkErr a
n SourcePos
l)
    mkErr :: a -> SourcePos -> UserError
mkErr a
n SourcePos
l                  = SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> TError t
ErrOther (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (Doc
"Bad new type declaration:" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PPrint a => a -> Doc
F.pprint a
n) :: UserError

------------------------------------------------------------------------------------------
makeSpecData :: GhcSrc -> Bare.Env -> Bare.SigEnv -> Bare.MeasEnv -> GhcSpecSig -> Bare.ModSpecs
             -> GhcSpecData
------------------------------------------------------------------------------------------
makeSpecData :: GhcSrc
-> Env
-> SigEnv
-> MeasEnv
-> GhcSpecSig
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> GhcSpecData
makeSpecData GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
sig HashMap ModName (Spec (Located BareType) LocSymbol)
specs = SpData
  { gsCtors :: [(TyVar, LocSpecType)]
gsCtors      = [Char] -> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"GS-CTORS"
                   [ (TyVar
x, if Bool
allowTC then LocSpecType
t else LocSpecType
tt)
                       | (TyVar
x, LocSpecType
t) <- MeasEnv -> [(TyVar, LocSpecType)]
Bare.meDataCons MeasEnv
measEnv
                       , let tt :: LocSpecType
tt  = Bool
-> SigEnv -> ModName -> PlugTV TyVar -> LocSpecType -> LocSpecType
Bare.plugHoles (Config -> Bool
typeclass (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env) SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.LqTV TyVar
x) LocSpecType
t
                   ]
  , gsMeas :: [(Symbol, LocSpecType)]
gsMeas       = [ (Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, RRType Reft -> SpecType
forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType (RRType Reft -> SpecType) -> Located (RRType Reft) -> LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located (RRType Reft)
t) | (Symbol
x, Located (RRType Reft)
t) <- [(Symbol, Located (RRType Reft))]
measVars ]
  , gsMeasures :: [Measure SpecType DataCon]
gsMeasures   = Env
-> ModName -> Measure SpecType DataCon -> Measure SpecType DataCon
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name (Measure SpecType DataCon -> Measure SpecType DataCon)
-> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Measure SpecType DataCon]
ms1 [Measure SpecType DataCon]
-> [Measure SpecType DataCon] -> [Measure SpecType DataCon]
forall a. [a] -> [a] -> [a]
++ [Measure SpecType DataCon]
ms2)
  , gsInvariants :: [(Maybe TyVar, LocSpecType)]
gsInvariants = ((Maybe TyVar, LocSpecType) -> SourcePos)
-> [(Maybe TyVar, LocSpecType)] -> [(Maybe TyVar, LocSpecType)]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (LocSpecType -> SourcePos
forall a. Located a -> SourcePos
F.loc (LocSpecType -> SourcePos)
-> ((Maybe TyVar, LocSpecType) -> LocSpecType)
-> (Maybe TyVar, LocSpecType)
-> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe TyVar, LocSpecType) -> LocSpecType
forall a b. (a, b) -> b
snd) [(Maybe TyVar, LocSpecType)]
invs
  , gsIaliases :: [(LocSpecType, LocSpecType)]
gsIaliases   = ((ModName, Spec (Located BareType) LocSymbol)
 -> [(LocSpecType, LocSpecType)])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(LocSpecType, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
  , gsUnsorted :: [UnSortedExpr]
gsUnsorted   = [UnSortedExpr]
usI [UnSortedExpr] -> [UnSortedExpr] -> [UnSortedExpr]
forall a. [a] -> [a] -> [a]
++ (Measure (Located BareType) LocSymbol -> [UnSortedExpr])
-> [Measure (Located BareType) LocSymbol] -> [UnSortedExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Measure (Located BareType) LocSymbol -> [UnSortedExpr]
forall ty ctor. Measure ty ctor -> [UnSortedExpr]
msUnSorted ((Spec (Located BareType) LocSymbol
 -> [Measure (Located BareType) LocSymbol])
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> [Measure (Located BareType) LocSymbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Spec (Located BareType) LocSymbol
-> [Measure (Located BareType) LocSymbol]
forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
  }
  where
    allowTC :: Bool
allowTC      = Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)
    measVars :: [(Symbol, Located (RRType Reft))]
measVars     = MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms      MeasEnv
measEnv -- ms'
                [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. [a] -> [a] -> [a]
++ MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meClassSyms MeasEnv
measEnv -- cms'
                [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
-> [(Symbol, Located (RRType Reft))]
forall a. [a] -> [a] -> [a]
++ Env -> [(Symbol, Located (RRType Reft))]
forall r. Monoid r => Env -> [(Symbol, Located (RRType r))]
Bare.varMeasures Env
env
    measuresSp :: MSpec SpecType DataCon
measuresSp   = MeasEnv -> MSpec SpecType DataCon
Bare.meMeasureSpec MeasEnv
measEnv
    ms1 :: [Measure SpecType DataCon]
ms1          = HashMap LocSymbol (Measure SpecType DataCon)
-> [Measure SpecType DataCon]
forall k v. HashMap k v -> [v]
M.elems (MSpec SpecType DataCon
-> HashMap LocSymbol (Measure SpecType DataCon)
forall ty ctor.
MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
Ms.measMap MSpec SpecType DataCon
measuresSp)
    ms2 :: [Measure SpecType DataCon]
ms2          = MSpec SpecType DataCon -> [Measure SpecType DataCon]
forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
Ms.imeas   MSpec SpecType DataCon
measuresSp
    mySpec :: Spec (Located BareType) LocSymbol
mySpec       = Spec (Located BareType) LocSymbol
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Spec (Located BareType) LocSymbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Spec (Located BareType) LocSymbol
forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
    name :: ModName
name         = GhcSrc -> ModName
_giTargetMod      GhcSrc
src
    ([(Maybe TyVar, LocSpecType)]
minvs,[UnSortedExpr]
usI)  = Env
-> ModName
-> GhcSpecSig
-> Spec (Located BareType) LocSymbol
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants Env
env ModName
name GhcSpecSig
sig Spec (Located BareType) LocSymbol
mySpec
    invs :: [(Maybe TyVar, LocSpecType)]
invs         = [(Maybe TyVar, LocSpecType)]
minvs [(Maybe TyVar, LocSpecType)]
-> [(Maybe TyVar, LocSpecType)] -> [(Maybe TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ ((ModName, Spec (Located BareType) LocSymbol)
 -> [(Maybe TyVar, LocSpecType)])
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(Maybe TyVar, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(Maybe TyVar, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)

makeIAliases :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(LocSpecType, LocSpecType)]
makeIAliases :: Env
-> SigEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv (ModName
name, Spec (Located BareType) LocSymbol
spec)
  = [ (LocSpecType, LocSpecType)
z | Right (LocSpecType, LocSpecType)
z <- (Located BareType, Located BareType)
-> Either [Error] (LocSpecType, LocSpecType)
mkIA ((Located BareType, Located BareType)
 -> Either [Error] (LocSpecType, LocSpecType))
-> [(Located BareType, Located BareType)]
-> [Either [Error] (LocSpecType, LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec (Located BareType) LocSymbol
-> [(Located BareType, Located BareType)]
forall ty bndr. Spec ty bndr -> [(ty, ty)]
Ms.ialiases Spec (Located BareType) LocSymbol
spec ]
  where
    -- mkIA :: (LocBareType, LocBareType) -> Either _ (LocSpecType, LocSpecType)
    mkIA :: (Located BareType, Located BareType)
-> Either [Error] (LocSpecType, LocSpecType)
mkIA (Located BareType
t1, Located BareType
t2) = (,) (LocSpecType -> LocSpecType -> (LocSpecType, LocSpecType))
-> Either [Error] LocSpecType
-> Either [Error] (LocSpecType -> (LocSpecType, LocSpecType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located BareType -> Either [Error] LocSpecType
mkI' Located BareType
t1 Either [Error] (LocSpecType -> (LocSpecType, LocSpecType))
-> Either [Error] LocSpecType
-> Either [Error] (LocSpecType, LocSpecType)
forall a b.
Either [Error] (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Located BareType -> Either [Error] LocSpecType
mkI' Located BareType
t2
    mkI' :: Located BareType -> Either [Error] LocSpecType
mkI'          = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> Either [Error] LocSpecType
Bare.cookSpecTypeE Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV

makeInvariants :: Bare.Env -> Bare.SigEnv -> (ModName, Ms.BareSpec) -> [(Maybe Ghc.Var, Located SpecType)]
makeInvariants :: Env
-> SigEnv
-> (ModName, Spec (Located BareType) LocSymbol)
-> [(Maybe TyVar, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv (ModName
name, Spec (Located BareType) LocSymbol
spec) =
  [ (Maybe TyVar
forall a. Maybe a
Nothing, LocSpecType
t)
    | (Maybe LocSymbol
_, Located BareType
bt) <- Spec (Located BareType) LocSymbol
-> [(Maybe LocSymbol, Located BareType)]
forall ty bndr. Spec ty bndr -> [(Maybe LocSymbol, ty)]
Ms.invariants Spec (Located BareType) LocSymbol
spec
    , Env -> ModName -> Located BareType -> Bool
Bare.knownGhcType Env
env ModName
name Located BareType
bt
    , let t :: LocSpecType
t = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV Located BareType
bt
  ] [(Maybe TyVar, LocSpecType)]
-> [(Maybe TyVar, LocSpecType)] -> [(Maybe TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++
  [[(Maybe TyVar, LocSpecType)]] -> [(Maybe TyVar, LocSpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Maybe TyVar
forall a. Maybe a
Nothing,) (LocSpecType -> (Maybe TyVar, LocSpecType))
-> (LocSpecType -> LocSpecType)
-> LocSpecType
-> (Maybe TyVar, LocSpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> LocSpecType -> LocSpecType
makeSizeInv LocSymbol
l (LocSpecType -> (Maybe TyVar, LocSpecType))
-> [LocSpecType] -> [(Maybe TyVar, LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>  [LocSpecType]
ts
    | ([Located BareType]
bts, LocSymbol
l) <- Spec (Located BareType) LocSymbol
-> [([Located BareType], LocSymbol)]
forall ty bndr. Spec ty bndr -> [([ty], LocSymbol)]
Ms.dsize Spec (Located BareType) LocSymbol
spec
    , (Located BareType -> Bool) -> [Located BareType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Env -> ModName -> Located BareType -> Bool
Bare.knownGhcType Env
env ModName
name) [Located BareType]
bts
    , let ts :: [LocSpecType]
ts = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV (Located BareType -> LocSpecType)
-> [Located BareType] -> [LocSpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BareType]
bts
  ]

makeSizeInv :: F.LocSymbol -> Located SpecType -> Located SpecType
makeSizeInv :: LocSymbol -> LocSpecType -> LocSpecType
makeSizeInv LocSymbol
s LocSpecType
lst = LocSpecType
lst{val = go (val lst)}
  where go :: RType c tv RReft -> RType c tv RReft
go (RApp c
c [RType c tv RReft]
ts [RTProp c tv RReft]
rs RReft
r) = c
-> [RType c tv RReft]
-> [RTProp c tv RReft]
-> RReft
-> RType c tv RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv RReft]
ts [RTProp c tv RReft]
rs (RReft
r RReft -> RReft -> RReft
forall r. Reftable r => r -> r -> r
`meet` RReft
nat)
        go (RAllT RTVU c tv
a RType c tv RReft
t RReft
r)    = RTVU c tv -> RType c tv RReft -> RReft -> RType c tv RReft
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU c tv
a (RType c tv RReft -> RType c tv RReft
go RType c tv RReft
t) RReft
r
        go RType c tv RReft
t = RType c tv RReft
t
        nat :: RReft
nat  = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
Reft (Symbol
vv_, Brel -> Expr -> Expr -> Expr
PAtom Brel
Le (Constant -> Expr
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Constant
I Integer
0) (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s) (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
vv_))))
                       Predicate
forall a. Monoid a => a
mempty

makeMeasureInvariants :: Bare.Env -> ModName -> GhcSpecSig -> Ms.BareSpec
                      -> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants :: Env
-> ModName
-> GhcSpecSig
-> Spec (Located BareType) LocSymbol
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants Env
env ModName
name GhcSpecSig
sig Spec (Located BareType) LocSymbol
mySpec
  = ([Maybe UnSortedExpr] -> [UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
forall b c d. (b -> c) -> (d, b) -> (d, c)
mapSnd [Maybe UnSortedExpr] -> [UnSortedExpr]
forall a. [Maybe a] -> [a]
Mb.catMaybes (([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
 -> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr]))
-> ([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
forall a b. (a -> b) -> a -> b
$
    [((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)]
-> ([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip (Env
-> ModName
-> (LocSymbol, (TyVar, LocSpecType))
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv Env
env ModName
name ((LocSymbol, (TyVar, LocSpecType))
 -> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr))
-> [(LocSymbol, (TyVar, LocSpecType))]
-> [((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol
x, (TyVar
y, LocSpecType
ty)) | LocSymbol
x <- [LocSymbol]
xs, (TyVar
y, LocSpecType
ty) <- [(TyVar, LocSpecType)]
sigs
                                         , Symbol -> TyVar -> Bool
isSymbolOfVar (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x) TyVar
y ])
  where
    sigs :: [(TyVar, LocSpecType)]
sigs = GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
sig
    xs :: [LocSymbol]
xs   = HashSet LocSymbol -> [LocSymbol]
forall a. HashSet a -> [a]
S.toList (Spec (Located BareType) LocSymbol -> HashSet LocSymbol
forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.hmeas  Spec (Located BareType) LocSymbol
mySpec)

isSymbolOfVar :: Symbol -> Ghc.Var -> Bool
isSymbolOfVar :: Symbol -> TyVar -> Bool
isSymbolOfVar Symbol
x TyVar
v = Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Symbol
symbol' TyVar
v
  where
    symbol' :: Ghc.Var -> Symbol
    symbol' :: TyVar -> Symbol
symbol' = Symbol -> Symbol
GM.dropModuleNames (Symbol -> Symbol) -> (TyVar -> Symbol) -> TyVar -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Name -> Symbol) -> (TyVar -> Name) -> TyVar -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Name
forall a. NamedThing a => a -> Name
Ghc.getName

measureTypeToInv :: Bare.Env -> ModName -> (LocSymbol, (Ghc.Var, LocSpecType)) -> ((Maybe Ghc.Var, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv :: Env
-> ModName
-> (LocSymbol, (TyVar, LocSpecType))
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv Env
env ModName
name (LocSymbol
x, (TyVar
v, LocSpecType
t))
  = [Char]
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
"measureTypeToInv" ((TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just TyVar
v, LocSpecType
t {val = Bare.qualifyTop env name (F.loc x) mtype}), Maybe UnSortedExpr
usorted)
  where
    trep :: RTypeRep RTyCon RTyVar RReft
trep = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
t)
    rts :: [SpecType]
rts  = RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
trep
    args :: [Symbol]
args = RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep
    res :: SpecType
res  = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res   RTypeRep RTyCon RTyVar RReft
trep
    z :: Symbol
z    = [Symbol] -> Symbol
forall a. HasCallStack => [a] -> a
last [Symbol]
args
    tz :: SpecType
tz   = [SpecType] -> SpecType
forall a. HasCallStack => [a] -> a
last [SpecType]
rts
    usorted :: Maybe UnSortedExpr
usorted = if SpecType -> Bool
forall {c} {tv} {r}. RType c tv r -> Bool
isSimpleADT SpecType
tz then Maybe UnSortedExpr
forall a. Maybe a
Nothing else (Symbol -> [Symbol]) -> (Symbol, Expr) -> UnSortedExpr
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[]) ((Symbol, Expr) -> UnSortedExpr)
-> Maybe (Symbol, Expr) -> Maybe UnSortedExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v) Symbol
z SpecType
tz SpecType
res
    mtype :: SpecType
mtype
      | [SpecType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecType]
rts
      = UserError -> SpecType
forall a. UserError -> a
uError (UserError -> SpecType) -> UserError -> SpecType
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Doc -> UserError
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSpecType -> SourcePos
forall a. Located a -> SourcePos
loc LocSpecType
t) (LocSymbol -> Doc
forall a. PPrint a => a -> Doc
pprint LocSymbol
x) Doc
"Measure has no arguments!"
      | Bool
otherwise
      = LocSymbol -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant LocSymbol
x Symbol
z SpecType
tz SpecType
res
    isSimpleADT :: RType c tv r -> Bool
isSimpleADT (RApp c
_ [RType c tv r]
ts [RTProp c tv r]
_ r
_) = (RType c tv r -> Bool) -> [RType c tv r] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all RType c tv r -> Bool
forall {c} {tv} {r}. RType c tv r -> Bool
isRVar [RType c tv r]
ts
    isSimpleADT RType c tv r
_               = Bool
False

mkInvariant :: LocSymbol -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant :: LocSymbol -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant LocSymbol
x Symbol
z SpecType
t SpecType
tr = SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen (RReft -> RReft
forall r. Reftable r => r -> r
top (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t) (Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft Reft
reft' Predicate
forall a. Monoid a => a
mempty)
      where
        reft' :: Reft
reft' = Reft -> ((Symbol, Expr) -> Reft) -> Maybe (Symbol, Expr) -> Reft
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Reft
forall a. Monoid a => a
mempty (Symbol, Expr) -> Reft
Reft Maybe (Symbol, Expr)
mreft
        mreft :: Maybe (Symbol, Expr)
mreft = LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft LocSymbol
x Symbol
z SpecType
t SpecType
tr


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


-- REBARE: formerly, makeGhcSpec3
-------------------------------------------------------------------------------------------
makeSpecName :: Bare.Env -> Bare.TycEnv -> Bare.MeasEnv -> ModName -> GhcSpecNames
-------------------------------------------------------------------------------------------
makeSpecName :: Env -> TycEnv -> MeasEnv -> ModName -> GhcSpecNames
makeSpecName Env
env TycEnv
tycEnv MeasEnv
measEnv ModName
name = SpNames
  { gsFreeSyms :: [(Symbol, TyVar)]
gsFreeSyms = Env -> [(Symbol, TyVar)]
Bare.reSyms Env
env
  , gsDconsP :: [Located DataCon]
gsDconsP   = [ DataConP -> DataCon -> Located DataCon
forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dc (DataConP -> DataCon
dcpCon DataConP
dc) | DataConP
dc <- [DataConP]
datacons [DataConP] -> [DataConP] -> [DataConP]
forall a. [a] -> [a] -> [a]
++ [DataConP]
cls ]
  , gsTconsP :: [TyConP]
gsTconsP   = Env -> ModName -> TyConP -> TyConP
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name (TyConP -> TyConP) -> [TyConP] -> [TyConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyConP]
tycons
  -- , gsLits = mempty                                              -- TODO-REBARE, redundant with gsMeas
  , gsTcEmbeds :: TCEmb TyCon
gsTcEmbeds = TycEnv -> TCEmb TyCon
Bare.tcEmbs     TycEnv
tycEnv
  , gsADTs :: [DataDecl]
gsADTs     = TycEnv -> [DataDecl]
Bare.tcAdts     TycEnv
tycEnv
  , gsTyconEnv :: TyConMap
gsTyconEnv = TycEnv -> TyConMap
Bare.tcTyConMap TycEnv
tycEnv
  }
  where
    datacons, cls :: [DataConP]
    datacons :: [DataConP]
datacons   = TycEnv -> [DataConP]
Bare.tcDataCons TycEnv
tycEnv
    cls :: [DataConP]
cls        = [Char] -> [DataConP] -> [DataConP]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"meClasses" ([DataConP] -> [DataConP]) -> [DataConP] -> [DataConP]
forall a b. (a -> b) -> a -> b
$ MeasEnv -> [DataConP]
Bare.meClasses MeasEnv
measEnv
    tycons :: [TyConP]
tycons     = TycEnv -> [TyConP]
Bare.tcTyCons   TycEnv
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 :: Config
-> ModName
-> Env
-> TCEmb TyCon
-> Spec (Located BareType) LocSymbol
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0 Config
cfg ModName
myName Env
env TCEmb TyCon
embs Spec (Located BareType) LocSymbol
mySpec HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs = (Diagnostics
diag0 Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Diagnostics
diag1, [Located DataConP]
datacons, Bare.TycEnv
  { tcTyCons :: [TyConP]
tcTyCons      = [TyConP]
tycons
  , tcDataCons :: [DataConP]
tcDataCons    = [DataConP]
forall a. Monoid a => a
mempty -- val <$> datacons
  , tcSelMeasures :: [Measure SpecType DataCon]
tcSelMeasures = [Measure SpecType DataCon]
dcSelectors
  , tcSelVars :: [(TyVar, LocSpecType)]
tcSelVars     = [(TyVar, LocSpecType)]
forall a. Monoid a => a
mempty -- recSelectors
  , tcTyConMap :: TyConMap
tcTyConMap    = TyConMap
tyi
  , tcAdts :: [DataDecl]
tcAdts        = [DataDecl]
adts
  , tcDataConMap :: DataConMap
tcDataConMap  = DataConMap
dm
  , tcEmbs :: TCEmb TyCon
tcEmbs        = TCEmb TyCon
embs
  , tcName :: ModName
tcName        = ModName
myName
  })
  where
    ([(ModName, TyConP, Maybe DataPropDecl)]
tcDds, [[Located DataConP]]
dcs)   = ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
conTys
    (Diagnostics
diag0, ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
conTys) = Lookup
  ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> (Diagnostics,
    ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup
   ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
 -> (Diagnostics,
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])))
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> (Diagnostics,
    ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
forall a b. (a -> b) -> a -> b
$ ModName
-> Env
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes ModName
myName Env
env [(ModName, Spec (Located BareType) LocSymbol)]
specs
    specs :: [(ModName, Spec (Located BareType) LocSymbol)]
specs         = (ModName
myName, Spec (Located BareType) LocSymbol
mySpec) (ModName, Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall a. a -> [a] -> [a]
: HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
iSpecs
    tcs :: [TyConP]
tcs           = (ModName, TyConP, Maybe DataPropDecl) -> TyConP
forall a b c. (a, b, c) -> b
Misc.snd3 ((ModName, TyConP, Maybe DataPropDecl) -> TyConP)
-> [(ModName, TyConP, Maybe DataPropDecl)] -> [TyConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, TyConP, Maybe DataPropDecl)]
tcDds
    tyi :: TyConMap
tyi           = Env -> ModName -> TyConMap -> TyConMap
forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
myName (TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap
makeTyConInfo TCEmb TyCon
embs [TyCon]
fiTcs [TyConP]
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 :: [TyConP]
tycons        = [TyConP]
tcs [TyConP] -> [TyConP] -> [TyConP]
forall a. [a] -> [a] -> [a]
++ Env -> ModName -> [TyConP]
knownWiredTyCons Env
env ModName
myName
    datacons :: [Located DataConP]
datacons      = Bool
-> TCEmb TyCon -> TyConMap -> Located DataConP -> Located DataConP
Bare.makePluggedDataCon (Config -> Bool
typeclass Config
cfg) TCEmb TyCon
embs TyConMap
tyi (Located DataConP -> Located DataConP)
-> [Located DataConP] -> [Located DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([[Located DataConP]] -> [Located DataConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Located DataConP]]
dcs [Located DataConP] -> [Located DataConP] -> [Located DataConP]
forall a. [a] -> [a] -> [a]
++ Env -> ModName -> [Located DataConP]
knownWiredDataCons Env
env ModName
myName)
    tds :: [(ModName, TyCon, DataPropDecl)]
tds           = [(ModName
name, TyConP -> TyCon
tcpCon TyConP
tcp, DataPropDecl
dd) | (ModName
name, TyConP
tcp, Just DataPropDecl
dd) <- [(ModName, TyConP, Maybe DataPropDecl)]
tcDds]
    (Diagnostics
diag1, [DataDecl]
adts) = Config
-> TCEmb TyCon
-> ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [Located DataConP]
-> (Diagnostics, [DataDecl])
Bare.makeDataDecls Config
cfg TCEmb TyCon
embs ModName
myName [(ModName, TyCon, DataPropDecl)]
tds       [Located DataConP]
datacons
    dm :: DataConMap
dm            = [DataDecl] -> DataConMap
Bare.dataConMap [DataDecl]
adts
    dcSelectors :: [Measure SpecType DataCon]
dcSelectors   = (Located DataConP -> [Measure SpecType DataCon])
-> [Located DataConP] -> [Measure SpecType DataCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Config
-> DataConMap -> Located DataConP -> [Measure SpecType DataCon]
Bare.makeMeasureSelectors Config
cfg DataConMap
dm) (if Config -> Bool
reflection Config
cfg then Located DataConP
charDataConLocated DataConP -> [Located DataConP] -> [Located DataConP]
forall a. a -> [a] -> [a]
:[Located DataConP]
datacons else [Located DataConP]
datacons)
    fiTcs :: [TyCon]
fiTcs         = GhcSrc -> [TyCon]
_gsFiTcs (Env -> GhcSrc
Bare.reSrc Env
env)



makeTycEnv1 ::
     ModName
  -> Bare.Env
  -> (Bare.TycEnv, [Located DataConP])
  -> (Ghc.CoreExpr -> F.Expr)
  -> (Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr)
  -> Ghc.TcRn Bare.TycEnv
makeTycEnv1 :: ModName
-> Env
-> (TycEnv, [Located DataConP])
-> (CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> TcRn TycEnv
makeTycEnv1 ModName
myName Env
env (TycEnv
tycEnv, [Located DataConP]
datacons) CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier = do
  -- fst for selector generation, snd for dataconsig generation
  [Located (DataConP, DataConP)]
lclassdcs <- [Located DataConP]
-> (Located DataConP
    -> IOEnv (Env TcGblEnv TcLclEnv) (Located (DataConP, DataConP)))
-> IOEnv (Env TcGblEnv TcLclEnv) [Located (DataConP, DataConP)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Located DataConP]
classdcs ((Located DataConP
  -> IOEnv (Env TcGblEnv TcLclEnv) (Located (DataConP, DataConP)))
 -> IOEnv (Env TcGblEnv TcLclEnv) [Located (DataConP, DataConP)])
-> (Located DataConP
    -> IOEnv (Env TcGblEnv TcLclEnv) (Located (DataConP, DataConP)))
-> IOEnv (Env TcGblEnv TcLclEnv) [Located (DataConP, DataConP)]
forall a b. (a -> b) -> a -> b
$ (DataConP -> IOEnv (Env TcGblEnv TcLclEnv) (DataConP, DataConP))
-> Located DataConP
-> IOEnv (Env TcGblEnv TcLclEnv) (Located (DataConP, DataConP))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> IOEnv (Env TcGblEnv TcLclEnv) (DataConP, DataConP)
Bare.elaborateClassDcp CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier)
  let recSelectors :: [(TyVar, LocSpecType)]
recSelectors = Env -> ModName -> [Located DataConP] -> [(TyVar, LocSpecType)]
Bare.makeRecordSelectorSigs Env
env ModName
myName ([Located DataConP]
dcs [Located DataConP] -> [Located DataConP] -> [Located DataConP]
forall a. [a] -> [a] -> [a]
++ ((Located (DataConP, DataConP) -> Located DataConP)
-> [Located (DataConP, DataConP)] -> [Located DataConP]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Located (DataConP, DataConP) -> Located DataConP)
 -> [Located (DataConP, DataConP)] -> [Located DataConP])
-> (((DataConP, DataConP) -> DataConP)
    -> Located (DataConP, DataConP) -> Located DataConP)
-> ((DataConP, DataConP) -> DataConP)
-> [Located (DataConP, DataConP)]
-> [Located DataConP]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((DataConP, DataConP) -> DataConP)
-> Located (DataConP, DataConP) -> Located DataConP
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (DataConP, DataConP) -> DataConP
forall a b. (a, b) -> b
snd [Located (DataConP, DataConP)]
lclassdcs)
  TycEnv -> TcRn TycEnv
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TycEnv -> TcRn TycEnv) -> TycEnv -> TcRn TycEnv
forall a b. (a -> b) -> a -> b
$
    TycEnv
tycEnv {Bare.tcSelVars = recSelectors, Bare.tcDataCons = F.val <$> ((fmap . fmap) fst lclassdcs ++ dcs )}
  where
    ([Located DataConP]
classdcs, [Located DataConP]
dcs) =
      (Located DataConP -> Bool)
-> [Located DataConP] -> ([Located DataConP], [Located DataConP])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition
        (TyCon -> Bool
Ghc.isClassTyCon (TyCon -> Bool)
-> (Located DataConP -> TyCon) -> Located DataConP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> TyCon
Ghc.dataConTyCon (DataCon -> TyCon)
-> (Located DataConP -> DataCon) -> Located DataConP -> TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon (DataConP -> DataCon)
-> (Located DataConP -> DataConP) -> Located DataConP -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located DataConP -> DataConP
forall a. Located a -> a
F.val) [Located DataConP]
datacons


knownWiredDataCons :: Bare.Env -> ModName -> [Located DataConP]
knownWiredDataCons :: Env -> ModName -> [Located DataConP]
knownWiredDataCons Env
env ModName
name = (Located DataConP -> Bool)
-> [Located DataConP] -> [Located DataConP]
forall a. (a -> Bool) -> [a] -> [a]
filter Located DataConP -> Bool
isKnown [Located DataConP]
wiredDataCons
  where
    isKnown :: Located DataConP -> Bool
isKnown                 = Env -> ModName -> LocSymbol -> Bool
Bare.knownGhcDataCon Env
env ModName
name (LocSymbol -> Bool)
-> (Located DataConP -> LocSymbol) -> Located DataConP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol (DataCon -> LocSymbol)
-> (Located DataConP -> DataCon) -> Located DataConP -> LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon (DataConP -> DataCon)
-> (Located DataConP -> DataConP) -> Located DataConP -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located DataConP -> DataConP
forall a. Located a -> a
val

knownWiredTyCons :: Bare.Env -> ModName -> [TyConP]
knownWiredTyCons :: Env -> ModName -> [TyConP]
knownWiredTyCons Env
env ModName
name = (TyConP -> Bool) -> [TyConP] -> [TyConP]
forall a. (a -> Bool) -> [a] -> [a]
filter TyConP -> Bool
isKnown [TyConP]
wiredTyCons
  where
    isKnown :: TyConP -> Bool
isKnown               = Env -> ModName -> LocSymbol -> Bool
Bare.knownGhcTyCon Env
env ModName
name (LocSymbol -> Bool) -> (TyConP -> LocSymbol) -> TyConP -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol (TyCon -> LocSymbol) -> (TyConP -> TyCon) -> TyConP -> LocSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConP -> TyCon
tcpCon


-- REBARE: formerly, makeGhcCHOP2
-------------------------------------------------------------------------------------------
makeMeasEnv :: Bare.Env -> Bare.TycEnv -> Bare.SigEnv -> Bare.ModSpecs ->
               Bare.Lookup Bare.MeasEnv
-------------------------------------------------------------------------------------------
makeMeasEnv :: Env
-> TycEnv
-> SigEnv
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv HashMap ModName (Spec (Located BareType) LocSymbol)
specs = do
  [(Class, [(ModName, TyVar, LocSpecType)])]
laws        <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.makeCLaws Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  ([DataConP]
cls, [(ModName, TyVar, LocSpecType)]
mts)  <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec (Located BareType) LocSymbol)
-> Lookup ([DataConP], [(ModName, TyVar, LocSpecType)])
Bare.makeClasses        Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec (Located BareType) LocSymbol)
specs
  let dms :: [(ModName, TyVar, LocSpecType)]
dms      = Env
-> [(ModName, TyVar, LocSpecType)]
-> [(ModName, TyVar, LocSpecType)]
Bare.makeDefaultMethods Env
env [(ModName, TyVar, LocSpecType)]
mts
  [MSpec SpecType DataCon]
measures0   <- ((ModName, Spec (Located BareType) LocSymbol)
 -> Either [Error] (MSpec SpecType DataCon))
-> [(ModName, Spec (Located BareType) LocSymbol)]
-> Either [Error] [MSpec SpecType DataCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env
-> SigEnv
-> ModName
-> (ModName, Spec (Located BareType) LocSymbol)
-> Either [Error] (MSpec SpecType DataCon)
Bare.makeMeasureSpec Env
env SigEnv
sigEnv ModName
name) (HashMap ModName (Spec (Located BareType) LocSymbol)
-> [(ModName, Spec (Located BareType) LocSymbol)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec (Located BareType) LocSymbol)
specs)
  let measures :: MSpec SpecType DataCon
measures = [MSpec SpecType DataCon] -> MSpec SpecType DataCon
forall a. Monoid a => [a] -> a
mconcat ([Measure SpecType DataCon] -> MSpec SpecType DataCon
forall ctor ty. Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
Ms.mkMSpec' [Measure SpecType DataCon]
dcSelectors MSpec SpecType DataCon
-> [MSpec SpecType DataCon] -> [MSpec SpecType DataCon]
forall a. a -> [a] -> [a]
: [MSpec SpecType DataCon]
measures0)
  let ([(TyVar, SpecType)]
cs, [(LocSymbol, RRType Reft)]
ms) = Bool
-> MSpec SpecType DataCon
-> ([(TyVar, SpecType)], [(LocSymbol, RRType Reft)])
Bare.makeMeasureSpec'  (Config -> Bool
typeclass (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)   MSpec SpecType DataCon
measures
  let cms :: [(LocSymbol, CMeasure (RRType Reft))]
cms      = MSpec SpecType DataCon -> [(LocSymbol, CMeasure (RRType Reft))]
forall c tv r2 t.
MSpec (RType c tv (UReft r2)) t
-> [(LocSymbol, CMeasure (RType c tv r2))]
Bare.makeClassMeasureSpec MSpec SpecType DataCon
measures
  let cms' :: [(Symbol, Located (RRType Reft))]
cms'     = [ (Symbol
x, SourcePos -> SourcePos -> RRType Reft -> Located (RRType Reft)
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (RRType Reft -> Located (RRType Reft))
-> RRType Reft -> Located (RRType Reft)
forall a b. (a -> b) -> a -> b
$ CMeasure (RRType Reft) -> RRType Reft
forall ty. CMeasure ty -> ty
cSort CMeasure (RRType Reft)
t)  | (Loc SourcePos
l SourcePos
l' Symbol
x, CMeasure (RRType Reft)
t) <- [(LocSymbol, CMeasure (RRType Reft))]
cms ]
  let ms' :: [(Symbol, Located (RRType Reft))]
ms'      = [ (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
lx, LocSymbol -> RRType Reft -> Located (RRType Reft)
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
lx RRType Reft
t) | (LocSymbol
lx, RRType Reft
t) <- [(LocSymbol, RRType Reft)]
ms
                                            , Maybe (Located (RRType Reft)) -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (Symbol
-> [(Symbol, Located (RRType Reft))]
-> Maybe (Located (RRType Reft))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx) [(Symbol, Located (RRType Reft))]
cms') ]
  let cs' :: [(TyVar, LocSpecType)]
cs'      = [ (TyVar
v, TyVar -> SpecType -> LocSpecType
forall {b}. NamedThing b => b -> SpecType -> LocSpecType
txRefs TyVar
v SpecType
t) | (TyVar
v, SpecType
t) <- Bool
-> TCEmb TyCon
-> [(TyVar, SpecType)]
-> [DataConP]
-> [(TyVar, SpecType)]
Bare.meetDataConSpec (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)) TCEmb TyCon
embs [(TyVar, SpecType)]
cs ([DataConP]
datacons [DataConP] -> [DataConP] -> [DataConP]
forall a. [a] -> [a] -> [a]
++ [DataConP]
cls)]
  MeasEnv -> Lookup MeasEnv
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return Bare.MeasEnv
    { meMeasureSpec :: MSpec SpecType DataCon
meMeasureSpec = MSpec SpecType DataCon
measures
    , meClassSyms :: [(Symbol, Located (RRType Reft))]
meClassSyms   = [(Symbol, Located (RRType Reft))]
cms'
    , meSyms :: [(Symbol, Located (RRType Reft))]
meSyms        = [(Symbol, Located (RRType Reft))]
ms'
    , meDataCons :: [(TyVar, LocSpecType)]
meDataCons    = [(TyVar, LocSpecType)]
cs'
    , meClasses :: [DataConP]
meClasses     = [DataConP]
cls
    , meMethods :: [(ModName, TyVar, LocSpecType)]
meMethods     = [(ModName, TyVar, LocSpecType)]
mts [(ModName, TyVar, LocSpecType)]
-> [(ModName, TyVar, LocSpecType)]
-> [(ModName, TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [(ModName, TyVar, LocSpecType)]
dms
    , meCLaws :: [(Class, [(ModName, TyVar, LocSpecType)])]
meCLaws       = [(Class, [(ModName, TyVar, LocSpecType)])]
laws
    }
  where
    txRefs :: b -> SpecType -> LocSpecType
txRefs b
v SpecType
t    = TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs (SpecType
t SpecType -> Located b -> LocSpecType
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ b -> Located b
forall a. NamedThing a => a -> Located a
GM.locNamedThing b
v)
    tyi :: TyConMap
tyi           = TycEnv -> TyConMap
Bare.tcTyConMap    TycEnv
tycEnv
    dcSelectors :: [Measure SpecType DataCon]
dcSelectors   = TycEnv -> [Measure SpecType DataCon]
Bare.tcSelMeasures TycEnv
tycEnv
    datacons :: [DataConP]
datacons      = TycEnv -> [DataConP]
Bare.tcDataCons    TycEnv
tycEnv
    embs :: TCEmb TyCon
embs          = TycEnv -> TCEmb TyCon
Bare.tcEmbs        TycEnv
tycEnv
    name :: ModName
name          = TycEnv -> ModName
Bare.tcName        TycEnv
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 :: ModName
-> GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> Spec (Located BareType) LocSymbol
-> Spec (Located BareType) LocSymbol
makeLiftedSpec ModName
name GhcSrc
src Env
_env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
sig GhcSpecQual
qual BareRTEnv
myRTE Spec (Located BareType) LocSymbol
lSpec0 = Spec (Located BareType) LocSymbol
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 :: [(LocSymbol, Located BareType)]
myDCs         = [(LocSymbol
x,Located BareType
t) | (LocSymbol
x,Located BareType
t) <- [(TyVar, LocSpecType)] -> [(LocSymbol, Located BareType)]
forall {f :: * -> *}.
Functor f =>
[(TyVar, f SpecType)] -> [(LocSymbol, f BareType)]
mkSigs (GhcSpecData -> [(TyVar, LocSpecType)]
gsCtors GhcSpecData
sData)
                           , ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== (Symbol, Symbol) -> Symbol
forall a b. (a, b) -> a
fst (Symbol -> (Symbol, Symbol)
GM.splitModuleName (Symbol -> (Symbol, Symbol)) -> Symbol -> (Symbol, Symbol)
forall a b. (a -> b) -> a -> b
$ LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
x)]
    mkSigs :: [(TyVar, f SpecType)] -> [(LocSymbol, f BareType)]
mkSigs [(TyVar, f SpecType)]
xts    = [ (TyVar, f SpecType) -> (LocSymbol, f BareType)
forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (LocSymbol, f BareType)
toBare (TyVar
x, f SpecType
t) | (TyVar
x, f SpecType
t) <- [(TyVar, f SpecType)]
xts
                    ,  TyVar -> HashSet TyVar -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member TyVar
x HashSet TyVar
sigVars Bool -> Bool -> Bool
&& TargetSrc -> TyVar -> Bool
isExportedVar (GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src) TyVar
x
                    ]
    toBare :: (TyVar, f SpecType) -> (LocSymbol, f BareType)
toBare (TyVar
x, f SpecType
t) = (TyVar -> LocSymbol
varLocSym TyVar
x, SpecType -> BareType
Bare.specToBare (SpecType -> BareType) -> f SpecType -> f BareType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f SpecType
t)
    xbs :: [(LocSymbol, Located BareType)]
xbs           = (TyVar, LocSpecType) -> (LocSymbol, Located BareType)
forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (LocSymbol, f BareType)
toBare ((TyVar, LocSpecType) -> (LocSymbol, Located BareType))
-> [(TyVar, LocSpecType)] -> [(LocSymbol, Located BareType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
reflTySigs
    sigVars :: HashSet TyVar
sigVars       = HashSet TyVar -> HashSet TyVar -> HashSet TyVar
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet TyVar
defVars HashSet TyVar
reflVars
    defVars :: HashSet TyVar
defVars       = [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (GhcSrc -> [TyVar]
_giDefVars GhcSrc
src)
    reflTySigs :: [(TyVar, LocSpecType)]
reflTySigs    = [(TyVar
x, LocSpecType
t) | (TyVar
x,LocSpecType
t,Equation
_) <- GhcSpecRefl -> [(TyVar, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl, TyVar
x TyVar -> [TyVar] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` GhcSpecRefl -> [TyVar]
gsWiredReft GhcSpecRefl
refl]
    reflVars :: HashSet TyVar
reflVars      = [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
reflTySigs)
    -- myAliases fld = M.elems . fld $ myRTE
    srcF :: [Char]
srcF          = GhcSrc -> [Char]
_giTarget GhcSrc
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 :: forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
f a
lx = [Char]
f [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
lifted Bool -> Bool -> Bool
|| Bool
isCompanion
  where
    lifted :: FilePath
    lifted :: [Char]
lifted = a -> [Char]
forall a. Loc a => a -> [Char]
locFile a
lx

    isCompanion :: Bool
    isCompanion :: Bool
isCompanion =
      [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Char] -> [Char]
dropExtension [Char]
f) ([Char] -> [Char]
dropExtension [Char]
lifted)
       Bool -> Bool -> Bool
&&  Ext -> [Char] -> Bool
isExtFile Ext
Hs [Char]
f
       Bool -> Bool -> Bool
&&  Ext -> [Char] -> Bool
isExtFile Ext
Files.Spec [Char]
lifted

locFile :: (F.Loc a) => a -> FilePath
locFile :: forall a. Loc a => a -> [Char]
locFile = ([Char], Line, Line) -> [Char]
forall a b c. (a, b, c) -> a
Misc.fst3 (([Char], Line, Line) -> [Char])
-> (a -> ([Char], Line, Line)) -> a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> ([Char], Line, Line)
F.sourcePosElts (SourcePos -> ([Char], Line, Line))
-> (a -> SourcePos) -> a -> ([Char], Line, Line)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> SourcePos
F.sp_start (SrcSpan -> SourcePos) -> (a -> SrcSpan) -> a -> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SrcSpan
forall a. Loc a => a -> SrcSpan
F.srcSpan

varLocSym :: Ghc.Var -> LocSymbol
varLocSym :: TyVar -> LocSymbol
varLocSym TyVar
v = TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyVar -> Symbol) -> Located TyVar -> LocSymbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> Located TyVar
forall a. NamedThing a => a -> Located a
GM.locNamedThing TyVar
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 :: GhcSrc -> Env -> SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv GhcSrc
src Env
env SigEnv
sigEnv BareRTEnv
rtEnv = [Located BareRTAlias]
-> [Located (RTAlias Symbol Expr)] -> BareRTEnv
forall x a.
[Located (RTAlias x a)]
-> [Located (RTAlias Symbol Expr)] -> RTEnv x a
mkRTE [Located BareRTAlias]
tAs' [Located (RTAlias Symbol Expr)]
eAs
  where
    tAs' :: [Located BareRTAlias]
tAs'                     = Env
-> SigEnv -> ModName -> Located BareRTAlias -> Located BareRTAlias
normalizeBareAlias Env
env SigEnv
sigEnv ModName
name (Located BareRTAlias -> Located BareRTAlias)
-> [Located BareRTAlias] -> [Located BareRTAlias]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BareRTAlias]
tAs
    tAs :: [Located BareRTAlias]
tAs                      = (BareRTEnv -> HashMap Symbol (Located BareRTAlias))
-> [Located BareRTAlias]
forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap Symbol (Located BareRTAlias)
forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases
    eAs :: [Located (RTAlias Symbol Expr)]
eAs                      = (BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr)))
-> [Located (RTAlias Symbol Expr)]
forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr))
forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases
    myAliases :: (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap k a
fld            = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> a -> Bool
forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF) ([a] -> [a]) -> (BareRTEnv -> [a]) -> BareRTEnv -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap k a -> [a]
forall k v. HashMap k v -> [v]
M.elems (HashMap k a -> [a])
-> (BareRTEnv -> HashMap k a) -> BareRTEnv -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> HashMap k a
fld (BareRTEnv -> [a]) -> BareRTEnv -> [a]
forall a b. (a -> b) -> a -> b
$ BareRTEnv
rtEnv
    srcF :: [Char]
srcF                     = GhcSrc -> [Char]
_giTarget    GhcSrc
src
    name :: ModName
name                     = GhcSrc -> ModName
_giTargetMod GhcSrc
src

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

normalizeBareAlias :: Bare.Env -> Bare.SigEnv -> ModName -> Located BareRTAlias
                   -> Located BareRTAlias
normalizeBareAlias :: Env
-> SigEnv -> ModName -> Located BareRTAlias -> Located BareRTAlias
normalizeBareAlias Env
env SigEnv
sigEnv ModName
name Located BareRTAlias
lx = BareRTAlias -> BareRTAlias
fixRTA (BareRTAlias -> BareRTAlias)
-> Located BareRTAlias -> Located BareRTAlias
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located BareRTAlias
lx
  where
    fixRTA  :: BareRTAlias -> BareRTAlias
    fixRTA :: BareRTAlias -> BareRTAlias
fixRTA  = (Symbol -> Symbol) -> BareRTAlias -> BareRTAlias
forall a b ty. (a -> b) -> RTAlias a ty -> RTAlias b ty
mapRTAVars Symbol -> Symbol
fixArg (BareRTAlias -> BareRTAlias)
-> (BareRTAlias -> BareRTAlias) -> BareRTAlias -> BareRTAlias
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BareType -> BareType) -> BareRTAlias -> BareRTAlias
forall a b. (a -> b) -> RTAlias Symbol a -> RTAlias Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BareType -> BareType
fixBody

    fixArg  :: Symbol -> Symbol
    fixArg :: Symbol -> Symbol
fixArg  = TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (TyVar -> Symbol) -> (Symbol -> TyVar) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> TyVar
GM.symbolTyVar

    fixBody :: BareType -> BareType
    fixBody :: BareType -> BareType
fixBody = SpecType -> BareType
Bare.specToBare
            (SpecType -> BareType)
-> (BareType -> SpecType) -> BareType -> BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSpecType -> SpecType
forall a. Located a -> a
F.val
            (LocSpecType -> SpecType)
-> (BareType -> LocSpecType) -> BareType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.RawTV
            (Located BareType -> LocSpecType)
-> (BareType -> Located BareType) -> BareType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located BareRTAlias -> BareType -> Located BareType
forall l b. Loc l => l -> b -> Located b
F.atLoc Located BareRTAlias
lx


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