{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE LambdaCase                #-}
{-# 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
  ) where

import           Control.Monad                              (forM, mplus, when)
import qualified Control.Exception                          as Ex
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           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.LHNameResolution
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.PredType
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Visitors
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.Resolve       as Resolve
import qualified Language.Haskell.Liquid.Bare.Typeclass     as Bare
import qualified Language.Haskell.Liquid.Transforms.CoreToLogic as CoreToLogic
import           Language.Haskell.Liquid.UX.Config
import Data.Hashable (Hashable)
import Data.Bifunctor (bimap, first)
import Data.Function (on)


{- $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
               -> Bare.LocalVars
               -> LogicNameEnv
               -> LogicMap
               -> TargetSrc
               -> BareSpec
               -> TargetDependencies
               -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec :: Config
-> LocalVars
-> LogicNameEnv
-> LogicMap
-> TargetSrc
-> Spec Symbol BareType
-> TargetDependencies
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec Config
cfg LocalVars
localVars LogicNameEnv
lnameEnv LogicMap
lmap TargetSrc
targetSrc Spec Symbol BareType
bareSpec TargetDependencies
dependencies = do
  let targDiagnostics :: Either Diagnostics ()
targDiagnostics     = Config -> TargetSrc -> Either Diagnostics ()
Bare.checkTargetSrc Config
cfg TargetSrc
targetSrc
  let depsDiagnostics :: Either Diagnostics [()]
depsDiagnostics     = ((ModName, Spec Symbol BareType) -> Either Diagnostics ())
-> [(ModName, Spec Symbol BareType)] -> Either Diagnostics [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Spec Symbol BareType -> Either Diagnostics ()
Bare.checkBareSpec (Spec Symbol BareType -> Either Diagnostics ())
-> ((ModName, Spec Symbol BareType) -> Spec Symbol BareType)
-> (ModName, Spec Symbol BareType)
-> Either Diagnostics ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec Symbol BareType) -> Spec Symbol BareType
forall a b. (a, b) -> b
snd) [(ModName, Spec Symbol BareType)]
legacyDependencies
  let bareSpecDiagnostics :: Either Diagnostics ()
bareSpecDiagnostics = Spec Symbol BareType -> Either Diagnostics ()
Bare.checkBareSpec Spec Symbol BareType
bareSpec
  case Either Diagnostics ()
targDiagnostics Either Diagnostics ()
-> Either Diagnostics [()] -> Either Diagnostics [()]
forall a b.
Either Diagnostics a
-> Either Diagnostics b -> Either Diagnostics b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics [()]
depsDiagnostics Either Diagnostics [()]
-> Either Diagnostics () -> Either Diagnostics ()
forall a b.
Either Diagnostics a
-> Either Diagnostics b -> Either Diagnostics b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Either Diagnostics ()
bareSpecDiagnostics of
   Left Diagnostics
d | Diagnostics -> Bool
noErrors Diagnostics
d -> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase (Diagnostics -> [Warning]
allWarnings Diagnostics
d)
   Left Diagnostics
d              -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
 -> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)))
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a b. (a -> b) -> a -> b
$ Diagnostics
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
forall a b. a -> Either a b
Left Diagnostics
d
   Right ()            -> [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase [Warning]
forall a. Monoid a => a
mempty
  where
    secondPhase :: [Warning] -> Ghc.TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
    secondPhase :: [Warning]
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
secondPhase [Warning]
phaseOneWarns = do
      diagOrSpec <- Config
-> LogicNameEnv
-> LocalVars
-> GhcSrc
-> LogicMap
-> Spec Symbol BareType
-> [(ModName, Spec Symbol BareType)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg LogicNameEnv
lnameEnv LocalVars
localVars (TargetSrc -> GhcSrc
fromTargetSrc TargetSrc
targetSrc) LogicMap
lmap Spec Symbol BareType
bareSpec [(ModName, Spec Symbol BareType)]
legacyDependencies
      case diagOrSpec of
        Left Diagnostics
d -> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
 -> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)))
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
forall a b. (a -> b) -> a -> b
$ Diagnostics
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
forall a b. a -> Either a b
Left Diagnostics
d
        Right ([Warning]
warns, GhcSpec
ghcSpec) -> do
          let targetSpec :: TargetSpec
targetSpec = GhcSpec -> TargetSpec
toTargetSpec GhcSpec
ghcSpec
              liftedSpec :: LiftedSpec
liftedSpec = GhcSpec -> LiftedSpec
ghcSpecToLiftedSpec GhcSpec
ghcSpec
          liftedSpec' <- LiftedSpec -> TcRn LiftedSpec
removeUnexportedLocalAssumptions LiftedSpec
liftedSpec
          return $ Right (phaseOneWarns <> warns, targetSpec, liftedSpec')

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

    legacyDependencies :: [(ModName, BareSpec)]
    legacyDependencies :: [(ModName, Spec Symbol BareType)]
legacyDependencies =
      -- Dependencies are sorted lexicographically to make predictable which
      -- logic names will have preference when exporting conflicting measures.
      --
      -- At the moment it is the measure from the last module after sorting.
      -- But if there is a local conflicting measure, that one is used.
      ((ModName, Spec Symbol BareType) -> ModName)
-> [(ModName, Spec Symbol BareType)]
-> [(ModName, Spec Symbol BareType)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn (ModName, Spec Symbol BareType) -> ModName
forall a b. (a, b) -> a
fst ([(ModName, Spec Symbol BareType)]
 -> [(ModName, Spec Symbol BareType)])
-> [(ModName, Spec Symbol BareType)]
-> [(ModName, Spec Symbol BareType)]
forall a b. (a -> b) -> a -> b
$ ((StableModule, LiftedSpec) -> (ModName, Spec Symbol BareType))
-> [(StableModule, LiftedSpec)]
-> [(ModName, Spec Symbol BareType)]
forall a b. (a -> b) -> [a] -> [b]
map (StableModule, LiftedSpec) -> (ModName, Spec Symbol BareType)
toLegacyDep ([(StableModule, LiftedSpec)] -> [(ModName, Spec Symbol BareType)])
-> [(StableModule, LiftedSpec)]
-> [(ModName, Spec Symbol BareType)]
forall a b. (a -> b) -> a -> b
$ HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)])
-> HashMap StableModule LiftedSpec -> [(StableModule, LiftedSpec)]
forall a b. (a -> b) -> a -> b
$ TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies TargetDependencies
dependencies

    -- Assumptions about local functions that are not exported aren't useful for
    -- other modules.
    removeUnexportedLocalAssumptions :: LiftedSpec -> Ghc.TcRn LiftedSpec
    removeUnexportedLocalAssumptions :: LiftedSpec -> TcRn LiftedSpec
removeUnexportedLocalAssumptions LiftedSpec
lspec = do
      tcg <- TcRnIf TcGblEnv TcLclEnv TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
Ghc.getGblEnv
      let exportedNames = [AvailInfo] -> NameSet
Ghc.availsToNameSet (TcGblEnv -> [AvailInfo]
Ghc.tcg_exports TcGblEnv
tcg)
          exportedAssumption (LHNResolved (LHRGHC Name
n) Symbol
_) =
            case Name -> Maybe (GenModule Unit)
Ghc.nameModule_maybe Name
n of
              Maybe (GenModule Unit)
Nothing -> Name -> NameSet -> Bool
Ghc.elemNameSet Name
n NameSet
exportedNames
              Just GenModule Unit
m -> GenModule Unit
m GenModule Unit -> GenModule Unit -> Bool
forall a. Eq a => a -> a -> Bool
/= TcGblEnv -> GenModule Unit
Ghc.tcg_mod TcGblEnv
tcg Bool -> Bool -> Bool
|| Name -> NameSet -> Bool
Ghc.elemNameSet Name
n NameSet
exportedNames
          exportedAssumption LHName
_ = Bool
True
      return lspec { liftedAsmSigs = S.filter (exportedAssumption . val . fst) (liftedAsmSigs lspec) }

    ghcSpecToLiftedSpec :: GhcSpec -> LiftedSpec
ghcSpecToLiftedSpec = BareSpecLHName -> LiftedSpec
toLiftedSpec (BareSpecLHName -> LiftedSpec)
-> (GhcSpec -> BareSpecLHName) -> GhcSpec -> LiftedSpec
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> LogicNameEnv -> Spec Symbol BareType -> BareSpecLHName
toBareSpecLHName Config
cfg LogicNameEnv
lnameEnv (Spec Symbol BareType -> BareSpecLHName)
-> (GhcSpec -> Spec Symbol BareType) -> GhcSpec -> BareSpecLHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GhcSpec -> Spec Symbol BareType
_gsLSpec


-------------------------------------------------------------------------------------
-- | @makeGhcSpec@ invokes @makeGhcSpec0@ to construct the @GhcSpec@ and then
--   validates it using @checkGhcSpec@.
-------------------------------------------------------------------------------------
makeGhcSpec :: Config
            -> LogicNameEnv
            -> Bare.LocalVars
            -> GhcSrc
            -> LogicMap
            -> Ms.BareSpec
            -> [(ModName, Ms.BareSpec)]
            -> Ghc.TcRn (Either Diagnostics ([Warning], GhcSpec))
-------------------------------------------------------------------------------------
makeGhcSpec :: Config
-> LogicNameEnv
-> LocalVars
-> GhcSrc
-> LogicMap
-> Spec Symbol BareType
-> [(ModName, Spec Symbol BareType)]
-> TcRn (Either Diagnostics ([Warning], GhcSpec))
makeGhcSpec Config
cfg LogicNameEnv
lenv LocalVars
localVars GhcSrc
src LogicMap
lmap Spec Symbol BareType
targetSpec [(ModName, Spec Symbol BareType)]
dependencySpecs = do
  ghcTyLookupEnv <- CoreProgram -> TcRn GHCTyLookupEnv
Bare.makeGHCTyLookupEnv (GhcSrc -> CoreProgram
_giCbs GhcSrc
src)
  tcg <- Ghc.getGblEnv
  instEnvs <- Ghc.tcGetInstEnvs
  (dg0, sp) <- makeGhcSpec0 cfg ghcTyLookupEnv tcg instEnvs lenv localVars src lmap targetSpec dependencySpecs
  let diagnostics = [Spec Symbol BareType]
-> TargetSrc
-> SEnv SortedReft
-> CoreProgram
-> TargetSpec
-> Either Diagnostics ()
Bare.checkTargetSpec (Spec Symbol BareType
targetSpec Spec Symbol BareType
-> [Spec Symbol BareType] -> [Spec Symbol BareType]
forall a. a -> [a] -> [a]
: ((ModName, Spec Symbol BareType) -> Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)] -> [Spec Symbol BareType]
forall a b. (a -> b) -> [a] -> [b]
map (ModName, Spec Symbol BareType) -> Spec Symbol BareType
forall a b. (a, b) -> b
snd [(ModName, Spec Symbol BareType)]
dependencySpecs)
                                         (GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src)
                                         (GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp)
                                         (GhcSrc -> CoreProgram
_giCbs GhcSrc
src)
                                         (GhcSpec -> TargetSpec
toTargetSpec GhcSpec
sp)
  pure $ if not (noErrors dg0) then Left dg0 else
           case diagnostics of
             Left Diagnostics
dg1
               | Diagnostics -> Bool
noErrors Diagnostics
dg1 -> ([Warning], GhcSpec) -> Either Diagnostics ([Warning], GhcSpec)
forall a. a -> Either Diagnostics a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Diagnostics -> [Warning]
allWarnings Diagnostics
dg1, GhcSpec
sp)
               | Bool
otherwise    -> Diagnostics -> Either Diagnostics ([Warning], GhcSpec)
forall a b. a -> Either a b
Left Diagnostics
dg1
             Right ()         -> ([Warning], GhcSpec) -> Either Diagnostics ([Warning], GhcSpec)
forall a. a -> Either Diagnostics a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Warning]
forall a. Monoid a => a
mempty, GhcSpec
sp)


ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv :: GhcSpec -> SEnv SortedReft
ghcSpecEnv GhcSpec
sp = [Char] -> SEnv SortedReft -> SEnv SortedReft
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"RENV" (SEnv SortedReft -> SEnv SortedReft)
-> SEnv SortedReft -> SEnv SortedReft
forall a b. (a -> b) -> a -> b
$ [(Symbol, SortedReft)] -> SEnv SortedReft
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [(Symbol, SortedReft)]
binds
  where
    emb :: TCEmb TyCon
emb       = GhcSpecNames -> TCEmb TyCon
gsTcEmbeds (GhcSpec -> GhcSpecNames
_gsName GhcSpec
sp)
    binds :: [(Symbol, SortedReft)]
binds     = [Char] -> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"binds" ([(Symbol, SortedReft)] -> [(Symbol, SortedReft)])
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a b. (a -> b) -> a -> b
$ [[(Symbol, SortedReft)]] -> [(Symbol, SortedReft)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                 [ [(Symbol
x,        SpecType -> SortedReft
forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort SpecType
t) | (Symbol
x, Loc SourcePos
_ SourcePos
_ SpecType
t)  <- GhcSpecData -> [(Symbol, LocSpecType)]
gsMeas     (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
                 , [(TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v, SpecType -> SortedReft
forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort SpecType
t) | (TyVar
v, Loc SourcePos
_ SourcePos
_ SpecType
t)  <- GhcSpecData -> [(TyVar, LocSpecType)]
gsCtors    (GhcSpec -> GhcSpecData
_gsData GhcSpec
sp)]
                 , [(TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v, TyVar -> SortedReft
vSort TyVar
v) | TyVar
v               <- GhcSpecRefl -> [TyVar]
gsReflects (GhcSpec -> GhcSpecRefl
_gsRefl GhcSpec
sp)]
                 , [(Symbol
x, Sort -> ReftV Symbol -> SortedReft
RR Sort
s ReftV Symbol
forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)          <- [(Symbol, Sort)]
wiredSortedSyms       ]
                 , [(Symbol
x, Sort -> ReftV Symbol -> SortedReft
RR Sort
s ReftV Symbol
forall a. Monoid a => a
mempty)    | (Symbol
x, Sort
s)          <- GhcSpec -> [(Symbol, Sort)]
_gsImps GhcSpec
sp       ]
                 ]
    vSort :: TyVar -> SortedReft
vSort     = SpecType -> SortedReft
forall {r}.
(PPrint r, SubsTy RTyVar (RType RTyCon RTyVar ()) r, Reftable r,
 Reftable (RTProp RTyCon RTyVar r)) =>
RRType r -> SortedReft
rSort (SpecType -> SortedReft)
-> (TyVar -> SpecType) -> TyVar -> SortedReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> SpecType -> SpecType
forall c tv r. Bool -> RType c tv r -> RType c tv r
classRFInfoType (Config -> Bool
typeclass (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ GhcSpec -> Config
forall t. HasConfig t => t -> Config
getConfig GhcSpec
sp) (SpecType -> SpecType) -> (TyVar -> SpecType) -> TyVar -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                (Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType :: Ghc.Type -> SpecType) (Type -> SpecType) -> (TyVar -> Type) -> TyVar -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Type
Ghc.varType
    rSort :: RRType r -> SortedReft
rSort     = TCEmb TyCon -> RRType r -> SortedReft
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> SortedReft
rTypeSortedReft    TCEmb TyCon
emb


-------------------------------------------------------------------------------------
-- | @makeGhcSpec0@ slurps up all the relevant information needed to generate
--   constraints for a target module and packages them into a @GhcSpec@
--   See [NOTE] LIFTING-STAGES to see why we split into lSpec0, lSpec1, etc.
--   essentially, to get to the `BareRTEnv` as soon as possible, as thats what
--   lets us use aliases inside data-constructor definitions.
-------------------------------------------------------------------------------------
makeGhcSpec0
  :: Config
  -> Bare.GHCTyLookupEnv
  -> Ghc.TcGblEnv
  -> Ghc.InstEnvs
  -> LogicNameEnv
  -> Bare.LocalVars
  -> GhcSrc
  -> LogicMap
  -> Ms.BareSpec
  -> [(ModName, Ms.BareSpec)]
  -> Ghc.TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 :: Config
-> GHCTyLookupEnv
-> TcGblEnv
-> InstEnvs
-> LogicNameEnv
-> LocalVars
-> GhcSrc
-> LogicMap
-> Spec Symbol BareType
-> [(ModName, Spec Symbol BareType)]
-> TcRn (Diagnostics, GhcSpec)
makeGhcSpec0 Config
cfg GHCTyLookupEnv
ghcTyLookupEnv TcGblEnv
tcg InstEnvs
instEnvs LogicNameEnv
lenv LocalVars
localVars GhcSrc
src LogicMap
lmap Spec Symbol BareType
targetSpec [(ModName, Spec Symbol BareType)]
dependencySpecs = do
  globalRdrEnv <- TcGblEnv -> GlobalRdrEnv
Ghc.tcg_rdr_env (TcGblEnv -> GlobalRdrEnv)
-> TcRnIf TcGblEnv TcLclEnv TcGblEnv
-> IOEnv (Env TcGblEnv TcLclEnv) GlobalRdrEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcRnIf TcGblEnv TcLclEnv TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
Ghc.getGblEnv
  -- build up environments
  tycEnv <- makeTycEnv1 env (tycEnv0, datacons) coreToLg simplifier
  let tyi      = TycEnv -> TyConMap
Bare.tcTyConMap   TycEnv
tycEnv
  let sigEnv   = TCEmb TyCon
-> TyConMap -> HashSet StableName -> BareRTEnv -> SigEnv
makeSigEnv  TCEmb TyCon
embs TyConMap
tyi (GhcSrc -> HashSet StableName
_gsExports GhcSrc
src) BareRTEnv
rtEnv
  let lSpec1   = Config
-> GhcSrc
-> TycEnv
-> LogicMap
-> Spec Symbol BareType
-> Spec Symbol BareType
makeLiftedSpec1 Config
cfg GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec Symbol BareType
mySpec1
  let mySpec   = Spec Symbol BareType
mySpec2 Spec Symbol BareType
-> Spec Symbol BareType -> Spec Symbol BareType
forall a. Semigroup a => a -> a -> a
<> Spec Symbol BareType
lSpec1
  let specs    = ModName
-> Spec Symbol BareType
-> HashMap ModName (Spec Symbol BareType)
-> HashMap ModName (Spec Symbol BareType)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert ModName
name Spec Symbol BareType
mySpec HashMap ModName (Spec Symbol BareType)
iSpecs2
  let myRTE    = GhcSrc -> Env -> SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv       GhcSrc
src Env
env SigEnv
sigEnv BareRTEnv
rtEnv
  -- NB: we first compute a measure environment w/o the opaque reflections, so that we can bootstrap
  -- the signature `sig`. Then we'll add the opaque reflections before we compute `sData` and al.
  let (dg1, measEnv0) = withDiagnostics $ makeMeasEnv      env tycEnv sigEnv       specs
  let (dg2, (specInstances, sig)) = withDiagnostics $ makeSpecSig cfg name mySpec iSpecs2 env sigEnv tycEnv measEnv0 (_giCbs src)
  elaboratedSig <-
    if allowTC then Bare.makeClassAuxTypes (elaborateSpecType coreToLg simplifier) datacons instMethods
                              >>= elaborateSig sig
               else pure sig
  let (dg3, refl)    = withDiagnostics $ makeSpecRefl src specs env name elaboratedSig tycEnv
  let eqs            = GhcSpecRefl -> [(TyVar, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl
  let (dg4, measEnv) = withDiagnostics $ addOpaqueReflMeas cfg tycEnv env mySpec measEnv0 specs eqs
  let qual = Config
-> Env
-> GlobalRdrEnv
-> TycEnv
-> MeasEnv
-> BareRTEnv
-> Spec Symbol BareType
-> HashMap ModName (Spec Symbol BareType)
-> GhcSpecQual
makeSpecQual Config
cfg Env
env GlobalRdrEnv
globalRdrEnv TycEnv
tycEnv MeasEnv
measEnv BareRTEnv
rtEnv Spec Symbol BareType
mySpec HashMap ModName (Spec Symbol BareType)
iSpecs2
  let (dg5, spcVars) = withDiagnostics $ makeSpecVars cfg src mySpec env measEnv
  let (dg6, spcTerm) = withDiagnostics $ makeSpecTerm cfg     mySpec lenv env
  let sData    = GhcSrc
-> Env
-> SigEnv
-> MeasEnv
-> GhcSpecSig
-> HashMap ModName (Spec Symbol BareType)
-> GhcSpecData
makeSpecData  GhcSrc
src Env
env SigEnv
sigEnv MeasEnv
measEnv GhcSpecSig
elaboratedSig HashMap ModName (Spec Symbol BareType)
specs
  let finalLiftedSpec = ModName
-> GhcSrc
-> Env
-> GhcSpecRefl
-> GhcSpecData
-> GhcSpecSig
-> GhcSpecQual
-> BareRTEnv
-> Spec Symbol BareType
-> Spec Symbol BareType
makeLiftedSpec ModName
name GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
elaboratedSig GhcSpecQual
qual BareRTEnv
myRTE (Spec Symbol BareType
lSpec0 Spec Symbol BareType
-> Spec Symbol BareType -> Spec Symbol BareType
forall a. Semigroup a => a -> a -> a
<> Spec Symbol BareType
lSpec1)
  let diags    = [Diagnostics] -> Diagnostics
forall a. Monoid a => [a] -> a
mconcat [Diagnostics
dg0, Diagnostics
dg1, Diagnostics
dg2, Diagnostics
dg3, Diagnostics
dg4, Diagnostics
dg5, Diagnostics
dg6]

  -- Dump reflections, if requested
  when (dumpOpaqueReflections cfg) . Ghc.liftIO $ do
    putStrLn ""
    if L.null (Bare.meOpaqueRefl measEnv) then do
      putStrLn "No opaque reflection was generated."
    else do
      putStrLn "Opaque reflections: "
      let sortedRefls = [TyVar] -> [TyVar]
forall a. Ord a => [a] -> [a]
L.sort ([TyVar] -> [TyVar]) -> [TyVar] -> [TyVar]
forall a b. (a -> b) -> a -> b
$ (TyVar, Measure (Located BareType) (Located LHName)) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, Measure (Located BareType) (Located LHName)) -> TyVar)
-> [(TyVar, Measure (Located BareType) (Located LHName))]
-> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(TyVar, Measure (Located BareType) (Located LHName))]
Bare.meOpaqueRefl MeasEnv
measEnv
      mapM_ (putStrLn . ("- " ++) . show) sortedRefls
    putStrLn ""

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

    , _gsLSpec  = finalLiftedSpec
                { expSigs   =
                    [ (lhNameToResolvedSymbol $ reflectGHCName thisModule $ Ghc.getName v, F.sr_sort $ Bare.varSortedReft embs v)
                    | v <- gsReflects refl
                    ]
                , dataDecls = Bare.dataDeclSize mySpec $ dataDecls mySpec
                  -- Placing mySpec at the end causes local measures to take precedence over
                  -- imported measures when their names clash.
                , measures  = mconcat $ map Ms.measures $ map snd dependencySpecs ++ [mySpec]
                  -- We want to export measures in a 'LiftedSpec', especially if they are
                  -- required to check termination of some 'liftedSigs' we export. Due to the fact
                  -- that 'lSpec1' doesn't contain the measures that we compute via 'makeHaskellMeasures',
                  -- we take them from 'mySpec', which has those.
                , asmSigs = Ms.asmSigs finalLiftedSpec ++ Ms.asmSigs mySpec
                  -- Export all the assumptions (not just the ones created out of reflection) in
                  -- a 'LiftedSpec'.
                , omeasures = Ms.omeasures finalLiftedSpec ++ (snd <$> Bare.meOpaqueRefl measEnv)
                  -- Preserve 'o-measures': they are the opaque reflections
                , imeasures = Ms.imeasures finalLiftedSpec ++ Ms.imeasures mySpec
                  -- Preserve user-defined 'imeasures'.
                , dvariance = Ms.dvariance finalLiftedSpec ++ Ms.dvariance mySpec
                  -- Preserve user-defined 'dvariance'.
                , rinstance = specInstances
                  -- Preserve rinstances.
                , asmReflectSigs = Ms.asmReflectSigs mySpec
                , reflects = Ms.reflects mySpec0
                , cmeasures  = mconcat $ map Ms.cmeasures $ map snd dependencySpecs ++ [targetSpec]
                , embeds = Ms.embeds targetSpec
                , privateReflects = mconcat $ map (privateReflects . snd) mspecs
                , defines = Ms.defines targetSpec
                , usedDataCons = usedDcs
                }
    })
  where
    thisModule :: GenModule Unit
thisModule = TcGblEnv -> GenModule Unit
Ghc.tcg_mod TcGblEnv
tcg
    -- typeclass elaboration

    coreToLg :: CoreExpr -> Expr
coreToLg CoreExpr
ce =
      case TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> ([Char] -> Error)
-> LogicM Expr
-> Either Error Expr
forall t.
TCEmb TyCon
-> LogicMap
-> DataConMap
-> Config
-> ([Char] -> Error)
-> LogicM t
-> Either Error t
CoreToLogic.runToLogic
             TCEmb TyCon
embs
             LogicMap
lmap
             DataConMap
dm
             Config
cfg
             (\[Char]
x -> Maybe SrcSpan -> [Char] -> Error
forall a. Maybe SrcSpan -> [Char] -> a
todo Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"coreToLogic not working " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
x))
             (CoreExpr -> LogicM Expr
CoreToLogic.coreToLogic CoreExpr
ce) of
        Left Error
msg -> Maybe SrcSpan -> [Char] -> Expr
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (Error -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Error
msg)
        Right Expr
e -> Expr
e
    elaborateSig :: GhcSpecSig
-> [(TyVar, LocSpecType)]
-> IOEnv (Env TcGblEnv TcLclEnv) GhcSpecSig
elaborateSig GhcSpecSig
si [(TyVar, LocSpecType)]
auxsig = do
      tySigs <-
        [(TyVar, LocSpecType)]
-> ((TyVar, LocSpecType)
    -> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
-> TcRn [(TyVar, LocSpecType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
si) (((TyVar, LocSpecType)
  -> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
 -> TcRn [(TyVar, LocSpecType)])
-> ((TyVar, LocSpecType)
    -> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType))
-> TcRn [(TyVar, LocSpecType)]
forall a b. (a -> b) -> a -> b
$ \(TyVar
x, LocSpecType
t) ->
          if TyVar -> Bool
forall a. NamedThing a => a -> Bool
GM.isFromGHCReal TyVar
x then
            (TyVar, LocSpecType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TyVar, LocSpecType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar
x, LocSpecType
t)
          else do t' <- (SpecType -> TcRn SpecType)
-> LocSpecType -> IOEnv (Env TcGblEnv TcLclEnv) LocSpecType
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Located a -> f (Located b)
traverse ((CoreExpr -> Expr)
-> (CoreExpr -> TcRn CoreExpr) -> SpecType -> TcRn SpecType
elaborateSpecType CoreExpr -> Expr
coreToLg CoreExpr -> TcRn CoreExpr
simplifier) LocSpecType
t
                  pure (x, t')
      -- things like len breaks the code
      -- asmsigs should be elaborated only if they are from the current module
      -- asmSigs <- forM (gsAsmSigs si) $ \(x, t) -> do
      --   t' <- traverse (elaborateSpecType (pure ()) coreToLg) t
      --   pure (x, fst <$> t')
      pure
        si
          { gsTySigs = F.notracepp ("asmSigs" ++ F.showpp (gsAsmSigs si)) tySigs ++ auxsig  }

    simplifier :: Ghc.CoreExpr -> Ghc.TcRn Ghc.CoreExpr
    simplifier :: CoreExpr -> TcRn CoreExpr
simplifier = CoreExpr -> TcRn CoreExpr
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure -- no simplification
    allowTC :: Bool
allowTC  = Config -> Bool
typeclass Config
cfg
    mySpec2 :: Spec Symbol BareType
mySpec2  = BareRTEnv
-> SourcePos -> Spec Symbol BareType -> Spec Symbol BareType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
Bare.expand BareRTEnv
rtEnv ([Char] -> SourcePos
F.dummyPos [Char]
"expand-mySpec2") Spec Symbol BareType
mySpec1
    iSpecs2 :: HashMap ModName (Spec Symbol BareType)
iSpecs2  = BareRTEnv
-> SourcePos
-> HashMap ModName (Spec Symbol BareType)
-> HashMap ModName (Spec Symbol BareType)
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
Bare.expand BareRTEnv
rtEnv ([Char] -> SourcePos
F.dummyPos [Char]
"expand-iSpecs2") ([(ModName, Spec Symbol BareType)]
-> HashMap ModName (Spec Symbol BareType)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(ModName, Spec Symbol BareType)]
dependencySpecs)
    rtEnv :: BareRTEnv
rtEnv    = Env
-> ModName
-> Spec Symbol BareType
-> [(ModName, Spec Symbol BareType)]
-> LogicMap
-> BareRTEnv
Bare.makeRTEnv Env
env ModName
name Spec Symbol BareType
mySpec1 [(ModName, Spec Symbol BareType)]
dependencySpecs LogicMap
lmap
    mspecs :: [(ModName, Spec Symbol BareType)]
mspecs   = (ModName
name, Spec Symbol BareType
mySpec0) (ModName, Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
-> [(ModName, Spec Symbol BareType)]
forall a. a -> [a] -> [a]
: [(ModName, Spec Symbol BareType)]
dependencySpecs
    (Spec Symbol BareType
mySpec0, [(ClsInst, [TyVar])]
instMethods)  = if Bool
allowTC
                              then GhcSrc
-> Env
-> (ModName, Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
-> (Spec Symbol BareType, [(ClsInst, [TyVar])])
Bare.compileClasses GhcSrc
src Env
env (ModName
name, Spec Symbol BareType
targetSpec) [(ModName, Spec Symbol BareType)]
dependencySpecs
                              else (Spec Symbol BareType
targetSpec, [])
    mySpec1 :: Spec Symbol BareType
mySpec1  = Spec Symbol BareType
mySpec0 Spec Symbol BareType
-> Spec Symbol BareType -> Spec Symbol BareType
forall a. Semigroup a => a -> a -> a
<> Spec Symbol BareType
lSpec0
    lSpec0 :: Spec Symbol BareType
lSpec0   = Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec Symbol BareType
-> Spec Symbol BareType
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec Symbol BareType
mySpec0
    embs :: TCEmb TyCon
embs     = GhcSrc -> GHCTyLookupEnv -> [Spec Symbol BareType] -> TCEmb TyCon
makeEmbeds          GhcSrc
src GHCTyLookupEnv
ghcTyLookupEnv (Spec Symbol BareType
mySpec0 Spec Symbol BareType
-> [Spec Symbol BareType] -> [Spec Symbol BareType]
forall a. a -> [a] -> [a]
: ((ModName, Spec Symbol BareType) -> Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)] -> [Spec Symbol BareType]
forall a b. (a -> b) -> [a] -> [b]
map (ModName, Spec Symbol BareType) -> Spec Symbol BareType
forall a b. (a, b) -> b
snd [(ModName, Spec Symbol BareType)]
dependencySpecs)
    dm :: DataConMap
dm       = TycEnv -> DataConMap
Bare.tcDataConMap TycEnv
tycEnv0
    (Diagnostics
dg0, [Located DataConP]
datacons, TycEnv
tycEnv0) = Config
-> ModName
-> Env
-> TCEmb TyCon
-> Spec Symbol BareType
-> HashMap ModName (Spec Symbol BareType)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0   Config
cfg ModName
name Env
env TCEmb TyCon
embs Spec Symbol BareType
mySpec2 HashMap ModName (Spec Symbol BareType)
iSpecs2
    env :: Env
env      = Config
-> GHCTyLookupEnv
-> [TyVar]
-> TcGblEnv
-> InstEnvs
-> LocalVars
-> GhcSrc
-> LogicMap
-> [(ModName, Spec Symbol BareType)]
-> Env
Bare.makeEnv Config
cfg GHCTyLookupEnv
ghcTyLookupEnv [TyVar]
dataConIds TcGblEnv
tcg InstEnvs
instEnvs LocalVars
localVars GhcSrc
src LogicMap
lmap ((ModName
name, Spec Symbol BareType
targetSpec) (ModName, Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
-> [(ModName, Spec Symbol BareType)]
forall a. a -> [a] -> [a]
: [(ModName, Spec Symbol BareType)]
dependencySpecs)
    -- check barespecs
    name :: ModName
name     = [Char] -> ModName -> ModName
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"ALL-SPECS" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
zzz) (ModName -> ModName) -> ModName -> ModName
forall a b. (a -> b) -> a -> b
$ GhcSrc -> ModName
_giTargetMod  GhcSrc
src
    zzz :: [Char]
zzz      = [ModName] -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp ((ModName, Spec Symbol BareType) -> ModName
forall a b. (a, b) -> a
fst ((ModName, Spec Symbol BareType) -> ModName)
-> [(ModName, Spec Symbol BareType)] -> [ModName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, Spec Symbol BareType)]
mspecs)

    usedDcs :: HashSet LHName
usedDcs  = CoreProgram -> [Spec Symbol BareType] -> HashSet LHName
collectAllDataCons (GhcSrc -> CoreProgram
_giCbs GhcSrc
src) ([Spec Symbol BareType] -> HashSet LHName)
-> [Spec Symbol BareType] -> HashSet LHName
forall a b. (a -> b) -> a -> b
$ Spec Symbol BareType
targetSpec Spec Symbol BareType
-> [Spec Symbol BareType] -> [Spec Symbol BareType]
forall a. a -> [a] -> [a]
: ((ModName, Spec Symbol BareType) -> Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)] -> [Spec Symbol BareType]
forall a b. (a -> b) -> [a] -> [b]
map (ModName, Spec Symbol BareType) -> Spec Symbol BareType
forall a b. (a, b) -> b
snd [(ModName, Spec Symbol BareType)]
dependencySpecs
    dataConIds :: [TyVar]
dataConIds =
      [ DataCon -> TyVar
Ghc.dataConWorkId DataCon
dc
      | LHName
lhn <- HashSet LHName -> [LHName]
forall a. HashSet a -> [a]
S.toList HashSet LHName
usedDcs
      , Just (Ghc.AConLike (Ghc.RealDataCon DataCon
dc)) <-
          [LHName -> Maybe Name
maybeReflectedLHName LHName
lhn Maybe Name -> (Name -> Maybe TyThing) -> Maybe TyThing
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= GHCTyLookupEnv -> Name -> Maybe TyThing
Resolve.lookupGhcTyThingFromName GHCTyLookupEnv
ghcTyLookupEnv]
      ]


collectAllDataCons :: Ghc.CoreProgram -> [BareSpec] -> S.HashSet LHName
collectAllDataCons :: CoreProgram -> [Spec Symbol BareType] -> HashSet LHName
collectAllDataCons CoreProgram
cbs =
    [HashSet LHName] -> HashSet LHName
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet LHName] -> HashSet LHName)
-> ([Spec Symbol BareType] -> [HashSet LHName])
-> [Spec Symbol BareType]
-> HashSet LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (HashSet LHName
castDCs HashSet LHName -> [HashSet LHName] -> [HashSet LHName]
forall a. a -> [a] -> [a]
:) ([HashSet LHName] -> [HashSet LHName])
-> ([Spec Symbol BareType] -> [HashSet LHName])
-> [Spec Symbol BareType]
-> [HashSet LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HashSet LHName
usedInCoreDCs HashSet LHName -> [HashSet LHName] -> [HashSet LHName]
forall a. a -> [a] -> [a]
:) ([HashSet LHName] -> [HashSet LHName])
-> ([Spec Symbol BareType] -> [HashSet LHName])
-> [Spec Symbol BareType]
-> [HashSet LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Spec Symbol BareType -> HashSet LHName)
-> [Spec Symbol BareType] -> [HashSet LHName]
forall a b. (a -> b) -> [a] -> [b]
map Spec Symbol BareType -> HashSet LHName
forall lname ty. Spec lname ty -> HashSet LHName
usedDataCons
  where
    -- Constraint generation might inserts data constructors which are not
    -- present in the original program.
    -- See Note [Type classes with a single method] in
    -- Haskell.Liquid.Constraint.Generate
    castDCs :: HashSet LHName
castDCs =
      [LHName] -> HashSet LHName
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([LHName] -> HashSet LHName) -> [LHName] -> HashSet LHName
forall a b. (a -> b) -> a -> b
$
      (DataCon -> LHName) -> [DataCon] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map DataCon -> LHName
forall {p}. NamedThing p => p -> LHName
makeLogicLHNameFromDC ([DataCon] -> [LHName]) -> [DataCon] -> [LHName]
forall a b. (a -> b) -> a -> b
$
      (Coercion -> Maybe DataCon) -> [Coercion] -> [DataCon]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Coercion -> Maybe DataCon
isClassConCoDC ([Coercion] -> [DataCon]) -> [Coercion] -> [DataCon]
forall a b. (a -> b) -> a -> b
$
      CoreProgram -> [Coercion]
collectCastCoercions CoreProgram
cbs

    makeLogicLHNameFromDC :: p -> LHName
makeLogicLHNameFromDC p
dc =
      let n :: Name
n = p -> Name
forall a. NamedThing a => a -> Name
Ghc.getName p
dc
          s :: Symbol
s = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (p -> [Char]
forall a. NamedThing a => a -> [Char]
Ghc.getOccString p
dc)
       in Symbol -> GenModule Unit -> Maybe Name -> LHName
makeLogicLHName
            Symbol
s
            (GenModule Unit -> Maybe (GenModule Unit) -> GenModule Unit
forall a. a -> Maybe a -> a
Mb.fromMaybe ([Char] -> GenModule Unit
forall a. HasCallStack => [Char] -> a
error [Char]
"expected module") (Maybe (GenModule Unit) -> GenModule Unit)
-> Maybe (GenModule Unit) -> GenModule Unit
forall a b. (a -> b) -> a -> b
$ Name -> Maybe (GenModule Unit)
Ghc.nameModule_maybe Name
n)
            (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n)

    usedInCoreDCs :: HashSet LHName
usedInCoreDCs =
      [LHName] -> HashSet LHName
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([LHName] -> HashSet LHName) -> [LHName] -> HashSet LHName
forall a b. (a -> b) -> a -> b
$
      (DataCon -> LHName) -> [DataCon] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map DataCon -> LHName
forall {p}. NamedThing p => p -> LHName
makeLogicLHNameFromDC ([DataCon] -> [LHName]) -> [DataCon] -> [LHName]
forall a b. (a -> b) -> a -> b
$
      [ DataCon
dc
      | TyVar
v <- HashSet TyVar -> CoreProgram -> [TyVar]
forall a. CBVisitable a => HashSet TyVar -> a -> [TyVar]
freeVars HashSet TyVar
forall a. HashSet a
S.empty CoreProgram
cbs
      , DataCon
dc <- case TyVar -> IdDetails
Ghc.idDetails TyVar
v of
          Ghc.DataConWrapId DataCon
dc -> [DataCon
dc]
          Ghc.DataConWorkId DataCon
dc -> [DataCon
dc]
          IdDetails
_ -> []
      ]

    isClassConCoDC :: Ghc.Coercion -> Maybe Ghc.DataCon
    -- See Note [Type classes with a single method] in
    -- Haskell.Liquid.Constraint.Generate
    isClassConCoDC :: Coercion -> Maybe DataCon
isClassConCoDC Coercion
co
      | Ghc.Pair Type
_t1 Type
t2 <- Coercion -> Pair Type
Ghc.coercionKind Coercion
co
      , Type -> Bool
Ghc.isClassPred Type
t2
      , (TyCon
tc,[Type]
_ts) <- Type -> (TyCon, [Type])
Ghc.splitTyConApp Type
t2
      , [DataCon
dc]    <- TyCon -> [DataCon]
Ghc.tyConDataCons TyCon
tc
      = DataCon -> Maybe DataCon
forall a. a -> Maybe a
Just DataCon
dc
      | Bool
otherwise
      = Maybe DataCon
forall a. Maybe a
Nothing

    collectCastCoercions :: [Ghc.CoreBind] -> [Ghc.Coercion]
    collectCastCoercions :: CoreProgram -> [Coercion]
collectCastCoercions = [Coercion] -> [CoreExpr] -> [Coercion]
forall {b}. [Coercion] -> [Expr b] -> [Coercion]
gos [] ([CoreExpr] -> [Coercion])
-> (CoreProgram -> [CoreExpr]) -> CoreProgram -> [Coercion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoreBind -> [CoreExpr]) -> CoreProgram -> [CoreExpr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap CoreBind -> [CoreExpr]
forall b. Bind b -> [Expr b]
Ghc.rhssOfBind
      where
        go :: [Coercion] -> Expr b -> [Coercion]
go [Coercion]
acc Expr b
e = case Expr b
e of
          Ghc.Var{} -> [Coercion]
acc
          Ghc.Lit{} -> [Coercion]
acc
          Ghc.Type{} -> [Coercion]
acc
          Ghc.Coercion{} -> [Coercion]
acc
          Ghc.App Expr b
e1 Expr b
e2 -> [Coercion] -> Expr b -> [Coercion]
go ([Coercion] -> Expr b -> [Coercion]
go [Coercion]
acc Expr b
e1) Expr b
e2
          Ghc.Cast Expr b
e1 Coercion
c -> [Coercion] -> Expr b -> [Coercion]
go (Coercion
cCoercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
acc) Expr b
e1
          Ghc.Tick CoreTickish
_ Expr b
e1 -> [Coercion] -> Expr b -> [Coercion]
go [Coercion]
acc Expr b
e1
          Ghc.Lam b
_ Expr b
e1 -> [Coercion] -> Expr b -> [Coercion]
go [Coercion]
acc Expr b
e1
          Ghc.Let Bind b
b Expr b
e1 -> [Coercion] -> Expr b -> [Coercion]
go ([Coercion] -> [Expr b] -> [Coercion]
gos [Coercion]
acc (Bind b -> [Expr b]
forall b. Bind b -> [Expr b]
Ghc.rhssOfBind Bind b
b)) Expr b
e1
          Ghc.Case Expr b
e1 b
_ Type
_ [Alt b]
alts -> [Coercion] -> Expr b -> [Coercion]
go ([Coercion] -> [Expr b] -> [Coercion]
gos [Coercion]
acc ([Alt b] -> [Expr b]
forall b. [Alt b] -> [Expr b]
Ghc.rhssOfAlts [Alt b]
alts)) Expr b
e1

        gos :: [Coercion] -> [Expr b] -> [Coercion]
gos [Coercion]
acc = (([Coercion] -> [Coercion]) -> [Coercion] -> [Coercion])
-> [Coercion] -> [[Coercion] -> [Coercion]] -> [Coercion]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([Coercion] -> [Coercion]) -> [Coercion] -> [Coercion]
forall a b. (a -> b) -> a -> b
($) [Coercion]
acc ([[Coercion] -> [Coercion]] -> [Coercion])
-> ([Expr b] -> [[Coercion] -> [Coercion]])
-> [Expr b]
-> [Coercion]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr b -> [Coercion] -> [Coercion])
-> [Expr b] -> [[Coercion] -> [Coercion]]
forall a b. (a -> b) -> [a] -> [b]
map (([Coercion] -> Expr b -> [Coercion])
-> Expr b -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Coercion] -> Expr b -> [Coercion]
go)


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


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

makeTyConEmbeds :: Bare.GHCTyLookupEnv -> Ms.BareSpec -> F.TCEmb Ghc.TyCon
makeTyConEmbeds :: GHCTyLookupEnv -> Spec Symbol BareType -> TCEmb TyCon
makeTyConEmbeds GHCTyLookupEnv
env Spec Symbol BareType
spec
  = [(TyCon, (Sort, TCArgs))] -> TCEmb TyCon
forall a. (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
F.tceFromList [ (TyCon
tc, (Sort, TCArgs)
t) | (Located LHName
c,(Sort, TCArgs)
t) <- TCEmb (Located LHName) -> [(Located LHName, (Sort, TCArgs))]
forall a. TCEmb a -> [(a, (Sort, TCArgs))]
F.tceToList (Spec Symbol BareType -> TCEmb (Located LHName)
forall lname ty. Spec lname ty -> TCEmb (Located LHName)
Ms.embeds Spec Symbol BareType
spec), TyCon
tc <- Located LHName -> [TyCon]
symTc Located LHName
c ]
    where
      symTc :: Located LHName -> [TyCon]
symTc = Maybe TyCon -> [TyCon]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe TyCon -> [TyCon])
-> (Located LHName -> Maybe TyCon) -> Located LHName -> [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Error] -> Maybe TyCon)
-> (TyCon -> Maybe TyCon) -> Either [Error] TyCon -> Maybe TyCon
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe TyCon -> [Error] -> Maybe TyCon
forall a b. a -> b -> a
const Maybe TyCon
forall a. Maybe a
Nothing) TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just (Either [Error] TyCon -> Maybe TyCon)
-> (Located LHName -> Either [Error] TyCon)
-> Located LHName
-> Maybe TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack =>
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
Bare.lookupGhcTyConLHName GHCTyLookupEnv
env

--------------------------------------------------------------------------------
-- | [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 Symbol BareType
-> Spec Symbol BareType
makeLiftedSpec1 Config
config GhcSrc
src TycEnv
tycEnv LogicMap
lmap Spec Symbol BareType
mySpec = Spec Symbol BareType
forall a. Monoid a => a
mempty
  { Ms.measures  = Bare.makeHaskellMeasures config src tycEnv lmap mySpec }

--------------------------------------------------------------------------------
-- | [NOTE]: LIFTING-STAGES
--
-- We split the lifting up into stage:
-- 0. Where we only lift inlines,
-- 1. Where we lift reflects, measures, and normalized tySigs
--
-- This is because we need the inlines to build the @BareRTEnv@ which then
-- does the alias @expand@ business, that in turn, lets us build the DataConP,
-- i.e. the refined datatypes and their associate selectors, projectors etc,
-- that are needed for subsequent stages of the lifting.
--------------------------------------------------------------------------------
makeLiftedSpec0 :: Config -> GhcSrc -> F.TCEmb Ghc.TyCon -> LogicMap -> Ms.BareSpec
                -> Ms.BareSpec
makeLiftedSpec0 :: Config
-> GhcSrc
-> TCEmb TyCon
-> LogicMap
-> Spec Symbol BareType
-> Spec Symbol BareType
makeLiftedSpec0 Config
cfg GhcSrc
src TCEmb TyCon
embs LogicMap
lmap Spec Symbol BareType
mySpec = Spec Symbol BareType
forall a. Monoid a => a
mempty
  { Ms.ealiases  = lmapEAlias . snd <$> Bare.makeHaskellInlines cfg src embs lmap mySpec
  , Ms.dataDecls = Bare.makeHaskellDataDecls cfg mySpec tcs
  }
  where
    tcs :: [TyCon]
tcs          = [TyCon] -> [TyCon]
forall a. Uniquable a => [a] -> [a]
uniqNub (GhcSrc -> [TyCon]
_gsTcs GhcSrc
src [TyCon] -> [TyCon] -> [TyCon]
forall a. [a] -> [a] -> [a]
++ [TyCon]
refTcs)
    refTcs :: [TyCon]
refTcs       = Config
-> TCEmb TyCon -> CoreProgram -> Spec Symbol BareType -> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs CoreProgram
cbs  Spec Symbol BareType
mySpec
    cbs :: CoreProgram
cbs          = GhcSrc -> CoreProgram
_giCbs       GhcSrc
src

uniqNub :: (Ghc.Uniquable a) => [a] -> [a]
uniqNub :: forall a. Uniquable a => [a] -> [a]
uniqNub [a]
xs = HashMap Word64 a -> [a]
forall k v. HashMap k v -> [v]
M.elems (HashMap Word64 a -> [a]) -> HashMap Word64 a -> [a]
forall a b. (a -> b) -> a -> b
$ [(Word64, a)] -> HashMap Word64 a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (a -> Word64
forall {a}. Uniquable a => a -> Word64
index a
x, a
x) | a
x <- [a]
xs ]
  where
    index :: a -> Word64
index  = Unique -> Word64
Ghc.getKey (Unique -> Word64) -> (a -> Unique) -> a -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Unique
forall a. Uniquable a => a -> Unique
Ghc.getUnique

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

reflectedTyCons :: Config -> TCEmb Ghc.TyCon -> [Ghc.CoreBind] -> Ms.BareSpec -> [Ghc.TyCon]
reflectedTyCons :: Config
-> TCEmb TyCon -> CoreProgram -> Spec Symbol BareType -> [TyCon]
reflectedTyCons Config
cfg TCEmb TyCon
embs CoreProgram
cbs Spec Symbol BareType
spec
  | Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg = (TyCon -> Bool) -> [TyCon] -> [TyCon]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TyCon -> Bool) -> TyCon -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> TyCon -> Bool
isEmbedded TCEmb TyCon
embs)
                    ([TyCon] -> [TyCon]) -> [TyCon] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ (TyVar -> [TyCon]) -> [TyVar] -> [TyCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyVar -> [TyCon]
varTyCons
                    ([TyVar] -> [TyCon]) -> [TyVar] -> [TyCon]
forall a b. (a -> b) -> a -> b
$ Spec Symbol BareType -> CoreProgram -> [TyVar]
reflectedVars Spec Symbol BareType
spec CoreProgram
cbs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ Spec Symbol BareType -> CoreProgram -> [TyVar]
measureVars Spec Symbol BareType
spec CoreProgram
cbs
  | Bool
otherwise       = []

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

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

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

reflectedVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
reflectedVars :: Spec Symbol BareType -> CoreProgram -> [TyVar]
reflectedVars Spec Symbol BareType
spec CoreProgram
cbs =
    (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter
      (Located LHName -> Bool
isReflSym (Located LHName -> Bool)
-> (TyVar -> Located LHName) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Located LHName
makeGHCLHNameLocatedFromId)
      (CoreProgram -> [TyVar]
forall b. [Bind b] -> [b]
Ghc.bindersOfBinds CoreProgram
cbs)
  where
    isReflSym :: Located LHName -> Bool
isReflSym Located LHName
x =
      Located LHName -> HashSet (Located LHName) -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Located LHName
x (Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.reflects Spec Symbol BareType
spec) Bool -> Bool -> Bool
||
      LocSymbol -> HashSet LocSymbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member ((LHName -> Symbol) -> Located LHName -> LocSymbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
lhNameToResolvedSymbol Located LHName
x) (Spec Symbol BareType -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
Ms.privateReflects Spec Symbol BareType
spec)

measureVars :: Ms.BareSpec -> [Ghc.CoreBind] -> [Ghc.Var]
measureVars :: Spec Symbol BareType -> CoreProgram -> [TyVar]
measureVars Spec Symbol BareType
spec CoreProgram
cbs =
    (TyVar -> Bool) -> [TyVar] -> [TyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter
      ((Located LHName -> HashSet (Located LHName) -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet (Located LHName)
measureSyms) (Located LHName -> Bool)
-> (TyVar -> Located LHName) -> TyVar -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Located LHName
makeGHCLHNameLocatedFromId)
      (CoreProgram -> [TyVar]
forall b. [Bind b] -> [b]
Ghc.bindersOfBinds CoreProgram
cbs)
  where
    measureSyms :: HashSet (Located LHName)
measureSyms = Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.hmeas Spec Symbol BareType
spec

------------------------------------------------------------------------------------------
makeSpecVars :: Config -> GhcSrc -> Ms.BareSpec -> Bare.Env -> Bare.MeasEnv
             -> Bare.Lookup GhcSpecVars
------------------------------------------------------------------------------------------
makeSpecVars :: Config
-> GhcSrc
-> Spec Symbol BareType
-> Env
-> MeasEnv
-> Lookup GhcSpecVars
makeSpecVars Config
cfg GhcSrc
src Spec Symbol BareType
mySpec Env
env MeasEnv
measEnv = do
  let tgtVars :: [TyVar]
tgtVars = ([Char] -> Maybe TyVar) -> [[Char]] -> [TyVar]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe ([Char] -> HashMap [Char] TyVar -> Maybe TyVar
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
`M.lookup` HashMap [Char] TyVar
hvars) (Config -> [[Char]]
checks     Config
cfg)
  igVars      <-  (Located LHName -> Either [Error] TyVar)
-> HashSet (Located LHName) -> Either [Error] (HashSet TyVar)
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env) (Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.ignores Spec Symbol BareType
mySpec)
  lVars       <-  sMapM (Bare.lookupGhcIdLHName env) (Ms.lvars   mySpec)
  return (SpVar tgtVars igVars lVars cMethods)
  where
    cMethods :: [TyVar]
cMethods   = (ModName, TyVar, LocSpecType) -> TyVar
forall a b c. (a, b, c) -> b
snd3 ((ModName, TyVar, LocSpecType) -> TyVar)
-> [(ModName, TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(ModName, TyVar, LocSpecType)]
Bare.meMethods MeasEnv
measEnv
    hvars :: HashMap [Char] TyVar
hvars = [([Char], TyVar)] -> HashMap [Char] TyVar
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
      [ (OccName -> [Char]
Ghc.occNameString (OccName -> [Char]) -> OccName -> [Char]
forall a b. (a -> b) -> a -> b
$ TyVar -> OccName
forall a. NamedThing a => a -> OccName
Ghc.getOccName TyVar
b, TyVar
b)
      | TyVar
b <- CoreProgram -> [TyVar]
forall b. [Bind b] -> [b]
Ghc.bindersOfBinds (GhcSrc -> CoreProgram
_giCbs GhcSrc
src)
      ]

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
 ys <- (a -> m b) -> [a] -> m [b]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM a -> m b
f (HashSet a -> [a]
forall a. HashSet a -> [a]
S.toList HashSet a
xSet)
 return (S.fromList ys)

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

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

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

qualifyFTycon
  :: Bare.Env
  -> Ghc.GlobalRdrEnv
  -> Bare.TycEnv
  -> F.FTycon
  -> Maybe F.Sort
qualifyFTycon :: Env -> GlobalRdrEnv -> TycEnv -> FTycon -> Maybe Sort
qualifyFTycon Env
env GlobalRdrEnv
globalRdrEnv TycEnv
tycEnv FTycon
c
  | Bool
isPrimFTC           = Sort -> Maybe Sort
forall a. a -> Maybe a
Just (FTycon -> Sort
FTC FTycon
c)
  | Bool
otherwise           = TCEmb TyCon -> Located TyCon -> Sort
tyConSort TCEmb TyCon
embs (Located TyCon -> Sort)
-> (TyCon -> Located TyCon) -> TyCon -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol -> TyCon -> Located TyCon
forall l b. Loc l => l -> b -> Located b
F.atLoc LocSymbol
tcs (TyCon -> Sort) -> Maybe TyCon -> Maybe Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe TyCon
ty
  where
    ty :: Maybe TyCon
ty                  = case GlobalRdrEnv -> LocSymbol -> Either Error (Located LHName)
resolveSymbolToTcName GlobalRdrEnv
globalRdrEnv LocSymbol
tcs of
      Left Error
e -> [Error] -> Maybe TyCon
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw [Error
e]
      Right Located LHName
lhname -> ([Error] -> Maybe TyCon)
-> (TyCon -> Maybe TyCon) -> Either [Error] TyCon -> Maybe TyCon
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Error] -> Maybe TyCon
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just (Either [Error] TyCon -> Maybe TyCon)
-> Either [Error] TyCon -> Maybe TyCon
forall a b. (a -> b) -> a -> b
$
                        HasCallStack =>
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
Bare.lookupGhcTyConLHName (Env -> GHCTyLookupEnv
Bare.reTyLookupEnv Env
env) Located LHName
lhname
    isPrimFTC :: Bool
isPrimFTC           = LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
tcs Symbol -> HashSet Symbol -> Bool
forall a. Eq a => a -> HashSet a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HashSet Symbol
F.prims
    tcs :: LocSymbol
tcs                 = FTycon -> LocSymbol
F.fTyconSymbol FTycon
c
    embs :: TCEmb TyCon
embs                = TycEnv -> TCEmb TyCon
Bare.tcEmbs TycEnv
tycEnv

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

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

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

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


makeLazy :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeLazy :: Env -> Spec Symbol BareType -> Either [Error] (HashSet TyVar)
makeLazy Env
env Spec Symbol BareType
spec =
  (Located LHName -> Either [Error] TyVar)
-> HashSet (Located LHName) -> Either [Error] (HashSet TyVar)
forall (m :: * -> *) b a.
(Monad m, Eq b, Hashable b) =>
(a -> m b) -> HashSet a -> m (HashSet b)
sMapM (HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env) (Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.lazy Spec Symbol BareType
spec)

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

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

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

makeRewriteWith' :: Bare.Env -> Spec lname ty -> Bare.Lookup [(Ghc.Var, [Ghc.Var])]
makeRewriteWith' :: forall lname ty.
Env -> Spec lname ty -> Either [Error] [(TyVar, [TyVar])]
makeRewriteWith' Env
env Spec lname ty
spec =
  [(Located LHName, [Located LHName])]
-> ((Located LHName, [Located LHName])
    -> Either [Error] (TyVar, [TyVar]))
-> Either [Error] [(TyVar, [TyVar])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (HashMap (Located LHName) [Located LHName]
-> [(Located LHName, [Located LHName])]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap (Located LHName) [Located LHName]
 -> [(Located LHName, [Located LHName])])
-> HashMap (Located LHName) [Located LHName]
-> [(Located LHName, [Located LHName])]
forall a b. (a -> b) -> a -> b
$ Spec lname ty -> HashMap (Located LHName) [Located LHName]
forall lname ty.
Spec lname ty -> HashMap (Located LHName) [Located LHName]
Ms.rewriteWith Spec lname ty
spec) (((Located LHName, [Located LHName])
  -> Either [Error] (TyVar, [TyVar]))
 -> Either [Error] [(TyVar, [TyVar])])
-> ((Located LHName, [Located LHName])
    -> Either [Error] (TyVar, [TyVar]))
-> Either [Error] [(TyVar, [TyVar])]
forall a b. (a -> b) -> a -> b
$ \(Located LHName
x, [Located LHName]
xs) -> do
    xv  <- HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env Located LHName
x
    xvs <- mapM (Bare.lookupGhcIdLHName env) xs
    return (xv, xvs)

makeAutoSize :: Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.TyCon)
makeAutoSize :: Env -> Spec Symbol BareType -> Lookup (HashSet TyCon)
makeAutoSize Env
env
  = ([TyCon] -> HashSet TyCon)
-> Either [Error] [TyCon] -> Lookup (HashSet TyCon)
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TyCon] -> HashSet TyCon
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
  (Either [Error] [TyCon] -> Lookup (HashSet TyCon))
-> (Spec Symbol BareType -> Either [Error] [TyCon])
-> Spec Symbol BareType
-> Lookup (HashSet TyCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName -> Either [Error] TyCon)
-> [Located LHName] -> Either [Error] [TyCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (HasCallStack =>
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
GHCTyLookupEnv -> Located LHName -> Either [Error] TyCon
Bare.lookupGhcTyConLHName (Env -> GHCTyLookupEnv
Bare.reTyLookupEnv Env
env))
  ([Located LHName] -> Either [Error] [TyCon])
-> (Spec Symbol BareType -> [Located LHName])
-> Spec Symbol BareType
-> Either [Error] [TyCon]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList
  (HashSet (Located LHName) -> [Located LHName])
-> (Spec Symbol BareType -> HashSet (Located LHName))
-> Spec Symbol BareType
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.autosize

makeSize :: LogicNameEnv -> Bare.Env -> Ms.BareSpec -> Bare.Lookup (S.HashSet Ghc.Var)
makeSize :: LogicNameEnv
-> Env -> Spec Symbol BareType -> Either [Error] (HashSet TyVar)
makeSize LogicNameEnv
lenv Env
env
  = ([TyVar] -> HashSet TyVar)
-> Either [Error] [TyVar] -> Either [Error] (HashSet TyVar)
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
  (Either [Error] [TyVar] -> Either [Error] (HashSet TyVar))
-> (Spec Symbol BareType -> Either [Error] [TyVar])
-> Spec Symbol BareType
-> Either [Error] (HashSet TyVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol -> Either [Error] TyVar)
-> [LocSymbol] -> Either [Error] [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM LocSymbol -> Either [Error] TyVar
lookupGhcSize
  ([LocSymbol] -> Either [Error] [TyVar])
-> (Spec Symbol BareType -> [LocSymbol])
-> Spec Symbol BareType
-> Either [Error] [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> Maybe LocSymbol) -> [DataDecl] -> [LocSymbol]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe DataDecl -> Maybe LocSymbol
getSizeFuns
  ([DataDecl] -> [LocSymbol])
-> (Spec Symbol BareType -> [DataDecl])
-> Spec Symbol BareType
-> [LocSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol BareType -> [DataDecl]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
Ms.dataDecls
  where
    lookupGhcSize :: LocSymbol -> Bare.Lookup Ghc.Var
    lookupGhcSize :: LocSymbol -> Either [Error] TyVar
lookupGhcSize LocSymbol
s =
      case Symbol -> SEnv LHName -> Maybe LHName
forall a. Symbol -> SEnv a -> Maybe a
lookupSEnv (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s) (LogicNameEnv -> SEnv LHName
lneLHName LogicNameEnv
lenv) of
        Maybe LHName
Nothing -> Maybe SrcSpan -> [Char] -> Either [Error] TyVar
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
s) ([Char] -> Either [Error] TyVar) -> [Char] -> Either [Error] TyVar
forall a b. (a -> b) -> a -> b
$ [Char]
"symbol not in scope: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s)
        Just LHName
n -> case LHName -> Maybe Name
maybeReflectedLHName LHName
n of
          Maybe Name
Nothing -> Maybe SrcSpan -> [Char] -> Either [Error] TyVar
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ LocSymbol -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSymbol
s) ([Char] -> Either [Error] TyVar) -> [Char] -> Either [Error] TyVar
forall a b. (a -> b) -> a -> b
$ [Char]
"symbol not reflected: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
s)
          Just Name
rn -> HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env (Name -> Symbol -> LHName
makeGHCLHName Name
rn (Name -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Name
rn) LHName -> LocSymbol -> Located LHName
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LocSymbol
s)

getSizeFuns :: DataDecl -> Maybe LocSymbol
getSizeFuns :: DataDecl -> Maybe LocSymbol
getSizeFuns DataDecl
decl
  | Just SizeFunV Symbol
x       <- DataDecl -> Maybe (SizeFunV Symbol)
forall v ty. DataDeclP v ty -> Maybe (SizeFunV v)
tycSFun DataDecl
decl
  , SymSizeFun LocSymbol
f <- SizeFunV Symbol
x
  = LocSymbol -> Maybe LocSymbol
forall a. a -> Maybe a
Just LocSymbol
f
  | Bool
otherwise
  = Maybe LocSymbol
forall a. Maybe a
Nothing


------------------------------------------------------------------------------------------
makeSpecRefl :: GhcSrc -> Bare.ModSpecs -> Bare.Env -> ModName -> GhcSpecSig -> Bare.TycEnv
             -> Bare.Lookup GhcSpecRefl
------------------------------------------------------------------------------------------
makeSpecRefl :: GhcSrc
-> HashMap ModName (Spec Symbol BareType)
-> Env
-> ModName
-> GhcSpecSig
-> TycEnv
-> Lookup GhcSpecRefl
makeSpecRefl GhcSrc
src HashMap ModName (Spec Symbol BareType)
specs Env
env ModName
name GhcSpecSig
sig TycEnv
tycEnv = do
  autoInst <- Env -> Spec Symbol BareType -> Either [Error] (HashSet TyVar)
makeAutoInst Env
env Spec Symbol BareType
mySpec
  rwr      <- makeRewrite env mySpec
  rwrWith  <- makeRewriteWith env mySpec
  xtes     <- Bare.makeHaskellAxioms src env tycEnv lmap sig mySpec
  asmReflAxioms <- Bare.makeAssumeReflectAxioms src env tycEnv sig mySpec
  let otherAxioms = (TyVar, LocSpecType, Equation) -> Equation
forall a b c. (a, b, c) -> c
thd3 ((TyVar, LocSpecType, Equation) -> Equation)
-> [(TyVar, LocSpecType, Equation)] -> [Equation]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType, Equation)]
asmReflAxioms
  let myAxioms =
        [ Equation
e {eqRec = S.member (eqName e) (exprSymbolsSet (eqBody e))}
        | (TyVar
_, LocSpecType
_, Equation
e) <- [(TyVar, LocSpecType, Equation)]
xtes
        ] [Equation] -> [Equation] -> [Equation]
forall a. [a] -> [a] -> [a]
++ [Equation]
otherAxioms
  let asmReflEls = Equation -> Symbol
forall v. EquationV v -> Symbol
eqName (Equation -> Symbol) -> [Equation] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Equation]
otherAxioms
  let impAxioms  = ((ModName, Spec Symbol BareType) -> [Equation])
-> [(ModName, Spec Symbol BareType)] -> [Equation]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Symbol]
asmReflEls) (Symbol -> Bool) -> (Equation -> Symbol) -> Equation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> Symbol
forall v. EquationV v -> Symbol
eqName) ([Equation] -> [Equation])
-> ((ModName, Spec Symbol BareType) -> [Equation])
-> (ModName, Spec Symbol BareType)
-> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol BareType -> [Equation]
forall lname ty. Spec lname ty -> [EquationV lname]
Ms.axeqs (Spec Symbol BareType -> [Equation])
-> ((ModName, Spec Symbol BareType) -> Spec Symbol BareType)
-> (ModName, Spec Symbol BareType)
-> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec Symbol BareType) -> Spec Symbol BareType
forall a b. (a, b) -> b
snd) (HashMap ModName (Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec Symbol BareType)
specs)
  case anyNonReflFn of
    Just (Located LHName
actSym , Located LHName
preSym) ->
      let preSym' :: [Char]
preSym' = Symbol -> [Char]
symbolString (Symbol -> [Char]) -> Symbol -> [Char]
forall a b. (a -> b) -> a -> b
$ HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
preSym) in
      let errorMsg :: [Char]
errorMsg = [Char]
preSym' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" must be reflected first using {-@ reflect " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
preSym' [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" @-}"
      in Error -> Lookup GhcSpecRefl
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw
           (SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrHMeas
             (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SourcePos
forall a. Located a -> SourcePos
loc Located LHName
actSym)
             (LHName -> Doc
forall a. PPrint a => a -> Doc
pprint (LHName -> Doc) -> LHName -> Doc
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val Located LHName
actSym)
             ([Char] -> Doc
text [Char]
errorMsg) :: Error)
    Maybe (Located LHName, Located LHName)
Nothing -> GhcSpecRefl -> Lookup GhcSpecRefl
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return SpRefl
      { gsLogicMap :: LogicMap
gsLogicMap   = LogicMap
lmap
      , gsAutoInst :: HashSet TyVar
gsAutoInst   = HashSet TyVar
autoInst
      , gsImpAxioms :: [Equation]
gsImpAxioms  = [Equation]
impAxioms
      , gsMyAxioms :: [Equation]
gsMyAxioms   = [Equation]
myAxioms
      , gsReflects :: [TyVar]
gsReflects   = ((TyVar, LocSpecType, Equation) -> TyVar
forall a b c. (a, b, c) -> a
fst3 ((TyVar, LocSpecType, Equation) -> TyVar)
-> [(TyVar, LocSpecType, Equation)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType, Equation)]
xtes) [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ ((TyVar, TyVar) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, TyVar) -> TyVar) -> [(TyVar, TyVar)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, TyVar)]
gsAsmReflects GhcSpecSig
sig)
      , gsHAxioms :: [(TyVar, LocSpecType, Equation)]
gsHAxioms    = [Char]
-> [(TyVar, LocSpecType, Equation)]
-> [(TyVar, LocSpecType, Equation)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"gsHAxioms" ([(TyVar, LocSpecType, Equation)]
 -> [(TyVar, LocSpecType, Equation)])
-> [(TyVar, LocSpecType, Equation)]
-> [(TyVar, LocSpecType, Equation)]
forall a b. (a -> b) -> a -> b
$ [(TyVar, LocSpecType, Equation)]
xtes [(TyVar, LocSpecType, Equation)]
-> [(TyVar, LocSpecType, Equation)]
-> [(TyVar, LocSpecType, Equation)]
forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType, Equation)]
asmReflAxioms
      , gsRewrites :: HashSet (Located TyVar)
gsRewrites   = HashSet (Located TyVar)
rwr
      , gsRewritesWith :: HashMap TyVar [TyVar]
gsRewritesWith = HashMap TyVar [TyVar]
rwrWith
      }
  where
    mySpec :: Spec Symbol BareType
mySpec       = Spec Symbol BareType
-> ModName
-> HashMap ModName (Spec Symbol BareType)
-> Spec Symbol BareType
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Spec Symbol BareType
forall a. Monoid a => a
mempty ModName
name HashMap ModName (Spec Symbol BareType)
specs
    lmap :: LogicMap
lmap         = Env -> LogicMap
Bare.reLMap Env
env
    notInReflOnes :: (a, Located LHName) -> Bool
notInReflOnes (a
_, Located LHName
a) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$
      Located LHName
a Located LHName -> HashSet (Located LHName) -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.reflects Spec Symbol BareType
mySpec Bool -> Bool -> Bool
||
      (LHName -> Symbol) -> Located LHName -> LocSymbol
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Symbol
lhNameToResolvedSymbol Located LHName
a LocSymbol -> HashSet LocSymbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` Spec Symbol BareType -> HashSet LocSymbol
forall lname ty. Spec lname ty -> HashSet LocSymbol
Ms.privateReflects Spec Symbol BareType
mySpec
    anyNonReflFn :: Maybe (Located LHName, Located LHName)
anyNonReflFn = ((Located LHName, Located LHName) -> Bool)
-> [(Located LHName, Located LHName)]
-> Maybe (Located LHName, Located LHName)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (Located LHName, Located LHName) -> Bool
forall {a}. (a, Located LHName) -> Bool
notInReflOnes (Spec Symbol BareType -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
Ms.asmReflectSigs Spec Symbol BareType
mySpec)

------------------------------------------------------------------------------------------
-- | @updateReflSpecSig@ uses the information about reflected functions (included the opaque ones) to update the
--   "assumed" signatures.
------------------------------------------------------------------------------------------
addReflSigs :: Bare.Env -> ModName -> BareRTEnv -> Bare.MeasEnv -> GhcSpecRefl -> GhcSpecSig -> GhcSpecSig
------------------------------------------------------------------------------------------
addReflSigs :: Env
-> ModName
-> BareRTEnv
-> MeasEnv
-> GhcSpecRefl
-> GhcSpecSig
-> GhcSpecSig
addReflSigs Env
env ModName
name BareRTEnv
rtEnv MeasEnv
measEnv GhcSpecRefl
refl GhcSpecSig
sig =
  GhcSpecSig
sig { gsRefSigs = F.notracepp ("gsRefSigs for " ++ F.showpp name) $ map expandReflectedSignature reflSigs
      , gsAsmSigs = F.notracepp ("gsAsmSigs for " ++ F.showpp name) combinedOpaqueAndReflectedAsmSigs
      }
  where
    -- We make sure that the reflected functions are excluded from `gsAsmSigs`, except for the signatures of
    -- actual functions in assume-reflect. The latter are added here because 1. it's what makes tests work
    -- and 2. so that we probably "shadow" the old signatures of the actual function correctly. Note that even if the
    -- signature of the actual function was asserted and not assumed, we do not put our new signature for the actual function
    -- in `gsTySigs` (which is for asserted signatures). Indeed, the new signature will *always* be an assumption since we
    -- add the extra post-condition that the actual and pretended function behave in the same way.
    -- Also, we add here the strengthened post-conditions relative to opaque reflections.
    -- We may redefine assumptions because of opaque reflections, so we just take the union of maps and ignore duplicates.
    -- Based on `M.union`'s handling of duplicates, the leftmost elements in the chain of `M.union` will precede over those
    -- after, which is why we put the opaque reflection first in the chain. The signatures for opaque reflections are created
    -- by strengthening the post-conditions, as in (assume-)reflection.
    combinedOpaqueAndReflectedAsmSigs :: [(TyVar, LocSpecType)]
combinedOpaqueAndReflectedAsmSigs = HashMap TyVar LocSpecType -> [(TyVar, LocSpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap TyVar LocSpecType -> [(TyVar, LocSpecType)])
-> HashMap TyVar LocSpecType -> [(TyVar, LocSpecType)]
forall a b. (a -> b) -> a -> b
$
        [(TyVar, LocSpecType)] -> HashMap TyVar LocSpecType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (TyVar -> (TyVar, LocSpecType)
createUpdatedSpecs (TyVar -> (TyVar, LocSpecType))
-> ((TyVar, Measure (Located BareType) (Located LHName)) -> TyVar)
-> (TyVar, Measure (Located BareType) (Located LHName))
-> (TyVar, LocSpecType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVar, Measure (Located BareType) (Located LHName)) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, Measure (Located BareType) (Located LHName))
 -> (TyVar, LocSpecType))
-> [(TyVar, Measure (Located BareType) (Located LHName))]
-> [(TyVar, LocSpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MeasEnv -> [(TyVar, Measure (Located BareType) (Located LHName))]
Bare.meOpaqueRefl MeasEnv
measEnv)
        HashMap TyVar LocSpecType
-> HashMap TyVar LocSpecType -> HashMap TyVar LocSpecType
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
`M.union` [(TyVar, LocSpecType)] -> HashMap TyVar LocSpecType
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (((TyVar, LocSpecType) -> Bool)
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (TyVar, LocSpecType) -> Bool
forall {b}. (TyVar, b) -> Bool
notReflected (GhcSpecSig -> [(TyVar, LocSpecType)]
gsAsmSigs GhcSpecSig
sig))
    -- Strengthen the post-condition of each of the opaque reflections.
    createUpdatedSpecs :: TyVar -> (TyVar, LocSpecType)
createUpdatedSpecs TyVar
var = (TyVar
var, AxiomType -> SpecType
Bare.aty (AxiomType -> SpecType) -> Located AxiomType -> LocSpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> Env -> TyVar -> LocSymbol -> Located AxiomType
Bare.strengthenSpecWithMeasure GhcSpecSig
sig Env
env TyVar
var (TyVar -> LocSymbol
Bare.varLocSym TyVar
var))
    -- See T1738. We need to expand and qualify any reflected signature /here/, after any
    -- relevant binder has been detected and \"promoted\". The problem stems from the fact that any input
    -- 'BareSpec' will have a 'reflects' list of binders to reflect under the form of an opaque 'Var', that
    -- qualifyExpand can't touch when we do a first pass in 'makeGhcSpec0'. However, once we reflected all
    -- the functions, we are left with a pair (Var, LocSpecType). The latter /needs/ to be qualified and
    -- expanded again, for example in case it has expression aliases derived from 'inlines'.
    expandReflectedSignature :: (Ghc.Var, LocSpecType) -> (Ghc.Var, LocSpecType)
    expandReflectedSignature :: (TyVar, LocSpecType) -> (TyVar, LocSpecType)
expandReflectedSignature = (LocSpecType -> LocSpecType)
-> (TyVar, LocSpecType) -> (TyVar, LocSpecType)
forall a b. (a -> b) -> (TyVar, a) -> (TyVar, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (BareRTEnv -> SourcePos -> LocSpecType -> LocSpecType
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
Bare.expand BareRTEnv
rtEnv ([Char] -> SourcePos
F.dummyPos [Char]
"expand-refSigs"))

    reflSigs :: [(TyVar, LocSpecType)]
reflSigs = [ (TyVar
x, LocSpecType
t) | (TyVar
x, LocSpecType
t, Equation
_) <- GhcSpecRefl -> [(TyVar, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl ]
    -- Get the set of all the actual functions (in assume-reflects)
    actualFnsInAssmRefl :: HashSet TyVar
actualFnsInAssmRefl     = [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([TyVar] -> HashSet TyVar) -> [TyVar] -> HashSet TyVar
forall a b. (a -> b) -> a -> b
$ (TyVar, TyVar) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, TyVar) -> TyVar) -> [(TyVar, TyVar)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GhcSpecSig -> [(TyVar, TyVar)]
gsAsmReflects GhcSpecSig
sig
    isActualFn :: TyVar -> Bool
isActualFn           TyVar
x  = TyVar -> HashSet TyVar -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member TyVar
x HashSet TyVar
actualFnsInAssmRefl
    -- Get all the variables from the axioms that are not actual functions (in assume-reflects)
    notReflActualTySigs :: [(TyVar, LocSpecType)]
notReflActualTySigs     = ((TyVar, LocSpecType) -> Bool)
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. (a -> Bool) -> [a] -> [a]
L.filter (Bool -> Bool
not (Bool -> Bool)
-> ((TyVar, LocSpecType) -> Bool) -> (TyVar, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar -> Bool
isActualFn (TyVar -> Bool)
-> ((TyVar, LocSpecType) -> TyVar) -> (TyVar, LocSpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst) [(TyVar, LocSpecType)]
reflSigs
    -- Get the list of reflected elements. We do not count actual functions in assume reflect as reflected
    reflected :: HashSet TyVar
reflected               = [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([TyVar] -> HashSet TyVar) -> [TyVar] -> HashSet TyVar
forall a b. (a -> b) -> a -> b
$ (TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
notReflActualTySigs
    notReflected :: (TyVar, b) -> Bool
notReflected (TyVar, b)
xt         = (TyVar, b) -> TyVar
forall a b. (a, b) -> a
fst (TyVar, b)
xt TyVar -> HashSet TyVar -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` HashSet TyVar
reflected

makeAutoInst :: Bare.Env -> Ms.BareSpec ->
                Bare.Lookup (S.HashSet Ghc.Var)
makeAutoInst :: Env -> Spec Symbol BareType -> Either [Error] (HashSet TyVar)
makeAutoInst Env
env Spec Symbol BareType
spec = [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([TyVar] -> HashSet TyVar)
-> Either [Error] [TyVar] -> Either [Error] (HashSet TyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either [Error] [TyVar]
kvs
  where
    kvs :: Either [Error] [TyVar]
kvs = [Located LHName]
-> (Located LHName -> Either [Error] TyVar)
-> Either [Error] [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList (Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.autois Spec Symbol BareType
spec)) ((Located LHName -> Either [Error] TyVar)
 -> Either [Error] [TyVar])
-> (Located LHName -> Either [Error] TyVar)
-> Either [Error] [TyVar]
forall a b. (a -> b) -> a -> b
$
            HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env


----------------------------------------------------------------------------------------
makeSpecSig :: Config -> ModName -> Ms.BareSpec -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv -> [Ghc.CoreBind]
            -> Bare.Lookup ([RInstance LocBareType], GhcSpecSig)
----------------------------------------------------------------------------------------
makeSpecSig :: Config
-> ModName
-> Spec Symbol BareType
-> HashMap ModName (Spec Symbol BareType)
-> Env
-> SigEnv
-> TycEnv
-> MeasEnv
-> CoreProgram
-> Lookup ([RInstance (Located BareType)], GhcSpecSig)
makeSpecSig Config
cfg ModName
name Spec Symbol BareType
mySpec HashMap ModName (Spec Symbol BareType)
specs Env
env SigEnv
sigEnv TycEnv
tycEnv MeasEnv
measEnv CoreProgram
cbs = do
  mySigs     <- Env
-> SigEnv
-> ModName
-> Spec Symbol BareType
-> Lookup [(TyVar, LocSpecType, Maybe [Located Expr])]
makeTySigs  Env
env SigEnv
sigEnv ModName
name Spec Symbol BareType
mySpec
  aSigs      <- F.notracepp ("makeSpecSig aSigs " ++ F.showpp name) $ makeAsmSigs env sigEnv name allSpecs
  let asmSigs =  TycEnv -> [(TyVar, LocSpecType)]
Bare.tcSelVars TycEnv
tycEnv [(TyVar, LocSpecType)]
-> [(TyVar, LocSpecType)] -> [(TyVar, LocSpecType)]
forall a. [a] -> [a] -> [a]
++ [(TyVar, LocSpecType)]
aSigs
  let tySigs  = [(TyVar, (Int, LocSpecType))] -> [(TyVar, LocSpecType)]
strengthenSigs ([(TyVar, (Int, LocSpecType))] -> [(TyVar, LocSpecType)])
-> ([[(TyVar, (Int, LocSpecType))]]
    -> [(TyVar, (Int, LocSpecType))])
-> [[(TyVar, (Int, LocSpecType))]]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(TyVar, (Int, LocSpecType))]] -> [(TyVar, (Int, LocSpecType))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(TyVar, (Int, LocSpecType))]] -> [(TyVar, LocSpecType)])
-> [[(TyVar, (Int, LocSpecType))]] -> [(TyVar, LocSpecType)]
forall a b. (a -> b) -> a -> b
$
                  [ [(TyVar
v, (Int
0, LocSpecType
t)) | (TyVar
v, LocSpecType
t,Maybe [Located Expr]
_) <- [(TyVar, LocSpecType, Maybe [Located Expr])]
mySigs                         ]   -- NOTE: these weights are to priortize
                  , [(TyVar
v, (Int
1, LocSpecType
t)) | (TyVar
v, LocSpecType
t  ) <- MeasEnv -> [(TyVar, LocSpecType)]
makeMthSigs MeasEnv
measEnv            ]   -- user defined sigs OVER auto-generated
                  , [(TyVar
v, (Int
2, LocSpecType
t)) | (TyVar
v, LocSpecType
t  ) <- Env
-> BareRTEnv
-> [(ModName, Spec Symbol BareType)]
-> [(TyVar, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv [(ModName, Spec Symbol BareType)]
allSpecs ]   -- during the strengthening, i.e. to KEEP
                  , [(TyVar
v, (Int
3, LocSpecType
t)) | (TyVar
v, LocSpecType
t  ) <- Env
-> BareRTEnv
-> [(ModName, Spec Symbol BareType)]
-> [(TyVar, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv [(ModName, Spec Symbol BareType)]
allSpecs ]   -- the binders used in USER-defined sigs
                  ]                                                               -- as they appear in termination metrics
  newTys     <-  makeNewTypes env sigEnv allSpecs
  relation   <-  makeRelation env name sigEnv (Ms.relational mySpec)
  asmRel     <-  makeRelation env name sigEnv (Ms.asmRel mySpec)
  return (instances, SpSig
    { gsTySigs   = tySigs
    , gsAsmSigs  = asmSigs
    , gsAsmReflects = bimap getVar getVar <$> concatMap (asmReflectSigs . snd) allSpecs
    , gsRefSigs  = []
    , gsDicts    = dicts
    -- , gsMethods  = if noclasscheck cfg then [] else Bare.makeMethodTypes dicts (Bare.meClasses  measEnv) cbs
    , gsMethods  = if noclasscheck cfg then [] else Bare.makeMethodTypes (typeclass cfg) dicts (Bare.meClasses  measEnv) cbs
    , gsInSigs   = mempty
    , gsNewTypes = newTys
    , gsTexprs   = [ (v, t, es) | (v, t, Just es) <- mySigs ]
    , gsRelation = relation
    , gsAsmRel   = asmRel
    })
  where
    ([RInstance (Located BareType)]
instances, DEnv TyVar LocSpecType
dicts) = Env
-> SigEnv
-> (ModName, Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
-> ([RInstance (Located BareType)], DEnv TyVar LocSpecType)
Bare.makeSpecDictionaries Env
env SigEnv
sigEnv (ModName
name, Spec Symbol BareType
mySpec) (HashMap ModName (Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec Symbol BareType)
specs)
    allSpecs :: [(ModName, Spec Symbol BareType)]
allSpecs   = (ModName
name, Spec Symbol BareType
mySpec) (ModName, Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
-> [(ModName, Spec Symbol BareType)]
forall a. a -> [a] -> [a]
: HashMap ModName (Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec Symbol BareType)
specs
    rtEnv :: BareRTEnv
rtEnv      = SigEnv -> BareRTEnv
Bare.sigRTEnv SigEnv
sigEnv
    getVar :: Located LHName -> TyVar
getVar Located LHName
sym = case HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env Located LHName
sym of
      Right TyVar
x -> TyVar
x
      Left [Error]
_ -> Maybe SrcSpan -> [Char] -> TyVar
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
sym) [Char]
"function to reflect not in scope"

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

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

makeInlSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeInlSigs :: Env
-> BareRTEnv
-> [(ModName, Spec Symbol BareType)]
-> [(TyVar, LocSpecType)]
makeInlSigs Env
env BareRTEnv
rtEnv
  = BareRTEnv
-> (TyVar -> SpecType) -> [TyVar] -> [(TyVar, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv (Bool -> TyVar -> SpecType
CoreToLogic.inlineSpecType (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)))
  ([TyVar] -> [(TyVar, LocSpecType)])
-> ([(ModName, Spec Symbol BareType)] -> [TyVar])
-> [(ModName, Spec Symbol BareType)]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName, Spec Symbol BareType) -> [TyVar])
-> [(ModName, Spec Symbol BareType)] -> [TyVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Located LHName -> TyVar) -> [Located LHName] -> [TyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Located LHName -> TyVar
lookupFunctionId Env
env) ([Located LHName] -> [TyVar])
-> ((ModName, Spec Symbol BareType) -> [Located LHName])
-> (ModName, Spec Symbol BareType)
-> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList (HashSet (Located LHName) -> [Located LHName])
-> ((ModName, Spec Symbol BareType) -> HashSet (Located LHName))
-> (ModName, Spec Symbol BareType)
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.inlines (Spec Symbol BareType -> HashSet (Located LHName))
-> ((ModName, Spec Symbol BareType) -> Spec Symbol BareType)
-> (ModName, Spec Symbol BareType)
-> HashSet (Located LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec Symbol BareType) -> Spec Symbol BareType
forall a b. (a, b) -> b
snd)

makeMsrSigs :: Bare.Env -> BareRTEnv -> [(ModName, Ms.BareSpec)] -> [(Ghc.Var, LocSpecType)]
makeMsrSigs :: Env
-> BareRTEnv
-> [(ModName, Spec Symbol BareType)]
-> [(TyVar, LocSpecType)]
makeMsrSigs Env
env BareRTEnv
rtEnv
  = BareRTEnv
-> (TyVar -> SpecType) -> [TyVar] -> [(TyVar, LocSpecType)]
makeLiftedSigs BareRTEnv
rtEnv (Bool -> TyVar -> SpecType
CoreToLogic.inlineSpecType (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)))
  ([TyVar] -> [(TyVar, LocSpecType)])
-> ([(ModName, Spec Symbol BareType)] -> [TyVar])
-> [(ModName, Spec Symbol BareType)]
-> [(TyVar, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ModName, Spec Symbol BareType) -> [TyVar])
-> [(ModName, Spec Symbol BareType)] -> [TyVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Located LHName -> TyVar) -> [Located LHName] -> [TyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Located LHName -> TyVar
lookupFunctionId Env
env) ([Located LHName] -> [TyVar])
-> ((ModName, Spec Symbol BareType) -> [Located LHName])
-> (ModName, Spec Symbol BareType)
-> [TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList (HashSet (Located LHName) -> [Located LHName])
-> ((ModName, Spec Symbol BareType) -> HashSet (Located LHName))
-> (ModName, Spec Symbol BareType)
-> [Located LHName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.hmeas (Spec Symbol BareType -> HashSet (Located LHName))
-> ((ModName, Spec Symbol BareType) -> Spec Symbol BareType)
-> (ModName, Spec Symbol BareType)
-> HashSet (Located LHName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, Spec Symbol BareType) -> Spec Symbol BareType
forall a b. (a, b) -> b
snd)

lookupFunctionId :: Bare.Env -> Located LHName -> Ghc.Id
lookupFunctionId :: Env -> Located LHName -> TyVar
lookupFunctionId Env
env Located LHName
x =
    ([Error] -> TyVar)
-> (TyVar -> TyVar) -> Either [Error] TyVar -> TyVar
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe SrcSpan -> [Char] -> [Error] -> TyVar
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (SrcSpan -> Maybe SrcSpan) -> SrcSpan -> Maybe SrcSpan
forall a b. (a -> b) -> a -> b
$ Located LHName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located LHName
x) [Char]
"function not found") TyVar -> TyVar
forall a. a -> a
id (Either [Error] TyVar -> TyVar) -> Either [Error] TyVar -> TyVar
forall a b. (a -> b) -> a -> b
$
    HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env Located LHName
x

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

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

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

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


makeAsmSigs :: Bare.Env -> Bare.SigEnv -> ModName -> [(ModName, Ms.BareSpec)] -> Bare.Lookup [(Ghc.Var, LocSpecType)]
makeAsmSigs :: Env
-> SigEnv
-> ModName
-> [(ModName, Spec Symbol BareType)]
-> Lookup [(TyVar, LocSpecType)]
makeAsmSigs Env
env SigEnv
sigEnv ModName
myName [(ModName, Spec Symbol BareType)]
specs = do
  raSigs <- Env
-> ModName
-> [(ModName, Spec Symbol BareType)]
-> Lookup [(ModName, TyVar, Located BareType)]
rawAsmSigs Env
env ModName
myName [(ModName, Spec Symbol BareType)]
specs
  return [ (x, t) | (name, x, bt) <- raSigs, let t = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name (TyVar -> PlugTV TyVar
forall v. v -> PlugTV v
Bare.LqTV TyVar
x) Located BareType
bt ]

rawAsmSigs :: Bare.Env -> ModName -> [(ModName, Ms.BareSpec)] -> Bare.Lookup [(ModName, Ghc.Var, LocBareType)]
rawAsmSigs :: Env
-> ModName
-> [(ModName, Spec Symbol BareType)]
-> Lookup [(ModName, TyVar, Located BareType)]
rawAsmSigs Env
env ModName
myName [(ModName, Spec Symbol BareType)]
specs = do
  aSigs <- Env
-> ModName
-> [(ModName, Spec Symbol BareType)]
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
allAsmSigs Env
env ModName
myName [(ModName, Spec Symbol BareType)]
specs
  return [ (m, v, t) | (v, sigs) <- aSigs, let (m, t) = myAsmSig v sigs ]

myAsmSig :: Ghc.Var -> [(Bool, ModName, LocBareType)] -> (ModName, LocBareType)
myAsmSig :: TyVar
-> [(Bool, ModName, Located BareType)]
-> (ModName, Located BareType)
myAsmSig TyVar
v [(Bool, ModName, Located BareType)]
sigs = (ModName, Located BareType)
-> Maybe (ModName, Located BareType) -> (ModName, Located BareType)
forall a. a -> Maybe a -> a
Mb.fromMaybe (ModName, Located BareType)
forall {a}. a
errImp (Maybe (ModName, Located BareType)
mbHome Maybe (ModName, Located BareType)
-> Maybe (ModName, Located BareType)
-> Maybe (ModName, Located BareType)
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` Maybe (ModName, Located BareType)
mbImp)
  where
    mbHome :: Maybe (ModName, Located BareType)
mbHome      = ([(ModName, Located BareType)] -> UserError)
-> [(ModName, Located BareType)]
-> Maybe (ModName, Located BareType)
forall e a. Exception e => ([a] -> e) -> [a] -> Maybe a
takeUnique [(ModName, Located BareType)] -> UserError
forall {a} {a}. [(a, Located a)] -> UserError
mkErr                  [(ModName, Located BareType)]
sigsHome
    -- In case we import multiple specifications for the same function stemming from `assume-reflect` from different modules, we want
    -- to follow the same convention as in other places and so take the last one in alphabetical order and shadow the others
    mbImp :: Maybe (ModName, Located BareType)
mbImp       = ((ModName, Located BareType) -> ModName)
-> [(ModName, Located BareType)]
-> Maybe (ModName, Located BareType)
forall b a. Ord b => (a -> b) -> [a] -> Maybe a
takeBiggest   (ModName, Located BareType) -> ModName
forall a b. (a, b) -> a
fst ([(Int, (ModName, Located BareType))]
-> [(ModName, Located BareType)]
forall k a. (Eq k, Ord k, Hashable k) => [(k, a)] -> [a]
Misc.firstGroup [(Int, (ModName, Located BareType))]
sigsImp) -- see [NOTE:Prioritize-Home-Spec]
    sigsHome :: [(ModName, Located BareType)]
sigsHome    = [(ModName
m, Located BareType
t)      | (Bool
True,  ModName
m, Located BareType
t) <- [(Bool, ModName, Located BareType)]
sigs ]
    sigsImp :: [(Int, (ModName, Located BareType))]
sigsImp     = [Char]
-> [(Int, (ModName, Located BareType))]
-> [(Int, (ModName, Located BareType))]
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"SIGS-IMP: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyVar -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp TyVar
v)
                  [(Int
d, (ModName
m, Located BareType
t)) | (Bool
False, ModName
m, Located BareType
t) <- [(Bool, ModName, Located BareType)]
sigs, let d :: Int
d = Symbol -> ModName -> Int
nameDistance Symbol
vName ModName
m]
    mkErr :: [(a, Located a)] -> UserError
mkErr [(a, Located a)]
ts    = SrcSpan -> Doc -> ListNE SrcSpan -> UserError
forall t. SrcSpan -> Doc -> ListNE SrcSpan -> TError t
ErrDupSpecs (TyVar -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan TyVar
v) (TyVar -> Doc
forall a. PPrint a => a -> Doc
F.pprint TyVar
v) (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan)
-> ((a, Located a) -> SourcePos) -> (a, Located a) -> SrcSpan
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> SourcePos
forall a. Located a -> SourcePos
F.loc (Located a -> SourcePos)
-> ((a, Located a) -> Located a) -> (a, Located a) -> SourcePos
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Located a) -> Located a
forall a b. (a, b) -> b
snd ((a, Located a) -> SrcSpan) -> [(a, Located a)] -> ListNE SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Located a)]
ts) :: UserError
    errImp :: a
errImp      = Maybe SrcSpan -> [Char] -> a
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"myAsmSig: cannot happen as sigs is non-null"
    vName :: Symbol
vName       = Symbol -> Symbol
GM.takeModuleNames (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyVar
v)

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

expandTermExpr :: BareRTEnv -> Located F.Expr -> Located F.Expr
expandTermExpr :: BareRTEnv -> Located Expr -> Located Expr
expandTermExpr BareRTEnv
rtEnv Located Expr
le
        = Located Expr -> Expr -> Located Expr
forall l b. Loc l => l -> b -> Located b
F.atLoc Located Expr
le (BareRTEnv -> SourcePos -> Expr -> Expr
forall a. Expand a => BareRTEnv -> SourcePos -> a -> a
Bare.expand BareRTEnv
rtEnv SourcePos
l Expr
e)
  where
    l :: SourcePos
l   = Located Expr -> SourcePos
forall a. Located a -> SourcePos
F.loc Located Expr
le
    e :: Expr
e   = Located Expr -> Expr
forall a. Located a -> a
F.val Located Expr
le

makeVarTExprs :: Bare.Env -> Ms.BareSpec -> Bare.Lookup [(Ghc.Var, [Located F.Expr])]
makeVarTExprs :: Env
-> Spec Symbol BareType -> Either [Error] [(TyVar, [Located Expr])]
makeVarTExprs Env
env Spec Symbol BareType
spec =
  [(Located LHName, [Located Expr])]
-> ((Located LHName, [Located Expr])
    -> Either [Error] (TyVar, [Located Expr]))
-> Either [Error] [(TyVar, [Located Expr])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec Symbol BareType -> [(Located LHName, [Located Expr])]
forall lname ty.
Spec lname ty -> [(Located LHName, [Located (ExprV lname)])]
Ms.termexprs Spec Symbol BareType
spec) (((Located LHName, [Located Expr])
  -> Either [Error] (TyVar, [Located Expr]))
 -> Either [Error] [(TyVar, [Located Expr])])
-> ((Located LHName, [Located Expr])
    -> Either [Error] (TyVar, [Located Expr]))
-> Either [Error] [(TyVar, [Located Expr])]
forall a b. (a -> b) -> a -> b
$ \(Located LHName
x, [Located Expr]
es) -> do
    vx <- HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env Located LHName
x
    return (vx, es)

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

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

takeBiggest :: (Ord b) => (a -> b) -> [a] -> Maybe a
takeBiggest :: forall b a. Ord b => (a -> b) -> [a] -> Maybe a
takeBiggest a -> b
_ []  = Maybe a
forall a. Maybe a
Nothing
takeBiggest a -> b
f [a]
xs  = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ (a -> a -> Ordering) -> [a] -> a
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
L.maximumBy (b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (b -> b -> Ordering) -> (a -> b) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f) [a]
xs

allAsmSigs :: Bare.Env -> ModName -> [(ModName, Ms.BareSpec)] ->
              Bare.Lookup [(Ghc.Var, [(Bool, ModName, LocBareType)])]
allAsmSigs :: Env
-> ModName
-> [(ModName, Spec Symbol BareType)]
-> Lookup [(TyVar, [(Bool, ModName, Located BareType)])]
allAsmSigs Env
env ModName
myName [(ModName, Spec Symbol BareType)]
specs = do
  let aSigs :: [(ModName, Bool, Located LHName, Located BareType)]
aSigs = [ (ModName
name, Bool
locallyDefined, Located LHName
x, Located BareType
t) | (ModName
name, Spec Symbol BareType
spec) <- [(ModName, Spec Symbol BareType)]
specs
                                   , (Bool
locallyDefined, Located LHName
x, Located BareType
t) <- ModName
-> ModName
-> Spec Symbol BareType
-> [(Bool, Located LHName, Located BareType)]
getAsmSigs ModName
myName ModName
name Spec Symbol BareType
spec ]
  vSigs    <- [(ModName, Bool, Located LHName, Located BareType)]
-> ((ModName, Bool, Located LHName, Located BareType)
    -> Either [Error] (TyVar, (Bool, ModName, Located BareType)))
-> Either [Error] [(TyVar, (Bool, ModName, Located BareType))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, Bool, Located LHName, Located BareType)]
aSigs (((ModName, Bool, Located LHName, Located BareType)
  -> Either [Error] (TyVar, (Bool, ModName, Located BareType)))
 -> Either [Error] [(TyVar, (Bool, ModName, Located BareType))])
-> ((ModName, Bool, Located LHName, Located BareType)
    -> Either [Error] (TyVar, (Bool, ModName, Located BareType)))
-> Either [Error] [(TyVar, (Bool, ModName, Located BareType))]
forall a b. (a -> b) -> a -> b
$ \(ModName
name, Bool
locallyDefined, Located LHName
x, Located BareType
t) -> do
                v <- HasCallStack => Env -> Located LHName -> Either [Error] TyVar
Env -> Located LHName -> Either [Error] TyVar
Bare.lookupGhcIdLHName Env
env Located LHName
x
                return (v, (locallyDefined, name, t))
  return $ Misc.groupList
    [ (v, z) | (v, z) <- vSigs
      -- TODO: we require signatures to be in scope because LH includes them in
      -- the environment of contraints sometimes. The criteria to add bindings to
      -- constraints should account instead for what logic functions are used in
      -- the constraints, which should be easier to do when precise renaming has
      -- been implemented for expressions and reflected functions.
    , isUsedExternalVar v ||
      isInScope v ||
      isNonTopLevelVar v -- Keep assumptions about non-top-level bindings
    ]
  where
    isUsedExternalVar :: Ghc.Var -> Bool
    isUsedExternalVar :: TyVar -> Bool
isUsedExternalVar TyVar
v = case TyVar -> IdDetails
Ghc.idDetails TyVar
v of
      Ghc.DataConWrapId DataCon
dc ->
        TyVar -> Name
forall a. NamedThing a => a -> Name
Ghc.getName TyVar
v Name -> NameSet -> Bool
`Ghc.elemNameSet` Env -> NameSet
Bare.reUsedExternals Env
env
         Bool -> Bool -> Bool
||
        TyVar -> Name
forall a. NamedThing a => a -> Name
Ghc.getName (DataCon -> TyVar
Ghc.dataConWorkId DataCon
dc) Name -> NameSet -> Bool
`Ghc.elemNameSet` Env -> NameSet
Bare.reUsedExternals Env
env
      IdDetails
_ ->
        TyVar -> Name
forall a. NamedThing a => a -> Name
Ghc.getName TyVar
v Name -> NameSet -> Bool
`Ghc.elemNameSet` Env -> NameSet
Bare.reUsedExternals Env
env

    isInScope :: Ghc.Var -> Bool
    isInScope :: TyVar -> Bool
isInScope TyVar
v0 =
      let inScope :: a -> Bool
inScope a
v = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Maybe (GlobalRdrEltX GREInfo) -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Maybe (GlobalRdrEltX GREInfo) -> Bool)
-> Maybe (GlobalRdrEltX GREInfo) -> Bool
forall a b. (a -> b) -> a -> b
$
            GlobalRdrEnv -> Name -> Maybe (GlobalRdrEltX GREInfo)
forall info.
Outputable info =>
GlobalRdrEnvX info -> Name -> Maybe (GlobalRdrEltX info)
Ghc.lookupGRE_Name
              (TcGblEnv -> GlobalRdrEnv
Ghc.tcg_rdr_env (TcGblEnv -> GlobalRdrEnv) -> TcGblEnv -> GlobalRdrEnv
forall a b. (a -> b) -> a -> b
$ Env -> TcGblEnv
Bare.reTcGblEnv Env
env)
              (a -> Name
forall a. NamedThing a => a -> Name
Ghc.getName a
v)
       in -- Names of data constructors are not found in the variable namespace
          -- so we look them instead in the data constructor namespace.
          case TyVar -> IdDetails
Ghc.idDetails TyVar
v0 of
            Ghc.DataConWrapId DataCon
dc -> DataCon -> Bool
forall a. NamedThing a => a -> Bool
inScope DataCon
dc
            Ghc.DataConWorkId DataCon
dc -> DataCon -> Bool
forall a. NamedThing a => a -> Bool
inScope DataCon
dc
            IdDetails
_ -> TyVar -> Bool
forall a. NamedThing a => a -> Bool
inScope TyVar
v0

    isNonTopLevelVar :: a -> Bool
isNonTopLevelVar = Maybe (GenModule Unit) -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (Maybe (GenModule Unit) -> Bool)
-> (a -> Maybe (GenModule Unit)) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Maybe (GenModule Unit)
Ghc.nameModule_maybe (Name -> Maybe (GenModule Unit))
-> (a -> Name) -> a -> Maybe (GenModule Unit)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Name
forall a. NamedThing a => a -> Name
Ghc.getName

getAsmSigs :: ModName -> ModName -> Ms.BareSpec -> [(Bool, Located LHName, LocBareType)]
getAsmSigs :: ModName
-> ModName
-> Spec Symbol BareType
-> [(Bool, Located LHName, Located BareType)]
getAsmSigs ModName
myName ModName
name Spec Symbol BareType
spec
  | ModName
myName ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName
name = [ (Bool
True, Located LHName
x,  Located BareType
t) | (Located LHName
x, Located BareType
t) <- Spec Symbol BareType -> [(Located LHName, Located BareType)]
forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
Ms.asmSigs Spec Symbol BareType
spec ] -- MUST    resolve, or error
  | Bool
otherwise      =
      [ (Bool
False, Located LHName
x, Located BareType
t)
      | (Located LHName
x, Located BareType
t) <- Spec Symbol BareType -> [(Located LHName, Located BareType)]
forall lname ty. Spec lname ty -> [(Located LHName, Located ty)]
Ms.asmSigs Spec Symbol BareType
spec
                  [(Located LHName, Located BareType)]
-> [(Located LHName, Located BareType)]
-> [(Located LHName, Located BareType)]
forall a. [a] -> [a] -> [a]
++ Spec Symbol BareType -> [(Located LHName, Located BareType)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located (BareTypeV lname))]
Ms.sigs Spec Symbol BareType
spec
      ]

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 Symbol BareType)]
-> Lookup [(TyCon, LocSpecType)]
makeNewTypes Env
env SigEnv
sigEnv [(ModName, Spec Symbol BareType)]
specs = do
  ([[(TyCon, LocSpecType)]] -> [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
-> Lookup [(TyCon, LocSpecType)]
forall a b. (a -> b) -> Either [Error] a -> Either [Error] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(TyCon, LocSpecType)]] -> [(TyCon, LocSpecType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Either [Error] [[(TyCon, LocSpecType)]]
 -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
-> Lookup [(TyCon, LocSpecType)]
forall a b. (a -> b) -> a -> b
$
    [(ModName, DataDecl)]
-> ((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(ModName, DataDecl)]
nameDecls (((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
 -> Either [Error] [[(TyCon, LocSpecType)]])
-> ((ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)])
-> Either [Error] [[(TyCon, LocSpecType)]]
forall a b. (a -> b) -> a -> b
$ (ModName -> DataDecl -> Lookup [(TyCon, LocSpecType)])
-> (ModName, DataDecl) -> Lookup [(TyCon, LocSpecType)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Env
-> SigEnv -> ModName -> DataDecl -> Lookup [(TyCon, LocSpecType)]
makeNewType Env
env SigEnv
sigEnv)
  where
    nameDecls :: [(ModName, DataDecl)]
nameDecls = [(ModName
name, DataDecl
d) | (ModName
name, Spec Symbol BareType
spec) <- [(ModName, Spec Symbol BareType)]
specs, DataDecl
d <- Spec Symbol BareType -> [DataDecl]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
Ms.newtyDecls Spec Symbol BareType
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
  tcMb <- Env -> ModName -> DataName -> Lookup (Maybe TyCon)
Bare.lookupGhcDnTyCon Env
env ModName
name DataName
tcName
  case tcMb of
    Just TyCon
tc -> [(TyCon, LocSpecType)] -> Lookup [(TyCon, LocSpecType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TyCon
tc, LocSpecType
lst)]
    Maybe TyCon
_       -> [(TyCon, LocSpecType)] -> Lookup [(TyCon, LocSpecType)]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  where
    tcName :: DataName
tcName                    = DataDecl -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName DataDecl
d
    lst :: LocSpecType
lst                       = Env
-> SigEnv
-> ModName
-> PlugTV TyVar
-> Located BareType
-> LocSpecType
Bare.cookSpecType Env
env SigEnv
sigEnv ModName
name PlugTV TyVar
forall v. PlugTV v
Bare.GenTV Located BareType
bt
    bt :: Located BareType
bt                        = DataName -> SourcePos -> [DataCtorP BareType] -> Located BareType
forall {a} {a}.
PPrint a =>
a -> SourcePos -> [DataCtorP a] -> Located a
getTy DataName
tcName (DataDecl -> SourcePos
forall v ty. DataDeclP v ty -> SourcePos
tycSrcPos DataDecl
d) ([DataCtorP BareType]
-> Maybe [DataCtorP BareType] -> [DataCtorP BareType]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] (DataDecl -> Maybe [DataCtorP BareType]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
tycDCons DataDecl
d))
    getTy :: a -> SourcePos -> [DataCtorP a] -> Located a
getTy a
_ SourcePos
l [DataCtorP a
c]
      | [(LHName
_, a
t)] <- DataCtorP a -> [(LHName, a)]
forall ty. DataCtorP ty -> [(LHName, ty)]
dcFields DataCtorP a
c = SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l a
t
    getTy a
n SourcePos
l [DataCtorP a]
_                = UserError -> Located a
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (a -> SourcePos -> UserError
forall {a}. PPrint a => a -> SourcePos -> UserError
mkErr a
n SourcePos
l)
    mkErr :: a -> SourcePos -> UserError
mkErr a
n SourcePos
l                  = SrcSpan -> Doc -> UserError
forall t. SrcSpan -> Doc -> TError t
ErrOther (SourcePos -> SrcSpan
GM.sourcePosSrcSpan SourcePos
l) (Doc
"Bad new type declaration:" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PPrint a => a -> Doc
F.pprint a
n) :: UserError

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

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

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

makeSizeInv :: F.Symbol -> Located SpecType -> Located SpecType
makeSizeInv :: Symbol -> LocSpecType -> LocSpecType
makeSizeInv Symbol
s LocSpecType
lst = LocSpecType
lst{val = go (val lst)}
  where go :: RTypeV v c tv (UReftV v (ReftV Symbol))
-> RTypeV v c tv (UReftV v (ReftV Symbol))
go (RApp c
c [RTypeV v c tv (UReftV v (ReftV Symbol))]
ts [RTPropV v c tv (UReftV v (ReftV Symbol))]
rs UReftV v (ReftV Symbol)
r) = c
-> [RTypeV v c tv (UReftV v (ReftV Symbol))]
-> [RTPropV v c tv (UReftV v (ReftV Symbol))]
-> UReftV v (ReftV Symbol)
-> RTypeV v c tv (UReftV v (ReftV Symbol))
forall v c tv r.
c
-> [RTypeV v c tv r] -> [RTPropV v c tv r] -> r -> RTypeV v c tv r
RApp c
c [RTypeV v c tv (UReftV v (ReftV Symbol))]
ts [RTPropV v c tv (UReftV v (ReftV Symbol))]
rs (UReftV v (ReftV Symbol)
r UReftV v (ReftV Symbol)
-> UReftV v (ReftV Symbol) -> UReftV v (ReftV Symbol)
forall r. Reftable r => r -> r -> r
`meet` UReftV v (ReftV Symbol)
forall {v}. Monoid (PredicateV v) => UReftV v (ReftV Symbol)
nat)
        go (RAllT RTVUV v c tv
a RTypeV v c tv (UReftV v (ReftV Symbol))
t UReftV v (ReftV Symbol)
r)    = RTVUV v c tv
-> RTypeV v c tv (UReftV v (ReftV Symbol))
-> UReftV v (ReftV Symbol)
-> RTypeV v c tv (UReftV v (ReftV Symbol))
forall v c tv r.
RTVUV v c tv -> RTypeV v c tv r -> r -> RTypeV v c tv r
RAllT RTVUV v c tv
a (RTypeV v c tv (UReftV v (ReftV Symbol))
-> RTypeV v c tv (UReftV v (ReftV Symbol))
go RTypeV v c tv (UReftV v (ReftV Symbol))
t) UReftV v (ReftV Symbol)
r
        go RTypeV v c tv (UReftV v (ReftV Symbol))
t = RTypeV v c tv (UReftV v (ReftV Symbol))
t
        nat :: UReftV v (ReftV Symbol)
nat  = ReftV Symbol -> PredicateV v -> UReftV v (ReftV Symbol)
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ((Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft (Symbol
vv_, Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
Le (Constant -> Expr
forall v. Constant -> ExprV v
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Constant
I Integer
0) (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
s) (Symbol -> Expr
forall a. Symbolic a => a -> Expr
eVar Symbol
vv_))))
                       PredicateV v
forall a. Monoid a => a
mempty

makeMeasureInvariants :: GhcSpecSig -> Ms.BareSpec -> ([(Maybe Ghc.Var, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants :: GhcSpecSig
-> Spec Symbol BareType
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
makeMeasureInvariants GhcSpecSig
sig Spec Symbol BareType
mySpec
  = [Maybe UnSortedExpr] -> [UnSortedExpr]
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe UnSortedExpr] -> [UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
-> ([(Maybe TyVar, LocSpecType)], [UnSortedExpr])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)]
-> ([(Maybe TyVar, LocSpecType)], [Maybe UnSortedExpr])
forall a b. [(a, b)] -> ([a], [b])
unzip ((Located LHName, (TyVar, LocSpecType))
-> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)
measureTypeToInv ((Located LHName, (TyVar, LocSpecType))
 -> ((Maybe TyVar, LocSpecType), Maybe UnSortedExpr))
-> [(Located LHName, (TyVar, LocSpecType))]
-> [((Maybe TyVar, LocSpecType), Maybe UnSortedExpr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Located LHName
x, (TyVar
y, LocSpecType
ty)) | Located LHName
x <- [Located LHName]
xs, (TyVar
y, LocSpecType
ty) <- [(TyVar, LocSpecType)]
sigs
                                         , Located LHName
x Located LHName -> Located LHName -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar -> Located LHName
makeGHCLHNameLocatedFromId TyVar
y ])
  where
    sigs :: [(TyVar, LocSpecType)]
sigs = GhcSpecSig -> [(TyVar, LocSpecType)]
gsTySigs GhcSpecSig
sig
    xs :: [Located LHName]
xs   = HashSet (Located LHName) -> [Located LHName]
forall a. HashSet a -> [a]
S.toList (Spec Symbol BareType -> HashSet (Located LHName)
forall lname ty. Spec lname ty -> HashSet (Located LHName)
Ms.hmeas  Spec Symbol BareType
mySpec)

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

mkInvariant :: Located LHName -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant :: Located LHName -> Symbol -> SpecType -> SpecType -> SpecType
mkInvariant Located LHName
x Symbol
z SpecType
t SpecType
tr = SpecType -> RReft -> SpecType
forall r v c tv.
Reftable r =>
RTypeV v c tv r -> r -> RTypeV v c tv r
strengthen (RReft -> RReft
forall r. Reftable r => r -> r
top (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
t) (ReftV Symbol -> PredicateV Symbol -> RReft
forall v r. r -> PredicateV v -> UReftV v r
MkUReft ReftV Symbol
reft' PredicateV Symbol
forall a. Monoid a => a
mempty)
      where
        reft' :: ReftV Symbol
reft' = ReftV Symbol
-> ((Symbol, Expr) -> ReftV Symbol)
-> Maybe (Symbol, Expr)
-> ReftV Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe ReftV Symbol
forall a. Monoid a => a
mempty (Symbol, Expr) -> ReftV Symbol
forall v. (Symbol, ExprV v) -> ReftV v
Reft Maybe (Symbol, Expr)
mreft
        mreft :: Maybe (Symbol, Expr)
mreft = Located LHName
-> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
mkReft Located LHName
x Symbol
z SpecType
t SpecType
tr


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


-- REBARE: formerly, makeGhcSpec3
-------------------------------------------------------------------------------------------
makeSpecName :: Bare.TycEnv -> Bare.MeasEnv -> [Ghc.Id] -> GhcSpecNames
-------------------------------------------------------------------------------------------
makeSpecName :: TycEnv -> MeasEnv -> [TyVar] -> GhcSpecNames
makeSpecName TycEnv
tycEnv MeasEnv
measEnv [TyVar]
dataConIds = SpNames
  { gsDconsP :: [Located DataCon]
gsDconsP   = [ DataConP -> DataCon -> Located DataCon
forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dc (DataConP -> DataCon
dcpCon DataConP
dc) | DataConP
dc <- [DataConP]
datacons [DataConP] -> [DataConP] -> [DataConP]
forall a. [a] -> [a] -> [a]
++ [DataConP]
cls ]
  , gsTconsP :: [TyConP]
gsTconsP   = [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
  , gsDataConIds :: [TyVar]
gsDataConIds = [TyVar]
dataConIds
  }
  where
    datacons, cls :: [DataConP]
    datacons :: [DataConP]
datacons   = TycEnv -> [DataConP]
Bare.tcDataCons TycEnv
tycEnv
    cls :: [DataConP]
cls        = [Char] -> [DataConP] -> [DataConP]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"meClasses" ([DataConP] -> [DataConP]) -> [DataConP] -> [DataConP]
forall a b. (a -> b) -> a -> b
$ MeasEnv -> [DataConP]
Bare.meClasses MeasEnv
measEnv
    tycons :: [TyConP]
tycons     = TycEnv -> [TyConP]
Bare.tcTyCons   TycEnv
tycEnv


-- REBARE: formerly, makeGhcCHOP1
-- split into two to break circular dependency. we need dataconmap for core2logic
-------------------------------------------------------------------------------------------
makeTycEnv0 :: Config -> ModName -> Bare.Env -> TCEmb Ghc.TyCon -> Ms.BareSpec -> Bare.ModSpecs
           -> (Diagnostics,  [Located DataConP], Bare.TycEnv)
-------------------------------------------------------------------------------------------
makeTycEnv0 :: Config
-> ModName
-> Env
-> TCEmb TyCon
-> Spec Symbol BareType
-> HashMap ModName (Spec Symbol BareType)
-> (Diagnostics, [Located DataConP], TycEnv)
makeTycEnv0 Config
cfg ModName
myName Env
env TCEmb TyCon
embs Spec Symbol BareType
mySpec HashMap ModName (Spec Symbol BareType)
iSpecs = (Diagnostics
diag0 Diagnostics -> Diagnostics -> Diagnostics
forall a. Semigroup a => a -> a -> a
<> Diagnostics
diag1, [Located DataConP]
datacons, Bare.TycEnv
  { tcTyCons :: [TyConP]
tcTyCons      = [TyConP]
tycons
  , tcDataCons :: [DataConP]
tcDataCons    = [DataConP]
forall a. Monoid a => a
mempty -- val <$> datacons
    -- See the documentation of @addOpaqueReflMeas@. The selectors here are only
    -- those belonging to types mentioned in the types of functions defined in
    -- the current module.
  , tcSelMeasures :: [Measure SpecType DataCon]
tcSelMeasures = [Measure SpecType DataCon]
dcSelectors
  , tcSelVars :: [(TyVar, LocSpecType)]
tcSelVars     = [(TyVar, LocSpecType)]
forall a. Monoid a => a
mempty -- recSelectors
  , tcTyConMap :: TyConMap
tcTyConMap    = TyConMap
tyi
  , tcAdts :: [DataDecl]
tcAdts        = [DataDecl]
adts
  , tcDataConMap :: DataConMap
tcDataConMap  = DataConMap
dm
  , tcEmbs :: TCEmb TyCon
tcEmbs        = TCEmb TyCon
embs
  , tcName :: ModName
tcName        = ModName
myName
  })
  where
    ([(ModName, TyConP, Maybe DataPropDecl)]
tcDds, [[Located DataConP]]
dcs)   = ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
conTys
    (Diagnostics
diag0, ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
conTys) = Lookup
  ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> (Diagnostics,
    ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
forall a. Monoid a => Lookup a -> (Diagnostics, a)
withDiagnostics (Lookup
   ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
 -> (Diagnostics,
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])))
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> (Diagnostics,
    ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
forall a b. (a -> b) -> a -> b
$ ModName
-> Env
-> [(ModName, Spec Symbol BareType)]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes ModName
myName Env
env [(ModName, Spec Symbol BareType)]
specs
    specs :: [(ModName, Spec Symbol BareType)]
specs         = (ModName
myName, Spec Symbol BareType
mySpec) (ModName, Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
-> [(ModName, Spec Symbol BareType)]
forall a. a -> [a] -> [a]
: HashMap ModName (Spec Symbol BareType)
-> [(ModName, Spec Symbol BareType)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ModName (Spec Symbol BareType)
iSpecs
    tcs :: [TyConP]
tcs           = (ModName, TyConP, Maybe DataPropDecl) -> TyConP
forall a b c. (a, b, c) -> b
Misc.snd3 ((ModName, TyConP, Maybe DataPropDecl) -> TyConP)
-> [(ModName, TyConP, Maybe DataPropDecl)] -> [TyConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(ModName, TyConP, Maybe DataPropDecl)]
tcDds
    tyi :: TyConMap
tyi           = TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap
makeTyConInfo TCEmb TyCon
embs [TyCon]
fiTcs [TyConP]
tycons
    -- tycons        = F.tracepp "TYCONS" $ Misc.replaceWith tcpCon tcs wiredTyCons
    -- datacons      =  Bare.makePluggedDataCons embs tyi (Misc.replaceWith (dcpCon . val) (F.tracepp "DATACONS" $ concat dcs) wiredDataCons)
    tycons :: [TyConP]
tycons        = [TyConP]
tcs [TyConP] -> [TyConP] -> [TyConP]
forall a. [a] -> [a] -> [a]
++ [TyConP]
wiredTyCons
    datacons :: [Located DataConP]
datacons      = Bool
-> TCEmb TyCon -> TyConMap -> Located DataConP -> Located DataConP
Bare.makePluggedDataCon (Config -> Bool
typeclass Config
cfg) TCEmb TyCon
embs TyConMap
tyi (Located DataConP -> Located DataConP)
-> [Located DataConP] -> [Located DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([[Located DataConP]] -> [Located DataConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Located DataConP]]
dcs [Located DataConP] -> [Located DataConP] -> [Located DataConP]
forall a. [a] -> [a] -> [a]
++ [Located DataConP]
wiredDataCons)
    tds :: [(ModName, TyCon, DataPropDecl)]
tds           = [(ModName
name, TyConP -> TyCon
tcpCon TyConP
tcp, DataPropDecl
dd) | (ModName
name, TyConP
tcp, Just DataPropDecl
dd) <- [(ModName, TyConP, Maybe DataPropDecl)]
tcDds]
    (Diagnostics
diag1, [DataDecl]
adts) = Config
-> TCEmb TyCon
-> ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [Located DataConP]
-> (Diagnostics, [DataDecl])
Bare.makeDataDecls Config
cfg TCEmb TyCon
embs ModName
myName [(ModName, TyCon, DataPropDecl)]
tds       [Located DataConP]
datacons
    dm :: DataConMap
dm            = [DataDecl] -> DataConMap
Bare.dataConMap [DataDecl]
adts
    dcSelectors :: [Measure SpecType DataCon]
dcSelectors   = (Located DataConP -> [Measure SpecType DataCon])
-> [Located DataConP] -> [Measure SpecType DataCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Config
-> DataConMap -> Located DataConP -> [Measure SpecType DataCon]
Bare.makeMeasureSelectors Config
cfg DataConMap
dm) (if Config -> Bool
reflection Config
cfg then Located DataConP
charDataConLocated DataConP -> [Located DataConP] -> [Located DataConP]
forall a. a -> [a] -> [a]
:[Located DataConP]
datacons else [Located DataConP]
datacons)
    fiTcs :: [TyCon]
fiTcs         = GhcSrc -> [TyCon]
_gsFiTcs (Env -> GhcSrc
Bare.reSrc Env
env)



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

-- REBARE: formerly, makeGhcCHOP2
-------------------------------------------------------------------------------------------
makeMeasEnv :: Bare.Env -> Bare.TycEnv -> Bare.SigEnv -> Bare.ModSpecs ->
               Bare.Lookup Bare.MeasEnv
-------------------------------------------------------------------------------------------
makeMeasEnv :: Env
-> TycEnv
-> SigEnv
-> HashMap ModName (Spec Symbol BareType)
-> Lookup MeasEnv
makeMeasEnv Env
env TycEnv
tycEnv SigEnv
sigEnv HashMap ModName (Spec Symbol BareType)
specs = do
  (cls, mts)  <- Env
-> SigEnv
-> ModName
-> HashMap ModName (Spec Symbol BareType)
-> Lookup ([DataConP], [(ModName, TyVar, LocSpecType)])
Bare.makeClasses        Env
env SigEnv
sigEnv ModName
name HashMap ModName (Spec Symbol BareType)
specs
  let dms      = Env
-> [(ModName, TyVar, LocSpecType)]
-> [(ModName, TyVar, LocSpecType)]
Bare.makeDefaultMethods Env
env [(ModName, TyVar, LocSpecType)]
mts
  measures0   <- mapM (Bare.makeMeasureSpec env sigEnv name) (M.toList specs)
  let measures = [MSpec SpecType DataCon] -> MSpec SpecType DataCon
forall a. Monoid a => [a] -> a
mconcat ([Measure SpecType DataCon] -> MSpec SpecType DataCon
forall ty. [Measure ty DataCon] -> MSpec ty DataCon
Ms.mkMSpec' [Measure SpecType DataCon]
dcSelectors MSpec SpecType DataCon
-> [MSpec SpecType DataCon] -> [MSpec SpecType DataCon]
forall a. a -> [a] -> [a]
: [MSpec SpecType DataCon]
measures0)
  let (cs, ms) = Bare.makeMeasureSpec'  (typeclass $ getConfig env)   measures
  let cms      = MSpec SpecType DataCon
-> [(Located LHName, CMeasure (RRType (ReftV Symbol)))]
forall c tv r2 t.
MSpec (RType c tv (UReft r2)) t
-> [(Located LHName, CMeasure (RType c tv r2))]
Bare.makeClassMeasureSpec MSpec SpecType DataCon
measures
  let cms'     = [ (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
l, CMeasure (RRType (ReftV Symbol)) -> RRType (ReftV Symbol)
forall ty. CMeasure ty -> ty
cSort CMeasure (RRType (ReftV Symbol))
t RRType (ReftV Symbol)
-> Located LHName -> Located (RRType (ReftV Symbol))
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Located LHName
l)  | (Located LHName
l, CMeasure (RRType (ReftV Symbol))
t) <- [(Located LHName, CMeasure (RRType (ReftV Symbol)))]
cms ]
  let ms'      = [ (LHName -> Symbol
lhNameToResolvedSymbol (Located LHName -> LHName
forall a. Located a -> a
F.val Located LHName
lx), Located LHName
-> RRType (ReftV Symbol) -> Located (RRType (ReftV Symbol))
forall l b. Loc l => l -> b -> Located b
F.atLoc Located LHName
lx RRType (ReftV Symbol)
t)
                 | (Located LHName
lx, RRType (ReftV Symbol)
t) <- [(Located LHName, RRType (ReftV Symbol))]
ms
                 , Maybe (Located (RRType (ReftV Symbol))) -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (LHName
-> [(LHName, Located (RRType (ReftV Symbol)))]
-> Maybe (Located (RRType (ReftV Symbol)))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Located LHName -> LHName
forall a. Located a -> a
val Located LHName
lx) [(LHName, Located (RRType (ReftV Symbol)))]
cms')
                 ]
  let cs'      = [ (TyVar
v, TyVar -> SpecType -> LocSpecType
forall {b}. NamedThing b => b -> SpecType -> LocSpecType
txRefs TyVar
v SpecType
t) | (TyVar
v, SpecType
t) <- Bool
-> TCEmb TyCon
-> [(TyVar, SpecType)]
-> [DataConP]
-> [(TyVar, SpecType)]
Bare.meetDataConSpec (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)) TCEmb TyCon
embs [(TyVar, SpecType)]
cs ([DataConP]
datacons [DataConP] -> [DataConP] -> [DataConP]
forall a. [a] -> [a] -> [a]
++ [DataConP]
cls)]
  return Bare.MeasEnv
    { meMeasureSpec = measures
    , meClassSyms   = map (first lhNameToResolvedSymbol) cms'
    , meSyms        = ms'
    , meDataCons    = cs'
    , meClasses     = cls
    , meMethods     = mts ++ dms
    , meOpaqueRefl  = mempty
    }
  where
    txRefs :: b -> SpecType -> LocSpecType
txRefs b
v SpecType
t    = TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs (SpecType
t SpecType -> Located b -> LocSpecType
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ b -> Located b
forall a. NamedThing a => a -> Located a
GM.locNamedThing b
v)
    tyi :: TyConMap
tyi           = TycEnv -> TyConMap
Bare.tcTyConMap    TycEnv
tycEnv
    dcSelectors :: [Measure SpecType DataCon]
dcSelectors   = TycEnv -> [Measure SpecType DataCon]
Bare.tcSelMeasures TycEnv
tycEnv
    datacons :: [DataConP]
datacons      = TycEnv -> [DataConP]
Bare.tcDataCons    TycEnv
tycEnv
    embs :: TCEmb TyCon
embs          = TycEnv -> TCEmb TyCon
Bare.tcEmbs        TycEnv
tycEnv
    name :: ModName
name          = TycEnv -> ModName
Bare.tcName        TycEnv
tycEnv


-- | Adds the opaque reflections to the measure environment
--
-- Returns a new environment that is the old one enhanced with the opaque
-- reflections.
--
-- At the moment this function also has the effect of adding selector and
-- checker measures for data constructors that are needed by reflected
-- functions. This even adds measures that are needed by functions reflected
-- from unfoldings (public and private), whose datatypes come from imported
-- modules. This overlaps a bit with 'makeTycEnv0', which also adds measures for
-- selectors and checkers, but only for datatypes mentioned in the type
-- signatures of functions defined in the current module.
-------------------------------------------------------------------------------------------
addOpaqueReflMeas :: Config -> Bare.TycEnv -> Bare.Env -> Ms.BareSpec -> Bare.MeasEnv -> Bare.ModSpecs ->
               [(Ghc.Var, LocSpecType, F.Equation)] ->
               Bare.Lookup Bare.MeasEnv
----------------------- --------------------------------------------------------------------
addOpaqueReflMeas :: Config
-> TycEnv
-> Env
-> Spec Symbol BareType
-> MeasEnv
-> HashMap ModName (Spec Symbol BareType)
-> [(TyVar, LocSpecType, Equation)]
-> Lookup MeasEnv
addOpaqueReflMeas Config
cfg TycEnv
tycEnv Env
env Spec Symbol BareType
spec MeasEnv
measEnv HashMap ModName (Spec Symbol BareType)
specs [(TyVar, LocSpecType, Equation)]
eqs = do
  dcs   <- ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> [[Located DataConP]]
forall a b. (a, b) -> b
snd (([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
 -> [[Located DataConP]])
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> Either [Error] [[Located DataConP]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env
-> ModName
-> Spec Symbol BareType
-> [DataDecl]
-> [(Located LHName, [Variance])]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
Bare.makeConTypes'' Env
env ModName
name Spec Symbol BareType
spec [DataDecl]
dataDecls []
  let datacons      = Bool
-> TCEmb TyCon -> TyConMap -> Located DataConP -> Located DataConP
Bare.makePluggedDataCon (Config -> Bool
typeclass Config
cfg) TCEmb TyCon
embs TyConMap
tyi (Located DataConP -> Located DataConP)
-> [Located DataConP] -> [Located DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Located DataConP]] -> [Located DataConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Located DataConP]]
dcs
  let dcSelectors   = (Located DataConP -> [Measure SpecType DataCon])
-> [Located DataConP] -> [Measure SpecType DataCon]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Config
-> DataConMap -> Located DataConP -> [Measure SpecType DataCon]
Bare.makeMeasureSelectors Config
cfg DataConMap
dm) [Located DataConP]
datacons
  -- Rest of the code is the same idea as for makeMeasEnv, only we just care on how to get
  -- `meSyms` (no class, data constructor or other stuff here).
  let measures = [MSpec SpecType DataCon] -> MSpec SpecType DataCon
forall a. Monoid a => [a] -> a
mconcat ([Measure SpecType DataCon] -> MSpec SpecType DataCon
forall ty. [Measure ty DataCon] -> MSpec ty DataCon
Ms.mkMSpec' [Measure SpecType DataCon]
dcSelectors MSpec SpecType DataCon
-> [MSpec SpecType DataCon] -> [MSpec SpecType DataCon]
forall a. a -> [a] -> [a]
: [MSpec SpecType DataCon]
measures0)
  let (cs, ms) = Bare.makeMeasureSpec'  (typeclass $ getConfig env)   measures
  let ms'      = [ (LHName -> Symbol
lhNameToResolvedSymbol (Located LHName -> LHName
forall a. Located a -> a
F.val Located LHName
lx), Located LHName
-> RRType (ReftV Symbol) -> Located (RRType (ReftV Symbol))
forall l b. Loc l => l -> b -> Located b
F.atLoc Located LHName
lx RRType (ReftV Symbol)
t) | (Located LHName
lx, RRType (ReftV Symbol)
t) <- [(Located LHName, RRType (ReftV Symbol))]
ms ]
  let cs'      = [ (TyVar
v, TyVar -> SpecType -> LocSpecType
forall {b}. NamedThing b => b -> SpecType -> LocSpecType
txRefs TyVar
v SpecType
t) | (TyVar
v, SpecType
t) <- Bool
-> TCEmb TyCon
-> [(TyVar, SpecType)]
-> [DataConP]
-> [(TyVar, SpecType)]
Bare.meetDataConSpec (Config -> Bool
typeclass (Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env)) TCEmb TyCon
embs [(TyVar, SpecType)]
cs (Located DataConP -> DataConP
forall a. Located a -> a
val (Located DataConP -> DataConP) -> [Located DataConP] -> [DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located DataConP]
datacons)]
  return $ measEnv <> mempty
    { Bare.meMeasureSpec = measures
    , Bare.meSyms        = ms'
    , Bare.meDataCons    = cs'
    , Bare.meOpaqueRefl  = opaqueRefl
    }
  where
    -- We compute things in the same way as in makeMeasEnv
    txRefs :: b -> SpecType -> LocSpecType
txRefs b
v SpecType
t    = TyConMap -> TCEmb TyCon -> LocSpecType -> LocSpecType
Bare.txRefSort TyConMap
tyi TCEmb TyCon
embs (SpecType
t SpecType -> Located b -> LocSpecType
forall a b. a -> Located b -> Located a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ b -> Located b
forall a. NamedThing a => a -> Located a
GM.locNamedThing b
v)
    ([MSpec SpecType DataCon]
measures0, [(TyVar, Measure (Located BareType) ctor)]
opaqueRefl) = Env
-> MeasEnv
-> HashMap ModName (Spec Symbol BareType)
-> [(TyVar, LocSpecType, Equation)]
-> ([MSpec SpecType DataCon],
    [(TyVar, Measure (Located BareType) ctor)])
forall ctor.
Env
-> MeasEnv
-> HashMap ModName (Spec Symbol BareType)
-> [(TyVar, LocSpecType, Equation)]
-> ([MSpec SpecType DataCon],
    [(TyVar, Measure (Located BareType) ctor)])
Bare.makeOpaqueReflMeasures Env
env MeasEnv
measEnv HashMap ModName (Spec Symbol BareType)
specs [(TyVar, LocSpecType, Equation)]
eqs
    -- Note: it is important to do toList after applying `dataConTyCon` because
    -- obviously several data constructors can refer to the same `TyCon` so we
    -- could have duplicates
    -- We skip the variables from the axiom equations that correspond to the actual functions
    -- of opaque reflections, since we never need to look at the unfoldings of those
    actualFns :: HashSet LHName
actualFns = [LHName] -> HashSet LHName
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([LHName] -> HashSet LHName) -> [LHName] -> HashSet LHName
forall a b. (a -> b) -> a -> b
$ Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> ((Located LHName, Located LHName) -> Located LHName)
-> (Located LHName, Located LHName)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName, Located LHName) -> Located LHName
forall a b. (a, b) -> a
fst ((Located LHName, Located LHName) -> LHName)
-> [(Located LHName, Located LHName)] -> [LHName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec Symbol BareType -> [(Located LHName, Located LHName)]
forall lname ty.
Spec lname ty -> [(Located LHName, Located LHName)]
Ms.asmReflectSigs Spec Symbol BareType
spec
    shouldBeUsedForScanning :: LHName -> Bool
shouldBeUsedForScanning LHName
sym = Bool -> Bool
not (LHName
sym LHName -> HashSet LHName -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet LHName
actualFns)
    varsUsedForTcScanning :: [TyVar]
varsUsedForTcScanning =
      [ TyVar
v
      | (TyVar
v, LocSpecType
_, Equation
_) <- [(TyVar, LocSpecType, Equation)]
eqs
      , LHName -> Bool
shouldBeUsedForScanning (LHName -> Bool) -> LHName -> Bool
forall a b. (a -> b) -> a -> b
$ Name -> Symbol -> LHName
makeGHCLHName (TyVar -> Name
forall a. NamedThing a => a -> Name
Ghc.getName TyVar
v) (TyVar -> Symbol
forall a. Symbolic a => a -> Symbol
symbol TyVar
v)
      ]
    tcs :: [TyCon]
tcs           = HashSet TyCon -> [TyCon]
forall a. HashSet a -> [a]
S.toList (HashSet TyCon -> [TyCon]) -> HashSet TyCon -> [TyCon]
forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
Ghc.dataConTyCon (DataCon -> TyCon) -> HashSet DataCon -> HashSet TyCon
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` MeasEnv -> [TyVar] -> HashSet DataCon
Bare.getReflDCs MeasEnv
measEnv [TyVar]
varsUsedForTcScanning
    dataDecls :: [DataDecl]
dataDecls     = Config -> Spec Symbol BareType -> [TyCon] -> [DataDecl]
Bare.makeHaskellDataDecls Config
cfg Spec Symbol BareType
spec [TyCon]
tcs
    tyi :: TyConMap
tyi           = TycEnv -> TyConMap
Bare.tcTyConMap    TycEnv
tycEnv
    embs :: TCEmb TyCon
embs          = TycEnv -> TCEmb TyCon
Bare.tcEmbs        TycEnv
tycEnv
    dm :: DataConMap
dm            = TycEnv -> DataConMap
Bare.tcDataConMap  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 Symbol BareType
-> Spec Symbol BareType
makeLiftedSpec ModName
name GhcSrc
src Env
env GhcSpecRefl
refl GhcSpecData
sData GhcSpecSig
sig GhcSpecQual
qual BareRTEnv
myRTE Spec Symbol BareType
lSpec0 = Spec Symbol BareType
lSpec0
  { Ms.asmSigs    = F.notracepp   ("makeLiftedSpec : ASSUMED-SIGS " ++ F.showpp name ) (xbs ++ myDCs)
  , Ms.sigs       = F.notracepp   ("makeLiftedSpec : LIFTED-SIGS " ++ F.showpp name ) $
                      mkSigs (gsTySigs sig)
  , Ms.invariants = [ (Bare.varLocSym <$> x, Bare.specToBare <$> t)
                       | (x, t) <- gsInvariants sData
                       , isLocInFile srcF t
                    ]
  , Ms.axeqs      = gsMyAxioms refl
  , Ms.aliases    = F.notracepp "MY-ALIASES" $ M.elems . typeAliases $ myRTE
  , Ms.ealiases   = M.elems . exprAliases $ myRTE
  , Ms.qualifiers = filter (isLocInFile srcF) (gsQualifiers qual)
  }
  where
    myDCs :: [(Located LHName, Located BareType)]
myDCs         = ((Located LHName, Located BareType) -> Bool)
-> [(Located LHName, Located BareType)]
-> [(Located LHName, Located BareType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (LHName -> Bool
isLocalName (LHName -> Bool)
-> ((Located LHName, Located BareType) -> LHName)
-> (Located LHName, Located BareType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> ((Located LHName, Located BareType) -> Located LHName)
-> (Located LHName, Located BareType)
-> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName, Located BareType) -> Located LHName
forall a b. (a, b) -> a
fst) ([(Located LHName, Located BareType)]
 -> [(Located LHName, Located BareType)])
-> [(Located LHName, Located BareType)]
-> [(Located LHName, Located BareType)]
forall a b. (a -> b) -> a -> b
$ [(TyVar, LocSpecType)] -> [(Located LHName, Located BareType)]
forall {f :: * -> *}.
Functor f =>
[(TyVar, f SpecType)] -> [(Located LHName, f BareType)]
mkSigs (GhcSpecData -> [(TyVar, LocSpecType)]
gsCtors GhcSpecData
sData)
    mkSigs :: [(TyVar, f SpecType)] -> [(Located LHName, f BareType)]
mkSigs [(TyVar, f SpecType)]
xts    = [ (TyVar, f SpecType) -> (Located LHName, f BareType)
forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (Located LHName, f BareType)
toBare (TyVar
x, f SpecType
t) | (TyVar
x, f SpecType
t) <- [(TyVar, f SpecType)]
xts
                    , Bool -> Bool
not (TyVar -> HashSet TyVar -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member TyVar
x HashSet TyVar
reflVars) Bool -> Bool -> Bool
&& TargetSrc -> TyVar -> Bool
isExportedVar (GhcSrc -> TargetSrc
toTargetSrc GhcSrc
src) TyVar
x
                    ]
    toBare :: (TyVar, f SpecType) -> (Located LHName, f BareType)
toBare (TyVar
x, f SpecType
t) = (TyVar -> Located LHName
makeGHCLHNameLocatedFromId TyVar
x, SpecType -> BareType
Bare.specToBare (SpecType -> BareType) -> f SpecType -> f BareType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f SpecType
t)
    xbs :: [(Located LHName, Located BareType)]
xbs           = (TyVar, LocSpecType) -> (Located LHName, Located BareType)
forall {f :: * -> *}.
Functor f =>
(TyVar, f SpecType) -> (Located LHName, f BareType)
toBare ((TyVar, LocSpecType) -> (Located LHName, Located BareType))
-> [(TyVar, LocSpecType)] -> [(Located LHName, Located BareType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
reflTySigs
    reflTySigs :: [(TyVar, LocSpecType)]
reflTySigs    = [(TyVar
x, LocSpecType
t) | (TyVar
x,LocSpecType
t,Equation
_) <- GhcSpecRefl -> [(TyVar, LocSpecType, Equation)]
gsHAxioms GhcSpecRefl
refl]
    reflVars :: HashSet TyVar
reflVars      = [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((TyVar, LocSpecType) -> TyVar
forall a b. (a, b) -> a
fst ((TyVar, LocSpecType) -> TyVar)
-> [(TyVar, LocSpecType)] -> [TyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyVar, LocSpecType)]
reflTySigs)
    -- myAliases fld = M.elems . fld $ myRTE
    srcF :: [Char]
srcF          = GhcSrc -> [Char]
_giTarget GhcSrc
src

    isLocalName :: LHName -> Bool
isLocalName = \case
      LHNResolved (LHRGHC Name
n) Symbol
_ ->
        GenModule Unit -> Maybe (GenModule Unit)
forall a. a -> Maybe a
Just (TcGblEnv -> GenModule Unit
Ghc.tcg_mod (Env -> TcGblEnv
Bare.reTcGblEnv Env
env)) Maybe (GenModule Unit) -> Maybe (GenModule Unit) -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Maybe (GenModule Unit)
Ghc.nameModule_maybe Name
n
      LHName
_ ->
        Bool
False

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

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

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

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


--------------------------------------------------------------------------------
-- | @myRTEnv@ slices out the part of RTEnv that was generated by aliases defined
--   in the _target_ file, "cooks" the aliases (by conversion to SpecType), and
--   then saves them back as BareType.
--------------------------------------------------------------------------------
myRTEnv :: GhcSrc -> Bare.Env -> Bare.SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv :: GhcSrc -> Env -> SigEnv -> BareRTEnv -> BareRTEnv
myRTEnv GhcSrc
src Env
env SigEnv
sigEnv BareRTEnv
rtEnv = [Located BareRTAlias]
-> [Located (RTAlias Symbol Expr)] -> BareRTEnv
forall x a.
[Located (RTAlias x a)]
-> [Located (RTAlias Symbol Expr)] -> RTEnv x a
mkRTE [Located BareRTAlias]
tAs' [Located (RTAlias Symbol Expr)]
eAs
  where
    tAs' :: [Located BareRTAlias]
tAs'                     = Env
-> SigEnv -> ModName -> Located BareRTAlias -> Located BareRTAlias
normalizeBareAlias Env
env SigEnv
sigEnv ModName
name (Located BareRTAlias -> Located BareRTAlias)
-> [Located BareRTAlias] -> [Located BareRTAlias]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located BareRTAlias]
tAs
    tAs :: [Located BareRTAlias]
tAs                      = (BareRTEnv -> HashMap Symbol (Located BareRTAlias))
-> [Located BareRTAlias]
forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap Symbol (Located BareRTAlias)
forall tv t. RTEnv tv t -> HashMap Symbol (Located (RTAlias tv t))
typeAliases
    eAs :: [Located (RTAlias Symbol Expr)]
eAs                      = (BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr)))
-> [Located (RTAlias Symbol Expr)]
forall {a} {k}. Loc a => (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap Symbol (Located (RTAlias Symbol Expr))
forall tv t.
RTEnv tv t -> HashMap Symbol (Located (RTAlias Symbol Expr))
exprAliases
    myAliases :: (BareRTEnv -> HashMap k a) -> [a]
myAliases BareRTEnv -> HashMap k a
fld            = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Char] -> a -> Bool
forall a. Loc a => [Char] -> a -> Bool
isLocInFile [Char]
srcF) ([a] -> [a]) -> (BareRTEnv -> [a]) -> BareRTEnv -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap k a -> [a]
forall k v. HashMap k v -> [v]
M.elems (HashMap k a -> [a])
-> (BareRTEnv -> HashMap k a) -> BareRTEnv -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BareRTEnv -> HashMap k a
fld (BareRTEnv -> [a]) -> BareRTEnv -> [a]
forall a b. (a -> b) -> a -> b
$ BareRTEnv
rtEnv
    srcF :: [Char]
srcF                     = GhcSrc -> [Char]
_giTarget    GhcSrc
src
    name :: ModName
name                     = GhcSrc -> ModName
_giTargetMod GhcSrc
src

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

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

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

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


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