{-# 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 LocBareType LocSymbol))
loadLiftedSpec Config
cfg [Char]
srcF
  | Config -> Bool
noLiftedImport Config
cfg = [Char] -> IO ()
putStrLn [Char]
"No LIFTED Import" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"Loading Binary Lifted Spec: " forall a. [a] -> [a] -> [a]
++ [Char]
specF forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ [Char]
"for source-file: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
srcF forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Bool
ex
      Maybe (Spec LocBareType LocSymbol)
lSp <- if Bool
ex
               then forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Binary a => [Char] -> IO a
B.decodeFile [Char]
specF
               else {- warnMissingLiftedSpec srcF specF >> -} forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      forall a. a -> IO a
Ex.evaluate Maybe (Spec LocBareType 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 LocBareType LocSymbol -> IO ()
saveLiftedSpec [Char]
srcF Spec LocBareType LocSymbol
lspec = do
  [Char] -> IO ()
ensurePath [Char]
specF
  forall a. Binary a => [Char] -> a -> IO ()
B.encodeFile [Char]
specF Spec LocBareType 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     = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ModName -> Spec LocBareType LocSymbol -> Either Diagnostics ()
Bare.checkBareSpec) [(ModName, Spec LocBareType LocSymbol)]
legacyDependencies
  let bareSpecDiagnostics :: Either Diagnostics ()
bareSpecDiagnostics = ModName -> Spec LocBareType LocSymbol -> Either Diagnostics ()
Bare.checkBareSpec (TargetSrc -> ModName
giTargetMod TargetSrc
targetSrc) Spec LocBareType LocSymbol
legacyBareSpec
  case Either Diagnostics ()
targDiagnostics forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics [()]
depsDiagnostics 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              -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Diagnostics
d
   Right ()            -> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase 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 LocBareType LocSymbol)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg (TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
targetSrc) LogicMap
lmap (Spec LocBareType LocSymbol
-> [(ModName, Spec LocBareType LocSymbol)]
allSpecs Spec LocBareType LocSymbol
legacyBareSpec)
      forall (m :: * -> *) a. Monad m => a -> m a
return 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
        forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
phaseOneWarns 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 LocBareType LocSymbol)
toLegacyDep (StableModule
sm, LiftedSpec
ls) = (ModType -> ModuleName -> ModName
ModName ModType
SrcImport (forall unit. GenModule unit -> ModuleName
Ghc.moduleName forall b c a. (b -> c) -> (a -> b) -> a -> c
. StableModule -> Module
Ghc.unStableModule forall a b. (a -> b) -> a -> b
$ StableModule
sm), LiftedSpec -> Spec LocBareType LocSymbol
unsafeFromLiftedSpec LiftedSpec
ls)

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

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

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

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


ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RENV" forall a b. (a -> b) -> a -> b
$ 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     = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"binds" forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                 [ [(Symbol
x,        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)]
                 , [(forall a. Symbolic a => a -> Symbol
symbol TyVar
v, 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)]
                 , [(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 forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)          <- [(Symbol, Sort)]
wiredSortedSyms       ]
                 , [(Symbol
x, Sort -> Reft -> SortedReft
RR Sort
s forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)          <- GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
sp       ]
                 ]
    vSort :: TyVar -> SortedReft
vSort     = forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. Bool -> RType c tv r -> RType c tv r
classRFInfoType (Config -> Bool
typeclass forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig GhcSpec
sp) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                (forall r. Monoid r => Type -> RRType r
ofType :: Ghc.Type -> SpecType) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType
    rSort :: RRType r -> SortedReft
rSort     = 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 LocBareType LocSymbol)]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 Config
cfg GhcSrc
src LogicMap
lmap [(ModName, Spec LocBareType 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 LocBareType LocSymbol
lSpec1   = Spec LocBareType LocSymbol
lSpec0 forall a. Semigroup a => a -> a -> a
<> Config
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec1 Config
cfg GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec LocBareType LocSymbol
mySpec1
  let mySpec :: Spec LocBareType LocSymbol
mySpec   = Spec LocBareType LocSymbol
mySpec2 forall a. Semigroup a => a -> a -> a
<> Spec LocBareType LocSymbol
lSpec1
  let specs :: HashMap ModName (Spec LocBareType LocSymbol)
specs    = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec LocBareType LocSymbol
mySpec HashMap ModName (Spec LocBareType 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) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Env
-> TycEnv
-> SigEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup MeasEnv
makeMeasEnv      Env
env TycEnv
tycEnv SigEnv
sigEnv       HashMap ModName (Spec LocBareType LocSymbol)
specs
  let (Diagnostics
dg4, GhcSpecSig
sig) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Config
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> Lookup GhcSpecSig
makeSpecSig Config
cfg ModName
name HashMap ModName (Spec LocBareType 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
                              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 forall (f :: * -> *) a. Applicative f => a -> f a
pure GhcSpecSig
sig
  let qual :: GhcSpecQual
qual     = Config
-> Env
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecQual
makeSpecQual Config
cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
rtEnv HashMap ModName (Spec LocBareType LocSymbol)
specs
  let sData :: GhcSpecData
sData    = GhcSrc
-> Env
-> SigEnv
-> MeasEnv
-> GhcSpecSig
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecData
makeSpecData  GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
elaboratedSig HashMap ModName (Spec LocBareType LocSymbol)
specs
  let (Diagnostics
dg1, GhcSpecVars
spcVars) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Config
-> GhcSrc
-> Spec LocBareType LocSymbol
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec LocBareType LocSymbol
mySpec Env
env MeasEnv
measEnv
  let (Diagnostics
dg2, GhcSpecTerm
spcTerm) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Config
-> Spec LocBareType LocSymbol
-> Env
-> ModName
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg     Spec LocBareType LocSymbol
mySpec Env
env       ModName
name
  let (Diagnostics
dg3, GhcSpecRefl
refl)    = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ Config
-> GhcSrc
-> MeasEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl Config
cfg GhcSrc
src MeasEnv
measEnv HashMap ModName (Spec LocBareType LocSymbol)
specs Env
env ModName
name GhcSpecSig
elaboratedSig TycEnv
tycEnv
  let laws :: GhcSpecLaws
laws     = Env
-> SigEnv
-> [(TyVar, LocSpecType)]
-> MeasEnv
-> HashMap ModName (Spec LocBareType LocSymbol)
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
elaboratedSig forall a. [a] -> [a] -> [a]
++ GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
elaboratedSig) MeasEnv
measEnv HashMap ModName (Spec LocBareType LocSymbol)
specs
  let finalLiftedSpec :: Spec LocBareType LocSymbol
finalLiftedSpec = ModName
-> GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> Spec LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec ModName
name GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
elaboratedSig GhcSpecQual
qual BareRTEnv
myRTE Spec LocBareType LocSymbol
lSpec1
  let diags :: Diagnostics
diags    = forall a. Monoid a => [a] -> a
mconcat [Diagnostics
dg0, Diagnostics
dg1, Diagnostics
dg2, Diagnostics
dg3, Diagnostics
dg4, Diagnostics
dg5]

  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics
diags, SP
    { _gsConfig :: Config
_gsConfig = Config
cfg
    , _gsImps :: [(Symbol, Sort)]
_gsImps   = [(ModName, Spec LocBareType LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec LocBareType 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 LocBareType LocSymbol
_gsLSpec  = Spec LocBareType LocSymbol
finalLiftedSpec
                { impSigs :: [(Symbol, Sort)]
impSigs   = [(ModName, Spec LocBareType LocSymbol)] -> [(Symbol, Sort)]
makeImports [(ModName, Spec LocBareType LocSymbol)]
mspecs
                , expSigs :: [(Symbol, Sort)]
expSigs   = [ (forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v, SortedReft -> Sort
F.sr_sort forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> TyVar -> SortedReft
Bare.varSortedReft TCEmb TyCon
embs TyVar
v) | TyVar
v <- GhcSpecRefl -> [TyVar]
gsReflects GhcSpecRefl
refl ]
                , dataDecls :: [DataDecl]
dataDecls = Spec LocBareType LocSymbol -> [DataDecl] -> [DataDecl]
Bare.dataDeclSize Spec LocBareType LocSymbol
mySpec forall a b. (a -> b) -> a -> b
$ forall ty bndr. Spec ty bndr -> [DataDecl]
dataDecls Spec LocBareType LocSymbol
mySpec
                , measures :: [Measure LocBareType LocSymbol]
measures  = forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.measures Spec LocBareType LocSymbol
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 :: [(LocSymbol, LocBareType)]
asmSigs = forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec LocBareType LocSymbol
finalLiftedSpec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec LocBareType LocSymbol
mySpec
                  -- Export all the assumptions (not just the ones created out of reflection) in
                  -- a 'LiftedSpec'.
                , imeasures :: [Measure LocBareType LocSymbol]
imeasures = forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.imeasures Spec LocBareType LocSymbol
finalLiftedSpec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [Measure ty bndr]
Ms.imeasures Spec LocBareType LocSymbol
mySpec
                  -- Preserve user-defined 'imeasures'.
                , dvariance :: [(LocSymbol, [Variance])]
dvariance = forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
Ms.dvariance Spec LocBareType LocSymbol
finalLiftedSpec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
Ms.dvariance Spec LocBareType LocSymbol
mySpec
                  -- Preserve user-defined 'dvariance'.
                , rinstance :: [RInstance LocBareType]
rinstance = forall ty bndr. Spec ty bndr -> [RInstance ty]
Ms.rinstance Spec LocBareType LocSymbol
finalLiftedSpec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [RInstance ty]
Ms.rinstance Spec LocBareType LocSymbol
mySpec
                  -- Preserve rinstances.
                }
    })
  where
    -- typeclass elaboration

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

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

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


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


makeEmbeds :: GhcSrc -> Bare.Env -> [(ModName, Ms.BareSpec)] -> F.TCEmb Ghc.TyCon
makeEmbeds :: GhcSrc
-> Env -> [(ModName, Spec LocBareType 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)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Monoid a => [a] -> a
mconcat
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Env -> (ModName, Spec LocBareType LocSymbol) -> TCEmb TyCon
makeTyConEmbeds Env
env)

makeTyConEmbeds :: Bare.Env -> (ModName, Ms.BareSpec) -> F.TCEmb Ghc.TyCon
makeTyConEmbeds :: Env -> (ModName, Spec LocBareType LocSymbol) -> TCEmb TyCon
makeTyConEmbeds Env
env (ModName
name, Spec LocBareType LocSymbol
spec)
  = forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
F.tceFromList [ (TyCon
tc, (Sort, TCArgs)
t) | (LocSymbol
c,(Sort, TCArgs)
t) <- forall a. TCEmb a -> [(a, (Sort, TCArgs))]
F.tceToList (forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
Ms.embeds Spec LocBareType LocSymbol
spec), TyCon
tc <- forall {a}. ResolveSym a => LocSymbol -> [a]
symTc LocSymbol
c ]
    where
      symTc :: LocSymbol -> [a]
symTc = forall a. Maybe a -> [a]
Mb.maybeToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec1 Config
config GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec LocBareType LocSymbol
mySpec = forall a. Monoid a => a
mempty
  { measures :: [Measure LocBareType LocSymbol]
Ms.measures  = Bool
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec LocBareType LocSymbol
-> [Measure LocBareType LocSymbol]
Bare.makeHaskellMeasures (Config -> Bool
typeclass Config
config) GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec LocBareType LocSymbol
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 LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec LocBareType LocSymbol
mySpec = forall a. Monoid a => a
mempty
  { ealiases :: [Located (RTAlias Symbol Expr)]
Ms.ealiases  = LMap -> Located (RTAlias Symbol Expr)
lmapEAlias forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec LocBareType LocSymbol
-> [(LocSymbol, LMap)]
Bare.makeHaskellInlines (Config -> Bool
typeclass Config
cfg) GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec LocBareType LocSymbol
mySpec
  , reflects :: HashSet LocSymbol
Ms.reflects  = forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec LocBareType LocSymbol
mySpec
  , dataDecls :: [DataDecl]
Ms.dataDecls = Config
-> ModName -> Spec LocBareType LocSymbol -> [TyCon] -> [DataDecl]
Bare.makeHaskellDataDecls Config
cfg ModName
name Spec LocBareType LocSymbol
mySpec [TyCon]
tcs
  , embeds :: TCEmb LocSymbol
Ms.embeds    = forall ty bndr. Spec ty bndr -> TCEmb LocSymbol
Ms.embeds Spec LocBareType LocSymbol
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.
  , cmeasures :: [Measure LocBareType ()]
Ms.cmeasures = forall ty bndr. Spec ty bndr -> [Measure ty ()]
Ms.cmeasures Spec LocBareType LocSymbol
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          = forall a. Uniquable a => [a] -> [a]
uniqNub (GhcSrc -> [TyCon]
_gsTcs GhcSrc
src forall a. [a] -> [a] -> [a]
++ [TyCon]
refTcs)
    refTcs :: [TyCon]
refTcs       = Config
-> TCEmb TyCon
-> [CoreBind]
-> Spec LocBareType LocSymbol
-> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs [CoreBind]
cbs  Spec LocBareType 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 = forall k v. HashMap k v -> [v]
M.elems forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall {a}. Uniquable a => a -> Int
index a
x, a
x) | a
x <- [a]
xs ]
  where
    index :: a -> Int
index  = Unique -> Int
Ghc.getKey forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 LocBareType LocSymbol
-> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs [CoreBind]
cbs Spec LocBareType LocSymbol
spec
  | forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs)
                    forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyVar -> [TyCon]
varTyCons
                    forall a b. (a -> b) -> a -> b
$ Spec LocBareType LocSymbol -> [CoreBind] -> [TyVar]
reflectedVars Spec LocBareType LocSymbol
spec [CoreBind]
cbs forall a. [a] -> [a] -> [a]
++ Spec LocBareType LocSymbol -> [CoreBind] -> [TyVar]
measureVars Spec LocBareType 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 = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Monoid r => Type -> RRType r
ofType forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType

specTypeCons           :: SpecType -> [Ghc.TyCon]
specTypeCons :: SpecType -> [TyCon]
specTypeCons         = forall acc c tv r.
(acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
foldRType 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 (forall c tv r. RType c tv r -> c
rt_tycon RType RTyCon tv r
t) 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 LocBareType LocSymbol -> [CoreBind] -> [TyVar]
reflectedVars Spec LocBareType LocSymbol
spec [CoreBind]
cbs = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, CoreExpr)]
xDefs
  where
    xDefs :: [(TyVar, CoreExpr)]
xDefs              = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Symbol -> [CoreBind] -> Maybe (TyVar, CoreExpr)
`GM.findVarDef` [CoreBind]
cbs) [Symbol]
reflSyms
    reflSyms :: [Symbol]
reflSyms           = forall a. Located a -> a
val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
S.toList (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec LocBareType LocSymbol
spec)

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

------------------------------------------------------------------------------------------
makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
             -> Bare.Lookup GhcSpecVars
------------------------------------------------------------------------------------------
makeSpecVars :: Config
-> GhcSrc
-> Spec LocBareType LocSymbol
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec LocBareType LocSymbol
mySpec Env
env MeasEnv
measEnv = do
  [TyVar]
tgtVars     <-   forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> [Char] -> Lookup TyVar
resolveStringVar  Env
env ModName
name)              (Config -> [[Char]]
checks     Config
cfg)
  HashSet TyVar
igVars      <-  forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"gs-ignores") (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.ignores Spec LocBareType LocSymbol
mySpec)
  HashSet TyVar
lVars       <-  forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"gs-lvars"  ) (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.lvars   Spec LocBareType LocSymbol
mySpec)
  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   = forall a b c. (a, b, c) -> b
snd3 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> m b
f (forall a. HashSet a -> [a]
S.toList HashSet a
xSet)
 forall (m :: * -> *) a. Monad m => a -> m a
return (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 = 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 (forall a. Symbolic a => a -> Symbol
F.symbol ModName
name) (forall a. Symbolic a => a -> Symbol
F.symbol a
s)

resolveStringVar :: Bare.Env -> ModName -> String -> Bare.Lookup Ghc.Var
resolveStringVar :: Env -> ModName -> [Char] -> Lookup TyVar
resolveStringVar Env
env ModName
name [Char]
s = Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"resolve-string-var" LocSymbol
lx
  where
    lx :: LocSymbol
lx                      = forall a. a -> Located a
dummyLoc (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 LocBareType LocSymbol)
-> GhcSpecQual
makeSpecQual Config
_cfg Env
env TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
_rtEnv HashMap ModName (Spec LocBareType LocSymbol)
specs = SpQual
  { gsQualifiers :: [Qualifier]
gsQualifiers = forall a. (a -> Bool) -> [a] -> [a]
filter forall {a}. (PPrint a, Subable a) => a -> Bool
okQual [Qualifier]
quals
  , gsRTAliases :: [Located SpecRTAlias]
gsRTAliases  = [] -- makeSpecRTAliases env rtEnv -- TODO-REBARE
  }
  where
    quals :: [Qualifier]
quals        = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall ty bndr.
Env -> TycEnv -> (ModName, Spec ty bndr) -> [Qualifier]
makeQualifiers Env
env TycEnv
tycEnv) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
    -- mSyms        = F.tracepp "MSYMS" $ M.fromList (Bare.meSyms measEnv ++ Bare.meClassSyms measEnv)
    okQual :: a -> Bool
okQual a
q     = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"okQual: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp a
q)
                   forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
mSyms) (forall a. Subable a => a -> [Symbol]
F.syms a
q)
    mSyms :: HashSet Symbol
mSyms        = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"MSYMS" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
                   forall a b. (a -> b) -> a -> b
$  (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
wiredSortedSyms)
                   forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meSyms MeasEnv
measEnv)
                   forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> a
fst 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)
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap        (forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env        ModName
modn)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Env -> TycEnv -> ModName -> Qualifier -> Maybe Qualifier
resolveQParams       Env
env TycEnv
tycEnv ModName
modn)
  forall a b. (a -> b) -> a -> b
$ 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   <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QualParam -> Maybe QualParam
goQP (Qualifier -> [QualParam]
F.qParams Qualifier
q)
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Qualifier
q { qParams :: [QualParam]
F.qParams = [QualParam]
qps }
  where
    goQP :: QualParam -> Maybe QualParam
goQP QualParam
qp          = do { Sort
s <- Sort -> Maybe Sort
go (QualParam -> Sort
F.qpSort QualParam
qp) ; forall (m :: * -> *) a. Monad m => a -> m a
return QualParam
qp { qpSort :: Sort
F.qpSort = Sort
s } }
    go               :: F.Sort -> Maybe F.Sort
    go :: Sort -> Maybe Sort
go (FAbs Int
i Sort
s)    = Int -> Sort -> Sort
FAbs Int
i 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  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s1 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   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sort -> Maybe Sort
go Sort
s1 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             = 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           = forall a. a -> Maybe a
Just (FTycon -> Sort
FTC FTycon
c)
  | Bool
otherwise           = TCEmb TyCon -> Located TyCon -> Sort
tyConSort TCEmb TyCon
embs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
tcs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a}. ResolveSym a => Maybe a
ty
  where
    ty :: Maybe a
ty                  = forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym Env
env ModName
name [Char]
"qualify-FTycon" LocSymbol
tcs
    isPrimFTC :: Bool
isPrimFTC           = forall a. Located a -> a
F.val LocSymbol
tcs 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 = forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe Sort
s0 forall a b. (a, b) -> a
fst (forall a.
(Eq a, Hashable a) =>
a -> TCEmb a -> Maybe (Sort, TCArgs)
F.tceLookup TyCon
c TCEmb TyCon
embs)
  where
    c :: TyCon
c             = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> FTycon
F.symbolFTycon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Symbolic a => a -> Symbol
F.symbol

------------------------------------------------------------------------------------------
makeSpecTerm :: Config -> Ms.BareSpec -> Bare.Env -> ModName ->
                Bare.Lookup GhcSpecTerm
------------------------------------------------------------------------------------------
makeSpecTerm :: Config
-> Spec LocBareType LocSymbol
-> Env
-> ModName
-> Lookup GhcSpecTerm
makeSpecTerm Config
cfg Spec LocBareType LocSymbol
mySpec Env
env ModName
name = do
  HashSet TyVar
sizes  <- if forall t. HasConfig t => t -> Bool
structuralTerm Config
cfg then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty else Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyVar)
makeSize Env
env ModName
name Spec LocBareType LocSymbol
mySpec
  HashSet TyVar
lazies <- Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyVar)
makeLazy     Env
env ModName
name Spec LocBareType LocSymbol
mySpec
  HashSet TyCon
autos  <- Env
-> ModName -> Spec LocBareType LocSymbol -> Lookup (HashSet TyCon)
makeAutoSize Env
env ModName
name Spec LocBareType LocSymbol
mySpec
  HashSet (Located TyVar)
gfail  <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashSet (Located TyVar))
makeFail Env
env ModName
name Spec LocBareType LocSymbol
mySpec
  forall (m :: * -> *) a. Monad m => a -> m a
return  forall a b. (a -> b) -> a -> b
$ SpTerm
    { gsLazy :: HashSet TyVar
gsLazy       = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert TyVar
dictionaryVar (HashSet TyVar
lazies 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  = 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, LocBareType, LocBareType, RelExpr,
     RelExpr)]
-> Lookup
     [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {e} {f}.
(LocSymbol, LocSymbol, LocBareType, LocBareType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
go
 where
  go :: (LocSymbol, LocSymbol, LocBareType, LocBareType, e, f)
-> Either [Error] (TyVar, TyVar, LocSpecType, LocSpecType, e, f)
go (LocSymbol
x, LocSymbol
y, LocBareType
tx, LocBareType
ty, e
a, f
e) = do
    TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
    TyVar
vy <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
y
    forall (m :: * -> *) a. Monad m => a -> m a
return
        ( TyVar
vx
        , TyVar
vy
        , Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.HsTV TyVar
vx) LocBareType
tx
        , Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.HsTV TyVar
vy) LocBareType
ty
        , e
a
        , f
e
        )


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

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

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

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

makeRewriteWith' :: Bare.Env -> ModName -> Spec ty bndr -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' :: forall ty bndr.
Env -> ModName -> Spec ty bndr -> Lookup [(TyVar, [TyVar])]
makeRewriteWith' Env
env ModName
name Spec ty bndr
spec =
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ forall ty bndr. Spec ty bndr -> HashMap LocSymbol [LocSymbol]
Ms.rewriteWith Spec ty bndr
spec) forall a b. (a -> b) -> a -> b
$ \(LocSymbol
x, [LocSymbol]
xs) -> do
    TyVar
xv  <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var1" LocSymbol
x
    [TyVar]
xvs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var2") [LocSymbol]
xs
    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 LocBareType LocSymbol -> Lookup (HashSet TyCon)
makeAutoSize Env
env ModName
name
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyCon
Bare.lookupGhcTyCon Env
env ModName
name [Char]
"TyCon")
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashSet a -> [a]
S.toList
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 LocBareType LocSymbol -> Lookup (HashSet TyVar)
makeSize Env
env ModName
name
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var")
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe LocSymbol
getSizeFuns
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
  = forall a. a -> Maybe a
Just LocSymbol
f
  | Bool
otherwise
  = 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 LocBareType LocSymbol)
-> GhcSpecLaws
makeSpecLaws Env
env SigEnv
sigEnv [(TyVar, LocSpecType)]
sigs MeasEnv
menv HashMap ModName (Spec LocBareType LocSymbol)
specs = SpLaws
  { gsLawDefs :: [(Class, [(TyVar, LocSpecType)])]
gsLawDefs = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall a b. (a -> b) -> [a] -> [b]
map (\(ModName
_,TyVar
x,LocSpecType
y) -> (TyVar
x,LocSpecType
y))) 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 LocBareType LocSymbol)
-> [LawInstance]
Bare.makeInstanceLaws Env
env SigEnv
sigEnv [(TyVar, LocSpecType)]
sigs HashMap ModName (Spec LocBareType 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 LocBareType LocSymbol)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl Config
cfg GhcSrc
src MeasEnv
menv HashMap ModName (Spec LocBareType LocSymbol)
specs Env
env ModName
name GhcSpecSig
sig TycEnv
tycEnv = do
  HashMap TyVar (Maybe Int)
autoInst <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashMap TyVar (Maybe Int))
makeAutoInst Env
env ModName
name Spec LocBareType LocSymbol
mySpec
  HashSet (Located TyVar)
rwr      <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashSet (Located TyVar))
makeRewrite Env
env ModName
name Spec LocBareType LocSymbol
mySpec
  HashMap TyVar [TyVar]
rwrWith  <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup (HashMap TyVar [TyVar])
makeRewriteWith Env
env ModName
name Spec LocBareType 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 LocBareType LocSymbol
-> Lookup [(TyVar, LocSpecType, Equation)]
Bare.makeHaskellAxioms Config
cfg GhcSrc
src Env
env TycEnv
tycEnv ModName
name LogicMap
lmap GhcSpecSig
sig Spec LocBareType LocSymbol
mySpec
  let myAxioms :: [Equation]
myAxioms =
        [ forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop
            Env
env
            ModName
name
            (forall a. Located a -> SourcePos
F.loc LocSpecType
lt)
            Equation
e {eqName :: Symbol
eqName = Symbol
s, eqRec :: Bool
eqRec = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
s (Expr -> HashSet Symbol
exprSymbolsSet (Equation -> Expr
eqBody Equation
e))}
        | (TyVar
x, LocSpecType
lt, Equation
e) <- [(TyVar, LocSpecType, Equation)]
xtes
        , let s :: Symbol
s = forall a. Symbolic a => a -> Symbol
symbol TyVar
x
        ]
  let sigVars :: [TyVar]
sigVars  = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"SIGVARS" forall a b. (a -> b) -> a -> b
$ (forall a b c. (a, b, c) -> a
fst3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType, Equation)]
xtes)            -- reflects
                                      forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> a
fst  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
sig)   -- assumes
                                      forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> a
fst  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, LocSpecType)]
gsRefSigs GhcSpecSig
sig)
  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  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall ty bndr. Spec ty bndr -> [Equation]
Ms.axeqs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
    , gsMyAxioms :: [Equation]
gsMyAxioms   = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsMyAxioms" [Equation]
myAxioms
    , gsReflects :: [TyVar]
gsReflects   = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsReflects" ([TyVar]
lawMethods forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter (HashSet Symbol -> TyVar -> Bool
isReflectVar HashSet Symbol
rflSyms) [TyVar]
sigVars forall a. [a] -> [a] -> [a]
++ [TyVar]
wRefls)
    , gsHAxioms :: [(TyVar, LocSpecType, Equation)]
gsHAxioms    = 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   = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"Law Methods" forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Class -> [TyVar]
Ghc.classMethods (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.meCLaws MeasEnv
menv)
    mySpec :: Spec LocBareType LocSymbol
mySpec       = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
    rflSyms :: HashSet Symbol
rflSyms      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (HashMap ModName (Spec LocBareType LocSymbol) -> [Symbol]
getReflects HashMap ModName (Spec LocBareType 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 = 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 (forall a. Symbolic a => a -> Symbol
symbol TyVar
v)

getReflects :: Bare.ModSpecs -> [Symbol]
getReflects :: HashMap ModName (Spec LocBareType LocSymbol) -> [Symbol]
getReflects  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashSet a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall ty bndr. Spec ty bndr -> HashSet LocSymbol
names forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [(k, v)]
M.toList
  where
    names :: Spec ty bndr -> HashSet LocSymbol
names  Spec ty bndr
z = forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions [ forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.reflects Spec ty bndr
z, forall ty bndr. Spec ty bndr -> HashSet LocSymbol
Ms.inlines Spec ty bndr
z, 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 :: [(TyVar, LocSpecType)]
gsRefSigs = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"gsRefSigs for " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (TyVar, LocSpecType) -> (TyVar, LocSpecType)
expandReflectedSignature [(TyVar, LocSpecType)]
reflSigs
      , gsAsmSigs :: [(TyVar, LocSpecType)]
gsAsmSigs = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"gsAsmSigs for " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name) ([(TyVar, LocSpecType)]
wreflSigs forall a. [a] -> [a] -> [a]
++ forall a. (a -> Bool) -> [a] -> [a]
filter forall {b}. (TyVar, b) -> Bool
notReflected (GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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)   = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition ((forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` GhcSpecRefl -> [TyVar]
gsWiredReft GhcSpecRefl
refl) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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       = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([(TyVar, LocSpecType)]
wreflSigs forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
reflSigs)
    notReflected :: (TyVar, b) -> Bool
notReflected (TyVar, b)
xt = forall a b. (a, b) -> a
fst (TyVar, b)
xt 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 LocBareType LocSymbol
-> Lookup (HashMap TyVar (Maybe Int))
makeAutoInst Env
env ModName
name Spec LocBareType LocSymbol
spec = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall k v. HashMap k v -> [(k, v)]
M.toList (forall ty bndr. Spec ty bndr -> HashMap LocSymbol (Maybe Int)
Ms.autois Spec LocBareType LocSymbol
spec)) forall a b. (a -> b) -> a -> b
$ \(LocSymbol
k, Maybe Int
val) -> do
            TyVar
vk <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
k
            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 LocBareType LocSymbol)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> [CoreBind]
-> Lookup GhcSpecSig
makeSpecSig Config
cfg ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs Env
env SigEnv
sigEnv TycEnv
tycEnv MeasEnv
measEnv [CoreBind]
cbs = do
  [(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs     <- Env
-> SigEnv
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs  Env
env SigEnv
sigEnv ModName
name Spec LocBareType LocSymbol
mySpec
  [(TyVar, LocSpecType)]
aSigs      <- forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"makeSpecSig aSigs " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name) forall a b. (a -> b) -> a -> b
$ Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
  let asmSigs :: [(TyVar, LocSpecType)]
asmSigs =  TycEnv -> [(TyVar, LocSpecType)]
Bare.tcSelVars TycEnv
tycEnv
              forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
aSigs
              forall a. [a] -> [a] -> [a]
++ [ (TyVar
x,LocSpecType
t) | (ModName
_, TyVar
x, LocSpecType
t) <- forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat 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 LocBareType LocSymbol)]
-> [(TyVar, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv [(ModName, Spec LocBareType LocSymbol)]
allSpecs ]   -- during the strengthening, i.e. to KEEP
                  , [(TyVar
v, (Int
3, LocSpecType
t)) | (TyVar
v, LocSpecType
t  ) <- Env
-> BareRTEnv
-> [(ModName, Spec LocBareType LocSymbol)]
-> [(TyVar, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv [(ModName, Spec LocBareType LocSymbol)]
allSpecs ]   -- the binders used in USER-defined sigs
                  ]                                                               -- as they appear in termination metrics
  [(TyCon, LocSpecType)]
newTys     <-  Env
-> SigEnv
-> [(ModName, Spec LocBareType LocSymbol)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec LocBareType LocSymbol)]
allSpecs
  [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
relation   <-  Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
     RelExpr)]
-> Lookup
     [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv (forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Ms.relational Spec LocBareType LocSymbol
mySpec)
  [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
asmRel     <-  Env
-> ModName
-> SigEnv
-> [(LocSymbol, LocSymbol, LocBareType, LocBareType, RelExpr,
     RelExpr)]
-> Lookup
     [(TyVar, TyVar, LocSpecType, LocSpecType, RelExpr, RelExpr)]
makeRelation Env
env ModName
name SigEnv
sigEnv (forall ty bndr.
Spec ty bndr -> [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]
Ms.asmRel Spec LocBareType LocSymbol
mySpec)
  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   = 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 LocBareType LocSymbol)
-> DEnv TyVar LocSpecType
Bare.makeSpecDictionaries Env
env SigEnv
sigEnv HashMap ModName (Spec LocBareType LocSymbol)
specs
    mySpec :: Spec LocBareType LocSymbol
mySpec     = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
    allSpecs :: [(ModName, Spec LocBareType LocSymbol)]
allSpecs   = forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType 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 = forall {a} {b}.
(PPrint a, Ord b) =>
(a, [(b, LocSpecType)]) -> (a, LocSpecType)
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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,) forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> a) -> [a] -> a
L.foldl1' (forall a b c. (a -> b -> c) -> b -> a -> c
flip LocSpecType -> LocSpecType -> LocSpecType
meetLoc) (forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"STRENGTHEN-SIGS: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp a
v) (forall {b} {b}. Ord b => [(b, b)] -> [b]
prio [(b, LocSpecType)]
ixs))
    prio :: [(b, b)] -> [b]
prio            = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
Misc.sortOn forall a b. (a, b) -> a
fst
    meetLoc         :: LocSpecType -> LocSpecType -> LocSpecType
    meetLoc :: LocSpecType -> LocSpecType -> LocSpecType
meetLoc LocSpecType
t1 LocSpecType
t2   = LocSpecType
t1 {val :: SpecType
val = forall a. Located a -> a
val LocSpecType
t1 forall r. Reftable r => r -> r -> r
`F.meet` forall a. Located a -> a
val LocSpecType
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 LocBareType 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 (forall t. HasConfig t => t -> Config
getConfig Env
env)))
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Spec LocBareType LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec LocBareType LocSymbol)]
-> [TyVar]
makeFromSet [Char]
"hinlines" 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 LocBareType 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 (forall t. HasConfig t => t -> Config
getConfig Env
env)))
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char]
-> (Spec LocBareType LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec LocBareType LocSymbol)]
-> [TyVar]
makeFromSet [Char]
"hmeas" 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 = forall a. NamedThing a => a -> Located a
GM.locNamedThing TyVar
x
             , let lt :: LocSpecType
lt = LocSpecType -> LocSpecType
expand forall a b. (a -> b) -> a -> b
$ Located TyVar
lx {val :: SpecType
val = TyVar -> SpecType
f TyVar
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 LocBareType LocSymbol -> HashSet LocSymbol)
-> Env
-> [(ModName, Spec LocBareType LocSymbol)]
-> [TyVar]
makeFromSet [Char]
msg Spec LocBareType LocSymbol -> HashSet LocSymbol
f Env
env [(ModName, Spec LocBareType LocSymbol)]
specs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ forall {b}. ResolveSym b => ModName -> [LocSymbol] -> [b]
mk ModName
n [LocSymbol]
xs | (ModName
n, Spec LocBareType LocSymbol
s) <- [(ModName, Spec LocBareType LocSymbol)]
specs, let xs :: [LocSymbol]
xs = forall a. HashSet a -> [a]
S.toList (Spec LocBareType LocSymbol -> HashSet LocSymbol
f Spec LocBareType LocSymbol
s)]
  where
    mk :: ModName -> [LocSymbol] -> [b]
mk ModName
name                 = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (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 LocBareType LocSymbol
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs Env
env SigEnv
sigEnv ModName
name Spec LocBareType LocSymbol
spec = do
  [(TyVar, LocBareType)]
bareSigs   <- Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocBareType)]
bareTySigs Env
env ModName
name                Spec LocBareType LocSymbol
spec
  [(TyVar, LocBareType, Maybe [Located Expr])]
expSigs    <- Env
-> ModName
-> [(TyVar, LocBareType)]
-> BareRTEnv
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocBareType, Maybe [Located Expr])]
makeTExpr  Env
env ModName
name [(TyVar, LocBareType)]
bareSigs BareRTEnv
rtEnv Spec LocBareType LocSymbol
spec
  let rawSigs :: [(TyVar, LocBareType, Maybe [Located Expr])]
rawSigs = Env
-> [(TyVar, LocBareType, Maybe [Located Expr])]
-> [(TyVar, LocBareType, Maybe [Located Expr])]
Bare.resolveLocalBinds Env
env [(TyVar, LocBareType, Maybe [Located Expr])]
expSigs
  forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
x, TyVar -> LocBareType -> LocSpecType
cook TyVar
x LocBareType
bt, Maybe [Located Expr]
z) | (TyVar
x, LocBareType
bt, Maybe [Located Expr]
z) <- [(TyVar, LocBareType, Maybe [Located Expr])]
rawSigs ]
  where
    rtEnv :: BareRTEnv
rtEnv     = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
    cook :: TyVar -> LocBareType -> LocSpecType
cook TyVar
x LocBareType
bt = Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.HsTV TyVar
x) LocBareType
bt

bareTySigs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, LocBareType)]
bareTySigs :: Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocBareType)]
bareTySigs Env
env ModName
name Spec LocBareType LocSymbol
spec = forall x t. Symbolic x => [(x, Located t)] -> [(x, Located t)]
checkDuplicateSigs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lookup [(TyVar, LocBareType)]
vts
  where
    vts :: Lookup [(TyVar, LocBareType)]
vts = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs Spec LocBareType LocSymbol
spec forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.localSigs Spec LocBareType LocSymbol
spec ) forall a b. (a -> b) -> a -> b
$ \ (LocSymbol
x, LocBareType
t) -> do
            TyVar
v <- forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"LOOKUP-GHC-VAR" forall a b. (a -> b) -> a -> b
$ Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"rawTySigs" LocSymbol
x
            forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar
v, LocBareType
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 forall k v. (Eq k, Hashable k) => [(k, v)] -> Either (k, [v]) [v]
Misc.uniqueByKey [(Symbol, SourcePos)]
symXs  of
  Left (Symbol
k, [SourcePos]
ls) -> forall a. UserError -> a
uError (forall t. Doc -> ListNE SrcSpan -> TError t
errDupSpecs (forall a. PPrint a => a -> Doc
pprint Symbol
k) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan 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 = [ (forall a. Symbolic a => a -> Symbol
F.symbol x
x, 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 LocBareType LocSymbol)
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
myName HashMap ModName (Spec LocBareType LocSymbol)
specs = do
  [(ModName, TyVar, LocBareType)]
raSigs <- Env
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(ModName, TyVar, LocBareType)]
rawAsmSigs Env
env ModName
myName HashMap ModName (Spec LocBareType LocSymbol)
specs
  forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
x, LocSpecType
t) | (ModName
name, TyVar
x, LocBareType
bt) <- [(ModName, TyVar, LocBareType)]
raSigs, let t :: LocSpecType
t = Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.LqTV TyVar
x) LocBareType
bt ]

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

myAsmSig :: Ghc.Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig :: TyVar -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig TyVar
v [(Bool, ModName, LocBareType)]
sigs = forall a. a -> Maybe a -> a
Mb.fromMaybe forall {a}. a
errImp (Maybe (ModName, LocBareType)
mbHome forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (ModName, LocBareType)
mbImp)
  where
    mbHome :: Maybe (ModName, LocBareType)
mbHome      = forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique forall {a} {a}. [(a, Located a)] -> UserError
mkErr                  [(ModName, LocBareType)]
sigsHome
    mbImp :: Maybe (ModName, LocBareType)
mbImp       = forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique forall {a} {a}. [(a, Located a)] -> UserError
mkErr (forall k a. (Eq k, Ord k, Hashable k) => [(k, a)] -> [a]
Misc.firstGroup [(Int, (ModName, LocBareType))]
sigsImp) -- see [NOTE:Prioritize-Home-Spec]
    sigsHome :: [(ModName, LocBareType)]
sigsHome    = [(ModName
m, LocBareType
t)      | (Bool
True,  ModName
m, LocBareType
t) <- [(Bool, ModName, LocBareType)]
sigs ]
    sigsImp :: [(Int, (ModName, LocBareType))]
sigsImp     = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"SIGS-IMP: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp TyVar
v)
                  [(Int
d, (ModName
m, LocBareType
t)) | (Bool
False, ModName
m, LocBareType
t) <- [(Bool, ModName, LocBareType)]
sigs, let d :: Int
d = Symbol -> ModName -> Int
nameDistance Symbol
vName ModName
m]
    mkErr :: [(a, Located a)] -> UserError
mkErr [(a, Located a)]
ts    = forall t. SrcSpan -> Doc -> ListNE SrcSpan -> TError t
ErrDupSpecs (forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan TyVar
v) (forall a. PPrint a => a -> Doc
F.pprint TyVar
v) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> SourcePos
F.loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Located a)]
ts) :: UserError
    errImp :: a
errImp      = forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing [Char]
"myAsmSig: cannot happen as sigs is non-null"
    vName :: Symbol
vName       = Symbol -> Symbol
GM.takeModuleNames (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, LocBareType)]
-> BareRTEnv
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, LocBareType, Maybe [Located Expr])]
makeTExpr Env
env ModName
name [(TyVar, LocBareType)]
tySigs BareRTEnv
rtEnv Spec LocBareType LocSymbol
spec = do
  HashMap TyVar [Located Expr]
vExprs       <- forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, [Located Expr])]
makeVarTExprs Env
env ModName
name Spec LocBareType LocSymbol
spec
  let vSigExprs :: HashMap TyVar (LocBareType, Maybe [Located Expr])
vSigExprs = forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
Misc.hashMapMapWithKey (\TyVar
v LocBareType
t -> (LocBareType
t, forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup TyVar
v HashMap TyVar [Located Expr]
vExprs)) HashMap TyVar LocBareType
vSigs
  forall (m :: * -> *) a. Monad m => a -> m a
return [ (TyVar
v, LocBareType
t, forall {f :: * -> *}.
Functor f =>
LocBareType -> f (Located Expr) -> f (Located Expr)
qual LocBareType
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Located Expr]
es) | (TyVar
v, (LocBareType
t, Maybe [Located Expr]
es)) <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap TyVar (LocBareType, Maybe [Located Expr])
vSigExprs ]
  where
    qual :: LocBareType -> f (Located Expr) -> f (Located Expr)
qual LocBareType
t f (Located Expr)
es   = Env
-> ModName
-> BareRTEnv
-> LocBareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv LocBareType
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Located Expr)
es
    vSigs :: HashMap TyVar LocBareType
vSigs       = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(TyVar, LocBareType)]
tySigs

qualifyTermExpr :: Bare.Env -> ModName -> BareRTEnv -> LocBareType -> Located F.Expr
                -> Located F.Expr
qualifyTermExpr :: Env
-> ModName
-> BareRTEnv
-> LocBareType
-> Located Expr
-> Located Expr
qualifyTermExpr Env
env ModName
name BareRTEnv
rtEnv LocBareType
t Located Expr
le
        = forall l b. Loc l => l -> b -> Located b
F.atLoc Located Expr
le (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   = forall a. Located a -> SourcePos
F.loc Located Expr
le
    e :: Expr
e   = forall a. Located a -> a
F.val Located Expr
le
    bs :: [Symbol]
bs  = forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val forall a b. (a -> b) -> a -> b
$ LocBareType
t

makeVarTExprs :: Bare.Env -> ModName -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
makeVarTExprs :: Env
-> ModName
-> Spec LocBareType LocSymbol
-> Lookup [(TyVar, [Located Expr])]
makeVarTExprs Env
env ModName
name Spec LocBareType LocSymbol
spec =
  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall ty bndr. Spec ty bndr -> [(LocSymbol, [Located Expr])]
Ms.termexprs Spec LocBareType LocSymbol
spec) forall a b. (a -> b) -> a -> b
$ \(LocSymbol
x, [Located Expr]
es) -> do
    TyVar
vx <- Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"Var" LocSymbol
x
    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 forall a. Eq a => a -> a -> Bool
== 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
_ []  = forall a. Maybe a
Nothing
takeUnique [a] -> e
_ [a
x] = forall a. a -> Maybe a
Just a
x
takeUnique [a] -> e
f [a]
xs  = 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 LocBareType LocSymbol)
-> Lookup [(TyVar, [(Bool, ModName, LocBareType)])]
allAsmSigs Env
env ModName
myName HashMap ModName (Spec LocBareType LocSymbol)
specs = do
  let aSigs :: [(ModName, Bool, LocSymbol, LocBareType)]
aSigs = [ (ModName
name, Bool
locallyDefined, LocSymbol
x, LocBareType
t) | (ModName
name, Spec LocBareType LocSymbol
spec) <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs
                                   , (Bool
locallyDefined, LocSymbol
x, LocBareType
t) <- ModName
-> ModName
-> Spec LocBareType LocSymbol
-> [(Bool, LocSymbol, LocBareType)]
getAsmSigs ModName
myName ModName
name Spec LocBareType LocSymbol
spec ]
  [(Maybe TyVar, (Bool, ModName, LocBareType))]
vSigs    <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, Bool, LocSymbol, LocBareType)]
aSigs forall a b. (a -> b) -> a -> b
$ \(ModName
name, Bool
locallyDefined, LocSymbol
x, LocBareType
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 (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#
                         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Maybe Symbol, Symbol) -> Maybe TyVar
lookupImportedSymMaybe (Maybe Symbol
mm, Symbol
s)
                forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe TyVar
vMb, (Bool
locallyDefined, ModName
name, LocBareType
t))
  forall (m :: * -> *) a. Monad m => a -> m a
return    forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [ (TyVar
v, (Bool, ModName, LocBareType)
z) | (Just TyVar
v, (Bool, ModName, LocBareType)
z) <- [(Maybe TyVar, (Bool, ModName, LocBareType))]
vSigs ]
  where
    lookupImportedSym :: LocSymbol -> (Maybe Symbol, Symbol) -> Lookup (Maybe TyVar)
lookupImportedSym LocSymbol
x (Maybe Symbol, Symbol)
qp =
      let errRes :: Either [Error] b
errRes = forall a b. a -> Either a b
Left [Doc -> [Char] -> LocSymbol -> Error
Bare.errResolve Doc
"variable" [Char]
"Var" LocSymbol
x]
       in forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall {b}. Either [Error] b
errRes (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) 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 <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
s (Env -> TyThingMap
Bare._reTyThings Env
env)
      Symbol
m <- Maybe Symbol
mm
      forall a. [a] -> Maybe a
Mb.listToMaybe [ TyVar
v | (Symbol
k, Ghc.AnId TyVar
v) <- [(Symbol, TyThing)]
mts, Symbol
k forall a. Eq a => a -> a -> Bool
== Symbol
m ]

    isAbsoluteQualifiedSym :: Maybe Symbol -> Bool
isAbsoluteQualifiedSym (Just Symbol
m) =
       Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Symbol
m 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 = forall a. a -> Maybe a
Just  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> ModName -> [Char] -> LocSymbol -> Lookup TyVar
Bare.lookupGhcVar Env
env ModName
name [Char]
"resolveAsmVar-True"  LocSymbol
lx
resolveAsmVar Env
env ModName
name Bool
False LocSymbol
lx = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$  forall a.
ResolveSym a =>
Env -> ModName -> [Char] -> LocSymbol -> Maybe a
Bare.maybeResolveSym     Env
env ModName
name [Char]
"resolveAsmVar-False" LocSymbol
lx  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Maybe TyVar
GM.maybeAuxVar (forall a. Located a -> a
F.val LocSymbol
lx)


getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, LocSymbol, LocBareType)]
getAsmSigs :: ModName
-> ModName
-> Spec LocBareType LocSymbol
-> [(Bool, LocSymbol, LocBareType)]
getAsmSigs ModName
myName ModName
name Spec LocBareType LocSymbol
spec
  | ModName
myName forall a. Eq a => a -> a -> Bool
== ModName
name = [ (Bool
True,  LocSymbol
x,  LocBareType
t) | (LocSymbol
x, LocBareType
t) <- forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec LocBareType LocSymbol
spec ] -- MUST    resolve, or error
  | Bool
otherwise      = [ (Bool
False, LocSymbol
x', LocBareType
t) | (LocSymbol
x, LocBareType
t) <- forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.asmSigs Spec LocBareType LocSymbol
spec
                                                  forall a. [a] -> [a] -> [a]
++ forall ty bndr. Spec ty bndr -> [(LocSymbol, ty)]
Ms.sigs Spec LocBareType LocSymbol
spec
                                      , let x' :: LocSymbol
x' = forall {f :: * -> *}. Functor f => f Symbol -> f Symbol
qSym LocSymbol
x           ]  -- MAY-NOT resolve
  where
    qSym :: f Symbol -> f Symbol
qSym           = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol -> Symbol -> Symbol
GM.qualifySymbol Symbol
ns)
    ns :: Symbol
ns             = 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  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {b}. RInstance b -> [(LocSymbol, b)]
go
  where
    go :: RInstance b -> [(LocSymbol, b)]
go    RInstance b
xts              = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe forall {f :: * -> *} {b}.
Functor f =>
(f Symbol, RISig b) -> Maybe (f Symbol, b)
goOne (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) = forall a. a -> Maybe a
Just (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
".$c" forall a. [a] -> [a] -> [a]
++ ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> [Char]
F.symbolString) f Symbol
x, b
t)
    goOne (f Symbol
_, RISig 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 LocBareType LocSymbol)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec LocBareType LocSymbol)]
specs = do
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, DataDecl)]
nameDecls forall a b. (a -> b) -> a -> b
$ 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 LocBareType LocSymbol
spec) <- [(ModName, Spec LocBareType LocSymbol)]
specs, DataDecl
d <- forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.newtyDecls Spec LocBareType 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return [(TyCon
tc, LocSpecType
lst)]
    Maybe TyCon
_       -> 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 -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name forall v. PlugTV v
Bare.GenTV LocBareType
bt
    bt :: LocBareType
bt                        = forall {a}. PPrint a => a -> SourcePos -> [DataCtor] -> LocBareType
getTy DataName
tcName (DataDecl -> SourcePos
tycSrcPos DataDecl
d) (forall a. a -> Maybe a -> a
Mb.fromMaybe [] (DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
d))
    getTy :: a -> SourcePos -> [DataCtor] -> LocBareType
getTy a
_ SourcePos
l [DataCtor
c]
      | [(Symbol
_, RType BTyCon BTyVar RReft
t)] <- DataCtor -> [(Symbol, RType BTyCon BTyVar RReft)]
dcFields DataCtor
c = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l RType BTyCon BTyVar RReft
t
    getTy a
n SourcePos
l [DataCtor]
_                = forall a e. Exception e => e -> a
Ex.throw (forall {a}. PPrint a => a -> SourcePos -> UserError
mkErr a
n SourcePos
l)
    mkErr :: a -> SourcePos -> UserError
mkErr a
n SourcePos
l                  = forall t. SrcSpan -> Doc -> TError t
ErrOther (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (Doc
"Bad new type declaration:" Doc -> Doc -> 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 LocBareType LocSymbol)
-> GhcSpecData
makeSpecData GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
sig HashMap ModName (Spec LocBareType LocSymbol)
specs = SpData
  { gsCtors :: [(TyVar, LocSpecType)]
gsCtors      = 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 forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig Env
env) SigEnv
sigEnv ModName
name (forall v. v -> PlugTV v
Bare.LqTV TyVar
x) LocSpecType
t
                   ]
  , gsMeas :: [(Symbol, LocSpecType)]
gsMeas       = [ (forall a. Symbolic a => a -> Symbol
F.symbol Symbol
x, forall c tv a. RType c tv a -> RType c tv (UReft a)
uRType 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   = forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Measure SpecType DataCon]
ms1 forall a. [a] -> [a] -> [a]
++ [Measure SpecType DataCon]
ms2)
  , gsInvariants :: [(Maybe TyVar, LocSpecType)]
gsInvariants = forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (forall a. Located a -> SourcePos
F.loc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Maybe TyVar, LocSpecType)]
invs
  , gsIaliases :: [(LocSpecType, LocSpecType)]
gsIaliases   = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName, Spec LocBareType LocSymbol)
-> [(LocSpecType, LocSpecType)]
makeIAliases Env
env SigEnv
sigEnv) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
  , gsUnsorted :: [UnSortedExpr]
gsUnsorted   = [UnSortedExpr]
usI forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ty ctor. Measure ty ctor -> [UnSortedExpr]
msUnSorted (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall ty bndr. Spec ty bndr -> [Measure ty bndr]
measures HashMap ModName (Spec LocBareType LocSymbol)
specs)
  }
  where
    allowTC :: Bool
allowTC      = Config -> Bool
typeclass (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'
                forall a. [a] -> [a] -> [a]
++ MeasEnv -> [(Symbol, Located (RRType Reft))]
Bare.meClassSyms MeasEnv
measEnv -- cms'
                forall a. [a] -> [a] -> [a]
++ 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          = forall k v. HashMap k v -> [v]
M.elems (forall ty ctor.
MSpec ty ctor -> HashMap LocSymbol (Measure ty ctor)
Ms.measMap MSpec SpecType DataCon
measuresSp)
    ms2 :: [Measure SpecType DataCon]
ms2          = forall ty ctor. MSpec ty ctor -> [Measure ty ctor]
Ms.imeas   MSpec SpecType DataCon
measuresSp
    mySpec :: Spec LocBareType LocSymbol
mySpec       = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
    name :: ModName
name         = GhcSrc -> ModName
_giTargetMod      GhcSrc
src
    ([(Maybe TyVar, LocSpecType)]
minvs,[UnSortedExpr]
usI)  = Env
-> ModName
-> GhcSpecSig
-> Spec LocBareType LocSymbol
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants Env
env ModName
name GhcSpecSig
sig Spec LocBareType LocSymbol
mySpec
    invs :: [(Maybe TyVar, LocSpecType)]
invs         = [(Maybe TyVar, LocSpecType)]
minvs forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Env
-> SigEnv
-> (ModName, Spec LocBareType LocSymbol)
-> [(Maybe TyVar, LocSpecType)]
makeInvariants Env
env SigEnv
sigEnv) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)

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

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

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

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

isSymbolOfVar :: Symbol -> Ghc.Var -> Bool
isSymbolOfVar :: Symbol -> TyVar -> Bool
isSymbolOfVar Symbol
x TyVar
v = Symbol
x 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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))
  = forall a. PPrint a => [Char] -> a -> a
notracepp [Char]
"measureTypeToInv" ((forall a. a -> Maybe a
Just TyVar
v, LocSpecType
t {val :: SpecType
val = forall a. Qualify a => Env -> ModName -> SourcePos -> a -> a
Bare.qualifyTop Env
env ModName
name (forall a. Located a -> SourcePos
F.loc LocSymbol
x) SpecType
mtype}), Maybe UnSortedExpr
usorted)
  where
    trep :: RTypeRep RTyCon RTyVar RReft
trep = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep (forall a. Located a -> a
val LocSpecType
t)
    rts :: [SpecType]
rts  = forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
trep
    args :: [Symbol]
args = forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
trep
    res :: SpecType
res  = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res   RTypeRep RTyCon RTyVar RReft
trep
    z :: Symbol
z    = forall a. [a] -> a
last [Symbol]
args
    tz :: SpecType
tz   = forall a. [a] -> a
last [SpecType]
rts
    usorted :: Maybe UnSortedExpr
usorted = if forall {c} {tv} {r}. RType c tv r -> Bool
isSimpleADT SpecType
tz then forall a. Maybe a
Nothing else forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (forall a. a -> [a] -> [a]
:[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft (forall a. a -> Located a
dummyLoc forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v) Symbol
z SpecType
tz SpecType
res
    mtype :: SpecType
mtype
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecType]
rts
      = forall a. UserError -> a
uError forall a b. (a -> b) -> a -> b
$ forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc LocSpecType
t) (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
_) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all 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 = forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen (forall r. Reftable r => r -> r
top forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t) (forall r. r -> Predicate -> UReft r
MkUReft Reft
reft' forall a. Monoid a => a
mempty)
      where
        reft' :: Reft
reft' = forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe 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 <- forall c tv r. RType c tv r -> Maybe r
stripRTypeBase SpecType
tr
  = let Reft (Symbol
v, Expr
p) = 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  forall a. a -> Maybe a
Just (Symbol
v, forall a. Subable a => Subst -> a -> a
subst Subst
su Expr
p)
mkReft LocSymbol
_ Symbol
_ SpecType
_ SpecType
_
  = 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   = [ forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dc (DataConP -> DataCon
dcpCon DataConP
dc) | DataConP
dc <- [DataConP]
datacons forall a. [a] -> [a] -> [a]
++ [DataConP]
cls ]
  , gsTconsP :: [TyConP]
gsTconsP   = forall a. Qualify a => Env -> ModName -> a -> a
Bare.qualifyTopDummy Env
env ModName
name 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        = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"meClasses" 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 LocBareType LocSymbol
-> HashMap ModName (Spec LocBareType LocSymbol)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0 Config
cfg ModName
myName Env
env TCEmb TyCon
embs Spec LocBareType LocSymbol
mySpec HashMap ModName (Spec LocBareType LocSymbol)
iSpecs = (Diagnostics
diag0 forall a. Semigroup a => a -> a -> a
<> Diagnostics
diag1, [Located DataConP]
datacons, Bare.TycEnv
  { tcTyCons :: [TyConP]
tcTyCons      = [TyConP]
tycons
  , tcDataCons :: [DataConP]
tcDataCons    = forall a. Monoid a => a
mempty -- val <$> datacons
  , tcSelMeasures :: [Measure SpecType DataCon]
tcSelMeasures = [Measure SpecType DataCon]
dcSelectors
  , tcSelVars :: [(TyVar, LocSpecType)]
tcSelVars     = 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) = forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics forall a b. (a -> b) -> a -> b
$ ModName
-> Env
-> [(ModName, Spec LocBareType LocSymbol)]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes ModName
myName Env
env [(ModName, Spec LocBareType LocSymbol)]
specs
    specs :: [(ModName, Spec LocBareType LocSymbol)]
specs         = (ModName
myName, Spec LocBareType LocSymbol
mySpec) forall a. a -> [a] -> [a]
: forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
iSpecs
    tcs :: [TyConP]
tcs           = forall a b c. (a, b, c) -> b
Misc.snd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, TyConP, Maybe DataPropDecl)]
tcDds
    tyi :: TyConMap
tyi           = 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Located DataConP]]
dcs 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   = 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
charDataConforall 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Located DataConP]
classdcs forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr)
-> DataConP
-> TcRn (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 forall a. [a] -> [a] -> [a]
++ (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a b. (a, b) -> b
snd [Located (DataConP, DataConP)]
lclassdcs)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    TycEnv
tycEnv {tcSelVars :: [(TyVar, LocSpecType)]
Bare.tcSelVars = [(TyVar, LocSpecType)]
recSelectors, tcDataCons :: [DataConP]
Bare.tcDataCons = forall a. Located a -> a
F.val forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) forall a b. (a, b) -> a
fst [Located (DataConP, DataConP)]
lclassdcs forall a. [a] -> [a] -> [a]
++ [Located DataConP]
dcs )}
  where
    ([Located DataConP]
classdcs, [Located DataConP]
dcs) =
      forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition
        (TyCon -> Bool
Ghc.isClassTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> TyCon
Ghc.dataConTyCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val

knownWiredTyCons :: Bare.Env -> ModName -> [TyConP]
knownWiredTyCons :: Env -> ModName -> [TyConP]
knownWiredTyCons Env
env ModName
name = 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol 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 LocBareType LocSymbol)
-> Lookup MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv HashMap ModName (Spec LocBareType LocSymbol)
specs = do
  [(Class, [(ModName, TyVar, LocSpecType)])]
laws        <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup [(Class, [(ModName, TyVar, LocSpecType)])]
Bare.makeCLaws Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec LocBareType LocSymbol)
specs
  ([DataConP]
cls, [(ModName, TyVar, LocSpecType)]
mts)  <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec LocBareType LocSymbol)
-> Lookup ([DataConP], [(ModName, TyVar, LocSpecType)])
Bare.makeClasses        Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec LocBareType 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   <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env
-> SigEnv
-> ModName
-> (ModName, Spec LocBareType LocSymbol)
-> Lookup (MSpec SpecType DataCon)
Bare.makeMeasureSpec Env
env SigEnv
sigEnv ModName
name) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec LocBareType LocSymbol)
specs)
  let measures :: MSpec SpecType DataCon
measures = forall a. Monoid a => [a] -> a
mconcat (forall ctor ty. Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor
Ms.mkMSpec' [Measure SpecType DataCon]
dcSelectors 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 forall a b. (a -> b) -> a -> b
$ forall t. HasConfig t => t -> Config
getConfig Env
env)   MSpec SpecType DataCon
measures
  let cms :: [(LocSymbol, CMeasure (RRType Reft))]
cms      = 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, forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' forall a b. (a -> b) -> a -> b
$ 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'      = [ (forall a. Located a -> a
F.val LocSymbol
lx, 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
                                            , forall a. Maybe a -> Bool
Mb.isNothing (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (forall a. Located a -> a
val LocSymbol
lx) [(Symbol, Located (RRType Reft))]
cms') ]
  let cs' :: [(TyVar, LocSpecType)]
cs'      = [ (TyVar
v, 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 (forall t. HasConfig t => t -> Config
getConfig Env
env)) TCEmb TyCon
embs [(TyVar, SpecType)]
cs ([DataConP]
datacons forall a. [a] -> [a] -> [a]
++ [DataConP]
cls)]
  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 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 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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 LocBareType LocSymbol
-> Spec LocBareType LocSymbol
makeLiftedSpec ModName
name GhcSrc
src Env
_env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
sig GhcSpecQual
qual BareRTEnv
myRTE Spec LocBareType LocSymbol
lSpec0 = Spec LocBareType LocSymbol
lSpec0
  { asmSigs :: [(LocSymbol, LocBareType)]
Ms.asmSigs    = forall a. PPrint a => [Char] -> a -> a
F.notracepp   ([Char]
"makeLiftedSpec : ASSUMED-SIGS " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name ) ([(LocSymbol, LocBareType)]
xbs forall a. [a] -> [a] -> [a]
++ [(LocSymbol, LocBareType)]
myDCs)
  , reflSigs :: [(LocSymbol, LocBareType)]
Ms.reflSigs   = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"REFL-SIGS"         [(LocSymbol, LocBareType)]
xbs
  , sigs :: [(LocSymbol, LocBareType)]
Ms.sigs       = forall a. PPrint a => [Char] -> a -> a
F.notracepp   ([Char]
"makeLiftedSpec : LIFTED-SIGS " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp ModName
name )  forall a b. (a -> b) -> a -> b
$ forall {f :: * -> *}.
Functor f =>
[(TyVar, f SpecType)]
-> [(LocSymbol, f (RType BTyCon BTyVar RReft))]
mkSigs (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
sig)
  , invariants :: [(Maybe LocSymbol, LocBareType)]
Ms.invariants = [ (TyVar -> LocSymbol
varLocSym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe TyVar
x, SpecType -> RType BTyCon BTyVar RReft
Bare.specToBare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LocSpecType
t)
                       | (Maybe TyVar
x, LocSpecType
t) <- GhcSpecData -> [(Maybe TyVar, LocSpecType)]
gsInvariants GhcSpecData
sData
                       , forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF LocSpecType
t
                    ]
  , axeqs :: [Equation]
Ms.axeqs      = GhcSpecRefl -> [Equation]
gsMyAxioms GhcSpecRefl
refl
  , aliases :: [Located BareRTAlias]
Ms.aliases    = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"MY-ALIASES" forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [v]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases forall a b. (a -> b) -> a -> b
$ BareRTEnv
myRTE
  , ealiases :: [Located (RTAlias Symbol Expr)]
Ms.ealiases   = forall k v. HashMap k v -> [v]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases forall a b. (a -> b) -> a -> b
$ BareRTEnv
myRTE
  , qualifiers :: [Qualifier]
Ms.qualifiers = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF) (GhcSpecQual -> [Qualifier]
gsQualifiers GhcSpecQual
qual)
  }
  where
    myDCs :: [(LocSymbol, LocBareType)]
myDCs         = [(LocSymbol
x,LocBareType
t) | (LocSymbol
x,LocBareType
t) <- forall {f :: * -> *}.
Functor f =>
[(TyVar, f SpecType)]
-> [(LocSymbol, f (RType BTyCon BTyVar RReft))]
mkSigs (GhcSpecData -> [(TyVar, LocSpecType)]
gsCtors GhcSpecData
sData)
                           , forall a. Symbolic a => a -> Symbol
F.symbol ModName
name forall a. Eq a => a -> a -> Bool
== forall a b. (a, b) -> a
fst (Symbol -> (Symbol, Symbol)
GM.splitModuleName forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val LocSymbol
x)]
    mkSigs :: [(TyVar, f SpecType)]
-> [(LocSymbol, f (RType BTyCon BTyVar RReft))]
mkSigs [(TyVar, f SpecType)]
xts    = [ forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (LocSymbol, f (RType BTyCon BTyVar RReft))
toBare (TyVar
x, f SpecType
t) | (TyVar
x, f SpecType
t) <- [(TyVar, f SpecType)]
xts
                    ,  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 (RType BTyCon BTyVar RReft))
toBare (TyVar
x, f SpecType
t) = (TyVar -> LocSymbol
varLocSym TyVar
x, SpecType -> RType BTyCon BTyVar RReft
Bare.specToBare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f SpecType
t)
    xbs :: [(LocSymbol, LocBareType)]
xbs           = forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (LocSymbol, f (RType BTyCon BTyVar RReft))
toBare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
reflTySigs
    sigVars :: HashSet TyVar
sigVars       = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet TyVar
defVars HashSet TyVar
reflVars
    defVars :: HashSet TyVar
defVars       = 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` GhcSpecRefl -> [TyVar]
gsWiredReft GhcSpecRefl
refl]
    reflVars :: HashSet TyVar
reflVars      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a b. (a, b) -> a
fst 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 forall a. Eq a => a -> a -> Bool
== [Char]
lifted Bool -> Bool -> Bool
|| Bool
isCompanion
  where
    lifted :: FilePath
    lifted :: [Char]
lifted = forall a. Loc a => a -> [Char]
locFile a
lx

    isCompanion :: Bool
    isCompanion :: Bool
isCompanion =
      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 = forall a b c. (a, b, c) -> a
Misc.fst3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourcePos -> ([Char], Line, Line)
F.sourcePosElts forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> SourcePos
F.sp_start forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Loc a => a -> SrcSpan
F.srcSpan

varLocSym :: Ghc.Var -> LocSymbol
varLocSym :: TyVar -> LocSymbol
varLocSym TyVar
v = forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BareRTAlias]
tAs
    tAs :: [Located BareRTAlias]
tAs                      = forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases
    eAs :: [Located (RTAlias Symbol Expr)]
eAs                      = forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases 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            = forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. HashMap k v -> [v]
M.elems forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> HashMap k a
fld 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 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (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 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (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   = forall x a. RTAlias x a -> Symbol
rtName forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Located BareRTAlias
lx
  where
    fixRTA  :: BareRTAlias -> BareRTAlias
    fixRTA :: BareRTAlias -> BareRTAlias
fixRTA  = forall a b ty. (a -> b) -> RTAlias a ty -> RTAlias b ty
mapRTAVars Symbol -> Symbol
fixArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RType BTyCon BTyVar RReft -> RType BTyCon BTyVar RReft
fixBody

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

    fixBody :: BareType -> BareType
    fixBody :: RType BTyCon BTyVar RReft -> RType BTyCon BTyVar RReft
fixBody = SpecType -> RType BTyCon BTyVar RReft
Bare.specToBare
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
F.val
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> SigEnv -> ModName -> PlugTV TyVar -> LocBareType -> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name forall v. PlugTV v
Bare.RawTV
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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, forall a. Monoid a => a
mempty)
withDiagnostics (Right a
v) = (Diagnostics
emptyDiagnostics, a
v)